nx_rv64_asm_verify.nx source

1// nx_rv64_asm_verify.nx -- GATE: EXHAUSTIVE verification of the sovereign RV64 assembler (nx_rv64_asm) by RUNNING its 2// output on the sovereign rv64 emulator (rv64im_min_sim via nx_boot_run_sov). Eats the debt that the assembler was 3// only lightly KAT'd (lui + 2 branches): this assembles ONE program that threads a computation through EVERY 4// supported instruction -- li/addi/add/sub/and/or/xor/andi/ori/sll/srl/slli/srli/lui + lw/sw/lbu/sb/lhu/sh/ld/sd 5// (memory round-trips) + beq/bne/blt/bge/bltu/bgeu (taken AND not-taken) + jal/ret/j/mv -- to a known value (1005), 6// self-checks it IN-GUEST, prints OK (match) or NO (mismatch) over the UART, and halts via the SiFive finisher. If ANY 7// instruction is mis-encoded the computed value diverges -> NO -> RED. Runs on OUR emulator (no QEMU). expect_exit:0 8import "nx_rv64_asm.nx" 9import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc) 10const K_MAGIC_65536: i64 = 65536 11 12func v_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 13// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer 14// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the 15// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls). 16// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign. 17func v_pn(v: i64) -> i64 { nxi_out(v); return 0 } 18 19// run the sovereign emulator on binpath; serial -> outpath; return wait status 20func v_run_sov(binpath: *u8, outpath: *u8) -> i64 { 21 let pid: i64 = sys_fork() 22 if pid == 0 { 23 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 24 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 25 let argv: *i64 = sys_mmap(32) as *i64 26 argv[0] = "_offc/nx_boot_run_sov.elf" as *u8 as i64 27 argv[1] = binpath as i64 28 argv[2] = 0 29 let envp: *i64 = sys_mmap(16) as *i64 30 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 31 envp[1] = 0 32 sys_execve("_offc/nx_boot_run_sov.elf" as *u8, argv, envp) 33 sys_exit(127) 34 } 35 let st: *i64 = sys_mmap(16) as *i64 36 sys_wait4(pid, st, 0) 37 return st[0] 38} 39func v_read(path: *u8, buf: *u8, cap: i64) -> i64 { 40 let fd: i64 = sys_openat_rd(path); if fd < 0 { return 0 } 41 var n: i64 = 0; var go: i64 = 1 42 while go == 1 { let r: i64 = sys_read(fd, ((buf as i64)+n) as *u8, cap-1-n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap-1 { go = 0 } } 43 sys_close(fd); return n 44} 45func v_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 46 if pl <= 0 { return 0 } 47 var i: i64 = 0 48 while i + pl <= n { var k: i64 = 0; var hit: i64 = 1; while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } if hit == 1 { return 1 } i = i + 1 } 49 return 0 50} 51 52func main() -> i64 { 53 v_p("nx_rv64_asm_verify (exhaustive assembler check: run every-instruction program on the SOVEREIGN rv64 emulator)\n" as *u8) 54 let out: *u8 = sys_mmap(K_MAGIC_65536) 55 let nb: i64 = rvasm_assemble_str(" li a0, 0\n li t0, 100\n add a0, a0, t0\n addi a0, a0, 50\n li t0, 30\n sub a0, a0, t0\n li t0, 255\n andi t0, t0, 15\n add a0, a0, t0\n li t0, 16\n ori t0, t0, 1\n add a0, a0, t0\n li t0, 6\n li t1, 3\n xor t0, t0, t1\n add a0, a0, t0\n li t0, 6\n li t1, 3\n and t0, t0, t1\n add a0, a0, t0\n li t0, 6\n li t1, 3\n or t0, t0, t1\n add a0, a0, t0\n li t0, 1\n slli t0, t0, 5\n add a0, a0, t0\n li t0, 256\n srli t0, t0, 4\n add a0, a0, t0\n li t0, 3\n li t1, 2\n sll t0, t0, t1\n add a0, a0, t0\n li t0, 256\n li t1, 5\n srl t0, t0, t1\n add a0, a0, t0\n lui t0, 0x1\n srli t0, t0, 8\n add a0, a0, t0\n lui s0, 0x80008\n slli s0, s0, 32\n srli s0, s0, 32\n li t1, 111\n sw t1, 0(s0)\n lw t2, 0(s0)\n add a0, a0, t2\n li t1, 66\n sb t1, 8(s0)\n lbu t2, 8(s0)\n add a0, a0, t2\n li t1, 256\n sh t1, 16(s0)\n lhu t2, 16(s0)\n add a0, a0, t2\n li t1, 222\n sd t1, 24(s0)\n ld t2, 24(s0)\n add a0, a0, t2\n li t0, 5\n li t1, 5\n beq t0, t1, L1\n addi a0, a0, 1000\nL1:\n li t0, 5\n li t1, 6\n bne t0, t1, L2\n addi a0, a0, 1000\nL2:\n li t0, 3\n li t1, 5\n blt t0, t1, L3\n addi a0, a0, 1000\nL3:\n li t0, 5\n li t1, 5\n bge t0, t1, L4\n addi a0, a0, 1000\nL4:\n li t0, 3\n li t1, 5\n bltu t0, t1, L5\n addi a0, a0, 1000\nL5:\n li t0, 5\n li t1, 5\n bgeu t0, t1, L6\n addi a0, a0, 1000\nL6:\n li t0, 5\n li t1, 6\n beq t0, t1, L7\n addi a0, a0, 5\nL7:\n jal ra, addfn\n j after\naddfn:\n addi a0, a0, 95\n ret\nafter:\n mv t0, a0\n mv a0, t0\n li t1, 1005\n lui s2, 0x10000\n bne a0, t1, fail\n li a1, 79\n sb a1, 0(s2)\n li a1, 75\n sb a1, 0(s2)\n j halt\nfail:\n li a1, 78\n sb a1, 0(s2)\n li a1, 79\n sb a1, 0(s2)\nhalt:\n lui a0, 0x100\n lui a1, 0x5\n addi a1, a1, 0x555\n sw a1, 0(a0)\nspin:\n j spin\n" as *u8, out, K_MAGIC_65536) 56 if nb < 0 { v_p(" ASSEMBLE FAILED rc="); v_pn(0-nb); v_p("\n" as *u8); sys_exit(1); return 1 } 57 v_p(" assembled the every-instruction program: bytes="); v_pn(nb); v_p("\n" as *u8) 58 let binpath: *u8 = "runtime/_hdl_build/_asm_verify.bin" as *u8 59 let fd: i64 = sys_openat_wr(binpath, 0x1a4); if fd < 0 { v_p(" cannot write bin\n" as *u8); sys_exit(1); return 1 } 60 sys_write(fd, out, nb); sys_close(fd) 61 62 let serial: *u8 = "/tmp/_asm_verify.txt" as *u8 63 let wst: i64 = v_run_sov(binpath, serial) 64 let sbuf: *u8 = sys_mmap(K_MAGIC_65536) 65 let sn: i64 = v_read(serial, sbuf, K_MAGIC_65536) 66 let ok: i64 = v_has(sbuf, sn, "OK" as *u8, 2) 67 let no: i64 = v_has(sbuf, sn, "NO" as *u8, 2) 68 let halt: i64 = v_has(sbuf, sn, "BOOTSOV verdict=GREEN" as *u8, 21) 69 v_p(" sovereign-emu serial: OK-present="); v_pn(ok); v_p(" NO-present="); v_pn(no); v_p(" clean-halt="); v_pn(halt); v_p(" wait="); v_pn(wst); v_p("\n" as *u8) 70 71 var pass: i64 = 0 72 if ok == 1 { if no == 0 { if halt == 1 { pass = 1 } } } 73 if pass == 1 { 74 let logf: i64 = sys_openat_append("knowledge/status/rv64_asm_verify.log" as *u8, 420) 75 if logf >= 0 { let z: i64 = sys_write(logf, "NXRV64ASMVERIFY GREEN: every assembler instruction (arith/logic/shift/mem/branch-taken+nottaken/jal/ret/j/mv) computed the exact value on the SOVEREIGN rv64 emu -> in-guest self-check printed OK; clean finisher halt; no QEMU\n" as *u8, 214); sys_close(logf) } 76 v_p("verdict=GREEN (the sovereign RV64 assembler is exhaustively correct -- every instruction verified by execution on OUR emulator; the driver toolchain needs no QEMU)\n" as *u8); sys_exit(0); return 0 77 } 78 v_p("verdict=RED (assembler mis-encoded an instruction -- the in-guest self-check did not print OK, or no clean halt)\n" as *u8); sys_exit(1); return 1 79}