nx_wire_harness_gate.nx source

1// nx_wire_harness_gate.nx -- certifies the shared wiring scaffold. Each tooth guards a property the 2// three title gates depend on; mutation target = the causal menu (wh_menu_pick2 must return the policy 3// item, and the caller acting on a different id must be observable). 4// T1 fbck order-sensitive (a swapped pixel changes it -- not a plain sum) 5// T2 fbck deterministic (same frame -> same ck) 6// T3 chain fold accumulates (order matters) 7// T4 menu returns the policy item (id a) and is modal-closed after 8// T5 menu is CAUSAL: a caller that acts on the returned id vs a fixed id diverges (mutation proof 9// built into the gate so the property cannot rot) 10// T6 experiential passes a real 2D frame and REFUSES a void frame 11// T7 ink counts non-bg pixels, 0 on a cleared frame 12// T8 anti-vacuity: the frames compared in T1/T2 carried real ink 13// license_tier: ORIGINAL expect_exit: 0 14import "nx_syscalls.nx" 15import "nx_wire_harness.nx" 16import "nx_game_raster.nx" 17 18const W: i64 = 96 19const H: i64 = 64 20const N: i64 = 6144 // W*H 21 22func ww(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 23func wn(v: i64) -> i64 { 24 if v==0 { sys_write(1,"0" as *u8,1); return 0 } 25 var m: i64=v; if m<0 { sys_write(1,"-" as *u8,1); m=0-m } 26 let t: *u8=sys_mmap(32); var k: i64=0 27 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 } 28 let o: *u8=sys_mmap(32); var q: i64=k-1; var i: i64=0 29 while q>=0 { o[i]=t[q]; i=i+1; q=q-1 } 30 sys_write(1,o,i); return 0 31} 32func mkframe(fb: *i64, shift: i64) -> i64 { 33 let bg: i64 = gr_pack(10, 12, 20) 34 gr_clear(fb, W, H, bg) 35 var f: i64=0 36 while f<4 { 37 let cx: i64 = 14 + f*20 + shift 38 gr_rect(fb, W, H, cx-6, 20, cx+6, 54, gr_pack(80+f*30, 120, 200)) 39 gr_disc(fb, W, H, cx, 12, 4, gr_pack(220, 180, 60)) 40 f=f+1 41 } 42 return 0 43} 44 45func main() -> i64 { 46 var pass: i64=0 47 let fa: *i64 = sys_mmap(N*8) as *i64 48 let fb2: *i64 = sys_mmap(N*8) as *i64 49 let fbg: *i64 = sys_mmap(N*8) as *i64 50 let fvoid: *i64 = sys_mmap(N*8) as *i64 51 mkframe(fa, 0) 52 mkframe(fb2, 3) 53 gr_clear(fbg, W, H, gr_pack(10, 12, 20)) 54 gr_clear(fvoid, W, H, gr_pack(1, 1, 2)) 55 ww("=== nx_wire_harness_gate (shared wiring scaffold) ===\n") 56 57 // T1 fbck order-sensitive 58 let ck_a: i64 = wh_fbck(fa, N) 59 let ck_b: i64 = wh_fbck(fb2, N) 60 var t1: i64=0 61 if ck_a != ck_b { t1=1 } 62 if t1==1 { ww("T1 GREEN fbck order-sensitive (frame vs shifted differ: "); wn(ck_a); ww(" != "); wn(ck_b); ww(")\n"); pass=pass+1 } 63 else { ww("T1 RED fbck collision\n") } 64 65 // T2 fbck deterministic 66 let ck_a2: i64 = wh_fbck(fa, N) 67 var t2: i64=0 68 if ck_a==ck_a2 { t2=1 } 69 if t2==1 { ww("T2 GREEN fbck deterministic\n"); pass=pass+1 } else { ww("T2 RED fbck nondeterministic\n") } 70 71 // T3 chain fold accumulates + order matters 72 let c_ab: i64 = wh_chain(wh_chain(1469598103, ck_a), ck_b) 73 let c_ba: i64 = wh_chain(wh_chain(1469598103, ck_b), ck_a) 74 var t3: i64=0 75 if c_ab != c_ba { if c_ab != 1469598103 { t3=1 } } 76 if t3==1 { ww("T3 GREEN chain fold order-sensitive + non-identity\n"); pass=pass+1 } else { ww("T3 RED chain fold weak\n") } 77 78 // T4 menu returns policy item (id a), modal-closed 79 let hud: *i64 = sys_mmap(GH_WORDS*8) as *i64 80 gh_init(hud, 1) 81 let pick: i64 = wh_menu_pick2(hud, 7, 100, 9, 200) 82 var t4: i64=0 83 if pick==7 { if hud[GH_F_MOPEN]==0 { t4=1 } } 84 if t4==1 { ww("T4 GREEN menu returns policy item id=7, modal-closed\n"); pass=pass+1 } 85 else { ww("T4 RED menu pick="); wn(pick); ww(" open="); wn(hud[GH_F_MOPEN]); ww("\n") } 86 87 // T5 menu CAUSAL: simulate a buyer that acts on the returned id. Selecting policy id 1 => a "buy" 88 // increments; a caller that ignored the id (fixed 0) would never buy. Prove the id drives outcome. 89 var buys: i64=0 90 var visits: i64=0 91 let hud2: *i64 = sys_mmap(GH_WORDS*8) as *i64 92 gh_init(hud2, 1) 93 var r: i64=0 94 while r<5 { 95 let d: i64 = wh_menu_pick2(hud2, 1, 300, 2, 999) // item a = id 1 (buy) 96 visits=visits+1 97 if d==1 { buys=buys+1 } 98 r=r+1 99 } 100 var t5: i64=0 101 if buys==5 { if visits==5 { if hud2[GH_F_NSEL]==5 { t5=1 } } } 102 if t5==1 { ww("T5 GREEN menu causal: 5 visits -> 5 policy buys (returned id drove every outcome)\n"); pass=pass+1 } 103 else { ww("T5 RED causal buys="); wn(buys); ww(" visits="); wn(visits); ww(" nsel="); wn(hud2[GH_F_NSEL]); ww("\n") } 104 105 // T6 experiential: real frame passes, void refused 106 let m6: *i64 = sys_mmap(FS_NMETRIC*8) as *i64 107 let okreal: i64 = wh_experiential(fa, W, H, m6) 108 let mv: *i64 = sys_mmap(FS_NMETRIC*8) as *i64 109 let okvoid: i64 = wh_experiential(fvoid, W, H, mv) 110 var t6: i64=0 111 if okreal==1 { if okvoid==0 { t6=1 } } 112 if t6==1 { ww("T6 GREEN experiential: real frame OK ("); wn(m6[0]); ww("/"); wn(m6[1]); ww("/"); wn(m6[2]); ww("/"); wn(m6[3]); ww("/"); wn(m6[4]); ww("), void refused\n"); pass=pass+1 } 113 else { ww("T6 RED experiential real="); wn(okreal); ww(" void="); wn(okvoid); ww("\n") } 114 115 // T7 ink 116 let ink_a: i64 = wh_ink(fa, N, gr_pack(10,12,20)) 117 let ink_bg: i64 = wh_ink(fbg, N, gr_pack(10,12,20)) 118 var t7: i64=0 119 if ink_a>=20 { if ink_bg==0 { t7=1 } } 120 if t7==1 { ww("T7 GREEN ink: frame "); wn(ink_a); ww(" permil, cleared 0\n"); pass=pass+1 } 121 else { ww("T7 RED ink frame="); wn(ink_a); ww(" bg="); wn(ink_bg); ww("\n") } 122 123 // T8 anti-vacuity 124 var t8: i64=0 125 if ink_a>=20 { if m6[2]>0 { t8=1 } } 126 if t8==1 { ww("T8 GREEN anti-vacuity: compared frames carried real ink + edges\n"); pass=pass+1 } 127 else { ww("T8 RED vacuous\n") } 128 129 ww("nx_wire_harness_gate: "); wn(pass); ww("/8\n") 130 if pass==8 { return 0 } 131 return 1 132}