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

↩ module page · 148 lines · 9007 B
1// nx_memvel_gate.nx -- referee for the SUSTAINED-GROWER predicate (rm_sustained_count), 2026-08-14.
2//
3// WHY THIS GATE EXISTS: nx_memvel had no referee at all, and the column its own header calls decisive
4// (grew_in = k/N) was printed PER ROW and never totalled, so no caller could branch on it. Every
5// consumer therefore fell back to nx_resmon's leak census, which is a SNAPSHOT relation
6// (VmSize==VmPeak) -- a LEVEL, and a level cannot express a leak. Measured on this box the same day:
7// 17 leak suspects against a red threshold of 6, so nx_resmon was RED PERMANENTLY, while the true
8// sustained-grower count was 0 in back-to-back runs.
9//
10// THE TOOTH THAT MATTERS IS T7. It asserts the two predicates DISAGREE on the shape that caused this
11// work: the screen calls nx_hub_gw a candidate, the velocity predicate clears it. A change that reduced
12// rm_sustained_count to echoing the screen would pass every other tooth here and fail only T7 -- and
13// that echo is precisely the defect this work removed.
14//
15// Every input is synthetic: no /proc, no fixture on disk, no added load, deterministic by construction.
16// license_tier: ORIGINAL  expect_exit: 0
17import "nx_syscalls.nx"
18import "nx_gate_verdict.nx"
19import "nx_resmon_lib.nx"
20import "nx_ctxtop_lib.nx"   // ct_admit / ct_admit_runq -- the admission rulers T10-T13 pin
21
22func main() -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_memvel_gate -- sustained-grower predicate: the sufficient half of the leak question" as *u8)
25
  let rounds: i64 = 5
27
  // FIXTURE A -- four processes. idx0 grew in EVERY window (a real leak). idx1 is the synoelasticd
  // shape actually measured 2026-08-14 (3396 kB/s, grew_in=4/5): a 200 MB/min headline that is NOT a
  // leak. idx2 never grew, idx3 grew once. Both signals live in ONE array so the teeth below prove
  // DISCRIMINATION rather than two isolated runs that each see only what they were built to see.
  let a: *i64 = sys_mmap(8 * 8) as *i64
  a[0] = 5
  a[1] = 4
  a[2] = 0
  a[3] = 1
37
  // T1 -- ASSERT THE FIXTURE REACHED THE CONDITION before asserting any outcome from it.
  // A fixture the defect cannot fail is not a test.
  var t1: i64 = 0
  if a[0] == rounds { t1 = 1 }
  gv_check("T1 fixture-reached-condition: a planted grower with k==N is really present" as *u8, t1, ctr)
43
  // T2 -- THE PLANTED KNOWN-BAD IS FOUND. A counter that has only ever returned zero is unverified.
  var t2: i64 = 0
  if rm_sustained_count(a, 4, rounds) == 1 { t2 = 1 }
  gv_check("T2 planted-known-bad: exactly the k==N process is counted, out of 4 present" as *u8, t2, ctr)
48
  // FIXTURE B -- the rotating top slot only: nothing reached every window.
  let b: *i64 = sys_mmap(8 * 8) as *i64
  b[0] = 4
  b[1] = 4
  b[2] = 3
54
  // T3 -- neg-control-rotating-top-slot: the real measured population must count ZERO.
  var t3: i64 = 0
  if rm_sustained_count(b, 3, rounds) == 0 { t3 = 1 }
  gv_check("T3 neg-control-rotating-top-slot: k less than N in every row counts zero" as *u8, t3, ctr)
59
  // T4 -- an empty population answers ZERO, and that zero is an ANSWER.
  var t4: i64 = 0
  if rm_sustained_count(a, 0, rounds) == 0 { t4 = 1 }
  gv_check("T4 empty population answers 0 (nothing grew), not an error" as *u8, t4, ctr)
64
  // T5 -- THIRD STATE. Zero observed windows cannot answer the question at all, and that must be
  // DISTINGUISHABLE from T4's honest zero: I could not look is not I looked and found nothing.
  var t5: i64 = 0
  if rm_sustained_count(a, 4, 0) == 0 - 1 { t5 = 1 }
  gv_check("T5 third-state: zero windows returns UNOBSERVABLE, never a confident zero" as *u8, t5, ctr)
70
  // T6 -- the window count is really READ, not baked in. The SAME array that counts 0 at N=5 must
  // count 2 at N=4. A predicate that ignored its rounds argument would still pass T2 and T3.
  var t6: i64 = 0
  if rm_sustained_count(b, 3, 4) == 2 { t6 = 1 }
  gv_check("T6 window-count-is-live: same array counts 0 at N=5 and 2 at N=4" as *u8, t6, ctr)
76
  // T7 -- ANTI-VACUITY, THE DEFECT ITSELF. nx_hub_gw: VmSize==VmPeak with 2.2 GiB committed. The
  // SCREEN must call it a candidate (it is necessary-not-sufficient and correct to do so) while its
  // flat growth record clears it. The two predicates MUST disagree here. The trivial wrong
  // implementation -- velocity echoes the screen -- is the one thing this tooth cannot accept.
  let c: *i64 = sys_mmap(8 * 8) as *i64
  c[0] = 0
  let screen: i64 = rm_is_leaker(6903268, 6903268, 161228, 2111640, 262144)
  let velocity: i64 = rm_sustained_count(c, 1, rounds)
  var t7: i64 = 0
  if screen == 1 { if velocity == 0 { t7 = 1 } }
  gv_check("T7 anti-vacuity: screen says CANDIDATE and velocity says NOT-A-LEAK on one process" as *u8, t7, ctr)
