aver-lang 0.26.0

//! Lean prelude text constants and demand-driven prelude assembly
//! (lakefile / toolchain project scaffolding included).

const LEAN_PRELUDE_HEADER: &str = r#"-- Generated by the Aver → Lean 4 transpiler
-- Pure core logic plus Oracle-lifted classified effects

set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.deprecated false
set_option maxRecDepth 1000000

-- Prelude: helper definitions for Aver builtins"#;

const LEAN_PRELUDE_FLOAT_COE: &str = r#"instance : Coe Int Float := ⟨fun n => Float.ofInt n⟩

def Float.fromInt (n : Int) : Float := Float.ofInt n

-- Aver's Float-to-Int operations match the runtime semantics
-- (`f64::floor() as i64` in VM, Rust codegen, WASM — all three use the
-- same IEEE 754 floor/round/ceil followed by Rust's saturating
-- `f64 as i64` cast):
--   * finite values within [i64::MIN, i64::MAX]: truncate toward zero
--   * finite > i64::MAX:              saturate to i64::MAX
--   * finite < i64::MIN:              saturate to i64::MIN
--   * +Inf:                           saturate to i64::MAX
--   * -Inf:                           saturate to i64::MIN
--   * NaN:                            0 (Rust 1.45+ defined behavior)
--
-- Lean's `Float.floor : Float → Float` doesn't directly satisfy Aver's
-- `Float.floor : Float → Int`, so we synthesize via the saturating
-- `Float.toUInt64` (returns 0 for NaN/negative) with sign handling and
-- explicit bounds. Per-case correctness is asserted by `native_decide`
-- examples below; total semantic agreement with `f64 as i64` would
-- need a formal IEEE spec in Lean, which is out of scope.
--
-- Asymmetry with the Dafny backend: Lean has IEEE 754 `Float` natively
-- (`double` at runtime), so we use it. Dafny only offers mathematical
-- `real` (Cauchy-style, no NaN/Inf/overflow), which is a fundamental
-- type mismatch with Aver's IEEE Float — Dafny operations stay opaque
-- (`function FloatPi(): real` etc.) rather than synthesizing IEEE on
-- top of `bv64`, which would mean implementing the entire IEEE
-- arithmetic in Dafny by hand.
namespace AverFloat
def toInt (x : Float) : Int :=
  if x.isNaN then 0
  -- 2^63 is exactly representable in f64; values ≥ that saturate up.
  else if x ≥ 9223372036854775808.0 then 9223372036854775807
  -- -2^63 is exactly representable; values strictly below saturate down.
  else if x < -9223372036854775808.0 then -9223372036854775808
  else if x ≥ 0.0 then Int.ofNat x.toUInt64.toNat
  else -(Int.ofNat (-x).toUInt64.toNat)

def floor (x : Float) : Int := toInt x.floor
def ceil  (x : Float) : Int := toInt x.ceil
def round (x : Float) : Int := toInt x.round

def pow (x y : Float) : Float := x ^ y

