def
definition
def or abbrev
lStep
show as:
view Lean formalization →
formal statement (Lean)
48def lStep (P : LProgram) (s : LState) : LState :=
proof body
Definition body.
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. -/