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 type class CommitmentTypes (instance-implicit section parameters, so the moduletype-generated definitions elaborate — the same pattern as [ProgramSpec]).
• EC module types become moduletypes.
• EC's parameterized modules (Correctness(S), HidingExperiment(S,U), BindingExperiment(S,B)) become module X (P : T) { … } declarations: the calls are written against the parameters' own fields and the holes are inferred from them.

class GaudisCrypt.Examples.Pedersen.CommitmentTypes : Type 1

The abstract types of EC's theory CommitmentProtocol: the public value (key), the message space, commitments, and opening keys. Inhabited is needed for program local variables of these types — that one is real content (a default value has to exist).

There is deliberately no DecidableEq here. It was a field (message_deceq), justified by EC's binding experiment comparing m ≠ m', but decidability is never needed for proofs — only to form a Bool-valued program expression via BEq — and no program in this development compares messages, so nothing consumed it. (Commitment never had one either, and that has never been missed.) When BindingExperiment does need m ≠ m', note that these programs are never executed — the semantics is a measure and every proc is noncomputable — so Classical.decEq at the point of use is enough; a class field buys nothing. See Lib/RO/CollisionResistance.lean, which does exactly that.

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

def GaudisCrypt.Examples.Pedersen.f (x y : ℕ) : ℕ

Equations

• GaudisCrypt.Examples.Pedersen.f x y = x + y

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedValue [CommitmentTypes] : Inhabited CommitmentTypes.Value

Equations

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedMessage [CommitmentTypes] : Inhabited CommitmentTypes.Message

Equations

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedCommitment [CommitmentTypes] : Inhabited CommitmentTypes.Commitment

Equations

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instInhabitedOpeningKey [CommitmentTypes] : Inhabited CommitmentTypes.OpeningKey

Equations

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

Disjointness of tuple-projection lenses

The proc macro binds each local variable to a Lens.id.ofst/.osnd projection chain into the local-state tuple; tuple assignment (c, d <- …) pairs those lenses via Lens.pair, which needs them disjoint. Distinct projection paths are always disjoint, and the instances deriving that (Lens.disjoint_ofst_osnd, Lens.disjoint_chain, …) now live in Language/Lens.lean — the "move them to the proper place" TODO that used to sit here is done, and they are no longer declared in this file.

⚠ They still do not make tuple assignment of locals work (re-tested 2026-08-07): the macro binds locals as let-variables, and instance search does not unfold local lets, so disjoint c d is searched at the opaque variables and never reaches these instances.

Both spellings fail, identically — [lvalRaw|] sends the parenthesised tuple to Lens.pair just as the comma-list does, so there is no way around it by rewriting the assignment:

c, d   <- call S.commit (…);   -- failed to synthesize instance of type class  disjoint c d
(c, d) <- call S.commit (…);   -- same

Until the macro binds locals differently (inlining the lens chains, or registering the disjointness facts itself), the experiments below use pair-typed locals and $-projections instead — var cd : Commitment × OpeningKey then ($cd).1/($cd).2.

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

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.mk_destruct [ProgramSpec] [CommitmentTypes] (s : Structure) : (mk s).structure = s

structure GaudisCrypt.Examples.Pedersen.CommitmentScheme.Structure [ProgramSpec] [CommitmentTypes] : Type (max 1 u_1)

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

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleCommitmentScheme [ProgramSpec] [CommitmentTypes] : IsModule CommitmentScheme

Equations

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

def GaudisCrypt.Examples.Pedersen.CommitmentScheme [ProgramSpec] [CommitmentTypes] : Type (max 1 u_1)

Equations

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

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

Equations

