@[reducible, inline]

abbrev FV.FV : Type 1

Equations

• FV.FV = DetermFootprint GaudisCrypt.VariableAssignment

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

Equations

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

noncomputable def FV.fv_setter {a : Type} {s : Type u_1} (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 {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 {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 {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 (m : GaudisCrypt.ModuleExpression) : DetermFootprint GaudisCrypt.VariableAssignment

Equations

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

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

Equations

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

@[implicit_reducible]

def FV.instReducibleGettersSettersDetermFootprintFvInductiveFunctionGS : GaudisCrypt.ReducibleGettersSetters fvInductiveFunctionGS

Equations

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

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

theorem FV.fv_app {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 {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 {A B : GaudisCrypt.ModuleTypeRep} (a : GaudisCrypt.Module (A.prod B)) : fv a.fst' ≤ fv a

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

@[simp]

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

noncomputable def FV.fv_proc {sig : GaudisCrypt.ProcedureSignature} {holes : GaudisCrypt.HoleSigs} (proc : GaudisCrypt.ProcedureWithHoles holes sig) : DetermFootprint GaudisCrypt.VariableAssignment

Equations

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

noncomputable def FV.fv_stmt {holes : GaudisCrypt.HoleSigs} (stmt : GaudisCrypt.StmtWithHoles holes) : DetermFootprint GaudisCrypt.ProgramState

Equations

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