From a56b9a60c4a085787a7bf1a88340ece14453819a Mon Sep 17 00:00:00 2001 From: erdemkan Date: Sat, 21 Mar 2026 22:07:01 +0300 Subject: [PATCH] fix linter issues --- CompPoly/Univariate/NTT/Forward.lean | 3 +- .../Univariate/NTT/Benchmark.lean | 10 +- .../CompPolyTests/Univariate/NTT/FastMul.lean | 108 ++++++++---------- .../CompPolyTests/Univariate/NTT/Forward.lean | 29 +++-- .../CompPolyTests/Univariate/NTT/Inverse.lean | 41 +++---- 5 files changed, 91 insertions(+), 100 deletions(-) diff --git a/CompPoly/Univariate/NTT/Forward.lean b/CompPoly/Univariate/NTT/Forward.lean index ab658a2a..90cf8acd 100644 --- a/CompPoly/Univariate/NTT/Forward.lean +++ b/CompPoly/Univariate/NTT/Forward.lean @@ -9,7 +9,8 @@ import CompPoly.Data.Nat.Bitwise /-! # Forward NTT -This file provides spec-level forward NTT definitions together with iterative radix-2 implementation. +This file provides spec-level forward NTT definitions together with an +iterative radix-2 implementation. -/ open scoped BigOperators diff --git a/tests/CompPolyTests/Univariate/NTT/Benchmark.lean b/tests/CompPolyTests/Univariate/NTT/Benchmark.lean index bd49c2a9..ef50ac86 100644 --- a/tests/CompPolyTests/Univariate/NTT/Benchmark.lean +++ b/tests/CompPolyTests/Univariate/NTT/Benchmark.lean @@ -45,7 +45,8 @@ def bestDomainForLength? (requiredLen : Nat) : Option (Domain KoalaBear.Field) : exact Nat.pow_le_pow_right (by decide : 1 ≤ 2) hlogN have hpow_lt : 2 ^ logN < KoalaBear.fieldSize := by have htop : 2 ^ KoalaBear.twoAdicity < KoalaBear.fieldSize := by - native_decide + simpa [KoalaBear.twoAdicity, KoalaBear.fieldSize] using + (by decide : 2 ^ 24 < 2 ^ 31 - 2 ^ 24 + 1) exact lt_of_le_of_lt hpow_le htop have hdiv : KoalaBear.fieldSize ∣ 2 ^ logN := by exact (ZMod.natCast_eq_zero_iff (2 ^ logN) KoalaBear.fieldSize).mp hzero @@ -109,8 +110,11 @@ def timeRepeated {α : Type} (reps : Nat) (f : Unit → α) : IO (Nat × α) := let winner := if nttMs ≤ rawMs then "NTT" else "raw" if crossover?.isNone && nttMs ≤ rawMs then crossover? := some n - IO.println - s!"{n} | {reps} | {benchDomain.logN} | {benchDomain.n} | {avgMsString nttMs reps} | {avgMsString rawMs reps} | {winner} | {speedupString nttMs rawMs}x" + let row := + s!"{n} | {reps} | {benchDomain.logN} | {benchDomain.n} | " ++ + s!"{avgMsString nttMs reps} | {avgMsString rawMs reps} | " ++ + s!"{winner} | {speedupString nttMs rawMs}x" + IO.println row match crossover? with | some n => IO.println s!"first measured crossover: NTT wins at size {n}" | none => IO.println "no measured crossover in this sweep" diff --git a/tests/CompPolyTests/Univariate/NTT/FastMul.lean b/tests/CompPolyTests/Univariate/NTT/FastMul.lean index ac862d4d..b4797b6f 100644 --- a/tests/CompPolyTests/Univariate/NTT/FastMul.lean +++ b/tests/CompPolyTests/Univariate/NTT/FastMul.lean @@ -19,71 +19,63 @@ namespace FastMulTests open TestCommon -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(0 : KoalaBear.Field)] - let q : CPolynomial.Raw KoalaBear.Field := #[(5 : KoalaBear.Field), 7, 9] - FastMul.fastMulImpl testDomain p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(0 : KoalaBear.Field)] + let q : CPolynomial.Raw KoalaBear.Field := #[(5 : KoalaBear.Field), 7, 9] + FastMul.fastMulImpl testDomain p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 4, 5] - let q : CPolynomial.Raw KoalaBear.Field := #[(7 : KoalaBear.Field), 2] - FastMul.fastMulImpl testDomain p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 4, 5] + let q : CPolynomial.Raw KoalaBear.Field := #[(7 : KoalaBear.Field), 2] + FastMul.fastMulImpl testDomain p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 3, 4, 5] - let q : CPolynomial.Raw KoalaBear.Field := #[(6 : KoalaBear.Field), 7, 8, 9] - FastMul.fastMulImpl testDomain p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 3, 4, 5] + let q : CPolynomial.Raw KoalaBear.Field := #[(6 : KoalaBear.Field), 7, 8, 9] + FastMul.fastMulImpl testDomain p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 0, 0] - let q : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 0, 4, 0] - FastMul.fastMulImpl testDomain p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 0, 0] + let q : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 0, 4, 0] + FastMul.fastMulImpl testDomain p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 3, 4, 5, 6] - let q : CPolynomial.Raw KoalaBear.Field := #[(7 : KoalaBear.Field), 8, 9, 10, 11] - FastMul.fastMulImpl testDomain32 p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 3, 4, 5, 6] + let q : CPolynomial.Raw KoalaBear.Field := #[(7 : KoalaBear.Field), 8, 9, 10, 11] + FastMul.fastMulImpl testDomain32 p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[ - (1 : KoalaBear.Field), 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 - ] - let q : CPolynomial.Raw KoalaBear.Field := #[ - (11 : KoalaBear.Field), 10, 9, 8, 7, 6, 5, 4, 3, 2, 1 - ] - FastMul.fastMulImpl testDomain32 p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[ + (1 : KoalaBear.Field), 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 + ] + let q : CPolynomial.Raw KoalaBear.Field := #[ + (11 : KoalaBear.Field), 10, 9, 8, 7, 6, 5, 4, 3, 2, 1 + ] + FastMul.fastMulImpl testDomain32 p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[ - (2 : KoalaBear.Field), 4, 6, 8, 10, 12, 14, 16, - 18, 20, 22, 24, 26, 28, 30, 32 - ] - let q : CPolynomial.Raw KoalaBear.Field := #[ - (1 : KoalaBear.Field), 3, 5, 7, 9, 11, 13, 15, - 17, 19, 21, 23, 25, 27, 29, 31 - ] - FastMul.fastMulImpl testDomain32 p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[ + (2 : KoalaBear.Field), 4, 6, 8, 10, 12, 14, 16, + 18, 20, 22, 24, 26, 28, 30, 32 + ] + let q : CPolynomial.Raw KoalaBear.Field := #[ + (1 : KoalaBear.Field), 3, 5, 7, 9, 11, 13, 15, + 17, 19, 21, 23, 25, 27, 29, 31 + ] + FastMul.fastMulImpl testDomain32 p q == p * q -example : - let p : CPolynomial.Raw KoalaBear.Field := #[ - (1 : KoalaBear.Field), 2, 3, 4, 5, 6, 7, - 8, 9, 10, 11, 12, 13, 14, - 15, 16, 17, 18, 19, 20, 21 - ] - let q : CPolynomial.Raw KoalaBear.Field := #[ - (21 : KoalaBear.Field), 20, 19, 18, 17, 16, 15, - 14, 13, 12, 11, 10, 9, 8, - 7, 6, 5, 4, 3, 2, 1 - ] - FastMul.fastMulImpl testDomain64 p q = p * q := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[ + (1 : KoalaBear.Field), 2, 3, 4, 5, 6, 7, + 8, 9, 10, 11, 12, 13, 14, + 15, 16, 17, 18, 19, 20, 21 + ] + let q : CPolynomial.Raw KoalaBear.Field := #[ + (21 : KoalaBear.Field), 20, 19, 18, 17, 16, 15, + 14, 13, 12, 11, 10, 9, 8, + 7, 6, 5, 4, 3, 2, 1 + ] + FastMul.fastMulImpl testDomain64 p q == p * q end FastMulTests end NTT diff --git a/tests/CompPolyTests/Univariate/NTT/Forward.lean b/tests/CompPolyTests/Univariate/NTT/Forward.lean index 7a4f0416..997e07c6 100644 --- a/tests/CompPolyTests/Univariate/NTT/Forward.lean +++ b/tests/CompPolyTests/Univariate/NTT/Forward.lean @@ -19,22 +19,19 @@ namespace ForwardTests open TestCommon -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 4, 5] - Forward.forwardImpl testDomain p = Forward.forwardSpec testDomain p := by - native_decide - -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 0, 0] - Forward.forwardImpl testDomain p = Forward.forwardSpec testDomain p := by - native_decide - -example : - let p : CPolynomial.Raw KoalaBear.Field := #[ - (1 : KoalaBear.Field), 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 - ] - Forward.forwardImpl testDomain32 p = Forward.forwardSpec testDomain32 p := by - native_decide +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 4, 5] + Forward.forwardImpl testDomain p == Forward.forwardSpec testDomain p + +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(1 : KoalaBear.Field), 2, 0, 0] + Forward.forwardImpl testDomain p == Forward.forwardSpec testDomain p + +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[ + (1 : KoalaBear.Field), 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 + ] + Forward.forwardImpl testDomain32 p == Forward.forwardSpec testDomain32 p end ForwardTests end NTT diff --git a/tests/CompPolyTests/Univariate/NTT/Inverse.lean b/tests/CompPolyTests/Univariate/NTT/Inverse.lean index c983d08d..001b6fff 100644 --- a/tests/CompPolyTests/Univariate/NTT/Inverse.lean +++ b/tests/CompPolyTests/Univariate/NTT/Inverse.lean @@ -19,28 +19,25 @@ namespace InverseTests open TestCommon -example : - let v : Array KoalaBear.Field := #[ - (1 : KoalaBear.Field), 4, 2, 7, 3, 6, 5, 8 - ] - Inverse.inverseImpl testDomain v = Inverse.inverseSpec testDomain v := by - native_decide - -example : - let p : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 4, 5] - let v := Forward.forwardSpec testDomain p - Inverse.inverseImpl testDomain v = Inverse.inverseSpec testDomain v := by - native_decide - -example : - let v : Array KoalaBear.Field := #[ - (1 : KoalaBear.Field), 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 - ] - Inverse.inverseImpl testDomain32 v = Inverse.inverseSpec testDomain32 v := by - native_decide +#guard + let v : Array KoalaBear.Field := #[ + (1 : KoalaBear.Field), 4, 2, 7, 3, 6, 5, 8 + ] + Inverse.inverseImpl testDomain v == Inverse.inverseSpec testDomain v + +#guard + let p : CPolynomial.Raw KoalaBear.Field := #[(3 : KoalaBear.Field), 4, 5] + let v := Forward.forwardSpec testDomain p + Inverse.inverseImpl testDomain v == Inverse.inverseSpec testDomain v + +#guard + let v : Array KoalaBear.Field := #[ + (1 : KoalaBear.Field), 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 + ] + Inverse.inverseImpl testDomain32 v == Inverse.inverseSpec testDomain32 v end InverseTests end NTT