Concrete syntax for modules

Surface syntax for module types (procmod, ×ₘ, →ₘ), for the moduletype and module commands, and the tactics the commands use in the proofs they emit. Program and procedure syntax is in ProgramSyntax.lean.

Module types — moduletype Name { … }

A top-level command declaring a record-like module type, e.g.:

moduletype TwoProcs {
  proc enc (k : Nat, m : Nat) -> Bool;
  module aux : ModuleTypeRep.arr (ModuleTypeRep.proc (procsig (Nat) -> Nat)) ModuleTypeRep.unit;
}

where each field's type is a ModuleTypeRep. A field may also be written proc fᵢ (A₁, …) -> R; as shorthand for module fᵢ : ModuleTypeRep.proc (procsig (A₁, …) -> R);, with the arguments optionally named as above — the one place where a parameter name is kept (in @[gaudiProcParamNames], a ProcedureSignature holding only types). It generates Name (the corresponding Module), a record Name.Structure with fields fᵢ : Module Tᵢ — a proc field getting the Module.Proc (procsig …) spelling of that, the one a module-declared procedure carries — accessors Name.fᵢ, a constructor Name.mk, a destructor Name.structure, and @[simp] lemmas relating them: Name.fᵢ.mk_simp reads a field back off a mk, and Name.mk_destruct/Name.destruct_mk are the round trip through Name.structure.

Module type of a procedure — procmod (…) -> R

procmod (T, …) -> R is Module.Proc (procsig (T,…) -> R): the same surface as proctype, but producing the module type of a procedure rather than the Procedure type. It is a Type, and so composes with the other module type formers (Module.Arr/→ₘ, Module.Prod/×ₘ), not with the ModuleTypeRep constructors — for a type rep write .proc (procsig (…) -> R).

The return type is parsed at precedence 36, above the usual infix operators, so a trailing one groups as (procmod (…) -> R) ⊙ … rather than folding into R. A product/function return type therefore needs parentheses: procmod (…) -> (A × B). (No uses clause: for a procedure-with-holes module type write ModuleTypeRep.arr explicitly.)

An argument may be named — procmod (h : G, m : F) -> Bool — and the name is then dropped, a ProcedureSignature recording types only. moduletype is the one place where a name is kept (in @[gaudiProcParamNames]).

def GaudisCrypt.«termProcmod(_)→->_» : Lean.ParserDescr

Equations

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

def GaudisCrypt.unexpandProcMod : Lean.PrettyPrinter.Unexpander

Equations

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

Concrete syntax for module types

M →ₘ N is Module.Arr M N and M ×ₘ N is Module.Prod M N: the arrow and the product on the types of modules (Module T, a name declared by moduletype, …), each side classified by an IsModule instance. Precedences mirror →/×: ×ₘ (35) binds tighter than →ₘ (25), both right-associative. Both are scoped to GaudisCrypt, so opening that namespace activates them.

procmod (…) -> R is the third of them: the module type Module.Proc (procsig (…) -> R).

ModuleTypeRep itself has no infix notation; its constructors are written .proc/.arr/.prod/.unit by dot notation.

def GaudisCrypt.«term_×ₘ_» : Lean.TrailingParserDescr

Equations

• GaudisCrypt.«term_×ₘ_» = Lean.ParserDescr.trailingNode `GaudisCrypt.«term_×ₘ_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ₘ ") (Lean.ParserDescr.cat `term 35))

def GaudisCrypt.«term_→ₘ_» : Lean.TrailingParserDescr

Equations

• GaudisCrypt.«term_→ₘ_» = Lean.ParserDescr.trailingNode `GaudisCrypt.«term_→ₘ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₘ ") (Lean.ParserDescr.cat `term 25))

Reporting what a command declared

moduletype and module both emit a whole batch of declarations from one command. Each of them is described by a DeclInfo, which carries the two things a user can be told about a generated name: a one-line blurb, listed by logDeclared in an info message right after the command, and a full doc, attached by docDeclared as the declaration's docstring so that hovering over X.f.apply_simp explains what that lemma is. Both live here, ahead of both commands, because moduletype (below) is the first user.

structure GaudisCrypt.ModuleDecl.DeclInfo : Type

One declaration a module/moduletype command generated, and what to say about it: blurb is the one-line description logDeclared puts in the Defined: listing, doc the Markdown docstring docDeclared attaches to the declaration itself.

name is the short name, as the command spelled it — it is resolved against the current namespace, which is where the commands put what they declare.

• name : Lean.Name

  The generated declaration's name, as the command spelled it (short, unqualified by the current namespace).

• blurb : String

  One line, for the Defined: listing: what this declaration is.

• doc : String

  The docstring to attach, in Markdown: what this declaration is for, spelled out.

def GaudisCrypt.ModuleDecl.docDeclared (declared : Array DeclInfo) : Lean.Elab.Command.CommandElabM Unit

Attach each generated declaration's docstring, so that hovering over it in the editor — and doc-gen4's API docs — explain what the command made it for. The declarations these commands emit have no source text of their own to carry a doc comment, so the docstring is put into the environment directly (addDocStringCore, i.e. Markdown, as if it had been written as /-- … -/ in front of the declaration).

Silently skips a name that does not resolve: a batch is reported even when a field or a procedure failed to elaborate.

Equations

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

def GaudisCrypt.ModuleDecl.insertLinkWidget : Lean.Widget.Module

A link that inserts suggestion over range and then moves the cursor to newSelection. Same idea as Lean.Meta.Hint.textInsertionWidget — whose link text is fixed to [apply] and which leaves the cursor where it was — and as ProofWidgets' MakeEditLink, which needs the document's URI up front; here it is read from the infoview's position context instead.

Equations

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

def GaudisCrypt.ModuleDecl.logDeclared (ref : Lean.Syntax) (declared : Array DeclInfo) : Lean.Elab.Command.CommandElabM Unit

Report the declarations a module/moduletype command generated, as

Defined:
  def X.g.procedure — body of proc g

where each name is a link that inserts #check <name> right after the command and puts the cursor at the end of the inserted line (the same edit is also offered as a code action). Each DeclInfo's blurb is the description shown after the name; its doc is what docDeclared attaches to the declaration, and is not repeated here.

Each name is prefixed as it would be written by hand: the @[simp] attribute when the generated lemma carries it — so the listing says not only what exists but what will fire on its own — and then the declaration's keyword (declKeyword), which distinguishes the definitions from the lemmas about them.

Equations

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

