nx_cidx_equiv_gate.nx source

1// nx_cidx_equiv_gate.nx -- PROOF (re-runnable) that the per-box computed-decl INDEX (the eagler paint-cliff 2// fix) is a pure accelerator: for EVERY box of a real page and every paint-side resolver (bg, border, 3// color, font-size int), the bucketed answer EQUALS the full-scan answer. T2 is the can-fail control: the 4// index genuinely engages (buckets are smaller than the whole array). If the stable-bucket reorder ever 5// broke cascade order, T1 catches it on the first divergent box. license_tier: ORIGINAL expect_exit: 0 6import "nx_syscalls.nx" 7import "nx_browser_render.nx" 8 9func gq_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 10func gq_n(v: i64) -> i64 { let t: *u8=sys_mmap(24); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} 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} let b: *u8=sys_mmap(24); var j: i64=0; while j<k{b[j]=t[k-1-j];j=j+1} sys_write(1,b,k); return 0 } 11 12func main() -> i64 { 13 gq_w("=== nx_cidx_equiv_gate -- bucketed cascade lookups == full scans (paint-cliff fix is pure) ===\n" as *u8) 14 let lb: *i64 = sys_mmap(16) as *i64 15 let html: *u8 = sys_read_file("knowledge/experiential_index.html\x00" as *u8, lb) 16 if (html as i64) == 0 { gq_w("no fixture page\n" as *u8); sys_exit(2); return 2 } 17 let page: *Page = sys_mmap(NX_PAGE_BYTES) as *Page 18 page.raw = html 19 page.raw_len = lb[0] 20 page.dark_mode = 0 21 br_layout(page, 1024) // builds the index at the end 22 let t: *LayoutTree = page.tree 23 let src: *u8 = page.buf 24 let comp: *CssComputedDecl = page.computed 25 let nc: i64 = page.ncomp 26 let wout1: *i64 = sys_mmap(16) as *i64 27 let wout2: *i64 = sys_mmap(16) as *i64 28 var fails: i64 = 0 29 var i: i64 = 0 30 while i < t.count { 31 // bucketed answers (index ON, as br_layout left it) 32 br_cidx_on = 1 33 let bg1: i64 = br_comp_bg(src, comp, nc, i) 34 let bc1: i64 = br_comp_border(src, comp, nc, i, wout1) 35 let co1: i64 = br_comp_color(src, comp, nc, i, "color\x00" as *u8, 5) 36 let fs1: i64 = br_comp_int(src, comp, nc, i, "font-size\x00" as *u8, 9, 16) 37 // full-scan answers (index OFF) 38 br_cidx_on = 0 39 let bg2: i64 = br_comp_bg(src, comp, nc, i) 40 let bc2: i64 = br_comp_border(src, comp, nc, i, wout2) 41 let co2: i64 = br_comp_color(src, comp, nc, i, "color\x00" as *u8, 5) 42 let fs2: i64 = br_comp_int(src, comp, nc, i, "font-size\x00" as *u8, 9, 16) 43 if bg1 != bg2 { fails=fails+1; gq_w(" DIVERGE bg box " as *u8); gq_n(i); gq_w("\n" as *u8) } 44 if bc1 != bc2 { fails=fails+1; gq_w(" DIVERGE border box " as *u8); gq_n(i); gq_w("\n" as *u8) } 45 if wout1[0] != wout2[0] { fails=fails+1; gq_w(" DIVERGE border-w box " as *u8); gq_n(i); gq_w("\n" as *u8) } 46 if co1 != co2 { fails=fails+1; gq_w(" DIVERGE color box " as *u8); gq_n(i); gq_w("\n" as *u8) } 47 if fs1 != fs2 { fails=fails+1; gq_w(" DIVERGE font-size box " as *u8); gq_n(i); gq_w("\n" as *u8) } 48 i = i + 1 49 } 50 br_cidx_on = 1 51 gq_w(" T1 equivalence over " as *u8); gq_n(t.count) 52 gq_w(" boxes x 4 resolvers: " as *u8) 53 if fails == 0 { gq_w("PASS (0 divergences)\n" as *u8) } else { gq_w("FAIL\n" as *u8) } 54 55 // T2 CAN-FAIL: the index genuinely engages -- some box's bucket is much smaller than ncomp 56 var engaged: i64 = 0 57 if br_cidx_nbox == t.count { 58 let cc: *i64 = br_cidx_cnt as *i64 59 var mx: i64 = 0 60 var s: i64 = 0 61 var k: i64 = 0 62 while k < br_cidx_nbox { if cc[k] > mx { mx = cc[k] } s = s + cc[k]; k = k + 1 } 63 gq_w(" T2 index engaged: ncomp=" as *u8); gq_n(nc) 64 gq_w(" bucketed=" as *u8); gq_n(s) 65 gq_w(" max-bucket=" as *u8); gq_n(mx) 66 if mx < nc { if s > 0 { engaged = 1 } } 67 } 68 if engaged == 1 { gq_w(" PASS (buckets < whole array -> lookups genuinely bounded)\n" as *u8) } else { fails=fails+1; gq_w(" FAIL (index vacuous)\n" as *u8) } 69 70 if fails == 0 { gq_w("NX-CIDX-EQUIV GREEN -- the index is a pure accelerator (same answers, bounded scans)\n" as *u8); sys_exit(0); return 0 } 71 gq_w("NX-CIDX-EQUIV RED fails=" as *u8); gq_n(fails); gq_w("\n" as *u8) 72 sys_exit(1); return 1 73}