Operator spacing and docstring clarity in the hashing modules

CompElliptic/Curves/Pasta.lean

@@ -52,9 +52,9 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) :=
 /-- `5` is a quadratic non-residue in the Pallas base field, so `y² = x³ + 5` has no point with
 `x = 0` (Zcash protocol spec §5.4.9.7).
 
-Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (p / 2) ≠ 1`. The LHS (`-1`) is
+Euler's criterion (`ZMod.euler_criterion`) reduces this to `5^(p / 2) ≠ 1`. The LHS (`-1`) is
 evaluated by `reduce_mod_char` (fast modular exponentiation via `NormNum.PowMod`), the same
-machinery the `PrattPartList.prime` legs use for their `a ^ k ≠ 1` conditions. -/
+machinery the `PrattPartList.prime` legs use for their `a^k ≠ 1` conditions. -/
 theorem five_not_isSquare : ¬ IsSquare (5 : PallasBaseField) := by
   rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (5 : PallasBaseField) ≠ 0)]
   reduce_mod_char
@@ -64,7 +64,7 @@ theorem five_not_isSquare : ¬ IsSquare (5 : PallasBaseField) := by
 unambiguously. -/
 theorem no_onCurve_x_zero (y : PallasBaseField) : ¬ OnCurve a b (0, y) := by
   intro h
-  have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
+  have h' : y^2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
 
 /-- `-5` is not a cube in the Pallas base field — the cubic analogue of `five_not_isSquare`, and
@@ -73,7 +73,7 @@ what rules out 2-torsion on the Pallas curve.
 `3 ∣ p - 1`, so `not_exists_pow_eq_of_pow_ne_one` reduces this to the single power
 `(-5)^((p-1)/3)`, which is not `1`. As for `five_not_isSquare`, `reduce_mod_char` (fast modular
 exponentiation) evaluates it and the kernel re-checks the result. -/
-theorem neg_five_not_isCube : ¬ ∃ x : PallasBaseField, x ^ 3 = -(5 : PallasBaseField) := by
+theorem neg_five_not_isCube : ¬ ∃ x : PallasBaseField, x^3 = -(5 : PallasBaseField) := by
   have hcard : Fintype.card PallasBaseField = PALLAS_BASE_CARD := ZMod.card _
   refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) (by decide) ?_
   rw [hcard]
@@ -87,7 +87,7 @@ theorem neg_five_not_isCube : ¬ ∃ x : PallasBaseField, x ^ 3 = -(5 : PallasBa
 not a cube (`neg_five_not_isCube`). Equivalently, the Pallas group has no 2-torsion. -/
 theorem no_onCurve_y_zero (x : PallasBaseField) : ¬ OnCurve a b (x, 0) := by
   intro h
-  have hsum : x ^ 3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm
+  have hsum : x^3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm
   exact neg_five_not_isCube ⟨x, by linear_combination hsum⟩
 
 -- `(-1, 2)` is on the curve: `2² = 4 = (-1)³ + 5`.
@@ -144,7 +144,7 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) :=
 /-- `5` is a quadratic non-residue in the Vesta base field, so `y² = x³ + 5` has no point with
 `x = 0` (Zcash protocol spec §5.4.9.7).
 
-As for Pallas: Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (q / 2) ≠ 1`, and
+As for Pallas: Euler's criterion (`ZMod.euler_criterion`) reduces this to `5^(q / 2) ≠ 1`, and
 `reduce_mod_char` (fast modular exponentiation) evaluates the power to `-1`. -/
 theorem five_not_isSquare : ¬ IsSquare (5 : VestaBaseField) := by
   rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (5 : VestaBaseField) ≠ 0)]
@@ -155,7 +155,7 @@ theorem five_not_isSquare : ¬ IsSquare (5 : VestaBaseField) := by
 unambiguously. -/
 theorem no_onCurve_x_zero (y : VestaBaseField) : ¬ OnCurve a b (0, y) := by
   intro h
