The Pedersen commitment scheme #
A transliteration of EasyCrypt's examples/Pedersen.ec:
- EC's
clone DLog(cyclic groupgroupwith generatorg, prime exponent fieldexp) becomes the structurePedersenGroup: the operations the programs mention, plus the laws the proofs turned out to need (f_commring,gpow_add,gpow_mul— the last two are EC'sexpD/expM). It is a sectionvariable (group : PedersenGroup), and hence a Lean parameter of everything below that mentions it. - EC's
PedersenTypes+ theCommitmentclone become theCommitmentTypesrecordgroup.types(value/commitment = group, message/openingkey = exponent), which everyCommitmentScheme-shaped name here is applied to. module Pedersen : CommitmentSchemebecomes amodule Pedersen : (CommitmentScheme group.types) { … }declaration — EC's own syntax, near enough, now that themodulecommand exists.- Correctness is stated as EC states it (
hoare[Correctness(Pedersen).main : true ==> res]): the output distribution puts no mass onres = false. Proven (pedersen_correctness), on standard axioms only, entirely on themodulecommand's generated lemmas — this file declares nothing of its own for it beyond the per-procedurewp_*lemmas.
The group setup (EC's DLog clone) #
A cyclic group G with generator g and exponent type F (EC's group/exp).
Multiplication and exponentiation, what the programs genuinely need of the types — a default
element (Inhabited, so local variables can be declared) and Fintype F (real content:
SubProbability.uniform samples it, and the wp lemmas sum over it) — and the algebraic laws
the proofs need, which are the three fields documented individually below. Correctness needs
none of the laws; they are all for Hiding.lean.
Decidable equality is not a field. verify does compare ($c == $c'), and == is BEq
derived from DecidableEq — but these programs are never executed: every proc is
noncomputable and the semantics is a measure, so the comparison only ever has to denote a
Bool, not compute one. Classical.decEq supplies that for free, which is why the instances
below are classical and the class is two fields shorter. Nothing in the proofs cares: they
reason about =, and beq_self_eq_true and friends hold for any DecidableEq witness.
- G : Type
- F : Type
- g : self.G
EC's exponent type is the prime field
DL.GP.ZModE; the hiding proof formsd + x * mand its inversed - x * m, so the additive group and the multiplication are both needed. (Only the ring structure is required — nothing here uses inverses.)- gpow_add (h : self.G) (a b : self.F) : self.gpow h (a + b) = self.gmul (self.gpow h a) (self.gpow h b)
EC's
expD: exponentiation turns addition into multiplication. EC's
expM: iterated exponentiation multiplies the exponents.
Instances For
Equations
- GaudisCrypt.Examples.Pedersen.instInhabitedG group = group.g_inhabited
Equations
Equations
- GaudisCrypt.Examples.Pedersen.instInhabitedF group = group.f_inhabited
Equations
- GaudisCrypt.Examples.Pedersen.instCommRingF group = group.f_commring
Equations
Equations
- GaudisCrypt.Examples.Pedersen.instFintypeF group = group.f_fintype
Equations
- GaudisCrypt.Examples.Pedersen.instMulG group = { mul := group.gmul }
Equations
- GaudisCrypt.Examples.Pedersen.instPowGF group = { pow := group.gpow }
gpow_add at the ^/* notation. The class fields have to be stated with the raw
gmul/gpow (the instances below them do not exist yet), but every use site sees the
notation, and rw matches on the notation's head — not the raw field.
EC's PedersenTypes + clone Commitment with …: value/commitment are group elements,
message/openingkey are exponents.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scheme #
EC's
module Pedersen : CommitmentScheme = {
proc gen() : value = { x <$ dt; h <- g ^ x; return h; }
proc commit(h, m) = { d <$ dt; c <- (g ^ d) * (h ^ m); return (c, d); }
proc verify(h, m, c, d) = { c' <- (g ^ d) * (h ^ m); return (c = c'); }
}.
transcribes directly with the module command. It declares, per procedure f, both the body
Pedersen.f.procedure and the module Pedersen.f : Module.Proc …, and assembles them into
Pedersen : CommitmentScheme with CommitmentScheme.mk (the field names match the moduletype's,
so the record constructor is used rather than a nest of Module.pairs). Pedersen has no
module parameters, so it is the scheme — there is nothing to apply it to, and hence no
Pedersen.apply_simp.
Instantiating the holes of Pedersen.commit.procedure with a tuple holeArgs of procedures: the body of proc commit 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 [Pedersen.commit.procedure.apply_simp]).
Instantiating the holes of Pedersen.verify.procedure with a tuple holeArgs of procedures: the body of proc verify 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 [Pedersen.verify.procedure.apply_simp]).
The body of proc commit of module Pedersen, 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 Pedersen.commit.procedure.apply_simp) rather than run. Use Pedersen.commit for this procedure as a module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The module declared by module Pedersen: the record of its procedures Pedersen.gen, Pedersen.commit, Pedersen.verify.
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 Pedersen.apply_simp to apply it with.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instantiating the holes of Pedersen.gen.procedure with a tuple holeArgs of procedures: the body of proc gen 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 [Pedersen.gen.procedure.apply_simp]).
The body of proc verify of module Pedersen, 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 Pedersen.verify.procedure.apply_simp) rather than run. Use Pedersen.verify for this procedure as a module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]: Pedersen.gen = Module.proc Pedersen.gen.procedure — true by definition, proc gen using no module parameter and so having no holes to fill.
proc commit of module Pedersen as a module: Module.proc Pedersen.commit.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Pedersen.commit.apply_simp says exactly that.
Equations
Instances For
@[simp]: Pedersen.commit = Module.proc Pedersen.commit.procedure — true by definition, proc commit using no module parameter and so having no holes to fill.
proc verify of module Pedersen as a module: Module.proc Pedersen.verify.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Pedersen.verify.apply_simp says exactly that.
Equations
Instances For
@[simp]: Pedersen.verify = Module.proc Pedersen.verify.procedure — true by definition, proc verify using no module parameter and so having no holes to fill.
The body of proc gen of module Pedersen, 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 Pedersen.gen.procedure.apply_simp) rather than run. Use Pedersen.gen for this procedure as a module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
proc gen of module Pedersen as a module: Module.proc Pedersen.gen.procedure, of type Module.Proc (procsig …). It uses no module parameter, so it is not a function — Pedersen.gen.apply_simp says exactly that.