init

formal source

  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