nx_isa_equiv_sov.nx source

1// nx_isa_equiv_sov.nx -- THE DIFFERENTIAL-REPLACEMENT TEST, ON THE HARDWARE. 2// 3// The operator's own method ("comp a working child, turn it off, emit ours, see if they 4// function the same") performed at the genesis-hardware level, with NO Claude crutch left: 5// 6// (1) the team COMPOSES its own random non-trivial target program T (over the REAL RV64IM 7// ALU ops that rv64im_min_sim executes -- ADD/SUB/MUL/AND/OR/SLT on a register machine), 8// (2) the team DERIVES a program G by evolutionary search that matches T's TRAIN examples 9// (search sees only (a,b)->T(a,b) points, never T's source), 10// (3) we ENCODE BOTH T and G to real RV64 machine code, run BOTH on rv64im_min_sim (god) 11// over 12 HELD-OUT inputs, and verify sim(T) == sim(G) as FULL 64-bit values. 12// 13// The equivalence verdict reads the hardware -- the interpreter only GUIDES the search, it is 14// NOT in the proof. Two controls keep it honest: a FAITHFUL-ENCODE control (all 6 ops 15// encode->run->match the ALU) and a NEGATIVE control (a perturbed G the differential MUST 16// catch -- proving the test discriminates, not rubber-stamps). 17// 18// Full 64-bit read-back: each program does `sd x3, RES_OFF(x5)` to scratch RAM; store64 writes 19// through to mem_buf (verified rv64im_min_sim.nx:415), which we read back directly. license_tier: ORIGINAL 20import "nx_syscalls.nx" 21import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc) 22import "nishi_hdl_primitives.nx" 23import "rv64im_min_decoder.nx" 24import "rv64im_min_alu.nx" 25import "rv64im_min_regfile.nx" 26import "rv64im_min_csr.nx" 27import "rv64im_min_clint.nx" 28import "rv64im_min_uart.nx" 29import "rv64im_min_sim.nx" 30const EVO_MAGIC_2862933555777941757: i64 = 2862933555777941757 31const EVO_MAGIC_3037000493: i64 = 3037000493 32const EVO_MAGIC_1000000000000: i64 = 1000000000000 33const EVO_MAGIC_10000000000000: i64 = 10000000000000 34const EVO_MAGIC_1000000000: i64 = 1000000000 35const EVO_MAGIC_2654435761: i64 = 2654435761 36const EVO_MAGIC_12345: i64 = 12345 37 38const NINSTR: i64 = 3 39const GLEN: i64 = 9 // NINSTR * 3 (op, rs1, rs2); rd = x3 fixed 40const EVO_P: i64 = 320 41const EVO_G: i64 = 1400 42const EVO_T: i64 = 5 43const NTRAIN: i64 = 6 44const NHELD: i64 = 12 45 46const IR_MEM_BASE: i64 = 0x80000000 47const IR_MEM_SIZE: i64 = 8192 48const IR_TX_CAP: i64 = 256 49const RES_OFF: i64 = 0x700 // scratch result slot (positive S-imm, past the ~52-byte code) 50 51// ---- prng / util ----------------------------------------------------------------------- 52func ie_rand(s: *i64) -> i64 { s[0] = s[0] * EVO_MAGIC_2862933555777941757 + EVO_MAGIC_3037000493; return (s[0] >> 17) & 0x3fffffff } 53func ie_abs(x: i64) -> i64 { if x < 0 { return 0 - x } return x } 54 55// train points (search fits these) and held-out points (verdict checks these; disjoint). 56func ie_pa(i: i64) -> i64 { if i==0 {return 6} if i==1 {return 4} if i==2 {return 9} if i==3 {return 5} if i==4 {return 7} return 2 } 57func ie_pb(i: i64) -> i64 { if i==0 {return 4} if i==1 {return 7} if i==2 {return 2} if i==3 {return 9} if i==4 {return 3} return 5 } 58func ie_ha(i: i64) -> i64 { if i==0 {return 3} if i==1 {return 8} if i==2 {return 11} if i==3 {return 2} if i==4 {return 10} if i==5 {return 13} if i==6 {return 7} if i==7 {return 4} if i==8 {return 12} if i==9 {return 6} if i==10 {return 9} return 5 } 59func ie_hb(i: i64) -> i64 { if i==0 {return 5} if i==1 {return 2} if i==2 {return 7} if i==3 {return 11} if i==4 {return 4} if i==5 {return 3} if i==6 {return 9} if i==7 {return 8} if i==8 {return 2} if i==9 {return 13} if i==10 {return 6} return 10 } 60 61// ---- the REAL RV64IM ALU op (semantics matched to rv64im_min_sim; 6 total functions) ---- 62func ie_op(op: i64, x: i64, y: i64) -> i64 { 63 if op == 0 { return x + y } // ADD 64 if op == 1 { return x - y } // SUB 65 if op == 2 { return x * y } // MUL 66 if op == 3 { return x & y } // AND 67 if op == 4 { return x | y } // OR 68 if x < y { return 1 } return 0 // SLT 69} 70// op index -> the sim's funct3 / funct7 (rv64im_min_sim.nx alu_select, verified). 71func ie_f3(op: i64) -> i64 { if op==3 {return 7} if op==4 {return 6} if op==5 {return 2} return 0 } // AND=7 OR=6 SLT=2 else 0 72func ie_f7(op: i64) -> i64 { if op==1 {return 0x20} if op==2 {return 0x01} return 0x00 } // SUB=0x20 MUL=0x01 else 0 73// register select: r0=0(x0), r1=a(x1), r2=b(x2), r3=acc(x3) -- index == x-register number. 74func ie_reg(idx: i64, a: i64, b: i64, acc: i64) -> i64 { 75 if idx == 0 { return 0 } 76 if idx == 1 { return a } 77 if idx == 2 { return b } 78 return acc 79} 80// interpreter: execute a genome (register-machine program) on inputs a,b -> acc (=x3). 81func ie_eval(gen: *i64, base: i64, a: i64, b: i64) -> i64 { 82 var acc: i64 = 0 83 var j: i64 = 0 84 while j < NINSTR { 85 let op: i64 = gen[base + j*3] 86 let rs1: i64 = gen[base + j*3 + 1] 87 let rs2: i64 = gen[base + j*3 + 2] 88 let x: i64 = ie_reg(rs1, a, b, acc) 89 let y: i64 = ie_reg(rs2, a, b, acc) 90 acc = ie_op(op, x, y) 91 j = j + 1 92 } 93 return acc 94} 95 96// ---- RV64 encoders (rv_rtype/rv_addi/rv_lui proven in nx_isa_run_sov; rv_store_imm = S-type) ---- 97func rv_addi(rd: i64, rs1: i64, imm: i64) -> i64 { return ((imm & 0xFFF) << 20) | (rs1 << 15) | (rd << 7) | 0x13 } 98func rv_lui(rd: i64, imm20: i64) -> i64 { return ((imm20 & 0xFFFFF) << 12) | (rd << 7) | 0x37 } 99func rv_rtype(f7: i64, rs2: i64, rs1: i64, f3: i64, rd: i64) -> i64 { return (f7 << 25) | (rs2 << 20) | (rs1 << 15) | (f3 << 12) | (rd << 7) | 0x33 } 100func rv_store_imm(rs2: i64, rs1: i64, f3: i64, imm: i64) -> i64 { 101 let hi: i64 = (imm >> 5) & 0x7f 102 let lo: i64 = imm & 0x1f 103 return (hi << 25) | (rs2 << 20) | (rs1 << 15) | (f3 << 12) | (lo << 7) | 0x23 104} 105func rv_w32(buf: *u8, off: i64, w: i64) -> i64 { 106 buf[off] = (w & 0xff) as u8 107 buf[off+1] = ((w >> 8) & 0xff) as u8 108 buf[off+2] = ((w >> 16) & 0xff) as u8 109 buf[off+3] = ((w >> 24) & 0xff) as u8 110 return off + 4 111} 112// emit: x1=a; x2=b; x3=0; <genome as R-type, rd=x3>; x5=RAM base; sd x3,RES_OFF(x5); finisher halt; spin. 113func ie_emit(mem: *u8, gen: *i64, base: i64, a: i64, b: i64) -> i64 { 114 var o: i64 = 0 115 o = rv_w32(mem, o, rv_addi(1, 0, a)) // addi x1, x0, a 116 o = rv_w32(mem, o, rv_addi(2, 0, b)) // addi x2, x0, b 117 o = rv_w32(mem, o, rv_addi(3, 0, 0)) // addi x3, x0, 0 (acc = 0) 118 var j: i64 = 0 119 while j < NINSTR { 120 let op: i64 = gen[base + j*3] 121 let rs1: i64 = gen[base + j*3 + 1] 122 let rs2: i64 = gen[base + j*3 + 2] 123 o = rv_w32(mem, o, rv_rtype(ie_f7(op), rs2, rs1, ie_f3(op), 3)) // x3 = op(x[rs1], x[rs2]) 124 j = j + 1 125 } 126 o = rv_w32(mem, o, rv_lui(5, 0x80000)) // lui x5, 0x80000 (x5 = RAM base 0x80000000) 127 o = rv_w32(mem, o, rv_store_imm(3, 5, 3, RES_OFF)) // sd x3, RES_OFF(x5) (full 64-bit result to RAM) 128 o = rv_w32(mem, o, rv_lui(7, 0x100)) // lui x7, 0x100 (finisher 0x100000) 129 o = rv_w32(mem, o, rv_lui(6, 0x5)) // lui x6, 0x5 130 o = rv_w32(mem, o, rv_addi(6, 6, 0x555)) // addi x6, x6, 0x555 (x6 = 0x5555 PASS) 131 o = rv_w32(mem, o, rv_store_imm(6, 7, 2, 0)) // sw x6, 0(x7) (finisher <- 0x5555 -> halt) 132 o = rv_w32(mem, o, 0x6F) // jal x0, 0 (spin) 133 return o 134} 135// read a little-endian i64 back from the scratch RAM slot (mirrors sim load64). 136func ie_read_i64(mem: *u8, off: i64) -> i64 { 137 var v: i64 = 0 138 var i: i64 = 0 139 while i < 8 { v = v | ((mem[off + i] as i64) << (i * 8)); i = i + 1 } 140 return v 141} 142// RUN a genome on the GENESIS SIM (fresh devices each call -> clean reset) and return its 64-bit result. 143func ie_run_prog(gen: *i64, base: i64, a: i64, b: i64) -> i64 { 144 let rf_storage: *i64 = (sys_mmap(8 * NX_RV64IM_RF_N_REGS)) as *i64 145 let csr_storage: *i64 = (sys_mmap(8 * NX_CSR_SLOT_N)) as *i64 146 let clint_storage: *i64 = (sys_mmap(8 * NX_CLINT_SLOT_N)) as *i64 147 let uart_storage: *i64 = (sys_mmap(8 * NX_UART_SLOT_N)) as *i64 148 let mem: *u8 = sys_mmap(IR_MEM_SIZE) 149 let tx_buf: *u8 = sys_mmap(IR_TX_CAP) 150 let rf: *NxRv64imRegfile = (sys_mmap(64)) as *NxRv64imRegfile 151 let csr: *NxRv64imCsrFile = (sys_mmap(64)) as *NxRv64imCsrFile 152 let clint: *NxClint = (sys_mmap(64)) as *NxClint 153 let uart: *NxUart = (sys_mmap(64)) as *NxUart 154 let sim: *NxRv64imSim = (sys_mmap(128)) as *NxRv64imSim 155 nx_rv64im_rf_init(rf, rf_storage) 156 nx_rv64im_csr_init(csr, csr_storage, 0) 157 nx_clint_init(clint, clint_storage) 158 nx_uart_init(uart, uart_storage, tx_buf, IR_TX_CAP) 159 nx_rv64im_sim_init(sim, rf, csr, clint, uart, IR_MEM_BASE, mem, IR_MEM_SIZE, 0) 160 ie_emit(mem, gen, base, a, b) 161 nx_rv64im_sim_run(sim, 400) 162 return ie_read_i64(mem, RES_OFF) 163} 164 165// ---- compose / derive (GA) ------------------------------------------------------------- 166func ie_setinstr(gen: *i64, j: i64, state: *i64) -> i64 { 167 gen[j*3] = ie_rand(state) % 6 // op (6 total-function ops) 168 gen[j*3 + 1] = ie_rand(state) % 4 // rs1 (x0..x3) 169 gen[j*3 + 2] = ie_rand(state) % 4 // rs2 170 return 0 171} 172// COMPOSE: random non-trivial target (depends on BOTH a and b). 173func ie_compose(state: *i64, T: *i64) -> i64 { 174 var tries: i64 = 0 175 while tries < 400 { 176 var j: i64 = 0 177 while j < NINSTR { ie_setinstr(T, j, state); j = j + 1 } 178 let y00: i64 = ie_eval(T, 0, 6, 4) 179 let ya: i64 = ie_eval(T, 0, 9, 4) 180 let yb: i64 = ie_eval(T, 0, 6, 9) 181 if y00 != ya { if y00 != yb { return 1 } } 182 tries = tries + 1 183 } 184 return 0 185} 186func ie_fit(pop: *i64, base: i64, T: *i64) -> i64 { 187 var err: i64 = 0; var i: i64 = 0 188 while i < NTRAIN { 189 let a: i64 = ie_pa(i); let b: i64 = ie_pb(i) 190 let r: i64 = ie_eval(pop, base, a, b) 191 let y: i64 = ie_eval(T, 0, a, b) 192 var d: i64 = ie_abs(r - y) 193 if r > EVO_MAGIC_1000000000000 { d = EVO_MAGIC_10000000000000 } 194 if r < (0 - EVO_MAGIC_1000000000000) { d = EVO_MAGIC_10000000000000 } 195 err = err + d; i = i + 1 196 } 197 return err 198} 199func ie_tourney(fit: *i64, state: *i64) -> i64 { 200 var bi: i64 = ie_rand(state) % EVO_P; var bd: i64 = fit[bi]; var k: i64 = 1 201 while k < EVO_T { let i: i64 = ie_rand(state) % EVO_P; if fit[i] < bd { bd = fit[i]; bi = i } k = k + 1 } 202 return bi 203} 204func ie_mut(gen: *i64, base: i64, state: *i64) -> i64 { 205 let j: i64 = ie_rand(state) % NINSTR 206 let f: i64 = ie_rand(state) % 3 207 if f == 0 { gen[base + j*3] = ie_rand(state) % 6 } else { gen[base + j*3 + f] = ie_rand(state) % 4 } 208 return 0 209} 210// DERIVE: evolve a program G matching T's TRAIN examples; store in G, return best_err. 211func ie_derive(T: *i64, state: *i64, G: *i64) -> i64 { 212 let pop: *i64 = sys_mmap(EVO_P * GLEN * 8) as *i64 213 let nxt: *i64 = sys_mmap(EVO_P * GLEN * 8) as *i64 214 let fit: *i64 = sys_mmap(EVO_P * 8) as *i64 215 var p: i64 = 0 216 while p < EVO_P { var j: i64 = 0; while j < NINSTR { ie_setinstr(pop, p*3 + j, state); j = j + 1 } p = p + 1 } 217 var best_err: i64 = EVO_MAGIC_1000000000 218 var g: i64 = 0 219 while g < EVO_G { 220 var gbest: i64 = EVO_MAGIC_1000000000; var gbp: i64 = 0 221 p = 0 222 while p < EVO_P { let e: i64 = ie_fit(pop, p*GLEN, T); fit[p] = e; if e < gbest { gbest = e; gbp = p } p = p + 1 } 223 if gbest < best_err { best_err = gbest; var j: i64 = 0; while j < GLEN { G[j] = pop[gbp*GLEN + j]; j = j + 1 } } 224 if best_err == 0 { g = EVO_G } else { 225 var j2: i64 = 0; while j2 < GLEN { nxt[j2] = G[j2]; j2 = j2 + 1 } 226 p = 1 227 while p < EVO_P { 228 let pa: i64 = ie_tourney(fit, state) * GLEN 229 let pb: i64 = ie_tourney(fit, state) * GLEN 230 let cut: i64 = ((ie_rand(state) % (NINSTR - 1)) + 1) * 3 231 var jj: i64 = 0 232 while jj < GLEN { if jj < cut { nxt[p*GLEN + jj] = pop[pa + jj] } else { nxt[p*GLEN + jj] = pop[pb + jj] } jj = jj + 1 } 233 ie_mut(nxt, p*GLEN, state) 234 p = p + 1 235 } 236 var c: i64 = 0; while c < EVO_P * GLEN { pop[c] = nxt[c]; c = c + 1 } 237 g = g + 1 238 } 239 } 240 return best_err 241} 242 243// ---- print ----------------------------------------------------------------------------- 244func ie_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 245// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer 246// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the 247// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls). 248// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign. 249func ie_pn(v: i64) -> i64 { nxi_out(v); return 0 } 250 251// CONTROL 1: every op encodes -> runs on the sim -> matches the ALU (faithful encode). 1-instr 252// genome [op,1,2] padded with no-ops [0,3,0] (acc = acc + x0 = acc). Returns 1 if all 6 pass. 253func ie_faithful() -> i64 { 254 let G: *i64 = sys_mmap(GLEN * 8) as *i64 255 var op: i64 = 0; var ok: i64 = 0 256 while op < 6 { 257 G[0] = op; G[1] = 1; G[2] = 2 258 G[3] = 0; G[4] = 3; G[5] = 0 259 G[6] = 0; G[7] = 3; G[8] = 0 260 let got: i64 = ie_run_prog(G, 0, 7, 3) 261 let exp: i64 = ie_op(op, 7, 3) 262 if got == exp { ok = ok + 1 } 263 op = op + 1 264 } 265 ie_p(" control-faithful: " as *u8); ie_pn(ok); ie_p("/6 ops encode->run-on-god->match ALU\n" as *u8) 266 if ok == 6 { return 1 } 267 return 0 268} 269 270// the HARDWARE differential: run BOTH genomes on god over held-out, count points where sim(A)==sim(B). 271func ie_hw_agree(A: *i64, B: *i64) -> i64 { 272 var agree: i64 = 0; var i: i64 = 0 273 while i < NHELD { 274 let a: i64 = ie_ha(i); let b: i64 = ie_hb(i) 275 if ie_run_prog(A, 0, a, b) == ie_run_prog(B, 0, a, b) { agree = agree + 1 } 276 i = i + 1 277 } 278 return agree 279} 280// faithfulness over held-out: sim(T) must equal the interpreter on every held-out point. 281func ie_hw_faithful(T: *i64) -> i64 { 282 var ok: i64 = 0; var i: i64 = 0 283 while i < NHELD { 284 let a: i64 = ie_ha(i); let b: i64 = ie_hb(i) 285 if ie_run_prog(T, 0, a, b) == ie_eval(T, 0, a, b) { ok = ok + 1 } 286 i = i + 1 287 } 288 return ok 289} 290 291// one seed: compose T, derive G, then PROVE on the hardware sim(T)==sim(G) over held-out. 292func ie_seed(seed: i64) -> i64 { 293 let state: *i64 = sys_mmap(8) as *i64; state[0] = seed * EVO_MAGIC_2654435761 + EVO_MAGIC_12345 294 let T: *i64 = sys_mmap(GLEN * 8) as *i64 295 let G: *i64 = sys_mmap(GLEN * 8) as *i64 296 if ie_compose(state, T) != 1 { ie_p("seed=" as *u8); ie_pn(seed); ie_p(" COMPOSE-FAIL\n" as *u8); return 0 } 297 let de: i64 = ie_derive(T, state, G) 298 // interpreter generalization (search saw only train; check it holds on held-out) 299 var imatch: i64 = 0; var i: i64 = 0 300 while i < NHELD { if ie_eval(G, 0, ie_ha(i), ie_hb(i)) == ie_eval(T, 0, ie_ha(i), ie_hb(i)) { imatch = imatch + 1 } i = i + 1 } 301 // THE PROOF: both run on god; verdict reads the hardware, not the interpreter. 302 let hf: i64 = ie_hw_faithful(T) 303 let hw: i64 = ie_hw_agree(T, G) 304 ie_p("seed=" as *u8); ie_pn(seed); ie_p(" derive_err=" as *u8); ie_pn(de) 305 ie_p(" interp_held=" as *u8); ie_pn(imatch); ie_p("/" as *u8); ie_pn(NHELD) 306 ie_p(" sim(T)==interp=" as *u8); ie_pn(hf); ie_p("/" as *u8); ie_pn(NHELD) 307 ie_p(" sim(T)==sim(G)=" as *u8); ie_pn(hw); ie_p("/" as *u8); ie_pn(NHELD) 308 if de == 0 { if imatch == NHELD { if hf == NHELD { if hw == NHELD { 309 ie_p(" GREEN\n" as *u8); return 1 310 }}}} 311 ie_p(" RED\n" as *u8); return 0 312} 313 314// CONTROL 2 (negative): perturb the derived G into G' that the INTERPRETER says differs from T 315// on some held-out point, then confirm the HARDWARE differential CATCHES it (sim(T) != sim(G') 316// somewhere). Proves the test discriminates -- a wrong program is NOT rubber-stamped GREEN. 317func ie_negctl(seed: i64) -> i64 { 318 let state: *i64 = sys_mmap(8) as *i64; state[0] = seed * EVO_MAGIC_2654435761 + 999 319 let T: *i64 = sys_mmap(GLEN * 8) as *i64 320 let G: *i64 = sys_mmap(GLEN * 8) as *i64 321 let Gp: *i64 = sys_mmap(GLEN * 8) as *i64 322 if ie_compose(state, T) != 1 { ie_p(" control-negative: COMPOSE-FAIL\n" as *u8); return 0 } 323 ie_derive(T, state, G) 324 // build G' = G with the last op swapped; pick a swap the interpreter says changes a held-out value. 325 var found_diff: i64 = 0 326 var cand: i64 = 0 327 while cand < 6 { 328 var c: i64 = 0; while c < GLEN { Gp[c] = G[c]; c = c + 1 } 329 Gp[(NINSTR-1)*3] = cand 330 var differs: i64 = 0; var i: i64 = 0 331 while i < NHELD { if ie_eval(Gp, 0, ie_ha(i), ie_hb(i)) != ie_eval(T, 0, ie_ha(i), ie_hb(i)) { differs = 1 } i = i + 1 } 332 if differs == 1 { found_diff = 1; cand = 6 } else { cand = cand + 1 } 333 } 334 if found_diff == 0 { ie_p(" control-negative: no distinguishing perturbation (inconclusive)\n" as *u8); return 0 } 335 let agree: i64 = ie_hw_agree(T, Gp) 336 ie_p(" control-negative: sim(T)==sim(G_wrong)=" as *u8); ie_pn(agree); ie_p("/" as *u8); ie_pn(NHELD) 337 if agree < NHELD { ie_p(" -> differential CAUGHT the wrong program (good)\n" as *u8); return 1 } 338 ie_p(" -> differential MISSED it (test broken)\n" as *u8); return 0 339} 340 341func main() -> i64 { 342 ie_p("ISAEQUIVSOV: differential-replacement test ON THE HARDWARE (compose T -> derive G -> run both on god)\n" as *u8) 343 let cf: i64 = ie_faithful() 344 var ok: i64 = 0 345 if ie_seed(101) == 1 { ok = ok + 1 } 346 if ie_seed(202) == 1 { ok = ok + 1 } 347 if ie_seed(303) == 1 { ok = ok + 1 } 348 if ie_seed(404) == 1 { ok = ok + 1 } 349 let nc: i64 = ie_negctl(101) 350 ie_p("ISAEQUIVSOV: " as *u8); ie_pn(ok); ie_p("/4 seeds: team-composed target == team-derived program, PROVEN on rv64im_min_sim over held-out\n" as *u8) 351 if cf == 1 { if ok == 4 { if nc == 1 { 352 ie_p("ISAEQUIVSOV GREEN: faithful-encode control PASS + negative control CAUGHT a wrong program + 4/4 hardware-verified equivalences\n" as *u8) 353 sys_exit(0); return 0 354 }}} 355 ie_p("ISAEQUIVSOV RED\n" as *u8) 356 sys_exit(1) 357 return 1 358}