Instantiate: shared base

RO procedure setup (RO_lazy/RO_eager, denotation bridges), the zoom/transferBy-agnostic monad-morphism lemmas, and the Footprint confinement core (ConfinedP, fvP_stmt, confinedP_of_fv, the Lens.lift framework, convertL_inFootprint). Shared by the transfer (TransferInstantiate) and relational (ROCouplingEquiv) developments.

@[implicit_reducible]

instance GaudisCrypt.Lib.RO.Instantiate.roSpec : ProgramSpec

The ambient state of an RO adversary is the RO state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roSpec = { state := state }

instance GaudisCrypt.Lib.RO.Instantiate.instNonemptyState : Nonempty State

State (= state) is inhabited — needed for Lens.lift_inRange_chain's factor_of_inRange padding.

@[reducible, inline]

abbrev GaudisCrypt.Lib.RO.Instantiate.roSig : ProcedureSignature

The oracle's signature: a query takes an input, returns an output. abbrev so roSig.ParamType reduces to input (for DecidableEq synthesis).

Equations

• GaudisCrypt.Lib.RO.Instantiate.roSig = { params := [input], ret := output }

@[reducible, inline]

abbrev GaudisCrypt.Lib.RO.Instantiate.roHoles : HoleSigs

One oracle hole.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roHoles = GaudisCrypt.HoleSigs.empty.append GaudisCrypt.Lib.RO.Instantiate.roSig

noncomputable def GaudisCrypt.Lib.RO.Instantiate.convertL {l : Type} : ProgramDenotation (ProcedureState l) Unit

convert lifted from the RO State to a procedure state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.convertL = GaudisCrypt.ProgramDenotation.zoom GaudisCrypt.ProcedureState.globalL convert

RO table as a procedure-state lens

roLift is the RO table viewed inside a procedure state. The confinement theorems below all hinge on convertL's probabilistic footprint convertL.inFootprint (roLift l).footprint (convertL_inFootprint), obtained from convert_inFootprint_ro via the Lens.lift framework.

noncomputable def GaudisCrypt.Lib.RO.Instantiate.roLift (l : Type) : Lens (input → Option output) (ProcedureState l)

The RO table as a lens into a procedure state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roLift l = GaudisCrypt.ProcedureState.globalL.chain random_oracle_state

instance GaudisCrypt.Lib.RO.Instantiate.instCountableProcedureState {l : Type} [Countable l] : Countable (ProcedureState l)

ProcedureState l is Countable when its locals are (the global RO state already is) — used to discharge the [Countable] on the instantiation theorems.

def GaudisCrypt.Lib.RO.Instantiate.roLocals : List ((t : Type) × Inhabited t)

The oracle procedure has one local variable, of type output, holding the result that return_val reads back.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roLocals = [⟨output, inferInstance⟩]

@[reducible, inline]

abbrev GaudisCrypt.Lib.RO.Instantiate.roLocalState : Type

The procedure's local state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roLocalState = GaudisCrypt.Lib.RO.Instantiate.roSig.LocalVariableState GaudisCrypt.Lib.RO.Instantiate.roLocals

def GaudisCrypt.Lib.RO.Instantiate.inpL : Lens input (ProcedureState roLocalState)

Read the query input. paramListToTuple [input] = input, so the lens into the parameter tuple is the identity, lifted into the procedure state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.inpL = GaudisCrypt.Lens.id.intoParams

def GaudisCrypt.Lib.RO.Instantiate.outL : Lens output (ProcedureState roLocalState)

Read/write the result. paramListToTuple [output] = output, so likewise.

Equations

• GaudisCrypt.Lib.RO.Instantiate.outL = GaudisCrypt.Lens.id.intoVars

noncomputable def GaudisCrypt.Lib.RO.Instantiate.roG : Lens (input → Option output) (ProcedureState roLocalState)

Read/write the RO table living in the global state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roG = GaudisCrypt.ProcedureState.globalL.chain random_oracle_state

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_lazy_body : StmtWithHoles HoleSigs.empty roLocalState

Lazy body: sample the result (cached → point mass, else uniform), then write the table entry. Two clean-lens statements; denotes to lazy_query.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_eager_body : StmtWithHoles HoleSigs.empty roLocalState

