code wiki / _hdl_build / nx_poly1305_pow_gate.nx
nx_poly1305_pow_gate.nx source
↩ module page · 144 lines · 6706 B
1// nx_poly1305_pow_gate.nx -- compute + verify the Poly1305 key powers r, r^2, r^3, r^4 (mod 2^130-5),
2// the precomputed multipliers the 4-way SIMD Poly1305 kernel needs (lanes multiplied by [r^4,r^3,r^2,r^1]).
3// Uses the SAME 5x26-bit-limb multiply as the verified scalar reference (nx_poly1305_gate). Prints the
4// limbs (to embed in the SIMD .s) and CROSS-CHECKS r^4 two independent ways (r^2*r^2 == r^3*r) = a
5// liar-kill that the multiply is consistent. license_tier: ORIGINAL
6import "nx_syscalls.nx"
7
8const POLY_LOG: *u8 = "knowledge/status/poly1305.log"
9
10func u8to32(p: *u8, o: i64) -> i64 {
11 return (p[o] as i64) | ((p[o + 1] as i64) << 8) | ((p[o + 2] as i64) << 16) | ((p[o + 3] as i64) << 24)
12}
13
14// out = x * y mod (2^130-5), 5x26-bit limbs; ys[k] = y[k]*5 (the reduction multipliers). Fully carried.
15func poly_mul(x: *i64, y: *i64, ys: *i64, out: *i64) -> i64 {
16 let a0: i64 = x[0]; let a1: i64 = x[1]; let a2: i64 = x[2]; let a3: i64 = x[3]; let a4: i64 = x[4]
17 var d0: i64 = a0 * y[0] + a1 * ys[4] + a2 * ys[3] + a3 * ys[2] + a4 * ys[1]
18 var d1: i64 = a0 * y[1] + a1 * y[0] + a2 * ys[4] + a3 * ys[3] + a4 * ys[2]
19 var d2: i64 = a0 * y[2] + a1 * y[1] + a2 * y[0] + a3 * ys[4] + a4 * ys[3]
20 var d3: i64 = a0 * y[3] + a1 * y[2] + a2 * y[1] + a3 * y[0] + a4 * ys[4]
21 var d4: i64 = a0 * y[4] + a1 * y[3] + a2 * y[2] + a3 * y[1] + a4 * y[0]
22 var c: i64 = d0 >> 26; out[0] = d0 & 0x3ffffff
23 d1 = d1 + c; c = d1 >> 26; out[1] = d1 & 0x3ffffff
24 d2 = d2 + c; c = d2 >> 26; out[2] = d2 & 0x3ffffff
25 d3 = d3 + c; c = d3 >> 26; out[3] = d3 & 0x3ffffff
26 d4 = d4 + c; c = d4 >> 26; out[4] = d4 & 0x3ffffff
27 out[0] = out[0] + c * 5; c = out[0] >> 26; out[0] = out[0] & 0x3ffffff
28 out[1] = out[1] + c
29 c = out[1] >> 26; out[1] = out[1] & 0x3ffffff; out[2] = out[2] + c
30 c = out[2] >> 26; out[2] = out[2] & 0x3ffffff; out[3] = out[3] + c
31 c = out[3] >> 26; out[3] = out[3] & 0x3ffffff; out[4] = out[4] + c
32 c = out[4] >> 26; out[4] = out[4] & 0x3ffffff; out[0] = out[0] + c * 5
33 c = out[0] >> 26; out[0] = out[0] & 0x3ffffff; out[1] = out[1] + c
34 return 0
35}
36
37func clamp_r(key: *u8, r: *i64) -> i64 {
38 let k0: i64 = u8to32(key, 0)
39 let k1: i64 = u8to32(key, 4)
40 let k2: i64 = u8to32(key, 8)
41 let k3: i64 = u8to32(key, 12)
42 r[0] = k0 & 0x3ffffff
43 r[1] = ((k0 >> 26) | (k1 << 6)) & 0x3ffff03
44 r[2] = ((k1 >> 20) | (k2 << 12)) & 0x3ffc0ff
45 r[3] = ((k2 >> 14) | (k3 << 18)) & 0x3f03fff
46 r[4] = (k3 >> 8) & 0x00fffff
47 return 0
48}
49
50func times5(x: *i64, xs: *i64) -> i64 {
51 xs[0] = 0; xs[1] = x[1] * 5; xs[2] = x[2] * 5; xs[3] = x[3] * 5; xs[4] = x[4] * 5
52 return 0
53}
54
55func pw(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 }
56func pwn(fd: i64, v: i64) -> i64 {
57 let bb: *u8 = sys_mmap(28); var m: i64 = v
58 let t: *u8 = sys_mmap(28); var k: i64 = 0
59 if m == 0 { t[0] = 48; k = 1 }
60 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
61 var i: i64 = 0
62 while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
63 sys_write(fd, bb, k); return 0
64}
65func print5(fd: i64, p: *i64) -> i64 {
66 var i: i64 = 0
67 while i < 5 { pwn(fd, p[i]); if i < 4 { pw(fd, "," as *u8) } i = i + 1 }
68 return 0
69}
70
71// emit one i64 as 8 little-endian decimal bytes "b0,b1,...,b7," (for .byte rodata)
72func eb(fd: i64, v: i64) -> i64 {
73 var i: i64 = 0
74 while i < 8 { pwn(fd, (v >> (i * 8)) & 0xff); pw(fd, "," as *u8); i = i + 1 }
75 return 0
76}
77// emit a label + a 4-lane BROADCAST of v (v repeated in all 4 ymm 64-bit lanes) as a .byte line
78func emit_bc(fd: i64, label: *u8, v: i64) -> i64 {
79 pw(fd, label); pw(fd, ": .byte " as *u8)
80 var j: i64 = 0
81 while j < 4 { eb(fd, v); j = j + 1 }
82 pw(fd, "\n" as *u8)
83 return 0
84}
85
86// emit a label + a 4-lane vector [v0,v1,v2,v3] (one value per ymm 64-bit lane) as a .byte line
87func emit_lane(fd: i64, label: *u8, v0: i64, v1: i64, v2: i64, v3: i64) -> i64 {
88 pw(fd, label); pw(fd, ": .byte " as *u8)
89 eb(fd, v0); eb(fd, v1); eb(fd, v2); eb(fd, v3)
90 pw(fd, "\n" as *u8)
91 return 0
92}
93
94func emit(fd: i64, r: *i64, r2: *i64, r3: *i64, r4: *i64, ok: i64) -> i64 {
95 pw(fd, "POLY1305POW R=" as *u8); print5(fd, r)
96 pw(fd, " R2=" as *u8); print5(fd, r2)
97 pw(fd, " R3=" as *u8); print5(fd, r3)
98 pw(fd, " R4=" as *u8); print5(fd, r4)
99 pw(fd, " xcheck_r4_two_ways=" as *u8); pwn(fd, ok)
100 if ok == 1 { pw(fd, " verdict=GREEN\n" as *u8) } else { pw(fd, " verdict=RED\n" as *u8) }
101 return 0
102}
103
104func main() -> i64 {
105 let key: *u8 = sys_mmap(16)
106 key[0] = 133 as u8; key[1] = 214 as u8; key[2] = 190 as u8; key[3] = 120 as u8
107 key[4] = 87 as u8; key[5] = 85 as u8; key[6] = 109 as u8; key[7] = 51 as u8
108 key[8] = 127 as u8; key[9] = 68 as u8; key[10] = 82 as u8; key[11] = 254 as u8
109 key[12] = 66 as u8; key[13] = 213 as u8; key[14] = 6 as u8; key[15] = 168 as u8
110 let r: *i64 = (sys_mmap(48)) as *i64
111 clamp_r(key, r)
112 let rs: *i64 = (sys_mmap(48)) as *i64
113 times5(r, rs)
114 let r2: *i64 = (sys_mmap(48)) as *i64
115 poly_mul(r, r, rs, r2)
116 let r2s: *i64 = (sys_mmap(48)) as *i64
117 times5(r2, r2s)
118 let r3: *i64 = (sys_mmap(48)) as *i64
119 poly_mul(r2, r, rs, r3)
120 let r4a: *i64 = (sys_mmap(48)) as *i64
121 poly_mul(r2, r2, r2s, r4a)
122 let r4b: *i64 = (sys_mmap(48)) as *i64
123 poly_mul(r3, r, rs, r4b)
124 var ok: i64 = 1
125 var k: i64 = 0
126 while k < 5 { if r4a[k] != r4b[k] { ok = 0 } k = k + 1 }
127 emit_bc(1, "racc0" as *u8, r[0]); emit_bc(1, "racc1" as *u8, r[1]); emit_bc(1, "racc2" as *u8, r[2]); emit_bc(1, "racc3" as *u8, r[3]); emit_bc(1, "racc4" as *u8, r[4])
128 emit_bc(1, "rs1" as *u8, rs[1]); emit_bc(1, "rs2" as *u8, rs[2]); emit_bc(1, "rs3" as *u8, rs[3]); emit_bc(1, "rs4" as *u8, rs[4])
129 pw(1, "expectr2: .byte " as *u8); eb(1, r2[0]); eb(1, r2[1]); eb(1, r2[2]); eb(1, r2[3]); eb(1, r2[4]); pw(1, "\n" as *u8)
130 emit_lane(1, "pw0" as *u8, r4a[0], r3[0], r2[0], r[0])
131 emit_lane(1, "pw1" as *u8, r4a[1], r3[1], r2[1], r[1])
132 emit_lane(1, "pw2" as *u8, r4a[2], r3[2], r2[2], r[2])
133 emit_lane(1, "pw3" as *u8, r4a[3], r3[3], r2[3], r[3])
134 emit_lane(1, "pw4" as *u8, r4a[4], r3[4], r2[4], r[4])
135 emit_lane(1, "ps1" as *u8, r4a[1] * 5, r3[1] * 5, r2[1] * 5, r[1] * 5)
136 emit_lane(1, "ps2" as *u8, r4a[2] * 5, r3[2] * 5, r2[2] * 5, r[2] * 5)
137 emit_lane(1, "ps3" as *u8, r4a[3] * 5, r3[3] * 5, r2[3] * 5, r[3] * 5)
138 emit_lane(1, "ps4" as *u8, r4a[4] * 5, r3[4] * 5, r2[4] * 5, r[4] * 5)
139 emit(1, r, r2, r3, r4a, ok)
140 let logf: i64 = sys_openat_append(POLY_LOG, 420)
141 if logf >= 0 { emit(logf, r, r2, r3, r4a, ok); sys_close(logf) }
142 if ok == 1 { return 0 }
143 return 1
144}