Tests for ModuleSyntax

def Experiment.TestModule : Type 1

The module type declared by moduletype TestModule, with fields main, aux: the type Module TestModule.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with TestModule.mk, read a single field off one with the accessors TestModule.main, TestModule.aux, and get the whole record back with TestModule.structure.

Equations

• Experiment.TestModule = GaudisCrypt.Module Experiment.TestModule.typeRep

@[reducible]

noncomputable def Experiment.TestModule.mk : Structure → TestModule

Builds a module of type TestModule from the record TestModule.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of TestModule.structure (TestModule.mk_destruct, TestModule.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas TestModule.main.mk_simp, TestModule.aux.mk_simp.

Equations

• Experiment.TestModule.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.main theRecord✝.aux

noncomputable def Experiment.TestModule.structure : TestModule → Structure

The record of a module's fields: TestModule.structure m is TestModule.Structure.mk applied to TestModule.main, TestModule.aux of m.

Inverse of TestModule.mk (TestModule.mk_destruct, TestModule.destruct_mk).

Equations

• theModule✝.structure = { main := theModule✝.main, aux := theModule✝.aux }

noncomputable def Experiment.TestModule.main : TestModule → procmod (String, ℕ) → Bool

The field main of a module of type TestModule: the projection onto component 0 of the right-nested tuple TestModule.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

TestModule.main.mk_simp reads this field back off a module built by TestModule.mk; TestModule.main.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.main = GaudisCrypt.Module.fst' theModule✝

noncomputable def Experiment.TestModule.main.utilities : GaudisCrypt.ModuleTypeUtilities TestModule (procmod (String, ℕ) → Bool) main

What is derivable about the accessor TestModule.main, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• TestModule.main.utilities.accessorModule : TestModule →ₘ … — the accessor as a module, a projection being a module morphism;
• TestModule.main.utilities.apply_simp — Module.app TestModule.main.utilities.accessorModule m = TestModule.main m: applying that module is the accessor;
• TestModule.main.utilities.expression_eq — the same at the level of expressions: (TestModule.main m).expression = (TestModule.main.utilities.proj m.expression).reduce.

Equations

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

@[simp]

theorem Experiment.TestModule.aux.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).aux = theRecord✝.aux

@[simp]: reading the field aux back off a module built from a record — TestModule.aux (TestModule.mk r) = r.aux.

It is what carries the right-hand side of an X.apply_simp (which is an TestModule.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.aux.apply_simp.

@[simp]

theorem Experiment.TestModule.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: TestModule.structure (TestModule.mk r) = r — destructing a module built from a record gives that record back.

noncomputable def Experiment.TestModule.aux : TestModule → GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

The field aux of a module of type TestModule: the projection onto component 1 of the right-nested tuple TestModule.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

TestModule.aux.mk_simp reads this field back off a module built by TestModule.mk; TestModule.aux.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.aux = GaudisCrypt.Module.snd' theModule✝

def Experiment.TestModule.typeRep : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying TestModule, the module type declared by moduletype TestModule: the right-nested product of its 2 field types, in declaration order.

TestModule is by definition Module TestModule.typeRep.

Equations

• Experiment.TestModule.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig (String, ℕ) → Bool)).prod ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

@[implicit_reducible]

instance Experiment.instIsModuleTestModule : GaudisCrypt.IsModule TestModule

The IsModule TestModule instance: TestModule is a module type, with representation TestModule.typeRep.

It is what lets the name TestModule stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module TestModule.typeRep would do on its own but TestModule, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleTestModule = { moduleTypeRep := Experiment.TestModule.typeRep, isModule := ⋯ }

structure Experiment.TestModule.Structure : Type 1

The record of the fields of a module of type TestModule: the fields main, aux, one per moduletype field, each of that field's own module type.

TestModule.mk turns such a record into a TestModule, TestModule.structure turns a TestModule back into one.

• main : procmod (String, ℕ) → Bool
• aux : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

@[simp]

theorem Experiment.TestModule.destruct_mk (theModule✝ : TestModule) : mk theModule✝.structure = theModule✝

@[simp]: TestModule.mk (TestModule.structure m) = m — rebuilding a module from its own fields gives that module back.

@[simp]

theorem Experiment.TestModule.main.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).main = theRecord✝.main

@[simp]: reading the field main back off a module built from a record — TestModule.main (TestModule.mk r) = r.main.

It is what carries the right-hand side of an X.apply_simp (which is an TestModule.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.main.apply_simp.

noncomputable def Experiment.TestModule.aux.utilities : GaudisCrypt.ModuleTypeUtilities TestModule (GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)) aux

What is derivable about the accessor TestModule.aux, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• TestModule.aux.utilities.accessorModule : TestModule →ₘ … — the accessor as a module, a projection being a module morphism;
• TestModule.aux.utilities.apply_simp — Module.app TestModule.aux.utilities.accessorModule m = TestModule.aux m: applying that module is the accessor;
• TestModule.aux.utilities.expression_eq — the same at the level of expressions: (TestModule.aux m).expression = (TestModule.aux.utilities.proj m.expression).reduce.

Equations

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

@[implicit_reducible]

instance Experiment.instIsModuleOneField : GaudisCrypt.IsModule OneField

The IsModule OneField instance: OneField is a module type, with representation OneField.typeRep.

It is what lets the name OneField stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module OneField.typeRep would do on its own but OneField, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleOneField = { moduleTypeRep := Experiment.OneField.typeRep, isModule := ⋯ }

structure Experiment.OneField.Structure : Type 1

The record of the fields of a module of type OneField: the fields only, one per moduletype field, each of that field's own module type.

OneField.mk turns such a record into a OneField, OneField.structure turns a OneField back into one.

• only : procmod (ℕ) → Bool

def Experiment.OneField : Type 1

The module type declared by moduletype OneField, with fields only: the type Module OneField.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with OneField.mk, read a single field off one with the accessors OneField.only, and get the whole record back with OneField.structure.

Equations

• Experiment.OneField = GaudisCrypt.Module Experiment.OneField.typeRep

def Experiment.OneField.typeRep : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying OneField, the module type declared by moduletype OneField: the right-nested product of its 1 field types, in declaration order.

OneField is by definition Module OneField.typeRep.

Equations

• Experiment.OneField.typeRep = GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → Bool)

@[simp]

theorem Experiment.OneField.only.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).only = theRecord✝.only

@[simp]: reading the field only back off a module built from a record — OneField.only (OneField.mk r) = r.only.

It is what carries the right-hand side of an X.apply_simp (which is an OneField.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.only.apply_simp.

noncomputable def Experiment.OneField.only.utilities : GaudisCrypt.ModuleTypeUtilities OneField (procmod (ℕ) → Bool) only

What is derivable about the accessor OneField.only, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• OneField.only.utilities.accessorModule : OneField →ₘ … — the accessor as a module, a projection being a module morphism;
• OneField.only.utilities.apply_simp — Module.app OneField.only.utilities.accessorModule m = OneField.only m: applying that module is the accessor;
• OneField.only.utilities.expression_eq — the same at the level of expressions: (OneField.only m).expression = (OneField.only.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.OneField.only : OneField → procmod (ℕ) → Bool

The field only of a module of type OneField: the projection onto component 0 of the right-nested tuple OneField.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

OneField.only.mk_simp reads this field back off a module built by OneField.mk; OneField.only.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.only = theModule✝

@[simp]

theorem Experiment.OneField.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: OneField.structure (OneField.mk r) = r — destructing a module built from a record gives that record back.

@[simp]

theorem Experiment.OneField.destruct_mk (theModule✝ : OneField) : mk theModule✝.structure = theModule✝

@[simp]: OneField.mk (OneField.structure m) = m — rebuilding a module from its own fields gives that module back.

noncomputable def Experiment.OneField.structure : OneField → Structure

The record of a module's fields: OneField.structure m is OneField.Structure.mk applied to OneField.only of m.

Inverse of OneField.mk (OneField.mk_destruct, OneField.destruct_mk).

Equations

• theModule✝.structure = { only := theModule✝.only }

@[reducible]

noncomputable def Experiment.OneField.mk : Structure → OneField

Builds a module of type OneField from the record OneField.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of OneField.structure (OneField.mk_destruct, OneField.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas OneField.only.mk_simp.

Equations

• Experiment.OneField.mk theRecord✝ = theRecord✝.only

noncomputable def Experiment.UnicodeArrowField.g : UnicodeArrowField → GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)

The field g of a module of type UnicodeArrowField: the projection onto component 1 of the right-nested tuple UnicodeArrowField.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

UnicodeArrowField.g.mk_simp reads this field back off a module built by UnicodeArrowField.mk; UnicodeArrowField.g.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.g = GaudisCrypt.Module.snd' theModule✝

noncomputable def Experiment.UnicodeArrowField.f.utilities : GaudisCrypt.ModuleTypeUtilities UnicodeArrowField (procmod (ℕ) → Bool) f

What is derivable about the accessor UnicodeArrowField.f, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• UnicodeArrowField.f.utilities.accessorModule : UnicodeArrowField →ₘ … — the accessor as a module, a projection being a module morphism;
• UnicodeArrowField.f.utilities.apply_simp — Module.app UnicodeArrowField.f.utilities.accessorModule m = UnicodeArrowField.f m: applying that module is the accessor;
• UnicodeArrowField.f.utilities.expression_eq — the same at the level of expressions: (UnicodeArrowField.f m).expression = (UnicodeArrowField.f.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.UnicodeArrowField.f : UnicodeArrowField → procmod (ℕ) → Bool

The field f of a module of type UnicodeArrowField: the projection onto component 0 of the right-nested tuple UnicodeArrowField.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

UnicodeArrowField.f.mk_simp reads this field back off a module built by UnicodeArrowField.mk; UnicodeArrowField.f.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.f = GaudisCrypt.Module.fst' theModule✝

def Experiment.UnicodeArrowField.typeRep : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying UnicodeArrowField, the module type declared by moduletype UnicodeArrowField: the right-nested product of its 2 field types, in declaration order.

UnicodeArrowField is by definition Module UnicodeArrowField.typeRep.

Equations

• Experiment.UnicodeArrowField.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → Bool)).prod ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)

@[simp]

theorem Experiment.UnicodeArrowField.destruct_mk (theModule✝ : UnicodeArrowField) : mk theModule✝.structure = theModule✝

@[simp]: UnicodeArrowField.mk (UnicodeArrowField.structure m) = m — rebuilding a module from its own fields gives that module back.

@[simp]

theorem Experiment.UnicodeArrowField.f.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).f = theRecord✝.f

@[simp]: reading the field f back off a module built from a record — UnicodeArrowField.f (UnicodeArrowField.mk r) = r.f.

It is what carries the right-hand side of an X.apply_simp (which is an UnicodeArrowField.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.f.apply_simp.

noncomputable def Experiment.UnicodeArrowField.structure : UnicodeArrowField → Structure

The record of a module's fields: UnicodeArrowField.structure m is UnicodeArrowField.Structure.mk applied to UnicodeArrowField.f, UnicodeArrowField.g of m.

Inverse of UnicodeArrowField.mk (UnicodeArrowField.mk_destruct, UnicodeArrowField.destruct_mk).

Equations

• theModule✝.structure = { f := theModule✝.f, g := theModule✝.g }

@[reducible]

noncomputable def Experiment.UnicodeArrowField.mk : Structure → UnicodeArrowField

Builds a module of type UnicodeArrowField from the record UnicodeArrowField.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of UnicodeArrowField.structure (UnicodeArrowField.mk_destruct, UnicodeArrowField.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas UnicodeArrowField.f.mk_simp, UnicodeArrowField.g.mk_simp.

Equations

• Experiment.UnicodeArrowField.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.f theRecord✝.g

@[simp]

theorem Experiment.UnicodeArrowField.g.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).g = theRecord✝.g

@[simp]: reading the field g back off a module built from a record — UnicodeArrowField.g (UnicodeArrowField.mk r) = r.g.

It is what carries the right-hand side of an X.apply_simp (which is an UnicodeArrowField.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.g.apply_simp.

def Experiment.UnicodeArrowField : Type 1

The module type declared by moduletype UnicodeArrowField, with fields f, g: the type Module UnicodeArrowField.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with UnicodeArrowField.mk, read a single field off one with the accessors UnicodeArrowField.f, UnicodeArrowField.g, and get the whole record back with UnicodeArrowField.structure.

Equations

• Experiment.UnicodeArrowField = GaudisCrypt.Module Experiment.UnicodeArrowField.typeRep

@[implicit_reducible]

instance Experiment.instIsModuleUnicodeArrowField : GaudisCrypt.IsModule UnicodeArrowField

The IsModule UnicodeArrowField instance: UnicodeArrowField is a module type, with representation UnicodeArrowField.typeRep.

It is what lets the name UnicodeArrowField stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module UnicodeArrowField.typeRep would do on its own but UnicodeArrowField, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleUnicodeArrowField = { moduleTypeRep := Experiment.UnicodeArrowField.typeRep, isModule := ⋯ }

@[simp]

theorem Experiment.UnicodeArrowField.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: UnicodeArrowField.structure (UnicodeArrowField.mk r) = r — destructing a module built from a record gives that record back.

structure Experiment.UnicodeArrowField.Structure : Type 1

The record of the fields of a module of type UnicodeArrowField: the fields f, g, one per moduletype field, each of that field's own module type.

UnicodeArrowField.mk turns such a record into a UnicodeArrowField, UnicodeArrowField.structure turns a UnicodeArrowField back into one.

• f : procmod (ℕ) → Bool
• g : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)

noncomputable def Experiment.UnicodeArrowField.g.utilities : GaudisCrypt.ModuleTypeUtilities UnicodeArrowField (GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)) g

What is derivable about the accessor UnicodeArrowField.g, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• UnicodeArrowField.g.utilities.accessorModule : UnicodeArrowField →ₘ … — the accessor as a module, a projection being a module morphism;
• UnicodeArrowField.g.utilities.apply_simp — Module.app UnicodeArrowField.g.utilities.accessorModule m = UnicodeArrowField.g m: applying that module is the accessor;
• UnicodeArrowField.g.utilities.expression_eq — the same at the level of expressions: (UnicodeArrowField.g m).expression = (UnicodeArrowField.g.utilities.proj m.expression).reduce.