Eager body: read the (pre-sampled) table entry into the result. Denotes to random_oracle_query.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_lazy_proc : Procedure roSig

The lazy oracle as a closed procedure.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_eager_proc : Procedure roSig

The eager oracle as a closed procedure.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_lazy : roHoles.Instantiation

The lazy instantiation of the single oracle hole.

Equations

• GaudisCrypt.Lib.RO.Instantiate.RO_lazy GaudisCrypt.HoleIndex.zero = GaudisCrypt.Lib.RO.Instantiate.RO_lazy_proc

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_eager : roHoles.Instantiation

The eager instantiation of the single oracle hole.

Equations

• GaudisCrypt.Lib.RO.Instantiate.RO_eager GaudisCrypt.HoleIndex.zero = GaudisCrypt.Lib.RO.Instantiate.RO_eager_proc

Denotation bridges: the procedures are lazy_query/random_oracle_query.

(zoom being a monad morphism — ProgramDenotation.zoom_pure/zoom_bind — now lives in GaudisCrypt; the transferBy lift transferBy_zoom in GaudisCrypt.Logic.TransferBy.)

theorem GaudisCrypt.Lib.RO.Instantiate.procDenotation_RO_eager (args : roSig.ParamType) : procedureDenotation RO_eager_proc args = random_oracle_query args

theorem GaudisCrypt.Lib.RO.Instantiate.procDenotation_RO_lazy (args : roSig.ParamType) : procedureDenotation RO_lazy_proc args = lazy_query args

theorem GaudisCrypt.Lib.RO.Instantiate.denote_call {l : Type} {sig : ProcedureSignature} (x : Setter sig.ret (ProcedureState l)) (proc : Procedure sig) (p : Getter sig.ParamType (ProcedureState l)) : programDenotation (StmtWithHoles.call x proc p) = do let args ← ProgramDenotation.get p let ret ← ProgramDenotation.zoom ProcedureState.globalL (procedureDenotation proc args) ProgramDenotation.set x ret

The denotation of a procedure call, with the called procedure kept intact (programDenotation reconstructs ⟨proc.locals, proc.body, proc.return_val⟩, which is proc by structure-eta).

The two subtask-3 theorems

Here A : ProcedureWithHoles roHoles sig is an adversary procedure carrying the single oracle hole. A.instantiate RO_lazy / A.instantiate RO_eager fill that hole, and procedureDenotation _ args : ProgramDenotation state sig.ret runs the result on the RO global state.

theorem GaudisCrypt.Lib.RO.Instantiate.procedureDenotation_eq_procWrap {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (inst : roHoles.Instantiation) : procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => inst) args = procWrap A.return_val (sig.localVariableInit A.locals args) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => inst))

procedureDenotation of an instantiated procedure is procWrap of its body (procWrap now lives in GaudisCrypt).

Faithful hypothesis: the adversary confined to its private local state

The honest "fv(A) disjoint from oracle_state" reading: the adversary's own operations live in its private local state ProcedureState.localL, which is disjoint from the oracle (the RO table sits in global). The magic is that liftRel P pins the locals to equality — so the same confinement assumption discharges both Loc (theorem 1) and LocP (theorem 2), the latter with no P-specific side condition (subtask 3's h' is subsumed).

instance GaudisCrypt.Lib.RO.Instantiate.instDisjointLocalGlobal {l : Type} : disjoint ProcedureState.localL ProcedureState.globalL

The locals and the global part of a ProcedureState are disjoint lenses.

instance GaudisCrypt.Lib.RO.Instantiate.instNonemptyProcedureState {l : Type} [Nonempty l] : Nonempty (ProcedureState l)

theorem GaudisCrypt.Lib.RO.Instantiate.roHole_paramType_countable {sig : ProcedureSignature} (n : HoleIndex roHoles sig) : Countable sig.ParamType

The single roHoles hole has signature roSig, whose query type is Countable. (HoleIndex roHoles sig forces sig = roSig.)

theorem GaudisCrypt.Lib.RO.Instantiate.inFootprint_selfRange {a s : Type} (p : ProgramDenotation s a) : p.inFootprint p.footprint

