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 [ProgramSpec] {holes : HoleSigs} {l : Type} (SL : ProgramDenotation (ProcedureState l) Unit) : StmtWithHoles holes l → 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} {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 [ProgramSpec] (S : ProgramDenotation State Unit) {holes : HoleSigs} {l : Type} (A : StmtWithHoles holes l) (eagerInst lazyInst : holes.Instantiation) : SwapLoc (ProgramDenotation.zoom ProcedureState.globalL S) A → (∀ {sig : ProcedureSignature} (n : HoleIndex holes sig) (x : Setter sig.ret (ProcedureState l)) (p : Getter sig.ParamType (ProcedureState l)), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p) → (∀ (ret : sig.ret), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) → (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.globalL S) (fun (σ₁ σ₂ : ProcedureState l) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x (eagerInst n) p)) (programDenotation (StmtWithHoles.call x (lazyInst n) p)) fun (u v : Unit × ProcedureState l) => u = v) → (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.globalL S) (fun (σ₁ σ₂ : ProcedureState l) => σ₁ = σ₂) (programDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst)) (programDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst)) fun (u v : Unit × ProcedureState l) => 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 [ProgramSpec] {sig : ProcedureSignature} {L : Type} (S : ProgramDenotation State Unit) (rv : Getter sig.ret (ProcedureState L)) (initL : L) (B : ProgramDenotation (ProcedureState L) Unit) : (procWrap rv initL do ProgramDenotation.zoom ProcedureState.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' [ProgramSpec] {sig : ProcedureSignature} {L : Type} (rv : Getter sig.ret (ProcedureState L)) : ProgramDenotation.get rv = fun (ps : ProcedureState L) => pure (rv.get ps, ps)

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

theorem GaudisCrypt.rv_block_stable [ProgramSpec] {sig : ProcedureSignature} {L : Type} (S : ProgramDenotation State Unit) (rv : Getter sig.ret (ProcedureState L)) (hret : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get rv) (ProgramDenotation.get rv)) (ps : ProcedureState L) : (do let q ← ProgramDenotation.zoom ProcedureState.globalL S ps pure (rv.get ps, q.2)) = do let q ← ProgramDenotation.zoom ProcedureState.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 [ProgramSpec] {sig : ProcedureSignature} {L : Type} (S : ProgramDenotation State Unit) (rv : Getter sig.ret (ProcedureState L)) (hret : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get rv) (ProgramDenotation.get rv)) (ps : ProcedureState L) : (do let w ← S ps.global pure (rv.get ps, w.2)) = do let w ← S ps.global pure (rv.get { global := w.2, locals := ps.locals }, w.2)

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

