nx_rv64im_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" 15const K_MAGIC_9223372036854775807: i64 = 9223372036854775807 16const K_MAGIC_4294967296: i64 = 4294967296 17const K_MAGIC_4294967295: i64 = 4294967295 18const K_MAGIC_2147483648: i64 = 2147483648 19const K_MAGIC_2147483647: i64 = 2147483647 20const K_MAGIC_8388608: i64 = 8388608 21const K_MAGIC_88172645463325252: i64 = 88172645463325252 22const K_MAGIC_6364136223846793005: i64 = 6364136223846793005 23const K_MAGIC_1442695040888963407: i64 = 1442695040888963407 24 25func _hex16(v: i64, out: *u8, pos: i64) -> i64 { 26 var k: i64 = 15 27 var p: i64 = pos 28 while k >= 0 { 29 let nib: i64 = (v >> (k * 4)) & 15 30 if nib < 10 { out[p] = (0x30 + nib) as u8 } 31 if nib >= 10 { out[p] = (0x61 + nib - 10) as u8 } 32 p = p + 1 33 k = k - 1 34 } 35 return p 36} 37 38func _dec2(v: i64, out: *u8, pos: i64) -> i64 { 39 var p: i64 = pos 40 if v >= 10 { out[p] = (0x30 + (v / 10)) as u8; p = p + 1 } 41 out[p] = (0x30 + (v % 10)) as u8 42 p = p + 1 43 return p 44} 45 46func _emit_vec(op: i64, a: i64, b: i64, out: *u8, pos: i64) -> i64 { 47 let r: i64 = nx_rv64im_alu_compute(op, a, b) 48 var p: i64 = pos 49 p = _dec2(op, out, p) 50 out[p] = 0x09 as u8; p = p + 1 51 p = _hex16(a, out, p) 52 out[p] = 0x09 as u8; p = p + 1 53 p = _hex16(b, out, p) 54 out[p] = 0x09 as u8; p = p + 1 55 p = _hex16(r, out, p) 56 out[p] = 0x0A as u8; p = p + 1 57 return p 58} 59 60func main() -> i64 { 61 // Edge-value table (built arithmetically; NishiLang large hex 62 // literals are avoided per the substrate idiom). 63 let E: *i64 = sys_mmap(8 * 16) as *i64 64 E[0]=0; E[1]=1; E[2]=2; E[3]=3; E[4]=7 65 E[5]=0 - 1 // 0xFFFFFFFFFFFFFFFF 66 E[6]=0 - 9223372036854775808 // INT_MIN 67 E[7]=K_MAGIC_9223372036854775807 // INT_MAX 68 E[8]=K_MAGIC_4294967296 // 1<<32 69 E[9]=K_MAGIC_4294967295 // 0xFFFFFFFF 70 E[10]=K_MAGIC_2147483648 // 1<<31 71 E[11]=K_MAGIC_2147483647 // 0x7FFFFFFF 72 E[12]=0 - K_MAGIC_2147483648 // -(1<<31) 73 E[13]=255 74 E[14]=256 75 E[15]=0 - 256 76 let ne: i64 = 16 77 78 let out: *u8 = sys_mmap(K_MAGIC_8388608) as *u8 // 8 MiB 79 var pos: i64 = 0 80 81 // LCG state (MMIX constants); deterministic. 82 var lcg: i64 = K_MAGIC_88172645463325252 83 84 var op: i64 = 1 85 while op < NX_RV64IM_ALU_N { 86 // trace current op to stderr so a native-divide trap is locatable 87 let tb: *u8 = sys_mmap(8) 88 var tp: i64 = _dec2(op, tb, 0) 89 tb[tp] = 0x0A as u8 90 sys_write(2, tb, tp + 1) 91 // All edge x edge crosses. 92 var i: i64 = 0 93 while i < ne { 94 var j: i64 = 0 95 while j < ne { 96 pos = _emit_vec(op, E[i], E[j], out, pos) 97 j = j + 1 98 } 99 i = i + 1 100 } 101 // LCG random pairs. 102 var k: i64 = 0 103 while k < 256 { 104 lcg = lcg * K_MAGIC_6364136223846793005 + K_MAGIC_1442695040888963407 105 let a: i64 = lcg 106 lcg = lcg * K_MAGIC_6364136223846793005 + K_MAGIC_1442695040888963407 107 let b: i64 = lcg 108 pos = _emit_vec(op, a, b, out, pos) 109 k = k + 1 110 } 111 op = op + 1 112 } 113 114 let path: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/alu_vectors.tsv\x00" 115 let ofd: i64 = sys_openat_wr(path, 0x1A4) 116 if ofd <= 0 { return 70 } 117 sys_write(ofd, out, pos) 118 sys_close(ofd) 119 120 let pass: *u8 = sys_mmap(16) 121 pass[0]=0x4F; pass[1]=0x4B; pass[2]=0x0A // "OK\n" 122 sys_write(1, pass, 3) 123 return 0 124}