aver-lang 0.25.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

-- 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.intercalate sep [x] = x` — the singleton-join collapse
/// (`String.join(List.concat([], [seg]), sep)` shapes). Pure `rfl`
/// over core `String.intercalate`; ships with `StringHadd` (any
/// String-mentioning body) because it does not depend on the
/// `StringHelpers` defs.
const LEAN_PRELUDE_STRING_INTERCALATE_SINGLETON: &str = r#"/-- Intercalating a singleton list is the element itself. -/
theorem String.intercalate_singleton (sep x : String) : String.intercalate sep [x] = x := 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.slice 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.slice, if_neg h0, if_neg h1]
  show String.mk (s.toList.take s.length) = s
  cases s with
  | mk data =>
      show String.mk (data.take data.length) = String.mk data
      rw [List.take_length]"#;

/// `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.slice (t ++ u) 0 (t.length : Int) = t := by
  show String.mk ((t.data ++ u.data).take t.data.length) = t
  rw [List.take_left]"#;

/// `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.charAt` 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.data.length) :
    String.charAt s pos = some (Char.toString (s.data[pos.toNat])) := by
  have hn : ¬ pos < 0 := by omega
  simp [String.charAt, String.toList, 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.charAt` at/past the end of the string is `none`. -/
theorem String.charAt_none_of_ge (s : String) (pos : Int) (h0 : 0 ≤ pos) (h : s.data.length ≤ pos.toNat) :
    String.charAt s pos = none := by
  have hn : ¬ pos < 0 := by omega
  simp [String.charAt, String.toList, 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.data.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"#;

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.get? 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.charAt (s : String) (i : Int) : Option String :=
  if i < 0 then none
  else (s.toList.get? i.toNat).map Char.toString
theorem String.charAt_length_none (s : String) : String.charAt s s.length = none := by
  have hs : ¬ ((s.length : Int) < 0) := by omega
  unfold String.charAt
  simp [hs]
  change s.data.length ≤ s.length
  exact Nat.le_refl _
def String.slice (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.mk ((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.mk (trimFloatTrailingZerosChars s.toList)
  else s
def String.fromFloat (f : Float) : String := normalizeFloatString (toString f)
def String.chars (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.mk chars = String.mk (c :: chars) := by
  rfl
private theorem string_intercalate_empty_char_strings_go (acc : String) (chars : List Char) :
    String.intercalate.go acc "" (chars.map Char.toString) = acc ++ String.mk chars := by
  induction chars generalizing acc with
  | nil =>
      simp [String.intercalate.go]
  | cons c rest ih =>
      calc
        String.intercalate.go acc "" ((c :: rest).map Char.toString)
            = String.intercalate.go (acc ++ Char.toString c) "" (rest.map Char.toString) := by
                simp [String.intercalate.go]
        _ = (acc ++ Char.toString c) ++ String.mk rest := by
                simpa using ih (acc ++ Char.toString c)
        _ = acc ++ String.mk (c :: rest) := by
                simp [String.append_assoc, char_to_string_append_mk]
private theorem string_intercalate_empty_char_strings (chars : List Char) :
    String.intercalate "" (chars.map Char.toString) = String.mk chars := by
  cases chars with
  | nil =>
      simp [String.intercalate]
  | cons c rest =>
      simpa [String.intercalate] using string_intercalate_empty_char_strings_go c.toString rest
theorem String.intercalate_empty_chars (s : String) :
    String.intercalate "" (String.chars s) = s := by
  cases s with
  | mk chars =>
      simpa [String.chars] using string_intercalate_empty_char_strings chars
namespace AverString
def splitOnCharGo (currentRev : List Char) (sep : Char) : List Char → List String
  | [] => [String.mk currentRev.reverse]
  | c :: cs =>
      if c == sep then
        String.mk 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.data = [c] := by
  rfl
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.mk (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.mk (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.data tail.data 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.data sep h_safe)
private theorem intercalate_go_prefix
    (pref acc sep : String) (rest : List String) :
    String.intercalate.go (pref ++ sep ++ acc) sep rest =
      pref ++ sep ++ String.intercalate.go acc sep rest := by
  induction rest generalizing acc with
  | nil =>
      simp [String.intercalate.go, String.append_assoc]
  | cons x xs ih =>
      simpa [String.intercalate.go, String.append_assoc] using
        (ih (acc ++ sep ++ x))
@[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.go part (Char.toString sep) [] ++ Char.toString sep) (Char.toString sep)
                = split (part ++ Char.toString sep) (Char.toString sep) := by
                    simp [String.intercalate.go]
            _ = part :: split "" (Char.toString sep) := by
                    simpa using split_single_char_append part "" sep h_part
            _ = [part, ""] := by
                    simp [split_single_char_no_sep, h_empty]
      | 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
          calc
            split
                  (String.intercalate.go part (Char.toString sep) (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
                    have h_join :
                        String.intercalate.go part (Char.toString sep) (next :: rest') ++ Char.toString sep
                          = part ++ Char.toString sep ++ (String.intercalate (Char.toString sep) (next :: rest') ++ Char.toString sep) := by
                        calc
                          String.intercalate.go part (Char.toString sep) (next :: rest') ++ Char.toString sep
                              = String.intercalate.go (part ++ Char.toString sep ++ next) (Char.toString sep) rest' ++ Char.toString sep := by
                                  simp [String.intercalate.go]
                          _ = part ++ Char.toString sep ++ (String.intercalate.go next (Char.toString sep) rest' ++ Char.toString sep) := by
                                  rw [intercalate_go_prefix part next (Char.toString sep) rest']
                                  simp [String.append_assoc]
                          _ = part ++ Char.toString sep ++ (String.intercalate (Char.toString sep) (next :: rest') ++ Char.toString sep) := by
                                  simp [String.intercalate, String.intercalate.go]
                    simpa using congrArg (fun s => split s (Char.toString sep)) h_join
            _ = 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

def String.fromInt (n : Int) : String :=
  match n with
  | .ofNat m => String.mk (AverDigits.natDigitsChars m)
  | .negSucc m => String.mk ('-' :: 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]
  | .negSucc m => by
      simp [String.fromInt, Int.fromString, AverDigits.parseNatChars_nat]
      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 over core `String.intercalate`).
/// 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());
    }
    if include_all_helpers || body.contains("String.intercalate_singleton") {
        parts.push(LEAN_PRELUDE_STRING_INTERCALATE_SINGLETON.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_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_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.15.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")
}