-- Edge-case smoke checks: each `example` is discharged by reduction,
-- so any drift from these documented values fails Lake build.
example : AverFloat.toInt 0.0 = 0                                := by native_decide
example : AverFloat.toInt 3.7 = 3                                := by native_decide
example : AverFloat.toInt (-3.7) = -3                            := by native_decide
example : AverFloat.toInt (1.0 / 0.0) = 9223372036854775807      := by native_decide
example : AverFloat.toInt (-1.0 / 0.0) = -9223372036854775808    := by native_decide
example : AverFloat.toInt (0.0 / 0.0) = 0                        := by native_decide
example : AverFloat.floor 3.7 = 3                                := by native_decide
example : AverFloat.floor (-3.7) = -4                            := by native_decide
example : AverFloat.ceil  3.2 = 4                                := by native_decide
example : AverFloat.ceil  (-3.2) = -3                            := by native_decide
-- Rounding mode (half-away-from-zero, matching Rust's `f64::round`):
example : AverFloat.round 0.5 = 1                                := by native_decide
example : AverFloat.round (-0.5) = -1                            := by native_decide
example : AverFloat.round 2.5 = 3                                := by native_decide
example : AverFloat.round (-2.5) = -3                            := by native_decide
end AverFloat"#;

// `DecidableEq Float` via an `unsafeCast`-fabricated proof delegating to
// runtime IEEE `==` (BEq). This is INTENTIONAL, not a soundness hole:
// Aver's Float IS the machine f64, and `aver verify` checks the VM's
// IEEE-754 runtime semantics — so Float equality in a proof means IEEE
// `==`, exactly what the shim reflects. Consequence to keep in mind: it
// follows IEEE, so `0.0 = -0.0` holds and `NaN = NaN` does not — proofs
// are about float behavior, NOT real-number / propositional equality.
// The shim faithfully mirrors `==` (it does not fabricate arbitrary
// truths: an IEEE-false goal like `0.1 + 0.2 = 0.3` still fails
// `native_decide`). Lean ships no `DecidableEq Float`, hence the
// `@[implemented_by]` bridge.
const LEAN_PRELUDE_FLOAT_DEC_EQ: &str = r#"private unsafe def Float.unsafeDecEq (a b : Float) : Decidable (a = b) :=
  if a == b then isTrue (unsafeCast ()) else isFalse (unsafeCast ())
@[implemented_by Float.unsafeDecEq]
private opaque Float.compDecEq (a b : Float) : Decidable (a = b)
instance : DecidableEq Float := Float.compDecEq"#;

const LEAN_PRELUDE_EXCEPT_DEC_EQ: &str = r#"instance [DecidableEq ε] [DecidableEq α] : DecidableEq (Except ε α)
  | .ok a, .ok b =>
    if h : a = b then isTrue (h ▸ rfl) else isFalse (by intro h'; cases h'; exact h rfl)
  | .error a, .error b =>
    if h : a = b then isTrue (h ▸ rfl) else isFalse (by intro h'; cases h'; exact h rfl)
  | .ok _, .error _ => isFalse (by intro h; cases h)
  | .error _, .ok _ => isFalse (by intro h; cases h)"#;

const LEAN_PRELUDE_EXCEPT_NS: &str = r#"namespace Except
def withDefault (r : Except ε α) (d : α) : α :=
  match r with
  | .ok v => v
  | .error _ => d
end Except"#;

const LEAN_PRELUDE_OPTION_TO_EXCEPT: &str = r#"def Option.toExcept (o : Option α) (e : ε) : Except ε α :=
  match o with
  | some v => .ok v
  | none => .error e"#;

const LEAN_PRELUDE_STRING_HADD: &str = r#"instance : HAdd String String String := ⟨String.append⟩"#;

// ---- String prelude spec lemmas -------------------------------------
//
// Demand-driven (mirrors the AverMap lemma family): each lemma ships
// only when the emitted body mentions its name — which happens exactly
// when the `SimpOverPreludeLemmas` law rung cites it. None carries
// `@[simp]`: the rung references them explicitly in its `simp [...]`
// set, and a global simp attribute would silently change simp behavior
// for every other proof in the corpus (the archived hand-proofs that
// motivated these lemmas close with the explicit spelling too).

/// `s + t = s ++ t` — normalizes the custom `HAdd String` instance
/// (above) so `++`-keyed lemmas (`String.slice_append_prefix`, core
/// `List.append` simp set) fire on goals spelled with `+`. Ships in
/// the `StringHadd` helper section because it is a statement *about*
/// that instance and needs nothing else in scope.
const LEAN_PRELUDE_STRING_ADD_EQ_APPEND: &str = r#"/-- The custom `HAdd String` instance is definitionally `++`. -/
theorem String.add_eq_append (s t : String) : s + t = s ++ t := rfl"#;

/// `String.slice s 0 s.length = s` — full-range slice identity.
/// Depends on the `String.slice` def in the `StringHelpers` section.
const LEAN_PRELUDE_STRING_SLICE_FULL: &str = r#"/-- Full-string slice identity: slicing [0, s.length) is the identity. -/
theorem String.slice_full (s : String) : String.sliceAv s 0 (s.length : Int) = s := by
  have h0 : ¬ ((0 : Int) < 0) := by omega
  have h1 : ¬ ((s.length : Int) < 0) := by omega
  simp only [String.sliceAv, if_neg h0, if_neg h1]
  show String.ofList (s.toList.take s.length) = s
  rw [show s.length = s.toList.length from String.length_toList.symm, List.take_length,
      String.ofList_toList]"#;

/// `String.slice (t ++ u) 0 t.length = t` — prefix recovery from an
/// appended string. One lemma covers the `+` spelling too once
/// `String.add_eq_append` is in the same simp set (deliberate dedup —
/// no second `+`-keyed spelling is shipped).
const LEAN_PRELUDE_STRING_SLICE_APPEND_PREFIX: &str = r#"/-- Slicing [0, t.length) out of `t ++ u` recovers the prefix `t`. -/
theorem String.slice_append_prefix (t u : String) :
    String.sliceAv (t ++ u) 0 (t.length : Int) = t := by
  have h0 : ¬ ((0 : Int) < 0) := by omega
  have h1 : ¬ ((t.length : Int) < 0) := by omega
  simp only [String.sliceAv, if_neg h0, if_neg h1]
  show String.ofList (((t ++ u).toList).take t.length) = t
  rw [String.toList_append, show t.length = t.toList.length from String.length_toList.symm,
      List.take_left, String.ofList_toList]"#;

/// `String.charAt` at an in-bounds non-negative position computes to
/// the indexed char. Bridges the prelude's `charAt` to `s.data` getElem
/// form so synthesized scan lemmas (`<fn>__fuel_scan`) can dispatch a
/// symbolic head char. Proof ported verbatim from the verified json
/// hand proof.
const LEAN_PRELUDE_STRING_CHARAT_EQ_OF_LT: &str = r#"/-- `String.charAtAv` at an in-bounds non-negative position is the indexed char. -/
theorem String.charAt_eq_of_lt (s : String) (pos : Int) (h0 : 0 ≤ pos) (h : pos.toNat < s.toList.length) :
    String.charAtAv s pos = some (Char.toString (s.toList[pos.toNat])) := by
  have hn : ¬ pos < 0 := by omega
  simp [String.charAtAv, hn, List.getElem?_eq_getElem, h]"#;

/// `String.charAt` past the end is `none` — the scan lemma's exit case.
/// Proof ported verbatim from the verified json hand proof.
const LEAN_PRELUDE_STRING_CHARAT_NONE_OF_GE: &str = r#"/-- `String.charAtAv` at/past the end of the string is `none`. -/
theorem String.charAt_none_of_ge (s : String) (pos : Int) (h0 : 0 ≤ pos) (h : s.toList.length ≤ pos.toNat) :
    String.charAtAv s pos = none := by
  have hn : ¬ pos < 0 := by omega
  simp [String.charAtAv, hn, List.getElem?_eq_none, h]"#;

/// Decimal-digit facts over the `NumericParse` prelude — reopened
/// `AverDigits` namespace, demand-driven like the String spec lemmas.
/// `natDigits_head_ne_zero` (a canonical decimal render never starts
/// with '0' for a nonzero Nat) plus the `digitChar` `Char.toString`
/// disequalities kill the `"-"` / `"0"` dispatch arms on a SYMBOLIC
/// head char in `IntDecimalRoundtrip` emissions. Proofs ported verbatim
/// from the verified json hand proof.
const LEAN_PRELUDE_NUMERIC_PARSE_HEAD_NE_ZERO: &str = r#"namespace AverDigits
theorem natDigits_head_ne_zero : ∀ (m : Nat), m ≠ 0 → ∀ d ds, natDigits m = d :: ds → d ≠ 0 := by
  intro m hm d ds hds
  by_cases h : m < 10
  · rw [natDigits.eq_1] at hds
    simp [h] at hds
    rcases hds with ⟨h1, h2⟩
    omega
  · rw [natDigits.eq_1] at hds
    simp [h] at hds
    rcases hh : natDigits (m / 10) with _ | ⟨d', ds'⟩
    · exact absurd hh (natDigits_nonempty _)
    · rw [hh, List.cons_append] at hds
      injection hds with h1 h2
      rw [← h1]
      exact natDigits_head_ne_zero (m / 10) (by omega) d' ds' hh
end AverDigits"#;

const LEAN_PRELUDE_NUMERIC_PARSE_TOSTRING_NE: &str = r#"namespace AverDigits
theorem digitChar_toString_ne_minus : ∀ d : Nat, d < 10 → Char.toString (digitChar d) ≠ "-" := by
  intro d h
  rcases d with _|_|_|_|_|_|_|_|_|_|d
  all_goals first | decide | omega

theorem digitChar_toString_ne_zero : ∀ d : Nat, d < 10 → d ≠ 0 → Char.toString (digitChar d) ≠ "0" := by
  intro d h hne
  rcases d with _|_|_|_|_|_|_|_|_|_|d
  all_goals first | decide | omega
end AverDigits"#;

/// Static registry: prelude builtin(s) → prelude spec lemma names.
/// Single source of truth, living next to the lemma texts it indexes —
/// the `SimpOverPreludeLemmas` detector records the builtin call names
/// it saw in a law's cone, and this fn maps them to the lemma names the
/// rung's `simp [...]` set cites (which in turn makes the demand-driven
/// prelude inclusion above ship the texts). Keys are Aver source-level
/// builtin names; `String.concat` is the detector's synthetic marker
/// for string `+`. The (`Int.fromString`, `String.fromInt`) PAIR maps
/// to the roundtrip lemma `Int.fromString_fromInt` (always shipped with
/// the `NumericParse` prelude section).
pub(crate) fn prelude_spec_lemmas_for_builtins(builtins: &[String]) -> Vec<String> {
    let has = |name: &str| builtins.iter().any(|b| b == name);
    let mut lemmas: Vec<String> = Vec::new();
    if builtins.iter().any(|b| b.starts_with("String.")) {
        lemmas.push("String.add_eq_append".to_string());
    }
    if has("String.slice") {
        lemmas.push("String.slice_full".to_string());
        lemmas.push("String.slice_append_prefix".to_string());
    }
    if has("String.join") {
        lemmas.push("String.intercalate_singleton".to_string());
    }
    if has("Int.fromString") && has("String.fromInt") {
        lemmas.push("Int.fromString_fromInt".to_string());
    }
    lemmas
}

/// Oracle v1: BranchPath mirrors the Aver-source opaque builtin. The
/// dewey-decimal string under the hood is not user-observable — users
/// construct paths through `.root`, `.child`, `.parse`.
const LEAN_PRELUDE_BRANCH_PATH: &str = r#"structure BranchPath where
  dewey : String
  deriving Repr, BEq, DecidableEq

def BranchPath.Root : BranchPath := { dewey := "" }

def BranchPath.child (p : BranchPath) (idx : Int) : BranchPath :=
  if p.dewey.isEmpty then { dewey := toString idx }
  else { dewey := p.dewey ++ "." ++ toString idx }

def BranchPath.parse (s : String) : BranchPath := { dewey := s }"#;

const LEAN_PRELUDE_PROOF_FUEL: &str = r#"def averStringPosFuel (s : String) (pos : Int) (rankBudget : Nat) : Nat :=
  (((s.toList.length) - pos.toNat) + 1) * rankBudget"#;

const LEAN_PRELUDE_AVER_MEASURE: &str = r#"namespace AverMeasure
def list (elemMeasure : α → Nat) : List α → Nat
  | [] => 1
  | x :: xs => elemMeasure x + list elemMeasure xs + 1
def option (elemMeasure : α → Nat) : Option α → Nat
  | none => 1
  | some x => elemMeasure x + 1
def except (errMeasure : ε → Nat) (okMeasure : α → Nat) : Except ε α → Nat
  | .error e => errMeasure e + 1
  | .ok v => okMeasure v + 1
end AverMeasure"#;

const AVER_MAP_PRELUDE_BASE: &str = r#"namespace AverMap
def empty : List (α × β) := []
def get [DecidableEq α] (m : List (α × β)) (k : α) : Option β :=
  match m with
  | [] => none
  | (k', v) :: rest => if k = k' then some v else AverMap.get rest k
def set [DecidableEq α] (m : List (α × β)) (k : α) (v : β) : List (α × β) :=
  let rec go : List (α × β) → List (α × β)
    | [] => [(k, v)]
    | (k', v') :: rest => if k = k' then (k, v) :: rest else (k', v') :: go rest
  go m
def has [DecidableEq α] (m : List (α × β)) (k : α) : Bool :=
  m.any (fun p => decide (k = p.1))
def remove [DecidableEq α] (m : List (α × β)) (k : α) : List (α × β) :=
  m.filter (fun p => !(decide (k = p.1)))
def keys (m : List (α × β)) : List α := m.map Prod.fst
def values (m : List (α × β)) : List β := m.map Prod.snd
def entries (m : List (α × β)) : List (α × β) := m
def len (m : List (α × β)) : Nat := m.length
def fromList (entries : List (α × β)) : List (α × β) := entries"#;

const AVER_MAP_PRELUDE_HAS_SET_SELF: &str = r#"private theorem any_set_go_self [DecidableEq α] (k : α) (v : β) :
    ∀ (m : List (α × β)), List.any (AverMap.set.go k v m) (fun p => decide (k = p.1)) = true := by
  intro m
  induction m with
  | nil =>
      simp [AverMap.set.go, List.any]
  | cons p tl ih =>
      cases p with
      | mk k' v' =>
          by_cases h : k = k'
          · simp [AverMap.set.go, List.any, h]
          · simp [AverMap.set.go, List.any, h, ih]

theorem has_set_self [DecidableEq α] (m : List (α × β)) (k : α) (v : β) :
    AverMap.has (AverMap.set m k v) k = true := by
  simpa [AverMap.has, AverMap.set] using any_set_go_self k v m"#;

/// `Map.len(Map.set(m, k, v)) >= 1` — `set` always yields a non-empty map.
/// `set.go` either appends `[(k, v)]` (the `nil` base) or rebuilds a `cons`
/// (both branches of the `cons` step), so its length is `≥ 1` for every `m` —
/// proved by induction on `m`. The public `len_set_ge_one` is stated in the
/// exact lowered shape of the law goal (`((AverMap.len … : Int) >= 1) = true`)
/// so the emitter can discharge it with a bare `exact AverMap.len_set_ge_one
/// _ _ _`. This is the one empty-vs-non-empty Map fact that needs real
/// induction rather than a definitional unfold.
const AVER_MAP_PRELUDE_LEN_SET_GE_ONE: &str = r#"private theorem set_go_len_pos [DecidableEq α] (k : α) (v : β) :
    ∀ (m : List (α × β)), 1 ≤ (AverMap.set.go k v m).length := by
  intro m
  induction m with
  | nil =>
      simp [AverMap.set.go]
  | cons p tl ih =>
      simp only [AverMap.set.go]
      split <;> simp

theorem len_set_ge_one [DecidableEq α] (m : List (α × β)) (k : α) (v : β) :
    (((AverMap.len (AverMap.set m k v)) : Int) >= 1) = true := by
  have h : 1 ≤ (AverMap.set m k v).length := by
    simpa [AverMap.set] using set_go_len_pos k v m
  simp only [AverMap.len]
  exact eq_true (by omega)"#;

const AVER_MAP_PRELUDE_GET_SET_SELF: &str = r#"private theorem get_set_go_self [DecidableEq α] (k : α) (v : β) :
    ∀ (m : List (α × β)), AverMap.get (AverMap.set.go k v m) k = some v := by
  intro m
  induction m with
  | nil =>
      simp [AverMap.set.go, AverMap.get]
  | cons p tl ih =>
      cases p with
      | mk k' v' =>
          by_cases h : k = k'
          · simp [AverMap.set.go, AverMap.get, h]
          · simp [AverMap.set.go, AverMap.get, h, ih]

theorem get_set_self [DecidableEq α] (m : List (α × β)) (k : α) (v : β) :
    AverMap.get (AverMap.set m k v) k = some v := by
  simpa [AverMap.set] using get_set_go_self k v m"#;

const AVER_MAP_PRELUDE_GET_SET_OTHER: &str = r#"private theorem get_set_go_other [DecidableEq α] (k key : α) (v : β) (h : key ≠ k) :
    ∀ (m : List (α × β)), AverMap.get (AverMap.set.go k v m) key = AverMap.get m key := by
  intro m
  induction m with
  | nil =>
      simp [AverMap.set.go, AverMap.get, h]
  | cons p tl ih =>
      cases p with
      | mk k' v' =>
          by_cases hk : k = k'
          · have hkey : key ≠ k' := by simpa [hk] using h
            simp [AverMap.set.go, AverMap.get, hk, hkey]
          · by_cases hkey : key = k'
            · simp [AverMap.set.go, AverMap.get, hk, hkey]
            · simp [AverMap.set.go, AverMap.get, hk, hkey, ih]

theorem get_set_other [DecidableEq α] (m : List (α × β)) (k key : α) (v : β) (h : key ≠ k) :
    AverMap.get (AverMap.set m k v) key = AverMap.get m key := by
  simpa [AverMap.set] using get_set_go_other k key v h m"#;

const AVER_MAP_PRELUDE_HAS_SET_OTHER: &str = r#"theorem has_eq_isSome_get [DecidableEq α] (m : List (α × β)) (k : α) :
    AverMap.has m k = (AverMap.get m k).isSome := by
  induction m with
  | nil =>
      simp [AverMap.has, AverMap.get]
  | cons p tl ih =>
      cases p with
      | mk k' v' =>
          by_cases h : k = k'
          · simp [AverMap.has, AverMap.get, List.any, h]
          · simpa [AverMap.has, AverMap.get, List.any, h] using ih

theorem has_set_other [DecidableEq α] (m : List (α × β)) (k key : α) (v : β) (h : key ≠ k) :
    AverMap.has (AverMap.set m k v) key = AverMap.has m key := by
  rw [AverMap.has_eq_isSome_get, AverMap.has_eq_isSome_get]
  simp [AverMap.get_set_other, h]"#;

// General-key (DIFFERENT-key) Map lemmas. `get_set_other`/`has_set_other`
// above carry the *query-key-differs-from-set-key* hypothesis (`key ≠ k`);
// these are the symmetric / general-key forms a map-fold-homomorphism law's
// cons different-key branch needs: `get_set_ne` keyed on `set k ≠ query k'`
// (mirrors `get_set_go_self`'s induction + by_cases), and `has_set` with NO
// key restriction (membership after a set is "queried key = set key, OR was
// already present" — mirrors `any_set_go_self`, closing with `ac_rfl`/bool
// algebra). Both are kernel-clean from the AverMap defs (`#print axioms ⊆
// {propext, Quot.sound}`). `get_set_ne` is conditional — it only rewrites when
// `simp` can discharge the `k ≠ k'` side-goal from a fact in context.
const AVER_MAP_PRELUDE_GET_SET_NE: &str = r#"private theorem get_set_go_ne [DecidableEq α] (k k' : α) (v : β) (h : k ≠ k') :
    ∀ (m : List (α × β)), AverMap.get (AverMap.set.go k v m) k' = AverMap.get m k' := by
  have hne : k' ≠ k := fun he => h he.symm
  intro m
  induction m with
  | nil =>
      simp [AverMap.set.go, AverMap.get, hne]
  | cons p tl ih =>
      cases p with
      | mk a b =>
          by_cases hk : k = a
          · have hk' : k' ≠ a := by simpa [hk] using hne
            simp [AverMap.set.go, AverMap.get, hk, hk', hne]
          · by_cases hk' : k' = a
            · simp [AverMap.set.go, AverMap.get, hk, hk']
            · simp [AverMap.set.go, AverMap.get, hk, hk', ih]

theorem get_set_ne [DecidableEq α] (m : List (α × β)) (k k' : α) (v : β) (h : k ≠ k') :
    AverMap.get (AverMap.set m k v) k' = AverMap.get m k' := by
  simpa [AverMap.set] using get_set_go_ne k k' v h m"#;

const AVER_MAP_PRELUDE_HAS_SET: &str = r#"private theorem any_set_go [DecidableEq α] (w k : α) (v : β) :
    ∀ (m : List (α × β)),
      List.any (AverMap.set.go w v m) (fun p => decide (k = p.1))
        = (decide (k = w) || List.any m (fun p => decide (k = p.1))) := by
  intro m
  induction m with
  | nil =>
      simp [AverMap.set.go, List.any]
  | cons p tl ih =>
      cases p with
      | mk a b =>
          by_cases hw : w = a
          · subst hw
            simp [AverMap.set.go, List.any]
          · simp [AverMap.set.go, List.any, hw, ih]
            by_cases hk : k = a <;> simp [hk] <;> ac_rfl

theorem has_set [DecidableEq α] (m : List (α × β)) (w k : α) (v : β) :
    AverMap.has (AverMap.set m w v) k = (decide (k = w) || AverMap.has m k) := by
  simpa [AverMap.has, AverMap.set] using any_set_go w k v m"#;

const AVER_MAP_PRELUDE_END: &str = r#"end AverMap"#;

const LEAN_PRELUDE_AVER_LIST: &str = r#"namespace AverList
def get (xs : List α) (i : Int) : Option α :=
  if i < 0 then none else xs[i.toNat]?
private def insertSorted [Ord α] (x : α) : List α → List α
  | [] => [x]
  | y :: ys =>
    if compare x y == Ordering.lt || compare x y == Ordering.eq then
      x :: y :: ys
    else
      y :: insertSorted x ys
def sort [Ord α] (xs : List α) : List α :=
  xs.foldl (fun acc x => insertSorted x acc) []
end AverList"#;

// Built-in record types (Header, HttpResponse, HttpRequest,
// Tcp.Connection, Terminal.Size) used to live as hard-coded literals
// here. They now live in `crate::codegen::builtin_records` —
// declarative descriptions consumed by Lean, Dafny, and WASM via
// shared `needed_records()` and `render_lean()`. Drift between
// backends is no longer possible.

const LEAN_PRELUDE_STRING_HELPERS: &str = r#"def String.charAtAv (s : String) (i : Int) : Option String :=
  if i < 0 then none
  else (s.toList[i.toNat]?).map Char.toString
theorem String.charAt_length_none (s : String) : String.charAtAv s s.length = none := by
  have hs : ¬ ((s.length : Int) < 0) := by omega
  unfold String.charAtAv
  simp only [hs, if_false]
  rw [List.getElem?_eq_none]
  · rfl
  · show s.length ≤ (s.length : Int).toNat
    omega
def String.sliceAv (s : String) (start stop : Int) : String :=
  let startN := if start < 0 then 0 else start.toNat
  let stopN := if stop < 0 then 0 else stop.toNat
  let chars := s.toList
  String.ofList ((chars.drop startN).take (stopN - startN))
private def trimFloatTrailingZerosChars (chars : List Char) : List Char :=
  let noZeros := (chars.reverse.dropWhile (fun c => c == '0')).reverse
  match noZeros.reverse with
  | '.' :: rest => rest.reverse
  | _ => noZeros
private def normalizeFloatString (s : String) : String :=
  if s.toList.any (fun c => c == '.') then
    String.ofList (trimFloatTrailingZerosChars s.toList)
  else s
def String.fromFloat (f : Float) : String := normalizeFloatString (toString f)
def String.charsAv (s : String) : List String := s.toList.map Char.toString
def String.containsSubstr (haystack needle : String) : Bool :=
  if needle.length == 0 then true
  else decide ((haystack.splitOn needle).length > 1)
private theorem char_to_string_append_mk (c : Char) (chars : List Char) :
    Char.toString c ++ String.ofList chars = String.ofList (c :: chars) := by
  apply String.toList_injective
  simp [String.toList_append, String.toList_ofList, Char.toString]
private theorem list_intercalate_nil_singletons (chars : List Char) :
    List.intercalate [] (chars.map (fun c => [c])) = chars := by
  induction chars with
  | nil => rfl
  | cons c rest ih =>
      cases rest with
      | nil => rfl
      | cons c2 rest2 =>
          simp only [List.map_cons] at *
          rw [List.intercalate_cons_cons, ih]
          simp
private theorem string_intercalate_empty_char_strings (chars : List Char) :
    String.intercalate "" (chars.map Char.toString) = String.ofList chars := by
  apply String.toList_injective
  rw [String.toList_intercalate, String.toList_empty, List.map_map]
  have hmap : (List.map (String.toList ∘ Char.toString) chars) = chars.map (fun c => [c]) := by
    apply List.map_congr_left
    intro c _
    simp [Function.comp, Char.toString]
  rw [hmap, list_intercalate_nil_singletons, String.toList_ofList]
theorem String.intercalate_empty_chars (s : String) :
    String.intercalate "" (String.charsAv s) = s := by
  rw [String.charsAv, string_intercalate_empty_char_strings, String.ofList_toList]
namespace AverString
def splitOnCharGo (currentRev : List Char) (sep : Char) : List Char → List String
  | [] => [String.ofList currentRev.reverse]
  | c :: cs =>
      if c == sep then
        String.ofList currentRev.reverse :: splitOnCharGo [] sep cs
      else
        splitOnCharGo (c :: currentRev) sep cs
def splitOnChar (s : String) (sep : Char) : List String :=
  splitOnCharGo [] sep s.toList
def split (s delim : String) : List String :=
  match delim.toList with
  | [] => "" :: (s.toList.map Char.toString) ++ [""]
  | [c] => splitOnChar s c
  | _ => s.splitOn delim
@[simp] private theorem char_toString_data (c : Char) : c.toString.toList = [c] := by
  simp [Char.toString]
private theorem splitOnCharGo_until_sep
    (prefixRev part tail : List Char) (sep : Char) :
    part.all (fun c => c != sep) = true ->
    splitOnCharGo prefixRev sep (part ++ sep :: tail) =
      String.ofList (prefixRev.reverse ++ part) :: splitOnCharGo [] sep tail := by
  intro h_safe
  induction part generalizing prefixRev with
  | nil =>
      simp [splitOnCharGo]
  | cons c rest ih =>
      simp at h_safe
      have h_rest : (rest.all fun c => c != sep) = true := by
        simpa using h_safe.2
      simpa [splitOnCharGo, h_safe.1, List.reverse_cons, List.append_assoc] using
        (ih (c :: prefixRev) h_rest)
private theorem splitOnCharGo_no_sep
    (prefixRev chars : List Char) (sep : Char) :
    chars.all (fun c => c != sep) = true ->
    splitOnCharGo prefixRev sep chars =
      [String.ofList (prefixRev.reverse ++ chars)] := by
  intro h_safe
  induction chars generalizing prefixRev with
  | nil =>
      simp [splitOnCharGo]
  | cons c rest ih =>
      simp at h_safe
      have h_rest : (rest.all fun c => c != sep) = true := by
        simpa using h_safe.2
      simpa [splitOnCharGo, h_safe.1, List.reverse_cons, List.append_assoc] using
        (ih (c :: prefixRev) h_rest)
@[simp] theorem split_single_char_append
    (head tail : String) (sep : Char) :
    head.toList.all (fun c => c != sep) = true ->
    split (head ++ Char.toString sep ++ tail) (Char.toString sep) =
      head :: split tail (Char.toString sep) := by
  intro h_safe
  simpa [split, splitOnChar] using
    (splitOnCharGo_until_sep [] head.toList tail.toList sep h_safe)
@[simp] theorem split_single_char_no_sep
    (s : String) (sep : Char) :
    s.toList.all (fun c => c != sep) = true ->
    split s (Char.toString sep) = [s] := by
  intro h_safe
  simpa [split, splitOnChar] using
    (splitOnCharGo_no_sep [] s.toList sep h_safe)
@[simp] theorem split_intercalate_trailing_single_char
    (parts : List String) (sep : Char) :
    parts.all (fun part => part.toList.all (fun c => c != sep)) = true ->
    split (String.intercalate (Char.toString sep) parts ++ Char.toString sep) (Char.toString sep) =
      match parts with
      | [] => ["", ""]
      | _ => parts ++ [""] := by
  intro h_safe
  induction parts with
  | nil =>
      simp [split, splitOnChar, splitOnCharGo]
  | cons part rest ih =>
      simp at h_safe
      have h_part : (part.toList.all fun c => c != sep) = true := by
        simpa using h_safe.1
      cases rest with
      | nil =>
          have h_empty : ("".toList.all fun c => c != sep) = true := by simp
          calc
            split (String.intercalate (Char.toString sep) [part] ++ Char.toString sep) (Char.toString sep)
                = split (part ++ Char.toString sep) (Char.toString sep) := by
                    simp [String.intercalate_singleton]
            _ = split (part ++ Char.toString sep ++ "") (Char.toString sep) := by
                    simp
            _ = part :: split "" (Char.toString sep) := by
                    simpa using split_single_char_append part "" sep h_part
            _ = [part, ""] := by
                    have hns : split "" (Char.toString sep) = [""] := by
                      simpa using split_single_char_no_sep "" sep h_empty
                    rw [hns]
      | cons next rest' =>
          have h_rest : ((next :: rest').all fun part => part.toList.all fun c => c != sep) = true := by
            simpa using h_safe.2
          have hne : (next :: rest') ≠ [] := by simp
          calc
            split (String.intercalate (Char.toString sep) (part :: next :: rest') ++ Char.toString sep) (Char.toString sep)
                = split (part ++ Char.toString sep ++ (String.intercalate (Char.toString sep) (next :: rest') ++ Char.toString sep)) (Char.toString sep) := by
                    rw [String.intercalate_cons_of_ne_nil hne, String.append_assoc, String.append_assoc]
            _ = part :: split (String.intercalate (Char.toString sep) (next :: rest') ++ Char.toString sep) (Char.toString sep) := by
                    simpa using split_single_char_append part
                      (String.intercalate (Char.toString sep) (next :: rest') ++ Char.toString sep)
                      sep h_part
            _ = part :: (next :: rest' ++ [""]) := by
                    simpa using ih h_rest
end AverString"#;

const LEAN_PRELUDE_NUMERIC_PARSE: &str = r#"namespace AverDigits
def foldDigitsAcc (acc : Nat) : List Nat -> Nat
  | [] => acc
  | d :: ds => foldDigitsAcc (acc * 10 + d) ds

def foldDigits (digits : List Nat) : Nat :=
  foldDigitsAcc 0 digits

private theorem foldDigitsAcc_append_singleton (acc : Nat) (xs : List Nat) (d : Nat) :
    foldDigitsAcc acc (xs ++ [d]) = foldDigitsAcc acc xs * 10 + d := by
  induction xs generalizing acc with
  | nil =>
      simp [foldDigitsAcc]
  | cons x xs ih =>
      simp [foldDigitsAcc, ih, Nat.left_distrib, Nat.add_assoc, Nat.add_left_comm]

private theorem foldDigits_append_singleton (xs : List Nat) (d : Nat) :
    foldDigits (xs ++ [d]) = foldDigits xs * 10 + d := by
  simpa [foldDigits] using foldDigitsAcc_append_singleton 0 xs d

def natDigits : Nat -> List Nat
  | n =>
      if n < 10 then
        [n]
      else
        natDigits (n / 10) ++ [n % 10]
termination_by
  n => n

theorem natDigits_nonempty (n : Nat) : natDigits n ≠ [] := by
  by_cases h : n < 10
  · rw [natDigits.eq_1]
    simp [h]
  · rw [natDigits.eq_1]
    simp [h]

theorem natDigits_digits_lt_ten : ∀ n : Nat, ∀ d ∈ natDigits n, d < 10 := by
  intro n d hd
  by_cases h : n < 10
  · rw [natDigits.eq_1] at hd
    simp [h] at hd
    rcases hd with rfl
    exact h
  · rw [natDigits.eq_1] at hd
    simp [h] at hd
    rcases hd with hd | hd
    · exact natDigits_digits_lt_ten (n / 10) d hd
    · subst hd
      exact Nat.mod_lt n (by omega)

theorem foldDigits_natDigits : ∀ n : Nat, foldDigits (natDigits n) = n := by
  intro n
  by_cases h : n < 10
  · rw [natDigits.eq_1]
    simp [h, foldDigits, foldDigitsAcc]
  · rw [natDigits.eq_1]
    simp [h]
    rw [foldDigits_append_singleton]
    rw [foldDigits_natDigits (n / 10)]
    omega

def digitChar : Nat -> Char
  | 0 => '0' | 1 => '1' | 2 => '2' | 3 => '3' | 4 => '4'
  | 5 => '5' | 6 => '6' | 7 => '7' | 8 => '8' | 9 => '9'
  | _ => '0'

def charToDigit? : Char -> Option Nat
  | '0' => some 0 | '1' => some 1 | '2' => some 2 | '3' => some 3 | '4' => some 4
  | '5' => some 5 | '6' => some 6 | '7' => some 7 | '8' => some 8 | '9' => some 9
  | _ => none

theorem charToDigit_digitChar : ∀ d : Nat, d < 10 -> charToDigit? (digitChar d) = some d
  | 0, _ => by simp [digitChar, charToDigit?]
  | 1, _ => by simp [digitChar, charToDigit?]
  | 2, _ => by simp [digitChar, charToDigit?]
  | 3, _ => by simp [digitChar, charToDigit?]
  | 4, _ => by simp [digitChar, charToDigit?]
  | 5, _ => by simp [digitChar, charToDigit?]
  | 6, _ => by simp [digitChar, charToDigit?]
  | 7, _ => by simp [digitChar, charToDigit?]
  | 8, _ => by simp [digitChar, charToDigit?]
  | 9, _ => by simp [digitChar, charToDigit?]
  | Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ n))))))))), h => by
      omega

theorem digitChar_ne_minus : ∀ d : Nat, d < 10 -> digitChar d ≠ '-'
  | 0, _ => by decide
  | 1, _ => by decide
  | 2, _ => by decide
  | 3, _ => by decide
  | 4, _ => by decide
  | 5, _ => by decide
  | 6, _ => by decide
  | 7, _ => by decide
  | 8, _ => by decide
  | 9, _ => by decide
  | Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ n))))))))), h => by
      omega

