Persistent source before_terminator counters/configuration without a second monotonic clock. The clock-bearing Control is a transient view assembled from these fields and the single actual runtime clock.

structure Miri.Interpreter.TerminatorControl.Configuration : Type

• gcInterval : UInt32
• preemptionRateBits : UInt64
• checkedArithmetic : Bool

structure Miri.Interpreter.TerminatorControl.Counters : Type

• basicBlockCount : UInt64
• sinceGc : UInt32
• configuration : Configuration

def Miri.Interpreter.TerminatorControl.initial (config : Configuration) : Counters

Equations

• Miri.Interpreter.TerminatorControl.initial config = { basicBlockCount := 0, sinceGc := 0, configuration := config }

def Miri.Interpreter.TerminatorControl.view {Host : Type} (counters : Counters) (clock : Clock.Monotonic Host) : TerminatorMachine.Control Host

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.TerminatorControl.fromView {Host : Type} (control : TerminatorMachine.Control Host) : Counters

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Miri.Interpreter.TerminatorControl.view_fromView {Host : Type} (control : TerminatorMachine.Control Host) : view (fromView control) control.monotonic = control

@[simp]

theorem Miri.Interpreter.TerminatorControl.fromView_view {Host : Type} (counters : Counters) (clock : Clock.Monotonic Host) : fromView (view counters clock) = counters