  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.