Formal Verification of Generalized Bulletproofs

Code artifacts, definitions and proofs for GBP/Bulletproofs built upon VCVio.

Definitions

This repository contains definitions of:

• (k1,...,kn) (Computional) Special Soundness
• Honest Verififer Zero-Knowledge
• Completeness

For "sigma-style" protocols, using the formulations/ideas from "Compressed Sigma Protocols" where each protocol is viewed as an interactive reduction from its relation to the language of accepting last round messages: the statement is the verifiers state and the proof is the last round message.

Composition Theorems

Additionally, this repository contains compositions theorems stating e.g.

Soundness:

If protocol is -special sound and protocol is -special sound.

Then (A followed by B) is -special sound

Zero-Knowledge:

If protocol is HVZK.

Then is HVZK for any

These enable "composing" a tower of reductions, which is how folding is expressed in this project.

Proofs

Finally, this repository contains proofs of:

• Generalized Bulletproofs (Arithmetization):
  • (Computional) -special soundness
  • Completeness
  • Perfect HVZK
• Improved Generalized Bulletproofs (Arithmetization):
  • (Computional) -special soundness (observe this protocol has an additional round).
  • Completeness
  • Perfect HVZK
• Bulletproof folding:
  • (Computional) 8-special soundness
  • Completeness
• Simplified Bulletproof folding:
  • (Computional) 4-special soundness
  • Completeness

Final Notes

This is part of a bigger project (hence the lack of git history), a teaser.

More exciting news to come...