fvP: the computed-footprint (free-variables) layer over Footprint

The probabilistic re-incarnation of the old FV development (now quarantined as CounterExamples/FV.lean), rebased from the deterministic DetermFootprint/Function.End foundation onto Footprint and the Kleisli monoid of sub-probability kernels m → SubProbability m.

It instantiates the generic InductiveFunctionGettersSetters/ReducibleGettersSetters machinery (from Language.Modules.InductiveFunctions) at T := Footprint, giving a syntactic over-approximation fvP of the part of the state a Module/Procedure can read or modify, together with the soundness bound fvP (m.toModule) ≤ fvPMexpr m.

fvP_extend_sup

theorem GaudisCrypt.kmul_prod_apply {a b : Type} (F G : a × b → SubProbability (a × b)) (x : a × b) : (F * G) x = G x >>= F

Kleisli product of a × b-kernels in bind form.

instance GaudisCrypt.instNonemptyComplContent {s : Type u_1} {a : Type u_2} [Nonempty s] (lens : Lens a s) : Nonempty lens.ComplContent

@[reducible]

def GaudisCrypt.Lens.instContentNonempty {s : Type u_1} {a : Type u_2} [Nonempty s] (lens : Lens a s) : Nonempty a

Equations

• ⋯ = ⋯

theorem GaudisCrypt.Lens.liftFootprint_iSup {a b : Type} {ι : Sort u_1} (lens : Lens a b) (rs : ι → Footprint a) : lens.liftFootprint (⨆ (i : ι), rs i) = ⨆ (i : ι), lens.liftFootprint (rs i)

Lens.liftFootprint distributes over arbitrary indexed suprema. Generalises Lens.liftFootprint_sup from binary joins to indexed families.

End of fvP_extend_sup

Lens.reduceFootprint_sup

End of Lens.reduceFootprint_sup

noncomputable def GaudisCrypt.ProgramDenotation.footprint' {s a b : Type} (progs : a → ProgramDenotation s b) : Footprint s

Family version of ProgramDenotation.footprint: the supremum of the per-input ranges. Used to give a setter (which is a family a → ProgramDenotation s Unit, one program per written value) a single footprint.

Equations

• GaudisCrypt.ProgramDenotation.footprint' progs = ⨆ (x : a), (progs x).footprint

Properties of Lens.reduceFootprint / Lens.liftFootprint needed for the framework instance.

lens.liftSubProbability is a monoid homomorphism, and the resulting closure algebra.

theorem GaudisCrypt.FVP.updateK_one {a b : Type} (lens : Lens a b) : lens.liftSubProbability 1 = 1

lens.liftSubProbability preserves the identity kernel.

theorem GaudisCrypt.FVP.updateK_diracKer {a s : Type} (lens : Lens a s) (g : Function.End a) : lens.liftSubProbability (diracKer g) = diracKer (lens.liftFunction g)

A diracKer of a localized deterministic update is the updateK of the base diracKer (alias of Lens.liftSubProbability_diracKer, kept under the updateK naming of this file).

theorem GaudisCrypt.FVP.Lens.reduceFootprint_extend_le {a b : Type} (lens : Lens a b) (r : Footprint a) : lens.reduceFootprint (lens.liftFootprint r) ≤ r

Lens.reduceFootprint is a retraction of Lens.liftFootprint (reduce (extend r) ≤ r): pushing a footprint forward along a lens and pulling it back recovers at most it. Proven in full from updateK being a monoid homomorphism (centralizer_preimage_image_subset).

theorem GaudisCrypt.FVP.Lens.reduceFootprint_extend {a b : Type} [Nonempty b] (lens : Lens a b) (r : Footprint a) : lens.reduceFootprint (lens.liftFootprint r) = r

