The marker every Lean runtime panic prints into captured build output.
Empirically pinned against real lake build transcripts (both panic
sites below produce it):
Panic message baked into every fuel wrapper’s exhaustion arm. This is a
SOUNDNESS marker, not just a diagnostic: Lean’s panic! does NOT abort
evaluation — it prints PANIC at … <this message> and returns the type’s
default value, so under native_decide an exhausted-fuel sample reduces
both sides of a model-vs-model equation to default and the kernel
certifies a vacuous (possibly FALSE) equality with lake still exiting 0.
aver proof --check therefore scans captured lake output for panic lines
(crate::codegen::lean::count_model_panic_lines) and treats any hit as
a hard check failure. The scan keys on Lean’s generic PANIC at line
marker — every prelude panic! site shares the vacuity vector, not just
this one — so this constant is purely the emission message; changing it
cannot blind the gate.
aver proof --explain residual probe — turns an emitted main law theorem’s
source lines into a normalization-only twin so Lean reports its residual
(unsolved goals). Used by the --check harness in the aver binary.
aver proof --explain residual probe: turn an emitted main law theorem’s
source lines into a normalization-only twin so Lean reports its residual
(unsolved goals). Re-exported up to codegen::lean for the --check
harness in the aver binary; see induction::residual_probe_body.
aver proof --explain residual probe. Given the EMITTED Lean source lines of
ONE main law theorem (the theorem … := by line through its last arm), render
a NORMALIZATION-ONLY twin whose body strips the closing tactic cascade so
Lean’s elaborator reports the law’s residual (unsolved goals) instead of
closing it with sorry/omega/split. The leftover goal IS what a
Lemma-Calculation agent applies the IH against, so the cons arm’s IH must stay
in canonical recursive form: each arm is replaced by (try simp only [<the theorem's own def simp set>, List.cons_append]) — def-unfold + cons-peel ONLY,
no done/omega/split/simp_all/| sorry.