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

↩ module page · 196 lines · 12609 B
1// nx_contentdiff_gate.nx -- THE REFEREE FOR THE PROMOTE CAPABILITY RULER.
2//
3// WHY IT EXISTS: nx_contentdiff_lib is the arithmetic behind BOTH the hand-run oracle (nx_contentdiff)
4// AND the staging guard inside md_promote_staged, i.e. it decides whether a promote is allowed to destroy
5// printable content. On 2026-09-03 a census found it had NO GATE ANYWHERE -- the ruler that judges every
6// promote in the estate was itself unjudged, so every property it claims rested on the fact that nobody
7// had seen it misbehave. ★A GREEN THAT NEVER HAD A CORRESPONDING RED IS UNVERIFIED, and here there was
8// not even a green: there was no test.
9//
10// It proves the properties the promote decision actually rests on:
11//   * the loss measure is CORRECT on constructed subset / superset / identical / disjoint inputs;
12//   * it is FAIL-CLOSED -- an empty or unreadable candidate is TOTAL loss, never clean (the direction that
13//     matters, because the flattering failure here silently blesses a broken artifact);
14//   * the SYMMETRY class names all four outcomes, so a rename cannot read as a removal;
15//   * the SOURCE-PATH partition is narrow enough that it cannot swallow real content, and it RECONCILES.
16// license_tier: ORIGINAL   Read-only. No hw writes (Rule 26).   expect_exit: 0
17import "nx_syscalls.nx"
18import "nx_gate_verdict.nx"
19import "_hdl_build/nx_contentdiff_lib.nx"
20
21const CG_BUF: i64 = 4096
22const CG_MINLEN: i64 = 6
23const CG_NUL: i64 = 0
24
25// append a printable run followed by one NUL separator; returns the new offset
26func cg_run(b: *u8, off: i64, s: *u8) -> i64 {
  var o: i64 = off
  var i: i64 = 0
  while s[i] != (0 as u8) { b[o] = s[i]; o = o + 1; i = i + 1 }
  b[o] = CG_NUL as u8
  return o + 1
32}
33
34func cg_prm() -> *i64 {
  let p: *i64 = sys_mmap(8 * CDL_P_SLOTS) as *i64
  p[CDL_P_MINLEN] = CG_MINLEN
  p[CDL_P_MAXSAMPLES] = 0
  p[CDL_P_MAXTOKLEN] = 0
  return p
40}
41
42func main(argc: i64, argv: *i64) -> i64 {
  gv_head("nx_contentdiff_gate -- the referee for the promote capability ruler (loss measure, fail-closed direction, symmetry class, source-path partition)" as *u8)
  let ctr: *i64 = gv_ctr()
  let prm: *i64 = cg_prm()
46
  // ---- FIXTURES, built in memory: no files, no forks, nothing on disk to go stale ----
  // THREE distinctive runs. A carries all three; B drops the third; C carries a fourth A lacks.
  let A: *u8 = sys_mmap(CG_BUF)
  let B: *u8 = sys_mmap(CG_BUF)
  let C: *u8 = sys_mmap(CG_BUF)
  var an: i64 = 0
  an = cg_run(A, an, "ALPHAKEEPER" as *u8)
  an = cg_run(A, an, "BRAVOKEEPER" as *u8)
  an = cg_run(A, an, "CHARLIEDROPPED" as *u8)
  var bn: i64 = 0
  bn = cg_run(B, bn, "ALPHAKEEPER" as *u8)
  bn = cg_run(B, bn, "BRAVOKEEPER" as *u8)
  var cn: i64 = 0
  cn = cg_run(C, cn, "ALPHAKEEPER" as *u8)
  cn = cg_run(C, cn, "BRAVOKEEPER" as *u8)
  cn = cg_run(C, cn, "DELTAADDED" as *u8)
  gv_check("fixture-reached-condition: three buffers built and non-empty, B a strict subset of A" as *u8,
      ((an > 0) as i64) * ((bn > 0) as i64) * ((cn > 0) as i64) * ((an > bn) as i64), ctr)
65
  let o1: *i64 = sys_mmap(8 * CDL_O_SLOTS) as *i64
  let o2: *i64 = sys_mmap(8 * CDL_O_SLOTS) as *i64
68
  // ---- the loss measure itself ----
  cdl_lost(A, an, A, an, prm, o1)
  gv_check("loss: a buffer against ITSELF loses nothing (the reflexive case a promote of an unchanged artifact hits)" as *u8,
      (o1[CDL_O_LOST] == 0) as i64, ctr)
  gv_check("loss: and it actually EXAMINED the runs (a zero over zero runs would be the vacuous pass)" as *u8,
      (o1[CDL_O_RUNS] == 3) as i64, ctr)
75
  let p_sub: i64 = cdl_lost(A, an, B, bn, prm, o1)
  gv_check("loss: a candidate MISSING one of three runs reports exactly one lost" as *u8,
      (o1[CDL_O_LOST] == 1) as i64, ctr)
  gv_check("loss: and the permil is derived from the checked count, not guessed (1 of 3 = 333)" as *u8,
      (p_sub == 333) as i64, ctr)
81
  cdl_lost(B, bn, A, an, prm, o2)
  gv_check("loss: reversed, a candidate that is a strict SUPERSET loses nothing" as *u8,
      (o2[CDL_O_LOST] == 0) as i64, ctr)
85
  // ---- FAIL-CLOSED: the direction where a flattering answer blesses a broken artifact ----
  let p_empty: i64 = cdl_lost(A, an, A, 0, prm, o2)
  gv_check("neg-control-an-EMPTY-candidate-is-TOTAL-loss-1000-permil-never-clean (fail-closed, the only safe direction)" as *u8,
      ((p_empty == 1000) as i64) * ((o2[CDL_O_LOST] == 3) as i64), ctr)
  let p_noLive: i64 = cdl_lost(A, 0, A, an, prm, o2)
  gv_check("loss: an empty LIVE side has nothing to lose and reports 0 with 0 runs (abstain, not a false alarm)" as *u8,
      ((p_noLive == 0) as i64) * ((o2[CDL_O_RUNS] == 0) as i64), ctr)
93
  // ---- the SYMMETRY class: all four outcomes, so a rename cannot read as a removal ----
  gv_check("symmetry: neither side missing anything is IDENTICAL-CONTENT" as *u8,
      (cdl_symclass(0, 0) == CDL_SYM_IDENTICAL) as i64, ctr)
  gv_check("symmetry: only the candidate missing runs is ONE-WAY-LOSS (the regression shape)" as *u8,
      (cdl_symclass(5, 0) == CDL_SYM_LOSS) as i64, ctr)
  gv_check("symmetry: only live missing runs is ONE-WAY-GAIN (a superset is a gift, not litter)" as *u8,
      (cdl_symclass(0, 5) == CDL_SYM_GAIN) as i64, ctr)
  gv_check("symmetry: BOTH directions losing is BIDIRECTIONAL -- a rename or re-encode, NOT a plain loss" as *u8,
      (cdl_symclass(5, 5) == CDL_SYM_BOTH) as i64, ctr)
  // and end to end on the fixtures, so the class is not merely arithmetic on hand-fed numbers
  cdl_lost(A, an, C, cn, prm, o1)
  cdl_lost(C, cn, A, an, prm, o2)
  gv_check("symmetry END-TO-END: two buffers that each hold a run the other lacks classify BIDIRECTIONAL" as *u8,
      (cdl_symclass(o1[CDL_O_LOST], o2[CDL_O_LOST]) == CDL_SYM_BOTH) as i64, ctr)
  gv_check("fixture-reached-condition: that BIDIRECTIONAL verdict came from a REAL 1-and-1 split, not from zeros" as *u8,
      ((o1[CDL_O_LOST] == 1) as i64) * ((o2[CDL_O_LOST] == 1) as i64), ctr)
110
  // ---- the SOURCE-PATH partition: narrow enough that it cannot swallow real content ----
  // ⚠OFFSETS AND LENGTHS ARE DERIVED FROM THE BUILDER, NEVER HAND-COUNTED. The first cut of these teeth
  // hand-wrote (62, 12) for the third run when the builder puts it at 63 -- one tooth then FAILED while
  // the buffer-walking partition tooth PASSED, and the partition was the one telling the truth.
  // ★A HAND-COUNTED OFFSET BESIDE A STRING LITERAL IS A SECOND COPY OF THAT LITERAL'S SHAPE AND THE TWO
  //  DRIFT SILENTLY -- the estate banks exactly this, and cg_run already returns the next offset, so the
  //  correct value was in hand the whole time. Bind it once, derive the rest.
  let S: *u8 = sys_mmap(CG_BUF)
  let s1: i64 = 0
  let s2: i64 = cg_run(S, s1, "runtime/nx_fcntl.nx" as *u8)
  let s3: i64 = cg_run(S, s2, "a message naming nx_fcntl.nx in the middle" as *u8)
  let s4: i64 = cg_run(S, s3, "PLAINMESSAGE" as *u8)
  let sn: i64 = cg_run(S, s4, ".debug_info" as *u8)
  // each run's length is (next start - this start - 1), the -1 being the NUL cg_run appends
  let l1: i64 = s2 - s1 - 1
  let l2: i64 = s3 - s2 - 1
  let l3: i64 = s4 - s3 - 1
  let l4: i64 = sn - s4 - 1
  let E: *u8 = sys_mmap(CG_BUF)
  let en: i64 = 0
  gv_check("fixture-reached-condition: the four classifier runs are the lengths the BUILDER produced (19 / 42 / 12 / 11), derived not hand-counted" as *u8,
      ((l1 == 19) as i64) * ((l2 == 42) as i64) * ((l3 == 12) as i64) * ((l4 == 11) as i64), ctr)
  gv_check("srcpath: a run ENDING in .nx is classified as a compiler-embedded source path" as *u8,
      cdl_is_srcpath(S, s1, l1), ctr)
  gv_check("neg-control-a-message-that-merely-MENTIONS-a-.nx-file-is-NOT-a-source-path (the class must be too narrow to hide content)" as *u8,
      (1 - cdl_is_srcpath(S, s2, l2)), ctr)
  gv_check("neg-control-a-run-with-no-.nx-suffix-at-all-is-not-a-source-path" as *u8,
      (1 - cdl_is_srcpath(S, s3, l3)), ctr)
  gv_check("neg-control-a-run-too-short-to-carry-a-suffix-is-not-a-source-path (no read before the buffer)" as *u8,
      (1 - cdl_is_srcpath(S, s1, 3)), ctr)
141
  // ---- the SYMBOL-NAME class, added after real data refuted a source-path-only axis --------------
  // On the live case lost_srcpath was 14 of 331 while the build line said `debug-info subprograms=325`:
  // -g embeds one symbol per function, and THAT is the dominant class. The first cut of this axis was
  // built from the 8 runs the oracle PRINTS -- a prefix of 332 -- which is the population/prefix error
  // the estate already names. These teeth pin the shape that actually occurs.
  gv_check("ident: an identifier-shaped run (letters, digits, underscore) is classified as a symbol name" as *u8,
      cdl_is_ident(S, s3, l3), ctr)
  gv_check("neg-control-a-message-WITH-SPACES-is-not-a-symbol-name (ordinary content must not be absorbed)" as *u8,
      (1 - cdl_is_ident(S, s2, l2)), ctr)
  gv_check("neg-control-a-source-PATH-is-not-a-symbol-name -- the two classes are DISJOINT by construction, so they cannot double-count" as *u8,
      (1 - cdl_is_ident(S, s1, l1)), ctr)
153
  // partition over a REAL loss: everything in S is absent from an empty candidate, so all three are lost
  cdl_lost(S, sn, E, en, prm, o1)
  let flav: i64 = cdl_lost_srcpath(S, sn, E, en, CG_MINLEN, o1)
  let sp: i64 = o1[CDL_O_SRCPATH]
  let idn: i64 = o1[CDL_O_IDENT]
  let sct: i64 = o1[CDL_O_SECT]
  let oth: i64 = o1[CDL_O_LOST] - flav
  gv_check("partition: lost_srcpath + lost_symbolname + lost_sectname + lost_other SUMS to lost_from_live (an unreconciled partition is a leak)" as *u8,
      ((sp + idn + sct + oth) == o1[CDL_O_LOST]) as i64, ctr)
  // ELF/DWARF SECTION NAMES are a THIRD metadata class, added 2026-09-03 after a real front-door run
  // reported lost_other=4 of which THREE were `.debug_info`, `.debug_abbrev` and `.shstrtab`. They are
  // caught by neither of the other two classes because they start with '.'.
  gv_check("sectname: an ELF/DWARF section name is classified as build metadata, not as actionable loss" as *u8,
      cdl_is_sectname(S, s4, l4), ctr)
  gv_check("neg-control-a-symbol-name-is-NOT-a-section-name (the three metadata classes stay disjoint so they cannot double-count)" as *u8,
      (1 - cdl_is_sectname(S, s3, l3)), ctr)
  gv_check("neg-control-a-message-with-spaces-is-NOT-a-section-name (no real message string can enter the metadata class)" as *u8,
      (1 - cdl_is_sectname(S, s2, l2)), ctr)
  gv_check("partition: the four fixture runs split 1 source path / 1 symbol name / 1 section name / 1 real message -- the axis discriminates all four" as *u8,
      ((sp == 1) as i64) * ((idn == 1) as i64) * ((sct == 1) as i64) * ((oth == 1) as i64), ctr)
  gv_check("partition: and it wrote all three counts where a caller can reconcile them (out[CDL_O_SRCPATH], out[CDL_O_IDENT], out[CDL_O_SECT])" as *u8,
      ((o1[CDL_O_SRCPATH] == sp) as i64) * ((o1[CDL_O_IDENT] == idn) as i64) * ((o1[CDL_O_SECT] == sct) as i64), ctr)
  // ★THE AXIS MUST NEVER MOVE THE VERDICT: prove the loss count is unchanged by measuring the partition
  let before: i64 = o1[CDL_O_LOST]
  cdl_lost_srcpath(S, sn, E, en, CG_MINLEN, o1)
  gv_check("neg-control-measuring-the-flavour-axis-does-NOT-change-the-loss-count-it-partitions (a separate axis, never a widened conjunct)" as *u8,
      (o1[CDL_O_LOST] == before) as i64, ctr)
181
  // ⚠this is the buffer's BYTE LENGTH, not its run count -- it shipped once as `fixture_runs_A` and
  // read as a flat contradiction of the tooth asserting 3 runs. A VALUE UNDER A WRONG KEY IS WORSE
  // THAN NO VALUE: it manufactures a disagreement the reader has to resolve before trusting anything.
  gv_kv("fixture_bytes_A" as *u8, an)
  gv_kv("fixture_runs_A" as *u8, cdl_count_runs(A, an, CG_MINLEN))
  gv_kv("loss_A_vs_B_permil" as *u8, p_sub)
  gv_kv("empty_candidate_permil" as *u8, p_empty)
  gv_kv("srcpath_of_3_lost" as *u8, sp)
  gv_kv("symbolname_of_4_lost" as *u8, idn)
  gv_kv("sectname_of_4_lost" as *u8, sct)
  gv_kv("other_of_3_lost" as *u8, oth)
193
  return gv_verdict("contentdiff" as *u8, ctr,
      "the promote capability ruler measures loss correctly on constructed subset/superset/identical/disjoint inputs, is fail-closed on an empty candidate, names all four symmetry outcomes so a rename cannot read as a removal, and partitions source-path losses on a SEPARATE axis that provably does not move the verdict" as *u8)
196}
nx_contentdiff_gate.nx source

`nx_contentdiff_gate.nx` source
