Abstract Polynomial Commitment Schemes

This file extends the abstract commitment scheme with evaluation opening: the prover can demonstrate that a committed polynomial evaluates to a claimed value at a given point, without revealing the polynomial.

Main definitions

• PolyCommitScheme — Extends CommitmentScheme with evaluation witness creation and verification
• EvalCorrect_Game — Evaluation correctness game
• EvalBinding_Game — Evaluation binding game
• PolyBinding_Game — Polynomial binding game

References

• SSProve/Commitments — PolyCom.v
• [Kate, Zaverucha, Goldberg, 2010 — §3.2]

Polynomial Commitment Scheme Structure

structure CatCrypt.Examples.Commitments.PolyCommitSchemeextends CatCrypt.Examples.Commitments.CommitmentScheme : Type 1

An abstract polynomial commitment scheme.

Extends CommitmentScheme with:

• An evaluation point type
• An evaluation value type
• A witness type for evaluation proofs
• create_witness: creates a proof that φ(z) = y
• verify_eval: checks the evaluation proof

• Key : Type
• Message : Type
• Commitment : Type
• Opening : Type
• instFintypeKey : Fintype self.Key
• instNonemptyKey : Nonempty self.Key
• instDecEqKey : DecidableEq self.Key
• instFintypeMessage : Fintype self.Message
• instNonemptyMessage : Nonempty self.Message
• instDecEqMessage : DecidableEq self.Message
• instFintypeCommitment : Fintype self.Commitment
• instNonemptyCommitment : Nonempty self.Commitment
• instDecEqCommitment : DecidableEq self.Commitment
• instFintypeOpening : Fintype self.Opening
• instNonemptyOpening : Nonempty self.Opening
• instDecEqOpening : DecidableEq self.Opening
• setup : Core.SPComp self.Key
• commit : self.Key → self.Message → Core.SPComp (self.Commitment × self.Opening)
• verify : self.Key → self.Message → self.Commitment → self.Opening → Bool
• Point : Type

  Evaluation point type

• Value : Type

  Evaluation value type

• Witness : Type

  Evaluation witness type

• instFintypePoint : Fintype self.Point
• instNonemptyPoint : Nonempty self.Point
• instDecEqPoint : DecidableEq self.Point
• instFintypeValue : Fintype self.Value
• instNonemptyValue : Nonempty self.Value
• instDecEqValue : DecidableEq self.Value
• instFintypeWitness : Fintype self.Witness
• instNonemptyWitness : Nonempty self.Witness
• instDecEqWitness : DecidableEq self.Witness
• create_witness : self.Key → self.Message → self.Point → Core.SPComp (self.Witness × self.Value)

  Create evaluation witness: given key, polynomial, and point, produce witness and value

• verify_eval : self.Key → self.Commitment → self.Point → self.Value → self.Witness → Bool

  Verify evaluation proof

Evaluation Correctness

noncomputable def CatCrypt.Examples.Commitments.EvalCorrect_Game (PS : PolyCommitScheme) (m : PS.Message) (z : PS.Point) : Core.SPComp Bool

Evaluation correctness game: setup, commit, create witness, verify eval. Returns true if verify_eval accepts the honest evaluation proof.

Equations

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

Polynomial Binding

@[reducible, inline]

abbrev CatCrypt.Examples.Commitments.PolyBindingAdversary (PS : PolyCommitScheme) : Type

Polynomial binding adversary: given key, output two different polynomials that have the same commitment

Equations

• CatCrypt.Examples.Commitments.PolyBindingAdversary PS = (PS.Key → CatCrypt.Core.SPComp (PS.Message × PS.Opening × PS.Message × PS.Opening × PS.Commitment))

noncomputable def CatCrypt.Examples.Commitments.PolyBinding_Game (PS : PolyCommitScheme) (A : PolyBindingAdversary PS) : Core.SPComp Bool

Polynomial binding game: adversary finds two polynomials with the same commitment. Same as Binding_Game for the underlying commitment scheme.

Equations

• CatCrypt.Examples.Commitments.PolyBinding_Game PS A = CatCrypt.Examples.Commitments.Binding_Game PS.toCommitmentScheme A

Evaluation Binding

@[reducible, inline]

abbrev CatCrypt.Examples.Commitments.EvalBindingAdversary (PS : PolyCommitScheme) : Type

Evaluation binding adversary: given key, output a commitment and two valid evaluation openings at the same point with different values

Equations

• CatCrypt.Examples.Commitments.EvalBindingAdversary PS = (PS.Key → CatCrypt.Core.SPComp (PS.Commitment × PS.Point × PS.Value × PS.Witness × PS.Value × PS.Witness))

noncomputable def CatCrypt.Examples.Commitments.EvalBinding_Game (PS : PolyCommitScheme) (A : EvalBindingAdversary PS) : Core.SPComp Bool

Evaluation binding game: adversary finds two valid evaluation openings at the same point with different values for the same commitment

Equations

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

noncomputable def CatCrypt.Examples.Commitments.EvalBinding_Advantage (PS : PolyCommitScheme) (A : EvalBindingAdversary PS) : ENNReal

Evaluation binding advantage

Equations

• CatCrypt.Examples.Commitments.EvalBinding_Advantage PS A = CatCrypt.Crypto.prTrue (CatCrypt.Examples.Commitments.EvalBinding_Game PS A) CatCrypt.Core.Heap.empty

Knowledge Soundness

structure CatCrypt.Examples.Commitments.KnowledgeSoundnessAdversary (PS : PolyCommitScheme) : Type

Knowledge soundness adversary: given key, output commitment C and evaluation proof (z, y, w). Extractor must recover the committed polynomial.

• run : PS.Key → Core.SPComp (PS.Commitment × PS.Point × PS.Value × PS.Witness)

  Adversary produces commitment and evaluation opening