nx_rule_soundness_test.nx source

1// nx_rule_soundness_test.nx -- FAIL-LOUD driver that PROVES the nx_eqsat rewrite 2// rules SOUND (algebraic identities mod 2^W) via nx_rule_soundness.nx. 3// 4// Strategy (winning): width-independent induction (reuses the divider-proof 5// template) + EXHAUSTIVE small-width at W=8, with nx_triangulate as the 6// independent cross-check, and TWO independent witnesses per vector ANDed. 7// 8// CERTIFIED-LIVE SET (this rung): the SIX width-trivial unary rules 9// {add_zero, sub_self, add_self, and_self, or_zero, mul_one} 10// swept exhaustively over x in [0,2^8). They have NO k boundary and ZERO owed 11// guards, so they are fully certifiable now. Known answer: total_unary == 1536 12// (= 6 * 256), all certified. 13// 14// mul_pow2 (NEXT rung -- theorem proven here but NOT in the certified-live set): 15// IN-RANGE: for all x in [0,2^8) and all k in [0,8), MUL(x,2^k) == SHL(x,k) 16// mod 2^8. Known answer: in_range == 2048 (= 256 * 8), all certified. 17// BOUNDARY (k>=W): the rule MUST NOT fire -- the identity is FALSE. We PROVE 18// unsoundness for k in [8,16) over all x (the owed k<W guard's location). 19// Known answer: neg_caught == neg_total == 2048 (= 256 * 8). mul_pow2 stays 20// OUT of the live-certified set until the k<W guard lands in nx_eqsat.nx. 21// 22// EXIT CODES (FAIL LOUD): 23// 1 a certified-unary rule vector failed (proven_unary != total_unary) 24// 2 unary total mismatch (total_unary != 1536) 25// 3 a mul_pow2 in-range vector failed (proven_ir != in_range) 26// 4 mul_pow2 in-range total mismatch (in_range != 2048) 27// 5 a mul_pow2 boundary vector did NOT demonstrate unsoundness (neg_caught != neg_total) 28// 6 boundary total mismatch (neg_total != 2048) 29// 0 ALL pass. 30// 31// KNOWN-ANSWER LINE printed (FAIL LOUD): the per-rule pass counts then the 32// exhaustive totals: 33// "<add_zero> <sub_self> <add_self> <and_self> <or_zero> <mul_one> | <rules_proven> <proven_unary> <total_unary> | <proven_ir> <in_range> | <neg_caught> <neg_total>" 34// 35// SOVEREIGN: no SMT, no .sh, no foreign oracle -- runs on the pinned compiler. 36 37import "nx_rule_soundness.nx" 38// ALSO import the membership proof: it owns the shift-merge in-range two-witness 39// battery (mp_battery_shift_merge), the i+j>=W boundary-unsound witness 40// (mp_shiftmerge_boundary_unsound), the proven-sound allow-list (mp_is_sound_rule), 41// and the live certifier (mp_certify_live). This soundness test PROVES the certified 42// shift-merge rule (shl (shl x i) j)->(shl x (i+j)) here, BEFORE the allow-list arm 43// is trusted -- the SAME discipline that admitted mul_pow2/xor_self. Both libraries 44// share the same transitive deps (nx_alu_divider/nx_triangulate); import-dedup-safe. 45// The shift-merge proof is asserted INTERNALLY (new exit codes) so the printed 46// known-answer line stays byte-identical (the mandated regression). 47import "nx_eqsat_membership_proof.nx" 48 49const RW: i64 = 8 // representative width: sweep x in [0,2^8) 50 51func _emit_num(v: i64) -> i64 { 52 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 53 let t2: *u8 = sys_mmap(28); var t: i64 = 0 54 if n == 0 { t2[0] = 48; t = 1 } 55 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 56 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 57 b[t] = 32; sys_write(1, b, t + 1); return 0 58} 59func _bar() -> i64 { let z: *u8 = sys_mmap(4); z[0] = 124; z[1] = 32; sys_write(1, z, 2); return 0 } 60func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 61 62// Exhaustively certify ONE unary rule over x in [0,2^RW). Returns the pass count 63// (should equal hi). Accumulates the shared gsim scratch via the caller's bufs. 64func sweep_unary(rule: i64, hi: i64, 65 vals: *i64, cells: *NxGsimCell, g: *NxGsim, 66 legs: *i64, v: *NxTriVerdict) -> i64 { 67 var pass: i64 = 0 68 var x: i64 = 0 69 while x < hi { 70 if nx_rs_certify_unary(rule, x, RW, vals, cells, g, legs, v) == 1 { 71 pass = pass + 1 72 } 73 x = x + 1 74 } 75 return pass 76} 77 78func main() -> i64 { 79 // Shared scratch (caller-owned, reset per vector by nx_rs_mk). 80 let vals: *i64 = sys_mmap(64 * 8) as *i64 81 let cells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell 82 let g: *NxGsim = sys_mmap(64) as *NxGsim 83 let legs: *i64 = sys_mmap(2 * 8) as *i64 84 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict 85 86 let hi: i64 = 1 << RW // 2^RW = 256 87 88 // ---- SIX width-trivial unary rules (the certified-live rung) ------------- 89 let p_addz: i64 = sweep_unary(NX_RS_ADD_ZERO, hi, vals, cells, g, legs, v) 90 let p_subs: i64 = sweep_unary(NX_RS_SUB_SELF, hi, vals, cells, g, legs, v) 91 let p_adds: i64 = sweep_unary(NX_RS_ADD_SELF, hi, vals, cells, g, legs, v) 92 let p_ands: i64 = sweep_unary(NX_RS_AND_SELF, hi, vals, cells, g, legs, v) 93 let p_orz: i64 = sweep_unary(NX_RS_OR_ZERO, hi, vals, cells, g, legs, v) 94 let p_mul1: i64 = sweep_unary(NX_RS_MUL_ONE, hi, vals, cells, g, legs, v) 95 96 let proven_unary: i64 = p_addz + p_subs + p_adds + p_ands + p_orz + p_mul1 97 let total_unary: i64 = 6 * hi // 6 * 256 = 1536 98 99 // rules_proven = number of the six rules that passed ALL 256 vectors. 100 var rules_proven: i64 = 0 101 if p_addz == hi { rules_proven = rules_proven + 1 } 102 if p_subs == hi { rules_proven = rules_proven + 1 } 103 if p_adds == hi { rules_proven = rules_proven + 1 } 104 if p_ands == hi { rules_proven = rules_proven + 1 } 105 if p_orz == hi { rules_proven = rules_proven + 1 } 106 if p_mul1 == hi { rules_proven = rules_proven + 1 } 107 108 // ---- mul_pow2 IN-RANGE theorem (NEXT rung; proven, not live-certified) --- 109 var proven_ir: i64 = 0 110 var in_range: i64 = 0 111 var x: i64 = 0 112 while x < hi { 113 var k: i64 = 0 114 while k < RW { // k in [0,W) 115 in_range = in_range + 1 116 if nx_rs_certify_mulpow2(x, k, RW, vals, cells, g, legs, v) == 1 { 117 proven_ir = proven_ir + 1 118 } 119 k = k + 1 120 } 121 x = x + 1 122 } 123 124 // ---- mul_pow2 BOUNDARY: prove UNSOUND for k>=W (the owed guard's home) --- 125 var neg_caught: i64 = 0 126 var neg_total: i64 = 0 127 var bx: i64 = 0 128 while bx < hi { 129 var bk: i64 = RW // k in [W, 2W) 130 while bk < (2 * RW) { 131 neg_total = neg_total + 1 132 if nx_rs_mulpow2_boundary_unsound(bx, bk, RW) == 1 { 133 neg_caught = neg_caught + 1 134 } 135 bk = bk + 1 136 } 137 bx = bx + 1 138 } 139 140 // ===== CERTIFIED SHIFT-MERGE RULE: prove sound BEFORE the engine cites it ===== 141 // (shl (shl x i) j) == (shl x (i+j)) for i,j CONST, i+j<W. Proven via the SAME 142 // method: W=8 masked exhaustive two-witness IN-RANGE battery + i+j>=W BOUNDARY 143 // unsound + a LIVE certification of a real shift-merge merge. Asserted INTERNALLY 144 // (new exit codes 7..12) so the printed known-answer line above stays byte-identical 145 // (the mandated regression). Uses the membership proof's owned batteries. 146 let mp_t: *NxTriTally = sys_mmap(64) as *NxTriTally 147 nx_tri_tally_init(mp_t) 148 let sm_total: i64 = mp_battery_shift_merge(g, vals, cells, mp_t) // 256 * 36 == 9216 149 let sm_passed: i64 = mp_t.passed 150 151 // BOUNDARY: prove UNSOUND for i+j>=W over all x and all (i,j) in [0,W)x[0,W) 152 // with i+j>=W (the i+j<W guard's home). lockstep i+j<W (in matcher) iff certified. 153 var sm_neg_caught: i64 = 0 154 var sm_neg_total: i64 = 0 155 var sx: i64 = 0 156 while sx < hi { 157 var si: i64 = 0 158 while si < RW { 159 var sj: i64 = 0 160 while sj < RW { 161 if (si + sj) >= RW { // boundary region only 162 sm_neg_total = sm_neg_total + 1 163 if mp_shiftmerge_boundary_unsound(sx, si, sj) == 1 { 164 sm_neg_caught = sm_neg_caught + 1 165 } 166 } 167 sj = sj + 1 168 } 169 si = si + 1 170 } 171 sx = sx + 1 172 } 173 174 // LIVE CERTIFICATION: build (shl (shl v 2) 3), enable prov + the DSL table (7 175 // builtins + shift-merge row), run the REAL saturator; the e-matcher merges the 176 // nested-shift class with (shl v 5) citing id 11; mp_certify_live must CERTIFY. 177 let sm_nodes: *NxENode = sys_mmap(128 * 64) as *NxENode 178 let sm_cls: *NxEClass = sys_mmap(128 * 32) as *NxEClass 179 let g5: *NxEGraph = sys_mmap(256) as *NxEGraph 180 nx_eqsat_init(g5, sm_nodes, 128, sm_cls, 128) 181 let sm_prov: *i64 = sys_mmap(128 * 8) as *i64 182 nx_eqsat_enable_prov(g5, sm_prov, 128) 183 let sm_tab: *NxDslRule = sys_mmap(16 * 96) as *NxDslRule 184 let sm_n: i64 = nx_eqsat_builtin_dsl_table(sm_tab) 185 nx_eqsat_dsl_set_row(sm_tab, sm_n, NX_EQSAT_RULE_SHIFT_MERGE, NX_EQ_OP_SHL, 186 DSL_VAR, 0, DSL_VAR, 0, 187 RHS_SHL_A_BY_IADDED_J, 0, 188 SC_SHIFT_MERGE_IJW, CNT_REAL_MERGE, 0) 189 nx_eqsat_enable_dsl(g5, sm_tab, 8, 16) 190 let sm_v: i64 = nx_eqsat_add_var(g5, 0) 191 let sm_c2: i64 = nx_eqsat_add_const(g5, 2) 192 let sm_inner: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_SHL, sm_v, sm_c2) // (shl v 2) 193 let sm_c3: i64 = nx_eqsat_add_const(g5, 3) 194 let sm_outer: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_SHL, sm_inner, sm_c3) // (shl (shl v 2) 3) 195 let sm_c5: i64 = nx_eqsat_add_const(g5, 5) 196 let sm_merged: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_SHL, sm_v, sm_c5) // (shl v 5) 197 let sm_sat: i64 = nx_eqsat_saturate(g5, 16) 198 let sm_cert_o: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate 199 let sm_cert: i64 = mp_certify_live(g5, sm_outer, sm_merged, sm_cert_o) 200 // did a shift-merge citation (id 11) actually get logged? 201 var sm_saw11: i64 = 0 202 var sq: i64 = 0 203 while sq < g5.n_prov { if g5.prov[sq] == NX_EQSAT_RULE_SHIFT_MERGE { sm_saw11 = 1 } sq = sq + 1 } 204 205 // ---- KNOWN-ANSWER LINE (FAIL LOUD) -------------------------------------- 206 _emit_num(p_addz); _emit_num(p_subs); _emit_num(p_adds); 207 _emit_num(p_ands); _emit_num(p_orz); _emit_num(p_mul1); _bar(); 208 _emit_num(rules_proven); _emit_num(proven_unary); _emit_num(total_unary); _bar(); 209 _emit_num(proven_ir); _emit_num(in_range); _bar(); 210 _emit_num(neg_caught); _emit_num(neg_total); _nl(); 211 212 // ---- FAIL-LOUD assertions on the known answers -------------------------- 213 if proven_unary != total_unary { sys_exit(1); return 1 } // every unary vector certified 214 if total_unary != 1536 { sys_exit(2); return 2 } // 6 * 256 215 if proven_ir != in_range { sys_exit(3); return 3 } // every mul_pow2 in-range vector certified 216 if in_range != 2048 { sys_exit(4); return 4 } // 256 * 8 217 if neg_caught != neg_total { sys_exit(5); return 5 } // every boundary vector proven unsound 218 if neg_total != 2048 { sys_exit(6); return 6 } // 256 * 8 219 // ---- SHIFT-MERGE internal assertions (not printed; KA byte-identical) ---- 220 if sm_total != 9216 { sys_exit(7); return 7 } // 256 * 36 (i+j<W triangle @W=8) 221 if sm_passed != sm_total { sys_exit(8); return 8 } // every in-range vector both-witness pass 222 if sm_neg_total != 7168 { sys_exit(9); return 9 } // 256 * 28 (i+j>=W region @W=8: 64-36 pairs) 223 if sm_neg_caught != sm_neg_total { sys_exit(10); return 10 } // every boundary vector proven unsound 224 if mp_is_sound_rule(NX_EQSAT_RULE_SHIFT_MERGE) != 1 { sys_exit(11); return 11 } // admitted only after battery 225 if sm_sat != NX_EQSAT_SATURATED { sys_exit(12); return 12 } // engine converged 226 if sm_saw11 != 1 { sys_exit(13); return 13 } // the rule actually fired (id 11 logged) 227 if sm_cert != 1 { sys_exit(14); return 14 } // membership-proof CERTIFIES the merge 228 sys_exit(0); return 0 229}