rv64im_min_cpu_crosscheck.nx source

1// nx_rv64im_cpu_crosscheck.nx -- 1:1 proof: our sovereign RV64IM CPU sim 2// vs qemu-system-riscv64 (canonical reference) on the SAME ELF. 3// 4// Loads cpu_crosscheck_prog.elf (sum of squares 1..20 = 2870, printed via 5// UART, exercising MUL/DIVU/REMU/branches/loads) into the sim, runs it, 6// and emits the captured UART byte stream to stdout + a proof file. The 7// off-box harness then diffs our UART against qemu's UART and the known 8// answer 2870. Asserts our output contains "SUM=2870". 9// 10// expect_exit: 0 11// license_tier: ORIGINAL 12 13import "nx_syscalls.nx" 14import "nishi_hdl_primitives.nx" 15import "rv64im_min_decoder.nx" 16import "rv64im_min_alu.nx" 17import "rv64im_min_regfile.nx" 18import "rv64im_min_csr.nx" 19import "rv64im_min_clint.nx" 20import "rv64im_min_uart.nx" 21import "rv64im_min_sim.nx" 22import "rv64im_min_elf_loader.nx" 23 24const CC_MEM_BASE: i64 = 0x80000000 25const CC_MEM_SIZE: i64 = 0x400000 // 4 MiB (covers prog + 0x80100000 buf + 0x80200000 stack) 26const CC_TX_CAP: i64 = 4096 27const CC_MAX_STEPS: i64 = 1000000 28 29func _contains(hay: *u8, hlen: i64, needle: *u8, nlen: i64) -> i64 { 30 if nlen == 0 { return 1 } 31 if hlen < nlen { return 0 } 32 let last: i64 = hlen - nlen 33 var i: i64 = 0 34 while i <= last { 35 var j: i64 = 0 36 var ok: i64 = 1 37 while j < nlen { 38 if hay[i + j] != needle[j] { ok = 0; j = nlen } 39 j = j + 1 40 } 41 if ok == 1 { return 1 } 42 i = i + 1 43 } 44 return 0 45} 46 47func _slen(s: *u8) -> i64 { 48 var n: i64 = 0 49 while s[n] != 0 { n = n + 1 } 50 return n 51} 52 53func main() -> i64 { 54 let path: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/cpu_crosscheck_prog.bin\x00" 55 let elf_len_out: *i64 = (sys_mmap(8)) as *i64 56 elf_len_out[0] = 0 57 let elf_bytes: *u8 = sys_read_file(path, elf_len_out) 58 let elf_size: i64 = elf_len_out[0] 59 if (elf_bytes as i64) == 0 { return 1 } 60 if elf_size < 64 { return 2 } 61 62 let rf_storage: *i64 = (sys_mmap(8 * NX_RV64IM_RF_N_REGS)) as *i64 63 let csr_storage: *i64 = (sys_mmap(8 * NX_CSR_SLOT_N)) as *i64 64 let clint_storage: *i64 = (sys_mmap(8 * NX_CLINT_SLOT_N)) as *i64 65 let uart_storage: *i64 = (sys_mmap(8 * NX_UART_SLOT_N)) as *i64 66 let mem: *u8 = sys_mmap(CC_MEM_SIZE) 67 let tx_buf: *u8 = sys_mmap(CC_TX_CAP) 68 69 let rf: *NxRv64imRegfile = (sys_mmap(64)) as *NxRv64imRegfile 70 let csr: *NxRv64imCsrFile = (sys_mmap(64)) as *NxRv64imCsrFile 71 let clint: *NxClint = (sys_mmap(64)) as *NxClint 72 let uart: *NxUart = (sys_mmap(64)) as *NxUart 73 let sim: *NxRv64imSim = (sys_mmap(128)) as *NxRv64imSim 74 75 nx_rv64im_rf_init(rf, rf_storage) 76 nx_rv64im_csr_init(csr, csr_storage, 0) 77 nx_clint_init(clint, clint_storage) 78 nx_uart_init(uart, uart_storage, tx_buf, CC_TX_CAP) 79 nx_rv64im_sim_init(sim, rf, csr, clint, uart, CC_MEM_BASE, mem, CC_MEM_SIZE, 0) 80 81 // Raw-load the flat program image at mem_base (sim_init already set 82 // pc = mem_base + 0). The ELF's own LOAD segment sits at 0x7ffff000 83 // (it carries the ELF headers) which is below our mem_base, so we use 84 // the objcopy'd flat binary instead -- byte 0 == the instruction at 85 // 0x80000000. 86 if elf_size > CC_MEM_SIZE { return 3 } 87 var ci: i64 = 0 88 while ci < elf_size { 89 mem[ci] = elf_bytes[ci] 90 ci = ci + 1 91 } 92 93 nx_rv64im_sim_run(sim, CC_MAX_STEPS) 94 95 let tx_n: i64 = nx_uart_tx_count(uart) 96 if tx_n == 0 { return 5 } 97 98 // emit captured UART to stdout + proof file 99 let banner: *u8 = "\n[our sovereign RV64IM CPU sim UART output]\n\x00" 100 sys_write(1, banner, 43) 101 sys_write(1, tx_buf, tx_n) 102 sys_write(1, banner, 1) 103 104 let outp: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/sim_uart_out.txt\x00" 105 let ofd: i64 = sys_openat_wr(outp, 0x1A4) 106 if ofd > 0 { sys_write(ofd, tx_buf, tx_n); sys_close(ofd) } 107 108 let want: *u8 = "SUM=2870\x00" 109 if _contains(tx_buf, tx_n, want, _slen(want)) != 1 { return 80 } 110 111 let pass: *u8 = sys_mmap(16) 112 pass[0]=0x50; pass[1]=0x41; pass[2]=0x53; pass[3]=0x53; pass[4]=0x0A 113 sys_write(2, pass, 5) 114 return 0 115}