code wiki / (root) / nx_provcensus_gate.nx
`nx_provcensus_gate.nx` source

↩ module page · 205 lines · 15802 B
1// nx_provcensus_gate.nx -- proves the fleet provenance-drift census's judgement half (2026-08-26).
2//
3// The subject is nx_provcensus_lib.nx, imported so it compiles INTO this binary. That is the whole
4// reason the lib exists as a separate file: this gate can be mutation-proven, whereas a gate that
5// fork/execs the deployed nx_provcensus.elf could not be -- every mutant would read NOT-REACHED and the
6// harness would report a fault in the gate rather than in the subject.
7//
8// What is actually at stake. The census exists to answer "how many ships proved the wrong subject", and
9// the only way it can lie in the FLATTERING direction is by letting something that is not a measured
10// CURRENT read as CURRENT. So the teeth below spend most of their effort on the three ways to fail to
11// observe -- an empty capture, a capture with no verdict token, and a verdict token this build has never
12// heard of -- and require all three to land in UNREADABLE.
13// license_tier: ORIGINAL   No hw writes (Rule 26).   expect_exit: 0
14import "nx_gate_verdict.nx"
15import "nx_provcensus_lib.nx"
16
17const PG_COUNTS_BYTES: i64 = 40      // PCX_NBUCKET slots of 8; the lib owns the bucket count
18// Scratch for the CRLF roster fixture, assembled byte-by-byte below. Sized well above the two short
19// rows it holds; the assembly is bounded by the literals it copies, not by this number.
20const PG_CRBUF: i64 = 128
21const PG_CR: i64 = 13
22const PG_LF: i64 = 10
23
24// Copies a NUL-terminated string into d at offset o and returns the new offset. Used only to BUILD
25// fixtures: a literal carriage return is not something to trust to the lexer, so the CR case is
26// constructed rather than written.
27func pg_put(d: *u8, o: i64, s: *u8) -> i64 {
  var p: i64 = o
  var i: i64 = 0
  while s[i] != (0 as u8) {
      d[p] = s[i]
      p = p + 1
      i = i + 1
  }
  return p
36}
37
38// Exact string equality, including length -- a prefix compare would call "CURRENT" and "CURRENTLY"
39// the same name and pass the teeth below for the wrong reason.
40func pg_streq(a: *u8, b: *u8) -> i64 {
  var i: i64 = 0
  while a[i] != (0 as u8) {
      if a[i] != b[i] { return 0 }
      i = i + 1
  }
  if b[i] != (0 as u8) { return 0 }
  return 1
48}
49
50func main() -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_provcensus_gate -- the census classifier: every nx_provcheck outcome, exactly one bucket" as *u8)
53
  // Fixtures shaped exactly like nx_provcheck's real stdout, so a change to its wording that this
  // classifier cannot read shows up here rather than as a silent fleet of UNREADABLE rows.
  let p_cur: *u8 = "PROVCHECK nx_a recorded=aa now=aa verdict=CURRENT (the artifact IS its sources)\n" as *u8
  let p_drf: *u8 = "PROVCHECK nx_b recorded=aa now=bb verdict=DRIFTED (a source in the import closure changed since this artifact was built)\n" as *u8
  let p_unr: *u8 = "PROVCHECK nx_c verdict=UNRECORDED (sidecar has no closure_sha256). This is NOT a pass and NOT a failure: rebuild to record one.\n" as *u8
  let p_nos: *u8 = "PROVCHECK nx_d verdict=NOSIDECAR path=./nx_d.provenance\n" as *u8
  let p_none: *u8 = "PROVCHECK nx_e recorded=aa now=bb\n" as *u8
  let p_unk: *u8 = "PROVCHECK nx_f recorded=aa now=bb verdict=BANANA\n" as *u8
  let p_decoy: *u8 = "PROVCHECK ./tree/verdict=CURRENT/nx_g recorded=aa now=bb verdict=DRIFTED (a source moved)\n" as *u8
63
  // A fixture the defect cannot fail is not a test: establish the fixtures are non-degenerate before
  // asserting anything about how they classify.
  var fixtures_ok: i64 = 0
  if pcx_slen(p_cur) > 0 {
      if pcx_slen(p_decoy) > pcx_slen(p_cur) { fixtures_ok = 1 }
  }
  gv_check("T0 the crafted nx_provcheck fixtures are non-empty and the decoy really is the longer one" as *u8, fixtures_ok == 1, ctr)
