Modules

A Module T is a closed, well-typed, normal ModuleExpression of type T, together with the operations on such (application, projections, pairing) and the IsModule bridge from Lean types to ModuleTypeReps. The underlying expression calculus lives in ModuleExpressions.lean.

structure GaudisCrypt.Module [ProgramSpec] (T : ModuleTypeRep) : Type (max 1 u_1)

• expression : ModuleExpression
• typed : self.expression.HasType [] T
• normal : self.expression.NormalClosed

noncomputable def GaudisCrypt.ModuleExpression.toModule [ProgramSpec] {T : ModuleTypeRep} (m : ModuleExpression) (h : m.HasType [] T := by moduletyping!) : Module T

Build a Module from a well-typed closed expression by normalising it.

Equations

• m.toModule h = { expression := m.reduce, typed := ⋯, normal := ⋯ }

@[implicit_reducible]

noncomputable instance GaudisCrypt.instCoeFunModuleArrForall [ProgramSpec] {T U : ModuleTypeRep} : CoeFun (Module (T.arr U)) fun (x : Module (T.arr U)) => Module T → Module U

Equations

• GaudisCrypt.instCoeFunModuleArrForall = { coe := fun (f : GaudisCrypt.Module (T.arr U)) (x : GaudisCrypt.Module T) => (f.expression.app x.expression).toModule ⋯ }

noncomputable def GaudisCrypt.Module.fst' [ProgramSpec] {T U : ModuleTypeRep} (m : Module (T.prod U)) : Module T

Equations

• m.fst' = m.expression.fst.toModule ⋯

noncomputable def GaudisCrypt.Module.snd' [ProgramSpec] {T U : ModuleTypeRep} (m : Module (T.prod U)) : Module U

Equations

• m.snd' = m.expression.snd.toModule ⋯

noncomputable def GaudisCrypt.Module.pair' [ProgramSpec] {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : Module (T.prod U)

Equations

• m1.pair' m2 = (m1.expression.pair m2.expression).toModule ⋯

theorem GaudisCrypt.Module.ext [ProgramSpec] {T : ModuleTypeRep} {m1 m2 : Module T} (h : m1.expression = m2.expression) : m1 = m2

theorem GaudisCrypt.Module.ext_iff [ProgramSpec] {T : ModuleTypeRep} {m1 m2 : Module T} : m1 = m2 ↔ m1.expression = m2.expression

@[simp]

theorem GaudisCrypt.Module.expression_fst' [ProgramSpec] {T U : ModuleTypeRep} (m : Module (T.prod U)) : m.fst'.expression = m.expression.fst.reduce

@[simp]

theorem GaudisCrypt.Module.expression_snd' [ProgramSpec] {T U : ModuleTypeRep} (m : Module (T.prod U)) : m.snd'.expression = m.expression.snd.reduce

@[simp]

theorem GaudisCrypt.Module.toModule_expression [ProgramSpec] {T : ModuleTypeRep} (m : ModuleExpression) (h : m.HasType [] T) : (m.toModule h).expression = m.reduce

@[simp]

theorem GaudisCrypt.Module.reduce_expression [ProgramSpec] {T : ModuleTypeRep} (m : Module T) : m.expression.reduce = m.expression

@[simp]

theorem GaudisCrypt.Module.substituteSimultaneously_expression [ProgramSpec] {T : ModuleTypeRep} (m : Module T) (σ : ℕ → ModuleExpression) : ModuleExpression.substituteSimultaneously σ m.expression = m.expression

A module's expression is closed, so a substitution leaves it alone.

@[simp]

theorem GaudisCrypt.Module.rename_expression [ProgramSpec] {T : ModuleTypeRep} (m : Module T) (ρ : ℕ → ℕ) : ModuleExpression.rename ρ m.expression = m.expression

A module's expression is closed, so a renaming leaves it alone. (This is what a substitution going under a binder does to it — liftSubst renames by Nat.succ — so normalising an application of a curried module needs this as well as Module.substituteSimultaneously_expression.)

