Relational program-logic baseline #
This file defines RelTriple via the generic two-monad algebra interface
MAlgRelOrdered, instantiated for OracleComp using coupling semantics.
HasCoupling and coupling lemmas remain as semantic bridge lemmas.
@[reducible, inline]
Relational postconditions over two output spaces.
Instances For
Equality relation helper for same-type outputs.
Instances For
def
OracleComp.ProgramLogic.Relational.CouplingPost
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
(oa : OracleComp spec₁ α)
(ob : OracleComp spec₂ β)
(R : RelPost α β)
:
Coupling-based semantic relational WP for OracleComp.
Instances For
@[implicit_reducible]
noncomputable instance
OracleComp.ProgramLogic.Relational.instMAlgRelOrdered
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
:
MAlgRelOrdered (OracleComp spec₁) (OracleComp spec₂) Prop
Relational algebra instance for OracleComp, based on coupling semantics.
@[reducible, inline]
abbrev
OracleComp.ProgramLogic.Relational.RelWP
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
(oa : OracleComp spec₁ α)
(ob : OracleComp spec₂ β)
(R : RelPost α β)
:
Relational weakest precondition induced by MAlgRelOrdered for OracleComp.
Instances For
@[reducible, inline]
abbrev
OracleComp.ProgramLogic.Relational.RelTriple
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
(oa : OracleComp spec₁ α)
(ob : OracleComp spec₂ β)
(R : RelPost α β)
:
Relational Hoare-style triple with implicit precondition True.
Instances For
@[simp]
theorem
OracleComp.ProgramLogic.Relational.relTriple_iff_relWP
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
{R : RelPost α β}
:
@[simp]
theorem
OracleComp.ProgramLogic.Relational.relWP_iff_couplingPost
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
{R : RelPost α β}
:
def
OracleComp.ProgramLogic.Relational.HasCoupling
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
(oa : OracleComp spec₁ α)
(ob : OracleComp spec₂ β)
:
Existence of an SPMF coupling witness between two computations.
Instances For
theorem
OracleComp.ProgramLogic.Relational.hasCoupling_of_relTriple
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
{R : RelPost α β}
(h : RelTriple oa ob R)
:
HasCoupling oa ob
Any relational triple yields a coupling witness.
theorem
OracleComp.ProgramLogic.Relational.relTriple_pure_pure
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{a : α}
{b : β}
{R : RelPost α β}
(h : R a b)
:
Pure values on both sides: R a b implies the coupling.
theorem
OracleComp.ProgramLogic.Relational.relTriple_refl
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
{α : Type}
(oa : OracleComp spec₁ α)
:
Reflexivity rule for relational triples on equality.
theorem
OracleComp.ProgramLogic.Relational.relTriple_post_mono
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
{R R' : RelPost α β}
(h : RelTriple oa ob R)
(hpost : ∀ ⦃x : α⦄ ⦃y : β⦄, R x y → R' x y)
:
RelTriple oa ob R'
Postcondition monotonicity for relational triples.
theorem
OracleComp.ProgramLogic.Relational.relTriple_bind
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β γ δ : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
{fa : α → OracleComp spec₁ γ}
{fb : β → OracleComp spec₂ δ}
{R : RelPost α β}
{S : RelPost γ δ}
(hxy : RelTriple oa ob R)
(hfg : ∀ (a : α) (b : β), R a b → RelTriple (fa a) (fb b) S)
:
Bind composition rule for relational triples.
theorem
OracleComp.ProgramLogic.Relational.relTriple_eqRel_of_eq
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
{α : Type}
{oa ob : OracleComp spec₁ α}
(h : oa = ob)
:
Equality of programs gives an equality-relation relational triple.
theorem
OracleComp.ProgramLogic.Relational.relTriple_eqRel_of_evalDist_eq
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ α}
(h : evalDist oa = evalDist ob)
:
Equality of evaluation distributions gives an equality-relation relational triple.
theorem
OracleComp.ProgramLogic.Relational.relTriple_of_evalDist_eq
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ α}
{R : RelPost α α}
(h : evalDist oa = evalDist ob)
(hR : ∀ (x : α), R x x)
:
RelTriple oa ob R
If two computations have equal output distributions, any reflexive postcondition holds.
theorem
OracleComp.ProgramLogic.Relational.relTriple_eqRel_of_probOutput_eq
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ α}
(h : ∀ (x : α), Pr[= x | oa] = Pr[= x | ob])
:
Pointwise output-probability equality gives an equality-relation relational triple.
theorem
OracleComp.ProgramLogic.Relational.probOutput_eq_of_relTriple_eqRel
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ α}
(h : RelTriple oa ob (EqRel α))
(x : α)
:
Equality-relation relational triples imply equality of point output probabilities.
theorem
OracleComp.ProgramLogic.Relational.evalDist_eq_of_relTriple_eqRel
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ α}
(h : RelTriple oa ob (EqRel α))
:
Equality-relation relational triples imply equality of evaluation distributions.
theorem
OracleComp.ProgramLogic.Relational.probOutput_true_eq_of_relTriple_eqRel
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{oa : OracleComp spec₁ Bool}
{ob : OracleComp spec₂ Bool}
(h : RelTriple oa ob (EqRel Bool))
:
Bool-specialized bridge from relational triples to game success equality.
Oracle query coupling rules (pRHL level) #
theorem
OracleComp.ProgramLogic.Relational.relTriple_query
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
(t : spec₁.Domain)
:
Same-type identity coupling: querying the same oracle on both sides yields equal outputs.
theorem
OracleComp.ProgramLogic.Relational.relTriple_query_bij
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
(t : spec₁.Domain)
{f : spec₁.Range t → spec₁.Range t}
(hf : Function.Bijective f)
:
Bijection coupling (the "rnd" rule from EasyCrypt):
querying the same oracle on both sides, related by a bijection f.
theorem
OracleComp.ProgramLogic.Relational.relTriple_map
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β γ δ : Type}
{R : RelPost γ δ}
{f : α → γ}
{g : β → δ}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
(h : RelTriple oa ob fun (a : α) (b : β) => R (f a) (g b))
:
theorem
OracleComp.ProgramLogic.Relational.evalDist_map_eq_of_relTriple
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β σ : Type}
{f : α → σ}
{g : β → σ}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
(h : RelTriple oa ob fun (a : α) (b : β) => f a = g b)
:
If a relational triple holds for fun a b => f a = g b, then mapping by f and g
produces equal distributions. Generalizes evalDist_eq_of_relTriple_eqRel.
theorem
OracleComp.ProgramLogic.Relational.relTriple_replicate
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{oa : OracleComp spec₁ α}
{ob : OracleComp spec₂ β}
{R : RelPost α β}
(n : ℕ)
(hstep : RelTriple oa ob R)
:
RelTriple (replicate n oa) (replicate n ob) (List.Forall₂ R)
Lift a one-step coupling through bounded iteration.
theorem
OracleComp.ProgramLogic.Relational.relTriple_replicate_eqRel
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
{α : Type}
{oa ob : OracleComp spec₁ α}
(n : ℕ)
(hstep : RelTriple oa ob (EqRel α))
:
Equality coupling version of relTriple_replicate.
theorem
OracleComp.ProgramLogic.Relational.relTriple_list_mapM
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β γ δ : Type}
{xs : List α}
{ys : List β}
{f : α → OracleComp spec₁ γ}
{g : β → OracleComp spec₂ δ}
{Rin : α → β → Prop}
{Rout : γ → δ → Prop}
(hxy : List.Forall₂ Rin xs ys)
(hfg : ∀ (a : α) (b : β), Rin a b → RelTriple (f a) (g b) Rout)
:
RelTriple (List.mapM f xs) (List.mapM g ys) (List.Forall₂ Rout)
Lift pointwise relational reasoning through finite list traversals.
theorem
OracleComp.ProgramLogic.Relational.relTriple_list_mapM_eqRel
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{xs : List α}
{f : α → OracleComp spec₁ β}
{g : α → OracleComp spec₂ β}
(hfg : ∀ (a : α), RelTriple (f a) (g a) (EqRel β))
:
Same-input equality-coupling specialization of relTriple_list_mapM.
theorem
OracleComp.ProgramLogic.Relational.relTriple_list_foldlM
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β σ₁ σ₂ : Type}
{xs : List α}
{ys : List β}
{f : σ₁ → α → OracleComp spec₁ σ₁}
{g : σ₂ → β → OracleComp spec₂ σ₂}
{Rin : α → β → Prop}
{S : σ₁ → σ₂ → Prop}
{s₁ : σ₁}
{s₂ : σ₂}
(hs : S s₁ s₂)
(hxy : List.Forall₂ Rin xs ys)
(hfg : ∀ (a : α) (b : β), Rin a b → ∀ (t₁ : σ₁) (t₂ : σ₂), S t₁ t₂ → RelTriple (f t₁ a) (g t₂ b) S)
:
RelTriple (List.foldlM f s₁ xs) (List.foldlM g s₂ ys) S
Loop-invariant rule for bounded left folds over related input lists.
theorem
OracleComp.ProgramLogic.Relational.relTriple_list_foldlM_same
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α σ₁ σ₂ : Type}
{xs : List α}
{f : σ₁ → α → OracleComp spec₁ σ₁}
{g : σ₂ → α → OracleComp spec₂ σ₂}
{S : σ₁ → σ₂ → Prop}
{s₁ : σ₁}
{s₂ : σ₂}
(hs : S s₁ s₂)
(hfg : ∀ (a : α) (t₁ : σ₁) (t₂ : σ₂), S t₁ t₂ → RelTriple (f t₁ a) (g t₂ a) S)
:
RelTriple (List.foldlM f s₁ xs) (List.foldlM g s₂ xs) S
Same-input specialization of relTriple_list_foldlM.
Synchronized branching rule #
theorem
OracleComp.ProgramLogic.Relational.relTriple_if
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{c : Prop}
[Decidable c]
{oa₁ oa₂ : OracleComp spec₁ α}
{ob₁ ob₂ : OracleComp spec₂ β}
{R : RelPost α β}
(htrue : c → RelTriple oa₁ ob₁ R)
(hfalse : ¬c → RelTriple oa₂ ob₂ R)
:
Synchronized conditional: if both sides branch on the same condition, the relational triple holds if it holds on both branches.
theorem
OracleComp.ProgramLogic.Relational.relTriple_pure_left
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{a : α}
{ob : OracleComp spec₂ β}
{R : RelPost α β}
(h : RelTriple (pure a) ob fun (x : α) (y : β) => x = a ∧ R x y)
:
Pure-left rule: the left side is a pure value, applied via bind decomposition.
theorem
OracleComp.ProgramLogic.Relational.relTriple_pure_right
{ι₁ ι₂ : Type u}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
[spec₁.Fintype]
[spec₁.Inhabited]
[spec₂.Fintype]
[spec₂.Inhabited]
{α β : Type}
{oa : OracleComp spec₁ α}
{b : β}
{R : RelPost α β}
(h : RelTriple oa (pure b) fun (x : α) (y : β) => y = b ∧ R x y)
:
Pure-right rule: the right side is a pure value, applied via bind decomposition.
theorem
OracleComp.ProgramLogic.Relational.relTriple_uniformSample_bij
{α : Type}
[SampleableType α]
{f : α → α}
(hf : Function.Bijective f)
(R : RelPost α α)
(hR : ∀ (x : α), R x (f x))
:
Relational coupling for uniform sampling via bijection.
Given a bijection f : α → α such that R x (f x) for all x,
the two uniform samples are related by R.
theorem
OracleComp.ProgramLogic.Relational.relTriple_uniformSample_refl
{α : Type}
[SampleableType α]
:
Identity coupling for uniform sampling.