code wiki / _hdl_build / nx_adoptdelta_gate.nx

nx_adoptdelta_gate.nx source

↩ module page · 176 lines · 12149 B

1// nx_adoptdelta_gate.nx -- THE REFEREE for nx_deltaclass `adoptdelta` (DM7, devmgmt rung). 2// END-TO-END: forks the DEPLOYED nx_deltaclass elf, so it grades the artifact callers run. 3// 4// The accept rule this enforces, verbatim from devmgmt.plan: "two consecutive beats emit deltas whose 5// arithmetic reconciles against the underlying logs, and any row whose reference is REF-FOSSIL is 6// excluded from the promotable delta rather than counted in it." 7// 8// The fixture is built so that a WRONG emitter cannot pass by luck. It carries, in one log: 9// * two PRODUCTION rows whose every class delta is a different number, so a transposed column shows; 10// * a GATE-FIXTURE row (reg= names another registry) with wildly different values BETWEEN them -- 11// an emitter that grades it as a beat gets visibly wrong deltas, which is the real hazard: the 12// live log genuinely contains a `distinct=6` fixture census between two `distinct=963` sweeps; 13// * a LEGACY row with no reg= at all -- UNKNOWN-PROVENANCE is its own bucket, and folding it into 14// either side is the "unrecognised value falls into a known bucket" defect; 15// * a PRODUCTION row whose own classes do not sum, which must be COUNTED as malformed rather than 16// silently averaged in; 17// * a `xstale=999` decoy immediately before the real ` stale=3`, because a key read by substring 18// rather than at a token boundary reports a different column under the right name -- a confident 19// wrong answer, the hardest kind to notice. 20// Fixtures live under /tmp/nx_adoptdelta_gate/ and are rewritten O_TRUNC on every run (idempotent); 21// a gate that shares scratch with a production path grades the fixture, not the code. 22// license_tier: ORIGINAL Read-only outside /tmp. No hw writes (Rule 26). 23import "nx_syscalls.nx" 24import "nx_sovjson_lib.nx" 25import "nx_gate_verdict.nx" 26import "nx_tool_run.nx" 27 28const AG_MODE_644: i64 = 420 29const AG_MODE_755: i64 = 493 30const AG_PATH: i64 = 512 31const AG_FIX: i64 = 65536 32const AG_OUT: i64 = 1048576 33const AG_EXIT_SKIP: i64 = 3 34const AG_RC_REFUSE: i64 = 3 35 36func ag_wr(path: *u8, buf: *u8, n: i64) -> i64 { 37 let fd: i64 = sys_openat_wr(path, AG_MODE_644) 38 if fd < 0 { return 0 - 1 } 39 sys_write(fd, buf, n) 40 sys_close(fd) 41 return n 42} 43func ag_run(subj: *u8, a1: *u8, a2: *u8, a3: *u8, a4: *u8, out: *u8, cl: *i64) -> i64 { 44 let av: *i64 = sys_mmap(64) as *i64 45 av[0] = subj as i64 46 av[1] = a1 as i64 47 av[2] = a2 as i64 48 av[3] = a3 as i64 49 av[4] = a4 as i64 50 av[5] = 0 51 return tr_run_capture(subj, av, out, AG_OUT - 8, cl) 52} 53 54func main(argc: i64, argv: *i64) -> i64 { 55 let ctr: *i64 = gv_ctr() 56 gv_head("nx_adoptdelta_gate -- a fixture census is not a beat, and a level is not a trajectory" as *u8) 57 58 let subj: *u8 = sys_mmap(AG_PATH) 59 var have: i64 = 0 60 if argc >= 2 { var z: i64 = sj_cat(subj, 0, argv[1] as *u8); subj[z] = 0 as u8; have = 1 } 61 if have == 0 { if sj_allow_path("nx_deltaclass" as *u8, subj) == 1 { have = 1 } } 62 if have == 0 { var z2: i64 = sj_cat(subj, 0, "./nx_deltaclass.elf" as *u8); subj[z2] = 0 as u8; have = 1 } 63 64 let root: *u8 = "/tmp/nx_adoptdelta_gate" as *u8 65 let flog: *u8 = "/tmp/nx_adoptdelta_gate/drift.log" as *u8 66 let fone: *u8 = "/tmp/nx_adoptdelta_gate/one_prod_row.log" as *u8 67 let fcat: *u8 = "/tmp/nx_adoptdelta_gate/catalog.capture" as *u8 68 let fabs: *u8 = "/tmp/nx_adoptdelta_gate/absent.log" as *u8 69 let prodreg: *u8 = "prod.conf" as *u8 70 let dash: *u8 = "-" as *u8 71 sys_mkdir(root, AG_MODE_755) 72 73 let b: *u8 = sys_mmap(AG_FIX) 74 var o: i64 = 0 75 // PRODUCTION but self-inconsistent: 1+1+0+0+0 != 10, so it must be COUNTED, never averaged in 76 o = sj_cat(b, o, "epoch=50 reg=prod.conf distinct=10 identical=1 stale=1 behind=1 ahead=0 resized=0 nobuild=0 noserved=0 stagedptr=0 sum=10 partition=BROKEN\n" as *u8) 77 // PRODUCTION beat A 78 o = sj_cat(b, o, "epoch=100 reg=prod.conf distinct=10 identical=4 stale=4 behind=2 ahead=1 resized=1 nobuild=1 noserved=0 stagedptr=1 sum=10 considerable=3 ref_fresh=2 ref_fossil=0 own_undeclared=3 own_inflight=1 partition=RECONCILES\n" as *u8) 79 // LEGACY, no reg= -- pre-dates the provenance stamp. UNKNOWN-PROVENANCE, its own bucket. 80 o = sj_cat(b, o, "epoch=150 distinct=999 identical=999 stale=0 behind=0 ahead=0 resized=0 nobuild=0 noserved=0 stagedptr=0 sum=999 partition=RECONCILES\n" as *u8) 81 // GATE FIXTURE census -- reg= names ANOTHER registry. Grading this as a beat is the real hazard. 82 o = sj_cat(b, o, "epoch=160 reg=gatefixture.conf distinct=6 identical=1 stale=5 behind=4 ahead=1 resized=0 nobuild=0 noserved=0 stagedptr=0 sum=6 considerable=0 ref_fresh=0 ref_fossil=0 own_undeclared=0 own_inflight=0 partition=RECONCILES\n" as *u8) 83 // PRODUCTION beat B, carrying the token-boundary decoy 84 o = sj_cat(b, o, "epoch=200 reg=prod.conf xstale=999 distinct=12 identical=7 stale=3 behind=1 ahead=1 resized=1 nobuild=1 noserved=0 stagedptr=1 sum=12 considerable=5 ref_fresh=3 ref_fossil=1 own_undeclared=4 own_inflight=2 partition=RECONCILES\n" as *u8) 85 let w1: i64 = ag_wr(flog, b, o) 86 o = 0 87 o = sj_cat(b, o, "epoch=100 reg=prod.conf distinct=10 identical=4 stale=4 behind=2 ahead=1 resized=1 nobuild=1 noserved=0 stagedptr=1 sum=10 partition=RECONCILES\n" as *u8) 88 o = sj_cat(b, o, "epoch=160 reg=gatefixture.conf distinct=6 identical=1 stale=5 behind=4 ahead=1 resized=0 nobuild=0 noserved=0 stagedptr=0 sum=6 partition=RECONCILES\n" as *u8) 89 let w2: i64 = ag_wr(fone, b, o) 90 o = 0 91 o = sj_cat(b, o, " VERDICT REGISTERED-DARK (S4) -- callable, authorised, no MCP invocation on record.\n" as *u8) 92 o = sj_cat(b, o, " VERDICT REGISTERED-DARK (S4) -- callable, authorised, no MCP invocation on record.\n" as *u8) 93 o = sj_cat(b, o, " VERDICT SOURCE-ONLY (S2) -- source exists, no shipped binary.\n" as *u8) 94 let w3: i64 = ag_wr(fcat, b, o) 95 sys_unlinkat(fabs) 96 97 var fixok: i64 = 0 98 if w1 > 0 { if w2 > 0 { if w3 > 0 { fixok = 1 } } } 99 gv_check("fixture-written-all-three (assert the fixture reached the condition before the outcome)" as *u8, fixok, ctr) 100 101 let out: *u8 = sys_mmap(AG_OUT) 102 let cl: *i64 = sys_mmap(16) as *i64 103 let rc: i64 = ag_run(subj, "adoptdelta" as *u8, flog, prodreg, dash, out, cl) 104 let n: i64 = cl[0] 105 if n <= 0 { 106 gv_puts("SKIP subject produced no output -- build/deploy nx_deltaclass, then re-run: " as *u8) 107 gv_puts(subj) 108 gv_puts("\n" as *u8) 109 sys_exit(AG_EXIT_SKIP) 110 return AG_EXIT_SKIP 111 } 112 gv_check("subject-ran-and-exited-zero-on-a-two-beat-log" as *u8, 1 - rc, ctr) 113 gv_check("subject-examined-a-nonzero-population-of-rows" as *u8, tr_contains(out, n, "production_rows=3" as *u8), ctr) 114 115 // ---- anti-vacuity: the deltas themselves, every class a DIFFERENT number ---- 116 gv_check("anti-vacuity-distinct-delta-is-exactly-plus-2" as *u8, tr_contains(out, n, "DELTA distinct prev=10 cur=12 d=2" as *u8), ctr) 117 gv_check("anti-vacuity-identical-delta-is-exactly-plus-3" as *u8, tr_contains(out, n, "DELTA identical prev=4 cur=7 d=3" as *u8), ctr) 118 gv_check("anti-vacuity-stale-delta-is-exactly-minus-1" as *u8, tr_contains(out, n, "DELTA stale prev=4 cur=3 d=-1" as *u8), ctr) 119 gv_check("behind-delta-is-exactly-minus-1-and-ahead-is-flat" as *u8, tr_contains(out, n, "DELTA behind prev=2 cur=1 d=-1" as *u8), ctr) 120 gv_check("ahead-the-class-a-promote-must-never-touch-is-reported-separately" as *u8, tr_contains(out, n, "DELTA ahead prev=1 cur=1 d=0" as *u8), ctr) 121 gv_check("owner-signal-deltas-travel-with-the-drift-deltas" as *u8, tr_contains(out, n, "DELTA own_undeclared prev=3 cur=4 d=1" as *u8), ctr) 122 123 // ---- provenance: THE guard, and each wrong answer has its own named control ---- 124 gv_check("provenance-partition-is-3-production-1-other-registry-1-unknown" as *u8, tr_contains(out, n, "production=3 other_registry=1 unknown_provenance=1" as *u8), ctr) 125 gv_check("provenance-partition-prints-its-sum-and-it-reconciles" as *u8, tr_contains(out, n, "sum=5 sum_ok=1" as *u8), ctr) 126 gv_check("neg-control-the-gate-fixture-census-is-NOT-one-of-the-two-beats" as *u8, tr_contains(out, n, "prev_epoch=100 cur_epoch=200" as *u8), ctr) 127 var nf: i64 = 1 128 if tr_contains(out, n, "cur=6 " as *u8) == 1 { nf = 0 } 129 gv_check("neg-control-no-delta-row-carries-the-fixture-census-value" as *u8, nf, ctr) 130 var nl: i64 = 1 131 if tr_contains(out, n, "cur=999" as *u8) == 1 { nl = 0 } 132 if tr_contains(out, n, "prev=999" as *u8) == 1 { nl = 0 } 133 gv_check("neg-control-no-delta-row-carries-the-legacy-unstamped-value" as *u8, nl, ctr) 134 gv_check("neg-control-a-key-read-at-a-token-boundary-ignores-the-xstale-decoy" as *u8, tr_contains(out, n, "cur=3 d=-1" as *u8), ctr) 135 gv_check("a-production-row-whose-classes-do-not-sum-is-COUNTED-not-averaged-in" as *u8, tr_contains(out, n, "malformed_production_rows=1" as *u8), ctr) 136 gv_check("both-chosen-beats-are-individually-partition-checked" as *u8, tr_contains(out, n, "prev_row_partition_ok=1 cur_row_partition_ok=1" as *u8), ctr) 137 138 // ---- the accept rule: the arithmetic reconciles, at both levels ---- 139 gv_check("ACCEPT-the-delta-of-the-partition-is-itself-a-partition-and-it-sums" as *u8, tr_contains(out, n, "d_distinct=2 d_classes_sum=2 delta_sum_ok=1" as *u8), ctr) 140 gv_check("ACCEPT-the-stale-sub-partition-delta-also-sums" as *u8, tr_contains(out, n, "d_stale=-1 d_stale_sub_sum=-1 stale_sub_sum_ok=1" as *u8), ctr) 141 gv_check("ACCEPT-promotable-delta-excludes-REF-FOSSIL-by-construction" as *u8, tr_contains(out, n, "PROMOTABLE prev=3 cur=5 d=2 fossil_excluded_by_construction=1" as *u8), ctr) 142 gv_check("ref_fossil-is-still-PUBLISHED-beside-the-promotable-delta-not-hidden" as *u8, tr_contains(out, n, "cur_ref_fossil=1" as *u8), ctr) 143 gv_check("the-final-line-carries-the-whole-run-verdict-as-sum_ok" as *u8, tr_contains(out, n, "ADOPTDELTA production_rows=3 d_distinct=2 d_stale=-1 sum_ok=1" as *u8), ctr) 144 145 // ---- the catalog axis: abstains when blind, tallies when fed ---- 146 gv_check("catalog-axis-ABSTAINS-and-names-its-input-when-not-given-one" as *u8, tr_contains(out, n, "CATALOG UNMEASURED input=" as *u8), ctr) 147 let rc2: i64 = ag_run(subj, "adoptdelta" as *u8, flog, prodreg, fcat, out, cl) 148 var cok: i64 = 0 149 if rc2 == 0 { 150 if tr_contains(out, cl[0], "CATALOG-CLASS REGISTERED-DARK n=2" as *u8) == 1 { 151 if tr_contains(out, cl[0], "CATALOG-CLASS SOURCE-ONLY n=1" as *u8) == 1 { cok = 1 } 152 } 153 } 154 gv_check("catalog-axis-tallies-a-real-nx_catalog-capture-per-verdict-class" as *u8, cok, ctr) 155 gv_check("catalog-tally-prints-its-own-partition-and-it-reconciles" as *u8, tr_contains(out, cl[0], "classes_sum=3 names=3 sum_ok=1" as *u8), ctr) 156 157 // ---- fail-closed: an instrument that cannot see refuses, it never reports zero movement ---- 158 let rc3: i64 = ag_run(subj, "adoptdelta" as *u8, fone, prodreg, dash, out, cl) 159 var r1: i64 = 0 160 if rc3 == AG_RC_REFUSE { if tr_contains(out, cl[0], "A LEVEL CANNOT EXPRESS A TRAJECTORY" as *u8) == 1 { r1 = 1 } } 161 gv_check("neg-control-one-production-row-REFUSES-rather-than-emitting-a-zero-delta" as *u8, r1, ctr) 162 let rc4: i64 = ag_run(subj, "adoptdelta" as *u8, fabs, prodreg, dash, out, cl) 163 var r2: i64 = 0 164 if rc4 == AG_RC_REFUSE { if tr_contains(out, cl[0], "REFUSED drift log unreadable" as *u8) == 1 { r2 = 1 } } 165 gv_check("neg-control-an-unreadable-log-REFUSES-rather-than-acquitting" as *u8, r2, ctr) 166 167 // ---- idempotence ---- 168 let rc5: i64 = ag_run(subj, "adoptdelta" as *u8, flog, prodreg, dash, out, cl) 169 var idem: i64 = 0 170 if rc5 == 0 { if tr_contains(out, cl[0], "ADOPTDELTA production_rows=3 d_distinct=2 d_stale=-1 sum_ok=1" as *u8) == 1 { idem = 1 } } 171 gv_check("idempotent-a-second-run-on-the-same-fixture-grades-identically" as *u8, idem, ctr) 172 173 let v: i64 = gv_verdict("ADOPTDELTA-GATE" as *u8, ctr, "the emitter separates production beats from fixture censuses, reconciles every partition and its delta, and abstains where the record cannot answer" as *u8) 174 sys_exit(v) 175 return v 176}