elicitation 0.11.0

//! Verus companion generator — standalone V11/V12 leaf + composition pattern.
//!
//! Generates a self-contained Verus file (no imports from the VSM crate) with:
//!
//! 1. An abstract state enum — verbatim from `verus_state_body` annotation
//! 2. The invariant `open spec fn` — verbatim from `verus_inv_body` annotation
//! 3. Shared postcondition predicates (one per transition class)
//! 4. Leaf `proof fn` lemmas with empty bodies that Z3 discharges automatically
//! 5. A transition tag enum + composition dispatch proof
//!
//! This pattern is compatible with `elicitation_verus` (built with `vargo`,
//! excluded from the cargo workspace) because it imports nothing from the VSM
//! crate.

use std::path::Path;

use crate::cli::generate::scanner::VsmDescriptor;

// ─── Public API ───────────────────────────────────────────────────────────────

/// Generate the Verus standalone companion file content for `vsm`.
///
/// Returns `Err` with an actionable message when a named invariant is present
/// but `verus_inv_body` could not be resolved.
#[tracing::instrument(skip(vsm, _crate_root), fields(machine = %vsm.machine))]
pub fn generate_verus_file(
    vsm: &VsmDescriptor,
    _crate_root: impl AsRef<Path>,
) -> Result<String, String> {
    let machine = &vsm.machine;
    let state_ty = machine.replace("Machine", "State");
    let machine_prefix = to_snake(machine.trim_end_matches("Machine"));

    // Resolve invariant — error only when an invariant exists without a body.
    let inv_parts: Option<InvParts> = match &vsm.invariant {
        Some(p) => {
            let inv_fn = p.verus_fn.as_deref().unwrap_or(p.name.as_str()).to_string();
            let inv_body = p.verus_inv_body.as_deref().ok_or_else(|| {
                let hint_fn = p.verus_fn.as_deref().unwrap_or("verus_invariant_fn");
                format!(
                    "cannot generate Verus companion for {machine}: \
                     invariant body for `{hint_fn}` not found\n  \
                     hint: add `verus_inv_body = \"...\"` to #[prop(...)] on `{name}`",
                    name = p.name,
                )
            })?;
            Some(InvParts {
                inv_fn,
                inv_body: inv_body.to_string(),
                state_body: p.verus_state_body.clone(),
            })
        }
        None => None,
    };

    let mut out = String::new();

    // ── Header ───────────────────────────────────────────────────────────────
    out.push_str("// AUTO-GENERATED by `elicitation generate verus` — DO NOT EDIT\n");
    out.push_str("//\n");
    out.push_str(&format!(
        "// Standalone Verus proof for {machine} (V13 assume_specification pattern).\n"
    ));
    out.push_str("// Regenerate: elicitation generate verus --crate-path <root>\n");
    out.push_str("//\n");
    out.push_str("// No imports from the VSM crate — self-contained for vargo builds.\n");
    out.push_str("// Architecture:\n");
    out.push_str("//   V11/V12 leaf + composition proof grounded by V13 assume_specification.\n");
    out.push_str("//   Each stub is trusted axiomatically (requires/ensures mirrors the\n");
    out.push_str("//   formal_method contract); Kani and Creusot independently verify the\n");
    out.push_str("//   real transition bodies in elicit_server.\n");
    out.push('\n');
    out.push_str("use vstd::prelude::*;\n");
    out.push_str("use verus_builtin_macros::verus;\n");
    out.push('\n');

    if let Some(inv) = &inv_parts {
        let special_variants = inv
            .state_body
            .as_deref()
            .map(parse_special_variants)
            .unwrap_or_default();

        let classified: Vec<(String, TransKind)> = vsm
            .transitions
            .iter()
            .map(|name| {
                let tf = vsm.transition_fns.iter().find(|tf| &tf.name == name);
                let kind = if let Some(class) = tf.and_then(|tf| tf.verus_class.as_deref()) {
                    TransKind::from_class_str_with_fallback(class, &special_variants)
                        .unwrap_or_else(|| {
                            let body = tf.and_then(|tf| tf.body.as_deref()).unwrap_or("");
                            classify_transition(body, &state_ty, &special_variants)
                        })
                } else {
                    let body = tf.and_then(|tf| tf.body.as_deref()).unwrap_or("");
                    classify_transition(body, &state_ty, &special_variants)
                };
                (name.clone(), kind)
            })
            .collect();

        let has_special = !special_variants.is_empty();
        let needs_passthrough = classified
            .iter()
            .any(|(_, k)| matches!(k, TransKind::Passthrough | TransKind::ConditionalSpecial(_)));
        let needs_special_false = classified
            .iter()
            .any(|(_, k)| matches!(k, TransKind::SpecialFalse(_)));
        let needs_conditional = classified
            .iter()
            .any(|(_, k)| matches!(k, TransKind::ConditionalSpecial(_)));
        let needs_pre = classified.iter().any(|(_, k)| k.needs_pre());

        // ── External stubs (outside verus! block) ────────────────────────────
        // Each stub represents the corresponding real transition in elicit_server.
        // Verus sees only the axiomatized spec; the body is unreachable (todo!()).
        // Note: these must be declared before the verus! block but they can
        // reference state_ty because Rust resolves items at module scope.
        out.push_str(
            "// ─── External transition stubs ─────────────────────────────────────────────────\n",
        );
        out.push_str("// These functions represent the real transitions in elicit_server.\n");
        out.push_str("// Verus does not verify their bodies; assume_specification below injects\n");
        out.push_str(
            "// the trusted contracts.  Kani/Creusot independently verify the real bodies.\n\n",
        );
        for (name, _kind) in &classified {
            out.push_str(&format!(
                "/// Stub for `{name}` — body is opaque to Verus.\n"
            ));
            out.push_str("#[verifier::external]\n");
            out.push_str(&format!(
                "pub fn {name}_stub(state: {state_ty}) -> {state_ty} {{ todo!() }}\n\n"
            ));
        }

        out.push_str("verus! {\n\n");

        // ── Abstract state enum ───────────────────────────────────────────────
        out.push_str(&format!(
            "/// Abstract mirror of `{state_ty}` (invariant-relevant variants only).\n"
        ));
        out.push_str("#[allow(unused_imports)]\nuse vstd::prelude::SpecOrd;\n\n");
        // Derive `Copy` only when all struct-variant field types are known to be Copy.
        // `String`, `Vec`, etc. are not Copy, so we check the state body.
        let is_copy = inv.state_body.as_deref().is_none_or(state_body_is_all_copy);
        let derives = if is_copy {
            "#[derive(Debug, Clone, Copy, PartialEq, Eq)]"
        } else {
            "#[derive(Debug, Clone, PartialEq, Eq)]"
        };
        out.push_str(derives);
        out.push('\n');
        out.push_str(&format!("pub enum {state_ty} {{\n"));
        if let Some(sb) = &inv.state_body {
            for segment in split_state_body(sb) {
                out.push_str(&format!("    {segment},\n"));
            }
        } else if inv.inv_body.trim() == "true" {
            // Trivial invariant: no state variants needed. `_Unspecified` is the correct
            // and complete representation — no annotation required from the user.
            out.push_str("    _Unspecified,\n");
        } else {
            // Non-trivial invariant but no state body: we cannot generate a sound file.
            // Fail fast rather than emitting a broken or incomplete proof.
            return Err(format!(
                "cannot generate Verus companion for {machine}: \
                 `verus_inv_body` references state variants but `verus_state_body` is missing\n  \
                 hint: add `verus_state_body = \"Variant1 {{ field: Type }}, _Other,\"` \
                 to #[prop(...)] to declare the abstract state enum"
            ));
        }
        out.push_str("}\n\n");

        // ── Invariant spec fn ─────────────────────────────────────────────────
        out.push_str(&format!("/// Invariant for `{machine}`.\n"));
        if inv.state_body.is_some() {
            out.push_str(&format!(
                "pub open spec fn {inv_fn}(state: &{state_ty}) -> bool {{ {inv_body} }}\n\n",
                inv_fn = inv.inv_fn,
                inv_body = inv.inv_body,
            ));
        } else {
            // Trivial invariant (`true`) — emit it cleanly, no state body needed.
            out.push_str(&format!(
                "pub open spec fn {inv_fn}(state: &{state_ty}) -> bool {{ true }}\n\n",
                inv_fn = inv.inv_fn,
            ));
        }

        // ── Postcondition predicates ──────────────────────────────────────────
        out.push_str(
            "// ─── Postcondition predicates ──────────────────────────────────────────────────\n\n",
        );

        let trivial_pred = if has_special {
            let not_special: String = special_variants
                .iter()
                .filter(|v| !v.starts_with('_'))
                .map(|v| {
                    if inv
                        .state_body
                        .as_deref()
                        .is_some_and(|sb| sb.contains(&format!("{v} {{")))
                    {
                        format!("!(post matches {state_ty}::{v} {{ .. }})")
                    } else {
                        format!("post != {state_ty}::{v}")
                    }
                })
                .collect::<Vec<_>>()
                .join(" && ");
            if not_special.is_empty() {
                "true".to_string()
            } else {
                not_special
            }
        } else {
            "true".to_string()
        };

        out.push_str(&format!(
            "/// Any non-special post-state — the `_ => true` arm of the invariant applies.\n\
             pub open spec fn {machine_prefix}_post_trivial(post: {state_ty}) -> bool {{ {trivial_pred} }}\n\n"
        ));

        if needs_passthrough {
            out.push_str(&format!(
                "/// Passthrough: post-state equals pre-state.\n\
                 pub open spec fn {machine_prefix}_post_passthrough(pre: {state_ty}, post: {state_ty}) -> bool {{ post == pre }}\n\n"
            ));
        }

        for variant in special_variants.iter().filter(|v| !v.starts_with('_')) {
            let v_lower = to_snake(variant);
            let has_fields = inv
                .state_body
                .as_deref()
                .is_some_and(|sb| sb.contains(&format!("{variant} {{")));

            if needs_special_false {
                out.push_str(&format!(
                    "/// `{variant}` post with non-violating field (invariant vacuously satisfied).\n"
                ));
                if has_fields {
                    if let Some((pattern, rhs)) = extract_inv_arm(&inv.inv_body, &state_ty, variant)
                    {
                        out.push_str(&format!(
                            "pub open spec fn {machine_prefix}_post_{v_lower}_false(post: {state_ty}) -> bool {{\n\
                             \x20\x20\x20\x20match post {{\n\
                             \x20\x20\x20\x20\x20\x20\x20\x20{pattern} => {rhs},\n\
                             \x20\x20\x20\x20\x20\x20\x20\x20_ => false,\n\
                             \x20\x20\x20\x20}}\n\
                             }}\n\n"
                        ));
                    } else {
                        // No explicit invariant arm — any value of this variant satisfies the invariant.
                        out.push_str(&format!(
                            "pub open spec fn {machine_prefix}_post_{v_lower}_false(post: {state_ty}) -> bool \
                             {{ post matches {state_ty}::{variant} {{ .. }} }}\n\n"
                        ));
                    }
                } else {
                    out.push_str(&format!(
                        "pub open spec fn {machine_prefix}_post_{v_lower}_false(post: {state_ty}) -> bool \
                         {{ post == {state_ty}::{variant} }}\n\n"
                    ));
                }
            }

            if needs_conditional {
                out.push_str(&format!(
                    "/// Conditional: `{variant}` with non-violating field, or unchanged passthrough.\n"
                ));
                out.push_str(&format!(
                    "pub open spec fn {machine_prefix}_post_conditional_{v_lower}(pre: {state_ty}, post: {state_ty}) -> bool {{\n"
                ));
                if has_fields {
                    out.push_str("    match pre {\n");
                    if let Some((pattern, rhs)) = extract_inv_arm(&inv.inv_body, &state_ty, variant)
                    {
                        out.push_str(&format!(
                            "        {state_ty}::{variant} {{ .. }} => match post {{\n\
                             \x20\x20\x20\x20\x20\x20\x20\x20\x20\x20\x20\x20{pattern} => {rhs},\n\
                             \x20\x20\x20\x20\x20\x20\x20\x20\x20\x20\x20\x20_ => false,\n\
                             \x20\x20\x20\x20\x20\x20\x20\x20}},\n"
                        ));
                    } else {
                        // No explicit invariant arm — any value of this variant satisfies the invariant.
                        out.push_str(&format!(
                            "        {state_ty}::{variant} {{ .. }} => post matches {state_ty}::{variant} {{ .. }},\n"
                        ));
                    }
                    out.push_str("        _ => post == pre,\n    }\n");
                } else {
                    out.push_str(&format!(
                        "    if pre == {state_ty}::{variant} {{ post == {state_ty}::{variant} }} else {{ post == pre }}\n"
                    ));
                }
                out.push_str("}\n\n");
            }
        }

        // ── Leaf lemmas ───────────────────────────────────────────────────────
        out.push_str(
            "// ─── Leaf lemmas ────────────────────────────────────────────────────────────────\n\n",
        );

        out.push_str(&format!(
            "/// Trivial post satisfies the invariant (`_ => true` arm applies).\n\
             pub proof fn {machine_prefix}_leaf_trivial(post: {state_ty})\n    \
             requires {machine_prefix}_post_trivial(post),\n    \
             ensures  {inv_fn}(&post),\n\
             {{}}\n\n",
            inv_fn = inv.inv_fn
        ));

        if needs_passthrough {
            out.push_str(&format!(
                "/// Passthrough preserves the invariant by induction.\n\
                 pub proof fn {machine_prefix}_leaf_passthrough(pre: {state_ty}, post: {state_ty})\n    \
                 requires\n        \
                 {inv_fn}(&pre),\n        \
                 {machine_prefix}_post_passthrough(pre, post),\n    \
                 ensures {inv_fn}(&post),\n\
                 {{}}\n\n",
                inv_fn = inv.inv_fn
            ));
        }

        for variant in special_variants.iter().filter(|v| !v.starts_with('_')) {
            let v_lower = to_snake(variant);

            if needs_special_false {
                out.push_str(&format!(
                    "/// `{variant}` with non-violating field — invariant is vacuously satisfied.\n\
                     pub proof fn {machine_prefix}_leaf_{v_lower}_false(post: {state_ty})\n    \
                     requires {machine_prefix}_post_{v_lower}_false(post),\n    \
                     ensures  {inv_fn}(&post),\n\
                     {{}}\n\n",
                    inv_fn = inv.inv_fn
                ));
            }

            if needs_conditional {
                out.push_str(&format!(
                    "/// Conditional `{variant}` — non-violating or passthrough — satisfies the invariant.\n\
                     pub proof fn {machine_prefix}_leaf_conditional_{v_lower}(pre: {state_ty}, post: {state_ty})\n    \
                     requires\n        \
                     {inv_fn}(&pre),\n        \
                     {machine_prefix}_post_conditional_{v_lower}(pre, post),\n    \
                     ensures {inv_fn}(&post),\n\
                     {{}}\n\n",
                    inv_fn = inv.inv_fn
                ));
            }
        }

        // ── Assume specifications + verified callers ─────────────────────────
        out.push_str(
            "// ─── Assume specifications (V13 trust anchors) ──────────────────────────────────\n\n",
        );
        out.push_str("// Each assume_specification axiomatizes the contract for its stub.\n");
        out.push_str(
            "// The postcondition predicate is the same one used by the leaf lemma above,\n",
        );
        out.push_str("// ensuring Verus proof and assume_specification are tightly aligned.\n\n");
        for (name, kind) in &classified {
            let post_pred = kind.assume_spec_ensures(&machine_prefix);
            let pre_needed = kind.needs_pre();
            out.push_str(&format!(
                "/// Contract for `{name}_stub` — mirrors the formal_method contract that\n\
                 /// Kani and Creusot independently verify on the real `{name}` body.\n"
            ));
            if pre_needed {
                out.push_str(&format!(
                    "pub assume_specification[{name}_stub](state: {state_ty}) -> (r: {state_ty})\n    \
                     requires {inv_fn}(&state),\n    \
                     ensures  {post_pred};\n\n",
                    inv_fn = inv.inv_fn,
                ));
            } else {
                out.push_str(&format!(
                    "pub assume_specification[{name}_stub](state: {state_ty}) -> (r: {state_ty})\n    \
                     requires {inv_fn}(&state),\n    \
                     ensures  {post_pred};\n\n",
                    inv_fn = inv.inv_fn,
                ));
            }
        }

        out.push_str(
            "// ─── Verified exec callers ───────────────────────────────────────────────────────\n\n",
        );
        out.push_str("// These exec fns close the proof loop: calling any stub on a consistent\n");
        out.push_str(
            "// pre-state yields a consistent post-state, by the assume_specification.\n\n",
        );
        for (name, _kind) in &classified {
            out.push_str(&format!(
                "/// Proof that `{name}` preserves the invariant (via assume_specification).\n\
                 pub fn {name}_verified(state: {state_ty}) -> (r: {state_ty})\n    \
                 requires {inv_fn}(&state),\n    \
                 ensures  {inv_fn}(&r),\n\
                 {{\n    \
                 {name}_stub(state)\n\
                 }}\n\n",
                inv_fn = inv.inv_fn,
            ));
        }

        // ── Transition tag enum ───────────────────────────────────────────────
        out.push_str(
            "// ─── Transition tags + composition ──────────────────────────────────────────────\n\n",
        );

        out.push_str(&format!(
            "/// One tag per `{machine}` transition — dispatch without re-verifying bodies.\n"
        ));
        out.push_str("#[derive(Debug, Clone, Copy, PartialEq, Eq)]\n");
        out.push_str(&format!("pub enum {machine}Trans {{\n"));
        for name in &vsm.transitions {
            out.push_str(&format!("    {},\n", to_pascal(name)));
        }
        out.push_str("}\n\n");

        // ── Dispatch spec fn ─────────────────────────────────────────────────
        let trans_ty = format!("{machine}Trans");
        out.push_str("/// Maps each transition tag to its postcondition predicate.\n");
        if needs_pre {
            out.push_str(&format!(
                "pub open spec fn {machine_prefix}_post(pre: {state_ty}, post: {state_ty}, tag: {trans_ty}) -> bool {{\n"
            ));
        } else {
            out.push_str(&format!(
                "pub open spec fn {machine_prefix}_post(post: {state_ty}, tag: {trans_ty}) -> bool {{\n"
            ));
        }
        out.push_str("    match tag {\n");
        for (name, kind) in &classified {
            let tag = to_pascal(name);
            let pred = kind.post_pred(&machine_prefix, &state_ty);
            out.push_str(&format!("        {trans_ty}::{tag} => {pred},\n"));
        }
        out.push_str("    }\n}\n\n");

        // ── Composition proof ─────────────────────────────────────────────────
        out.push_str(
            "/// Composition: any post-state produced by a tagged transition satisfies the invariant.\n",
        );
        if needs_pre {
            out.push_str(&format!(
                "pub proof fn {machine_prefix}_composition(pre: {state_ty}, post: {state_ty}, tag: {trans_ty})\n"
            ));
        } else {
            out.push_str(&format!(
                "pub proof fn {machine_prefix}_composition(post: {state_ty}, tag: {trans_ty})\n"
            ));
        }
        out.push_str("    requires\n");
        if needs_pre {
            out.push_str(&format!("        {}(&pre),\n", inv.inv_fn));
            out.push_str(&format!("        {machine_prefix}_post(pre, post, tag),\n"));
        } else {
            out.push_str(&format!("        {machine_prefix}_post(post, tag),\n"));
        }
        out.push_str(&format!("    ensures {}(&post),\n", inv.inv_fn));
        out.push_str("{\n    match tag {\n");
        for (name, kind) in &classified {
            let tag = to_pascal(name);
            let call = kind.leaf_call(&machine_prefix);
            out.push_str(&format!("        {trans_ty}::{tag} => {call},\n"));
        }
        out.push_str("    }\n}\n\n");

        out.push_str("} // verus!\n");
    }

    Ok(out)
}

