nx_isa_loop_sov.nx source

1// nx_isa_loop_sov.nx -- LOOP rung: derive ITERATIVE programs with a BACKWARD branch, run on god. 2// 3// The forward-branch rung (nx_isa_cf_sov) exercised a data-dependent path; this exercises a real 4// LOOP -- a backward JAL (negative, sign-extended imm_j) around a decrementing counter (guaranteed 5// termination). The new hardware path proven: the sim's negative branch/jump immediate. 6// 7// target/derived shape: acc = 0; i = a; while i > 0 { acc = acc + BODY(i,a,b); i = i - 1 } 8// BODY = op2( op1(reg,reg), reg ) over registers {0, i, a, b}, op in {ADD,SUB,MUL}. 9// 10// (1) team COMPOSES a random non-trivial such loop T (non-constant over train, not all-zero), 11// (2) team DERIVES a same-shape G by GA on T's TRAIN examples, 12// (3) ENCODE both to a real RV64 loop (beq exit + backward jal) + run BOTH on rv64im_min_sim 13// over 12 HELD-OUT inputs + verify sim(T)==sim(G). 14// 15// Termination is structural (counter i = a <= 13 decrements to 0), so every candidate halts; the 16// search never hangs. Controls: FAITHFUL (loops with KNOWN closed forms a*a, a(a+1)/2, 17// b*a(a+1)/2 -- correct only if the loop truly iterates a times on the hardware) + NEGATIVE 18// (a perturbed body the differential must catch). license_tier: ORIGINAL 19import "nx_syscalls.nx" 20import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc) 21import "nishi_hdl_primitives.nx" 22import "rv64im_min_decoder.nx" 23import "rv64im_min_alu.nx" 24import "rv64im_min_regfile.nx" 25import "rv64im_min_csr.nx" 26import "rv64im_min_clint.nx" 27import "rv64im_min_uart.nx" 28import "rv64im_min_sim.nx" 29const EVO_MAGIC_2862933555777941757: i64 = 2862933555777941757 30const EVO_MAGIC_3037000493: i64 = 3037000493 31const EVO_MAGIC_1000000000000: i64 = 1000000000000 32const EVO_MAGIC_10000000000000: i64 = 10000000000000 33const EVO_MAGIC_1000000000: i64 = 1000000000 34const EVO_MAGIC_2654435761: i64 = 2654435761 35const EVO_MAGIC_12345: i64 = 12345 36 37const GLEN: i64 = 5 // [op1, r1, r2, op2, r3] (BODY = op2(op1(reg r1,reg r2), reg r3)) 38const EVO_P: i64 = 256 39const EVO_G: i64 = 800 40const EVO_T: i64 = 5 41const NTRAIN: i64 = 8 42const NHELD: i64 = 12 43 44const IR_MEM_BASE: i64 = 0x80000000 45const IR_MEM_SIZE: i64 = 8192 46const IR_TX_CAP: i64 = 256 47const RES_OFF: i64 = 0x700 48 49func lp_rand(s: *i64) -> i64 { s[0] = s[0] * EVO_MAGIC_2862933555777941757 + EVO_MAGIC_3037000493; return (s[0] >> 17) & 0x3fffffff } 50func lp_abs(x: i64) -> i64 { if x < 0 { return 0 - x } return x } 51 52func lp_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 } 53func lp_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 } 54func lp_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 } 55func lp_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 } 56 57// ---- interpreter (reference: guides search + faithfulness control; NOT the verdict) ---- 58func lp_aluop(op: i64, x: i64, y: i64) -> i64 { 59 if op == 0 { return x + y } 60 if op == 1 { return x - y } 61 return x * y 62} 63func lp_reg(idx: i64, i: i64, a: i64, b: i64) -> i64 { 64 if idx == 0 { return 0 } 65 if idx == 1 { return i } 66 if idx == 2 { return a } 67 return b 68} 69func lp_body(gen: *i64, base: i64, i: i64, a: i64, b: i64) -> i64 { 70 let t: i64 = lp_aluop(gen[base], lp_reg(gen[base+1], i, a, b), lp_reg(gen[base+2], i, a, b)) 71 return lp_aluop(gen[base+3], t, lp_reg(gen[base+4], i, a, b)) 72} 73func lp_eval_at(gen: *i64, base: i64, a: i64, b: i64) -> i64 { 74 var acc: i64 = 0 75 var i: i64 = a 76 while i > 0 { acc = acc + lp_body(gen, base, i, a, b); i = i - 1 } 77 return acc 78} 79func lp_eval(gen: *i64, a: i64, b: i64) -> i64 { return lp_eval_at(gen, 0, a, b) } 80 81// ---- RV64 encoders (rv_branch/rv_jal round-trip imm_b/imm_j incl. NEGATIVE imm) ---- 82func rv_addi(rd: i64, rs1: i64, imm: i64) -> i64 { return ((imm & 0xFFF) << 20) | (rs1 << 15) | (rd << 7) | 0x13 } 83func rv_lui(rd: i64, imm20: i64) -> i64 { return ((imm20 & 0xFFFFF) << 12) | (rd << 7) | 0x37 } 84func 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 } 85func 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 } 86func rv_branch(f3: i64, rs1: i64, rs2: i64, imm: i64) -> i64 { 87 return (((imm >> 12) & 1) << 31) | (((imm >> 5) & 0x3f) << 25) | (rs2 << 20) | (rs1 << 15) | (f3 << 12) | (((imm >> 1) & 0xf) << 8) | (((imm >> 11) & 1) << 7) | 0x63 88} 89func rv_jal(rd: i64, imm: i64) -> i64 { 90 return (((imm >> 20) & 1) << 31) | (((imm >> 1) & 0x3ff) << 21) | (((imm >> 11) & 1) << 20) | (((imm >> 12) & 0xff) << 12) | (rd << 7) | 0x6f 91} 92func lp_f7(op: i64) -> i64 { if op == 1 { return 0x20 } if op == 2 { return 0x01 } return 0x00 } 93// genome reg index -> actual x-register: 0->x0(0), 1->x4(i), 2->x1(a), 3->x2(b). 94func lp_regx(idx: i64) -> i64 { if idx == 0 { return 0 } if idx == 1 { return 4 } if idx == 2 { return 1 } return 2 } 95func rv_w32(buf: *u8, off: i64, w: i64) -> i64 { 96 buf[off] = (w & 0xff) as u8 97 buf[off+1] = ((w >> 8) & 0xff) as u8 98 buf[off+2] = ((w >> 16) & 0xff) as u8 99 buf[off+3] = ((w >> 24) & 0xff) as u8 100 return off + 4 101} 102// emit the full loop program. x1=a x2=b x3=acc x4=i x5=RAMbase x6=body-temp x7=finisher. 103// 0 addi x1,a 4 addi x2,b 8 lui x5 12 addi x3,0 16 addi x4,x1,0 (i=a) 104// 20 beq x4,x0,+24 -> EXIT(44) (LOOP_TOP=20) 105// 24 x6=op1(reg r1,reg r2) 28 x6=op2(x6,reg r3) 32 add x3,x3,x6 36 addi x4,x4,-1 106// 40 jal x0,-20 -> 20 (BACKWARD) 107// 44 sd x3,RES_OFF(x5) 48 lui x7,0x100 52 lui x6,0x5 56 addi x6,0x555 60 sw x6,0(x7) 64 jal 0 108func lp_emit(mem: *u8, gen: *i64, a: i64, b: i64) -> i64 { 109 rv_w32(mem, 0, rv_addi(1, 0, a)) 110 rv_w32(mem, 4, rv_addi(2, 0, b)) 111 rv_w32(mem, 8, rv_lui(5, 0x80000)) 112 rv_w32(mem, 12, rv_addi(3, 0, 0)) 113 rv_w32(mem, 16, rv_addi(4, 1, 0)) // i = a 114 rv_w32(mem, 20, rv_branch(0, 4, 0, 24)) // beq x4,x0,+24 -> EXIT 115 rv_w32(mem, 24, rv_rtype(lp_f7(gen[0]), lp_regx(gen[2]), lp_regx(gen[1]), 0, 6)) // x6 = op1(...) 116 rv_w32(mem, 28, rv_rtype(lp_f7(gen[3]), lp_regx(gen[4]), 6, 0, 6)) // x6 = op2(x6, reg r3) 117 rv_w32(mem, 32, rv_rtype(0x00, 6, 3, 0, 3)) // x3 = x3 + x6 (acc += body) 118 rv_w32(mem, 36, rv_addi(4, 4, 0 - 1)) // i -= 1 119 rv_w32(mem, 40, rv_jal(0, 0 - 20)) // BACKWARD jal -> LOOP_TOP(20) 120 rv_w32(mem, 44, rv_store_imm(3, 5, 3, RES_OFF)) // sd x3, RES_OFF(x5) 121 rv_w32(mem, 48, rv_lui(7, 0x100)) 122 rv_w32(mem, 52, rv_lui(6, 0x5)) 123 rv_w32(mem, 56, rv_addi(6, 6, 0x555)) 124 rv_w32(mem, 60, rv_store_imm(6, 7, 2, 0)) // sw x6,0(x7) -> finisher halt 125 rv_w32(mem, 64, 0x6F) // jal x0,0 spin 126 return 0 127} 128func lp_read_i64(mem: *u8, off: i64) -> i64 { 129 var v: i64 = 0; var i: i64 = 0 130 while i < 8 { v = v | ((mem[off + i] as i64) << (i * 8)); i = i + 1 } 131 return v 132} 133// RUN a loop genome on the GENESIS SIM (fresh devices) -> its 64-bit result. 600 steps (<= 13 iters). 134func lp_run_prog(gen: *i64, a: i64, b: i64) -> i64 { 135 let rf_storage: *i64 = (sys_mmap(8 * NX_RV64IM_RF_N_REGS)) as *i64 136 let csr_storage: *i64 = (sys_mmap(8 * NX_CSR_SLOT_N)) as *i64 137 let clint_storage: *i64 = (sys_mmap(8 * NX_CLINT_SLOT_N)) as *i64 138 let uart_storage: *i64 = (sys_mmap(8 * NX_UART_SLOT_N)) as *i64 139 let mem: *u8 = sys_mmap(IR_MEM_SIZE) 140 let tx_buf: *u8 = sys_mmap(IR_TX_CAP) 141 let rf: *NxRv64imRegfile = (sys_mmap(64)) as *NxRv64imRegfile 142 let csr: *NxRv64imCsrFile = (sys_mmap(64)) as *NxRv64imCsrFile 143 let clint: *NxClint = (sys_mmap(64)) as *NxClint 144 let uart: *NxUart = (sys_mmap(64)) as *NxUart 145 let sim: *NxRv64imSim = (sys_mmap(128)) as *NxRv64imSim 146 nx_rv64im_rf_init(rf, rf_storage) 147 nx_rv64im_csr_init(csr, csr_storage, 0) 148 nx_clint_init(clint, clint_storage) 149 nx_uart_init(uart, uart_storage, tx_buf, IR_TX_CAP) 150 nx_rv64im_sim_init(sim, rf, csr, clint, uart, IR_MEM_BASE, mem, IR_MEM_SIZE, 0) 151 lp_emit(mem, gen, a, b) 152 nx_rv64im_sim_run(sim, 600) 153 return lp_read_i64(mem, RES_OFF) 154} 155 156// ---- compose / derive ------------------------------------------------------------------ 157func lp_randslot(idx: i64, state: *i64) -> i64 { 158 if idx == 0 { return lp_rand(state) % 3 } 159 if idx == 3 { return lp_rand(state) % 3 } 160 return lp_rand(state) % 4 161} 162func lp_fill(gen: *i64, base: i64, state: *i64) -> i64 { 163 var i: i64 = 0 164 while i < GLEN { gen[base + i] = lp_randslot(i, state); i = i + 1 } 165 return 0 166} 167// COMPOSE: non-constant over train AND not all-zero (so the loop's accumulation actually matters). 168func lp_compose(state: *i64, T: *i64) -> i64 { 169 var tries: i64 = 0 170 while tries < 600 { 171 lp_fill(T, 0, state) 172 let y0: i64 = lp_eval(T, lp_ta(0), lp_tb(0)) 173 var nonconst: i64 = 0; var nonzero: i64 = 0; var i: i64 = 0 174 while i < NTRAIN { 175 let v: i64 = lp_eval(T, lp_ta(i), lp_tb(i)) 176 if v != y0 { nonconst = 1 } 177 if v != 0 { nonzero = 1 } 178 i = i + 1 179 } 180 if nonconst == 1 { if nonzero == 1 { return 1 } } 181 tries = tries + 1 182 } 183 return 0 184} 185func lp_fit(pop: *i64, base: i64, T: *i64) -> i64 { 186 var err: i64 = 0; var i: i64 = 0 187 while i < NTRAIN { 188 let a: i64 = lp_ta(i); let b: i64 = lp_tb(i) 189 let r: i64 = lp_eval_at(pop, base, a, b) 190 let y: i64 = lp_eval(T, a, b) 191 var d: i64 = lp_abs(r - y) 192 if r > EVO_MAGIC_1000000000000 { d = EVO_MAGIC_10000000000000 } 193 if r < (0 - EVO_MAGIC_1000000000000) { d = EVO_MAGIC_10000000000000 } 194 err = err + d; i = i + 1 195 } 196 return err 197} 198func lp_tourney(fit: *i64, state: *i64) -> i64 { 199 var bi: i64 = lp_rand(state) % EVO_P; var bd: i64 = fit[bi]; var k: i64 = 1 200 while k < EVO_T { let i: i64 = lp_rand(state) % EVO_P; if fit[i] < bd { bd = fit[i]; bi = i } k = k + 1 } 201 return bi 202} 203func lp_mut(gen: *i64, base: i64, state: *i64) -> i64 { 204 let idx: i64 = lp_rand(state) % GLEN 205 gen[base + idx] = lp_randslot(idx, state) 206 return 0 207} 208func lp_derive(T: *i64, state: *i64, G: *i64) -> i64 { 209 let pop: *i64 = sys_mmap(EVO_P * GLEN * 8) as *i64 210 let nxt: *i64 = sys_mmap(EVO_P * GLEN * 8) as *i64 211 let fit: *i64 = sys_mmap(EVO_P * 8) as *i64 212 var p: i64 = 0 213 while p < EVO_P { lp_fill(pop, p*GLEN, state); p = p + 1 } 214 var best_err: i64 = EVO_MAGIC_1000000000 215 var g: i64 = 0 216 while g < EVO_G { 217 var gbest: i64 = EVO_MAGIC_1000000000; var gbp: i64 = 0 218 p = 0 219 while p < EVO_P { let e: i64 = lp_fit(pop, p*GLEN, T); fit[p] = e; if e < gbest { gbest = e; gbp = p } p = p + 1 } 220 if gbest < best_err { best_err = gbest; var j: i64 = 0; while j < GLEN { G[j] = pop[gbp*GLEN + j]; j = j + 1 } } 221 if best_err == 0 { g = EVO_G } else { 222 var j2: i64 = 0; while j2 < GLEN { nxt[j2] = G[j2]; j2 = j2 + 1 } 223 p = 1 224 while p < EVO_P { 225 let pa: i64 = lp_tourney(fit, state) * GLEN 226 let pb: i64 = lp_tourney(fit, state) * GLEN 227 let cut: i64 = (lp_rand(state) % (GLEN - 1)) + 1 228 var jj: i64 = 0 229 while jj < GLEN { if jj < cut { nxt[p*GLEN + jj] = pop[pa + jj] } else { nxt[p*GLEN + jj] = pop[pb + jj] } jj = jj + 1 } 230 lp_mut(nxt, p*GLEN, state) 231 p = p + 1 232 } 233 var c: i64 = 0; while c < EVO_P * GLEN { pop[c] = nxt[c]; c = c + 1 } 234 g = g + 1 235 } 236 } 237 return best_err 238} 239 240// ---- print ----------------------------------------------------------------------------- 241func lp_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 242// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer 243// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the 244// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls). 245// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign. 246func lp_pn(v: i64) -> i64 { nxi_out(v); return 0 } 247 248// CONTROL 1 (faithful): loops with KNOWN closed forms, run on god. Correct ONLY if the loop truly 249// iterates a times on the hardware (backward branch works). L1 body=a -> a*a ; L2 body=i -> 250// a(a+1)/2 ; L3 body=i*b -> b*a(a+1)/2. 251func lp_set(g: *i64, o1: i64, r1: i64, r2: i64, o2: i64, r3: i64) -> i64 { g[0]=o1; g[1]=r1; g[2]=r2; g[3]=o2; g[4]=r3; return 0 } 252func lp_faithful() -> i64 { 253 let g: *i64 = sys_mmap(GLEN * 8) as *i64 254 var ok: i64 = 0; var tot: i64 = 0 255 lp_set(g, 0, 2, 0, 0, 0) // body = ADD(a,0) then ADD(.,0) = a -> sum = a*a 256 var i: i64 = 0 257 while i < NHELD { let a: i64 = lp_ha(i); let b: i64 = lp_hb(i); if lp_run_prog(g, a, b) == a*a { ok = ok + 1 } tot = tot + 1; i = i + 1 } 258 lp_set(g, 0, 1, 0, 0, 0) // body = i -> sum = a(a+1)/2 259 i = 0 260 while i < NHELD { let a: i64 = lp_ha(i); let b: i64 = lp_hb(i); if lp_run_prog(g, a, b) == (a*(a+1))/2 { ok = ok + 1 } tot = tot + 1; i = i + 1 } 261 lp_set(g, 2, 1, 3, 0, 0) // body = MUL(i,b) then ADD(.,0) = i*b -> sum = b*a(a+1)/2 262 i = 0 263 while i < NHELD { let a: i64 = lp_ha(i); let b: i64 = lp_hb(i); if lp_run_prog(g, a, b) == (b*(a*(a+1)))/2 { ok = ok + 1 } tot = tot + 1; i = i + 1 } 264 lp_p(" control-faithful: "); lp_pn(ok); lp_p("/"); lp_pn(tot); lp_p(" hand-built LOOPS run on god == known closed form (a*a, a(a+1)/2, b*a(a+1)/2)\n") 265 if ok == tot { return 1 } 266 return 0 267} 268 269// HARDWARE differential: both genomes run on god over held-out; count where sim(A)==sim(B). 270func lp_hw_agree(A: *i64, B: *i64) -> i64 { 271 var agree: i64 = 0; var i: i64 = 0 272 while i < NHELD { if lp_run_prog(A, lp_ha(i), lp_hb(i)) == lp_run_prog(B, lp_ha(i), lp_hb(i)) { agree = agree + 1 } i = i + 1 } 273 return agree 274} 275func lp_hw_faithful(T: *i64) -> i64 { 276 var ok: i64 = 0; var i: i64 = 0 277 while i < NHELD { if lp_run_prog(T, lp_ha(i), lp_hb(i)) == lp_eval(T, lp_ha(i), lp_hb(i)) { ok = ok + 1 } i = i + 1 } 278 return ok 279} 280 281func lp_seed(seed: i64) -> i64 { 282 let state: *i64 = sys_mmap(8) as *i64; state[0] = seed * EVO_MAGIC_2654435761 + EVO_MAGIC_12345 283 let T: *i64 = sys_mmap(GLEN * 8) as *i64 284 let G: *i64 = sys_mmap(GLEN * 8) as *i64 285 if lp_compose(state, T) != 1 { lp_p("seed="); lp_pn(seed); lp_p(" COMPOSE-FAIL\n"); return 0 } 286 let de: i64 = lp_derive(T, state, G) 287 var imatch: i64 = 0; var i: i64 = 0 288 while i < NHELD { if lp_eval_at(G, 0, lp_ha(i), lp_hb(i)) == lp_eval(T, lp_ha(i), lp_hb(i)) { imatch = imatch + 1 } i = i + 1 } 289 let hf: i64 = lp_hw_faithful(T) 290 let hw: i64 = lp_hw_agree(T, G) 291 lp_p("seed="); lp_pn(seed); lp_p(" derive_err="); lp_pn(de) 292 lp_p(" interp_held="); lp_pn(imatch); lp_p("/"); lp_pn(NHELD) 293 lp_p(" sim(T)==interp="); lp_pn(hf); lp_p("/"); lp_pn(NHELD) 294 lp_p(" sim(T)==sim(G)="); lp_pn(hw); lp_p("/"); lp_pn(NHELD) 295 if de == 0 { if imatch == NHELD { if hf == NHELD { if hw == NHELD { 296 lp_p(" GREEN\n"); return 1 297 }}}} 298 lp_p(" RED\n"); return 0 299} 300 301// CONTROL 2 (negative): perturb G's body op1 so the INTERPRETER differs from T on some held-out 302// point; confirm the HARDWARE differential CATCHES it. 303func lp_negctl(seed: i64) -> i64 { 304 let state: *i64 = sys_mmap(8) as *i64; state[0] = seed * EVO_MAGIC_2654435761 + 777 305 let T: *i64 = sys_mmap(GLEN * 8) as *i64 306 let G: *i64 = sys_mmap(GLEN * 8) as *i64 307 let Gp: *i64 = sys_mmap(GLEN * 8) as *i64 308 if lp_compose(state, T) != 1 { lp_p(" control-negative: COMPOSE-FAIL\n"); return 0 } 309 lp_derive(T, state, G) 310 var found: i64 = 0; var cand: i64 = 0 311 while cand < 3 { 312 var c: i64 = 0; while c < GLEN { Gp[c] = G[c]; c = c + 1 } 313 Gp[0] = cand 314 var differs: i64 = 0; var i: i64 = 0 315 while i < NHELD { if lp_eval_at(Gp, 0, lp_ha(i), lp_hb(i)) != lp_eval(T, lp_ha(i), lp_hb(i)) { differs = 1 } i = i + 1 } 316 if differs == 1 { found = 1; cand = 3 } else { cand = cand + 1 } 317 } 318 if found == 0 { lp_p(" control-negative: no distinguishing body (inconclusive)\n"); return 0 } 319 let agree: i64 = lp_hw_agree(T, Gp) 320 lp_p(" control-negative: sim(T)==sim(G_wrongbody)="); lp_pn(agree); lp_p("/"); lp_pn(NHELD) 321 if agree < NHELD { lp_p(" -> differential CAUGHT the wrong loop body (good)\n"); return 1 } 322 lp_p(" -> differential MISSED it (test broken)\n"); return 0 323} 324 325func main() -> i64 { 326 lp_p("ISALOOPSOV: loop rung -- derive ITERATIVE programs (acc=sum_{i=1..a} body) with a BACKWARD branch, run on god\n") 327 let cfaith: i64 = lp_faithful() 328 var ok: i64 = 0 329 if lp_seed(101) == 1 { ok = ok + 1 } 330 if lp_seed(202) == 1 { ok = ok + 1 } 331 if lp_seed(303) == 1 { ok = ok + 1 } 332 if lp_seed(404) == 1 { ok = ok + 1 } 333 let nc: i64 = lp_negctl(202) 334 lp_p("ISALOOPSOV: "); lp_pn(ok); lp_p("/4 seeds: team-composed LOOP == team-derived program, PROVEN on rv64im_min_sim over held-out\n") 335 if cfaith == 1 { if ok == 4 { if nc == 1 { 336 lp_p("ISALOOPSOV GREEN: faithful closed-form control PASS + negative control CAUGHT a wrong body + 4/4 hardware-verified equivalences -- god's BACKWARD branch (loop) exercised\n") 337 sys_exit(0); return 0 338 }}} 339 lp_p("ISALOOPSOV RED\n") 340 sys_exit(1) 341 return 1 342}