code wiki / _hdl_build / nx_hmaccounter_extvec_gate.nx
nx_hmaccounter_extvec_gate.nx source
↩ module page · 227 lines · 9442 B
1// nx_hmaccounter_extvec_gate.nx -- HMAC-SHA-1 over an 8-byte COUNTER, vs RFC 4226 Appendix D Table 1.
2//
3// CLOSES THE LAST UNGRADED TABLE IN A DOCUMENT ALREADY ON DISK. RFC 4226 Appendix D publishes TWO tables;
4// Table 2 (the HOTP codes) is graded by nx_hotp_extvec_gate, and Table 1 -- ten RAW HMAC-SHA-1 values keyed
5// by counter -- sat unused. ★ACQUIRED IS NOT COVERED, and a document is not finished when one of its tables
6// passes (third time this session: rfc6234/rfc9106 sat pinned-but-ungated, and RFC 4648 needed all four
7// encodings before it was actually done).
8//
9// ★WHY THIS IS NOT REDUNDANT WITH RFC 2202. RFC 2202 exercises HMAC-SHA-1 over ASCII strings and repeated
10// byte fills. Table 1 exercises it over an 8-BYTE BIG-ENDIAN COUNTER -- a message that is mostly ZERO bytes
11// with a low-order value, and exactly the shape HOTP/TOTP feed it in production.
12// * A PRIMITIVE VALIDATED ONLY ON THE INPUT SHAPES SOMEONE THOUGHT TO PUBLISH IS VALIDATED ONLY ON THOSE
13// SHAPES. Zero-heavy inputs are where length-handling and padding bugs hide.
14//
15// The secret is read from the document (`Secret = 0x3132...3930`), never typed from recall.
16// Document pinned to a CORROBORATED digest (sovereign fetch and .NET WebClient agree).
17// license_tier: ORIGINAL expect_exit: 0
18import "nx_syscalls.nx"
19import "nx_sha256_wasm.nx"
20import "nx_hmac_sha1.nx"
21import "nx_gate_verdict.nx"
22
23func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
24func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 }
25
26func nn(v: i64) -> i64 {
27 var m: i64 = v
28 if m < 0 { w("-" as *u8); m = 0 - m }
29 let t: *u8 = sys_mmap(32)
30 var k: i64 = 0
31 if m == 0 { t[0] = 48 as u8; k = 1 }
32 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
33 let b: *u8 = sys_mmap(32)
34 var j: i64 = 0
35 while j < k { b[j] = t[k - 1 - j]; j = j + 1 }
36 sys_write(1, b, k)
37 return 0
38}
39
40func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v }
41func ph(v: i64) -> i64 {
42 let t: *u8 = sys_mmap(8)
43 t[0] = hexnib((v / 16) & 15) as u8
44 t[1] = hexnib(v & 15) as u8
45 sys_write(1, t, 2)
46 return 0
47}
48func hexval(c: i64) -> i64 {
49 if c >= 48 { if c <= 57 { return c - 48 } }
50 if c >= 97 { if c <= 102 { return c - 87 } }
51 if c >= 65 { if c <= 70 { return c - 55 } }
52 return 0 - 1
53}
54func isws(c: i64) -> i64 {
55 if c == 32 { return 1 }
56 if c == 10 { return 1 }
57 if c == 13 { return 1 }
58 if c == 9 { return 1 }
59 return 0
60}
61func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64 {
62 var i: i64 = 0
63 while s[i] != (0 as u8) {
64 if at + i >= n { return 0 }
65 if b[at + i] != s[i] { return 0 }
66 i = i + 1
67 }
68 return 1
69}
70func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64 {
71 var p: i64 = from
72 while p < n { if starts(b, n, p, s) == 1 { return p } p = p + 1 }
73 return 0 - 1
74}
75func parsehex_run(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 {
76 var p: i64 = from
77 var got: i64 = 0
78 while got < want {
79 if p + 1 >= n { return 0 - 1 }
80 let h1: i64 = hexval(b[p] as i64)
81 let h2: i64 = hexval(b[p + 1] as i64)
82 if h1 < 0 { return 0 - 1 }
83 if h2 < 0 { return 0 - 1 }
84 out[got] = ((h1 * 16) + h2) as u8
85 got = got + 1
86 p = p + 2
87 }
88 return p
89}
90// Decimal token; endp receives the position just past it. ★endp is an OUT slot ONLY -- the caller keeps its
91// own cursor. Conflating the two cost a whole build in the TOTP gate.
92func next_dec(b: *u8, n: i64, p0: i64, endp: *i64) -> i64 {
93 var p: i64 = p0
94 var d: i64 = 0
95 while d == 0 {
96 if p >= n { return 0 - 1 }
97 if isws(b[p] as i64) == 1 { p = p + 1 } else { d = 1 }
98 }
99 var v: i64 = 0
100 var any: i64 = 0
101 var done: i64 = 0
102 while done == 0 {
103 if p >= n { done = 1 }
104 else {
105 let c: i64 = b[p] as i64
106 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); any = 1; p = p + 1 } else { done = 1 } }
107 else { done = 1 }
108 }
109 }
110 if any == 0 { return 0 - 1 }
111 endp[0] = p
112 return v
113}
114func skip_ws(b: *u8, n: i64, p0: i64) -> i64 {
115 var p: i64 = p0
116 while p < n { if isws(b[p] as i64) == 1 { p = p + 1 } else { return p } }
117 return p
118}
119
120func main() -> i64 {
121 w("nx_hmaccounter_extvec_gate -- HMAC-SHA-1 over an 8-byte counter, vs RFC 4226 Table 1\n" as *u8)
122
123 let lp: *i64 = sys_mmap(16) as *i64
124 lp[0] = 0
125 let b: *u8 = sys_read_file("knowledge/extvec/rfc4226.txt\x00" as *u8, lp)
126 if lp[0] <= 0 { w("RED: fetched vector file absent -- run nx_vecfetch.\n" as *u8); return 1 }
127
128 let ctx: *u8 = sys_mmap(1024)
129 let dg: *u8 = sys_mmap(64)
130 nx_sha256_one_shot(b, lp[0], ctx, dg)
131 let hx: *u8 = sys_mmap(80)
132 var i: i64 = 0
133 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 }
134 let wnt: *u8 = "db6974cd02ca33560ec3a191ee9b1016067cd11d1f5d89e7efa36be69482229d\x00" as *u8
135 var pin: i64 = 1
136 i = 0
137 while i < 64 { if hx[i] != wnt[i] { pin = 0 } i = i + 1 }
138 if pin == 0 { w("RED: PIN FAILED -- not the corroborated document.\n" as *u8); return 1 }
139 w(" PIN OK -- CORROBORATED (sovereign fetch and .NET WebClient agree)\n" as *u8)
140
141 let sat: i64 = findfrom(b, lp[0], "Secret = 0x" as *u8, 0)
142 if sat < 0 { w("RED: no secret in document\n" as *u8); return 1 }
143 let secret: *u8 = sys_mmap(64)
144 if parsehex_run(b, lp[0], sat + 11, secret, 20) < 0 { w("RED: secret short\n" as *u8); return 1 }
145 var sok: i64 = 0
146 if secret[0] == (49 as u8) { if secret[19] == (48 as u8) { sok = 1 } }
147 if sok == 0 { w("RED: PARSE SELF-CHECK FAILED -- secret is not the ASCII digit run; the READER.\n" as *u8); return 1 }
148 w(" secret parsed: 20 bytes, self-check OK\n\n" as *u8)
149
150 // Table 1 header. NOTE it is a PREFIX of nothing else, but Table 2's header begins with the same
151 // "Count Hexadecimal" -- anchoring on that shorter string finds THIS table first, which is why the
152 // HOTP gate had to use Table 2's FULL header. Here the full Table-1 header is used symmetrically.
153 let tab: i64 = findfrom(b, lp[0], "Count Hexadecimal HMAC-SHA-1" as *u8, 0)
154 if tab < 0 { w("RED: Table 1 header not found\n" as *u8); return 1 }
155 var p: i64 = tab
156 var dh: i64 = 0
157 while dh == 0 { if p >= lp[0] { dh = 1 } else { if b[p] == (10 as u8) { p = p + 1; dh = 1 } else { p = p + 1 } } }
158
159 let ep: *i64 = sys_mmap(16) as *i64
160 let exp: *u8 = sys_mmap(64)
161 let got: *u8 = sys_mmap(64)
162 let msg: *u8 = sys_mmap(32)
163
164 var pass: i64 = 0
165 var fail: i64 = 0
166 var seen: i64 = 0
167 var row: i64 = 0
168 while row < 10 {
169 ep[0] = 0
170 let cnt: i64 = next_dec(b, lp[0], p, ep)
171 if cnt < 0 { row = 10 }
172 else {
173 let after: i64 = ep[0]
174 let hstart: i64 = skip_ws(b, lp[0], after)
175 if parsehex_run(b, lp[0], hstart, exp, 20) < 0 { row = 10 }
176 else {
177 p = hstart + 40
178 // 8-byte BIG-ENDIAN counter, exactly as HOTP feeds it (RFC 4226 sec 5.1)
179 var k: i64 = 0
180 while k < 8 { msg[7 - k] = ((cnt >> (k * 8)) & 255) as u8; k = k + 1 }
181 hmac_sha1(secret, 20, msg, 8, got)
182 var same: i64 = 1
183 i = 0
184 while i < 20 { if got[i] != exp[i] { same = 0 } i = i + 1 }
185 seen = seen + 1
186 if same == 1 {
187 pass = pass + 1
188 w(" PASS count=" as *u8); nn(cnt); w(" HMAC=" as *u8)
189 var z: i64 = 0
190 while z < 6 { ph(exp[z] as i64); z = z + 1 }
191 w("...\n" as *u8)
192 } else {
193 fail = fail + 1
194 w(" FAIL count=" as *u8); nn(cnt); w(" expected " as *u8)
195 var z2: i64 = 0
196 while z2 < 8 { ph(exp[z2] as i64); z2 = z2 + 1 }
197 w(" got " as *u8)
198 z2 = 0
199 while z2 < 8 { ph(got[z2] as i64); z2 = z2 + 1 }
200 w("\n" as *u8)
201 }
202 row = row + 1
203 }
204 }
205 }
206
207 if seen < 10 {
208 w("\n RED: only " as *u8); nn(seen); w(" of 10 published values graded -- refusing GREEN on a partial read.\n" as *u8)
209 fail = fail + 1
210 }
211
212 w("\n refsrc=https://www.rfc-editor.org/rfc/rfc4226.txt\n" as *u8)
213 w(" refsrcdig=" as *u8); wb(hx, 64); w("\n" as *u8)
214 w(" ref=RFC4226-AppendixD-Table1 gate=nx_hmaccounter_extvec_gate\n" as *u8)
215 w(" BOUND: nx_hmac_sha1.nx -> nx_sha1.nx (the repaired family)\n" as *u8)
216 w("nx_hmaccounter_extvec_gate: values=" as *u8); nn(seen)
217 w(" pass=" as *u8); nn(pass); w(" fail=" as *u8); nn(fail)
218 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
219 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
220 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
221 let ctr__dry: *i64 = gv_ctr()
222 ctr__dry[0] = pass
223 ctr__dry[1] = pass + fail
224 let rc__dry: i64 = gv_verdict("HMACCOUNTER-EXTVEC-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
225 sys_exit(rc__dry)
226 return rc__dry
227}