• m.verify = (GaudisCrypt.Module.snd' m).snd'

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.mk [ProgramSpec] [CommitmentTypes] (s : Structure) : CommitmentScheme

Equations

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

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

Equations

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

def GaudisCrypt.Examples.Pedersen.CommitmentScheme.typeRep [CommitmentTypes] : ModuleTypeRep

Equations

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

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

Equations

• m.commit = (GaudisCrypt.Module.snd' m).fst'

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.CommitmentScheme.destruct_mk [ProgramSpec] [CommitmentTypes] (m : CommitmentScheme) : mk m.structure = m

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.structure [ProgramSpec] [CommitmentTypes] (m : CommitmentScheme) : Structure

Equations

• m.structure = { gen := m.gen, commit := m.commit, verify := m.verify }

noncomputable def GaudisCrypt.Examples.Pedersen.CommitmentScheme.gen [ProgramSpec] [CommitmentTypes] (m : CommitmentScheme) : procmod () → CommitmentTypes.Value

Equations

• m.gen = GaudisCrypt.Module.fst' m

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

Equations

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

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.mk [ProgramSpec] [CommitmentTypes] (s : Structure) : Unhider

Equations

• GaudisCrypt.Examples.Pedersen.Unhider.mk s = GaudisCrypt.Module.pair' s.choose s.guess

def GaudisCrypt.Examples.Pedersen.Unhider.typeRep [CommitmentTypes] : ModuleTypeRep

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.structure [ProgramSpec] [CommitmentTypes] (m : Unhider) : Structure

Equations

• m.structure = { choose := m.choose, guess := m.guess }

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleUnhider [ProgramSpec] [CommitmentTypes] : IsModule Unhider

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Unhider.mk_destruct [ProgramSpec] [CommitmentTypes] (s : Structure) : (mk s).structure = s

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.guess [ProgramSpec] [CommitmentTypes] (m : Unhider) : procmod (CommitmentTypes.Commitment) → Bool

Equations

• m.guess = GaudisCrypt.Module.snd' m

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Unhider.destruct_mk [ProgramSpec] [CommitmentTypes] (m : Unhider) : mk m.structure = m

noncomputable def GaudisCrypt.Examples.Pedersen.Unhider.choose [ProgramSpec] [CommitmentTypes] (m : Unhider) : procmod (CommitmentTypes.Value) → (CommitmentTypes.Message × CommitmentTypes.Message)

Equations

• m.choose = GaudisCrypt.Module.fst' m

def GaudisCrypt.Examples.Pedersen.Unhider [ProgramSpec] [CommitmentTypes] : Type (max 1 u_1)

Equations

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

structure GaudisCrypt.Examples.Pedersen.Unhider.Structure [ProgramSpec] [CommitmentTypes] : Type (max 1 u_1)

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

def GaudisCrypt.Examples.Pedersen.Binder [ProgramSpec] [CommitmentTypes] : Type (max 1 u_1)

Equations

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

@[reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.mk [ProgramSpec] [CommitmentTypes] (s : Structure) : Binder

Equations

• GaudisCrypt.Examples.Pedersen.Binder.mk s = s.bind

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.structure [ProgramSpec] [CommitmentTypes] (m : Binder) : Structure

Equations

• m.structure = { bind := m.bind }

def GaudisCrypt.Examples.Pedersen.Binder.typeRep [CommitmentTypes] : ModuleTypeRep

Equations

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

structure GaudisCrypt.Examples.Pedersen.Binder.Structure [ProgramSpec] [CommitmentTypes] : Type (max 1 u_1)

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

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Binder.bind [ProgramSpec] [CommitmentTypes] (m : Binder) : procmod (CommitmentTypes.Value) → (CommitmentTypes.Commitment × CommitmentTypes.Message × CommitmentTypes.OpeningKey × CommitmentTypes.Message × CommitmentTypes.OpeningKey)

Equations

• m.bind = m

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Binder.mk_destruct [ProgramSpec] [CommitmentTypes] (s : Structure) : (mk s).structure = s

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.instIsModuleBinder [ProgramSpec] [CommitmentTypes] : IsModule Binder

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Binder.destruct_mk [ProgramSpec] [CommitmentTypes] (m : Binder) : mk m.structure = m

instance GaudisCrypt.Examples.Pedersen.LocalVariableState.disjoint_varsL_paramsL {a b : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} {x : Lens a (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))} {y : Lens b (paramListToTuple paramTypes)} : disjoint (LocalVariableState.varsL.chain x) (LocalVariableState.paramsL.chain y)

params and vars are distinct fields of LocalVariableState, so writes through projections of the two commute — no hypothesis on x, y needed.

instance GaudisCrypt.Examples.Pedersen.LocalVariableState.disjoint_paramsL_varsL {a b : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} {x : Lens a (paramListToTuple paramTypes)} {y : Lens b (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))} : disjoint (LocalVariableState.paramsL.chain x) (LocalVariableState.varsL.chain y)

The mirror image of LocalVariableState.disjoint_varsL_paramsL; disjoint.symm is a theorem, not an instance, so search needs both orientations spelled out.

instance GaudisCrypt.Examples.Pedersen.Programs.disjoint_intoParams [ProgramSpec] {a b : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} {x : Lens a (paramListToTuple paramTypes)} {y : Lens b (paramListToTuple paramTypes)} [disjoint x y] : disjoint x.intoParams y.intoParams

Parameter-slot counterpart of Programs.disjoint_intoVars: distinct parameter slots stay disjoint after intoParams (two chain layers).

instance GaudisCrypt.Examples.Pedersen.Programs.disjoint_intoVars_intoParams [ProgramSpec] {a b : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} {x : Lens a (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))} {y : Lens b (paramListToTuple paramTypes)} : disjoint x.intoVars y.intoParams

