@[reducible, inline]

abbrev FV.FV [GaudisCrypt.ProgramSpec] : Type u_1

Equations

• FV.FV = DetermFootprint GaudisCrypt.State

noncomputable def FV.fv_getter {a s : Type} (getter : GaudisCrypt.Getter a s) : DetermFootprint s

Equations

• FV.fv_getter getter = (GaudisCrypt.ProgramDenotation.get getter).range

noncomputable def FV.fv_setter {a s : Type} (setter : GaudisCrypt.Setter a s) : DetermFootprint s

Equations

• FV.fv_setter setter = GaudisCrypt.ProgramDenotation.range' (GaudisCrypt.ProgramDenotation.set setter)

def FV.fv_reduce {a : Type u_1} {b : Type u_2} (lens : GaudisCrypt.Lens a b) (range : DetermFootprint b) : DetermFootprint a

Equations

• FV.fv_reduce lens range = DetermFootprint.from {f : Function.End a | ∀ g ∈ range.updates, lens.liftFunction f * g = g * lens.liftFunction f}.centralizer

def FV.fv_extend {a : Type u_1} {b : Type u_2} (lens : GaudisCrypt.Lens a b) (range : DetermFootprint a) : DetermFootprint b

Equations

• FV.fv_extend lens range = DetermFootprint.from (lens.liftFunction '' range.updates)

Properties of fv_reduce / fv_extend needed for fv_proc_instantiate.

These are stated as axioms for review. Once fv_reduce/fv_extend have real definitions they should become theorems. Note: the proof of fv_proc_instantiate needs no properties of fv_getter/fv_setter — they are used opaquely.

theorem FV.fv_reduce_sup {a : Type u_1} {b : Type u_2} (lens : GaudisCrypt.Lens a b) (r₁ r₂ : DetermFootprint b) : fv_reduce lens (r₁ ⊔ r₂) = fv_reduce lens r₁ ⊔ fv_reduce lens r₂

theorem FV.fv_extend_sup [GaudisCrypt.ProgramSpec] {a : Type u_1} {b : Type u_2} (lens : GaudisCrypt.Lens a b) (r₁ r₂ : DetermFootprint a) : fv_extend lens (r₁ ⊔ r₂) = fv_extend lens r₁ ⊔ fv_extend lens r₂

fv_extend distributes over joins.

theorem FV.fv_extend_updates [GaudisCrypt.ProgramSpec] {a : Type u_1} {b : Type u_2} (lens : GaudisCrypt.Lens a b) (range : DetermFootprint a) : (fv_extend lens range).updates = lens.liftFunction '' range.updates

theorem FV.fv_reduce_extend [GaudisCrypt.ProgramSpec] {a : Type u_1} {b : Type u_2} (lens : GaudisCrypt.Lens a b) (r : DetermFootprint a) : fv_reduce lens (fv_extend lens r) ≤ r

fv_reduce is a retraction of fv_extend: pushing a footprint forward along a lens and pulling it back recovers it. (Only ≤ is used in the proof.)

noncomputable def FV.fvInductiveFunctionGS : GaudisCrypt.InductiveFunctionGettersSetters DetermFootprint

Equations

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

noncomputable def FV.fvMexpr [GaudisCrypt.ProgramSpec] (m : GaudisCrypt.ModuleExpression) : DetermFootprint GaudisCrypt.State

Equations

• FV.fvMexpr m = FV.fvInductiveFunctionGS.evalMexpr m

noncomputable def FV.fv [GaudisCrypt.ProgramSpec] {t : GaudisCrypt.ModuleTypeRep} (m : GaudisCrypt.Module t) : FV

Equations

• FV.fv m = FV.fvInductiveFunctionGS.eval m

@[implicit_reducible]

def FV.instReducibleGettersSettersDetermFootprintFvInductiveFunctionGS [GaudisCrypt.ProgramSpec] : GaudisCrypt.ReducibleGettersSetters fvInductiveFunctionGS

Equations

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

theorem FV.fvMexpr_upper_bound [GaudisCrypt.ProgramSpec] {t : GaudisCrypt.ModuleTypeRep} {m : GaudisCrypt.ModuleExpression} (h : m.HasType [] t) : fv (m.toModule h) ≤ fvMexpr m

theorem FV.fv_app [GaudisCrypt.ProgramSpec] {A B : GaudisCrypt.ModuleTypeRep} (a : GaudisCrypt.Module (A.arr B)) (b : GaudisCrypt.Module A) : fv (a.app' b) ≤ fv a ⊔ fv b

theorem FV.fv_pair [GaudisCrypt.ProgramSpec] {A B : GaudisCrypt.ModuleTypeRep} (a : GaudisCrypt.Module A) (b : GaudisCrypt.Module B) : fv (GaudisCrypt.Module.pair a b) = fv a ⊔ fv b

theorem FV.fv_fst [GaudisCrypt.ProgramSpec] {A B : GaudisCrypt.ModuleTypeRep} (a : GaudisCrypt.Module (A.prod B)) : fv a.fst' ≤ fv a

theorem FV.fv_snd [GaudisCrypt.ProgramSpec] {A B : GaudisCrypt.ModuleTypeRep} (a : GaudisCrypt.Module (A.prod B)) : fv a.snd' ≤ fv a

@[simp]

theorem FV.fv_unit [GaudisCrypt.ProgramSpec] (a : GaudisCrypt.Module GaudisCrypt.ModuleTypeRep.unit) : fv a = ⊥

noncomputable def FV.fv_proc [GaudisCrypt.ProgramSpec] {sig : GaudisCrypt.ProcedureSignature} {holes : GaudisCrypt.HoleSigs} (proc : GaudisCrypt.ProcedureWithHoles holes sig) : DetermFootprint GaudisCrypt.State

Equations

• FV.fv_proc proc = FV.fvInductiveFunctionGS.proc proc

noncomputable def FV.fv_stmt [GaudisCrypt.ProgramSpec] {s : Type} {holes : GaudisCrypt.HoleSigs} (stmt : GaudisCrypt.StmtWithHoles holes s) : DetermFootprint (GaudisCrypt.ProcedureState s)

Equations

• FV.fv_stmt stmt = FV.fvInductiveFunctionGS.stmt stmt