Generic commitment schemes

A transliteration of EasyCrypt's theories/crypto/Commitment.ec (theory CommitmentProtocol) into the Gaudí module/procedure syntax.

• EC's abstract theory types value, message, commitment, openingkey become the fields of the structure CommitmentTypes, declared here as a section variable (types : CommitmentTypes) and hence a Lean parameter of every moduletype and module below that mentions one of them.
• EC module types become moduletypes.
• EC's parameterized modules (Correctness(S), HidingExperiment(S,U), BindingExperiment(S,B)) become module X … using (P : T) { … } declarations: the calls are written against the parameters' own fields and the holes are inferred from them.

structure GaudisCrypt.Examples.Pedersen.CommitmentTypes : Type 1

• Value : Type
• Message : Type
• Commitment : Type
• OpeningKey : Type
• value_inhabited : Inhabited self.Value
• message_inhabited : Inhabited self.Message
• commitment_inhabited : Inhabited self.Commitment
• openingKey_inhabited : Inhabited self.OpeningKey

@[reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedValue (types : CommitmentTypes) : Inhabited types.Value

Equations

• GaudisCrypt.Examples.Pedersen.instInhabitedValue types = types.value_inhabited

@[reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedMessage (types : CommitmentTypes) : Inhabited types.Message

Equations

• GaudisCrypt.Examples.Pedersen.instInhabitedMessage types = types.message_inhabited

@[reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedCommitment (types : CommitmentTypes) : Inhabited types.Commitment

Equations

• GaudisCrypt.Examples.Pedersen.instInhabitedCommitment types = types.commitment_inhabited

@[reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedOpeningKey (types : CommitmentTypes) : Inhabited types.OpeningKey

Equations

• GaudisCrypt.Examples.Pedersen.instInhabitedOpeningKey types = types.openingKey_inhabited

Module types

module type CommitmentScheme = {
  proc gen() : value
  proc commit(x: value, m: message) : commitment * openingkey
  proc verify(x: value, m: message, c: commitment, d: openingkey) : bool
}.

def GaudisCrypt.Examples.Pedersen.CommitmentScheme (types : CommitmentTypes) : Type 1

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

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

Equations

• GaudisCrypt.Examples.Pedersen.CommitmentScheme types = GaudisCrypt.Module (GaudisCrypt.Examples.Pedersen.CommitmentScheme.typeRep types)

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.commit.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : commit types (mk types theRecord✝) = theRecord✝.commit

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

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleCommitmentScheme (types : CommitmentTypes) : IsModule (CommitmentScheme types)

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

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

Equations

• GaudisCrypt.Examples.Pedersen.instIsModuleCommitmentScheme types = { moduleTypeRep := GaudisCrypt.Examples.Pedersen.CommitmentScheme.typeRep types, isModule := ⋯ }

def GaudisCrypt.Examples.Pedersen.CommitmentScheme.typeRep (types : CommitmentTypes) : ModuleTypeRep

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

CommitmentScheme is by definition Module CommitmentScheme.typeRep.

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.mk_destruct (types : CommitmentTypes) (theRecord✝ : Structure types) : «structure» types (mk types theRecord✝) = theRecord✝

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

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.mk (types : CommitmentTypes) : Structure types → CommitmentScheme types

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

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

Equations

• GaudisCrypt.Examples.Pedersen.CommitmentScheme.mk types theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.gen (GaudisCrypt.Module.pair' theRecord✝.commit theRecord✝.verify)

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.destruct_mk (types : CommitmentTypes) (theModule✝ : CommitmentScheme types) : mk types («structure» types theModule✝) = theModule✝

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

structure GaudisCrypt.Examples.Pedersen.CommitmentScheme.Structure (types : CommitmentTypes) : Type 1

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

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

• gen : procmod () → types.Value
• commit : procmod (types.Value, types.Message) → (types.Commitment × types.OpeningKey)
• verify : procmod (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.verify.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : verify types (mk types theRecord✝) = theRecord✝.verify

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

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

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.verify (types : CommitmentTypes) : CommitmentScheme types → procmod (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool

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

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

Its parameters are named x, m, c, d, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• GaudisCrypt.Examples.Pedersen.CommitmentScheme.verify types theModule✝ = (GaudisCrypt.Module.snd' theModule✝).snd'

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.verify.utilities (types : CommitmentTypes) : ModuleTypeUtilities (CommitmentScheme types) (procmod (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool) (verify types)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.commit.utilities (types : CommitmentTypes) : ModuleTypeUtilities (CommitmentScheme types) (procmod (types.Value, types.Message) → (types.Commitment × types.OpeningKey)) (commit types)

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

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.gen.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : gen types (mk types theRecord✝) = theRecord✝.gen

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

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

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.commit (types : CommitmentTypes) : CommitmentScheme types → procmod (types.Value, types.Message) → (types.Commitment × types.OpeningKey)

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

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

Its parameters are named x, m, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• GaudisCrypt.Examples.Pedersen.CommitmentScheme.commit types theModule✝ = (GaudisCrypt.Module.snd' theModule✝).fst'

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.gen.utilities (types : CommitmentTypes) : ModuleTypeUtilities (CommitmentScheme types) (procmod () → types.Value) (gen types)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.gen (types : CommitmentTypes) : CommitmentScheme types → procmod () → types.Value

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

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

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

Equations

• GaudisCrypt.Examples.Pedersen.CommitmentScheme.gen types theModule✝ = GaudisCrypt.Module.fst' theModule✝

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.structure (types : CommitmentTypes) : CommitmentScheme types → Structure types

The record of a module's fields: CommitmentScheme.structure m is CommitmentScheme.Structure.mk applied to CommitmentScheme.gen, CommitmentScheme.commit, CommitmentScheme.verify of m.

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

Equations

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

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.mk (types : CommitmentTypes) : Structure types → Unhider types

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

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

Equations

• GaudisCrypt.Examples.Pedersen.Unhider.mk types theRecord✝ = GaudisCrypt.Module.pair' theRecord✝.choose theRecord✝.guess

def GaudisCrypt.Examples.Pedersen.Unhider.typeRep (types : CommitmentTypes) : ModuleTypeRep

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

Unhider is by definition Module Unhider.typeRep.

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Unhider.mk_destruct (types : CommitmentTypes) (theRecord✝ : Structure types) : «structure» types (mk types theRecord✝) = theRecord✝

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Unhider.guess.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : guess types (mk types theRecord✝) = theRecord✝.guess

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

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Unhider.destruct_mk (types : CommitmentTypes) (theModule✝ : Unhider types) : mk types («structure» types theModule✝) = theModule✝

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

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.guess (types : CommitmentTypes) : Unhider types → procmod (types.Commitment) → Bool

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

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

Its parameters are named c, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• GaudisCrypt.Examples.Pedersen.Unhider.guess types theModule✝ = GaudisCrypt.Module.snd' theModule✝

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.choose.utilities (types : CommitmentTypes) : ModuleTypeUtilities (Unhider types) (procmod (types.Value) → (types.Message × types.Message)) (choose types)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.structure (types : CommitmentTypes) : Unhider types → Structure types

The record of a module's fields: Unhider.structure m is Unhider.Structure.mk applied to Unhider.choose, Unhider.guess of m.

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Unhider.choose.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : choose types (mk types theRecord✝) = theRecord✝.choose

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

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleUnhider (types : CommitmentTypes) : IsModule (Unhider types)

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

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

Equations

• GaudisCrypt.Examples.Pedersen.instIsModuleUnhider types = { moduleTypeRep := GaudisCrypt.Examples.Pedersen.Unhider.typeRep types, isModule := ⋯ }

structure GaudisCrypt.Examples.Pedersen.Unhider.Structure (types : CommitmentTypes) : Type 1

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

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

• choose : procmod (types.Value) → (types.Message × types.Message)
• guess : procmod (types.Commitment) → Bool

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.choose (types : CommitmentTypes) : Unhider types → procmod (types.Value) → (types.Message × types.Message)

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

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

Its parameters are named x, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• GaudisCrypt.Examples.Pedersen.Unhider.choose types theModule✝ = GaudisCrypt.Module.fst' theModule✝

def GaudisCrypt.Examples.Pedersen.Unhider (types : CommitmentTypes) : Type 1

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

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

Equations

• GaudisCrypt.Examples.Pedersen.Unhider types = GaudisCrypt.Module (GaudisCrypt.Examples.Pedersen.Unhider.typeRep types)

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.guess.utilities (types : CommitmentTypes) : ModuleTypeUtilities (Unhider types) (procmod (types.Commitment) → Bool) (guess types)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.bind (types : CommitmentTypes) : Binder types → procmod (types.Value) → (types.Commitment × types.Message × types.OpeningKey × types.Message × types.OpeningKey)

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

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

Its parameters are named x, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• GaudisCrypt.Examples.Pedersen.Binder.bind types theModule✝ = theModule✝

structure GaudisCrypt.Examples.Pedersen.Binder.Structure (types : CommitmentTypes) : Type 1

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

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

• bind : procmod (types.Value) → (types.Commitment × types.Message × types.OpeningKey × types.Message × types.OpeningKey)

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.mk (types : CommitmentTypes) : Structure types → Binder types

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

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

Equations

• GaudisCrypt.Examples.Pedersen.Binder.mk types theRecord✝ = theRecord✝.bind

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Binder.destruct_mk (types : CommitmentTypes) (theModule✝ : Binder types) : mk types («structure» types theModule✝) = theModule✝

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Binder.mk_destruct (types : CommitmentTypes) (theRecord✝ : Structure types) : «structure» types (mk types theRecord✝) = theRecord✝

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Binder.bind.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : bind types (mk types theRecord✝) = theRecord✝.bind

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

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleBinder (types : CommitmentTypes) : IsModule (Binder types)

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

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

Equations

• GaudisCrypt.Examples.Pedersen.instIsModuleBinder types = { moduleTypeRep := GaudisCrypt.Examples.Pedersen.Binder.typeRep types, isModule := ⋯ }

def GaudisCrypt.Examples.Pedersen.Binder.typeRep (types : CommitmentTypes) : ModuleTypeRep

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

Binder is by definition Module Binder.typeRep.

Equations

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

def GaudisCrypt.Examples.Pedersen.Binder (types : CommitmentTypes) : Type 1

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

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

Equations

• GaudisCrypt.Examples.Pedersen.Binder types = GaudisCrypt.Module (GaudisCrypt.Examples.Pedersen.Binder.typeRep types)

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.bind.utilities (types : CommitmentTypes) : ModuleTypeUtilities (Binder types) (procmod (types.Value) → (types.Commitment × types.Message × types.OpeningKey × types.Message × types.OpeningKey)) (bind types)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.structure (types : CommitmentTypes) : Binder types → Structure types

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

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

Equations

• GaudisCrypt.Examples.Pedersen.Binder.structure types theModule✝ = { bind := GaudisCrypt.Examples.Pedersen.Binder.bind types theModule✝ }

noncomputable def GaudisCrypt.Examples.Pedersen.CorrectnessT.structure (types : CommitmentTypes) : CorrectnessT types → Structure types

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

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

Equations

• GaudisCrypt.Examples.Pedersen.CorrectnessT.structure types theModule✝ = { main := GaudisCrypt.Examples.Pedersen.CorrectnessT.main types theModule✝ }

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CorrectnessT.destruct_mk (types : CommitmentTypes) (theModule✝ : CorrectnessT types) : mk types («structure» types theModule✝) = theModule✝

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

def GaudisCrypt.Examples.Pedersen.CorrectnessT (types : CommitmentTypes) : Type 1

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

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

Equations

• GaudisCrypt.Examples.Pedersen.CorrectnessT types = GaudisCrypt.Module (GaudisCrypt.Examples.Pedersen.CorrectnessT.typeRep types)

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CorrectnessT.mk_destruct (types : CommitmentTypes) (theRecord✝ : Structure types) : «structure» types (mk types theRecord✝) = theRecord✝

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

noncomputable def GaudisCrypt.Examples.Pedersen.CorrectnessT.main.utilities (types : CommitmentTypes) : ModuleTypeUtilities (CorrectnessT types) (procmod (types.Message) → Bool) (main types)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.CorrectnessT.main (types : CommitmentTypes) : CorrectnessT types → procmod (types.Message) → Bool

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

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

Its parameters are named m, in that order (recorded in @[gaudiProcParamNames], a ProcedureSignature holding only their types).

Equations

• GaudisCrypt.Examples.Pedersen.CorrectnessT.main types theModule✝ = theModule✝

def GaudisCrypt.Examples.Pedersen.CorrectnessT.typeRep (types : CommitmentTypes) : ModuleTypeRep

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

CorrectnessT is by definition Module CorrectnessT.typeRep.

Equations

• GaudisCrypt.Examples.Pedersen.CorrectnessT.typeRep types = GaudisCrypt.ModuleTypeRep.proc (procsig (types.Message) → Bool)

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleCorrectnessT (types : CommitmentTypes) : IsModule (CorrectnessT types)

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

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

Equations

• GaudisCrypt.Examples.Pedersen.instIsModuleCorrectnessT types = { moduleTypeRep := GaudisCrypt.Examples.Pedersen.CorrectnessT.typeRep types, isModule := ⋯ }

structure GaudisCrypt.Examples.Pedersen.CorrectnessT.Structure (types : CommitmentTypes) : Type 1

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

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

• main : procmod (types.Message) → Bool

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CorrectnessT.main.mk_simp (types : CommitmentTypes) (theRecord✝ : Structure types) : main types (mk types theRecord✝) = theRecord✝.main

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

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

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.CorrectnessT.mk (types : CommitmentTypes) : Structure types → CorrectnessT types

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

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

Equations

• GaudisCrypt.Examples.Pedersen.CorrectnessT.mk types theRecord✝ = theRecord✝.main

noncomputable def GaudisCrypt.Examples.Pedersen.Correctness.main.procedure (types : CommitmentTypes) : proctype (types.Message) → Bool uses (() → types.Value, (types.Value, types.Message) → types.Commitment × types.OpeningKey, (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool)

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

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Correctness.main.apply_simp (types : CommitmentTypes) (S : CommitmentScheme types) : Module.app (main types) S = Module.proc ((procedure types).instantiate ((CommitmentScheme.gen types S).procedure, (CommitmentScheme.commit types S).procedure, (CommitmentScheme.verify types S).procedure))

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Correctness.apply_simp (types : CommitmentTypes) (S : CommitmentScheme types) : Module.app (Correctness types) S = CorrectnessT.mk types { main := Module.app (main types) S }

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

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

noncomputable def GaudisCrypt.Examples.Pedersen.Correctness (types : CommitmentTypes) : Module.Arr (CommitmentScheme types) (CorrectnessT types)

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

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

Equations

• GaudisCrypt.Examples.Pedersen.Correctness types = ((GaudisCrypt.Examples.Pedersen.Correctness.main types).expression.app (GaudisCrypt.ModuleExpression.var 0)).abs.toModule ⋯

theorem GaudisCrypt.Examples.Pedersen.Correctness.main.procedure.apply_simp (types : CommitmentTypes) (holeArgs✝ : (HoleSigs.cons (procsig () → types.Value) (HoleSigs.cons (procsig (types.Value, types.Message) → types.Commitment × types.OpeningKey) (HoleSigs.cons (procsig (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool) HoleSigs.empty))).Instantiation) : (procedure types).instantiate holeArgs✝ = proc (m : types.Message) : Bool { var x : types.Value, c : types.Commitment, d : types.OpeningKey, b : Bool; x <- call (holeArgs✝.lookup HoleIndex.zero) (); c, d <- call (holeArgs✝.lookup HoleIndex.zero.succ) (§x, §m); b <- call (holeArgs✝.lookup HoleIndex.zero.succ.succ) (§x, §m, §c, §d); return §b }

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

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

noncomputable def GaudisCrypt.Examples.Pedersen.Correctness.main (types : CommitmentTypes) : Module.Arr (CommitmentScheme types) (procmod (types.Message) → Bool)

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

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperimentT.destruct_mk (theModule✝ : HidingExperimentT) : mk theModule✝.structure = theModule✝

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

def GaudisCrypt.Examples.Pedersen.HidingExperimentT : Type 1

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

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

Equations

• GaudisCrypt.Examples.Pedersen.HidingExperimentT = GaudisCrypt.Module GaudisCrypt.Examples.Pedersen.HidingExperimentT.typeRep

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperimentT.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

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

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperimentT.main.utilities : ModuleTypeUtilities HidingExperimentT (procmod () → Bool) main

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

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

Equations

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

def GaudisCrypt.Examples.Pedersen.HidingExperimentT.typeRep : ModuleTypeRep

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

HidingExperimentT is by definition Module HidingExperimentT.typeRep.

Equations

• GaudisCrypt.Examples.Pedersen.HidingExperimentT.typeRep = GaudisCrypt.ModuleTypeRep.proc (procsig () → Bool)

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperimentT.mk : Structure → HidingExperimentT

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

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

Equations

• GaudisCrypt.Examples.Pedersen.HidingExperimentT.mk theRecord✝ = theRecord✝.main

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleHidingExperimentT : IsModule HidingExperimentT

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

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

Equations

• GaudisCrypt.Examples.Pedersen.instIsModuleHidingExperimentT = { moduleTypeRep := GaudisCrypt.Examples.Pedersen.HidingExperimentT.typeRep, isModule := ⋯ }

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperimentT.structure : HidingExperimentT → Structure

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

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

Equations

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

structure GaudisCrypt.Examples.Pedersen.HidingExperimentT.Structure : Type 1

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

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

• main : procmod () → Bool

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperimentT.main : HidingExperimentT → procmod () → Bool

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

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

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

Equations

• theModule✝.main = theModule✝

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperimentT.main.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).main = theRecord✝.main

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

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

theorem GaudisCrypt.Examples.Pedersen.HidingExperiment.main.procedure.apply_simp (types : CommitmentTypes) (holeArgs✝ : (HoleSigs.cons (procsig () → types.Value) (HoleSigs.cons (procsig (types.Value) → types.Message × types.Message) (HoleSigs.cons (procsig (types.Value, types.Message) → types.Commitment × types.OpeningKey) (HoleSigs.cons (procsig (types.Commitment) → Bool) HoleSigs.empty)))).Instantiation) : (procedure types).instantiate holeArgs✝ = proc () : Bool { var x : types.Value, m0 : types.Message, m1 : types.Message, b : Bool, c : types.Commitment, d : types.OpeningKey, b' : Bool; x <- call (holeArgs✝.lookup HoleIndex.zero) (); m0, m1 <- call (holeArgs✝.lookup HoleIndex.zero.succ) (§x); b <$ SubProbability.uniform; c, d <- call (holeArgs✝.lookup HoleIndex.zero.succ.succ) (§x, if §b = true then §m1 else §m0); b' <- call (holeArgs✝.lookup HoleIndex.zero.succ.succ.succ) (§c); return §b == §b' }

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

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperiment.apply_simp (types : CommitmentTypes) (S : CommitmentScheme types) (U : Unhider types) : Module.app (HidingExperiment types) (Module.pair S U) = HidingExperimentT.mk { main := Module.app (Module.app (main types) S) U }

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

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

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperiment (types : CommitmentTypes) : Module.Arr (Module.Prod (CommitmentScheme types) (Unhider types)) HidingExperimentT

The module declared by module HidingExperiment, abstracted over its 2 parameters S, U, 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 HidingExperiment.main, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma HidingExperiment.apply_simp says.

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperiment.main.procedure (types : CommitmentTypes) : proctype () → Bool uses (() → types.Value, (types.Value) → types.Message × types.Message, (types.Value, types.Message) → types.Commitment × types.OpeningKey, (types.Commitment) → Bool)

The body of proc main of module HidingExperiment, as a procedure of its own: the 4 calls it makes to module parameters (S, U) 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 HidingExperiment.main.procedure.apply_simp) rather than run. Use HidingExperiment.main for this procedure as a module.

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperiment.main.apply_simp (types : CommitmentTypes) (S : CommitmentScheme types) (U : Unhider types) : Module.app (Module.app (main types) S) U = Module.proc ((procedure types).instantiate ((CommitmentScheme.gen types S).procedure, (Unhider.choose types U).procedure, (CommitmentScheme.commit types S).procedure, (Unhider.guess types U).procedure))

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

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperiment.main (types : CommitmentTypes) : Module.Arr (CommitmentScheme types) (Module.Arr (Unhider types) (procmod () → Bool))

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

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

Equations

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleBindingExperimentT : IsModule BindingExperimentT

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

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

Equations

• GaudisCrypt.Examples.Pedersen.instIsModuleBindingExperimentT = { moduleTypeRep := GaudisCrypt.Examples.Pedersen.BindingExperimentT.typeRep, isModule := ⋯ }

def GaudisCrypt.Examples.Pedersen.BindingExperimentT.typeRep : ModuleTypeRep

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

BindingExperimentT is by definition Module BindingExperimentT.typeRep.

Equations

• GaudisCrypt.Examples.Pedersen.BindingExperimentT.typeRep = GaudisCrypt.ModuleTypeRep.proc (procsig () → Bool)

def GaudisCrypt.Examples.Pedersen.BindingExperimentT : Type 1

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

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

Equations

• GaudisCrypt.Examples.Pedersen.BindingExperimentT = GaudisCrypt.Module GaudisCrypt.Examples.Pedersen.BindingExperimentT.typeRep

structure GaudisCrypt.Examples.Pedersen.BindingExperimentT.Structure : Type 1

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

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

• main : procmod () → Bool

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperimentT.mk_destruct (theRecord✝ : Structure) : (mk theRecord✝).structure = theRecord✝

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

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperimentT.main.utilities : ModuleTypeUtilities BindingExperimentT (procmod () → Bool) main

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

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperimentT.main.mk_simp (theRecord✝ : Structure) : (mk theRecord✝).main = theRecord✝.main

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

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

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperimentT.structure : BindingExperimentT → Structure

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

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

Equations

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

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperimentT.mk : Structure → BindingExperimentT

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

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

Equations

• GaudisCrypt.Examples.Pedersen.BindingExperimentT.mk theRecord✝ = theRecord✝.main

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperimentT.destruct_mk (theModule✝ : BindingExperimentT) : mk theModule✝.structure = theModule✝

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

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperimentT.main : BindingExperimentT → procmod () → Bool

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

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

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

Equations

• theModule✝.main = theModule✝

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperiment.main.apply_simp (types : CommitmentTypes) (S : CommitmentScheme types) (B : Binder types) : Module.app (Module.app (main types) S) B = Module.proc ((procedure types).instantiate ((CommitmentScheme.gen types S).procedure, (Binder.bind types B).procedure, (CommitmentScheme.verify types S).procedure))

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

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperiment.main (types : CommitmentTypes) : Module.Arr (CommitmentScheme types) (Module.Arr (Binder types) (procmod () → Bool))

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperiment.main.procedure (types : CommitmentTypes) : proctype () → Bool uses (() → types.Value, (types.Value) → types.Commitment × types.Message × types.OpeningKey × types.Message × types.OpeningKey, (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool)

The body of proc main of module BindingExperiment, as a procedure of its own: the 3 calls it makes to module parameters (S, 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 BindingExperiment.main.procedure.apply_simp) rather than run. Use BindingExperiment.main for this procedure as a module.

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperiment (types : CommitmentTypes) : Module.Arr (Module.Prod (CommitmentScheme types) (Binder types)) BindingExperimentT

The module declared by module BindingExperiment, abstracted over its 2 parameters S, 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 BindingExperiment.main, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma BindingExperiment.apply_simp says.

Equations

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

theorem GaudisCrypt.Examples.Pedersen.BindingExperiment.main.procedure.apply_simp (types : CommitmentTypes) (holeArgs✝ : (HoleSigs.cons (procsig () → types.Value) (HoleSigs.cons (procsig (types.Value) → types.Commitment × types.Message × types.OpeningKey × types.Message × types.OpeningKey) (HoleSigs.cons (procsig (types.Value, types.Message, types.Commitment, types.OpeningKey) → Bool) HoleSigs.empty))).Instantiation) : (procedure types).instantiate holeArgs✝ = proc () : Bool { var c : types.Commitment, m : types.Message, d : types.OpeningKey, m' : types.Message, d' : types.OpeningKey, v : Bool, v' : Bool; have _ : DecidableEq types.Message := Classical.decEq types.Message; (localVarLens "x" types.Value) <- call (holeArgs✝.lookup HoleIndex.zero) (); c, m, d, m', d' <- call (holeArgs✝.lookup HoleIndex.zero.succ) (§(localVarLens "x" types.Value)); v <- call (holeArgs✝.lookup HoleIndex.zero.succ.succ) (§(localVarLens "x" types.Value), §m, §c, §d); v' <- call (holeArgs✝.lookup HoleIndex.zero.succ.succ) (§(localVarLens "x" types.Value), §m', §c, §d'); return §v && §v' && !§m == §m' }

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

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperiment.apply_simp (types : CommitmentTypes) (S : CommitmentScheme types) (B : Binder types) : Module.app (BindingExperiment types) (Module.pair S B) = BindingExperimentT.mk { main := Module.app (Module.app (main types) S) B }

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

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