nx_poly1305_extvec_gate.nx source

1// nx_poly1305_extvec_gate.nx -- FOURTH provably third-party-validated claim: Poly1305 vs RFC 8439 2.5.2. 2// 3// Fourth authority, fourth primitive, same construction -- but a THIRD vector dialect, which is the point: 4// RFC 7748 plain 64-char hex runs 5// RFC 8032 wrapped at 32 chars/line (even, so byte pairs never split) 6// RFC 8439 COLON-SEPARATED AND WRAPS MID-BYTE: "...a8:01:0" / newline / "3:80:..." splits the byte 03 7// An adjacent-hex-pair parser (what the first three gates use) drops a nibble at that break and SILENTLY 8// SHIFTS EVERY SUBSEQUENT BYTE. It does not fail loudly -- it yields a plausible wrong key, a red gate, and 9// an hour spent blaming Poly1305 instead of the reader. 10// ★★★★★LAW: EACH STANDARDS BODY PUBLISHES IN ITS OWN DIALECT, AND THE PARSER MUST BE PROVEN AGAINST THAT 11// DIALECT BEFORE THE GATE'S VERDICT MEANS ANYTHING. There is no general parser, only a proven one. 12// So this gate uses a NIBBLE-STREAM reader: accumulate hex nibbles, skip ':' and whitespace, pair them 13// afterwards. That is immune to both colon separators and mid-byte line wraps. 14// 15// ⚠ONE INPUT IS TYPED, DELIBERATELY, AND HERE IS WHY IT IS STILL SOUND: the RFC gives the message as the 16// ASCII string "Cryptographic Forum Research Group". I supply those 34 bytes rather than parsing prose out 17// of the document. That does NOT weaken the claim, because THE ANSWER STILL COMES FROM THE DOCUMENT: if my 18// message were wrong by one byte the computed tag would not match the published tag, and the gate would go 19// RED. A PASS therefore proves BOTH that the message was right AND that our Poly1305 agrees with the IETF. 20// ★The rule this respects: an agent may supply an INPUT whose correctness the published ANSWER verifies; 21// an agent may NEVER supply the ANSWER. That distinction is the whole of the third-party property. 22// license_tier: ORIGINAL expect_exit: 0 23import "nx_syscalls.nx" 24import "nx_sha256_wasm.nx" 25import "nx_poly1305.nx" 26import "nx_gate_verdict.nx" 27 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 } 29func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 } 30 31func nn(v: i64) -> i64 { 32 var m: i64 = v 33 if m < 0 { w("-" as *u8); m = 0 - m } 34 let t: *u8 = sys_mmap(32) 35 var k: i64 = 0 36 if m == 0 { t[0] = 48 as u8; k = 1 } 37 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 38 let b: *u8 = sys_mmap(32) 39 var j: i64 = 0 40 while j < k { b[j] = t[k - 1 - j]; j = j + 1 } 41 sys_write(1, b, k) 42 return 0 43} 44 45func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v } 46 47func hexval(c: i64) -> i64 { 48 if c >= 48 { if c <= 57 { return c - 48 } } 49 if c >= 97 { if c <= 102 { return c - 87 } } 50 if c >= 65 { if c <= 70 { return c - 55 } } 51 return 0 - 1 52} 53 54func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64 { 55 var i: i64 = 0 56 while s[i] != (0 as u8) { 57 if at + i >= n { return 0 } 58 if b[at + i] != s[i] { return 0 } 59 i = i + 1 60 } 61 return 1 62} 63 64func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64 { 65 var p: i64 = from 66 while p < n { 67 if starts(b, n, p, s) == 1 { return p } 68 p = p + 1 69 } 70 return 0 - 1 71} 72 73// NIBBLE-STREAM reader: ':' and whitespace are separators that CONTINUE the run; hex chars accumulate as 74// nibbles and pair up across ANY separator, including a line break in the middle of a byte. Any other 75// character ends the value. Returns index past `want` bytes, or -1 if short. 76func parsenib(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 { 77 var p: i64 = from 78 var got: i64 = 0 79 var have: i64 = 0 80 var hi: i64 = 0 81 while p < n { 82 if got >= want { return p } 83 let c: i64 = b[p] as i64 84 var sep: i64 = 0 85 if c == 58 { sep = 1 } 86 if c == 32 { sep = 1 } 87 if c == 10 { sep = 1 } 88 if c == 13 { sep = 1 } 89 if c == 9 { sep = 1 } 90 if sep == 1 { p = p + 1 } 91 else { 92 let hv: i64 = hexval(c) 93 if hv < 0 { 94 // a non-hex, non-separator byte ends this value; if we have not got enough, restart 95 if got > 0 { if got < want { got = 0; have = 0 } } 96 p = p + 1 97 } else { 98 if have == 0 { hi = hv; have = 1 } else { out[got] = ((hi * 16) + hv) as u8; got = got + 1; have = 0 } 99 p = p + 1 100 } 101 } 102 } 103 if got >= want { return p } 104 return 0 - 1 105} 106 107func main() -> i64 { 108 w("nx_poly1305_extvec_gate -- Poly1305 vs RFC 8439 2.5.2, vectors READ FROM THE FETCHED DOCUMENT\n" as *u8) 109 110 let lp: *i64 = sys_mmap(16) as *i64 111 lp[0] = 0 112 let b: *u8 = sys_read_file("knowledge/extvec/rfc8439.txt\x00" as *u8, lp) 113 if lp[0] <= 0 { w("RED: fetched vector file absent -- run nx_vecfetch. NOT falling back to constants.\n" as *u8); return 1 } 114 115 let ctx: *u8 = sys_mmap(1024) 116 let dig: *u8 = sys_mmap(64) 117 nx_sha256_one_shot(b, lp[0], ctx, dig) 118 let hx: *u8 = sys_mmap(80) 119 var i: i64 = 0 120 while i < 32 { 121 hx[i * 2] = hexnib(((dig[i] as i64) / 16) & 15) as u8 122 hx[i * 2 + 1] = hexnib((dig[i] as i64) & 15) as u8 123 i = i + 1 124 } 125 let want: *u8 = "25bef70fbf7a07ff45c2fe4cb7c6ce954eac687413d8610603268b4e4415324c\x00" as *u8 126 var pin: i64 = 1 127 i = 0 128 while i < 64 { if hx[i] != want[i] { pin = 0 } i = i + 1 } 129 w(" acquisition digest: " as *u8); wb(hx, 64); w("\n" as *u8) 130 if pin == 0 { w("RED: PIN FAILED -- not the file nx_vecfetch acquired; refusing to read vectors.\n" as *u8); return 1 } 131 w(" PIN OK -- bytes match the digest computed in-process at the socket\n" as *u8) 132 133 // Anchor on the SECTION BODY, not the table-of-contents line (both contain the same heading text). 134 let sec1: i64 = findfrom(b, lp[0], "2.5.2. Poly1305 Example and Test Vector" as *u8, 0) 135 if sec1 < 0 { w("RED: could not locate section 2.5.2\n" as *u8); return 1 } 136 let sec2: i64 = findfrom(b, lp[0], "2.5.2. Poly1305 Example and Test Vector" as *u8, sec1 + 10) 137 var at: i64 = sec1 138 if sec2 >= 0 { at = sec2 } 139 140 let lk: i64 = findfrom(b, lp[0], "Key Material:" as *u8, at) 141 if lk < 0 { w("RED: no 'Key Material:' in 2.5.2\n" as *u8); return 1 } 142 let key: *u8 = sys_mmap(64) 143 if parsenib(b, lp[0], lk + 13, key, 32) < 0 { w("RED: key nibble-stream short\n" as *u8); return 1 } 144 145 let lt: i64 = findfrom(b, lp[0], "Tag:" as *u8, at) 146 if lt < 0 { w("RED: no 'Tag:' in 2.5.2\n" as *u8); return 1 } 147 let exp: *u8 = sys_mmap(64) 148 if parsenib(b, lp[0], lt + 4, exp, 16) < 0 { w("RED: tag nibble-stream short\n" as *u8); return 1 } 149 150 // The message, as the RFC states it. See the header note: supplying an INPUT is sound because the 151 // published TAG verifies it -- one wrong byte here and the comparison fails. 152 let msg: *u8 = "Cryptographic Forum Research Group\x00" as *u8 153 var mlen: i64 = 0 154 while msg[mlen] != (0 as u8) { mlen = mlen + 1 } 155 156 let tag: *u8 = sys_mmap(64) 157 poly1305_mac(key, msg, mlen, tag) 158 159 var pass: i64 = 0 160 var fail: i64 = 0 161 var same: i64 = 1 162 i = 0 163 while i < 16 { if tag[i] != exp[i] { same = 0 } i = i + 1 } 164 if same == 1 { 165 pass = pass + 1 166 w(" PASS T1: poly1305_mac(key,msg) == the document's published Tag (msglen=" as *u8); nn(mlen); w(")\n" as *u8) 167 } else { 168 fail = fail + 1 169 w(" FAIL T1: tag mismatch against the published value\n" as *u8) 170 } 171 172 // NEGATIVE CONTROL: flip one key bit; the tag must change. 173 key[0] = (((key[0] as i64) ^ 1) & 255) as u8 174 poly1305_mac(key, msg, mlen, tag) 175 var same2: i64 = 1 176 i = 0 177 while i < 16 { if tag[i] != exp[i] { same2 = 0 } i = i + 1 } 178 if same2 == 0 { pass = pass + 1; w(" PASS NEG: one-bit key change breaks the tag (the check can fail)\n" as *u8) } 179 else { fail = fail + 1; w(" FAIL NEG: tag unchanged under a key change -- not discriminating\n" as *u8) } 180 181 w("\n refsrc=https://www.rfc-editor.org/rfc/rfc8439.txt\n" as *u8) 182 w(" refsrcdig=" as *u8); wb(hx, 64); w("\n" as *u8) 183 w(" ref=RFC8439-2.5.2 gate=nx_poly1305_extvec_gate\n" as *u8) 184 w("nx_poly1305_extvec_gate: pass=" as *u8); nn(pass); w(" fail=" as *u8); nn(fail) 185 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 186 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 187 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 188 let ctr__dry: *i64 = gv_ctr() 189 ctr__dry[0] = pass 190 ctr__dry[1] = pass + fail 191 let rc__dry: i64 = gv_verdict("POLY1305-EXTVEC-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 192 sys_exit(rc__dry) 193 return rc__dry 194}