The monadic interpreter — one small-step engine

A single small-step evaluation engine over the imperative semantics, written tagless-final against InterpEffects, which bundles the two axes the engine abstracts over as capabilities of the monad m:

• nondeterminism — choose produces a value of a requested type (P.Ty): the oracle instance pops it from the remaining oracle tail, the symbolic instance mints a fresh variable, a random instance samples;
• observation — emit observes an Event; the replay instance records it in its trace and stops only when its configured stop hook fires on the event, so the engine itself never polls a predicate.

Expression evaluation is not an axis (it does not vary per instance): the fuel-bounded evaluator lives in the language typeclass InterpLang.boundedEval (Core: Core.evalBounded, never the unbounded P.eval), which the engine applies directly.

The engine mirrors the reference event-trace relation EvalCmdE/StepStmtE faithfully: .assert/.assume/.cover emit their unevaluated condition and runtime snapshot (Cmd.rEmittedEvents) and skip; target-detection sits on top of that faithful image (in the instance's emit).

Lemmas about the engine are in InterpreterProps.lean.

class Imperative.InterpEffects (P : PureExpr) [InterpLang P] (m : Type → Type) : Type 1

The two axes the monadic interpreter abstracts over, as capabilities of m.

choose returns m P.Expr (not Option): "cannot choose" (oracle exhausted, ill-typed) is routed through the monad's error channel, and the requested P.Ty covers guards too (a Boolean guard is a value of HasBool.boolTy). emit observes an event and may record instance-local state. branch resolves a deterministic guard whose value is not a Boolean literal; its default throws, as the reference semantics prescribes.

• choose : InterpLang.RFactory P → RStore P → P.Ty → m P.Expr

  Resolve one nondeterministic choice: a runtime value of the requested type.

• emit : IEvent P → m Unit

  Observe one runtime event.

• branch [MonadExcept StopReason m] (factory : InterpLang.RFactory P) (store : RStore P) (value : P.Expr) : m Bool

  Resolve a deterministic guard that evaluated to a value that is neither HasBool.tt nor HasBool.ff: true takes the then-branch (loop entry), false the else-branch (loop exit). By default it throws expressionWasNotBoolean, since the reference semantics has no step there; a symbolic instance may fork instead.

@[reducible, inline]

abbrev Imperative.StepCmdM (P : PureExpr) [InterpLang P] (CmdT : Type) (m : Type → Type) : Type

A monadic per-command stepper: given the current fuel and Env, it produces the configuration the command becomes, emitting events and signalling "cannot continue" through the monad's error channel (no result Option). Returning an IConfig rather than a store leaves room for a stepper that splices a callee body into the configuration; the steppers in this development run a call to completion, as the reference semantics does, and return .terminal.

Equations

• Imperative.StepCmdM P CmdT m = (Nat → Imperative.IEnv P → CmdT → m (Imperative.IConfig P CmdT))

def Imperative.stepBaseCmdStore {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (fuel : Nat) (factory : InterpLang.RFactory P) (store : IStore P) (cmd : Cmd P) : m (IStore P)

Generic base-command stepper for Cmd P. Deterministic .init/.set reduce their RHS through InterpLang.boundedEval; nondeterministic .init draws a typed value through choose; .assert/.assume/.cover emit their captured condition (via Cmd.rEmittedEvents) and leave the store unchanged, exactly as EvalCmdE.

Nondeterministic .set x := * (a havoc x) looks up x's current value (programSetTargetUndefined if x is unbound), takes its type through InterpLang.typeOf (unsupportedNondetSet if the type is unknown), draws a value of that type through choose, and applies the same isValue/sameType checks as a deterministic .set (illTypedValue otherwise).

Equations

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

def Imperative.baseStepCmd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] : StepCmdM P (Cmd P) m

The base config-level command stepper (for CmdT = Cmd P): run the atomic base command via stepBaseCmdStore and present the result as a .terminal configuration.

Equations

• Imperative.baseStepCmd fuel env cmd = do let store ← Imperative.stepBaseCmdStore fuel env.factory env.store cmd pure (Imperative.IConfig.terminal { store := store, factory := env.factory })

def Imperative.resolveGuard {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (fuel : Nat) (env : IEnv P) : ExprOrNondet P → m Bool

Resolve a guard to a branch: true takes the then-branch (loop entry), false the else-branch (loop exit). A deterministic guard is evaluated with InterpLang.boundedEval, a nondeterministic one draws a value of the Boolean type through choose. The value must be HasBool.tt or HasBool.ff up to metadata (InterpLang.boolLit?); any other evaluated value is handed to InterpEffects.branch (concrete instances throw expressionWasNotBoolean there), any other chosen value is an error (expectedBooleanChoice).

Equations

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

def Imperative.stepInterp {P : PureExpr} {CmdT : Type} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [CmdDefs P CmdT] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (stepCmd : StepCmdM P CmdT m) (fuel : Nat) : IConfig P CmdT → m (IConfig P CmdT)

One small step over IConfig, monadic and event-emitting: it resolves nondeterminism and events through InterpEffects, evaluates expressions with InterpLang.boundedEval, and delegates commands to stepCmd. Guards are resolved by resolveGuard.

A block opens with the frame ScopeFrame.opened of the current store; a step of a block's inner configuration updates the frame with ScopeFrame.record, and the block's exit store is ScopeFrame.exit.

Returns the next configuration. A terminal/exiting configuration steps to itself (a no-op) — the driver runInterp detects those and stops, so there is no result Option; can't-continue is the monad's error channel.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.stmt (Imperative.Stmt.cmd cmd) env) = stepCmd fuel env cmd
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.stmt (Imperative.Stmt.exit label md) env) = pure (Imperative.IConfig.exiting label env)
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.stmt (Imperative.Stmt.typeDecl tc md) env) = pure (Imperative.IConfig.terminal env)
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.stmts [] env) = pure (Imperative.IConfig.terminal env)
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.stmts [stmt] env) = pure ((Imperative.IConfig.stmt stmt env).seqs 0)
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.stmts (stmt :: rest) env) = pure ((Imperative.IConfig.stmt stmt env).seq rest)
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.terminal env) = pure (Imperative.IConfig.terminal env)
• Imperative.stepInterp stepCmd fuel (Imperative.IConfig.exiting label env) = pure (Imperative.IConfig.exiting label env)
• Imperative.stepInterp stepCmd fuel ((Imperative.IConfig.terminal env).seq rest) = pure (Imperative.IConfig.stmts rest env)
• Imperative.stepInterp stepCmd fuel ((Imperative.IConfig.exiting label env).seq rest) = pure (Imperative.IConfig.exiting label env)
• Imperative.stepInterp stepCmd fuel (inner.seq rest) = do let inner ← Imperative.stepInterp stepCmd fuel inner pure (inner.seq rest)
• Imperative.stepInterp stepCmd fuel ((Imperative.IConfig.terminal env).seqs 0) = pure (Imperative.IConfig.stmts [] env)
• Imperative.stepInterp stepCmd fuel ((Imperative.IConfig.terminal env).seqs k_2.succ) = pure ((Imperative.IConfig.stmts [] env).seqs k_2)
• Imperative.stepInterp stepCmd fuel ((Imperative.IConfig.exiting label env).seqs 0) = pure (Imperative.IConfig.exiting label env)
• Imperative.stepInterp stepCmd fuel ((Imperative.IConfig.exiting label env).seqs k_2.succ) = pure ((Imperative.IConfig.exiting label env).seqs k_2)

def Imperative.runInterp {P : PureExpr} {CmdT : Type} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [CmdDefs P CmdT] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (stepCmd : StepCmdM P CmdT m) : Nat → IConfig P CmdT → m (IConfig P CmdT)

Fuel-bounded driver: iterate stepInterp until a terminal/exiting configuration or out of fuel. Out of fuel with a non-terminal configuration throws replayFuelExhausted.

The single fuel argument is the decreasing measure and the bound each step hands to InterpLang.boundedEval.

Equations

• Imperative.runInterp stepCmd x✝ (Imperative.IConfig.terminal env) = pure (Imperative.IConfig.terminal env)
• Imperative.runInterp stepCmd x✝ (Imperative.IConfig.exiting label env) = pure (Imperative.IConfig.exiting label env)
• Imperative.runInterp stepCmd 0 x✝ = throw Imperative.StopReason.replayFuelExhausted
• Imperative.runInterp stepCmd k_1.succ x✝ = do let next ← Imperative.stepInterp stepCmd (k_1 + 1) x✝ Imperative.runInterp stepCmd k_1 next