Skip to content

Commit d4e283b

Browse files
FerinkoFerinko
committed
Merge remote-tracking branch 'upstream/main' into Ferinko/ElijahVlasov/johnson
2 parents 7f62c24 + 597ea03 commit d4e283b

155 files changed

Lines changed: 17707 additions & 13740 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/blueprint.yml‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,10 @@ name: Compile blueprint
22

33
on:
44
push:
5-
# branches:
6-
# - main # Trigger on pushes to ANY branch now
5+
branches: [main]
76
workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
8-
# pull_request:
9-
# branches: [main]
7+
pull_request:
8+
branches: [main]
109

1110
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
1211
permissions:
@@ -38,7 +37,7 @@ jobs:
3837
3938
- name: check that all files are imported
4039
run: git diff --exit-code
41-
40+
4241
build_project:
4342
runs-on: ubuntu-latest
4443
name: Build project
@@ -57,7 +56,6 @@ jobs:
5756
- name: Build project
5857
run: ~/.elan/bin/lake build ArkLib
5958

60-
6159
- name: Build blueprint and copy to `home_page/blueprint`
6260
uses: xu-cheng/texlive-action@v2
6361
with:

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,3 +19,5 @@
1919
/blueprint/src/web.pdf
2020

2121
.nvim.lua
22+
# Web files for local viewing
23+
/blueprint/web/

‎AUTHORS‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,6 @@ Bolton Bailey
55
Frantisek Silvasi
66
Ilia Vlasov
77
Julian Sutherland
8-
Chung Thai Nguyen
8+
Chung Thai Nguyen
9+
Poulami Das
10+
Mirco Richter

‎ArkLib.lean‎

