The call-aware monadic-interpreter stepper, over any PureExpr

Calls.stepCmd π steps a CmdExt P command: a base command through the generic stepBaseCmdStore, and a .call as an exact run-to-completion of the callee body in the same effect monad, at strictly smaller fuel: a structured body through the Imperative driver runInterp, a CFG body through the CFG driver runInterpCFG. It follows the reference rule Calls.EvalCmdExtE.call_sem: callEntryStore is its InitCallFrame, the argument evaluation and out read its other CallEntry premises, the trailing readVarList/bindPositional pair its CallExit, and the callee's non-free pre- and postconditions are emitted as assertion events (never adjudicated) around the body run.

An unresolved callee and a positional arity mismatch are refused.

It also defines, over this stepper, the target-event predicates assertFailureHalt and targetReached and the replay verdicts genuine, genuineFeasible, genuineEnforced.

Lemmas about these definitions are in InterpreterCallProps.lean.

Executable call helpers

def Imperative.Calls.evalBoundedList {P : PureExpr} [InterpLang P] (fuel : Nat) (factory : InterpLang.RFactory P) (store : RStore P) : List P.Expr → Option (List P.Expr)

Evaluate a list of expressions with the language's fuel-bounded evaluator, short-circuiting to none if any does not reduce.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.Calls.evalBoundedList fuel factory store [] = some []

def Imperative.Calls.storeUpdate {P : PureExpr} [DecidableEq P.Ident] {V : Type u_2} (σ : P.Ident → Option V) (x : P.Ident) (v : V) : P.Ident → Option V

A point update of a store of any value type (runtime or semantic).

Equations

• Imperative.Calls.storeUpdate σ x v y = if y = x then some v else σ y

theorem Imperative.Calls.storeUpdate_eq_update {P : PureExpr} [DecidableEq P.Ident] (σ : SemanticStore P) (x : P.Ident) (v : P.Val) : storeUpdate σ x v = σ.update x v

On semantic stores, storeUpdate is SemanticStore.update.

def Imperative.Calls.bindPositional {P : PureExpr} [DecidableEq P.Ident] {V : Type u_2} (store : P.Ident → Option V) (names : List P.Ident) (values : List V) : P.Ident → Option V

Positionally bind names to values on top of a store (point updates, in order). Extra names or extra values are dropped.

Equations

• Imperative.Calls.bindPositional store (name :: names_2) (value :: values_2) = Imperative.Calls.bindPositional (Imperative.Calls.storeUpdate store name value) names_2 values_2
• Imperative.Calls.bindPositional store names values = store

def Imperative.Calls.readVarList {P : PureExpr} {V : Type u_2} (store : P.Ident → Option V) : List P.Ident → Option (List V)

Read a list of variables from a store, short-circuiting to none if any is undefined.

Equations

• Imperative.Calls.readVarList store [] = some []
• Imperative.Calls.readVarList store (name :: rest) = match store name with | some value => Option.map (fun (x : List V) => value :: x) (Imperative.Calls.readVarList store rest) | none => none

def Imperative.Calls.writeBackTyped {P : PureExpr} {RF : Type} (ops : ReplayValueOps P RF) (f : RF) (olds vals : List P.Expr) : Bool

The typed write-back check of a call: every written-back value passes the runtime value check isValue and has the type of the value its target held before the call (sameType), pairing the targets' previous values olds with the written values vals positionally.

Equations

• Imperative.Calls.writeBackTyped ops f olds vals = (olds.zip vals).all fun (x : P.Expr × P.Expr) => match x with | (o, v) => ops.isValue f v && ops.sameType f o v

def Imperative.Calls.withOldSnapshotsV {P : PureExpr} [DecidableEq P.Ident] [HasOldIdent P] {V : Type u_2} (snapshot : List P.Ident) (σ : P.Ident → Option V) : P.Ident → Option V

withOldSnapshots over stores of any value type (runtime or semantic): every name of snapshot is also readable under its old name.

Equations

• Imperative.Calls.withOldSnapshotsV snapshot σ id = match List.find? (fun (g : P.Ident) => Imperative.HasOldIdent.mkOld g == id) snapshot with | some g => σ g | none => σ id

theorem Imperative.Calls.withOldSnapshotsV_eq {P : PureExpr} [DecidableEq P.Ident] [HasOldIdent P] (snapshot : List P.Ident) (σ : SemanticStore P) : withOldSnapshotsV snapshot σ = withOldSnapshots snapshot σ

