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

↩ module page · 320 lines · 19765 B
1// nx_eqsat_membership_proof_test.nx -- proves the MEMBERSHIP-AS-PROOF
2// CERTIFICATE for (mul x 8) == (shl x 3), and proves the certificate is
3// LOAD-BEARING (it FAILS when a non-sound rule is used or the endpoints are not
4// in the same e-class). FAIL LOUD known-answer; exit 0 iff every check holds.
5//
6// STRUCTURE (each step self-asserts; mismatch => sys_exit(nonzero)):
7//   STEP 1  SOUND SET: run the W=8 masked exhaustive battery for the SIX
8//           width-trivial unary rules + mul_pow2 in-range. Establishes the
9//           proven-sound set this run (total == 1536 + 2048 == 3584, all pass).
10//           BOTH witnesses (algebraic Witness A AND triangulated gsim Witness B)
11//           must agree on every vector. This is what JUSTIFIES the allow-list.
12//   STEP 0  LOCKSTEP: the membership organ's MP_RULE_* ids must equal the
13//           engine's NX_EQSAT_RULE_* (single source of truth) so the LIVE log
14//           the engine writes is never mislabeled against this allow-list.
15//   STEP 2  CERTIFICATE (positive, LIVE): build an e-graph, add (mul x 8) and
16//           (shl x 3), ENABLE provenance, run the REAL nx_eqsat_saturate (not a
17//           gated driver), and certify STRICTLY FROM THE LOG the engine wrote at
18//           its union chokepoint -- mul_pow2 fires at k=3<W, logs RULE_MUL_POW2,
19//           find(mul8)==find(shl3), every logged id sound + no overflow ->
20//           certified. This PROMOTES mul_pow2 into the proven-sound set, now
21//           exercised through the live engine + its k<W guard.
22//   STEP 3  LOAD-BEARING NEG-A (non-sound rule): the gated leg cites the BOGUS
23//           rule (mul x 3)==(shl x 1) -> recorder REFUSES + certificate FAILS;
24//           AND a LIVE leg -- the live engine has no bogus rule, so it never
25//           unions (mul x 4) with (shl x 1) => live membership/certificate FAIL.
26//   STEP 4  LOAD-BEARING NEG-B (endpoints not in same class): LIVE-certify
27//           (mul x 8) against (shl x 2) -- the live engine merges mul8 with
28//           (shl x 3), not (shl x 2), so membership FAILS and the certificate
29//           FAILS even though the log is sound.
30//   STEP 5  LOAD-BEARING NEG-C (k>=W boundary): the membership organ's
31//           k<MP_W side-condition (mp_mul_pow2_k_ok==0 at k==W) must REFUSE +
32//           FAIL the gated certificate; in the LIVE engine this class is
33//           discharged at union time by the k<NX_EQSAT_W guard (never logged).
34//   STEP 6  LOAD-BEARING NEG-D (log completeness): an UNDERSIZED prov buffer
35//           (cap=0) still lets the real merge happen (membership holds) but the
36//           overflow flag must POISON the certificate (FAIL CLOSED) -- a
37//           truncated log can never yield a passing-but-incomplete certificate.
38//
39// Known answer (FAIL LOUD): prints "<sound_passed> <sound_total> <cert> " where
40// sound_total==3584, sound_passed==3584, cert==1 (cert is now the LIVE
41// certificate). exit 0 iff all steps hold.
42
43import "nx_eqsat_membership_proof.nx"
44
45func _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
52}
53func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
54
55// Independent cross-check: does (mul x 2^k) == (shl x k) hold for ALL x mod 2^W,
56// evaluated on the gsim (masked) vs the doubling oracle? Returns passed vectors.
57// Used as defense-in-depth for the certified equivalence and for NEG-B failure.
58func _cross_check_pow2(g: *NxGsim, vals: *i64, cells: *NxGsimCell,
                     mul_const: i64, shl_amt: i64, oracle_k: i64,
                     t: *NxTriTally) -> i64 {
  let hi: i64 = mp_count()
  var x: i64 = 0
  while x < hi {
      let lhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_MUL, x, mul_const)
      let rhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_SHL, x, shl_amt)
      let oracle: i64 = _mp_oracle_double_k(x, oracle_k)
      let legs: *i64 = sys_mmap(2 * 8) as *i64
      legs[0] = lhs
      legs[1] = rhs
      let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict
      nx_tri_pass_strict(legs, 2, oracle, 2, v)
      nx_tri_tally_add(t, v, x)
      x = x + 1
  }
  return t.passed
