Tests for Inline.lean

One command per pass, so a failure localizes. Every command checks the proof it gets (Meta.check, and that it proves the expected statement about the input), and every command that prints surface syntax also re-parses what it printed (ProgTest.roundtrip). #flattenCall prints the uncleaned output of Flatten.flattenCall — full of applyLens and chain*; its shape is determined by the input's shape, with no simp set in the loop.

def GaudisCrypt.InlineTest.elabInput (t : Lean.Term) : Lean.Elab.TermElabM Lean.Expr

Elaborate a test's input term.

Equations

• GaudisCrypt.InlineTest.elabInput t = do let e ← Lean.Elab.Term.elabTerm t.raw none Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing Lean.instantiateMVars e

def GaudisCrypt.InlineTest.checkStep (input : Lean.Expr) (step : Flatten.FlattenStep) : Lean.MetaM Unit

Check that step.proof proves input.EquivInLens step.stmt step.trafo.

Equations

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

def GaudisCrypt.InlineTest.checkProc (p p' proof : Lean.Expr) : Lean.MetaM Unit

Check that proof proves procedureDenotation p' = procedureDenotation p.

Equations

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

def GaudisCrypt.InlineTest.«command#flattenCall_In_» : Lean.ParserDescr

Flatten call n of a statement, uncleaned.

Equations

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

def GaudisCrypt.InlineTest.«command#flattenCallCleaned_In_» : Lean.ParserDescr

Flatten call n of a statement, cleaned.

Equations

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

def GaudisCrypt.InlineTest.«command#flatten_» : Lean.ParserDescr

The whole pass on a statement.

Equations

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

def GaudisCrypt.InlineTest.«command#flattenProc_» : Lean.ParserDescr

The whole pass on a procedure.

Equations

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

def GaudisCrypt.InlineTest.«command#flattenSeq_» : Lean.ParserDescr

flattenSeq alone.

Equations

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

def GaudisCrypt.InlineTest.«command#unfoldProc_» : Lean.ParserDescr

Unfold a module term to the procedure it denotes.

Equations

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

def GaudisCrypt.InlineTest.«command#inlineRaw_In_» : Lean.ParserDescr

Unfold the callee of one call site.

Equations

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

def GaudisCrypt.InlineTest.«command#inline_In_» : Lean.ParserDescr

Unfold the callee of one call site, then flatten it.

Equations

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

def GaudisCrypt.InlineTest.«command#inlineProc_In_» : Lean.ParserDescr

Inline one call site of a procedure.

Equations

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

A first end-to-end case

noncomputable def GaudisCrypt.InlineTest.caller : proctype () → ℕ

The callee is spelled out at the call site: only literal callees are flattened.

Equations

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

More cases

noncomputable def GaudisCrypt.InlineTest.twoCalls : proctype () → ℕ

Two calls in one body, and a name collision: both callees call their local w, and so does the caller. The caller's w keeps its name; the callees' are renamed.

Equations

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

noncomputable def GaudisCrypt.InlineTest.nested : proctype () → ℕ

A callee that itself calls: the fixed point needs two rounds.

Equations

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

noncomputable def GaudisCrypt.InlineTest.branching : proctype (Bool) → ℕ

A call inside if and one inside while: the guards travel along the lens, and the callee's frame is reset on every iteration.

Equations

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

noncomputable def GaudisCrypt.InlineTest.twoParams : proctype () → ℕ

Several parameters (a tuple assignment), and a callee with no variables but its parameters.

Equations

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

noncomputable def GaudisCrypt.InlineTest.degenerate : proctype (ℕ) → ℕ

A callee with no parameters and no variables.

Equations

• GaudisCrypt.InlineTest.degenerate = proc (p : ℕ) : ℕ { var r : ℕ; r <- call (proc () : ℕ { skip; return 42 }) (); return §r + §p }

noncomputable def GaudisCrypt.InlineTest.unusedParam : proctype (ℕ) → ℕ

A callee whose variable has the name of a parameter of the caller that the body never mentions: the parameter keeps its name (the entry state has to stay the same), the callee's variable is renamed.

Equations

• GaudisCrypt.InlineTest.unusedParam = proc (q : ℕ) : ℕ { var r : ℕ; r <- call (proc (q : ℕ) : ℕ { skip; return §q + 1 }) (Nat.succ 0); return §r }

flattenSeq on its own

Nested blocks and skips, with no call anywhere: the spine is re-associated to the right and the skips disappear, and the proof is a chain of seq_assoc/skip_seq/seq_skip.

noncomputable def GaudisCrypt.InlineTest.blocky : proctype () → ℕ

Equations

• GaudisCrypt.InlineTest.blocky = proc () : ℕ { var x : ℕ; x <- 1; { skip; x <- 2; x <- 3; skip; } x <- 4; return §x }

What is left alone

A callee that is not spelled out at the call site stays a call, and a statement with no flattenable call at all is an error.

noncomputable def GaudisCrypt.InlineTest.opaqueCallee : proctype (ℕ) → ℕ

Called through a name, so it is not flattened: the callee is not literal.

Equations

• GaudisCrypt.InlineTest.opaqueCallee = proc (z : ℕ) : ℕ { var t : ℕ; t <- §z + 1; return §t }

noncomputable def GaudisCrypt.InlineTest.callsOpaque : proctype () → ℕ

Equations

• GaudisCrypt.InlineTest.callsOpaque = proc () : ℕ { var x : ℕ; x <- 1; x <- call GaudisCrypt.InlineTest.opaqueCallee (§x); return §x }

noncomputable def GaudisCrypt.InlineTest.callFree : proctype () → ℕ

A statement with no call at all.

Equations

• GaudisCrypt.InlineTest.callFree = proc () : ℕ { var x : ℕ; x <- 1; return §x }

Inlining: callees named through modules

A module type with one procedure, a module over it that calls a parameter, and a module that calls nothing: the two shapes inlining evaluates, T.f ‹module expression› and M.f.

structure GaudisCrypt.InlineTest.U.Structure : Type 1

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

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

• g : procmod (ℕ) → ℕ

noncomputable def GaudisCrypt.InlineTest.U.structure : U → Structure

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

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

Equations

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

@[reducible]

noncomputable def GaudisCrypt.InlineTest.U.mk : Structure → U

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

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

Equations

• GaudisCrypt.InlineTest.U.mk theRecord✝ = theRecord✝.g

@[simp]

theorem GaudisCrypt.InlineTest.U.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

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

@[simp]

theorem GaudisCrypt.InlineTest.U.destruct_mk (theModule✝ : U) : mk theModule✝.structure = theModule✝

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

noncomputable def GaudisCrypt.InlineTest.U.g.utilities : ModuleTypeUtilities U (procmod (ℕ) → ℕ) g

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

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

Equations

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

noncomputable def GaudisCrypt.InlineTest.U.g : U → procmod (ℕ) → ℕ

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

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

Equations

• theModule✝.g = theModule✝

def GaudisCrypt.InlineTest.U.typeRep : ModuleTypeRep

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

U is by definition Module U.typeRep.

Equations

• GaudisCrypt.InlineTest.U.typeRep = GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → ℕ)