-  have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
+  have h' : y^2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
 
 /-- `-5` is not a cube in the Vesta base field — the cubic analogue of `five_not_isSquare`, and
@@ -164,7 +164,7 @@ what rules out 2-torsion on the Vesta curve.
 `3 ∣ q - 1`, so `not_exists_pow_eq_of_pow_ne_one` reduces this to the single power
 `(-5)^((q-1)/3)`, which is not `1`. As for `five_not_isSquare`, `reduce_mod_char` (fast modular
 exponentiation) evaluates it and the kernel re-checks the result. -/
-theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x ^ 3 = -(5 : VestaBaseField) := by
+theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x^3 = -(5 : VestaBaseField) := by
   have hcard : Fintype.card VestaBaseField = PALLAS_SCALAR_CARD := ZMod.card _
   refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) (by decide) ?_
   rw [hcard]
@@ -179,7 +179,7 @@ theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x ^ 3 = -(5 : VestaBase
 a cube (`neg_five_not_isCube`). Equivalently, the Vesta group has no 2-torsion. -/
 theorem no_onCurve_y_zero (x : VestaBaseField) : ¬ OnCurve a b (x, 0) := by
   intro h
-  have hsum : x ^ 3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm
+  have hsum : x^3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm
   exact neg_five_not_isCube ⟨x, by linear_combination hsum⟩
 
 -- `(-1, 2)` is on the curve: `2² = 4 = (-1)³ + 5`.

CompElliptic/Fields/Residue.lean

@@ -30,14 +30,14 @@ parameters.
 
 namespace CompElliptic.Fields
 
-/-- If `n ∣ #F - 1` and `a ^ ((#F - 1) / n) ≠ 1`, then `a` is not an `n`-th power in `F`.
+/-- If `n ∣ #F - 1` and `a^((#F - 1) / n) ≠ 1`, then `a` is not an `n`-th power in `F`.
 
 An `n`-th root `x` of `a` is nonzero along with `a`, so Fermat's little theorem forces
-`a ^ ((#F - 1) / n) = x ^ (n * ((#F - 1) / n)) = x ^ (#F - 1) = 1`. Contrapositively, evaluating
+`a^((#F - 1) / n) = x^(n * ((#F - 1) / n)) = x^(#F - 1) = 1`. Contrapositively, evaluating
 that one power and finding it is not `1` rules out every root at once. -/
 theorem not_exists_pow_eq_of_pow_ne_one {F : Type*} [Field F] [Fintype F] {n : ℕ} {a : F}
     (hn : n ∣ Fintype.card F - 1) (ha : a ≠ 0)
-    (h : a ^ ((Fintype.card F - 1) / n) ≠ 1) : ¬ ∃ x : F, x^n = a := by
+    (h : a^((Fintype.card F - 1) / n) ≠ 1) : ¬ ∃ x : F, x^n = a := by
   -- `n = 0` is already impossible: the exponent `(#F - 1) / 0` is `0`, so `h` reads `1 ≠ 1`.
   have hn0 : n ≠ 0 := by rintro rfl; simp at h
   rintro ⟨x, rfl⟩
@@ -55,51 +55,51 @@ This is Cardano's formula run backwards. A root would split as `x = u + v` with
 `3·u·v = -A`, making `u³` and `v³` the two roots of the resolvent quadratic `t² + q·t - A³/27`;
 `w` is one of those roots, so it would be a cube. The proof stays inside `F`, with no
 splitting field: for a root `x` with `3·x² + A ≠ 0`, setting `r := 3·s/(3·x² + A)` gives
-`((x+r)³ - 8·w)·((x-r)³ - 8·w) = 0` as a polynomial consequence of the hypotheses, so `w` is
-the cube of `(x+r)/2` or of `(x-r)/2`. A root with `3·x² + A = 0` forces `s = 0` and
+`((x + r)³ - 8·w)·((x - r)³ - 8·w) = 0` as a polynomial consequence of the hypotheses, so `w` is
+the cube of `(x + r)/2` or of `(x - r)/2`. A root with `3·x² + A = 0` forces `s = 0` and
 `w = (-x)³` directly.
 
 Over a finite field a cubic with no roots is irreducible. So this lemma, with
 `not_exists_pow_eq_of_pow_ne_one` certifying the non-cube, makes RFC 9380's criterion 3
 checkable by `decide` from two precomputed field elements. -/
 theorem cubic_no_root_of_resolvent_noncube {F : Type*} [Field F]
     (h2 : (2 : F) ≠ 0) (h3 : (3 : F) ≠ 0) {A q s w : F}
-    (hs : 27 * s ^ 2 = 27 * q ^ 2 + 4 * A ^ 3)
-    (hw : 2 * w = -q + s)
-    (hnc : ¬ ∃ u : F, u ^ 3 = w) :
-    ∀ x : F, x ^ 3 + A * x + q ≠ 0 := by
+    (hs : 27 * s^2 = 27 * q^2 + 4 * A^3)
+    (hw : 2*w = -q + s)
+    (hnc : ¬ ∃ u : F, u^3 = w) :
+    ∀ x : F, x^3 + A*x + q ≠ 0 := by
   intro x hx
   have h27 : (27 : F) ≠ 0 := by
     have h := pow_ne_zero 3 h3
     norm_num at h
     exact h
-  by_cases hd : 3 * x ^ 2 + A = 0
+  by_cases hd : 3 * x^2 + A = 0
   · -- A root that is also a critical point: then `s = 0` and `w = (-x)³`, a cube.
-    have hq : q = 2 * x ^ 3 := by linear_combination hx - x * hd
+    have hq : q = 2 * x^3 := by linear_combination hx - x*hd
     have hs0 : s = 0 := by
-      have h0 : 27 * s ^ 2 = 0 := by
-        linear_combination hs + 27 * (q + 2 * x ^ 3) * hq
-          + 4 * (A ^ 2 - 3 * A * x ^ 2 + 9 * x ^ 4) * hd
+      have h0 : 27 * s^2 = 0 := by
+        linear_combination hs + 27 * (q + 2 * x^3) * hq
+          + 4 * (A^2 - 3 * A * x^2 + 9 * x^4) * hd
       exact sq_eq_zero_iff.mp ((mul_eq_zero.mp h0).resolve_left h27)
     refine hnc ⟨-x, mul_left_cancel₀ h2 ?_⟩
     linear_combination -hw + hq - hs0
-  · -- Cardano's split inside `F`: `(x+r)/2` and `(x-r)/2` play the roles of `u` and `v`.
-    obtain ⟨r, hr⟩ : ∃ r : F, r = 3 * s / (3 * x ^ 2 + A) := ⟨_, rfl⟩
-    have hkey : 27 * s ^ 2 = (3 * x ^ 2 + A) ^ 2 * (3 * x ^ 2 + 4 * A) := by
-      linear_combination hs + 27 * (q - x ^ 3 - A * x) * hx
-    have hr3 : 3 * r ^ 2 = 3 * x ^ 2 + 4 * A := by
+  · -- Cardano's split inside `F`: `(x + r)/2` and `(x - r)/2` play the roles of `u` and `v`.
+    obtain ⟨r, hr⟩ : ∃ r : F, r = 3*s / (3 * x^2 + A) := ⟨_, rfl⟩
+    have hkey : 27 * s^2 = (3 * x^2 + A)^2 * (3 * x^2 + 4*A) := by
+      linear_combination hs + 27 * (q - x^3 - A*x) * hx
+    have hr3 : 3 * r^2 = 3 * x^2 + 4*A := by
       rw [hr]
       field_simp
       linear_combination hkey
-    have hpr : 3 * ((x + r) * (x - r)) = -(4 * A) := by linear_combination -hr3
-    have hsum : (x + r) ^ 3 + (x - r) ^ 3 = -(8 * q) := by
-      linear_combination 2 * x * hr3 + 8 * hx
-    have hwq : 108 * (w ^ 2 + q * w) = 4 * A ^ 3 := by
-      linear_combination hs + 27 * (2 * w + q + s) * hw
-    have h0 : 27 * (((x + r) ^ 3 - 8 * w) * ((x - r) ^ 3 - 8 * w)) = 0 := by
+    have hpr : 3 * ((x + r) * (x - r)) = -(4*A) := by linear_combination -hr3
+    have hsum : (x + r)^3 + (x - r)^3 = -(8*q) := by
+      linear_combination 2*x*hr3 + 8*hx
+    have hwq : 108 * (w^2 + q*w) = 4 * A^3 := by
+      linear_combination hs + 27 * (2*w + q + s) * hw
+    have h0 : 27 * (((x + r)^3 - 8*w) * ((x - r)^3 - 8*w)) = 0 := by
       linear_combination
-        (9 * ((x + r) * (x - r)) ^ 2 - 12 * ((x + r) * (x - r)) * A + 16 * A ^ 2) * hpr
-          - 216 * w * hsum + 16 * hwq
+        (9 * ((x + r) * (x - r))^2 - 12 * ((x + r) * (x - r)) * A + 16 * A^2) * hpr
+          - 216*w*hsum + 16*hwq
     rcases mul_eq_zero.mp ((mul_eq_zero.mp h0).resolve_left h27) with h | h
     · refine hnc ⟨(x + r) / 2, ?_⟩
       field_simp

CompElliptic/Fields/Sqrt.lean

@@ -88,9 +88,9 @@ where
 /-- Spec of the `go` accumulator: when some `2^j`-th power of `b2k` (with `j ≤ fuel`) is `1`,
 `go k b2k fuel = k + j₀` where `j₀` is the *least* such exponent. -/
 theorem leastPow2Order.go_spec {F : Type*} [Monoid F] [DecidableEq F] :
-    ∀ (fuel k : ℕ) (b2k : F), (∃ j ≤ fuel, b2k ^ 2^j = 1) →
-      ∃ j ≤ fuel, leastPow2Order.go k b2k fuel = k + j ∧ b2k ^ 2^j = 1 ∧
-        ∀ i < j, b2k ^ 2^i ≠ 1 := by
+    ∀ (fuel k : ℕ) (b2k : F), (∃ j ≤ fuel, b2k^(2^j) = 1) →
+      ∃ j ≤ fuel, leastPow2Order.go k b2k fuel = k + j ∧ b2k^(2^j) = 1 ∧
+        ∀ i < j, b2k^(2^i) ≠ 1 := by
   intro fuel
   induction fuel with
   | zero =>
@@ -101,12 +101,12 @@ theorem leastPow2Order.go_spec {F : Type*} [Monoid F] [DecidableEq F] :
   | succ fuel ih =>
     intro k b2k hex
     obtain ⟨j, hj, hbj⟩ := hex
-    have hconv : ∀ m : ℕ, (b2k * b2k) ^ 2^m = b2k ^ 2^(m+1) := fun m => by
+    have hconv : ∀ m : ℕ, (b2k * b2k)^(2^m) = b2k^(2^(m+1)) := fun m => by
       rw [← pow_two, ← pow_mul, ← pow_succ']
     by_cases hb1 : b2k = 1
     · exact ⟨0, Nat.zero_le _, by simp [leastPow2Order.go, hb1], by simpa using hb1,
         fun i hi => absurd hi (Nat.not_lt_zero i)⟩
-    · have hex' : ∃ j' ≤ fuel, (b2k * b2k) ^ 2^j' = 1 := by
+    · have hex' : ∃ j' ≤ fuel, (b2k * b2k)^(2^j') = 1 := by
         obtain _ | j := j
         · exact absurd (by simpa using hbj) hb1
         · exact ⟨j, by omega, by rw [hconv]; exact hbj⟩
@@ -131,18 +131,18 @@ theorem leastPow2Order_spec {F : Type*} [Monoid F] [DecidableEq F] (b : F) (y :
     · exact h
   have hconv : ∀ m : ℕ, (b*b)^(2^m) = b^(2^(m+1)) := fun m => by
     rw [← pow_two, ← pow_mul, ← pow_succ']
-  have hwit : (b*b)^(2^(y-2)) = 1 := by rw [hconv, show y-2+1 = y-1 from by omega]; exact hy
-  obtain ⟨j, hj, hgo, hbj, hmin⟩ := leastPow2Order.go_spec y 1 (b*b) ⟨y-2, by omega, hwit⟩
+  have hwit : (b*b)^(2^(y - 2)) = 1 := by rw [hconv, show y - 2 + 1 = y-1 from by omega]; exact hy
+  obtain ⟨j, hj, hgo, hbj, hmin⟩ := leastPow2Order.go_spec y 1 (b*b) ⟨y - 2, by omega, hwit⟩
   have hk : leastPow2Order b y = 1 + j := hgo
-  have hjle : j ≤ y-2 := by
-    by_contra h; exact hmin (y-2) (Nat.lt_of_not_le h) hwit
+  have hjle : j ≤ y - 2 := by
+    by_contra h; exact hmin (y - 2) (Nat.lt_of_not_le h) hwit
   have hbk1 : b^(2^j) ≠ 1 := by
     obtain _ | j := j
     · simpa using hb
     · rw [← hconv]; exact hmin j (by omega)
   refine ⟨by omega, by omega, ?_, ?_⟩
   · rw [hk, show (1:ℕ)+j = j+1 from by omega, ← hconv]; exact hbj
-  · rw [hk, show 1+j-1 = j from by omega]; exact hbk1
+  · rw [hk, show 1 + j - 1 = j from by omega]; exact hbk1
 
 /-- Validity of Tonelli–Shanks data for `F`, as a predicate on the *bare components* (mirroring
 `IsCanonical` for encodings): the 2-adic factorization `card - 1 = 2^twoAdicity * oddPart` holds
@@ -219,8 +219,8 @@ theorem loop_sound {F : Type*} [Field F] [DecidableEq F] (a : F) :
       have hy2 : 2 ≤ y := by omega
       set k := leastPow2Order b y with hkdef
       set w := iterSq c (y - k - 1) with hwdef
-      have hw2 : w*w = c^(2^(y-k)) := by
-        rw [hwdef, iterSq_spec, ← pow_add, ← two_mul, ← pow_succ', show y-k-1+1 = y-k from by omega]
+      have hw2 : w*w = c^(2^(y - k)) := by
+        rw [hwdef, iterSq_spec, ← pow_add, ← two_mul, ← pow_succ', show y - k - 1 + 1 = y - k from by omega]
       have hcm1 : c^(2^(y-1)) = -1 := by
         have hne : c^(2^(y-1)) ≠ 1 := by
           intro h
@@ -245,12 +245,12 @@ theorem loop_sound {F : Type*} [Field F] [DecidableEq F] (a : F) :
       have hnewx : (x*w) * (x*w) = a * (b * (w*w)) := by
         rw [show (x*w) * (x*w) = (x*x) * (w*w) from by ring, hx]; ring
       have hnewb : (b * (w*w))^(2^(k-1)) = 1 := by
-        rw [hw2, mul_pow, hbm1, ← pow_mul, ← pow_add, show (y-k) + (k-1) = y-1 from by omega, hcm1]
+        rw [hw2, mul_pow, hbm1, ← pow_mul, ← pow_add, show (y - k) + (k-1) = y-1 from by omega, hcm1]
         ring
       have hnewc : orderOf (w*w) = 2^k := by
-        rw [hw2, orderOf_pow' c (pow_ne_zero (y-k) (by norm_num)), hc,
-            Nat.gcd_eq_right (pow_dvd_pow 2 (by omega : y-k ≤ y)),
-            Nat.pow_div (by omega : y-k ≤ y) (by norm_num), show y - (y-k) = k from by omega]
+        rw [hw2, orderOf_pow' c (pow_ne_zero (y - k) (by norm_num)), hc,
+            Nat.gcd_eq_right (pow_dvd_pow 2 (by omega : y - k ≤ y)),
+            Nat.pow_div (by omega : y - k ≤ y) (by norm_num), show y - (y - k) = k from by omega]
       have hkf : k ≤ fuel := by omega
       simp only [loop, if_neg hb1]
       exact ih (x*w) (b * (w*w)) (w*w) k hkf hnewx hnewb hnewc
@@ -311,7 +311,7 @@ theorem sqrt?_isSome_of_isSquare {F : Type*} [Field F] [Fintype F] [DecidableEq
     exact absurd (by rw [fpow_spec, ← hexp]; exact (FiniteField.isSquare_iff hchar h0).mp ha) h1
 
 /-- A valid `rootOfUnity` is a quadratic non-residue. It has full 2-power order, so its
-Euler power `rootOfUnity ^ ((card-1)/2) = (rootOfUnity ^ (2^(twoAdicity-1)))^oddPart`
+Euler power `rootOfUnity^((card-1)/2) = (rootOfUnity^(2^(twoAdicity-1)))^oddPart`
 evaluates to `(-1)^oddPart = -1`, whereas Euler's criterion gives `1` for a nonzero
 square. This lets a deployment reuse `rootOfUnity` as an auxiliary nonsquare with no
 per-field computation. -/
@@ -329,15 +329,15 @@ theorem rootOfUnity_not_isSquare {F : Type*} [Field F] [Fintype F]
   have hexp : Fintype.card F / 2 = 2^(d.twoAdicity - 1) * d.oddPart := by
     rw [d.valid.card_eq, hpow, mul_assoc]; omega
   -- `rootOfUnity ≠ 0`, since it has a power equal to `1`.
-  have hone : d.rootOfUnity ^ 2^d.twoAdicity = 1 := by
+  have hone : d.rootOfUnity^(2^d.twoAdicity) = 1 := by
     rw [← d.valid.rootOfUnity_order]; exact pow_orderOf_eq_one _
   have hne : d.rootOfUnity ≠ 0 := fun h0 => by
     rw [h0, zero_pow (by positivity : (2:ℕ)^d.twoAdicity ≠ 0)] at hone
     exact zero_ne_one hone
   -- The half power squares to `1` but is not `1` (the order is too big), so it is `-1`.
-  have hhalf : d.rootOfUnity ^ 2^(d.twoAdicity - 1) = -1 := by
-    have hsq1 : d.rootOfUnity ^ 2^(d.twoAdicity - 1)
-        * d.rootOfUnity ^ 2^(d.twoAdicity - 1) = 1 := by
+  have hhalf : d.rootOfUnity^(2^(d.twoAdicity - 1)) = -1 := by
+    have hsq1 : d.rootOfUnity^(2^(d.twoAdicity - 1))
+        * d.rootOfUnity^(2^(d.twoAdicity - 1)) = 1 := by
       rw [← pow_add, ← two_mul, ← hpow]; exact hone
     refine (mul_self_eq_one_iff.mp hsq1).resolve_left fun h1 => ?_
     have hdvd : orderOf d.rootOfUnity ∣ 2^(d.twoAdicity - 1) :=
@@ -347,7 +347,7 @@ theorem rootOfUnity_not_isSquare {F : Type*} [Field F] [Fintype F]
     have := d.valid.twoAdicity_pos
     omega
   -- Euler's power of the square is `1`, but it evaluates to `(-1)^oddPart = -1`.
-  have heuler : d.rootOfUnity ^ (Fintype.card F / 2) = 1 :=
+  have heuler : d.rootOfUnity^(Fintype.card F / 2) = 1 :=
     (FiniteField.isSquare_iff hchar hne).mp hsq
   rw [hexp, pow_mul, hhalf, d.valid.oddPart_odd.neg_one_pow] at heuler
   exact Ring.neg_one_ne_one_of_char_ne_two hchar heuler