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
Ring Switching
▶
3.3.1
The packing profile
3.3.2
Packing the witness
3.3.3
The reduction
3.3.4
Security
3.4
Binius
▶
3.4.1
Binary Tower Fields
3.5
The Spartan Protocol
▶
3.5.1
Preliminaries
3.5.2
Description in Paper
3.5.3
Formalization using IOR Composition
3.6
Stir
▶
3.6.1
Tools for Reed Solomon codes
3.6.2
Stir Main theorems
3.7
Whir
▶
3.7.1
Tools for Reed Solomon codes
3.8
The Spartan Protocol
3.9
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
5.4
The Subfield \(R_q^H \cong \mathbb {F}_{q^k}\) (Hachi Lemma 5)
▶
5.4.1
What already exists
5.4.2
Target
5.4.3
Reduction to “\(R_q^H\) is a field”
5.4.4
The crux: \(R_q^{\sigma _{-1}}\) is a field
5.4.5
The swap (Phase 4): \(\sigma _{-1}\) and polynomial reversal
5.4.6
Phase 5: assembling the field and the isomorphism
5.4.7
Status and dependency summary
6
References
7
Bibliography
Chapter 1 graph
Chapter 2 graph
Chapter 3 graph
Chapter 4 graph
Chapter 5 graph
Chapter 6 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
Ring Switching
3.3.1
The packing profile
3.3.2
Packing the witness
3.3.3
The reduction
3.3.4
Security
3.4
Binius
3.4.1
Binary Tower Fields
3.5
The Spartan Protocol
3.5.1
Preliminaries
3.5.2
Description in Paper
3.5.3
Formalization using IOR Composition
3.6
Stir
3.6.1
Tools for Reed Solomon codes
3.6.2
Stir Main theorems
3.7
Whir
3.7.1
Tools for Reed Solomon codes
3.8
The Spartan Protocol
3.9
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
5.4
The Subfield \(R_q^H \cong \mathbb {F}_{q^k}\) (Hachi Lemma 5)
5.4.1
What already exists
5.4.2
Target
5.4.3
Reduction to “\(R_q^H\) is a field”
5.4.4
The crux: \(R_q^{\sigma _{-1}}\) is a field
5.4.5
The swap (Phase 4): \(\sigma _{-1}\) and polynomial reversal
5.4.6
Phase 5: assembling the field and the isomorphism
5.4.7
Status and dependency summary
6
References
7
Bibliography