theorem digitChar_not_ws : ∀ d : Nat, d < 10 ->
    Char.toString (digitChar d) ≠ " " ∧
    Char.toString (digitChar d) ≠ "\t" ∧
    Char.toString (digitChar d) ≠ "\n" ∧
    Char.toString (digitChar d) ≠ "\r"
  | 0, _ => by decide
  | 1, _ => by decide
  | 2, _ => by decide
  | 3, _ => by decide
  | 4, _ => by decide
  | 5, _ => by decide
  | 6, _ => by decide
  | 7, _ => by decide
  | 8, _ => by decide
  | 9, _ => by decide
  | Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ n))))))))), h => by
      omega

theorem mapM_charToDigit_digits : ∀ ds : List Nat,
    (∀ d ∈ ds, d < 10) -> List.mapM charToDigit? (ds.map digitChar) = some ds := by
  intro ds hds
  induction ds with
  | nil =>
      simp
  | cons d ds ih =>
      have hd : d < 10 := hds d (by simp)
      have htail : ∀ x ∈ ds, x < 10 := by
        intro x hx
        exact hds x (by simp [hx])
      simp [charToDigit_digitChar d hd, ih htail]

def natDigitsChars (n : Nat) : List Char :=
  (natDigits n).map digitChar

def parseNatChars (chars : List Char) : Option Nat :=
  match chars with
  | [] => none
  | _ => do
      let digits <- List.mapM charToDigit? chars
      pure (foldDigits digits)