Equations

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

axiom Experiment.testMain : procmod (String, ℕ) → Bool

axiom Experiment.testAux : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

noncomputable def Experiment.myMod : TestModule

Equations

• Experiment.myMod = Experiment.TestModule.mk { main := Experiment.testMain, aux := Experiment.testAux }

theorem Experiment.test : myMod.main = testMain

structure Experiment.M2.Structure : Type 1

The record of the fields of a module of type M2: the fields g, h, one per moduletype field, each of that field's own module type.

M2.mk turns such a record into a M2, M2.structure turns a M2 back into one.

• g : procmod () → Unit
• h : procmod () → Unit

noncomputable def Experiment.M2.g.utilities : GaudisCrypt.ModuleTypeUtilities M2 (procmod () → Unit) g

What is derivable about the accessor M2.g, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• M2.g.utilities.accessorModule : M2 →ₘ … — the accessor as a module, a projection being a module morphism;
• M2.g.utilities.apply_simp — Module.app M2.g.utilities.accessorModule m = M2.g m: applying that module is the accessor;
• M2.g.utilities.expression_eq — the same at the level of expressions: (M2.g m).expression = (M2.g.utilities.proj m.expression).reduce.

Equations

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

@[simp]

theorem Experiment.M2.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: M2.structure (M2.mk r) = r — destructing a module built from a record gives that record back.

@[implicit_reducible]

instance Experiment.instIsModuleM2 : GaudisCrypt.IsModule M2

The IsModule M2 instance: M2 is a module type, with representation M2.typeRep.

It is what lets the name M2 stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module M2.typeRep would do on its own but M2, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleM2 = { moduleTypeRep := Experiment.M2.typeRep, isModule := ⋯ }

@[reducible]

noncomputable def Experiment.M2.mk : Structure → M2

Builds a module of type M2 from the record M2.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of M2.structure (M2.mk_destruct, M2.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas M2.g.mk_simp, M2.h.mk_simp.

Equations

• Experiment.M2.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.g theRecord✝.h

@[simp]

theorem Experiment.M2.destruct_mk (theModule✝ : M2) : mk theModule✝.structure = theModule✝

@[simp]: M2.mk (M2.structure m) = m — rebuilding a module from its own fields gives that module back.

noncomputable def Experiment.M2.g : M2 → procmod () → Unit

The field g of a module of type M2: the projection onto component 0 of the right-nested tuple M2.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

M2.g.mk_simp reads this field back off a module built by M2.mk; M2.g.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• theModule✝.g = GaudisCrypt.Module.fst' theModule✝

def Experiment.M2.typeRep : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying M2, the module type declared by moduletype M2: the right-nested product of its 2 field types, in declaration order.

M2 is by definition Module M2.typeRep.

Equations

• Experiment.M2.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig () → Unit)).prod (GaudisCrypt.ModuleTypeRep.proc (procsig () → Unit))

@[simp]

theorem Experiment.M2.g.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).g = theRecord✝.g

@[simp]: reading the field g back off a module built from a record — M2.g (M2.mk r) = r.g.

It is what carries the right-hand side of an X.apply_simp (which is an M2.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.g.apply_simp.

@[simp]

theorem Experiment.M2.h.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).h = theRecord✝.h

@[simp]: reading the field h back off a module built from a record — M2.h (M2.mk r) = r.h.

It is what carries the right-hand side of an X.apply_simp (which is an M2.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.h.apply_simp.

noncomputable def Experiment.M2.h.utilities : GaudisCrypt.ModuleTypeUtilities M2 (procmod () → Unit) h

What is derivable about the accessor M2.h, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• M2.h.utilities.accessorModule : M2 →ₘ … — the accessor as a module, a projection being a module morphism;
• M2.h.utilities.apply_simp — Module.app M2.h.utilities.accessorModule m = M2.h m: applying that module is the accessor;
• M2.h.utilities.expression_eq — the same at the level of expressions: (M2.h m).expression = (M2.h.utilities.proj m.expression).reduce.

Equations

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

def Experiment.M2 : Type 1

The module type declared by moduletype M2, with fields g, h: the type Module M2.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with M2.mk, read a single field off one with the accessors M2.g, M2.h, and get the whole record back with M2.structure.

Equations

• Experiment.M2 = GaudisCrypt.Module Experiment.M2.typeRep

noncomputable def Experiment.M2.structure : M2 → Structure

The record of a module's fields: M2.structure m is M2.Structure.mk applied to M2.g, M2.h of m.

Inverse of M2.mk (M2.mk_destruct, M2.destruct_mk).

Equations

• theModule✝.structure = { g := theModule✝.g, h := theModule✝.h }

noncomputable def Experiment.M2.h : M2 → procmod () → Unit

The field h of a module of type M2: the projection onto component 1 of the right-nested tuple M2.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

M2.h.mk_simp reads this field back off a module built by M2.mk; M2.h.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• theModule✝.h = GaudisCrypt.Module.snd' theModule✝

theorem Experiment.X.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of X.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [X.h.procedure.apply_simp]).

noncomputable def Experiment.X.g.procedure : proctype () → Unit uses (() → Unit)

The body of proc g of module X, as a procedure of its own: the one call it makes to a module parameter (A) is its single hole.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see X.g.procedure.apply_simp) rather than run. Use X.g for this procedure as a module.

Equations

• Experiment.X.g.procedure = proc () uses (_hole0 : () → Unit) : Unit { call _hole0 (); call _hole0 (); call Experiment.myMod.main.procedure ("hello", 5); return () }

@[simp]

theorem Experiment.X.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: X.h = Module.proc X.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

noncomputable def Experiment.X.h : procmod () → Unit

proc h of module X as a module: Module.proc X.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — X.h.apply_simp says exactly that.

Equations

• Experiment.X.h = GaudisCrypt.Module.proc Experiment.X.h.procedure

@[simp]

theorem Experiment.X.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) : GaudisCrypt.Module.app X (GaudisCrypt.Module.pair A B) = M2.mk { g := GaudisCrypt.Module.app g A, h := h }

@[simp]: applying X to a tuple of its 2 parameters A, B — the record of its procedures X.g, X.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with X.g.apply_simp, X.h.apply_simp to fill that procedure's holes.

noncomputable def Experiment.X.g : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (procmod () → Unit)

proc g of module X as a module, abstracted over the module parameters it uses (A, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma X.g.apply_simp, which fills the holes of X.g.procedure with the callees the body called.

Equations

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

noncomputable def Experiment.X : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) TestModule) M2

The module declared by module X, abstracted over its 2 parameters A, B, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the module type it was declared with.

Applied to such a tuple it is the record of its procedures X.g, X.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma X.apply_simp says.

Equations

• Experiment.X = ((Experiment.X.g.expression.app (GaudisCrypt.ModuleExpression.var 0).fst).pair Experiment.X.h.expression).abs.toModule Experiment.X._proof_1

@[simp]

theorem Experiment.X.g.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app g A = GaudisCrypt.Module.proc (procedure.instantiate (GaudisCrypt.Module.app A myMod).procedure)

@[simp]: applying X.g to the parameters proc g uses (A) is Module.proc (X.g.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

noncomputable def Experiment.X.h.procedure : proctype () -> Unit

The body of proc h of module X, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see X.h.procedure.apply_simp) rather than run. Use X.h for this procedure as a module.

Equations

• Experiment.X.h.procedure = proc () : Unit { skip; return () }

theorem Experiment.X.g.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig () → Unit) GaudisCrypt.HoleSigs.empty).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); call myMod.main.procedure ("hello", 5); return () }

Instantiating the holes of X.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [X.g.procedure.apply_simp]).

noncomputable def Experiment.Y.h : procmod () → Unit

proc h of module Y as a module: Module.proc Y.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Y.h.apply_simp says exactly that.

Equations

• Experiment.Y.h = GaudisCrypt.Module.proc Experiment.Y.h.procedure

@[simp]

theorem Experiment.Y.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) : GaudisCrypt.Module.app Y (GaudisCrypt.Module.pair A B) = M2.mk { g := GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) B, h := h }

@[simp]: applying Y to a tuple of its 2 parameters A, B — the record of its procedures Y.g, Y.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with Y.g.apply_simp, Y.h.apply_simp to fill that procedure's holes.

noncomputable def Experiment.Y.h.procedure : proctype () -> Unit

The body of proc h of module Y, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Y.h.procedure.apply_simp) rather than run. Use Y.h for this procedure as a module.

Equations

• Experiment.Y.h.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.Y.g : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Arr TestModule (procmod () → Unit))

proc g of module Y as a module, abstracted over the module parameters it uses (A, B, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma Y.g.apply_simp, which fills the holes of Y.g.procedure with the callees the body called.

Equations

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

noncomputable def Experiment.Y.g.procedure : proctype () → Unit uses ((String, ℕ) → Bool, () → Unit)

The body of proc g of module Y, as a procedure of its own: the 2 calls it makes to module parameters (A, B) are its holes, in the order the body makes them.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Y.g.procedure.apply_simp) rather than run. Use Y.g for this procedure as a module.

Equations

• Experiment.Y.g.procedure = proc () uses (B_main : (String, ℕ) → Bool, _hole1 : () → Unit) : Unit { call B_main ("hi", 3); call _hole1 (); return () }

noncomputable def Experiment.Y : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) TestModule) M2

The module declared by module Y, abstracted over its 2 parameters A, B, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the module type it was declared with.

Applied to such a tuple it is the record of its procedures Y.g, Y.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma Y.apply_simp says.

Equations

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

theorem Experiment.Y.g.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig (String, ℕ) → Bool) (GaudisCrypt.HoleSigs.cons (procsig () → Unit) GaudisCrypt.HoleSigs.empty)).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) ("hi", 3); call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero.succ) (); return () }

Instantiating the holes of Y.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Y.g.procedure.apply_simp]).

@[simp]

theorem Experiment.Y.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: Y.h = Module.proc Y.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

theorem Experiment.Y.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of Y.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Y.h.procedure.apply_simp]).

@[simp]

theorem Experiment.Y.g.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) : GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) B = GaudisCrypt.Module.proc (procedure.instantiate (B.main.procedure, (GaudisCrypt.Module.app A myMod).procedure))

@[simp]: applying Y.g to the parameters proc g uses (A, B) is Module.proc (Y.g.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

def Experiment.M3 : Type 1

Equations

• Experiment.M3 = Experiment.M2

@[simp]

theorem Experiment.NoParams.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: NoParams.h = Module.proc NoParams.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

noncomputable def Experiment.NoParams : M2

The module declared by module NoParams: the record of its procedures NoParams.g, NoParams.h.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no NoParams.apply_simp to apply it with.

Equations

• Experiment.NoParams = Experiment.M2.mk { g := Experiment.NoParams.g, h := Experiment.NoParams.h }

noncomputable def Experiment.NoParams.g.procedure : proctype () -> Unit

The body of proc g of module NoParams, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see NoParams.g.procedure.apply_simp) rather than run. Use NoParams.g for this procedure as a module.

Equations

• Experiment.NoParams.g.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.NoParams.h : procmod () → Unit

proc h of module NoParams as a module: Module.proc NoParams.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — NoParams.h.apply_simp says exactly that.

Equations

• Experiment.NoParams.h = GaudisCrypt.Module.proc Experiment.NoParams.h.procedure

noncomputable def Experiment.NoParams.h.procedure : proctype () -> Unit

The body of proc h of module NoParams, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see NoParams.h.procedure.apply_simp) rather than run. Use NoParams.h for this procedure as a module.

Equations

• Experiment.NoParams.h.procedure = proc () : Unit { skip; return () }

theorem Experiment.NoParams.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of NoParams.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [NoParams.h.procedure.apply_simp]).

@[simp]

theorem Experiment.NoParams.g.apply_simp : g = GaudisCrypt.Module.proc procedure

@[simp]: NoParams.g = Module.proc NoParams.g.procedure — true by definition, proc g using no module parameter and so having no holes to fill.

theorem Experiment.NoParams.g.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of NoParams.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [NoParams.g.procedure.apply_simp]).

noncomputable def Experiment.NoParams.g : procmod () → Unit

proc g of module NoParams as a module: Module.proc NoParams.g.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — NoParams.g.apply_simp says exactly that.

Equations

• Experiment.NoParams.g = GaudisCrypt.Module.proc Experiment.NoParams.g.procedure

@[simp]

theorem Experiment.EmptyParams.apply_simp (paramTuple✝ : GaudisCrypt.Module.Unit) : GaudisCrypt.Module.app EmptyParams paramTuple✝ = M2.mk { g := g, h := h }

@[simp]: applying EmptyParams to the empty tuple — the record of its procedures EmptyParams.g, EmptyParams.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with EmptyParams.g.apply_simp, EmptyParams.h.apply_simp to fill that procedure's holes.

noncomputable def Experiment.EmptyParams.g : procmod () → Unit

proc g of module EmptyParams as a module: Module.proc EmptyParams.g.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — EmptyParams.g.apply_simp says exactly that.

Equations

• Experiment.EmptyParams.g = GaudisCrypt.Module.proc Experiment.EmptyParams.g.procedure

noncomputable def Experiment.EmptyParams : GaudisCrypt.Module.Arr GaudisCrypt.Module.Unit M2

The module declared by module EmptyParams, abstracted over its empty parameter list: Module.Arr Module.Unit M, with M the module type it was declared with, so that the only argument it takes is the empty tuple.

Applied to such a tuple it is the record of its procedures EmptyParams.g, EmptyParams.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma EmptyParams.apply_simp says.

Equations

• Experiment.EmptyParams = (Experiment.EmptyParams.g.expression.pair Experiment.EmptyParams.h.expression).abs.toModule Experiment.EmptyParams._proof_1

noncomputable def Experiment.EmptyParams.h : procmod () → Unit

