`flags`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.VM.State on GitHub at line 11.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   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 :=

papers checked against this theorem

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