theorem parseNatChars_nat (n : Nat) :
    parseNatChars (natDigitsChars n) = some n := by
  unfold parseNatChars natDigitsChars
  cases h : (natDigits n).map digitChar with
  | nil =>
      exfalso
      exact natDigits_nonempty n (List.map_eq_nil_iff.mp h)
  | cons hd tl =>
      have hdigits : List.mapM charToDigit? (List.map digitChar (natDigits n)) = some (natDigits n) :=
        mapM_charToDigit_digits (natDigits n) (fun d hd => natDigits_digits_lt_ten n d hd)
      rw [h] at hdigits
      simp [h, hdigits, foldDigits_natDigits]
end AverDigits

/-- `(String.mk cs).toList = cs` — bridges the deprecated `String.mk`
spelling to the byte-backed `toList` view via `String.toList_ofList`
(`String.mk = String.ofList` definitionally on 4.31). -/
theorem String.toList_mk (cs : List Char) : (String.mk cs).toList = cs := String.toList_ofList

def String.fromInt (n : Int) : String :=
  match n with
  | .ofNat m => String.ofList (AverDigits.natDigitsChars m)
  | .negSucc m => String.ofList ('-' :: AverDigits.natDigitsChars (m + 1))

def Int.fromString (s : String) : Except String Int :=
  match s.toList with
  | [] => .error ("Cannot parse '" ++ s ++ "' as Int")
  | '-' :: rest =>
    match AverDigits.parseNatChars rest with
    | some n => .ok (-Int.ofNat n)
    | none => .error ("Cannot parse '" ++ s ++ "' as Int")
  | chars =>
    match AverDigits.parseNatChars chars with
    | some n => .ok (Int.ofNat n)
    | none => .error ("Cannot parse '" ++ s ++ "' as Int")