// ─── Internal types ───────────────────────────────────────────────────────────

struct InvParts {
    inv_fn: String,
    inv_body: String,
    state_body: Option<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
enum TransKind {
    /// No special variant in body — `_ => true` arm of the invariant applies.
    Trivial,
    /// Has a wildcard arm (`other => other`) but no special variant.
    Passthrough,
    /// Returns a specific named variant with a non-violating field (no passthrough arm).
    SpecialFalse(String),
    /// Returns a specific named variant OR passes through unchanged.
    ConditionalSpecial(String),
}

impl TransKind {
    /// Map a `verus_class = "..."` string to a `TransKind`, returning `None` for unknown values.
    /// For `SpecialFalse`/`ConditionalSpecial` without a named variant, falls back to first special.
    fn from_class_str_with_fallback(s: &str, special_variants: &[String]) -> Option<Self> {
        let first = special_variants
            .iter()
            .find(|v| !v.starts_with('_'))
            .cloned()
            .unwrap_or_else(|| "unknown".to_string());
        match s {
            "trivial" => Some(TransKind::Trivial),
            "passthrough" => Some(TransKind::Passthrough),
            "special_false" => Some(TransKind::SpecialFalse(first)),
            "conditional_special" => Some(TransKind::ConditionalSpecial(first)),
            _ => None,
        }
    }

