nx_ed25519_field_test.nx source
↩ module page · 106 lines · 3996 B
1// nx_ed25519_field_test.nx -- KAT for Ed25519 field primitives.
2//
3// Verifies:
4// A. fe_neg(fe_one) + fe_one canonically encodes to zero
5// B. fe_pow22523(fe_one) canonically encodes to one
6// C. ED25519_SQRT_M1 squared canonically encodes to fe_neg(fe_one)
7// (the defining property of sqrt(-1))
8// D. ED25519_D bytes match RFC 8032 §6 spec byte-exact
9//
10// expect_exit: 0
11// license_tier: ORIGINAL
12
13import "nx_syscalls.nx"
14import "nx_x25519.nx"
15import "nx_ed25519_field.nx"
16
17func main() -> i64 {
18 // ---- Test A: fe_neg(1) + 1 == 0 ----
19 let one: *i64 = fe_alloc()
20 fe_one(one)
21 let neg_one: *i64 = fe_alloc()
22 fe_neg(neg_one, one)
23 let sum: *i64 = fe_alloc()
24 fe_add(sum, neg_one, one)
25 let zero: *i64 = fe_alloc()
26 fe_zero(zero)
27 if fe_canonical_equal(sum, zero) != 1 { return 1 }
28
29 // ---- Test B: fe_pow22523(1) == 1 ----
30 let pow_one: *i64 = fe_alloc()
31 fe_pow22523(pow_one, one)
32 if fe_canonical_equal(pow_one, one) != 1 { return 2 }
33
34 // ---- Test C: SQRT_M1^2 == -1 ----
35 let sqrt_m1: *i64 = fe_alloc()
36 ed25519_sqrt_m1_fe(sqrt_m1)
37 let sqrt_m1_sq: *i64 = fe_alloc()
38 fe_sq(sqrt_m1_sq, sqrt_m1)
39 if fe_canonical_equal(sqrt_m1_sq, neg_one) != 1 { return 3 }
40
41 // ---- Test D: ED25519_D bytes byte-exact ----
42 let d_bytes: *u8 = sys_mmap(32)
43 ed25519_d_bytes(d_bytes)
44 // First + last + a couple middle bytes per RFC 8032 §6:
45 if (d_bytes[0] & 0xff) != 0xa3 { return 4 }
46 if (d_bytes[1] & 0xff) != 0x78 { return 5 }
47 if (d_bytes[15] & 0xff) != 0x00 { return 6 }
48 if (d_bytes[16] & 0xff) != 0x98 { return 7 }
49 if (d_bytes[31] & 0xff) != 0x52 { return 8 }
50
51 // ---- Test E: ED25519_SQRT_M1 bytes byte-exact ----
52 let s_bytes: *u8 = sys_mmap(32)
53 ed25519_sqrt_m1_bytes(s_bytes)
54 if (s_bytes[0] & 0xff) != 0xb0 { return 9 }
55 if (s_bytes[31] & 0xff) != 0x2b { return 10 }
56
57 // ---- Test F: ED25519_D as fe + fe_to_bytes round-trips to same bytes ----
58 let d_fe: *i64 = fe_alloc()
59 ed25519_d_fe(d_fe)
60 let d_re: *u8 = sys_mmap(32)
61 fe_to_bytes(d_re, d_fe)
62 var i: i64 = 0
63 while i < 32 {
64 if (d_re[i] & 0xff) != (d_bytes[i] & 0xff) { return 20 + i }
65 i = i + 1
66 }
67
68 // ---- Test G: fe_pow22523 self-consistency on a non-trivial input ----
69 // Choose z = 4 (the canonical "small QR"). z^((p-5)/8) is the
70 // inverse square root of z. Then (z^((p-5)/8))^2 * z should
71 // equal z^((p-3)/4) * z = z^((p+1)/4) which is the principal
72 // sqrt. Square that and we should get z back (since z is a QR
73 // and we computed sqrt(z)^2).
74 let z: *i64 = fe_alloc()
75 let four_bytes: *u8 = sys_mmap(32)
76 four_bytes[0] = 4
77 var k: i64 = 1
78 while k < 32 { four_bytes[k] = 0; k = k + 1 }
79 fe_from_bytes(z, four_bytes)
80
81 let inv_sqrt_z: *i64 = fe_alloc()
82 fe_pow22523(inv_sqrt_z, z)
83 // sqrt(z) = z * inv_sqrt(z) where inv_sqrt(z) = z^((p-5)/8)
84 let sqrt_z: *i64 = fe_alloc()
85 fe_mul(sqrt_z, z, inv_sqrt_z)
86 // (sqrt(z))^2 should equal ±z. For curve25519, p ≡ 5 mod 8, so
87 // sqrt_z = z^((p+3)/8) and sqrt_z^2 = z^((p+3)/4) = z * z^((p-1)/4).
88 // z^((p-1)/4) is ±1 when z is a QR (Euler). When +1, sqrt_z_sq == z;
89 // when -1, sqrt_z_sq == -z and the full sqrt algorithm multiplies
90 // by sqrt(-1). For z=4=2^2 with p≡5 mod 8, 2 is a non-residue so
91 // z^((p-1)/4) = 2^((p-1)/2) = -1. Substrate-honest: accept either.
92 let sqrt_z_sq: *i64 = fe_alloc()
93 fe_sq(sqrt_z_sq, sqrt_z)
94 let neg_z: *i64 = fe_alloc()
95 fe_neg(neg_z, z)
96 let eq_pos: i64 = fe_canonical_equal(sqrt_z_sq, z)
97 let eq_neg: i64 = fe_canonical_equal(sqrt_z_sq, neg_z)
98 if eq_pos != 1 { if eq_neg != 1 { return 50 } }
99
100 // ---- Test H: verdict gate ----
101 if nx_ed25519_verdict_is_valid(NX_ED25519_VERDICT_OK) != 1 { return 60 }
102 if nx_ed25519_verdict_is_valid(NX_ED25519_VERDICT_N) != 0 { return 61 }
103 if nx_ed25519_verdict_is_valid(0 - 1) != 0 { return 62 }
104
105 return 0
106}