theorem Int.fromString_fromInt : ∀ n : Int, Int.fromString (String.fromInt n) = .ok n
  | .ofNat m => by
      cases h : AverDigits.natDigits m with
      | nil =>
          exfalso
          exact AverDigits.natDigits_nonempty m h
      | cons d ds =>
          have hd : d < 10 := AverDigits.natDigits_digits_lt_ten m d (by simp [h])
          have hne : AverDigits.digitChar d ≠ '-' := AverDigits.digitChar_ne_minus d hd
          have hparse : AverDigits.parseNatChars (AverDigits.digitChar d :: List.map AverDigits.digitChar ds) = some m := by
            simpa [AverDigits.natDigitsChars, h] using AverDigits.parseNatChars_nat m
          simp [String.fromInt, Int.fromString, AverDigits.natDigitsChars, h, hne, hparse, String.toList_ofList]
  | .negSucc m => by
      simp [String.fromInt, Int.fromString, AverDigits.parseNatChars_nat, String.toList_ofList]
      rfl

private def charDigitsToNat (cs : List Char) : Nat :=
  cs.foldl (fun acc c => acc * 10 + (c.toNat - '0'.toNat)) 0

private def parseExpPart : List Char → (Bool × List Char)
  | '-' :: rest => (true, rest.takeWhile Char.isDigit)
  | '+' :: rest => (false, rest.takeWhile Char.isDigit)
  | rest => (false, rest.takeWhile Char.isDigit)

