aver-lang 0.27.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]"#;

/// `String.charAtAv s pos = some c` forces `pos` into `[0, s.length)`.
/// The termination witness for the graduated native string-position
/// SKIP scanner: `decreasing_by` reads the outer match's `charAtAv …
/// = some c` equation and this lemma turns it into `pos.toNat <
/// s.toList.length`, which `omega` uses to discharge the strict
/// decrease of the `s.toList.length - pos.toNat` measure. Sibling of
/// `charAt_eq_of_lt` / `charAt_none_of_ge`; core-only (no `by_contra`
/// / `push_neg`, neither of which is in the emitted prelude).
const LEAN_PRELUDE_STRING_CHARAT_SOME_BOUNDS: &str = r#"/-- `String.charAtAv` returning `some` pins the position in bounds. -/
theorem String.charAt_some_bounds (s : String) (pos : Int) (c : String)
    (h : String.charAtAv s pos = some c) :
    0 ≤ pos ∧ pos.toNat < s.toList.length := by
  unfold String.charAtAv at h
  by_cases hneg : pos < 0
  · simp [hneg] at h
  · simp only [hneg, if_false] at h
    refine ⟨by omega, ?_⟩
    rcases Nat.lt_or_ge pos.toNat s.toList.length with hlt | hge
    · exact hlt
    · exfalso
      rw [List.getElem?_eq_none hge] at h
      simp at 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"#;

/// The nonlinear nonneg/order closing kit for the `NonlinearNonneg`
/// strategy (the Newton-Raphson error bounds of `projects/k5_fdiv`).
/// Core `Int` only — no Mathlib, no `nlinarith`/`positivity`. Shipped
/// demand-driven (only when a proof actually invokes `aver_int_order`),
/// so corpora that never need it get byte-identical output.
///
/// `aver_int_order` is the nonlinear analog of `omega` for the
/// products-and-squares fragment: ONE generic decision step, not a
/// per-figure template. On a nonnegativity goal `0 ≤ a * b` it recurses
/// with `Int.mul_nonneg`; on an order goal where the two products share their
/// right factor (`a*c ≤ b*c` from `a ≤ b`, `0 ≤ c`, with no `0 ≤ b` in hand)
/// it uses `Int.mul_le_mul_of_nonneg_right`, and on a general two-product
/// order `a*c ≤ b*d` it recurses with `Int.mul_le_mul`; a square `0 ≤ t * t`
/// (or its bound)
/// bottoms out on `aver_sq_nonneg` (the sign-split base case —
/// `Int.mul_self_nonneg` does not exist in core); a conjunctive premise is
/// split; and the remaining LINEAR leaves are closed by `omega` (placed
/// second so it disposes of them before the product rungs can backtrack on
/// a linear goal — the ordering that keeps the search shallow and fast).
/// The emitter wraps every use in `first | (…; aver_int_order) | sorry`,
/// so a goal outside the fragment (e.g. a `prod ≤ var` transitivity, which
/// needs a witness this step does not synthesize) falls to an honest caught
/// `sorry` — never a build error — and credit stays fail-closed behind the
/// `#print axioms` whitelist.
const LEAN_PRELUDE_NONLINEAR_NONNEG: &str = r#"/-- A square is never negative — the sign-split base case the product
closer bottoms out on (`Int.mul_self_nonneg` is absent from core Int). -/
theorem aver_sq_nonneg (t : Int) : 0 ≤ t * t := by
  rcases Int.le_total 0 t with h | h
  · exact Int.mul_nonneg h h
  · have h2 : 0 ≤ -t := by omega
    have := Int.mul_nonneg h2 h2
    rwa [Int.neg_mul_neg] at this

