Probabilistic Relational Hoare Logic - Judgment #
This file defines the fundamental pRHL judgment.
Main definitions #
rHoare Φ c₁ c₂ Ψ- The pRHL judgment
Notation #
⊨ ⦃Φ⦄ c₁ ~ c₂ ⦃Ψ⦄- pRHL judgmentc₁ ~ c₂ : Φ ==> Ψ- EasyCrypt-style notation
References #
- SSProve: theories/Crypt/package/pkg_rhl.v
- EasyCrypt pRHL
The pRHL Judgment #
def
CatCrypt.Relational.rHoare
{α : Type u_1}
{β : Type u_2}
(Φ : RPre)
(c₁ : Core.SPComp α)
(c₂ : Core.SPComp β)
(Ψ : RPost α β)
:
The fundamental pRHL judgment.
rHoare Φ c₁ c₂ Ψ (written ⊨ ⦃Φ⦄ c₁ ~ c₂ ⦃Ψ⦄) means:
For all pairs of heaps (h₁, h₂) satisfying precondition Φ, there exists a coupling of the output distributions (c₁ h₁) and (c₂ h₂) such that all coupled pairs of outputs satisfy postcondition Ψ.
This is the semantic definition based on probabilistic couplings.
Equations
- CatCrypt.Relational.rHoare Φ c₁ c₂ Ψ = ∀ (h₁ h₂ : CatCrypt.Core.Heap), Φ h₁ h₂ → c₁ h₁ ⟨fun (p₁ : α × CatCrypt.Core.Heap) (p₂ : β × CatCrypt.Core.Heap) => Ψ p₁.1 p₁.2 p₂.1 p₂.2⟩# c₂ h₂
Instances For
Basic properties #
theorem
CatCrypt.Relational.rHoare_mono_post
{α : Type u_1}
{β : Type u_2}
{Φ : RPre}
{Ψ Ψ' : RPost α β}
{c₁ : Core.SPComp α}
{c₂ : Core.SPComp β}
(h : rHoare Φ c₁ c₂ Ψ)
(hΨ : ∀ (a₁ : α) (h₁ : Core.Heap) (a₂ : β) (h₂ : Core.Heap), Ψ a₁ h₁ a₂ h₂ → Ψ' a₁ h₁ a₂ h₂)
:
rHoare Φ c₁ c₂ Ψ'
rHoare is monotone in the postcondition
theorem
CatCrypt.Relational.rHoare_mono_pre
{α : Type u_1}
{β : Type u_2}
{Φ Φ' : RPre}
{Ψ : RPost α β}
{c₁ : Core.SPComp α}
{c₂ : Core.SPComp β}
(h : rHoare Φ c₁ c₂ Ψ)
(hΦ : ∀ (h₁ h₂ : Core.Heap), Φ' h₁ h₂ → Φ h₁ h₂)
:
rHoare Φ' c₁ c₂ Ψ
rHoare is antimonotone in the precondition