pRHL Loop-Congruence Rules

Relational Hoare rules for List.forM and List.foldlM over SPComp, analogous to VCVio's rvcstep congruence steps for List.mapM/List.foldlM.

Instead of manually unrolling lists with repeated rHoare_bind/rHoare_ret, these rules discharge a synchronized loop in one application:

• rHoare_forM — the two sides iterate over lists xs, ys related pointwise by R (a List.Forall₂ R xs ys witness); a heap invariant I : RPre is carried through every iteration.
• rHoare_forM_same — the common synchronous specialization: same input list, two different loop bodies related pointwise.
• rHoare_foldlM — like rHoare_forM, but List.foldlM additionally threads accumulators; a value relation V on the accumulators is carried alongside the heap invariant I.
• rHoare_foldlM_same — synchronous foldlM specialization (same list, same accumulator relation, bodies related pointwise).

A unary companion section (in the CatCrypt.Core.SPComp namespace) provides the IsPure loop lemmas:

• SPComp.mapM_isPure / SPComp.forM_isPure / SPComp.foldlM_isPure — a monadic loop whose body is heap-pure at every element of the list is heap-pure. These discharge the IsPure side conditions on games defined via List.mapM (e.g. Helios privacy_real/privacy_ideal).

Usage sketch

-- Both sides write the same key schedule; heap equality is invariant:
example (l : Location) (vs : List l.ty) :
    rHoare eqPre (vs.forM fun v => SPComp.set l v)
                 (vs.forM fun v => SPComp.set l v)
      (fun _ h₁ _ h₂ => eqPre h₁ h₂) :=
  rHoare_forM_same vs fun v _ => rHoare_set_sync l v ...

Unary IsPure loop lemmas

theorem CatCrypt.Core.SPComp.mapM_isPure {α : Type u'} {β : Type v'} {f : α → SPComp β} {xs : List α} (h : ∀ x ∈ xs, (f x).IsPure) : (List.mapM f xs).IsPure

List.mapM over SPComp is heap-pure when the body is heap-pure at every element of the list.

theorem CatCrypt.Core.SPComp.forM_isPure {α : Type u'} {f : α → SPComp PUnit.{u_1 + 1}} {xs : List α} (h : ∀ x ∈ xs, (f x).IsPure) : (xs.forM f).IsPure

List.forM over SPComp is heap-pure when the body is heap-pure at every element of the list.

theorem CatCrypt.Core.SPComp.foldlM_isPure {α : Type u'} {σ : Type w'} {f : σ → α → SPComp σ} {xs : List α} (h : ∀ (s : σ), ∀ x ∈ xs, (f s x).IsPure) {s : σ} : (List.foldlM f s xs).IsPure

List.foldlM over SPComp is heap-pure when the step is heap-pure at every accumulator and every element of the list.

List.forM congruence

theorem CatCrypt.Relational.rHoare_forM {α : Type u} {β : Type v} {R : α → β → Prop} {I : RPre} {f : α → Core.SPComp PUnit.{u_1 + 1}} {g : β → Core.SPComp PUnit.{u_2 + 1}} {xs : List α} {ys : List β} (hR : List.Forall₂ R xs ys) (hbody : ∀ (x : α) (y : β), R x y → rHoare I (f x) (g y) fun (x : PUnit.{u_1 + 1}) (h₁ : Core.Heap) (x_1 : PUnit.{u_2 + 1}) (h₂ : Core.Heap) => I h₁ h₂) : rHoare I (xs.forM f) (ys.forM g) fun (x : PUnit.{u_1 + 1}) (h₁ : Core.Heap) (x_1 : PUnit.{u_2 + 1}) (h₂ : Core.Heap) => I h₁ h₂

Loop congruence for List.forM: if xs and ys are related pointwise by R and every related pair of loop bodies preserves the heap invariant I, then the two loops preserve I.

theorem CatCrypt.Relational.rHoare_forM_same {α : Type u} {I : RPre} {f : α → Core.SPComp PUnit.{u_1 + 1}} {g : α → Core.SPComp PUnit.{u_2 + 1}} (xs : List α) (hbody : ∀ x ∈ xs, rHoare I (f x) (g x) fun (x : PUnit.{u_1 + 1}) (h₁ : Core.Heap) (x_1 : PUnit.{u_2 + 1}) (h₂ : Core.Heap) => I h₁ h₂) : rHoare I (xs.forM f) (xs.forM g) fun (x : PUnit.{u_1 + 1}) (h₁ : Core.Heap) (x_1 : PUnit.{u_2 + 1}) (h₂ : Core.Heap) => I h₁ h₂

Synchronous specialization of rHoare_forM: both sides iterate over the same list xs, with loop bodies f and g related pointwise on the elements of xs.

List.foldlM congruence

theorem CatCrypt.Relational.rHoare_foldlM {α : Type u} {β : Type v} {σ₁ : Type w} {σ₂ : Type x} {R : α → β → Prop} {V : σ₁ → σ₂ → Prop} {I : RPre} {f : σ₁ → α → Core.SPComp σ₁} {g : σ₂ → β → Core.SPComp σ₂} {xs : List α} {ys : List β} (hR : List.Forall₂ R xs ys) (hbody : ∀ (s₁ : σ₁) (s₂ : σ₂) (x : α) (y : β), R x y → V s₁ s₂ → rHoare I (f s₁ x) (g s₂ y) fun (t₁ : σ₁) (h₁ : Core.Heap) (t₂ : σ₂) (h₂ : Core.Heap) => I h₁ h₂ ∧ V t₁ t₂) {s₁ : σ₁} {s₂ : σ₂} (hV : V s₁ s₂) : rHoare I (List.foldlM f s₁ xs) (List.foldlM g s₂ ys) fun (t₁ : σ₁) (h₁ : Core.Heap) (t₂ : σ₂) (h₂ : Core.Heap) => I h₁ h₂ ∧ V t₁ t₂

Loop congruence for List.foldlM: in addition to the heap invariant I, a value relation V on the accumulators is threaded through every iteration. If the initial accumulators are V-related and each related step preserves both I and V, the folds end I-and-V-related.

theorem CatCrypt.Relational.rHoare_foldlM_same {α : Type u} {σ₁ : Type w} {σ₂ : Type x} {V : σ₁ → σ₂ → Prop} {I : RPre} {f : σ₁ → α → Core.SPComp σ₁} {g : σ₂ → α → Core.SPComp σ₂} (xs : List α) (hbody : ∀ (s₁ : σ₁) (s₂ : σ₂), ∀ x ∈ xs, V s₁ s₂ → rHoare I (f s₁ x) (g s₂ x) fun (t₁ : σ₁) (h₁ : Core.Heap) (t₂ : σ₂) (h₂ : Core.Heap) => I h₁ h₂ ∧ V t₁ t₂) {s₁ : σ₁} {s₂ : σ₂} (hV : V s₁ s₂) : rHoare I (List.foldlM f s₁ xs) (List.foldlM g s₂ xs) fun (t₁ : σ₁) (h₁ : Core.Heap) (t₂ : σ₂) (h₂ : Core.Heap) => I h₁ h₂ ∧ V t₁ t₂

Synchronous specialization of rHoare_foldlM: both sides fold over the same list xs, with step functions related pointwise on elements of xs.

Examples