rv64im_min_alu_proof.nx source

1// nx_rv64im_alu_proof.nx -- vector dumper to PROVE the RV64IM ALU. 2// 3// Runs nx_rv64im_alu_compute over every ALU op (1..28) across a 4// deterministic mix of edge values + LCG-generated 64-bit operands, 5// and writes "<op_dec>\t<a_hex16>\t<b_hex16>\t<r_hex16>\n" lines to 6// the proof folder. An independent Python implementation of the 7// RV64IM spec then recomputes each result and diffs -- 1:1 proof, 8// not "assertions PASS". 9// 10// expect_exit: 0 11// license_tier: ORIGINAL 12 13import "nx_syscalls.nx" 14import "rv64im_min_alu.nx" 15 16func _hex16(v: i64, out: *u8, pos: i64) -> i64 { 17 var k: i64 = 15 18 var p: i64 = pos 19 while k >= 0 { 20 let nib: i64 = (v >> (k * 4)) & 15 21 if nib < 10 { out[p] = (0x30 + nib) as u8 } 22 if nib >= 10 { out[p] = (0x61 + nib - 10) as u8 } 23 p = p + 1 24 k = k - 1 25 } 26 return p 27} 28 29func _dec2(v: i64, out: *u8, pos: i64) -> i64 { 30 var p: i64 = pos 31 if v >= 10 { out[p] = (0x30 + (v / 10)) as u8; p = p + 1 } 32 out[p] = (0x30 + (v % 10)) as u8 33 p = p + 1 34 return p 35} 36 37func _emit_vec(op: i64, a: i64, b: i64, out: *u8, pos: i64) -> i64 { 38 let r: i64 = nx_rv64im_alu_compute(op, a, b) 39 var p: i64 = pos 40 p = _dec2(op, out, p) 41 out[p] = 0x09 as u8; p = p + 1 42 p = _hex16(a, out, p) 43 out[p] = 0x09 as u8; p = p + 1 44 p = _hex16(b, out, p) 45 out[p] = 0x09 as u8; p = p + 1 46 p = _hex16(r, out, p) 47 out[p] = 0x0A as u8; p = p + 1 48 return p 49} 50 51func main() -> i64 { 52 // Edge-value table (built arithmetically; NishiLang large hex 53 // literals are avoided per the substrate idiom). 54 let E: *i64 = sys_mmap(8 * 16) as *i64 55 E[0]=0; E[1]=1; E[2]=2; E[3]=3; E[4]=7 56 E[5]=0 - 1 // 0xFFFFFFFFFFFFFFFF 57 E[6]=0 - 9223372036854775808 // INT_MIN 58 E[7]=9223372036854775807 // INT_MAX 59 E[8]=4294967296 // 1<<32 60 E[9]=4294967295 // 0xFFFFFFFF 61 E[10]=2147483648 // 1<<31 62 E[11]=2147483647 // 0x7FFFFFFF 63 E[12]=0 - 2147483648 // -(1<<31) 64 E[13]=255 65 E[14]=256 66 E[15]=0 - 256 67 let ne: i64 = 16 68 69 let out: *u8 = sys_mmap(8388608) as *u8 // 8 MiB 70 var pos: i64 = 0 71 72 // LCG state (MMIX constants); deterministic. 73 var lcg: i64 = 88172645463325252 74 75 var op: i64 = 1 76 while op < NX_RV64IM_ALU_N { 77 // trace current op to stderr so a native-divide trap is locatable 78 let tb: *u8 = sys_mmap(8) 79 var tp: i64 = _dec2(op, tb, 0) 80 tb[tp] = 0x0A as u8 81 sys_write(2, tb, tp + 1) 82 // All edge x edge crosses. 83 var i: i64 = 0 84 while i < ne { 85 var j: i64 = 0 86 while j < ne { 87 pos = _emit_vec(op, E[i], E[j], out, pos) 88 j = j + 1 89 } 90 i = i + 1 91 } 92 // LCG random pairs. 93 var k: i64 = 0 94 while k < 256 { 95 lcg = lcg * 6364136223846793005 + 1442695040888963407 96 let a: i64 = lcg 97 lcg = lcg * 6364136223846793005 + 1442695040888963407 98 let b: i64 = lcg 99 pos = _emit_vec(op, a, b, out, pos) 100 k = k + 1 101 } 102 op = op + 1 103 } 104 105 let path: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/alu_vectors.tsv\x00" 106 let ofd: i64 = sys_openat_wr(path, 0x1A4) 107 if ofd <= 0 { return 70 } 108 sys_write(ofd, out, pos) 109 sys_close(ofd) 110 111 let pass: *u8 = sys_mmap(16) 112 pass[0]=0x4F; pass[1]=0x4B; pass[2]=0x0A // "OK\n" 113 sys_write(1, pass, 3) 114 return 0 115}