Std.Do handler specifications for the replay fork oracle

Lifts the per-query support-based invariants of OracleComp.replayOracle (established in VCVio.CryptoFoundations.ReplayFork) into Std.Do.Triple specifications consumable by mvcgen. Whole-program simulations are then obtained for free via simulateQ_triple_preserves_invariant from VCVio.ProgramLogic.Unary.HandlerSpecs.

Main results

• OracleComp.replayOracle_triple_prefix - per-query @[spec] triple for preservation of ReplayPrefixInvariant i.
• OracleComp.replayOracle_triple_replacement - per-query @[spec] triple for preservation of ReplayReplacementInvariant i.
• OracleComp.replayOracle_triple_immutable - per-query @[spec] triple recording that forkQuery, replacement, and trace never change.
• OracleComp.simulateQ_replayOracle_preserves_prefix - whole-program prefix-invariant preservation for arbitrary oa : OracleComp spec α.
• OracleComp.simulateQ_replayOracle_preserves_replacement - whole-program replacement-invariant preservation.
• OracleComp.simulateQ_replayOracle_preserves_immutable - whole-program triple stating the immutable parameters of the replay state never change (relative to a fixed initial state).

The whole-program lemmas reproduce the three public theorems replayRunWithTraceValue_preservesPrefixInvariant, replayRunWithTraceValue_preservesReplacementInvariant, and the trio replayRunWithTraceValue_{forkQuery,replacement,trace}_eq at the Std.Do.Triple level: any property that is provable on a single replayOracle step lifts uniformly through the simulator.

Per-query specs (consumable by mvcgen)

theorem OracleComp.ProgramLogic.StdDo.replayOracle_triple_prefix {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] [spec.DecidableEq] (i t : ι) : ⦃fun (st : ReplayForkState spec i) => ⌜ReplayPrefixInvariant i st⌝⦄ replayOracle i t ⦃Std.Do.PostCond.noThrow fun (x : spec.Range t) (st' : ReplayForkState spec i) => ⌜ReplayPrefixInvariant i st'⌝⦄

Triple form of OracleComp.replayOracle_preservesPrefixInvariant: each replayOracle i t step preserves the replay prefix invariant.

Not marked @[spec]. replayOracle i t admits three distinct useful invariants (prefix / replacement / immutable parameters). mvcgen's findSpec is keyed by the syntactic head of the computation, not by the shape of the assertion, so if more than one of these were registered as @[spec] for the same head (replayOracle i t) the tactic would pick an arbitrary one and silently drop the others. Instead, we leave all three as plain theorems and ask the caller to pass the relevant one explicitly, e.g. mvcgen [replayOracle_triple_prefix]. The same pattern applies to replayOracle_triple_replacement and replayOracle_triple_immutable below.

theorem OracleComp.ProgramLogic.StdDo.replayOracle_triple_replacement {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] [spec.DecidableEq] (i t : ι) : ⦃fun (st : ReplayForkState spec i) => ⌜ReplayReplacementInvariant i st⌝⦄ replayOracle i t ⦃Std.Do.PostCond.noThrow fun (x : spec.Range t) (st' : ReplayForkState spec i) => ⌜ReplayReplacementInvariant i st'⌝⦄

Triple form of OracleComp.replayOracle_preservesReplacementInvariant: each replayOracle i t step preserves the replay replacement invariant.

Not marked @[spec] to avoid colliding with replayOracle_triple_prefix under mvcgen; pass it explicitly via mvcgen [replayOracle_triple_replacement].

theorem OracleComp.ProgramLogic.StdDo.replayOracle_triple_immutable {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] [spec.DecidableEq] (i t : ι) (st₀ : ReplayForkState spec i) : ⦃fun (st : ReplayForkState spec i) => ⌜st = st₀⌝⦄ replayOracle i t ⦃Std.Do.PostCond.noThrow fun (x : spec.Range t) (st' : ReplayForkState spec i) => ⌜st'.forkQuery = st₀.forkQuery ∧ st'.replacement = st₀.replacement ∧ st'.trace = st₀.trace⌝⦄

Triple form of OracleComp.replayOracle_immutable_params: each replayOracle i t step leaves forkQuery, replacement, and trace untouched. The triple is parametric in the witness st₀ of the initial state.

Not marked @[spec] to avoid colliding with replayOracle_triple_prefix under mvcgen; pass it explicitly via mvcgen [replayOracle_triple_immutable].

Whole-program corollaries via simulateQ_triple_preserves_invariant

theorem OracleComp.ProgramLogic.StdDo.simulateQ_replayOracle_preserves_prefix {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] [spec.DecidableEq] {α : Type} (i : ι) (oa : OracleComp spec α) : ⦃fun (st : ReplayForkState spec i) => ⌜ReplayPrefixInvariant i st⌝⦄ simulateQ (replayOracle i) oa ⦃Std.Do.PostCond.noThrow fun (x : α) (st' : ReplayForkState spec i) => ⌜ReplayPrefixInvariant i st'⌝⦄

Whole-program preservation: simulateQ (replayOracle i) oa preserves the replay prefix invariant for any oa. Direct corollary of simulateQ_triple_preserves_invariant and replayOracle_triple_prefix.

theorem OracleComp.ProgramLogic.StdDo.simulateQ_replayOracle_preserves_replacement {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] [spec.DecidableEq] {α : Type} (i : ι) (oa : OracleComp spec α) : ⦃fun (st : ReplayForkState spec i) => ⌜ReplayReplacementInvariant i st⌝⦄ simulateQ (replayOracle i) oa ⦃Std.Do.PostCond.noThrow fun (x : α) (st' : ReplayForkState spec i) => ⌜ReplayReplacementInvariant i st'⌝⦄

Whole-program preservation: simulateQ (replayOracle i) oa preserves the replay replacement invariant for any oa.

theorem OracleComp.ProgramLogic.StdDo.simulateQ_replayOracle_preserves_immutable {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] [spec.DecidableEq] {α : Type} (i : ι) (oa : OracleComp spec α) (st₀ : ReplayForkState spec i) : ⦃fun (st : ReplayForkState spec i) => ⌜st = st₀⌝⦄ simulateQ (replayOracle i) oa ⦃Std.Do.PostCond.noThrow fun (x : α) (st' : ReplayForkState spec i) => ⌜st'.forkQuery = st₀.forkQuery ∧ st'.replacement = st₀.replacement ∧ st'.trace = st₀.trace⌝⦄

Whole-program immutability: simulateQ (replayOracle i) oa never mutates forkQuery, replacement, or trace, relative to a fixed initial state st₀.

Worked examples