Self-range over Footprint (PROVEN). For any program with countable return, p.inFootprint p.footprint. This is exactly the statement that is FALSE for DetermFootprint (witness: range_get_fst_eq_bot), whose failure forced get_confined_of_fv/call' to be sorry. Every leaf bridge below is a corollary.

theorem GaudisCrypt.Lib.RO.Instantiate.get_confinedP_of_fv {a l : Type} (c : Getter a (ProcedureState l)) {R : Footprint (ProcedureState l)} (h : (ProgramDenotation.get c).footprint ≤ R) : (ProgramDenotation.get c).inFootprint R

The get bridge over Footprint — PROVEN (the litmus). The probabilistic counterpart of get_confined_of_fv (the open sorry): where the DetermFootprint bridge is self-range for a read (false), this is the litmus, which holds for any read with countable result.

theorem GaudisCrypt.Lib.RO.Instantiate.set_confinedP_of_fv {a l : Type} (y : Setter a (ProcedureState l)) (w : a) {R : Footprint (ProcedureState l)} (h : (ProgramDenotation.set y w).footprint ≤ R) : (ProgramDenotation.set y w).inFootprint R

The setter bridge over Footprint — PROVEN (the litmus). In confined_of_fv the setter bridge had to be assumed (hset); here it is the litmus, for free.

noncomputable def GaudisCrypt.Lib.RO.Instantiate.fvP_stmt {holes : HoleSigs} {l : Type} : StmtWithHoles holes l → Footprint (ProcedureState l)

The probabilistic footprint of a statement. The Footprint analogue of fv_stmt, defined directly as the join of each leaf's own footprint — no fv_reduce/fv_extend machinery is needed, because self-range makes every program its own footprint. In particular the nested call' leaf is just (programDenotation (call' …)).footprint.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.Lib.RO.Instantiate.fvP_stmt GaudisCrypt.StmtWithHoles.skip = ⊥
• GaudisCrypt.Lib.RO.Instantiate.fvP_stmt (GaudisCrypt.StmtWithHoles.sample x_1 e) = (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.sample x_1 e)).footprint
• GaudisCrypt.Lib.RO.Instantiate.fvP_stmt (GaudisCrypt.StmtWithHoles.call' x_1 ls b r p) = (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.call' x_1 ls b r p)).footprint
• GaudisCrypt.Lib.RO.Instantiate.fvP_stmt (s1.seq s2) = GaudisCrypt.Lib.RO.Instantiate.fvP_stmt s1 ⊔ GaudisCrypt.Lib.RO.Instantiate.fvP_stmt s2
• GaudisCrypt.Lib.RO.Instantiate.fvP_stmt (GaudisCrypt.StmtWithHoles.while c t) = (GaudisCrypt.ProgramDenotation.get c).footprint ⊔ GaudisCrypt.Lib.RO.Instantiate.fvP_stmt t

noncomputable def GaudisCrypt.Lib.RO.Instantiate.fvP_proc {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) : Footprint (ProcedureState (sig.LocalVariableState A.locals))

The full probabilistic footprint of a procedure: the body's footprint joined with the return getter's. A single fvP_proc A ≤ R bound feeds both the body confinement and the return-value condition — replacing the separate hbody/hret hypotheses.

Equations

• GaudisCrypt.Lib.RO.Instantiate.fvP_proc A = GaudisCrypt.Lib.RO.Instantiate.fvP_stmt A.body ⊔ (GaudisCrypt.ProgramDenotation.get A.return_val).footprint

theorem GaudisCrypt.Lib.RO.Instantiate.fvP_stmt_body_le_fvP_proc {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) : fvP_stmt A.body ≤ fvP_proc A

theorem GaudisCrypt.Lib.RO.Instantiate.get_return_val_le_fvP_proc {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) : (ProgramDenotation.get A.return_val).footprint ≤ fvP_proc A

noncomputable def GaudisCrypt.Lib.RO.Instantiate.glob {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) : Getter (Quotient (fvP_proc A)ᶜ.orbit_setoid) (ProcedureState (sig.LocalVariableState A.locals))

glob A — the EasyCrypt-style global window of a procedure: the touched_getter of its footprint fvP_proc A. (glob A).get x = (glob A).get y iff x, y agree on everything A owns (they differ only outside fvP_proc A) — i.e. ={glob A}.

