nx_isa_spec_test.nx source

1// nx_isa_spec_test.nx -- prove the SPEC-DRIVEN encoder: (1) it reproduces the 2// oracle-verified KAT words (the same ones riscv64-as emits, per nx_emu_rv64_test), 3// (2) instructions added by DATA (xor, or) encode correctly, and (3) a program the 4// SEARCH authored, lowered THROUGH the spec table to BOTH RV64 and AArch64, runs 5// correctly on the sovereign emulators. No per-instruction encoder was hand-written 6// -- each instruction is a data row + one shared format assembler. 7// 8// Known answer: KATs match, both arches execute x*C for the searched constants, 9// exit 0. 10 11import "nx_isa_spec.nx" 12import "nx_emu_rv64.nx" 13import "nx_emu_arm64.nx" 14 15func is_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 16func is_num(v: i64) -> i64 { 17 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 18 let t: *u8 = sys_mmap(28); var k: i64 = 0 19 if m == 0 { t[0] = 48; k = 1 } 20 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 21 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 22 sys_write(1, b, k); return 0 23} 24func is_put_w(code: *u8, o: i64, w: i64) -> i64 { 25 code[o] = w & 0xff; code[o+1] = (w >> 8) & 0xff; code[o+2] = (w >> 16) & 0xff; code[o+3] = (w >> 24) & 0xff 26 return o + 4 27} 28 29// the GENERATOR (search): cheapest (x<<a) op (x<<b) == x*C. 30func is_eval(a: i64, op: i64, b: i64, x: i64) -> i64 { if op == 0 { return (x << a) + (x << b) } return (x << a) - (x << b) } 31func is_best(C: i64, out: *i64) -> i64 { 32 var a: i64 = 0 33 while a < 12 { 34 var b: i64 = 0 35 while b < 12 { 36 var op: i64 = 0 37 while op < 2 { 38 var ok: i64 = 1 39 var s: i64 = 19088743; var t: i64 = 0 40 while t < 20 { s = s * 6364136223846793005 + 1442695040888963407; if is_eval(a, op, b, s) != s * C { ok = 0 } t = t + 1 } 41 if ok == 1 { let c: i64 = 1 + a + b + b 42 if out[3] < 0 { out[0]=a; out[1]=op; out[2]=b; out[3]=c } else { if c < out[3] { out[0]=a; out[1]=op; out[2]=b; out[3]=c } } } 43 op = op + 1 44 } 45 b = b + 1 46 } 47 a = a + 1 48 } 49 if out[3] < 0 { return 0 } 50 return 1 51} 52 53// assemble x*C (plan a,op,b) for RV64 from the SPEC TABLE; run; return result. 54func is_run_rv(x: i64, a: i64, op: i64, b: i64) -> i64 { 55 let code: *u8 = sys_mmap(64); var o: i64 = 0 56 o = is_put_w(code, o, isa_emit(I_RV_ADDI, 11, 0, 0, x)) 57 o = is_put_w(code, o, isa_emit(I_RV_SLLI, 5, 11, 0, a)) 58 o = is_put_w(code, o, isa_emit(I_RV_SLLI, 6, 11, 0, b)) 59 if op == 0 { o = is_put_w(code, o, isa_emit(I_RV_ADD, 10, 5, 6, 0)) } else { o = is_put_w(code, o, isa_emit(I_RV_SUB, 10, 5, 6, 0)) } 60 o = is_put_w(code, o, isa_emit(I_RV_ADDI, 17, 0, 0, 93)) 61 o = is_put_w(code, o, isa_emit(I_RV_ECALL, 0, 0, 0, 0)) 62 return emu_rv64_run(code, o) 63} 64// same for AArch64 from the SPEC TABLE. 65func is_run_a64(x: i64, a: i64, op: i64, b: i64) -> i64 { 66 let code: *u8 = sys_mmap(64); var o: i64 = 0 67 o = is_put_w(code, o, isa_emit(I_A64_MOVZ, 1, 0, 0, x)) 68 o = is_put_w(code, o, isa_emit(I_A64_ADD, 9, 31, 1, a)) 69 if op == 0 { o = is_put_w(code, o, isa_emit(I_A64_ADD, 0, 9, 1, b)) } else { o = is_put_w(code, o, isa_emit(I_A64_SUB, 0, 9, 1, b)) } 70 o = is_put_w(code, o, isa_emit(I_A64_MOVZ, 8, 0, 0, 93)) 71 o = is_put_w(code, o, isa_emit(I_A64_SVC, 0, 0, 0, 0)) 72 return emu_arm64_run(code, o) 73} 74 75func main() -> i64 { 76 is_puts("=== SPEC-DRIVEN encoder: data rows + one assembler, multi-arch ===\n" as *u8) 77 var katfail: i64 = 0 78 79 // (1) oracle-verified KAT words (same as nx_emu_rv64_test / riscv64-as). 80 if isa_emit(I_RV_ADDI, 10, 0, 0, 40) != 0x02800513 { katfail = katfail + 1 } // addi a0,zero,40 81 if isa_emit(I_RV_ADD, 10, 10, 5, 0) != 0x00550533 { katfail = katfail + 1 } // add a0,a0,t0 82 if isa_emit(I_RV_SUB, 10, 10, 5, 0) != 0x40550533 { katfail = katfail + 1 } // sub a0,a0,t0 83 if isa_emit(I_RV_ECALL, 0, 0, 0, 0) != 0x73 { katfail = katfail + 1 } // ecall 84 if isa_emit(I_A64_SVC, 0, 0, 0, 0) != 0xD4000001 { katfail = katfail + 1 } // svc #0 85 // (2) instructions added by DATA (no new encoder code) -- xor / or, manual-checked. 86 if isa_emit(I_RV_XOR, 10, 10, 5, 0) != 0x00554533 { katfail = katfail + 1 } // xor a0,a0,t0 87 if isa_emit(I_RV_OR, 10, 10, 5, 0) != 0x00556533 { katfail = katfail + 1 } // or a0,a0,t0 88 is_puts(" KAT + new-by-data encodings mismatched: " as *u8); is_num(katfail); is_puts("\n" as *u8) 89 90 // (3) the search authors x*C; the SPEC TABLE lowers it to both ISAs; run them. 91 let consts: *i64 = sys_mmap(8 * 8) as *i64 92 var n: i64 = 0 93 consts[n] = 7; n = n + 1 94 consts[n] = 9; n = n + 1 95 consts[n] = 5; n = n + 1 96 let out: *i64 = sys_mmap(32) as *i64 97 var rv_ok: i64 = 0 98 var a64_ok: i64 = 0 99 var i: i64 = 0 100 while i < n { 101 let C: i64 = consts[i] 102 out[3] = 0 - 1 103 if is_best(C, out) == 1 { 104 let a: i64 = out[0]; let op: i64 = out[1]; let b: i64 = out[2] 105 let maxx: i64 = 255 / C 106 var rok: i64 = 1 107 var aok: i64 = 1 108 var x: i64 = 0 109 while x <= maxx { 110 if is_run_rv(x, a, op, b) != x * C { rok = 0 } 111 if is_run_a64(x, a, op, b) != x * C { aok = 0 } 112 x = x + 1 113 } 114 is_puts(" x*" as *u8); is_num(C); is_puts(" (spec-assembled) " as *u8) 115 if rok == 1 { rv_ok = rv_ok + 1; is_puts("RV64:exec-ok " as *u8) } else { is_puts("RV64:FAIL " as *u8) } 116 if aok == 1 { a64_ok = a64_ok + 1; is_puts("ARM64:exec-ok\n" as *u8) } else { is_puts("ARM64:FAIL\n" as *u8) } 117 } 118 i = i + 1 119 } 120 121 is_puts("----------------------------------------------------------------\n" as *u8) 122 is_puts(" spec-driven encoder proven: RV64 " as *u8); is_num(rv_ok); is_puts("/" as *u8); is_num(n) 123 is_puts(" ARM64 " as *u8); is_num(a64_ok); is_puts("/" as *u8); is_num(n); is_puts("\n" as *u8) 124 is_puts(" the team encodes any instruction from a DATA row -- no hand-written encoder.\n" as *u8) 125 126 if katfail != 0 { sys_exit(1); return 1 } 127 if rv_ok != n { sys_exit(2); return 2 } 128 if a64_ok != n { sys_exit(3); return 3 } 129 sys_exit(0) 130 return 0 131}