The eager abstract-call rule (EasyCrypt's eager proc/eager call)

The instantiation layer of the eager calculus: for a procedure-with-holes A and two hole-instantiations, the whole procedure is eager for a block S provided each hole is (hhole) and A's own operations swap with the lifted block (SwapLoc). This is the calculus-level rule whose soundness is a once-and-for-all induction over the adversary's syntax — the analogue of EasyCrypt's trusted eager proc rule (justified by induction in the metatheory); client derivations only ever apply it.

• SwapLoc SL A — locality: every operation of A outside the holes swaps with the lifted block SL (self-transferBy). For SL := convertL this is definitionally the RO development's Loc, so the existing footprint discharge (confinedP_loc) applies unchanged.
• eager_body — the induction over StmtWithHoles, threading the eagerR rules (eagerR_pure/eagerR_seq/eagerR_while) over the statement structure.
• procWrap_block_in / procWrap_block_out — the block slides through the procedure wrapper (zoom globalL S inside ↔ S outside), generalizing the convert-specific wrapper lemmas.
• eager_call — the assembled rule at the level of procedureDenotation.

Locality

def GaudisCrypt.SwapLoc {holes : HoleSigs} (SL : ProgramDenotation ProgramState Unit) : StmtWithHoles holes → Prop

Swap-locality: every operation of A outside the holes swaps with the block SL (self-transferBy). For a hole, this is the surrounding read (get p) and write (set x) — the hole call itself is not required to swap (it is handled by the per-hole hypothesis).

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.SwapLoc SL GaudisCrypt.StmtWithHoles.skip = True
• GaudisCrypt.SwapLoc SL (s1.seq s2) = (GaudisCrypt.SwapLoc SL s1 ∧ GaudisCrypt.SwapLoc SL s2)
• GaudisCrypt.SwapLoc SL (GaudisCrypt.StmtWithHoles.while c t) = (SL.transferBy (GaudisCrypt.ProgramDenotation.get c) (GaudisCrypt.ProgramDenotation.get c) ∧ GaudisCrypt.SwapLoc SL t)

theorem GaudisCrypt.eagerR_self_of_transferBy {s : Type u_1} {α : Type} {SL : ProgramDenotation s Unit} {p : ProgramDenotation s α} (h : SL.transferBy p p) : SL.eagerR SL (fun (σ₁ σ₂ : s) => σ₁ = σ₂) p p fun (u v : α × s) => u = v

A self-transferBy fact is a (diagonal) self-eager judgment.

The body induction (EC's eager proc)

theorem GaudisCrypt.eager_body (S : ProgramDenotation VariableAssignment Unit) {holes : HoleSigs} (A : StmtWithHoles holes) (eagerInst lazyInst : holes.Instantiation) : SwapLoc (ProgramDenotation.zoom ProgramState.globalL S) A → (∀ {sig : ProcedureSignature} (n : HoleIndex holes sig) (x : Setter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p) → (∀ (ret : sig.ret), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) → (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) (fun (σ₁ σ₂ : ProgramState) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x (eagerInst.lookup n) p)) (programDenotation (StmtWithHoles.call x (lazyInst.lookup n) p)) fun (u v : Unit × ProgramState) => u = v) → (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) (fun (σ₁ σ₂ : ProgramState) => σ₁ = σ₂) (programDenotation (A.instantiate eagerInst)) (programDenotation (A.instantiate lazyInst)) fun (u v : Unit × ProgramState) => u = v

Eager body induction: an arbitrary syntactic body A is eager for the block SL across two hole-instantiations, given swap-locality of its own operations and a per-hole eager hypothesis. The eagerR rules are threaded over the statement structure.

The block slides through the procedure wrapper

theorem GaudisCrypt.procWrap_block_in {sig : ProcedureSignature} (S : ProgramDenotation VariableAssignment Unit) (rv : Getter sig.ret ProgramState) (initL : VariableAssignment) (B : ProgramDenotation ProgramState Unit) : (procWrap rv initL do ProgramDenotation.zoom ProgramState.globalL S B) = do S procWrap rv initL B

The lifted block slides in: S before the wrapper = zoom globalL S before the body, inside the wrapper. Structural.

theorem GaudisCrypt.programGet_eq' {sig : ProcedureSignature} (rv : Getter sig.ret ProgramState) : ProgramDenotation.get rv = fun (ps : ProgramState) => pure (rv.get ps, ps)

ProgramDenotation.get rv reads rv and threads the state through unchanged.

theorem GaudisCrypt.rv_block_stable {sig : ProcedureSignature} (S : ProgramDenotation VariableAssignment Unit) (rv : Getter sig.ret ProgramState) (hret : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get rv) (ProgramDenotation.get rv)) (ps : ProgramState) : (do let q ← ProgramDenotation.zoom ProgramState.globalL S ps pure (rv.get ps, q.2)) = do let q ← ProgramDenotation.zoom ProgramState.globalL S ps pure (rv.get q.2, q.2)