Equations

• GaudisCrypt.Lib.RO.Instantiate.glob A = (GaudisCrypt.Lib.RO.Instantiate.fvP_proc A).touched_getter

theorem GaudisCrypt.Lib.RO.Instantiate.lift_inFootprint_self {c s a : Type} (M : Lens c s) (Q : ProgramDenotation c a) : (M.lift Q).inFootprint M.footprint

A lift lives in its lens's probabilistic range — the inFootprint analogue of Lens.lift_inRange_self. The y-generator of (M.lift Q).footprint is the M-localized kernel for Q conditioned on returning y, so Mlocalized_in_footprint applies.

theorem GaudisCrypt.Lib.RO.Instantiate.lift_inFootprint_chain {c s d a : Type} [Nonempty c] (L : Lens c s) (v : Lens d c) (P : ProgramDenotation c a) (hP : P.inFootprint v.footprint) : (L.lift P).inFootprint (L.chain v).footprint

Lift confines the footprint through the chained lens — inFootprint analogue of Lens.lift_inRange_chain. Factor P as v.lift (v.factor P), fold the double lift into a single (L.chain v)-lift (lift_lift_chain), and confine via lift_inFootprint_self.

theorem GaudisCrypt.Lib.RO.Instantiate.convertL_inFootprint {l : Type} : convertL.inFootprint (roLift l).footprint

convertL is confined to the (lifted) RO table, as a probabilistic range. Via the lift framework (avoiding the zoom-rewrite's state/State rw obstacle): convertL = globalL.lift convert, and convert.inFootprint random_oracle_state.footprint (convert_inFootprint_ro).

def GaudisCrypt.Lib.RO.Instantiate.ConfinedP {holes : HoleSigs} {l : Type} (R : Footprint (ProcedureState l)) : StmtWithHoles holes l → Prop

Probabilistic confinement predicate. The inFootprint/footprint analogue of Confined: each leaf's footprint lies in the adversary region L_adv. Crucially the get-leaves are now soundly derivable from footprint disjointness (litmus), unlike Confined (DetermFootprint), where get's ProgramDenotation.range collapses (the get_confined_of_fv sorry).

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.Lib.RO.Instantiate.ConfinedP R GaudisCrypt.StmtWithHoles.skip = True
• GaudisCrypt.Lib.RO.Instantiate.ConfinedP R (GaudisCrypt.StmtWithHoles.sample x_1 e) = (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.sample x_1 e)).inFootprint R
• GaudisCrypt.Lib.RO.Instantiate.ConfinedP R (GaudisCrypt.StmtWithHoles.call' x_1 ls b r p) = (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.call' x_1 ls b r p)).inFootprint R
• GaudisCrypt.Lib.RO.Instantiate.ConfinedP R (s1.seq s2) = (GaudisCrypt.Lib.RO.Instantiate.ConfinedP R s1 ∧ GaudisCrypt.Lib.RO.Instantiate.ConfinedP R s2)
• GaudisCrypt.Lib.RO.Instantiate.ConfinedP R (GaudisCrypt.StmtWithHoles.while c t) = ((GaudisCrypt.ProgramDenotation.get c).inFootprint R ∧ GaudisCrypt.Lib.RO.Instantiate.ConfinedP R t)

theorem GaudisCrypt.Lib.RO.Instantiate.confinedP_of_fv {holes : HoleSigs} {l : Type} (R : Footprint (ProcedureState l)) (hc : ∀ {sig : ProcedureSignature} (a : HoleIndex holes sig), Countable sig.ParamType) (A : StmtWithHoles holes l) : fvP_stmt A ≤ R → ConfinedP R A

fvP-disjointness ⟹ ConfinedP — COMPLETE, no sorry. The full structural reduction that confined_of_fv (DetermFootprint) could only achieve modulo the get sorry (get_confined_of_fv), the orthogonal call' sorry, and an assumed setter bridge (hset). Over Footprint every leaf — get, set, sample, and the nested call' — discharges by the litmus (self-range, inFootprint_selfRange), so the reduction is total. Composing with confinedP_loc/confinedP_locP gives the two main theorems directly from a footprint-disjointness hypothesis.

