The transferBy calculus

The generic "sliding coupling" relation between programs:

• ProgramDenotation.transferBy c p q holds when the coupling program c (think: convert, filling in a lazily sampled random-oracle table) slides from after p to before q, preserving p's value: (p >>= fun a => c >>= fun _ => pure a) = (c >>= fun _ => q).

• Closure combinators: transferBy_pure, transferBy_bind, transferBy_while_loop (Kleene/ωSup argument), transferBy_zoom (lifting along a lens into a larger state).

• Reflexivity from commutation: transferBy_refl_of_commute and its footprint form transferBy_refl_of_inFootprint_compl — a program whose probabilistic footprint avoids c's footprint transfers to itself. transferBy_comm_cont is the converse direction (self-transfer gives commutation in continuation-passing form).

• Consequences at the wp/marginal level: transferBy_wp_invariant, transferBy_wp_value, transferBy_marginal_invariant, transferBy_value_marginal — for c-invariant (resp. state-blind) postconditions, transfer gives wp-equality and equal output marginals.

The lazy/eager random-oracle transfer (ProgramDenotation.transfer in GaudisCrypt.Lib.RO.TransferConvert) is transferBy convert; its ProcedureState variant (Stable/Loc in GaudisCrypt.Lib.RO.TransferInstantiate) is transferBy convertL.

def GaudisCrypt.ProgramDenotation.transferBy {s α : Type} (c : ProgramDenotation s Unit) (p q : ProgramDenotation s α) : Prop

Generic transfer: c slides from after p to before q, preserving the value.

Equations

• c.transferBy p q = ((do let a ← p c pure a) = do c q)

Monad-law combinators

theorem GaudisCrypt.ProgramDenotation.transferBy_pure {s α : Type} {c : ProgramDenotation s Unit} (a : α) : c.transferBy (pure a) (pure a)

pure transfers to itself.

