Skip to content

Commit e5cc3ba

Browse files
EduardogbgEduardogbg
committed
tests: Pedersen and EmbeddedCurveOps reference vectors in the Lampe Tests lib
- Lampe/Tests/Pedersen.lean validates the pure pedersenCommitment / pedersenHash functions against Aztec's published test vectors from assert_pedersen in the Noir stdlib: 20 example blocks covering all N in {1..10} for both pedersen_hash_with_separator and pedersen_commitment_with_separator with inputs [1, ..., N] and separator N, each closed by native_decide. This certifies byte-for-byte agreement with Barretenberg's BLAKE3 hash-to-curve, try-and-increment counter handling, parity convention, generator index encoding, and MSM composition. - Lampe/Tests/EmbeddedCurveOps.lean validates the canonicalDecomp / scalarCanonical machinery on BN254: edge cases (0, 1, -1, pow128, pow128 - 1, pow128 * phi, a random-looking value), the limb identity f = lo + 2^128 * hi, and the (0, 0) vs (plo, phi) uniqueness corner case that motivates canonical_decomp_unique's disjunction hypothesis. Both live in the Lampe Tests lib (mirroring Lampe/Tests/Blake3.lean) so they are exercised by the regular build, instead of standalone stdlib files requiring direct `lake env lean` invocation.
1 parent dd04ca0 commit e5cc3ba

2 files changed

Lines changed: 320 additions & 0 deletions

File tree

‎Lampe/Tests/EmbeddedCurveOps.lean‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
import Lampe.Crypto.Bn254.Prime
2+
import Lampe.Crypto.EmbeddedCurve
3+
4+
/-!
5+
# Canonical-decomposition validation vectors
6+
7+
Concrete `native_decide` tests on the `canonicalDecomp` /
8+
`scalarCanonical` machinery introduced for the Pedersen wrapper
9+
deterministic corollaries. Tests cover edge cases (`f = 0`, `f = 1`,
10+
`f = p - 1`, the boundary `pow128`, and the `(plo, phi)` collision
11+
point that the uniqueness lemma rules out) plus a handful of
12+
random-looking values.
13+
14+
The tests verify three properties for each chosen `f`:
15+
16+
1. `canonicalDecomp f` satisfies `scalarCanonical`
17+
(limb-range canonicality: `lo.val < 2^128 ∧ hi.val < 2^126`).
18+
2. `canonicalDecomp f` recovers `f` via the limb identity
19+
`f = lo + 2^128 · hi`.
20+
3. `canonicalDecomp` agrees with the explicit `(0, 0)` decomposition
21+
on `f = 0`, ruling out the spurious `(plo, phi)` alternative.
22+
23+
These exercise the machinery the Pedersen `_spec_canonical` corollaries
24+
depend on (`canonicalDecomp_unique`, `canonicalDecomp_decomposes`,
25+
`canonicalDecomp_canonical`).
26+
-/
27+
28+
namespace Tests.EmbeddedCurveOps
29+
30+
open Lampe (Fp Prime)
31+
open Lampe.Crypto.EmbeddedCurve
32+
33+
/-- BN254 scalar field prime — the field for embedded-curve scalars. -/
34+
abbrev P : Lampe.Prime := Lampe.Crypto.Bn254.prime
35+
36+
/-! ### `scalarCanonical` holds on `canonicalDecomp` -/
37+
38+
/-- `canonicalDecomp 0 = (0, 0)` and is canonical. -/
39+
example : scalarCanonical (canonicalDecomp (0 : Fp P)) := by
40+
native_decide
41+
42+
/-- `canonicalDecomp 1 = (1, 0)` and is canonical. -/
43+
example : scalarCanonical (canonicalDecomp (1 : Fp P)) := by
44+
native_decide
45+
46+
/-- `canonicalDecomp (p - 1) = (plo - 1, phi)` and is canonical (high
47+
limb is `phi`, just below the `2^126` bound; low limb is `plo - 1`,
48+
just below the `2^128` bound). -/
49+
example : scalarCanonical (canonicalDecomp (-1 : Fp P)) := by
50+
native_decide
51+
52+
/-- `canonicalDecomp (pow128) = (0, 1)` — boundary between low- and
53+
high-limb regimes. -/
54+
example :
55+
scalarCanonical (canonicalDecomp ((Lampe.pow128 : Nat) : Fp P)) := by
56+
native_decide
57+
58+
/-- `canonicalDecomp (pow128 - 1) = (pow128 - 1, 0)` — largest pure-low
59+
value. -/
60+
example :
61+
scalarCanonical (canonicalDecomp ((Lampe.pow128 - 1 : Nat) : Fp P)) := by
62+
native_decide
63+
64+
/-- `canonicalDecomp (pow128 * phi) = (0, phi)` — top of the
65+
canonical-range branch (a) boundary. -/
66+
example :
67+
scalarCanonical
68+
(canonicalDecomp
69+
((Lampe.pow128 * Lampe.Crypto.Bn254.phi : Nat) : Fp P)) := by
70+
native_decide
71+
72+
/-- A random-looking value in the middle of the field. -/
73+
example :
74+
scalarCanonical
75+
(canonicalDecomp
76+
((12345678901234567890123456789012345678901234567890123456789012345 : Nat) : Fp P)) := by
77+
native_decide
78+
79+
/-! ### `canonicalDecomp` recovers `f` via the limb identity -/
80+
81+
/-- The limb identity `f = lo + 2^128 · hi` holds on `f = pow128 + 7`. -/
82+
example :
83+
let f : Fp P := ((Lampe.pow128 + 7 : Nat) : Fp P)
84+
let s := canonicalDecomp f
85+
f = scalarLo s + ((Lampe.pow128 : Nat) : Fp P) * scalarHi s := by
86+
native_decide
87+
88+
/-- The limb identity holds on `f = p - 1` (the wraparound edge case). -/
89+
example :
90+
let f : Fp P := (-1 : Fp P)
91+
let s := canonicalDecomp f
92+
f = scalarLo s + ((Lampe.pow128 : Nat) : Fp P) * scalarHi s := by
93+
native_decide
94+
95+
/-! ### Uniqueness corner case: `f = 0` resolves to `(0, 0)`, not `(plo, phi)` -/
96+
97+
/-- On `f = 0`, `canonicalDecomp` picks the `(0, 0)` witness, not the
98+
arithmetically-equivalent `(plo, phi)` witness. This is the
99+
counterexample to "any canonical-range decomposition of a field
100+
element is unique" — the `canonicalDecomp_unique` lemma's
101+
`hdisj` hypothesis breaks the tie. -/
102+
example :
103+
(scalarLo (canonicalDecomp (0 : Fp P))).val = 0 ∧
104+
(scalarHi (canonicalDecomp (0 : Fp P))).val = 0 := by
105+
native_decide
106+
107+
/-- The spurious `(plo, phi)` witness is **not** what `canonicalDecomp`
108+
returns on `f = 0`, even though it satisfies the limb identity
109+
`plo + 2^128 · phi = p ≡ 0 (mod p)`. -/
110+
example :
111+
(scalarLo (canonicalDecomp (0 : Fp P))).val ≠ Lampe.Crypto.Bn254.plo ∨
112+
(scalarHi (canonicalDecomp (0 : Fp P))).val ≠ Lampe.Crypto.Bn254.phi := by
113+
native_decide
114+
115+
end Tests.EmbeddedCurveOps