Self-soundness and the lift/procedureDenotation footprint bounds for call'.

theorem GaudisCrypt.Lib.RO.Instantiate.programDenotation_footprint_le_fvP_stmt {l : Type} (s : Stmt l) : (programDenotation s).footprint ≤ fvP_stmt s

Self-soundness of the pipeline footprint: the denotation of a statement is confined to its own semantic footprint Instantiate.fvP_stmt s. Leaves are equalities; the compound nodes use footprint_bind_le + the recursive bound; while uses while_loop_inFootprint.

theorem GaudisCrypt.Lib.RO.Instantiate.lift_footprint_le {c s a : Type} (L : Lens c s) (Q : ProgramDenotation c a) : (L.lift Q).footprint ≤ L.liftFootprint Q.footprint

The footprint of a lens-lift is bounded by the liftFootprint of the inner footprint. Each return-value slice of L.lift Q is the L-lift of the corresponding slice of Q, so every generator of (L.lift Q).footprint is a generator of liftFootprint L Q.footprint.

theorem GaudisCrypt.Lib.RO.Instantiate.procDenot_core {sig : ProcedureSignature} (ls : List ((t : Type) × Inhabited t)) (r : Getter sig.ret (ProcedureState (sig.LocalVariableState ls))) (σ : State) (f : State → SubProbability State) (pb : ProgramDenotation (ProcedureState (sig.LocalVariableState ls)) Unit) (init : sig.LocalVariableState ls) (hbc : (fun (st : ProcedureState (sig.LocalVariableState ls)) => ProcedureState.globalL.liftSubProbability f st >>= pb) = fun (st : ProcedureState (sig.LocalVariableState ls)) => do let w ← pb st let st'' ← ProcedureState.globalL.liftSubProbability f w.2 pure (w.1, st'')) (hrc : (fun (st : ProcedureState (sig.LocalVariableState ls)) => ProcedureState.globalL.liftSubProbability f st >>= ProgramDenotation.get r) = fun (st : ProcedureState (sig.LocalVariableState ls)) => do let w ← ProgramDenotation.get r st let st'' ← ProcedureState.globalL.liftSubProbability f w.2 pure (w.1, st'')) : (do let σ' ← f σ let w ← pb { global := σ', locals := init } pure (r.get w.2, w.2.global)) = do let u ← do let w ← pb { global := σ, locals := init } pure (r.get w.2, w.2.global) let s'' ← f u.2 pure (u.1, s'')

Core call' commutation. Given that the body pb and the return getter r both commute with globalL.liftSubProbability f, the reduced procedure denotation commutes with f — the heart of the procedureDenotation footprint bound.

theorem GaudisCrypt.Lib.RO.Instantiate.procedureDenotation_inFootprint_reduce {sig : ProcedureSignature} (ls : List ((t : Type) × Inhabited t)) (b : StmtWithHoles HoleSigs.empty (sig.LocalVariableState ls)) (r : Getter sig.ret (ProcedureState (sig.LocalVariableState ls))) (av : sig.ParamType) (Y : Footprint (ProcedureState (sig.LocalVariableState ls))) (hb : (programDenotation b).footprint ≤ Y) (hr : (ProgramDenotation.get r).footprint ≤ Y) : (procedureDenotation { locals := ls, body := b, return_val := r } av).inFootprint (ProcedureState.globalL.reduceFootprint Y)

The reduced procedure denotation is confined to the globalL-reduction of its body+return footprint. Ingredient of the call' FV-soundness case: f outside Lens.reduceFootprint globalL Y lifts to globalL.liftSubProbability f ∈ Yᶜ (Fubini), so the body and return getter commute with it, and procDenot_core then commutes the whole procedure with f.

theorem GaudisCrypt.Lib.RO.Instantiate.fvP_stmt_call_le {holes : HoleSigs} {l : Type} {sig : ProcedureSignature} (x : Setter sig.ret (ProcedureState l)) (ls : List ((t : Type) × Inhabited t)) (b : StmtWithHoles HoleSigs.empty (sig.LocalVariableState ls)) (r : Getter sig.ret (ProcedureState (sig.LocalVariableState ls))) (p : Getter sig.ParamType (ProcedureState l)) (hbody : fvP_stmt b ≤ FVP.fvP_stmt b) : fvP_stmt (StmtWithHoles.call' x ls b r p) ≤ FVP.fvP_stmt (StmtWithHoles.call' x ls b r p)

