The eager relational judgment (EasyCrypt's eager logic)

EasyCrypt's judgment eager [S₁, c₁ ~ c₂, S₂] : P ==> Q means {P} S₁; c₁ ~ c₂; S₂ {Q} — two independent swapped blocks, leading on the left program and trailing on the right. We mirror that literally:

`eagerR S₁ S₂ P p q Q  :=  {P}  S₁; p  ~  q; S₂  {Q}`   (as a `prhl2` coupling)

so p is the "eager" side (the block leads) and q the "lazy" side (the block trails, keeping q's result). The generality of two blocks is load-bearing: EC's eager seq threads a middle block (eager[S₁,c₁~c₁',S] → eager[S,c₂~c₂',S₂] → eager[S₁,c₁;c₂~c₁';c₂',S₂]), which eagerR_seq reproduces. The judgment is a prhl2 judgment about the two composite programs, so a derivation built from the rules below is a pRHL derivation.

The bridge

At equality invariants the eager judgment is program equality of the composites:

• prhl2_eq_iff — equality couplings are sound and complete for program equality: prhl2 (=) p q (=) ↔ ∀ σ, p σ = q σ. (Soundness is the diagonal coupling; completeness reads the marginals off the diagonal support, atom by atom.)
• eagerR_eq_iff_transferBy — the diagonal (S₁ = S₂) equality-invariant judgment is the distributional transfer relation, transferBy S q p.

The equality-invariant rules (eagerR_pure, eagerR_seq, eagerR_while, eagerR_zoom) are proven through the bridge; eagerR_conseq is native. EasyCrypt's own eager workflow runs at ={glob …} invariants, which in this shallow embedding are handled by composing the equality-invariant judgment with invariant self-couplings (see the abstract-call rule in Logic/EagerProc.lean).

def GaudisCrypt.ProgramDenotation.eagerR {s α : Type} (S₁ S₂ : ProgramDenotation s Unit) (P : s → s → Prop) (p q : ProgramDenotation s α) (Q : α × s → α × s → Prop) : Prop

The eager judgment (EasyCrypt's eager [S₁, p ~ q, S₂] : P ==> Q): {P} S₁; p ~ q; S₂ {Q} as a prhl2 coupling; the trailing block keeps q's result.

Equations

• S₁.eagerR S₂ P p q Q = GaudisCrypt.ProgramDenotation.prhl2 P (do S₁ p) (do let a ← q S₂ pure a) Q

Equality couplings are sound and complete

theorem GaudisCrypt.ProgramDenotation.eq_of_prhl2_eq {s α : Type} {p q : ProgramDenotation s α} (h : prhl2 (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) (σ : s) : p σ = q σ

Completeness: a coupling with equality pre/post forces pointwise equal distributions — off-diagonal atoms vanish, so the two marginals agree atom by atom.

theorem GaudisCrypt.ProgramDenotation.prhl2_of_eq {s α : Type} {p q : ProgramDenotation s α} (h : ∀ (σ : s), p σ = q σ) : prhl2 (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v

Soundness: pointwise equal programs couple diagonally.

theorem GaudisCrypt.ProgramDenotation.prhl2_eq_iff {s α : Type} (p q : ProgramDenotation s α) : (prhl2 (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) ↔ ∀ (σ : s), p σ = q σ

Equality couplings ↔ program equality.

theorem GaudisCrypt.ProgramDenotation.eagerR_of_eq {s α : Type} {S₁ S₂ : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h : (do S₁ p) = do let a ← q S₂ pure a) : S₁.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v

Introduce an equality-invariant eager judgment from program equality of the two composites (the semantic entry point for per-operation eager lemmas).

theorem GaudisCrypt.ProgramDenotation.eagerR_to_eq {s α : Type} {S₁ S₂ : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h : S₁.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) : (do S₁ p) = do let a ← q S₂ pure a

Extract program equality of the composites from an equality-invariant eager judgment.

theorem GaudisCrypt.ProgramDenotation.eagerR_eq_iff_transferBy {s α : Type} (S : ProgramDenotation s Unit) (p q : ProgramDenotation s α) : (S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) ↔ S.transferBy q p

The bridge: the diagonal equality-invariant eager judgment is the distributional transfer relation (note the side swap: q is the lazy side).

The eager rule set (equality invariants)

theorem GaudisCrypt.ProgramDenotation.eagerR_conseq {s α : Type} {S₁ S₂ : ProgramDenotation s Unit} {P P' : s → s → Prop} {p q : ProgramDenotation s α} {Q Q' : α × s → α × s → Prop} (h : S₁.eagerR S₂ P p q Q) (hP : ∀ (σ₁ σ₂ : s), P' σ₁ σ₂ → P σ₁ σ₂) (hQ : ∀ (u v : α × s), Q u v → Q' u v) : S₁.eagerR S₂ P' p q Q'

Rule of consequence for the eager judgment (native, any invariants).

theorem GaudisCrypt.ProgramDenotation.eagerR_pure {s α : Type} (S : ProgramDenotation s Unit) (a : α) : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) (pure a) (pure a) fun (u v : α × s) => u = v

pure swaps with any block.

theorem GaudisCrypt.ProgramDenotation.eagerR_seq {s α β : Type} {S₁ S S₂ : ProgramDenotation s Unit} {p₁ q₁ : ProgramDenotation s α} {p₂ q₂ : α → ProgramDenotation s β} (h₁ : S₁.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p₁ q₁ fun (u v : α × s) => u = v) (h₂ : ∀ (a : α), S.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) (p₂ a) (q₂ a) fun (u v : β × s) => u = v) : S₁.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) (p₁ >>= p₂) (q₁ >>= q₂) fun (u v : β × s) => u = v

EC's eager seq: eager judgments chain under >>= through a middle block S — eager[S₁,p₁~q₁,S] then eager[S,p₂~q₂,S₂] give eager[S₁, p₁;p₂ ~ q₁;q₂, S₂].

theorem GaudisCrypt.ProgramDenotation.eagerR_while {s : Type} {S : ProgramDenotation s Unit} {cond : ProgramDenotation s Bool} (h_cond : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) cond cond fun (u v : Bool × s) => u = v) {body_e body_l : ProgramDenotation s Unit} (h_body : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) body_e body_l fun (u v : Unit × s) => u = v) : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) (while_loop cond body_e) (while_loop cond body_l) fun (u v : Unit × s) => u = v