A local variable is disjoint from any parameter: they live in different fields of the scope record, so no disjoint x y hypothesis is required.

instance GaudisCrypt.Examples.Pedersen.Programs.disjoint_intoParams_intoVars [ProgramSpec] {a b : Type} {paramTypes : List Type} {locals : List ((t : Type) × Inhabited t)} {x : Lens a (paramListToTuple paramTypes)} {y : Lens b (paramListToTuple (List.map (fun (x : (t : Type) × Inhabited t) => x.fst) locals))} : disjoint x.intoParams y.intoVars

The other orientation of Programs.disjoint_intoVars_intoParams.

noncomputable def GaudisCrypt.Examples.Pedersen.Correctness [ProgramSpec] [CommitmentTypes] : Module.Arr CommitmentScheme (procmod (CommitmentTypes.Message) → Bool)

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Correctness.main.apply_simp [ProgramSpec] [CommitmentTypes] (S : CommitmentScheme) : Module.app main S = Module.proc (procedure.instantiate fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.nil) (Module.procedure S.gen)) (Module.procedure S.commit)) (Module.procedure S.verify))

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Correctness.apply_simp [ProgramSpec] [CommitmentTypes] (S : CommitmentScheme) : Module.app Correctness S = Module.app main S

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Correctness.main.procedure.apply_simp [ProgramSpec] [CommitmentTypes] (args : (((HoleSigs.empty.append (procsig () → CommitmentTypes.Value)).append (procsig (CommitmentTypes.Value, CommitmentTypes.Message) → CommitmentTypes.Commitment × CommitmentTypes.OpeningKey)).append (procsig (CommitmentTypes.Value, CommitmentTypes.Message, CommitmentTypes.Commitment, CommitmentTypes.OpeningKey) → Bool)).Instantiation) : (procedure.instantiate fun {sig : ProcedureSignature} => args) = proc (m : CommitmentTypes.Message) : Bool { var x : CommitmentTypes.Value, cd : CommitmentTypes.Commitment × CommitmentTypes.OpeningKey, b : Bool; x <- call (args HoleIndex.zero.succ.succ) (); cd <- call (args HoleIndex.zero.succ) (§x, §m); b <- call (args HoleIndex.zero) (§x, §m, (§cd).1, (§cd).2); return §b }

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperiment.main.apply_simp [ProgramSpec] [CommitmentTypes] (S : CommitmentScheme) (U : Unhider) : Module.app (Module.app main S) U = Module.proc (procedure.instantiate fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.nil) (Module.procedure S.gen)) (Module.procedure U.choose)) (Module.procedure S.commit)) (Module.procedure U.guess))

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

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.HidingExperiment [ProgramSpec] [CommitmentTypes] : Module.Arr (Module.Prod CommitmentScheme Unhider) (procmod () → Bool)

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperiment.apply_simp [ProgramSpec] [CommitmentTypes] (S : CommitmentScheme) (U : Unhider) : Module.app HidingExperiment (Module.pair S U) = Module.app (Module.app main S) U

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.HidingExperiment.main.procedure.apply_simp [ProgramSpec] [CommitmentTypes] (args : ((((HoleSigs.empty.append (procsig () → CommitmentTypes.Value)).append (procsig (CommitmentTypes.Value) → CommitmentTypes.Message × CommitmentTypes.Message)).append (procsig (CommitmentTypes.Value, CommitmentTypes.Message) → CommitmentTypes.Commitment × CommitmentTypes.OpeningKey)).append (procsig (CommitmentTypes.Commitment) → Bool)).Instantiation) : (procedure.instantiate fun {sig : ProcedureSignature} => args) = proc () : Bool { var x : CommitmentTypes.Value, mm : CommitmentTypes.Message × CommitmentTypes.Message, b : Bool, cd : CommitmentTypes.Commitment × CommitmentTypes.OpeningKey, bg : Bool; x <- call (args HoleIndex.zero.succ.succ.succ) (); mm <- call (args HoleIndex.zero.succ.succ) (§x); b <$ SubProbability.uniform; cd <- call (args HoleIndex.zero.succ) (§x, if §b = true then (§mm).2 else (§mm).1); bg <- call (args HoleIndex.zero) ((§cd).1); return §b == §bg }

