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
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