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}