76}
77
78func main() -> i64 {
  // shared gsim scratch (generous fixed caps; the netlists are tiny)
  let vals: *i64 = sys_mmap(64 * 8) as *i64
  let cells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell
  let g: *NxGsim = sys_mmap(64) as *NxGsim
83
  // ========================================================================
  // STEP 0: rule-id LOCKSTEP -- the membership organ's MP_RULE_* must match the
  // engine's NX_EQSAT_RULE_* exactly, or the live log the engine writes could be
  // mislabeled against this certifier's allow-list. (Defends the mislabel trap.)
  // ========================================================================
  if mp_rule_ids_lockstep() != 1 { sys_exit(70); return 70 }
90
  // ========================================================================
  // STEP 1: establish the SOUND SET via the W=8 masked exhaustive battery.
  // ========================================================================
  let t: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(t)
  var sound_total: i64 = 0
  sound_total = sound_total + mp_battery_unary(g, vals, cells, MP_RULE_ADD_ZERO, t)
  sound_total = sound_total + mp_battery_unary(g, vals, cells, MP_RULE_SUB_SELF, t)
  sound_total = sound_total + mp_battery_unary(g, vals, cells, MP_RULE_ADD_SELF, t)
  sound_total = sound_total + mp_battery_unary(g, vals, cells, MP_RULE_AND_SELF, t)
  sound_total = sound_total + mp_battery_unary(g, vals, cells, MP_RULE_OR_ZERO, t)
  sound_total = sound_total + mp_battery_unary(g, vals, cells, MP_RULE_MUL_ONE, t)
  let pow2_total: i64 = mp_battery_mul_pow2_inrange(g, vals, cells, t)
  sound_total = sound_total + pow2_total
105
  let sound_passed: i64 = t.passed
  // six unary rules each sweep 2^W = 256 vectors -> 1536; mul_pow2 = 256*8 = 2048
  let expect_total: i64 = 6 * mp_count() + mp_count() * MP_W
109
  // ========================================================================
  // STEP 2: the MEMBERSHIP-AS-PROOF CERTIFICATE (positive) for mul x 8 == shl x 3.
  // ========================================================================
  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(96) as *NxEGraph
  if nx_eqsat_init(eg, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { sys_exit(30); return 30 }
119
  let vx: i64 = nx_eqsat_add_var(eg, 0)              // x
  let c8: i64 = nx_eqsat_add_const(eg, 8)            // 8 = 2^3
  let c3: i64 = nx_eqsat_add_const(eg, 3)            // 3
  let mul8: i64 = nx_eqsat_add_binary(eg, NX_EQ_OP_MUL, vx, c8)   // (mul x 8)
  let shl3: i64 = nx_eqsat_add_binary(eg, NX_EQ_OP_SHL, vx, c3)   // (shl x 3)
125
  // Pre-merge: distinct e-classes (membership must NOT yet hold).
  if nx_eqsat_find(eg, mul8) == nx_eqsat_find(eg, shl3) { sys_exit(31); return 31 }
128
  // LIVE saturation: enable provenance, run the REAL engine (NOT a gated driver),
  // and certify STRICTLY FROM THE LOG the engine wrote at its union chokepoint.
  // mul_pow2 fires at k=3<W (its k<W guard admits it) and merges mul8 with shl3,
  // logging RULE_MUL_POW2 -- the ONLY real merge on this graph. This PROMOTES
  // mul_pow2 into the proven-sound set, exercised through the live engine.
  let plog: *i64 = sys_mmap(64 * 8) as *i64
  if nx_eqsat_enable_prov(eg, plog, 64) != NX_EQSAT_OK { sys_exit(32); return 32 }
  let sat2: i64 = nx_eqsat_saturate(eg, 16)
  if sat2 != NX_EQSAT_SATURATED { sys_exit(38); return 38 }   // engine converged
138
  let cert: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok: i64 = mp_certify_live(eg, mul8, shl3, cert)
  if cert.member != 1 { sys_exit(33); return 33 }    // MEMBERSHIP holds (live find==find)
  if cert.sound != 1  { sys_exit(34); return 34 }    // PROVENANCE: all logged ids sound
  if cok != 1         { sys_exit(35); return 35 }    // CERTIFIED (live)
  // The live engine logged at least the mul_pow2 merge, all sound, no overflow.
  if eg.n_prov < 1        { sys_exit(39); return 39 }   // a real merge WAS logged
  if eg.prov_overflow != 0 { sys_exit(47); return 47 }  // log did not overflow
147
  // Cross-check the SAME equivalence with a fresh triangulation battery.
  let tc: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(tc)
  let cc_passed: i64 = _cross_check_pow2(g, vals, cells, 8, 3, 3, tc)
  if tc.total != mp_count() { sys_exit(36); return 36 }
  if cc_passed != tc.total  { sys_exit(37); return 37 }  // defense in depth agrees
154
  // ========================================================================
  // STEP 3: LOAD-BEARING NEG-A -- a NON-sound rule must NOT certify.
  // ========================================================================
  // 3a: the bogus identity's own W=8 battery must DISAGREE (so it can never
  //     enter the sound set). (mul x 3) vs (shl x 1): false for almost all x.
  let tb: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(tb)
  // oracle = true (x*3) mod 2^W via doublings is NOT a power-of-two; build it
  // directly so the oracle is the honest value, and BOTH legs (mul x 3, shl x 1)
  // are checked against it -- they will diverge.
  let hi: i64 = mp_count()
  var bx: i64 = 0
  while bx < hi {
      let blhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_MUL, bx, 3)
      let brhs: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_SHL, bx, 1)
      let boracle: i64 = ((bx & mp_mask()) * 3) & mp_mask()   // honest (x*3) mod 2^W
      let blegs: *i64 = sys_mmap(2 * 8) as *i64
      blegs[0] = blhs
      blegs[1] = brhs
      let bv: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict
      nx_tri_pass_strict(blegs, 2, boracle, 2, bv)
      nx_tri_tally_add(tb, bv, bx)
      bx = bx + 1
  }
  // The bogus identity MUST fail the battery (not all vectors agree).
  if tb.passed == tb.total { sys_exit(40); return 40 }   // bogus must NOT be sound
  // The bogus rule id must NOT be in the proven-sound allow-list.
  if mp_is_sound_rule(MP_RULE_BOGUS_MUL3) != 0 { sys_exit(41); return 41 }