proc h of module EmptyParams as a module: Module.proc EmptyParams.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — EmptyParams.h.apply_simp says exactly that.

Equations

• Experiment.EmptyParams.h = GaudisCrypt.Module.proc Experiment.EmptyParams.h.procedure

noncomputable def Experiment.EmptyParams.h.procedure : proctype () -> Unit

The body of proc h of module EmptyParams, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see EmptyParams.h.procedure.apply_simp) rather than run. Use EmptyParams.h for this procedure as a module.

Equations

• Experiment.EmptyParams.h.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.EmptyParams.g.procedure : proctype () -> Unit

The body of proc g of module EmptyParams, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see EmptyParams.g.procedure.apply_simp) rather than run. Use EmptyParams.g for this procedure as a module.

Equations

• Experiment.EmptyParams.g.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.EmptyParams.g.apply_simp : g = GaudisCrypt.Module.proc procedure

@[simp]: EmptyParams.g = Module.proc EmptyParams.g.procedure — true by definition, proc g using no module parameter and so having no holes to fill.

theorem Experiment.EmptyParams.g.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of EmptyParams.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [EmptyParams.g.procedure.apply_simp]).

@[simp]

theorem Experiment.EmptyParams.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: EmptyParams.h = Module.proc EmptyParams.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

theorem Experiment.EmptyParams.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of EmptyParams.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [EmptyParams.h.procedure.apply_simp]).

noncomputable def Experiment.NoType.g.procedure : proctype () → Unit uses (() → Unit)

The body of proc g of module NoType, as a procedure of its own: the one call it makes to a module parameter (A) is its single hole.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see NoType.g.procedure.apply_simp) rather than run. Use NoType.g for this procedure as a module.

Equations

• Experiment.NoType.g.procedure = proc () uses (_hole0 : () → Unit) : Unit { call _hole0 (); return () }

noncomputable def Experiment.NoType.h.procedure : proctype () -> Bool

The body of proc h of module NoType, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see NoType.h.procedure.apply_simp) rather than run. Use NoType.h for this procedure as a module.

Equations

• Experiment.NoType.h.procedure = proc () : Bool { skip; return true }

noncomputable def Experiment.NoType : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Prod (procmod () → Unit) (procmod () → Bool))

The module declared by module NoType, abstracted over its single parameter A, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the anonymous product of the procedures' own types, the declaration naming no module type.

Applied to such a tuple it is the record of its procedures NoType.g, NoType.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma NoType.apply_simp says.

Equations

• Experiment.NoType = ((Experiment.NoType.g.expression.app (GaudisCrypt.ModuleExpression.var 0)).pair Experiment.NoType.h.expression).abs.toModule Experiment.NoType._proof_1

noncomputable def Experiment.NoType.h : procmod () → Bool

proc h of module NoType as a module: Module.proc NoType.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — NoType.h.apply_simp says exactly that.

Equations

• Experiment.NoType.h = GaudisCrypt.Module.proc Experiment.NoType.h.procedure

@[simp]

theorem Experiment.NoType.g.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app g A = GaudisCrypt.Module.proc (procedure.instantiate (GaudisCrypt.Module.app A myMod).procedure)

@[simp]: applying NoType.g to the parameters proc g uses (A) is Module.proc (NoType.g.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

theorem Experiment.NoType.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Bool { skip; return true }

Instantiating the holes of NoType.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [NoType.h.procedure.apply_simp]).

theorem Experiment.NoType.g.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig () → Unit) GaudisCrypt.HoleSigs.empty).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); return () }

Instantiating the holes of NoType.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [NoType.g.procedure.apply_simp]).

noncomputable def Experiment.NoType.g : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (procmod () → Unit)

proc g of module NoType as a module, abstracted over the module parameters it uses (A, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma NoType.g.apply_simp, which fills the holes of NoType.g.procedure with the callees the body called.

Equations

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

@[simp]

theorem Experiment.NoType.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: NoType.h = Module.proc NoType.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

@[simp]

theorem Experiment.NoType.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app NoType A = GaudisCrypt.Module.pair (GaudisCrypt.Module.app g A) h

@[simp]: applying NoType to a tuple of its single parameter A — the record of its procedures NoType.g, NoType.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with NoType.g.apply_simp, NoType.h.apply_simp to fill that procedure's holes.

noncomputable def Experiment.Deep : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Prod TestModule (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)))) M2

The module declared by module Deep, abstracted over its 3 parameters A, B, C, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the module type it was declared with.

Applied to such a tuple it is the record of its procedures Deep.g, Deep.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma Deep.apply_simp says.

Equations

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

noncomputable def Experiment.Deep.h : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)

proc h of module Deep as a module, abstracted over the module parameters it uses (B, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma Deep.h.apply_simp, which fills the holes of Deep.h.procedure with the callees the body called.

Equations

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

@[simp]

theorem Experiment.Deep.h.apply_simp (B : TestModule) : GaudisCrypt.Module.app h B = GaudisCrypt.Module.proc (procedure.instantiate B.main.procedure)

@[simp]: applying Deep.h to the parameters proc h uses (B) is Module.proc (Deep.h.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

@[simp]

theorem Experiment.Deep.g.apply_simp (A C : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) C = GaudisCrypt.Module.proc (procedure.instantiate ((GaudisCrypt.Module.app C myMod).procedure, (GaudisCrypt.Module.app A myMod).procedure))

@[simp]: applying Deep.g to the parameters proc g uses (A, C) is Module.proc (Deep.g.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

@[simp]

theorem Experiment.Deep.apply_simp (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) (C : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app Deep (GaudisCrypt.Module.pair A (GaudisCrypt.Module.pair B C)) = M2.mk { g := GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) C, h := GaudisCrypt.Module.app h B }

@[simp]: applying Deep to a tuple of its 3 parameters A, B, C — the record of its procedures Deep.g, Deep.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with Deep.g.apply_simp, Deep.h.apply_simp to fill that procedure's holes.

theorem Experiment.Deep.g.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig () → Unit) (GaudisCrypt.HoleSigs.cons (procsig () → Unit) GaudisCrypt.HoleSigs.empty)).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero.succ) (); return () }

Instantiating the holes of Deep.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Deep.g.procedure.apply_simp]).

noncomputable def Experiment.Deep.g.procedure : proctype () → Unit uses (() → Unit, () → Unit)

The body of proc g of module Deep, as a procedure of its own: the 2 calls it makes to module parameters (A, C) are its holes, in the order the body makes them.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Deep.g.procedure.apply_simp) rather than run. Use Deep.g for this procedure as a module.

Equations

• Experiment.Deep.g.procedure = proc () uses (_hole0 : () → Unit, _hole1 : () → Unit) : Unit { call _hole0 (); call _hole1 (); return () }

noncomputable def Experiment.Deep.h.procedure : proctype () → Unit uses ((String, ℕ) → Bool)

The body of proc h of module Deep, as a procedure of its own: the one call it makes to a module parameter (B) is its single hole.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Deep.h.procedure.apply_simp) rather than run. Use Deep.h for this procedure as a module.

Equations

• Experiment.Deep.h.procedure = proc () uses (B_main : (String, ℕ) → Bool) : Unit { call B_main ("hi", 3); return () }

noncomputable def Experiment.Deep.g : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (procmod () → Unit))

proc g of module Deep as a module, abstracted over the module parameters it uses (A, C, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma Deep.g.apply_simp, which fills the holes of Deep.g.procedure with the callees the body called.

Equations

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

theorem Experiment.Deep.h.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig (String, ℕ) → Bool) GaudisCrypt.HoleSigs.empty).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) ("hi", 3); return () }

Instantiating the holes of Deep.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Deep.h.procedure.apply_simp]).

@[simp]

theorem Experiment.SharedType.g.apply_simp (A B : TestModule) : GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) B = GaudisCrypt.Module.proc (procedure.instantiate (A.main.procedure, B.main.procedure))

@[simp]: applying SharedType.g to the parameters proc g uses (A, B) is Module.proc (SharedType.g.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

theorem Experiment.SharedType.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of SharedType.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [SharedType.h.procedure.apply_simp]).

noncomputable def Experiment.SharedType.h : procmod () → Unit

proc h of module SharedType as a module: Module.proc SharedType.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — SharedType.h.apply_simp says exactly that.

Equations

• Experiment.SharedType.h = GaudisCrypt.Module.proc Experiment.SharedType.h.procedure

noncomputable def Experiment.SharedType.h.procedure : proctype () -> Unit

The body of proc h of module SharedType, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see SharedType.h.procedure.apply_simp) rather than run. Use SharedType.h for this procedure as a module.

Equations

• Experiment.SharedType.h.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.SharedType.apply_simp (A B : TestModule) : GaudisCrypt.Module.app SharedType (GaudisCrypt.Module.pair A B) = M2.mk { g := GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) B, h := h }

@[simp]: applying SharedType to a tuple of its 2 parameters A, B — the record of its procedures SharedType.g, SharedType.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with SharedType.g.apply_simp, SharedType.h.apply_simp to fill that procedure's holes.

theorem Experiment.SharedType.g.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig (String, ℕ) → Bool) (GaudisCrypt.HoleSigs.cons (procsig (String, ℕ) → Bool) GaudisCrypt.HoleSigs.empty)).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) ("hi", 3); call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero.succ) ("ho", 4); return () }

Instantiating the holes of SharedType.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [SharedType.g.procedure.apply_simp]).

noncomputable def Experiment.SharedType.g.procedure : proctype () → Unit uses ((String, ℕ) → Bool, (String, ℕ) → Bool)

The body of proc g of module SharedType, as a procedure of its own: the 2 calls it makes to module parameters (A, B) are its holes, in the order the body makes them.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see SharedType.g.procedure.apply_simp) rather than run. Use SharedType.g for this procedure as a module.

Equations

• Experiment.SharedType.g.procedure = proc () uses (A_main : (String, ℕ) → Bool, B_main : (String, ℕ) → Bool) : Unit { call A_main ("hi", 3); call B_main ("ho", 4); return () }

noncomputable def Experiment.SharedType : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod TestModule TestModule) M2

The module declared by module SharedType, abstracted over its 2 parameters A, B, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the module type it was declared with.

Applied to such a tuple it is the record of its procedures SharedType.g, SharedType.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma SharedType.apply_simp says.

Equations

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

@[simp]

theorem Experiment.SharedType.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: SharedType.h = Module.proc SharedType.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

noncomputable def Experiment.SharedType.g : GaudisCrypt.Module.Arr TestModule (GaudisCrypt.Module.Arr TestModule (procmod () → Unit))

proc g of module SharedType as a module, abstracted over the module parameters it uses (A, B, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma SharedType.g.apply_simp, which fills the holes of SharedType.g.procedure with the callees the body called.

Equations

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

theorem Experiment.NoTypeNoParams.g.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of NoTypeNoParams.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [NoTypeNoParams.g.procedure.apply_simp]).

noncomputable def Experiment.NoTypeNoParams.g : procmod () → Unit

proc g of module NoTypeNoParams as a module: Module.proc NoTypeNoParams.g.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — NoTypeNoParams.g.apply_simp says exactly that.

Equations

• Experiment.NoTypeNoParams.g = GaudisCrypt.Module.proc Experiment.NoTypeNoParams.g.procedure

noncomputable def Experiment.NoTypeNoParams : procmod () → Unit

The module declared by module NoTypeNoParams: the record of its procedures NoTypeNoParams.g.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no NoTypeNoParams.apply_simp to apply it with.

Equations

• Experiment.NoTypeNoParams = Experiment.NoTypeNoParams.g

noncomputable def Experiment.NoTypeNoParams.g.procedure : proctype () -> Unit

The body of proc g of module NoTypeNoParams, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see NoTypeNoParams.g.procedure.apply_simp) rather than run. Use NoTypeNoParams.g for this procedure as a module.

Equations

• Experiment.NoTypeNoParams.g.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.NoTypeNoParams.g.apply_simp : g = GaudisCrypt.Module.proc procedure

@[simp]: NoTypeNoParams.g = Module.proc NoTypeNoParams.g.procedure — true by definition, proc g using no module parameter and so having no holes to fill.

noncomputable def Experiment.Sized.gen (n : ℕ) : Sized n → procmod () → Fin (n + 1)

The field gen of a module of type Sized: the projection onto component 0 of the right-nested tuple Sized.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Sized.gen.mk_simp reads this field back off a module built by Sized.mk; Sized.gen.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• Experiment.Sized.gen n theModule✝ = GaudisCrypt.Module.fst' theModule✝

@[reducible]

noncomputable def Experiment.Sized.mk (n : ℕ) : Structure n → Sized n

