code wiki / _hdl_build / nx_eqsat_constfold_test.nx
`nx_eqsat_constfold_test.nx` source

↩ module page · 211 lines · 13585 B
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_gate_verdict.nx"
29import "nx_eqsat_membership_proof.nx"
30
31func _emit_num(v: i64) -> i64 {
  let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n }
  let t2: *u8 = sys_mmap(28); var t: i64 = 0
  if n == 0 { t2[0] = 48; t = 1 }
  while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
  var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
  b[t] = 32; sys_write(1, b, t + 1); return 0
38}
39func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
40
41// Does the live provenance log contain rule-id `want`?
42func _log_has(g: *NxEGraph, want: i64) -> i64 {
  var i: i64 = 0
  while i < g.n_prov {
      if g.prov[i] == want { return 1 }
      i = i + 1
  }
  return 0
49}
50
51// Build a fresh e-graph that folds a binary op of two constants, return the
52// folded value read from the resulting class's best_node + whether it CERTIFIES.
53// cert_out[0] = mp_certify_live verdict. Returns the folded constant value.
54func _fold_binop(op: i64, a: i64, b: i64, cert_out: *i64) -> i64 {
  let cap_nodes: i64 = 64
  let cap_cls: i64 = 64
  let nodes: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let classes: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
  if nx_eqsat_init(eg, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { sys_exit(80); return 80 }
  // enable provenance + const-fold BEFORE adding the op node (the hook fires at add)
  let plog: *i64 = sys_mmap(64 * 8) as *i64
  if nx_eqsat_enable_prov(eg, plog, 64) != NX_EQSAT_OK { sys_exit(81); return 81 }
  if nx_eqsat_enable_constfold(eg) != NX_EQSAT_OK { sys_exit(82); return 82 }
  let ca: i64 = nx_eqsat_add_const(eg, a)
  let cb: i64 = nx_eqsat_add_const(eg, b)
  let top: i64 = nx_eqsat_add_binary(eg, op, ca, cb)      // hook folds here
  // The expected constant (added separately) for the membership endpoint.
  // gsim is the engine's oracle; recompute the same value via the SAME oracle.
  let expect: i64 = nx_gsim_eval_cell(nx_eqsat_op_to_gate_kind(op), a, b, 0)
  let cexp: i64 = nx_eqsat_add_const(eg, expect)
  // run the real saturator (idempotent; the fold already merged at add-time)
  nx_eqsat_saturate(eg, 16)
  // certify the equivalence top == CONST(expect) STRICTLY FROM THE LOG.
  let cert: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok: i64 = mp_certify_live(eg, top, cexp, cert)
  cert_out[0] = cok
  // sanity: the log must contain RULE_CONSTFOLD (the merge was const-fold)
  if _log_has(eg, NX_EQSAT_RULE_CONSTFOLD) != 1 { sys_exit(83); return 83 }
  // read the folded value off top's canonical best_node
  let canon: i64 = nx_eqsat_find(eg, top)
  let bn: i64 = eg.classes[canon].best_node
  if eg.nodes[bn].op != NX_EQ_OP_CONST { sys_exit(84); return 84 }
  return eg.nodes[bn].payload
85}
86
87func main() -> i64 {
  // ====================================================================
  // STEP 0: LOCKSTEP + allow-list admission.
  // ====================================================================
  // MIGRATED OFF A HAND-ROLLED VERDICT 2026-08-14, and NEVER COMPILED BEFORE THAT DAY (nx_eqsat.nx
  // itself did not compile). The teeth were already strong -- this file carries more negative controls
  // than positives -- they simply had no way to report to anything outside the process, and an
  // exit-code-as-assertion-number protocol stops at the FIRST failure, hiding the rest.
  gv_head("nx_eqsat const-fold gate -- e-class analysis folds only ops with a faithful oracle cell" as *u8)
  let ctr: *i64 = gv_ctr()
97
  gv_check("rule ids are in lockstep between the engine and the membership prover" as *u8, mp_rule_ids_lockstep() == 1, ctr)
  gv_check("MP_RULE_CONSTFOLD and NX_EQSAT_RULE_CONSTFOLD are the same id" as *u8, MP_RULE_CONSTFOLD == NX_EQSAT_RULE_CONSTFOLD, ctr)
  gv_check("const-fold is admitted to the proven-sound allow-list" as *u8, mp_is_sound_rule(MP_RULE_CONSTFOLD) == 1, ctr)
  // 12 is a KNOWN-ANSWER oracle, not a magic number: it pins the rule-table size so that appending a
  // rule without extending this gate is a RED rather than a silent widening of what counts as sound.
  gv_check("the rule table is still the size this gate was written against" as *u8, NX_EQSAT_RULE_N == 12, ctr)
104
  // ====================================================================
  // STEP 1 + STEP 2: positive folds + certificates.
  // ====================================================================
  let ca: *i64 = sys_mmap(8) as *i64
  let cm: *i64 = sys_mmap(8) as *i64
  let cs: *i64 = sys_mmap(8) as *i64
  let f_add: i64 = _fold_binop(NX_EQ_OP_ADD, 2, 3, ca)   // 2+3 = 5
  let f_mul: i64 = _fold_binop(NX_EQ_OP_MUL, 6, 7, cm)   // 6*7 = 42
  let f_shl: i64 = _fold_binop(NX_EQ_OP_SHL, 1, 4, cs)   // 1<<4 = 16
114
  _emit_num(f_add); _emit_num(f_mul); _emit_num(f_shl)
  _emit_num(ca[0]); _emit_num(cm[0]); _emit_num(cs[0])
  _nl()
118
  // ====================================================================
  // STEP 3a: NEGATIVE -- an UNMAPPED op (DIV) never folds (no faithful cell).
  // ====================================================================
  // FIVE OPS THE FOLDER MUST REFUSE because no gate cell computes them faithfully. These are the
  // teeth that stop const-fold from becoming fold-everything-and-hope.
  gv_check("neg-control-DIV-has-no-faithful-cell-and-is-refused" as *u8, nx_eqsat_op_to_gate_kind(NX_EQ_OP_DIV) < 0, ctr)
  gv_check("neg-control-REM-is-refused" as *u8, nx_eqsat_op_to_gate_kind(NX_EQ_OP_REM) < 0, ctr)
  gv_check("neg-control-SHR-is-refused-logical-is-not-arithmetic" as *u8, nx_eqsat_op_to_gate_kind(NX_EQ_OP_SHR) < 0, ctr)
  gv_check("neg-control-SAR-is-refused" as *u8, nx_eqsat_op_to_gate_kind(NX_EQ_OP_SAR) < 0, ctr)
  gv_check("neg-control-NEG-is-refused-NOT-is-not-negate" as *u8, nx_eqsat_op_to_gate_kind(NX_EQ_OP_NEG) < 0, ctr)
  // build (div 12 3) with const children + const-fold ON: it must NOT fold.
  let cap_nodes: i64 = 64
  let cap_cls: i64 = 64
  let n2: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let c2: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg2: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
  if nx_eqsat_init(eg2, n2, cap_nodes, c2, cap_cls) != NX_EQSAT_OK { sys_exit(15); return 15 }
  let plog2: *i64 = sys_mmap(64 * 8) as *i64
  nx_eqsat_enable_prov(eg2, plog2, 64)
  nx_eqsat_enable_constfold(eg2)
  let d12: i64 = nx_eqsat_add_const(eg2, 12)
  let d3: i64 = nx_eqsat_add_const(eg2, 3)
  let divv: i64 = nx_eqsat_add_binary(eg2, NX_EQ_OP_DIV, d12, d3)   // would-be 4, but REFUSED
  let four: i64 = nx_eqsat_add_const(eg2, 4)
  nx_eqsat_saturate(eg2, 16)
  gv_check("neg-control-a-refused-op-with-const-children-does-NOT-fold-to-its-value" as *u8, nx_eqsat_find(eg2, divv) != nx_eqsat_find(eg2, four), ctr)
  gv_check("neg-control-a-refused-fold-logs-NO-constfold-id" as *u8, _log_has(eg2, NX_EQSAT_RULE_CONSTFOLD) == 0, ctr)
  // the DIV node's best_node must still be a DIV (no const merged in)
  let dc: i64 = nx_eqsat_find(eg2, divv)
  gv_check("neg-control-the-refused-node-still-extracts-as-DIV-not-a-constant" as *u8, eg2.nodes[eg2.classes[dc].best_node].op == NX_EQ_OP_DIV, ctr)
149
  // ====================================================================
  // STEP 3b: NEGATIVE -- an UNPROVEN rule id is refused by the certifier. A
  // back-door merge citing RULE_NONE (the legacy 2-arg union) poisons the log,
  // so mp_log_all_sound refuses it -> the certificate cannot pass even though
  // the endpoints ARE in the same class (membership holds).
  // ====================================================================
  let n3: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let c3a: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg3: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
  if nx_eqsat_init(eg3, n3, cap_nodes, c3a, cap_cls) != NX_EQSAT_OK { sys_exit(20); return 20 }
  let plog3: *i64 = sys_mmap(64 * 8) as *i64
  nx_eqsat_enable_prov(eg3, plog3, 64)
  let va: i64 = nx_eqsat_add_var(eg3, 0)
  let vb: i64 = nx_eqsat_add_var(eg3, 1)
  // merge two UNEQUAL vars through the RULE_NONE back door (an unsound merge).
  nx_eqsat_union(eg3, va, vb)
  let certN: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cokN: i64 = mp_certify_live(eg3, va, vb, certN)
  // THE SHARPEST CONTROL IN THE FILE: membership and soundness are SEPARATED. A back-door union
  // really does put the two vars in one class, so a certifier that only checked membership would
  // pass -- and it must not, because the merge cites no proven rule.
  gv_check("back-door merged endpoints ARE in one class, so membership genuinely holds" as *u8, certN.member == 1, ctr)
  gv_check("neg-control-an-uncited-RULE_NONE-merge-poisons-soundness" as *u8, certN.sound == 0, ctr)
  gv_check("neg-control-the-certificate-FAILS-despite-membership-holding" as *u8, cokN == 0, ctr)
  gv_check("neg-control-RULE_NONE-is-not-in-the-proven-sound-allow-list" as *u8, mp_is_sound_rule(MP_RULE_NONE) == 0, ctr)
  gv_check("neg-control-a-deliberately-bogus-rule-is-not-admitted" as *u8, mp_is_sound_rule(MP_RULE_BOGUS_MUL3) == 0, ctr)
176
  // ====================================================================
  // STEP 3c: const-fold is OFF by default (opt-in). With NO enable call, an
  // all-const op must NOT fold and must NOT log a CONSTFOLD id (byte-identical
  // backward-compat by construction).
  // ====================================================================
  let n4: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let c4: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg4: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
  if nx_eqsat_init(eg4, n4, cap_nodes, c4, cap_cls) != NX_EQSAT_OK { sys_exit(30); return 30 }
  let plog4: *i64 = sys_mmap(64 * 8) as *i64
  nx_eqsat_enable_prov(eg4, plog4, 64)
  // NOTE: NO nx_eqsat_enable_constfold call -- folding stays OFF.
  let oa: i64 = nx_eqsat_add_const(eg4, 2)
  let ob: i64 = nx_eqsat_add_const(eg4, 3)
  let osum: i64 = nx_eqsat_add_binary(eg4, NX_EQ_OP_ADD, oa, ob)
  let ofive: i64 = nx_eqsat_add_const(eg4, 5)
  nx_eqsat_saturate(eg4, 16)
  gv_check("neg-control-with-const-fold-OFF-an-all-const-op-does-NOT-fold" as *u8, nx_eqsat_find(eg4, osum) != nx_eqsat_find(eg4, ofive), ctr)
  gv_check("neg-control-with-const-fold-OFF-nothing-is-logged" as *u8, _log_has(eg4, NX_EQSAT_RULE_CONSTFOLD) == 0, ctr)
196
  // ====================================================================
  // FINAL known-answer gate (FAIL LOUD).
  // ====================================================================
  // THE POSITIVES. Every tooth above asserts a REFUSAL, and a folder that folded NOTHING would pass
  // all of them -- these three are the discrimination controls that make the refusals mean something.
  gv_check("folds add: 2 plus 3 is 5" as *u8, f_add == 5, ctr)
  gv_check("folds mul: 6 times 7 is 42" as *u8, f_mul == 42, ctr)
  gv_check("folds shl: 1 shifted left 4 is 16" as *u8, f_shl == 16, ctr)
  gv_check("the add fold CERTIFIES live from the provenance log" as *u8, ca[0] == 1, ctr)
  gv_check("the mul fold CERTIFIES live" as *u8, cm[0] == 1, ctr)
  gv_check("the shl fold CERTIFIES live" as *u8, cs[0] == 1, ctr)
208
  return gv_verdict("nx_eqsat_constfold_test" as *u8, ctr,
      "const-fold e-class analysis: three certified folds against ten refusal controls, including an uncited back-door merge that holds membership yet fails its certificate" as *u8)
211}
nx_eqsat_constfold_test.nx source

`nx_eqsat_constfold_test.nx` source
