rv64im_min_decoder_proof.nx source

1// nx_rv64im_decoder_dump.nx -- dump rv64im_min_decoder field outputs 2// for every word in decode_words.bin, so an independent Python RV64 3// decoder can diff them 1:1. Per-word line (all hex16, tab-sep): 4// word opcode funct3 funct7 rd rs1 rs2 imm_i imm_s imm_b imm_u imm_j kind 5// 6// expect_exit: 0 7// license_tier: ORIGINAL 8import "nx_syscalls.nx" 9import "nishi_hdl_primitives.nx" 10import "rv64im_min_decoder.nx" 11 12func _hex16(v: i64, out: *u8, pos: i64) -> i64 { 13 var k: i64 = 15 14 var p: i64 = pos 15 while k >= 0 { 16 let nib: i64 = (v >> (k * 4)) & 15 17 if nib < 10 { out[p] = (0x30 + nib) as u8 } 18 if nib >= 10 { out[p] = (0x61 + nib - 10) as u8 } 19 p = p + 1 20 k = k - 1 21 } 22 return p 23} 24 25func _field(out: *u8, pos: i64, v: i64, sep: i64) -> i64 { 26 var p: i64 = _hex16(v, out, pos) 27 out[p] = sep as u8 28 return p + 1 29} 30 31func main() -> i64 { 32 let path: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/decode_words.bin\x00" 33 let len_p: *i64 = sys_mmap(8) as *i64 34 let bytes: *u8 = sys_read_file(path, len_p) 35 let blen: i64 = len_p[0] 36 if (bytes as i64) == 0 { return 1 } 37 let nwords: i64 = blen / 4 38 39 let out: *u8 = sys_mmap(16777216) as *u8 // 16 MiB 40 var pos: i64 = 0 41 var i: i64 = 0 42 while i < nwords { 43 let o: i64 = i * 4 44 let b0: i64 = (bytes[o] as i64) & 255 45 let b1: i64 = (bytes[o + 1] as i64) & 255 46 let b2: i64 = (bytes[o + 2] as i64) & 255 47 let b3: i64 = (bytes[o + 3] as i64) & 255 48 let w: i64 = b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 49 pos = _field(out, pos, w, 9) 50 pos = _field(out, pos, nx_rv64im_opcode(w), 9) 51 pos = _field(out, pos, nx_rv64im_funct3(w), 9) 52 pos = _field(out, pos, nx_rv64im_funct7(w), 9) 53 pos = _field(out, pos, nx_rv64im_rd(w), 9) 54 pos = _field(out, pos, nx_rv64im_rs1(w), 9) 55 pos = _field(out, pos, nx_rv64im_rs2(w), 9) 56 pos = _field(out, pos, nx_rv64im_imm_i(w), 9) 57 pos = _field(out, pos, nx_rv64im_imm_s(w), 9) 58 pos = _field(out, pos, nx_rv64im_imm_b(w), 9) 59 pos = _field(out, pos, nx_rv64im_imm_u(w), 9) 60 pos = _field(out, pos, nx_rv64im_imm_j(w), 9) 61 pos = _field(out, pos, nx_rv64im_decode_kind(w), 10) 62 i = i + 1 63 } 64 65 let outp: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/decode_dump.tsv\x00" 66 let ofd: i64 = sys_openat_wr(outp, 0x1A4) 67 if ofd <= 0 { return 70 } 68 sys_write(ofd, out, pos) 69 sys_close(ofd) 70 71 let pass: *u8 = sys_mmap(8) 72 pass[0]=0x4F; pass[1]=0x4B; pass[2]=0x0A 73 sys_write(1, pass, 3) 74 return 0 75}