    fn needs_pre(&self) -> bool {
        matches!(
            self,
            TransKind::Passthrough | TransKind::ConditionalSpecial(_)
        )
    }

    fn post_pred(&self, prefix: &str, _state_ty: &str) -> String {
        match self {
            TransKind::Trivial => format!("{prefix}_post_trivial(post)"),
            TransKind::Passthrough => format!("{prefix}_post_passthrough(pre, post)"),
            TransKind::SpecialFalse(v) => {
                let v_lower = to_snake(v);
                format!("{prefix}_post_{v_lower}_false(post)")
            }
            TransKind::ConditionalSpecial(v) => {
                let v_lower = to_snake(v);
                format!("{prefix}_post_conditional_{v_lower}(pre, post)")
            }
        }
    }

    fn leaf_call(&self, prefix: &str) -> String {
        match self {
            TransKind::Trivial => format!("{prefix}_leaf_trivial(post)"),
            TransKind::Passthrough => format!("{prefix}_leaf_passthrough(pre, post)"),
            TransKind::SpecialFalse(v) => {
                let v_lower = to_snake(v);
                format!("{prefix}_leaf_{v_lower}_false(post)")
            }
            TransKind::ConditionalSpecial(v) => {
                let v_lower = to_snake(v);
                format!("{prefix}_leaf_conditional_{v_lower}(pre, post)")
            }
        }
    }