Builds a module of type Sized from the record Sized.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of Sized.structure (Sized.mk_destruct, Sized.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas Sized.gen.mk_simp, Sized.use.mk_simp.

Equations

• Experiment.Sized.mk n theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.gen theRecord✝.use

@[simp]

theorem Experiment.Sized.use.mk_simp (n : ℕ) (theRecord✝ : Structure n) : use n (mk n theRecord✝) = theRecord✝.use

@[simp]: reading the field use back off a module built from a record — Sized.use (Sized.mk r) = r.use.

It is what carries the right-hand side of an X.apply_simp (which is an Sized.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.use.apply_simp.

@[simp]

theorem Experiment.Sized.gen.mk_simp (n : ℕ) (theRecord✝ : Structure n) : gen n (mk n theRecord✝) = theRecord✝.gen

@[simp]: reading the field gen back off a module built from a record — Sized.gen (Sized.mk r) = r.gen.

It is what carries the right-hand side of an X.apply_simp (which is an Sized.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.gen.apply_simp.

noncomputable def Experiment.Sized.use.utilities (n : ℕ) : GaudisCrypt.ModuleTypeUtilities (Sized n) (procmod (Fin (n + 1)) → Bool) (use n)

What is derivable about the accessor Sized.use, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Sized.use.utilities.accessorModule : Sized →ₘ … — the accessor as a module, a projection being a module morphism;
• Sized.use.utilities.apply_simp — Module.app Sized.use.utilities.accessorModule m = Sized.use m: applying that module is the accessor;
• Sized.use.utilities.expression_eq — the same at the level of expressions: (Sized.use m).expression = (Sized.use.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.Sized.use (n : ℕ) : Sized n → procmod (Fin (n + 1)) → Bool

The field use of a module of type Sized: the projection onto component 1 of the right-nested tuple Sized.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Sized.use.mk_simp reads this field back off a module built by Sized.mk; Sized.use.utilities has the accessor as a module, and the lemmas about it.

Equations

• Experiment.Sized.use n theModule✝ = GaudisCrypt.Module.snd' theModule✝

noncomputable def Experiment.Sized.structure (n : ℕ) : Sized n → Structure n

The record of a module's fields: Sized.structure m is Sized.Structure.mk applied to Sized.gen, Sized.use of m.

Inverse of Sized.mk (Sized.mk_destruct, Sized.destruct_mk).

Equations

• Experiment.Sized.structure n theModule✝ = { gen := Experiment.Sized.gen n theModule✝, use := Experiment.Sized.use n theModule✝ }

def Experiment.Sized.typeRep (n : ℕ) : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying Sized, the module type declared by moduletype Sized: the right-nested product of its 2 field types, in declaration order.

Sized is by definition Module Sized.typeRep.

Equations

• Experiment.Sized.typeRep n = (GaudisCrypt.ModuleTypeRep.proc (procsig () → Fin (n + 1))).prod (GaudisCrypt.ModuleTypeRep.proc (procsig (Fin (n + 1)) → Bool))

@[simp]

theorem Experiment.Sized.destruct_mk (n : ℕ) (theModule✝ : Sized n) : mk n («structure» n theModule✝) = theModule✝

@[simp]: Sized.mk (Sized.structure m) = m — rebuilding a module from its own fields gives that module back.

structure Experiment.Sized.Structure (n : ℕ) : Type 1

The record of the fields of a module of type Sized: the fields gen, use, one per moduletype field, each of that field's own module type.

Sized.mk turns such a record into a Sized, Sized.structure turns a Sized back into one.

• gen : procmod () → Fin (n + 1)
• use : procmod (Fin (n + 1)) → Bool

def Experiment.Sized (n : ℕ) : Type 1

The module type declared by moduletype Sized, with fields gen, use: the type Module Sized.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with Sized.mk, read a single field off one with the accessors Sized.gen, Sized.use, and get the whole record back with Sized.structure.

Equations

• Experiment.Sized n = GaudisCrypt.Module (Experiment.Sized.typeRep n)

@[implicit_reducible]

instance Experiment.instIsModuleSized (n : ℕ) : GaudisCrypt.IsModule (Sized n)

The IsModule Sized instance: Sized is a module type, with representation Sized.typeRep.

It is what lets the name Sized stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module Sized.typeRep would do on its own but Sized, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleSized n = { moduleTypeRep := Experiment.Sized.typeRep n, isModule := ⋯ }

@[simp]

theorem Experiment.Sized.mk_destruct (n : ℕ) (theRecord✝ : Structure n) : «structure» n (mk n theRecord✝) = theRecord✝

@[simp]: Sized.structure (Sized.mk r) = r — destructing a module built from a record gives that record back.

noncomputable def Experiment.Sized.gen.utilities (n : ℕ) : GaudisCrypt.ModuleTypeUtilities (Sized n) (procmod () → Fin (n + 1)) (gen n)

What is derivable about the accessor Sized.gen, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Sized.gen.utilities.accessorModule : Sized →ₘ … — the accessor as a module, a projection being a module morphism;
• Sized.gen.utilities.apply_simp — Module.app Sized.gen.utilities.accessorModule m = Sized.gen m: applying that module is the accessor;
• Sized.gen.utilities.expression_eq — the same at the level of expressions: (Sized.gen m).expression = (Sized.gen.utilities.proj m.expression).reduce.

Equations

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

@[implicit_reducible]

instance Experiment.instIsModulePoly {α : Type} [_gaudiParam0 : Inhabited α] : GaudisCrypt.IsModule Poly

The IsModule Poly instance: Poly is a module type, with representation Poly.typeRep.

It is what lets the name Poly stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module Poly.typeRep would do on its own but Poly, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModulePoly = { moduleTypeRep := Experiment.Poly.typeRep, isModule := ⋯ }

noncomputable def Experiment.Poly.gen {α : Type} [_gaudiParam0 : Inhabited α] : Poly → procmod () → α

The field gen of a module of type Poly: the projection onto component 0 of the right-nested tuple Poly.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Poly.gen.mk_simp reads this field back off a module built by Poly.mk; Poly.gen.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• theModule✝.gen = GaudisCrypt.Module.fst' theModule✝

@[reducible]

noncomputable def Experiment.Poly.mk {α : Type} [_gaudiParam0 : Inhabited α] : Structure → Poly

Builds a module of type Poly from the record Poly.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of Poly.structure (Poly.mk_destruct, Poly.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas Poly.gen.mk_simp, Poly.use.mk_simp.

Equations

• Experiment.Poly.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.gen theRecord✝.use

def Experiment.Poly {α : Type} [_gaudiParam0 : Inhabited α] : Type 1

The module type declared by moduletype Poly, with fields gen, use: the type Module Poly.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with Poly.mk, read a single field off one with the accessors Poly.gen, Poly.use, and get the whole record back with Poly.structure.

Equations

• Experiment.Poly = GaudisCrypt.Module Experiment.Poly.typeRep

@[simp]

theorem Experiment.Poly.gen.mk_simp {α : Type} [_gaudiParam0 : Inhabited α] (theRecord✝ : Structure) : (mk theRecord✝).gen = theRecord✝.gen

@[simp]: reading the field gen back off a module built from a record — Poly.gen (Poly.mk r) = r.gen.

It is what carries the right-hand side of an X.apply_simp (which is an Poly.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.gen.apply_simp.

@[simp]

theorem Experiment.Poly.destruct_mk {α : Type} [_gaudiParam0 : Inhabited α] (theModule✝ : Poly) : mk theModule✝.structure = theModule✝

@[simp]: Poly.mk (Poly.structure m) = m — rebuilding a module from its own fields gives that module back.

@[simp]

theorem Experiment.Poly.use.mk_simp {α : Type} [_gaudiParam0 : Inhabited α] (theRecord✝ : Structure) : (mk theRecord✝).use = theRecord✝.use

@[simp]: reading the field use back off a module built from a record — Poly.use (Poly.mk r) = r.use.

It is what carries the right-hand side of an X.apply_simp (which is an Poly.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.use.apply_simp.

noncomputable def Experiment.Poly.use.utilities {α : Type} [_gaudiParam0 : Inhabited α] : GaudisCrypt.ModuleTypeUtilities Poly (procmod (α) → Bool) use

What is derivable about the accessor Poly.use, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Poly.use.utilities.accessorModule : Poly →ₘ … — the accessor as a module, a projection being a module morphism;
• Poly.use.utilities.apply_simp — Module.app Poly.use.utilities.accessorModule m = Poly.use m: applying that module is the accessor;
• Poly.use.utilities.expression_eq — the same at the level of expressions: (Poly.use m).expression = (Poly.use.utilities.proj m.expression).reduce.

Equations

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

@[simp]

theorem Experiment.Poly.mk_destruct {α : Type} [_gaudiParam0 : Inhabited α] (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: Poly.structure (Poly.mk r) = r — destructing a module built from a record gives that record back.

noncomputable def Experiment.Poly.gen.utilities {α : Type} [_gaudiParam0 : Inhabited α] : GaudisCrypt.ModuleTypeUtilities Poly (procmod () → α) gen

What is derivable about the accessor Poly.gen, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Poly.gen.utilities.accessorModule : Poly →ₘ … — the accessor as a module, a projection being a module morphism;
• Poly.gen.utilities.apply_simp — Module.app Poly.gen.utilities.accessorModule m = Poly.gen m: applying that module is the accessor;
• Poly.gen.utilities.expression_eq — the same at the level of expressions: (Poly.gen m).expression = (Poly.gen.utilities.proj m.expression).reduce.

Equations

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

structure Experiment.Poly.Structure {α : Type} [_gaudiParam0 : Inhabited α] : Type 1

The record of the fields of a module of type Poly: the fields gen, use, one per moduletype field, each of that field's own module type.

Poly.mk turns such a record into a Poly, Poly.structure turns a Poly back into one.

• gen : procmod () → α
• use : procmod (α) → Bool

def Experiment.Poly.typeRep {α : Type} [_gaudiParam0 : Inhabited α] : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying Poly, the module type declared by moduletype Poly: the right-nested product of its 2 field types, in declaration order.

Poly is by definition Module Poly.typeRep.

Equations

• Experiment.Poly.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig () → α)).prod (GaudisCrypt.ModuleTypeRep.proc (procsig (α) → Bool))

noncomputable def Experiment.Poly.structure {α : Type} [_gaudiParam0 : Inhabited α] : Poly → Structure

The record of a module's fields: Poly.structure m is Poly.Structure.mk applied to Poly.gen, Poly.use of m.

Inverse of Poly.mk (Poly.mk_destruct, Poly.destruct_mk).

Equations

• theModule✝.structure = { gen := theModule✝.gen, use := theModule✝.use }

noncomputable def Experiment.Poly.use {α : Type} [_gaudiParam0 : Inhabited α] : Poly → procmod (α) → Bool

The field use of a module of type Poly: the projection onto component 1 of the right-nested tuple Poly.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Poly.use.mk_simp reads this field back off a module built by Poly.mk; Poly.use.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.use = GaudisCrypt.Module.snd' theModule✝

@[simp]

theorem Experiment.Twice.main.apply_simp (n : ℕ) (S : Sized n) : GaudisCrypt.Module.app (main n) S = GaudisCrypt.Module.proc ((procedure n).instantiate ((Sized.gen n S).procedure, (Sized.use n S).procedure))

@[simp]: applying Twice.main to the parameters proc main uses (S) is Module.proc (Twice.main.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

noncomputable def Experiment.Twice.main.procedure (n : ℕ) : proctype () → Bool uses (() → Fin (n + 1), (Fin (n + 1)) → Bool)

The body of proc main of module Twice, as a procedure of its own: the 2 calls it makes to module parameters (S) are its holes, in the order the body makes them.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Twice.main.procedure.apply_simp) rather than run. Use Twice.main for this procedure as a module.

Equations

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

theorem Experiment.Twice.main.procedure.apply_simp (n : ℕ) (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig () → Fin (n + 1)) (GaudisCrypt.HoleSigs.cons (procsig (Fin (n + 1)) → Bool) GaudisCrypt.HoleSigs.empty)).Instantiation) : (procedure n).instantiate holeArgs✝ = proc () : Bool { var x : Fin (n + 1), b : Bool; x <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); b <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero.succ) (§x); return §b }

Instantiating the holes of Twice.main.procedure with a tuple holeArgs of procedures: the body of proc main as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Twice.main.procedure.apply_simp]).

noncomputable def Experiment.Twice.main (n : ℕ) : GaudisCrypt.Module.Arr (Sized n) (procmod () → Bool)

proc main of module Twice as a module, abstracted over the module parameters it uses (S, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma Twice.main.apply_simp, which fills the holes of Twice.main.procedure with the callees the body called.

Equations

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

noncomputable def Experiment.Twice (n : ℕ) : GaudisCrypt.Module.Arr (Sized n) (procmod () → Bool)

The module declared by module Twice, abstracted over its single parameter S, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the anonymous product of the procedures' own types, the declaration naming no module type.

Applied to such a tuple it is the record of its procedures Twice.main, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma Twice.apply_simp says.

Equations

• Experiment.Twice n = ((Experiment.Twice.main n).expression.app (GaudisCrypt.ModuleExpression.var 0)).abs.toModule ⋯

@[simp]

theorem Experiment.Twice.apply_simp (n : ℕ) (S : Sized n) : GaudisCrypt.Module.app (Twice n) S = GaudisCrypt.Module.app (main n) S

@[simp]: applying Twice to a tuple of its single parameter S — the record of its procedures Twice.main, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with Twice.main.apply_simp to fill that procedure's holes.

noncomputable def Experiment.Fixed.main (k : ℕ) : procmod (Fin (k + 1)) → Fin (k + 1)

proc main of module Fixed as a module: Module.proc Fixed.main.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Fixed.main.apply_simp says exactly that.

Equations

• Experiment.Fixed.main k = GaudisCrypt.Module.proc (Experiment.Fixed.main.procedure k)

@[simp]

theorem Experiment.Fixed.main.apply_simp (k : ℕ) : main k = GaudisCrypt.Module.proc (procedure k)

@[simp]: Fixed.main = Module.proc Fixed.main.procedure — true by definition, proc main using no module parameter and so having no holes to fill.

theorem Experiment.Fixed.main.procedure.apply_simp (k : ℕ) (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure k).instantiate holeArgs✝ = proc (y : Fin (k + 1)) : (Fin (k + 1)) { skip; return §y }

Instantiating the holes of Fixed.main.procedure with a tuple holeArgs of procedures: the body of proc main as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Fixed.main.procedure.apply_simp]).

noncomputable def Experiment.Fixed (k : ℕ) : procmod (Fin (k + 1)) → Fin (k + 1)

The module declared by module Fixed: the record of its procedures Fixed.main.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no Fixed.apply_simp to apply it with.

Equations

• Experiment.Fixed k = Experiment.Fixed.main k

noncomputable def Experiment.Fixed.main.procedure (k : ℕ) : proctype (Fin (k + 1)) -> Fin (k + 1)

The body of proc main of module Fixed, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Fixed.main.procedure.apply_simp) rather than run. Use Fixed.main for this procedure as a module.

Equations

• Experiment.Fixed.main.procedure k = proc (y : Fin (k + 1)) : (Fin (k + 1)) { skip; return §y }

@[simp]

theorem Experiment.AllTheNames.gen.mk_simp (m s e args t : ℕ) (theRecord✝ : Structure m s e args t) : gen m s e args t (mk m s e args t theRecord✝) = theRecord✝.gen

