code wiki / _hdl_build / nx_poly1305_gate.nx

nx_poly1305_gate.nx

buildroot/runtime/_hdl_build/nx_poly1305_gate.nx

9678 B202 linesdepth 3pulls 3 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 2 imports · 0 importers

nx_syscalls.nx nx_gate_verdict.nx nx_poly1305_gate.nx

imports: nx_syscalls.nxnx_gate_verdict.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 nxa_die sys_write sys_exit nxa_lock_take nxa_lock_addr sys_write ↻ nxa_lock_give nxa_lock_addr ↻ nxa_report_overrun sys_write ↻ nxa_dump_printable sys_write ↻ nxa_dump_sizes sys_write ↻ 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 gv_ctr sys_mmap ↻ gv_verdict gv_note_bare_rate gv_bare_rate gv_at

structs

none

consts

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

functions

20func u8to32(p: *u8, o: i64) -> i64
called by 2: poly_blockpoly1305
26func poly_block(m: *u8, off: i64, hibit: i64, h: *i64, r: *i64, s: *i64) -> i64
called by 1: poly1305 calls 1: u8to32
53func poly1305(key: *u8, msg: *u8, mlen: i64, tag: *u8) -> i64
called by 1: main calls 3: sys_mmapu8to32poly_block
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 }
called by 2: emitmain calls 1: sys_write
119func pwn(fd: i64, v: i64) -> i64
called by 1: emit calls 2: sys_mmapsys_write
128func pwhex(fd: i64, tag: *u8, n: i64) -> i64
called by 2: emitmain calls 2: sys_mmapsys_write
139func emit(fd: i64, okA: i64, diff: i64, tag: *u8, ok: i64) -> i64
called by 1: main calls 3: pwpwnpwhex
149func main() -> i64
calls 10: sys_mmappoly1305pwpwhexemitsys_openat_append+4