    /// Generates the `ensures` clause for an `assume_specification` block.
    ///
    /// Uses `state` (parameter name) and `r` (return binder name) rather than
    /// the `pre`/`post` names used by the dispatch spec fn and composition proof.
    fn assume_spec_ensures(&self, prefix: &str) -> String {
        match self {
            TransKind::Trivial => format!("{prefix}_post_trivial(r)"),
            TransKind::Passthrough => format!("{prefix}_post_passthrough(state, r)"),
            TransKind::SpecialFalse(v) => {
                let v_lower = to_snake(v);
                format!("{prefix}_post_{v_lower}_false(r)")
            }
            TransKind::ConditionalSpecial(v) => {
                let v_lower = to_snake(v);
                format!("{prefix}_post_conditional_{v_lower}(state, r)")
            }
        }
    }
}

// ─── Classification helpers ───────────────────────────────────────────────────

/// Split a `verus_state_body` string by top-level commas (not inside `{}`), returning trimmed segments.
///
/// This preserves struct-like variants: `"SqlEditor { running: bool, result: Option<u64> }, _Other"`
/// splits into `["SqlEditor { running: bool, result: Option<u64> }", "_Other"]`.
fn split_state_body(state_body: &str) -> Vec<String> {
    let mut segments: Vec<String> = Vec::new();
    let mut depth: i32 = 0;
    let mut current = String::new();

    for ch in state_body.chars() {
        match ch {
            '{' => {
                depth += 1;
                current.push(ch);
            }
            '}' => {
                depth -= 1;
                current.push(ch);
            }
            ',' if depth == 0 => {
                let trimmed = current.trim().to_string();
                if !trimmed.is_empty() {
                    segments.push(trimmed);
                }
                current.clear();
            }
            _ => current.push(ch),
        }
    }
    let trimmed = current.trim().to_string();
    if !trimmed.is_empty() {
        segments.push(trimmed);
    }
    segments
}

/// Extract named (non-`_`-prefixed) and wildcard variants from a `verus_state_body` string.
///
/// Handles nested braces so `SqlEditor { running: bool, result: Option<u64> }` is one variant.
fn parse_special_variants(state_body: &str) -> Vec<String> {
    let mut variants: Vec<String> = Vec::new();
    let mut depth: i32 = 0;
    let mut current = String::new();

    for ch in state_body.chars() {
        match ch {
            '{' => {
                depth += 1;
                current.push(ch);
            }
            '}' => {
                depth -= 1;
                current.push(ch);
            }
            ',' if depth == 0 => {
                if let Some(v) = first_ident(&current) {
                    variants.push(v);
                }
                current.clear();
            }
            _ => current.push(ch),
        }
    }
    if let Some(v) = first_ident(&current) {
        if !v.is_empty() {
            variants.push(v);
        }
    }
    variants
}

fn first_ident(s: &str) -> Option<String> {
    let s = s.trim();
    let ident: String = s
        .chars()
        .take_while(|c| c.is_alphanumeric() || *c == '_')
        .collect();
    if ident.is_empty() { None } else { Some(ident) }
}

/// Extract the explicit match arm for `variant` from a `verus_inv_body` match expression.
///
/// Given e.g. `"match *state { ArchiveNavState::NavFiltered { filter, .. } => filter@.len() > 0, _ => true, }"`,
/// `state_ty = "ArchiveNavState"`, and `variant = "NavFiltered"`, returns:
/// `Some(("ArchiveNavState::NavFiltered { filter, .. }", "filter@.len() > 0"))`.
///
/// Returns `None` if the variant has no explicit arm in the body (it falls through to a `_` arm,
/// meaning the invariant is trivially satisfied — any value of that variant is valid).
fn extract_inv_arm(inv_body: &str, state_ty: &str, variant: &str) -> Option<(String, String)> {
    let qualified = format!("{state_ty}::{variant}");
    let start = inv_body.find(&qualified)?;
    let from_start = &inv_body[start..];

    // Scan from the variant name to find "=>" at brace depth 0, skipping over
    // any `{ field_name, .. }` struct pattern.
    let bytes = from_start.as_bytes();
    let mut depth: i32 = 0;
    let mut arrow_end: Option<usize> = None;
    let mut i = 0;
    while i < bytes.len() {
        match bytes[i] {
            b'{' => depth += 1,
            b'}' => depth -= 1,
            b'=' if depth == 0 && i + 1 < bytes.len() && bytes[i + 1] == b'>' => {
                arrow_end = Some(i + 2);
                break;
            }
            _ => {}
        }
        i += 1;
    }
    let arrow_end = arrow_end?;

    // Pattern is everything from the variant name up to (not including) "=>", trimmed.
    let pattern = from_start[..arrow_end - 2].trim().to_string();

    // RHS expression is after "=>", up to the next top-level "," or closing "}".
    let rhs_str = from_start[arrow_end..].trim_start();
    let bytes = rhs_str.as_bytes();
    let mut depth: i32 = 0;
    let mut rhs_end = rhs_str.len();
    let mut i = 0;
    while i < bytes.len() {
        match bytes[i] {
            b'{' | b'(' | b'[' => depth += 1,
            b'}' | b')' | b']' => {
                if depth == 0 {
                    rhs_end = i;
                    break;
                }
                depth -= 1;
            }
            b',' if depth == 0 => {
                rhs_end = i;
                break;
            }
            _ => {}
        }
        i += 1;
    }
    let rhs = rhs_str[..rhs_end].trim().to_string();

    // A bare "_" or "true" RHS means the invariant is trivially satisfied — treat as no explicit arm.
    if rhs.is_empty() || rhs == "_" || rhs == "true" {
        None
    } else {
        Some((pattern, rhs))
    }
}

/// Classify a transition by inspecting its tokenised body string.
///
/// The body comes from `quote::ToTokens` so `::` becomes ` :: ` (with spaces).
/// Detects the SPECIFIC named variant the transition returns (not just whether any special
/// variant appears), so each transition maps to its own postcondition predicate.
fn classify_transition(body: &str, state_ty: &str, special_variants: &[String]) -> TransKind {
    let has_passthrough = body.contains("other =>") || body.contains("_ =>");

    // Find the SPECIFIC named variant this transition constructs.
    let specific_variant = special_variants
        .iter()
        .filter(|v| !v.starts_with('_'))
        .find(|v| {
            body.contains(&format!("{state_ty} :: {v}"))
                || body.contains(&format!("{state_ty}::{v}"))
        })
        .cloned();

    match (specific_variant, has_passthrough) {
        (Some(v), true) => TransKind::ConditionalSpecial(v),
        (Some(v), false) => TransKind::SpecialFalse(v),
        (None, true) => TransKind::Passthrough,
        (None, false) => TransKind::Trivial,
    }
}

// ─── String helpers ───────────────────────────────────────────────────────────

/// Returns `true` if all struct-variant field types in `state_body` are known `Copy` types.
///
/// Used to decide whether to include `Copy` in the state enum `#[derive(...)]`.
/// Types like `String`, `Vec`, `Box`, `Rc`, and `Arc` are not `Copy`, so if any appear
/// in the state body the enum must not derive `Copy`.
fn state_body_is_all_copy(state_body: &str) -> bool {
    const NON_COPY_MARKERS: &[&str] = &["String", "Vec<", "Box<", "Rc<", "Arc<"];
    !NON_COPY_MARKERS.iter().any(|t| state_body.contains(t))
}

/// Convert `PascalCase` → `snake_case`.
fn to_snake(s: &str) -> String {
    let mut out = String::new();
    for (i, ch) in s.chars().enumerate() {
        if ch.is_uppercase() && i > 0 {
            out.push('_');
        }
        out.push(ch.to_ascii_lowercase());
    }
    out
}

/// Convert `snake_case` → `PascalCase`.
fn to_pascal(s: &str) -> String {
    s.split('_')
        .map(|seg| {
            let mut c = seg.chars();
            match c.next() {
                None => String::new(),
                Some(f) => f.to_uppercase().collect::<String>() + c.as_str(),
            }
        })
        .collect()
}