Documentation

VCVio.ProgramLogic.Relational.HandlerFromUnary

Lifting Std.Do handler triples to relational triples #

This file generalizes the unary-to-relational bridge in Relational.FromUnary from pure OracleComp computations to stateful handlers. It bridges the gap between

Main results #

The hsync argument is what bridges product (independent) reasoning to the synchronized coupling expected by relTriple_simulateQ_run: even if the underlying unary triples are independent, an external sync argument (determinism of the handler, agreement of random choices, etc.) is needed to upgrade pairwise postconditions to output equality plus a state invariant.

The whole-program lift fixes OracleSpec.{0, 0} because the unary triple_stateT_iff_forall_support bridge in VCVio.ProgramLogic.Unary.HandlerSpecs is stated at that universe.

Per-call lifts (one transformer layer) #

source
theorem OracleComp.ProgramLogic.Relational.relTriple_run_of_triple {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {σ₁ σ₂ α β : Type} (mx₁ : StateT σ₁ (OracleComp spec₁) α) (mx₂ : StateT σ₂ (OracleComp spec₂) β) (s₁ : σ₁) (s₂ : σ₂) (P₁ : σ₁ → Prop) (P₂ : σ₂ → Prop) (Q₁ : α → σ₁ → Prop) (Q₂ : β → σ₂ → Prop) (hP₁ : P₁ s₁) (hP₂ : P₂ s₂) (h₁ : ⦃fun (s : σ₁) => ⌜P₁ s⌝⦄ mx₁ ⦃Std.Do.PostCond.noThrow fun (a : α) (s' : σ₁) => ⌜Q₁ a s'⌝⦄) (h₂ : ⦃fun (s : σ₂) => ⌜P₂ s⌝⦄ mx₂ ⦃Std.Do.PostCond.noThrow fun (b : β) (s' : σ₂) => ⌜Q₂ b s'⌝⦄) :
RelTriple (mx₁.run s₁) (mx₂.run s₂) fun (p₁ : α × σ₁) (p₂ : β × σ₂) => Q₁ p₁.1 p₁.2 ∧ Q₂ p₂.1 p₂.2

Per-call lift from two unary Std.Do.Triples to a relational product coupling on the .run distributions.

Each triple's postcondition is interpreted as a property of the (value, final_state) pair; the relational postcondition is the pairwise conjunction. This is the stateful generalization of relTriple_prod_of_triple.

source
theorem OracleComp.ProgramLogic.Relational.relTriple_run_writerT_of_triple {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β ω₁ ω₂ : Type} [EmptyCollection ω₁] [Append ω₁] [LawfulAppend ω₁] [EmptyCollection ω₂] [Append ω₂] [LawfulAppend ω₂] (mx₁ : WriterT ω₁ (OracleComp spec₁) α) (mx₂ : WriterT ω₂ (OracleComp spec₂) β) (s₁ : ω₁) (s₂ : ω₂) (P₁ : ω₁ → Prop) (P₂ : ω₂ → Prop) (Q₁ : α → ω₁ → Prop) (Q₂ : β → ω₂ → Prop) (hP₁ : P₁ s₁) (hP₂ : P₂ s₂) (h₁ : ⦃fun (s : ω₁) => ⌜P₁ s⌝⦄ mx₁ ⦃Std.Do.PostCond.noThrow fun (a : α) (s' : ω₁) => ⌜Q₁ a s'⌝⦄) (h₂ : ⦃fun (s : ω₂) => ⌜P₂ s⌝⦄ mx₂ ⦃Std.Do.PostCond.noThrow fun (b : β) (s' : ω₂) => ⌜Q₂ b s'⌝⦄) :
RelTriple mx₁.run mx₂.run fun (p₁ : α × ω₁) (p₂ : β × ω₂) => Q₁ p₁.1 (s₁ ++ p₁.2) ∧ Q₂ p₂.1 (s₂ ++ p₂.2)

WriterT analogue of relTriple_run_of_triple.

Two unary Std.Do.Triples on WriterT ωᵢ (OracleComp specᵢ) lift to a product coupling on the (value, accumulated_log) pairs of the underlying OracleComp. The starting log of each side is fixed at s₁ : ω₁ and s₂ : ω₂ and the postconditions are read at Q₁ a (s₁ ++ w) / Q₂ b (s₂ ++ w) where w is the writer increment produced by the run.

The starting logs default to ∅ for the typical WriterT.run call but are kept arbitrary so the lemma composes cleanly with prefix-style log specs (e.g. loggingOracle's log' = log₀ ++ [⟨t, v⟩]).

source
theorem OracleComp.ProgramLogic.Relational.relTriple_run_writerT_of_triple_monoid {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β ω₁ ω₂ : Type} [Monoid ω₁] [Monoid ω₂] (mx₁ : WriterT ω₁ (OracleComp spec₁) α) (mx₂ : WriterT ω₂ (OracleComp spec₂) β) (s₁ : ω₁) (s₂ : ω₂) (P₁ : ω₁ → Prop) (P₂ : ω₂ → Prop) (Q₁ : α → ω₁ → Prop) (Q₂ : β → ω₂ → Prop) (hP₁ : P₁ s₁) (hP₂ : P₂ s₂) (h₁ : ⦃fun (s : ω₁) => ⌜P₁ s⌝⦄ mx₁ ⦃Std.Do.PostCond.noThrow fun (a : α) (s' : ω₁) => ⌜Q₁ a s'⌝⦄) (h₂ : ⦃fun (s : ω₂) => ⌜P₂ s⌝⦄ mx₂ ⦃Std.Do.PostCond.noThrow fun (b : β) (s' : ω₂) => ⌜Q₂ b s'⌝⦄) :
RelTriple mx₁.run mx₂.run fun (p₁ : α × ω₁) (p₂ : β × ω₂) => Q₁ p₁.1 (s₁ * p₁.2) ∧ Q₂ p₂.1 (s₂ * p₂.2)

Monoid-variant of relTriple_run_writerT_of_triple.

For WriterT ωᵢ (OracleComp specᵢ) with [Monoid ωᵢ], two unary Std.Do.Triples lift to a product coupling on the (value, accumulated_log) pairs where each postcondition is read at Q₁ a (s₁ * w) / Q₂ b (s₂ * w) (monoid multiplication). Used by countingOracle / costOracle reasoning.

source
theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_of_triples {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {σ₁ σ₂ α ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec₂))) (R_state : σ₁ → σ₂ → Prop) (oa : OracleComp spec α) (Q₁ : (t : spec.Domain) → σ₁ → spec.Range t → σ₁ → Prop) (Q₂ : (t : spec.Domain) → σ₂ → spec.Range t → σ₂ → Prop) (h₁ : ∀ (t : spec.Domain) (s : σ₁), ⦃fun (s' : σ₁) => ⌜s' = s⌝⦄ impl₁ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : σ₁) => ⌜Q₁ t s a s'⌝⦄) (h₂ : ∀ (t : spec.Domain) (s : σ₂), ⦃fun (s' : σ₂) => ⌜s' = s⌝⦄ impl₂ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : σ₂) => ⌜Q₂ t s a s'⌝⦄) (hsync : ∀ (t : spec.Domain) (s₁' : σ₁) (s₂' : σ₂), R_state s₁' s₂' → ∀ (a₁ : spec.Range t) (s₁'' : σ₁) (a₂ : spec.Range t) (s₂'' : σ₂), Q₁ t s₁' a₁ s₁'' → Q₂ t s₂' a₂ s₂'' → a₁ = a₂ ∧ R_state s₁'' s₂'') (s₁ : σ₁) (s₂ : σ₂) (hs : R_state s₁ s₂) :
RelTriple ((simulateQ impl₁ oa).run s₁) ((simulateQ impl₂ oa).run s₂) fun (p₁ : α × σ₁) (p₂ : α × σ₂) => p₁.1 = p₂.1 ∧ R_state p₁.2 p₂.2

Whole-program handler lift: given matching unary handler triples on two simulators with parametric pre/postconditions and a synchronization condition relating the postconditions, derive a RelTriple on the entire simulateQ outputs.

The unary triples are quantified over the initial handler state; their postconditions may depend on it. The synchronization condition hsync extracts output equality and the state-relation invariant from a paired instance of the two unary postconditions, which is exactly the bridge needed by relTriple_simulateQ_run.

source
theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_writerT_of_triples {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ω₁ ω₂ : Type} [Monoid ω₁] [Monoid ω₂] (impl₁ : QueryImpl spec (WriterT ω₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (WriterT ω₂ (OracleComp spec₂))) (R_writer : ω₁ → ω₂ → Prop) (hR_one : R_writer 1 1) (hR_mul : ∀ (w₁ w₁' : ω₁) (w₂ w₂' : ω₂), R_writer w₁ w₂ → R_writer w₁' w₂' → R_writer (w₁ * w₁') (w₂ * w₂')) (oa : OracleComp spec α) (Q₁ : (t : spec.Domain) → spec.Range t → ω₁ → Prop) (Q₂ : (t : spec.Domain) → spec.Range t → ω₂ → Prop) (h₁ : ∀ (t : spec.Domain), ⦃fun (s : ω₁) => ⌜s = 1⌝⦄ impl₁ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : ω₁) => ⌜Q₁ t a s'⌝⦄) (h₂ : ∀ (t : spec.Domain), ⦃fun (s : ω₂) => ⌜s = 1⌝⦄ impl₂ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : ω₂) => ⌜Q₂ t a s'⌝⦄) (hsync : ∀ (t : spec.Domain) (a₁ : spec.Range t) (w₁ : ω₁) (a₂ : spec.Range t) (w₂ : ω₂), Q₁ t a₁ w₁ → Q₂ t a₂ w₂ → a₁ = a₂ ∧ R_writer w₁ w₂) :
RelTriple (simulateQ impl₁ oa).run (simulateQ impl₂ oa).run fun (p₁ : α × ω₁) (p₂ : α × ω₂) => p₁.1 = p₂.1 ∧ R_writer p₁.2 p₂.2

WriterT analogue of relTriple_simulateQ_run_of_triples (monoid variant).

Given matching unary Std.Do.Triple specs for two WriterT-based handlers, a monoid-congruent writer relation R_writer (via hR_one and hR_mul), and a synchronization condition on per-query postconditions, derive a whole-program RelTriple on the full (output, writer) outputs of the two simulations.

The per-query triples are specialized to starting writer 1 (which corresponds to WriterT.run-style entry); their postconditions are evaluated at the resulting step writer. Typical instantiations are countingOracle_triple and costOracle_triple with qc₀ = 0 / s₀ = 1.

source
theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_writerT'_of_triples {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ω₁ ω₂ : Type} [Monoid ω₁] [Monoid ω₂] (impl₁ : QueryImpl spec (WriterT ω₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (WriterT ω₂ (OracleComp spec₂))) (R_writer : ω₁ → ω₂ → Prop) (hR_one : R_writer 1 1) (hR_mul : ∀ (w₁ w₁' : ω₁) (w₂ w₂' : ω₂), R_writer w₁ w₂ → R_writer w₁' w₂' → R_writer (w₁ * w₁') (w₂ * w₂')) (oa : OracleComp spec α) (Q₁ : (t : spec.Domain) → spec.Range t → ω₁ → Prop) (Q₂ : (t : spec.Domain) → spec.Range t → ω₂ → Prop) (h₁ : ∀ (t : spec.Domain), ⦃fun (s : ω₁) => ⌜s = 1⌝⦄ impl₁ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : ω₁) => ⌜Q₁ t a s'⌝⦄) (h₂ : ∀ (t : spec.Domain), ⦃fun (s : ω₂) => ⌜s = 1⌝⦄ impl₂ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : ω₂) => ⌜Q₂ t a s'⌝⦄) (hsync : ∀ (t : spec.Domain) (a₁ : spec.Range t) (w₁ : ω₁) (a₂ : spec.Range t) (w₂ : ω₂), Q₁ t a₁ w₁ → Q₂ t a₂ w₂ → a₁ = a₂ ∧ R_writer w₁ w₂) :
RelTriple (Prod.fst <$> (simulateQ impl₁ oa).run) (Prod.fst <$> (simulateQ impl₂ oa).run) (EqRel α)

Output-projection variant of relTriple_simulateQ_run_writerT_of_triples.

Drops the writer component, leaving only EqRel α on outputs.

source
theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run'_of_triples {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {σ₁ σ₂ α ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec₂))) (R_state : σ₁ → σ₂ → Prop) (oa : OracleComp spec α) (Q₁ : (t : spec.Domain) → σ₁ → spec.Range t → σ₁ → Prop) (Q₂ : (t : spec.Domain) → σ₂ → spec.Range t → σ₂ → Prop) (h₁ : ∀ (t : spec.Domain) (s : σ₁), ⦃fun (s' : σ₁) => ⌜s' = s⌝⦄ impl₁ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : σ₁) => ⌜Q₁ t s a s'⌝⦄) (h₂ : ∀ (t : spec.Domain) (s : σ₂), ⦃fun (s' : σ₂) => ⌜s' = s⌝⦄ impl₂ t ⦃Std.Do.PostCond.noThrow fun (a : spec.Range t) (s' : σ₂) => ⌜Q₂ t s a s'⌝⦄) (hsync : ∀ (t : spec.Domain) (s₁' : σ₁) (s₂' : σ₂), R_state s₁' s₂' → ∀ (a₁ : spec.Range t) (s₁'' : σ₁) (a₂ : spec.Range t) (s₂'' : σ₂), Q₁ t s₁' a₁ s₁'' → Q₂ t s₂' a₂ s₂'' → a₁ = a₂ ∧ R_state s₁'' s₂'') (s₁ : σ₁) (s₂ : σ₂) (hs : R_state s₁ s₂) :
RelTriple ((simulateQ impl₁ oa).run' s₁) ((simulateQ impl₂ oa).run' s₂) (EqRel α)

Output-projection variant of relTriple_simulateQ_run_of_triples.

Drops the final state from both sides, leaving only a relational equality on the return values. This is the canonical shape needed for probability transport (via probOutput_eq_of_relTriple_eqRel), matching relTriple_simulateQ_run' at the handler-triple layer.

Bridge to support-based simulation lemmas #

The lemmas below convert Std.Do.Triple invariant specs produced by mvcgen into the support-based hypotheses that the existing Relational/SimulateQ.lean infrastructure consumes. They're the recommended entry point from the mvcgen proof style into whole-program relational reasoning.

source
theorem OracleComp.ProgramLogic.Relational.support_preservesInv_of_triple {ι₁ : Type} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ : Type} (impl : QueryImpl spec (StateT σ (OracleComp spec₁))) (Inv : σ → Prop) (h : ∀ (t : spec.Domain), ⦃fun (s' : σ) => ⌜Inv s'⌝⦄ impl t ⦃Std.Do.PostCond.noThrow fun (x : spec.Range t) (s' : σ) => ⌜Inv s'⌝⦄) (t : spec.Domain) (s : σ) :
Inv s → ∀ z ∈ support ((impl t).run s), Inv z.2

Convert a unary Std.Do.Triple invariant-preservation spec into the support-based preservation hypothesis consumed by relTriple_simulateQ_run_of_impl_eq_preservesInv and friends.

The mvcgen proof style produces invariant-preservation specs as Std.Do.Triple judgments; most of the existing SimulateQ.lean relational infrastructure is phrased in terms of support. This lemma is the direct translator, lifting over triple_stateT_iff_forall_support.

source
theorem OracleComp.ProgramLogic.Relational.writerPreservesInv_of_triple {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ω : Type} [Monoid ω] (impl : QueryImpl spec (WriterT ω (OracleComp spec))) (Inv : ω → Prop) (h : ∀ (t : spec.Domain), ⦃fun (s : ω) => ⌜Inv s⌝⦄ impl t ⦃Std.Do.PostCond.noThrow fun (x : spec.Range t) (s' : ω) => ⌜Inv s'⌝⦄) :
impl.WriterPreservesInv Inv

WriterT analogue of support_preservesInv_of_triple. Converts a unary Std.Do.Triple invariant-preservation spec for a WriterT-based handler (with [Monoid ω]) into the WriterPreservesInv hypothesis consumed by OracleComp.simulateQ_run_writerPreservesInv.

Use this whenever a writer-invariant-preservation proof is available as an mvcgen-style Std.Do.Triple, and the downstream consumer is a support-based whole-program lemma.

source
theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_of_impl_eq_triple {α ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ : Type} (impl₁ impl₂ : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → Prop) (oa : OracleComp spec α) (himpl_eq : ∀ (t : spec.Domain) (s : σ), Inv s → (impl₁ t).run s = (impl₂ t).run s) (hpres₂ : ∀ (t : spec.Domain), ⦃fun (s' : σ) => ⌜Inv s'⌝⦄ impl₂ t ⦃Std.Do.PostCond.noThrow fun (x : spec.Range t) (s' : σ) => ⌜Inv s'⌝⦄) (s : σ) (hs : Inv s) :
RelTriple ((simulateQ impl₁ oa).run s) ((simulateQ impl₂ oa).run s) (EqRel (α × σ))

Whole-program equality coupling when two handlers agree pointwise on an invariant Inv and the target handler preserves Inv. This is the Std.Do.Triple-fronted version of relTriple_simulateQ_run_of_impl_eq_preservesInv: the preservation hypothesis is supplied via mvcgen-style Std.Do.Triples rather than a support-based quantifier.

Smoke tests #

Whole-program WriterT smoke tests #