Lean parameters of a module/moduletype declaration

Both commands take, after the name, a list of ordinary Lean binders — types, values, implicit and instance arguments — exactly as def and theorem do:

moduletype Sized (n : Nat) { proc f (Fin n) -> Bool; }
module Twice (n : Nat) using (S : Sized n) { … }

Every declaration the command generates is abstracted over those binders, and every reference one generated declaration makes to another passes them along by name (X.typeRep (n := n), so that implicit and instance parameters travel too). That is the whole of the semantics: a parameterised declaration is the declaration it would be with those binders written on it by hand.

A parameter may also come from a section variable, and then need not be written at all:

variable (n : Nat)

moduletype Sized { proc f (Fin n) -> Bool; }
module Twice using (S : Sized n) { … }

means the same as the pair above. A section variable the declaration mentions anywhere — in a field type, in a procedure body, in a module parameter's type — becomes a Lean parameter of it, in front of the ones it writes itself, together with the variables it depends on and the instance variables that are about them (variable {α} [Inhabited α]; using α brings the instance too). Lean's own auto-inclusion is left the variables no declaration of the batch mentions (instance variables about nothing the batch mentions, say): it works per declaration, by use, and the generated declarations of one command refer to one another and so all have to take the same parameters.

The module parameters are a different thing and are now written after using. They used to be written in the same position as the Lean parameters are, and they look like a Lean binder list that got a comma in it — which is not valid Lean binder syntax. Rather than let that fail in the parser with a message about the comma, gaudi_param parses such a group and the commands reject it themselves, pointing at using. A single module parameter, (S : CommitmentScheme), is valid Lean binder syntax and so parses as a Lean parameter; that is a warning (linter.gaudisCrypt.using, below), not an error, since a module-typed Lean parameter is a legitimate — if unusual — thing to want.

def gaudiBinder : Lean.Parser.Parser

Lean.Parser.Term.bracketedBinder under a name that syntax will accept: the core one is not tagged for use in generated parsers ("refusing to generate code for imported parser declaration"), and the attribute is what makes an alias of it usable.

Equations

• gaudiBinder = Lean.Parser.Term.bracketedBinder

def gaudi_param.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.gaudi_param : Category

One entry of a module/moduletype parameter list: an ordinary Lean binder, or a parenthesised comma-separated group, which is only ever the old spelling of module parameters and exists here to be rejected with a message naming using.

Equations

• Lean.Parser.Category.gaudi_param = { }

def gaudiParamBinder : Lean.ParserDescr

Equations

• gaudiParamBinder = Lean.ParserDescr.node `gaudiParamBinder 1022 (Lean.ParserDescr.parser `gaudiBinder)

def gaudiParamGroup : Lean.ParserDescr

Equations

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

opaque linter.gaudisCrypt.using : Lean.Option Bool

def GaudisCrypt.ModuleDecl.paramBinders (what : String) (ps : Array (Lean.TSyntax `gaudi_param)) : Lean.Elab.Command.CommandElabM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

The binder syntax of a gaudi_param list, with the comma groups rejected. what names the command, for the error message.

Equations

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

def GaudisCrypt.ModuleDecl.internalIdent (base : Lean.Name) : Lean.Elab.Command.CommandElabM Lean.Ident

A binder one of the commands invents for itself — the module an accessor takes, the record mk takes, and so on. Hygienic, so that a Lean parameter of the same name cannot capture it: the generated declarations refer to these binders by name, and a user parameter called m used to shadow the module binder in def X.gen (m : Nat) (m : X (m := m)) : … (Fin (m+1)), whereupon the field type read the module where it wanted the number and the whole batch failed from there.

The names are also spelled out rather than single letters, which is a separate matter from the capture: these are what shows up in every #check of a generated declaration and in every goal one appears in, and the delaborator strips the macro scopes again, so what a reader sees is theRecord, not theRecord✝. Renaming alone would only have moved the collision to a less likely name; hygiene alone would have left the single letters on display.

Equations

• GaudisCrypt.ModuleDecl.internalIdent base = do let __do_lift ← Lean.MonadQuotation.addMacroScope base pure (Lean.mkIdent __do_lift)

structure GaudisCrypt.ModuleDecl.LeanParams : Type

The Lean parameters of a module/moduletype declaration: the binders every generated declaration is abstracted over, and the names that pass them from one to the next.

• binders : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

  The binders, every position named (see nameParams).

• args : Array Lean.Ident

  Their names, in order.

def GaudisCrypt.ModuleDecl.nameParams (bs : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) : Lean.Elab.Command.CommandElabM LeanParams

Give every binder position a name, and return the binders so named together with the arguments that pass them on. A reference from one generated declaration to another names each parameter, so it needs a name even for the positions the user left anonymous ([Inhabited α], (_ : T)).

Equations

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

partial def GaudisCrypt.ModuleDecl.mentions (names : List Lean.Name) (s : Lean.Syntax) : Bool

Does s mention one of the identifiers names? A name also counts as mentioned when it heads a field access (types.Value is one identifier, not two).

def GaudisCrypt.ModuleDecl.sectionBinders (stx : Lean.Syntax) (own : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) : Lean.Elab.Command.CommandElabM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

The section variables (variable (types : CommitmentTypes)) that a declaration written as stx uses, to go in front of the parameters own it writes itself: the ones whose names stx mentions, the ones those in turn mention, and the instance variables among them that are about variables already taken. A variable whose name own binds is left alone — the written binder wins.

The section variables a declaration uses have to become Lean parameters of it rather than be left to Lean's own auto-inclusion, because a module/moduletype is a batch of declarations that refer to one another by name (X.typeRep (types := types)): auto-inclusion puts a variable only in those declarations whose body happens to mention it, and a reference from one of the batch to another would then be missing an argument. Only the variables that no declaration of the batch takes a stand on — mentioned by none of them — are left to it.

Equations

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

def GaudisCrypt.ModuleDecl.LeanParams.ref (P : LeanParams) (id : Lean.Ident) : Lean.Elab.Command.CommandElabM Lean.Term

How a generated declaration refers to another one: bare when there are no parameters, and X.f (a₁ := a₁) … (aₙ := aₙ) when there are. Named arguments, not @: @ would also expose the section variables auto-included in the referenced declaration, which are none of this command's business, while a name reaches an implicit or instance parameter without disturbing them.

Equations

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

def GaudisCrypt.ModuleDecl.LeanParams.withBinders {α : Type} (P : LeanParams) (k : Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

Run k with the Lean parameters in the local context, so that a term mentioning them (a procedure body, a signature to be read back) can be elaborated.

Equations

• P.withBinders k = Lean.Elab.Term.elabBinders (Array.map (fun (x : Lean.TSyntax `Lean.Parser.Term.bracketedBinder) => x.raw) P.binders) fun (x : Array Lean.Expr) => k

