Documentation

GaudisCrypt.Lib.RO.TransferInstantiate

Transfer instantiate (theorem 1) #

Lazy/eager distribution equivalence (ProgramDenotation.transfer) for a syntactic adversary: the transferBy calculus, Stable/Loc, the body/wrapper lemmas, and the single confinement entry point ProgramDenotation.transfer_instantiate_of_fvP.

The generic transferBy calculus #

ProgramDenotation.transfer is transferBy convert. We need the same relation at the ProgramState level (with convertL), so we use the generic calculus ProgramDenotation.transferBy from GaudisCrypt.Logic.TransferBy — monad-law combinators, the Kleene while_loop closure, and the zoom lifting lemma (convertL = zoom globalL convert, and zoom is a monad morphism, so any state-level transfer lifts to a zoomed ProgramState one).

Honest locality + the body induction #

fv_proc is sorry in FV.lean, and a computed footprint for an opaque getter/setter is genuinely undefinable. The honest, usable locality condition is semantic: each of the adversary's own operations commutes with convert (i.e. transfers to itself). Loc A collects exactly these per-leaf facts. The oracle hole is exempt — it is handled by the hhole hypothesis (later discharged by the per-query transfer lemma).

source
def GaudisCrypt.Lib.RO.Instantiate.Stable {α : Type} (p : ProgramDenotation ProgramState α) :
Prop

p commutes with convertL ("transfers to itself").