From the return-value swap: reading rv commutes with the lifted block (clean form).

theorem GaudisCrypt.rv_block_invariant {sig : ProcedureSignature} (S : ProgramDenotation VariableAssignment Unit) (rv : Getter sig.ret ProgramState) (hret : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get rv) (ProgramDenotation.get rv)) (ps : ProgramState) : (do let w ← S ps.globals pure (rv.get ps, w.2)) = do let w ← S ps.globals pure (rv.get { globals := w.2, locals := ps.locals }, w.2)

Reading rv is invariant under the block changing the global component.

theorem GaudisCrypt.procWrap_block_out {sig : ProcedureSignature} (S : ProgramDenotation VariableAssignment Unit) (rv : Getter sig.ret ProgramState) (initL : VariableAssignment) (B : ProgramDenotation ProgramState Unit) (hret : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get rv) (ProgramDenotation.get rv)) : (do let r ← procWrap rv initL B S pure r) = procWrap rv initL do let a ← B ProgramDenotation.zoom ProgramState.globalL S pure a

The block slides out: S after the wrapper = the lifted block after the body, inside the wrapper. Consumes hret (the return value swaps with the block, so reading it commutes with the block changing the globals).

The assembled rule

theorem GaudisCrypt.eager_wrapper {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (S : ProgramDenotation VariableAssignment Unit) (hbody : (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) (fun (σ₁ σ₂ : ProgramState) => σ₁ = σ₂) (programDenotation (A.body.instantiate eagerInst)) (programDenotation (A.body.instantiate lazyInst)) fun (u v : Unit × ProgramState) => u = v) (hret : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get A.return_val) (ProgramDenotation.get A.return_val)) : S.eagerR S (fun (σ₁ σ₂ : VariableAssignment) => σ₁ = σ₂) (procedureDenotation (A.instantiate eagerInst) args) (procedureDenotation (A.instantiate lazyInst) args) fun (u v : sig.ret × VariableAssignment) => u = v

Procedure wrapper for the eager judgment: a body-level eager judgment (block zoom globalL S) lifts to a state-level eager judgment (block S) of the whole procedure denotations, provided the return value swaps with the lifted block.

