//! Lean renderer for [`crate::ir::ProofStrategy::StringEscapeRoundtrip`] —
//! the escaped-string parse/serialize roundtrip
//! (`examples/data/json.av` `escapeJsonString.parseStringRoundtrip` /
//! `parseStringChunk.escapedStringRoundtrip`).
//!
//! The proof skeleton is ported from the verified json hand proof
//! (closed kernel-clean on Lean 4.15, #print axioms = [propext,
//! Quot.sound]) with the fn names, constructor names, escape table and
//! literals parameterized from the IR pin. Structure, in emission
//! order (every generated name carries the law's `theorem_base` as a
//! prefix so two laws over the same pair — wrapper-entry and
//! scanner-entry — emit independent, collision-free stacks):
//!
//! 1. string/char data prelude (`str_ext`, `data_append`,
//! `String.intercalate ""` algebra, …) — static text;
//! 2. suffix-cursor algebra in drop-form (`drop_succ_of_drop`,
//! `charAt_of_drop`, `slice_snoc`) — the composition-friendly form
//! of the shipped index-arithmetic scan lemmas;
//! 3. producer fold normalization: the acc-free view `escL` and the
//! accumulator homomorphism `fold cs acc = acc ++ fold cs ""` (one
//! induction generalizing `acc`);
//! 4. per-fuel-arm consumer step lemmas, one per validated match arm
//! (`simp [<fn>__fuel, <arm hypotheses>]` each), incl. the
//! `readHex` micro-stepper and the producer classifier's
//! hypothesis-guarded unfolds;
//! 5. the chunk invariant `Inv cs` with the carried scanner state
//! (`segmentStart`, `chunks`) universally quantified, closed by
//! one branch lemma per producer char class (terminator-exit /
//! two-char escape / hex control escape / printable passthrough)
//! and a `by_cases` classification ladder driven by the pinned
//! escape table;
//! 6. law glue: unfold the entry wrapper onto the scanner's fuel form
//! (the `averStringPosFuel` rank is probed from the actual
//! emission), instantiate the invariant at `pos = segStart = 1,
//! chunks = []`, discharge fuel adequacy by `omega`.
//!
//! HONEST FLOOR: every synthesized theorem (support stack AND the law
//! proof) carries a `first | (…; done) | sorry` alternative — a
//! template regression degrades to caught honest sorries (the budget
//! pin flips loud-red), never an unsolved-goals build error, and
//! `native_decide` never appears in this path.
use super::super::expr::aver_name_to_lean;
use super::AutoProof;
use crate::ast::{Expr, Spanned, VerifyLaw};
use crate::codegen::CodegenContext;
use crate::ir::StringEscapeRoundtripPin;
/// Lean escape for one char inside a literal. `in_string` selects
/// which quote needs escaping.
fn lean_escape_char(c: char, in_string: bool) -> String {
match c {
'\\' => "\\\\".to_string(),
'\n' => "\\n".to_string(),
'\t' => "\\t".to_string(),
'\r' => "\\r".to_string(),
'"' if in_string => "\\\"".to_string(),
'\'' if !in_string => "\\'".to_string(),
c if (c as u32) < 0x20 || (c as u32) == 0x7f => format!("\\x{:02x}", c as u32),
c => c.to_string(),
}
}
/// Lean char literal (`'\\n'`).
fn lean_char(c: char) -> String {
format!("'{}'", lean_escape_char(c, false))
}
/// Lean string literal (`"\\n"`).
fn lean_str(s: &str) -> String {
let inner: String = s.chars().map(|c| lean_escape_char(c, true)).collect();
format!("\"{inner}\"")
}
/// Source ctor name (`ParseResult.Ok`) → Lean ctor name
/// (`ParseResult.ok`) — Lean convention lowercases the variant leaf.
fn lean_ctor(name: &str) -> String {
match name.rsplit_once('.') {
Some((ty, variant)) => {
format!("{}.{}", ty, crate::codegen::common::to_lower_first(variant))
}
None => crate::codegen::common::to_lower_first(name),
}
}
/// Wrap a tactic block (lines at base indent 0) in the honest floor:
///
/// ```text
/// <decl> := by
/// first
/// | (<line 1>
/// <line 2>
/// …
/// done)
/// | sorry
/// ```
fn floored(decl: &str, body: &str) -> String {
let mut out = String::new();
out.push_str(decl);
out.push_str(" := by\n first\n");
for (i, line) in body.lines().enumerate() {
if i == 0 {
out.push_str(&format!(" | ({line}\n"));
} else if line.is_empty() {
out.push('\n');
} else {
out.push_str(&format!(" {line}\n"));
}
}
out.push_str(" done)\n | sorry");
out
}
/// Render the `StringEscapeRoundtrip` proof. Returns `None` (caller
/// falls through to the bare-sorry universal) when the probed
/// emission facts don't line up with the pin — the scanner SCC must
/// be fuel-emitted with a string-pos wrapper of rank >= 2 (the
/// invariant's fuel slope), and the producer fold must NOT be
/// fuel-emitted (the homomorphism unfolds its native equations).
pub(super) fn emit_string_escape_roundtrip_law(
law: &VerifyLaw,
ctx: &CodegenContext,
theorem_base: &str,
pin: &StringEscapeRoundtripPin,
) -> Option<AutoProof> {
let emit = |e: &Spanned<Expr>| super::super::expr::emit_expr_legacy(e, ctx, None);
// ---- law-side text (must byte-match the emitted statement) ------
let Expr::FnCall(_, lhs_args) = &law.lhs.node else {
return None;
};
let subject = lhs_args.first()?;
let Expr::BinOp(crate::ast::BinOp::Add, open_prod, _term) = &subject.node else {
return None;
};
let Expr::BinOp(crate::ast::BinOp::Add, _open, prod_call) = &open_prod.node else {
return None;
};
let n = aver_name_to_lean(&law.givens.first()?.name);
let subj = format!("({})", emit(subject));
let prod_text = emit(prod_call);
// Belt-and-braces: the rhs must carry the producer sub-term the
// glue's position rewrite keys on.
if !emit(&law.rhs).replace('\n', " ").contains(&prod_text) {
return None;
}
// ---- emission facts (probed, not assumed) ------------------------
// The scanner must be fuel-emitted with a string-pos wrapper; its
// rank must cover the invariant's fuel slope (2 ticks per consumed
// char). The producer fold must have native equations (no fuel).
let rank = super::super::toplevel::law_string_pos_rank(&pin.scan_fn, ctx)?;
if rank < 2 {
return None;
}
for consumer in [
&pin.scan_fn,
&pin.escape_fn,
&pin.validate_fn,
&pin.unicode_fn,
&pin.codepoint_fn,
&pin.apply_fn,
&pin.read_hex_fn,
] {
if super::super::toplevel::law_fuel_simp_names(consumer, ctx).is_empty() {
return None;
}
}
if !super::super::toplevel::law_fuel_simp_names(&pin.fold_fn, ctx).is_empty() {
return None;
}
// ---- names --------------------------------------------------------
let p = theorem_base;
let fuel = |f: &str| crate::codegen::recursion::fuel_helper_name(f);
let scan_f = fuel(&pin.scan_fn);
let esc_f = fuel(&pin.escape_fn);
let val_f = fuel(&pin.validate_fn);
let uni_f = fuel(&pin.unicode_fn);
let cp_f = fuel(&pin.codepoint_fn);
let app_f = fuel(&pin.apply_fn);
let hex_f = fuel(&pin.read_hex_fn);
let hex_w = aver_name_to_lean(&pin.read_hex_fn);
let fin = aver_name_to_lean(&pin.finish_fn);
let hexval = aver_name_to_lean(&pin.hex_val_fn);
let hi_fn = aver_name_to_lean(&pin.high_surrogate_fn);
let lo_fn = aver_name_to_lean(&pin.low_surrogate_fn);
let prod = aver_name_to_lean(&pin.producer_fn);
let fold = aver_name_to_lean(&pin.fold_fn);
let cls = aver_name_to_lean(&pin.classifier_fn);
let ctl = aver_name_to_lean(&pin.control_fn);
let cce = aver_name_to_lean(&pin.control_escape_fn);
let okc = lean_ctor(&pin.ok_ctor);
let strc = lean_ctor(&pin.str_ctor);
let term_c = lean_char(pin.terminator);
let term_s = lean_str(&pin.terminator.to_string());
let esc_c = lean_char(pin.escape_char);
let esc_s = lean_str(&pin.escape_char.to_string());
let uni_c = lean_char(pin.unicode_letter);
let uni_s = lean_str(&pin.unicode_letter.to_string());
let prefix_s = lean_str(&format!("{}{}00", pin.escape_char, pin.unicode_letter));
let t = pin.control_threshold;
let hi_min = pin.high_surrogate_min;
let lo_min = pin.low_surrogate_min;
// ---- escape-table orderings ----------------------------------------
// 1-based index over the pin's pair vec (classifier arms in arm
// order, then control-ladder arms in ladder order) names the
// per-pair step lemmas and the by_cases hypotheses consistently.
let pairs: Vec<(usize, &crate::ir::EscapePairSpec)> = pin
.pairs
.iter()
.enumerate()
.map(|(i, e)| (i + 1, e))
.collect();
let cls_pairs: Vec<&(usize, &crate::ir::EscapePairSpec)> = pairs
.iter()
.filter(|(_, e)| !e.from_control_ladder)
.collect();
let ladder_pairs: Vec<&(usize, &crate::ir::EscapePairSpec)> = pairs
.iter()
.filter(|(_, e)| e.from_control_ladder)
.collect();
let cls_low: Vec<&(usize, &crate::ir::EscapePairSpec)> = cls_pairs
.iter()
.filter(|(_, e)| (e.decoded as i64) < t)
.copied()
.collect();
let cls_high: Vec<&(usize, &crate::ir::EscapePairSpec)> = cls_pairs
.iter()
.filter(|(_, e)| (e.decoded as i64) >= t)
.copied()
.collect();
let idx_term = cls_pairs
.iter()
.find(|(_, e)| e.decoded == pin.terminator)?
.0;
let idx_esc = cls_pairs
.iter()
.find(|(_, e)| e.decoded == pin.escape_char)?
.0;
let mut support: Vec<String> = Vec::new();
let mut push = |s: String| support.push(s);
// ================= A. string data basics (static) =================
push(floored(
&format!("private theorem {p}_str_ext {{a b : String}} (h : a.toList = b.toList) : a = b"),
"exact String.toList_injective h",
));
push(floored(
&format!(
"private theorem {p}_data_append (a b : String) : (a ++ b).toList = a.toList ++ b.toList"
),
"simp [String.toList_append]",
));
push(floored(
&format!(
"private theorem {p}_data_add (a b : String) : (a + b).toList = a.toList ++ b.toList"
),
"show (a ++ b).toList = a.toList ++ b.toList\nsimp [String.toList_append]",
));
push(floored(
&format!("private theorem {p}_empty_data : (\"\" : String).toList = ([] : List Char)"),
"simp",
));
push(floored(
&format!("private theorem {p}_ts_data (c : Char) : (Char.toString c).toList = [c]"),
"simp [Char.toString]",
));
push(floored(
&format!(
"private theorem {p}_mk_cons (c : Char) (cs : List Char) :\n Char.toString c ++ String.ofList cs = String.ofList (c :: cs)"
),
&format!(
"apply {p}_str_ext\nsimp [String.toList_append, String.toList_ofList, Char.toString]"
),
));
push(floored(
&format!("private theorem {p}_mk_data_self (s : String) : String.ofList s.toList = s"),
"simp [String.ofList_toList]",
));
push(floored(
&format!("private theorem {p}_str_append_empty (s : String) : s ++ \"\" = s"),
&format!("exact {p}_str_ext (by simp [{p}_data_append, {p}_empty_data])"),
));
push(floored(
&format!("private theorem {p}_str_empty_append (s : String) : \"\" ++ s = s"),
&format!("exact {p}_str_ext (by simp [{p}_data_append, {p}_empty_data])"),
));
push(floored(
&format!(
"private theorem {p}_str_append_assoc (a b c : String) : (a ++ b) ++ c = a ++ (b ++ c)"
),
&format!("exact {p}_str_ext (by simp [{p}_data_append, List.append_assoc])"),
));
push(floored(
&format!(
"private theorem {p}_toString_inj {{a b : Char}} (h : Char.toString a = Char.toString b) : a = b"
),
&format!(
"have h2 : (Char.toString a).toList = (Char.toString b).toList := by rw [h]\nsimpa [{p}_ts_data] using h2"
),
));
push(format!(
"private theorem {p}_ts_ne {{a b : Char}} (h : a ≠ b) : Char.toString a ≠ Char.toString b :=\n fun hh => h ({p}_toString_inj hh)"
));
push(floored(
&format!(
"private theorem {p}_toCode_toString (c : Char) : Char.toCode (Char.toString c) = (c.toNat : Int)"
),
"simp [Char.toCode, Char.toString]",
));
push(floored(
&format!(
"private theorem {p}_inter_snoc (xs : List String) (a : String) :\n String.intercalate \"\" (xs ++ [a]) = String.intercalate \"\" xs ++ a"
),
&format!(
"induction xs with\n| nil => simp [String.intercalate_singleton, {p}_str_empty_append]\n| cons x xs ih =>\n cases xs with\n | nil =>\n rw [List.cons_append, List.nil_append]\n rw [String.intercalate_cons_cons, String.intercalate_singleton, String.intercalate_singleton]\n simp [{p}_str_empty_append, String.append_assoc]\n | cons y ys =>\n have hne : (y :: ys) ≠ [] := by simp\n have hne2 : ((y :: ys) ++ [a]) ≠ [] := by simp\n rw [List.cons_append, String.intercalate_cons_of_ne_nil hne2,\n String.intercalate_cons_of_ne_nil hne, ih]\n simp [{p}_str_empty_append, String.append_assoc]"
),
));
push(floored(
&format!("private theorem {p}_inter_single (a : String) : String.intercalate \"\" [a] = a"),
"simp [String.intercalate_singleton]",
));
push(floored(
&format!(
"private theorem {p}_inter_nil : String.intercalate \"\" ([] : List String) = \"\""
),
"simp [String.intercalate_nil]",
));
push(floored(
&format!(
"private theorem {p}_char_eq_of_toNat {{c : Char}} {{m : Nat}} (h : c.toNat = m) : c = Char.ofNat m"
),
"rw [← h, Char.ofNat_toNat]",
));
// ================= B/C. drop-form suffix cursor (static) ==========
push(floored(
&format!(
"private theorem {p}_getElem_of_drop : ∀ {{l : List Char}} {{m : Nat}} {{c : Char}} {{rest : List Char}},\n l.drop m = c :: rest → l[m]? = some c"
),
"intro l\ninduction l with\n| nil => intro m c rest h; simp at h\n| cons a l ih =>\n intro m c rest h\n cases m with\n | zero =>\n simp only [List.drop_zero] at h\n injection h with h1 h2\n simp [h1]\n | succ m =>\n simp only [List.drop_succ_cons] at h\n simpa using ih h",
));
push(floored(
&format!(
"private theorem {p}_drop_succ_of_drop {{l : List Char}} {{m : Nat}} {{c : Char}} {{rest : List Char}}\n (h : l.drop m = c :: rest) : l.drop (m + 1) = rest"
),
"have key : (l.drop m).drop 1 = l.drop (m + 1) := by rw [List.drop_drop]\nrw [← key, h]\nrfl",
));
push(floored(
&format!(
"private theorem {p}_take_succ_of_drop : ∀ {{l : List Char}} {{m : Nat}} {{c : Char}} {{rest : List Char}},\n l.drop m = c :: rest → l.take (m + 1) = l.take m ++ [c]"
),
"intro l\ninduction l with\n| nil => intro m c rest h; simp at h\n| cons a l ih =>\n intro m c rest h\n cases m with\n | zero =>\n simp only [List.drop_zero] at h\n injection h with h1 h2\n simp [h1]\n | succ m =>\n simp only [List.drop_succ_cons] at h\n simp [List.take_succ_cons, ih h]",
));
push(floored(
&format!(
"private theorem {p}_charAt_of_drop {{s : String}} {{pos : Int}} {{c : Char}} {{rest : List Char}}\n (h0 : 0 ≤ pos) (h : s.toList.drop pos.toNat = c :: rest) :\n String.charAtAv s pos = some (Char.toString c)"
),
&format!(
"have hneg : ¬ pos < 0 := by omega\nsimp only [String.charAtAv, hneg, if_false]\nrw [{p}_getElem_of_drop h]\nrfl"
),
));
push(floored(
&format!(
"private theorem {p}_slice_self (s : String) (a : Int) : String.sliceAv s a a = \"\""
),
&format!("apply {p}_str_ext\nsimp [String.sliceAv, {p}_empty_data]"),
));
push(floored(
&format!(
"private theorem {p}_slice_snoc {{s : String}} {{a b : Int}} {{c : Char}} {{rest : List Char}}\n (h0 : 0 ≤ a) (hab : a ≤ b) (h : s.toList.drop b.toNat = c :: rest) :\n String.sliceAv s a (b + 1) = String.sliceAv s a b ++ Char.toString c"
),
&format!(
"apply {p}_str_ext\nhave ha : ¬ a < 0 := by omega\nhave hb : ¬ b < 0 := by omega\nhave hb1 : ¬ b + 1 < 0 := by omega\nsimp [String.sliceAv, ha, hb, hb1, {p}_data_append, {p}_ts_data, String.toList_ofList]\nhave h1 : (b + 1).toNat - a.toNat = (b.toNat - a.toNat) + 1 := by omega\nrw [h1]\nhave h2 : (s.toList.drop a.toNat).drop (b.toNat - a.toNat) = c :: rest := by\n rw [List.drop_drop]\n have heq : a.toNat + (b.toNat - a.toNat) = b.toNat := by omega\n rw [heq]\n exact h\nexact {p}_take_succ_of_drop h2"
),
));
// ================= D. producer fold normalization =================
push(format!(
"private def {p}_escL (cs : List Char) : String := {fold} (cs.map Char.toString) \"\""
));
push(floored(
&format!(
"private theorem {p}_acc_hom (cs : List String) (acc : String) :\n {fold} cs acc = acc ++ {fold} cs \"\""
),
&format!(
"induction cs generalizing acc with\n| nil => simp [{fold}, {p}_str_append_empty]\n| cons c rest ih =>\n rw [{fold}, {fold}]\n rw [ih (acc + {cls} c), ih (\"\" + {cls} c)]\n apply {p}_str_ext\n simp [{p}_data_append, {p}_data_add, {p}_empty_data, List.append_assoc]"
),
));
push(floored(
&format!("private theorem {p}_escL_nil : {p}_escL [] = \"\""),
&format!("simp [{p}_escL, {fold}]"),
));
push(floored(
&format!(
"private theorem {p}_escL_cons (c : Char) (cs : List Char) :\n {p}_escL (c :: cs) = {cls} (Char.toString c) ++ {p}_escL cs"
),
&format!(
"unfold {p}_escL\nrw [List.map_cons, {fold}, {p}_acc_hom]\napply {p}_str_ext\nsimp [{p}_data_append, {p}_data_add, {p}_empty_data]"
),
));
push(format!(
"private theorem {p}_producer_eq (s : String) : {prod} s = {p}_escL s.toList := rfl"
));
// ================= E. consumer step lemmas =========================
push(floored(
&format!(
"private theorem {p}_step_finish {{s : String}} {{pos segStart : Int}} {{chunks : List String}} {{f : Nat}}\n (hAt : String.charAtAv s pos = some {term_s}) :\n {scan_f} (f + 1) s pos segStart chunks =\n {fin} s (pos + 1) segStart chunks"
),
&format!("simp [{scan_f}, hAt]"),
));
push(floored(
&format!(
"private theorem {p}_step_escape {{s : String}} {{pos segStart : Int}} {{chunks : List String}} {{f : Nat}}\n (hAt : String.charAtAv s pos = some {esc_s}) :\n {scan_f} (f + 1) s pos segStart chunks =\n {esc_f} f s (pos + 1) pos segStart chunks"
),
&format!("simp [{scan_f}, hAt]"),
));
push(floored(
&format!(
"private theorem {p}_step_default {{s : String}} {{pos segStart : Int}} {{chunks : List String}} {{f : Nat}} {{c : Char}}\n (hAt : String.charAtAv s pos = some (Char.toString c))\n (h1 : Char.toString c ≠ {term_s}) (h2 : Char.toString c ≠ {esc_s}) :\n {scan_f} (f + 1) s pos segStart chunks =\n {val_f} f s pos segStart chunks (Char.toString c)"
),
&format!(
"simp only [Char.toString_eq_singleton] at h1 h2\nsimp [{scan_f}, hAt, Char.toString_eq_singleton, h1, h2]"
),
));
push(floored(
&format!(
"private theorem {p}_step_validate {{s : String}} {{pos segStart : Int}} {{chunks : List String}} {{f : Nat}} {{c : Char}}\n (hge : ¬ ((c.toNat : Int) < {t})) :\n {val_f} (f + 1) s pos segStart chunks (Char.toString c) =\n {scan_f} f s (pos + 1) segStart chunks"
),
&format!("simp only [{val_f}]\nrw [{p}_toCode_toString]\nsimp [hge]"),
));
for (idx, pair) in &pairs {
let letter_s = lean_str(&pair.letter.to_string());
let dec_s = lean_str(&pair.decoded.to_string());
push(floored(
&format!(
"private theorem {p}_step_esc_{idx} {{s : String}} {{pos slashPos segStart : Int}} {{chunks : List String}} {{f : Nat}}\n (hAt : String.charAtAv s pos = some {letter_s}) :\n {esc_f} (f + 1) s pos slashPos segStart chunks =\n {scan_f} f s (pos + 1) (pos + 1)\n ((chunks ++ [String.sliceAv s segStart slashPos]) ++ [{dec_s}])"
),
&format!("simp [{esc_f}, hAt]"),
));
}
push(floored(
&format!(
"private theorem {p}_step_esc_uni {{s : String}} {{pos slashPos segStart : Int}} {{chunks : List String}} {{f : Nat}}\n (hAt : String.charAtAv s pos = some {uni_s}) :\n {esc_f} (f + 1) s pos slashPos segStart chunks =\n {uni_f} f s (pos + 1) (pos + 1)\n (chunks ++ [String.sliceAv s segStart slashPos])"
),
&format!("simp [{esc_f}, hAt]"),
));
push(floored(
&format!(
"private theorem {p}_step_unicode {{s : String}} {{pos escapePos : Int}} {{chunks : List String}} {{f : Nat}} {{cp : Int}}\n (hread : {hex_w} s pos 0 0 = some cp) :\n {uni_f} (f + 1) s pos escapePos chunks =\n {cp_f} f s (pos + 4) escapePos chunks cp"
),
&format!("simp [{uni_f}, hread]"),
));
push(floored(
&format!(
"private theorem {p}_high_false {{cp : Int}} (h : ¬ cp ≥ {hi_min}) : {hi_fn} cp = false"
),
&format!("simp [{hi_fn}, h]"),
));
push(floored(
&format!(
"private theorem {p}_low_false {{cp : Int}} (h : ¬ cp ≥ {lo_min}) : {lo_fn} cp = false"
),
&format!("simp [{lo_fn}, h]"),
));
push(floored(
&format!(
"private theorem {p}_step_codepoint {{s : String}} {{pos escapePos : Int}} {{chunks : List String}} {{f : Nat}} {{cp : Int}}\n (hh : {hi_fn} cp = false) (hl : {lo_fn} cp = false) :\n {cp_f} (f + 1) s pos escapePos chunks cp =\n {app_f} f s pos escapePos chunks cp"
),
&format!("simp [{cp_f}, hh, hl]"),
));
push(floored(
&format!(
"private theorem {p}_step_apply {{s : String}} {{pos escapePos : Int}} {{chunks : List String}} {{f : Nat}} {{cp : Int}} {{str : String}}\n (hfc : Char.fromCode cp = some str) :\n {app_f} (f + 1) s pos escapePos chunks cp =\n {scan_f} f s pos pos (chunks ++ [str])"
),
&format!("simp [{app_f}, hfc]"),
));
push(floored(
&format!(
"private theorem {p}_fromCode_small {{m : Nat}} (h : m < 55296) :\n Char.fromCode (m : Int) = some (Char.toString (Char.ofNat m))"
),
"have h1 : ¬ ((m : Int) < 0) := by omega\nhave h2 : ¬ ((m : Int) > 1114111) := by omega\nhave h3 : ¬ ((m : Int) ≥ 55296) := by omega\nsimp [Char.fromCode, h1, h2, h3]",
));
push(floored(
&format!(
"private theorem {p}_readhex_step {{fuel : Nat}} {{s : String}} {{pos acc count : Int}} {{c : Char}} {{rest : List Char}} {{d : Int}}\n (hdrop : s.toList.drop pos.toNat = c :: rest)\n (hv : {hexval} (Char.toString c) = some d)\n (hcount : (count == 4) = false)\n (h0 : 0 ≤ pos) :\n {hex_f} (fuel + 1) s pos acc count =\n {hex_f} fuel s (pos + 1) (acc * 16 + d) (count + 1)"
),
&format!(
"simp only [Char.toString_eq_singleton] at hv\nsimp [{hex_f}, hcount, {p}_charAt_of_drop h0 hdrop, Char.toString_eq_singleton, hv]"
),
));
push(floored(
&format!(
"private theorem {p}_readhex_done {{fuel : Nat}} {{s : String}} {{pos acc : Int}} :\n {hex_f} (fuel + 1) s pos acc 4 = some acc"
),
&format!("simp [{hex_f}]"),
));
push(floored(
&format!(
"private theorem {p}_hexDigit_data :\n ∀ d : Nat, d < 16 → (hexDigit (d : Int)).toList = [(hexDigit (d : Int)).toList.head!]"
),
"decide",
));
push(floored(
&format!(
"private theorem {p}_hexVal_round :\n ∀ d : Nat, d < 16 → {hexval} (Char.toString ((hexDigit (d : Int)).toList.head!)) = some (d : Int)"
),
"decide",
));
// Producer classifier unfolds (hypothesis-guarded).
let ladder_ne_shows: String = ladder_pairs
.iter()
.map(|(_, e)| {
format!(
"\n show ¬ ((c.toNat : Int) = {}) from by omega,",
e.decoded as u32
)
})
.collect();
push(floored(
&format!(
"private theorem {p}_control_print {{c : Char}} (hge : ¬ (c.toNat < {t})) :\n {ctl} (Char.toString c) = Char.toString c"
),
&format!(
"simp only [{ctl}]\nrw [{p}_toCode_toString]\nsimp [{ladder_ne_shows}\n show ¬ ((c.toNat : Int) < {t}) from by omega]"
),
));
{
let hyps: String = cls_pairs
.iter()
.map(|(i, e)| {
format!(
" (h{i} : Char.toString c ≠ {})",
lean_str(&e.decoded.to_string())
)
})
.collect();
let at_hyps: String = cls_pairs.iter().map(|(i, _)| format!(" h{i}")).collect();
let simp_hyps: String = cls_pairs.iter().map(|(i, _)| format!(", h{i}")).collect();
push(floored(
&format!(
"private theorem {p}_classifier_default {{c : Char}}{hyps} :\n {cls} (Char.toString c) = {ctl} (Char.toString c)"
),
&format!(
"simp only [Char.toString_eq_singleton] at{at_hyps}\nsimp [{cls}, Char.toString_eq_singleton{simp_hyps}]"
),
));
}
{
let ladder_hyps: String = ladder_pairs
.iter()
.map(|(i, e)| format!(" (hk{i} : c.toNat ≠ {})", e.decoded as u32))
.collect();
push(floored(
&format!(
"private theorem {p}_control_u {{c : Char}} (h32 : c.toNat < {t}){ladder_hyps} :\n {ctl} (Char.toString c) =\n {prefix_s} + (hexDigit ((c.toNat : Int) / 16) ++ hexDigit ((c.toNat : Int) % 16))"
),
&format!(
"simp only [{ctl}]\nrw [{p}_toCode_toString]\nsimp [{ladder_ne_shows}\n show ((c.toNat : Int) < {t}) from by omega,\n {cce}, AverByte.toHex,\n show ¬ ((c.toNat : Int) < 0) from by omega,\n show ¬ ((c.toNat : Int) > 255) from by omega,\n byteToHex]"
),
));
}
push(floored(
&format!(
"private theorem {p}_finish_shape (s : String) (pos segStart : Int) (chunks : List String) :\n {fin} s (pos + 1) segStart chunks =\n {okc}\n ({strc} (String.intercalate \"\" (chunks ++ [String.sliceAv s segStart pos])))\n (pos + 1)"
),
&format!("simp [{fin}, Int.add_sub_cancel]"),
));
push(floored(
&format!(
"private theorem {p}_ok_eq {{v1 v2 : String}} {{p1 p2 : Int}} (hv : v1 = v2) (hp : p1 = p2) :\n {okc} ({strc} v1) p1 = {okc} ({strc} v2) p2"
),
"rw [hv, hp]",
));
// ================= F. the suffix invariant =========================
push(format!(
"private def {p}_inv (cs : List Char) : Prop :=\n ∀ (s : String) (pos segStart : Int) (chunks : List String) (fuel : Nat),\n 0 ≤ segStart → segStart ≤ pos →\n s.toList.drop pos.toNat = ({p}_escL cs).toList ++ [{term_c}] →\n 2 * ({p}_escL cs).toList.length + 2 ≤ fuel →\n {scan_f} fuel s pos segStart chunks =\n {okc}\n ({strc} (String.intercalate \"\" (chunks ++ [String.sliceAv s segStart pos]) ++ String.ofList cs))\n (pos + ({p}_escL cs).toList.length + 1)"
));
push(floored(
&format!("private theorem {p}_nil_branch : {p}_inv []"),
&format!(
"intro s pos segStart chunks fuel h0 hsp hdrop hfuel\nhave hpos : (0:Int) ≤ pos := by omega\nrw [{p}_escL_nil] at hdrop\nsimp only [{p}_empty_data, List.nil_append] at hdrop\nobtain ⟨f1, rfl⟩ : ∃ f1, fuel = f1 + 1 := ⟨fuel - 1, by omega⟩\nrw [{p}_step_finish ({p}_charAt_of_drop hpos hdrop)]\nrw [{p}_finish_shape]\napply {p}_ok_eq\n· rw [show String.ofList ([] : List Char) = \"\" from rfl, {p}_str_append_empty]\n· have hl0 : ({p}_escL ([] : List Char)).toList.length = 0 := by rw [{p}_escL_nil]; rfl\n omega"
),
));
push(floored(
&format!(
"private theorem {p}_pair_branch (c eL : Char) (dec : String) {{cs : List Char}}\n (ih : {p}_inv cs)\n (hesc : ({cls} (Char.toString c)).toList = [{esc_c}, eL])\n (hdec : dec = Char.toString c)\n (hstep : ∀ (s : String) (pos slashPos segStart : Int) (chunks : List String) (f : Nat),\n String.charAtAv s pos = some (Char.toString eL) →\n {esc_f} (f + 1) s pos slashPos segStart chunks =\n {scan_f} f s (pos + 1) (pos + 1)\n ((chunks ++ [String.sliceAv s segStart slashPos]) ++ [dec])) :\n {p}_inv (c :: cs)"
),
&format!(
"intro s pos segStart chunks fuel h0 hsp hdrop hfuel\nhave hpos : (0:Int) ≤ pos := by omega\nhave hlen : ({p}_escL (c :: cs)).toList.length = 2 + ({p}_escL cs).toList.length := by\n rw [{p}_escL_cons, {p}_data_append, List.length_append, hesc]\n rfl\nrw [{p}_escL_cons, {p}_data_append, hesc] at hdrop\nsimp only [List.cons_append, List.nil_append, List.append_assoc] at hdrop\nhave hn1 : s.toList.drop (pos.toNat + 1) = eL :: (({p}_escL cs).toList ++ [{term_c}]) := {p}_drop_succ_of_drop hdrop\nhave hn2 : s.toList.drop (pos.toNat + 1 + 1) = ({p}_escL cs).toList ++ [{term_c}] := {p}_drop_succ_of_drop hn1\nhave hi1 : s.toList.drop (pos + 1).toNat = eL :: (({p}_escL cs).toList ++ [{term_c}]) := by\n rw [show (pos + 1).toNat = pos.toNat + 1 from by omega]; exact hn1\nhave hi2 : s.toList.drop ((pos + 1) + 1).toNat = ({p}_escL cs).toList ++ [{term_c}] := by\n rw [show ((pos + 1) + 1).toNat = pos.toNat + 1 + 1 from by omega]; exact hn2\nhave hAt0 : String.charAtAv s pos = some (Char.toString {esc_c}) := {p}_charAt_of_drop hpos hdrop\nhave hAt1 : String.charAtAv s (pos + 1) = some (Char.toString eL) := {p}_charAt_of_drop (by omega) hi1\nobtain ⟨f1, rfl⟩ : ∃ f1, fuel = f1 + 1 := ⟨fuel - 1, by omega⟩\nobtain ⟨f2, rfl⟩ : ∃ f2, f1 = f2 + 1 := ⟨f1 - 1, by omega⟩\nrw [{p}_step_escape hAt0]\nrw [hstep s (pos + 1) pos segStart chunks f2 hAt1]\nrw [ih s ((pos + 1) + 1) ((pos + 1) + 1) ((chunks ++ [String.sliceAv s segStart pos]) ++ [dec]) f2\n (by omega) (by omega) hi2 (by omega)]\napply {p}_ok_eq\n· rw [{p}_slice_self, hdec]\n simp only [{p}_inter_snoc, {p}_inter_nil, {p}_str_append_empty, {p}_str_empty_append, {p}_str_append_assoc, {p}_mk_cons]\n· omega"
),
));
// printable branch — generated hypothesis bundle per classifier arm.
{
let hyp_params: String = cls_high
.iter()
.map(|(i, e)| format!(" (hq{i} : c ≠ {})", lean_char(e.decoded)))
.collect();
let mut body = String::new();
body.push_str("intro s pos segStart chunks fuel h0 hsp hdrop hfuel\n");
body.push_str("have hpos : (0:Int) ≤ pos := by omega\n");
for (i, e) in &cls_low {
body.push_str(&format!(
"have hq{i} : c ≠ {} := fun h => by subst h; exact absurd h32 (by decide)\n",
lean_char(e.decoded)
));
}
for (i, e) in &cls_pairs {
body.push_str(&format!(
"have e{i} : Char.toString c ≠ {} := {p}_ts_ne hq{i}\n",
lean_str(&e.decoded.to_string())
));
}
let e_args: String = cls_pairs.iter().map(|(i, _)| format!(" e{i}")).collect();
body.push_str(&format!(
"have hesc : {cls} (Char.toString c) = Char.toString c := by\n rw [{p}_classifier_default{e_args}, {p}_control_print h32]\n"
));
body.push_str(&format!(
"have hlen : ({p}_escL (c :: cs)).toList.length = 1 + ({p}_escL cs).toList.length := by\n rw [{p}_escL_cons, hesc, {p}_data_append, List.length_append, {p}_ts_data]\n rfl\n"
));
body.push_str(&format!(
"rw [{p}_escL_cons, hesc, {p}_data_append, {p}_ts_data] at hdrop\n"
));
body.push_str(
"simp only [List.cons_append, List.nil_append, List.append_assoc] at hdrop\n",
);
body.push_str(&format!(
"have hn1 : s.toList.drop (pos.toNat + 1) = ({p}_escL cs).toList ++ [{term_c}] := {p}_drop_succ_of_drop hdrop\n"
));
body.push_str(&format!(
"have hi1 : s.toList.drop (pos + 1).toNat = ({p}_escL cs).toList ++ [{term_c}] := by\n rw [show (pos + 1).toNat = pos.toNat + 1 from by omega]; exact hn1\n"
));
body.push_str(&format!(
"have hAt0 : String.charAtAv s pos = some (Char.toString c) := {p}_charAt_of_drop hpos hdrop\n"
));
body.push_str("obtain ⟨f1, rfl⟩ : ∃ f1, fuel = f1 + 1 := ⟨fuel - 1, by omega⟩\n");
body.push_str("obtain ⟨f2, rfl⟩ : ∃ f2, f1 = f2 + 1 := ⟨f1 - 1, by omega⟩\n");
body.push_str(&format!(
"rw [{p}_step_default hAt0 e{idx_term} e{idx_esc}]\n"
));
body.push_str(&format!(
"rw [{p}_step_validate (by omega : ¬ ((c.toNat : Int) < {t}))]\n"
));
body.push_str("rw [ih s (pos + 1) segStart chunks f2 h0 (by omega) hi1 (by omega)]\n");
body.push_str(&format!(
"apply {p}_ok_eq\n· rw [{p}_slice_snoc h0 hsp hdrop]\n simp only [{p}_inter_snoc, {p}_inter_nil, {p}_str_append_empty, {p}_str_empty_append, {p}_str_append_assoc, {p}_mk_cons]\n· omega"
));
push(floored(
&format!(
"private theorem {p}_printable_branch {{c : Char}} {{cs : List Char}} (ih : {p}_inv cs)\n (h32 : ¬ c.toNat < {t}){hyp_params} : {p}_inv (c :: cs)"
),
&body,
));
}
// control branch — the hex-escape path (6 consumed chars, 5 scan
// ticks + the separately-fueled readHex micro-run).
{
let ladder_params: String = ladder_pairs
.iter()
.map(|(i, e)| format!(" (hk{i} : c.toNat ≠ {})", e.decoded as u32))
.collect();
let low_params: String = cls_low
.iter()
.map(|(i, e)| format!(" (hq{i} : c ≠ {})", lean_char(e.decoded)))
.collect();
let mut body = String::new();
body.push_str("intro s pos segStart chunks fuel h0 hsp hdrop hfuel\n");
body.push_str("have hpos : (0:Int) ≤ pos := by omega\n");
for (i, e) in &cls_high {
body.push_str(&format!(
"have hq{i} : c ≠ {} := fun h => by subst h; exact absurd h32 (by decide)\n",
lean_char(e.decoded)
));
}
for (i, e) in &cls_pairs {
body.push_str(&format!(
"have e{i} : Char.toString c ≠ {} := {p}_ts_ne hq{i}\n",
lean_str(&e.decoded.to_string())
));
}
body.push_str(
"have hdiv : ((c.toNat : Int)) / 16 = ((c.toNat / 16 : Nat) : Int) := by omega\n",
);
body.push_str(
"have hmod : ((c.toNat : Int)) % 16 = ((c.toNat % 16 : Nat) : Int) := by omega\n",
);
let e_args: String = cls_pairs.iter().map(|(i, _)| format!(" e{i}")).collect();
let hk_args: String = ladder_pairs
.iter()
.map(|(i, _)| format!(" hk{i}"))
.collect();
body.push_str(&format!(
"have hesc : {cls} (Char.toString c) =\n {prefix_s} + (hexDigit ((c.toNat / 16 : Nat) : Int) ++ hexDigit ((c.toNat % 16 : Nat) : Int)) := by\n rw [{p}_classifier_default{e_args}, {p}_control_u h32{hk_args}, hdiv, hmod]\n"
));
body.push_str(&format!(
"have hA := {p}_hexDigit_data (c.toNat / 16) (by omega)\n"
));
body.push_str(&format!(
"have hB := {p}_hexDigit_data (c.toNat % 16) (by omega)\n"
));
body.push_str(&format!(
"have hdataE : ({cls} (Char.toString c)).toList\n = {esc_c} :: {uni_c} :: '0' :: '0' ::\n (hexDigit ((c.toNat / 16 : Nat) : Int)).toList.head! ::\n (hexDigit ((c.toNat % 16 : Nat) : Int)).toList.head! :: [] := by\n rw [hesc, {p}_data_add, {p}_data_append, hA, hB]\n rfl\n"
));
body.push_str(&format!(
"have hlen : ({p}_escL (c :: cs)).toList.length = 6 + ({p}_escL cs).toList.length := by\n rw [{p}_escL_cons, {p}_data_append, List.length_append, hdataE]\n rfl\n"
));
body.push_str(&format!(
"rw [{p}_escL_cons, {p}_data_append, hdataE] at hdrop\n"
));
body.push_str(
"simp only [List.cons_append, List.nil_append, List.append_assoc] at hdrop\n",
);
for k in 1..=6 {
let prev = if k == 1 {
"hdrop".to_string()
} else {
format!("hn{}", k - 1)
};
body.push_str(&format!("have hn{k} := {p}_drop_succ_of_drop {prev}\n"));
}
let hex_a = "(hexDigit ((c.toNat / 16 : Nat) : Int)).toList.head!";
let hex_b = "(hexDigit ((c.toNat % 16 : Nat) : Int)).toList.head!";
let tail = format!("(({p}_escL cs).toList ++ [{term_c}])");
let suffixes: [String; 5] = [
format!("{uni_c} :: '0' :: '0' :: {hex_a} :: {hex_b} :: {tail}"),
format!("'0' :: '0' :: {hex_a} :: {hex_b} :: {tail}"),
format!("'0' :: {hex_a} :: {hex_b} :: {tail}"),
format!("{hex_a} :: {hex_b} :: {tail}"),
format!("{hex_b} :: {tail}"),
];
let pos_forms: [&str; 5] = [
"(pos + 1)",
"((pos + 1) + 1)",
"(((pos + 1) + 1) + 1)",
"((((pos + 1) + 1) + 1) + 1)",
"(((((pos + 1) + 1) + 1) + 1) + 1)",
];
for k in 1..=5usize {
let nat_form = (0..k).map(|_| " + 1").collect::<String>();
body.push_str(&format!(
"have hi{k} : s.toList.drop {}.toNat = {} := by\n rw [show {}.toNat = pos.toNat{nat_form} from by omega]; exact hn{k}\n",
pos_forms[k - 1],
suffixes[k - 1],
pos_forms[k - 1],
));
}
body.push_str(&format!(
"have hi6 : s.toList.drop (((pos + 1) + 1) + 4).toNat = ({p}_escL cs).toList ++ [{term_c}] := by\n rw [show (((pos + 1) + 1) + 4).toNat = pos.toNat + 1 + 1 + 1 + 1 + 1 + 1 from by omega]; exact hn6\n"
));
body.push_str(&format!(
"have hAt0 : String.charAtAv s pos = some (Char.toString {esc_c}) := {p}_charAt_of_drop hpos hdrop\n"
));
body.push_str(&format!(
"have hAt1 : String.charAtAv s (pos + 1) = some (Char.toString {uni_c}) := {p}_charAt_of_drop (by omega) hi1\n"
));
for k in 1..=5 {
let prev = if k == 1 {
"fuel".to_string()
} else {
format!("f{}", k - 1)
};
body.push_str(&format!(
"obtain ⟨f{k}, rfl⟩ : ∃ f{k}, {prev} = f{k} + 1 := ⟨{prev} - 1, by omega⟩\n"
));
}
body.push_str(&format!("rw [{p}_step_escape hAt0]\n"));
body.push_str(&format!("rw [{p}_step_esc_uni hAt1]\n"));
body.push_str(&format!(
"have hread : {hex_w} s ((pos + 1) + 1) 0 0 = some ((c.toNat : Int)) := by\n unfold {hex_w}\n rw [{p}_readhex_step hi2 (by decide : {hexval} (Char.toString '0') = some 0)\n (by decide) (by omega : (0:Int) ≤ (pos + 1) + 1)]\n rw [show Int.natAbs (4 - (0:Int)) = 3 + 1 from by decide]\n rw [show ((0:Int) + 1) = 1 from by decide]\n rw [{p}_readhex_step hi3 (by decide : {hexval} (Char.toString '0') = some 0)\n (by decide) (by omega : (0:Int) ≤ ((pos + 1) + 1) + 1)]\n rw [show ((3:Nat)) = 2 + 1 from by decide]\n rw [show ((1:Int) + 1) = 2 from by decide]\n rw [{p}_readhex_step hi4 ({p}_hexVal_round (c.toNat / 16) (by omega))\n (by decide) (by omega : (0:Int) ≤ (((pos + 1) + 1) + 1) + 1)]\n rw [show ((2:Nat)) = 1 + 1 from by decide]\n rw [show ((2:Int) + 1) = 3 from by decide]\n rw [{p}_readhex_step hi5 ({p}_hexVal_round (c.toNat % 16) (by omega))\n (by decide) (by omega : (0:Int) ≤ ((((pos + 1) + 1) + 1) + 1) + 1)]\n rw [show ((1:Nat)) = 0 + 1 from by decide]\n rw [show ((3:Int) + 1) = 4 from by decide]\n rw [{p}_readhex_done]\n congr 1\n omega\n"
));
body.push_str(&format!("rw [{p}_step_unicode hread]\n"));
body.push_str(&format!(
"rw [{p}_step_codepoint ({p}_high_false (by omega)) ({p}_low_false (by omega))]\n"
));
body.push_str(&format!(
"rw [{p}_step_apply ({p}_fromCode_small (by omega : c.toNat < 55296))]\n"
));
body.push_str("rw [Char.ofNat_toNat]\n");
body.push_str(
"rw [ih s (((pos + 1) + 1) + 4) (((pos + 1) + 1) + 4)\n ((chunks ++ [String.sliceAv s segStart pos]) ++ [Char.toString c]) f5\n (by omega) (by omega) hi6 (by omega)]\n",
);
body.push_str(&format!(
"apply {p}_ok_eq\n· rw [{p}_slice_self]\n simp only [{p}_inter_snoc, {p}_inter_nil, {p}_str_append_empty, {p}_str_empty_append, {p}_str_append_assoc, {p}_mk_cons]\n· omega"
));
// TEST-ONLY (`AVER_PROOF_ESCAPE_SABOTAGE`): replace the
// control branch's tactic block with a no-op so the floor's
// behaviour is observable end-to-end — the branch theorem
// falls to its caught `sorry` (budget pin flips loud-red,
// `lake build` still SUCCEEDS), proving a template regression
// can never be a hard build error. Mirrors the quarantine
// lane's `AVER_PROOF_LANE_SABOTAGE` hook.
let body = if std::env::var("AVER_PROOF_ESCAPE_SABOTAGE")
.map(|v| !v.is_empty())
.unwrap_or(false)
{
"skip".to_string()
} else {
body
};
push(floored(
&format!(
"private theorem {p}_control_branch {{c : Char}} {{cs : List Char}} (ih : {p}_inv cs)\n (h32 : c.toNat < {t}){ladder_params}{low_params} : {p}_inv (c :: cs)"
),
&body,
));
}
// chunk invariant — the by_cases classification ladder over the
// pinned escape table.
{
let mut body = String::new();
body.push_str("intro cs\n");
body.push_str("induction cs with\n");
body.push_str(&format!("| nil => exact {p}_nil_branch\n"));
body.push_str("| cons c cs ih =>\n");
for (i, e) in &cls_pairs {
body.push_str(&format!(
" by_cases hq{i} : c = {}\n · subst hq{i}\n exact {p}_pair_branch {} {} {} ih (by decide) rfl\n (fun _ _ _ _ _ _ hAt => {p}_step_esc_{i} hAt)\n",
lean_char(e.decoded),
lean_char(e.decoded),
lean_char(e.letter),
lean_str(&e.decoded.to_string()),
));
}
for (i, e) in &ladder_pairs {
body.push_str(&format!(
" by_cases hk{i} : c.toNat = {}\n · have hc : c = {} := by rw [{p}_char_eq_of_toNat hk{i}]\n subst hc\n exact {p}_pair_branch {} {} {} ih (by decide) rfl\n (fun _ _ _ _ _ _ hAt => {p}_step_esc_{i} hAt)\n",
e.decoded as u32,
lean_char(e.decoded),
lean_char(e.decoded),
lean_char(e.letter),
lean_str(&e.decoded.to_string()),
));
}
let hk_args: String = ladder_pairs
.iter()
.map(|(i, _)| format!(" hk{i}"))
.collect();
let low_args: String = cls_low.iter().map(|(i, _)| format!(" hq{i}")).collect();
let high_args: String = cls_high.iter().map(|(i, _)| format!(" hq{i}")).collect();
body.push_str(&format!(
" by_cases hctl : c.toNat < {t}\n · exact {p}_control_branch ih hctl{hk_args}{low_args}\n · exact {p}_printable_branch ih hctl{high_args}"
));
push(floored(
&format!("private theorem {p}_chunk_inv : ∀ cs : List Char, {p}_inv cs"),
&body,
));
}
// ================= G. law glue (the proof body) ====================
let glue = format!(
"have hdata : {subj}.toList = {open_c} :: (({p}_escL {n}.toList).toList ++ [{term_c}]) := by\n rw [{p}_data_add, {p}_data_add, {p}_producer_eq]\n rfl\nshow {scan_f} (averStringPosFuel {subj} 1 {rank}) {subj} 1 1 [] = _\nrw [{p}_chunk_inv {n}.toList {subj} 1 1 [] (averStringPosFuel {subj} 1 {rank})\n (by omega) (by omega)\n (by rw [hdata]; rfl)\n (by simp [averStringPosFuel, hdata]; omega)]\nrw [{p}_slice_self]\nhave hval : String.intercalate \"\" ([] ++ [(\"\" : String)]) ++ String.ofList {n}.toList = {n} := by\n simp [{p}_inter_single, {p}_str_empty_append, {p}_mk_data_self]\nrw [hval]\nhave hpos : ((1 : Int) + (({p}_escL {n}.toList).toList.length : Int) + 1) =\n ((({prod_text}).length : Int) + 2) := by\n rw [{p}_producer_eq]\n show (1 : Int) + (({p}_escL {n}.toList).toList.length : Int) + 1 = ((({p}_escL {n}.toList).toList.length : Int) + 2)\n omega\nrw [hpos]",
open_c = lean_char(open_char(law)?),
);
let mut proof_lines = vec![format!(" intro {n}"), " first".to_string()];
for (i, line) in glue.lines().enumerate() {
if i == 0 {
proof_lines.push(format!(" | ({line}"));
} else if line.is_empty() {
proof_lines.push(String::new());
} else {
proof_lines.push(format!(" {line}"));
}
}
proof_lines.push(" done)".to_string());
proof_lines.push(" | sorry".to_string());
Some(AutoProof {
support_lines: support,
body: crate::codegen::lean::tactic_ir::Tactic::raw(proof_lines),
replaces_theorem: false,
})
}
/// The opening char of the law's subject string (`<open> + escape(s)
/// + <terminator>`). The detector validated it's a 1-char literal.
fn open_char(law: &VerifyLaw) -> Option<char> {
let Expr::FnCall(_, lhs_args) = &law.lhs.node else {
return None;
};
let Expr::BinOp(crate::ast::BinOp::Add, open_prod, _) = &lhs_args.first()?.node else {
return None;
};
let Expr::BinOp(crate::ast::BinOp::Add, open_lit, _) = &open_prod.node else {
return None;
};
let Expr::Literal(crate::ast::Literal::Str(s)) = &open_lit.node else {
return None;
};
s.chars().next()
}