@[simp]: reading the field gen back off a module built from a record — AllTheNames.gen (AllTheNames.mk r) = r.gen.

It is what carries the right-hand side of an X.apply_simp (which is an AllTheNames.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.gen.apply_simp.

noncomputable def Experiment.AllTheNames.structure (m s e args t : ℕ) : AllTheNames m s e args t → Structure m s e args t

The record of a module's fields: AllTheNames.structure m is AllTheNames.Structure.mk applied to AllTheNames.gen, AllTheNames.use of m.

Inverse of AllTheNames.mk (AllTheNames.mk_destruct, AllTheNames.destruct_mk).

Equations

• Experiment.AllTheNames.structure m s e args t theModule✝ = { gen := Experiment.AllTheNames.gen m s e args t theModule✝, use := Experiment.AllTheNames.use m s e args t theModule✝ }

def Experiment.AllTheNames.typeRep (m s e args t : ℕ) : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying AllTheNames, the module type declared by moduletype AllTheNames: the right-nested product of its 2 field types, in declaration order.

AllTheNames is by definition Module AllTheNames.typeRep.

Equations

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

noncomputable def Experiment.AllTheNames.use (m s e args t : ℕ) : AllTheNames m s e args t → procmod (Fin (m + s + e + args + t + 1)) → Bool

The field use of a module of type AllTheNames: the projection onto component 1 of the right-nested tuple AllTheNames.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

AllTheNames.use.mk_simp reads this field back off a module built by AllTheNames.mk; AllTheNames.use.utilities has the accessor as a module, and the lemmas about it.

Equations

• Experiment.AllTheNames.use m s e args t theModule✝ = GaudisCrypt.Module.snd' theModule✝

@[reducible]

noncomputable def Experiment.AllTheNames.mk (m s e args t : ℕ) : Structure m s e args t → AllTheNames m s e args t

Builds a module of type AllTheNames from the record AllTheNames.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of AllTheNames.structure (AllTheNames.mk_destruct, AllTheNames.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas AllTheNames.gen.mk_simp, AllTheNames.use.mk_simp.

Equations

• Experiment.AllTheNames.mk m s e args t theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.gen theRecord✝.use

noncomputable def Experiment.AllTheNames.gen.utilities (m s e args t : ℕ) : GaudisCrypt.ModuleTypeUtilities (AllTheNames m s e args t) (procmod () → Fin (m + s + e + args + t + 1)) (gen m s e args t)

What is derivable about the accessor AllTheNames.gen, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• AllTheNames.gen.utilities.accessorModule : AllTheNames →ₘ … — the accessor as a module, a projection being a module morphism;
• AllTheNames.gen.utilities.apply_simp — Module.app AllTheNames.gen.utilities.accessorModule m = AllTheNames.gen m: applying that module is the accessor;
• AllTheNames.gen.utilities.expression_eq — the same at the level of expressions: (AllTheNames.gen m).expression = (AllTheNames.gen.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.AllTheNames.use.utilities (m s e args t : ℕ) : GaudisCrypt.ModuleTypeUtilities (AllTheNames m s e args t) (procmod (Fin (m + s + e + args + t + 1)) → Bool) (use m s e args t)

What is derivable about the accessor AllTheNames.use, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• AllTheNames.use.utilities.accessorModule : AllTheNames →ₘ … — the accessor as a module, a projection being a module morphism;
• AllTheNames.use.utilities.apply_simp — Module.app AllTheNames.use.utilities.accessorModule m = AllTheNames.use m: applying that module is the accessor;
• AllTheNames.use.utilities.expression_eq — the same at the level of expressions: (AllTheNames.use m).expression = (AllTheNames.use.utilities.proj m.expression).reduce.

Equations

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

@[simp]

theorem Experiment.AllTheNames.destruct_mk (m s e args t : ℕ) (theModule✝ : AllTheNames m s e args t) : mk m s e args t («structure» m s e args t theModule✝) = theModule✝

@[simp]: AllTheNames.mk (AllTheNames.structure m) = m — rebuilding a module from its own fields gives that module back.

@[implicit_reducible]

instance Experiment.instIsModuleAllTheNames (m s e args t : ℕ) : GaudisCrypt.IsModule (AllTheNames m s e args t)

The IsModule AllTheNames instance: AllTheNames is a module type, with representation AllTheNames.typeRep.

It is what lets the name AllTheNames stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module AllTheNames.typeRep would do on its own but AllTheNames, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleAllTheNames m s e args t = { moduleTypeRep := Experiment.AllTheNames.typeRep m s e args t, isModule := ⋯ }

def Experiment.AllTheNames (m s e args t : ℕ) : Type 1

The module type declared by moduletype AllTheNames, with fields gen, use: the type Module AllTheNames.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with AllTheNames.mk, read a single field off one with the accessors AllTheNames.gen, AllTheNames.use, and get the whole record back with AllTheNames.structure.

Equations

• Experiment.AllTheNames m s e args t = GaudisCrypt.Module (Experiment.AllTheNames.typeRep m s e args t)

noncomputable def Experiment.AllTheNames.gen (m s e args t : ℕ) : AllTheNames m s e args t → procmod () → Fin (m + s + e + args + t + 1)

The field gen of a module of type AllTheNames: the projection onto component 0 of the right-nested tuple AllTheNames.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

AllTheNames.gen.mk_simp reads this field back off a module built by AllTheNames.mk; AllTheNames.gen.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• Experiment.AllTheNames.gen m s e args t theModule✝ = GaudisCrypt.Module.fst' theModule✝

@[simp]

theorem Experiment.AllTheNames.use.mk_simp (m s e args t : ℕ) (theRecord✝ : Structure m s e args t) : use m s e args t (mk m s e args t theRecord✝) = theRecord✝.use

@[simp]: reading the field use back off a module built from a record — AllTheNames.use (AllTheNames.mk r) = r.use.

It is what carries the right-hand side of an X.apply_simp (which is an AllTheNames.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.use.apply_simp.

@[simp]

theorem Experiment.AllTheNames.mk_destruct (m s e args t : ℕ) (theRecord✝ : Structure m s e args t) : «structure» m s e args t (mk m s e args t theRecord✝) = theRecord✝

@[simp]: AllTheNames.structure (AllTheNames.mk r) = r — destructing a module built from a record gives that record back.

structure Experiment.AllTheNames.Structure (m s e args t : ℕ) : Type 1

The record of the fields of a module of type AllTheNames: the fields gen, use, one per moduletype field, each of that field's own module type.

AllTheNames.mk turns such a record into a AllTheNames, AllTheNames.structure turns a AllTheNames back into one.

• gen : procmod () → Fin (m + s + e + args + t + 1)
• use : procmod (Fin (m + s + e + args + t + 1)) → Bool

noncomputable def Experiment.UsesThemToo.main (args : ℕ) : GaudisCrypt.Module.Arr OneField (procmod () → Bool)

proc main of module UsesThemToo as a module, abstracted over the module parameters it uses (S, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma UsesThemToo.main.apply_simp, which fills the holes of UsesThemToo.main.procedure with the callees the body called.

Equations

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

theorem Experiment.UsesThemToo.main.procedure.apply_simp (args : ℕ) (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig (ℕ) → Bool) GaudisCrypt.HoleSigs.empty).Instantiation) : (procedure args).instantiate holeArgs✝ = proc () : Bool { var b : Bool; b <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (args); return §b }

Instantiating the holes of UsesThemToo.main.procedure with a tuple holeArgs of procedures: the body of proc main as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [UsesThemToo.main.procedure.apply_simp]).

noncomputable def Experiment.UsesThemToo.main.procedure (args : ℕ) : proctype () → Bool uses ((ℕ) → Bool)

The body of proc main of module UsesThemToo, as a procedure of its own: the one call it makes to a module parameter (S) is its single hole.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see UsesThemToo.main.procedure.apply_simp) rather than run. Use UsesThemToo.main for this procedure as a module.

Equations

• Experiment.UsesThemToo.main.procedure args = proc () uses (S_only : (ℕ) → Bool) : Bool { var b : Bool; b <- call S_only (args); return §b }

@[simp]

theorem Experiment.UsesThemToo.main.apply_simp (args : ℕ) (S : OneField) : GaudisCrypt.Module.app (main args) S = GaudisCrypt.Module.proc ((procedure args).instantiate S.only.procedure)

@[simp]: applying UsesThemToo.main to the parameters proc main uses (S) is Module.proc (UsesThemToo.main.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

@[simp]

theorem Experiment.UsesThemToo.apply_simp (args : ℕ) (S : OneField) : GaudisCrypt.Module.app (UsesThemToo args) S = GaudisCrypt.Module.app (main args) S

@[simp]: applying UsesThemToo to a tuple of its single parameter S — the record of its procedures UsesThemToo.main, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with UsesThemToo.main.apply_simp to fill that procedure's holes.

noncomputable def Experiment.UsesThemToo (args : ℕ) : GaudisCrypt.Module.Arr OneField (procmod () → Bool)

The module declared by module UsesThemToo, abstracted over its single parameter S, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the anonymous product of the procedures' own types, the declaration naming no module type.

Applied to such a tuple it is the record of its procedures UsesThemToo.main, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma UsesThemToo.apply_simp says.

Equations

• Experiment.UsesThemToo args = ((Experiment.UsesThemToo.main args).expression.app (GaudisCrypt.ModuleExpression.var 0)).abs.toModule ⋯

noncomputable def Experiment.Boxed.use {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : Boxed k → procmod (α) → Fin (k + 1)

The field use of a module of type Boxed: the projection onto component 1 of the right-nested tuple Boxed.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Boxed.use.mk_simp reads this field back off a module built by Boxed.mk; Boxed.use.utilities has the accessor as a module, and the lemmas about it.

Equations

• Experiment.Boxed.use k theModule✝ = GaudisCrypt.Module.snd' theModule✝

@[simp]

theorem Experiment.Boxed.gen.mk_simp {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (theRecord✝ : Structure k) : gen k (mk k theRecord✝) = theRecord✝.gen

@[simp]: reading the field gen back off a module built from a record — Boxed.gen (Boxed.mk r) = r.gen.

It is what carries the right-hand side of an X.apply_simp (which is an Boxed.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.gen.apply_simp.

def Experiment.Boxed {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : Type 1

The module type declared by moduletype Boxed, with fields gen, use: the type Module Boxed.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with Boxed.mk, read a single field off one with the accessors Boxed.gen, Boxed.use, and get the whole record back with Boxed.structure.

Equations

• Experiment.Boxed k = GaudisCrypt.Module (Experiment.Boxed.typeRep k)

@[simp]

theorem Experiment.Boxed.destruct_mk {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (theModule✝ : Boxed k) : mk k («structure» k theModule✝) = theModule✝

@[simp]: Boxed.mk (Boxed.structure m) = m — rebuilding a module from its own fields gives that module back.

@[simp]

theorem Experiment.Boxed.use.mk_simp {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (theRecord✝ : Structure k) : use k (mk k theRecord✝) = theRecord✝.use

@[simp]: reading the field use back off a module built from a record — Boxed.use (Boxed.mk r) = r.use.

It is what carries the right-hand side of an X.apply_simp (which is an Boxed.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.use.apply_simp.

structure Experiment.Boxed.Structure {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : Type 1

The record of the fields of a module of type Boxed: the fields gen, use, one per moduletype field, each of that field's own module type.

Boxed.mk turns such a record into a Boxed, Boxed.structure turns a Boxed back into one.

• gen : procmod () → α
• use : procmod (α) → Fin (k + 1)

@[reducible]

noncomputable def Experiment.Boxed.mk {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : Structure k → Boxed k

Builds a module of type Boxed from the record Boxed.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of Boxed.structure (Boxed.mk_destruct, Boxed.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas Boxed.gen.mk_simp, Boxed.use.mk_simp.

Equations

• Experiment.Boxed.mk k theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.gen theRecord✝.use

@[simp]

theorem Experiment.Boxed.mk_destruct {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (theRecord✝ : Structure k) : «structure» k (mk k theRecord✝) = theRecord✝

@[simp]: Boxed.structure (Boxed.mk r) = r — destructing a module built from a record gives that record back.

def Experiment.Boxed.typeRep {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying Boxed, the module type declared by moduletype Boxed: the right-nested product of its 2 field types, in declaration order.

Boxed is by definition Module Boxed.typeRep.

Equations

• Experiment.Boxed.typeRep k = (GaudisCrypt.ModuleTypeRep.proc (procsig () → α)).prod (GaudisCrypt.ModuleTypeRep.proc (procsig (α) → Fin (k + 1)))

noncomputable def Experiment.Boxed.use.utilities {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : GaudisCrypt.ModuleTypeUtilities (Boxed k) (procmod (α) → Fin (k + 1)) (use k)

What is derivable about the accessor Boxed.use, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Boxed.use.utilities.accessorModule : Boxed →ₘ … — the accessor as a module, a projection being a module morphism;
• Boxed.use.utilities.apply_simp — Module.app Boxed.use.utilities.accessorModule m = Boxed.use m: applying that module is the accessor;
• Boxed.use.utilities.expression_eq — the same at the level of expressions: (Boxed.use m).expression = (Boxed.use.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.Boxed.gen {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : Boxed k → procmod () → α

The field gen of a module of type Boxed: the projection onto component 0 of the right-nested tuple Boxed.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Boxed.gen.mk_simp reads this field back off a module built by Boxed.mk; Boxed.gen.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• Experiment.Boxed.gen k theModule✝ = GaudisCrypt.Module.fst' theModule✝

noncomputable def Experiment.Boxed.structure {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : Boxed k → Structure k

The record of a module's fields: Boxed.structure m is Boxed.Structure.mk applied to Boxed.gen, Boxed.use of m.

Inverse of Boxed.mk (Boxed.mk_destruct, Boxed.destruct_mk).

Equations

• Experiment.Boxed.structure k theModule✝ = { gen := Experiment.Boxed.gen k theModule✝, use := Experiment.Boxed.use k theModule✝ }

@[implicit_reducible]

instance Experiment.instIsModuleBoxed {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : GaudisCrypt.IsModule (Boxed k)

The IsModule Boxed instance: Boxed is a module type, with representation Boxed.typeRep.

It is what lets the name Boxed stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module Boxed.typeRep would do on its own but Boxed, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleBoxed k = { moduleTypeRep := Experiment.Boxed.typeRep k, isModule := ⋯ }

noncomputable def Experiment.Boxed.gen.utilities {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : GaudisCrypt.ModuleTypeUtilities (Boxed k) (procmod () → α) (gen k)

What is derivable about the accessor Boxed.gen, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Boxed.gen.utilities.accessorModule : Boxed →ₘ … — the accessor as a module, a projection being a module morphism;
• Boxed.gen.utilities.apply_simp — Module.app Boxed.gen.utilities.accessorModule m = Boxed.gen m: applying that module is the accessor;
• Boxed.gen.utilities.expression_eq — the same at the level of expressions: (Boxed.gen m).expression = (Boxed.gen.utilities.proj m.expression).reduce.

Equations

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

theorem Experiment.Unbox.main.procedure.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig () → α) (GaudisCrypt.HoleSigs.cons (procsig (α) → Fin (k + 1)) GaudisCrypt.HoleSigs.empty)).Instantiation) : (procedure k).instantiate holeArgs✝ = proc () : (Fin (k + 1)) { var x : α, i : Fin (k + 1); x <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); i <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero.succ) (§x); return §i }

Instantiating the holes of Unbox.main.procedure with a tuple holeArgs of procedures: the body of proc main as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Unbox.main.procedure.apply_simp]).

@[simp]

theorem Experiment.Unbox.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (S : Boxed k) : GaudisCrypt.Module.app (Unbox k) S = GaudisCrypt.Module.app (main k) S

@[simp]: applying Unbox to a tuple of its single parameter S — the record of its procedures Unbox.main, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with Unbox.main.apply_simp to fill that procedure's holes.

noncomputable def Experiment.Unbox.main {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : GaudisCrypt.Module.Arr (Boxed k) (procmod () → Fin (k + 1))

proc main of module Unbox as a module, abstracted over the module parameters it uses (S, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma Unbox.main.apply_simp, which fills the holes of Unbox.main.procedure with the callees the body called.

Equations

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

noncomputable def Experiment.Unbox.main.procedure {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : proctype () → Fin (k + 1) uses (() → α, (α) → Fin (k + 1))

The body of proc main of module Unbox, as a procedure of its own: the 2 calls it makes to module parameters (S) are its holes, in the order the body makes them.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Unbox.main.procedure.apply_simp) rather than run. Use Unbox.main for this procedure as a module.

Equations

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

noncomputable def Experiment.Unbox {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) : GaudisCrypt.Module.Arr (Boxed k) (procmod () → Fin (k + 1))

The module declared by module Unbox, abstracted over its single parameter S, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the anonymous product of the procedures' own types, the declaration naming no module type.

Applied to such a tuple it is the record of its procedures Unbox.main, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma Unbox.apply_simp says.

Equations

• Experiment.Unbox k = ((Experiment.Unbox.main k).expression.app (GaudisCrypt.ModuleExpression.var 0)).abs.toModule ⋯

@[simp]

theorem Experiment.Unbox.main.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] (k : ℕ) (S : Boxed k) : GaudisCrypt.Module.app (main k) S = GaudisCrypt.Module.proc ((procedure k).instantiate ((Boxed.gen k S).procedure, (Boxed.use k S).procedure))

@[simp]: applying Unbox.main to the parameters proc main uses (S) is Module.proc (Unbox.main.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

@[reducible]

noncomputable def Experiment.Shadow.mk (k : ℕ) : Structure k → Shadow k

Builds a module of type Shadow from the record Shadow.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of Shadow.structure (Shadow.mk_destruct, Shadow.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas Shadow.gen.mk_simp, Shadow.use.mk_simp.

Equations

• Experiment.Shadow.mk k theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.gen theRecord✝.use

noncomputable def Experiment.Shadow.structure (k : ℕ) : Shadow k → Structure k

The record of a module's fields: Shadow.structure m is Shadow.Structure.mk applied to Shadow.gen, Shadow.use of m.

Inverse of Shadow.mk (Shadow.mk_destruct, Shadow.destruct_mk).

Equations

• Experiment.Shadow.structure k theModule✝ = { gen := Experiment.Shadow.gen k theModule✝, use := Experiment.Shadow.use k theModule✝ }

@[implicit_reducible]

instance Experiment.instIsModuleShadow (k : ℕ) : GaudisCrypt.IsModule (Shadow k)

The IsModule Shadow instance: Shadow is a module type, with representation Shadow.typeRep.

It is what lets the name Shadow stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module Shadow.typeRep would do on its own but Shadow, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleShadow k = { moduleTypeRep := Experiment.Shadow.typeRep k, isModule := ⋯ }

@[simp]

theorem Experiment.Shadow.use.mk_simp (k : ℕ) (theRecord✝ : Structure k) : use k (mk k theRecord✝) = theRecord✝.use

@[simp]: reading the field use back off a module built from a record — Shadow.use (Shadow.mk r) = r.use.

It is what carries the right-hand side of an X.apply_simp (which is an Shadow.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.use.apply_simp.

@[simp]

theorem Experiment.Shadow.destruct_mk (k : ℕ) (theModule✝ : Shadow k) : mk k («structure» k theModule✝) = theModule✝

@[simp]: Shadow.mk (Shadow.structure m) = m — rebuilding a module from its own fields gives that module back.

structure Experiment.Shadow.Structure (k : ℕ) : Type 1

The record of the fields of a module of type Shadow: the fields gen, use, one per moduletype field, each of that field's own module type.

Shadow.mk turns such a record into a Shadow, Shadow.structure turns a Shadow back into one.

• gen : procmod () → Fin (k + 1)
• use : procmod (Fin (k + 1)) → Bool

@[simp]

theorem Experiment.Shadow.gen.mk_simp (k : ℕ) (theRecord✝ : Structure k) : gen k (mk k theRecord✝) = theRecord✝.gen

@[simp]: reading the field gen back off a module built from a record — Shadow.gen (Shadow.mk r) = r.gen.

It is what carries the right-hand side of an X.apply_simp (which is an Shadow.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.gen.apply_simp.

noncomputable def Experiment.Shadow.use.utilities (k : ℕ) : GaudisCrypt.ModuleTypeUtilities (Shadow k) (procmod (Fin (k + 1)) → Bool) (use k)

What is derivable about the accessor Shadow.use, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Shadow.use.utilities.accessorModule : Shadow →ₘ … — the accessor as a module, a projection being a module morphism;
• Shadow.use.utilities.apply_simp — Module.app Shadow.use.utilities.accessorModule m = Shadow.use m: applying that module is the accessor;
• Shadow.use.utilities.expression_eq — the same at the level of expressions: (Shadow.use m).expression = (Shadow.use.utilities.proj m.expression).reduce.

Equations

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

def Experiment.Shadow.typeRep (k : ℕ) : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying Shadow, the module type declared by moduletype Shadow: the right-nested product of its 2 field types, in declaration order.

Shadow is by definition Module Shadow.typeRep.

Equations

• Experiment.Shadow.typeRep k = (GaudisCrypt.ModuleTypeRep.proc (procsig () → Fin (k + 1))).prod (GaudisCrypt.ModuleTypeRep.proc (procsig (Fin (k + 1)) → Bool))

def Experiment.Shadow (k : ℕ) : Type 1

The module type declared by moduletype Shadow, with fields gen, use: the type Module Shadow.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with Shadow.mk, read a single field off one with the accessors Shadow.gen, Shadow.use, and get the whole record back with Shadow.structure.

Equations

• Experiment.Shadow k = GaudisCrypt.Module (Experiment.Shadow.typeRep k)

noncomputable def Experiment.Shadow.gen.utilities (k : ℕ) : GaudisCrypt.ModuleTypeUtilities (Shadow k) (procmod () → Fin (k + 1)) (gen k)

What is derivable about the accessor Shadow.gen, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• Shadow.gen.utilities.accessorModule : Shadow →ₘ … — the accessor as a module, a projection being a module morphism;
• Shadow.gen.utilities.apply_simp — Module.app Shadow.gen.utilities.accessorModule m = Shadow.gen m: applying that module is the accessor;
• Shadow.gen.utilities.expression_eq — the same at the level of expressions: (Shadow.gen m).expression = (Shadow.gen.utilities.proj m.expression).reduce.

Equations

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

@[simp]

theorem Experiment.Shadow.mk_destruct (k : ℕ) (theRecord✝ : Structure k) : «structure» k (mk k theRecord✝) = theRecord✝

@[simp]: Shadow.structure (Shadow.mk r) = r — destructing a module built from a record gives that record back.

noncomputable def Experiment.Shadow.use (k : ℕ) : Shadow k → procmod (Fin (k + 1)) → Bool

The field use of a module of type Shadow: the projection onto component 1 of the right-nested tuple Shadow.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Shadow.use.mk_simp reads this field back off a module built by Shadow.mk; Shadow.use.utilities has the accessor as a module, and the lemmas about it.

Equations

• Experiment.Shadow.use k theModule✝ = GaudisCrypt.Module.snd' theModule✝

noncomputable def Experiment.Shadow.gen (k : ℕ) : Shadow k → procmod () → Fin (k + 1)

The field gen of a module of type Shadow: the projection onto component 0 of the right-nested tuple Shadow.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

Shadow.gen.mk_simp reads this field back off a module built by Shadow.mk; Shadow.gen.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• Experiment.Shadow.gen k theModule✝ = GaudisCrypt.Module.fst' theModule✝

theorem Experiment.MkSized.gen.procedure.apply_simp (n : ℕ) (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure n).instantiate holeArgs✝ = proc () : (Fin (n + 1)) { skip; return 0 }

Instantiating the holes of MkSized.gen.procedure with a tuple holeArgs of procedures: the body of proc gen as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [MkSized.gen.procedure.apply_simp]).

noncomputable def Experiment.MkSized.gen (n : ℕ) : procmod () → Fin (n + 1)

proc gen of module MkSized as a module: Module.proc MkSized.gen.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — MkSized.gen.apply_simp says exactly that.

Equations

• Experiment.MkSized.gen n = GaudisCrypt.Module.proc (Experiment.MkSized.gen.procedure n)

@[simp]

theorem Experiment.MkSized.use.apply_simp (n : ℕ) : use n = GaudisCrypt.Module.proc (procedure n)

@[simp]: MkSized.use = Module.proc MkSized.use.procedure — true by definition, proc use using no module parameter and so having no holes to fill.

noncomputable def Experiment.MkSized.gen.procedure (n : ℕ) : proctype () -> Fin (n + 1)

The body of proc gen of module MkSized, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see MkSized.gen.procedure.apply_simp) rather than run. Use MkSized.gen for this procedure as a module.

Equations

• Experiment.MkSized.gen.procedure n = proc () : (Fin (n + 1)) { skip; return 0 }

theorem Experiment.MkSized.use.procedure.apply_simp (n : ℕ) (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure n).instantiate holeArgs✝ = proc (_x : Fin (n + 1)) : Bool { skip; return true }

Instantiating the holes of MkSized.use.procedure with a tuple holeArgs of procedures: the body of proc use as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [MkSized.use.procedure.apply_simp]).

noncomputable def Experiment.MkSized.use (n : ℕ) : procmod (Fin (n + 1)) → Bool

proc use of module MkSized as a module: Module.proc MkSized.use.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — MkSized.use.apply_simp says exactly that.

Equations

• Experiment.MkSized.use n = GaudisCrypt.Module.proc (Experiment.MkSized.use.procedure n)

noncomputable def Experiment.MkSized.use.procedure (n : ℕ) : proctype (Fin (n + 1)) -> Bool

The body of proc use of module MkSized, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see MkSized.use.procedure.apply_simp) rather than run. Use MkSized.use for this procedure as a module.

Equations

• Experiment.MkSized.use.procedure n = proc (_x : Fin (n + 1)) : Bool { skip; return true }

noncomputable def Experiment.MkSized (n : ℕ) : Sized n

The module declared by module MkSized: the record of its procedures MkSized.gen, MkSized.use.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no MkSized.apply_simp to apply it with.

Equations

• Experiment.MkSized n = Experiment.Sized.mk n { gen := Experiment.MkSized.gen n, use := Experiment.MkSized.use n }

@[simp]

theorem Experiment.MkSized.gen.apply_simp (n : ℕ) : gen n = GaudisCrypt.Module.proc (procedure n)

@[simp]: MkSized.gen = Module.proc MkSized.gen.procedure — true by definition, proc gen using no module parameter and so having no holes to fill.

noncomputable def Experiment.MkPoly {α : Type} [_gaudiParam0 : Inhabited α] : Poly

The module declared by module MkPoly: the record of its procedures MkPoly.gen, MkPoly.use.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no MkPoly.apply_simp to apply it with.

Equations

• Experiment.MkPoly = Experiment.Poly.mk { gen := Experiment.MkPoly.gen, use := Experiment.MkPoly.use }

theorem Experiment.MkPoly.gen.procedure.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : α { skip; return default }

Instantiating the holes of MkPoly.gen.procedure with a tuple holeArgs of procedures: the body of proc gen as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [MkPoly.gen.procedure.apply_simp]).

noncomputable def Experiment.MkPoly.use.procedure {α : Type} [_gaudiParam0 : Inhabited α] : proctype (α) -> Bool

The body of proc use of module MkPoly, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see MkPoly.use.procedure.apply_simp) rather than run. Use MkPoly.use for this procedure as a module.

Equations

• Experiment.MkPoly.use.procedure = proc (_x : α) : Bool { skip; return true }

noncomputable def Experiment.MkPoly.gen {α : Type} [_gaudiParam0 : Inhabited α] : procmod () → α

proc gen of module MkPoly as a module: Module.proc MkPoly.gen.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — MkPoly.gen.apply_simp says exactly that.

Equations

• Experiment.MkPoly.gen = GaudisCrypt.Module.proc Experiment.MkPoly.gen.procedure

noncomputable def Experiment.MkPoly.use {α : Type} [_gaudiParam0 : Inhabited α] : procmod (α) → Bool

proc use of module MkPoly as a module: Module.proc MkPoly.use.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — MkPoly.use.apply_simp says exactly that.

Equations

• Experiment.MkPoly.use = GaudisCrypt.Module.proc Experiment.MkPoly.use.procedure

noncomputable def Experiment.MkPoly.gen.procedure {α : Type} [_gaudiParam0 : Inhabited α] : proctype () -> α

The body of proc gen of module MkPoly, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see MkPoly.gen.procedure.apply_simp) rather than run. Use MkPoly.gen for this procedure as a module.

Equations

• Experiment.MkPoly.gen.procedure = proc () : α { skip; return default }

@[simp]

theorem Experiment.MkPoly.gen.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] : gen = GaudisCrypt.Module.proc procedure

@[simp]: MkPoly.gen = Module.proc MkPoly.gen.procedure — true by definition, proc gen using no module parameter and so having no holes to fill.

theorem Experiment.MkPoly.use.procedure.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc (_x : α) : Bool { skip; return true }

Instantiating the holes of MkPoly.use.procedure with a tuple holeArgs of procedures: the body of proc use as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [MkPoly.use.procedure.apply_simp]).

@[simp]

theorem Experiment.MkPoly.use.apply_simp {α : Type} [_gaudiParam0 : Inhabited α] : use = GaudisCrypt.Module.proc procedure

@[simp]: MkPoly.use = Module.proc MkPoly.use.procedure — true by definition, proc use using no module parameter and so having no holes to fill.

@[simp]

theorem Experiment.WrapSized.use.apply_simp (n : ℕ) (S : Sized n) : GaudisCrypt.Module.app (use n) S = GaudisCrypt.Module.proc ((procedure n).instantiate (Sized.use n S).procedure)

@[simp]: applying WrapSized.use to the parameters proc use uses (S) is Module.proc (WrapSized.use.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

@[simp]

theorem Experiment.WrapSized.gen.apply_simp (n : ℕ) (S : Sized n) : GaudisCrypt.Module.app (gen n) S = GaudisCrypt.Module.proc ((procedure n).instantiate (Sized.gen n S).procedure)

@[simp]: applying WrapSized.gen to the parameters proc gen uses (S) is Module.proc (WrapSized.gen.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

@[simp]

theorem Experiment.WrapSized.apply_simp (n : ℕ) (S : Sized n) : GaudisCrypt.Module.app (WrapSized n) S = Sized.mk n { gen := GaudisCrypt.Module.app (gen n) S, use := GaudisCrypt.Module.app (use n) S }

@[simp]: applying WrapSized to a tuple of its single parameter S — the record of its procedures WrapSized.gen, WrapSized.use, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with WrapSized.gen.apply_simp, WrapSized.use.apply_simp to fill that procedure's holes.

theorem Experiment.WrapSized.gen.procedure.apply_simp (n : ℕ) (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig () → Fin (n + 1)) GaudisCrypt.HoleSigs.empty).Instantiation) : (procedure n).instantiate holeArgs✝ = proc () : (Fin (n + 1)) { var r : Fin (n + 1); r <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (); return §r }

Instantiating the holes of WrapSized.gen.procedure with a tuple holeArgs of procedures: the body of proc gen as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [WrapSized.gen.procedure.apply_simp]).

noncomputable def Experiment.WrapSized.gen.procedure (n : ℕ) : proctype () → Fin (n + 1) uses (() → Fin (n + 1))

The body of proc gen of module WrapSized, as a procedure of its own: the one call it makes to a module parameter (S) is its single hole.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see WrapSized.gen.procedure.apply_simp) rather than run. Use WrapSized.gen for this procedure as a module.

Equations

• Experiment.WrapSized.gen.procedure n = proc () uses (S_gen : () → Fin (n + 1)) : (Fin (n + 1)) { var r : Fin (n + 1); r <- call S_gen (); return §r }

noncomputable def Experiment.WrapSized (n : ℕ) : GaudisCrypt.Module.Arr (Sized n) (Sized n)

The module declared by module WrapSized, abstracted over its single parameter S, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the module type it was declared with.

Applied to such a tuple it is the record of its procedures WrapSized.gen, WrapSized.use, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma WrapSized.apply_simp says.

Equations

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

noncomputable def Experiment.WrapSized.gen (n : ℕ) : GaudisCrypt.Module.Arr (Sized n) (procmod () → Fin (n + 1))

proc gen of module WrapSized as a module, abstracted over the module parameters it uses (S, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma WrapSized.gen.apply_simp, which fills the holes of WrapSized.gen.procedure with the callees the body called.

Equations

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

noncomputable def Experiment.WrapSized.use (n : ℕ) : GaudisCrypt.Module.Arr (Sized n) (procmod (Fin (n + 1)) → Bool)

proc use of module WrapSized as a module, abstracted over the module parameters it uses (S, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma WrapSized.use.apply_simp, which fills the holes of WrapSized.use.procedure with the callees the body called.

Equations

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

theorem Experiment.WrapSized.use.procedure.apply_simp (n : ℕ) (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig (Fin (n + 1)) → Bool) GaudisCrypt.HoleSigs.empty).Instantiation) : (procedure n).instantiate holeArgs✝ = proc (x : Fin (n + 1)) : Bool { var b : Bool; b <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) (§x); return §b }

Instantiating the holes of WrapSized.use.procedure with a tuple holeArgs of procedures: the body of proc use as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [WrapSized.use.procedure.apply_simp]).

noncomputable def Experiment.WrapSized.use.procedure (n : ℕ) : proctype (Fin (n + 1)) → Bool uses ((Fin (n + 1)) → Bool)

The body of proc use of module WrapSized, as a procedure of its own: the one call it makes to a module parameter (S) is its single hole.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see WrapSized.use.procedure.apply_simp) rather than run. Use WrapSized.use for this procedure as a module.

Equations

• Experiment.WrapSized.use.procedure n = proc (x : Fin (n + 1)) uses (S_use : (Fin (n + 1)) → Bool) : Bool { var b : Bool; b <- call S_use (§x); return §b }

@[reducible]

def Experiment.three : ℕ

Equations

• Experiment.three = 3

@[simp]

theorem Experiment.Warned.g.apply_simp (A : TestModule) : g A = GaudisCrypt.Module.proc (procedure A)

@[simp]: Warned.g = Module.proc Warned.g.procedure — true by definition, proc g using no module parameter and so having no holes to fill.

noncomputable def Experiment.Warned (A : TestModule) : procmod () → Unit

The module declared by module Warned: the record of its procedures Warned.g.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no Warned.apply_simp to apply it with.

Equations

• Experiment.Warned A = Experiment.Warned.g A

noncomputable def Experiment.Warned.g (A : TestModule) : procmod () → Unit

proc g of module Warned as a module: Module.proc Warned.g.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Warned.g.apply_simp says exactly that.

Equations

• Experiment.Warned.g A = GaudisCrypt.Module.proc (Experiment.Warned.g.procedure A)

noncomputable def Experiment.Warned.g.procedure (A : TestModule) : proctype () -> Unit

The body of proc g of module Warned, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Warned.g.procedure.apply_simp) rather than run. Use Warned.g for this procedure as a module.

Equations

• Experiment.Warned.g.procedure A = proc () : Unit { skip; return () }

theorem Experiment.Warned.g.procedure.apply_simp (A : TestModule) (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure A).instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of Warned.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Warned.g.procedure.apply_simp]).

@[simp]

theorem Experiment.Quiet.g.apply_simp (A : TestModule) : g A = GaudisCrypt.Module.proc (procedure A)

@[simp]: Quiet.g = Module.proc Quiet.g.procedure — true by definition, proc g using no module parameter and so having no holes to fill.

noncomputable def Experiment.Quiet (A : TestModule) : procmod () → Unit

The module declared by module Quiet: the record of its procedures Quiet.g.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no Quiet.apply_simp to apply it with.

Equations

• Experiment.Quiet A = Experiment.Quiet.g A

noncomputable def Experiment.Quiet.g.procedure (A : TestModule) : proctype () -> Unit

The body of proc g of module Quiet, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see Quiet.g.procedure.apply_simp) rather than run. Use Quiet.g for this procedure as a module.