88
  // T8 -- THE ROUND TRIP, and this is the tooth that would have caught the real defect. The status
  // file is WRITTEN by nx_memvel and PARSED by nx_resmon using rm_field, which is LINE-ANCHORED
  // ("first integer on the line that STARTS with key"). The first implementation put all six fields
  // on ONE line: epoch= parsed, every later field returned -1, and nx_resmon reported the leak axis
  // UNOBSERVABLE while holding a perfectly valid file. ★★★★★★A PRODUCER AND A CONSUMER THAT ARE EACH
  // CORRECT IN ISOLATION CAN STILL DISAGREE ON THE WIRE, AND ONLY A ROUND-TRIP TOOTH SEES THE WIRE.
  // Checking the LAST fields is the anti-vacuity part: a single-line regression still parses the FIRST.
  let sfx: *u8 = sys_mmap(256)
  let lit: *u8 = "epoch=1786735678\nsustained=2\nkbps=41\nrounds=5\nprocs=560\ncoverage=1\n" as *u8
  var q: i64 = 0
  while lit[q] != (0 as u8) { sfx[q] = lit[q]; q = q + 1 }
  sfx[q] = 0 as u8
  var t8: i64 = 0
  if rm_field(sfx, q, "epoch=" as *u8) == 1786735678 {
  if rm_field(sfx, q, "sustained=" as *u8) == 2 {
  if rm_field(sfx, q, "kbps=" as *u8) == 41 {
  if rm_field(sfx, q, "procs=" as *u8) == 560 {
  if rm_field(sfx, q, "coverage=" as *u8) == 1 { t8 = 1 } } } } }
  gv_check("T8 round-trip: EVERY status field parses, not just the first on its line" as *u8, t8, ctr)
108
  // T9 neg-control-single-line-is-rejected: the EXACT shape of the defect must NOT parse. Without
  // this, T8 could pass on a format that happens to work while the broken one also silently "works".
  let bad: *u8 = sys_mmap(256)
  let blit: *u8 = "epoch=1786735678 sustained=2 kbps=41\n" as *u8
  var bq: i64 = 0
  while blit[bq] != (0 as u8) { bad[bq] = blit[bq]; bq = bq + 1 }
  bad[bq] = 0 as u8
  var t9: i64 = 0
  if rm_field(bad, bq, "epoch=" as *u8) == 1786735678 { if rm_field(bad, bq, "sustained=" as *u8) == 0 - 1 { t9 = 1 } }
  gv_check("T9 neg-control-single-line: a space-packed line parses field 1 and LOSES the rest" as *u8, t9, ctr)
119
  // ---- ADMISSION AXIS (2026-08-21): the ruler deciding whether this organ runs AT ALL ----
  // THE INCIDENT THESE PIN: nx_memvel gated on /proc/loadavg (ct_admit) against a bar of 800. On this
  // NAS loadavg counts RAID D-state and sits at 1000-2000 while procs_running is 1-3 of 8, so the LEAK
  // detector -- the LEADING indicator -- was refused CONTINUOUSLY for 7.4 h while swap climbed to 812
  // permil past its 700 bar. Measured A/B on ONE box state (procs_running=1, load1=15.49): the loadavg
  // ruler REFUSED (exit 4), the run-queue ruler RAN (exit 0, 422 procs, 6 growers).
  var t10: i64 = 0
  if ct_admit_runq(1, 8) == 1 { t10 = 1 }
  gv_check("T10 the-regression-case: CPU idle (run 1 of 8) ADMITS -- the exact input that stayed dark 7.4h" as *u8, t10, ctr)
129
  var t11: i64 = 0
  if ct_admit_runq(8, 8) == 0 { if ct_admit_runq(7, 8) == 1 { t11 = 1 } }
  gv_check("T11 boundary: run==ncpu REFUSES and run==ncpu-1 ADMITS (saturation is >=, not >)" as *u8, t11, ctr)
133
  var t12: i64 = 0
  if ct_admit_runq(0 - 1, 8) == 0 { if ct_admit_runq(1, 0) == 0 { if ct_admit_runq(1, 0 - 1) == 0 { t12 = 1 } } }
  gv_check("T12 neg-control-fail-closed: an unreadable run queue OR an unreadable ncpu REFUSES, never admits" as *u8, t12, ctr)
137
  // T13 ANTI-VACUITY. T10 alone passes against a ruler that admits EVERYTHING; T11/T12 kill that, but
  // a ruler that merely COPIED ct_admit would still pass all three. This asserts the two rulers
  // DISAGREE on the exact measured inputs, in the measured direction: the retired axis refuses what
  // the new axis admits. Both are evaluated here, so the claim cannot rot into a one-sided assertion.
  var t13: i64 = 0
  if ct_admit(1549, 800) == 0 { if ct_admit_runq(1, 8) == 1 { t13 = 1 } }
  gv_check("T13 anti-vacuity: the retired loadavg ruler REFUSES the very inputs the run-queue ruler ADMITS" as *u8, t13, ctr)
145
  let rc: i64 = gv_verdict("MEMVEL-GATE" as *u8, ctr, "planted k==N found, 4-of-5 rejected, third state distinct from an honest zero, rounds proven live, and the screen-versus-velocity disagreement pinned" as *u8)
  return rc
148}
nx_memvel_gate.nx source

`nx_memvel_gate.nx` source
