`lStep`

definition

show as: view math explainer →

module: IndisputableMonolith.VM.State
domain: VM
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.VM.State on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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.