code wiki / _hdl_build / nx_poly1305_pow_gate.nx
`nx_poly1305_pow_gate.nx` source

↩ module page · 152 lines · 7244 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"
7import "nx_gate_verdict.nx"
8
9const POLY_LOG: *u8 = "knowledge/status/poly1305.log"
10
11func u8to32(p: *u8, o: i64) -> i64 {
  return (p[o] as i64) | ((p[o + 1] as i64) << 8) | ((p[o + 2] as i64) << 16) | ((p[o + 3] as i64) << 24)
13}
14
15// out = x * y mod (2^130-5), 5x26-bit limbs; ys[k] = y[k]*5 (the reduction multipliers). Fully carried.
16func poly_mul(x: *i64, y: *i64, ys: *i64, out: *i64) -> i64 {
  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]
  var d0: i64 = a0 * y[0] + a1 * ys[4] + a2 * ys[3] + a3 * ys[2] + a4 * ys[1]
  var d1: i64 = a0 * y[1] + a1 * y[0] + a2 * ys[4] + a3 * ys[3] + a4 * ys[2]
  var d2: i64 = a0 * y[2] + a1 * y[1] + a2 * y[0] + a3 * ys[4] + a4 * ys[3]
  var d3: i64 = a0 * y[3] + a1 * y[2] + a2 * y[1] + a3 * y[0] + a4 * ys[4]
  var d4: i64 = a0 * y[4] + a1 * y[3] + a2 * y[2] + a3 * y[1] + a4 * y[0]
  var c: i64 = d0 >> 26; out[0] = d0 & 0x3ffffff
  d1 = d1 + c; c = d1 >> 26; out[1] = d1 & 0x3ffffff
  d2 = d2 + c; c = d2 >> 26; out[2] = d2 & 0x3ffffff
  d3 = d3 + c; c = d3 >> 26; out[3] = d3 & 0x3ffffff
  d4 = d4 + c; c = d4 >> 26; out[4] = d4 & 0x3ffffff
  out[0] = out[0] + c * 5; c = out[0] >> 26; out[0] = out[0] & 0x3ffffff
  out[1] = out[1] + c
  c = out[1] >> 26; out[1] = out[1] & 0x3ffffff; out[2] = out[2] + c
  c = out[2] >> 26; out[2] = out[2] & 0x3ffffff; out[3] = out[3] + c
  c = out[3] >> 26; out[3] = out[3] & 0x3ffffff; out[4] = out[4] + c
  c = out[4] >> 26; out[4] = out[4] & 0x3ffffff; out[0] = out[0] + c * 5
  c = out[0] >> 26; out[0] = out[0] & 0x3ffffff; out[1] = out[1] + c
  return 0
