obsReplay, the ReplayM observation

• replayRun: runs a ReplayM program from a config and a state; its run lemmas (replayRun_pure, replayRun_bind, replayRun_emit_state, replayRun_choose, ...).
• interruptOff, RunBridge: a run with the stop hook against the same run without it.
• obsReplay: ReplayM as an InterpObs instance.

Further run lemmas, the RunBridge lemmas and whole-run replay soundness (runInterp_sound_replay) are in InterpreterObsProps.lean.

ReplayM run lemmas under replayRun

def Imperative.replayRun {P : PureExpr} [InterpLang P] {α : Type} (x : ReplayM P α) (cfg : ReplayCfg P) (st : ReplayState P) : Except StopReason α × ReplayState P

Run a ReplayM computation under the configuration cfg from the state st, returning its outcome and final state.

Equations

• Imperative.replayRun x cfg st = (ReaderT.run x cfg).run.run st

theorem Imperative.replayRun_read_bind {P : PureExpr} [InterpLang P] {α : Type} (f : ReplayCfg P → ReplayM P α) (cfg : ReplayCfg P) (st : ReplayState P) : replayRun (read >>= f) cfg st = replayRun (f cfg) cfg st

replayRun of read >>= f runs f on the run's config.

theorem Imperative.replayRun_get_bind {P : PureExpr} [InterpLang P] {α : Type} (f : ReplayState P → ReplayM P α) (cfg : ReplayCfg P) (st : ReplayState P) : replayRun (get >>= f) cfg st = replayRun (f st) cfg st

replayRun of get >>= f runs f on the current state.

theorem Imperative.replayRun_modify_bind {P : PureExpr} [InterpLang P] {α : Type} (g : ReplayState P → ReplayState P) (f : PUnit → ReplayM P α) (cfg : ReplayCfg P) (st : ReplayState P) : replayRun (modify g >>= f) cfg st = replayRun (f PUnit.unit) cfg (g st)

replayRun of modify g >>= f runs f from the updated state g st.

theorem Imperative.replayRun_pure {P : PureExpr} [InterpLang P] {α : Type} (x : α) (cfg : ReplayCfg P) (st : ReplayState P) : replayRun (pure x) cfg st = (Except.ok x, st)

replayRun of pure x succeeds with x and leaves the state unchanged.

theorem Imperative.replayRun_throw {P : PureExpr} [InterpLang P] {α : Type} (r : StopReason) (cfg : ReplayCfg P) (st : ReplayState P) : replayRun (throw r) cfg st = (Except.error r, st)

replayRun of throw r fails with r and leaves the state unchanged.

theorem Imperative.replayRun_bind {P : PureExpr} [InterpLang P] {α β : Type} (x : ReplayM P α) (g : α → ReplayM P β) (cfg : ReplayCfg P) (st : ReplayState P) : replayRun (x >>= g) cfg st = match replayRun x cfg st with | (Except.ok a, st') => replayRun (g a) cfg st' | (Except.error e, st') => (Except.error e, st')

replayRun of x >>= g: continue with g on success, stop with the error otherwise.

theorem Imperative.replayRun_emit_state {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] (ev : IEvent P) (cfg : ReplayCfg P) (st : ReplayState P) : (replayRun (InterpEffects.emit ev) cfg st).snd = { remaining := st.remaining, usedRev := st.usedRev, traceRev := ev :: st.traceRev }

emit records the event in every outcome, whatever interruptOn says.

theorem Imperative.replayRun_choose {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] (factory : InterpLang.RFactory P) (store : RStore P) (ty : P.Ty) (cfg : ReplayCfg P) (st : ReplayState P) (v : P.Expr) (st' : ReplayState P) (h : replayRun (InterpEffects.choose factory store ty) cfg st = (Except.ok v, st')) : (InterpLang.ops.isValue factory v = true ∧ InterpLang.ops.hasType factory v ty = true) ∧ st'.traceRev = st.traceRev

A successful choose in ReplayM passed the value checks and left the trace unchanged.

RunBridge: the interrupt-on run against the interrupt-off run

def Imperative.interruptOff {P : PureExpr} [InterpLang P] (cfg : ReplayCfg P) : ReplayCfg P

cfg with the stop hook disabled (interruptOn := fun _ => none), so emit is record-only.

Equations

• Imperative.interruptOff cfg = { oracleConfig := cfg.oracleConfig }

@[reducible]

def Imperative.RunBridge {P : PureExpr} [InterpLang P] {α : Type} (x : ReplayM P α) (cfg : ReplayCfg P) (st : ReplayState P) : Prop

Relates the run of x under cfg to its run with the stop hook disabled (interruptOff cfg): the trace recorded under cfg is a suffix of the trace recorded with the hook off, and a run under cfg that succeeds coincides with the hook-off run.

Equations

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

def Imperative.obsReplay {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] : InterpObs P (ReplayM P)

The replay observation: ReplayM's reader config, state, run projection and recorded trace. @[expose]d so its fields unfold in statements outside this module.

Equations

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