theorem GaudisCrypt.ProgramDenotation.transferBy_bind {s α β : Type} {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} {p' q' : α → ProgramDenotation s β} (h : c.transferBy p q) (h' : ∀ (a : α), c.transferBy (p' a) (q' a)) : c.transferBy (p >>= p') (q >>= q')

transferBy chains under >>=.

theorem GaudisCrypt.ProgramDenotation.transferBy_unit_bind {s : Type} {c p q : ProgramDenotation s Unit} (h : c.transferBy p q) : (do p c) = do c q

For Unit-valued programs the transfer is a plain bind equation: p; c = c; q.

theorem GaudisCrypt.ProgramDenotation.transferBy_of_unit_bind {s : Type} {c p q : ProgramDenotation s Unit} (h : (do p c) = do c q) : c.transferBy p q

Converse of transferBy_unit_bind: a plain bind equation between Unit-valued programs is a transfer.

theorem GaudisCrypt.ProgramDenotation.transferBy_zoom {s t α : Type} (lens : Lens s t) {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h : c.transferBy p q) : (zoom lens c).transferBy (zoom lens p) (zoom lens q)

zoom lifts transferBy: a state-level transfer becomes a zoomed one.

Reflexivity from commutation

theorem GaudisCrypt.ProgramDenotation.transferBy_refl_of_commute {s α : Type} {c : ProgramDenotation s Unit} {p : ProgramDenotation s α} (h : (do let a ← p let b ← c pure (a, b)) = do let b ← c let a ← p pure (a, b)) : c.transferBy p p

Self-transfer from pair-output commutation with c.

theorem GaudisCrypt.ProgramDenotation.transferBy_cont {s α β : Type} {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h : c.transferBy p q) (k : α → ProgramDenotation s β) : (do let a ← p c k a) = c >>= fun (x : Unit) => q >>= k

Continuation form of the transfer: c slides past p in front of any continuation k, turning p into q. At p = q this says a self-transferring program commutes with c (the converse direction of transferBy_refl_of_commute).

theorem GaudisCrypt.ProgramDenotation.transferBy_refl_of_inFootprint_compl {s α : Type} {F : Footprint s} {c : ProgramDenotation s Unit} (hc : c.inFootprint F) {p : ProgramDenotation s α} (hp : p.inFootprint Fᶜ) : c.transferBy p p

Self-transfer from footprint disjointness: a program whose probabilistic footprint avoids c's footprint commutes with c (commute_of_disjoint_footprint), so transfers to itself. The ᶜ-form makes the disjointness hypothesis le_refl.

Closure under while_loop (Kleene/ωSup argument)

Couple every finite iterate of the two loops via an intermediate whileBy_Ψ whose else-branch is c (representing "loop terminates, then couple"), then take the ωSup.

theorem GaudisCrypt.ProgramDenotation.transferBy_while_loop {s : Type} {c : ProgramDenotation s Unit} {cond : ProgramDenotation s Bool} (h_cond : c.transferBy cond cond) {body_lazy body_eager : ProgramDenotation s Unit} (h_body : c.transferBy body_lazy body_eager) : c.transferBy (while_loop cond body_lazy) (while_loop cond body_eager)

transferBy is preserved by while_loop. If the condition transfers to itself (e.g. by transferBy_refl_of_inFootprint_compl) and the body transfers, then the two loops transfer.

Consequences at the wp and marginal level

theorem GaudisCrypt.ProgramDenotation.wp_const_of_mass_one {s : Type} {c : ProgramDenotation s Unit} (h_mass : ∀ (σ : s), c.wp (fun (x : Unit × s) => 1) σ = 1) (k : ENNReal) (σ : s) : c.wp (fun (x : Unit × s) => k) σ = k

c.wp of a constant post is that constant, provided c has total mass 1.

theorem GaudisCrypt.ProgramDenotation.transferBy_wp_invariant {s α : Type} {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h_transfer : c.transferBy p q) (h_absorb : (do c q) = q) (F : α × s → ENNReal) (hF_inv : ∀ (a : α) (σ : s), c.wp (fun (uσ : Unit × s) => F (a, uσ.2)) σ = F (a, σ)) (σ₀ : s) : p.wp F σ₀ = q.wp F σ₀

Transfer at the wp level for c-invariant postconditions: if the post F is invariant under running c (in the wp sense), then transfer + absorption give wp-equality of p and q on F at any starting state.

theorem GaudisCrypt.ProgramDenotation.transferBy_wp_value {s α : Type} {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h_transfer : c.transferBy p q) (h_absorb : (do c q) = q) (h_mass : ∀ (σ : s), c.wp (fun (x : Unit × s) => 1) σ = 1) (G : α → ENNReal) (σ₀ : s) : p.wp (fun (aσ : α × s) => G aσ.1) σ₀ = q.wp (fun (aσ : α × s) => G aσ.1) σ₀

Transfer at the wp level for value-only postconditions: for G : α → ENNReal, the wps of p and q against fun aσ => G aσ.1 agree, given transfer, absorption, and that c is a probability (mass 1).

theorem GaudisCrypt.ProgramDenotation.transferBy_value_marginal {s α : Type} {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h_transfer : c.transferBy p q) (h_absorb : (do c q) = q) (h_mass : ∀ (σ : s), c.wp (fun (x : Unit × s) => 1) σ = 1) (σ₀ : s) : (do let aσ ← p σ₀ pure aσ.1) = do let aσ ← q σ₀ pure aσ.1

Value marginal: SubProb-level statement of the transfer.

theorem GaudisCrypt.ProgramDenotation.transferBy_marginal_invariant {s α β : Type} {c : ProgramDenotation s Unit} {p q : ProgramDenotation s α} (h_transfer : c.transferBy p q) (h_absorb : (do c q) = q) (h : s → β) (h_inv : ∀ (g : β → ENNReal) (σ : s), c.wp (fun (uσ : Unit × s) => g (h uσ.2)) σ = g (h σ)) (σ₀ : s) : (do let aσ ← p σ₀ pure (aσ.1, h aσ.2)) = do let aσ ← q σ₀ pure (aσ.1, h aσ.2)

Marginal at the (value × c-invariant projection) level: instead of projecting to just the value, additionally include any state projection h : s → β that is invariant under running c (in the wp sense).