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 (Nat, 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);. 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 round-trip @[simp] lemmas relating them.

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.)

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. logDeclared is the shared way of telling the user what they were: an info message listing every generated name as a link that inserts #check <name> after the command. It lives here, ahead of both commands, because moduletype (below) is the first user.

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 (Lean.Name × String)) : Lean.Elab.Command.CommandElabM Unit

Report the declarations a module/moduletype command generated, as

Defined:
  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). declared pairs each name with a short description of what it is.

Equations

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

def tacticAccessor_apply_ : Lean.ParserDescr

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 module_apply: 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".

Equations

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

def tacticAccessor_expression_ : Lean.ParserDescr

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.

Equations

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

def moduletypeField.quot : Lean.ParserDescr

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 «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 the two round-trip @[simp] lemmas 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.

Everything it declares is reported by logDeclared.

Equations

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

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

module X (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 parameter list 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.

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;
• every other callee is a closed module expression, converted with Module.procedure.

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, also @[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 HoleIndex.zero, args HoleIndex.zero.succ, …, the last-declared hole being .zero). After X.<f>.apply_simp — and with HoleSigs.Instantiation.push_zero/_succ to look the indices up — simp takes an application of X all the way to a hole-free Procedure.

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_proc.quot : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

def tacticModule_apply_ : Lean.ParserDescr

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.

Equations

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

def tacticModule_callee : Lean.ParserDescr

Discharges one component of the callee tuple in proc_apply: 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.

Equations

• tacticModule_callee = Lean.ParserDescr.node `tacticModule_callee 1024 (Lean.ParserDescr.nonReservedSymbol "module_callee" false)

def tacticProc_apply_ : Lean.ParserDescr

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 module_apply 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 module_apply);
• 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 peeled off component by component with Module.reduce_tuple_cons, each component being discharged by module_callee.

Equations

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

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

The name of the i-th generated hole (both the uses binder and its call sites).

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.

Equations

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

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

Does s mention one of the identifiers names (the module's parameters)? A parameter also counts as mentioned when it heads a field access (B.main is one identifier, not two).

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.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 (procId : Lean.Ident) : 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 (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.

• 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.procedure of each).

• instThmId : Lean.Ident

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

def GaudisCrypt.ModuleDecl.elabProcedure (nm : Lean.Ident) (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 and reversed, matching HoleSigs.toModuleTypeRepTuple (the last-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) (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) (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
          (HoleSigs.Instantiation.nil.push (Module.procedure c₁) |>.push … ))

— 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.procedure. Pushed in hole order, so the last declared hole ends up at HoleIndex.zero, which is how HoleSigs.Instantiation.toModuleExpr reads a tuple back.

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 the proc_apply tactic.

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.Ident)

If the declared module type is a name 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.

Equations

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

def GaudisCrypt.ModuleDecl.mkRecord (mkId? : Option Lean.Ident) (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 mkId? 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) (paramBs : Array (Lean.Ident × Lean.Term)) (mkId? : Option Lean.Ident) (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 the module_apply tactic, which normalises both sides.

Equations

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

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

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.