theorem GaudisCrypt.eager_call {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (S : ProgramDenotation VariableAssignment Unit) (hloc : SwapLoc (ProgramDenotation.zoom ProgramState.globalL S) A.body) (hret : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get A.return_val) (ProgramDenotation.get A.return_val)) (hhole : ∀ {sig' : ProcedureSignature} (n : HoleIndex holes sig') (x : Setter sig'.ret ProgramState) (p : Getter sig'.ParamType ProgramState), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p) → (∀ (ret : sig'.ret), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) → (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) (fun (σ₁ σ₂ : ProgramState) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x (eagerInst.lookup n) p)) (programDenotation (StmtWithHoles.call x (lazyInst.lookup n) p)) fun (u v : Unit × ProgramState) => u = v) : S.eagerR S (fun (σ₁ σ₂ : VariableAssignment) => σ₁ = σ₂) (procedureDenotation (A.instantiate eagerInst) args) (procedureDenotation (A.instantiate lazyInst) args) fun (u v : sig.ret × VariableAssignment) => u = v

EC's eager call on an abstract procedure (equality invariants): the whole procedure is eager for S across two hole-instantiations, given swap-locality of its own operations, a swapping return read, and the per-hole eager hypothesis.

theorem GaudisCrypt.eagerR_call {sig : ProcedureSignature} (S : ProgramDenotation VariableAssignment Unit) (f f' : Procedure sig) (x : Setter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) (hspec : ∀ (args : sig.ParamType), S.eagerR S (fun (σ₁ σ₂ : VariableAssignment) => σ₁ = σ₂) (procedureDenotation f args) (procedureDenotation f' args) fun (u v : sig.ret × VariableAssignment) => u = v) (hp : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p)) (hx : ∀ (ret : sig.ret), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) : (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) (fun (σ₁ σ₂ : ProgramState) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x f p)) (programDenotation (StmtWithHoles.call x f' p)) fun (u v : Unit × ProgramState) => u = v

EC's eager call: a (closed) call site is eager, given a proven procedure-level eager specification and swap-stability of the surrounding argument read and result write.

theorem GaudisCrypt.eagerR_call_inv {sig : ProcedureSignature} (S : ProgramDenotation VariableAssignment Unit) (f f' : Procedure sig) (x : Setter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) {P : ProgramState → ProgramState → Prop} {Q : Unit × ProgramState → Unit × ProgramState → Prop} (hspec : ∀ (args : sig.ParamType), S.eagerR S (fun (σ₁ σ₂ : VariableAssignment) => σ₁ = σ₂) (procedureDenotation f args) (procedureDenotation f' args) fun (u v : sig.ret × VariableAssignment) => u = v) (hp : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p)) (hx : ∀ (ret : sig.ret), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) (hself : ProgramDenotation.prhl2 P (do let a ← programDenotation (StmtWithHoles.call x f' p) ProgramDenotation.zoom ProgramState.globalL S pure a) (do let a ← programDenotation (StmtWithHoles.call x f' p) ProgramDenotation.zoom ProgramState.globalL S pure a) Q) : (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) P (programDenotation (StmtWithHoles.call x f p)) (programDenotation (StmtWithHoles.call x f' p)) Q

EC's eager call with an invariant: the equality-level call rule strengthened by a framing self-coupling of the lazy call site.

theorem GaudisCrypt.eager_call_inv {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (S : ProgramDenotation VariableAssignment Unit) {P : VariableAssignment → VariableAssignment → Prop} {Q : sig.ret × VariableAssignment → sig.ret × VariableAssignment → Prop} (hloc : SwapLoc (ProgramDenotation.zoom ProgramState.globalL S) A.body) (hret : (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get A.return_val) (ProgramDenotation.get A.return_val)) (hhole : ∀ {sig' : ProcedureSignature} (n : HoleIndex holes sig') (x : Setter sig'.ret ProgramState) (p : Getter sig'.ParamType ProgramState), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p) → (∀ (ret : sig'.ret), (ProgramDenotation.zoom ProgramState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) → (ProgramDenotation.zoom ProgramState.globalL S).eagerR (ProgramDenotation.zoom ProgramState.globalL S) (fun (σ₁ σ₂ : ProgramState) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x (eagerInst.lookup n) p)) (programDenotation (StmtWithHoles.call x (lazyInst.lookup n) p)) fun (u v : Unit × ProgramState) => u = v) (hself : ProgramDenotation.prhl2 P (do let a ← procedureDenotation (A.instantiate lazyInst) args S pure a) (do let a ← procedureDenotation (A.instantiate lazyInst) args S pure a) Q) : S.eagerR S P (procedureDenotation (A.instantiate eagerInst) args) (procedureDenotation (A.instantiate lazyInst) args) Q

EC's eager proc I on an abstract procedure: the equality-level abstract-call rule strengthened to an invariant P, given a framing self-coupling of the lazy composite under P — the packaged form of EC's per-oracle fl ~ fl / s ~ s : I ==> I side conditions (which discharge it via the standard relational body machinery).