@[implicit_reducible]

instance GaudisCrypt.InlineTest.instIsModuleU : IsModule U

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

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

Equations

• GaudisCrypt.InlineTest.instIsModuleU = { moduleTypeRep := GaudisCrypt.InlineTest.U.typeRep, isModule := ⋯ }

def GaudisCrypt.InlineTest.U : Type 1

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

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

Equations

• GaudisCrypt.InlineTest.U = GaudisCrypt.Module GaudisCrypt.InlineTest.U.typeRep

@[simp]

theorem GaudisCrypt.InlineTest.U.g.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).g = theRecord✝.g

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

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

def GaudisCrypt.InlineTest.T : Type 1

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

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

Equations

• GaudisCrypt.InlineTest.T = GaudisCrypt.Module GaudisCrypt.InlineTest.T.typeRep

def GaudisCrypt.InlineTest.T.typeRep : ModuleTypeRep

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

T is by definition Module T.typeRep.

Equations

• GaudisCrypt.InlineTest.T.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → ℕ)).prod (GaudisCrypt.ModuleTypeRep.proc (procsig () → ℕ))

noncomputable def GaudisCrypt.InlineTest.T.structure : T → Structure

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

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

Equations

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

@[reducible]

noncomputable def GaudisCrypt.InlineTest.T.mk : Structure → T

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

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

