Formally Verified Arguments of Knowledge in Lean
1
Introduction
2
Oracle Reductions
▶
2.1
Definitions
▶
2.1.1
Format
2.1.2
Execution Semantics
2.1.3
Security Properties
2.2
Composition of Oracle Reductions
▶
2.2.1
Sequential Composition
2.2.2
Lifting Contexts
2.3
The Fiat-Shamir Transformation
▶
2.3.1
Oracle Interface for Fiat-Shamir Challenges
2.3.2
Fiat-Shamir Transformation for Provers
2.3.3
Transcript Derivation and Verifier Transformation
2.3.4
Fiat-Shamir Transformation for Reductions
2.3.5
Security Properties
3
Proof Systems
▶
3.1
Simple Oracle Reductions
▶
3.1.1
Trivial Reduction
3.1.2
Sending the Witness
3.1.3
Oracle Equality Testing
3.1.4
Sending a Claim
3.1.5
Claim Reduction
3.1.6
Claim Verification
3.2
The Sum-Check Protocol
▶
3.2.1
Standard Description
3.2.2
Modular Description
3.3
The Spartan Protocol
▶
3.3.1
Preliminaries
3.3.2
Description in Paper
3.3.3
Formalization using IOR Composition
3.4
Stir
▶
3.4.1
Tools for Reed Solomon codes
3.4.2
Stir Main theorems
3.5
Whir
▶
3.5.1
Tools for Reed Solomon codes
3.6
The Spartan Protocol
3.7
The Ligero Polynomial Commitment Scheme
4
Commitment Schemes
▶
4.1
Definitions
4.2
Merkle Trees
5
Supporting Theories
▶
5.1
Polynomials
5.2
Coding Theory
5.3
The VCVio Library
6
References
7
Bibliography
Dependency graph
6 References