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

↩ module page · 354 lines · 22445 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_gate_verdict.nx"
44import "nx_eqsat_membership_proof.nx"
45
46func _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
53}
54func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
55
56// Independent cross-check: does (mul x 2^k) == (shl x k) hold for ALL x mod 2^W,
57// evaluated on the gsim (masked) vs the doubling oracle? Returns passed vectors.
58// Used as defense-in-depth for the certified equivalence and for NEG-B failure.
59func _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
77}
78
79func main() -> i64 {
  // MIGRATED OFF A HAND-ROLLED VERDICT 2026-08-14, and NEVER COMPILED BEFORE THAT DAY. This is the
  // deepest gate in the eqsat family -- four load-bearing negative controls against three positives --
  // and its exit-code-as-assertion-number protocol meant it stopped at the FIRST failure and reported
  // one number to a caller that could not read it.
  gv_head("nx_eqsat membership-as-proof gate -- a certificate that fails closed on every unsound path" as *u8)
  let ctr: *i64 = gv_ctr()
  // 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
90
  // ========================================================================
  // 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 }
97
  // ========================================================================
  // 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
112
  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
116
  // ========================================================================
  // 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(NX_EQSAT_GRAPH_BYTES) as *NxEGraph
  if nx_eqsat_init(eg, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { sys_exit(30); return 30 }
126
  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)
132
  // 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 }
135
  // 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
145
  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
154
  // 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
161
  // ========================================================================
  // 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 }
190
  // 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(NX_EQSAT_GRAPH_BYTES) 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)
  // captured; asserted as teeth at the end so a single run reports ALL of them
  let cert2: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok2: i64 = mp_certify(eg2, mul4, shl1, prov2, cert2)
  // cok2 asserted below
210
  // 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)
  // cert2b.member and cok2b asserted below
221
  // ========================================================================
  // 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(NX_EQSAT_GRAPH_BYTES) 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)
  // cert3.member and cok3 asserted below
  // 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
  // td.passed vs td.total asserted below
249
  // ========================================================================
  // 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.
  let k_at_W_ok: i64 = mp_mul_pow2_k_ok(MP_W)
  let k_below_W_ok: i64 = mp_mul_pow2_k_ok(MP_W - 1)
  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(NX_EQSAT_GRAPH_BYTES) 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)
  // admitted4 and prov4.all_sound asserted below
  let cert4: *NxMpCertificate = sys_mmap(64) as *NxMpCertificate
  let cok4: i64 = mp_certify(eg4, mul256, shlW, prov4, cert4)
  // cok4 asserted below
  // 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
  }
  // blind_agree asserted below -- this is the subtlest tooth in the file
286
  // ========================================================================
  // 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(NX_EQSAT_GRAPH_BYTES) 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)
  // cert5 / overflow / cok5 asserted below
310
  // ========================================================================
  // FINAL known-answer gate (FAIL LOUD).
  // ========================================================================
  _emit_num(sound_passed); _emit_num(sound_total); _emit_num(cok); _nl()
315
  // ---- THE POSITIVE. Every control below asserts a REFUSAL; without these three a certifier that
  // refused everything would score full marks on the whole file.
  gv_check("the soundness battery swept its full vector domain" as *u8, sound_total == expect_total, ctr)
  gv_check("every vector passed on BOTH witnesses" as *u8, sound_passed == sound_total, ctr)
  gv_check("the positive certificate for mul-by-8 equals shl-by-3 HOLDS" as *u8, cok == 1, ctr)
321
  // ---- NEG-A: a citation of a rule that was never proven sound.
  gv_check("neg-control-a-union-citing-an-unproven-rule-is-REFUSED-at-admission" as *u8, admitted2 == 0, ctr)
  gv_check("neg-control-the-refused-citation-POISONS-the-provenance" as *u8, prov2.all_sound == 0, ctr)
  gv_check("neg-control-the-poison-NAMES-the-offending-rule" as *u8, prov2.bad_rule == MP_RULE_BOGUS_MUL3, ctr)
  gv_check("neg-control-the-gated-certificate-FAILS-on-a-poisoned-log" as *u8, cok2 == 0, ctr)
  gv_check("neg-control-the-LIVE-engine-never-merges-the-falsely-claimed-pair" as *u8, cert2b.member == 0, ctr)
  gv_check("neg-control-the-live-certificate-FAILS-too" as *u8, cok2b == 0, ctr)
329
  // ---- NEG-B: endpoints that are genuinely inequivalent.
  gv_check("neg-control-membership-FAILS-for-inequivalent-endpoints" as *u8, cert3.member == 0, ctr)
  gv_check("neg-control-the-certificate-FAILS-even-though-the-log-is-clean" as *u8, cok3 == 0, ctr)
  gv_check("neg-control-the-independent-cross-check-DISAGREES-so-the-claim-really-is-false" as *u8, td.passed != td.total, ctr)
334
  // ---- NEG-C: the boundary the equality sweep cannot see. THIS IS THE SUBTLEST TOOTH HERE.
  // At k == W the masked values coincide -- x*2^W and x<<W are BOTH zero for every x -- so an
  // equality battery agrees on all 256 vectors and is therefore BLIND to the unsoundness. Only the
  // k < W side-condition catches it. A suite built purely on value comparison would pass this bug.
  gv_check("neg-control-the-rule-side-condition-REFUSES-k-equal-to-W" as *u8, k_at_W_ok == 0, ctr)
  gv_check("the same side-condition ACCEPTS k just below W, so it is not refusing everything" as *u8, k_below_W_ok == 1, ctr)
  gv_check("neg-control-a-boundary-union-is-REFUSED-at-admission" as *u8, admitted4 == 0, ctr)
  gv_check("neg-control-the-boundary-refusal-poisons-the-provenance" as *u8, prov4.all_sound == 0, ctr)
  gv_check("neg-control-the-boundary-certificate-FAILS" as *u8, cok4 == 0, ctr)
  gv_check("PROOF THE EQUALITY SWEEP IS BLIND AT THE BOUNDARY: both sides agree on every vector" as *u8, blind_agree == mp_count(), ctr)
345
  // ---- NEG-D: an undersized provenance log must fail CLOSED, not silently drop entries.
  gv_check("neg-control-the-merge-really-did-happen-so-membership-holds" as *u8, cert5.member == 1, ctr)
  gv_check("neg-control-an-undersized-log-raises-the-overflow-flag" as *u8, eg5.prov_overflow == 1, ctr)
  gv_check("neg-control-a-truncated-log-is-NOT-sound" as *u8, cert5.sound == 0, ctr)
  gv_check("neg-control-the-certificate-FAILS-CLOSED-on-a-truncated-log" as *u8, cok5 == 0, ctr)
351
  return gv_verdict("nx_eqsat_membership_proof_test" as *u8, ctr,
      "membership-as-proof certificate for mul-to-shl, against four load-bearing controls: an unproven rule id, inequivalent endpoints, the k=W boundary that a pure equality sweep is provably blind to, and an undersized log that must fail closed" as *u8)
354}
nx_eqsat_membership_proof_test.nx source

`nx_eqsat_membership_proof_test.nx` source
