Skip to content

Fix NTT test lint violations #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
doran2728 merged 1 commit into from
Mar 21, 2026
Merged

Fix NTT test lint violations #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion CompPoly/Univariate/NTT/Forward.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 7 additions & 3 deletions tests/CompPolyTests/Univariate/NTT/Benchmark.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down
108 changes: 50 additions & 58 deletions tests/CompPolyTests/Univariate/NTT/FastMul.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
29 changes: 13 additions & 16 deletions tests/CompPolyTests/Univariate/NTT/Forward.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
41 changes: 19 additions & 22 deletions tests/CompPolyTests/Univariate/NTT/Inverse.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading