nx_p256_field_inv_test.nx source
↩ module page · 111 lines · 3779 B
1// nx_p256_field_inv_test.nx -- KAT for P-256 modular inverse via
2// Fermat's little theorem.
3//
4// Strategy: prove a * inv(a) == 1 mod p for many a values.
5//
6// expect_exit: 0
7// license_tier: ORIGINAL
8
9import "nx_syscalls.nx"
10import "nx_u256.nx"
11import "nx_p256_field.nx"
12import "nx_p256_field_mul.nx"
13import "nx_p256_field_inv.nx"
14
15func main() -> i64 {
16 let a: *i64 = u256_alloc()
17 let inv: *i64 = u256_alloc()
18 let r: *i64 = u256_alloc()
19 let one: *i64 = u256_alloc()
20 let p: *i64 = u256_alloc()
21 p256_field_one(one)
22 p256_field_load_p(p)
23
24 // ---- Test A: load_p_minus_2 differs from p ONLY in LSB limb ----
25 let pm2: *i64 = u256_alloc()
26 p256_field_load_p_minus_2(pm2)
27 if pm2[0] != 0xFFFFFFFD { return 1 }
28 var i: i64 = 1
29 while i < 8 {
30 if (pm2[i] & 0xFFFFFFFF) != (p[i] & 0xFFFFFFFF) { return 2 + i }
31 i = i + 1
32 }
33
34 // ---- Test B: p256_field_bit_at picks correct bits ----
35 let probe: *i64 = u256_alloc()
36 u256_zero(probe); probe[0] = 0xFFFFFFFD // bits 0,2,3,...,31 set
37 if p256_field_bit_at(probe, 0) != 1 { return 11 } // bit 0 set
38 if p256_field_bit_at(probe, 1) != 0 { return 12 } // bit 1 clear
39 if p256_field_bit_at(probe, 2) != 1 { return 13 }
40 if p256_field_bit_at(probe, 31) != 1 { return 14 }
41 if p256_field_bit_at(probe, 32) != 0 { return 15 } // limb[1] is 0
42
43 u256_zero(probe); probe[6] = 1
44 if p256_field_bit_at(probe, 6 * 32) != 1 { return 16 } // bit 192 set
45 if p256_field_bit_at(probe, 6 * 32 + 1) != 0 { return 17 }
46
47 u256_zero(probe); probe[7] = 0x80000000
48 if p256_field_bit_at(probe, 7 * 32 + 31) != 1 { return 18 } // bit 255 set
49 if p256_field_bit_at(probe, 7 * 32 + 30) != 0 { return 19 }
50
51 // ---- Test C: inv(1) = 1 ----
52 p256_field_one(a)
53 p256_field_inv(inv, a)
54 if p256_field_eq(inv, one) != 1 { return 20 }
55
56 // ---- Test D: inv(2) * 2 = 1 ----
57 u256_zero(a); a[0] = 2
58 p256_field_inv(inv, a)
59 p256_field_mul(r, inv, a)
60 if p256_field_eq(r, one) != 1 { return 30 }
61
62 // ---- Test E: inv(p-1) = p-1 (since (p-1)^2 == 1) ----
63 u256_copy(a, p)
64 p256_field_sub(a, a, one) // a = p-1
65 p256_field_inv(inv, a)
66 if p256_field_eq(inv, a) != 1 { return 40 }
67 // Cross-check: (p-1) * (p-1) == 1
68 p256_field_mul(r, a, a)
69 if p256_field_eq(r, one) != 1 { return 41 }
70
71 // ---- Test F: inv(3) * 3 = 1 ----
72 u256_zero(a); a[0] = 3
73 p256_field_inv(inv, a)
74 p256_field_mul(r, inv, a)
75 if p256_field_eq(r, one) != 1 { return 50 }
76
77 // ---- Test G: random-looking a, verify a * inv(a) == 1 ----
78 u256_zero(a)
79 a[0] = 0x12345678; a[3] = 0xABCDEF01; a[5] = 0x55555555; a[7] = 0x00112233
80 if u256_cmp(a, p) != (0 - 1) { return 60 } // ensure canonical
81 p256_field_inv(inv, a)
82 p256_field_mul(r, inv, a)
83 if p256_field_eq(r, one) != 1 { return 61 }
84
85 // ---- Test H: another random-looking a ----
86 u256_zero(a)
87 a[1] = 0xDEADBEEF; a[2] = 0xCAFEBABE; a[6] = 0x00ABCDEF; a[7] = 0x12345678
88 if u256_cmp(a, p) != (0 - 1) { return 70 }
89 p256_field_inv(inv, a)
90 p256_field_mul(r, inv, a)
91 if p256_field_eq(r, one) != 1 { return 71 }
92
93 // ---- Test I: inv is involutive: inv(inv(a)) = a ----
94 u256_zero(a)
95 a[0] = 0x77777777; a[4] = 0x11223344
96 if u256_cmp(a, p) != (0 - 1) { return 80 }
97 p256_field_inv(inv, a)
98 let inv2: *i64 = u256_alloc()
99 p256_field_inv(inv2, inv)
100 if p256_field_eq(inv2, a) != 1 { return 81 }
101
102 // ---- Test J: aliasing -- out == a ----
103 u256_zero(a); a[0] = 7
104 let a_save: *i64 = u256_alloc()
105 u256_copy(a_save, a)
106 p256_field_inv(a, a) // a := a^(-1)
107 p256_field_mul(r, a, a_save)
108 if p256_field_eq(r, one) != 1 { return 90 }
109
110 return 0
111}