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

↩ module page · 328 lines · 17810 B
1// nx_eqsat_dsl_parity_test.nx -- the 24th GATE: proves the egg-style DATA-driven
2// rule DSL + general e-matcher (nx_eqsat_apply_dsl_table) is BEHAVIORALLY-IDENTICAL
3// to the 7 hand-coded inline rules, AND proves ONE genuinely-new sound rule
4// ((xor x x)==0) is admitted-only-after-proof, applied via the DSL, and CERTIFIES
5// through membership-as-proof -- with a load-bearing NEGATIVE control showing an
6// UNPROVEN/un-admitted rule is REFUSED.
7//
8// WHY behavioral-parity (not byte-identity) for the DSL path: the inline saturate
9// runs verbatim whenever g.dsl==null (byte-identity by construction, proven by the
10// four frozen organs staying 1:1). This gate proves the OPT-IN DSL path produces
11// the SAME observable result -- same canonical partition, same extracted op+cost,
12// same provenance multiset, same saturate return code -- over multiple graphs, so
13// the data table genuinely DRIVES saturation (it is not a no-op shim).
14//
15// STRUCTURE (each step self-asserts; mismatch => sys_exit(nonzero)):
16//   STEP 1  PARITY over eqsat_test Case 1 (add (mul x x) 0): inline vs DSL agree on
17//           find-partition + recompute_best op/cost + provenance multiset + sat rc.
18//   STEP 2  PARITY over eqsat_test Case 2 (mul x 8 -> shl x 3): same checks; this
19//           exercises the mul_pow2 side-condition + real-merge counting AS DATA.
20//   STEP 3  PARITY over a RULE-DENSE graph touching all 7 rules at once.
21//   STEP 4  NEW RULE soundness: run the W=8 masked exhaustive two-witness battery
22//           for xor_self; assert passed==total==256 (this JUSTIFIES the allow-list
23//           arm). Without this passing, mp_is_sound_rule(9) must not be trusted.
24//   STEP 5  NEW RULE applied via DSL + CERTIFIED: build (xor v v), enable prov+DSL
25//           with the 8-row table (7 builtins + xor_self), saturate; the e-matcher
26//           merges the xor-class with const-0 citing id 9; mp_certify_live==1.
27//   STEP 6  NEGATIVE CONTROL (load-bearing): a graph whose only merge cites an
28//           UN-admitted rule id must REFUSE. We drive the certifier's log scan with
29//           a hand-forged log containing an un-admitted id (200) and assert
30//           mp_log_all_sound==0 -> certificate refused; AND assert the engine's
31//           xor_self merge, if its id were NOT in the allow-list, would refute
32//           (mp_is_sound_rule on a bogus id == 0). Proves the gate is load-bearing.
33//
34// KNOWN ANSWER (FAIL LOUD), one line:
35//   "<p1> <p2> <p3> <xor_passed> <xor_total> <xor_cert> <neg_refused>"
36//   = "1 1 1 256 256 1 1 "   exit 0 iff every assertion holds.
37//
38// SOVEREIGN: no SMT, no .sh; runs on the pinned NishiLang compiler. license_tier: ORIGINAL
39
40import "nx_gate_verdict.nx"
41import "nx_eqsat_membership_proof.nx"
42
43func _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
50}
51func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
52
53// Per-rule-id histogram of a provenance log (ids 0..MP_RULE_N-1). Used to compare
54// the inline vs DSL logged-rule-id MULTISET exactly (order-independent equality).
55func _log_hist(g: *NxEGraph, hist: *i64) -> i64 {
  var i: i64 = 0
  while i < NX_EQSAT_RULE_N { hist[i] = 0; i = i + 1 }
  var j: i64 = 0
  while j < g.n_prov {
      let id: i64 = g.prov[j]
      if id >= 0 { if id < NX_EQSAT_RULE_N { hist[id] = hist[id] + 1 } }
      j = j + 1
  }
  return g.n_prov
65}
66
67func _hist_eq(a: *i64, b: *i64) -> i64 {
  var i: i64 = 0
  while i < NX_EQSAT_RULE_N {
      if a[i] != b[i] { return 0 }
      i = i + 1
  }
  return 1
74}
75
76// Fresh e-graph factory (caller owns scratch via mmap). Returns the graph ptr.
77func _mk_graph(cap_nodes: i64, cap_cls: i64) -> *NxEGraph {
  let nodes: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let classes: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let g: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
  nx_eqsat_init(g, nodes, cap_nodes, classes, cap_cls)
  return g
83}
84
85// Build the 7-row builtin table + (optionally) append xor_self as an 8th row.
86func _mk_table(with_xor: i64) -> *NxDslRule {
  let table: *NxDslRule = sys_mmap(16 * 96) as *NxDslRule    // 16 rows of >=88B
  let n: i64 = nx_eqsat_builtin_dsl_table(table)
  if with_xor == 1 {
      // ONE new data row: (xor x x)==0. zero new matcher control flow.
      // CNT_REAL_MERGE so saturation converges (the union is idempotent).
      nx_eqsat_dsl_set_row(table, n, NX_EQSAT_RULE_XOR_SELF, NX_EQ_OP_XOR,
                           DSL_VAR, 0, DSL_SAME_AS_A, 0,
                           RHS_CONST, 0, SC_NONE, CNT_REAL_MERGE, 0)
  }
  return table
97}
98
99// Run ONE parity comparison: build the SAME graph twice (inline path then DSL
100// path), saturate both with provenance ON, and assert identical observable result.
101// graph_kind selects which input to build. Returns 1 iff every facet agrees.
102func _parity(graph_kind: i64) -> i64 {
  let cap_nodes: i64 = 256
  let cap_cls: i64 = 256
105
  // ---------- INLINE path ----------
  let gi: *NxEGraph = _mk_graph(cap_nodes, cap_cls)
  let plogi: *i64 = sys_mmap(256 * 8) as *i64
  nx_eqsat_enable_prov(gi, plogi, 256)
  // roots of interest (filled per graph kind)
  var r0i: i64 = 0 - 1
  var r1i: i64 = 0 - 1
  if graph_kind == 1 {
      // Case 1: (add (mul x x) 0)
      let x: i64 = nx_eqsat_add_var(gi, 0)
      let mxx: i64 = nx_eqsat_add_binary(gi, NX_EQ_OP_MUL, x, x)
      let z: i64 = nx_eqsat_add_const(gi, 0)
      r0i = nx_eqsat_add_binary(gi, NX_EQ_OP_ADD, mxx, z)
      r1i = mxx
  }
  if graph_kind == 2 {
      // Case 2: (mul x 8)
      let x: i64 = nx_eqsat_add_var(gi, 0)
      let c8: i64 = nx_eqsat_add_const(gi, 8)
      r0i = nx_eqsat_add_binary(gi, NX_EQ_OP_MUL, x, c8)
      r1i = r0i
  }
  if graph_kind == 3 {
      // rule-dense: (add (sub y y) 0), (add w w), (and z z), (or u 0), (mul v 1),
      // (mul v 16) -- touches add_zero, sub_self, add_self, and_self, or_zero,
      // mul_one, mul_pow2 in ONE graph.
      let y: i64 = nx_eqsat_add_var(gi, 1)
      let suby: i64 = nx_eqsat_add_binary(gi, NX_EQ_OP_SUB, y, y)
      let z0: i64 = nx_eqsat_add_const(gi, 0)
      r0i = nx_eqsat_add_binary(gi, NX_EQ_OP_ADD, suby, z0)        // add_zero + sub_self
      let w: i64 = nx_eqsat_add_var(gi, 2)
      r1i = nx_eqsat_add_binary(gi, NX_EQ_OP_ADD, w, w)            // add_self
      let zz: i64 = nx_eqsat_add_var(gi, 3)
      nx_eqsat_add_binary(gi, NX_EQ_OP_AND, zz, zz)               // and_self
      let u: i64 = nx_eqsat_add_var(gi, 4)
      let zc: i64 = nx_eqsat_add_const(gi, 0)
      nx_eqsat_add_binary(gi, NX_EQ_OP_OR, u, zc)                 // or_zero
      let v: i64 = nx_eqsat_add_var(gi, 5)
      let one: i64 = nx_eqsat_add_const(gi, 1)
      nx_eqsat_add_binary(gi, NX_EQ_OP_MUL, v, one)              // mul_one
      let c16: i64 = nx_eqsat_add_const(gi, 16)
      nx_eqsat_add_binary(gi, NX_EQ_OP_MUL, v, c16)             // mul_pow2 (k=4)
  }
  let sati: i64 = nx_eqsat_saturate(gi, 16)
  nx_eqsat_recompute_best(gi)
  let bni0: i64 = nx_eqsat_extract_best_node(gi, r0i)
  let opi0: i64 = gi.nodes[bni0].op
  let costi0: i64 = nx_eqsat_best_cost(gi, r0i)
  let memi: i64 = if nx_eqsat_find(gi, r0i) == nx_eqsat_find(gi, r1i) then 1 else 0
  let histi: *i64 = sys_mmap(NX_EQSAT_RULE_N * 8) as *i64
  _log_hist(gi, histi)
  let nprovi: i64 = gi.n_prov
158
  // ---------- DSL path (SAME graph, opt-in table) ----------
  let gd: *NxEGraph = _mk_graph(cap_nodes, cap_cls)
  let plogd: *i64 = sys_mmap(256 * 8) as *i64
  nx_eqsat_enable_prov(gd, plogd, 256)
  let table: *NxDslRule = _mk_table(0)            // 7 builtins only (parity set)
  nx_eqsat_enable_dsl(gd, table, 7, 16)
  var r0d: i64 = 0 - 1
  var r1d: i64 = 0 - 1
  if graph_kind == 1 {
      let x: i64 = nx_eqsat_add_var(gd, 0)
      let mxx: i64 = nx_eqsat_add_binary(gd, NX_EQ_OP_MUL, x, x)
      let z: i64 = nx_eqsat_add_const(gd, 0)
      r0d = nx_eqsat_add_binary(gd, NX_EQ_OP_ADD, mxx, z)
      r1d = mxx
  }
  if graph_kind == 2 {
      let x: i64 = nx_eqsat_add_var(gd, 0)
      let c8: i64 = nx_eqsat_add_const(gd, 8)
      r0d = nx_eqsat_add_binary(gd, NX_EQ_OP_MUL, x, c8)
      r1d = r0d
  }
  if graph_kind == 3 {
      let y: i64 = nx_eqsat_add_var(gd, 1)
      let suby: i64 = nx_eqsat_add_binary(gd, NX_EQ_OP_SUB, y, y)
      let z0: i64 = nx_eqsat_add_const(gd, 0)
      r0d = nx_eqsat_add_binary(gd, NX_EQ_OP_ADD, suby, z0)
      let w: i64 = nx_eqsat_add_var(gd, 2)
      r1d = nx_eqsat_add_binary(gd, NX_EQ_OP_ADD, w, w)
      let zz: i64 = nx_eqsat_add_var(gd, 3)
      nx_eqsat_add_binary(gd, NX_EQ_OP_AND, zz, zz)
      let u: i64 = nx_eqsat_add_var(gd, 4)
      let zc: i64 = nx_eqsat_add_const(gd, 0)
      nx_eqsat_add_binary(gd, NX_EQ_OP_OR, u, zc)
      let v: i64 = nx_eqsat_add_var(gd, 5)
      let one: i64 = nx_eqsat_add_const(gd, 1)
      nx_eqsat_add_binary(gd, NX_EQ_OP_MUL, v, one)
      let c16: i64 = nx_eqsat_add_const(gd, 16)
      nx_eqsat_add_binary(gd, NX_EQ_OP_MUL, v, c16)
  }
  let satd: i64 = nx_eqsat_saturate(gd, 16)
  nx_eqsat_recompute_best(gd)
  let bnd0: i64 = nx_eqsat_extract_best_node(gd, r0d)
  let opd0: i64 = gd.nodes[bnd0].op
  let costd0: i64 = nx_eqsat_best_cost(gd, r0d)
  let memd: i64 = if nx_eqsat_find(gd, r0d) == nx_eqsat_find(gd, r1d) then 1 else 0
  let histd: *i64 = sys_mmap(NX_EQSAT_RULE_N * 8) as *i64
  _log_hist(gd, histd)
  let nprovd: i64 = gd.n_prov
207
  // ---------- compare every observable facet ----------
  if sati != satd { return 0 }            // same saturate return code
  if opi0 != opd0 { return 0 }            // same extracted root op
  if costi0 != costd0 { return 0 }        // same extracted cost
  if memi != memd { return 0 }            // same canonical partition (root pair)
  if nprovi != nprovd { return 0 }        // same number of logged merges
  if _hist_eq(histi, histd) != 1 { return 0 }   // same logged-rule-id MULTISET
  return 1
216}
217
218func main() -> i64 {
  // MIGRATED OFF A HAND-ROLLED VERDICT 2026-08-14, and NEVER COMPILED BEFORE THAT DAY -- nx_eqsat.nx
  // itself did not compile, so this proof and its siblings had all sat on disk unbuilt. The teeth were
  // already among the strongest in the estate; they had no way to report to anything outside the process,
  // and an exit-code-as-assertion-number protocol stops at the FIRST failure and hides the rest.
  gv_head("nx_eqsat DSL-parity gate -- the data-driven rule table is behaviourally identical to the hand-written rules" as *u8)
  let ctr: *i64 = gv_ctr()
225
  // shared gsim scratch for the soundness battery
  let vals: *i64 = sys_mmap(64 * 8) as *i64
  let cells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell
  let gs: *NxGsim = sys_mmap(64) as *NxGsim
230
  // STEP 0: lockstep (engine ids == membership ids, incl the new xor_self id 9).
  let lockstep: i64 = mp_rule_ids_lockstep()
233
  // ===================== STEP 1-3: behavioral PARITY ========================
  let p1: i64 = _parity(1)
  let p2: i64 = _parity(2)
  let p3: i64 = _parity(3)
238
  // ===================== STEP 4: NEW RULE soundness battery =================
  // The W=8 masked exhaustive two-witness battery for xor_self MUST be unanimous;
  // this is what JUSTIFIES admitting MP_RULE_XOR_SELF to the proven-sound set.
  let t: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(t)
  let xor_total: i64 = mp_battery_xor_self(gs, vals, cells, t)
  let xor_passed: i64 = t.passed
246
  // ===================== STEP 5: NEW RULE applied + CERTIFIED ===============
  // Build (xor v v), enable prov + DSL with the 8-row table, run the REAL
  // saturator. The e-matcher merges the xor-class with const-0 citing id 9.
  let cap_nodes: i64 = 64
  let cap_cls: i64 = 64
  let g5: *NxEGraph = _mk_graph(cap_nodes, cap_cls)
  let plog5: *i64 = sys_mmap(64 * 8) as *i64
  if nx_eqsat_enable_prov(g5, plog5, 64) != NX_EQSAT_OK { sys_exit(50); return 50 }
  let table8: *NxDslRule = _mk_table(1)      // 7 builtins + xor_self
  if nx_eqsat_enable_dsl(g5, table8, 8, 16) != NX_EQSAT_OK { sys_exit(51); return 51 }
  let v: i64 = nx_eqsat_add_var(g5, 0)
  let xorvv: i64 = nx_eqsat_add_binary(g5, NX_EQ_OP_XOR, v, v)    // (xor v v)
  let zero5: i64 = nx_eqsat_add_const(g5, 0)                      // 0
  // pre-merge: distinct classes
  // ANTI-VACUITY: if the xor class were ALREADY merged with zero before saturation, the whole of
  // STEP 5 would prove nothing about the DSL rule.
  var pre5_distinct: i64 = 1
  if nx_eqsat_find(g5, xorvv) == nx_eqsat_find(g5, zero5) { pre5_distinct = 0 }
  let sat5: i64 = nx_eqsat_saturate(g5, 16)
  var sat5_fixpoint: i64 = 0
  if sat5 == NX_EQSAT_SATURATED { sat5_fixpoint = 1 }
  // certify (xor v v) == 0 strictly from the engine's log.
  let cert5: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let xor_cert: i64 = mp_certify_live(g5, xorvv, zero5, cert5)
  // values captured; asserted as teeth at the end so EVERY one is reported in a single run
  // the logged merge cited id 9 (xor_self), proving the DSL rule fired.
  var saw_xor: i64 = 0
  var qi: i64 = 0
  while qi < g5.n_prov { if g5.prov[qi] == NX_EQSAT_RULE_XOR_SELF { saw_xor = 1 } qi = qi + 1 }
  // saw_xor asserted as a tooth below
277
  // ===================== STEP 6: NEGATIVE CONTROL (load-bearing) ============
  // (6a) An UN-admitted rule id in the log must REFUSE the certificate. Forge a
  // log on a fresh graph whose only "merge" cites a bogus id (200) and assert the
  // certifier's log scan refuses it. This is the same poison path RULE_NONE uses.
  let g6: *NxEGraph = _mk_graph(cap_nodes, cap_cls)
  let plog6: *i64 = sys_mmap(64 * 8) as *i64
  nx_eqsat_enable_prov(g6, plog6, 64)
  // hand-forge ONE un-admitted citation directly into the live log buffer.
  plog6[0] = 200            // an id NOT in the proven-sound allow-list
  g6.n_prov = 1
  let neg_scan: i64 = mp_log_all_sound(g6)        // must be 0 (refused)
  // (6b) prove the allow-list arm is load-bearing: mp_is_sound_rule on a bogus id
  // is 0, so had xor_self's id NOT been admitted (battery never run), certify would
  // refute -- the membership check is a real consequence of admission, not free.
  let bogus_sound: i64 = mp_is_sound_rule(200)    // must be 0
  let xor_admitted: i64 = mp_is_sound_rule(NX_EQSAT_RULE_XOR_SELF)  // must be 1 (after battery)
  var neg_refused: i64 = 0
  if neg_scan == 0 { if bogus_sound == 0 { if xor_admitted == 1 { neg_refused = 1 } } }
296
  // ===================== known answer + FAIL-LOUD ==========================
  _emit_num(p1); _emit_num(p2); _emit_num(p3);
  _emit_num(xor_passed); _emit_num(xor_total); _emit_num(xor_cert); _emit_num(neg_refused); _nl()
300
  gv_check("engine rule ids and membership-prover ids are in lockstep" as *u8, lockstep == 1, ctr)
  // THE PARITY RESULT: the data-driven table and the hand-written inline rules produce the SAME
  // merge history, across three graph shapes. This is what lets rules become DATA without becoming
  // a second, differently-behaved engine.
  gv_check("DSL and inline rules agree on graph shape 1" as *u8, p1 == 1, ctr)
  gv_check("DSL and inline rules agree on graph shape 2" as *u8, p2 == 1, ctr)
  gv_check("DSL and inline rules agree on the rule-dense shape" as *u8, p3 == 1, ctr)
  // ADMISSION BY PROOF: the new rule is allowed into the sound set only because an exhaustive
  // two-witness battery was unanimous over the whole masked domain.
  gv_check("the xor-self battery swept the full 2^W vector domain" as *u8, xor_total == 256, ctr)
  gv_check("every vector in the battery passed on BOTH witnesses" as *u8, xor_passed == xor_total, ctr)
  // THE NEW RULE, END TO END: distinct before, merged after, cited, certified.
  gv_check("pre-state: the xor class and zero start in DIFFERENT classes" as *u8, pre5_distinct == 1, ctr)
  gv_check("saturation reached a fixpoint" as *u8, sat5_fixpoint == 1, ctr)
  gv_check("the xor class really was merged with zero" as *u8, cert5.member == 1, ctr)
  gv_check("every id in the log is sound, including the newly admitted one" as *u8, cert5.sound == 1, ctr)
  gv_check("the equivalence CERTIFIES from the log alone" as *u8, xor_cert == 1, ctr)
  gv_check("a real merge was actually logged" as *u8, g5.n_prov >= 1, ctr)
  gv_check("the provenance log is complete, not overflowed" as *u8, g5.prov_overflow == 0, ctr)
  gv_check("the logged merge cites the DSL rule, proving the data-driven path fired" as *u8, saw_xor == 1, ctr)
  // THE LOAD-BEARING CONTROL. Without it every tooth above would pass for a certifier that
  // approved anything: a hand-forged citation of an UN-ADMITTED rule id must be refused, the bogus
  // id must not be in the allow-list, and the new rule must be there only because its battery ran.
  gv_check("neg-control-a-forged-unadmitted-citation-is-REFUSED-by-the-certifier" as *u8, neg_refused == 1, ctr)
325
  return gv_verdict("nx_eqsat_dsl_parity_test" as *u8, ctr,
      "data-driven rule table proven behaviourally identical to the hand-written rules on three shapes, plus one genuinely new rule admitted only after an exhaustive battery, applied through the DSL, cited and certified, against a forged-citation control" as *u8)
328}
nx_eqsat_dsl_parity_test.nx source

`nx_eqsat_dsl_parity_test.nx` source