Lines changed: 73 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,34 @@ import ArkLib.Data.CodingTheory.JohnsonBound
1010
import ArkLib.Data.CodingTheory.ProximityGap
1111
import ArkLib.Data.CodingTheory.ReedMuller
1212
import ArkLib.Data.CodingTheory.ReedSolomon
13+
import ArkLib.Data.Classes.DCast
14+
import ArkLib.Data.Classes.HasSize
15+
import ArkLib.Data.Classes.Initialize
16+
import ArkLib.Data.Classes.Serde
17+
import ArkLib.Data.Classes.Zeroize
1318
import ArkLib.Data.CodingTheory
19+
import ArkLib.Data.CodingTheory.Basic
20+
import ArkLib.Data.CodingTheory.BerlekampWelch
21+
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
22+
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
23+
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
24+
import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
25+
import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
26+
import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
27+
import ArkLib.Data.CodingTheory.DivergenceOfSets
28+
import ArkLib.Data.CodingTheory.InterleavedCode
29+
import ArkLib.Data.CodingTheory.ListDecodability
30+
import ArkLib.Data.CodingTheory.PolishchukSpielman
31+
import ArkLib.Data.CodingTheory.Prelims
32+
import ArkLib.Data.CodingTheory.ProximityGap
33+
import ArkLib.Data.CodingTheory.ReedMuller
34+
import ArkLib.Data.CodingTheory.ReedSolomon
1435
import ArkLib.Data.EllipticCurve.BN254
15-
import ArkLib.Data.FieldTheory.BinaryTowerField.Basic
16-
import ArkLib.Data.FieldTheory.BinaryTowerField.Prelude
36+
import ArkLib.Data.FieldTheory.BinaryField.AdditiveNTT.NovelPolynomialBasis
37+
import ArkLib.Data.FieldTheory.BinaryField.AdditiveNTT.Prelude
38+
import ArkLib.Data.FieldTheory.BinaryField.Tower.Basic
39+
import ArkLib.Data.FieldTheory.BinaryField.Tower.Impl
40+
import ArkLib.Data.FieldTheory.BinaryField.Tower.Prelude
1741
import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_377
1842
import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_381
1943
import ArkLib.Data.FieldTheory.NonBinaryField.BN254
@@ -23,22 +47,33 @@ import ArkLib.Data.FieldTheory.NonBinaryField.Goldilocks
2347
import ArkLib.Data.FieldTheory.NonBinaryField.Mersenne
2448
import ArkLib.Data.FieldTheory.NonBinaryField.Secp256k1
2549
import ArkLib.Data.Fin.Basic
50+
import ArkLib.Data.Fin.Lift
51+
import ArkLib.Data.Fin.Pad
52+
import ArkLib.Data.Hash.DomainSep
53+
import ArkLib.Data.Hash.DuplexSponge
2654
import ArkLib.Data.Math.Basic
27-
import ArkLib.Data.Math.DepCast
2855
import ArkLib.Data.Math.HList
56+
import ArkLib.Data.Matrix.Basic
57+
import ArkLib.Data.Matrix.Sparse
2958
import ArkLib.Data.MlPoly.Basic
3059
import ArkLib.Data.MlPoly.Equiv
3160
import ArkLib.Data.MvPolynomial.Degrees
3261
import ArkLib.Data.MvPolynomial.Interpolation
62+
import ArkLib.Data.MvPolynomial.LinearMvExtension
3363
import ArkLib.Data.MvPolynomial.Multilinear
3464
import ArkLib.Data.MvPolynomial.Notation
3565
import ArkLib.Data.MvPolynomial.Sumcheck
66+
import ArkLib.Data.Polynomial.Bivariate
3667
import ArkLib.Data.Polynomial.EvenAndOdd
68+
import ArkLib.Data.Polynomial.Interface
3769
import ArkLib.Data.Probability.Instances
3870
import ArkLib.Data.Probability.Notation
71+
import ArkLib.Data.Tree.Binary
72+
import ArkLib.Data.Tree.General
3973
import ArkLib.Data.UniPoly.Basic
4074
import ArkLib.Data.UniPoly.BasicOld
4175
import ArkLib.Data.UniPoly.PolynomialReflection
76+
import ArkLib.OracleReduction.BCS.Basic
4277
import ArkLib.OracleReduction.Basic
4378
import ArkLib.OracleReduction.Cast
4479
import ArkLib.OracleReduction.Composition.Parallel.Basic
@@ -47,15 +82,24 @@ import ArkLib.OracleReduction.Composition.Sequential.General
4782
import ArkLib.OracleReduction.Composition.Sequential.ProtocolSpec
4883
import ArkLib.OracleReduction.Equiv
4984
import ArkLib.OracleReduction.Execution
50-
import ArkLib.OracleReduction.LiftContext.Basic
85+
import ArkLib.OracleReduction.FiatShamir.Basic
86+
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.State
87+
import ArkLib.OracleReduction.LiftContext.Lens
88+
import ArkLib.OracleReduction.LiftContext.OracleReduction
89+
import ArkLib.OracleReduction.LiftContext.Reduction
5190
import ArkLib.OracleReduction.OracleInterface
5291
import ArkLib.OracleReduction.Prelude
92+
import ArkLib.OracleReduction.ProtocolSpec
5393
import ArkLib.OracleReduction.Security.Basic
54-
import ArkLib.OracleReduction.Transform.BCS
55-
import ArkLib.OracleReduction.Transform.FiatShamir
94+
import ArkLib.OracleReduction.Security.Implications
95+
import ArkLib.OracleReduction.Security.Rewinding
96+
import ArkLib.OracleReduction.Security.RoundByRound
97+
import ArkLib.OracleReduction.Security.StateRestoration
5698
import ArkLib.OracleReduction.VectorIOR
57-
import ArkLib.ProofSystem.Component.CheckPred
99+
import ArkLib.ProofSystem.Component.CheckClaim
100+
import ArkLib.ProofSystem.Component.DoNothing
58101
import ArkLib.ProofSystem.Component.RandomQuery
102+
import ArkLib.ProofSystem.Component.ReduceClaim
59103
import ArkLib.ProofSystem.Component.SendClaim
60104
import ArkLib.ProofSystem.Component.SendWitness
61105
import ArkLib.ProofSystem.ConstraintSystem.IndexedLookup
@@ -65,12 +109,32 @@ import ArkLib.ProofSystem.DSL
65109
import ArkLib.ProofSystem.Fri.RoundConsistency
66110
import ArkLib.ProofSystem.Plonk.Basic
67111
import ArkLib.ProofSystem.Spartan.Basic
68-
import ArkLib.ProofSystem.Sumcheck.Basic
69-
import ArkLib.ProofSystem.Sumcheck.SingleRound
112+
import ArkLib.ProofSystem.Stir
113+
import ArkLib.ProofSystem.Stir.Combine
114+
import ArkLib.ProofSystem.Stir.Folding
115+
import ArkLib.ProofSystem.Stir.MainThm
116+
import ArkLib.ProofSystem.Stir.OutOfDomSmpl
117+
import ArkLib.ProofSystem.Stir.ProximityBound
118+
import ArkLib.ProofSystem.Stir.ProximityGap
119+
import ArkLib.ProofSystem.Stir.Quotienting
120+
import ArkLib.ProofSystem.Sumcheck.Impl.Basic
121+
import ArkLib.ProofSystem.Sumcheck.Spec.General
122+
import ArkLib.ProofSystem.Sumcheck.Spec.SingleRound
123+
import ArkLib.ProofSystem.Whir
124+
import ArkLib.ProofSystem.Whir.BlockRelDistance
125+
import ArkLib.ProofSystem.Whir.Folding
126+
import ArkLib.ProofSystem.Whir.GenMutualCorrAgreement
127+
import ArkLib.ProofSystem.Whir.MainThm
128+
import ArkLib.ProofSystem.Whir.OutofDomainSmpl
129+
import ArkLib.ProofSystem.Whir.ProximityGap
130+
import ArkLib.ProofSystem.Whir.ProximityGen
70131
import ArkLib.ToMathlib.BigOperators.Fin
71132
import ArkLib.ToMathlib.Finset.Basic
72133
import ArkLib.ToMathlib.Finsupp.Fin
73134
import ArkLib.ToMathlib.MvPolynomial.Equiv
74135
import ArkLib.ToMathlib.NumberTheory.PrattCertificate
75136
import ArkLib.ToMathlib.UInt.Equiv
137+
import ArkLib.ToVCVio.DistEq
138+
import ArkLib.ToVCVio.Lemmas
76139
import ArkLib.ToVCVio.Oracle
140+
import ArkLib.ToVCVio.SimOracle

