The Pedersen commitment scheme

A transliteration of EasyCrypt's examples/Pedersen.ec:

• EC's clone DLog (cyclic group group with generator g, prime exponent field exp) becomes the class PedersenGroup: 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's expD/expM).
• EC's PedersenTypes + the Commitment clone become the CommitmentTypes instance (value/commitment = group, message/openingkey = exponent).
• module Pedersen : CommitmentScheme becomes a module Pedersen : CommitmentScheme { … } declaration — EC's own syntax, near enough, now that the module command exists.
• Correctness is stated as EC states it (hoare[Correctness(Pedersen).main : true ==> res]): the output distribution puts no mass on res = false. Proven (pedersen_correctness), on standard axioms only, entirely on the module command's generated lemmas — this file declares nothing of its own for it beyond the per-procedure wp_* lemmas.

The group setup (EC's DLog clone)

class GaudisCrypt.Examples.Pedersen.PedersenGroup : Type 1

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 : G
• gmul : G → G → G
• gpow : G → F → G
• g_inhabited : Inhabited G
• f_inhabited : Inhabited F
• f_fintype : Fintype F
• f_commring : CommRing F

  EC's exponent type is the prime field DL.GP.ZModE; the hiding proof forms d + x * m and its inverse d - 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 : G) (a b : F) : gpow h (a + b) = gmul (gpow h a) (gpow h b)

  EC's expD: exponentiation turns addition into multiplication.

• gpow_mul (h : G) (a b : F) : gpow (gpow h a) b = gpow h (a * b)

  EC's expM: iterated exponentiation multiplies the exponents.

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instInhabitedG [PedersenGroup] : Inhabited G

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instInhabitedG = GaudisCrypt.Examples.Pedersen.PedersenGroup.g_inhabited

@[implicit_reducible]

noncomputable instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instDecidableEqG [PedersenGroup] : DecidableEq G

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instDecidableEqG = Classical.decEq GaudisCrypt.Examples.Pedersen.PedersenGroup.G

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instInhabitedF [PedersenGroup] : Inhabited F

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instInhabitedF = GaudisCrypt.Examples.Pedersen.PedersenGroup.f_inhabited

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instCommRingF [PedersenGroup] : CommRing F

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instCommRingF = GaudisCrypt.Examples.Pedersen.PedersenGroup.f_commring

@[implicit_reducible]

noncomputable instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instDecidableEqF [PedersenGroup] : DecidableEq F

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instDecidableEqF = Classical.decEq GaudisCrypt.Examples.Pedersen.PedersenGroup.F

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instFintypeF [PedersenGroup] : Fintype F

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instFintypeF = GaudisCrypt.Examples.Pedersen.PedersenGroup.f_fintype

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instMulG [PedersenGroup] : Mul G

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instMulG = { mul := GaudisCrypt.Examples.Pedersen.PedersenGroup.gmul }

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.PedersenGroup.instPowGF [PedersenGroup] : Pow G F

Equations

• GaudisCrypt.Examples.Pedersen.PedersenGroup.instPowGF = { pow := GaudisCrypt.Examples.Pedersen.PedersenGroup.gpow }

theorem GaudisCrypt.Examples.Pedersen.PedersenGroup.pow_add [PedersenGroup] (h : G) (a b : F) : h ^ (a + b) = h ^ a * h ^ b

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.

theorem GaudisCrypt.Examples.Pedersen.PedersenGroup.pow_mul [PedersenGroup] (h : G) (a b : F) : (h ^ a) ^ b = h ^ (a * b)

gpow_mul at the ^ notation.

@[implicit_reducible]

instance GaudisCrypt.Examples.Pedersen.pedersenTypes [PedersenGroup] : CommitmentTypes

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.

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.

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen.verify [ProgramSpec] [PedersenGroup] : procmod (PedersenGroup.G, PedersenGroup.F, PedersenGroup.G, PedersenGroup.F) → Bool

Equations

• GaudisCrypt.Examples.Pedersen.Pedersen.verify = GaudisCrypt.Module.proc GaudisCrypt.Examples.Pedersen.Pedersen.verify.procedure

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Pedersen.verify.apply_simp [ProgramSpec] [PedersenGroup] : verify = Module.proc procedure

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen.gen [ProgramSpec] [PedersenGroup] : procmod () → PedersenGroup.G

Equations

• GaudisCrypt.Examples.Pedersen.Pedersen.gen = GaudisCrypt.Module.proc GaudisCrypt.Examples.Pedersen.Pedersen.gen.procedure

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen.commit [ProgramSpec] [PedersenGroup] : procmod (PedersenGroup.G, PedersenGroup.F) → (PedersenGroup.G × PedersenGroup.F)

Equations

• GaudisCrypt.Examples.Pedersen.Pedersen.commit = GaudisCrypt.Module.proc GaudisCrypt.Examples.Pedersen.Pedersen.commit.procedure

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Pedersen.verify.procedure.apply_simp [ProgramSpec] [PedersenGroup] (args : HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : ProcedureSignature} => args) = proc (h : PedersenGroup.G, m : PedersenGroup.F, c : PedersenGroup.G, d : PedersenGroup.F) : Bool { var c' : PedersenGroup.G; c' <- PedersenGroup.g ^ §d * §h ^ §m; return §c == §c' }

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Pedersen.commit.procedure.apply_simp [ProgramSpec] [PedersenGroup] (args : HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : ProcedureSignature} => args) = proc (h : PedersenGroup.G, m : PedersenGroup.F) : (PedersenGroup.G × PedersenGroup.F) { var c : PedersenGroup.G, d : PedersenGroup.F; d <$ SubProbability.uniform; c <- PedersenGroup.g ^ §d * §h ^ §m; return (§c, §d) }

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Pedersen.gen.procedure.apply_simp [ProgramSpec] [PedersenGroup] (args : HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : ProcedureSignature} => args) = proc () : PedersenGroup.G { var x : PedersenGroup.F, h : PedersenGroup.G; x <$ SubProbability.uniform; h <- PedersenGroup.g ^ §x; return §h }

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen.verify.procedure [ProgramSpec] [PedersenGroup] : proctype (PedersenGroup.G, PedersenGroup.F, PedersenGroup.G, PedersenGroup.F) -> Bool

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen [ProgramSpec] [PedersenGroup] : CommitmentScheme

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Pedersen.gen.apply_simp [ProgramSpec] [PedersenGroup] : gen = Module.proc procedure

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen.gen.procedure [ProgramSpec] [PedersenGroup] : proctype () -> PedersenGroup.G

Equations

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

noncomputable def GaudisCrypt.Examples.Pedersen.Pedersen.commit.procedure [ProgramSpec] [PedersenGroup] : proctype (PedersenGroup.G, PedersenGroup.F) -> PedersenGroup.G × PedersenGroup.F

Equations

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

@[simp]

theorem GaudisCrypt.Examples.Pedersen.Pedersen.commit.apply_simp [ProgramSpec] [PedersenGroup] : commit = Module.proc procedure

Correctness

To run an applied functor module we extract its procedure: a normal closed module expression of procedure type is a .proc node (proc_type_is_proc / Module.procedure, now in Language/Modules.lean).

Correctness Pedersen β/δ-normalizes to Correctness.main with Pedersen's procedures in the holes. That reduction used to be done by hand here, by a functorApp_procedure bridge lemma, a functor_procedure tactic, a Pedersen_expression record equation and a pedersenInst naming the hole filling. None of it is needed any more, and all of it is gone (see the history of this file if you want it back): the module/moduletype commands emit @[simp] apply_simp lemmas and tag their accessors @[module_accessor], and those do the whole reduction inline in pedersen_correctness.

Per-procedure wp lemmas (EC's inline+auto steps, done once per procedure)

All three are stated at the CommitmentTypes-spelled signature the instantiated game carries, not at G/F. The two are definitionally equal, but Eq carries its type as an index, so the spelling is what makes them the same proposition as the goal — see the ⚠ below.

theorem GaudisCrypt.Examples.Pedersen.wp_gen [ProgramSpec] [PedersenGroup] (f : ProgramDenotation.Post State CommitmentTypes.Value) : (procedureDenotation Pedersen.gen.procedure ()).wp f = fun (st : State) => ∑ x : PedersenGroup.F, f (PedersenGroup.g ^ x, st) / ↑(Fintype.card PedersenGroup.F)

theorem GaudisCrypt.Examples.Pedersen.wp_commit [ProgramSpec] [PedersenGroup] (args : PedersenGroup.G × PedersenGroup.F) (f : ProgramDenotation.Post State (CommitmentTypes.Commitment × CommitmentTypes.OpeningKey)) : (procedureDenotation Pedersen.commit.procedure args).wp f = fun (st : State) => ∑ x : PedersenGroup.F, f ((PedersenGroup.g ^ x * args.1 ^ args.2, x), st) / ↑(Fintype.card PedersenGroup.F)

theorem GaudisCrypt.Examples.Pedersen.wp_verify [ProgramSpec] [PedersenGroup] (args : PedersenGroup.G × PedersenGroup.F × PedersenGroup.G × PedersenGroup.F) (f : ProgramDenotation.Post State Bool) : (procedureDenotation Pedersen.verify.procedure args).wp f = fun (st : State) => f (args.2.2.1 == PedersenGroup.g ^ args.2.2.2 * args.1 ^ args.2.1, st)

Reducing the applied functor

Correctness.main.procedure.apply_simp fills Correctness.main's holes with the callees they were made from — which, since Correctness's body calls S.gen, are the moduletype accessors CommitmentScheme.gen Pedersen and friends. The wp_* lemmas above are stated at Pedersen.gen.procedure, a separate definition the module command emits. Adding module_accessor (the simp set the accessors are tagged with), Pedersen, and the Module.proc/Module.procedure_proc round-trip to the main simp call is all it takes to close that gap. So the whole reduction is the commands' own lemmas plus one simp set: no bridge lemma, no hand-written hole instantiation, nothing declared for the purpose.

(Module.procedure_proc has to be paired with unfolding Module.proc: the library states the round-trip with Module.proc already unfolded, as (ModuleExpression.proc p).toModule (.proc p), so on its own it never fires against the folded Module.proc that X.<f>.apply_simp emits.)

⚠ One thing to know before touching this: CommitmentScheme.gen Pedersen and Pedersen.gen both print as Pedersen.gen (dot-notation collision) and are not defeq — the accessor is a chain of Module.fst'/Module.snd' through Pedersen's expression. So a lemma or rewrite aimed at the wrong one of the two fails with the two sides displaying identically, or with "did not find an occurrence of the pattern" against a goal in which the pattern is apparently right there. set_option pp.explicit true is what tells them apart. A second, similar trap: signature spellings must be CommitmentTypes.*, not G/F — those are defeq, but Eq carries its type as an index, so the two are different propositions and exact rejects the mismatch, again printing identically (convert … using 2 exposes that one). The wp_* lemmas above are spelled CommitmentTypes.* for exactly this reason.

theorem GaudisCrypt.Examples.Pedersen.pedersen_correctness [ProgramSpec] [PedersenGroup] (m : PedersenGroup.F) (σ : State) : (procedureDenotation (Module.procedure (Module.app Correctness Pedersen)) m σ).ofEvent {r : Bool × State | r.1 = false} = 0

Correctness of Pedersen — EC's hoare[Correctness(Pedersen).main : true ==> res]: from any initial state, the correctness game never returns false.