nx_chacha20_extvec_gate.nx source

1// nx_chacha20_extvec_gate.nx -- FIFTH provably third-party-validated claim: ChaCha20 block function vs 2// RFC 8439 2.3.2, read from the same pinned document the Poly1305 gate uses. 3// 4// ★★★★★THIS GATE EXISTS BECAUSE ONE DOCUMENT CONTAINS TWO DIALECTS. RFC 8439 states its INPUTS as 5// colon-separated hex (Key = 00:01:...) and its OUTPUT as a HEXDUMP with an offset column and an ASCII 6// gutter: 7// 000 10 f1 e7 e4 d1 3b 59 15 50 0f dd 1f a3 20 71 c4 .....;Y.P.... q. 8// 032 d2 82 64 46 07 9f aa 09 14 c2 d7 05 d9 8b 02 a2 ..dF............ 9// The nibble-stream reader that is CORRECT for the Poly1305 section would produce COMPLETE GARBAGE here: 10// it would swallow the offset column (000/016/032/048 -- every character hex-valid) and then the ASCII 11// gutter (d, F, 3, a, b ... all hex-valid). ★A PARSER PROVEN ON ONE SECTION IS NOT PROVEN ON THE DOCUMENT. 12// 13// THE DISCRIMINATOR, chosen by looking at the layout rather than by guessing: a data byte is a 14// whitespace-delimited token of EXACTLY TWO hex characters. The offset is three characters; the ASCII 15// gutter contains no two-character all-hex token. So "accept only 2-char all-hex tokens" cleanly selects 16// the 64 data bytes and rejects both decorations -- no line/column arithmetic, nothing to drift. 17// 18// ★AND THE TARGET IS THE *SERIALIZED BLOCK*, NOT the "state after 20 rounds" printed just above it. 19// 2.3.2 shows THREE near-identical 16-word blocks (input state, after-20-rounds, and the final serialized 20// output = after-rounds PLUS input state). chacha20_block() returns the THIRD. Comparing against the 21// second is a silent mis-selection that yields a confident RED against a correct implementation -- 22// a document that shows its INTERMEDIATE STATES is more dangerous than one that shows only answers, 23// and the discriminator is SEMANTIC (what does the function return?), never syntactic. 24// license_tier: ORIGINAL expect_exit: 0 25import "nx_syscalls.nx" 26import "nx_sha256_wasm.nx" 27import "nx_chacha20.nx" 28import "nx_gate_verdict.nx" 29 30func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 31func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 } 32 33func nn(v: i64) -> i64 { 34 var m: i64 = v 35 if m < 0 { w("-" as *u8); m = 0 - m } 36 let t: *u8 = sys_mmap(32) 37 var k: i64 = 0 38 if m == 0 { t[0] = 48 as u8; k = 1 } 39 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 40 let b: *u8 = sys_mmap(32) 41 var j: i64 = 0 42 while j < k { b[j] = t[k - 1 - j]; j = j + 1 } 43 sys_write(1, b, k) 44 return 0 45} 46 47func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v } 48 49func hexval(c: i64) -> i64 { 50 if c >= 48 { if c <= 57 { return c - 48 } } 51 if c >= 97 { if c <= 102 { return c - 87 } } 52 if c >= 65 { if c <= 70 { return c - 55 } } 53 return 0 - 1 54} 55 56func isws(c: i64) -> i64 { 57 if c == 32 { return 1 } 58 if c == 10 { return 1 } 59 if c == 13 { return 1 } 60 if c == 9 { return 1 } 61 return 0 62} 63 64func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64 { 65 var i: i64 = 0 66 while s[i] != (0 as u8) { 67 if at + i >= n { return 0 } 68 if b[at + i] != s[i] { return 0 } 69 i = i + 1 70 } 71 return 1 72} 73 74func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64 { 75 var p: i64 = from 76 while p < n { 77 if starts(b, n, p, s) == 1 { return p } 78 p = p + 1 79 } 80 return 0 - 1 81} 82 83// Nibble-stream reader for the COLON-HEX inputs (Key / Nonce). Separators continue a run. 84func parsenib(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 { 85 var p: i64 = from 86 var got: i64 = 0 87 var have: i64 = 0 88 var hi: i64 = 0 89 while p < n { 90 if got >= want { return p } 91 let c: i64 = b[p] as i64 92 var sep: i64 = 0 93 if c == 58 { sep = 1 } 94 if isws(c) == 1 { sep = 1 } 95 if sep == 1 { p = p + 1 } 96 else { 97 let hv: i64 = hexval(c) 98 if hv < 0 { 99 if got > 0 { if got < want { got = 0; have = 0 } } 100 p = p + 1 101 } else { 102 if have == 0 { hi = hv; have = 1 } else { out[got] = ((hi * 16) + hv) as u8; got = got + 1; have = 0 } 103 p = p + 1 104 } 105 } 106 } 107 if got >= want { return p } 108 return 0 - 1 109} 110 111// HEXDUMP reader -- LINE-BOUNDED BY TOKEN POSITION, not by token content. 112// ⚠MY FIRST VERSION CLASSIFIED BY CONTENT ("a data byte is a 2-char all-hex token") and it is UNSOUND. 113// It happens to work on THIS section because its ASCII gutter is mostly dots -- but RFC 8439 2.4.2's 114// gutter is ENGLISH and contains the word "be", a whitespace-delimited exactly-2-char ALL-HEX token that 115// would be absorbed as byte 0xbe and shift every byte after it. 116// ★★★★LAW: A DISCRIMINATOR PROVEN ON ONE INSTANCE OF A DIALECT IS NOT PROVEN ON THE DIALECT. English in a 117// hexdump gutter will eventually spell be / ad / de / fa / ba. 118// So: per line, token 0 is the OFFSET (skipped), tokens 1..16 are the DATA, everything after is gutter and 119// is ignored by POSITION. Counting is structural; classifying by content is a guess that survives only 120// until the content changes. 121func parsedump(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 { 122 var p: i64 = from 123 var got: i64 = 0 124 // step to the start of the next line: `from` points just past the label 125 var dz: i64 = 0 126 while dz == 0 { 127 if p >= n { dz = 1 } 128 else { if b[p] == (10 as u8) { p = p + 1; dz = 1 } else { p = p + 1 } } 129 } 130 var tok: i64 = 0 131 while p < n { 132 if got >= want { return p } 133 // skip whitespace -- DONE-FLAG loops, never arithmetic-to-break. My first draft used `p = n + 1` 134 // to exit and then tried to undo it (`p = p - n - 1 + n`), which silently loses the real position. 135 // A loop whose exit corrupts the variable it was scanning is worse than no loop. 136 // skip spaces/tabs, but a NEWLINE ends the line and resets the token counter 137 var d1: i64 = 0 138 while d1 == 0 { 139 if p >= n { d1 = 1 } 140 else { 141 if b[p] == (10 as u8) { tok = 0; p = p + 1 } 142 else { if isws(b[p] as i64) == 1 { p = p + 1 } else { d1 = 1 } } 143 } 144 } 145 if p >= n { return 0 - 1 } 146 // measure the token (bounded by whitespace OR newline) 147 var end: i64 = p 148 var d2: i64 = 0 149 while d2 == 0 { 150 if end >= n { d2 = 1 } 151 else { if isws(b[end] as i64) == 1 { d2 = 1 } else { end = end + 1 } } 152 } 153 let len: i64 = end - p 154 // token 0 = offset column (skip). tokens 1..16 = the data bytes. Anything beyond 16 is the ASCII 155 // gutter and is ignored BY POSITION -- never by what it looks like. 156 if tok >= 1 { if tok <= 16 { if len == 2 { 157 let h1: i64 = hexval(b[p] as i64) 158 let h2: i64 = hexval(b[p + 1] as i64) 159 if h1 >= 0 { if h2 >= 0 { out[got] = ((h1 * 16) + h2) as u8; got = got + 1 } } 160 } } } 161 tok = tok + 1 162 p = end 163 } 164 if got >= want { return p } 165 return 0 - 1 166} 167 168func main() -> i64 { 169 w("nx_chacha20_extvec_gate -- ChaCha20 block vs RFC 8439 2.3.2, READ FROM THE FETCHED DOCUMENT\n" as *u8) 170 171 let lp: *i64 = sys_mmap(16) as *i64 172 lp[0] = 0 173 let b: *u8 = sys_read_file("knowledge/extvec/rfc8439.txt\x00" as *u8, lp) 174 if lp[0] <= 0 { w("RED: fetched vector file absent -- run nx_vecfetch.\n" as *u8); return 1 } 175 176 let ctx: *u8 = sys_mmap(1024) 177 let dig: *u8 = sys_mmap(64) 178 nx_sha256_one_shot(b, lp[0], ctx, dig) 179 let hx: *u8 = sys_mmap(80) 180 var i: i64 = 0 181 while i < 32 { 182 hx[i * 2] = hexnib(((dig[i] as i64) / 16) & 15) as u8 183 hx[i * 2 + 1] = hexnib((dig[i] as i64) & 15) as u8 184 i = i + 1 185 } 186 let want: *u8 = "25bef70fbf7a07ff45c2fe4cb7c6ce954eac687413d8610603268b4e4415324c\x00" as *u8 187 var pin: i64 = 1 188 i = 0 189 while i < 64 { if hx[i] != want[i] { pin = 0 } i = i + 1 } 190 w(" acquisition digest: " as *u8); wb(hx, 64); w("\n" as *u8) 191 if pin == 0 { w("RED: PIN FAILED -- not the file nx_vecfetch acquired.\n" as *u8); return 1 } 192 w(" PIN OK -- bytes match the digest computed in-process at the socket\n" as *u8) 193 194 let sec: i64 = findfrom(b, lp[0], "2.3.2. Test Vector for the ChaCha20 Block Function" as *u8, 0) 195 if sec < 0 { w("RED: could not locate section 2.3.2\n" as *u8); return 1 } 196 let sec2: i64 = findfrom(b, lp[0], "2.3.2. Test Vector for the ChaCha20 Block Function" as *u8, sec + 10) 197 var at: i64 = sec 198 if sec2 >= 0 { at = sec2 } 199 200 let lk: i64 = findfrom(b, lp[0], "Key = " as *u8, at) 201 if lk < 0 { w("RED: no 'Key = ' in 2.3.2\n" as *u8); return 1 } 202 let key: *u8 = sys_mmap(64) 203 if parsenib(b, lp[0], lk + 6, key, 32) < 0 { w("RED: key short\n" as *u8); return 1 } 204 205 let ln: i64 = findfrom(b, lp[0], "Nonce = " as *u8, at) 206 if ln < 0 { w("RED: no 'Nonce = ' in 2.3.2\n" as *u8); return 1 } 207 let nonce: *u8 = sys_mmap(32) 208 if parsenib(b, lp[0], ln + 8, nonce, 12) < 0 { w("RED: nonce short\n" as *u8); return 1 } 209 210 // THE SERIALIZED BLOCK -- the value chacha20_block() actually returns. NOT the "state after 20 rounds" 211 // printed above it, which is an intermediate and would slander a correct implementation. 212 let lsb: i64 = findfrom(b, lp[0], "Serialized Block:" as *u8, at) 213 if lsb < 0 { w("RED: no 'Serialized Block:' in 2.3.2\n" as *u8); return 1 } 214 let exp: *u8 = sys_mmap(128) 215 if parsedump(b, lp[0], lsb + 17, exp, 64) < 0 { w("RED: serialized block short\n" as *u8); return 1 } 216 217 let out: *u8 = sys_mmap(128) 218 chacha20_block(key, 1, nonce, out) 219 220 var pass: i64 = 0 221 var fail: i64 = 0 222 var same: i64 = 1 223 i = 0 224 while i < 64 { if out[i] != exp[i] { same = 0 } i = i + 1 } 225 if same == 1 { pass = pass + 1; w(" PASS T1: chacha20_block(key,1,nonce) == the document's Serialized Block (64 bytes)\n" as *u8) } 226 else { 227 fail = fail + 1 228 w(" FAIL T1: block mismatch. first expected byte=" as *u8); nn(exp[0] as i64) 229 w(" got=" as *u8); nn(out[0] as i64); w("\n" as *u8) 230 } 231 232 // NEGATIVE CONTROL: change the block counter; the keystream must change. 233 chacha20_block(key, 2, nonce, out) 234 var same2: i64 = 1 235 i = 0 236 while i < 64 { if out[i] != exp[i] { same2 = 0 } i = i + 1 } 237 if same2 == 0 { pass = pass + 1; w(" PASS NEG: counter=2 yields a different block (the check can fail)\n" as *u8) } 238 else { fail = fail + 1; w(" FAIL NEG: counter change did not alter the block\n" as *u8) } 239 240 w("\n refsrc=https://www.rfc-editor.org/rfc/rfc8439.txt\n" as *u8) 241 w(" refsrcdig=" as *u8); wb(hx, 64); w("\n" as *u8) 242 w(" ref=RFC8439-2.3.2 gate=nx_chacha20_extvec_gate\n" as *u8) 243 w("nx_chacha20_extvec_gate: pass=" as *u8); nn(pass); w(" fail=" as *u8); nn(fail) 244 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 245 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 246 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 247 let ctr__dry: *i64 = gv_ctr() 248 ctr__dry[0] = pass 249 ctr__dry[1] = pass + fail 250 let rc__dry: i64 = gv_verdict("CHACHA20-EXTVEC-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 251 sys_exit(rc__dry) 252 return rc__dry 253}