‎ArkLib/CommitmentScheme/Basic.lean‎

Lines changed: 24 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -29,39 +29,41 @@ namespace Commitment
2929

3030
open OracleSpec OracleComp SubSpec
3131

32-
variable {n : ℕ} {ι : Type}
32+
variable {ι : Type} (oSpec : OracleSpec ι) (Data Randomness Commitment : Type)
3333

34-
structure Commit (oSpec : OracleSpec ι) (Data Randomness Commitment : Type) where
34+
structure Commit where
3535
commit : Data → Randomness → OracleComp oSpec Commitment
3636

37-
structure Opening (pSpec : ProtocolSpec n) (oSpec : OracleSpec ι) (Data : Type)
38-
[O : OracleInterface Data] (Randomness Commitment : Type) where
39-
opening : Proof pSpec oSpec (Commitment × O.Query × O.Response) (Data × Randomness)
37+
variable [O : OracleInterface Data] {n : ℕ} (pSpec : ProtocolSpec n)
38+
39+
structure Opening where
40+
opening : Proof oSpec (Commitment × O.Query × O.Response) (Data × Randomness) pSpec
4041

4142
-- abbrev Statement (Data Commitment : Type) [O : OracleInterface Data] :=
4243
-- Commitment × O.Query × O.Response
4344

4445
-- abbrev Witness (Data Randomness : Type) := Data × Randomness
4546

46-
structure Scheme (pSpec : ProtocolSpec n) (oSpec : OracleSpec ι) (Data : Type) [O : OracleInterface Data]
47-
(Randomness Commitment : Type) extends
48-
Commit oSpec Data Randomness Commitment,
49-
Opening pSpec oSpec Data Randomness Commitment
47+
structure Scheme extends
48+
Commit oSpec Data Randomness Commitment,
49+
Opening oSpec Data Randomness Commitment pSpec
5050

5151
section Security
5252

5353
noncomputable section
5454

5555
open scoped NNReal
5656

57-
variable {pSpec : ProtocolSpec n} [∀ i, VCVCompatible (pSpec.Challenge i)] [DecidableEq ι]
58-
{oSpec : OracleSpec ι} {Data : Type} [O : OracleInterface Data] {Randomness : Type} [Fintype Randomness]
59-
{Commitment : Type} [oSpec.FiniteRange]
57+
variable [∀ i, VCVCompatible (pSpec.Challenge i)] [DecidableEq ι]
58+
{oSpec : OracleSpec ι} {Data : Type} [O : OracleInterface Data] {Randomness : Type}
59+
[Fintype Randomness]
60+
{Commitment : Type} [oSpec.FiniteRange] {n : ℕ} {pSpec : ProtocolSpec n}
61+
[∀ i, VCVCompatible (pSpec.Challenge i)]
6062