183
  // 3b: a gated saturation citing the bogus rule must REFUSE the merge and the
  //     certificate must FAIL. Use a fresh e-graph with (mul x 4) and (shl x 1).
  let nodes2: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let classes2: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg2: *NxEGraph = sys_mmap(96) as *NxEGraph
  if nx_eqsat_init(eg2, nodes2, cap_nodes, classes2, cap_cls) != NX_EQSAT_OK { sys_exit(42); return 42 }
  let vx2: i64 = nx_eqsat_add_var(eg2, 0)
  let c4b: i64 = nx_eqsat_add_const(eg2, 4)
  let c1b: i64 = nx_eqsat_add_const(eg2, 1)
  let mul4: i64 = nx_eqsat_add_binary(eg2, NX_EQ_OP_MUL, vx2, c4b)
  let shl1: i64 = nx_eqsat_add_binary(eg2, NX_EQ_OP_SHL, vx2, c1b)
  let prov2: *NxMpProvenance = sys_mmap(64) as *NxMpProvenance
  mp_prov_init(prov2)
  // Cite the BOGUS rule -- the recorder must refuse + poison the certificate.
  let admitted2: i64 = mp_prov_admit_union(prov2, eg2, mul4, shl1, MP_RULE_BOGUS_MUL3, 1)
  if admitted2 != 0 { sys_exit(43); return 43 }      // bogus union must be REFUSED
  if prov2.all_sound != 0 { sys_exit(44); return 44 } // provenance poisoned
  if prov2.bad_rule != MP_RULE_BOGUS_MUL3 { sys_exit(45); return 45 }
  let cert2: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok2: i64 = mp_certify(eg2, mul4, shl1, prov2, cert2)
  if cok2 != 0 { sys_exit(46); return 46 }           // certificate MUST fail (gated leg)
