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

↩ module page · 479 lines · 30070 B
1// nx_undopath_gate.nx -- proves nx_undopath_lib, and CENSUSES every deploy row's reverse gear.
2//
3// THE THIRD QUESTION IN THE DEPLOY FAMILY. nx_deploycover_gate asks "is there a row at all";
4// nx_deploy_listen_gate asks "did the post-deploy check verify the INCOMING listener". This asks:
5// WHEN THE ROW'S REVERSE GEAR FIRES, DOES IT REVERSE THIS TARGET -- OR SOMEBODY ELSE'S?
6//
7// It exists because on 2026-09-03 the answer was "somebody else's" for 16 of 31 rows: they declared
8// `rollback`, and cmd_rollback() takes no target argument -- it renames sites.elf.prev over sites.elf and
9// kills sites.elf. /api/deploy's health watchdog invokes that field, so a failed deploy of any of those
10// daemons would AUTOMATICALLY have reverted the public front door and left the bad daemon live.
11//
12// ADVISORY ON THE CENSUS, HARD ON THE RULER. The pure classifier and the ratchet are teeth: they fail the
13// gate. The live census RATCHETS -- wrong-subject may only fall -- because a permanently-red detector is
14// one everybody learns to ignore, and because the honest remedy for a wrong row is a source change in the
15// control plane, not a blocked build. A RISE is RED and the baseline is NOT rewritten.
16//
17// WHY IT COMPOSES md_resolve_target INSTEAD OF PARSING THE CONF ITSELF: that function IS the resolution
18// /api/deploy performs -- primary knowledge/hosting path, cwd fallback, and the compiled-in builtin rows.
19// A hand-rolled parser would measure a DIFFERENT SUBJECT than the deploy plane actually reads, which is
20// the exact wrong-subject error this gate exists to catch. The row NAMES are enumerated from the conf
21// (that is a list, not a resolution); every rb verb comes from the shipping resolver.
22// license_tier: ORIGINAL   Read-only. No hw writes (Rule 26).   expect_exit: 0
23import "nx_syscalls.nx"
24import "nx_gate_verdict.nx"
25import "nx_gatekit_lib.nx"
26import "nx_undopath_lib.nx"
27import "_hdl_build/nx_mgmt_data.nx"
28
29const UG_FX: *u8 = "/tmp/nx_undopath_gate"
30const UG_FX_SRC: *u8 = "/tmp/nx_undopath_gate/fixture_hostctl.nx"
31const UG_FX_ABSENT: *u8 = "/tmp/nx_undopath_gate/does-not-exist.nx"
32const UG_FX_CONSTSRC: *u8 = "/tmp/nx_undopath_gate/fixture_consts.nx"
33// a verb whose body names its subject ONLY through a const -- the cmd_superrollback / cmd_toolchainrollback
34// shape. There is deliberately NO literal "nx_gamma.elf" inside the function body.
35const UG_FX_CONSTBODY: *u8 = "const HC_GAMMA_LIVE: *u8 = \"/srv/nx_gamma.elf\"\nconst HC_GAMMA_PREV: *u8 = \"/srv/nx_gamma.elf.prev\"\nfunc cmd_gammarollback() -> i64 {\n    let r: i64 = sys_renameat(HC_GAMMA_PREV, HC_GAMMA_LIVE)\n    return r\n}\nfunc cmd_other() -> i64 { return 0 }\n"
36const UG_FX_TRAILSRC: *u8 = "/tmp/nx_undopath_gate/fixture_trailing_comment.nx"
37// THE LIVE DEFECT, PLANTED: cmd_kapparollback is followed by the NEXT function's comment block, and that
38// comment names HC_LAMBDA_LIVE. A span that ends at the next `func` swallows that comment and resolves
39// nx_lambda.elf as this verb's subject -- which is exactly how cmd_loginrollback read as ambiguous while
40// being correct all along. This fixture fails against the old boundary and passes against the brace.
41const UG_FX_TRAILBODY: *u8 = "const HC_KAPPA_LIVE: *u8 = \"/srv/nx_kappa.elf\"\nconst HC_KAPPA_PREV: *u8 = \"/srv/nx_kappa.elf.prev\"\nconst HC_LAMBDA_LIVE: *u8 = \"/srv/nx_lambda.elf\"\nfunc cmd_kapparollback() -> i64 {\n    return sys_renameat(HC_KAPPA_PREV, HC_KAPPA_LIVE)\n}\n\n// LAMBDA deploy prep: the supervisor's HC_LAMBDA_LIVE guard then auto-launches it.\n// Idempotent and never-brick.\nfunc cmd_lambdadeploy() -> i64 {\n    return 0\n}\n"
42const UG_FX_PAIRSRC: *u8 = "/tmp/nx_undopath_gate/fixture_pair.nx"
43// a BRIDGING forward gear + its reverse gear + an UNRELATED reverse gear. The staged artifact
44// (nx_theta.sov.elf.new, in one directory) and the live artifact (nx_theta.elf, in another) differ exactly
45// as galxgw's do, so hops 1 and 2 cannot resolve the reverse gear and only the PAIR can.
46const UG_FX_PAIRBODY: *u8 = "const HC_T_SOVNEW: *u8 = \"/nishihost/nx_theta.sov.elf.new\"\nconst HC_T_NEW: *u8 = \"/srv/app/nx_theta.elf.new\"\nconst HC_T_LIVE: *u8 = \"/srv/app/nx_theta.elf\"\nconst HC_T_PREV: *u8 = \"/srv/app/nx_theta.elf.prev\"\nconst HC_I_LIVE: *u8 = \"/srv/app/nx_iota.elf\"\nconst HC_I_PREV: *u8 = \"/srv/app/nx_iota.elf.prev\"\nfunc cmd_thetadeploy() -> i64 {\n    hc_copyfile(HC_T_SOVNEW, HC_T_NEW)\n    return hc_publish(HC_T_NEW, HC_T_LIVE)\n}\nfunc cmd_thetarollback() -> i64 {\n    return sys_renameat(HC_T_PREV, HC_T_LIVE)\n}\nfunc cmd_iotarollback() -> i64 {\n    return sys_renameat(HC_I_PREV, HC_I_LIVE)\n}\n"
47const UG_HOSTCTL: *u8 = "buildroot/runtime/_hdl_build/nx_hostctl.nx"
48const UG_HOSTCTL_B: *u8 = "runtime/_hdl_build/nx_hostctl.nx"
49const UG_CONF: *u8 = "deploy_targets.conf"
50const UG_CONF_B: *u8 = "knowledge/hosting/deploy_targets.conf"
51const UG_RATCHET: *u8 = "knowledge/status/undopath.ratchet"
52const UG_RATCHET_B: *u8 = "../knowledge/status/undopath.ratchet"
53const UG_MODE: i64 = 420
54
55// fixture source: two verbs whose bodies name DIFFERENT artifacts, so the body-resolution teeth have a
56// real subject to get right and a real subject to get wrong.
57const UG_FX_BODY: *u8 = "func cmd_alpharollback() -> i64 {\n    let r: i64 = sys_renameat(\"nx_alpha.elf.prev\" as *u8, \"nx_alpha.elf\" as *u8)\n    return r\n}\nfunc cmd_betarollback() -> i64 {\n    let r: i64 = sys_renameat(\"nx_beta.elf.prev\" as *u8, \"nx_beta.elf\" as *u8)\n    return r\n}\n"
58
59const UG_ROWCAP: i64 = 64
60const UG_NAMEW: i64 = 64
61const UG_PATHCAP: i64 = 512
62const UG_SMALL: i64 = 256
63const UG_CONFCAP: i64 = 65536
64const UG_SRCCAP: i64 = 1048576
65const UG_NL: i64 = 10
66const UG_HASH: i64 = 35
67const UG_SP: i64 = 32
68
69func ug_slot(names: *u8, i: i64) -> *u8 { return ((names as i64) + i * UG_NAMEW) as *u8 }
70
71// enumerate ROW NAMES (field 0) out of the conf. A list, not a resolution -- every rb comes from
72// md_resolve_target below, so this cannot disagree with the deploy plane about what a row MEANS.
73func ug_row_names(path: *u8, names: *u8) -> i64 {
  let box: *i64 = sys_mmap(16) as *i64
  let buf: *u8 = sys_read_file(path, box)
  if (buf as i64) == 0 { return 0 }
  let n: i64 = box[0]
  if n <= 0 { return 0 }
  var cnt: i64 = 0
  var i: i64 = 0
  while i < n {
      let e: i64 = gk_eol(buf, i, n)
      if e > i {
          if (buf[i] as i64) != UG_HASH {
              if cnt < UG_ROWCAP {
                  let d: *u8 = ug_slot(names, cnt)
                  var w: i64 = 0
                  var p: i64 = i
                  while p < e {
                      if (buf[p] as i64) == UG_SP { p = e } else {
                          if w + 1 < UG_NAMEW { d[w] = buf[p]; w = w + 1 }
                          p = p + 1
                      }
                  }
                  d[w] = 0 as u8
                  if w > 0 { cnt = cnt + 1 }
              }
          }
      }
      i = e + 1
  }
  return cnt
103}
104
105func ug_read_src(a: *u8, b: *u8, box: *i64) -> *u8 {
  var buf: *u8 = sys_read_file(a, box)
  if (buf as i64) == 0 { buf = sys_read_file(b, box) }
  return buf
109}
110
111func ug_ratchet_read(a: *u8, b: *u8) -> i64 {
  let buf: *u8 = sys_mmap(UG_SMALL)
  var n: i64 = gk_read(a, buf, UG_SMALL - 1)
  if n <= 0 { n = gk_read(b, buf, UG_SMALL - 1) }
  if n <= 0 { return 0 - 1 }
  var v: i64 = 0
  var seen: i64 = 0
  var i: i64 = 0
  while i < n {
      let c: i64 = buf[i] as i64
      if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); seen = 1 } }
      i = i + 1
  }
  if seen == 0 { return 0 - 1 }
  return v