On semantic stores, withOldSnapshotsV is withOldSnapshots.

def Imperative.Calls.rDefaultAssertEvents {P : PureExpr} {RF : Type} (rf : RF) (σ : RStore P) (checks : ListMap String (Check P)) : List (REvent P RF)

The runtime counterpart of defaultAssertEvents: the non-free clauses of checks as runtime assert events at the runtime snapshot (rf, σ).

Equations

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

def Imperative.Calls.callEntryStore {P : PureExpr} [DecidableEq P.Ident] [HasOldIdent P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] (p : Procedure P (CmdExt P) Hdr) {V : Type u_2} (inputVals outOnlyVals : List V) : P.Ident → Option V

The callee's entry frame σAO: a fresh, empty store in which the input formals hold the evaluated input values, the output-only formals hold the caller's out-actual values, and each inout formal is snapshotted under old. Executable counterpart of InitCallFrame.

Equations

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

The stepper

def Imperative.Calls.runCallee {P : PureExpr} [DecidableEq P.Ident] [HasBool P] [DecidableEq P.Expr] [InterpLang P] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (step : StepCmdM P (CmdExt P) m) (procName : String) (body : Body P (CmdExt P)) (fac : InterpLang.RFactory P) (fuel : Nat) (entryStore : RStore P) : m (RStore P)

The callee body run of a .call, from the entry frame entryStore at the caller's factory fac and driver fuel fuel, over the command stepper step; it returns the body's final store. A structured body ss runs as .block "" ss through runInterp, and its final store is the store of the terminal configuration. A CFG body g runs through runInterpCFG from its entry block, each command through step at the running store, and its final store is the halting store projected through the entry frame (projectStore), as in BigStepE. A body that does not end in a terminal configuration stops with programCallBodyExited.

Equations

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

@[irreducible]

def Imperative.Calls.stepCmd {P : PureExpr} [DecidableEq P.Ident] [HasOldIdent P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] [HasBool P] [DecidableEq P.Expr] [InterpLang P] [HasFvar P] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (π : String → Option (Procedure P (CmdExt P) Hdr)) (depth fuel : Nat) (env : IEnv P) (cmd : CmdExt P) : m (IConfig P (CmdExt P))

The call-aware command stepper, generic over the effect monad m. depth is the remaining call-depth budget: how many more calls may nest inside this one. Base commands go through stepBaseCmdStore (presented as .terminal). .call at fuel fuel' + 1 stops with callDepthExceeded at budget 0; at budget depth' + 1 it evaluates its arguments, builds the callee frame, emits the non-free preconditions with their site metadata (checksAtCall md), runs the callee body (runCallee) at the caller's factory with this stepper baked at budget depth' and fuel fuel', emits the non-free postconditions at the callee's final store, checks that each output has the type of the value its target held (writeBackTyped; illTypedValue otherwise), and writes the outputs back.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.Calls.stepCmd π depth 0 env (Imperative.CmdExt.call procName args md) = throw Imperative.StopReason.replayFuelExhausted
• Imperative.Calls.stepCmd π 0 depth'.succ env (Imperative.CmdExt.call procName args md) = throw Imperative.StopReason.callDepthExceeded

def Imperative.Calls.runCallInterp {P : PureExpr} [DecidableEq P.Ident] [HasOldIdent P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] [HasBool P] [DecidableEq P.Expr] [InterpLang P] [HasFvar P] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (π : String → Option (Procedure P (CmdExt P) Hdr)) (fuel : Nat) (cfg : IConfig P (CmdExt P)) (maxCallDepth : Nat := defaultMaxCallDepth) : m (IConfig P (CmdExt P))

The call-aware driver: runInterp over stepCmd π maxCallDepth, nesting at most maxCallDepth calls.

Equations

• Imperative.Calls.runCallInterp π fuel cfg maxCallDepth = Imperative.runInterp (Imperative.Calls.stepCmd π maxCallDepth) fuel cfg

Target-event predicates

def Imperative.Calls.assertFailureHalt {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] (target : AssertId P) (fuel : Nat) : IEvent P → Bool

The halting predicate: fire on the event matching the target obligation id (label and md) whose recorded condition evaluates, under the bounded evaluator, to the literal that witnesses the obligation, up to metadata (InterpLang.eqModuloMeta): ff (a failing assertion) for an .assert, tt (a reached cover) for a .cover.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.Calls.assertFailureHalt target fuel x✝ = false

