feat: rename oracle => answer in OracleInterface (Verified-zkEVM#134)

* rename `oracle` => `answer` in OracleInterface

* fix

* fix lint

* delete tree, no longer needed

* update import

* remove binary tree stuff

Author: quangvdao

ArkLib.lean

@@ -97,8 +97,6 @@ import ArkLib.Data.Polynomial.RationalFunctions
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.Probability.Notation
 import ArkLib.Data.RingTheory.TowerOfAlgebra
-import ArkLib.Data.Tree.Binary
-import ArkLib.Data.Tree.General
 import ArkLib.Data.UniPoly.Basic
 import ArkLib.Data.UniPoly.BasicOld
 import ArkLib.Data.UniPoly.PolynomialReflection

ArkLib/CommitmentScheme/Basic.lean

@@ -25,6 +25,9 @@ import ArkLib.OracleReduction.Security.Basic
   security definitions for commitment schemes have to be stated differently than those for IOPs.
 -/
 
+-- Note: remove this once we properly define the security definitions for commitment schemes
+set_option linter.unusedVariables false
+
 namespace Commitment
 
 open OracleSpec OracleComp SubSpec
@@ -70,7 +73,7 @@ def correctness (scheme : Scheme oSpec Data Randomness Commitment pSpec)
   ∀ query : O.Query,
     [ fun x => x.2.1 | do
         let cm ← liftComp (scheme.commit data randomness) _
-        let ⟨result, _⟩ ← scheme.opening.run ⟨cm, query, O.oracle data query⟩ ⟨data, randomness⟩
+        let ⟨result, _⟩ ← scheme.opening.run ⟨cm, query, O.answer data query⟩ ⟨data, randomness⟩
         return result] ≥ 1 - correctnessError
 
 /-- A commitment scheme satisfies **perfect correctness** if it satisfies correctness with no error.
@@ -98,7 +101,7 @@ def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type)
   Informally, evaluation binding says that it's computationally infeasible to open a commitment to
   two different responses for the same query. -/
 def binding (scheme : Scheme oSpec Data Randomness Commitment pSpec)
-    (bindingError : ℝ≥0): Prop :=
+    (bindingError : ℝ≥0) : Prop :=
   ∀ AuxState : Type,
   ∀ adversary : BindingAdversary oSpec Data Commitment AuxState,
   ∀ prover : Prover oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit pSpec,
@@ -129,7 +132,7 @@ def ExtractabilityAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState :
     opening procedure that takes in `st`, the probability that:
 
   1. The verifier accepts in the opening procedure given `cm, q, r`
-  2. The extracted data `d` is inconsistent with the claimed response (i.e., `O.oracle d q ≠ r`)
+  2. The extracted data `d` is inconsistent with the claimed response (i.e., `O.answer d q ≠ r`)
 
   is at most `extractabilityError`.
 
@@ -143,7 +146,7 @@ def extractability (scheme : Scheme oSpec Data Randomness Commitment pSpec)
   ∀ adversary : ExtractabilityAdversary oSpec Data Commitment AuxState,
   ∀ prover : Prover oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit pSpec,
     False
