code wiki / _hdl_build / nx_poly1305_gate.nx
nx_poly1305_gate.nx source
↩ module page · 202 lines · 9678 B
1// nx_poly1305_gate.nx -- GATE for the SCALAR Poly1305 reference (the MAC half of the room's
2// ChaCha20-Poly1305 AEAD). Proves, by RUNNING, byte-exact against the RFC-8439 ยง2.5.2 test
3// vector. This is the CORRECTNESS FOUNDATION for the SIMD Poly1305 exceed (same 5x26-bit limb
4// layout the AVX2 kernel will vectorize over powers of r). poly1305-donna 32-bit algorithm,
5// 5 limbs of 26 bits each, products fit i64 (no 128-bit/mulq needed).
6//
7// TWO GATES:
8// A RFC KAT: tag("Cryptographic Forum Research Group", rfc-key) == a8061dc1...27a9 (byte-exact).
9// B LIAR-KILL: flip one message byte -> tag MUST differ from the RFC tag (kills a hardcoded cheat).
10//
11// genealogy_id: bernstein_2005_poly1305 (realized_in nx_poly1305)
12// lineage_id: sovereign_poly1305_scalar_26bit_limb_v1
13// license_tier: ORIGINAL
14import "nx_syscalls.nx"
15import "nx_gate_verdict.nx"
16
17const POLY_LOG: *u8 = "knowledge/status/poly1305.log"
18
19// load 4 little-endian bytes at p[o..o+3] as a 32-bit value (0 .. 2^32-1, fits i64).
20func u8to32(p: *u8, o: i64) -> i64 {
21 return (p[o] as i64) | ((p[o + 1] as i64) << 8) | ((p[o + 2] as i64) << 16) | ((p[o + 3] as i64) << 24)
22}
23
24// process one 16-byte block m[off..off+15] into accumulator h, given clamped r and s=r*5.
25// hibit = 0x1000000 (1<<24) for full blocks (the 2^128 term), 0 for the padded final block.
26func poly_block(m: *u8, off: i64, hibit: i64, h: *i64, r: *i64, s: *i64) -> i64 {
27 let t0: i64 = u8to32(m, off + 0)
28 let t1: i64 = u8to32(m, off + 4)
29 let t2: i64 = u8to32(m, off + 8)
30 let t3: i64 = u8to32(m, off + 12)
31 let a0: i64 = h[0] + (t0 & 0x3ffffff)
32 let a1: i64 = h[1] + (((t0 >> 26) | (t1 << 6)) & 0x3ffffff)
33 let a2: i64 = h[2] + (((t1 >> 20) | (t2 << 12)) & 0x3ffffff)
34 let a3: i64 = h[3] + (((t2 >> 14) | (t3 << 18)) & 0x3ffffff)
35 let a4: i64 = h[4] + ((t3 >> 8) | hibit)
36 var d0: i64 = a0 * r[0] + a1 * s[4] + a2 * s[3] + a3 * s[2] + a4 * s[1]
37 var d1: i64 = a0 * r[1] + a1 * r[0] + a2 * s[4] + a3 * s[3] + a4 * s[2]
38 var d2: i64 = a0 * r[2] + a1 * r[1] + a2 * r[0] + a3 * s[4] + a4 * s[3]
39 var d3: i64 = a0 * r[3] + a1 * r[2] + a2 * r[1] + a3 * r[0] + a4 * s[4]
40 var d4: i64 = a0 * r[4] + a1 * r[3] + a2 * r[2] + a3 * r[1] + a4 * r[0]
41 var c: i64 = d0 >> 26
42 h[0] = d0 & 0x3ffffff
43 d1 = d1 + c; c = d1 >> 26; h[1] = d1 & 0x3ffffff
44 d2 = d2 + c; c = d2 >> 26; h[2] = d2 & 0x3ffffff
45 d3 = d3 + c; c = d3 >> 26; h[3] = d3 & 0x3ffffff
46 d4 = d4 + c; c = d4 >> 26; h[4] = d4 & 0x3ffffff
47 h[0] = h[0] + c * 5; c = h[0] >> 26; h[0] = h[0] & 0x3ffffff
48 h[1] = h[1] + c
49 return 0
50}
51
52// full Poly1305: tag = (poly(msg) + s) mod 2^128, written 16 bytes LE to tag.
53func poly1305(key: *u8, msg: *u8, mlen: i64, tag: *u8) -> i64 {
54 let r: *i64 = (sys_mmap(48)) as *i64
55 let s: *i64 = (sys_mmap(48)) as *i64
56 let h: *i64 = (sys_mmap(48)) as *i64
57 let k0: i64 = u8to32(key, 0)
58 let k1: i64 = u8to32(key, 4)
59 let k2: i64 = u8to32(key, 8)
60 let k3: i64 = u8to32(key, 12)
61 r[0] = k0 & 0x3ffffff
62 r[1] = ((k0 >> 26) | (k1 << 6)) & 0x3ffff03
63 r[2] = ((k1 >> 20) | (k2 << 12)) & 0x3ffc0ff
64 r[3] = ((k2 >> 14) | (k3 << 18)) & 0x3f03fff
65 r[4] = (k3 >> 8) & 0x00fffff
66 s[1] = r[1] * 5
67 s[2] = r[2] * 5
68 s[3] = r[3] * 5
69 s[4] = r[4] * 5
70 h[0] = 0; h[1] = 0; h[2] = 0; h[3] = 0; h[4] = 0
71 var off: i64 = 0
72 while off + 16 <= mlen {
73 poly_block(msg, off, 0x1000000, h, r, s)
74 off = off + 16
75 }
76 let rem: i64 = mlen - off
77 if rem > 0 {
78 let buf: *u8 = sys_mmap(16)
79 var i: i64 = 0
80 while i < 16 { buf[i] = 0 as u8; i = i + 1 }
81 i = 0
82 while i < rem { buf[i] = msg[off + i]; i = i + 1 }
83 buf[rem] = 1 as u8
84 poly_block(buf, 0, 0, h, r, s)
85 }
86 // fully carry h
87 var c: i64 = h[1] >> 26; h[1] = h[1] & 0x3ffffff; h[2] = h[2] + c
88 c = h[2] >> 26; h[2] = h[2] & 0x3ffffff; h[3] = h[3] + c
89 c = h[3] >> 26; h[3] = h[3] & 0x3ffffff; h[4] = h[4] + c
90 c = h[4] >> 26; h[4] = h[4] & 0x3ffffff; h[0] = h[0] + c * 5
91 c = h[0] >> 26; h[0] = h[0] & 0x3ffffff; h[1] = h[1] + c
92 // g = h - p (p = 2^130-5): if g >= 0 (h >= p) use g
93 var g0: i64 = h[0] + 5; c = g0 >> 26; g0 = g0 & 0x3ffffff
94 var g1: i64 = h[1] + c; c = g1 >> 26; g1 = g1 & 0x3ffffff
95 var g2: i64 = h[2] + c; c = g2 >> 26; g2 = g2 & 0x3ffffff
96 var g3: i64 = h[3] + c; c = g3 >> 26; g3 = g3 & 0x3ffffff
97 var g4: i64 = h[4] + c - 0x4000000
98 if g4 >= 0 {
99 h[0] = g0; h[1] = g1; h[2] = g2; h[3] = g3; h[4] = g4
100 }
101 // pack 5x26 -> 4x32
102 var p0: i64 = (h[0] | (h[1] << 26)) & 0xffffffff
103 var p1: i64 = ((h[1] >> 6) | (h[2] << 20)) & 0xffffffff
104 var p2: i64 = ((h[2] >> 12) | (h[3] << 14)) & 0xffffffff
105 var p3: i64 = ((h[3] >> 18) | (h[4] << 8)) & 0xffffffff
106 // tag = (h + s) mod 2^128, s = key[16..31] LE
107 var f: i64 = p0 + u8to32(key, 16); p0 = f & 0xffffffff
108 f = p1 + u8to32(key, 20) + (f >> 32); p1 = f & 0xffffffff
109 f = p2 + u8to32(key, 24) + (f >> 32); p2 = f & 0xffffffff
110 f = p3 + u8to32(key, 28) + (f >> 32); p3 = f & 0xffffffff
111 tag[0] = (p0 & 0xff) as u8; tag[1] = ((p0 >> 8) & 0xff) as u8; tag[2] = ((p0 >> 16) & 0xff) as u8; tag[3] = ((p0 >> 24) & 0xff) as u8
112 tag[4] = (p1 & 0xff) as u8; tag[5] = ((p1 >> 8) & 0xff) as u8; tag[6] = ((p1 >> 16) & 0xff) as u8; tag[7] = ((p1 >> 24) & 0xff) as u8
113 tag[8] = (p2 & 0xff) as u8; tag[9] = ((p2 >> 8) & 0xff) as u8; tag[10] = ((p2 >> 16) & 0xff) as u8; tag[11] = ((p2 >> 24) & 0xff) as u8
114 tag[12] = (p3 & 0xff) as u8; tag[13] = ((p3 >> 8) & 0xff) as u8; tag[14] = ((p3 >> 16) & 0xff) as u8; tag[15] = ((p3 >> 24) & 0xff) as u8
115 return 0
116}
117
118func pw(fd: i64, str: *u8) -> i64 { var n: i64 = 0; while str[n] != (0 as u8) { n = n + 1 } sys_write(fd, str, n); return 0 }
119func pwn(fd: i64, v: i64) -> i64 {
120 let bb: *u8 = sys_mmap(28); var m: i64 = v
121 let t: *u8 = sys_mmap(28); var k: i64 = 0
122 if m == 0 { t[0] = 48; k = 1 }
123 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
124 var i: i64 = 0
125 while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
126 sys_write(fd, bb, k); return 0
127}
128func pwhex(fd: i64, tag: *u8, n: i64) -> i64 {
129 let hx: *u8 = "0123456789abcdef" as *u8
130 let bb: *u8 = sys_mmap(64); var i: i64 = 0
131 while i < n {
132 bb[i * 2] = hx[(tag[i] as i64) >> 4]
133 bb[i * 2 + 1] = hx[(tag[i] as i64) & 15]
134 i = i + 1
135 }
136 sys_write(fd, bb, n * 2); return 0
137}
138
139func emit(fd: i64, okA: i64, diff: i64, tag: *u8, ok: i64) -> i64 {
140 pw(fd, "POLY1305GATE authored=organ engine=scalar-26bit-limb-donna task=rfc8439-2.5.2-kat" as *u8)
141 pw(fd, " | A_rfc_kat_pass=" as *u8); pwn(fd, okA)
142 pw(fd, " tag=" as *u8); pwhex(fd, tag, 16)
143 pw(fd, " want=a8061dc1305136c6c22b8baf0c0127a9" as *u8)
144 pw(fd, " | B_liarkill_tamper_differs=" as *u8); pwn(fd, diff)
145 if ok == 1 { pw(fd, " verdict=GREEN\n" as *u8) } else { pw(fd, " verdict=RED\n" as *u8) }
146 return 0
147}
148
149func main() -> i64 {
150 let key: *u8 = sys_mmap(32)
151 key[0] = 133 as u8; key[1] = 214 as u8; key[2] = 190 as u8; key[3] = 120 as u8
152 key[4] = 87 as u8; key[5] = 85 as u8; key[6] = 109 as u8; key[7] = 51 as u8
153 key[8] = 127 as u8; key[9] = 68 as u8; key[10] = 82 as u8; key[11] = 254 as u8
154 key[12] = 66 as u8; key[13] = 213 as u8; key[14] = 6 as u8; key[15] = 168 as u8
155 key[16] = 1 as u8; key[17] = 3 as u8; key[18] = 128 as u8; key[19] = 138 as u8
156 key[20] = 251 as u8; key[21] = 13 as u8; key[22] = 178 as u8; key[23] = 253 as u8
157 key[24] = 74 as u8; key[25] = 191 as u8; key[26] = 246 as u8; key[27] = 175 as u8
158 key[28] = 65 as u8; key[29] = 73 as u8; key[30] = 245 as u8; key[31] = 27 as u8
159 let exp: *u8 = sys_mmap(16)
160 exp[0] = 168 as u8; exp[1] = 6 as u8; exp[2] = 29 as u8; exp[3] = 193 as u8
161 exp[4] = 48 as u8; exp[5] = 81 as u8; exp[6] = 54 as u8; exp[7] = 198 as u8
162 exp[8] = 194 as u8; exp[9] = 43 as u8; exp[10] = 139 as u8; exp[11] = 175 as u8
163 exp[12] = 12 as u8; exp[13] = 1 as u8; exp[14] = 39 as u8; exp[15] = 169 as u8
164 let msg: *u8 = "Cryptographic Forum Research Group" as *u8
165 let mlen: i64 = 34
166 let tag: *u8 = sys_mmap(16)
167 poly1305(key, msg, mlen, tag)
168 var okA: i64 = 1
169 var i: i64 = 0
170 while i < 16 { if tag[i] != exp[i] { okA = 0 } i = i + 1 }
171 // liar-kill: tamper one message byte -> tag must differ
172 let msg2: *u8 = sys_mmap(40)
173 i = 0
174 while i < mlen { msg2[i] = msg[i]; i = i + 1 }
175 msg2[0] = (msg2[0] + 1) as u8
176 let tag2: *u8 = sys_mmap(16)
177 poly1305(key, msg2, mlen, tag2)
178 var diff: i64 = 0
179 i = 0
180 while i < 16 { if tag2[i] != exp[i] { diff = 1 } i = i + 1 }
181 let msg64: *u8 = sys_mmap(64)
182 i = 0
183 while i < 64 { msg64[i] = i as u8; i = i + 1 }
184 let tag64: *u8 = sys_mmap(16)
185 poly1305(key, msg64, 64, tag64)
186 pw(1, "TAG64_for_msg_0..63=" as *u8); pwhex(1, tag64, 16); pw(1, "\n" as *u8)
187 var ok: i64 = 1
188 if okA != 1 { ok = 0 }
189 if diff != 1 { ok = 0 }
190 emit(1, okA, diff, tag, ok)
191 let logf: i64 = sys_openat_append(POLY_LOG, 420)
192 if logf >= 0 { emit(logf, okA, diff, tag, ok); sys_close(logf) }
193 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
194 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
195 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
196 let ctr__dry: *i64 = gv_ctr()
197 ctr__dry[0] = ok
198 ctr__dry[1] = 1
199 let rc__dry: i64 = gv_verdict("POLY1305-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
200 sys_exit(rc__dry)
201 return rc__dry
202}