Equations

• Experiment.Quiet.g.procedure A = proc () : Unit { skip; return () }

theorem Experiment.Quiet.g.procedure.apply_simp (A : TestModule) (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure A).instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of Quiet.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [Quiet.g.procedure.apply_simp]).

noncomputable def Experiment.Quiet.g (A : TestModule) : procmod () → Unit

proc g of module Quiet as a module: Module.proc Quiet.g.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Quiet.g.apply_simp says exactly that.

Equations

• Experiment.Quiet.g A = GaudisCrypt.Module.proc (Experiment.Quiet.g.procedure A)

theorem Experiment.HoleNames.h.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { skip; return () }

Instantiating the holes of HoleNames.h.procedure with a tuple holeArgs of procedures: the body of proc h as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [HoleNames.h.procedure.apply_simp]).

@[simp]

theorem Experiment.HoleNames.h.apply_simp : h = GaudisCrypt.Module.proc procedure

@[simp]: HoleNames.h = Module.proc HoleNames.h.procedure — true by definition, proc h using no module parameter and so having no holes to fill.

@[simp]

theorem Experiment.HoleNames.g.apply_simp (S T : TestModule) : GaudisCrypt.Module.app (GaudisCrypt.Module.app g S) T = GaudisCrypt.Module.proc (procedure.instantiate (S.main.procedure, T.main.procedure))