6163
/-- A commitment scheme satisfies **correctness** with error `correctnessError` if for all
6264
`data : Data`, `randomness : Randomness`, and `query : O.Query`, the probability of accepting upon
6365
executing the commitment and opening procedures honestly is at least `1 - correctnessError`. -/
64-
def correctness (scheme : Scheme pSpec oSpec Data Randomness Commitment)
66+
def correctness (scheme : Scheme oSpec Data Randomness Commitment pSpec)
6567
(correctnessError : ℝ≥0) : Prop :=
6668
∀ data : Data,
6769
∀ randomness : Randomness,
@@ -72,14 +74,15 @@ def correctness (scheme : Scheme pSpec oSpec Data Randomness Commitment)
7274
return result] ≥ 1 - correctnessError
7375

7476
/-- A commitment scheme satisfies **perfect correctness** if it satisfies correctness with no error.
75-
-/
76-
def perfectCorrectness (scheme : Scheme pSpec oSpec Data Randomness Commitment) : Prop :=
77+
-/
78+
def perfectCorrectness (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop :=
7779
correctness scheme 0
7880

7981
/-- An adversary in the (evaluation) binding game returns a commitment `cm`, a query `q`, two
8082
purported responses `r₁, r₂` to the query, and an auxiliary private state (to be passed to the
8183
malicious prover in the opening procedure). -/
82-
def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type) [O : OracleInterface Data] :=
84+
def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type)
85+
[O : OracleInterface Data] :=
8386
OracleComp oSpec (Commitment × O.Query × O.Response × O.Response × AuxState)
8487

8588
/-- A commitment scheme satisfies **(evaluation) binding** with error `bindingError` if for all
@@ -94,11 +97,11 @@ def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type) [
9497
9598
Informally, evaluation binding says that it's computationally infeasible to open a commitment to
9699
two different responses for the same query. -/
97-
def binding (scheme : Scheme pSpec oSpec Data Randomness Commitment)
100+
def binding (scheme : Scheme oSpec Data Randomness Commitment pSpec)
98101
(bindingError : ℝ≥0): Prop :=
99102
∀ AuxState : Type,
100103
∀ adversary : BindingAdversary oSpec Data Commitment AuxState,
101-
∀ prover : Prover pSpec oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit,
104+
∀ prover : Prover oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit pSpec,
102105
False
103106
-- [ fun ⟨x, x', b₁, b₂⟩ => x ≠ x' ∧ b₁ ∧ b₂ | do
104107
-- let result ← liftM adversary
@@ -133,12 +136,12 @@ def ExtractabilityAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState :
133136
Informally, extractability says that if an adversary can convince the verifier to accept an
134137
opening, then the extractor must be able to recover some underlying data that is consistent with
135138
the evaluation query. -/
136-
def extractability (scheme : Scheme pSpec oSpec Data Randomness Commitment)
139+
def extractability (scheme : Scheme oSpec Data Randomness Commitment pSpec)
137140
(extractabilityError : ℝ≥0) : Prop :=
138141
∃ extractor : StraightlineExtractor oSpec Data Commitment,
139142
∀ AuxState : Type,
140143
∀ adversary : ExtractabilityAdversary oSpec Data Commitment AuxState,
141-
∀ prover : Prover pSpec oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit,
144+
∀ prover : Prover oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit pSpec,
142145
False
143146
-- [ fun ⟨b, d, q, r⟩ => b ∧ O.oracle d q = r | do
144147
-- let result ← liftM (simulate loggingOracle ∅ adversary)
@@ -156,7 +159,7 @@ def extractability (scheme : Scheme pSpec oSpec Data Randomness Commitment)
156159
/-- A commitment scheme satisfies **hiding** with error `hidingError` if ....
157160
158161
Note: have to put it as `hiding'` because `hiding` is already used somewhere else. -/
159-
def hiding' (scheme : Scheme pSpec oSpec Data Randomness Commitment) : Prop := sorry
162+
def hiding' (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop := sorry
160163

161164
#check seededOracle
162165

0 commit comments

Comments
 (0)