126}
127
128func main(argc: i64, argv: *i64) -> i64 {
  gv_head("nx_undopath_gate -- does each deploy target's REVERSE GEAR reverse its OWN subject? (pure classifier, body resolution, ratchet, live census)" as *u8)
  let ctr: *i64 = gv_ctr()
  gk_mkdir(UG_FX)
  gk_write(UG_FX_SRC, UG_FX_BODY)
  gk_rm(UG_FX_ABSENT)
  gv_check("fixture-reached-condition: fixture source present and the absent path absent" as *u8,
      gk_exists(UG_FX_SRC) * (1 - gk_exists(UG_FX_ABSENT)), ctr)
136
  // ---- PURE classifier: every branch, with the two catastrophic ones as named neg-controls ----
  gv_check("classify: the edge gear on the EDGE row is OWN-SUBJECT (correct for exactly one row)" as *u8,
      (up_classify(1, 1, 0, 0, 1, 0, 0) == UP_OWN) as i64, ctr)
  gv_check("neg-control-edge-gear-on-a-NON-edge-row-is-WRONG-SUBJECT (the 16-row defect: it reverts the front door)" as *u8,
      (up_classify(0, 1, 0, 0, 1, 0, 0) == UP_WRONG) as i64, ctr)
  gv_check("classify: the per-row gear pointed at ITSELF is OWN-SUBJECT" as *u8,
      (up_classify(0, 0, 1, 0, 1, 0, 0) == UP_OWN) as i64, ctr)
  gv_check("neg-control-per-row-gear-pointed-at-ANOTHER-row-is-WRONG-SUBJECT" as *u8,
      (up_classify(0, 0, 0, 1, 1, 0, 0) == UP_WRONG) as i64, ctr)
  gv_check("classify: an unimplemented verb is FAILSAFE (the dispatcher's proven no-op), never OWN" as *u8,
      (up_classify(0, 0, 0, 0, 0, 0, 0) == UP_FAILSAFE) as i64, ctr)
  // THE VACUITY THAT WAS IN THIS RULER UNTIL 2026-09-03: a row pointed at the per-row gear read OWN from
  // its own spelling, even where the control plane does not implement that gear. These two teeth are the
  // guard -- declaring a reverse gear is not the same as having one.
  gv_check("neg-control-a-per-row-gear-whose-DISPATCH-TARGET-does-not-exist-is-FAILSAFE-not-OWN (declaring a gear is not having one)" as *u8,
      (up_classify(0, 0, 1, 0, 0, 0, 0) == UP_FAILSAFE) as i64, ctr)
  gv_check("neg-control-the-EDGE-gear-with-no-cmd_rollback-in-the-control-plane-is-FAILSAFE-not-WRONG (an absent verb harms nobody)" as *u8,
      (up_classify(0, 1, 0, 0, 0, 0, 0) == UP_FAILSAFE) as i64, ctr)
  gv_check("classify: a dedicated verb whose body names THIS row's artifact is OWN-SUBJECT" as *u8,
      (up_classify(0, 0, 0, 0, 1, 1, 0) == UP_OWN) as i64, ctr)
  gv_check("neg-control-dedicated-verb-naming-ANOTHER-artifact-is-WRONG-SUBJECT (the docportal shape)" as *u8,
      (up_classify(0, 0, 0, 0, 1, 0, 1) == UP_WRONG) as i64, ctr)
  gv_check("classify: a body naming BOTH artifacts is UNPROVEN -- ambiguity abstains, never acquits" as *u8,
      (up_classify(0, 0, 0, 0, 1, 1, 1) == UP_UNPROVEN) as i64, ctr)
  gv_check("classify: a verb that exists but resolves to NO artifact is UNPROVEN, never OWN" as *u8,
      (up_classify(0, 0, 0, 0, 1, 0, 0) == UP_UNPROVEN) as i64, ctr)
  gv_check("classify: the edge gear is decided BEFORE body resolution (a body hit cannot launder it)" as *u8,
      (up_classify(0, 1, 0, 0, 1, 1, 0) == UP_WRONG) as i64, ctr)
  gv_bite("bite: the SAME classifier says WRONG for the edge gear off-edge and OWN for it on-edge" as *u8,
      (up_classify(0, 1, 0, 0, 1, 0, 0) == UP_WRONG) as i64,
      (up_classify(1, 1, 0, 0, 1, 0, 0) == UP_WRONG) as i64, ctr)
168
  // ---- body resolution over a fixture source with two rival artifacts ----
  let sbox: *i64 = sys_mmap(16) as *i64
  let fsrc: *u8 = sys_read_file(UG_FX_SRC, sbox)
  var fn: i64 = 0
  if (fsrc as i64) != 0 { fn = sbox[0] }
  let span: *i64 = sys_mmap(32) as *i64
  let found: i64 = up_verb_body(fsrc, fn, "alpharollback" as *u8, span)
  gv_check("fixture-reached-condition: the fixture source loaded and carries two rival verbs" as *u8,
      ((fn > 0) as i64) * ((up_find(fsrc, fn, "cmd_betarollback" as *u8) >= 0) as i64), ctr)
  gv_check("body: the span of cmd_alpharollback is found and bounded before the NEXT func" as *u8,
      (found as i64) * ((span[1] > span[0]) as i64), ctr)
  var body_own: i64 = 0
  var body_other: i64 = 0
  if found == 1 {
      let bp: *u8 = ((fsrc as i64) + span[0]) as *u8
      let bn: i64 = span[1] - span[0]
      if up_find(bp, bn, "nx_alpha.elf" as *u8) >= 0 { body_own = 1 }
      if up_find(bp, bn, "nx_beta.elf" as *u8) >= 0 { body_other = 1 }
  }
  gv_check("body: cmd_alpharollback's span names nx_alpha.elf and NOT nx_beta.elf (the span really is bounded)" as *u8,
      body_own * (1 - body_other), ctr)
  gv_check("neg-control-a-verb-that-does-not-exist-resolves-no-span" as *u8,
      (up_verb_body(fsrc, fn, "zzznosuchrollback" as *u8, span) == 0) as i64, ctr)
  let bnbuf: *u8 = sys_mmap(UG_SMALL)
  up_basename("/volume1/homes/elderwesto/nishihost/nx_fin_serve.elf" as *u8, bnbuf, UG_SMALL)
  gv_check("basename: a live path reduces to the artifact name a reverse gear must mention" as *u8,
      up_streq(bnbuf, "nx_fin_serve.elf" as *u8), ctr)
  // ---- the STEM and the CONST hop: the two reasons the first census left 8 rows UNPROVEN ----
  let stbuf: *u8 = sys_mmap(UG_SMALL)
  up_stem("nx_mgmt_api.elf.new" as *u8, stbuf, UG_SMALL)
  gv_check("stem: a STAGED name reduces to what a reverse gear actually touches (nx_mgmt_api.elf.new -> nx_mgmt_api.elf)" as *u8,
      up_streq(stbuf, "nx_mgmt_api.elf" as *u8), ctr)
  up_stem("nx_torrent_daemon.sov.elf.new" as *u8, stbuf, UG_SMALL)
  gv_check("stem: a .sov.elf.new staged name reduces to its .sov.elf stem" as *u8,
      up_streq(stbuf, "nx_torrent_daemon.sov.elf" as *u8), ctr)
  up_stem("/a/b/nx_plain.elf" as *u8, stbuf, UG_SMALL)
  gv_check("neg-control-stem-leaves-a-name-with-no-.new-suffix-untouched" as *u8,
      up_streq(stbuf, "nx_plain.elf" as *u8), ctr)
  // fixture: a verb naming its subject ONLY through a const, which is the cmd_superrollback shape
  gk_write(UG_FX_CONSTSRC, UG_FX_CONSTBODY)
  let cbox: *i64 = sys_mmap(16) as *i64
  let csrc: *u8 = sys_read_file(UG_FX_CONSTSRC, cbox)
  var cn: i64 = 0
  if (csrc as i64) != 0 { cn = cbox[0] }
  let cspan: *i64 = sys_mmap(32) as *i64
  let cfound: i64 = up_verb_body(csrc, cn, "gammarollback" as *u8, cspan)
  gv_check("fixture-reached-condition: the const-only fixture loaded and its body carries NO literal artifact name" as *u8,
      ((cn > 0) as i64) * (cfound as i64) * ((up_find(((csrc as i64) + cspan[0]) as *u8, cspan[1] - cspan[0], "nx_gamma.elf" as *u8) < 0) as i64), ctr)
  let cvb: *u8 = sys_mmap(UG_PATHCAP)
  gv_check("const: a const's VALUE is resolvable by name from the source" as *u8,
      (up_const_value(csrc, cn, "HC_GAMMA_LIVE" as *u8, cvb, UG_PATHCAP) as i64) * up_streq(cvb, "/srv/nx_gamma.elf" as *u8), ctr)
  gv_check("CONST HOP: a body that names its subject ONLY through a const still resolves as naming it" as *u8,
      up_body_names(csrc, cn, cspan[0], cspan[1], "nx_gamma.elf" as *u8), ctr)
  gv_check("neg-control-const-hop-does-not-invent-a-match-for-an-unrelated-artifact" as *u8,
      (1 - up_body_names(csrc, cn, cspan[0], cspan[1], "nx_delta.elf" as *u8)), ctr)
  gv_check("neg-control-an-empty-stem-never-matches (a row with no resolvable artifact cannot read as OWN)" as *u8,
      (1 - up_body_names(csrc, cn, cspan[0], cspan[1], "" as *u8)), ctr)
226
  // ---- SPAN BOUNDARY: a body must not absorb the NEXT function's comment block ----
  gk_write(UG_FX_TRAILSRC, UG_FX_TRAILBODY)
  let tbox: *i64 = sys_mmap(16) as *i64
  let tsrc: *u8 = sys_read_file(UG_FX_TRAILSRC, tbox)
  var tn: i64 = 0
  if (tsrc as i64) != 0 { tn = tbox[0] }
  let tsp: *i64 = sys_mmap(32) as *i64
  let tfound: i64 = up_verb_body(tsrc, tn, "kapparollback" as *u8, tsp)
  gv_check("fixture-reached-condition: the trailing-comment fixture loaded, the span resolved, and the file DOES carry the neighbour's const" as *u8,
      ((tn > 0) as i64) * tfound * ((up_find(tsrc, tn, "HC_LAMBDA_LIVE" as *u8) >= 0) as i64), ctr)
  gv_check("SPAN BOUNDARY: the span ends at the verb's own closing brace, so it EXCLUDES the next function's comment block" as *u8,
      (up_find(((tsrc as i64) + tsp[0]) as *u8, tsp[1] - tsp[0], "LAMBDA deploy prep" as *u8) < 0) as i64, ctr)
  gv_check("neg-control-a-verb-does-NOT-resolve-its-NEIGHBOUR's-artifact (the live opaquelogin false-ambiguity, bitten)" as *u8,
      (1 - up_body_names(tsrc, tn, tsp[0], tsp[1], "nx_lambda.elf" as *u8)), ctr)
  gv_check("SPAN BOUNDARY: and it still resolves its OWN subject through the const hop (the tightening did not blind it)" as *u8,
      up_body_names(tsrc, tn, tsp[0], tsp[1], "nx_kappa.elf" as *u8), ctr)
243
  // ---- HOP 3: THE PAIR. artifact-name reduction, the pair hop, and the additivity proof ----
  let anb: *u8 = sys_mmap(UG_SMALL)
  up_artifact_name("/srv/nx_theta.elf.new" as *u8, anb, UG_SMALL)
  gv_check("artifact-name: a staged .new reduces to the live artifact" as *u8,
      up_streq(anb, "nx_theta.elf" as *u8), ctr)
  up_artifact_name("/srv/nx_theta.elf.prev" as *u8, anb, UG_SMALL)
  gv_check("artifact-name: a banked .prev reduces to the SAME live artifact (that shared token IS the pair)" as *u8,
      up_streq(anb, "nx_theta.elf" as *u8), ctr)
  up_artifact_name("/srv/nx_theta.elf" as *u8, anb, UG_SMALL)
  gv_check("neg-control-artifact-name-leaves-a-live-path-untouched" as *u8,
      up_streq(anb, "nx_theta.elf" as *u8), ctr)
255
  // fixture: a BRIDGING forward gear (staged name differs from the live name by a .sov infix AND a
  // directory) beside its reverse gear -- the galxgw shape, which hops 1 and 2 both correctly miss.
  gk_write(UG_FX_PAIRSRC, UG_FX_PAIRBODY)
  let pbox: *i64 = sys_mmap(16) as *i64
  let psrc: *u8 = sys_read_file(UG_FX_PAIRSRC, pbox)
  var pn: i64 = 0
  if (psrc as i64) != 0 { pn = pbox[0] }
  let fsp: *i64 = sys_mmap(32) as *i64
  let rsp: *i64 = sys_mmap(32) as *i64
  let osp: *i64 = sys_mmap(32) as *i64
  let ffound: i64 = up_verb_body(psrc, pn, "thetadeploy" as *u8, fsp)
  let rfound: i64 = up_verb_body(psrc, pn, "thetarollback" as *u8, rsp)
  let ofound: i64 = up_verb_body(psrc, pn, "iotarollback" as *u8, osp)
  gv_check("fixture-reached-condition: the bridging-pair fixture loaded and all three verb spans resolved" as *u8,
      ((pn > 0) as i64) * ffound * rfound * ofound, ctr)
  // the whole point: hop 1+2 CANNOT see this, so the pair hop is not measuring something already covered
  gv_check("fixture-reached-condition: the reverse gear does NOT name the row's STAGED stem (hops 1+2 both miss it)" as *u8,
      (1 - up_body_names(psrc, pn, rsp[0], rsp[1], "nx_theta.sov.elf" as *u8)), ctr)
  gv_check("PAIR HOP: a reverse gear that names the artifact its own FORWARD gear writes resolves as OWN-SUBJECT" as *u8,
      up_pair_common(psrc, pn, fsp[0], fsp[1], rsp[0], rsp[1]), ctr)
  gv_check("neg-control-pair-hop-does-not-pair-a-forward-gear-with-ANOTHER-artifact's-reverse-gear" as *u8,
      (1 - up_pair_common(psrc, pn, fsp[0], fsp[1], osp[0], osp[1])), ctr)
  gv_check("neg-control-pair-hop-on-an-empty-span-cannot-match (a missing forward verb never acquits)" as *u8,
      (1 - up_pair_common(psrc, pn, 0, 0, rsp[0], rsp[1])), ctr)
280
  // ADDITIVITY, PROVEN EXHAUSTIVELY OVER ALL 128 INPUT COMBINATIONS rather than asserted in a comment.
  // The safety claim is that the pair hop can ONLY convert UNPROVEN -> OWN. If it could convert WRONG ->
  // OWN it would acquit exactly the defect this gate exists to find, so this is the load-bearing tooth.
  var addok: i64 = 1
  var neutok: i64 = 1
  var rescued: i64 = 0
  var m: i64 = 0
  while m < 128 {
      let a0: i64 = m - (m / 2) * 2
      let a1: i64 = (m / 2) - (m / 4) * 2
      let a2: i64 = (m / 4) - (m / 8) * 2
      let a3: i64 = (m / 8) - (m / 16) * 2
      let a4: i64 = (m / 16) - (m / 32) * 2
      let a5: i64 = (m / 32) - (m / 64) * 2
      let a6: i64 = m / 64
      let base: i64 = up_classify(a0, a1, a2, a3, a4, a5, a6)
      let with1: i64 = up_classify_pair(a0, a1, a2, a3, a4, a5, a6, 1)
      let with0: i64 = up_classify_pair(a0, a1, a2, a3, a4, a5, a6, 0)
      if with0 != base { neutok = 0 }
      if base == UP_UNPROVEN {
          if with1 != UP_OWN { addok = 0 }
          rescued = rescued + 1
      } else {
          if with1 != base { addok = 0 }
      }
      m = m + 1
  }
  gv_check("PAIR ADDITIVITY (all 128 combinations): pair_own=1 changes ONLY the UNPROVEN verdicts -- it can never turn WRONG into OWN" as *u8,
      addok, ctr)
  gv_check("neg-control-pair-hop-is-a-no-op-when-it-does-not-fire (pair_own=0 reproduces the incumbent verdict on all 128)" as *u8,
      neutok, ctr)
  gv_check("fixture-reached-condition: the additivity sweep actually visited UNPROVEN cases (a vacuous sweep would prove nothing)" as *u8,
      (rescued > 0) as i64, ctr)
314
  // ---- ratchet arithmetic ----
  gv_check("ratchet: first sight baselines (floor -1, wrong 3 -> 3)" as *u8, (up_ratchet_next(0 - 1, 3) == 3) as i64, ctr)
  gv_check("ratchet: falls (3 -> 0)" as *u8, (up_ratchet_next(3, 0) == 0) as i64, ctr)
  gv_check("ratchet: holds (0 -> 0)" as *u8, (up_ratchet_next(0, 0) == 0) as i64, ctr)
  gv_check("neg-control-ratchet-refuses-to-rise (0 -> 2 is -1, baseline NOT rewritten)" as *u8,
      (up_ratchet_next(0, 2) == (0 - 1)) as i64, ctr)
321
  // ---- LIVE CENSUS: every row, resolved through the shipping resolver ----
  let names: *u8 = sys_mmap(UG_ROWCAP * UG_NAMEW)
  var nrows: i64 = ug_row_names(UG_CONF, names)
  if nrows == 0 { nrows = ug_row_names(UG_CONF_B, names) }
  let hbox: *i64 = sys_mmap(16) as *i64
  let hsrc: *u8 = ug_read_src(UG_HOSTCTL, UG_HOSTCTL_B, hbox)
  var hn: i64 = 0
  if (hsrc as i64) != 0 { hn = hbox[0] }
  gv_need("live: deploy_targets.conf rows enumerated (a census over zero rows must never read as clean)" as *u8, (nrows > 0) as i64, ctr)
  gv_need("live: control-plane source readable (an unreadable reverse gear cannot be judged)" as *u8, (hn > 0) as i64, ctr)
332
  var c_own: i64 = 0
  var c_wrong: i64 = 0
  var c_fail: i64 = 0
  var c_unpr: i64 = 0
  if nrows > 0 { if hn > 0 {
      let kindb: *i64 = sys_mmap(16) as *i64
      let srcb: *u8 = sys_mmap(UG_PATHCAP)
      let subb: *u8 = sys_mmap(UG_SMALL)
      let urlb: *u8 = sys_mmap(UG_SMALL)
      let rbb: *u8 = sys_mmap(UG_SMALL)
      var r: i64 = 0
      while r < nrows {
          let nm: *u8 = ug_slot(names, r)
          md_resolve_target(UG_CONF, nm, 0, up_len(nm), kindb, srcb, subb, urlb, rbb)
          let is_edge: i64 = up_streq(nm, UP_EDGE_ROW)
          let rb_edge: i64 = up_streq(rbb, UP_EDGE_GEAR)
          var rb_self: i64 = 0
          var rb_other: i64 = 0
          if up_prefix(rbb, UP_PERROW_PFX) == 1 {
              let who: *u8 = ((rbb as i64) + UP_PERROW_PFXLEN) as *u8
              if up_streq(who, nm) == 1 { rb_self = 1 } else { rb_other = 1 }
          }
          var vex: i64 = 0
          var bown: i64 = 0
          var bother: i64 = 0
          let othb: *u8 = sys_mmap(UG_SMALL)
          othb[0] = 0 as u8
          // ASK ABOUT THE VERB THAT WILL ACTUALLY RUN, for EVERY branch. The edge gear dispatches to
          // cmd_rollback and the per-row gear to cmd_gdeploy_rollback; only the third case runs a verb
          // named by the row itself. Resolving existence for all three is what stops a row from reading
          // OWN-SUBJECT purely because someone wrote the right word in field 5.
          var vname: *u8 = rbb
          if rb_edge == 1 { vname = UP_EDGE_GEAR }
          if rb_self == 1 { vname = UP_PERROW_VERB }
          if rb_other == 1 { vname = UP_PERROW_VERB }
          if up_verb_body(hsrc, hn, vname, span) == 1 { vex = 1 }
          if rb_edge == 0 { if rb_self == 0 { if rb_other == 0 {
              if vex == 1 {
                  let bp2: *u8 = ((hsrc as i64) + span[0]) as *u8
                  let bn2: i64 = span[1] - span[0]
                  // OWN: the verb body names THIS row's artifact STEM, directly or via a const it mentions.
                  // The stem (not the staged .new name) is what a REVERSE gear touches -- see up_stem.
                  let ownb: *u8 = sys_mmap(UG_SMALL)
                  up_stem(srcb, ownb, UG_SMALL)
                  if up_body_names(hsrc, hn, span[0], span[1], ownb) == 1 { bown = 1 }
                  // OTHER: it names some sibling row's staged artifact instead
                  var q: i64 = 0
                  while q < nrows {
                      if q != r {
                          let nm2: *u8 = ug_slot(names, q)
                          let k2: *i64 = sys_mmap(16) as *i64
                          let s2: *u8 = sys_mmap(UG_PATHCAP)
                          let u2: *u8 = sys_mmap(UG_SMALL)
                          let v2: *u8 = sys_mmap(UG_SMALL)
                          let b2: *u8 = sys_mmap(UG_SMALL)
                          md_resolve_target(UG_CONF, nm2, 0, up_len(nm2), k2, s2, u2, v2, b2)
                          let onb: *u8 = sys_mmap(UG_SMALL)
                          up_stem(s2, onb, UG_SMALL)
                          if up_len(onb) > 0 { if up_streq(onb, ownb) == 0 {
                              if up_body_names(hsrc, hn, span[0], span[1], onb) == 1 {
                                  bother = 1
                                  // NAME THE COLLIDING STEM. "other=1" alone sends the next reader to
                                  // re-derive which of 30 siblings matched -- the reason is in hand HERE.
                                  if up_len(othb) == 0 { up_stem(s2, othb, UG_SMALL) }
                              }
                          } }
                      }
                      q = q + 1
                  }
              }
          } } }
          // HOP 3, THE PAIR: a reverse gear is correct iff it acts on the artifact its own FORWARD gear
          // writes. subb is field 4 -- the deploy sub the row itself declares -- so this compares the
          // actual pair, not the row's staged filename, which a legitimate bridge makes differ.
          var pown: i64 = 0
          if vex == 1 { if bown == 0 { if bother == 0 {
              let fspan: *i64 = sys_mmap(16) as *i64
              if up_verb_body(hsrc, hn, subb, fspan) == 1 {
                  pown = up_pair_common(hsrc, hn, fspan[0], fspan[1], span[0], span[1])
              }
          } } }
          let st: i64 = up_classify_pair(is_edge, rb_edge, rb_self, rb_other, vex, bown, bother, pown)
          if st == UP_OWN { c_own = c_own + 1 }
          if st == UP_WRONG { c_wrong = c_wrong + 1 }
          if st == UP_FAILSAFE { c_fail = c_fail + 1 }
          if st == UP_UNPROVEN { c_unpr = c_unpr + 1 }
          // a count without a worklist is not actionable: name every row that is not OWN
          if st != UP_OWN {
              gv_puts("  " as *u8); gv_puts(up_state_name(st))
              gv_puts(" row=" as *u8); gv_puts(nm)
              gv_puts(" rb=" as *u8); gv_puts(rbb)
              // THE REASON TRAVELS WITH THE COUNT: a worklist row that does not say WHICH conjunct failed
              // costs the next reader the whole investigation again. These flags are already in hand.
              gv_puts(" [verb=" as *u8); gv_num(vex)
              gv_puts(" own=" as *u8); gv_num(bown)
              gv_puts(" other=" as *u8); gv_num(bother)
              if bother == 1 { gv_puts(" collides_with=" as *u8); gv_puts(othb) }
              gv_puts(" pair=" as *u8); gv_num(pown)
              gv_puts(" fwd=" as *u8); gv_puts(subb)
              gv_puts("]\n" as *u8)
          }
          r = r + 1
      }
  } }
  // DECLARE THE SUBJECT. This census reads the control plane's SOURCE, so every verdict is a statement
  // about what hostctl IMPLEMENTS -- not about what the deployed binary currently does. Those differ
  // whenever the artifact is BEHIND its source, which is exactly the window in which a freshly declared
  // reverse gear is real in the source and still absent from the running binary. Saying so here costs
  // one line and stops the census being read as a liveness claim it never made.
  gv_puts("UNDOPATH subject=SOURCE hostctl_src_bytes=" as *u8); gv_num(hn)
  gv_puts(" (a gear counted OWN is IMPLEMENTED; whether it is DEPLOYED is nx_artifactdrift's BEHIND axis, not this gate's)\n" as *u8)
  gv_puts("UNDOPATH rows=" as *u8); gv_num(nrows)
  gv_puts(" own=" as *u8); gv_num(c_own)
  gv_puts(" wrong=" as *u8); gv_num(c_wrong)
  gv_puts(" failsafe=" as *u8); gv_num(c_fail)
  gv_puts(" unproven=" as *u8); gv_num(c_unpr)
  gv_puts("\n" as *u8)
  gv_check("live: the partition SUMS to the row count (an unreconciled census is a leak)" as *u8,
      ((c_own + c_wrong + c_fail + c_unpr) == nrows) as i64, ctr)
  let floor: i64 = ug_ratchet_read(UG_RATCHET, UG_RATCHET_B)
  let nxt: i64 = up_ratchet_next(floor, c_wrong)
  gv_puts("  ratchet floor=" as *u8); gv_num(floor)
  gv_puts(" observed_wrong=" as *u8); gv_num(c_wrong)
  gv_puts("\n" as *u8)
  gv_check("live-ratchet: wrong-subject rows are at or below the persisted floor (a RISE is RED and the floor is NOT rewritten)" as *u8,
      (nxt >= 0) as i64, ctr)
  if nxt >= 0 {
      if floor < 0 {
          let wb: *u8 = sys_mmap(UG_SMALL)
          let wn: i64 = gk_catn(wb, 0, nxt)
          wb[wn] = UG_NL as u8
          wb[wn + 1] = 0 as u8
          gk_write(UG_RATCHET, wb)
          gv_puts("  UNDOPATH-RATCHET baselined at " as *u8); gv_num(nxt); gv_puts("\n" as *u8)
      }
      if floor > nxt {
          let wb2: *u8 = sys_mmap(UG_SMALL)
          let wn2: i64 = gk_catn(wb2, 0, nxt)
          wb2[wn2] = UG_NL as u8
          wb2[wn2 + 1] = 0 as u8
          gk_write(UG_RATCHET, wb2)
          gv_puts("  UNDOPATH-RATCHET tightened to " as *u8); gv_num(nxt); gv_puts("\n" as *u8)
      }
  }
  return gv_verdict("nx_undopath_gate" as *u8, ctr,
      "the pure classifier over every branch incl. both catastrophic neg-controls, verb-body span resolution on a two-rival fixture, basename reduction, ratchet arithmetic, and a live census of every deploy row resolved through the SHIPPING md_resolve_target -- naming each row that is not OWN-SUBJECT" as *u8)
479}
nx_undopath_gate.nx source

`nx_undopath_gate.nx` source
