Unary Probabilistic Hoare Logic - Judgment

This file defines the unary probabilistic Hoare logic judgment for CatCrypt. It is analogous to EasyCrypt's pHL but for our SPComp monad.

Main definitions

• UPre - Unary precondition (predicate on initial heap)
• UPost α - Unary postcondition (predicate on result and final heap)
• pHoare P c Q - The pHL judgment: for all heaps satisfying P, every outcome in the support of c h satisfies Q

References

• EasyCrypt pHL (unary probabilistic Hoare logic)
• CatCrypt Relational.Judgment (the relational counterpart)

Unary assertion types

@[reducible, inline]

abbrev CatCrypt.Unary.UPre : Type

Unary precondition: predicate on initial heap

Equations

• CatCrypt.Unary.UPre = (CatCrypt.Core.Heap → Prop)

@[reducible, inline]

abbrev CatCrypt.Unary.UPost (α : Type u_3) : Type u_3

Unary postcondition: predicate on result and final heap

Equations

• CatCrypt.Unary.UPost α = (α → CatCrypt.Core.Heap → Prop)

Standard preconditions

def CatCrypt.Unary.truePre : UPre

True precondition: always holds

Equations

• CatCrypt.Unary.truePre x✝ = True

def CatCrypt.Unary.falsePre : UPre

False precondition: never holds

Equations

• CatCrypt.Unary.falsePre x✝ = False

The pHL Judgment

def CatCrypt.Unary.pHoare {α : Type u_1} (P : UPre) (c : Core.SPComp α) (Q : UPost α) : Prop

The probabilistic Hoare logic judgment (pHL).

pHoare P c Q means: for all initial heaps h satisfying P h, every outcome (a, h') in the support of c h satisfies Q a h'.

An outcome (a, h') is in the support when (c h) (some (a, h')) ≠ 0, i.e., it has nonzero probability.

Equations

• CatCrypt.Unary.pHoare P c Q = ∀ (h : CatCrypt.Core.Heap), P h → ∀ (a : α) (h' : CatCrypt.Core.Heap), (c h) (some (a, h')) ≠ 0 → Q a h'

Basic properties

theorem CatCrypt.Unary.pHoare_mono_post {α : Type u_1} {P : UPre} {Q Q' : UPost α} {c : Core.SPComp α} (h : pHoare P c Q) (hQ : ∀ (a : α) (h : Core.Heap), Q a h → Q' a h) : pHoare P c Q'

pHoare is monotone in the postcondition

theorem CatCrypt.Unary.pHoare_mono_pre {α : Type u_1} {P P' : UPre} {Q : UPost α} {c : Core.SPComp α} (h : pHoare P c Q) (hP : ∀ (h : Core.Heap), P' h → P h) : pHoare P' c Q

pHoare is antimonotone in the precondition

theorem CatCrypt.Unary.pHoare_conseq {α : Type u_1} {P P' : UPre} {Q Q' : UPost α} {c : Core.SPComp α} (hPre : ∀ (h : Core.Heap), P' h → P h) (hPost : ∀ (a : α) (h : Core.Heap), Q a h → Q' a h) (h : pHoare P c Q) : pHoare P' c Q'

Consequence rule: strengthen precondition, weaken postcondition

theorem CatCrypt.Unary.pHoare_and {α : Type u_1} {P : UPre} {Q₁ Q₂ : UPost α} {c : Core.SPComp α} (h₁ : pHoare P c Q₁) (h₂ : pHoare P c Q₂) : pHoare P c fun (a : α) (h : Core.Heap) => Q₁ a h ∧ Q₂ a h

Conjunction of postconditions

theorem CatCrypt.Unary.pHoare_or_pre {α : Type u_1} {P₁ P₂ : UPre} {Q : UPost α} {c : Core.SPComp α} (h₁ : pHoare P₁ c Q) (h₂ : pHoare P₂ c Q) : pHoare (fun (h : Core.Heap) => P₁ h ∨ P₂ h) c Q

Disjunction of preconditions

theorem CatCrypt.Unary.pHoare_true_pre {α : Type u_1} {P : UPre} {Q : UPost α} {c : Core.SPComp α} (h : pHoare truePre c Q) : pHoare P c Q

True precondition implies any precondition suffices

theorem CatCrypt.Unary.pHoare_false_pre {α : Type u_1} {Q : UPost α} {c : Core.SPComp α} : pHoare falsePre c Q

False precondition makes any judgment trivially true