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}