forked from Verified-zkEVM/ArkLib
-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathArkLib.lean
More file actions
71 lines (71 loc) · 3 KB
/
ArkLib.lean
File metadata and controls
71 lines (71 loc) · 3 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
import ArkLib.AGM.Basic
import ArkLib.CommitmentScheme.Basic
import ArkLib.CommitmentScheme.Fold
import ArkLib.CommitmentScheme.MerkleTree
import ArkLib.CommitmentScheme.SimpleRO
import ArkLib.CommitmentScheme.Tensor
import ArkLib.CommitmentScheme.Trivial
import ArkLib.Data.CodingTheory
import ArkLib.Data.EllipticCurve.BN254
import ArkLib.Data.FieldTheory.BinaryTowerField.Basic
import ArkLib.Data.FieldTheory.BinaryTowerField.Prelude
import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_377
import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_381
import ArkLib.Data.FieldTheory.NonBinaryField.BN254
import ArkLib.Data.FieldTheory.NonBinaryField.BabyBear
import ArkLib.Data.FieldTheory.NonBinaryField.Basic
import ArkLib.Data.FieldTheory.NonBinaryField.Goldilocks
import ArkLib.Data.FieldTheory.NonBinaryField.Mersenne
import ArkLib.Data.FieldTheory.NonBinaryField.Secp256k1
import ArkLib.Data.Fin.Basic
import ArkLib.Data.Math.Basic
import ArkLib.Data.Math.DepCast
import ArkLib.Data.Math.HList
import ArkLib.Data.MlPoly.Basic
import ArkLib.Data.MlPoly.Equiv
import ArkLib.Data.MvPolynomial.Degrees
import ArkLib.Data.MvPolynomial.Interpolation
import ArkLib.Data.MvPolynomial.Multilinear
import ArkLib.Data.MvPolynomial.Notation
import ArkLib.Data.MvPolynomial.Sumcheck
import ArkLib.Data.Polynomial.EvenAndOdd
import ArkLib.Data.Probability.Instances
import ArkLib.Data.Probability.Notation
import ArkLib.Data.UniPoly.Basic
import ArkLib.Data.UniPoly.BasicOld
import ArkLib.Data.UniPoly.PolynomialReflection
import ArkLib.OracleReduction.Basic
import ArkLib.OracleReduction.Cast
import ArkLib.OracleReduction.Composition.Parallel.Basic
import ArkLib.OracleReduction.Composition.Sequential.Append
import ArkLib.OracleReduction.Composition.Sequential.General
import ArkLib.OracleReduction.Composition.Sequential.ProtocolSpec
import ArkLib.OracleReduction.Equiv
import ArkLib.OracleReduction.Execution
import ArkLib.OracleReduction.LiftContext.Basic
import ArkLib.OracleReduction.OracleInterface
import ArkLib.OracleReduction.Prelude
import ArkLib.OracleReduction.Security.Basic
import ArkLib.OracleReduction.Transform.BCS
import ArkLib.OracleReduction.Transform.FiatShamir
import ArkLib.OracleReduction.VectorIOR
import ArkLib.ProofSystem.Component.CheckPred
import ArkLib.ProofSystem.Component.RandomQuery
import ArkLib.ProofSystem.Component.SendClaim
import ArkLib.ProofSystem.Component.SendWitness
import ArkLib.ProofSystem.ConstraintSystem.IndexedLookup
import ArkLib.ProofSystem.ConstraintSystem.Plonk
import ArkLib.ProofSystem.ConstraintSystem.R1CS
import ArkLib.ProofSystem.DSL
import ArkLib.ProofSystem.Fri.RoundConsistency
import ArkLib.ProofSystem.Plonk.Basic
import ArkLib.ProofSystem.Spartan.Basic
import ArkLib.ProofSystem.Sumcheck.Basic
import ArkLib.ProofSystem.Sumcheck.SingleRound
import ArkLib.ToMathlib.BigOperators.Fin
import ArkLib.ToMathlib.Finset.Basic
import ArkLib.ToMathlib.Finsupp.Fin
import ArkLib.ToMathlib.MvPolynomial.Equiv
import ArkLib.ToMathlib.NumberTheory.PrattCertificate
import ArkLib.ToMathlib.UInt.Equiv
import ArkLib.ToVCVio.Oracle