pRHL loop rules

Synchronized invariant rules for the bounded loop combinator loop_n and for the unbounded while_loop.

The while_loop rule follows EasyCrypt's synchronized while: the guards must agree under the invariant (PostC refines the invariant by the guard value), the bodies preserve the invariant from PostC true, and the loop relates at PostC false. The proof needs no Kleene induction: the left loop's wp is a least fixed point (wp_while), so it suffices to exhibit a prefixed point — fun τ₁ => ⨅ τ₂, ⨅ (_ : Inv τ₁ τ₂), (while₂).wp G τ₂ — the same ENNReal-interpolant trick as rel.trans.

theorem GaudisCrypt.ProgramDenotation.rel.loop_n {s₁ s₂ : Type} {body₁ : ProgramDenotation s₁ Unit} {body₂ : ProgramDenotation s₂ Unit} {Inv : s₁ → s₂ → Prop} (h : body₁.rel body₂ Inv fun (x : Unit × s₁) (y : Unit × s₂) => Inv x.2 y.2) (n : ℕ) : (GaudisCrypt.loop_n n body₁).rel (GaudisCrypt.loop_n n body₂) Inv fun (x : Unit × s₁) (y : Unit × s₂) => Inv x.2 y.2

Synchronized loop rule: if the bodies preserve the relational invariant Inv (as a state relation), so do n synchronized iterations.

theorem GaudisCrypt.ProgramDenotation.relE.loop_n {s₁ s₂ : Type} {body₁ : ProgramDenotation s₁ Unit} {body₂ : ProgramDenotation s₂ Unit} {Inv : s₁ → s₂ → Prop} (h : body₁.relE body₂ Inv fun (x : Unit × s₁) (y : Unit × s₂) => Inv x.2 y.2) (n : ℕ) : (GaudisCrypt.loop_n n body₁).relE (GaudisCrypt.loop_n n body₂) Inv fun (x : Unit × s₁) (y : Unit × s₂) => Inv x.2 y.2

Two-sided synchronized loop rule.

Synchronized while_loop rule

theorem GaudisCrypt.ProgramDenotation.rel.while_loop {s₁ s₂ : Type} {cond₁ : ProgramDenotation s₁ Bool} {body₁ : ProgramDenotation s₁ Unit} {cond₂ : ProgramDenotation s₂ Bool} {body₂ : ProgramDenotation s₂ Unit} {Inv : s₁ → s₂ → Prop} {PostC : Bool → s₁ → s₂ → Prop} (h_cond : cond₁.rel cond₂ Inv fun (u : Bool × s₁) (v : Bool × s₂) => u.1 = v.1 ∧ PostC u.1 u.2 v.2) (h_body : body₁.rel body₂ (PostC true) fun (u : Unit × s₁) (v : Unit × s₂) => Inv u.2 v.2) : (GaudisCrypt.while_loop cond₁ body₁).rel (GaudisCrypt.while_loop cond₂ body₂) Inv fun (u : Unit × s₁) (v : Unit × s₂) => PostC false u.2 v.2

Synchronized while rule: under the invariant the guards agree (PostC b records the invariant refined by the guard value b), the bodies preserve the invariant from PostC true, and the loops relate at PostC false.

theorem GaudisCrypt.ProgramDenotation.relE.while_loop {s₁ s₂ : Type} {cond₁ : ProgramDenotation s₁ Bool} {body₁ : ProgramDenotation s₁ Unit} {cond₂ : ProgramDenotation s₂ Bool} {body₂ : ProgramDenotation s₂ Unit} {Inv : s₁ → s₂ → Prop} {PostC : Bool → s₁ → s₂ → Prop} (h_cond : cond₁.relE cond₂ Inv fun (u : Bool × s₁) (v : Bool × s₂) => u.1 = v.1 ∧ PostC u.1 u.2 v.2) (h_body : body₁.relE body₂ (PostC true) fun (u : Unit × s₁) (v : Unit × s₂) => Inv u.2 v.2) : (GaudisCrypt.while_loop cond₁ body₁).relE (GaudisCrypt.while_loop cond₂ body₂) Inv fun (u : Unit × s₁) (v : Unit × s₂) => PostC false u.2 v.2

Two-sided synchronized while rule.