Seq-Swap / Reorder Rules

Relational rules for commuting operations without syntactically rewriting programs. These are the CatCrypt analogue of Bluebell's seq-swap rule: when the head operations on two sides of a pRHL judgment don't match, we commute pure or independent operations past each other to bring them into alignment.

Main theorems

• rHoare_reorder_pure_l — commute an IsPure computation past anything on LHS
• rHoare_reorder_pure_r — symmetric variant for RHS
• rHoare_sample_comm — both sides sample α,β but in opposite order
• rHoare_sample_past_get_l — commute sample past get on LHS
• rHoare_sample_past_set_l — commute sample past set on LHS

References

• Bluebell (POPL 2025) — seq-swap rule for randomness alignment

Pure reordering

theorem CatCrypt.Relational.rHoare_reorder_pure_l {α β γ δ : Type} {c : Core.SPComp α} {d : Core.SPComp β} {k : α → β → Core.SPComp γ} {c₂ : Core.SPComp δ} {Φ : RPre} {Ψ : RPost γ δ} (hPure : c.IsPure) (h : rHoare Φ (d.bind fun (y : β) => c.bind fun (x : α) => k x y) c₂ Ψ) : rHoare Φ (c.bind fun (x : α) => d.bind fun (y : β) => k x y) c₂ Ψ

Reorder LHS: commute an IsPure computation past any other computation.

If c is pure (heap-independent), then c >>= fun x => d >>= fun y => k x y is equivalent to d >>= fun y => c >>= fun x => k x y. We use this to align heads when the LHS starts with a pure operation but the RHS starts with something else.

theorem CatCrypt.Relational.rHoare_reorder_pure_r {α β γ δ : Type} {c₁ : Core.SPComp γ} {c : Core.SPComp α} {d : Core.SPComp β} {k : α → β → Core.SPComp δ} {Φ : RPre} {Ψ : RPost γ δ} (hPure : c.IsPure) (h : rHoare Φ c₁ (d.bind fun (y : β) => c.bind fun (x : α) => k x y) Ψ) : rHoare Φ c₁ (c.bind fun (x : α) => d.bind fun (y : β) => k x y) Ψ

Reorder RHS: symmetric variant for the right-hand side.

Advantage-level reordering

theorem CatCrypt.Relational.advantage_factorization_comm {α β γ : Type} (pfx : Core.SPComp α) (G₁ G₂ : Core.SPComp β) (k : α → β → Core.SPComp γ) (hPure : pfx.IsPure) (A : γ → Core.SPComp Bool) : Crypto.AdvantageA (pfx.bind fun (p : α) => G₁.bind fun (r : β) => k p r) (pfx.bind fun (p : α) => G₂.bind fun (r : β) => k p r) A = Crypto.AdvantageA G₁ G₂ fun (r : β) => pfx.bind fun (p : α) => (k p r).bind A

Factor out a common IsPure prefix from two games.

If both games have the form pfx.bind(p => Gᵢ.bind(r => k p r)), where pfx is IsPure, then we can commute pfx past Gᵢ and factor:

AdvantageA (pfx.bind(p => G₁.bind(r => k p r))) (pfx.bind(p => G₂.bind(r => k p r))) A = AdvantageA G₁ G₂ (fun r => pfx.bind(p => (k p r).bind A))

This combines isPure_bind_comm + advantage_factorization into a single step, which is the key pattern in the Double Ratchet inductive step.

Sample commutativity

theorem CatCrypt.Relational.rHoare_sample_comm {α β γ : Type} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] {k₁ k₂ : α → β → Core.SPComp γ} {Φ : RPre} {Ψ : RPost γ γ} (h : ∀ (a : α) (b : β), rHoare Φ (k₁ a b) (k₂ a b) Ψ) : rHoare Φ ((Core.SPComp.sample α).bind fun (x : α) => (Core.SPComp.sample β).bind fun (y : β) => k₁ x y) ((Core.SPComp.sample β).bind fun (y : β) => (Core.SPComp.sample α).bind fun (x : α) => k₂ x y) Ψ

Both sides sample α,β but in opposite order: align them.

If the LHS samples α then β, and the RHS samples β then α, we can swap the RHS to match.

Sample past get/set

theorem CatCrypt.Relational.rHoare_sample_past_get_l {α β δ : Type} [Fintype α] [Nonempty α] {l : Core.Location} {k : α → l.ty → Core.SPComp β} {c₂ : Core.SPComp δ} {Φ : RPre} {Ψ : RPost β δ} (h : rHoare Φ ((Core.SPComp.get l).bind fun (v : l.ty) => (Core.SPComp.sample α).bind fun (x : α) => k x v) c₂ Ψ) : rHoare Φ ((Core.SPComp.sample α).bind fun (x : α) => (Core.SPComp.get l).bind fun (v : l.ty) => k x v) c₂ Ψ

Commute sample past get on the LHS.

sample α >>= fun x => get l >>= fun v => k x v is equivalent to get l >>= fun v => sample α >>= fun x => k x v because sample doesn't read the heap and get doesn't modify the distribution.

theorem CatCrypt.Relational.rHoare_sample_past_set_l {α β δ : Type} [Fintype α] [Nonempty α] {l : Core.Location} {v : l.ty} {k : α → Core.SPComp β} {c₂ : Core.SPComp δ} {Φ : RPre} {Ψ : RPost β δ} (h : rHoare Φ ((Core.SPComp.set l v).bind fun (x : Unit) => (Core.SPComp.sample α).bind fun (x : α) => k x) c₂ Ψ) : rHoare Φ ((Core.SPComp.sample α).bind fun (x : α) => (Core.SPComp.set l v).bind fun (x_1 : Unit) => k x) c₂ Ψ

Commute sample past set on the LHS.

sample α >>= fun x => set l v >> k x is equivalent to set l v >> sample α >>= fun x => k x because sample is independent of the heap.