‎Lampe/Tests/Pedersen.lean‎

Lines changed: 205 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,205 @@
1+
import Lampe.Crypto.Bn254.Prime
2+
import Lampe.Crypto.Pedersen
3+
4+
/-!
5+
# Pedersen reference vectors
6+
7+
Verifies the pure `Lampe.Crypto.Pedersen.pedersenCommitment` and
8+
`Lampe.Crypto.Pedersen.pedersenHash` functions — the exact closed
9+
forms guaranteed by the stdlib `_spec_canonical` theorems — against
10+
Aztec's published test vectors (from `assert_pedersen` in the Noir
11+
stdlib, extracted at
12+
`stdlib/lampe/std-1.0.0-beta.14/Extracted/Hash/Mod.lean` starting at
13+
line 251).
14+
15+
Inputs are `[1, 2, ..., N]` as Fields, separator = N. Outputs are
16+
the published Aztec curve points (for commitment) and field elements
17+
(for hash). Negative literals are field elements expressed as their
18+
signed representative; the `Int` → `Fp P` cast reduces them mod `p`.
19+
-/
20+
21+
namespace Tests.Pedersen
22+
23+
open Lampe (Fp Prime)
24+
open Lampe.Crypto.EmbeddedCurve
25+
open Lampe.Crypto.Pedersen
26+
27+
/-- BN254 scalar field prime — the field for Pedersen scalars and the
28+
base field for Grumpkin. -/
29+
abbrev P : Lampe.Prime := Lampe.Crypto.Bn254.prime
30+
31+
/-- The test-vector input `[1, 2, ..., n]` as field elements. -/
32+
def inputs (n : Nat) : List.Vector (Fp P) n :=
33+
List.Vector.ofFn (fun i : Fin n => ((i.val + 1 : Nat) : Fp P))
34+
35+
-- N = 1
36+
37+
/-- pedersen_hash_with_separator<1>([1], 1) — Aztec reference. -/
38+
example :
39+
pedersenHash P defaultDomainBytes (inputs 1) 1 =
40+
((-9563966249275741675388072609438711537348680428347819854678797696612266004386 : Int) : Fp P) := by
41+
native_decide
42+
43+
/-- pedersen_commitment_with_separator<1>([1], 1) — Aztec reference. -/
44+
example :
45+
pedersenCommitment P defaultDomainBytes (inputs 1) 1 =
46+
mkPoint
47+
((2393473289045184898987089634332637236754766663897650125720167164137088869378 : Int) : Fp P)
48+
((-7135402912423807765050323395026152633898511180575289670895350565966806597339 : Int) : Fp P)
49+
false := by
50+
native_decide
51+
52+
-- N = 2
53+
54+
/-- pedersen_hash_with_separator<2>([1..2], 2) — Aztec reference. -/
55+
example :
56+
pedersenHash P defaultDomainBytes (inputs 2) 2 =
57+
((-4514641934080458214240751313245257091597283372119704256508270041112972328364 : Int) : Fp P) := by
58+
native_decide
59+
60+
/-- pedersen_commitment_with_separator<2>([1..2], 2) — Aztec reference. -/
61+
example :
62+
pedersenCommitment P defaultDomainBytes (inputs 2) 2 =
63+
mkPoint
64+
((-1005469533000889117657666498472954572857833872027279582301287737791321798830 : Int) : Fp P)
65+
((-197930408253518363600434091261593976805802346006803044607495721019065268361 : Int) : Fp P)
66+
false := by
67+
native_decide
68+
69+
-- N = 3
70+
71+
/-- pedersen_hash_with_separator<3>([1..3], 3) — Aztec reference. -/
72+
example :
73+
pedersenHash P defaultDomainBytes (inputs 3) 3 =
74+
((5326303462429251635333445553787815334884504473158538697533567972354818497508 : Int) : Fp P) := by
75+
native_decide
76+
77+
/-- pedersen_commitment_with_separator<3>([1..3], 3) — Aztec reference. -/
78+
example :
79+
pedersenCommitment P defaultDomainBytes (inputs 3) 3 =
80+
mkPoint
81+
((-7445492827528947374509602945629683494533192071041804482180938699494227714940 : Int) : Fp P)
82+
((-346969586742294743999106690738565516862306986837138292504091779330690805808 : Int) : Fp P)
83+
false := by
84+
native_decide
85+
86+
-- N = 4
87+
88+
/-- pedersen_hash_with_separator<4>([1..4], 4) — Aztec reference. -/
89+
example :
90+
pedersenHash P defaultDomainBytes (inputs 4) 4 =
91+
((386725976317305842536127973743796063021078557104668993698335256486699462108 : Int) : Fp P) := by
92+
native_decide
93+
94+
/-- pedersen_commitment_with_separator<4>([1..4], 4) — Aztec reference. -/
95+
example :
96+
pedersenCommitment P defaultDomainBytes (inputs 4) 4 =
97+
mkPoint
98+
((3474050104565946163748262682994355436071725368663608454945085151569694677961 : Int) : Fp P)
99+
((4969143737471383592015577254419974288705429190161323890019554309538525237268 : Int) : Fp P)
100+
false := by
101+
native_decide
102+
103+
-- N = 5
104+
105+
/-- pedersen_hash_with_separator<5>([1..5], 5) — Aztec reference. -/
106+
example :
107+
pedersenHash P defaultDomainBytes (inputs 5) 5 =
108+
((445627510378474786942205982382342880084933256779806571759234109296077544482 : Int) : Fp P) := by
109+
native_decide
110+
111+
/-- pedersen_commitment_with_separator<5>([1..5], 5) — Aztec reference. -/
112+
example :
113+
pedersenCommitment P defaultDomainBytes (inputs 5) 5 =
114+
mkPoint
115+
((10552833461612204383225982278685649771700648236894998952452362214619168226089 : Int) : Fp P)
116+
((-1251131729610909206337824637802607977413231765663205492654376476649374713610 : Int) : Fp P)
117+
false := by
118+
native_decide
119+
120+
-- N = 6
121+
122+
/-- pedersen_hash_with_separator<6>([1..6], 6) — Aztec reference. -/
123+
example :
124+
pedersenHash P defaultDomainBytes (inputs 6) 6 =
125+
((10217545977856619241380062255630350521414270790482717416408002401121937565042 : Int) : Fp P) := by
126+
native_decide
127+
128+
/-- pedersen_commitment_with_separator<6>([1..6], 6) — Aztec reference. -/
129+
example :
130+
pedersenCommitment P defaultDomainBytes (inputs 6) 6 =
131+
mkPoint
132+
((11335069702571578236117888955050736139682779524214984889155721704928197387927 : Int) : Fp P)
133+
((-7733361908666485801415200275635877656445756448956549185022038133647049615622 : Int) : Fp P)
134+
false := by
135+
native_decide
136+
137+
-- N = 7
138+
139+
/-- pedersen_hash_with_separator<7>([1..7], 7) — Aztec reference. -/
140+
example :
141+
pedersenHash P defaultDomainBytes (inputs 7) 7 =
142+
((8389099894375185114295483291630893019224023442848409888108611454294869536227 : Int) : Fp P) := by
143+
native_decide
144+
145+
/-- pedersen_commitment_with_separator<7>([1..7], 7) — Aztec reference. -/
146+
example :
147+
pedersenCommitment P defaultDomainBytes (inputs 7) 7 =
148+
mkPoint
149+
((601182919381464537093882307577577658521785998356796832152269409048770009401 : Int) : Fp P)
150+
((-8704984668101593449807889537070046830501821124601109099832679891796819531525 : Int) : Fp P)
151+
false := by
152+
native_decide
153+
154+
-- N = 8
155+
156+
/-- pedersen_hash_with_separator<8>([1..8], 8) — Aztec reference. -/
157+
example :
158+
pedersenHash P defaultDomainBytes (inputs 8) 8 =
159+
((-364414833671337260860436705614307386127212237115043515297237560718972836517 : Int) : Fp P) := by
160+
native_decide
161+
162+
/-- pedersen_commitment_with_separator<8>([1..8], 8) — Aztec reference. -/
163+
example :
164+
pedersenCommitment P defaultDomainBytes (inputs 8) 8 =
165+
mkPoint
166+
((10105395258059943854471547573391327707179901153940064586773125525172385465411 : Int) : Fp P)
167+
((-7764172381957047914625405480055519449068901615240110013280942913930205438090 : Int) : Fp P)
168+
false := by
169+
native_decide
170+
171+
-- N = 9
172+
173+
/-- pedersen_hash_with_separator<9>([1..9], 9) — Aztec reference. -/
174+
example :
175+
pedersenHash P defaultDomainBytes (inputs 9) 9 =
176+
((5694292929090063810102755351119629986122166830204542196709417013467308391399 : Int) : Fp P) := by
177+
native_decide
178+
179+
/-- pedersen_commitment_with_separator<9>([1..9], 9) — Aztec reference. -/
180+
example :
181+
pedersenCommitment P defaultDomainBytes (inputs 9) 9 =
182+
mkPoint
183+
((4630760469979870165820917922898436050077118370325830990580986530746633543789 : Int) : Fp P)
184+
((445421188486227550820408419830973545028032672242093648088931561027838255858 : Int) : Fp P)
185+
false := by
186+
native_decide
187+
188+
-- N = 10
189+
190+
/-- pedersen_hash_with_separator<10>([1..10], 10) — Aztec reference. -/
191+
example :
192+
pedersenHash P defaultDomainBytes (inputs 10) 10 =
193+
((-1612865150156425111011383725280441289912228955196006102547487828548180279661 : Int) : Fp P) := by
194+
native_decide
195+
196+
/-- pedersen_commitment_with_separator<10>([1..10], 10) — Aztec reference. -/
197+
example :
198+
pedersenCommitment P defaultDomainBytes (inputs 10) 10 =
199+
mkPoint
200+
((-311556882567474412576811669014419164866085063813982345701073780395111226613 : Int) : Fp P)
201+
((-163948955461070038478898748306472919392980231474444415480716967232318545340 : Int) : Fp P)
202+
false := by
203+
native_decide
204+
205+
end Tests.Pedersen

0 commit comments

Comments
 (0)