code wiki / _hdl_build / nx_poly1305_gate.nx
nx_poly1305_gate.nx source
↩ module page · 194 lines · 9144 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"
15
16const POLY_LOG: *u8 = "knowledge/status/poly1305.log"
17
18// load 4 little-endian bytes at p[o..o+3] as a 32-bit value (0 .. 2^32-1, fits i64).
19func u8to32(p: *u8, o: i64) -> i64 {
20 return (p[o] as i64) | ((p[o + 1] as i64) << 8) | ((p[o + 2] as i64) << 16) | ((p[o + 3] as i64) << 24)
21}
22
23// process one 16-byte block m[off..off+15] into accumulator h, given clamped r and s=r*5.
24// hibit = 0x1000000 (1<<24) for full blocks (the 2^128 term), 0 for the padded final block.
25func poly_block(m: *u8, off: i64, hibit: i64, h: *i64, r: *i64, s: *i64) -> i64 {
26 let t0: i64 = u8to32(m, off + 0)
27 let t1: i64 = u8to32(m, off + 4)
28 let t2: i64 = u8to32(m, off + 8)
29 let t3: i64 = u8to32(m, off + 12)
30 let a0: i64 = h[0] + (t0 & 0x3ffffff)
31 let a1: i64 = h[1] + (((t0 >> 26) | (t1 << 6)) & 0x3ffffff)
32 let a2: i64 = h[2] + (((t1 >> 20) | (t2 << 12)) & 0x3ffffff)
33 let a3: i64 = h[3] + (((t2 >> 14) | (t3 << 18)) & 0x3ffffff)
34 let a4: i64 = h[4] + ((t3 >> 8) | hibit)
35 var d0: i64 = a0 * r[0] + a1 * s[4] + a2 * s[3] + a3 * s[2] + a4 * s[1]
36 var d1: i64 = a0 * r[1] + a1 * r[0] + a2 * s[4] + a3 * s[3] + a4 * s[2]
37 var d2: i64 = a0 * r[2] + a1 * r[1] + a2 * r[0] + a3 * s[4] + a4 * s[3]
38 var d3: i64 = a0 * r[3] + a1 * r[2] + a2 * r[1] + a3 * r[0] + a4 * s[4]
39 var d4: i64 = a0 * r[4] + a1 * r[3] + a2 * r[2] + a3 * r[1] + a4 * r[0]
40 var c: i64 = d0 >> 26
41 h[0] = d0 & 0x3ffffff
42 d1 = d1 + c; c = d1 >> 26; h[1] = d1 & 0x3ffffff
43 d2 = d2 + c; c = d2 >> 26; h[2] = d2 & 0x3ffffff
44 d3 = d3 + c; c = d3 >> 26; h[3] = d3 & 0x3ffffff
45 d4 = d4 + c; c = d4 >> 26; h[4] = d4 & 0x3ffffff
46 h[0] = h[0] + c * 5; c = h[0] >> 26; h[0] = h[0] & 0x3ffffff
47 h[1] = h[1] + c
48 return 0
49}
50
51// full Poly1305: tag = (poly(msg) + s) mod 2^128, written 16 bytes LE to tag.
52func poly1305(key: *u8, msg: *u8, mlen: i64, tag: *u8) -> i64 {
53 let r: *i64 = (sys_mmap(48)) as *i64
54 let s: *i64 = (sys_mmap(48)) as *i64
55 let h: *i64 = (sys_mmap(48)) as *i64
56 let k0: i64 = u8to32(key, 0)
57 let k1: i64 = u8to32(key, 4)
58 let k2: i64 = u8to32(key, 8)
59 let k3: i64 = u8to32(key, 12)
60 r[0] = k0 & 0x3ffffff
61 r[1] = ((k0 >> 26) | (k1 << 6)) & 0x3ffff03
62 r[2] = ((k1 >> 20) | (k2 << 12)) & 0x3ffc0ff
63 r[3] = ((k2 >> 14) | (k3 << 18)) & 0x3f03fff
64 r[4] = (k3 >> 8) & 0x00fffff
65 s[1] = r[1] * 5
66 s[2] = r[2] * 5
67 s[3] = r[3] * 5
68 s[4] = r[4] * 5
69 h[0] = 0; h[1] = 0; h[2] = 0; h[3] = 0; h[4] = 0
70 var off: i64 = 0
71 while off + 16 <= mlen {
72 poly_block(msg, off, 0x1000000, h, r, s)
73 off = off + 16
74 }
75 let rem: i64 = mlen - off
76 if rem > 0 {
77 let buf: *u8 = sys_mmap(16)
78 var i: i64 = 0
79 while i < 16 { buf[i] = 0 as u8; i = i + 1 }
80 i = 0
81 while i < rem { buf[i] = msg[off + i]; i = i + 1 }
82 buf[rem] = 1 as u8
83 poly_block(buf, 0, 0, h, r, s)
84 }
85 // fully carry h
86 var c: i64 = h[1] >> 26; h[1] = h[1] & 0x3ffffff; h[2] = h[2] + c
87 c = h[2] >> 26; h[2] = h[2] & 0x3ffffff; h[3] = h[3] + c
88 c = h[3] >> 26; h[3] = h[3] & 0x3ffffff; h[4] = h[4] + c
89 c = h[4] >> 26; h[4] = h[4] & 0x3ffffff; h[0] = h[0] + c * 5
90 c = h[0] >> 26; h[0] = h[0] & 0x3ffffff; h[1] = h[1] + c
91 // g = h - p (p = 2^130-5): if g >= 0 (h >= p) use g
92 var g0: i64 = h[0] + 5; c = g0 >> 26; g0 = g0 & 0x3ffffff
93 var g1: i64 = h[1] + c; c = g1 >> 26; g1 = g1 & 0x3ffffff
94 var g2: i64 = h[2] + c; c = g2 >> 26; g2 = g2 & 0x3ffffff
95 var g3: i64 = h[3] + c; c = g3 >> 26; g3 = g3 & 0x3ffffff
96 var g4: i64 = h[4] + c - 0x4000000
97 if g4 >= 0 {
98 h[0] = g0; h[1] = g1; h[2] = g2; h[3] = g3; h[4] = g4
99 }
100 // pack 5x26 -> 4x32
101 var p0: i64 = (h[0] | (h[1] << 26)) & 0xffffffff
102 var p1: i64 = ((h[1] >> 6) | (h[2] << 20)) & 0xffffffff
103 var p2: i64 = ((h[2] >> 12) | (h[3] << 14)) & 0xffffffff
104 var p3: i64 = ((h[3] >> 18) | (h[4] << 8)) & 0xffffffff
105 // tag = (h + s) mod 2^128, s = key[16..31] LE
106 var f: i64 = p0 + u8to32(key, 16); p0 = f & 0xffffffff
107 f = p1 + u8to32(key, 20) + (f >> 32); p1 = f & 0xffffffff
108 f = p2 + u8to32(key, 24) + (f >> 32); p2 = f & 0xffffffff
109 f = p3 + u8to32(key, 28) + (f >> 32); p3 = f & 0xffffffff
110 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
111 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
112 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
113 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
114 return 0
115}
116
117func 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 }
118func pwn(fd: i64, v: i64) -> i64 {
119 let bb: *u8 = sys_mmap(28); var m: i64 = v
120 let t: *u8 = sys_mmap(28); var k: i64 = 0
121 if m == 0 { t[0] = 48; k = 1 }
122 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
123 var i: i64 = 0
124 while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
125 sys_write(fd, bb, k); return 0
126}
127func pwhex(fd: i64, tag: *u8, n: i64) -> i64 {
128 let hx: *u8 = "0123456789abcdef" as *u8
129 let bb: *u8 = sys_mmap(64); var i: i64 = 0
130 while i < n {
131 bb[i * 2] = hx[(tag[i] as i64) >> 4]
132 bb[i * 2 + 1] = hx[(tag[i] as i64) & 15]
133 i = i + 1
134 }
135 sys_write(fd, bb, n * 2); return 0
136}
137
138func emit(fd: i64, okA: i64, diff: i64, tag: *u8, ok: i64) -> i64 {
139 pw(fd, "POLY1305GATE authored=organ engine=scalar-26bit-limb-donna task=rfc8439-2.5.2-kat" as *u8)
140 pw(fd, " | A_rfc_kat_pass=" as *u8); pwn(fd, okA)
141 pw(fd, " tag=" as *u8); pwhex(fd, tag, 16)
142 pw(fd, " want=a8061dc1305136c6c22b8baf0c0127a9" as *u8)
143 pw(fd, " | B_liarkill_tamper_differs=" as *u8); pwn(fd, diff)
144 if ok == 1 { pw(fd, " verdict=GREEN\n" as *u8) } else { pw(fd, " verdict=RED\n" as *u8) }
145 return 0
146}
147
148func main() -> i64 {
149 let key: *u8 = sys_mmap(32)
150 key[0] = 133 as u8; key[1] = 214 as u8; key[2] = 190 as u8; key[3] = 120 as u8
151 key[4] = 87 as u8; key[5] = 85 as u8; key[6] = 109 as u8; key[7] = 51 as u8
152 key[8] = 127 as u8; key[9] = 68 as u8; key[10] = 82 as u8; key[11] = 254 as u8
153 key[12] = 66 as u8; key[13] = 213 as u8; key[14] = 6 as u8; key[15] = 168 as u8
154 key[16] = 1 as u8; key[17] = 3 as u8; key[18] = 128 as u8; key[19] = 138 as u8
155 key[20] = 251 as u8; key[21] = 13 as u8; key[22] = 178 as u8; key[23] = 253 as u8
156 key[24] = 74 as u8; key[25] = 191 as u8; key[26] = 246 as u8; key[27] = 175 as u8
157 key[28] = 65 as u8; key[29] = 73 as u8; key[30] = 245 as u8; key[31] = 27 as u8
158 let exp: *u8 = sys_mmap(16)
159 exp[0] = 168 as u8; exp[1] = 6 as u8; exp[2] = 29 as u8; exp[3] = 193 as u8
160 exp[4] = 48 as u8; exp[5] = 81 as u8; exp[6] = 54 as u8; exp[7] = 198 as u8
161 exp[8] = 194 as u8; exp[9] = 43 as u8; exp[10] = 139 as u8; exp[11] = 175 as u8
162 exp[12] = 12 as u8; exp[13] = 1 as u8; exp[14] = 39 as u8; exp[15] = 169 as u8
163 let msg: *u8 = "Cryptographic Forum Research Group" as *u8
164 let mlen: i64 = 34
165 let tag: *u8 = sys_mmap(16)
166 poly1305(key, msg, mlen, tag)
167 var okA: i64 = 1
168 var i: i64 = 0
169 while i < 16 { if tag[i] != exp[i] { okA = 0 } i = i + 1 }
170 // liar-kill: tamper one message byte -> tag must differ
171 let msg2: *u8 = sys_mmap(40)
172 i = 0
173 while i < mlen { msg2[i] = msg[i]; i = i + 1 }
174 msg2[0] = (msg2[0] + 1) as u8
175 let tag2: *u8 = sys_mmap(16)
176 poly1305(key, msg2, mlen, tag2)
177 var diff: i64 = 0
178 i = 0
179 while i < 16 { if tag2[i] != exp[i] { diff = 1 } i = i + 1 }
180 let msg64: *u8 = sys_mmap(64)
181 i = 0
182 while i < 64 { msg64[i] = i as u8; i = i + 1 }
183 let tag64: *u8 = sys_mmap(16)
184 poly1305(key, msg64, 64, tag64)
185 pw(1, "TAG64_for_msg_0..63=" as *u8); pwhex(1, tag64, 16); pw(1, "\n" as *u8)
186 var ok: i64 = 1
187 if okA != 1 { ok = 0 }
188 if diff != 1 { ok = 0 }
189 emit(1, okA, diff, tag, ok)
190 let logf: i64 = sys_openat_append(POLY_LOG, 420)
191 if logf >= 0 { emit(logf, okA, diff, tag, ok); sys_close(logf) }
192 if ok == 1 { return 0 }
193 return 1
194}