IndisputableMonolith.VM.State

   1import Mathlib
   2import IndisputableMonolith.Config.Flags
   3import IndisputableMonolith.LNAL.Registers
   4import IndisputableMonolith.LNAL.VM
   5
   6namespace IndisputableMonolith.VM
   7
   8open IndisputableMonolith
   9open IndisputableMonolith.LNAL
  10
  11private def flags : Config.Flags := Config.default
  12
  13/-- Feature flag mirror for the VM module. -/
  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. -/
  48def lStep (P : LProgram) (s : LState) : LState :=
  49  let base' := LNAL.lStep P s.base
  50  let boundary := base'.winIdx8 = 0
  51  let windowIdx := if boundary then s.windowIdx + 1 else s.windowIdx
  52  let s' := { s with base := base', windowIdx := windowIdx }
  53  if enableV2Certs then
  54    jBudgetUpdate s'
  55  else
  56    { s' with winJ := s.winJ, winJPrev := s.winJPrev }
  57
  58/-- Eight-tick cycle helper derived from the wrapped stepper. -/
  59def lCycle (P : LProgram) (s : LState) : LState :=
  60  Nat.iterate (lStep P) 8 s
  61
  62end IndisputableMonolith.VM
  63