205
  // 3c: LIVE leg (belt-and-suspenders) -- the live engine has NO bogus rule, so
  // it can NEVER union (mul x 4) with (shl x 1) (the bogus claim is false; the
  // sound mul_pow2 would merge mul4 with SHL(x,2), not shl1). So live membership
  // FAILS => the live certificate FAILS, with a clean (all-sound) log.
  let plog2: *i64 = sys_mmap(64 * 8) as *i64
  if nx_eqsat_enable_prov(eg2, plog2, 64) != NX_EQSAT_OK { sys_exit(48); return 48 }
  nx_eqsat_saturate(eg2, 16)
  let cert2b: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok2b: i64 = mp_certify_live(eg2, mul4, shl1, cert2b)
  if cert2b.member != 0 { sys_exit(49); return 49 }  // live engine never merges them
  if cok2b != 0 { sys_exit(54); return 54 }          // live certificate MUST fail
217
  // ========================================================================
  // STEP 4: LOAD-BEARING NEG-B -- endpoints not in the same e-class.
  // ========================================================================
  // Certify (mul x 8) against (shl x 2): genuinely inequivalent (8 != 2^2).
  let nodes3: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let classes3: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg3: *NxEGraph = sys_mmap(96) as *NxEGraph
  if nx_eqsat_init(eg3, nodes3, cap_nodes, classes3, cap_cls) != NX_EQSAT_OK { sys_exit(50); return 50 }
  let vx3: i64 = nx_eqsat_add_var(eg3, 0)
  let c8c: i64 = nx_eqsat_add_const(eg3, 8)
  let c2c: i64 = nx_eqsat_add_const(eg3, 2)
  let mul8c: i64 = nx_eqsat_add_binary(eg3, NX_EQ_OP_MUL, vx3, c8c)
  let shl2c: i64 = nx_eqsat_add_binary(eg3, NX_EQ_OP_SHL, vx3, c2c)
  // LIVE: enable provenance + run the REAL saturator. mul_pow2 merges (mul x 8)
  // with (shl x 3), NOT (shl x 2) -- so mul8c and shl2c stay in distinct classes.
  // Membership FAILS => the live certificate FAILS, even though the log is sound.
  let plog3: *i64 = sys_mmap(64 * 8) as *i64
  if nx_eqsat_enable_prov(eg3, plog3, 64) != NX_EQSAT_OK { sys_exit(55); return 55 }
  nx_eqsat_saturate(eg3, 16)
  let cert3: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok3: i64 = mp_certify_live(eg3, mul8c, shl2c, cert3)
  if cert3.member != 0 { sys_exit(51); return 51 }   // membership MUST fail (live)
  if cok3 != 0 { sys_exit(52); return 52 }           // certificate MUST fail (live)
  // And the equivalence really is false: cross-check must DISAGREE.
  let td: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(td)
  _cross_check_pow2(g, vals, cells, 8, 2, 3, td)      // oracle = x*8, rhs = x<<2
  if td.passed == td.total { sys_exit(53); return 53 } // must NOT all agree