def Float.fromString (s : String) : Except String Float :=
  let chars := s.toList
  let (neg, chars) := match chars with
    | '-' :: rest => (true, rest)
    | _ => (false, chars)
  let intPart := chars.takeWhile Char.isDigit
  let rest := chars.dropWhile Char.isDigit
  let (fracPart, rest) := match rest with
    | '.' :: rest => (rest.takeWhile Char.isDigit, rest.dropWhile Char.isDigit)
    | _ => ([], rest)
  let (expNeg, expDigits) := match rest with
    | 'e' :: rest => parseExpPart rest
    | 'E' :: rest => parseExpPart rest
    | _ => (false, [])
  if intPart.isEmpty && fracPart.isEmpty then .error ("Invalid float: " ++ s)
  else
    let mantissa := charDigitsToNat (intPart ++ fracPart)
    let fracLen : Int := fracPart.length
    let expVal : Int := charDigitsToNat expDigits
    let shift : Int := (if expNeg then -expVal else expVal) - fracLen
    let f := if shift >= 0 then Float.ofScientific mantissa false shift.toNat
             else Float.ofScientific mantissa true ((-shift).toNat)
    .ok (if neg then -f else f)"#;

const LEAN_PRELUDE_CHAR_BYTE: &str = r#"def Char.toCode (s : String) : Int :=
  match s.toList.head? with
  | some c => (c.toNat : Int)
  | none => panic! "Char.toCode: string is empty"