-    -- [ fun ⟨b, d, q, r⟩ => b ∧ O.oracle d q = r | do
+    -- [ fun ⟨b, d, q, r⟩ => b ∧ O.answer d q = r | do
     --     let result ← liftM (simulate loggingOracle ∅ adversary)
     --     let ⟨⟨cm, query, response, st⟩, queryLog⟩ := result
     --     let proof : Proof pSpec oSpec (Commitment × O.Query × O.Response) AuxState :=

ArkLib/CommitmentScheme/MerkleTree.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Quang Dao
 -/
 
-import ArkLib.Data.Tree.Binary
 import Mathlib.Data.Vector.Snoc
 import VCVio.OracleComp.QueryTracking.CachingOracle
 
@@ -313,49 +312,3 @@ section Test
 end Test
 
 end MerkleTree
-
--- Alternative definition of Merkle tree using inductive type
-
-variable {α : Type}
-
-/-- Helper function to get the proof for a value at a given path. -/
-def getProofHelper [DecidableEq α] : List Bool → BinaryTree α → List α
-  | _, BinaryTree.nil => []
-  | _, BinaryTree.leaf _ => []
-  | [], BinaryTree.node _ _ _ => []
-  | false :: rest, BinaryTree.node _ l r =>
-    match BinaryTree.getRoot r with
-    | none => getProofHelper rest l
-    | some v => v :: getProofHelper rest l
-  | true :: rest, BinaryTree.node _ l r =>
-    match BinaryTree.getRoot l with
-    | none => getProofHelper rest r
-    | some v => v :: getProofHelper rest r
-
-/-- Generate a Merkle proof for a leaf with value 'a'.
-    The proof consists of the sibling hashes needed to recompute the root. -/
-def generateProof [DecidableEq α] (a : α) (tree : BinaryTree α) : Option (List α) :=
-  match BinaryTree.findPath a tree with
-  | none => none
-  | some path => some (getProofHelper path tree)
-
-/-- Verify a Merkle proof that a value 'a' is in the tree with root 'root'.
-    The 'proof' contains sibling hashes, and 'path' is the position (left/right) at each level. -/
-def verifyProof [DecidableEq α] (hashFn : α → α → α) (a : α) (root : α)
-    (proof : List α) (path : List Bool) : Bool :=
-  let rec verify (current : α) (p : List α) (dirs : List Bool) : Bool :=
-    match p, dirs with
-    | [], [] => current = root
-    | sibling :: restProof, dir :: restPath =>
-      let nextHash := if dir then hashFn sibling current else hashFn current sibling
-      verify nextHash restProof restPath
-    | _, _ => false -- Proof and path lengths don't match
-  verify a proof path
-
--- /-- Build a Merkle tree from a list of leaves using a hash function. -/
--- def buildMerkleTree [DecidableEq α] [Inhabited α]
---     (hashFn : α → α → α) (leaves : List α) : BinaryTree α :=
---   -- Find the smallest power of 2 that fits all leaves
---   -- We can estimate 2^n >= leaves.length by using n = ceiling(log2(leaves.length))
---   let n := Nat.ceil (Nat.log 2 (leaves.length + 1)) -- Ceiling of log base 2
---   LeafTree.toMerkleTree hashFn (LeafTree.fromList n leaves)

ArkLib/CommitmentScheme/SimpleRO.lean

@@ -53,7 +53,7 @@ def verify [BEq γ] (cm : γ) (v : α) (r : β) : OracleComp (ROspec α β γ) U
 local instance : OracleInterface α where
   Query := Unit
   Response := α
-  oracle := fun x _ => x
+  answer := fun x _ => x
 
 def commitmentScheme : Commitment.Scheme (oSpec α β γ) α β γ !p[] where
   commit := fun v r => commit v

ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean

@@ -2162,7 +2162,7 @@ theorem concreteTowerAlgebraMap_assoc :
 **Formalization of Cross - Level Algebra**  : For any `k ≤ τ`, `ConcreteBTField τ` is an
 algebra over `ConcreteBTField k`.
 -/
-instance instAssocTowerOfAlgebraConcreteBTF: AssocTowerOfAlgebra (ConcreteBTField) where
+instance instAssocTowerOfAlgebraConcreteBTF : AssocTowerOfAlgebra (ConcreteBTField) where
   towerAlgebraMap := concreteTowerAlgebraMap
   smul := fun i j h => by
     exact (concreteTowerAlgebraMap i j h).toAlgebra.toSMul -- derive same smul from algebra
@@ -2585,7 +2585,7 @@ theorem PowerBasis.cast_basis_succ_of_eq_rec_apply
   -- The proof of the theorem itself remains simple.
   subst h_r
   simp only [ConcreteBTFieldAlgebra_id,
-    Algebra.id.map_eq_id, PowerBasis.coe_basis, Fin.coe_cast, RingHom.id_apply]
+    Algebra.algebraMap_self, PowerBasis.coe_basis, Fin.coe_cast, RingHom.id_apply]
   rw [Basis_cast_index_apply (h_eq:=by
     exact powerBasisSucc_dim r1) (h_le:=by omega)]
   simp only [PowerBasis.coe_basis, Fin.coe_cast]
@@ -2771,12 +2771,12 @@ noncomputable def towerEquiv_zero : RingEquiv (R:=GF(2)) (S:=ConcreteBTField 0)
       · simp only [y_zero, or_true, ↓reduceIte]
       · simp only [y_one, one_ne_zero, or_false, ↓reduceIte]
 }
