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.

@[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.cons GaudisCrypt.Lib.RO.Instantiate.roSig GaudisCrypt.HoleSigs.empty

noncomputable def GaudisCrypt.Lib.RO.Instantiate.convertL : ProgramDenotation ProgramState Unit

convert lifted from the RO state to a program state.

Equations

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

RO table as a program-state lens

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

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

The RO table as a lens into a program state.

Equations

• GaudisCrypt.Lib.RO.Instantiate.roLift = GaudisCrypt.ProgramState.globalL.chain random_oracle_state

noncomputable def GaudisCrypt.Lib.RO.Instantiate.inpL : Lens input ProgramState

Read the query input: the oracle's parameter slot inp : input.

Equations

• GaudisCrypt.Lib.RO.Instantiate.inpL = GaudisCrypt.localVarLens "inp" input GaudisCrypt.Lib.RO.Instantiate.inpL._proof_1

noncomputable def GaudisCrypt.Lib.RO.Instantiate.outL : Lens output ProgramState

Read/write the result: the oracle's local out : output, which return_val reads back.

Equations

• GaudisCrypt.Lib.RO.Instantiate.outL = GaudisCrypt.localVarLens "out" output GaudisCrypt.Lib.RO.Instantiate.outL._proof_1

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

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

Equations

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

noncomputable def GaudisCrypt.Lib.RO.Instantiate.RO_lazy_body : Stmt

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 : Stmt

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.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.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.inpL_get_entry (st : state) (args : roSig.ParamType) : inpL.get { globals := st, locals := ProcedureWithHoles.initLocals RO_lazy_proc args } = args

On entry, inp holds the query (both oracle procedures have the parameter names ["inp"]).

theorem GaudisCrypt.Lib.RO.Instantiate.inpL_get_entry_eager (st : state) (args : roSig.ParamType) : inpL.get { globals := st, locals := ProcedureWithHoles.initLocals RO_eager_proc args } = args

theorem GaudisCrypt.Lib.RO.Instantiate.inpL_get_outL_set (v : output) (s : ProgramState) : inpL.get (outL.set v s) = inpL.get s

Writing out leaves inp alone.

theorem GaudisCrypt.Lib.RO.Instantiate.outL_get_outL_set (v : output) (s : ProgramState) : outL.get (outL.set v s) = v

theorem GaudisCrypt.Lib.RO.Instantiate.roG_get_outL_set (v : output) (s : ProgramState) : roG.get (outL.set v s) = roG.get s

The RO table and the oracle's locals live in different components.

theorem GaudisCrypt.Lib.RO.Instantiate.outL_get_roG_set (g : input → Option output) (s : ProgramState) : outL.get (roG.set g s) = outL.get s

theorem GaudisCrypt.Lib.RO.Instantiate.roG_get (s : ProgramState) : roG.get s = random_oracle_state.get s.globals

theorem GaudisCrypt.Lib.RO.Instantiate.roG_set_globals (g : input → Option output) (s : ProgramState) : (roG.set g s).globals = random_oracle_state.set g s.globals

theorem GaudisCrypt.Lib.RO.Instantiate.outL_set_globals (v : output) (s : ProgramState) : (outL.set v s).globals = s.globals

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 {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (proc : Procedure sig) (p : Getter sig.ParamType ProgramState) : programDenotation (StmtWithHoles.call x proc p) = do let args ← ProgramDenotation.get p let ret ← ProgramDenotation.zoom ProgramState.globalL (procedureDenotation proc args) ProgramDenotation.set x ret

The denotation of a procedure call, with the called procedure kept intact (programDenotation reconstructs proc from its fields, 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 inst) args = procWrap A.return_val (A.initLocals args) (programDenotation (A.body.instantiate 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 "fv(A) disjoint from oracle_state" reading: the adversary's own operations live in its private local state ProgramState.localL, which is disjoint from the oracle (the RO table sits in globals; the disjointness instance is ProgramState.disjoint_localL_globalL). 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.instNonemptyProgramState : Nonempty ProgramState

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 : Type} {s : Type u_1} (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 : Type} (c : Getter a ProgramState) {R : Footprint ProgramState} (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 : Type} (y : Setter a ProgramState) (w : a) {R : Footprint ProgramState} (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} : StmtWithHoles holes → Footprint ProgramState

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 ns hl hn b r p) = (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.call' x_1 ns hl hn 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 ProgramState

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) ProgramState

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 : Type u} {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 : Type u} {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.

def GaudisCrypt.Lib.RO.Instantiate.ConfinedP {holes : HoleSigs} (R : Footprint ProgramState) : StmtWithHoles holes → 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 ns hl hn b r p) = (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.call' x_1 ns hl hn 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} (R : Footprint ProgramState) (hc : ∀ {sig : ProcedureSignature} (a : HoleIndex holes sig), Countable sig.ParamType) (A : StmtWithHoles holes) : 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 (s : Stmt) : (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 : Type u} {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.convertL_inFootprint : convertL.inFootprint roLift.footprint

convertL is confined to the (lifted) RO table, as a probabilistic range. convertL = globalL.lift convert, whose footprint lies in the globalL-lift of convert's (lift_footprint_le), and convert.inFootprint random_oracle_state.footprint (convert_inFootprint_ro); Lens.footprint_chain identifies the lift of the latter with roLift.footprint. (lift_inFootprint_chain does not apply: its Lens.factor step needs the RO table type in the universe of the state.)

theorem GaudisCrypt.Lib.RO.Instantiate.procDenot_core {sig : ProcedureSignature} (r : Getter sig.ret ProgramState) (σ : state) (f : state → SubProbability state) (pb : ProgramDenotation ProgramState Unit) (init : VariableAssignment) (hbc : (fun (st : ProgramState) => ProgramState.globalL.liftSubProbability f st >>= pb) = fun (st : ProgramState) => do let w ← pb st let st'' ← ProgramState.globalL.liftSubProbability f w.2 pure (w.1, st'')) (hrc : (fun (st : ProgramState) => ProgramState.globalL.liftSubProbability f st >>= ProgramDenotation.get r) = fun (st : ProgramState) => do let w ← ProgramDenotation.get r st let st'' ← ProgramState.globalL.liftSubProbability f w.2 pure (w.1, st'')) : (do let σ' ← f σ let w ← pb { globals := σ', locals := init } pure (r.get w.2, w.2.globals)) = do let u ← do let w ← pb { globals := σ, locals := init } pure (r.get w.2, w.2.globals) 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} (ns : List String) (hl : ns.length = sig.params.length) (hn : ns.Nodup) (b : Stmt) (r : Getter sig.ret ProgramState) (av : sig.ParamType) (Y : Footprint ProgramState) (hb : (programDenotation b).footprint ≤ Y) (hr : (ProgramDenotation.get r).footprint ≤ Y) : (procedureDenotation { parameterNames := ns, parameterNames_length := hl, parameterNames_nodup := hn, body := b, return_val := r } av).inFootprint (ProgramState.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} {sig : ProcedureSignature} (x : Setter sig.ret ProgramState) (ns : List String) (hl : ns.length = sig.params.length) (hn : ns.Nodup) (b : Stmt) (r : Getter sig.ret ProgramState) (p : Getter sig.ParamType ProgramState) (hbody : fvP_stmt b ≤ FVP.fvP_stmt b) : fvP_stmt (StmtWithHoles.call' x ns hl hn b r p) ≤ FVP.fvP_stmt (StmtWithHoles.call' x ns hl hn 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} {a : Type} (x : Setter a ProgramState) (e : Getter (SubProbability a) ProgramState) : 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} (s : StmtWithHoles holes) : 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 ≤ random_oracle_state.footprintᶜ) : fvP_proc A ≤ roLift.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.