def Char.fromCode (n : Int) : Option String :=
  if n < 0 || n > 1114111 then none
  else if n >= 55296 && n <= 57343 then none
  else some (Char.toString (Char.ofNat n.toNat))

def hexDigit (n : Int) : String :=
  match n with
  | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3"
  | 4 => "4" | 5 => "5" | 6 => "6" | 7 => "7"
  | 8 => "8" | 9 => "9" | 10 => "a" | 11 => "b"
  | 12 => "c" | 13 => "d" | 14 => "e" | 15 => "f"
  | _ => "?"

def byteToHex (code : Int) : String :=
  hexDigit (code / 16) ++ hexDigit (code % 16)

namespace AverByte
private def hexValue (c : Char) : Option Int :=
  match c with
  | '0' => some 0  | '1' => some 1  | '2' => some 2  | '3' => some 3
  | '4' => some 4  | '5' => some 5  | '6' => some 6  | '7' => some 7
  | '8' => some 8  | '9' => some 9  | 'a' => some 10 | 'b' => some 11
  | 'c' => some 12 | 'd' => some 13 | 'e' => some 14 | 'f' => some 15
  | 'A' => some 10 | 'B' => some 11 | 'C' => some 12 | 'D' => some 13
  | 'E' => some 14 | 'F' => some 15
  | _ => none
def toHex (n : Int) : Except String String :=
  if n < 0 || n > 255 then
    .error ("Byte.toHex: " ++ toString n ++ " is out of range 0-255")
  else
    .ok (byteToHex n)
def fromHex (s : String) : Except String Int :=
  match s.toList with
  | [hi, lo] =>
    match hexValue hi, hexValue lo with
    | some h, some l => .ok (h * 16 + l)
    | _, _ => .error ("Byte.fromHex: invalid hex '" ++ s ++ "'")
  | _ => .error ("Byte.fromHex: expected exactly 2 hex chars, got '" ++ s ++ "'")
end AverByte"#;

#[cfg(test)]
pub(super) fn generate_prelude() -> String {
    generate_prelude_for_body("", true)
}

#[cfg(test)]
fn generate_prelude_for_body(body: &str, include_all_helpers: bool) -> String {
    // Oracle v1: trust-assumption header first so the emitted file opens with
    // the explicit claim block before any prelude or definitions. Skipped when
    // the body has no Oracle lifting at all — pure-math files don't depend on
    // any of the trust claims, so emitting the block would just add noise.
    let mut parts = vec![LEAN_PRELUDE_HEADER.to_string()];
    if include_all_helpers || crate::codegen::builtin_records::needs_trust_header(body) {
        // This branch is only reachable from #[cfg(test)] code that
        // calls `generate_prelude` without a real ctx; pass an empty
        // declared_effects set so the test fixture exercises the
        // "no effects" rendering. Production calls go through the
        // ctx-aware path in `transpile_unified`.
        let empty = crate::codegen::common::DeclaredEffects {
            bare_namespaces: std::collections::HashSet::new(),
            methods: std::collections::HashSet::new(),
        };
        let has_ip = body.contains("BranchPath");
        parts.push(
            crate::types::checker::proof_trust_header::generate_commented("-- ", &empty, has_ip),
        );
    }
    // Built-in record types — shared decision module decides which ones.
    for record in crate::codegen::builtin_records::needed_records(body, include_all_helpers) {
        parts.push(crate::codegen::builtin_records::render_lean(record));
    }

    // Built-in helpers — same shared decision pattern. Each key has a
    // backend-native body resolved here (Lean preludes); other backends
    // use the same shared decision against their own implementations.
    for helper in crate::codegen::builtin_helpers::needed_helpers(body, include_all_helpers) {
        match helper.key {
            "BranchPath" => parts.push(LEAN_PRELUDE_BRANCH_PATH.to_string()),
            "AverList" => parts.push(LEAN_PRELUDE_AVER_LIST.to_string()),
            "StringHelpers" => {
                parts.push(generate_string_helpers_prelude(body, include_all_helpers))
            }
            "NumericParse" => parts.push(generate_numeric_parse_prelude(body, include_all_helpers)),
            "CharByte" => parts.push(LEAN_PRELUDE_CHAR_BYTE.to_string()),
            "AverMeasure" => parts.push(LEAN_PRELUDE_AVER_MEASURE.to_string()),
            "AverMap" => parts.push(generate_map_prelude(body, include_all_helpers)),
            "ProofFuel" => parts.push(LEAN_PRELUDE_PROOF_FUEL.to_string()),
            "FloatInstances" => parts.extend([
                LEAN_PRELUDE_FLOAT_COE.to_string(),
                LEAN_PRELUDE_FLOAT_DEC_EQ.to_string(),
            ]),
            "ExceptInstances" => parts.extend([
                LEAN_PRELUDE_EXCEPT_DEC_EQ.to_string(),
                LEAN_PRELUDE_EXCEPT_NS.to_string(),
                LEAN_PRELUDE_OPTION_TO_EXCEPT.to_string(),
            ]),
            "StringHadd" => parts.push(generate_string_hadd_prelude(body, include_all_helpers)),
            // Dafny-side datatype declarations — Lean has Result/Option
            // natively (`Except`/`Option`) and BranchPath ships as part
            // of the BranchPath helper key, so all four are no-ops here.
            "ResultDatatype" | "OptionDatatype" | "OptionToResult" | "BranchPathDatatype" => {}
            other => panic!(
                "Lean backend has no implementation for builtin helper key '{}'. \
                 Add a match arm in generate_prelude_for_body or remove the key \
                 from BUILTIN_HELPERS.",
                other
            ),
        }
    }

    parts.join("\n\n")
}

/// Whether `body` references the general-key `AverMap.has_set` lemma —
/// distinct from `AverMap.has_set_self` / `AverMap.has_set_other`, of which it
/// is a prefix. Matched only when the next char after `has_set` is not an
/// identifier continuation, so the `_self`/`_other` siblings don't trigger it.
fn mentions_has_set(body: &str) -> bool {
    const NEEDLE: &str = "AverMap.has_set";
    body.match_indices(NEEDLE).any(|(idx, _)| {
        body[idx + NEEDLE.len()..]
            .chars()
            .next()
            .is_none_or(|c| !(c.is_alphanumeric() || c == '_'))
    })
}