The call' leaf's footprint is bounded by FV's syntactic footprint. The nested call denotation is get p; zoom globalL (procedureDenotation …); set x; each piece is bounded — the zoom via lift_footprint_le + procedureDenotation_inFootprint_reduce + self-soundness of the body — and the transferred sub-body/return footprints match FV's transfer summands. Takes the body's FV soundness hbody as a hypothesis (from the recursive fvP_stmt_le_FVP).

theorem GaudisCrypt.Lib.RO.Instantiate.fvP_stmt_sample_le {holes : HoleSigs} {l a : Type} (x : Setter a (ProcedureState l)) (e : Getter (SubProbability a) (ProcedureState l)) : fvP_stmt (StmtWithHoles.sample x e) ≤ FVP.fvP_stmt (StmtWithHoles.sample x e)

The sample leaf's footprint is bounded by setter x ⊔ getter e — the sample case of FV soundness, isolated (so unification never has to reduce programDenotation while matching the outer join). The inner sample-body μ.toProgramDenotation >>= set x lands in setter x (its sampled part is ⊥), and the leading get e in getter e.

theorem GaudisCrypt.Lib.RO.Instantiate.fvP_stmt_le_FVP {holes : HoleSigs} {l : Type} (s : StmtWithHoles holes l) : fvP_stmt s ≤ FVP.fvP_stmt s

FV soundness (statement level) — ingredient (A): the pipeline's semantic per-statement footprint Instantiate.fvP_stmt s is bounded by FV's syntactic one FVP.fvP_stmt s. By structural recursion on s: leaves are bounded via footprint_bind_le (matching setter/ getter), the call' leaf via fvP_stmt_call_le (fed the body's recursive bound), and the structural nodes by ⊔-monotonicity + the recursive bound.

theorem GaudisCrypt.Lib.RO.Instantiate.fvP_proc_le_roLift_compl {holes : HoleSigs} {sig : ProcedureSignature} (A : ProcedureWithHoles holes sig) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : fvP_proc A ≤ (roLift (sig.LocalVariableState A.locals)).footprintᶜ

Bridge: FV's (global, syntactic) fvP_proc disjointness ⟹ the pipeline's (procedure-state, semantic) disjointness. FVP.fvP_proc A (a Footprint State, the globalL-reduction of A's syntactic footprint) over-approximates the pipeline's semantic fvP_proc A after reduction, so a disjointness from random_oracle_state on the global state gives the disjointness from roLift = globalL.chain random_oracle_state the confinement needs. Two ingredients: (1) FV soundness — the pipeline's semantic fvP_stmt is bounded by FV's syntactic one; and (2) the reduce/chain transfer through globalL (where the locals drop out — they are ⊥ to the oracle).

theorem GaudisCrypt.Lib.RO.Instantiate.procedureDenotation_inFootprint_fvP_proc {sig : ProcedureSignature} (P : Procedure sig) (args : sig.ParamType) : (procedureDenotation P args).inFootprint (FVP.fvP_proc P)

Procedure confinement at the global state: a procedure's denotation lies in the footprint FV computes for it. (procedureDenotation P args).inFootprint (FVP.fvP_proc P).

This is the companion of FVP.glob — glob P reads what P may touch, and this says P only acts there — and it is what a ={glob P} adversary rule has to be fed: with it, prhl2_self_of_orbit (GlobTransfer.lean) applies to any procedure, since the orbit precondition there is exactly what (FVP.fvP_proc P).touched_getter-equality unfolds to.

Nothing here is RO-specific; it is assembled from the generic parts of this file (procedureDenotation_inFootprint_reduce at Y := FVP.fvP_stmt body ⊔ (get return).footprint, plus FV soundness programDenotation_footprint_le_fvP_stmt/fvP_stmt_le_FVP for the body), together with FVP.fvP_proc being definitionally the globalL-reduction of that same Y. Like those ingredients it would sit better beside FVP.fvP_proc in FV.lean; that move is blocked only by the fact that the whole generic block lives here, downstream of FV.lean.