Lens.reduceFootprint is an exact left inverse of Lens.liftFootprint (strengthening Lens.reduceFootprint_extend to equality): every p ∈ r.updates is itself Lens.reduceSubProbability lens (lens.liftSubProbability p, i, o) for the trivial i () = pure β / o _ = pure (), hence lies in the generator set defining Lens.reduceFootprint.

noncomputable def GaudisCrypt.FVP.fvpInductiveFunctionGS : InductiveFunctionGettersSetters Footprint

Equations

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

noncomputable def GaudisCrypt.FVP.fvPMexpr [ProgramSpec] (m : ModuleExpression) : Footprint State

Equations

• GaudisCrypt.FVP.fvPMexpr m = GaudisCrypt.FVP.fvpInductiveFunctionGS.evalMexpr m

noncomputable def GaudisCrypt.FVP.fvP [ProgramSpec] {M : Type 1} [IsModule M] (m : M) : Footprint State

Equations

• GaudisCrypt.FVP.fvP m = GaudisCrypt.FVP.fvpInductiveFunctionGS.eval m

@[implicit_reducible]

def GaudisCrypt.FVP.instReducibleGettersSettersFootprintFvpInductiveFunctionGS : ReducibleGettersSetters fvpInductiveFunctionGS

Equations

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

theorem GaudisCrypt.FVP.fvPMexpr_upper_bound [ProgramSpec] {mt : ModuleTypeRep} {m : ModuleExpression} (h : m.HasType [] mt) : fvP (m.toModule h) ≤ fvPMexpr m

theorem GaudisCrypt.FVP.fvP_app [ProgramSpec] {A B : Type 1} [IsModule A] [IsModule B] (a : Module.Arr A B) (b : A) : fvP (Module.app a b) ≤ fvP a ⊔ fvP b

theorem GaudisCrypt.FVP.fvP_pair [ProgramSpec] {A B : Type 1} [IsModule A] [IsModule B] (a : A) (b : B) : fvP (Module.pair a b) = fvP a ⊔ fvP b

theorem GaudisCrypt.FVP.fvP_fst [ProgramSpec] {A B : Type 1} [IsModule A] [IsModule B] (a : Module.Prod A B) : fvP (Module.fst a) ≤ fvP a

theorem GaudisCrypt.FVP.fvP_snd [ProgramSpec] {A B : Type 1} [IsModule A] [IsModule B] (a : Module.Prod A B) : fvP (Module.snd a) ≤ fvP a

@[simp]

theorem GaudisCrypt.FVP.fvP_unit [ProgramSpec] (a : Module.Unit) : fvP a = ⊥

noncomputable def GaudisCrypt.FVP.fvP_proc [ProgramSpec] {sig : ProcedureSignature} {holes : HoleSigs} (proc : ProcedureWithHoles holes sig) : Footprint State

Equations

• GaudisCrypt.FVP.fvP_proc proc = GaudisCrypt.FVP.fvpInductiveFunctionGS.proc proc

noncomputable def GaudisCrypt.FVP.fvP_stmt [ProgramSpec] {s : Type} {holes : HoleSigs} (stmt : StmtWithHoles holes s) : Footprint (ProcedureState s)

Equations

• GaudisCrypt.FVP.fvP_stmt stmt = GaudisCrypt.FVP.fvpInductiveFunctionGS.stmt stmt

noncomputable def GaudisCrypt.FVP.glob [ProgramSpec] {sig : ProcedureSignature} {holes : HoleSigs} (A : ProcedureWithHoles holes sig) : Getter (Quotient (fvP_proc A)ᶜ.orbit_setoid) State

EasyCrypt's glob A: the getter reading everything the procedure A may touch — the touched_getter of its computed footprint. ={glob A} between two states is (glob A).get σ₁ = (glob A).get σ₂: the states differ only by updates outside fvP_proc A.

Equations

• GaudisCrypt.FVP.glob A = (GaudisCrypt.FVP.fvP_proc A).touched_getter

Footprint/reduce/lift algebra