Equations

• GaudisCrypt.InlineTest.T.mk theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.f theRecord✝.h

noncomputable def GaudisCrypt.InlineTest.T.f.utilities : ModuleTypeUtilities T (procmod (ℕ) → ℕ) f

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

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

Equations

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

@[simp]

theorem GaudisCrypt.InlineTest.T.destruct_mk (theModule✝ : T) : mk theModule✝.structure = theModule✝

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

noncomputable def GaudisCrypt.InlineTest.T.f : T → procmod (ℕ) → ℕ

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

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

Equations

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

noncomputable def GaudisCrypt.InlineTest.T.h : T → procmod () → ℕ

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

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

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

Equations

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

@[simp]

theorem GaudisCrypt.InlineTest.T.h.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).h = theRecord✝.h

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

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

@[simp]

theorem GaudisCrypt.InlineTest.T.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

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

@[simp]

theorem GaudisCrypt.InlineTest.T.f.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).f = theRecord✝.f

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

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

structure GaudisCrypt.InlineTest.T.Structure : Type 1

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

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

• f : procmod (ℕ) → ℕ
• h : procmod () → ℕ

noncomputable def GaudisCrypt.InlineTest.T.h.utilities : ModuleTypeUtilities T (procmod () → ℕ) h

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

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

Equations

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

@[implicit_reducible]

instance GaudisCrypt.InlineTest.instIsModuleT : IsModule T

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

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

Equations

• GaudisCrypt.InlineTest.instIsModuleT = { moduleTypeRep := GaudisCrypt.InlineTest.T.typeRep, isModule := ⋯ }

noncomputable def GaudisCrypt.InlineTest.M.f : Module.Arr U (procmod (ℕ) → ℕ)

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

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

Equations

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

theorem GaudisCrypt.InlineTest.M.f.procedure.apply_simp (holeArgs✝ : (HoleSigs.cons (procsig (ℕ) → ℕ) HoleSigs.empty).Instantiation) : procedure.instantiate holeArgs✝ = proc (x : ℕ) : ℕ { var y : ℕ; y <- call (holeArgs✝.lookup HoleIndex.zero) (§x); return §y + 1 }

Instantiating the holes of M.f.procedure with a tuple holeArgs of procedures: the body of proc f 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 [M.f.procedure.apply_simp]).

@[simp]

theorem GaudisCrypt.InlineTest.M.f.apply_simp (A : U) : Module.app f A = Module.proc (procedure.instantiate A.g.procedure)

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

noncomputable def GaudisCrypt.InlineTest.M.h : procmod () → ℕ

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

Equations

• GaudisCrypt.InlineTest.M.h = GaudisCrypt.Module.proc GaudisCrypt.InlineTest.M.h.procedure

theorem GaudisCrypt.InlineTest.M.h.procedure.apply_simp (holeArgs✝ : HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : ℕ { skip; return 5 }

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

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

@[simp]

theorem GaudisCrypt.InlineTest.M.h.apply_simp : h = Module.proc procedure

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

noncomputable def GaudisCrypt.InlineTest.M : Module.Arr U T

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

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

Equations

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

@[simp]

theorem GaudisCrypt.InlineTest.M.apply_simp (A : U) : Module.app M A = T.mk { f := Module.app f A, h := h }

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

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

noncomputable def GaudisCrypt.InlineTest.M.f.procedure : proctype (ℕ) → ℕ uses ((ℕ) → ℕ)

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

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

Equations

• GaudisCrypt.InlineTest.M.f.procedure = proc (x : ℕ) uses (A_g : (ℕ) → ℕ) : ℕ { var y : ℕ; y <- call A_g (§x); return §y + 1 }

noncomputable def GaudisCrypt.InlineTest.M.h.procedure : proctype () -> ℕ

The body of proc h of module M, 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 M.h.procedure.apply_simp) rather than run. Use M.h for this procedure as a module.