36}
37
38func clamp_r(key: *u8, r: *i64) -> i64 {
  let k0: i64 = u8to32(key, 0)
  let k1: i64 = u8to32(key, 4)
  let k2: i64 = u8to32(key, 8)
  let k3: i64 = u8to32(key, 12)
  r[0] = k0 & 0x3ffffff
  r[1] = ((k0 >> 26) | (k1 << 6)) & 0x3ffff03
  r[2] = ((k1 >> 20) | (k2 << 12)) & 0x3ffc0ff
  r[3] = ((k2 >> 14) | (k3 << 18)) & 0x3f03fff
  r[4] = (k3 >> 8) & 0x00fffff
  return 0
49}
50
51func times5(x: *i64, xs: *i64) -> i64 {
  xs[0] = 0; xs[1] = x[1] * 5; xs[2] = x[2] * 5; xs[3] = x[3] * 5; xs[4] = x[4] * 5
  return 0
54}
55
56func 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 }
57func pwn(fd: i64, v: i64) -> i64 {
  let bb: *u8 = sys_mmap(28); var m: i64 = v
  let t: *u8 = sys_mmap(28); var k: i64 = 0
  if m == 0 { t[0] = 48; k = 1 }
  while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
  var i: i64 = 0
  while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
  sys_write(fd, bb, k); return 0
65}
66func print5(fd: i64, p: *i64) -> i64 {
  var i: i64 = 0
  while i < 5 { pwn(fd, p[i]); if i < 4 { pw(fd, "," as *u8) } i = i + 1 }
  return 0
70}
71
72// emit one i64 as 8 little-endian decimal bytes "b0,b1,...,b7," (for .byte rodata)
73func eb(fd: i64, v: i64) -> i64 {
  var i: i64 = 0
  while i < 8 { pwn(fd, (v >> (i * 8)) & 0xff); pw(fd, "," as *u8); i = i + 1 }
  return 0
77}
78// emit a label + a 4-lane BROADCAST of v (v repeated in all 4 ymm 64-bit lanes) as a .byte line
79func emit_bc(fd: i64, label: *u8, v: i64) -> i64 {
  pw(fd, label); pw(fd, ": .byte " as *u8)
  var j: i64 = 0
  while j < 4 { eb(fd, v); j = j + 1 }
  pw(fd, "\n" as *u8)
  return 0
85}
86
87// emit a label + a 4-lane vector [v0,v1,v2,v3] (one value per ymm 64-bit lane) as a .byte line
88func emit_lane(fd: i64, label: *u8, v0: i64, v1: i64, v2: i64, v3: i64) -> i64 {
  pw(fd, label); pw(fd, ": .byte " as *u8)
  eb(fd, v0); eb(fd, v1); eb(fd, v2); eb(fd, v3)
  pw(fd, "\n" as *u8)
  return 0
93}
94
95func emit(fd: i64, r: *i64, r2: *i64, r3: *i64, r4: *i64, ok: i64) -> i64 {
  pw(fd, "POLY1305POW R=" as *u8); print5(fd, r)
  pw(fd, " R2=" as *u8); print5(fd, r2)
  pw(fd, " R3=" as *u8); print5(fd, r3)
  pw(fd, " R4=" as *u8); print5(fd, r4)
  pw(fd, " xcheck_r4_two_ways=" as *u8); pwn(fd, ok)
  if ok == 1 { pw(fd, " verdict=GREEN\n" as *u8) } else { pw(fd, " verdict=RED\n" as *u8) }
  return 0
103}
104
105func main() -> i64 {
  let key: *u8 = sys_mmap(16)
  key[0] = 133 as u8; key[1] = 214 as u8; key[2] = 190 as u8; key[3] = 120 as u8
  key[4] = 87 as u8; key[5] = 85 as u8; key[6] = 109 as u8; key[7] = 51 as u8
  key[8] = 127 as u8; key[9] = 68 as u8; key[10] = 82 as u8; key[11] = 254 as u8
  key[12] = 66 as u8; key[13] = 213 as u8; key[14] = 6 as u8; key[15] = 168 as u8
  let r: *i64 = (sys_mmap(48)) as *i64
  clamp_r(key, r)
  let rs: *i64 = (sys_mmap(48)) as *i64
  times5(r, rs)
  let r2: *i64 = (sys_mmap(48)) as *i64
  poly_mul(r, r, rs, r2)
  let r2s: *i64 = (sys_mmap(48)) as *i64
  times5(r2, r2s)
  let r3: *i64 = (sys_mmap(48)) as *i64
  poly_mul(r2, r, rs, r3)
  let r4a: *i64 = (sys_mmap(48)) as *i64
  poly_mul(r2, r2, r2s, r4a)
  let r4b: *i64 = (sys_mmap(48)) as *i64
  poly_mul(r3, r, rs, r4b)
  var ok: i64 = 1
  var k: i64 = 0
  while k < 5 { if r4a[k] != r4b[k] { ok = 0 } k = k + 1 }
  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])
  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])
  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)
  emit_lane(1, "pw0" as *u8, r4a[0], r3[0], r2[0], r[0])
  emit_lane(1, "pw1" as *u8, r4a[1], r3[1], r2[1], r[1])
  emit_lane(1, "pw2" as *u8, r4a[2], r3[2], r2[2], r[2])
  emit_lane(1, "pw3" as *u8, r4a[3], r3[3], r2[3], r[3])
  emit_lane(1, "pw4" as *u8, r4a[4], r3[4], r2[4], r[4])
  emit_lane(1, "ps1" as *u8, r4a[1] * 5, r3[1] * 5, r2[1] * 5, r[1] * 5)
  emit_lane(1, "ps2" as *u8, r4a[2] * 5, r3[2] * 5, r2[2] * 5, r[2] * 5)
  emit_lane(1, "ps3" as *u8, r4a[3] * 5, r3[3] * 5, r2[3] * 5, r[3] * 5)
  emit_lane(1, "ps4" as *u8, r4a[4] * 5, r3[4] * 5, r2[4] * 5, r[4] * 5)
  emit(1, r, r2, r3, r4a, ok)
  let logf: i64 = sys_openat_append(POLY_LOG, 420)
  if logf >= 0 { emit(logf, r, r2, r3, r4a, ok); sys_close(logf) }
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = ok
  ctr__dry[1] = 1
  let rc__dry: i64 = gv_verdict("POLY1305-POW-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
152}
nx_poly1305_pow_gate.nx source

`nx_poly1305_pow_gate.nx` source