71
  gv_check("T1 a CURRENT capture classifies as CURRENT" as *u8, pcx_classify(p_cur, pcx_slen(p_cur)) == PCX_CURRENT, ctr)
  gv_check("T2 a DRIFTED capture classifies as DRIFTED" as *u8, pcx_classify(p_drf, pcx_slen(p_drf)) == PCX_DRIFTED, ctr)
  gv_check("T3 an UNRECORDED capture classifies as UNRECORDED, not as a pass and not as a failure" as *u8, pcx_classify(p_unr, pcx_slen(p_unr)) == PCX_UNRECORDED, ctr)
  gv_check("T4 a NOSIDECAR capture classifies as NOSIDECAR" as *u8, pcx_classify(p_nos, pcx_slen(p_nos)) == PCX_NOSIDECAR, ctr)
76
  // The three ways to fail to observe. Each must land in UNREADABLE; none may read as CURRENT.
  gv_check("T5 an empty capture is UNREADABLE, never CURRENT" as *u8, pcx_classify(p_cur, 0) == PCX_UNREADABLE, ctr)
  gv_check("T6 a capture carrying no verdict token at all is UNREADABLE" as *u8, pcx_classify(p_none, pcx_slen(p_none)) == PCX_UNREADABLE, ctr)
  gv_check("T7 a verdict token this build has never heard of is UNREADABLE, not silently folded into a known bucket" as *u8, pcx_classify(p_unk, pcx_slen(p_unk)) == PCX_UNREADABLE, ctr)
81
  // THE PARSE-ANCHOR TOOTH. nx_provcheck prints its verdict last; an unanchored first-match parse
  // reads the DATA as the ANSWER the moment anything upstream echoes the word -- here a directory
  // literally named verdict=CURRENT sitting in the path, with the real answer DRIFTED at the end.
  // Getting this backwards would report a drifted gate as current, which is the flattering direction.
  gv_check("T8 the parse anchors on the LAST verdict token, so an echoed one upstream cannot be read as the answer" as *u8, pcx_classify(p_decoy, pcx_slen(p_decoy)) == PCX_DRIFTED, ctr)
87
  // Population membership.
  let n_side: *u8 = "nx_thing_gate.provenance" as *u8
  let n_plain: *u8 = "nx_thing.provenance" as *u8
  let n_bak: *u8 = "nx_thing_gate.provenance.bak" as *u8
  let n_short: *u8 = "x" as *u8
  gv_check("T9 a gate sidecar is recognised as population" as *u8, pcx_ends_with(n_side, pcx_slen(n_side), "_gate.provenance" as *u8) == 1, ctr)
  gv_check("T10 a non-gate sidecar is excluded" as *u8, pcx_ends_with(n_plain, pcx_slen(n_plain), "_gate.provenance" as *u8) == 0, ctr)
  gv_check("T11 a name shorter than the suffix is excluded rather than read out of bounds" as *u8, pcx_ends_with(n_short, pcx_slen(n_short), "_gate.provenance" as *u8) == 0, ctr)
96
  // Reconciliation. A partition is a claim; these two teeth are the claim being checked.
  let counts: *i64 = sys_mmap(PG_COUNTS_BYTES) as *i64
  counts[PCX_CURRENT] = 3
  counts[PCX_DRIFTED] = 2
  counts[PCX_UNRECORDED] = 1
  counts[PCX_NOSIDECAR] = 0
  counts[PCX_UNREADABLE] = 4
  gv_check("T12 the parts are summed, not assumed: a partition that sums to its population reconciles" as *u8, pcx_reconciles(counts, 10) == 1, ctr)
  gv_check("neg-control-reconciliation-refuses-a-partition-that-does-not-sum" as *u8, pcx_reconciles(counts, 11) == 0, ctr)
  gv_check("T13 the sum is reported as a value the caller can print beside the population" as *u8, pcx_total(counts) == 10, ctr)
107
  // Bites: a classifier that answered the same way for everything would pass a suite that only ever
  // asks "did it refuse?", and a suffix test implemented as a substring search would pass T9 and T10
  // while quietly admitting every .bak in the directory.
  gv_bite("neg-control-classifier-refuses-an-unknown-verdict-yet-still-accepts-a-known-one" as *u8,
          pcx_classify(p_unk, pcx_slen(p_unk)) == PCX_UNREADABLE,
          pcx_classify(p_cur, pcx_slen(p_cur)) == PCX_UNREADABLE, ctr)
  gv_bite("neg-control-suffix-test-is-anchored-at-the-end-not-a-substring-search" as *u8,
          pcx_ends_with(n_side, pcx_slen(n_side), "_gate.provenance" as *u8),
          pcx_ends_with(n_bak, pcx_slen(n_bak), "_gate.provenance" as *u8), ctr)