def GaudisCrypt.ModuleDecl.warnModuleTypedParam (P : LeanParams) : Lean.Elab.Command.CommandElabM Unit

Warn when the last Lean parameter of a module declaration has a module type, which almost always means the module parameters were written without using. Silent when the declaration has a using clause (the author has then clearly chosen), and suppressed by set_option linter.gaudisCrypt.using false.

Equations

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

def GaudisCrypt.introAnonymous : Lean.Elab.Tactic.TacticM Unit

intro _: introduce one hypothesis under an inaccessible name. Same step Elab.Tactic.evalIntro takes for a _ argument (MVarId.intro _`).

Equations

• GaudisCrypt.introAnonymous = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => do let __do_lift ← g.intro `_ pure [__do_lift.2]

def GaudisCrypt.applyConst (c : Lean.Name) : Lean.Elab.Tactic.TacticM Unit

apply c for a constant c, named rather than parsed. Elab.Tactic.evalApply on an ident resolves it to exactly this constant (Term.resolveId?) and then calls MVarId.apply; the synthesizeSyntheticMVarsNoPostponing afterwards is its too, for the instance metavariables the apply may leave.

Equations

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

def GaudisCrypt.tryTac (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

try tac, which is first | tac | skip.

The first | t₁ | … | tₙ these scripts use is spelled t₁ <|> … <|> tₙ below: that is what Elab.Tactic.evalFirst chains its alternatives with, and TacticM's MonadExcept instance is the backtracking one (Tactic.tryCatchRestore), so a failed alternative is rolled back.

Equations

• GaudisCrypt.tryTac tac = (tac <|> pure ())

def GaudisCrypt.repeatTac (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

repeat tac: run tac on the main goal until it fails, rolling the failing attempt back. The loop Elab.Tactic.evalRepeat runs, including its withoutRecover.

Equations

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

def GaudisCrypt.repeatAllTac (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

repeat' tac: apply tac to every goal, recursively to the subgoals it produces, until it fails on all of them. Elab.Tactic.evalRepeat' is Meta.repeat' over the goal list with tac run on one goal at a time, which is what this is.

Equations

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

def GaudisCrypt.simpOnlyConsts (names : Array Lean.Name) (extraSets : Array Lean.Meta.SimpTheorems := #[]) : Lean.Elab.Tactic.TacticM Unit

simp only [c₁, …, cₙ] on the main goal, as a TacticM function, with the constants given as Names instead of as syntax — so that a rename of one of them is a compile error here rather than a proof that stops working somewhere downstream.

Assembled the way Elab.Tactic.mkSimpContext assembles a simp only: the theorem set starts from simpOnlyBuiltins (eq_self, iff_self) and nothing else, there are no simprocs, and each argument is added as a rewrite rule or as a definition to unfold according to whether its type is a Prop — the same split Elab.Tactic.elabDeclToUnfoldOrTheorem makes. extraSets are whole simp sets (simp only [module_accessor]), which simp only keeps in their own slots of the theorem array rather than merging into the argument set.

Failure on a goal it does not change is Simp.Config.failIfUnchanged, on by default and left that way: the trys and firsts around these scripts depend on it.

Equations

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

def GaudisCrypt.moduleAccessorTheorems : Lean.Elab.Tactic.TacticM Lean.Meta.SimpTheorems

The module_accessor simp set (Modules.lean), as simp only [module_accessor] picks it up: a whole extension, pushed into its own slot of the theorem array rather than merged in with the named constants.

Equations

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

def GaudisCrypt.resolveHere (n : Lean.Name) : Lean.Elab.Tactic.TacticM Lean.Name

The accessor moduletype hands these tactics is spelled relative to the namespace the declaration sits in (TestModule.f inside namespace Experiment), so it has to be resolved where the proof runs, exactly as the ident spliced into a simp only used to be. The fixed lemma names around it need none of this: they are ``-literals, resolved when this file compiles.

Equations

• GaudisCrypt.resolveHere n = liftM (Lean.realizeGlobalConstNoOverload (Lean.mkIdent n).raw)

The lemma lists these scripts share. They were spelled out in each script while the scripts were tactic quotations, where nothing could be named or reused; as Array Names they are written once.

def GaudisCrypt.reduceStripInner : Array Lean.Name

Pushes a .reduce out of a .fst/.snd, undoing what a toModule left inside a composite expression.

Equations

• GaudisCrypt.reduceStripInner = #[`GaudisCrypt.ModuleExpression.reduce_fst_inner, `GaudisCrypt.ModuleExpression.reduce_snd_inner]

def GaudisCrypt.reduceStripComposite : Array Lean.Name

reduceStripInner with the .app and .pair positions in front of it: the whole set of stripping lemmas, for the scripts that unfold Module.pair as well.

Equations

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

def GaudisCrypt.moduleCombinators : Array Lean.Name

The Module-level combinators, unfolded down to the toModules they are built from.

Equations

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

def GaudisCrypt.moduleUnfoldStep (x : Lean.Name) : Array Lean.Name

The opening step moduleApply and procApply share: unfold the declaration x, then the Module combinators, then strip the .reduces that exposes.

Equations

• GaudisCrypt.moduleUnfoldStep x = #[x] ++ GaudisCrypt.moduleCombinators ++ GaudisCrypt.reduceStripComposite

def GaudisCrypt.accessorApply (acc : Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Proves the apply_simp field of the X.f.utilities : ModuleTypeUtilities … that moduletype emits for each field — ∀ m, Module.app accessorModule m = X.f m, relating the accessor as a module (a projection .abs of ModuleExpressions) to the accessor as a Lean function (a chain of Module.fst's and Module.snd's). acc is the accessor, unfolded by name; the module needs no name, being the sibling field's value and hence already inlined in the goal.

Same shape as moduleApply: normalise both sides. Unfolding acc and the Module-level combinators leaves ModuleExpressions under .reduce; the stripping lemmas remove the inner .reduces that toModule left behind, exposing the β-redex .app (.abs proj) m.expression, and reduce_simp takes it. The two trailing steps are try: for the single-field case the accessor is the identity, the first simp only already closes the goal, and a bare reduce_simp would then fail with "no goals".

A TacticM function rather than a syntax/macro_rules pair, so it adds nothing to the tactic grammar, and no tactic quotation either: every lemma it names is a ``-literal, checked when this file compiles. moduletype's elaborator passes the accessor's Name and invokes it with run_tac.

Equations

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

def GaudisCrypt.accessorExpression (acc : Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Proves the expression_eq field of X.f.utilities — ∀ m, (X.f m).expression = (proj m.expression).reduce, the accessor read at the level of expressions. acc is the accessor.

No normalisation here, only unfolding: Module.fst'/snd' are toModules of the projection, and each of them leaves a .reduce inside the next, which the two stripping lemmas pull out until what is left is one .reduce of the whole chain — the right-hand side. Module.reduce_expression is for the single-field case, where the chain is empty and the two sides differ by exactly the outermost .reduce.

A TacticM function, like accessorApply, and reached the same way — moduletype's elaborator passes the accessor's Name and invokes it with run_tac. No tactic quotation: the script is intro _ followed by one simp only, both spelled against the Meta API, so every lemma it names is checked when this file compiles.

Equations

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

def Lean.Parser.Category.moduletypeField : Category

A field f : Module T of a moduletype declaration.

Equations

• Lean.Parser.Category.moduletypeField = { }

def moduletypeField.quot : Lean.ParserDescr

Equations

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

def «moduletypeFieldModule_:_;» : Lean.ParserDescr

Equations

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

def «moduletypeFieldProc_(_)→->_;» : Lean.ParserDescr

Equations

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

def «commandModuletype___{_}» : Lean.ParserDescr

moduletype Name { module f₁ : T₁; … ; module fₙ : Tₙ } declares a record-like module type, where each Tᵢ is a ModuleTypeRep. A field may also be written proc fᵢ (A₁, …) -> R;, shorthand for module fᵢ : ModuleTypeRep.proc (procsig (A₁, …) -> R);. It expands to: Name := Module (ModuleTypeRep.prod T₁ (… Tₙ)) (right-nested product of the field types), a record Name.Structure with fields fᵢ : Module Tᵢ — written Module.Proc sig for a proc field, so that the record and the procedures a module declaration puts into it are stated in the same terms, which is what lets simp chain X.apply_simp into X.f.apply_simp — accessors Name.fᵢ (via Module.fst'/Module.snd'), a constructor Name.mk, a destructor Name.structure, and three kinds of @[simp] lemma: Name.fᵢ.mk_simp (Name.fᵢ (Name.mk r) = r.fᵢ — the one that carries an X.apply_simp's right-hand side on to the field the caller asked for) and the two round-trips Name.mk_destruct / Name.destruct_mk.

What is derivable about an accessor goes into a single Name.fᵢ.utilities : ModuleTypeUtilities … per field — the accessor as a module (a projection is a module morphism), Name.fᵢ.utilities.accessorModule : Name →ₘ Tᵢ, plus …utilities.apply_simp (Module.app …accessorModule m = Name.fᵢ m) and …utilities.expression_eq (the accessor at the level of expressions: (Name.fᵢ m).expression = (proj m.expression).reduce). Bundling them keeps one name per field in the namespace instead of one per fact.

A proc field may name its arguments — proc commit (h : Value, m : Message) -> Bool; — which a ProcedureSignature cannot record, holding only their types. When every argument of a field has a name, the names are put on that field's accessor in the @[gaudiProcParamNames] attribute (and into its docstring, printing having nowhere to show them), so that notation about Name.fᵢ can bind the parameters by name even for an abstract module of this type — which has no procedure body to read names off. Naming only some arguments of a field records nothing and warns.

Name may take ordinary Lean parameters, written as for a def: moduletype Sized (n : Nat) { proc f (Fin n) -> Bool; }. Every declaration above is then abstracted over them and refers to its siblings with them applied (see the section on Lean parameters).

Everything it declares is reported by logDeclared.

Equations

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

Module definitions — module X … using (…) : T { proc f (…) : R { … }; … }

module X using (A : Module.Arr TestModule (procmod () → Unit), B : TestModule) : M2 {
  proc g () : Unit {
    _ <- call (Module.app A myMod) ();
    _ <- call (myMod.main) ("hello", 5);
    return ();
  };
  proc h () : Unit { return (); };
}

declares a module X with module parameters A, B (the using clause is optional) whose fields are the procedures g, h. Procedure bodies use the ordinary statement syntax, except that the callee of a call is a module (Module.Proc sig) rather than a bare Procedure sig.

Between the name and using come ordinary Lean parameters, as for a def — module Twice (n : Nat) using (S : CommitmentScheme) { … }. Every declaration listed below is abstracted over them and refers to its siblings with them applied; see the section on Lean parameters. They are a different thing from the module parameters, which is why the latter now need using to introduce them: a module parameter list is almost a Lean binder list, and one that happens to be exactly a Lean binder list — a single (S : CommitmentScheme) — would otherwise be read as either at the parser's whim. Written without using, that is now a Lean parameter, with a warning (linter.gaudisCrypt.using) saying so.

Elaboration is in two passes. First the whole body of each procedure is type-checked as written — with the module parameters in the local context and every callee in place (each callee that mentions a parameter ascribed to Module (.proc ?sig)). Only then, from the signatures that this typing assigns to those ?sig, is each procedure emitted as a constant X.<f>.procedure : ProcedureWithHoles …, in which

• a call whose callee mentions a module parameter has become a hole (the callee, having done its job for typing, is dropped). Two calls with the same callee syntax share one hole. The hole is named after that callee, S.gen giving the hole S_gen, so that a printed procedure still says which call each of its holes stands for;
• every other callee is a closed module expression, converted with Module.Proc.procedure.

A procedure's parameter names are recorded in @[gaudiProcParamNames] on both X.<f>.procedure and X.<f>, as moduletype does for a named proc field — the names are in the source but not in the ProcedureSignature, which holds only their types.

Each procedure also gets a module X.<f>. When it uses no module parameter that is simply Module.proc X.<f>.procedure. Otherwise it is curried over the parameters it does use, in declaration order — X.<f> : Module.Arr T₁ (… (Module.Arr Tₖ (Module.Proc sig))) — as Module.procWithHoles X.<f>.procedure applied to the tuple of its callees, under k .abs binders. The callees are read back from their elaborated form for this: each is either closed (then it is used as it stands) or built from the parameters with Module.app/fst/snd/pair, possibly after unfolding — a callee that is anything else has no ModuleExpression counterpart and is rejected.

Finally X itself is the record of those procedures (a right-nested .pair, as moduletype nests its fields), abstracted over all the parameters — used or not — which it takes as one right-nested tuple: X : Module.Arr (Module.Prod T₁ (… Tₙ)) M, where M is the module type written after the :, or Module.Prod (Module.Proc sig₁) (… (Module.Proc sigₙ)) — the anonymous record of the procedures' own types — when there is none. With an empty parameter list that tuple is Module.Unit; with no parameter list at all X is not a function but an M.

A declaration with a parameter list also gets the @[simp] lemma X.apply_simp for applying X: Module.app X (Module.pair A (… Z)) = M.mk { f₁ := Module.app X.f₁ A, … }, i.e. the record of the procedures, each applied to the parameters it uses (Module.pair in place of M.mk when M is not a moduletype name). So the two ways of instantiating a module — applying the record X or applying the individual X.f — agree, by simp.

Every procedure gets one of its own, X.<f>.apply_simp, which carries the application all the way down to a procedure: Module.app (… (Module.app X.f A) …) Z = Module.proc (X.f.procedure.instantiate …), the holes filled by the callees they were made from (each of them as written, with the arguments in place of the module parameters). A procedure with no holes uses no parameter either, and the lemma is then just X.f = Module.proc X.f.procedure.

The last step — getting rid of the instantiate — is X.<f>.procedure.apply_simp, the one lemma of the batch that is not @[simp]:

theorem X.f.procedure.apply_simp (args : ‹hole context›.Instantiation) :
    X.f.procedure.instantiate args = proc (x : T, …) : R { … }

whose right-hand side is the procedure as it was declared, only with each hole call written back as an ordinary call args ‹the hole's index› (so the callees of the body appear as args.lookup HoleIndex.zero, args.lookup HoleIndex.zero.succ, …, the first-declared hole being .zero). After X.<f>.apply_simp — and with HoleSigs.Instantiation.lookup_zero/_succ to look the indices up — naming it takes an application of X all the way to a hole-free Procedure.

It is left out of the simp set on purpose. Its right-hand side is the whole procedure body, so as a @[simp] lemma it turns every goal that so much as mentions an instantiated procedure into that body; inlining a procedure is a step to ask for by name. The @[simp] lemmas above it stop exactly at Module.proc (X.<f>.procedure.instantiate …).

def gaudi_module_proc.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.gaudi_module_proc : Category

One procedure of a module declaration: proc f (x : T, …) : R { … };. Same shape as the proc term syntax (which it expands to), plus a name and a trailing ;.

Equations

• Lean.Parser.Category.gaudi_module_proc = { }

def «gaudi_module_procProc_(_):_{Var_;_Return_;};» : Lean.ParserDescr

Equations

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

def «commandModule____Using(_):_{_}» : Lean.ParserDescr

Equations

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

def GaudisCrypt.moduleApply (x : Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Proves Module.app X (Module.pair A (… Z)) = <record of the procedures of X, applied to the parameters each of them uses> for the module X of a module X (…) { … } declaration — the X.apply_simp lemma the command emits (ModuleDecl.elabApplySimp). X must be given as its name, which the script unfolds.

Both sides are .reduces of concrete expressions, so this is a normalisation proof: unfold both sides down to ModuleExpressions, normalise, compare.

• the first simp only unfolds — X itself, then the Module-level combinators, down to the toModules they are built from. The four reduce_app_left/_right/reduce_pair_left/_right (and the fst/snd variants) strip the .reduces those toModules leave behind inside a composite expression, which is what exposes the β-redex .app (.abs body) (.pair …) to the next step;
• reduce_simp then normalises: β, the substitution it produces, and the projections .fst/.snd of the argument tuple that the substitution puts in place;
• the last simp only finishes at the Module level, where reduce_simp cannot reach: Module.substituteSimultaneously_expression (a procedure's own expression is closed, so the substitution passes through it) and Module.reduce_expression (a module's expression is already normal) — Module is defined after reduce_simp in Modules.lean, so its simp set can't know either. The stripping lemmas run once more, to put the .reduces that surface here in the same places on both sides.

A TacticM function, not a syntax/macro_rules pair, so it adds nothing to the tactic grammar, and no tactic quotation either. X comes in as a Name, since the only caller is elabApplySimp, which reaches this through run_tac.

Equations

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

def GaudisCrypt.moduleCallee : Lean.Elab.Tactic.TacticM Unit

Discharges one component of the callee tuple in procApply: c.reduce = m.expression, where c is the adapter expression the module command derived from the call site and m the callee module itself.

Both sides are the same term up to reduces sitting at inner positions, and reduce ∘ reduce = reduce is propositional, not definitional — so rfl only works when the adapter is trivial:

• callee a bare module parameter (c = B.expression): Module.reduce_expression;
• callee a field of a module parameter (c = S.expression.snd.snd): the accessor S.verify is a chain of Module.fst'/Module.snd', each of which wraps its argument in a toModule, i.e. in a reduce. Unfolding the accessor — hence the module_accessor simp set, since its name is not known here — and pushing those reduces out with reduce_fst_inner/reduce_snd_inner makes the two sides equal.

A TacticM function, not a syntax/macro_rules pair. Its only caller is procApply, which is one too and so can call it directly — no tactic keyword is needed for the two to compose.

rfl stays a quotation, and is the one step here that does. It is not a single tactic but three macro_rules alternatives in core (exact HEq.rfl, eq_refl, apply_rfl, tried in that order), so spelling it out by hand would freeze a copy of that chain that core could later grow past. It also names no lemma of ours, so writing it out would buy none of the compile-time checking that is the point of the rest.

Equations

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

def GaudisCrypt.procApply (x : Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Proves Module.app (… (Module.app X.f A₁) …) Aₖ = Module.proc (X.f.procedure.instantiate …) for one procedure f of a module X (…) { … } declaration — the X.f.apply_simp lemma the command emits (ModuleDecl.elabProcApplySimp). X.f must be given as its name, which the script unfolds.

Like moduleApply this is a normalisation proof, but it ends at the δ-rule rather than at a record: X.f is Module.procWithHoles X.f.procedure applied to the tuple of its callees, under one .abs per parameter it uses.

• the first simp only unfolds X.f and the Module-level combinators down to toModules, the stripping lemmas removing the .reduces those leave inside a composite expression (as in moduleApply);
• the loop then alternates reduce_simp with the Module-level rewrites it cannot do itself: β-reducing one parameter at a time leaves both a substitution and a rename (from liftSubst, going under the next binder) sitting on the argument's expression, and only Module.substituteSimultaneously_expression/Module.rename_expression — a module's expression being closed — get them out of the way so that the next redex becomes visible. Module is defined after reduce_simp in Modules.lean, hence the alternation;
• what is left is reduce (.app (Module.procWithHoles p).expression <tuple of callees>), which Module.reduce_app_procWithHoles turns into the instantiated procedure once its side goal — the tuple reduces to the instantiation's own tuple — is discharged. That side goal carries a written-out instantiation, so HoleSigs.Instantiation.toModuleExpr computes on it and both sides become plain expression tuples; Module.reduce_pair_of then peels them component by component, each component discharged by moduleCallee (after Module.procedure_spec turns the .proc node back into the callee's expression). Peeling at the expression level keeps HoleSigs.Instantiation out of the unification problem, which matters because it does not reduce while its hole context is a metavariable.

A TacticM function, not a syntax/macro_rules pair, so it adds nothing to the tactic grammar; X.f comes in as a Name, since the only caller is elabProcApplySimp, which reaches this through run_tac.

exact, refine and rw are the steps that stay quotations, for the reason rfl does in moduleCallee: reproducing them means reproducing elaboration against an expected type, postponed synthetic holes, and rw's motive — where a hand-written copy can silently drift from the tactic. What does not stay syntax is any name of ours: every lemma below is spliced in from a ``-literal, so a rename is an error here rather than a proof that stops working downstream. The _/?_ placeholders and the dot-notation (.unit, .proc) have to stay in the quotation, as they are resolved from the expected type.

Equations

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

Keeping the generated @[simp] lemmas findable

A generated lemma is stated over the declaration's Lean parameters — ∀ (types : CommitmentTypes), Module.app (X.main types) S = … — and simp files it under a discrimination key computed from its left-hand side at reducible transparency. The key therefore contains, at the type arguments of Module.app and friends, the field types as the abstract parameter spells them (ProcedureSignature.mk [types.Message] Bool). A caller who instantiates that parameter with a @[reducible] definition — as Pedersen.lean does, deliberately, with @[reducible] def PedersenGroup.types — gives simp a goal whose key has those same positions already reduced (ProcedureSignature.mk [group.F] Bool). Different key, so the lemma is never retrieved and silently does not fire, and the caller is pushed back to rw.

The fix is no_index, which tells the discrimination tree to index a subterm as a wildcard. The type arguments carry no information that is not already in the head of the function argument (X.main), so blanking them costs no selectivity and makes the lemma fire at every instantiation. The helpers below are the only places these applications are written, so every generated lemma gets it — the module-type arguments of Module.app/Module.pair and the hole/signature arguments of ProcedureWithHoles.instantiate.

no_index is a reducible identity, so what it changes is the index and nothing else: the lemma states the same proposition it did before.

def GaudisCrypt.ModuleDecl.appR (f x : Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

Module.app f x, with the two module types kept out of simp's discrimination key.

Equations

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

def GaudisCrypt.ModuleDecl.pairR (a b : Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

Module.pair a b, with the two module types kept out of simp's discrimination key.

Equations

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

def GaudisCrypt.ModuleDecl.instantiateR (p args : Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

p.instantiate args, with the hole signatures and the procedure signature kept out of simp's discrimination key.

Equations

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

def GaudisCrypt.ModuleDecl.holeIdent (i : ℕ) : Lean.Ident

The positional name of the i-th generated hole. Only a fallback: a hole is normally named after the callee it stands for, see holeIdentsOfCallees.

Equations

• GaudisCrypt.ModuleDecl.holeIdent i = Lean.mkIdent (Lean.Name.mkSimple (toString "_hole" ++ toString i))

def GaudisCrypt.ModuleDecl.holeCallee (i : ℕ) : Lean.Term

holeIdent in callee position. Used for the first, throw-away rewriting pass, the one that only collects the callees — the names the holes end up with are made from those.

Equations

• GaudisCrypt.ModuleDecl.holeCallee i = { raw := (GaudisCrypt.ModuleDecl.holeIdent i).raw }

partial def GaudisCrypt.ModuleDecl.unparen (s : Lean.Syntax) : Lean.Syntax

Strip the redundant parentheses a callee is usually written with ((S.gen)). A tuple and a type ascription have kinds of their own, so only real parentheses are stripped.

def GaudisCrypt.ModuleDecl.holeNameOfCallee? (callee : Lean.Term) : Option Lean.Name

The name a hole takes from the callee it was made from: that callee's own name with the dots turned into underscores, S.gen ↦ S_gen. none for a callee that is not a plain identifier (an applied one, say), which then falls back to holeIdent.

Equations

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

def GaudisCrypt.ModuleDecl.holeIdentsOfCallees (used : Array Lean.Name) (callees : Array Lean.Term) : Array Lean.Ident

Names for the holes made from callees, in hole order. A hole is named after its callee, and the name is kept clear of used (the binders already in scope where the hole will be) and of the other holes' names by appending 2, 3, … — two calls of B.bind on different parameters give B_bind and B_bind2.

Equations

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

def GaudisCrypt.ModuleDecl.binderNames (b : Lean.TSyntax `proc_binder) : Array Lean.Ident

The names a proc_binder declares (x y : T declares two).

Equations

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

partial def GaudisCrypt.ModuleDecl.sameSyntax : Lean.Syntax → Lean.Syntax → Bool

Syntactic equality ignoring source positions — two calls of the same module argument should share a single hole.

partial def GaudisCrypt.ModuleDecl.rewriteCalls (params : List Lean.Name) (mkCallee : ℕ → Lean.Term) (s : Lean.Syntax) : StateM (Array Lean.Term) Lean.Syntax

Rewrite the calls of a module body (recursing through the whole statement tree). A callee that mentions a module parameter is replaced by mkCallee i for its (deduplicated) hole number i, and the state accumulates those callees in hole order. Any other callee is a Module.Proc, so Module.Proc.procedure extracts the procedure the call statement expects.

Two runs with the same params produce the same hole numbering, which is what lets the type-checking pass and the final pass agree on it.

def GaudisCrypt.ModuleDecl.sigHole (i : ℕ) : Lean.Term

The named metavariable ?_holeSigᵢ standing for the signature of the i-th hole: it is solved by elaborating the body with the real callees in place, and read back afterwards.

Equations

• GaudisCrypt.ModuleDecl.sigHole i = { raw := (Lean.mkNode `Lean.Parser.Term.syntheticHole #[Lean.mkAtom "?", (Lean.mkIdent (GaudisCrypt.ModuleDecl.sigHole.sigName i)).raw]).raw }

def GaudisCrypt.ModuleDecl.sigHole.sigName (i : ℕ) : Lean.Name

Equations

• GaudisCrypt.ModuleDecl.sigHole.sigName i = Lean.Name.mkSimple (toString "_holeSig" ++ toString i)

def GaudisCrypt.ModuleDecl.withParams {α : Type} : List (Lean.Ident × Lean.Term) → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α

Bring the module parameters into the local context (with their declared types) so that a callee mentioning them can be elaborated. The continuation gets their free variables, in declaration order.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.ModuleDecl.withParams [] x✝ = x✝ #[]

partial def GaudisCrypt.ModuleDecl.listLit? (e : Lean.Expr) : Lean.MetaM (Option (List Lean.Expr))

Read a List literal off an Expr.

def GaudisCrypt.ModuleDecl.errorCount (msgs : Lean.MessageLog) : ℕ

How many errors a message log holds (used to tell whether the type-checking pass failed).

Equations

• GaudisCrypt.ModuleDecl.errorCount msgs = List.countP (fun (x : Lean.Message) => x.severity == Lean.MessageSeverity.error) msgs.toList

def GaudisCrypt.ModuleDecl.sigSyntax (callee : Lean.Term) (sigMVar : Lean.Expr) : Lean.Elab.TermElabM (Array Lean.Term × Lean.Term)

Split a solved ?_holeSigᵢ into the syntax of its parameter types and its return type (for the uses clause of the generated proc).

Equations

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

def GaudisCrypt.ModuleDecl.paramName (i : ℕ) : Lean.Name

The name of the placeholder standing for the module parameter declared at position i inside a callee's ModuleExpression.

Equations

• GaudisCrypt.ModuleDecl.paramName i = Lean.Name.mkSimple (toString "_param" ++ toString i)

def GaudisCrypt.ModuleDecl.paramPlaceholder (i : ℕ) : Lean.Term

The placeholder for the i-th module parameter. A callee is read back with these in place of the parameters, because the two consumers need different things there: X.<f> substitutes a de Bruijn .var (it is curried over the parameters it uses), X a projection of its single argument tuple.

Equations

• GaudisCrypt.ModuleDecl.paramPlaceholder i = { raw := (Lean.mkIdent (GaudisCrypt.ModuleDecl.paramName i)).raw }

partial def GaudisCrypt.ModuleDecl.substParams (subst : Array Lean.Term) (s : Lean.Syntax) : Lean.Syntax

Replace the parameter placeholders of s: the one for position i by subst[i].

partial def GaudisCrypt.ModuleDecl.toModuleExpr (params : List (Lean.FVarId × ℕ)) (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Term

Translate a module-valued term into ModuleExpression syntax, with the module parameters (given as params, each with the position at which it was declared) becoming paramPlaceholders.

A subterm mentioning no parameter is closed, so it is emitted as Module.expression ‹subterm›. Otherwise the head has to be one of the module operations handled below; anything else is unfolded and retried, and if that gets stuck the term is rejected. (Rejecting is the only option: a Lean function T → Module _ cannot in general be reflected into a .abs.)

def GaudisCrypt.ModuleDecl.procSig (P : LeanParams) (procRef : Lean.Term) : Lean.Elab.TermElabM Lean.Term

The signature of an already-declared procedure, as syntax (procsig (…) -> …). Used for the type of the generated module, where ProcedureWithHoles.signature p would work too but would show up unevaluated in every hover.

Equations

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

def GaudisCrypt.ModuleDecl.checkBody (P : LeanParams) (paramBs : List (Lean.Ident × Lean.Term)) (callees : Array Lean.Term) (body : Lean.Term) : Lean.Elab.TermElabM (Array (Array Lean.Term × Lean.Term) × Array Lean.Term)

Type-check a procedure body with the module parameters in the local context and the real callees in place (each hole callee ascribed to Module (.proc ?_holeSigᵢ)), and return, for each hole, the signature that this elaboration assigns to its ?_holeSigᵢ together with the callee read back as a ModuleExpression over the parameters (which appear in it as paramPlaceholders).

Holes are made only afterwards, from these signatures — so a call is typed exactly as written before it loses its callee.

Equations

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

structure GaudisCrypt.ModuleDecl.ProcResult : Type

What elabProcedure leaves for elabProcModule to work with.

• fn : Lean.Ident

  The procedure's name as written in the declaration.

• declId : Lean.Ident

  The constant just declared: X.<f>.procedure.

• declRef : Lean.Term

  The same constant, with the Lean parameters applied — how everything else refers to it.

• usedPos : Array ℕ

  The positions (in the module's parameter list) of the parameters this procedure uses, in declaration order.

• calleeExprs : Array Lean.Term

  Its hole callees as ModuleExpressions over the module parameters (which appear in them as paramPlaceholders), in hole order.

• callees : Array Lean.Term

  The same callees as they were written — module terms, mentioning the module parameters by name, in hole order. X.<f>.apply_simp states what applying X.<f> to those parameters is, and names the callees this way (Module.Proc.procedure of each).

• instThmId : Lean.Ident

  The name of the X.<f>.procedure.apply_simp lemma declared alongside X.<f>.procedure.

• paramNames : Array Lean.Ident

  Its parameter names, as the declaration wrote them (a binder naming several parameters contributing one each). Recorded in @[gaudiProcParamNames] on both X.<f>.procedure and X.<f>.

def GaudisCrypt.ModuleDecl.elabProcedure (nm : Lean.Ident) (P : LeanParams) (paramBs : Array (Lean.Ident × Lean.Term)) (p : Lean.TSyntax `gaudi_module_proc) : Lean.Elab.Command.CommandElabM (Option ProcResult)

Declare X.<f>.procedure for one proc f (…) : R { … } of a module X (…) declaration. Returns none if the body does not type-check (the errors have then been reported already).

Equations

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

def GaudisCrypt.ModuleDecl.procApplied (r : ProcResult) (subst : Array Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

The ModuleExpression of the procedure r, with subst[i] put for the module parameter declared at position i: either the closed Module.proc X.<f>.procedure, or Module.procWithHoles X.<f>.procedure applied to the tuple of its callees. That tuple is right-nested in declaration order, matching HoleSigs.toModuleTypeRepTuple (the first-declared hole is the outermost .fst).

Equations

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

def GaudisCrypt.ModuleDecl.procModId (nm : Lean.Ident) (r : ProcResult) : Lean.Ident

The constant X.<f> that elabProcModule declares for the procedure r of module X.

Equations

• GaudisCrypt.ModuleDecl.procModId nm r = Lean.mkIdent (Lean.TSyntax.getId nm ++ Lean.TSyntax.getId r.fn)

def GaudisCrypt.ModuleDecl.elabProcModule (nm : Lean.Ident) (P : LeanParams) (paramBs : Array (Lean.Ident × Lean.Term)) (r : ProcResult) : Lean.Elab.Command.CommandElabM Lean.Ident

Declare the module X.<f> of a procedure already declared by elabProcedure: either Module.proc X.<f>.procedure (no module parameter used), or procApplied abstracted over the parameters it does use, of type Module.Arr T₁ (… (Module.Arr Tₖ (Module.Proc sig))). Returns the constant it declared.

Equations

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

def GaudisCrypt.ModuleDecl.elabProcApplySimp (nm : Lean.Ident) (P : LeanParams) (paramBs : Array (Lean.Ident × Lean.Term)) (r : ProcResult) : Lean.Elab.Command.CommandElabM Lean.Ident

Declare X.<f>.apply_simp, the @[simp] lemma that applies the procedure module X.<f> to the parameters f uses:

theorem X.f.apply_simp (A : T₁) … (Z : Tₖ) :
    Module.app (… (Module.app X.f A) …) Z
      = Module.proc (X.f.procedure.instantiate
          (Module.Proc.procedure c₁, …, Module.Proc.procedure cₙ))

— the procedure with its holes filled by the callees c₁ … they were made from, each written as it was in the body (with A … Z in place of the module parameters) and turned into a Procedure by Module.Proc.procedure. An instantiation is a tuple in declaration order, which is also index order: HoleIndex.zero is the first hole the body declared, and a one-hole instantiation is its procedure rather than a pair.

A procedure with no holes uses no parameter either (a hole is exactly a call to a callee mentioning one), and X.<f> is then Module.proc X.<f>.procedure by definition — the lemma says just that.

Proved by procApply.

Equations

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

def GaudisCrypt.ModuleDecl.rightNest (f : Lean.Term → Lean.Term → Lean.Elab.Command.CommandElabM Lean.Term) (xs : Array Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

f x₁ (f x₂ (… xₙ)) — every tuple built here is right-nested, and a one-element one is just its element (as in moduletype, whose product of n field types has n-1 .prods). xs must not be empty.

Equations

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

def GaudisCrypt.ModuleDecl.moduletypeMk? (mt? : Option Lean.Term) (fns : Array Lean.Name) : Lean.Elab.Command.CommandElabM (Option Lean.Term)

If the declared module type is one introduced by moduletype whose fields are exactly the procedures declared here (same names, order immaterial), its constructor N.mk; none otherwise. N.mk takes the record N.Structure, so the module can then be written N.mk { f₁ := …, fₙ := … } rather than as a nest of Module.pairs.

The declared type may be applied to Lean parameters of its own — : (Sized n) for a moduletype Sized (n : Nat) — and the constructor is then applied to the same arguments, Sized.mk n. That works positionally because the command gives N and N.mk the very same binders, so an argument list that fits the type fits the constructor: Sized n ⟹ Sized.mk n, and a Poly whose parameters are all implicit stays bare at both.

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.ModuleDecl.moduletypeMk? mt? fns = pure none

def GaudisCrypt.ModuleDecl.mkRecord (mk? : Option Lean.Term) (procs : Array ProcResult) (fields : Array Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

The record whose field i is fields[i]: N.mk { f₁ := …, fₙ := … } when mk? is the constructor of a moduletype with exactly these fields (see moduletypeMk?), and the right-nested Module.pair of them — which is the same record, only anonymous — otherwise.

Equations

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

def GaudisCrypt.ModuleDecl.elabApplySimp (nm : Lean.Ident) (P : LeanParams) (paramBs : Array (Lean.Ident × Lean.Term)) (mkId? : Option Lean.Term) (procs : Array ProcResult) : Lean.Elab.Command.CommandElabM Lean.Ident

Declare X.apply_simp, the @[simp] lemma that applies X to its parameters:

theorem X.apply_simp (A : T₁) … (Z : Tₙ) :
    Module.app X (Module.pair A (… Z)) = N.mk { f₁ := Module.app X.f₁ A, … }

— the record of the procedures, each applied to the parameters it uses (Module.pair in place of N.mk when the module type is not a moduletype name, as in mkRecord). For an empty parameter list the tuple is the only argument X can take, a variable of Module.Unit.

Proved by moduleApply, which normalises both sides.

Equations

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

def GaudisCrypt.ModuleDecl.elabModule (nm : Lean.Ident) (P : LeanParams) (params? : Option (Array (Lean.Ident × Lean.Term))) (mt? : Option Lean.Term) (procs : Array ProcResult) : Lean.Elab.Command.CommandElabM (Array DeclInfo)

Declare the module X itself: the record of its procedures (a right-nested .pair, as moduletype nests its fields) — each of them the constant X.<f> declared by elabProcModule, applied to the parameters that f uses — abstracted over all the parameters at once, used or not, which it takes as one right-nested tuple. So X : Module.Arr (Module.Prod T₁ (… Tₙ)) M, with M the declared module type, degenerating to Module.Arr Module.Unit M for an empty parameter list and to plain M when the declaration has no parameter list at all.

A declaration without a module type gets the record of the procedures' own types for M, i.e. Module.Prod (Module.Proc sig₁) (… (Module.Proc sigₙ)) — which is what a moduletype of these procedures unfolds to anyway, only anonymous.

With no parameter list there is no .abs, and no procedure can call a parameter either, so the whole thing stays at the Module level: X is then Module.pair X.f₁ (… X.fₙ), with no detour through ModuleExpression and toModule — and when the declared module type is a moduletype name N with exactly these fields, the named form N.mk { f₁ := X.f₁, … } instead.

With a parameter list X also gets the @[simp] lemma X.apply_simp for applying it to one (see elabApplySimp).

Declares nothing (and returns #[]) if the declaration has no procedures. The result lists what was declared, for logDeclared.

Equations

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