Tests for HoareSyntax #
What is derivable about the accessor TestSig.g, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):
TestSig.g.utilities.accessorModule : TestSig →ₘ …— the accessor as a module, a projection being a module morphism;TestSig.g.utilities.apply_simp—Module.app TestSig.g.utilities.accessorModule m = TestSig.g m: applying that module is the accessor;TestSig.g.utilities.expression_eq— the same at the level of expressions:(TestSig.g m).expression = (TestSig.g.utilities.proj m.expression).reduce.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Builds a module of type TestSig from the record TestSig.Structure of its fields, as a right-nested Module.pair'. @[reducible].
Inverse of TestSig.structure (TestSig.mk_destruct, TestSig.destruct_mk); a single field of a module built this way is read back by the @[simp] lemmas TestSig.f.mk_simp, TestSig.g.mk_simp.
Equations
- GaudisCrypt.HoareSyntaxTest.TestSig.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.f theRecord✝.g
Instances For
@[simp]: reading the field g back off a module built from a record — TestSig.g (TestSig.mk r) = r.g.
It is what carries the right-hand side of an X.apply_simp (which is an TestSig.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.g.apply_simp.
The field f of a module of type TestSig: the projection onto component 0 of the right-nested tuple TestSig.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].
TestSig.f.mk_simp reads this field back off a module built by TestSig.mk; TestSig.f.utilities has the accessor as a module, and the lemmas about it.
Its parameters are named a, b, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).
Equations
- theModule✝.f = GaudisCrypt.Module.fst' theModule✝
Instances For
The record of a module's fields: TestSig.structure m is TestSig.Structure.mk applied to TestSig.f, TestSig.g of m.
Inverse of TestSig.mk (TestSig.mk_destruct, TestSig.destruct_mk).
Instances For
The field g of a module of type TestSig: the projection onto component 1 of the right-nested tuple TestSig.typeRep, as a chain of Module.fst'/Module.snd'. Tagged @[module_accessor].
TestSig.g.mk_simp reads this field back off a module built by TestSig.mk; TestSig.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.snd' theModule✝
Instances For
@[simp]: TestSig.structure (TestSig.mk r) = r — destructing a module built from a record gives that record back.
@[simp]: TestSig.mk (TestSig.structure m) = m — rebuilding a module from its own fields gives that module back.
What is derivable about the accessor TestSig.f, bundled into one ModuleTypeUtilities (one name per field in the namespace, rather than one per fact):
TestSig.f.utilities.accessorModule : TestSig →ₘ …— the accessor as a module, a projection being a module morphism;TestSig.f.utilities.apply_simp—Module.app TestSig.f.utilities.accessorModule m = TestSig.f m: applying that module is the accessor;TestSig.f.utilities.expression_eq— the same at the level of expressions:(TestSig.f m).expression = (TestSig.f.utilities.proj m.expression).reduce.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The IsModule TestSig instance: TestSig is a module type, with representation TestSig.typeRep.
It is what lets the name TestSig stand where a module type is expected — in Module.Arr/Module.Prod (→ₘ/×ₘ), say — which the underlying Module TestSig.typeRep would do on its own but TestSig, a plain (non-reducible) def, would not.
Equations
- GaudisCrypt.HoareSyntaxTest.instIsModuleTestSig = { moduleTypeRep := GaudisCrypt.HoareSyntaxTest.TestSig.typeRep, isModule := ⋯ }
The module type declared by moduletype TestSig, with fields f, g: the type Module TestSig.typeRep of modules that are a right-nested tuple of the field types.
Build one from a record of its fields with TestSig.mk, read a single field off one with the accessors TestSig.f, TestSig.g, and get the whole record back with TestSig.structure.
Equations
Instances For
@[simp]: reading the field f back off a module built from a record — TestSig.f (TestSig.mk r) = r.f.
It is what carries the right-hand side of an X.apply_simp (which is an TestSig.mk) on to the field the caller actually asked for, so that simp chains X.apply_simp into X.f.apply_simp.
The ModuleTypeRep underlying TestSig, the module type declared by moduletype TestSig: the right-nested product of its 2 field types, in declaration order.
TestSig is by definition Module TestSig.typeRep.
Equations
Instances For
The record of the fields of a module of type TestSig: the fields f, g, one per moduletype field, each of that field's own module type.
TestSig.mk turns such a record into a TestSig, TestSig.structure turns a TestSig back into one.
Instances For
The body of proc p of module TestMod, 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 TestMod.p.procedure.apply_simp) rather than run. Use TestMod.p for this procedure as a module.
Equations
- GaudisCrypt.HoareSyntaxTest.TestMod.p.procedure = proc (u : ℤ) : ℤ { skip; return §u }
Instances For
The module declared by module TestMod: the record of its procedures TestMod.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 TestMod.apply_simp to apply it with.
Instances For
Instantiating the holes of TestMod.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 [TestMod.p.procedure.apply_simp]).
@[simp]: TestMod.p = Module.proc TestMod.p.procedure — true by definition, proc p using no module parameter and so having no holes to fill.
proc p of module TestMod as a module: Module.proc TestMod.p.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — TestMod.p.apply_simp says exactly that.