code wiki / _hdl_build / nx_poly1305_gate.nx

nx_poly1305_gate.nx

buildroot/runtime/_hdl_build/nx_poly1305_gate.nx

9144 B194 linesdepth 2pulls 2 transitivereach 0 importersview sourcekind gate/prooftopic poly1305
docsdependenciesstructsconstsfunctions

about

nx_poly1305_gate.nx -- GATE for the SCALAR Poly1305 reference (the MAC half of the room's ChaCha20-Poly1305 AEAD). Proves, by RUNNING, byte-exact against the RFC-8439 ยง2.5.2 test vector. This is the CORRECTNESS FOUNDATION for the SIMD Poly1305 exceed (same 5x26-bit limb layout the AVX2 kernel will vectorize over powers of r). poly1305-donna 32-bit algorithm, 5 limbs of 26 bits each, products fit i64 (no 128-bit/mulq needed). TWO GATES: A RFC KAT: tag("Cryptographic Forum Research Group", rfc-key) == a8061dc1...27a9 (byte-exact). B LIAR-KILL: flip one message byte -> tag MUST differ from the RFC tag (kills a hardcoded cheat). genealogy_id: bernstein_2005_poly1305 (realized_in nx_poly1305) lineage_id: sovereign_poly1305_scalar_26bit_limb_v1 license_tier: ORIGINAL

dependencies 1 imports · 0 importers

nx_syscalls.nx nx_poly1305_gate.nx

imports: nx_syscalls.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main sys_mmap poly1305 sys_mmap ↻ u8to32 poly_block u8to32 ↻ pw sys_write pwhex sys_mmap ↻ sys_write ↻ emit pw ↻ pwn sys_mmap ↻ sys_write ↻ pwhex ↻ sys_openat_append sys_close

structs

none

consts

16const POLY_LOG: *u8 = "knowledge/status/poly1305.log"

functions

19func u8to32(p: *u8, o: i64) -> i64
called by 2: poly_blockpoly1305
25func poly_block(m: *u8, off: i64, hibit: i64, h: *i64, r: *i64, s: *i64) -> i64
called by 1: poly1305 calls 1: u8to32
52func poly1305(key: *u8, msg: *u8, mlen: i64, tag: *u8) -> i64
called by 1: main calls 3: sys_mmapu8to32poly_block
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 }
called by 2: emitmain calls 1: sys_write
118func pwn(fd: i64, v: i64) -> i64
called by 1: emit calls 2: sys_mmapsys_write
127func pwhex(fd: i64, tag: *u8, n: i64) -> i64
called by 2: emitmain calls 2: sys_mmapsys_write
138func emit(fd: i64, okA: i64, diff: i64, tag: *u8, ok: i64) -> i64
called by 1: main calls 3: pwpwnpwhex
148func main() -> i64
calls 7: sys_mmappoly1305pwpwhexemitsys_openat_append+1