Equations

• GaudisCrypt.InlineTest.M.h.procedure = proc () : ℕ { skip; return 5 }

noncomputable def GaudisCrypt.InlineTest.N.h : procmod () → ℕ

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

Equations

• GaudisCrypt.InlineTest.N.h = GaudisCrypt.Module.proc GaudisCrypt.InlineTest.N.h.procedure

@[simp]

theorem GaudisCrypt.InlineTest.N.f.apply_simp : f = Module.proc procedure

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

theorem GaudisCrypt.InlineTest.N.h.procedure.apply_simp (holeArgs✝ : HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : ℕ { skip; return 7 }

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

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

noncomputable def GaudisCrypt.InlineTest.N.h.procedure : proctype () -> ℕ

The body of proc h of module N, 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 N.h.procedure.apply_simp) rather than run. Use N.h for this procedure as a module.

Equations

• GaudisCrypt.InlineTest.N.h.procedure = proc () : ℕ { skip; return 7 }

theorem GaudisCrypt.InlineTest.N.f.procedure.apply_simp (holeArgs✝ : HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc (x : ℕ) : ℕ { var y : ℕ; y <- §x * 2; return §y }

Instantiating the holes of N.f.procedure with a tuple holeArgs of procedures: the body of proc f 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 [N.f.procedure.apply_simp]).

noncomputable def GaudisCrypt.InlineTest.N : T

The module declared by module N: the record of its procedures N.f, N.h.

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

Equations

• GaudisCrypt.InlineTest.N = GaudisCrypt.InlineTest.T.mk { f := GaudisCrypt.InlineTest.N.f, h := GaudisCrypt.InlineTest.N.h }

noncomputable def GaudisCrypt.InlineTest.N.f : procmod (ℕ) → ℕ

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

Equations

• GaudisCrypt.InlineTest.N.f = GaudisCrypt.Module.proc GaudisCrypt.InlineTest.N.f.procedure

noncomputable def GaudisCrypt.InlineTest.N.f.procedure : proctype (ℕ) -> ℕ

The body of proc f of module N, 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 N.f.procedure.apply_simp) rather than run. Use N.f for this procedure as a module.

Equations

• GaudisCrypt.InlineTest.N.f.procedure = proc (x : ℕ) : ℕ { var y : ℕ; y <- §x * 2; return §y }

@[simp]

theorem GaudisCrypt.InlineTest.N.h.apply_simp : h = Module.proc procedure

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

noncomputable def GaudisCrypt.InlineTest.Q.f : Module.Arr U (Module.Arr U (procmod (ℕ) → ℕ))

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

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

Equations

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

@[simp]

theorem GaudisCrypt.InlineTest.Q.apply_simp (A B : U) : Module.app Q (Module.pair A B) = T.mk { f := Module.app (Module.app f A) B, h := h }

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

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

noncomputable def GaudisCrypt.InlineTest.Q.h : procmod () → ℕ

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

Equations

• GaudisCrypt.InlineTest.Q.h = GaudisCrypt.Module.proc GaudisCrypt.InlineTest.Q.h.procedure

@[simp]

theorem GaudisCrypt.InlineTest.Q.h.apply_simp : h = Module.proc procedure

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

noncomputable def GaudisCrypt.InlineTest.Q.f.procedure : proctype (ℕ) → ℕ uses ((ℕ) → ℕ, (ℕ) → ℕ)

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

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

Equations

• GaudisCrypt.InlineTest.Q.f.procedure = proc (x : ℕ) uses (A_g : (ℕ) → ℕ, B_g : (ℕ) → ℕ) : ℕ { var y : ℕ; y <- call A_g (§x); y <- call B_g (§y); return §y }

@[simp]

theorem GaudisCrypt.InlineTest.Q.f.apply_simp (A B : U) : Module.app (Module.app f A) B = Module.proc (procedure.instantiate (A.g.procedure, B.g.procedure))

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