theorem GaudisCrypt.Module.expression_pair' [ProgramSpec] {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : (m1.pair' m2).expression = m1.expression.pair m2.expression

Pairing two modules pairs their expressions — no reduce left over, both being normal.

theorem GaudisCrypt.Module.reduce_pair_expression [ProgramSpec] {T U : ModuleTypeRep} {a b : ModuleExpression} (m1 : Module T) (m2 : Module U) (ha : a.reduce = m1.expression) (hb : b.reduce = m2.expression) : (a.pair b).reduce = (m1.pair' m2).expression

Reducing a pair componentwise: if the components reduce to the expressions of the modules m1/m2, the pair reduces to the expression of their Module.pair'. Turns a reduce of a whole record into the record of the reduced components, with no detour through termination — normality of the result comes from the modules m1/m2. (Currently unused: module_apply used to peel X.apply_simp's record with it, but now normalises both sides with reduce_simp instead.)

@[simp]

theorem GaudisCrypt.Module.fst_pair' [ProgramSpec] {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : (m1.pair' m2).fst' = m1

@[simp]

theorem GaudisCrypt.Module.snd_pair' [ProgramSpec] {T U : ModuleTypeRep} (m1 : Module T) (m2 : Module U) : (m1.pair' m2).snd' = m2

theorem GaudisCrypt.Module.pair_fst_snd' [ProgramSpec] {a✝ a✝¹ : ModuleTypeRep} {m : Module (a✝.prod a✝¹)} : m.fst'.pair' m.snd' = m

@[reducible, inline]

abbrev GaudisCrypt.Module.Unit [ProgramSpec] : Type (max 1 u_1)

Equations

• GaudisCrypt.Module.Unit = GaudisCrypt.Module GaudisCrypt.ModuleTypeRep.unit

noncomputable def GaudisCrypt.Module.unit [ProgramSpec] : Module ModuleTypeRep.unit

Equations

• GaudisCrypt.Module.unit = GaudisCrypt.ModuleExpression.unit.toModule ⋯

class GaudisCrypt.IsModule [ProgramSpec] (T : Type (max 1 u_1)) : Type 1

• moduleTypeRep : ModuleTypeRep
• isModule : T = Module (moduleTypeRep T)

@[reducible]

instance GaudisCrypt.instIsModuleModule [ProgramSpec] {t : ModuleTypeRep} : IsModule (Module t)

Equations

• GaudisCrypt.instIsModuleModule = { moduleTypeRep := t, isModule := ⋯ }

def GaudisCrypt.Module.moduleTypeRep [ProgramSpec] (T : Type (max 1 u_1)) [inst : IsModule T] : ModuleTypeRep

Equations

• GaudisCrypt.Module.moduleTypeRep T = GaudisCrypt.IsModule.moduleTypeRep T

def GaudisCrypt.Module.cast [ProgramSpec] (T : Type (max 1 u_1)) [inst : IsModule T] (m : T) : Module (moduleTypeRep T)

Equations

• GaudisCrypt.Module.cast T m = ⋯ ▸ m

def GaudisCrypt.Module.cast' [ProgramSpec] (T : Type (max 1 u_1)) [inst : IsModule T] (m : Module (moduleTypeRep T)) : T

Equations

• GaudisCrypt.Module.cast' T m = ⋯ ▸ m

def GaudisCrypt.Module.Arr [ProgramSpec] (M N : Type (max 1 u_1)) [IsModule M] [IsModule N] : Type (max 1 u_1)

Equations

• GaudisCrypt.Module.Arr M N = GaudisCrypt.Module ((GaudisCrypt.Module.moduleTypeRep M).arr (GaudisCrypt.Module.moduleTypeRep N))

@[implicit_reducible]

instance GaudisCrypt.instIsModuleArr [ProgramSpec] (M N : Type (max 1 u_1)) [IsModule M] [IsModule N] : IsModule (Module.Arr M N)

Equations