117
  // BUCKET NAMES ARE THE PUBLISHED OUTPUT, so they need teeth of their own. Added 2026-08-26 after a
  // mutation run: nx_gate_bite reported killed=1 mutant_live=0 (GREEN, non-vacuity proven) but three
  // LITERAL mutants SURVIVED inside these very return strings -- nothing asserted the words the census
  // prints, so a mutant could rename a bucket and every tooth still passed. A surviving mutant is a
  // measurement; this is the gap it measured, closed rather than argued away.
  gv_check("T14 the CURRENT bucket renders its exact published name" as *u8, pg_streq(pcx_bucket_name(PCX_CURRENT), "CURRENT" as *u8) == 1, ctr)
  gv_check("T15 the DRIFTED bucket renders its exact published name" as *u8, pg_streq(pcx_bucket_name(PCX_DRIFTED), "DRIFTED" as *u8) == 1, ctr)
  gv_check("T16 the UNRECORDED bucket renders its exact published name" as *u8, pg_streq(pcx_bucket_name(PCX_UNRECORDED), "UNRECORDED" as *u8) == 1, ctr)
  gv_check("T17 the NOSIDECAR bucket renders its exact published name" as *u8, pg_streq(pcx_bucket_name(PCX_NOSIDECAR), "NOSIDECAR" as *u8) == 1, ctr)
  gv_check("T18 the UNREADABLE bucket renders its exact published name" as *u8, pg_streq(pcx_bucket_name(PCX_UNREADABLE), "UNREADABLE" as *u8) == 1, ctr)
  // An index outside the partition must render UNKNOWN rather than silently borrowing a real bucket's
  // name -- the same law the classifier obeys, checked on the rendering side.
  gv_check("T19 a bucket index outside the partition renders UNKNOWN, not a real bucket's name" as *u8, pg_streq(pcx_bucket_name(PCX_NBUCKET), "UNKNOWN" as *u8) == 1, ctr)
  gv_bite("neg-control-bucket-name-comparison-is-exact-not-a-prefix-match" as *u8,
          pg_streq(pcx_bucket_name(PCX_CURRENT), "CURRENT" as *u8),
          pg_streq(pcx_bucket_name(PCX_CURRENT), "CURRENTLY" as *u8), ctr)
134
  // ---- ROSTER MEMBERSHIP: the split that turns a count into a worklist ---------------------------
  // A DRIFTED artifact nothing runs is a hazard sitting still; a DRIFTED artifact the roster beat
  // fires every beat is publishing a verdict about code that is not the tree. The census can only
  // separate them if this membership test is right, and the way it goes WRONG is asymmetric: a false
  // OFF-ROSTER shrinks the actionable worklist and reads as good news, so it is the direction nobody
  // audits. Most of the teeth below aim there.
  //
  // The fixture is shaped like the real confs: a comment row that NAMES GATES IN PROSE (gateroster.conf
  // really does carry re-homing notes listing dozens), an indented row, a path-prefixed row, a blank
  // row, and plain rows.
  let r_fix: *u8 = "; re-homed 2026-08-22 to gateroster_slow.conf: nx_ghost_gate nx_phantom_gate\nnx_alpha_gate\n   nx_beta_gate   \n_offc/nx_entropy_gate\n\nnx_softtissue_gate\n" as *u8
  let r_len: i64 = pcx_slen(r_fix)
147
  // ASSERT THE FIXTURE REACHED THE CONDITION BEFORE ASSERTING THE OUTCOME. Without this, the
  // comment-exclusion neg-control below would pass for the WRONG REASON -- a name that is simply
  // absent from the buffer is excluded by every implementation, including a broken one.
  gv_check("R0 the fixture really does name nx_ghost_gate inside its comment row, so the exclusion tooth cannot pass by absence" as *u8, pcx_find(r_fix, r_len, "nx_ghost_gate" as *u8, 0) >= 0, ctr)
  gv_check("R1 a plain roster row is a member" as *u8, pcx_roster_has(r_fix, r_len, "nx_alpha_gate" as *u8) == 1, ctr)
  gv_check("R2 an indented row with trailing spaces is still a member, so whitespace cannot hide a rostered gate" as *u8, pcx_roster_has(r_fix, r_len, "nx_beta_gate" as *u8) == 1, ctr)
  gv_check("R3 a path-prefixed row matches on its basename, the way the beat resolves it" as *u8, pcx_roster_has(r_fix, r_len, "nx_entropy_gate" as *u8) == 1, ctr)
  gv_check("R4 a row after a blank line is still reached, so a blank cannot truncate the walk" as *u8, pcx_roster_has(r_fix, r_len, "nx_softtissue_gate" as *u8) == 1, ctr)
