nx_isa_synth_sov.nx source

1// nx_isa_synth_sov.nx -- SHAPE-DISCOVERY SYNTHESIS: the team is given only (a,b)->T(a,b) examples 2// and must DISCOVER the control-flow CLASS that fits -- straight-line, conditional, or loop -- AND 3// the computation, then prove it on god. Removes the last crutch of the trilogy (shape was TOLD). 4// 5// One UNIFIED program space (gene[0]=shape in {0 straight, 1 conditional, 2 loop}; gene[1..7]=payload): 6// shape 0 STRAIGHT: res = op2( op1(reg,reg), reg ) over {0,a,b} 7// shape 1 COND: if cmp(a,b) then op(reg,reg) else op(reg,reg) over {0,a,b} 8// shape 2 LOOP: acc=0; i=a; while i>0 { acc += op2(op1(reg,reg),reg); i-- } over {0,i,a,b} 9// All three terminate, so the search never hangs. The GA searches shape AND payload together, so it 10// DISCOVERS the structure. Emit dispatches to the matching RV64 skeleton (each path already verified 11// in nx_isa_equiv/cf/loop_sov); run BOTH T and G on rv64im_min_sim over 12 HELD-OUT; verify 12// sim(T)==sim(G). When the derived SHAPE != the target shape but sim==sim, that is structural 13// divergence with behavioral equivalence -- reported. Controls: FAITHFUL (one known program of EACH 14// shape on god == known answer) + NEGATIVE (a perturbed G the differential must catch). license_tier: ORIGINAL 15import "nx_syscalls.nx" 16import "nishi_hdl_primitives.nx" 17import "rv64im_min_decoder.nx" 18import "rv64im_min_alu.nx" 19import "rv64im_min_regfile.nx" 20import "rv64im_min_csr.nx" 21import "rv64im_min_clint.nx" 22import "rv64im_min_uart.nx" 23import "rv64im_min_sim.nx" 24const EVO_MAGIC_2862933555777941757: i64 = 2862933555777941757 25const EVO_MAGIC_3037000493: i64 = 3037000493 26const EVO_MAGIC_1000000000000: i64 = 1000000000000 27const EVO_MAGIC_10000000000000: i64 = 10000000000000 28const EVO_MAGIC_1000000000: i64 = 1000000000 29const EVO_MAGIC_2654435761: i64 = 2654435761 30const EVO_MAGIC_12345: i64 = 12345 31 32const GLEN: i64 = 8 // [shape, p1..p7] 33const EVO_P: i64 = 400 34const EVO_G: i64 = 1500 35const EVO_T: i64 = 5 36const NTRAIN: i64 = 8 37const NHELD: i64 = 12 38 39const IR_MEM_BASE: i64 = 0x80000000 40const IR_MEM_SIZE: i64 = 8192 41const IR_TX_CAP: i64 = 256 42const RES_OFF: i64 = 0x700 43 44func su_rand(s: *i64) -> i64 { s[0] = s[0] * EVO_MAGIC_2862933555777941757 + EVO_MAGIC_3037000493; return (s[0] >> 17) & 0x3fffffff } 45func su_abs(x: i64) -> i64 { if x < 0 { return 0 - x } return x } 46 47func su_ta(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} if i==5 {return 3} if i==6 {return 8} return 2 } 48func su_tb(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} if i==5 {return 6} if i==6 {return 5} return 8 } 49func su_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 } 50func su_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 } 51 52// ---- interpreter (reference) ----------------------------------------------------------- 53func su_aluop(op: i64, x: i64, y: i64) -> i64 { 54 if (op % 3) == 0 { return x + y } 55 if (op % 3) == 1 { return x - y } 56 return x * y 57} 58func su_reg(idx: i64, a: i64, b: i64) -> i64 { // straight/cond reg: 0->0 1->a 2->b 3->a 59 if idx == 0 { return 0 } 60 if idx == 1 { return a } 61 if idx == 2 { return b } 62 return a 63} 64func su_regl(idx: i64, i: i64, a: i64, b: i64) -> i64 { // loop reg: 0->0 1->i 2->a 3->b 65 if idx == 0 { return 0 } 66 if idx == 1 { return i } 67 if idx == 2 { return a } 68 return b 69} 70func su_cmp(c: i64, a: i64, b: i64) -> i64 { 71 if c == 0 { if a < b { return 1 } return 0 } 72 if c == 1 { if a >= b { return 1 } return 0 } 73 if c == 2 { if a == b { return 1 } return 0 } 74 if a != b { return 1 } return 0 75} 76func su_eval_at(g: *i64, base: i64, a: i64, b: i64) -> i64 { 77 let shape: i64 = g[base] 78 let p1: i64 = g[base+1]; let p2: i64 = g[base+2]; let p3: i64 = g[base+3]; let p4: i64 = g[base+4] 79 let p5: i64 = g[base+5]; let p6: i64 = g[base+6]; let p7: i64 = g[base+7] 80 if shape == 0 { 81 let t: i64 = su_aluop(p1, su_reg(p2, a, b), su_reg(p3, a, b)) 82 return su_aluop(p4, t, su_reg(p5, a, b)) 83 } 84 if shape == 1 { 85 if su_cmp(p1, a, b) == 1 { return su_aluop(p2, su_reg(p3, a, b), su_reg(p4, a, b)) } 86 return su_aluop(p5, su_reg(p6, a, b), su_reg(p7, a, b)) 87 } 88 var acc: i64 = 0; var i: i64 = a 89 while i > 0 { 90 let t: i64 = su_aluop(p1, su_regl(p2, i, a, b), su_regl(p3, i, a, b)) 91 acc = acc + su_aluop(p4, t, su_regl(p5, i, a, b)) 92 i = i - 1 93 } 94 return acc 95} 96func su_eval(g: *i64, a: i64, b: i64) -> i64 { return su_eval_at(g, 0, a, b) } 97 98// ---- RV64 encoders (all verified in the trilogy) ---- 99func rv_addi(rd: i64, rs1: i64, imm: i64) -> i64 { return ((imm & 0xFFF) << 20) | (rs1 << 15) | (rd << 7) | 0x13 } 100func rv_lui(rd: i64, imm20: i64) -> i64 { return ((imm20 & 0xFFFFF) << 12) | (rd << 7) | 0x37 } 101func 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 } 102func rv_store_imm(rs2: i64, rs1: i64, f3: i64, imm: i64) -> i64 { return (((imm >> 5) & 0x7f) << 25) | (rs2 << 20) | (rs1 << 15) | (f3 << 12) | ((imm & 0x1f) << 7) | 0x23 } 103func rv_branch(f3: i64, rs1: i64, rs2: i64, imm: i64) -> i64 { return (((imm >> 12) & 1) << 31) | (((imm >> 5) & 0x3f) << 25) | (rs2 << 20) | (rs1 << 15) | (f3 << 12) | (((imm >> 1) & 0xf) << 8) | (((imm >> 11) & 1) << 7) | 0x63 } 104func rv_jal(rd: i64, imm: i64) -> i64 { return (((imm >> 20) & 1) << 31) | (((imm >> 1) & 0x3ff) << 21) | (((imm >> 11) & 1) << 20) | (((imm >> 12) & 0xff) << 12) | (rd << 7) | 0x6f } 105func su_f7(op: i64) -> i64 { if (op % 3) == 1 { return 0x20 } if (op % 3) == 2 { return 0x01 } return 0x00 } 106func su_bf3(c: i64) -> i64 { if c == 0 { return 4 } if c == 1 { return 5 } if c == 2 { return 0 } return 1 } 107func su_regx(idx: i64) -> i64 { if idx == 0 { return 0 } if idx == 1 { return 1 } if idx == 2 { return 2 } return 1 } // straight/cond: a=x1 b=x2 108func su_regxl(idx: i64) -> i64 { if idx == 0 { return 0 } if idx == 1 { return 4 } if idx == 2 { return 1 } return 2 } // loop: i=x4 a=x1 b=x2 109func rv_w32(buf: *u8, off: i64, w: i64) -> i64 { 110 buf[off] = (w & 0xff) as u8 111 buf[off+1] = ((w >> 8) & 0xff) as u8 112 buf[off+2] = ((w >> 16) & 0xff) as u8 113 buf[off+3] = ((w >> 24) & 0xff) as u8 114 return off + 4 115} 116// tail: sd x3,RES_OFF(x5) at `o`, then finisher halt. returns nothing. 117func su_emit_tail(mem: *u8, o: i64) -> i64 { 118 var p: i64 = o 119 p = rv_w32(mem, p, rv_store_imm(3, 5, 3, RES_OFF)) 120 p = rv_w32(mem, p, rv_lui(7, 0x100)) 121 p = rv_w32(mem, p, rv_lui(6, 0x5)) 122 p = rv_w32(mem, p, rv_addi(6, 6, 0x555)) 123 p = rv_w32(mem, p, rv_store_imm(6, 7, 2, 0)) 124 p = rv_w32(mem, p, 0x6F) 125 return 0 126} 127func su_emit(mem: *u8, g: *i64, a: i64, b: i64) -> i64 { 128 let shape: i64 = g[0] 129 let p1: i64 = g[1]; let p2: i64 = g[2]; let p3: i64 = g[3]; let p4: i64 = g[4] 130 let p5: i64 = g[5]; let p6: i64 = g[6]; let p7: i64 = g[7] 131 rv_w32(mem, 0, rv_addi(1, 0, a)) 132 rv_w32(mem, 4, rv_addi(2, 0, b)) 133 rv_w32(mem, 8, rv_lui(5, 0x80000)) 134 if shape == 0 { 135 rv_w32(mem, 12, rv_rtype(su_f7(p1), su_regx(p3), su_regx(p2), 0, 6)) // x6 = op1(reg p2, reg p3) 136 rv_w32(mem, 16, rv_rtype(su_f7(p4), su_regx(p5), 6, 0, 3)) // x3 = op2(x6, reg p5) 137 su_emit_tail(mem, 20) 138 return 0 139 } 140 if shape == 1 { 141 rv_w32(mem, 12, rv_branch(su_bf3(p1), 1, 2, 12)) // B<cmp> x1,x2,+12 -> THEN(24) 142 rv_w32(mem, 16, rv_rtype(su_f7(p5), su_regx(p7), su_regx(p6), 0, 3)) // ELSE: x3 = op(reg p6,reg p7) 143 rv_w32(mem, 20, rv_jal(0, 8)) // -> 28 (store) 144 rv_w32(mem, 24, rv_rtype(su_f7(p2), su_regx(p4), su_regx(p3), 0, 3)) // THEN: x3 = op(reg p3,reg p4) 145 su_emit_tail(mem, 28) 146 return 0 147 } 148 rv_w32(mem, 12, rv_addi(3, 0, 0)) // acc=0 149 rv_w32(mem, 16, rv_addi(4, 1, 0)) // i=a 150 rv_w32(mem, 20, rv_branch(0, 4, 0, 24)) // beq x4,x0,+24 -> EXIT(44) 151 rv_w32(mem, 24, rv_rtype(su_f7(p1), su_regxl(p3), su_regxl(p2), 0, 6)) // x6 = op1(reg p2,reg p3) 152 rv_w32(mem, 28, rv_rtype(su_f7(p4), su_regxl(p5), 6, 0, 6)) // x6 = op2(x6, reg p5) 153 rv_w32(mem, 32, rv_rtype(0x00, 6, 3, 0, 3)) // x3 += x6 154 rv_w32(mem, 36, rv_addi(4, 4, 0 - 1)) // i-- 155 rv_w32(mem, 40, rv_jal(0, 0 - 20)) // -> LOOP_TOP(20) 156 su_emit_tail(mem, 44) 157 return 0 158} 159func su_read_i64(mem: *u8, off: i64) -> i64 { 160 var v: i64 = 0; var i: i64 = 0 161 while i < 8 { v = v | ((mem[off + i] as i64) << (i * 8)); i = i + 1 } 162 return v 163} 164func su_run_prog(g: *i64, a: i64, b: i64) -> i64 { 165 let rf_storage: *i64 = (sys_mmap(8 * NX_RV64IM_RF_N_REGS)) as *i64 166 let csr_storage: *i64 = (sys_mmap(8 * NX_CSR_SLOT_N)) as *i64 167 let clint_storage: *i64 = (sys_mmap(8 * NX_CLINT_SLOT_N)) as *i64 168 let uart_storage: *i64 = (sys_mmap(8 * NX_UART_SLOT_N)) as *i64 169 let mem: *u8 = sys_mmap(IR_MEM_SIZE) 170 let tx_buf: *u8 = sys_mmap(IR_TX_CAP) 171 let rf: *NxRv64imRegfile = (sys_mmap(64)) as *NxRv64imRegfile 172 let csr: *NxRv64imCsrFile = (sys_mmap(64)) as *NxRv64imCsrFile 173 let clint: *NxClint = (sys_mmap(64)) as *NxClint 174 let uart: *NxUart = (sys_mmap(64)) as *NxUart 175 let sim: *NxRv64imSim = (sys_mmap(128)) as *NxRv64imSim 176 nx_rv64im_rf_init(rf, rf_storage) 177 nx_rv64im_csr_init(csr, csr_storage, 0) 178 nx_clint_init(clint, clint_storage) 179 nx_uart_init(uart, uart_storage, tx_buf, IR_TX_CAP) 180 nx_rv64im_sim_init(sim, rf, csr, clint, uart, IR_MEM_BASE, mem, IR_MEM_SIZE, 0) 181 su_emit(mem, g, a, b) 182 nx_rv64im_sim_run(sim, 600) 183 return su_read_i64(mem, RES_OFF) 184} 185 186// ---- compose / derive ------------------------------------------------------------------ 187func su_randslot(idx: i64, state: *i64) -> i64 { if idx == 0 { return su_rand(state) % 3 } return su_rand(state) % 4 } 188func su_fill(g: *i64, base: i64, state: *i64) -> i64 { var i: i64 = 0; while i < GLEN { g[base + i] = su_randslot(i, state); i = i + 1 } return 0 } 189// non-trivial: non-constant over train AND not all-zero; conditional must exercise BOTH branches. 190func su_nontrivial(T: *i64) -> i64 { 191 let y0: i64 = su_eval(T, su_ta(0), su_tb(0)) 192 var nonconst: i64 = 0; var nonzero: i64 = 0; var took: i64 = 0; var fell: i64 = 0; var i: i64 = 0 193 while i < NTRAIN { 194 let a: i64 = su_ta(i); let b: i64 = su_tb(i) 195 let v: i64 = su_eval(T, a, b) 196 if v != y0 { nonconst = 1 } 197 if v != 0 { nonzero = 1 } 198 if T[0] == 1 { if su_cmp(T[1], a, b) == 1 { took = 1 } else { fell = 1 } } 199 i = i + 1 200 } 201 if nonconst == 0 { return 0 } 202 if nonzero == 0 { return 0 } 203 if T[0] == 1 { if took == 0 { return 0 } if fell == 0 { return 0 } } 204 return 1 205} 206func su_compose(state: *i64, T: *i64) -> i64 { 207 var tries: i64 = 0 208 while tries < 800 { su_fill(T, 0, state); if su_nontrivial(T) == 1 { return 1 } tries = tries + 1 } 209 return 0 210} 211func su_fit(pop: *i64, base: i64, T: *i64) -> i64 { 212 var err: i64 = 0; var i: i64 = 0 213 while i < NTRAIN { 214 let a: i64 = su_ta(i); let b: i64 = su_tb(i) 215 let r: i64 = su_eval_at(pop, base, a, b) 216 let y: i64 = su_eval(T, a, b) 217 var d: i64 = su_abs(r - y) 218 if r > EVO_MAGIC_1000000000000 { d = EVO_MAGIC_10000000000000 } 219 if r < (0 - EVO_MAGIC_1000000000000) { d = EVO_MAGIC_10000000000000 } 220 err = err + d; i = i + 1 221 } 222 return err 223} 224func su_tourney(fit: *i64, state: *i64) -> i64 { 225 var bi: i64 = su_rand(state) % EVO_P; var bd: i64 = fit[bi]; var k: i64 = 1 226 while k < EVO_T { let i: i64 = su_rand(state) % EVO_P; if fit[i] < bd { bd = fit[i]; bi = i } k = k + 1 } 227 return bi 228} 229func su_mut(g: *i64, base: i64, state: *i64) -> i64 { let idx: i64 = su_rand(state) % GLEN; g[base + idx] = su_randslot(idx, state); return 0 } 230func su_derive(T: *i64, state: *i64, G: *i64) -> i64 { 231 let pop: *i64 = sys_mmap(EVO_P * GLEN * 8) as *i64 232 let nxt: *i64 = sys_mmap(EVO_P * GLEN * 8) as *i64 233 let fit: *i64 = sys_mmap(EVO_P * 8) as *i64 234 var p: i64 = 0 235 while p < EVO_P { su_fill(pop, p*GLEN, state); p = p + 1 } 236 var best_err: i64 = EVO_MAGIC_1000000000 237 var g: i64 = 0 238 while g < EVO_G { 239 var gbest: i64 = EVO_MAGIC_1000000000; var gbp: i64 = 0 240 p = 0 241 while p < EVO_P { let e: i64 = su_fit(pop, p*GLEN, T); fit[p] = e; if e < gbest { gbest = e; gbp = p } p = p + 1 } 242 if gbest < best_err { best_err = gbest; var j: i64 = 0; while j < GLEN { G[j] = pop[gbp*GLEN + j]; j = j + 1 } } 243 if best_err == 0 { g = EVO_G } else { 244 var j2: i64 = 0; while j2 < GLEN { nxt[j2] = G[j2]; j2 = j2 + 1 } 245 p = 1 246 while p < EVO_P { 247 let pa: i64 = su_tourney(fit, state) * GLEN 248 let pb: i64 = su_tourney(fit, state) * GLEN 249 let cut: i64 = (su_rand(state) % (GLEN - 1)) + 1 250 var jj: i64 = 0 251 while jj < GLEN { if jj < cut { nxt[p*GLEN + jj] = pop[pa + jj] } else { nxt[p*GLEN + jj] = pop[pb + jj] } jj = jj + 1 } 252 su_mut(nxt, p*GLEN, state) 253 p = p + 1 254 } 255 var c: i64 = 0; while c < EVO_P * GLEN { pop[c] = nxt[c]; c = c + 1 } 256 g = g + 1 257 } 258 } 259 return best_err 260} 261 262// ---- print ----------------------------------------------------------------------------- 263func su_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 264func su_pn(v: i64) -> i64 { 265 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 } 266 var neg: i64 = 0; var m: i64 = v 267 if m < 0 { neg = 1; m = 0 - m } 268 var k: i64 = 0; let t: *u8 = sys_mmap(32) 269 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 270 if neg == 1 { sys_write(1, "-" as *u8, 1) } 271 while k > 0 { k = k - 1; sys_write(1, (((t as i64)+k) as *u8), 1) } 272 return 0 273} 274func su_shape(s: i64) -> i64 { if s == 0 { su_p("straight") } else { if s == 1 { su_p("cond") } else { su_p("loop") } } return 0 } 275 276// CONTROL 1 (faithful): one KNOWN program of EACH shape, run on god, must match -- proves all three 277// emit paths in the unified organ. straight a+b ; cond max(a,b) ; loop a*a. 278func su_set8(g: *i64, s: i64, p1: i64,p2: i64,p3: i64,p4: i64,p5: i64,p6: i64,p7: i64) -> i64 { 279 g[0]=s; g[1]=p1; g[2]=p2; g[3]=p3; g[4]=p4; g[5]=p5; g[6]=p6; g[7]=p7; return 0 280} 281func su_faithful() -> i64 { 282 let g: *i64 = sys_mmap(GLEN * 8) as *i64 283 var ok: i64 = 0; var tot: i64 = 0; var i: i64 = 0 284 su_set8(g, 0, 0,1,2, 0,0, 0,0) // straight: (a+b)+0 = a+b 285 i = 0; while i < NHELD { let a: i64 = su_ha(i); let b: i64 = su_hb(i); if su_run_prog(g, a, b) == a + b { ok = ok + 1 } tot = tot + 1; i = i + 1 } 286 su_set8(g, 1, 1, 0,1,0, 0,2,0) // cond: if a>=b then ADD(a,0)=a else ADD(b,0)=b = max 287 i = 0; while i < NHELD { let a: i64 = su_ha(i); let b: i64 = su_hb(i); var e: i64 = b; if a >= b { e = a } if su_run_prog(g, a, b) == e { ok = ok + 1 } tot = tot + 1; i = i + 1 } 288 su_set8(g, 2, 0,2,0, 0,0, 0,0) // loop: body ADD(a,0)=a -> sum = a*a 289 i = 0; while i < NHELD { let a: i64 = su_ha(i); let b: i64 = su_hb(i); if su_run_prog(g, a, b) == a*a { ok = ok + 1 } tot = tot + 1; i = i + 1 } 290 su_p(" control-faithful: "); su_pn(ok); su_p("/"); su_pn(tot); su_p(" known programs of each shape (straight a+b, cond max, loop a*a) run on god == answer\n") 291 if ok == tot { return 1 } 292 return 0 293} 294func su_hw_agree(A: *i64, B: *i64) -> i64 { 295 var agree: i64 = 0; var i: i64 = 0 296 while i < NHELD { if su_run_prog(A, su_ha(i), su_hb(i)) == su_run_prog(B, su_ha(i), su_hb(i)) { agree = agree + 1 } i = i + 1 } 297 return agree 298} 299func su_hw_faithful(T: *i64) -> i64 { 300 var ok: i64 = 0; var i: i64 = 0 301 while i < NHELD { if su_run_prog(T, su_ha(i), su_hb(i)) == su_eval(T, su_ha(i), su_hb(i)) { ok = ok + 1 } i = i + 1 } 302 return ok 303} 304func su_seed(seed: i64) -> i64 { 305 let state: *i64 = sys_mmap(8) as *i64; state[0] = seed * EVO_MAGIC_2654435761 + EVO_MAGIC_12345 306 let T: *i64 = sys_mmap(GLEN * 8) as *i64 307 let G: *i64 = sys_mmap(GLEN * 8) as *i64 308 if su_compose(state, T) != 1 { su_p("seed="); su_pn(seed); su_p(" COMPOSE-FAIL\n"); return 0 } 309 let de: i64 = su_derive(T, state, G) 310 var imatch: i64 = 0; var i: i64 = 0 311 while i < NHELD { if su_eval_at(G, 0, su_ha(i), su_hb(i)) == su_eval(T, su_ha(i), su_hb(i)) { imatch = imatch + 1 } i = i + 1 } 312 let hf: i64 = su_hw_faithful(T) 313 let hw: i64 = su_hw_agree(T, G) 314 su_p("seed="); su_pn(seed); su_p(" target="); su_shape(T[0]); su_p(" derived="); su_shape(G[0]) 315 su_p(" derive_err="); su_pn(de); su_p(" interp_held="); su_pn(imatch); su_p("/"); su_pn(NHELD) 316 su_p(" sim(T)==interp="); su_pn(hf); su_p("/"); su_pn(NHELD) 317 su_p(" sim(T)==sim(G)="); su_pn(hw); su_p("/"); su_pn(NHELD) 318 if T[0] != G[0] { su_p(" [DIFF-SHAPE, equivalent]") } 319 if de == 0 { if imatch == NHELD { if hf == NHELD { if hw == NHELD { 320 su_p(" GREEN\n"); return 1 321 }}}} 322 su_p(" RED\n"); return 0 323} 324// CONTROL 2 (negative): perturb the derived G's shape gene so the INTERPRETER differs from T on some 325// held-out point; confirm the HARDWARE differential CATCHES it. 326func su_negctl(seed: i64) -> i64 { 327 let state: *i64 = sys_mmap(8) as *i64; state[0] = seed * EVO_MAGIC_2654435761 + 777 328 let T: *i64 = sys_mmap(GLEN * 8) as *i64 329 let G: *i64 = sys_mmap(GLEN * 8) as *i64 330 let Gp: *i64 = sys_mmap(GLEN * 8) as *i64 331 if su_compose(state, T) != 1 { su_p(" control-negative: COMPOSE-FAIL\n"); return 0 } 332 su_derive(T, state, G) 333 var found: i64 = 0; var cand: i64 = 0 334 while cand < 3 { 335 var c: i64 = 0; while c < GLEN { Gp[c] = G[c]; c = c + 1 } 336 Gp[0] = cand 337 var differs: i64 = 0; var i: i64 = 0 338 while i < NHELD { if su_eval_at(Gp, 0, su_ha(i), su_hb(i)) != su_eval(T, su_ha(i), su_hb(i)) { differs = 1 } i = i + 1 } 339 if differs == 1 { found = 1; cand = 3 } else { cand = cand + 1 } 340 } 341 if found == 0 { su_p(" control-negative: no distinguishing shape (inconclusive)\n"); return 0 } 342 let agree: i64 = su_hw_agree(T, Gp) 343 su_p(" control-negative: sim(T)==sim(G_wrongshape)="); su_pn(agree); su_p("/"); su_pn(NHELD) 344 if agree < NHELD { su_p(" -> differential CAUGHT the wrong shape (good)\n"); return 1 } 345 su_p(" -> differential MISSED it (test broken)\n"); return 0 346} 347 348func main() -> i64 { 349 su_p("ISASYNTHSOV: shape-discovery synthesis -- from I/O examples alone, DISCOVER the control-flow class + computation, prove on god\n") 350 let cfaith: i64 = su_faithful() 351 var ok: i64 = 0 352 if su_seed(101) == 1 { ok = ok + 1 } 353 if su_seed(202) == 1 { ok = ok + 1 } 354 if su_seed(303) == 1 { ok = ok + 1 } 355 if su_seed(404) == 1 { ok = ok + 1 } 356 if su_seed(505) == 1 { ok = ok + 1 } 357 if su_seed(606) == 1 { ok = ok + 1 } 358 let nc: i64 = su_negctl(303) 359 su_p("ISASYNTHSOV: "); su_pn(ok); su_p("/6 seeds: shape DISCOVERED from examples + team-derived == team-composed, PROVEN on rv64im_min_sim\n") 360 if cfaith == 1 { if ok == 6 { if nc == 1 { 361 su_p("ISASYNTHSOV GREEN: faithful per-shape control PASS + negative control CAUGHT a wrong shape + 6/6 hardware-verified equivalences with shape discovered (not told)\n") 362 sys_exit(0); return 0 363 }}} 364 su_p("ISASYNTHSOV RED\n") 365 sys_exit(1) 366 return 1 367}