@[simp]: applying HoleNames.g to the parameters proc g uses (S, T) is Module.proc (HoleNames.g.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.

noncomputable def Experiment.HoleNames.h : procmod () → Unit

proc h of module HoleNames as a module: Module.proc HoleNames.h.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — HoleNames.h.apply_simp says exactly that.

Equations

• Experiment.HoleNames.h = GaudisCrypt.Module.proc Experiment.HoleNames.h.procedure

noncomputable def Experiment.HoleNames.g : GaudisCrypt.Module.Arr TestModule (GaudisCrypt.Module.Arr TestModule (procmod () → Unit))

proc g of module HoleNames as a module, abstracted over the module parameters it uses (S, T, in declaration order): Module.Arr … (Module.Proc (procsig …)).

Apply it with the @[simp] lemma HoleNames.g.apply_simp, which fills the holes of HoleNames.g.procedure with the callees the body called.

Equations

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

noncomputable def Experiment.HoleNames.g.procedure : proctype () → Unit uses ((String, ℕ) → Bool, (String, ℕ) → Bool)

The body of proc g of module HoleNames, as a procedure of its own: the 2 calls it makes to module parameters (S, T) are its holes, in the order the body makes them.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see HoleNames.g.procedure.apply_simp) rather than run. Use HoleNames.g for this procedure as a module.

Equations

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

theorem Experiment.HoleNames.g.procedure.apply_simp (holeArgs✝ : (GaudisCrypt.HoleSigs.cons (procsig (String, ℕ) → Bool) (GaudisCrypt.HoleSigs.cons (procsig (String, ℕ) → Bool) GaudisCrypt.HoleSigs.empty)).Instantiation) : procedure.instantiate holeArgs✝ = proc () : Unit { var S_main : Bool; S_main <- call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero) ("hi", 3); call (holeArgs✝.lookup GaudisCrypt.HoleIndex.zero.succ) ("ho", 4); return () }

Instantiating the holes of HoleNames.g.procedure with a tuple holeArgs of procedures: the body of proc g as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [HoleNames.g.procedure.apply_simp]).

noncomputable def Experiment.HoleNames.h.procedure : proctype () -> Unit

The body of proc h of module HoleNames, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see HoleNames.h.procedure.apply_simp) rather than run. Use HoleNames.h for this procedure as a module.

Equations

• Experiment.HoleNames.h.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.HoleNames.apply_simp (S T : TestModule) : GaudisCrypt.Module.app HoleNames (GaudisCrypt.Module.pair S T) = M2.mk { g := GaudisCrypt.Module.app (GaudisCrypt.Module.app g S) T, h := h }

@[simp]: applying HoleNames to a tuple of its 2 parameters S, T — the record of its procedures HoleNames.g, HoleNames.h, each applied to the parameters it uses.

This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with HoleNames.g.apply_simp, HoleNames.h.apply_simp to fill that procedure's holes.

noncomputable def Experiment.HoleNames : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod TestModule TestModule) M2

The module declared by module HoleNames, abstracted over its 2 parameters S, T, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the module type it was declared with.

Applied to such a tuple it is the record of its procedures HoleNames.g, HoleNames.h, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma HoleNames.apply_simp says.

Equations

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

noncomputable def Experiment.NamedParams.plain : NamedParams → GaudisCrypt.Module GaudisCrypt.ModuleTypeRep.unit

The field plain of a module of type NamedParams: the projection onto component 3 of the right-nested tuple NamedParams.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

