nx_eqsat_constfold_test.nx source

1// nx_eqsat_constfold_test.nx -- the CONST-FOLD GATE: proves the egg-style e-class 2// ANALYSIS (constant folding / propagation) newly integrated into nx_eqsat.nx is 3// (a) SOUND BY EVALUATION (folds via the PROVEN nx_gsim_eval_cell oracle), 4// (b) CERTIFIED through membership-as-proof (cites NX_EQSAT_RULE_CONSTFOLD, admitted 5// to the proven-sound allow-list + lockstep), and 6// (c) LOAD-BEARING (a wrong fold / unmapped op / unproven rule is REFUSED). 7// 8// FAIL LOUD known-answer; exit 0 iff every check holds. 9// 10// STEPS (each self-asserts; mismatch => sys_exit(nonzero)): 11// STEP 0 LOCKSTEP: MP_RULE_CONSTFOLD == NX_EQSAT_RULE_CONSTFOLD (and the whole 12// id table agrees), so the live log the engine writes is never mislabeled. 13// Also: MP_RULE_CONSTFOLD must be in the proven-sound allow-list. 14// STEP 1 POSITIVE (add 2 3)->5, LIVE + CERTIFIED: enable prov + constfold, run the 15// REAL saturator, assert find(add23)==find(5), the log contains RULE_CONSTFOLD, 16// and mp_certify_live CERTIFIES (member && sound). 17// STEP 2 MORE OPS: (mul 6 7)->42 and (shl 1 4)->16 fold + certify (same engine path). 18// STEP 3 NEGATIVE -- WRONG FOLD REFUSED: (a) an unmapped op (DIV) never folds even 19// with const children (nx_eqsat_op_to_gate_kind(DIV) < 0) -- find stays 20// distinct from any const; (b) an UNPROVEN rule id (BOGUS) is NOT in the 21// allow-list so mp_log_all_sound would refuse it -- a back-door wrong fold 22// cannot certify; (c) folding is OFF by default (no enable => no fold => no 23// CONSTFOLD in the log) so the feature is opt-in by construction. 24// 25// Known answer (FAIL LOUD): prints "5 42 16 1 1 1 " == folded(add 2 3), folded(mul 6 7), 26// folded(shl 1 4), cert_add, cert_mul, cert_shl. exit 0 iff all steps hold. 27 28import "nx_eqsat_membership_proof.nx" 29 30func _emit_num(v: i64) -> i64 { 31 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 32 let t2: *u8 = sys_mmap(28); var t: i64 = 0 33 if n == 0 { t2[0] = 48; t = 1 } 34 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 35 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 36 b[t] = 32; sys_write(1, b, t + 1); return 0 37} 38func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 39 40// Does the live provenance log contain rule-id `want`? 41func _log_has(g: *NxEGraph, want: i64) -> i64 { 42 var i: i64 = 0 43 while i < g.n_prov { 44 if g.prov[i] == want { return 1 } 45 i = i + 1 46 } 47 return 0 48} 49 50// Build a fresh e-graph that folds a binary op of two constants, return the 51// folded value read from the resulting class's best_node + whether it CERTIFIES. 52// cert_out[0] = mp_certify_live verdict. Returns the folded constant value. 53func _fold_binop(op: i64, a: i64, b: i64, cert_out: *i64) -> i64 { 54 let cap_nodes: i64 = 64 55 let cap_cls: i64 = 64 56 let nodes: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 57 let classes: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 58 let eg: *NxEGraph = sys_mmap(128) as *NxEGraph 59 if nx_eqsat_init(eg, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { sys_exit(80); return 80 } 60 // enable provenance + const-fold BEFORE adding the op node (the hook fires at add) 61 let plog: *i64 = sys_mmap(64 * 8) as *i64 62 if nx_eqsat_enable_prov(eg, plog, 64) != NX_EQSAT_OK { sys_exit(81); return 81 } 63 if nx_eqsat_enable_constfold(eg) != NX_EQSAT_OK { sys_exit(82); return 82 } 64 let ca: i64 = nx_eqsat_add_const(eg, a) 65 let cb: i64 = nx_eqsat_add_const(eg, b) 66 let top: i64 = nx_eqsat_add_binary(eg, op, ca, cb) // hook folds here 67 // The expected constant (added separately) for the membership endpoint. 68 // gsim is the engine's oracle; recompute the same value via the SAME oracle. 69 let expect: i64 = nx_gsim_eval_cell(nx_eqsat_op_to_gate_kind(op), a, b, 0) 70 let cexp: i64 = nx_eqsat_add_const(eg, expect) 71 // run the real saturator (idempotent; the fold already merged at add-time) 72 nx_eqsat_saturate(eg, 16) 73 // certify the equivalence top == CONST(expect) STRICTLY FROM THE LOG. 74 let cert: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate 75 let cok: i64 = mp_certify_live(eg, top, cexp, cert) 76 cert_out[0] = cok 77 // sanity: the log must contain RULE_CONSTFOLD (the merge was const-fold) 78 if _log_has(eg, NX_EQSAT_RULE_CONSTFOLD) != 1 { sys_exit(83); return 83 } 79 // read the folded value off top's canonical best_node 80 let canon: i64 = nx_eqsat_find(eg, top) 81 let bn: i64 = eg.classes[canon].best_node 82 if eg.nodes[bn].op != NX_EQ_OP_CONST { sys_exit(84); return 84 } 83 return eg.nodes[bn].payload 84} 85 86func main() -> i64 { 87 // ==================================================================== 88 // STEP 0: LOCKSTEP + allow-list admission. 89 // ==================================================================== 90 if mp_rule_ids_lockstep() != 1 { sys_exit(1); return 1 } 91 if MP_RULE_CONSTFOLD != NX_EQSAT_RULE_CONSTFOLD { sys_exit(2); return 2 } 92 if mp_is_sound_rule(MP_RULE_CONSTFOLD) != 1 { sys_exit(3); return 3 } // admitted 93 if NX_EQSAT_RULE_N != 12 { sys_exit(4); return 4 } // RULE_N bumped (10 constfold + 11 shift_merge) 94 95 // ==================================================================== 96 // STEP 1 + STEP 2: positive folds + certificates. 97 // ==================================================================== 98 let ca: *i64 = sys_mmap(8) as *i64 99 let cm: *i64 = sys_mmap(8) as *i64 100 let cs: *i64 = sys_mmap(8) as *i64 101 let f_add: i64 = _fold_binop(NX_EQ_OP_ADD, 2, 3, ca) // 2+3 = 5 102 let f_mul: i64 = _fold_binop(NX_EQ_OP_MUL, 6, 7, cm) // 6*7 = 42 103 let f_shl: i64 = _fold_binop(NX_EQ_OP_SHL, 1, 4, cs) // 1<<4 = 16 104 105 _emit_num(f_add); _emit_num(f_mul); _emit_num(f_shl) 106 _emit_num(ca[0]); _emit_num(cm[0]); _emit_num(cs[0]) 107 _nl() 108 109 // ==================================================================== 110 // STEP 3a: NEGATIVE -- an UNMAPPED op (DIV) never folds (no faithful cell). 111 // ==================================================================== 112 if nx_eqsat_op_to_gate_kind(NX_EQ_OP_DIV) >= 0 { sys_exit(10); return 10 } // DIV refused 113 if nx_eqsat_op_to_gate_kind(NX_EQ_OP_REM) >= 0 { sys_exit(11); return 11 } // REM refused 114 if nx_eqsat_op_to_gate_kind(NX_EQ_OP_SHR) >= 0 { sys_exit(12); return 12 } // SHR refused (logical!=arith) 115 if nx_eqsat_op_to_gate_kind(NX_EQ_OP_SAR) >= 0 { sys_exit(13); return 13 } // SAR refused 116 if nx_eqsat_op_to_gate_kind(NX_EQ_OP_NEG) >= 0 { sys_exit(14); return 14 } // NEG refused (NOT != neg) 117 // build (div 12 3) with const children + const-fold ON: it must NOT fold. 118 let cap_nodes: i64 = 64 119 let cap_cls: i64 = 64 120 let n2: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 121 let c2: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 122 let eg2: *NxEGraph = sys_mmap(128) as *NxEGraph 123 if nx_eqsat_init(eg2, n2, cap_nodes, c2, cap_cls) != NX_EQSAT_OK { sys_exit(15); return 15 } 124 let plog2: *i64 = sys_mmap(64 * 8) as *i64 125 nx_eqsat_enable_prov(eg2, plog2, 64) 126 nx_eqsat_enable_constfold(eg2) 127 let d12: i64 = nx_eqsat_add_const(eg2, 12) 128 let d3: i64 = nx_eqsat_add_const(eg2, 3) 129 let divv: i64 = nx_eqsat_add_binary(eg2, NX_EQ_OP_DIV, d12, d3) // would-be 4, but REFUSED 130 let four: i64 = nx_eqsat_add_const(eg2, 4) 131 nx_eqsat_saturate(eg2, 16) 132 if nx_eqsat_find(eg2, divv) == nx_eqsat_find(eg2, four) { sys_exit(16); return 16 } // must NOT fold 133 if _log_has(eg2, NX_EQSAT_RULE_CONSTFOLD) != 0 { sys_exit(17); return 17 } // no constfold logged 134 // the DIV node's best_node must still be a DIV (no const merged in) 135 let dc: i64 = nx_eqsat_find(eg2, divv) 136 if eg2.nodes[eg2.classes[dc].best_node].op != NX_EQ_OP_DIV { sys_exit(18); return 18 } 137 138 // ==================================================================== 139 // STEP 3b: NEGATIVE -- an UNPROVEN rule id is refused by the certifier. A 140 // back-door merge citing RULE_NONE (the legacy 2-arg union) poisons the log, 141 // so mp_log_all_sound refuses it -> the certificate cannot pass even though 142 // the endpoints ARE in the same class (membership holds). 143 // ==================================================================== 144 let n3: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 145 let c3a: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 146 let eg3: *NxEGraph = sys_mmap(128) as *NxEGraph 147 if nx_eqsat_init(eg3, n3, cap_nodes, c3a, cap_cls) != NX_EQSAT_OK { sys_exit(20); return 20 } 148 let plog3: *i64 = sys_mmap(64 * 8) as *i64 149 nx_eqsat_enable_prov(eg3, plog3, 64) 150 let va: i64 = nx_eqsat_add_var(eg3, 0) 151 let vb: i64 = nx_eqsat_add_var(eg3, 1) 152 // merge two UNEQUAL vars through the RULE_NONE back door (an unsound merge). 153 nx_eqsat_union(eg3, va, vb) 154 let certN: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate 155 let cokN: i64 = mp_certify_live(eg3, va, vb, certN) 156 if certN.member != 1 { sys_exit(21); return 21 } // they ARE merged (membership holds) 157 if certN.sound != 0 { sys_exit(22); return 22 } // but RULE_NONE poisons soundness 158 if cokN != 0 { sys_exit(23); return 23 } // certificate MUST fail (unproven rule) 159 // RULE_NONE / BOGUS must not be in the proven-sound allow-list. 160 if mp_is_sound_rule(MP_RULE_NONE) != 0 { sys_exit(24); return 24 } 161 if mp_is_sound_rule(MP_RULE_BOGUS_MUL3) != 0 { sys_exit(25); return 25 } 162 163 // ==================================================================== 164 // STEP 3c: const-fold is OFF by default (opt-in). With NO enable call, an 165 // all-const op must NOT fold and must NOT log a CONSTFOLD id (byte-identical 166 // backward-compat by construction). 167 // ==================================================================== 168 let n4: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 169 let c4: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 170 let eg4: *NxEGraph = sys_mmap(128) as *NxEGraph 171 if nx_eqsat_init(eg4, n4, cap_nodes, c4, cap_cls) != NX_EQSAT_OK { sys_exit(30); return 30 } 172 let plog4: *i64 = sys_mmap(64 * 8) as *i64 173 nx_eqsat_enable_prov(eg4, plog4, 64) 174 // NOTE: NO nx_eqsat_enable_constfold call -- folding stays OFF. 175 let oa: i64 = nx_eqsat_add_const(eg4, 2) 176 let ob: i64 = nx_eqsat_add_const(eg4, 3) 177 let osum: i64 = nx_eqsat_add_binary(eg4, NX_EQ_OP_ADD, oa, ob) 178 let ofive: i64 = nx_eqsat_add_const(eg4, 5) 179 nx_eqsat_saturate(eg4, 16) 180 if nx_eqsat_find(eg4, osum) == nx_eqsat_find(eg4, ofive) { sys_exit(31); return 31 } // OFF => no fold 181 if _log_has(eg4, NX_EQSAT_RULE_CONSTFOLD) != 0 { sys_exit(32); return 32 } // nothing logged 182 183 // ==================================================================== 184 // FINAL known-answer gate (FAIL LOUD). 185 // ==================================================================== 186 if f_add != 5 { sys_exit(40); return 40 } // 2 + 3 = 5 187 if f_mul != 42 { sys_exit(41); return 41 } // 6 * 7 = 42 188 if f_shl != 16 { sys_exit(42); return 42 } // 1 << 4 = 16 189 if ca[0] != 1 { sys_exit(43); return 43 } // (add 2 3)==5 certified (live) 190 if cm[0] != 1 { sys_exit(44); return 44 } // (mul 6 7)==42 certified 191 if cs[0] != 1 { sys_exit(45); return 45 } // (shl 1 4)==16 certified 192 sys_exit(0); return 0 193}