Std.Do / mvcgen bridge for the Interaction / UC runtime

Equip the runtime primitives in VCVio.Interaction.UC.Runtime (Spec.sampleTranscript, Concurrent.StepOver.sample, Concurrent.ProcessOver.runSteps) with the equational and Hoare-triple machinery mvcgen needs, so users can prove triples about UC executions in the same style as VCVio.ProgramLogic.Unary.HandlerSpecs.

Architecture

The runtime primitives are defined by structural recursion over the Interaction.Spec tree (for transcript sampling) or over fuel ℕ (for runSteps). Neither recursion is walked by mvcgen, so we expose the recursive equations as @[simp] lemmas and provide a closed-form runSteps_triple_preserves_invariant for the most common "fuel-indexed invariant" pattern.

The bridge is intentionally monad-parametric: every result is phrased for an arbitrary [Monad m] [WPMonad m ps]. This covers both m = ProbComp (coin-flip-only protocols) and m = OracleComp superSpec (shared random oracle / CRS protocols), since both carry Std.Do.WPMonad instances via VCVio.ProgramLogic.Unary.StdDoBridge.

Main results

• Spec.sampleTranscript_done, Spec.sampleTranscript_node — rfl-level unfolding of Spec.sampleTranscript for base and step cases.
• Concurrent.StepOver.sample_eq — unfolds StepOver.sample in terms of sampleTranscript.
• Concurrent.ProcessOver.runSteps_zero, Concurrent.ProcessOver.runSteps_succ — base and step unfolding of runSteps on fuel.
• Concurrent.ProcessOver.runSteps_triple_preserves_invariant — lifts a per-step invariant triple to a whole-runSteps triple, by induction on fuel.

All equations are proved by rfl and are tagged @[simp] so that mvcgen can walk an exposed sampleTranscript / sample / runSteps body in one simp pass before the usual do-block traversal.

@[simp]

theorem Interaction.Spec.sampleTranscript_done {m : Type → Type} [Monad m] (samp : Sampler m done) : done.sampleTranscript samp = pure PUnit.unit

@[simp]

theorem Interaction.Spec.sampleTranscript_node {m : Type → Type} [Monad m] {X : Type} (rest : X → Spec) (samp : m X) (sampRest : (x : X) → Sampler m (rest x)) : (node X rest).sampleTranscript (samp, sampRest) = do let x ← samp let tr ← (rest x).sampleTranscript (sampRest x) pure ⟨x, tr⟩

@[simp]

theorem Interaction.Concurrent.StepOver.sample_eq {m : Type → Type} [Monad m] {Γ : Spec.Node.Context} {P : Type} (step : StepOver Γ P) (sampler : Spec.Sampler m step.spec) : step.sample sampler = do let tr ← step.spec.sampleTranscript sampler pure (step.next tr)

@[simp]

theorem Interaction.Concurrent.ProcessOver.runSteps_zero {m : Type → Type} [Monad m] {Γ : Spec.Node.Context} (process : ProcessOver Γ) (sampler : (p : process.Proc) → Spec.Sampler m (process.step p).spec) (s : process.Proc) : process.runSteps sampler 0 s = pure s

@[simp]

theorem Interaction.Concurrent.ProcessOver.runSteps_succ {m : Type → Type} [Monad m] {Γ : Spec.Node.Context} (process : ProcessOver Γ) (sampler : (p : process.Proc) → Spec.Sampler m (process.step p).spec) (n : ℕ) (s : process.Proc) : process.runSteps sampler (n + 1) s = do let s' ← (process.step s).sample (sampler s) process.runSteps sampler n s'

Invariant preservation for runSteps

theorem Interaction.Concurrent.ProcessOver.runSteps_triple_preserves_invariant {m : Type → Type} [Monad m] {ps : Std.Do.PostShape} [Std.Do.WPMonad m ps] {Γ : Spec.Node.Context} (process : ProcessOver Γ) (sampler : (p : process.Proc) → Spec.Sampler m (process.step p).spec) (I : process.Proc → Prop) (hstep : ∀ (p : process.Proc), ⦃⌜I p⌝⦄ (process.step p).sample (sampler p) ⦃Std.Do.PostCond.noThrow fun (p' : process.Proc) => ⌜I p'⌝⦄) (n : ℕ) (s₀ : process.Proc) : ⦃⌜I s₀⌝⦄ process.runSteps sampler n s₀ ⦃Std.Do.PostCond.noThrow fun (s' : process.Proc) => ⌜I s'⌝⦄

If every one-step execution preserves an invariant I on the process state, then runSteps n preserves I for any fuel n.

This is the process-runtime analogue of OracleComp.ProgramLogic.StdDo.simulateQ_triple_preserves_invariant: a generic invariant lemma that factors out the fuel induction so downstream proofs stay inside the Std.Do world.

Smoke test: increment process

A minimal worked example demonstrating the bridge: an always-increment process over Proc := ℕ whose every step advances the counter by one without consuming any moves. The counter is trivially monotone and the whole-execution corollary follows directly from runSteps_triple_preserves_invariant.