def
definition
commitEvent
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.VM.Commit on GitHub at line 12.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
9open IndisputableMonolith.LNAL
10
11/-- Predicate witnessing a conservative COMMIT boundary under the v2 flag. -/
12def commitEvent (s : LState) : Bool :=
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