code wiki / _hdl_build / nx_vc_gate.nx
nx_vc_gate.nx source
↩ module page · 298 lines · 14236 B
1// nx_vc_gate.nx -- ENGINEER gate for nx_video_client_wasm (the browser
2// client core). Runs NATIVELY (same source the WAT target ships) and
3// proves, evidence-driven:
4// - NV1 cross-implementation: containers packed with vc_* validate GREEN
5// under nx_nv1.nx (the team-side authority) and field-for-field match;
6// vc_nv1_next walks exactly the chunks that were packed
7// - wire frames: pack -> parse round-trips kind/id/seq/payload
8// - sample plane: integer IEEE-754 f32->i16 matches known vectors incl.
9// clamp/NaN/Inf/denormal edges; i16->f32 is exact on all 65536 values
10// (round-trips through the inverse map where exactness is defined)
11// - ladder governor: degrade/recover hysteresis decisions
12// license_tier: ORIGINAL
13
14import "nx_video_client_wasm.nx"
15import "nx_nv1_lpc.nx"
16
17func g_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
18func g_check(name: *u8, cond: i64) -> i64 {
19 if cond==1 { g_puts(" PASS " as *u8) } else { g_puts(" FAIL " as *u8) }
20 g_puts(name); g_puts("\n" as *u8); return cond
21}
22func g_pn(v: i64) -> i64 {
23 let b: *u8 = sys_mmap(28)
24 var x: i64 = v
25 if x < 0 { b[0]=45; sys_write(1,b,1); x = 0 - x }
26 if x == 0 { b[0]=48; sys_write(1,b,1); return 0 }
27 var d: i64=0; var y: i64=x
28 while y>0 { d=d+1; y=y/10 }
29 var i: i64=d-1; y=x
30 while i>=0 { b[i]=(48+(y%10)) as u8; y=y/10; i=i-1 }
31 sys_write(1,b,d); return 0
32}
33
34func main() -> i64 {
35 g_puts("nx_video_client gate (wasm core vs team authority, native)\n" as *u8)
36 var pass: i64 = 0
37 var total: i64 = 0
38
39 // ---- NV1 cross-implementation ----
40 let pcm: *u8 = sys_mmap(8192)
41 var i: i64 = 0
42 while i < 8192 { pcm[i] = ((i * 7 + 3) & 255) as u8; i = i + 1 }
43 let jpg: *u8 = sys_mmap(1000)
44 i = 0
45 while i < 1000 { jpg[i] = ((i * 13 + 5) & 255) as u8; i = i + 1 }
46
47 let buf: *u8 = sys_mmap(65536)
48 var w: i64 = vc_nv1_header(buf, 48000)
49 w = vc_nv1_chunk(buf, w, 65, 0, pcm, 8192)
50 w = vc_nv1_chunk(buf, w, 86, 10, jpg, 1000)
51 w = vc_nv1_chunk(buf, w, 65, 85, pcm, 8192)
52 w = vc_nv1_end(buf, w, 512)
53
54 let info: *i64 = sys_mmap(64) as *i64
55 let rc_auth: i64 = nv1_validate(buf, w, info)
56 var auth_ok: i64 = 0
57 if rc_auth == 0 { if info[0] == 48000 { if info[1] == 2 { if info[2] == 8192 { auth_ok = 1 } } } }
58 pass = pass + g_check("vc-packed container GREEN under nx_nv1 authority (rate/chunks/samples)" as *u8, auth_ok); total = total + 1
59
60 let rc_vc: i64 = vc_nv1_validate(buf, w, info)
61 pass = pass + g_check("vc validator agrees (cross-check both ways)" as *u8, rc_vc == 0); total = total + 1
62
63 // authority-packed container walks correctly under vc_nv1_next
64 let buf2: *u8 = sys_mmap(65536)
65 var w2: i64 = nv1_write_header(buf2, 44100)
66 w2 = nv1_write_chunk(buf2, w2, 86, 7, jpg, 1000)
67 w2 = nv1_write_chunk(buf2, w2, 65, 11, pcm, 8192)
68 w2 = nv1_write_end(buf2, w2, 99)
69 let ci: *i64 = sys_mmap(64) as *i64
70 var off: i64 = 24
71 off = vc_nv1_next(buf2, w2, off, ci)
72 var walk_ok: i64 = 1
73 if ci[0] != 86 { walk_ok = 0 }
74 if ci[1] != 1000 { walk_ok = 0 }
75 if ci[2] != 7 { walk_ok = 0 }
76 off = vc_nv1_next(buf2, w2, off, ci)
77 if ci[0] != 65 { walk_ok = 0 }
78 if ci[1] != 8192 { walk_ok = 0 }
79 let fin: i64 = vc_nv1_next(buf2, w2, off, ci)
80 if fin != 0 { walk_ok = 0 }
81 if ci[0] != 69 { walk_ok = 0 }
82 if ci[2] != 99 { walk_ok = 0 }
83 pass = pass + g_check("vc_nv1_next walks authority-packed chunks (kinds/lens/times/end)" as *u8, walk_ok); total = total + 1
84
85 // ---- wire frames ----
86 let wirebuf: *u8 = sys_mmap(16384)
87 let wn: i64 = vc_wire_pack(wirebuf, 0x56, "userwasm" as *u8, 77, jpg, 1000)
88 let wi: *i64 = sys_mmap(64) as *i64
89 let wrc: i64 = vc_wire_parse(wirebuf, wn, wi)
90 var wire_ok: i64 = 0
91 if wrc == 0 { if wi[0] == 0x56 { if wi[1] == 77 { if wi[3] == 1000 { wire_ok = 1 } } } }
92 if wire_ok == 1 {
93 var k: i64 = 0
94 while k < 1000 {
95 if wirebuf[wi[2] + k] != jpg[k] { wire_ok = 0; k = 1000 } else { k = k + 1 }
96 }
97 if wirebuf[1] != (117 as u8) { wire_ok = 0 } // 'u'
98 }
99 pass = pass + g_check("wire frame pack->parse round-trips (kind/id/seq/payload)" as *u8, wire_ok); total = total + 1
100
101 // ---- f32 -> i16 known vectors (bits -> expected) ----
102 var fok: i64 = 1
103 if vc_f32_bits_to_i16(0x3F800000) != 32767 { fok = 0 } // +1.0 clamps to max
104 if vc_f32_bits_to_i16(0xBF800000) != 0 - 32768 { fok = 0 } // -1.0 exact
105 if vc_f32_bits_to_i16(0x3F000000) != 16384 { fok = 0 } // 0.5 exact
106 if vc_f32_bits_to_i16(0xBF000000) != 0 - 16384 { fok = 0 } // -0.5 exact
107 if vc_f32_bits_to_i16(0) != 0 { fok = 0 } // +0
108 if vc_f32_bits_to_i16(0x80000000) != 0 { fok = 0 } // -0
109 if vc_f32_bits_to_i16(0x40490FDB) != 32767 { fok = 0 } // pi clamps
110 if vc_f32_bits_to_i16(0x7F800000) != 32767 { fok = 0 } // +Inf clamps
111 if vc_f32_bits_to_i16(0xFF800000) != 0 - 32768 { fok = 0 } // -Inf clamps
112 if vc_f32_bits_to_i16(0x7FC00000) != 0 { fok = 0 } // NaN -> 0
113 if vc_f32_bits_to_i16(0x00000001) != 0 { fok = 0 } // denormal -> 0
114 if vc_f32_bits_to_i16(0x3F7FFFFF) != 32767 { fok = 0 } // 1-ulp under 1.0
115 if vc_f32_bits_to_i16(0x38000000) != 1 { fok = 0 } // 2^-15 -> 1 exact
116 if vc_f32_bits_to_i16(0x38800001) != 2 { fok = 0 } // (1+2^-23)*2^-14 -> 2
117 pass = pass + g_check("f32->i16 integer-IEEE754 vectors (symmetric 32768, clamp/NaN/Inf edges)" as *u8, fok); total = total + 1
118
119 // ---- i16 -> f32 exactness on ALL 65536 values ----
120 // For each i16 v, decode the produced f32 bits back with integer math
121 // and require EXACT equality v == round_trip (exactness is total here:
122 // every v/32768 is representable in binary32).
123 var all_ok: i64 = 1
124 var v: i64 = 0 - 32768
125 while v <= 32767 {
126 let bits: i64 = vc_i16_to_f32_bits(v)
127 // decode: sign/exp/mant -> a = mant_full * 2^(e-150) * 32768
128 var back: i64 = 0
129 if bits != 0 {
130 let bs: i64 = (bits / 2147483648) & 1
131 let be: i64 = (bits / 8388608) & 0xff
132 let bm: i64 = (bits & 8388607) + 8388608
133 // value*32768 = bm * 2^(be-150+15) = bm * 2^(be-135)
134 var sh: i64 = 135 - be
135 var mag: i64 = bm
136 var lost: i64 = 0
137 while sh > 0 {
138 if (mag & 1) == 1 { lost = 1 }
139 mag = mag / 2
140 sh = sh - 1
141 }
142 if lost == 1 { all_ok = 0 }
143 back = mag
144 if bs == 1 { back = 0 - back }
145 }
146 if back != v { all_ok = 0; v = 32768 }
147 v = v + 1
148 }
149 pass = pass + g_check("i16->f32 EXACT on all 65536 values (zero loss both directions)" as *u8, all_ok); total = total + 1
150
151 // ---- buffer forms round-trip: f32(i16(x)) == x for the exact map ----
152 let i16buf: *u8 = sys_mmap(131072)
153 let f32buf: *u8 = sys_mmap(262144)
154 let i16buf2: *u8 = sys_mmap(131072)
155 var s: i64 = 0
156 while s < 65536 {
157 var sv: i64 = s - 32768
158 if sv < 0 { sv = sv + 65536 }
159 i16buf[s * 2] = (sv & 255) as u8
160 i16buf[s * 2 + 1] = ((sv / 256) & 255) as u8
161 s = s + 1
162 }
163 vc_i16_to_f32(i16buf, 65536, f32buf)
164 vc_f32_to_i16(f32buf, 65536, i16buf2)
165 // symmetric 32768 scale -> EVERY value round-trips, including -32768.
166 var rt_ok: i64 = 1
167 s = 0
168 while s < 65536 {
169 if i16buf2[s * 2] != i16buf[s * 2] { rt_ok = 0; s = 65536 }
170 else { if i16buf2[s * 2 + 1] != i16buf[s * 2 + 1] { rt_ok = 0; s = 65536 } else { s = s + 1 } }
171 }
172 pass = pass + g_check("buffer round-trip i16->f32->i16 identical (65535 values; -32768 clamps by design)" as *u8, rt_ok); total = total + 1
173
174 // ---- ladder governor ----
175 let good: *i64 = sys_mmap(16) as *i64
176 good[0] = 0
177 var lk: i64 = 1
178 if vc_ladder_step(0, 5, 500, 400, 180, good) != 1 { lk = 0 } // degrade
179 if vc_ladder_step(4, 5, 500, 400, 180, good) != 4 { lk = 0 } // floor
180 good[0] = 0
181 if vc_ladder_step(2, 5, 100, 400, 180, good) != 2 { lk = 0 } // 1 good: hold
182 if vc_ladder_step(2, 5, 100, 400, 180, good) != 2 { lk = 0 } // 2 good: hold
183 if vc_ladder_step(2, 5, 100, 400, 180, good) != 1 { lk = 0 } // 3 good: recover
184 if vc_ladder_step(0, 5, 100, 400, 180, good) != 0 { lk = 0 } // ceiling
185 if vc_ladder_step(2, 5, 300, 400, 180, good) != 2 { lk = 0 } // dead zone holds
186 pass = pass + g_check("ladder governor (degrade/3-good-recover/bounds/dead-zone)" as *u8, lk); total = total + 1
187
188 // ---- baseline-relative recovery (overseas link: RTT floor > absolute recover_ms) ----
189 // The OLD governor recovered only when rtt<recover_ms(180); an intercontinental
190 // link sits at ~220ms baseline, so it could NEVER climb back up -> pinned at the
191 // bottom rung -> the "stuck at low fps" bug. New: recover when RTT is back near
192 // its own baseline. Prove the climb happens AND the baseline tracked the floor.
193 let good2: *i64 = sys_mmap(16) as *i64
194 good2[0] = 0; good2[1] = 0
195 var bi: i64 = 0
196 while bi < 4 { vc_ladder_step(3, 5, 220, 400, 180, good2); bi = bi + 1 } // establish baseline ~220
197 good2[0] = 0 // clean 3-good window
198 var ridx: i64 = 3
199 var ri: i64 = 0
200 while ri < 3 { ridx = vc_ladder_step(ridx, 5, 230, 400, 180, good2); ri = ri + 1 } // calm-near-baseline
201 var br: i64 = 1
202 if ridx != 2 { br = 0 } // climbed 3->2 although 230 >= absolute recover_ms(180)
203 if good2[1] != 220 { br = 0 } // baseline tracked the min RTT
204 pass = pass + g_check("baseline-relative recovery: overseas RTT-floor 220>180 still climbs (nx_room_bwe)" as *u8, br); total = total + 1
205
206 // ---- no false recovery while congested (rtt well above baseline+delta) ----
207 let good3: *i64 = sys_mmap(16) as *i64
208 good3[0] = 0; good3[1] = 0
209 var ci4: i64 = 0
210 while ci4 < 4 { vc_ladder_step(3, 5, 220, 400, 180, good3); ci4 = ci4 + 1 } // baseline 220
211 good3[0] = 0
212 var cidx: i64 = 3
213 var cj: i64 = 0
214 while cj < 5 { cidx = vc_ladder_step(cidx, 5, 360, 400, 180, good3); cj = cj + 1 } // 360 >> 220+100, < degrade 400
215 var noclimb: i64 = 0
216 if cidx == 3 { noclimb = 1 } // congested (queue over baseline) must NOT climb
217 pass = pass + g_check("no false recovery under congestion (360ms >> baseline+delta holds the rung)" as *u8, noclimb); total = total + 1
218
219 // ---- LPC live-audio: core vs nx_nv1_lpc authority, BOTH directions ----
220 // speech-ish PCM (triangle + dither) like the live mic path carries
221 let lpcm: *u8 = sys_mmap(8400)
222 var seed: i64 = 4242
223 var si: i64 = 0
224 while si < 4096 {
225 let ph: i64 = si % 256
226 var tv: i64 = ph * 127 - 8128
227 if ph >= 128 { tv = 8128 - (ph - 128) * 127 }
228 seed = (seed * 1103515245 + 12345) & 0x7fffffff
229 var sv: i64 = tv + ((seed >> 8) & 127) - 64
230 if sv < 0 { sv = sv + 65536 }
231 lpcm[si * 2] = (sv & 255) as u8
232 lpcm[si * 2 + 1] = ((sv / 256) & 255) as u8
233 si = si + 1
234 }
235 let lscr: *i64 = sys_mmap(70000) as *i64
236 let lpay: *u8 = sys_mmap(8400)
237 let ldec: *u8 = sys_mmap(8400)
238 // core encodes -> AUTHORITY decodes bit-exact
239 let cel: i64 = vc_lpc_encode(lpcm, 4096, lpay, 6 + 8192 + 64, lscr)
240 var x1: i64 = 0
241 if cel > 0 {
242 if nv1l_decode(lpay, cel, ldec, 8400) == 4096 {
243 x1 = 1
244 var ci2: i64 = 0
245 while ci2 < 8192 {
246 if ldec[ci2] != lpcm[ci2] { x1 = 0; ci2 = 8192 } else { ci2 = ci2 + 1 }
247 }
248 }
249 }
250 pass = pass + g_check("LPC: core-encoded payload decodes BIT-EXACT under nx_nv1_lpc authority" as *u8, x1); total = total + 1
251 // AUTHORITY encodes -> core decodes bit-exact
252 let ael: i64 = nv1l_encode(lpcm, 4096, lpay, 6 + 8192 + 64)
253 var x2: i64 = 0
254 if ael > 0 {
255 if vc_lpc_decode(lpay, ael, ldec, 8400, lscr) == 4096 {
256 x2 = 1
257 var ci3: i64 = 0
258 while ci3 < 8192 {
259 if ldec[ci3] != lpcm[ci3] { x2 = 0; ci3 = 8192 } else { ci3 = ci3 + 1 }
260 }
261 }
262 }
263 pass = pass + g_check("LPC: authority-encoded payload decodes BIT-EXACT under the core" as *u8, x2); total = total + 1
264 // identical byte output (same cost model -> same chosen payload)
265 var x3: i64 = 0
266 if cel == ael { x3 = 1 }
267 pass = pass + g_check("LPC: core and authority choose the same payload size" as *u8, x3); total = total + 1
268 // FLAC-class on the speech-ish vector + never-expand law
269 g_puts(" RATIO live-audio payload=" as *u8); g_pn(cel)
270 g_puts("B raw=8192B permil=" as *u8); g_pn((cel * 1000) / 8192); g_puts("\n" as *u8)
271 pass = pass + g_check("LPC: speech-ish permil <= 700 (the live-audio halving)" as *u8,
272 (cel * 1000) / 8192 <= 700); total = total + 1
273 // tamper-evidence: out-of-range reconstruction refused by the core too
274 let tp: *u8 = sys_mmap(64)
275 tp[0] = 1 as u8
276 tp[1] = 0 as u8
277 vc_wr_u32(tp, 2, 2)
278 var hv: i64 = 32767
279 tp[6] = (hv & 255) as u8
280 tp[7] = ((hv / 256) & 255) as u8
281 tp[8] = 3 as u8
282 pass = pass + g_check("LPC: core refuses out-of-range reconstruction (-7)" as *u8,
283 vc_lpc_decode(tp, 9, ldec, 8400, lscr) == 0 - 7); total = total + 1
284
285 // ---- N-aware ladder floor rows ----
286 var flo: i64 = 1
287 if vc_ladder_floor(1) != 0 { flo = 0 }
288 if vc_ladder_floor(2) != 0 { flo = 0 }
289 if vc_ladder_floor(3) != 1 { flo = 0 }
290 if vc_ladder_floor(4) != 2 { flo = 0 }
291 if vc_ladder_floor(5) != 3 { flo = 0 }
292 if vc_ladder_floor(8) != 3 { flo = 0 }
293 pass = pass + g_check("ladder floor by room size (2->0 3->1 4->2 5+->3)" as *u8, flo); total = total + 1
294
295 g_puts("---- vc gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8)
296 if pass == total { return 0 }
297 return 1
298}