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

↩ module page · 301 lines · 15359 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_eqsat_membership_proof.nx"
41
42func _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
49}
50func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
51
52// Per-rule-id histogram of a provenance log (ids 0..MP_RULE_N-1). Used to compare
53// the inline vs DSL logged-rule-id MULTISET exactly (order-independent equality).
54func _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
64}
65
66func _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
73}
74
75// Fresh e-graph factory (caller owns scratch via mmap). Returns the graph ptr.
76func _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(256) as *NxEGraph
  nx_eqsat_init(g, nodes, cap_nodes, classes, cap_cls)
  return g
82}
83
84// Build the 7-row builtin table + (optionally) append xor_self as an 8th row.
85func _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
96}
97
98// Run ONE parity comparison: build the SAME graph twice (inline path then DSL
99// path), saturate both with provenance ON, and assert identical observable result.
100// graph_kind selects which input to build. Returns 1 iff every facet agrees.
101func _parity(graph_kind: i64) -> i64 {
  let cap_nodes: i64 = 256
  let cap_cls: i64 = 256
104
  // ---------- 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
157
  // ---------- 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
206
  // ---------- 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
215}
216
217func main() -> i64 {
  // 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
222
  // STEP 0: lockstep (engine ids == membership ids, incl the new xor_self id 9).
  if mp_rule_ids_lockstep() != 1 { sys_exit(70); return 70 }
225
  // ===================== STEP 1-3: behavioral PARITY ========================
  let p1: i64 = _parity(1)
  let p2: i64 = _parity(2)
  let p3: i64 = _parity(3)
230
  // ===================== 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
238
  // ===================== 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
  if nx_eqsat_find(g5, xorvv) == nx_eqsat_find(g5, zero5) { sys_exit(52); return 52 }
  let sat5: i64 = nx_eqsat_saturate(g5, 16)
  if sat5 != NX_EQSAT_SATURATED { sys_exit(53); return 53 }
  // 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)
  if cert5.member != 1 { sys_exit(54); return 54 }   // xor-class merged with 0
  if cert5.sound  != 1 { sys_exit(55); return 55 }   // every logged id sound (incl 9)
  if xor_cert != 1     { sys_exit(56); return 56 }   // CERTIFIED via membership-as-proof
  if g5.n_prov < 1     { sys_exit(57); return 57 }   // a real merge WAS logged
  if g5.prov_overflow != 0 { sys_exit(58); return 58 }
  // 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 }
  if saw_xor != 1 { sys_exit(59); return 59 }
269
  // ===================== 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 } } }
288
  // ===================== 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()
292
  if p1 != 1 { sys_exit(1); return 1 }                 // parity Case 1
  if p2 != 1 { sys_exit(2); return 2 }                 // parity Case 2
  if p3 != 1 { sys_exit(3); return 3 }                 // parity rule-dense
  if xor_total != 256 { sys_exit(4); return 4 }        // 2^W vectors swept
  if xor_passed != xor_total { sys_exit(5); return 5 } // every vector both-witness pass
  if xor_cert != 1 { sys_exit(6); return 6 }           // new rule CERTIFIED live
  if neg_refused != 1 { sys_exit(7); return 7 }        // negative control: unproven => refused
  sys_exit(0); return 0
301}
nx_eqsat_dsl_parity_test.nx source

`nx_eqsat_dsl_parity_test.nx` source
