nx_p256_fieldmul_mulx_difftest.nx source
↩ module page · 61 lines · 3122 B
1// nx_p256_fieldmul_mulx_difftest.nx -- prove the fused-intrinsic P-256 field multiply is bit-exact
2// vs the production p256_field_mul over many random field elements. Since both reduce with the
3// SAME _p256_solinas_reduce, this reduces correctness to the (already silicon-proven) 512-bit
4// product -- but running the FULL field-mul path end-to-end is the real composition proof.
5// expect_exit: 0 license_tier: ORIGINAL
6import "nx_p256_fieldmul_mulx.nx" // p256_field_mul_mulx + (transitively) p256_field_mul
7const K_MAGIC_6364136223846793005: i64 = 6364136223846793005
8const K_MAGIC_1442695040888963407: i64 = 1442695040888963407
9const K_MAGIC_4000: i64 = 4000
10
11func dp(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
12func dn(v: i64) -> i64 {
13 let t: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
14 let b: *u8 = sys_mmap(28); var k: i64 = 0; if m == 0 { t[0] = 48 as u8; k = 1 }
15 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
16 var i: i64 = 0; while i < k { b[i] = t[k-1-i]; i = i + 1 } sys_write(1, b, k); return 0
17}
18func dhex(v: i64) -> i64 {
19 let b: *u8 = sys_mmap(16); var i: i64 = 0
20 while i < 16 { let nib: i64 = (v >> ((15 - i) * 4)) & 15; if nib < 10 { b[i] = (48 + nib) as u8 } else { b[i] = (87 + nib) as u8 } i = i + 1 }
21 sys_write(1, b, 16); return 0
22}
23func lcg(st: *i64) -> i64 { let x: i64 = st[0] * K_MAGIC_6364136223846793005 + K_MAGIC_1442695040888963407; st[0] = x; return x }
24
25func main() -> i64 {
26 dp("=== nx_p256_fieldmul_mulx_difftest: p256_field_mul_mulx vs p256_field_mul ===\n" as *u8)
27 let a: *i64 = sys_mmap(8 * 8) as *i64
28 let b: *i64 = sys_mmap(8 * 8) as *i64
29 let r_ref: *i64 = sys_mmap(8 * 8) as *i64
30 let r_mux: *i64 = sys_mmap(8 * 8) as *i64
31 let st: *i64 = sys_mmap(8) as *i64
32 st[0] = 0x9e3779b97f4a7c15
33 var pass: i64 = 0
34 var total: i64 = 0
35
36 var n: i64 = 0
37 while n < K_MAGIC_4000 {
38 var k: i64 = 0
39 // random 8x32 field inputs (each limb 0..2^32-1); both paths reduce identically mod p
40 if n == 0 { k = 0; while k < 8 { a[k] = 0; b[k] = 0; k = k + 1 } }
41 else { if n == 1 { k = 0; while k < 8 { a[k] = 0xffffffff; b[k] = 0xffffffff; k = k + 1 } }
42 else {
43 k = 0; while k < 8 { a[k] = lcg(st) & 0xffffffff; b[k] = lcg(st) & 0xffffffff; k = k + 1 }
44 } }
45 p256_field_mul(r_ref, a, b)
46 p256_field_mul_mulx(r_mux, a, b)
47 var ok: i64 = 1
48 k = 0
49 while k < 8 { if (r_ref[k] & 0xffffffff) != (r_mux[k] & 0xffffffff) { ok = 0 } k = k + 1 }
50 if ok == 1 { pass = pass + 1 }
51 else {
52 dp(" [FAIL] n=" as *u8); dn(n); dp(" ref[0]=" as *u8); dhex(r_ref[0]); dp(" mux[0]=" as *u8); dhex(r_mux[0]); dp("\n" as *u8)
53 }
54 total = total + 1
55 n = n + 1
56 }
57
58 dp("=== FIELDMUL-MULX-DIFFTEST pass=" as *u8); dn(pass); dp("/" as *u8); dn(total)
59 if pass == total { dp(" verdict=GREEN ===\n" as *u8); sys_exit(0); return 0 }
60 dp(" verdict=RED ===\n" as *u8); sys_exit(1); return 1
61}