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}