code wiki / _hdl_build / nx_poly1305_extvec_gate.nx

nx_poly1305_extvec_gate.nx

buildroot/runtime/_hdl_build/nx_poly1305_extvec_gate.nx

8819 B194 linesdepth 3pulls 5 transitivereach 0 importersview sourcekind gate/prooftopic poly1305
docsdependenciesstructsconstsfunctions

about

nx_poly1305_extvec_gate.nx -- FOURTH provably third-party-validated claim: Poly1305 vs RFC 8439 2.5.2. Fourth authority, fourth primitive, same construction -- but a THIRD vector dialect, which is the point: RFC 7748 plain 64-char hex runs RFC 8032 wrapped at 32 chars/line (even, so byte pairs never split) RFC 8439 COLON-SEPARATED AND WRAPS MID-BYTE: "...a8:01:0" / newline / "3:80:..." splits the byte 03 An adjacent-hex-pair parser (what the first three gates use) drops a nibble at that break and SILENTLY SHIFTS EVERY SUBSEQUENT BYTE. It does not fail loudly -- it yields a plausible wrong key, a red gate, and an hour spent blaming Poly1305 instead of the reader. ★★★★★LAW: EACH STANDARDS BODY PUBLISHES IN ITS OWN DIALECT, AND THE PARSER MUST BE PROVEN AGAINST THAT DIALECT BEFORE THE GATE'S VERDICT MEANS ANYTHING. There is no general parser, only a proven one. So this gate uses a NIBBLE-STREAM reader: accumulate hex nibbles, skip ':' and whitespace, pair them afterwards. That is immune to both colon separators and mid-byte line wraps. ⚠ONE INPUT IS TYPED, DELIBERATELY, AND HERE IS WHY IT IS STILL SOUND: the RFC gives the message as the ASCII string "Cryptographic Forum Research Group". I supply those 34 bytes rather than parsing prose out of the document. That does NOT weaken the claim, because THE ANSWER STILL COMES FROM THE DOCUMENT: if my message were wrong by one byte the computed tag would not match the published tag, and the gate would go RED. A PASS therefore proves BOTH that the message was right AND that our Poly1305 agrees with the IETF. ★The rule this respects: an agent may supply an INPUT whose correctness the published ANSWER verifies; an agent may NEVER supply the ANSWER. That distinction is the whole of the third-party property. license_tier: ORIGINAL expect_exit: 0

dependencies 4 imports · 0 importers

nx_syscalls.nx nx_sha256_wasm.nx nx_poly1305.nx nx_gate_verdict.nx nx_poly1305_extvec_gate.nx

imports: nx_syscalls.nxnx_sha256_wasm.nxnx_poly1305.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 w sys_write 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 ↻ sys_read_file sys_openat_rd sys_lseek sys_mmap ↻ sys_read sys_munmap sys_close nx_sha256_one_shot _h_set _sha256_compress _blk_word_be _rotr32 _h_get _sha256_k _h_set ↻ _h_get ↻ hexnib wb sys_write ↻ findfrom starts parsenib

structs

none

consts

none

functions

28func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
called by 2: nnmain calls 1: sys_write
29func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 }
called by 1: main calls 1: sys_write
31func nn(v: i64) -> i64
called by 1: main calls 3: wsys_mmapsys_write
45func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v }
called by 1: main
47func hexval(c: i64) -> i64
called by 1: parsenib
54func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64
called by 1: findfrom
64func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64
called by 1: main calls 1: starts
76func parsenib(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64
called by 1: main calls 1: hexval
107func main() -> i64