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

↩ module page · 229 lines · 16495 B
1// nx_resmon_gate.nx -- referee for nx_resmon's two policy predicates (debt seq1005).
2//
3// It gates the SAME functions the organ runs (nx_resmon_lib.nx), not a reimplementation, and it needs
4// no /proc and no fixtures on disk -- every input is synthetic, so the result is deterministic.
5//
6// T2 AND T4 ARE THE TEETH THAT MATTER:
7//   T2 is the NON-VACUITY control: with thresholds set unreachably high, measurements that trip RED
8//      under real thresholds must return GREEN. If T2 ever fails, T1 is passing for free.
9//   T4 pins the EXACT false positive this instrument made on its first live run: a process with a huge
10//      RESERVED VmData but almost nothing committed reported a worst case of 40.6 GiB on a 36.9 GB box.
11//      A leaker is judged on rss+swap, never on reserved address space. That regression cannot return
12//      silently now.
13//
14// license_tier: ORIGINAL  expect_exit: 0
15import "nx_gate.nx"
16import "nx_gate_verdict.nx"
17import "nx_resmon_lib.nx"
18
19// The age this leak axis ACTUALLY reported on 2026-08-21: 7.2 h against a 900 s freshness bound, i.e.
20// ~43 consecutive missed 600 s beats, while the pressure axis sat amber at swap 754 permil.
21// ★NAMED FOR ITS PURPOSE -- "an observed age far past the bound" -- never for its digits, which is the
22// distinction the magic-number ratchet's own refusal text draws and which nx_magic's auto-hoist
23// (K_MAGIC_27259) cannot make for you. ★KEPT AT THE MEASURED VALUE so T8 regresses against the real
24// incident rather than against a round number somebody chose afterwards.
25const RG_STALE_AGE_OBSERVED_S: i64 = 27259
26
27// The blind-alarm fixtures below are DERIVED from the bound and the lib's OWN multiplier, never written
28// as digits: if RM_BLIND_ALARM_WINDOWS is ever retuned, these fixtures move with it and the test cannot
29// silently stop testing the threshold it names. A literal 1800 here would be a second copy of the policy's
30// shape, and the two drift the moment one side changes -- the same defect as a hand-counted length beside
31// a string literal.
32const RG_MAX_AGE_S: i64 = 900                                            // the declared memvel freshness bound
33const RG_BLIND_ALARM_AGE_S: i64 = RG_MAX_AGE_S * RM_BLIND_ALARM_WINDOWS  // DERIVED: exactly at the alarm
34const RG_BLIND_UNDER_ALARM_S: i64 = RG_BLIND_ALARM_AGE_S - 1             // DERIVED: one second short of it
35
36// (rg_row removed 2026-08-14: the shared base class renders the check rows now. A hand-rolled row
37//  printer beside gv_check is the duplicate-ruler defect, and leaving it defined-but-uncalled would
38//  show up as a fresh nx_unwired hit.)
39
40func main() -> i64 {
  // ---- T1: the verdict ladder moves with the thresholds (data-driven, not hardcoded) ----
  // same measurement (swap 934 permil, the real reading from the incident), three threshold sets.
  var t1: i64 = 0
  let g: i64 = rm_verdict(934, 500, 0, 1,  940, 990, 250, 100, 3, 6)   // below amber -> GREEN
  let a: i64 = rm_verdict(934, 500, 0, 1,  700, 990, 250, 100, 3, 6)   // over amber only -> AMBER
  let r: i64 = rm_verdict(934, 500, 0, 1,  700, 850, 250, 100, 3, 6)   // over red -> RED
  if g == 0 { if a == 1 { if r == 2 { t1 = 1 } } }
48
  // ---- T2 NON-VACUITY: unreachable thresholds must NOT flip the verdict ----
  // 934 permil swap, 23 leakers -- catastrophic in reality -- but no threshold can be crossed.
  var t2: i64 = 0
  if rm_verdict(934, 500, 23, 1, 9999, 9999, 0 - 1, 0 - 1, 9999, 9999) == 0 { t2 = 1 }
53
  // ---- T3: EACH axis can raise the verdict on its own ----
  var t3: i64 = 0
  let byswap: i64  = rm_verdict(900, 900, 0, 1, 700, 850, 250, 100, 3, 6)  // swap alone -> RED
  let byavail: i64 = rm_verdict(0, 50, 0, 1,   700, 850, 250, 100, 3, 6)   // avail alone -> RED
  let byleak: i64  = rm_verdict(0, 900, 7, 1,  700, 850, 250, 100, 3, 6)   // leakers alone -> RED
  if byswap == 2 { if byavail == 2 { if byleak == 2 { t3 = 1 } } }
60
  // ---- T4: RESERVED-but-untouched is NOT a leak; COMMITTED is ----
  // (a) the real first-run false positive: 40.6 GiB reserved, ~1 MiB committed -> NOT a leaker.
  // (b) a genuine leaker: monotonic address space AND 3.02 GiB actually committed -> IS a leaker.
  // (c) monotonic but small -> below the floor -> NOT a leaker.
  // (d) big and committed but VmSize != VmPeak (it has shrunk) -> NOT the fingerprint.
  var t4: i64 = 0
  let fp:  i64 = rm_is_leaker(42581844, 42581844, 1024, 0, 262144)
  let real: i64 = rm_is_leaker(6903268, 6903268, 161228, 2111640, 262144)
  let small: i64 = rm_is_leaker(2668, 2668, 600, 0, 262144)
  let shrunk: i64 = rm_is_leaker(1000000, 4000000, 500000, 500000, 262144)
  if fp == 0 { if real == 1 { if small == 0 { if shrunk == 0 { t4 = 1 } } } }
72
  // ---- T5: rm_field parses both shapes it must serve, and reports absence honestly ----
  var t5: i64 = 0
  let b: *u8 = sys_mmap(512)
  let s: *u8 = "Name:\tnx_hub_gw.elf\nVmPeak:\t 6903268 kB\nVmSize:\t 6903268 kB\nVmRSS:\t  161228 kB\nleak-min-kb = 262144\n" as *u8
  var i: i64 = 0
  while s[i] != (0 as u8) { b[i] = s[i]; i = i + 1 }
  b[i] = 0 as u8
  let vpk: i64 = rm_field(b, i, "VmPeak:" as *u8)
  let vrs: i64 = rm_field(b, i, "VmRSS:" as *u8)
  let cfg: i64 = rm_field(b, i, "leak-min-kb" as *u8)
  let miss: i64 = rm_field(b, i, "VmSwap:" as *u8)
  if vpk == 6903268 { if vrs == 161228 { if cfg == 262144 { if miss == 0 - 1 { t5 = 1 } } } }
85
  // ---- T6: an UNOBSERVABLE leak axis contributes NOTHING, and the ONLY variable is that one bit ----
  // Same measurement, same thresholds, one flag apart. A rm_verdict that ignored leak_observed would
  // return RED for BOTH of these and fail here. ★TWO ARMS ONE VARIABLE APART IS WHAT MAKES A RESULT
  // ATTRIBUTABLE -- two tests that each isolate one signal do not prove discrimination between them.
  var t6: i64 = 0
  let seen: i64   = rm_verdict(0, 900, 7, 1, 700, 850, 250, 100, 3, 6)   // 7 growers OBSERVED -> RED
  let unseen: i64 = rm_verdict(0, 900, 7, 0, 700, 850, 250, 100, 3, 6)   // the SAME 7, unobserved -> GREEN
  if seen == 2 { if unseen == 0 { t6 = 1 } }
94
  // ---- T7 neg-control-unobservable-is-not-a-green-vote ----
  // ★★★★★AN AXIS THAT CANNOT SEE MUST ABSTAIN, NOT ACQUIT. With the leak axis blind AND swap over
  // its red threshold, the verdict must still be RED: the other axes are levels, a snapshot measures
  // them exactly, and they still decide. A naive implementation that short-circuited to GREEN the
  // moment the leak axis went unobservable would pass T6 and fail ONLY here -- which is the point.
  var t7: i64 = 0
  if rm_verdict(900, 900, 7, 0, 700, 850, 250, 100, 3, 6) == 2 { t7 = 1 }
102
  // MIGRATED onto nx_gate_verdict (D001) 2026-08-14, in the FULL form -- deliberately NOT the
  // generator's minimal form. nx_gate_dry_apply offered `ctr[0]=green; ctr[1]=1`, which makes the
  // verdict readable but collapses FIVE teeth into ONE boolean: it reports passed 1/1, and a tooth
  // that silently stopped running would still read GREEN. That is exactly the defect gv_ctr exists
  // to prevent -- DECLARED MUST EQUAL EXECUTED BY CONSTRUCTION -- so the counter is driven per tooth
  // by gv_check instead. ★★★★★★A ONE-STATE JUDGE CANNOT SEE A DROPPED CONJUNCT: nx_gate_green would
  // have accepted the minimal form, because it only ever reads the verdict line. Reading the
  // candidate is what caught it. This also retires the hardcoded /5 denominator, a magic number
  // pinned to the tooth count that silently lies the moment a sixth tooth is added.
  // ---- T8: the blind CLASSIFIER separates two states with OPPOSITE remedies ----
  // ★A beat that RAN AND WAS REFUSED and a beat that IS DEAD are indistinguishable from outside, and
  // that indistinguishability IS the defect this closes. REFUSING -> shed load, the axis recovers by
  // itself. DEAD -> the beat is broken, go fix it. Collapsing them into one word sent four lanes at
  // four different mechanisms for the same symptom on 2026-08-21.
  var t8: i64 = 0
  let notblind: i64 = rm_blind_class(1, 232, 900)       // measurement fresh -> not blind at all
  let refusing: i64 = rm_blind_class(0, 232, 900)       // no measurement, FRESH refusal stamp
  let deadnostamp: i64 = rm_blind_class(0, 0 - 1, 900)  // no refusal stamp has ever been written
  let deadstale: i64 = rm_blind_class(0, RG_STALE_AGE_OBSERVED_S, 900)    // the REAL 7.2 h reading, far past the bound
  if notblind == 0 { if refusing == 1 { if deadnostamp == 2 { if deadstale == 2 { t8 = 1 } } } }
123
  // ---- T9 ANTI-VACUITY: leak_observed DOMINATES, so this is not merely an age comparison ----
  // ★★★★★TWO ARMS ONE VARIABLE APART IS WHAT MAKES A RESULT ATTRIBUTABLE. An implementation that
  // ignored leak_observed and only compared the age would pass every arm of T8 and fail ONLY here.
  var t9: i64 = 0
  let dom_a: i64 = rm_blind_class(1, 0 - 1, 900)   // fresh measurement, NO stamp -> still NOT blind
  let dom_b: i64 = rm_blind_class(0, 0 - 1, 900)   // identical age, measurement gone -> DEAD
  if dom_a == 0 { if dom_b == 2 { t9 = 1 } }
131
  // ---- T10 neg-control-clock-skew-and-the-bound-pinned-on-both-sides ----
  // ★A NEGATIVE AGE IS CLOCK SKEW, NOT FRESHNESS: a future-stamped file must never read REFUSING, or
  // it reads fresh forever -- the stale-fixture defect wearing a clock. The bound is pinned on BOTH
  // sides so a later >= / > slip cannot pass silently.
  var t10: i64 = 0
  let skew: i64 = rm_blind_class(0, 0 - 5, 900)     // future stamp -> DEAD, never REFUSING
  let atbound: i64 = rm_blind_class(0, 900, 900)    // exactly at the bound -> still counts as fresh
  let overbound: i64 = rm_blind_class(0, 901, 900)  // one second past -> DEAD
  if skew == 2 { if atbound == 1 { if overbound == 2 { t10 = 1 } } }
141
  // ---- T11: THE ALARM AN ABSTAINING AXIS OWES ----
  // ★Abstention is SAFE for the verdict and INVISIBLE to the operator, so a detector that goes blind
  // raises nothing anywhere. rm_verdict is RIGHT to let UNOBSERVABLE cast no vote; rm_verdict_blind adds
  // the missing half -- an alarm on the BLINDNESS ITSELF, never a leak claim about something unmeasured.
  // TWO ARMS ONE VARIABLE APART: identical records, only the axis visibility differs.
  var t11: i64 = 0
  let quiet_seen: i64  = rm_verdict_blind(0, 900, 0, 1, 700, 850, 250, 100, 3, 6, 0, RG_MAX_AGE_S)
  let quiet_blind: i64 = rm_verdict_blind(0, 900, 0, 0, 700, 850, 250, 100, 3, 6, RG_BLIND_ALARM_AGE_S, RG_MAX_AGE_S)
  if quiet_seen == 0 { if quiet_blind == 1 { t11 = 1 } }
151
  // ---- T12 neg-control-one-stale-window-is-still-only-abstention ----
  // ★max_age is already sized to absorb one FULL missed beat, so a single stale window is the transient
  // miss the abstention already covers. Alarming there would leave the detector permanently amber on a
  // healthy box, and a permanently-amber detector is one everyone learns to ignore. The bound is pinned
  // on BOTH sides so a later >= / > slip cannot pass silently.
  var t12: i64 = 0
  let justunder: i64 = rm_verdict_blind(0, 900, 0, 0, 700, 850, 250, 100, 3, 6, RG_BLIND_UNDER_ALARM_S, RG_MAX_AGE_S)
  let atalarm: i64   = rm_verdict_blind(0, 900, 0, 0, 700, 850, 250, 100, 3, 6, RG_BLIND_ALARM_AGE_S, RG_MAX_AGE_S)
  if justunder == 0 { if atalarm == 1 { t12 = 1 } }
161
  // ---- T13 neg-control-a-blind-axis-must-never-LOWER-a-verdict ----
  // ★The alarm may only RAISE. If it could lower, a dark LEADING axis would mask a red PRESSURE axis --
  // precisely the inversion that makes the safest verdict the most flattering one. Second arm pins clock
  // skew: an unusable age IS a blindness and must alarm, not read as fresh forever.
  var t13: i64 = 0
  let redblind: i64  = rm_verdict_blind(900, 900, 0, 0, 700, 850, 250, 100, 3, 6, RG_BLIND_ALARM_AGE_S, RG_MAX_AGE_S)
  let skewblind: i64 = rm_verdict_blind(0, 900, 0, 0, 700, 850, 250, 100, 3, 6, 0 - 5, RG_MAX_AGE_S)
  if redblind == 2 { if skewblind == 1 { t13 = 1 } }
170
  // ---- T14: THE TREND READER KEEPS THE TAIL OF AN OVER-CAP LOG (2026-09-02) ----
  // THE ONE TOOTH HERE THAT TOUCHES DISK, deliberately: the property under test IS file geometry (a log
  // larger than the read cap), and no synthetic input can express it. Fixture assembled at RUNTIME under
  // /tmp/nx_resmon_gate/ (the fixture-ratchet law), never a source literal. Planted: 3,000 rows whose
  // worst= is an OLD process, then ONE final row whose worst= is NEWEST_ROW; cap = well under a quarter
  // of the file. The head-bounded reader this replaces (measured live 2026-09-02: 65 frozen UNOBSERVABLE
  // beats after resmon.log crossed 1 MiB) returned a window whose last line was a TORN old row.
  var t14: i64 = 0
  sys_mkdir("/tmp/nx_resmon_gate" as *u8, 493)
  let fxp: *u8 = "/tmp/nx_resmon_gate/overcap.log" as *u8
  let ffd: i64 = sys_openat_wr(fxp, 420)
  if ffd >= 0 {
      let row: *u8 = "RESMON swap_used_permil=900 mem_avail_permil=500 load1_centi=1500 worst_committed_kb=1000000 worst=old_row_process\n" as *u8
      var rn: i64 = 0
      while rn < 3000 { sys_write(ffd, row, rm_slen(row)); rn = rn + 1 }
      let last: *u8 = "RESMON swap_used_permil=900 mem_avail_permil=500 load1_centi=1500 worst_committed_kb=2000000 worst=NEWEST_ROW\n" as *u8
      sys_write(ffd, last, rm_slen(last))
      sys_close(ffd)
      let fcap: i64 = 32768
      let fbuf: *u8 = sys_mmap(fcap)
      let fenv: *i64 = sys_mmap(64) as *i64
      let fn: i64 = rm_trend_read_tail(fxp, fbuf, fcap, fenv)
      // the retained window must END with the newest row, DECLARE truncation, report the true file size,
      // and START on a record boundary (the torn first record trimmed) -- four conjuncts, one tooth.
      var tailok: i64 = 0
      if fn > 0 { if fenv[3] == 1 { if fenv[0] > fcap {
          let needle: *u8 = "worst=NEWEST_ROW\n" as *u8
          let nl: i64 = rm_slen(needle)
          var m: i64 = 1
          var k: i64 = 0
          while k < nl { if fbuf[fn - nl + k] != needle[k] { m = 0 } k = k + 1 }
          if m == 1 { if fbuf[0] == (82 as u8) { tailok = 1 } }
      } } }
      t14 = tailok
  }
206
  let ctr: *i64 = gv_ctr()
  gv_head("nx_resmon_gate -- pressure + leak-census predicates (seq1005)" as *u8)
  gv_check("T1-verdict-ladder-is-threshold-driven" as *u8, t1, ctr)
  gv_check("T2-NONVACUITY-unreachable-stays-GREEN" as *u8, t2, ctr)
  gv_check("T3-each-axis-can-raise-alone" as *u8, t3, ctr)
  gv_check("T4-reserved-not-leak-committed-is" as *u8, t4, ctr)
  gv_check("T5-field-parse-status-conf-and-absent" as *u8, t5, ctr)
  gv_check("T6-unobservable-leak-axis-casts-no-vote" as *u8, t6, ctr)
  gv_check("T7-neg-control-unobservable-is-not-a-green-vote" as *u8, t7, ctr)
  gv_check("T8-blind-classifier-separates-REFUSING-from-DEAD" as *u8, t8, ctr)
  gv_check("T9-ANTIVACUITY-leak-observed-dominates-not-just-age" as *u8, t9, ctr)
  gv_check("T10-neg-control-clock-skew-is-DEAD-and-bound-pinned-both-sides" as *u8, t10, ctr)
  gv_check("T11-a-blind-LEADING-axis-raises-an-alarm-of-its-own" as *u8, t11, ctr)
  gv_check("T12-neg-control-one-stale-window-is-still-only-abstention" as *u8, t12, ctr)
  gv_check("T13-neg-control-blindness-may-only-RAISE-never-lower-a-verdict" as *u8, t13, ctr)
  gv_check("T14-trend-reader-keeps-the-TAIL-of-an-over-cap-log-and-declares-truncation" as *u8, t14, ctr)
  // CANONICAL ANCHOR, LAST LINE, POSITIONAL (seq585). gv_last_line reads only the FINAL line, so the
  // rich domain row above is preserved untouched and the machine-readable verdict rides alone here.
  // ★FIX THE EMITTER, NEVER WIDEN THE READER -- widening is how an estate ends up with two readers
  // and two spellings of success. Without this tail nothing can judge the gate: /api/promote refuses
  // it as D001 and nx_gate_green cannot read its outcome, so flake and erosion stay invisible.
  return gv_verdict("RESMON-GATE" as *u8, ctr, "the policy predicates in nx_resmon_lib, gated as PURE functions on synthetic inputs -- no /proc, no fixture, no clock. Each tooth states its own claim above; this note deliberately does NOT recite them, because a note that enumerates teeth goes stale the moment one is added and drifts toward understatement, which is the direction nobody audits" as *u8)
229}
nx_resmon_gate.nx source

`nx_resmon_gate.nx` source
