Formally Verified Arguments of Knowledge in Lean
1
Introduction
2
Oracle Reductions
▶
2.1
Definitions
▶
2.1.1
Format
2.1.2
Security properties
2.2
A Program Logic for Oracle Reductions
▶
2.2.1
Changing Relations and Oracles
2.2.2
Sequential Composition
2.2.3
Virtualization
2.2.4
Substitution
3
Proof Systems
▶
3.1
Simple Oracle Reductions
▶
3.1.1
Polynomial Equality Testing
3.1.2
Batching Polynomial Evaluation Claims
3.2
The Sum-Check Protocol
3.3
The Spartan Protocol
3.4
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