-noncomputable def towerRingEquiv0: BTField 0 ≃+* ConcreteBTField 0 := by
+noncomputable def towerRingEquiv0 : BTField 0 ≃+* ConcreteBTField 0 := by
   apply RingEquiv.trans (R:=BTField 0) (S:=GF(2)) (S':=ConcreteBTField 0)
   · exact RingEquiv.refl (BTField 0)
   · exact towerEquiv_zero
 
-noncomputable def towerRingEquivFromConcrete0: ConcreteBTField 0 ≃+* BTField 0 := by
+noncomputable def towerRingEquivFromConcrete0 : ConcreteBTField 0 ≃+* BTField 0 := by
   exact towerRingEquiv0.symm
 
 noncomputable def towerRingHomForwardMap (k : ℕ) : ConcreteBTField k → BTField k := by
@@ -2818,10 +2818,10 @@ lemma towerRingHomForwardMap0_eq :
   simp only [RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, ↓reduceDIte]
 
 structure TowerEquivResult (k : ℕ) where
-  ringEquiv: ConcreteBTField k ≃+* BTField k
-  ringEquivForwardMapEq: ringEquiv = towerRingHomForwardMap k
-  mapGenerator: (towerRingHomForwardMap k) (Z k) = BinaryTower.Z k
-  mapSplit: (h_pos: k > 0) → ∀ x : ConcreteBTField k, ringEquiv.toFun (x) =
+  ringEquiv : ConcreteBTField k ≃+* BTField k
+  ringEquivForwardMapEq : ringEquiv = towerRingHomForwardMap k
+  mapGenerator : (towerRingHomForwardMap k) (Z k) = BinaryTower.Z k
+  mapSplit : (h_pos: k > 0) → ∀ x : ConcreteBTField k, ringEquiv.toFun x =
     BinaryTower.join_via_add_smul (k:=k) (h_pos:=h_pos) (hi_btf := by
       have hi_btf := (split (k:=k) (h:=h_pos) x).fst
       exact towerRingHomForwardMap (k:=k-1) hi_btf
@@ -2876,7 +2876,7 @@ noncomputable def towerEquiv (n : ℕ) : TowerEquivResult n := by
       mapSplit := fun h_pos x => by sorry
     }
 
-noncomputable instance instAssocTowerOfAlgebraEquiv: AssocTowerOfAlgebraEquiv
+noncomputable instance instAssocTowerOfAlgebraEquiv : AssocTowerOfAlgebraEquiv
   (ConcreteBTField) (BTField) where
   toRingEquiv := fun i => (towerEquiv i).ringEquiv
   commutesLeft' := fun i j h r => by

ArkLib/Data/FieldTheory/NonBinaryField/Basic.lean

@@ -41,26 +41,26 @@ private lemma coeffs_of_comp_minus_x_pos_degree {f : Polynomial F} {n : ℕ} (h
   · rintro _ _ _ (_ | _) <;> aesop (add simp [Nat.even_add_one, Nat.even_iff])
   · rintro _ _ _ _ (_ | _) <;> aesop
 
-theorem coeffs_of_comp_minus_x {f : Polynomial F} {n : ℕ}  :
+theorem coeffs_of_comp_minus_x {f : Polynomial F} {n : ℕ} :
     (f.comp (-X)).coeff n = if Even n then f.coeff n else -f.coeff n := by
     by_cases hpos : 0 < f.degree
     · rw [coeffs_of_comp_minus_x_pos_degree hpos]
     · have : f.natDegree = 0 := by aesop (add simp natDegree_pos_iff_degree_pos.symm)
       cases n <;> aesop (add simp natDegree_eq_zero)
 
-private lemma comp_x_square_coeff_pos_deg {f : Polynomial F} {n : ℕ} (h : 0 < f.degree):
+private lemma comp_x_square_coeff_pos_deg {f : Polynomial F} {n : ℕ} (h : 0 < f.degree) :
   (f.comp (X * X)).coeff n = if Even n then f.coeff (n / 2) else 0 := by
   revert n
   apply degree_pos_induction_on (h0 := h) (P := fun f => _)
-  · rintro _ _ (_ | n) <;> 
+  · rintro _ _ (_ | n) <;>
     aesop (add simp [coeff_X, Even]) (add safe [(by existsi 1), (by omega)])
   · rintro _ _ _ (_ | _ | n) <;> try simp [←mul_assoc]
     have : (n + 1 + 1) / 2 = n / 2 + 1 := by omega
     split <;> aesop (add safe (by omega)) (add simp [Nat.even_iff])
   · rintro _ _ _ _ (_ | _ | n) <;> try simp_all
     have : (n + 1 + 1) / 2 = n / 2 + 1 := by omega
     simp_all only [coeff_C_succ, add_zero]
-    
+
 theorem comp_x_square_coeff {f : Polynomial F} {n : ℕ} :
   (f.comp (X * X)).coeff n = if Even n then f.coeff (n / 2) else 0 := by
   by_cases hpos : 0 < f.degree
@@ -74,7 +74,7 @@ theorem comp_x_square_coeff {f : Polynomial F} {n : ℕ} :
 lemma eq_poly_deg_one {a b c d : F} {x₁ x₂ : F}
   (h1 : a + b * x₁ = c + d * x₁)
   (h2 : a + b * x₂ = c + d * x₂)
-  (h1_2 : x₁ ≠ x₂):
+  (h1_2 : x₁ ≠ x₂) :
   Polynomial.C a + Polynomial.C b * Polynomial.X
     = Polynomial.C c + Polynomial.C d * Polynomial.X := by
   by_cases h_b_d : b = d

ArkLib/Data/MlPoly/Basic.lean

@@ -60,7 +60,7 @@ instance inhabited [Inhabited R] : Inhabited (MlPoly R n) := by simp [MlPoly]; i
 /-- Conform a list of coefficients to a `MlPoly` with a given number of variables.
     May either pad with zeros or truncate. -/
 @[inline]
-def ofArray [Zero R] (coeffs : Array R) (n : ℕ): MlPoly R n :=
+def ofArray [Zero R] (coeffs : Array R) (n : ℕ) : MlPoly R n :=
   .ofFn (fun i => if h : i.1 < coeffs.size then coeffs[i] else 0)
   -- ⟨((coeffs.take (2 ^ n)).rightpad (2 ^ n) 0 : Array R), by simp⟩
   -- Not sure which is better performance wise?
@@ -190,7 +190,7 @@ instance inhabited [Inhabited R] : Inhabited (MlPolyEval R n) := by
 /-- Conform a list of coefficients to a `MlPolyEval` with a given number of variables.
     May either pad with zeros or truncate. -/
 @[inline]
-def ofArray [Zero R] (coeffs : Array R) (n : ℕ): MlPolyEval R n :=
+def ofArray [Zero R] (coeffs : Array R) (n : ℕ) : MlPolyEval R n :=
   .ofFn (fun i => if h : i.1 < coeffs.size then coeffs[i] else 0)
   -- ⟨((coeffs.take (2 ^ n)).rightpad (2 ^ n) 0 : Array R), by simp⟩
   -- Not sure which is better performance wise?
@@ -409,7 +409,7 @@ lemma forwardRange_getElem (n : ℕ) (r : Fin n) (l : Fin (r.val + 1)) (k : Fin
   simp only [List.get_eq_getElem]
   simp only [List.getElem_ofFn]
 
-lemma forwardRange_succ_right_ne_empty (n : ℕ) (r : Fin (n-1)) (l : Fin (r.val + 1)) :
+lemma forwardRange_succ_right_ne_empty (n : ℕ) (r : Fin (n - 1)) (l : Fin (r.val + 1)) :
   forwardRange n ⟨r + 1, by omega⟩ ⟨l, by simp only; omega⟩ ≠ [] := by
   rw [forwardRange]
   simp only [List.ofFn_succ, Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero, Fin.val_succ, ne_eq,
@@ -421,7 +421,7 @@ lemma forwardRange_pred_le_ne_empty (n : ℕ) (r : Fin n) (l : Fin (r.val + 1))
   simp only [List.ofFn_succ, Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero, Fin.val_succ, ne_eq,
     reduceCtorEq, not_false_eq_true]
 
-lemma forwardRange_dropLast (n : ℕ) (r : Fin (n-1)) (l : Fin (r.val + 1)) :
+lemma forwardRange_dropLast (n : ℕ) (r : Fin (n - 1)) (l : Fin (r.val + 1)) :
     (forwardRange n ⟨r + 1, by omega⟩ ⟨l, by simp only; omega⟩).dropLast
     = forwardRange n ⟨r, by omega⟩ ⟨l, by simp only [Fin.is_lt]⟩ := by
   apply List.ext_getElem
@@ -494,7 +494,7 @@ def lagrangeToMono_segment (n : ℕ) (r : Fin n) (l : Fin (r.val + 1)) :
   let range := forwardRange n r l
   (range.foldr (fun h acc => lagrangeToMonoLevel h acc))
 
-lemma monoToLagrange_eq_monoToLagrange_segment (n: ℕ) [NeZero n] (v: Vector R (2 ^ n)) :
+lemma monoToLagrange_eq_monoToLagrange_segment (n : ℕ) [NeZero n] (v : Vector R (2 ^ n)) :
   have h_n_ne_zero: n ≠ 0 := by exact NeZero.ne n
   monoToLagrange n v = monoToLagrange_segment n (r:=⟨n - 1, by omega⟩) (l:=⟨0, by omega⟩) v := by
   have h_n_ne_zero: n ≠ 0 := by exact NeZero.ne n
@@ -503,7 +503,7 @@ lemma monoToLagrange_eq_monoToLagrange_segment (n: ℕ) [NeZero n] (v: Vector R
   congr
   exact Eq.symm (forwardRange_0_eq_finRange n)
 
-lemma lagrangeToMono_eq_lagrangeToMono_segment (n: ℕ) [NeZero n] (v: Vector R (2 ^ n)) :
+lemma lagrangeToMono_eq_lagrangeToMono_segment (n : ℕ) [NeZero n] (v : Vector R (2 ^ n)) :
   have h_n_ne_zero: n ≠ 0 := by exact NeZero.ne n
   lagrangeToMono n v = lagrangeToMono_segment n (r:=⟨n - 1, by omega⟩) (l:=⟨0, by omega⟩) v := by
   have h_n_ne_zero: n ≠ 0 := by exact NeZero.ne n
@@ -512,7 +512,7 @@ lemma lagrangeToMono_eq_lagrangeToMono_segment (n: ℕ) [NeZero n] (v: Vector R
   congr
   exact Eq.symm (forwardRange_0_eq_finRange n)
 
-lemma testBit_of_sub_two_pow_of_bit_1 {n i: ℕ} (h_testBit_eq_1: (n).testBit i = true) :
+lemma testBit_of_sub_two_pow_of_bit_1 {n i : ℕ} (h_testBit_eq_1 : (n).testBit i = true) :
   (n - 2^i).testBit i = false := by
   have h := Nat.testBit_false_eq_getBit_eq_0 (n:=n - 2^i) (k:=i)
   rw [h]

ArkLib/Data/MlPoly/Equiv.lean

@@ -40,7 +40,7 @@ noncomputable def monomialOfNat (i : ℕ) : (Fin n) →₀ ℕ :=
     simp only [ne_eq, Finset.mem_univ, implies_true]) -- the support set is exactly Finset.univ
 
 theorem eq_monomialOfNat_iff_eq_bitRepr (m : Fin n →₀ ℕ)
-  (h_binary : ∀ j: Fin n, m j ≤ 1) (i: Fin (2^n)) :
+  (h_binary : ∀ j : Fin n, m j ≤ 1) (i: Fin (2^n)) :
   monomialOfNat i = m ↔ i = Nat.binaryFinMapToNat m h_binary := by
   constructor
   · intro h_mono_eq
@@ -115,7 +115,7 @@ theorem toMvPolynomial_is_multilinear (p : MlPoly R n) :
     exact Fintype.sum_eq_zero (fun a ↦ 0) (congrFun rfl)
   exact hs h_sum_zero
 
-theorem coeff_of_toMvPolynomial_eq_coeff_of_MlPoly (p : MlPoly R n) (m : Fin n →₀ ℕ):
+theorem coeff_of_toMvPolynomial_eq_coeff_of_MlPoly (p : MlPoly R n) (m : Fin n →₀ ℕ) :
   coeff m (toMvPolynomial p) =
     if h_binary: (∀ j: Fin n, m j ≤ 1) then
       let i_of_m: ℕ := Nat.binaryFinMapToNat (m:=m) (h_binary:=h_binary)

ArkLib/Data/Polynomial/EvenAndOdd.lean

@@ -16,7 +16,7 @@ import ArkLib.Data.FieldTheory.NonBinaryField.Basic
 
 namespace Polynomial
 
-variable {F : Type} [NonBinaryField F]
+variable {F : Type*} [NonBinaryField F]
 
 /-- The even part of a polynomial `f = a_0 + a_1 X + a_2 X² + ...`, which is the polynomial
 
@@ -101,7 +101,7 @@ noncomputable def oddPart_x (f : Polynomial F) : Polynomial F := deevenize (oddP
 -- Merged the `Lemmas` files into here
 section Lemmas
 
-variable {F: Type} [NonBinaryField F]
+variable {F : Type*} [NonBinaryField F]
 
 private noncomputable def evenPart' (f : Polynomial F) : Polynomial F :=
   match f with
@@ -111,7 +111,7 @@ private noncomputable def evenPart' (f : Polynomial F) : Polynomial F :=
   }⟩⟩
 
 @[simp]
-private lemma evenPart'_coeffs {f : Polynomial F} {n : ℕ}:
+private lemma evenPart'_coeffs {f : Polynomial F} {n : ℕ} :
     (evenPart' f).coeff n = if Even n then f.coeff n else 0 := by
   rcases f with ⟨⟨supp, g, h⟩⟩
   simp [evenPart']
@@ -124,7 +124,7 @@ private noncomputable def x_times_oddPart' (f : Polynomial F) : Polynomial F :=
     }⟩⟩
 
 @[simp]
-private lemma x_times_oddPart'_coeff {f : Polynomial F} {n : ℕ}:
+private lemma x_times_oddPart'_coeff {f : Polynomial F} {n : ℕ} :
     (x_times_oddPart' f).coeff n = if Odd n then f.coeff n else 0 := by
   rcases f with ⟨⟨supp, g, h⟩⟩
   simp [x_times_oddPart']
@@ -234,7 +234,7 @@ lemma evenize_eq_comp_x_squared {f : Polynomial F} :
   intro n
   simp [comp_x_square_coeff]
 
-lemma deevenize_comp_x_squared {f : Polynomial F} (hEven : EvenPoly f):
+lemma deevenize_comp_x_squared {f : Polynomial F} (hEven : EvenPoly f) :
     (deevenize f).comp (Polynomial.X * Polynomial.X) = f := by
   apply Polynomial.ext
   intro n
@@ -257,7 +257,7 @@ lemma evenize_is_even {f : Polynomial F} :
   rw [←Nat.not_odd_iff_even] at hEven
   tauto
 
-lemma eq_evenize_deevenize {f : Polynomial F} (hEven : EvenPoly f):
+lemma eq_evenize_deevenize {f : Polynomial F} (hEven : EvenPoly f) :
     evenize (deevenize f) = f := by
   apply Polynomial.ext
   intro n
@@ -280,7 +280,7 @@ lemma deevenize_evenize {f : Polynomial F} :
   apply Polynomial.ext
   simp
 
-lemma evenize_eval {f : Polynomial F} {s : F}:
+lemma evenize_eval {f : Polynomial F} {s : F} :
     (evenize f).eval s = f.eval (s * s) := by
   rw [evenize_eq_comp_x_squared]
   simp [Polynomial.eval_comp, Polynomial.eval_mul]