Equations
Instances For
    source
    def GaudisCrypt.Lib.RO.Instantiate.Loc {holes : HoleSigs} :
    StmtWithHoles holes → Prop

    Locality: every operation of A outside the oracle interface is Stable. For a hole, this is the surrounding read (get p) and write (set x) — the oracle query itself is not required stable (it transfers, lazy↦eager).

    Equations
    Instances For
      source
      theorem GaudisCrypt.Lib.RO.Instantiate.transferL_while_loop {c : ProgramDenotation ProgramState Bool} {body_lazy body_eager : ProgramDenotation ProgramState Unit} (hc : Stable c) (hbody : convertL.transferBy body_lazy body_eager) :
      convertL.transferBy (while_loop c body_lazy) (while_loop c body_eager)

      The former hard lemma (now proved): transferBy convertL is closed under while_loop. Instantiates the generic Kleene closure ProgramDenotation.transferBy_while_loop with c := convertL; the condition's self-transfer is literally Stable c.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.body_transfer_gen {holes : HoleSigs} (A : StmtWithHoles holes) (lazyInst eagerInst : holes.Instantiation) :
      Loc A → (∀ {sig : ProcedureSignature} (n : HoleIndex holes sig) (x : Setter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState), Stable (ProgramDenotation.get p) → (∀ (ret : sig.ret), Stable (ProgramDenotation.set x ret)) → convertL.transferBy (programDenotation (StmtWithHoles.call x (lazyInst.lookup n) p)) (programDenotation (StmtWithHoles.call x (eagerInst.lookup n) p))) → convertL.transferBy (programDenotation (A.instantiate lazyInst)) (programDenotation (A.instantiate eagerInst))

      Body induction: an arbitrary syntactic adversary A transfers from its lazy to its eager instantiation, given locality (Loc) of its own operations and a per-hole transfer hypothesis (hhole). Generic over the holes so the induction goes through; specialized to the RO hole below.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.ro_hhole {sig : ProcedureSignature} (n : HoleIndex roHoles sig) (x : Setter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) (hp : Stable (ProgramDenotation.get p)) (hx : ∀ (ret : sig.ret), Stable (ProgramDenotation.set x ret)) :
      convertL.transferBy (programDenotation (StmtWithHoles.call x (RO_lazy.lookup n) p)) (programDenotation (StmtWithHoles.call x (RO_eager.lookup n) p))

      Discharge of the oracle hypothesis for RO: the lazy and eager oracle calls transfer, given the surrounding read/write are stable. This is the concrete hhole for body_transfer_gen with RO_lazy/RO_eager: the query itself transfers by ProgramDenotation.transfer_lazy_query (lifted via transferBy_zoom), and the bridges identify the procedures with the semantic queries.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.transfer_instantiate_body (A : StmtWithHoles roHoles) (hloc : Loc A) :
      convertL.transferBy (programDenotation (A.instantiate RO_lazy)) (programDenotation (A.instantiate RO_eager))

      Body-level RO transfer — fully assembled (only transferL_while_loop remains, via body_transfer_gen). For any syntactic adversary body A that is Local (touches the RO table only through the oracle hole), the lazy and eager instantiations transfer at the ProgramState level.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.procWrap_convertL_in {sig : ProcedureSignature} (rv : Getter sig.ret ProgramState) (initL : VariableAssignment) (B : ProgramDenotation ProgramState Unit) :
      (procWrap rv initL do convertL B) = do convert procWrap rv initL B

      convertL slides in: convert before the wrapper = convertL before the body, inside the wrapper. Structural (no return-value hypothesis).

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.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.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.rv_convertL_stable {sig : ProcedureSignature} (rv : Getter sig.ret ProgramState) (hret : Stable (ProgramDenotation.get rv)) (ps : ProgramState) :
      (do let q ← convertL ps pure (rv.get ps, q.2)) = do let q ← convertL ps pure (rv.get q.2, q.2)

      From hret: reading rv commutes with convertL (clean convertL-form).

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.rv_convert_invariant {sig : ProcedureSignature} (rv : Getter sig.ret ProgramState) (hret : Stable (ProgramDenotation.get rv)) (ps : ProgramState) :
      (do let w ← convert ps.globals pure (rv.get ps, w.2)) = do let w ← convert ps.globals pure (rv.get { globals := w.2, locals := ps.locals }, w.2)

      key: reading rv is invariant under convert changing the table (the global component of rv_convertL_stable).

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.procWrap_convert_out {sig : ProcedureSignature} (rv : Getter sig.ret ProgramState) (initL : VariableAssignment) (B : ProgramDenotation ProgramState Unit) (hret : Stable (ProgramDenotation.get rv)) :
      (do let r ← procWrap rv initL B convert pure r) = procWrap rv initL do let a ← B convertL pure a

      convert slides out: convert after the wrapper = convertL after the body, inside the wrapper. Consumes hret (the return value is RO-disjoint, so reading it commutes with convert changing the table) via rv_convert_invariant.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.transfer_wrapper {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hbody : convertL.transferBy (programDenotation (A.body.instantiate RO_lazy)) (programDenotation (A.body.instantiate RO_eager))) (hret : Stable (ProgramDenotation.get A.return_val)) :
      ProgramDenotation.transfer (procedureDenotation (A.instantiate RO_lazy) args) (procedureDenotation (A.instantiate RO_eager) args)

      Procedure wrapper: a body-level transferBy convertL lifts to a state-level ProgramDenotation.transfer of the whole procedure denotation, provided the return value is RO-disjoint. Assembled from procedureDenotation_eq_procWrap, procWrap_convert_out (uses hret), hbody, and procWrap_convertL_in.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.stable_of_inFootprint_compl {α : Type} {p : ProgramDenotation ProgramState α} (hp : p.inFootprint roLift.footprintᶜ) :
      Stable p

      Stable from probabilistic footprint disjointness. A program confined (in the inFootprint sense) to the complement of the RO table commutes with convertL, i.e. is Stable. The Footprint analogue of stable_of_inRange_compl; the ᶜ-form makes the commute_of_disjoint_footprint disjointness hypothesis le_refl, so no complement_range analog is needed.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.stable_of_confinedP_footprint {α : Type} (R : Footprint ProgramState) (hdisj : R ≤ roLift.footprintᶜ) {p : ProgramDenotation ProgramState α} (hp : p.inFootprint R) :
      Stable p

      Stable from confinement to a footprint disjoint from the RO (probabilistic). The Footprint analogue of stable_of_confined_lens. No complement_range needed — the ᶜ-form bound hdisj feeds inFootprint_mono directly.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.confinedP_loc {holes : HoleSigs} (R : Footprint ProgramState) (hdisj : R ≤ roLift.footprintᶜ) (hc : ∀ {sig : ProcedureSignature} (a : HoleIndex holes sig), Countable sig.ParamType) (A : StmtWithHoles holes) :
      ConfinedP R A → Loc A

      ConfinedP discharges Loc (theorem-1 locality), leaf by leaf — reusing the existing Loc→theorems chain. The Footprint analogue of confined_loc.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.ProgramDenotation.transfer_instantiate_of_fvP {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : fvP_proc A ≤ roLift.footprintᶜ) :
      ProgramDenotation.transfer (procedureDenotation (A.instantiate RO_lazy) args) (procedureDenotation (A.instantiate RO_eager) args)

      Theorem 1, end-to-end from footprint disjointness. Lazy/eager indistinguishability for any adversary whose full footprint fvP_proc A (body + return) is disjoint from the random-oracle state — fvP_proc A ≤ (roLift _).footprintᶜ — derived from that single bound, with no per-leaf confinement to check by hand (lens-free, R-free). Inlines the whole fvP → ConfinedP → Loc → transfer chain — the sole entry point.

      Whole-game form: initialisations included, coupling output #

      The per-query eager/lazy coupling is pointwise unsatisfiable (a fixed eager table entry cannot couple with a fresh lazy sample), so theorem 2's h cannot be discharged for the genuine RO pair. The true lazy = eager statement lives at the whole-game level, where random_oracle_init supplies the eager table's randomness — and that is exactly theorem 1. The results below convert theorem 1 into the coupling format (prhl2 with a result-decided post), giving the h-free end-to-end transfer.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.convert_lossless (σ : state) :
      ↑(convert σ) Set.univ = 1

      convert is lossless (measure form of convert_mass): from any state its run has total mass 1.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.convert_satisfies_of_ro_invariant {β : Type u_1} (g : state → β) (hg : ∀ (Z : input → Option output) (σ : state), g (random_oracle_state.set Z σ) = g σ) (σ : state) :
      (convert σ).satisfies fun (x : Unit × state) => g x.2 = g σ

      convert's support only performs a random_oracle_state write: any state projection g invariant under RO writes is preserved along convert's run. Via the explicit convert_wp_eq formula — no support analysis of the monadic plumbing needed.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.glob_ro_set_invariant {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (hdisj : FVP.fvP_proc A ≤ random_oracle_state.footprintᶜ) (Z : input → Option output) (σ : state) :
      (FVP.glob A).get (random_oracle_state.set Z σ) = (FVP.glob A).get σ

      Writes to the RO table do not move glob A, for any A whose footprint avoids the oracle: under hdisj the write random_oracle_state.set Z is a (fvP_proc A)ᶜ-orbit step, and the touched getter is constant on (fvP_proc A)ᶜ-orbits.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.game_transfer_of_fvP {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : fvP_proc A ≤ roLift.footprintᶜ) :
      (do let a ← do lazy_init procedureDenotation (A.instantiate RO_lazy) args convert pure a) = do random_oracle_init procedureDenotation (A.instantiate RO_eager) args

      Theorem 1 at whole-game level: with the initialisations included, the lazy game followed by a result-preserving convert equals the eager game. Unlike the per-query coupling, this is unconditionally true from footprint disjointness — the eager table's randomness is supplied by random_oracle_init = lazy_init; convert.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.output_win_transfer_games_of_fvP {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (Win : sig.ret → Prop) (hdisj : fvP_proc A ≤ roLift.footprintᶜ) :
      ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (do lazy_init procedureDenotation (A.instantiate RO_lazy) args) (do random_oracle_init procedureDenotation (A.instantiate RO_eager) args) fun (u v : sig.ret × state) => Win u.1 ↔ Win v.1

      Game-level output-decided transfer, semantic disjointness form — see output_win_transfer_games for the user-facing (syntactic-FVP) statement.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.output_win_transfer_games {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (Win : sig.ret → Prop) (hdisj : FVP.fvP_proc A ≤ random_oracle_state.footprintᶜ) :
      ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (do lazy_init procedureDenotation (A.instantiate RO_lazy) args) (do random_oracle_init procedureDenotation (A.instantiate RO_eager) args) fun (u v : sig.ret × state) => Win u.1 ↔ Win v.1

      Game-level output-decided transfer — the h-free counterpart of output_win_transfer, for any adversary whose variables avoid the oracle (FVP.fvP_proc A ≤ oracleᶜ, the same EasyCrypt-style hypothesis as prhl_instantiate_of_glob) and any predicate Win on its result: the whole games (initialisation included) couple with Win u.1 ↔ Win v.1. Collision resistance is the instance where Win r reads "r is a collision A produced". Everything is discharged by theorem 1 (convert-sliding), which owns the eager table's initialisation randomness — no per-query coupling hypothesis remains.

      ={glob A} in the postcondition #

      glob A := (FVP.fvP_proc A).touched_getter (EasyCrypt's glob A). The whole-game coupling not only decides the result: the coupled final states also agree on everything A may touch. The two legs differ by the trailing convert only, convert writes the RO table only, and — under the footprint disjointness — RO writes are (fvP_proc A)ᶜ-orbit steps, invisible to glob A.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.output_glob_transfer_games {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : FVP.fvP_proc A ≤ random_oracle_state.footprintᶜ) :
      ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (do lazy_init procedureDenotation (A.instantiate RO_lazy) args) (do random_oracle_init procedureDenotation (A.instantiate RO_eager) args) fun (u v : sig.ret × state) => u.1 = v.1 ∧ (FVP.glob A).get u.2 = (FVP.glob A).get v.2

      Whole-game transfer with ={glob A} in the postcondition: from equal initial states, the lazy and eager games couple with equal results and (glob A)-equal final states. The glob-enriched form of the coupling behind output_win_transfer_games.

      source
      theorem GaudisCrypt.Lib.RO.Instantiate.output_win_transfer_games_glob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (Win : sig.ret → Prop) (hdisj : FVP.fvP_proc A ≤ random_oracle_state.footprintᶜ) :
      ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (do lazy_init procedureDenotation (A.instantiate RO_lazy) args) (do random_oracle_init procedureDenotation (A.instantiate RO_eager) args) fun (u v : sig.ret × state) => (Win u.1 ↔ Win v.1) ∧ (FVP.glob A).get u.2 = (FVP.glob A).get v.2

      output_win_transfer_games, strengthened with ={glob A}: the games couple with Win-agreement on the results and (glob A)-equal final states.