/-- Generic nonneg/order decision step for nonlinear Int products: the
`omega`-analog for the products-and-squares fragment. Recurse on a product
with `Int.mul_nonneg` (nonneg goal `0 ≤ a*b`), `Int.mul_pos` (strict goal
`0 < a*b`, the value-magnitude positivity the rounding sign condition needs),
or `Int.mul_le_mul` (product ≤ product),
close a product order whose two sides share their right factor (`a*c ≤ b*c`
from `a ≤ b`, `0 ≤ c`) with `Int.mul_le_mul_of_nonneg_right`, bottom squares
out on `aver_sq_nonneg`, split a conjunctive premise, and discharge the linear
leaves with `omega`. The `mul_pos` rung sits right after `mul_nonneg` (their
conclusions `0 < _` / `0 ≤ _` never unify, so neither shadows the other). The
`mul_le_mul_of_nonneg_right` rung sits BEFORE
`mul_le_mul`, and that order is load-bearing for performance: `mul_le_mul`
would also unify with `a*c ≤ b*c` (taking `d := c`) but spawns a `0 ≤ b` leaf
that is NOT derivable when the law carries no `0 ≤ a` guard. Trying
`mul_le_mul_of_nonneg_right` first closes such a goal directly from `a ≤ b` /
`0 ≤ c` and never spawns `0 ≤ b`; on the squared shapes (`e*e ≤ b*b`, the
contraction's `s²` bound) its shared-right-factor unification fails fast (the
two right factors differ), so `mul_le_mul` still takes them — and any genuine
`0 ≤ b` leaf there is closed by the early `omega` rung from that family's
`0 ≤ e ≤ b` guards. The `mul_le_mul` arm is NOT heartbeat-capped: a
deterministic `whnf` timeout is a HARD, uncatchable failure of a `first`
portfolio at the tactic level — it aborts `lake build` rather than falling
through to the next `first` alternative. `set_option maxHeartbeats … in` only
takes effect at the COMMAND level, never inside a `first | …` tactic
alternative (measured 2026-07-02 across three controlled builds under Lean
4.31: the inline wrapper changed nothing). So this timeout class is not
containable here. What actually keeps this arm from diverging in practice is
the narrower conjunction split below (keyed to the named `h_when` guard rather
than an anonymous `_ ∧ _` match, so it no longer feeds spurious metavariable
products into the product rungs), not any cap. When a timeout does occur its
class is surfaced truthfully by the `--check-json` `build_errors` field; the
named follow-up is driver-level re-emission of the offending law WITHOUT this
arm (a tactic-level cap cannot do it).

The MULTIPLY-BY-POSITIVE rungs (`mul_lt_mul_of_pos_left` / `_right` for a strict
product order `m*a < m*b` / `a*m < b*m`, and `mul_le_mul_of_nonneg_left` for the
nonstrict `m*a ≤ m*b`) sit LAST, after the `<=`-conclusion rungs. They are the
generic non-recursive composition step `omega`/`grind` cannot do — multiplying an
inequality `a < b` by a positive factor `m` — and close any goal already in the
multiplied form `m*a < m*b` from `a < b` (`assumption`) and `0 < m` (the
`mul_pos` recursion on the positive factor). The rational-floor truncation-error
bound (Lemma 7.2.2) ring-bridges its goal into exactly that shape and hands it to
this rung; the same rung is the general non-recursive `mulLeTrans`/`fpMulValue`
composition step. Placed last so their strict (`<`) conclusion never shadows a
`<=`/`0 <=`/`0 <` goal the earlier rungs own (a strict-conclusion lemma cannot
unify with a non-strict goal, but keeping them last also keeps the common
nonneg/positivity search shallow and the output byte-identical for corpora that
never hit a multiplied-form goal).

The final arm splits a named guard conjunction and recurses. It reads the
hypothesis LITERALLY named `h_when` — the order-law emitters
(`law_auto/inequality.rs`, `law_auto/induction/floor_bound.rs`) intro the guard
under exactly that name and `simp … at h_when ⊢` — takes `And.left`/`And.right`,
and recurses. This is a NAMING CONTRACT: any new order-law emitter that renames
the guard makes this arm silently no-op (no `h_when` in context), and the goal
falls to `sorry`. It also peels ONE level only (measured): a right-nested guard
of three-plus conjuncts (`A ∧ (B ∧ C)`) yields `h_when_left := A` /
`h_when_right := B ∧ C`, leaving the inner conjunction bundled. -/
syntax "aver_int_order" : tactic
macro_rules
  | `(tactic| aver_int_order) => `(tactic|
      first
        | assumption
        | omega
        | exact aver_sq_nonneg _
        | (apply Int.mul_nonneg <;> aver_int_order)
        | (apply Int.mul_pos <;> aver_int_order)
        | (apply Int.mul_le_mul_of_nonneg_right <;> aver_int_order)
        | (apply Int.mul_le_mul <;> aver_int_order)
        | (apply Int.mul_lt_mul_of_pos_left <;> aver_int_order)
        | (apply Int.mul_lt_mul_of_pos_right <;> aver_int_order)
        | (apply Int.mul_le_mul_of_nonneg_left <;> aver_int_order)
        | (have h_when_left := And.left h_when
           have h_when_right := And.right h_when
           clear h_when
           aver_int_order))"#;

