code wiki / _hdl_build / nx_video_embed_export_gate.nx

nx_video_embed_export_gate.nx source

↩ module page · 152 lines · 7433 B

1import "nx_gate_base.nx" 2// nx_video_embed_export_gate.nx -- proves the shipped embed bundle (web_assets/nishi-video.js) is 3// INTERNALLY EXPORT-CONSISTENT: every wasm export the JS component calls (NX.<name>) is REALLY exported 4// by the wasm carried in the SAME bundle. It decodes the embedded base64 core, parses its WASM export 5// section (section id 7), and checks every NX.<ident> the component references against the export set. 6// Catches the #1 silent browser break the marker-check + byte-identical gate CANNOT: a typo'd / renamed / 7// missing export ("NX.vc_x is not a function") that serves 200, passes every funcheck, then throws at 8// runtime in every browser. This is the "serves != works" honesty rung for the native <nishi-video> embed. 9// expect_exit: 0 license_tier: ORIGINAL 10import "nx_syscalls.nx" 11import "nx_base64.nx" 12import "nx_gate_verdict.nx" 13 14func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 15" as *u8); return ok } 16func gn(v: i64) -> i64 { 17 let b: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} 18 let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} 19 var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 } 20func wr_bytes(p: *u8, off: i64, n: i64) -> i64 { sys_write(1, ((p as i64)+off) as *u8, n); return 0 } 21 22// find NUL-terminated needle in hay[0..n); returns offset AFTER the needle, or -1 23func find_after(hay: *u8, n: i64, needle: *u8) -> i64 { 24 var nl: i64=0; while needle[nl]!=(0 as u8){nl=nl+1} 25 var i: i64=0 26 while i+nl<=n { var j: i64=0; var ok: i64=1; while j<nl { if hay[i+j]!=needle[j]{ok=0;j=nl} else {j=j+1} } if ok==1{return i+nl} i=i+1 } 27 return 0 - 1 } 28 29func isident(c: i64) -> i64 { 30 if c>=48 { if c<=57 { return 1 } } 31 if c>=65 { if c<=90 { return 1 } } 32 if c>=97 { if c<=122 { return 1 } } 33 if c==95 { return 1 } 34 return 0 } 35 36func buf_eq(a: *u8, ao: i64, al: i64, b: *u8, bo: i64, bl: i64) -> i64 { 37 if al != bl { return 0 } 38 var i: i64 = 0 39 while i < al { if (a[ao+i] as i64) != (b[bo+i] as i64) { return 0 } i = i + 1 } 40 return 1 } 41 42// LEB128 unsigned decode from buf at cur[0]; advances cur[0] past the value (no <</| in nx -> use *128) 43func uleb(buf: *u8, cur: *i64) -> i64 { 44 var result: i64 = 0 45 var powv: i64 = 1 46 var go: i64 = 1 47 while go==1 { 48 let bb: i64 = buf[cur[0]] as i64 49 cur[0] = cur[0] + 1 50 result = result + ((bb & 0x7f) * powv) 51 if (bb & 0x80) == 0 { go = 0 } else { powv = powv * 128 } 52 } 53 return result } 54 55func main() -> i64 { 56 gw("=== nx_video_embed_export_gate: shipped bundle JS<->wasm export consistency ===\n" as *u8) 57 let jbox: *i64 = sys_mmap(16) as *i64; jbox[0]=0 58 let js: *u8 = sys_read_file("web_assets/nishi-video.js" as *u8, jbox) 59 if (js as i64)==0 { gw("no nishi-video.js (run nx_video_embed_bundle)\n" as *u8); return 1 } 60 let jn: i64 = jbox[0] 61 // decode the embedded wasm core from the SAME bundle we ship 62 let start: i64 = find_after(js, jn, "WASM_B64=\"" as *u8) 63 if start < 0 { gw("no WASM_B64 in bundle -> RED\n" as *u8); return 1 } 64 var end: i64 = start 65 var goe: i64 = 1 66 while goe==1 { if end<jn { if (js[end] as i64)==34 { goe=0 } else { end=end+1 } } else { goe=0 } } 67 let blen: i64 = end - start 68 let wasm: *u8 = sys_mmap(blen + 64) 69 let wlen: i64 = b64_decode(((js as i64)+start) as *u8, blen, wasm) 70 gw(" embedded wasm decoded = " as *u8); gn(wlen); gw("B\n" as *u8) 71 // wasm magic: 00 61 73 6d ("\0asm") 72 if (wasm[0] as i64)!=0 { gw("bad wasm magic -> RED\n" as *u8); return 1 } 73 if (wasm[1] as i64)!=97 { gw("bad wasm magic -> RED\n" as *u8); return 1 } 74 if (wasm[2] as i64)!=115 { gw("bad wasm magic -> RED\n" as *u8); return 1 } 75 if (wasm[3] as i64)!=109 { gw("bad wasm magic -> RED\n" as *u8); return 1 } 76 // walk sections to the export section (id 7) 77 let cbox: *i64 = sys_mmap(16) as *i64 78 var cur: i64 = 8 79 var exp_start: i64 = 0 - 1 80 var gs: i64 = 1 81 while gs==1 { 82 if cur < wlen { 83 let sid: i64 = wasm[cur] as i64 84 cur = cur + 1 85 cbox[0] = cur 86 let ssize: i64 = uleb(wasm, cbox) 87 cur = cbox[0] 88 if sid == 7 { exp_start = cur } 89 cur = cur + ssize 90 } else { gs = 0 } 91 } 92 if exp_start < 0 { gw("no export section -> RED\n" as *u8); return 1 } 93 // parse export names: count, then count x [name_len][name][kind:1][index] 94 cbox[0] = exp_start 95 let ecount: i64 = uleb(wasm, cbox) 96 let eoff: *i64 = sys_mmap((ecount + 8) * 8) as *i64 97 let elen: *i64 = sys_mmap((ecount + 8) * 8) as *i64 98 var e: i64 = 0 99 while e < ecount { 100 let nlen: i64 = uleb(wasm, cbox) 101 eoff[e] = cbox[0] 102 elen[e] = nlen 103 cbox[0] = cbox[0] + nlen 104 cbox[0] = cbox[0] + 1 // export kind byte 105 uleb(wasm, cbox) // export index (advance past, unused) 106 e = e + 1 107 } 108 gw(" wasm exports = " as *u8); gn(ecount); gw("\n" as *u8) 109 // scan the bundle for NX.<ident> (base64 blob has no '.', so scanning the whole file is safe) 110 let soff: *i64 = sys_mmap(256 * 8) as *i64 111 let slen: *i64 = sys_mmap(256 * 8) as *i64 112 var scount: i64 = 0 113 var green: i64 = 1 114 var i: i64 = 0 115 while i + 3 <= jn { 116 var k: i64 = i + 1 117 var matched: i64 = 0 118 if (js[i] as i64)==78 { if (js[i+1] as i64)==88 { if (js[i+2] as i64)==46 { matched=1 } } } 119 if matched==1 { 120 k = i + 3 121 var g: i64 = 1 122 while g==1 { if k<jn { if isident(js[k] as i64)==1 { k=k+1 } else { g=0 } } else { g=0 } } 123 let idoff: i64 = i + 3 124 let idlen: i64 = k - idoff 125 if idlen > 0 { 126 var seen: i64 = 0 127 var s: i64 = 0 128 while s < scount { if buf_eq(js, soff[s], slen[s], js, idoff, idlen)==1 { seen=1; s=scount } else { s=s+1 } } 129 if seen==0 { 130 if scount < 256 { soff[scount]=idoff; slen[scount]=idlen; scount=scount+1 } 131 var found: i64 = 0 132 var m: i64 = 0 133 while m < ecount { if buf_eq(js, idoff, idlen, wasm, eoff[m], elen[m])==1 { found=1; m=ecount } else { m=m+1 } } 134 gw(" NX." as *u8); wr_bytes(js, idoff, idlen) 135 if found==1 { gw(" -> exported OK\n" as *u8) } else { gw(" -> !!! NOT EXPORTED (browser will throw) !!!\n" as *u8); green=0 } 136 } 137 } 138 } 139 i = k 140 } 141 gw(" distinct NX.<export> calls checked = " as *u8); gn(scount); gw("\n" as *u8) 142 if scount==0 { gw("EMBED-EXPORT-GATE verdict=RED -- no NX.<export> calls found (scan/regression bug)\n" as *u8); return 1 } 143 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 144 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 145 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 146 let ctr__dry: *i64 = gv_ctr() 147 ctr__dry[0] = green 148 ctr__dry[1] = 1 149 let rc__dry: i64 = gv_verdict("VIDEO-EMBED-EXPORT-GATE" as *u8, ctr__dry, "every export the shipped component calls is really exported by the bundled wasm" as *u8) 150 sys_exit(rc__dry) 151 return rc__dry 152}