theorem GaudisCrypt.procWrap_block_out [ProgramSpec] {sig : ProcedureSignature} {L : Type} (S : ProgramDenotation State Unit) (rv : Getter sig.ret (ProcedureState L)) (initL : L) (B : ProgramDenotation (ProcedureState L) Unit) (hret : (ProgramDenotation.zoom ProcedureState.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 ProcedureState.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 [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (S : ProgramDenotation State Unit) (hbody : (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.globalL S) (fun (σ₁ σ₂ : ProcedureState (sig.LocalVariableState A.locals)) => σ₁ = σ₂) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => eagerInst)) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => lazyInst)) fun (u v : Unit × ProcedureState (sig.LocalVariableState A.locals)) => u = v) (hret : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get A.return_val) (ProgramDenotation.get A.return_val)) : S.eagerR S (fun (σ₁ σ₂ : State) => σ₁ = σ₂) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args) fun (u v : sig.ret × State) => 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 [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (S : ProgramDenotation State Unit) (hloc : SwapLoc (ProgramDenotation.zoom ProcedureState.globalL S) A.body) (hret : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get A.return_val) (ProgramDenotation.get A.return_val)) (hhole : ∀ {sig' : ProcedureSignature} (n : HoleIndex holes sig') (x : Setter sig'.ret (ProcedureState (sig.LocalVariableState A.locals))) (p : Getter sig'.ParamType (ProcedureState (sig.LocalVariableState A.locals))), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p) → (∀ (ret : sig'.ret), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) → (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.globalL S) (fun (σ₁ σ₂ : ProcedureState (sig.LocalVariableState A.locals)) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x (eagerInst n) p)) (programDenotation (StmtWithHoles.call x (lazyInst n) p)) fun (u v : Unit × ProcedureState (sig.LocalVariableState A.locals)) => u = v) : S.eagerR S (fun (σ₁ σ₂ : State) => σ₁ = σ₂) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args) fun (u v : sig.ret × State) => 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 [ProgramSpec] {l : Type} {sig : ProcedureSignature} (S : ProgramDenotation State Unit) (f f' : Procedure sig) (x : Setter sig.ret (ProcedureState l)) (p : Getter sig.ParamType (ProcedureState l)) (hspec : ∀ (args : sig.ParamType), S.eagerR S (fun (σ₁ σ₂ : State) => σ₁ = σ₂) (procedureDenotation f args) (procedureDenotation f' args) fun (u v : sig.ret × State) => u = v) (hp : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p)) (hx : ∀ (ret : sig.ret), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) : (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.globalL S) (fun (σ₁ σ₂ : ProcedureState l) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x f p)) (programDenotation (StmtWithHoles.call x f' p)) fun (u v : Unit × ProcedureState l) => 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 [ProgramSpec] {l : Type} {sig : ProcedureSignature} (S : ProgramDenotation State Unit) (f f' : Procedure sig) (x : Setter sig.ret (ProcedureState l)) (p : Getter sig.ParamType (ProcedureState l)) {P : ProcedureState l → ProcedureState l → Prop} {Q : Unit × ProcedureState l → Unit × ProcedureState l → Prop} (hspec : ∀ (args : sig.ParamType), S.eagerR S (fun (σ₁ σ₂ : State) => σ₁ = σ₂) (procedureDenotation f args) (procedureDenotation f' args) fun (u v : sig.ret × State) => u = v) (hp : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p)) (hx : ∀ (ret : sig.ret), (ProgramDenotation.zoom ProcedureState.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 ProcedureState.globalL S pure a) (do let a ← programDenotation (StmtWithHoles.call x f' p) ProgramDenotation.zoom ProcedureState.globalL S pure a) Q) : (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.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 [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (S : ProgramDenotation State Unit) {P : State → State → Prop} {Q : sig.ret × State → sig.ret × State → Prop} (hloc : SwapLoc (ProgramDenotation.zoom ProcedureState.globalL S) A.body) (hret : (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get A.return_val) (ProgramDenotation.get A.return_val)) (hhole : ∀ {sig' : ProcedureSignature} (n : HoleIndex holes sig') (x : Setter sig'.ret (ProcedureState (sig.LocalVariableState A.locals))) (p : Getter sig'.ParamType (ProcedureState (sig.LocalVariableState A.locals))), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.get p) (ProgramDenotation.get p) → (∀ (ret : sig'.ret), (ProgramDenotation.zoom ProcedureState.globalL S).transferBy (ProgramDenotation.set x ret) (ProgramDenotation.set x ret)) → (ProgramDenotation.zoom ProcedureState.globalL S).eagerR (ProgramDenotation.zoom ProcedureState.globalL S) (fun (σ₁ σ₂ : ProcedureState (sig.LocalVariableState A.locals)) => σ₁ = σ₂) (programDenotation (StmtWithHoles.call x (eagerInst n) p)) (programDenotation (StmtWithHoles.call x (lazyInst n) p)) fun (u v : Unit × ProcedureState (sig.LocalVariableState A.locals)) => u = v) (hself : ProgramDenotation.prhl2 P (do let a ← procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args S pure a) (do let a ← procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args S pure a) Q) : S.eagerR S P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => 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).