Unary Probabilistic Hoare Logic - Proof Rules

This file provides proof rules for the unary probabilistic Hoare logic.

Main theorems

• pHoare_ret - Return rule: pure values satisfy postconditions derivable from precondition
• pHoare_fail - Fail rule: fail satisfies any postcondition (vacuously)
• pHoare_sample - Sample rule: if Q holds for all sampled values, the judgment holds
• pHoare_get - Get rule: reading from a location
• pHoare_set - Set rule: writing to a location
• pHoare_bind - Bind rule: sequential composition
• pHoare_assert - Assert rule: assertion with continuation

Implementation notes

The key proof technique is extracting information from support membership. For SDistr.pure x, the only element with nonzero probability is x itself. We use SDistr.mem_support_pure_iff which states b ∈ (pure a).support ↔ a = b without requiring DecidableEq.

For SDistr.bind, the challenge is that if (d.bind f)(some y) ≠ 0 then there must exist some x with d(some x) ≠ 0 and (f x)(some y) ≠ 0. This requires analyzing the sum ∑ x, d(x) * (f x)(y) which is nonzero only if at least one term is nonzero.

Return rules

theorem CatCrypt.Unary.pHoare_ret {α : Type u_1} {P : UPre} {a : α} {Q : UPost α} (h : ∀ (h₀ : Core.Heap), P h₀ → Q a h₀) : pHoare P (Core.SPComp.pure a) Q

Return rule: pure values satisfy any postcondition derivable from precondition.

For SPComp.pure a, the only outcome is (a, h₀) where h₀ is the initial heap. So we need Q a h₀ which follows from the hypothesis.

Fail rule

theorem CatCrypt.Unary.pHoare_fail {α : Type u_1} {P : UPre} {Q : UPost α} : pHoare P Core.SPComp.fail Q

Fail satisfies any postcondition (vacuously, since no outcomes exist).

SPComp.fail returns SDistr.fail which assigns probability 0 to all some outcomes, so the support is empty and the universal quantification is vacuously true.

Sample rule

theorem CatCrypt.Unary.pHoare_sample {α : Type u_1} [Fintype α] [Nonempty α] {P : UPre} {Q : UPost α} (h : ∀ (h₀ : Core.Heap) (a : α), P h₀ → Q a h₀) : pHoare P (Core.SPComp.sample α) Q

Sample rule: if Q holds for all possible sampled values, the judgment holds.

SPComp.sample α draws uniformly from α and does not change the heap. So any outcome (a, h') in the support satisfies h' = h₀, and we need Q a h₀ for all a, which the hypothesis provides.

State rules

theorem CatCrypt.Unary.pHoare_get {P : UPre} {l : Core.Location} {Q : UPost l.ty} (h : ∀ (h₀ : Core.Heap), P h₀ → Q (h₀.get l) h₀) : pHoare P (Core.SPComp.get l) Q

Get rule: reading from a location.

SPComp.get l returns SDistr.pure (h₀.get l, h₀), so the only outcome is (h₀.get l, h₀).

theorem CatCrypt.Unary.pHoare_set {P : UPre} {l : Core.Location} {v : l.ty} {Q : UPost Unit} (h : ∀ (h₀ : Core.Heap), P h₀ → Q () (h₀.set l v)) : pHoare P (Core.SPComp.set l v) Q

Set rule: writing to a location.

SPComp.set l v returns SDistr.pure ((), h₀.set l v), so the only outcome is ((), h₀.set l v).

Bind rule

theorem CatCrypt.Unary.pHoare_bind {α : Type u_1} {β : Type u_2} {P : UPre} {Mid : UPost α} {Q : UPost β} {c : Core.SPComp α} {f : α → Core.SPComp β} (hc : pHoare P c Mid) (hf : ∀ (a : α), pHoare (Mid a) (f a) Q) : pHoare P (c.bind f) Q

Bind rule: sequential composition.

This is the most important structural rule. To prove pHoare P (c.bind f) Q, we need an intermediate postcondition Mid such that:

• c establishes Mid from P
• For each intermediate result a, f a establishes Q from Mid a

The key proof obligation is: if (c h₀).bind (fun (a, h₁) => f a h₁) assigns nonzero probability to (b, h'), then there exists an intermediate (a, h₁) with nonzero probability in c h₀ such that f a h₁ assigns nonzero probability to (b, h'). This follows from the fact that a sum of nonneg terms is nonzero iff at least one term is nonzero.

Assert rule

theorem CatCrypt.Unary.pHoare_assert {P : UPre} {Q : UPost Unit} {p : Prop} [Decidable p] (hp : ∀ (h₀ : Core.Heap), P h₀ → p) (hQ : ∀ (h₀ : Core.Heap), P h₀ → Q () h₀) : pHoare P (Core.SPComp.assert p) Q

Assert rule: if precondition implies the assertion, continue.

SPComp.assert p is if p then pure () else fail. When p holds (which it does, given P implies p), it reduces to pure ().

Derived rules

theorem CatCrypt.Unary.pHoare_frame {α : Type u_1} {P : UPre} {Q : UPost α} {R : Core.Heap → Prop} {c : Core.SPComp α} (hPQ : pHoare P c Q) (hR : pHoare P c fun (x : α) (h' : Core.Heap) => R h') : pHoare (fun (h : Core.Heap) => P h ∧ R h) c fun (a : α) (h' : Core.Heap) => Q a h' ∧ R h'

Frame rule: pHoare is preserved under conjunction with a frame condition.

If c preserves R (i.e., R holds before and after), and we have pHoare P c Q, then we can add R to both pre- and postcondition.

theorem CatCrypt.Unary.pHoare_exists {α : Type u_1} {β : Type u_2} {P : β → UPre} {Q : UPost α} {c : Core.SPComp α} (h : ∀ (b : β), pHoare (P b) c Q) : pHoare (fun (h₀ : Core.Heap) => ∃ (b : β), P b h₀) c Q

Existential rule: if for some witness the judgment holds, the judgment holds.

theorem CatCrypt.Unary.pHoare_ret_eq {α : Type u_1} {P : UPre} {a : α} : pHoare P (Core.SPComp.pure a) fun (a' : α) (h' : Core.Heap) => ∃ (h₀ : Core.Heap), P h₀ ∧ a' = a ∧ h' = h₀

Weakening the return rule: if we know the exact return value