@[implicit_reducible]

noncomputable def GaudisCrypt.Examples.Pedersen.instDecidableEqMessage [CommitmentTypes] : DecidableEq CommitmentTypes.Message

Equations

• GaudisCrypt.Examples.Pedersen.instDecidableEqMessage = Classical.decEq GaudisCrypt.Examples.Pedersen.CommitmentTypes.Message

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperiment.main.procedure.apply_simp [ProgramSpec] [CommitmentTypes] (args : (((HoleSigs.empty.append (procsig () → CommitmentTypes.Value)).append (procsig (CommitmentTypes.Value) → CommitmentTypes.Commitment × CommitmentTypes.Message × CommitmentTypes.OpeningKey × CommitmentTypes.Message × CommitmentTypes.OpeningKey)).append (procsig (CommitmentTypes.Value, CommitmentTypes.Message, CommitmentTypes.Commitment, CommitmentTypes.OpeningKey) → Bool)).Instantiation) : (procedure.instantiate fun {sig : ProcedureSignature} => args) = proc () : Bool { var x : CommitmentTypes.Value, r : CommitmentTypes.Commitment × CommitmentTypes.Message × CommitmentTypes.OpeningKey × CommitmentTypes.Message × CommitmentTypes.OpeningKey, v : Bool, v' : Bool; x <- call (args HoleIndex.zero.succ.succ) (); r <- call (args HoleIndex.zero.succ) (§x); v <- call (args HoleIndex.zero) (§x, (§r).2.1, (§r).1, (§r).2.2.1); v' <- call (args HoleIndex.zero) (§x, (§r).2.2.2.1, (§r).1, (§r).2.2.2.2); return §v && §v' && !(§r).2.1 == (§r).2.2.2.1 }

noncomputable def GaudisCrypt.Examples.Pedersen.BindingExperiment [ProgramSpec] [CommitmentTypes] : Module.Arr (Module.Prod CommitmentScheme Binder) (procmod () → Bool)

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperiment.main.apply_simp [ProgramSpec] [CommitmentTypes] (S : CommitmentScheme) (B : Binder) : Module.app (Module.app main S) B = Module.proc (procedure.instantiate fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.push (fun {sig : ProcedureSignature} => HoleSigs.Instantiation.nil) (Module.procedure S.gen)) (Module.procedure B.bind)) (Module.procedure S.verify))

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

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.BindingExperiment.apply_simp [ProgramSpec] [CommitmentTypes] (S : CommitmentScheme) (B : Binder) : Module.app BindingExperiment (Module.pair S B) = Module.app (Module.app main S) B

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

Equations

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