246
  // ========================================================================
  // STEP 5: LOAD-BEARING NEG-C -- mul_pow2 at k>=W boundary must be REFUSED.
  // ========================================================================
  // At k==W the masked equality MUL/SHL coincides (0==0), so an equality sweep
  // is BLIND to the bug -- but the k<W side-condition is not. The recorder must
  // refuse the merge and the certificate must fail.
  if mp_mul_pow2_k_ok(MP_W) != 0 { sys_exit(60); return 60 }     // k==W is not ok
  if mp_mul_pow2_k_ok(MP_W - 1) != 1 { sys_exit(61); return 61 } // k==W-1 is ok
  let nodes4: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let classes4: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg4: *NxEGraph = sys_mmap(96) as *NxEGraph
  if nx_eqsat_init(eg4, nodes4, cap_nodes, classes4, cap_cls) != NX_EQSAT_OK { sys_exit(62); return 62 }
  let vx4: i64 = nx_eqsat_add_var(eg4, 0)
  let c256: i64 = nx_eqsat_add_const(eg4, 256)       // 2^8 = 2^W
  let cW: i64 = nx_eqsat_add_const(eg4, MP_W)        // shift by W
  let mul256: i64 = nx_eqsat_add_binary(eg4, NX_EQ_OP_MUL, vx4, c256)
  let shlW: i64 = nx_eqsat_add_binary(eg4, NX_EQ_OP_SHL, vx4, cW)
  let prov4: *NxMpProvenance = sys_mmap(64) as *NxMpProvenance
  mp_prov_init(prov4)
  // Cite mul_pow2 but at k==W -- the side-condition must REFUSE it.
  let admitted4: i64 = mp_prov_admit_union(prov4, eg4, mul256, shlW, MP_RULE_MUL_POW2, MP_W)
  if admitted4 != 0 { sys_exit(63); return 63 }      // boundary union must be REFUSED
  if prov4.all_sound != 0 { sys_exit(64); return 64 }
  let cert4: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok4: i64 = mp_certify(eg4, mul256, shlW, prov4, cert4)
  if cok4 != 0 { sys_exit(65); return 65 }           // certificate MUST fail at boundary
  // Prove the equality sweep alone is BLIND here (masked MUL==SHL==0 at k=W):
  // x * 256 mod 256 == 0 and x << 8 mod 256 == 0 for all x in [0,256).
  var wx: i64 = 0
  var blind_agree: i64 = 0
  while wx < mp_count() {
      let wl: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_MUL, wx, 256)
      let wr: i64 = _mp_eval_op_const(g, vals, cells, NX_GATE_KIND_SHL, wx, MP_W)
      if wl == wr { if wl == 0 { blind_agree = blind_agree + 1 } }
      wx = wx + 1
  }
  if blind_agree != mp_count() { sys_exit(66); return 66 } // confirms equality is blind
284
  // ========================================================================
  // STEP 6: LOAD-BEARING NEG-D -- log COMPLETENESS. An UNDERSIZED provenance
  // buffer must FAIL CLOSED: the live engine still performs the real merge (so
  // membership holds), but the truncated/overflowed log must POISON the
  // certificate. A log that can silently drop entries would let an unsound
  // union beyond the cap slip through invisibly; this proves it cannot.
  // ========================================================================
  let nodes5: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode
  let classes5: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass
  let eg5: *NxEGraph = sys_mmap(96) as *NxEGraph
  if nx_eqsat_init(eg5, nodes5, cap_nodes, classes5, cap_cls) != NX_EQSAT_OK { sys_exit(67); return 67 }
  let vx5: i64 = nx_eqsat_add_var(eg5, 0)
  let c8e: i64 = nx_eqsat_add_const(eg5, 8)
  let c3e: i64 = nx_eqsat_add_const(eg5, 3)
  let mul8e: i64 = nx_eqsat_add_binary(eg5, NX_EQ_OP_MUL, vx5, c8e)
  let shl3e: i64 = nx_eqsat_add_binary(eg5, NX_EQ_OP_SHL, vx5, c3e)
  let plog5: *i64 = sys_mmap(8) as *i64
  // cap_prov = 0 -- the very first real merge cannot be logged -> overflow flag.
  if nx_eqsat_enable_prov(eg5, plog5, 0) != NX_EQSAT_OK { sys_exit(68); return 68 }
  nx_eqsat_saturate(eg5, 16)
  let cert5: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok5: i64 = mp_certify_live(eg5, mul8e, shl3e, cert5)
  if cert5.member != 1 { sys_exit(69); return 69 }       // the merge DID happen (membership holds)
  if eg5.prov_overflow != 1 { sys_exit(71); return 71 }  // log overflowed (fail-closed armed)
  if cert5.sound != 0 { sys_exit(72); return 72 }        // truncated log => NOT sound
  if cok5 != 0 { sys_exit(73); return 73 }               // certificate MUST fail closed
311
  // ========================================================================
  // FINAL known-answer gate (FAIL LOUD).
  // ========================================================================
  _emit_num(sound_passed); _emit_num(sound_total); _emit_num(cok); _nl()
  if sound_total != expect_total { sys_exit(1); return 1 }   // 3584 vectors swept
  if sound_passed != sound_total { sys_exit(2); return 2 }   // every vector both-witness pass
  if cok != 1 { sys_exit(3); return 3 }                       // positive certificate holds
  sys_exit(0); return 0
320}
nx_eqsat_membership_proof_test.nx source

`nx_eqsat_membership_proof_test.nx` source