General footprint, Lens.reduceFootprint and Lens.liftFootprint facts, independent of any particular program spec.

theorem GaudisCrypt.chain_liftFunction_diracKer {a b c : Type} (L : Lens b c) (v : Lens a b) (g : Function.End a) : diracKer ((L.chain v).liftFunction g) = L.liftSubProbability (diracKer (v.liftFunction g))

A chained lens's footprint is the liftFootprint of the inner lens's footprint through the outer lens (generator-level): diracKer ((L.chain v).liftFunction g) is exactly L.liftSubProbability (diracKer (v.liftFunction g)). The chained overwrite is the inner overwrite performed on the L-content and written back.

theorem GaudisCrypt.liftSubProbability_comm_of_reduce_disj {t s c : Type} {L : Lens s c} {v : Lens t s} {R : Footprint c} (hred : L.reduceFootprint R ≤ v.footprintᶜ) {f : s → SubProbability s} (hf : f ∈ v.footprint.updates) {k : c → SubProbability c} (hk : k ∈ R.updates) : L.liftSubProbability f * k = k * L.liftSubProbability f

The lift of a v.footprint-update commutes with every R-update, when the L-reduction of R is disjoint from v.footprint — the lens-region instance of Footprint.liftSubProbability_comm_reduce_compl.

theorem GaudisCrypt.reduce_chain_le_compl {t s c : Type} {L : Lens s c} {v : Lens t s} {R : Footprint c} (hred : L.reduceFootprint R ≤ v.footprintᶜ) : R ≤ (L.chain v).footprintᶜ

A chained lens's footprint lies in Rᶜ whenever the inner footprint's L-reduction does: from Lens.reduceFootprint L R ≤ (v.footprint)ᶜ conclude R ≤ ((L.chain v).footprint)ᶜ. Route: flip the goal via le_compl_comm to (L.chain v).footprint ≤ Rᶜ, then show each generator L.liftSubProbability (diracKer (v.liftFunction g)) commutes with every k ∈ R.updates via liftSubProbability_comm_of_reduce_disj.

theorem GaudisCrypt.globalL_liftSubProbability_pad [ProgramSpec] {l : Type} (f : State → SubProbability State) (g : State) (loc : l) : ProcedureState.globalL.liftSubProbability f { global := g, locals := loc } = do let a ← f g pure { global := a, locals := loc }

globalL.liftSubProbability f applied to a padded state applies f to the global.

theorem GaudisCrypt.globalL_liftSubProbability_global [ProgramSpec] {l : Type} (f : State → SubProbability State) (w2 : ProcedureState l) {ρ : Type} (x : ρ) : (do let s'' ← ProcedureState.globalL.liftSubProbability f w2 pure (x, s''.global)) = do let a ← f w2.global pure (x, a)

Reading the global out of globalL.liftSubProbability f recovers f on the global.

theorem GaudisCrypt.inFootprint_toProgramDenotation {s a : Type} (μ : SubProbability a) : μ.toProgramDenotation.inFootprint ⊥

A sampled value's footprint is trivial — μ.toProgramDenotation only draws its result, it touches no state, so it lies in ⊥ (mirrors inFootprint_uniform for an arbitrary μ).

Chained and FromLens footprints

Moved here from Footprint.lean: the chain law's nontrivial inclusion — the intermediate bicommutant closure adds nothing — is exactly the Lens.liftFootprint_updates extraction.

theorem GaudisCrypt.Footprint.FromLens.from_lens {a s : Type} (lens : Lens a s) : lens.footprint.FromLens

theorem GaudisCrypt.Lens.fst_compl_footprint {a b : Type} : fst.compl.footprint = snd.footprint

The complement of Lens.fst, as a footprint, is Lens.snd. (Lens.fst).compl has abstract ComplContent type, so this is a footprint equality (via the getter that identifies fst.compl.get with snd.get), not a lens equality.