structure
definition
LState
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.VM.State on GitHub at line 17.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
14def enableV2Certs : Bool := flags.enableV2Certs
15
16/-- VM state wrapper that tracks per-window budgeting for vNext certificates. -/
17structure LState where
18 /-- Base LNAL VM state (legacy semantics). -/
19 base : LNAL.LState
20 /-- Monotone window counter (increments every eight ticks). -/
21 windowIdx : Nat
22 /-- Current window J budget accumulator. -/
23 winJ : Nat
24 /-- Previous window J budget snapshot. -/
25 winJPrev : Nat
26deriving Repr
27
28namespace LState
29
30/-- Initialize the augmented VM state from legacy registers. -/
31@[simp] def init (reg6 : Reg6) (aux5 : Aux5) : LState :=
32 let base := LNAL.LState.init reg6 aux5
33 { base := base, windowIdx := 0, winJ := 0, winJPrev := 0 }
34
35/-- Detect if the current window budget has been depleted. -/
36def winJZero (s : LState) : Bool := s.winJ = 0
37
38end LState
39
40/-- Update the J budget accumulator, rolling snapshots at window boundaries. -/
41def jBudgetUpdate (s : LState) : LState :=
42 let boundary := s.base.winIdx8 = 0
43 let winJPrev := if boundary then s.winJ else s.winJPrev
44 let winJ := if boundary then 0 else s.winJ + 1
45 { s with winJ := winJ, winJPrev := winJPrev }
46
47/-- Wrapped small-step that preserves legacy semantics while tracking vNext counters. -/