Synchronized pRHL Rules

This file contains synchronized pRHL rules, where the same operation is performed on both sides of the relational judgment simultaneously.

Main definitions

• r_get_vs_get - Synchronized get on both sides
• r_put_vs_put - Synchronized put on both sides
• r_sample_vs_sample - Synchronized sampling on both sides

References

• SSProve: theories/Crypt/package/pkg_rhl.v
• EasyCrypt pRHL

Synchronized Get Rules

theorem CatCrypt.Relational.r_get_vs_get {Φ : RPre} (l : Core.Location) (hSync : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → h₁.get l = h₂.get l) : rHoare Φ (Core.SPComp.get l) (Core.SPComp.get l) fun (v₁ : l.ty) (h₁ : Core.Heap) (v₂ : l.ty) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ v₁ = v₂

Synchronized get on both sides at the same location. Precondition must imply the locations have the same value. Postcondition gets both values equal and preserves the invariant.

theorem CatCrypt.Relational.r_get_vs_get' {Φ : RPre} (l : Core.Location) (_hSync : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → h₁.get l = h₂.get l) : rHoare Φ (Core.SPComp.get l) (Core.SPComp.get l) fun (v₁ : l.ty) (h₁ : Core.Heap) (v₂ : l.ty) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ v₁ = h₁.get l ∧ v₂ = h₂.get l

Synchronized get at same location, where the invariant implies equality. This version gives a more explicit postcondition that captures the read value.

theorem CatCrypt.Relational.r_get_vs_get_diff {Φ : RPre} (l : Core.Location) (hSync : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → h₁.get l = h₂.get l) : rHoare Φ (Core.SPComp.get l) (Core.SPComp.get l) fun (v₁ : l.ty) (h₁ : Core.Heap) (v₂ : l.ty) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ v₁ = v₂

Synchronized get at different locations with same type. Each side reads from its respective location. Note: This rule is complex due to type casts; prefer using r_get_vs_get when both locations have the same type.

Synchronized Put Rules

theorem CatCrypt.Relational.r_put_vs_put {Φ : RPre} (l : Core.Location) (v : l.ty) (hInv : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → Φ (h₁.set l v) (h₂.set l v)) : rHoare Φ (Core.SPComp.set l v) (Core.SPComp.set l v) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => Φ h₁ h₂

Synchronized put on both sides at the same location with the same value. Preserves invariants that are preserved under the synchronized update.

theorem CatCrypt.Relational.r_put_vs_put_diff {Φ Ψ : RPre} (l : Core.Location) (v₁ v₂ : l.ty) (hTrans : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → Ψ (h₁.set l v₁) (h₂.set l v₂)) : rHoare Φ (Core.SPComp.set l v₁) (Core.SPComp.set l v₂) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => Ψ h₁ h₂

Synchronized put with different values on each side. Useful when transforming an invariant that relates values at the location.

theorem CatCrypt.Relational.r_put_vs_put_diff_loc {Φ Ψ : RPre} (l₁ l₂ : Core.Location) (v₁ : l₁.ty) (v₂ : l₂.ty) (hTrans : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → Ψ (h₁.set l₁ v₁) (h₂.set l₂ v₂)) : rHoare Φ (Core.SPComp.set l₁ v₁) (Core.SPComp.set l₂ v₂) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => Ψ h₁ h₂

Synchronized put at different locations. Each side writes to its respective location.

Synchronized Sampling Rules

theorem CatCrypt.Relational.r_sample_vs_sample {Φ : RPre} (α : Type u_4) [Fintype α] [Nonempty α] : rHoare Φ (Core.SPComp.sample α) (Core.SPComp.sample α) fun (a₁ : α) (h₁ : Core.Heap) (a₂ : α) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ a₁ = a₂

Synchronized sampling from the same distribution on both sides. Uses the diagonal coupling where both sides get the same value.

theorem CatCrypt.Relational.r_sample_vs_sample_bij {Φ : RPre} (α : Type u_4) (β : Type u_5) [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (f : α ≃ β) : rHoare Φ (Core.SPComp.sample α) (Core.SPComp.sample β) fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ f a = b

Synchronized sampling with a bijection coupling. The values on each side are related by the bijection f.

theorem CatCrypt.Relational.r_sample_vs_sample_coupling {Φ : RPre} (α : Type u_4) (β : Type u_5) [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (R : α → β → Prop) (hCoupling : Prob.SDistr.uniform α ⟨R⟩# Prob.SDistr.uniform β) : rHoare Φ (Core.SPComp.sample α) (Core.SPComp.sample β) fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Φ h₁ h₂ ∧ R a b

Synchronized sampling with an arbitrary coupling relation. This is the most general form, requiring a proof that the coupling exists.

Combined Synchronized Operations

theorem CatCrypt.Relational.r_get_put_vs_get_put {Φ Ψ : RPre} (l : Core.Location) (f : l.ty → l.ty) (_hSync : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → h₁.get l = h₂.get l) (hInv : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → Ψ (h₁.set l (f (h₁.get l))) (h₂.set l (f (h₂.get l)))) : rHoare Φ (do let v ← Core.SPComp.get l Core.SPComp.set l (f v)) (do let v ← Core.SPComp.get l Core.SPComp.set l (f v)) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => Ψ h₁ h₂

Get then put on the same location, synchronized on both sides. Updates the location with a function of its current value.

theorem CatCrypt.Relational.r_sample_put_vs_sample_put {Φ Ψ : RPre} (l : Core.Location) [Fintype l.ty] [Nonempty l.ty] (hInv : ∀ (h₁ h₂ : Core.Heap) (v : l.ty), Φ h₁ h₂ → Ψ (h₁.set l v) (h₂.set l v)) : rHoare Φ (do let v ← Core.SPComp.sample l.ty Core.SPComp.set l v) (do let v ← Core.SPComp.sample l.ty Core.SPComp.set l v) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => Ψ h₁ h₂

Sample then put on both sides. Samples a value and writes it to the same location.

Swap Rules

theorem CatCrypt.Relational.r_swap {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} (h : rHoare (fun (h₂ h₁ : Core.Heap) => Φ h₁ h₂) c₂ c₁ fun (b : β) (h₂ : Core.Heap) (a : α) (h₁ : Core.Heap) => Ψ a h₁ b h₂) : rHoare Φ c₁ c₂ Ψ

Swap lemma: if same code is run on swapped heaps with swapped pre/post, then we can use it on the original judgment.

Frame Rules

theorem CatCrypt.Relational.r_frame {α : Type u_1} {β : Type u_2} {Φ Ψ : RPre} {Θ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} (hInner : rHoare Φ c₁ c₂ Θ) (hFrame : ∀ (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap), Θ a h₁ b h₂ → Ψ h₁ h₂) : rHoare (Φ ⋀ Ψ) c₁ c₂ fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Θ a h₁ b h₂ ∧ Ψ h₁ h₂

Frame rule: if the invariant only depends on certain locations, and the code only modifies those locations, the invariant is preserved.