nx_gop_present_gate.nx source

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// nx_gop_present_gate.nx -- GATE for GX1: the UEFI GOP linear-framebuffer presentation sink (nx_gop_present). 4// The x86 on-metal display path's CORE logic, proven in software against a MODELED linear framebuffer (the 5// EFI-app emission + the real-metal run are the later operator-gated rung). Hits every hazard the swapchain 6// safety envelope names: stride-vs-width, rgba-vs-rgb-channel-order, silent-stub-no-op. 7// T1 STRIDE: present a frame to an LFB whose pitch (40) EXCEEDS the width (32), BGRX; reading back with the 8// pitch reconstructs the image PIXEL-EXACT (0 mismatch). Encodes a PNG (eyeball). 9// T2 PADDING: the stride padding columns [w,pitch) are NEVER written (sentinel 0xAA preserved) -- no overrun. 10// T3 PIXEL FORMAT: the SAME frame presented RGBX vs BGRX swaps the R/B bytes exactly (channel order correct). 11// T4 HONEST-STUB + NEVER-BRICK: an unsupported pixel format returns NOT_IMPL (never a silent no-op); the 12// blit is deterministic (re-present -> byte-identical); bounded; volatile gui-axis (no firmware write). 13// T5 NEG-CONTROL: pitch < width is REFUSED (BAD_SIZE); and reading a pitch-40 LFB with the WRONG stride (32) 14// mismatches -- proving the pitch is load-bearing, not cosmetic. 15// expect_exit: 0 license_tier: ORIGINAL 16import "nx_gop_present.nx" 17import "nx_png.nx" 18import "nx_syscalls.nx" 19 20func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 21" as *u8); return ok } 22 23// a deterministic colorful test frame (the games' packed-RGB format). 24func fill_fb(fb: *i64, w: i64, h: i64) -> i64 { 25 var y: i64=0 26 while y < h { 27 var x: i64=0 28 while x < w { 29 let r: i64=(x*7)&0xFF; let g: i64=(y*9)&0xFF; let b: i64=(x^y)&0xFF 30 fb[y*w + x] = r | (g<<8) | (b<<16) 31 x=x+1 32 } 33 y=y+1 34 } 35 return 0 36} 37 38func memset_u8(p: *u8, n: i64, v: i64) -> i64 { var i: i64=0; while i<n { p[i]=v as u8; i=i+1 } return 0 } 39 40func main() -> i64 { 41 gw("=== nx_gop_present_gate: GX1 -- the UEFI GOP linear-framebuffer presentation sink (the x86 on-metal display path) ===\n" as *u8) 42 var pass: i64 = 0; var total: i64 = 0 43 let W: i64=32; let H: i64=24; let PITCH: i64=40 // pitch > width = a padded LFB (the real case) 44 let LBYTES: i64 = PITCH*H*4 45 46 let fb: *i64=sys_mmap(8*(W*H+8)) as *i64 47 fill_fb(fb, W, H) 48 let lfb1: *u8=sys_mmap(LBYTES); let recon: *i64=sys_mmap(8*(W*H+8)) as *i64 49 50 // ---- T1: STRIDE -- present (pitch 40, BGRX), reconstruct with the pitch == fb ---- 51 memset_u8(lfb1, LBYTES, 0xAA) 52 let r1: i64 = nx_gop_present(fb, W, H, lfb1, PITCH, NX_GOP_FMT_BGRX) 53 var mism: i64=0; var y: i64=0 54 while y < H { 55 var x: i64=0 56 while x < W { 57 let o: i64=(y*PITCH + x)*4 58 let bb: i64=lfb1[o] as i64; let gg: i64=lfb1[o+1] as i64; let rr: i64=lfb1[o+2] as i64 // BGRX 59 let px: i64=rr | (gg<<8) | (bb<<16) 60 recon[y*W+x]=px 61 if px != fb[y*W+x] { mism=mism+1 } 62 x=x+1 63 } 64 y=y+1 65 } 66 write_png(recon, W, H, "knowledge/nx_gop_lfb.png" as *u8) 67 var t1ok: i64=1; if r1 != W*H { t1ok=0 } if mism != 0 { t1ok=0 } 68 total=total+1; if t1ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 69 gw("T1 stride: presented " as *u8); gn(r1); gw(" px to a pitch=40 BGRX LFB, reconstruct(pitch)==fb mismatches=" as *u8); gn(mism); gw(" (PNG knowledge/nx_gop_lfb.png)\n" as *u8) 70 71 // ---- T2: PADDING untouched (stride columns [W,PITCH) stay 0xAA) ---- 72 var pad_ok: i64=1; y=0 73 while y < H { let o: i64=(y*PITCH + (W+3))*4; if (lfb1[o] as i64) != 0xAA { pad_ok=0 } y=y+1 } 74 total=total+1; if pad_ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 75 gw("T2 padding: the stride columns [W,PITCH) were never written (sentinel 0xAA preserved) -- no overrun past width\n" as *u8) 76 77 // ---- T3: PIXEL FORMAT -- RGBX vs BGRX swap R/B for a known pixel ---- 78 let lfb_rgbx: *u8=sys_mmap(LBYTES); let lfb_bgrx: *u8=sys_mmap(LBYTES) 79 memset_u8(lfb_rgbx, LBYTES, 0); memset_u8(lfb_bgrx, LBYTES, 0) 80 nx_gop_present(fb, W, H, lfb_rgbx, PITCH, NX_GOP_FMT_RGBX) 81 nx_gop_present(fb, W, H, lfb_bgrx, PITCH, NX_GOP_FMT_BGRX) 82 let px53: i64=fb[3*W + 5]; let R53: i64=px53&0xFF; let B53: i64=(px53>>16)&0xFF 83 let o53: i64=(3*PITCH + 5)*4 84 var t3ok: i64=1 85 if (lfb_rgbx[o53] as i64) != R53 { t3ok=0 } // RGBX: first byte = R 86 if (lfb_bgrx[o53] as i64) != B53 { t3ok=0 } // BGRX: first byte = B 87 if R53 == B53 { t3ok=0 } // ensure the witness pixel actually has R != B 88 total=total+1; if t3ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 89 gw("T3 format: pixel(5,3) R=" as *u8); gn(R53); gw(" B=" as *u8); gn(B53); gw(" -> RGBX first byte=" as *u8); gn(lfb_rgbx[o53] as i64); gw(", BGRX first byte=" as *u8); gn(lfb_bgrx[o53] as i64); gw(" (channel order correct)\n" as *u8) 90 91 // ---- T4: HONEST-STUB (unsupported format -> NOT_IMPL) + NEVER-BRICK (deterministic re-present) ---- 92 let lfb_b2: *u8=sys_mmap(LBYTES); memset_u8(lfb_b2, LBYTES, 0) 93 let r_uns: i64=nx_gop_present(fb, W, H, lfb_b2, PITCH, 2) // pixfmt 2 = BitMask (unsupported) 94 nx_gop_present(fb, W, H, lfb_b2, PITCH, NX_GOP_FMT_BGRX) // now a valid present 95 var ddiff: i64=0; var i: i64=0 96 while i < LBYTES { if lfb_b2[i] != lfb_bgrx[i] { ddiff=ddiff+1 } i=i+1 } 97 var t4ok: i64=1; if r_uns != NX_GOP_ERR_NOT_IMPL { t4ok=0 } if ddiff != 0 { t4ok=0 } 98 total=total+1; if t4ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 99 gw("T4 honest-stub: unsupported format returned " as *u8); gn(r_uns); gw(" (NOT_IMPL, not a silent no-op); never-brick: deterministic re-present byte-identical (diffs=" as *u8); gn(ddiff); gw("), bounded, volatile gui-axis\n" as *u8) 100 101 // ---- T5: NEG-CONTROL -- pitch<width refused; and pitch is load-bearing (wrong stride mismatches) ---- 102 let r_bad: i64=nx_gop_present(fb, W, H, lfb1, W-1, NX_GOP_FMT_BGRX) 103 var wrongmis: i64=0; y=0 104 while y < H { 105 var x: i64=0 106 while x < W { 107 let o: i64=(y*W + x)*4 // WRONG: stride=W instead of PITCH 108 let bb: i64=lfb_bgrx[o] as i64; let gg: i64=lfb_bgrx[o+1] as i64; let rr: i64=lfb_bgrx[o+2] as i64 109 if (rr | (gg<<8) | (bb<<16)) != fb[y*W+x] { wrongmis=wrongmis+1 } 110 x=x+1 111 } 112 y=y+1 113 } 114 var t5ok: i64=1; if r_bad != NX_GOP_ERR_BAD_SIZE { t5ok=0 } if wrongmis <= 0 { t5ok=0 } 115 total=total+1; if t5ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 116 gw("T5 neg-control: pitch<width returned " as *u8); gn(r_bad); gw(" (BAD_SIZE); reading the pitch-40 LFB with stride=32 mismatched " as *u8); gn(wrongmis); gw(" px (pitch is load-bearing)\n" as *u8) 117 118 gw("\n=== nx_gop_present_gate " as *u8); gn(pass); gw("/" as *u8); gn(total) 119 if pass == total { gw(" GREEN (the GOP linear-framebuffer sink: stride + pixel-format correct, honest-stub, never-brick -- the games' pixels are ready for a real x86 screen)\n" as *u8); sys_exit(0); return 0 } 120 gw(" RED\n" as *u8); sys_exit(1); return 1 121}