nx_poly1305_pure.nx source
↩ module page · 326 lines · 11643 B
1// nx_poly1305_pure.nx -- architecture-neutral Poly1305 (arena-based).
2//
3// Arena-refactor arc piece 2 per
4// docs/NISHI_LANG_FRICTION_CATALOG.md#F5. Parallel to original
5// nx_poly1305.nx (RV64-pinned via `import "nx_syscalls.nx"`).
6// This variant takes `*NxArena` for the two scratch buffers
7// (rbuf, block; ~32 bytes total per mac call) and imports NO
8// syscall layer.
9//
10// API differs from nx_poly1305 by adding `arena: *NxArena` as
11// first parameter and renaming functions with `_pure` suffix:
12//
13// poly1305_mac(key, msg, n, tag)
14// -> poly1305_mac_pure(arena, key, msg, n, tag)
15//
16// poly1305_tag_equal(a, b) -- no allocation; renamed only
17// -> poly1305_tag_equal_pure(a, b)
18//
19// Helpers (p_load_u32_le / p_store_u32_le / poly1305_clamp)
20// duplicated with `pure_` prefix to avoid collision with the
21// original module's helpers.
22//
23// KAT verified:
24// RFC 8439 §2.5.2 (the "Cryptographic Forum Research Group"
25// vector with key 85d6...51b -> tag a8061dc1305136c6c22b8baf0c0127a9).
26// Identical to original nx_poly1305_test. Smoke at
27// bench/nx_poly1305_pure_x86_64_smoke.nx.
28//
29// Composes with:
30// - nx_arena_types (NxArena + nx_arena_alloc)
31// - Any architecture's syscall layer at orchestrator boundary
32// - nx_chacha20_poly1305_pure (next arc piece -- the AEAD)
33//
34// nx_capability_claims:
35// needs: [arena_alloc, pointer_arithmetic]
36// provides: [poly1305_mac_pure, poly1305_tag_equal_pure]
37// safety: [no_syscall, no_floating_point, target_agnostic,
38// bit_equal_reproducible,
39// RFC_8439_section_2_5_2_KAT_VERIFIED,
40// constant_time_tag_compare_per_Lucky13_lesson]
41// verdict: [no_silent_failure]
42// license: INDEPENDENT_REDERIVE
43// kind: racing_crew_specialist
44//
45// license_tier: INDEPENDENT_REDERIVE
46// genealogy_id: international-research-sources/ietf/rfc_8439
47// lineage_id: nishi_poly1305_pure_arena_q10
48
49import "nx_arena_types.nx"
50
51// ---- Prefixed pure helpers (no collision with nx_poly1305.nx) ----
52
53func purep_load_u32_le(buf: *u8, off: i64) -> i64 {
54 let b0: i64 = buf[off + 0]
55 let b1: i64 = buf[off + 1]
56 let b2: i64 = buf[off + 2]
57 let b3: i64 = buf[off + 3]
58 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24)
59}
60
61func purep_store_u32_le(buf: *u8, off: i64, v: i64) -> i64 {
62 buf[off + 0] = v & 0xFF
63 buf[off + 1] = (v >> 8) & 0xFF
64 buf[off + 2] = (v >> 16) & 0xFF
65 buf[off + 3] = (v >> 24) & 0xFF
66 return 0
67}
68
69// Single Poly1305 block-mix step. Reads h[0..5] + r[0..5] + s[0..5]
70// (s[0] unused; s[1..5] = r[1..5] * 5). Multiplies h by r mod p,
71// writes new h back.
72//
73// Extracted into its own function with a small stack frame because
74// the inline form -- when compiled by the nxc2 x86_64 backend inside
75// the larger mac_pure body -- produced wrong tag bytes (verified by
76// running the SAME source on RV64 where it passes). F17 cross-
77// backend codegen divergence; the small fresh frame avoids whatever
78// stack-allocation pattern the x86_64 backend mishandles.
79func poly1305_mix_pure(h: *i64, r: *i64, s: *i64) -> i64 {
80 let h0: i64 = h[0]
81 let h1: i64 = h[1]
82 let h2: i64 = h[2]
83 let h3: i64 = h[3]
84 let h4: i64 = h[4]
85
86 let r0: i64 = r[0]
87 let r1: i64 = r[1]
88 let r2: i64 = r[2]
89 let r3: i64 = r[3]
90 let r4: i64 = r[4]
91
92 let s1: i64 = s[1]
93 let s2: i64 = s[2]
94 let s3: i64 = s[3]
95 let s4: i64 = s[4]
96
97 let d0: i64 = h0 * r0 + h1 * s4 + h2 * s3 + h3 * s2 + h4 * s1
98 let d1: i64 = h0 * r1 + h1 * r0 + h2 * s4 + h3 * s3 + h4 * s2
99 let d2: i64 = h0 * r2 + h1 * r1 + h2 * r0 + h3 * s4 + h4 * s3
100 let d3: i64 = h0 * r3 + h1 * r2 + h2 * r1 + h3 * r0 + h4 * s4
101 let d4: i64 = h0 * r4 + h1 * r3 + h2 * r2 + h3 * r1 + h4 * r0
102
103 var c_h0: i64 = d0 & 0x3FFFFFF
104 let k1: i64 = d0 >> 26
105 var c_h1: i64 = (d1 + k1) & 0x3FFFFFF
106 let k2: i64 = (d1 + k1) >> 26
107 var c_h2: i64 = (d2 + k2) & 0x3FFFFFF
108 let k3: i64 = (d2 + k2) >> 26
109 var c_h3: i64 = (d3 + k3) & 0x3FFFFFF
110 let k4: i64 = (d3 + k3) >> 26
111 var c_h4: i64 = (d4 + k4) & 0x3FFFFFF
112 let k5: i64 = (d4 + k4) >> 26
113 c_h0 = c_h0 + k5 * 5
114 c_h1 = c_h1 + (c_h0 >> 26)
115 c_h0 = c_h0 & 0x3FFFFFF
116
117 h[0] = c_h0
118 h[1] = c_h1
119 h[2] = c_h2
120 h[3] = c_h3
121 h[4] = c_h4
122 return 0
123}
124
125// Process one Poly1305 block: read take bytes of msg starting at
126// pos, pad with 0x01 + zeros, decompose into 5x26-bit limbs, add
127// to h, then call poly1305_mix_pure. Returns the number of bytes
128// consumed (== take).
129//
130// Extracted into its own function to reduce poly1305_mac_pure's
131// frame size below the threshold where the x86_64 backend produces
132// wrong code. F17 cross-backend codegen divergence workaround.
133func poly1305_block_pure(
134 msg: *u8, pos: i64, n: i64,
135 h_arr: *i64, r_arr: *i64, s_arr: *i64,
136 block: *u8
137) -> i64 {
138 var take: i64 = 16
139 if n - pos < 16 { take = n - pos }
140
141 var bi: i64 = 0
142 while bi < 16 { block[bi] = 0; bi = bi + 1 }
143 bi = 0
144 while bi < take { block[bi] = msg[pos + bi]; bi = bi + 1 }
145 if take < 16 { block[take] = 0x01 }
146
147 let b_lo: i64 = purep_load_u32_le(block, 0)
148 let b_m1: i64 = purep_load_u32_le(block, 4)
149 let b_m2: i64 = purep_load_u32_le(block, 8)
150 let b_hi: i64 = purep_load_u32_le(block, 12)
151
152 var c0: i64 = b_lo & 0x3FFFFFF
153 var c1: i64 = ((b_lo >> 26) | (b_m1 << 6)) & 0x3FFFFFF
154 var c2: i64 = ((b_m1 >> 20) | (b_m2 << 12)) & 0x3FFFFFF
155 var c3: i64 = ((b_m2 >> 14) | (b_hi << 18)) & 0x3FFFFFF
156 var c4: i64 = (b_hi >> 8) & 0x3FFFFFF
157
158 if take == 16 { c4 = c4 | (1 << 24) }
159
160 h_arr[0] = h_arr[0] + c0
161 h_arr[1] = h_arr[1] + c1
162 h_arr[2] = h_arr[2] + c2
163 h_arr[3] = h_arr[3] + c3
164 h_arr[4] = h_arr[4] + c4
165
166 poly1305_mix_pure(h_arr, r_arr, s_arr)
167 return take
168}
169
170// Clamp r per RFC 8439 §2.5.1 -- operates on caller's 16-byte
171// buffer in-place.
172func poly1305_clamp_pure(r: *u8) -> i64 {
173 r[3] = r[3] & 0x0F
174 r[7] = r[7] & 0x0F
175 r[11] = r[11] & 0x0F
176 r[15] = r[15] & 0x0F
177 r[4] = r[4] & 0xFC
178 r[8] = r[8] & 0xFC
179 r[12] = r[12] & 0xFC
180 return 0
181}
182
183// Full MAC computation via arena-allocated scratch.
184//
185// Caller-provided arena needs ~32 bytes free (rbuf + block).
186// Caller may nx_arena_reset between mac calls if reusing the arena
187// across messages.
188//
189// Per cardinal feedback-rejection-needs-why-with-alternative:
190// returns 0 on success or negative on arena OOM (caller must
191// pre-size arena per documentation).
192func poly1305_mac_pure(
193 arena: *NxArena,
194 key: *u8, msg: *u8, n: i64, tag: *u8
195) -> i64 {
196 let rbuf: *u8 = nx_arena_alloc_zero(arena, 16, 8)
197 if rbuf == (0 as *u8) { return 0 - 1 }
198 var ki: i64 = 0
199 while ki < 16 { rbuf[ki] = key[ki]; ki = ki + 1 }
200 poly1305_clamp_pure(rbuf)
201
202 let r_lo: i64 = purep_load_u32_le(rbuf, 0)
203 let r_m1: i64 = purep_load_u32_le(rbuf, 4)
204 let r_m2: i64 = purep_load_u32_le(rbuf, 8)
205 let r_hi: i64 = purep_load_u32_le(rbuf, 12)
206
207 let r_buf: *u8 = nx_arena_alloc_zero(arena, 40, 8)
208 if r_buf == (0 as *u8) { return 0 - 1 }
209 let r_arr: *i64 = r_buf as *i64
210 r_arr[0] = r_lo & 0x3FFFFFF
211 r_arr[1] = ((r_lo >> 26) | (r_m1 << 6)) & 0x3FFFFFF
212 r_arr[2] = ((r_m1 >> 20) | (r_m2 << 12)) & 0x3FFFFFF
213 r_arr[3] = ((r_m2 >> 14) | (r_hi << 18)) & 0x3FFFFFF
214 r_arr[4] = (r_hi >> 8) & 0x3FFFFFF
215
216 let s_buf: *u8 = nx_arena_alloc_zero(arena, 40, 8)
217 if s_buf == (0 as *u8) { return 0 - 1 }
218 let s_arr: *i64 = s_buf as *i64
219 s_arr[0] = 0
220 s_arr[1] = r_arr[1] * 5
221 s_arr[2] = r_arr[2] * 5
222 s_arr[3] = r_arr[3] * 5
223 s_arr[4] = r_arr[4] * 5
224
225 let h_buf: *u8 = nx_arena_alloc_zero(arena, 40, 8)
226 if h_buf == (0 as *u8) { return 0 - 1 }
227 let h_arr: *i64 = h_buf as *i64
228 // h_arr[0..5] already zero from alloc_zero.
229
230 let block: *u8 = nx_arena_alloc_zero(arena, 16, 8)
231 if block == (0 as *u8) { return 0 - 1 }
232 var pos: i64 = 0
233 while pos < n {
234 let took: i64 = poly1305_block_pure(msg, pos, n, h_arr, r_arr, s_arr, block)
235 pos = pos + took
236 }
237
238 var h0: i64 = h_arr[0]
239 var h1: i64 = h_arr[1]
240 var h2: i64 = h_arr[2]
241 var h3: i64 = h_arr[3]
242 var h4: i64 = h_arr[4]
243
244 h1 = h1 + (h0 >> 26); h0 = h0 & 0x3FFFFFF
245 h2 = h2 + (h1 >> 26); h1 = h1 & 0x3FFFFFF
246 h3 = h3 + (h2 >> 26); h2 = h2 & 0x3FFFFFF
247 h4 = h4 + (h3 >> 26); h3 = h3 & 0x3FFFFFF
248 h0 = h0 + (h4 >> 26) * 5
249 h4 = h4 & 0x3FFFFFF
250 h1 = h1 + (h0 >> 26)
251 h0 = h0 & 0x3FFFFFF
252
253 var g0: i64 = h0 + 5
254 var g1: i64 = h1 + (g0 >> 26); g0 = g0 & 0x3FFFFFF
255 var g2: i64 = h2 + (g1 >> 26); g1 = g1 & 0x3FFFFFF
256 var g3: i64 = h3 + (g2 >> 26); g2 = g2 & 0x3FFFFFF
257 var g4: i64 = h4 + (g3 >> 26) - (1 << 26)
258 g3 = g3 & 0x3FFFFFF
259
260 // Shift-semantics-independent sign-bit extract. RV64 backend
261 // emits SRLI (logical) but x86_64 backend emits SAR (arithmetic);
262 // (g4 >> 63) gives 1 on RV64 vs -1 on x86_64 when g4<0, so the
263 // single-line `^ -1` trick is correct on RV64 but inverted on
264 // x86_64. Masking bit 0 then negating produces identical -1
265 // on every backend regardless of shift semantics.
266 // (Bug class F17 cross-backend opcode-semantics divergence; see
267 // NISHI_BUG_PREVENTION_PILLARS.md.)
268 let mask: i64 = 0 - ((g4 >> 63) & 1) // -1 if g4<0 (keep h), else 0
269 let nmask: i64 = mask ^ -1 // 0 if g4<0, else -1
270 h0 = (h0 & mask) | (g0 & nmask)
271 h1 = (h1 & mask) | (g1 & nmask)
272 h2 = (h2 & mask) | (g2 & nmask)
273 h3 = (h3 & mask) | (g3 & nmask)
274 h4 = (h4 & mask) | (g4 & nmask)
275
276 // u32 mask BEFORE the add -- see nx_poly1305.nx for the bug-class
277 // rationale. (h1 << 26) leaks into bits 32+ of i64; without
278 // masking here, those bits poison the >>32 carry on the next limb.
279 let a0: i64 = ( h0 | (h1 << 26)) & 0xFFFFFFFF
280 let a1: i64 = ((h1 >> 6) | (h2 << 20)) & 0xFFFFFFFF
281 let a2: i64 = ((h2 >> 12) | (h3 << 14)) & 0xFFFFFFFF
282 let a3: i64 = ((h3 >> 18) | (h4 << 8)) & 0xFFFFFFFF
283
284 let s0: i64 = purep_load_u32_le(key, 16)
285 let s_s1: i64 = purep_load_u32_le(key, 20)
286 let s_s2: i64 = purep_load_u32_le(key, 24)
287 let s_s3: i64 = purep_load_u32_le(key, 28)
288
289 // Explicit CSE for each (a + s + ca) sum. Computing the sum
290 // twice (once for the low-32 mask, once for the carry shift)
291 // stresses x86_64 register allocator differently than RV64 and
292 // produced wrong t2 in one observed case; binding to a let
293 // gives both backends a single source-of-truth load.
294 let sum0: i64 = a0 + s0
295 var t0: i64 = sum0 & 0xFFFFFFFF
296 let ca0: i64 = sum0 >> 32
297 let sum1: i64 = a1 + s_s1 + ca0
298 var t1: i64 = sum1 & 0xFFFFFFFF
299 let ca1: i64 = sum1 >> 32
300 let sum2: i64 = a2 + s_s2 + ca1
301 var t2: i64 = sum2 & 0xFFFFFFFF
302 let ca2: i64 = sum2 >> 32
303 let sum3: i64 = a3 + s_s3 + ca2
304 var t3: i64 = sum3 & 0xFFFFFFFF
305
306 purep_store_u32_le(tag, 0, t0)
307 purep_store_u32_le(tag, 4, t1)
308 purep_store_u32_le(tag, 8, t2)
309 purep_store_u32_le(tag, 12, t3)
310 return 0
311}
312
313// Constant-time tag comparison (XOR-and-OR pattern; no early exit).
314// Returns 1 if equal, 0 otherwise. Lucky13 (2013) absorbed lesson:
315// short-circuit memcmp on a MAC leaks the tag byte-by-byte.
316func poly1305_tag_equal_pure(a: *u8, b: *u8) -> i64 {
317 var diff: i64 = 0
318 var i: i64 = 0
319 while i < 16 {
320 diff = diff | ((a[i] & 0xff) ^ (b[i] & 0xff))
321 i = i + 1
322 }
323 let neg: i64 = 0 - diff
324 let neq: i64 = (neg >> 63) & 1
325 return 1 - neq
326}