def Imperative.Calls.targetReached {P : PureExpr} [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] (target : AssertId P) : IEvent P → Bool

Target-id match of an event (an .assert/.cover with the target's label and metadata), with no evaluation of the condition.

Equations

• Imperative.Calls.targetReached target (Imperative.REvent.assert arg) = (target.label == arg.label && decide (target.md = arg.metadata))
• Imperative.Calls.targetReached target (Imperative.REvent.cover arg) = (target.label == arg.label && decide (target.md = arg.metadata))
• Imperative.Calls.targetReached target x✝ = false

def Imperative.Calls.targetReachedE {P : PureExpr} [DecidableEq P.Expr] [DecidableEq P.Ident] (target : AssertId P) : Event P → Bool

Target-id match of a semantic event, with no evaluation of the condition: the semantic counterpart of targetReached.

Equations

• Imperative.Calls.targetReachedE target (Imperative.Event.assert arg) = (target.label == arg.label && decide (target.md = arg.metadata))
• Imperative.Calls.targetReachedE target (Imperative.Event.cover arg) = (target.label == arg.label && decide (target.md = arg.metadata))
• Imperative.Calls.targetReachedE target x✝ = false

Replay verdicts over the call-aware stepper

def Imperative.Calls.targetInterrupt {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] (target : AssertId P) (fuel : Nat) : IEvent P → Option StopReason

Production stop hook, interrupt only: throw .interrupted at a failing target occurrence.

Equations

• Imperative.Calls.targetInterrupt target fuel ev = if Imperative.Calls.assertFailureHalt target fuel ev = true then some (Imperative.StopReason.interrupted "target failure reached") else none

def Imperative.Calls.enforceInterrupt {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] (target : AssertId P) (fuel : Nat) : IEvent P → Option StopReason

Production stop hook: targetInterrupt, plus a throw on an .assume not evaluating to tt up to metadata (InterpLang.boolLit?).

Equations

• One or more equations did not get rendered due to their size.
• Imperative.Calls.enforceInterrupt target fuel ev = if Imperative.Calls.assertFailureHalt target fuel ev = true then some (Imperative.StopReason.interrupted "target failure reached") else none

def Imperative.Calls.PathFeasible {P : PureExpr} [HasBool P] [InterpLang P] (fuel : Nat) (evs : List (IEvent P)) : Prop

Path-feasibility of a replay trace: every .assume event evaluates under the bounded evaluator to tt up to metadata (InterpLang.boolLit?).

Equations

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

def Imperative.Calls.replayWith {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [HasOldIdent P] [HasFvar P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] (cex : CexA P (CmdExt P)) (target : AssertId P) (fuel : Nat) (π : String → Option (Procedure P (CmdExt P) Hdr) := fun (x : String) => none) (maxCallDepth : Nat := defaultMaxCallDepth) : CEValidationVerdict StopReason

Strict record-only replay of cex through runCallInterp π at fuel fuel and call-depth limit maxCallDepth, halting on the target id.

Equations

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

def Imperative.Calls.genuine {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [HasOldIdent P] [HasFvar P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] (π : String → Option (Procedure P (CmdExt P) Hdr)) (target : AssertId P) (fuel : Nat) (cex : CexA P (CmdExt P)) (maxCallDepth : Nat := defaultMaxCallDepth) : Prop

Genuineness: cex replays, at fuel fuel and call-depth limit maxCallDepth, to the target failure.

Equations

• Imperative.Calls.genuine π target fuel cex maxCallDepth = (Imperative.Calls.replayWith cex target fuel π maxCallDepth = Imperative.CEValidationVerdict.genuine)

def Imperative.Calls.genuineFeasible {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [HasOldIdent P] [HasFvar P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] (π : String → Option (Procedure P (CmdExt P) Hdr)) (target : AssertId P) (fuel : Nat) (cex : CexA P (CmdExt P)) (maxCallDepth : Nat := defaultMaxCallDepth) : Prop

Genuineness with path-feasibility of the enforcing production run's trace.

Equations

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

def Imperative.Calls.genuineEnforced {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [HasOldIdent P] [HasFvar P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] (π : String → Option (Procedure P (CmdExt P) Hdr)) (target : AssertId P) (fuel : Nat) (cex : CexA P (CmdExt P)) (maxCallDepth : Nat := defaultMaxCallDepth) : Prop

Genuineness of the enforcing production run.

Equations

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