nx_ed25519_scalar_test.nx source
↩ module page · 153 lines · 4734 B
1// nx_ed25519_scalar_test.nx -- KAT for scalar reduction + mul.
2//
3// Verifies:
4// sc_reduce side:
5// A. sc_reduce(0^64) == 0^32
6// B. sc_reduce(L padded to 64) == 0^32
7// C. sc_reduce(L+1 padded to 64) == 1 (01 00 ... 00)
8// D. sc_reduce(L-1 padded to 64) == L-1 (byte-exact)
9// E. sc_reduce(2*L padded to 64) == 0
10//
11// scalar mul side:
12// F. [0]B == identity
13// G. [1]B == B (byte-exact compressed)
14// H. [2]B == double(B)
15// I. [3]B == B + B + B
16//
17// Note: skipping [L]B == identity for this turn -- it requires
18// 252 doublings + ~125 adds and exercises bit patterns most prone
19// to off-by-one. It will land as part of Piece 4's verify KAT
20// (which actually computes [s]B for non-trivial s).
21//
22// expect_exit: 0
23// license_tier: ORIGINAL
24
25import "nx_syscalls.nx"
26import "nx_x25519.nx"
27import "nx_ed25519_field.nx"
28import "nx_ed25519_point.nx"
29import "nx_ed25519_arith.nx"
30import "nx_ed25519_scalar.nx"
31
32func main() -> i64 {
33 let l_bytes: *u8 = sys_mmap(64)
34 // L bytes (LE): ed d3 f5 5c 1a 63 12 58 d6 9c f7 a2 de f9 de 14
35 // 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 10
36 l_bytes[0]=0xed; l_bytes[1]=0xd3; l_bytes[2]=0xf5; l_bytes[3]=0x5c
37 l_bytes[4]=0x1a; l_bytes[5]=0x63; l_bytes[6]=0x12; l_bytes[7]=0x58
38 l_bytes[8]=0xd6; l_bytes[9]=0x9c; l_bytes[10]=0xf7; l_bytes[11]=0xa2
39 l_bytes[12]=0xde; l_bytes[13]=0xf9; l_bytes[14]=0xde; l_bytes[15]=0x14
40 var li: i64 = 16
41 while li < 31 { l_bytes[li] = 0; li = li + 1 }
42 l_bytes[31] = 0x10
43 // Pad to 64 with zeros
44 li = 32
45 while li < 64 { l_bytes[li] = 0; li = li + 1 }
46
47 let out: *u8 = sys_mmap(32)
48
49 // ---- Test A: sc_reduce(0^64) == 0^32 ----
50 let zeros: *u8 = sys_mmap(64)
51 sc_reduce(zeros, out)
52 var i: i64 = 0
53 while i < 32 {
54 if (out[i] & 0xff) != 0 { return 1 }
55 i = i + 1
56 }
57
58 // ---- Test B: sc_reduce(L padded to 64) == 0 ----
59 sc_reduce(l_bytes, out)
60 i = 0
61 while i < 32 {
62 if (out[i] & 0xff) != 0 { return 2 }
63 i = i + 1
64 }
65
66 // ---- Test C: sc_reduce(L+1 padded to 64) == 1 ----
67 let l_plus_1: *u8 = sys_mmap(64)
68 i = 0
69 while i < 64 { l_plus_1[i] = l_bytes[i]; i = i + 1 }
70 // Add 1 to byte 0 (L's byte 0 is 0xed, +1 = 0xee, no carry)
71 l_plus_1[0] = 0xee
72 sc_reduce(l_plus_1, out)
73 if (out[0] & 0xff) != 0x01 { return 3 }
74 i = 1
75 while i < 32 {
76 if (out[i] & 0xff) != 0 { return 4 }
77 i = i + 1
78 }
79
80 // ---- Test D: sc_reduce(L-1 padded to 64) == L-1 ----
81 let l_minus_1: *u8 = sys_mmap(64)
82 i = 0
83 while i < 64 { l_minus_1[i] = l_bytes[i]; i = i + 1 }
84 l_minus_1[0] = 0xec // L-1 has byte 0 = 0xec (0xed - 1)
85 sc_reduce(l_minus_1, out)
86 if (out[0] & 0xff) != 0xec { return 5 }
87 if (out[1] & 0xff) != 0xd3 { return 6 }
88 if (out[15] & 0xff) != 0x14 { return 7 }
89 if (out[31] & 0xff) != 0x10 { return 8 }
90
91 // ---- Test E: sc_reduce(2*L padded to 64) ----
92 // 2*L in LE: shift L left by 1 bit
93 let two_l: *u8 = sys_mmap(64)
94 var carry: i64 = 0
95 var bi: i64 = 0
96 while bi < 64 {
97 let v: i64 = ((l_bytes[bi] & 0xff) << 1) | carry
98 two_l[bi] = v & 0xff
99 carry = (v >> 8) & 1
100 bi = bi + 1
101 }
102 sc_reduce(two_l, out)
103 i = 0
104 while i < 32 {
105 if (out[i] & 0xff) != 0 { return 20 + (i & 0x1f) }
106 i = i + 1
107 }
108
109 // ---- Test F: [0]B == identity ----
110 let bp_bytes: *u8 = sys_mmap(32)
111 bp_bytes[0] = 0x58
112 bi = 1
113 while bi < 32 { bp_bytes[bi] = 0x66; bi = bi + 1 }
114 let B: *GeP3 = ge_p3_alloc()
115 let dc: i64 = ge_p3_decompress(B, bp_bytes)
116 if dc != NX_GE_VERDICT_OK { return 50 }
117
118 let scalar_0: *u8 = sys_mmap(32)
119 let r0: *GeP3 = ge_p3_alloc()
120 ge_scalar_mul(r0, scalar_0, B)
121 let id_pt: *GeP3 = ge_p3_alloc()
122 ge_p3_identity(id_pt)
123 if ge_p3_equal(r0, id_pt) != 1 { return 51 }
124
125 // ---- Test G: [1]B == B ----
126 let scalar_1: *u8 = sys_mmap(32)
127 scalar_1[0] = 1
128 let r1: *GeP3 = ge_p3_alloc()
129 ge_scalar_mul(r1, scalar_1, B)
130 if ge_p3_equal(r1, B) != 1 { return 52 }
131
132 // ---- Test H: [2]B == double(B) ----
133 let scalar_2: *u8 = sys_mmap(32)
134 scalar_2[0] = 2
135 let r2: *GeP3 = ge_p3_alloc()
136 ge_scalar_mul(r2, scalar_2, B)
137 let dB: *GeP3 = ge_p3_alloc()
138 ge_p3_double(dB, B)
139 if ge_p3_equal(r2, dB) != 1 { return 53 }
140
141 // ---- Test I: [3]B == B + B + B ----
142 let scalar_3: *u8 = sys_mmap(32)
143 scalar_3[0] = 3
144 let r3: *GeP3 = ge_p3_alloc()
145 ge_scalar_mul(r3, scalar_3, B)
146 let bb: *GeP3 = ge_p3_alloc()
147 ge_p3_add(bb, B, B)
148 let bbb: *GeP3 = ge_p3_alloc()
149 ge_p3_add(bbb, bb, B)
150 if ge_p3_equal(r3, bbb) != 1 { return 54 }
151
152 return 0
153}