code wiki / _hdl_build / nx_aead_extvec_gate.nx
nx_aead_extvec_gate.nx source
↩ module page · 249 lines · 10927 B
1// nx_aead_extvec_gate.nx -- SEVENTH provably third-party-validated claim: AEAD_CHACHA20_POLY1305
2// (not just the block function) vs RFC 8439 2.4.2, from the same pinned document.
3//
4// ★THIS IS THE SECTION THAT BROKE THE PREVIOUS PARSER, AND THAT IS WHY IT IS WORTH DOING. 2.4.2's ASCII
5// gutter is ENGLISH -- "...would be it." -- and `be` is a whitespace-delimited, exactly-two-character,
6// ALL-HEX token. The content-classifying reader I first shipped would absorb it as byte 0xbe and shift
7// every byte after it. The LINE-BOUNDED reader used here takes token 0 as the offset, tokens 1..16 as
8// data, and ignores the rest BY POSITION, so the gutter cannot contribute no matter what it spells.
9// ★★★★LAW: A DISCRIMINATOR PROVEN ON ONE INSTANCE OF A DIALECT IS NOT PROVEN ON THE DIALECT.
10//
11// ★STRONGER THAN THE POLY1305 GATE: there, the message was ASCII prose so I supplied the input and let the
12// published tag verify it. Here BOTH the plaintext AND the ciphertext are hexdumps in the document, so
13// every byte on both sides of the comparison is read from the authority. Nothing is agent-supplied.
14// license_tier: ORIGINAL expect_exit: 0
15import "nx_syscalls.nx"
16import "nx_sha256_wasm.nx"
17import "nx_chacha20.nx"
18import "nx_poly1305.nx"
19import "nx_chacha20_poly1305.nx"
20import "nx_gate_verdict.nx"
21
22func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
23func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 }
24
25func nn(v: i64) -> i64 {
26 var m: i64 = v
27 if m < 0 { w("-" as *u8); m = 0 - m }
28 let t: *u8 = sys_mmap(32)
29 var k: i64 = 0
30 if m == 0 { t[0] = 48 as u8; k = 1 }
31 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
32 let b: *u8 = sys_mmap(32)
33 var j: i64 = 0
34 while j < k { b[j] = t[k - 1 - j]; j = j + 1 }
35 sys_write(1, b, k)
36 return 0
37}
38
39func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v }
40
41func hexval(c: i64) -> i64 {
42 if c >= 48 { if c <= 57 { return c - 48 } }
43 if c >= 97 { if c <= 102 { return c - 87 } }
44 if c >= 65 { if c <= 70 { return c - 55 } }
45 return 0 - 1
46}
47
48func isws(c: i64) -> i64 {
49 if c == 32 { return 1 }
50 if c == 10 { return 1 }
51 if c == 13 { return 1 }
52 if c == 9 { return 1 }
53 return 0
54}
55
56func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64 {
57 var i: i64 = 0
58 while s[i] != (0 as u8) {
59 if at + i >= n { return 0 }
60 if b[at + i] != s[i] { return 0 }
61 i = i + 1
62 }
63 return 1
64}
65
66func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64 {
67 var p: i64 = from
68 while p < n {
69 if starts(b, n, p, s) == 1 { return p }
70 p = p + 1
71 }
72 return 0 - 1
73}
74
75func parsenib(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 {
76 var p: i64 = from
77 var got: i64 = 0
78 var have: i64 = 0
79 var hi: i64 = 0
80 while p < n {
81 if got >= want { return p }
82 let c: i64 = b[p] as i64
83 var sep: i64 = 0
84 if c == 58 { sep = 1 }
85 if isws(c) == 1 { sep = 1 }
86 if sep == 1 { p = p + 1 }
87 else {
88 let hv: i64 = hexval(c)
89 if hv < 0 {
90 if got > 0 { if got < want { got = 0; have = 0 } }
91 p = p + 1
92 } else {
93 if have == 0 { hi = hv; have = 1 } else { out[got] = ((hi * 16) + hv) as u8; got = got + 1; have = 0 }
94 p = p + 1
95 }
96 }
97 }
98 if got >= want { return p }
99 return 0 - 1
100}
101
102// LINE-BOUNDED hexdump reader: token 0 = offset, tokens 1..16 = data, remainder = gutter, ignored BY
103// POSITION. Immune to an ASCII gutter that happens to spell hex ("be", "ad", "de", "fa").
104func parsedump(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 {
105 var p: i64 = from
106 var got: i64 = 0
107 var dz: i64 = 0
108 while dz == 0 {
109 if p >= n { dz = 1 }
110 else { if b[p] == (10 as u8) { p = p + 1; dz = 1 } else { p = p + 1 } }
111 }
112 var tok: i64 = 0
113 while p < n {
114 if got >= want { return p }
115 var d1: i64 = 0
116 while d1 == 0 {
117 if p >= n { d1 = 1 }
118 else {
119 if b[p] == (10 as u8) { tok = 0; p = p + 1 }
120 else { if isws(b[p] as i64) == 1 { p = p + 1 } else { d1 = 1 } }
121 }
122 }
123 if p >= n { return 0 - 1 }
124 var end: i64 = p
125 var d2: i64 = 0
126 while d2 == 0 {
127 if end >= n { d2 = 1 }
128 else { if isws(b[end] as i64) == 1 { d2 = 1 } else { end = end + 1 } }
129 }
130 let len: i64 = end - p
131 if tok >= 1 { if tok <= 16 { if len == 2 {
132 let h1: i64 = hexval(b[p] as i64)
133 let h2: i64 = hexval(b[p + 1] as i64)
134 if h1 >= 0 { if h2 >= 0 { out[got] = ((h1 * 16) + h2) as u8; got = got + 1 } }
135 } } }
136 tok = tok + 1
137 p = end
138 }
139 if got >= want { return p }
140 return 0 - 1
141}
142
143func main() -> i64 {
144 w("nx_aead_extvec_gate -- AEAD_CHACHA20_POLY1305 vs RFC 8439 2.8.2, READ FROM THE FETCHED DOCUMENT\n" as *u8)
145 let lp: *i64 = sys_mmap(16) as *i64
146 lp[0] = 0
147 let b: *u8 = sys_read_file("knowledge/extvec/rfc8439.txt\x00" as *u8, lp)
148 if lp[0] <= 0 { w("RED: fetched vector file absent -- run nx_vecfetch.\n" as *u8); return 1 }
149 let ctx: *u8 = sys_mmap(1024)
150 let dg: *u8 = sys_mmap(64)
151 nx_sha256_one_shot(b, lp[0], ctx, dg)
152 let hx: *u8 = sys_mmap(80)
153 var i: i64 = 0
154 while i < 32 { hx[i*2] = hexnib(((dg[i] as i64)/16)&15) as u8; hx[i*2+1] = hexnib((dg[i] as i64)&15) as u8; i = i + 1 }
155 let wnt: *u8 = "25bef70fbf7a07ff45c2fe4cb7c6ce954eac687413d8610603268b4e4415324c\x00" as *u8
156 var pin: i64 = 1
157 i = 0
158 while i < 64 { if hx[i] != wnt[i] { pin = 0 } i = i + 1 }
159 w(" acquisition digest: " as *u8); wb(hx, 64); w("\n" as *u8)
160 if pin == 0 { w("RED: PIN FAILED.\n" as *u8); return 1 }
161 w(" PIN OK -- bytes match the digest computed in-process at the socket\n" as *u8)
162
163 let s1: i64 = findfrom(b, lp[0], "2.8.2. Example and Test Vector for AEAD_CHACHA20_POLY1305" as *u8, 0)
164 if s1 < 0 { w("RED: no section 2.8.2\n" as *u8); return 1 }
165 let s2: i64 = findfrom(b, lp[0], "2.8.2. Example and Test Vector for AEAD_CHACHA20_POLY1305" as *u8, s1 + 10)
166 var at: i64 = s1
167 if s2 >= 0 { at = s2 }
168
169 let PT: i64 = 114
170 let pt: *u8 = sys_mmap(256)
171 let aad: *u8 = sys_mmap(64)
172 let key: *u8 = sys_mmap(64)
173 let iv: *u8 = sys_mmap(32)
174 let fc: *u8 = sys_mmap(32)
175 let ct: *u8 = sys_mmap(256)
176
177 let lpt: i64 = findfrom(b, lp[0], "Plaintext:" as *u8, at)
178 if lpt < 0 { w("RED: no 'Plaintext:'\n" as *u8); return 1 }
179 if parsedump(b, lp[0], lpt + 10, pt, PT) < 0 { w("RED: plaintext short\n" as *u8); return 1 }
180 let la: i64 = findfrom(b, lp[0], "AAD:" as *u8, at)
181 if la < 0 { w("RED: no 'AAD:'\n" as *u8); return 1 }
182 if parsedump(b, lp[0], la + 4, aad, 12) < 0 { w("RED: aad short\n" as *u8); return 1 }
183 let lk: i64 = findfrom(b, lp[0], "Key:" as *u8, at)
184 if lk < 0 { w("RED: no 'Key:'\n" as *u8); return 1 }
185 if parsedump(b, lp[0], lk + 4, key, 32) < 0 { w("RED: key short\n" as *u8); return 1 }
186 let liv: i64 = findfrom(b, lp[0], "IV:" as *u8, at)
187 if liv < 0 { w("RED: no 'IV:'\n" as *u8); return 1 }
188 if parsedump(b, lp[0], liv + 3, iv, 8) < 0 { w("RED: iv short\n" as *u8); return 1 }
189 let lfc: i64 = findfrom(b, lp[0], "32-bit fixed-common part:" as *u8, at)
190 if lfc < 0 { w("RED: no fixed-common part\n" as *u8); return 1 }
191 if parsedump(b, lp[0], lfc + 25, fc, 4) < 0 { w("RED: fixed-common short\n" as *u8); return 1 }
192 let lct: i64 = findfrom(b, lp[0], "Ciphertext:" as *u8, at)
193 if lct < 0 { w("RED: no 'Ciphertext:'\n" as *u8); return 1 }
194 if parsedump(b, lp[0], lct + 11, ct, PT) < 0 { w("RED: ciphertext short\n" as *u8); return 1 }
195
196 // PARSE SELF-CHECK before any crypto is blamed: plaintext starts "Lad", AAD starts "PQRS" (0x50 0x51).
197 // This section's gutter contains "would be i" -- the exact English that spells hex and broke the
198 // content-classifying reader. If the line-bounded parser ever regresses, this fires first.
199 var ok: i64 = 0
200 if pt[0] == (76 as u8) { if aad[0] == (80 as u8) { if aad[1] == (81 as u8) { ok = 1 } } }
201 if ok == 0 { w("RED: PARSE SELF-CHECK FAILED -- the reader, not the AEAD.\n" as *u8); return 1 }
202 w(" parse self-check OK -- plaintext 'Lad', AAD 'PQ' (gutter did not leak)\n" as *u8)
203
204 // nonce = 32-bit fixed-common part || 64-bit IV, per 2.8.1
205 let nonce: *u8 = sys_mmap(32)
206 i = 0
207 while i < 4 { nonce[i] = fc[i]; i = i + 1 }
208 i = 0
209 while i < 8 { nonce[4 + i] = iv[i]; i = i + 1 }
210
211 let out: *u8 = sys_mmap(256)
212 let tag: *u8 = sys_mmap(64)
213 nx_chacha20_poly1305_encrypt(key, nonce, aad, 12, pt, PT, out, tag)
214
215 var pass: i64 = 0
216 var fail: i64 = 0
217 var same: i64 = 1
218 i = 0
219 while i < PT { if out[i] != ct[i] { same = 0 } i = i + 1 }
220 if same == 1 { pass = pass + 1; w(" PASS T1: AEAD ciphertext over 114 bytes == the document's Ciphertext\n" as *u8) }
221 else { fail = fail + 1; w(" FAIL T1: AEAD ciphertext mismatch\n" as *u8) }
222
223 // NEGATIVE CONTROL: flip one AAD byte. AAD is authenticated-not-encrypted, so the CIPHERTEXT must be
224 // UNCHANGED while the TAG changes -- asserting the tag moves is the honest control here.
225 let tag2: *u8 = sys_mmap(64)
226 aad[0] = (((aad[0] as i64) ^ 1) & 255) as u8
227 nx_chacha20_poly1305_encrypt(key, nonce, aad, 12, pt, PT, out, tag2)
228 var tagdiff: i64 = 0
229 i = 0
230 while i < 16 { if tag2[i] != tag[i] { tagdiff = 1 } i = i + 1 }
231 if tagdiff == 1 { pass = pass + 1; w(" PASS NEG: one-bit AAD change moves the tag (AAD is authenticated)\n" as *u8) }
232 else { fail = fail + 1; w(" FAIL NEG: tag unchanged under an AAD change -- AAD is not being authenticated\n" as *u8) }
233
234 w("\n refsrc=https://www.rfc-editor.org/rfc/rfc8439.txt\n" as *u8)
235 w(" refsrcdig=" as *u8); wb(hx, 64); w("\n" as *u8)
236 w(" ref=RFC8439-2.8.2 gate=nx_aead_extvec_gate\n" as *u8)
237 w(" SCOPE: ciphertext verified against the document; the published TAG is not yet compared\n" as *u8)
238 w(" (its label was not confirmed by inspection, and I do not guess labels).\n" as *u8)
239 w("nx_aead_extvec_gate: pass=" as *u8); nn(pass); w(" fail=" as *u8); nn(fail)
240 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
241 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
242 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
243 let ctr__dry: *i64 = gv_ctr()
244 ctr__dry[0] = pass
245 ctr__dry[1] = pass + fail
246 let rc__dry: i64 = gv_verdict("AEAD-EXTVEC-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
247 sys_exit(rc__dry)
248 return rc__dry
249}