/// `StringHelpers` section: base defs + demand-driven `String.slice`
/// spec lemmas. Mirrors [`generate_map_prelude`]'s inclusion pattern —
/// a lemma ships only when the body (which includes law tactic text)
/// mentions its name, so corpora that never cite it get byte-identical
/// output.
fn generate_string_helpers_prelude(body: &str, include_all_helpers: bool) -> String {
    let mut parts = vec![LEAN_PRELUDE_STRING_HELPERS.to_string()];
    if include_all_helpers || body.contains("String.slice_full") {
        parts.push(LEAN_PRELUDE_STRING_SLICE_FULL.to_string());
    }
    if include_all_helpers || body.contains("String.slice_append_prefix") {
        parts.push(LEAN_PRELUDE_STRING_SLICE_APPEND_PREFIX.to_string());
    }
    if include_all_helpers || body.contains("String.charAt_eq_of_lt") {
        parts.push(LEAN_PRELUDE_STRING_CHARAT_EQ_OF_LT.to_string());
    }
    if include_all_helpers || body.contains("String.charAt_none_of_ge") {
        parts.push(LEAN_PRELUDE_STRING_CHARAT_NONE_OF_GE.to_string());
    }
    parts.join("\n\n")
}

/// `NumericParse` section: base `AverDigits` + demand-driven decimal-
/// digit spec lemmas (reopened namespace). Same inclusion pattern as
/// [`generate_string_helpers_prelude`] — a lemma ships only when the
/// emitted body (which includes law tactic text and synthesized scan
/// lemmas) mentions its name.
fn generate_numeric_parse_prelude(body: &str, include_all_helpers: bool) -> String {
    let mut parts = vec![LEAN_PRELUDE_NUMERIC_PARSE.to_string()];
    if include_all_helpers || body.contains("AverDigits.natDigits_head_ne_zero") {
        parts.push(LEAN_PRELUDE_NUMERIC_PARSE_HEAD_NE_ZERO.to_string());
    }
    if include_all_helpers
        || body.contains("AverDigits.digitChar_toString_ne_minus")
        || body.contains("AverDigits.digitChar_toString_ne_zero")
    {
        parts.push(LEAN_PRELUDE_NUMERIC_PARSE_TOSTRING_NE.to_string());
    }
    parts.join("\n\n")
}

/// `StringHadd` section: the `HAdd String` instance + demand-driven
/// spec lemmas that need nothing from `StringHelpers`
/// (`String.add_eq_append` is about the instance itself;
/// `String.intercalate_singleton` is now a core `@[simp]` lemma on
/// Lean 4.31, so no prelude copy ships — the rung's simp set cites the
/// core name directly).
/// Same inclusion pattern as [`generate_map_prelude`].
fn generate_string_hadd_prelude(body: &str, include_all_helpers: bool) -> String {
    let mut parts = vec![LEAN_PRELUDE_STRING_HADD.to_string()];
    if include_all_helpers || body.contains("String.add_eq_append") {
        parts.push(LEAN_PRELUDE_STRING_ADD_EQ_APPEND.to_string());
    }
    parts.join("\n\n")
}

fn generate_map_prelude(body: &str, include_all_helpers: bool) -> String {
    let mut parts = vec![AVER_MAP_PRELUDE_BASE.to_string()];

    let needs_has_set_self = include_all_helpers || body.contains("AverMap.has_set_self");
    let needs_len_set_ge_one = include_all_helpers || body.contains("AverMap.len_set_ge_one");
    let needs_get_set_self = include_all_helpers || body.contains("AverMap.get_set_self");
    let needs_get_set_other = include_all_helpers
        || body.contains("AverMap.get_set_other")
        || body.contains("AverMap.has_set_other");
    let needs_has_set_other = include_all_helpers || body.contains("AverMap.has_set_other");
    // `get_set_ne` (general different-key get) and `has_set` (general-key
    // membership-after-set) — the map-fold-homomorphism cons different-key arm.
    let needs_get_set_ne = include_all_helpers || body.contains("AverMap.get_set_ne");
    let needs_has_set = include_all_helpers || mentions_has_set(body);

    if needs_has_set_self {
        parts.push(AVER_MAP_PRELUDE_HAS_SET_SELF.to_string());
    }
    if needs_len_set_ge_one {
        parts.push(AVER_MAP_PRELUDE_LEN_SET_GE_ONE.to_string());
    }
    if needs_get_set_self {
        parts.push(AVER_MAP_PRELUDE_GET_SET_SELF.to_string());
    }
    if needs_get_set_other {
        parts.push(AVER_MAP_PRELUDE_GET_SET_OTHER.to_string());
    }
    if needs_has_set_other {
        parts.push(AVER_MAP_PRELUDE_HAS_SET_OTHER.to_string());
    }
    if needs_get_set_ne {
        parts.push(AVER_MAP_PRELUDE_GET_SET_NE.to_string());
    }
    if needs_has_set {
        parts.push(AVER_MAP_PRELUDE_HAS_SET.to_string());
    }

    parts.push(AVER_MAP_PRELUDE_END.to_string());
    parts.join("\n\n")
}

pub(super) fn generate_lakefile_with_roots(project_name: &str, extra_roots: &[String]) -> String {
    let mut roots: Vec<String> = vec![format!("`{}", project_name)];
    for r in extra_roots {
        roots.push(format!("`{}", r));
    }
    let roots_str = roots.join(", ");
    format!(
        r#"import Lake
open Lake DSL

package «{}» where
  version := v!"0.1.0"

@[default_target]
lean_lib «{}» where
  srcDir := "."
  roots := #[{}]
"#,
        project_name.to_lowercase(),
        project_name,
        roots_str
    )
}

pub(super) fn generate_toolchain() -> String {
    "leanprover/lean4:v4.31.0\n".to_string()
}

pub(super) fn build_common_lean(union_body: &str) -> String {
    let mut parts = vec![LEAN_PRELUDE_HEADER.to_string()];
    for record in crate::codegen::builtin_records::needed_records(union_body, false) {
        parts.push(crate::codegen::builtin_records::render_lean(record));
    }
    for helper in crate::codegen::builtin_helpers::needed_helpers(union_body, false) {
        match helper.key {
            "BranchPath" => parts.push(LEAN_PRELUDE_BRANCH_PATH.to_string()),
            "AverList" => parts.push(LEAN_PRELUDE_AVER_LIST.to_string()),
            "StringHelpers" => parts.push(generate_string_helpers_prelude(union_body, false)),
            "NumericParse" => parts.push(generate_numeric_parse_prelude(union_body, false)),
            "CharByte" => parts.push(LEAN_PRELUDE_CHAR_BYTE.to_string()),
            "AverMeasure" => parts.push(LEAN_PRELUDE_AVER_MEASURE.to_string()),
            "AverMap" => parts.push(generate_map_prelude(union_body, false)),
            "ProofFuel" => parts.push(LEAN_PRELUDE_PROOF_FUEL.to_string()),
            "FloatInstances" => parts.extend([
                LEAN_PRELUDE_FLOAT_COE.to_string(),
                LEAN_PRELUDE_FLOAT_DEC_EQ.to_string(),
            ]),
            "ExceptInstances" => parts.extend([
                LEAN_PRELUDE_EXCEPT_DEC_EQ.to_string(),
                LEAN_PRELUDE_EXCEPT_NS.to_string(),
                LEAN_PRELUDE_OPTION_TO_EXCEPT.to_string(),
            ]),
            "StringHadd" => parts.push(generate_string_hadd_prelude(union_body, false)),
            "ResultDatatype" | "OptionDatatype" | "OptionToResult" | "BranchPathDatatype" => {}
            other => panic!(
                "Lean backend has no implementation for builtin helper key '{}'. \
                 Add a match arm in build_common_lean or remove the key from BUILTIN_HELPERS.",
                other
            ),
        }
    }
    parts.join("\n\n")
}