156
  // THE LOAD-BEARING EXCLUSION. A substring search over the conf would report every gate named in a
  // re-homing comment as rostered, inflating the invoked count with gates the beat will never fire.
  gv_check("R5 a gate named ONLY inside a comment row is NOT rostered, though the bytes are in the file" as *u8, pcx_roster_has(r_fix, r_len, "nx_ghost_gate" as *u8) == 0, ctr)
  gv_check("R6 a second gate named only in that same comment row is likewise not rostered" as *u8, pcx_roster_has(r_fix, r_len, "nx_phantom_gate" as *u8) == 0, ctr)
161
  // Prefix conflation, both directions. These are different gates and a prefix test would merge them.
  gv_check("R7 a query that is a strict PREFIX of a live row does not match it" as *u8, pcx_roster_has(r_fix, r_len, "nx_alpha" as *u8) == 0, ctr)
  gv_check("R8 a query that strictly EXTENDS a live row does not match it either" as *u8, pcx_roster_has(r_fix, r_len, "nx_alpha_gate_extra" as *u8) == 0, ctr)
  gv_check("R9 a gate absent from every row is absent" as *u8, pcx_roster_has(r_fix, r_len, "nx_softtissue_mr_gate" as *u8) == 0, ctr)
166
  // A roster that could not be loaded must not answer membership for anything. The PROGRAM is what
  // refuses to publish a split in that case; this only fixes the lib half of the contract.
  gv_check("R10 an empty roster buffer answers 0 for a gate that is otherwise a member" as *u8, pcx_roster_has(r_fix, 0, "nx_alpha_gate" as *u8) == 0, ctr)
  gv_check("R11 an empty NAME never matches, so a blank row cannot be read as a member" as *u8, pcx_roster_has(r_fix, r_len, "" as *u8) == 0, ctr)
171
  // The live-row count is what makes a failed or empty load ANNOUNCE itself instead of silently
  // making every gate read OFF-ROSTER. Bind it to the fixture's real content, not to a shape.
  gv_check("R12 the live-row count counts exactly the non-comment non-blank rows" as *u8, pcx_roster_rows(r_fix, r_len) == 4, ctr)
  gv_check("R13 an empty roster buffer reports 0 live rows rather than a shape" as *u8, pcx_roster_rows(r_fix, 0) == 0, ctr)
176
  // CRLF, built byte-by-byte because a literal carriage return is not something to trust to the lexer.
  // An untrimmed CR makes every row compare unequal by one invisible byte -- the whole roster would
  // read as absent, confidently and silently.
  let crb: *u8 = sys_mmap(PG_CRBUF)
  var cp: i64 = pg_put(crb, 0, "nx_crlf_gate" as *u8)
  let cr_at: i64 = cp
  crb[cp] = PG_CR as u8
  cp = cp + 1
  crb[cp] = PG_LF as u8
  cp = cp + 1
  cp = pg_put(crb, cp, "nx_plain_gate" as *u8)
  crb[cp] = PG_LF as u8
  cp = cp + 1
  gv_check("R14 the CRLF fixture really does carry a carriage return, so the next tooth is not vacuous" as *u8, (crb[cr_at]&0xff) == PG_CR, ctr)
  gv_check("R15 a CRLF-terminated row still matches, so line endings cannot blank an entire roster" as *u8, pcx_roster_has(crb, cp, "nx_crlf_gate" as *u8) == 1, ctr)
  gv_check("R16 the row after a CRLF row is still reached" as *u8, pcx_roster_has(crb, cp, "nx_plain_gate" as *u8) == 1, ctr)
193
  // Bites. A membership test that answered 1 for everything would pass every positive tooth above,
  // and one that answered 0 for everything would pass every negative one; each bite pairs a must-hold
  // with a must-not-hold so neither degenerate implementation survives.
  gv_bite("neg-control-comment-rows-are-excluded-yet-live-rows-still-match" as *u8,
          pcx_roster_has(r_fix, r_len, "nx_alpha_gate" as *u8) == 1,
          pcx_roster_has(r_fix, r_len, "nx_ghost_gate" as *u8) == 1, ctr)
  gv_bite("neg-control-membership-is-exact-not-a-prefix-or-substring-search" as *u8,
          pcx_roster_has(r_fix, r_len, "nx_entropy_gate" as *u8) == 1,
          pcx_roster_has(r_fix, r_len, "nx_alpha" as *u8) == 1, ctr)
203
  return gv_verdict("provcensus" as *u8, ctr, "every nx_provcheck outcome maps to exactly one bucket, the parse is anchored positionally, an unrecognised verdict can never read as CURRENT, and roster membership is decided by live rows rather than by bytes that merely appear in the file" as *u8)
205}
nx_provcensus_gate.nx source

`nx_provcensus_gate.nx` source