EC's eager while (same block at both ends): if the condition swaps with S and the body is eager, the loops are eager.

theorem GaudisCrypt.ProgramDenotation.eagerR_zoom {s t α : Type} (lens : Lens s t) {S₁ S₂ : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h : S₁.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) : (zoom lens S₁).eagerR (zoom lens S₂) (fun (σ₁ σ₂ : t) => σ₁ = σ₂) (zoom lens p) (zoom lens q) fun (u v : α × t) => u = v

Zoom-lifting: an eager judgment on the inner state lifts along a lens (the blocks lift with it).

Invariant introduction

EasyCrypt's invariant-carrying eager rules (eager seq … : R, eager while I, eager proc I) all decompose the same way, visible in the subgoals their kernel generates: the equality-invariant eager judgment plus framing self-couplings of one composite under the invariant (EC's c ~ c / s ~ s : I ==> I side conditions). The two master rules below are that decomposition as a theorem: an invariant eager judgment is a self-coupling of either composite glued to the equality judgment by prhl2.trans. The EC-shaped composite rules (eagerR_seq_inv, eagerR_while_inv, eager_call_inv) derive from them.

theorem GaudisCrypt.ProgramDenotation.eagerR_of_self_left {s α : Type} {S₁ S₂ : ProgramDenotation s Unit} {p q : ProgramDenotation s α} {P : s → s → Prop} {Q : α × s → α × s → Prop} (hself : prhl2 P (do S₁ p) (do S₁ p) Q) (heq : S₁.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) : S₁.eagerR S₂ P p q Q

