rv64im_min_gfx_gate.nx source

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// rv64im_min_gfx_gate.nx -- GATE: SF4 / the BEHAVIORAL sovereign SoC renders a real-resolution game frame. 4// SF1/SF2 proved a display controller + the FABRIC CPU drawing pixels (real gates, toy resolution -- the 5// fabric eval is slow by construction). This rung uses the FAST behavioral RV64IM-min sim (rv64im_min_sim, 6// the same CPU that boots kernels) to render a FULL 64x48 frame from a real hand-encoded RV64IM program. 7// 8// THE HONEST HARDWARE MODEL = a DRAM-BACKED FRAMEBUFFER (the common SoC architecture): the CPU stores pixels 9// into a region of DRAM (guest RAM), and the "display controller" SCANS OUT that region -> pixels. No core- 10// sim edit needed -- the framebuffer is just a convention over guest RAM, exactly as a real DRAM framebuffer 11// is. (SF1/SF2's MMIO-aperture flavor is the gate-level proof; this DRAM-backed flavor is the real-res proof.) 12// 13// The program (hand-encoded RV64IM, position-independent): AUIPC s0,1 to get the framebuffer base 14// (= PC+0x1000 = 0x80001000, avoiding LUI's sign-extension at 0x80000000), then a y/x double loop that for 15// each pixel computes a colorful procedural scene -- R = (x<<2)&255 (gradient ->), G = (y<<2)&255 (gradient 16// down), B = (x^y)&255 (the classic XOR/munching-squares texture) -- packs R|G<<8|B<<16 and SW's it to a 17// running framebuffer pointer. A trailing all-zero word halts the sim. 18// T1 the program HALTS cleanly AND the scanned-out framebuffer == an independent reference, pixel-exact 19// (0 mismatch over all 3072 pixels). Encodes a real PNG (eyeball). 20// T2 it is a REAL rendered scene (the four corners are four DISTINCT colors -- spatial variation, not a fill). 21// T3 NEVER-BRICK (#26): the sovereign sim is deterministic (re-run -> bit-identical frame), bounded, zero 22// host/persistent writes. 23// T4 LIAR-KILL: corrupt ONE instruction (the XOR -> ADD) and the rendered frame diverges -- the pixels are 24// the CPU's real computation, not pre-filled. 25// expect_exit: 0 license_tier: ORIGINAL 26import "nx_syscalls.nx" 27import "nishi_hdl_primitives.nx" 28import "rv64im_min_decoder.nx" 29import "rv64im_min_alu.nx" 30import "rv64im_min_regfile.nx" 31import "rv64im_min_csr.nx" 32import "rv64im_min_clint.nx" 33import "rv64im_min_uart.nx" 34import "rv64im_min_sim.nx" 35import "nx_png.nx" 36 37func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 38" as *u8); return ok } 39 40// ---- RV64IM instruction encoders ---- 41func e_auipc(rd: i64, imm20: i64) -> i64 { return ((imm20 & 0xFFFFF) << 12) | (rd << 7) | 0x17 } 42func e_addi(rd: i64, rs1: i64, imm: i64) -> i64 { return ((imm & 0xFFF) << 20) | (rs1 << 15) | (rd << 7) | 0x13 } 43func e_andi(rd: i64, rs1: i64, imm: i64) -> i64 { return ((imm & 0xFFF) << 20) | (rs1 << 15) | (7 << 12) | (rd << 7) | 0x13 } 44func e_slli(rd: i64, rs1: i64, sh: i64) -> i64 { return ((sh & 0x3F) << 20) | (rs1 << 15) | (1 << 12) | (rd << 7) | 0x13 } 45func e_rr(rd: i64, rs1: i64, rs2: i64, f3: i64) -> i64 { return (rs2 << 20) | (rs1 << 15) | (f3 << 12) | (rd << 7) | 0x33 } 46func e_sw(rs1: i64, rs2: i64, imm: i64) -> i64 { return (((imm>>5)&0x7F)<<25) | (rs2<<20) | (rs1<<15) | (2<<12) | ((imm&0x1F)<<7) | 0x23 } 47func e_blt(rs1: i64, rs2: i64, off: i64) -> i64 { 48 let i12: i64=(off>>12)&1; let i11: i64=(off>>11)&1; let i10_5: i64=(off>>5)&0x3F; let i4_1: i64=(off>>1)&0xF 49 return (i12<<31) | (i10_5<<25) | (rs2<<20) | (rs1<<15) | (4<<12) | (i4_1<<8) | (i11<<7) | 0x63 50} 51 52func w32(mem: *u8, off: i64, v: i64) -> i64 { 53 mem[off]=(v&0xff) as u8; mem[off+1]=((v>>8)&0xff) as u8; mem[off+2]=((v>>16)&0xff) as u8; mem[off+3]=((v>>24)&0xff) as u8 54 return 0 55} 56 57// build the renderer program into prog[]; returns instruction count. (W=64,H=48 wired into the immediates.) 58func build_prog(prog: *i64) -> i64 { 59 // regs: zero=0 t0=5 t1=6 s0=8 s1=9 a0=10 a1=11 t3=28 t4=29 t5=30 60 prog[0]=e_auipc(8, 1) // s0 = PC + 0x1000 = 0x80001000 (framebuffer base) 61 prog[1]=e_addi(10, 0, 64) // a0 = W 62 prog[2]=e_addi(11, 0, 48) // a1 = H 63 prog[3]=e_addi(9, 8, 0) // s1 = p = FB base 64 prog[4]=e_addi(5, 0, 0) // t0 = y = 0 65 prog[5]=e_addi(6, 0, 0) // t1 = x = 0 <- loop_y target (instr 5) 66 prog[6]=e_slli(28, 6, 2) // t3 = x<<2 <- loop_x target (instr 6) 67 prog[7]=e_andi(28, 28, 255) // t3 = R 68 prog[8]=e_slli(29, 5, 2) // t4 = y<<2 69 prog[9]=e_andi(29, 29, 255) // t4 = G 70 prog[10]=e_slli(29, 29, 8) // t4 = G<<8 71 prog[11]=e_rr(30, 6, 5, 4) // t5 = x ^ y (XOR, f3=4) 72 prog[12]=e_andi(30, 30, 255) // t5 = B 73 prog[13]=e_slli(30, 30, 16) // t5 = B<<16 74 prog[14]=e_rr(28, 28, 29, 6) // t3 = t3 | t4 (OR, f3=6) 75 prog[15]=e_rr(28, 28, 30, 6) // t3 = t3 | t5 = pixel 76 prog[16]=e_sw(9, 28, 0) // sw t3, 0(s1) *p = pixel 77 prog[17]=e_addi(9, 9, 4) // s1 = p + 4 78 prog[18]=e_addi(6, 6, 1) // x++ 79 prog[19]=e_blt(6, 10, 0-52) // blt x<W -> loop_x (instr6): (6-19)*4 = -52 80 prog[20]=e_addi(5, 5, 1) // y++ 81 prog[21]=e_blt(5, 11, 0-64) // blt y<H -> loop_y (instr5): (5-21)*4 = -64 82 prog[22]=0 // halt sentinel 83 return 23 84} 85 86// run a program on a FRESH behavioral sim; scan the DRAM framebuffer (guest offset 0x1000) into fb_out[W*H]. 87// returns sim.halted (1 = clean halt). 88func run_frame(prog: *i64, nprog: i64, fb_out: *i64, W: i64, H: i64) -> i64 { 89 let MEM_BASE: i64 = 0x80000000; let MEM_SIZE: i64 = 0x8000; let FBOFF: i64 = 0x1000 90 let rf_s: *i64=(sys_mmap(8*NX_RV64IM_RF_N_REGS)) as *i64; let csr_s: *i64=(sys_mmap(8*NX_CSR_SLOT_N)) as *i64 91 let clint_s: *i64=(sys_mmap(8*NX_CLINT_SLOT_N)) as *i64; let uart_s: *i64=(sys_mmap(8*NX_UART_SLOT_N)) as *i64 92 let mem: *u8=sys_mmap(MEM_SIZE); let tx: *u8=sys_mmap(256) 93 let rf: *NxRv64imRegfile=(sys_mmap(64)) as *NxRv64imRegfile; let csr: *NxRv64imCsrFile=(sys_mmap(64)) as *NxRv64imCsrFile 94 let clint: *NxClint=(sys_mmap(64)) as *NxClint; let uart: *NxUart=(sys_mmap(64)) as *NxUart; let sim: *NxRv64imSim=(sys_mmap(128)) as *NxRv64imSim 95 nx_rv64im_rf_init(rf, rf_s); nx_rv64im_csr_init(csr, csr_s, 0); nx_clint_init(clint, clint_s); nx_uart_init(uart, uart_s, tx, 256) 96 nx_rv64im_sim_init(sim, rf, csr, clint, uart, MEM_BASE, mem, MEM_SIZE, 0) 97 var i: i64=0; while i < nprog { w32(mem, i*4, prog[i]); i=i+1 } 98 nx_rv64im_sim_run(sim, 200000) 99 // scanout: read each 4-byte pixel from DRAM at FBOFF -> packed R|G<<8|B<<16 100 var idx: i64=0 101 while idx < W*H { 102 let o: i64 = FBOFF + idx*4 103 fb_out[idx] = (mem[o] as i64) | ((mem[o+1] as i64)<<8) | ((mem[o+2] as i64)<<16) 104 idx=idx+1 105 } 106 return sim.halted 107} 108 109func main() -> i64 { 110 gw("=== rv64im_min_gfx_gate: SF4 -- the behavioral RV64IM SoC renders a real-resolution frame (DRAM framebuffer) ===\n" as *u8) 111 var pass: i64 = 0; var total: i64 = 0 112 let W: i64=64; let H: i64=48 113 let prog: *i64=sys_mmap(8*64) as *i64 114 let np: i64=build_prog(prog) 115 let fb1: *i64=sys_mmap(8*(W*H+8)) as *i64 116 117 let halted: i64 = run_frame(prog, np, fb1, W, H) 118 119 // ---- T1: halted cleanly + scanout == independent reference, pixel-exact ---- 120 var mism: i64=0; var idx: i64=0 121 while idx < W*H { 122 let x: i64 = idx % W; let y: i64 = idx / W 123 let r: i64 = (x<<2)&255; let g: i64 = (y<<2)&255; let b: i64 = (x^y)&255 124 let ref: i64 = r | (g<<8) | (b<<16) 125 if fb1[idx] != ref { mism=mism+1 } 126 idx=idx+1 127 } 128 write_png(fb1, W, H, "knowledge/rv64im_gfx.png" as *u8) 129 var t1ok: i64=1; if halted != 1 { t1ok=0 } if mism != 0 { t1ok=0 } 130 total=total+1; if t1ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 131 gw("T1 program halted=" as *u8); gn(halted); gw(", scanned-out framebuffer == reference over " as *u8); gn(W*H); gw(" pixels, mismatches=" as *u8); gn(mism); gw(" (PNG knowledge/rv64im_gfx.png)\n" as *u8) 132 133 // ---- T2: a REAL rendered scene -- the four corners are four DISTINCT colors ---- 134 let c00: i64=fb1[0]; let c10: i64=fb1[W-1]; let c01: i64=fb1[(H-1)*W]; let c11: i64=fb1[(H-1)*W + (W-1)] 135 var t2ok: i64=1 136 if c00==c10 { t2ok=0 } if c00==c01 { t2ok=0 } if c00==c11 { t2ok=0 } if c10==c01 { t2ok=0 } if c10==c11 { t2ok=0 } if c01==c11 { t2ok=0 } 137 total=total+1; if t2ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 138 gw("T2 real scene: 4 corners are 4 distinct colors (" as *u8); gn(c00); gw("," as *u8); gn(c10); gw("," as *u8); gn(c01); gw("," as *u8); gn(c11); gw(") -- spatial variation, not a fill\n" as *u8) 139 140 // ---- T3: never-brick -- deterministic (re-run -> bit-identical) ---- 141 let fb2: *i64=sys_mmap(8*(W*H+8)) as *i64 142 run_frame(prog, np, fb2, W, H) 143 var dmis: i64=0; idx=0; while idx < W*H { if fb1[idx] != fb2[idx] { dmis=dmis+1 } idx=idx+1 } 144 total=total+1; if dmis==0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 145 gw("T3 never-brick (#26): the sovereign sim is deterministic (re-run bit-identical, diffs=" as *u8); gn(dmis); gw("), bounded, zero host/persistent writes\n" as *u8) 146 147 // ---- T4: liar-kill -- corrupt the XOR (instr 11) into an ADD -> the frame must diverge ---- 148 let saved: i64=prog[11] 149 prog[11]=e_rr(30, 6, 5, 0) // f3=0 -> ADD instead of XOR (blue = (x+y) not (x^y)) 150 let fb3: *i64=sys_mmap(8*(W*H+8)) as *i64 151 run_frame(prog, np, fb3, W, H) 152 prog[11]=saved 153 var bdiff: i64=0; idx=0; while idx < W*H { if fb3[idx] != fb1[idx] { bdiff=bdiff+1 } idx=idx+1 } 154 total=total+1; if bdiff > 0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 155 gw("T4 liar-kill: corrupting the XOR->ADD changed " as *u8); gn(bdiff); gw(" pixels -- the frame is the CPU's real computation, not pre-filled\n" as *u8) 156 157 gw("\n=== rv64im_min_gfx_gate " as *u8); gn(pass); gw("/" as *u8); gn(total) 158 if pass == total { gw(" verdict=GREEN (a real hand-encoded RV64IM program renders a full real-resolution frame on the behavioral sovereign CPU into a DRAM framebuffer -> scanout)\n" as *u8); sys_exit(0); return 0 } 159 gw(" verdict=RED\n" as *u8); sys_exit(1); return 1 160}