NamedParams.plain.mk_simp reads this field back off a module built by NamedParams.mk; NamedParams.plain.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.plain = (GaudisCrypt.Module.snd' theModule✝).snd'.snd'

@[reducible]

noncomputable def Experiment.NamedParams.mk : Structure → NamedParams

Builds a module of type NamedParams from the record NamedParams.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of NamedParams.structure (NamedParams.mk_destruct, NamedParams.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas NamedParams.commit.mk_simp, NamedParams.gen.mk_simp, NamedParams.unnamed.mk_simp, NamedParams.plain.mk_simp.

Equations

• Experiment.NamedParams.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.commit (GaudisCrypt.Module.pair' theRecord✝.gen (GaudisCrypt.Module.pair' theRecord✝.unnamed theRecord✝.plain))

noncomputable def Experiment.NamedParams.plain.utilities : GaudisCrypt.ModuleTypeUtilities NamedParams (GaudisCrypt.Module GaudisCrypt.ModuleTypeRep.unit) plain

What is derivable about the accessor NamedParams.plain, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• NamedParams.plain.utilities.accessorModule : NamedParams →ₘ … — the accessor as a module, a projection being a module morphism;
• NamedParams.plain.utilities.apply_simp — Module.app NamedParams.plain.utilities.accessorModule m = NamedParams.plain m: applying that module is the accessor;
• NamedParams.plain.utilities.expression_eq — the same at the level of expressions: (NamedParams.plain m).expression = (NamedParams.plain.utilities.proj m.expression).reduce.

Equations

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

def Experiment.NamedParams.typeRep : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying NamedParams, the module type declared by moduletype NamedParams: the right-nested product of its 4 field types, in declaration order.

NamedParams is by definition Module NamedParams.typeRep.

Equations

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

@[simp]

theorem Experiment.NamedParams.destruct_mk (theModule✝ : NamedParams) : mk theModule✝.structure = theModule✝

@[simp]: NamedParams.mk (NamedParams.structure m) = m — rebuilding a module from its own fields gives that module back.

noncomputable def Experiment.NamedParams.gen : NamedParams → procmod () → ℕ

The field gen of a module of type NamedParams: the projection onto component 1 of the right-nested tuple NamedParams.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

NamedParams.gen.mk_simp reads this field back off a module built by NamedParams.mk; NamedParams.gen.utilities has the accessor as a module, and the lemmas about it.

It takes no parameters (recorded in @[gaudiProcParamNames]).

Equations

• theModule✝.gen = (GaudisCrypt.Module.snd' theModule✝).fst'

@[simp]

theorem Experiment.NamedParams.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: NamedParams.structure (NamedParams.mk r) = r — destructing a module built from a record gives that record back.

@[simp]

theorem Experiment.NamedParams.gen.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).gen = theRecord✝.gen

@[simp]: reading the field gen back off a module built from a record — NamedParams.gen (NamedParams.mk r) = r.gen.

It is what carries the right-hand side of an X.apply_simp (which is an NamedParams.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.gen.apply_simp.

noncomputable def Experiment.NamedParams.commit.utilities : GaudisCrypt.ModuleTypeUtilities NamedParams (procmod (ℕ, Bool) → Bool) commit

What is derivable about the accessor NamedParams.commit, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• NamedParams.commit.utilities.accessorModule : NamedParams →ₘ … — the accessor as a module, a projection being a module morphism;
• NamedParams.commit.utilities.apply_simp — Module.app NamedParams.commit.utilities.accessorModule m = NamedParams.commit m: applying that module is the accessor;
• NamedParams.commit.utilities.expression_eq — the same at the level of expressions: (NamedParams.commit m).expression = (NamedParams.commit.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.NamedParams.commit : NamedParams → procmod (ℕ, Bool) → Bool

The field commit of a module of type NamedParams: the projection onto component 0 of the right-nested tuple NamedParams.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

NamedParams.commit.mk_simp reads this field back off a module built by NamedParams.mk; NamedParams.commit.utilities has the accessor as a module, and the lemmas about it.

Its parameters are named h, m, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• theModule✝.commit = GaudisCrypt.Module.fst' theModule✝

@[simp]

theorem Experiment.NamedParams.plain.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).plain = theRecord✝.plain

@[simp]: reading the field plain back off a module built from a record — NamedParams.plain (NamedParams.mk r) = r.plain.

It is what carries the right-hand side of an X.apply_simp (which is an NamedParams.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.plain.apply_simp.

noncomputable def Experiment.NamedParams.unnamed : NamedParams → procmod (ℕ) → ℕ

The field unnamed of a module of type NamedParams: the projection onto component 2 of the right-nested tuple NamedParams.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

NamedParams.unnamed.mk_simp reads this field back off a module built by NamedParams.mk; NamedParams.unnamed.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.unnamed = (GaudisCrypt.Module.snd' theModule✝).snd'.fst'

@[implicit_reducible]

instance Experiment.instIsModuleNamedParams : GaudisCrypt.IsModule NamedParams

The IsModule NamedParams instance: NamedParams is a module type, with representation NamedParams.typeRep.

It is what lets the name NamedParams stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module NamedParams.typeRep would do on its own but NamedParams, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModuleNamedParams = { moduleTypeRep := Experiment.NamedParams.typeRep, isModule := ⋯ }

noncomputable def Experiment.NamedParams.gen.utilities : GaudisCrypt.ModuleTypeUtilities NamedParams (procmod () → ℕ) gen

What is derivable about the accessor NamedParams.gen, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• NamedParams.gen.utilities.accessorModule : NamedParams →ₘ … — the accessor as a module, a projection being a module morphism;
• NamedParams.gen.utilities.apply_simp — Module.app NamedParams.gen.utilities.accessorModule m = NamedParams.gen m: applying that module is the accessor;
• NamedParams.gen.utilities.expression_eq — the same at the level of expressions: (NamedParams.gen m).expression = (NamedParams.gen.utilities.proj m.expression).reduce.

Equations

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

@[simp]

theorem Experiment.NamedParams.commit.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).commit = theRecord✝.commit

@[simp]: reading the field commit back off a module built from a record — NamedParams.commit (NamedParams.mk r) = r.commit.

It is what carries the right-hand side of an X.apply_simp (which is an NamedParams.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.commit.apply_simp.

structure Experiment.NamedParams.Structure : Type 1

The record of the fields of a module of type NamedParams: the fields commit, gen, unnamed, plain, one per moduletype field, each of that field's own module type.

NamedParams.mk turns such a record into a NamedParams, NamedParams.structure turns a NamedParams back into one.

• commit : procmod (ℕ, Bool) → Bool
• gen : procmod () → ℕ
• unnamed : procmod (ℕ) → ℕ
• plain : GaudisCrypt.Module GaudisCrypt.ModuleTypeRep.unit

@[simp]

theorem Experiment.NamedParams.unnamed.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).unnamed = theRecord✝.unnamed

@[simp]: reading the field unnamed back off a module built from a record — NamedParams.unnamed (NamedParams.mk r) = r.unnamed.

It is what carries the right-hand side of an X.apply_simp (which is an NamedParams.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.unnamed.apply_simp.

noncomputable def Experiment.NamedParams.structure : NamedParams → Structure

The record of a module's fields: NamedParams.structure m is NamedParams.Structure.mk applied to NamedParams.commit, NamedParams.gen, NamedParams.unnamed, NamedParams.plain of m.

Inverse of NamedParams.mk (NamedParams.mk_destruct, NamedParams.destruct_mk).

Equations

• theModule✝.structure = { commit := theModule✝.commit, gen := theModule✝.gen, unnamed := theModule✝.unnamed, plain := theModule✝.plain }

def Experiment.NamedParams : Type 1

The module type declared by moduletype NamedParams, with fields commit, gen, unnamed, plain: the type Module NamedParams.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with NamedParams.mk, read a single field off one with the accessors NamedParams.commit, NamedParams.gen, NamedParams.unnamed, NamedParams.plain, and get the whole record back with NamedParams.structure.

Equations

• Experiment.NamedParams = GaudisCrypt.Module Experiment.NamedParams.typeRep

noncomputable def Experiment.NamedParams.unnamed.utilities : GaudisCrypt.ModuleTypeUtilities NamedParams (procmod (ℕ) → ℕ) unnamed

What is derivable about the accessor NamedParams.unnamed, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• NamedParams.unnamed.utilities.accessorModule : NamedParams →ₘ … — the accessor as a module, a projection being a module morphism;
• NamedParams.unnamed.utilities.apply_simp — Module.app NamedParams.unnamed.utilities.accessorModule m = NamedParams.unnamed m: applying that module is the accessor;
• NamedParams.unnamed.utilities.expression_eq — the same at the level of expressions: (NamedParams.unnamed m).expression = (NamedParams.unnamed.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.NamedProcs.p.procedure : proctype (ℕ, ℕ) -> ℕ

The body of proc p of module NamedProcs, as a procedure of its own: it calls no module parameter, so it has no holes.

A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see NamedProcs.p.procedure.apply_simp) rather than run. Use NamedProcs.p for this procedure as a module.

Equations

• Experiment.NamedProcs.p.procedure = proc (a : ℕ, b : ℕ) : ℕ { skip; return §a }

theorem Experiment.NamedProcs.p.procedure.apply_simp (holeArgs✝ : GaudisCrypt.HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc (a : ℕ, b : ℕ) : ℕ { skip; return §a }

Instantiating the holes of NamedProcs.p.procedure with a tuple holeArgs of procedures: the body of proc p as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.

Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [NamedProcs.p.procedure.apply_simp]).

noncomputable def Experiment.NamedProcs.p : procmod (ℕ, ℕ) → ℕ

proc p of module NamedProcs as a module: Module.proc NamedProcs.p.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — NamedProcs.p.apply_simp says exactly that.

Equations

• Experiment.NamedProcs.p = GaudisCrypt.Module.proc Experiment.NamedProcs.p.procedure

@[simp]

theorem Experiment.NamedProcs.p.apply_simp : p = GaudisCrypt.Module.proc procedure

@[simp]: NamedProcs.p = Module.proc NamedProcs.p.procedure — true by definition, proc p using no module parameter and so having no holes to fill.

noncomputable def Experiment.NamedProcs : procmod (ℕ, ℕ) → ℕ

The module declared by module NamedProcs: the record of its procedures NamedProcs.p.

The declaration has no parameter list, so no procedure of it can call one either and the module is not a function — it is the plain record itself, and there is no NamedProcs.apply_simp to apply it with.

Equations

• Experiment.NamedProcs = Experiment.NamedProcs.p

noncomputable def Experiment.PartlyNamed.f.utilities : GaudisCrypt.ModuleTypeUtilities PartlyNamed (procmod (ℕ, Bool) → Bool) f

What is derivable about the accessor PartlyNamed.f, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):

• PartlyNamed.f.utilities.accessorModule : PartlyNamed →ₘ … — the accessor as a module, a projection being a module morphism;
• PartlyNamed.f.utilities.apply_simp — Module.app PartlyNamed.f.utilities.accessorModule m = PartlyNamed.f m: applying that module is the accessor;
• PartlyNamed.f.utilities.expression_eq — the same at the level of expressions: (PartlyNamed.f m).expression = (PartlyNamed.f.utilities.proj m.expression).reduce.

Equations

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

noncomputable def Experiment.PartlyNamed.f : PartlyNamed → procmod (ℕ, Bool) → Bool

The field f of a module of type PartlyNamed: the projection onto component 0 of the right-nested tuple PartlyNamed.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].

PartlyNamed.f.mk_simp reads this field back off a module built by PartlyNamed.mk; PartlyNamed.f.utilities has the accessor as a module, and the lemmas about it.

Equations

• theModule✝.f = theModule✝

def Experiment.PartlyNamed : Type 1

The module type declared by moduletype PartlyNamed, with fields f: the type Module PartlyNamed.typeRep of modules that are a right-nested tuple of the field types.

Build one from a record of its fields with PartlyNamed.mk, read a single field off one with the accessors PartlyNamed.f, and get the whole record back with PartlyNamed.structure.

Equations

• Experiment.PartlyNamed = GaudisCrypt.Module Experiment.PartlyNamed.typeRep

@[simp]

theorem Experiment.PartlyNamed.destruct_mk (theModule✝ : PartlyNamed) : mk theModule✝.structure = theModule✝

@[simp]: PartlyNamed.mk (PartlyNamed.structure m) = m — rebuilding a module from its own fields gives that module back.

@[simp]

theorem Experiment.PartlyNamed.f.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).f = theRecord✝.f

@[simp]: reading the field f back off a module built from a record — PartlyNamed.f (PartlyNamed.mk r) = r.f.

It is what carries the right-hand side of an X.apply_simp (which is an PartlyNamed.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.f.apply_simp.

@[simp]

theorem Experiment.PartlyNamed.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

@[simp]: PartlyNamed.structure (PartlyNamed.mk r) = r — destructing a module built from a record gives that record back.

def Experiment.PartlyNamed.typeRep : GaudisCrypt.ModuleTypeRep

The ModuleTypeRep underlying PartlyNamed, the module type declared by moduletype PartlyNamed: the right-nested product of its 1 field types, in declaration order.

PartlyNamed is by definition Module PartlyNamed.typeRep.

Equations

• Experiment.PartlyNamed.typeRep = GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ, Bool) → Bool)

structure Experiment.PartlyNamed.Structure : Type 1

The record of the fields of a module of type PartlyNamed: the fields f, one per moduletype field, each of that field's own module type.

PartlyNamed.mk turns such a record into a PartlyNamed, PartlyNamed.structure turns a PartlyNamed back into one.

• f : procmod (ℕ, Bool) → Bool

@[implicit_reducible]

instance Experiment.instIsModulePartlyNamed : GaudisCrypt.IsModule PartlyNamed

The IsModule PartlyNamed instance: PartlyNamed is a module type, with representation PartlyNamed.typeRep.

It is what lets the name PartlyNamed stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module PartlyNamed.typeRep would do on its own but PartlyNamed, a plain (non-reducible) def, would not.

Equations

• Experiment.instIsModulePartlyNamed = { moduleTypeRep := Experiment.PartlyNamed.typeRep, isModule := ⋯ }

noncomputable def Experiment.PartlyNamed.structure : PartlyNamed → Structure

The record of a module's fields: PartlyNamed.structure m is PartlyNamed.Structure.mk applied to PartlyNamed.f of m.

Inverse of PartlyNamed.mk (PartlyNamed.mk_destruct, PartlyNamed.destruct_mk).

Equations

• theModule✝.structure = { f := theModule✝.f }

@[reducible]

noncomputable def Experiment.PartlyNamed.mk : Structure → PartlyNamed

Builds a module of type PartlyNamed from the record PartlyNamed.Structure of its fields, as a right-nested Module.pair'. @[reducible].

Inverse of PartlyNamed.structure (PartlyNamed.mk_destruct, PartlyNamed.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas PartlyNamed.f.mk_simp.

Equations

• Experiment.PartlyNamed.mk theRecord✝ = theRecord✝.f