• GaudisCrypt.instIsModuleArr M N = { moduleTypeRep := (GaudisCrypt.Module.moduleTypeRep M).arr (GaudisCrypt.Module.moduleTypeRep N), isModule := ⋯ }

def GaudisCrypt.Module.Proc [ProgramSpec] (sig : ProcedureSignature) : Type (max 1 u_1)

Equations

• GaudisCrypt.Module.Proc sig = GaudisCrypt.Module (GaudisCrypt.ModuleTypeRep.proc sig)

@[implicit_reducible]

instance GaudisCrypt.instIsModuleProc [ProgramSpec] {sig : ProcedureSignature} : IsModule (Module.Proc sig)

Equations

• GaudisCrypt.instIsModuleProc = { moduleTypeRep := GaudisCrypt.ModuleTypeRep.proc sig, isModule := ⋯ }

noncomputable def GaudisCrypt.Module.app' [ProgramSpec] {A B : ModuleTypeRep} (m : Module (A.arr B)) (m' : Module A) : Module B

Equations

• m.app' m' = (m.expression.app m'.expression).toModule ⋯

noncomputable def GaudisCrypt.Module.app [ProgramSpec] {M N : Type (max 1 u)} [iM : IsModule M] [iN : IsModule N] (m : Arr M N) (m' : M) : N

Equations

• GaudisCrypt.Module.app m m' = ⋯ ▸ (⋯ ▸ m).app' (⋯ ▸ m')

theorem GaudisCrypt.Module.cast_app [ProgramSpec] {M N : Type (max 1 u_1)} [IsModule M] [IsModule N] (a : Arr M N) (b : M) : cast N (app a b) = (cast (Arr M N) a).app' (cast M b)

def GaudisCrypt.Parser.Attr.module_accessor_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def GaudisCrypt.Parser.Attr.module_accessor : Lean.ParserDescr

Simp set collecting the field accessors moduletype emits (X.f : X → Tᵢ, a chain of Module.fst'/Module.snd').

A goal about a field of an abstract module — S : CommitmentScheme a parameter, not a literal record — can only make progress by unfolding the accessor, and a tactic cannot know the accessor's name. This set is how proc_apply reaches them.

Equations

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

structure GaudisCrypt.ModuleTypeUtilities [ProgramSpec] (M T : Type (max 1 u_1)) [IsModule M] [IsModule T] (acc : M → T) : Type (max 1 u_1)

What is derivable about a field accessor acc : M → T of a module type, bundled into one declaration.

The moduletype command emits one of these per field, as X.f.utilities, rather than a separate declaration per fact — the facts are reached as X.f.utilities.accessorModule and so on. It is a structure and not a class: there is nothing to synthesise, the command hands the value over by name.

• proj : ModuleExpression → ModuleExpression

  The projection acc implements, as it acts on ModuleExpressions (fun e => e.snd.fst, …).

• accessorModule : Module.Arr M T

  The accessor as a module of its own: a projection is a module morphism.

• apply_simp (m : M) : Module.app self.accessorModule m = acc m

  …and applying that module is the accessor.

• expression_eq (m : M) : (Module.cast T (acc m)).expression = (self.proj (Module.cast M m).expression).reduce

  The accessor at the level of expressions: it is proj, reduced. The .reduce is not removable — Module.expression is always a reduct, and proj m.expression need not be normal.

def GaudisCrypt.Module.Prod [ProgramSpec] (M N : Type (max 1 u_1)) [IsModule M] [IsModule N] : Type (max 1 u_1)

Equations

• GaudisCrypt.Module.Prod M N = GaudisCrypt.Module ((GaudisCrypt.Module.moduleTypeRep M).prod (GaudisCrypt.Module.moduleTypeRep N))

@[implicit_reducible]

instance GaudisCrypt.instIsModuleProd [ProgramSpec] (M N : Type (max 1 u_1)) [IsModule M] [IsModule N] : IsModule (Module.Prod M N)

Equations

• GaudisCrypt.instIsModuleProd M N = { moduleTypeRep := (GaudisCrypt.Module.moduleTypeRep M).prod (GaudisCrypt.Module.moduleTypeRep N), isModule := ⋯ }

noncomputable def GaudisCrypt.Module.fst [ProgramSpec] {M N : Type (max 1 u)} [iM : IsModule M] [iN : IsModule N] (m : Prod M N) : M

Equations

• GaudisCrypt.Module.fst m = ⋯ ▸ (⋯ ▸ m).fst'

noncomputable def GaudisCrypt.Module.snd [ProgramSpec] {M N : Type (max 1 u)} [iM : IsModule M] [iN : IsModule N] (m : Prod M N) : N

Equations

• GaudisCrypt.Module.snd m = ⋯ ▸ (⋯ ▸ m).snd'

noncomputable def GaudisCrypt.Module.pair [ProgramSpec] {M N : Type (max 1 u)} [iM : IsModule M] [iN : IsModule N] (m1 : M) (m2 : N) : Prod M N

Equations

• GaudisCrypt.Module.pair m1 m2 = ⋯ ▸ (⋯ ▸ m1).pair' (⋯ ▸ m2)

@[simp]

theorem GaudisCrypt.Module.fst_pair [ProgramSpec] {M N : Type (max 1 u)} [IsModule M] [IsModule N] (m1 : M) (m2 : N) : fst (pair m1 m2) = m1

@[simp]

theorem GaudisCrypt.Module.snd_pair [ProgramSpec] {M N : Type (max 1 u)} [IsModule M] [IsModule N] (m1 : M) (m2 : N) : snd (pair m1 m2) = m2

theorem GaudisCrypt.Module.pair_fst_snd [ProgramSpec] {M N : Type (max 1 u)} [IsModule M] [IsModule N] (m : Prod M N) : pair (fst m) (snd m) = m

noncomputable def GaudisCrypt.Module.proc [ProgramSpec] {sig : ProcedureSignature} (p : Procedure sig) : Proc sig

Equations

• GaudisCrypt.Module.proc p = (GaudisCrypt.ModuleExpression.proc p).toModule ⋯

theorem GaudisCrypt.proc_type_is_proc [ProgramSpec] {sig : ProcedureSignature} {m : ModuleExpression} (ht : m.HasType [] (ModuleTypeRep.proc sig)) (h : m.NormalClosed) : ∃ (p : Procedure sig), m = ModuleExpression.proc p

Canonical forms at procedure type: a closed normal expression of type .proc sig is literally a .proc p node.

noncomputable def GaudisCrypt.Module.procedure [ProgramSpec] {sig : ProcedureSignature} (m : Module (ModuleTypeRep.proc sig)) : Procedure sig

The procedure of a proc-typed module — the inverse of Module.proc. (Classical.choose only escapes the Prop-to-data restriction; the witness is unique — see Module.procedure_spec and Module.procedure_proc.)

Equations

• m.procedure = ⋯.choose

theorem GaudisCrypt.Module.procedure_spec [ProgramSpec] {sig : ProcedureSignature} (m : Module (ModuleTypeRep.proc sig)) : m.expression = ModuleExpression.proc m.procedure

Module.procedure is characterized by its defining equation (the witness of proc_type_is_proc is unique by constructor injectivity).

@[simp]

theorem GaudisCrypt.Module.procedure_proc [ProgramSpec] {sig : ProcedureSignature} (p : Procedure sig) : ((ModuleExpression.proc p).toModule ⋯).procedure = p

Round-trip: wrapping a procedure as a module and extracting recovers it.

theorem GaudisCrypt.Module.typed_weaken [ProgramSpec] {T : ModuleTypeRep} (m : Module T) (Δ : ModuleContext) : m.expression.HasType Δ T

A module's expression is well-typed in any context, not just the empty one — it is closed. This is what lets moduletyping type an expression built from already-formed modules (whose leaves are m.expression rather than a HasType constructor).

noncomputable def GaudisCrypt.Module.const [ProgramSpec] {T U : Type (max 1 u_1)} [IsModule T] [iu : IsModule U] (m : U) : Arr T U

Equations

• GaudisCrypt.Module.const m = (⋯ ▸ m).expression.abs.toModule ⋯

noncomputable def GaudisCrypt.Module.procWithHoles [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) : Arr (Module holes.toModuleTypeRepTuple) (Proc sig)

Equations

• GaudisCrypt.Module.procWithHoles p_2 = GaudisCrypt.Module.const (GaudisCrypt.Module.proc p_2)
• GaudisCrypt.Module.procWithHoles p_2 = (GaudisCrypt.ModuleExpression.procHoles True.intro p_2).toModule ⋯

Applying a procedure-with-holes to its callees

The δ-rule ReductionStep.delta fires only on a literal tuple of .proc nodes (HoleSigs.Instantiation.toModuleExpr). What one has in practice is a tuple of arbitrary module expressions — the callees, as they were written — which merely reduce to such a tuple, each of them to the .proc of a Module.procedure. These lemmas bridge the two: reduce_tuple_nil/ reduce_tuple_cons build the reduction of the tuple component by component, and reduce_app_procWithHoles then takes the δ-step. Together they are what the proc_apply tactic (GaudisCrypt/Language/Syntax2.lean) runs on the X.<f>.apply_simp goals the module command emits.

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_nil [ProgramSpec] : (toModuleExpr fun {sig : ProcedureSignature} => nil) = ModuleExpression.unit

@[simp]

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_push [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (inst : holes.Instantiation) (p : Procedure sig) : (toModuleExpr fun {sig_1 : ProcedureSignature} => push (fun {sig : ProcedureSignature} => inst) p) = (ModuleExpression.proc p).pair (toModuleExpr fun {sig : ProcedureSignature} => inst)

theorem GaudisCrypt.HoleSigs.Instantiation.toModuleExpr_normal [ProgramSpec] {holes : HoleSigs} (inst : holes.Instantiation) : (toModuleExpr fun {sig : ProcedureSignature} => inst).Normal

A tuple of procedures is normal: it is built from .proc nodes and .unit alone.

theorem GaudisCrypt.Module.reduce_tuple_nil [ProgramSpec] : ModuleExpression.unit.reduce = HoleSigs.Instantiation.toModuleExpr fun {sig : ProcedureSignature} => HoleSigs.Instantiation.nil

The empty tuple: .unit is already the instantiation of no holes.

theorem GaudisCrypt.Module.reduce_tuple_cons [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (inst : holes.Instantiation) (m : Module (ModuleTypeRep.proc sig)) (c rest : ModuleExpression) (hc : c.reduce = m.expression) (hrest : rest.reduce = HoleSigs.Instantiation.toModuleExpr fun {sig : ProcedureSignature} => inst) : (c.pair rest).reduce = HoleSigs.Instantiation.toModuleExpr fun {sig_1 : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => inst) m.procedure

One component of the tuple: if c reduces to the expression of a proc-typed module m — which by canonicity is a .proc node, namely .proc m.procedure — and the rest of the tuple reduces to inst's, then the whole pair reduces to that of inst extended by m.procedure.

theorem GaudisCrypt.Module.reduce_app_procWithHoles [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) (T : ModuleExpression) (inst : holes.Instantiation) (h : T.reduce = HoleSigs.Instantiation.toModuleExpr fun {sig : ProcedureSignature} => inst) : ((procWithHoles p).expression.app T).reduce = ModuleExpression.proc (p.instantiate fun {sig : ProcedureSignature} => inst)

The δ-step, on an argument that only reduces to a tuple of procedures: applying Module.procWithHoles p to it is the procedure p with its holes instantiated. With no holes at all Module.procWithHoles p is the constant function Module.proc p, and instantiating changes nothing (ProcedureWithHoles.instantiate_empty) — so the statement covers that case too.