def
definition
mockProgram
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.VM.Commit on GitHub at line 16.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
13 enableV2Certs && s.winJ ≤ s.winJPrev
14
15/-- Mock program used for cycle evaluation examples. -/
16@[simp] def mockProgram : LProgram := fun _ => { op := Opcode.BALANCE }
17
18/-- Baseline augmented state for examples. -/
19@[simp] def mockState : LState := LState.init Reg6.zero Aux5.zero
20
21/-- Smoke-test cycle demonstration for tooling. -/
22def cycleReport : String :=
23 let final := lCycle mockProgram mockState
24 s!"cycle windowIdx={final.windowIdx}, winJ={final.winJ}, commit={commitEvent final}"
25
26#eval cycleReport
27
28end IndisputableMonolith.VM