theorem GaudisCrypt.InlineTest.Q.h.procedure.apply_simp (holeArgs✝ : HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : ℕ { skip; return 1 }

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

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

theorem GaudisCrypt.InlineTest.Q.f.procedure.apply_simp (holeArgs✝ : (HoleSigs.cons (procsig (ℕ) → ℕ) (HoleSigs.cons (procsig (ℕ) → ℕ) HoleSigs.empty)).Instantiation) : procedure.instantiate holeArgs✝ = proc (x : ℕ) : ℕ { var y : ℕ; y <- call (holeArgs✝.lookup HoleIndex.zero) (§x); y <- call (holeArgs✝.lookup HoleIndex.zero.succ) (§y); return §y }

Instantiating the holes of Q.f.procedure with a tuple holeArgs of procedures: the body of proc f 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 [Q.f.procedure.apply_simp]).

noncomputable def GaudisCrypt.InlineTest.Q : Module.Arr (Module.Prod U U) T

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

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

Equations

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

noncomputable def GaudisCrypt.InlineTest.Q.h.procedure : proctype () -> ℕ

The body of proc h of module Q, 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 Q.h.procedure.apply_simp) rather than run. Use Q.h for this procedure as a module.

Equations

• GaudisCrypt.InlineTest.Q.h.procedure = proc () : ℕ { skip; return 1 }

axiom GaudisCrypt.InlineTest.someU : U

axiom GaudisCrypt.InlineTest.otherU : U

axiom GaudisCrypt.InlineTest.absM : Module.Arr U T

noncomputable def GaudisCrypt.InlineTest.modCaller : proctype () → ℕ

A caller whose callee is named through modules: flattening cannot handle it (the callee is not spelled out at the call site), inlining can unfold it first.

Equations

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

Call sites are numbered including holes

P.f calls its module parameter first and a concrete module second, so its body has two call sites: number 0 is the hole, number 1 the call — and neither pass will renumber them.

theorem GaudisCrypt.InlineTest.P.h.procedure.apply_simp (holeArgs✝ : HoleSigs.empty.Instantiation) : procedure.instantiate holeArgs✝ = proc () : ℕ { skip; return 0 }

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

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

noncomputable def GaudisCrypt.InlineTest.P.f : Module.Arr U (procmod (ℕ) → ℕ)

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

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

Equations

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

@[simp]

theorem GaudisCrypt.InlineTest.P.apply_simp (A : U) : Module.app P A = T.mk { f := Module.app f A, h := h }

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

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

@[simp]

theorem GaudisCrypt.InlineTest.P.h.apply_simp : h = Module.proc procedure

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

theorem GaudisCrypt.InlineTest.P.f.procedure.apply_simp (holeArgs✝ : (HoleSigs.cons (procsig (ℕ) → ℕ) HoleSigs.empty).Instantiation) : procedure.instantiate holeArgs✝ = proc (x : ℕ) : ℕ { var y : ℕ, z : ℕ; y <- call (holeArgs✝.lookup HoleIndex.zero) (§x); z <- call N.f.procedure (§y); return §z }

Instantiating the holes of P.f.procedure with a tuple holeArgs of procedures: the body of proc f 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 [P.f.procedure.apply_simp]).

noncomputable def GaudisCrypt.InlineTest.P : Module.Arr U T

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

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

Equations

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

noncomputable def GaudisCrypt.InlineTest.P.f.procedure : proctype (ℕ) → ℕ uses ((ℕ) → ℕ)

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

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

Equations

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

@[simp]

theorem GaudisCrypt.InlineTest.P.f.apply_simp (A : U) : Module.app f A = Module.proc (procedure.instantiate A.g.procedure)

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

noncomputable def GaudisCrypt.InlineTest.P.h : procmod () → ℕ

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

Equations

• GaudisCrypt.InlineTest.P.h = GaudisCrypt.Module.proc GaudisCrypt.InlineTest.P.h.procedure

noncomputable def GaudisCrypt.InlineTest.P.h.procedure : proctype () -> ℕ

The body of proc h of module P, 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 P.h.procedure.apply_simp) rather than run. Use P.h for this procedure as a module.

Equations

• GaudisCrypt.InlineTest.P.h.procedure = proc () : ℕ { skip; return 0 }