#[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,
                false,
            )),
            "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
            ),
        }
    }

    if include_all_helpers || body.contains("aver_int_order") {
        parts.push(LEAN_PRELUDE_NONLINEAR_NONNEG.to_string());
    }

    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.
/// Return `src` with every top-level attribute-carrying declaration removed.
/// A declaration whose first (column-0) line opens with `@[` (e.g. `@[simp]`)
/// is the only string-prelude shape that trips the certificate checker's
/// elaboration-executes-code wall; those `@[simp]` spec lemmas exist purely for
/// the `SimpOverPreludeLemmas` law rung, which a certificate never proves, and
/// nothing else in the section (its `def`s, its plain spec lemmas, or the model
/// that imports it) references them. Plain `theorem`s are kept — the model's own
/// `decreasing_by` proofs cite some of them by name, and they carry no wall
/// token. Continuation lines are indented or blank, so a declaration runs until
/// the next column-0 line.
fn strip_proof_only_decls(src: &str) -> String {
    let is_decl_start = |line: &str| !line.is_empty() && !line.starts_with([' ', '\t']);
    let mut out: Vec<&str> = Vec::new();
    let mut dropping = false;
    for line in src.lines() {
        if is_decl_start(line) {
            dropping = line.starts_with("@[");
        }
        if !dropping {
            out.push(line);
        }
    }
    out.join("\n")
}

fn generate_string_helpers_prelude(
    body: &str,
    include_all_helpers: bool,
    cert_model: bool,
) -> String {
    // The string prelude carries `@[simp]` spec lemmas (for the
    // `SimpOverPreludeLemmas` law rung) that a certificate never proves and
    // whose `@[` token the checker wall rejects. Cert mode drops just those; the
    // computational `def`s and the plain spec lemmas the model's own
    // `decreasing_by` cites (e.g. `String.charAt_*`) stay, including the
    // demand-driven additions below.
    let base = if cert_model {
        strip_proof_only_decls(LEAN_PRELUDE_STRING_HELPERS)
    } else {
        LEAN_PRELUDE_STRING_HELPERS.to_string()
    };
    let mut parts = vec![base];
    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());
    }
    if include_all_helpers || body.contains("String.charAt_some_bounds") {
        parts.push(LEAN_PRELUDE_STRING_CHARAT_SOME_BOUNDS.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.32.0\n".to_string()
}

pub(super) fn build_common_lean(union_body: &str, cert_model: bool) -> 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, cert_model,
            )),
            "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()),
            // The `Float` `DecidableEq` shim is `@[implemented_by]`/`unsafe`
            // (proof-only, for `native_decide` on float literals). A cert model
            // needs the `Coe Int Float` definition but not the shim, which the
            // checker wall rejects; drop just the shim in cert mode.
            "FloatInstances" if cert_model => parts.push(LEAN_PRELUDE_FLOAT_COE.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
            ),
        }
    }
    // Nonlinear-nonnegativity closing kit — demand-driven on the tactic
    // name the `NonlinearNonneg` emit invokes, so files that never need it
    // stay byte-identical. Not a `BUILTIN_HELPERS` key: it is Lean-only
    // proof infrastructure (Z3 carries these natively, so Dafny ships
    // nothing), keyed on emitted tactic text rather than a builtin call.
    if union_body.contains("aver_int_order") {
        parts.push(LEAN_PRELUDE_NONLINEAR_NONNEG.to_string());
    }
    parts.join("\n\n")
}