Invariant introduction (left): self-couple the eager composite S₁; p under the invariant, then glue the equality-invariant judgment on the right.

theorem GaudisCrypt.ProgramDenotation.eagerR_of_self_right {s α : Type} {S₁ S₂ : ProgramDenotation s Unit} {p q : ProgramDenotation s α} {P : s → s → Prop} {Q : α × s → α × s → Prop} (heq : S₁.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) (hself : prhl2 P (do let a ← q S₂ pure a) (do let a ← q S₂ pure a) Q) : S₁.eagerR S₂ P p q Q

Invariant introduction (right): symmetrically, self-couple the lazy composite q; S₂ under the invariant.

theorem GaudisCrypt.ProgramDenotation.eagerR_seq_inv {s α β : Type} {S₁ S S₂ : ProgramDenotation s Unit} {p₁ q₁ : ProgramDenotation s α} {p₂ q₂ : α → ProgramDenotation s β} {P : s → s → Prop} {M : α × s → α × s → Prop} {Q : β × s → β × s → Prop} (h₁ : S₁.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p₁ q₁ fun (u v : α × s) => u = v) (h₂ : ∀ (a : α), S.eagerR S₂ (fun (σ₁ σ₂ : s) => σ₁ = σ₂) (p₂ a) (q₂ a) fun (u v : β × s) => u = v) (hframe₁ : prhl2 P (do S₁ p₁) (do S₁ p₁) M) (hframe₂ : ∀ (a₁ a₂ : α), prhl2 (fun (τ₁ τ₂ : s) => M (a₁, τ₁) (a₂, τ₂)) (p₂ a₁) (p₂ a₂) Q) : S₁.eagerR S₂ P (p₁ >>= p₂) (q₁ >>= q₂) Q

EC's eager seq with invariants (their four-subgoal form): the two equality-level eager judgments plus framing self-couplings of the eager-side pieces, threaded through a middle relation M.

theorem GaudisCrypt.ProgramDenotation.eagerR_while_inv {s : Type} {S : ProgramDenotation s Unit} {cond : ProgramDenotation s Bool} {body_e body_l : ProgramDenotation s Unit} {P Inv : s → s → Prop} {PostC : Bool → s → s → Prop} (h_cond_eq : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) cond cond fun (u v : Bool × s) => u = v) (h_body_eq : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) body_e body_l fun (u v : Unit × s) => u = v) (hS_self : prhl2 P S S fun (u v : Unit × s) => Inv u.2 v.2) (h_cond_self : prhl2 Inv cond cond fun (u v : Bool × s) => u.1 = v.1 ∧ PostC u.1 u.2 v.2) (h_body_self : prhl2 (PostC true) body_e body_e fun (u v : Unit × s) => Inv u.2 v.2) : S.eagerR S P (while_loop cond body_e) (while_loop cond body_l) fun (u v : Unit × s) => PostC false u.2 v.2

EC's eager while with invariants (their six-subgoal form, coupling formulation): the equality-level eager judgments for guard and body, plus framing self-couplings — the block establishes the loop invariant Inv, the guard couples to agree under it, and the body preserves it.

Endpoint conversion

theorem GaudisCrypt.ProgramDenotation.eagerR_to_coupling {s α β : Type} {S : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (g : s → β) (hll : ∀ (σ : s), ↑(S σ) Set.univ = 1) (hkeep : ∀ (σ : s), (S σ).satisfies fun (x : Unit × s) => g x.2 = g σ) (h : S.eagerR S (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p q fun (u v : α × s) => u = v) : prhl2 (fun (σ₁ σ₂ : s) => σ₁ = σ₂) q (do S p) fun (u v : α × s) => u.1 = v.1 ∧ g u.2 = g v.2

Absorb the trailing block into a direct coupling: from a diagonal eager judgment and losslessness of S, couple the lazy side q directly against the S-led eager side, with equal results and any S-preserved state projection g (e.g. ={glob A}) equal on the final states.