nx_boardcontra.nx source
↩ module page · 232 lines · 10660 B
1// nx_boardcontra.nx -- TWO BOARDS, ONE SYMBOL, OPPOSITE CLAIMS (2026-09-04)
2//
3// THE DEFECT, MEASURED. /compare/procgen logged nx_gi_path as "ABSENT: no source exists" at epoch
4// 1788371100. /compare/graphics logged the SAME organ BUILT, PROMOTED and REGISTERED at 1788377700 --
5// 6,600 seconds later, the same day. Nothing propagated the change back and the first board stood wrong
6// for two days. A seat reading only procgen would have rebuilt a capability that was already live.
7// EVERY EXISTING INSTRUMENT ON THIS SURFACE IS PER-BOARD. The emitter re-measures each watch cell, the
8// contract gate classifies each row, the refs gate checks each citation -- all of them WITHIN one board.
9// A contradiction that only exists BETWEEN two boards is invisible to every one of them, which is why it
10// survived: no instrument was wrong, the question was simply never asked.
11//
12// THE MECHANICAL FORM OF THAT QUESTION: one symbol is declared an OPEN CONTRACT (_ABSENT_:<sym>) on board
13// A while board B carries the SAME symbol as a PRESENT capability. Both cannot be true. This is deliberately
14// narrower than the prose case that motivated it -- it needs no natural language at all -- and it is the
15// half that can be decided from the DATA rather than from sentences.
16//
17// WHY NOT AN AXIS INSIDE nx_board_contract_gate: that organ is proven 12/12 and its two-pass table sizing
18// is tuned to CONTRACT rows only. This question needs every row of every board, present ones included, so
19// it is a different population, not a different predicate over the same one. Extending the incumbent would
20// have meant widening its tables and re-proving its partition; a separate organ leaves that proof intact.
21// CHECK-BEFORE-BUILD RUN AND ADJUDICATED: nx_spendgate's top hit was nx_atlas_contra at the maximum score,
22// READ RATHER THAN ACCEPTED -- it is a two-integer rigor comparator for the knowledge atlas and scores on
23// the word "contra" alone. Not a duplicate. That is the spendgate's own documented behaviour: the top hit
24// is frequently not the answer, which is why it publishes a list and refuses a verdict.
25//
26// PUBLISHES PAIRS, NEVER A WINNER. Which board is right is a judgement about the world; this organ only
27// proves the two disagree. Naming a winner would need a rigor model this has no grounds for.
28//
29// exit: 0 scanned (with or without hits) . 3 no board list readable license_tier: ORIGINAL No hw writes.
30import "nx_syscalls.nx"
31
32const BK_PATH: i64 = 1024
33const BK_CAP: i64 = 1048576
34const BK_LIST: i64 = 65536
35const BK_NL: i64 = 10
36const BK_BAR: i64 = 124
37const BK_HASH: i64 = 35
38const BK_AT: i64 = 64
39const BK_NAMECAP: i64 = 64
40const BK_SYMCAP: i64 = 256
41const BK_MARKLEN: i64 = 9
42
43func bk_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
44func bk_w(s: *u8) -> i64 { sys_write(1, s, bk_slen(s)); return 0 }
45func bk_cat(dst: *u8, off: i64, s: *u8) -> i64 { var o: i64 = off; var i: i64 = 0; while s[i] != (0 as u8) { dst[o] = s[i]; o = o + 1; i = i + 1 } dst[o] = 0 as u8; return o }
46func bk_num(v: i64) -> i64 {
47 let t: *u8 = sys_mmap(32)
48 var m: i64 = v
49 var k: i64 = 0
50 if m == 0 { t[0] = 48 as u8; k = 1 }
51 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
52 let o: *u8 = sys_mmap(34)
53 var j: i64 = 0
54 while j < k { o[j] = t[k - 1 - j]; j = j + 1 }
55 o[k] = 0 as u8
56 bk_w(o)
57 return 0
58}
59func bk_streq(a: *u8, b: *u8) -> i64 {
60 var i: i64 = 0
61 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 }
62 if b[i] != (0 as u8) { return 0 }
63 return 1
64}
65func bk_read(path: *u8, buf: *u8, cap: i64) -> i64 {
66 let fd: i64 = sys_openat_rd(path)
67 if fd < 0 { return 0 - 1 }
68 var off: i64 = 0
69 var r: i64 = 1
70 while r > 0 {
71 if off >= cap - 1 { r = 0 } else {
72 r = sys_read(fd, (buf as i64 + off) as *u8, cap - 1 - off)
73 if r > 0 { off = off + r }
74 }
75 }
76 sys_close(fd)
77 buf[off] = 0 as u8
78 return off
79}
80// TWO ROOTS, because this estate has two compare trees and which one a bare path names depends on the
81// CWD of the process, never on the literal. Probing both is the resolver's job, not the caller's.
82func bk_read_compare(dom: *u8, ext: *u8, buf: *u8, cap: i64) -> i64 {
83 let p: *u8 = sys_mmap(BK_PATH)
84 var o: i64 = bk_cat(p, 0, "buildroot/knowledge/compare/" as *u8); o = bk_cat(p, o, dom); o = bk_cat(p, o, ext)
85 var n: i64 = bk_read(p, buf, cap)
86 if n > 0 { return n }
87 o = bk_cat(p, 0, "knowledge/compare/" as *u8); o = bk_cat(p, o, dom); o = bk_cat(p, o, ext)
88 n = bk_read(p, buf, cap)
89 return n
90}
91func bk_field(buf: *u8, ls: i64, le: i64, idx: i64, out: *u8, cap: i64) -> i64 {
92 var f: i64 = 0
93 var i: i64 = ls
94 var start: i64 = ls
95 while i <= le {
96 var atend: i64 = 0
97 if i == le { atend = 1 }
98 if atend == 0 { if (buf[i] as i64) == BK_BAR { atend = 1 } }
99 if atend == 1 {
100 if f == idx {
101 var n: i64 = i - start
102 if n >= cap { n = cap - 1 }
103 var k: i64 = 0
104 while k < n { out[k] = buf[start + k]; k = k + 1 }
105 out[n] = 0 as u8
106 return n
107 }
108 f = f + 1
109 start = i + 1
110 }
111 i = i + 1
112 }
113 out[0] = 0 as u8
114 return 0 - 1
115}
116func bk_starts(s: *u8, p: *u8) -> i64 {
117 var i: i64 = 0
118 while p[i] != (0 as u8) { if s[i] != p[i] { return 0 } i = i + 1 }
119 return 1
120}
121
122// Walk one domain's matrix. mode 0 = COUNT contracts only. mode 1 = FILL the contract table.
123// mode 2 = CHECK every PRESENT symbol against the filled table.
124// The count/fill split exists so the table is sized by MEASUREMENT and never by a guessed ceiling.
125func bk_walk(dom: *u8, mode: i64, mbuf: *u8, t_sym: *i64, t_dom: *i64, nrec: *i64, hits: *i64) -> i64 {
126 let n: i64 = bk_read_compare(dom, ".matrix" as *u8, mbuf, BK_CAP)
127 if n <= 0 { return 0 }
128 let symf: *u8 = sys_mmap(BK_SYMCAP)
129 var ls: i64 = 0
130 while ls < n {
131 var le: i64 = ls
132 while le < n { if (mbuf[le] as i64) == BK_NL { break } le = le + 1 }
133 var skip: i64 = 0
134 if le <= ls { skip = 1 }
135 if skip == 0 { if (mbuf[ls] as i64) == BK_HASH { skip = 1 } }
136 if skip == 0 { if (mbuf[ls] as i64) == BK_AT { skip = 1 } }
137 if skip == 0 {
138 if bk_field(mbuf, ls, le, 2, symf, BK_SYMCAP) > 0 {
139 let isabs: i64 = bk_starts(symf, "_ABSENT_" as *u8)
140 if isabs == 1 {
141 // only a WATCH contract names a symbol; a bare _ABSENT_ names nothing and is skipped
142 if bk_starts(symf, "_ABSENT_:" as *u8) == 1 {
143 if mode == 0 { nrec[0] = nrec[0] + 1 }
144 if mode == 1 {
145 let k: i64 = nrec[0]
146 let sp: *u8 = sys_mmap(BK_SYMCAP)
147 bk_cat(sp, 0, (symf as i64 + BK_MARKLEN) as *u8)
148 let dp: *u8 = sys_mmap(BK_NAMECAP)
149 bk_cat(dp, 0, dom)
150 t_sym[k] = sp as i64
151 t_dom[k] = dp as i64
152 nrec[0] = k + 1
153 }
154 }
155 }
156 if isabs == 0 {
157 if mode == 2 {
158 var i: i64 = 0
159 while i < nrec[0] {
160 if bk_streq(t_sym[i] as *u8, symf) == 1 {
161 // SAME BOARD is not a contradiction: a board may legitimately carry an open
162 // contract and a shipped row for one symbol at different rungs.
163 if bk_streq(t_dom[i] as *u8, dom) == 0 {
164 hits[0] = hits[0] + 1
165 bk_w("CONTRADICTION symbol=" as *u8); bk_w(symf)
166 bk_w(" OPEN-on=" as *u8); bk_w(t_dom[i] as *u8)
167 bk_w(" PRESENT-on=" as *u8); bk_w(dom)
168 bk_w(" -- one board calls it an unbuilt contract while the other claims it shipped\n" as *u8)
169 }
170 }
171 i = i + 1
172 }
173 }
174 }
175 }
176 }
177 ls = le + 1
178 }
179 return 1
180}
181
182func bk_all(lst: *u8, ln: i64, mode: i64, mbuf: *u8, t_sym: *i64, t_dom: *i64, nrec: *i64, hits: *i64) -> i64 {
183 let dom: *u8 = sys_mmap(BK_NAMECAP)
184 var ds: i64 = 0
185 while ds < ln {
186 var de: i64 = ds
187 while de < ln { if (lst[de] as i64) == BK_NL { break } de = de + 1 }
188 var dl: i64 = de - ds
189 if dl > 0 {
190 if dl >= BK_NAMECAP { dl = BK_NAMECAP - 1 }
191 var i: i64 = 0
192 while i < dl { dom[i] = lst[ds + i]; i = i + 1 }
193 dom[dl] = 0 as u8
194 bk_walk(dom, mode, mbuf, t_sym, t_dom, nrec, hits)
195 }
196 ds = de + 1
197 }
198 return 1
199}
200
201func main(argc: i64, argv: *i64) -> i64 {
202 bk_w("NX-BOARDCONTRA: one symbol, two boards, opposite claims\n" as *u8)
203 let lst: *u8 = sys_mmap(BK_LIST)
204 var ln: i64 = bk_read_compare("regen" as *u8, ".list" as *u8, lst, BK_LIST)
205 if ln <= 0 {
206 bk_w(" NO-BOARD-LIST readable from this CWD -- nothing was examined, and that is reported as a\n" as *u8)
207 bk_w(" refusal rather than as zero contradictions. A census that read nothing must never read clean.\n" as *u8)
208 return 3
209 }
210 let mbuf: *u8 = sys_mmap(BK_CAP)
211 let nrec: *i64 = sys_mmap(16) as *i64
212 let hits: *i64 = sys_mmap(16) as *i64
213 nrec[0] = 0
214 hits[0] = 0
215 bk_all(lst, ln, 0, mbuf, 0 as *i64, 0 as *i64, nrec, hits)
216 var nalloc: i64 = nrec[0]
217 if nalloc < 1 { nalloc = 1 }
218 let t_sym: *i64 = sys_mmap(nalloc * 8) as *i64
219 let t_dom: *i64 = sys_mmap(nalloc * 8) as *i64
220 let ncontract: i64 = nrec[0]
221 nrec[0] = 0
222 bk_all(lst, ln, 1, mbuf, t_sym, t_dom, nrec, hits)
223 bk_all(lst, ln, 2, mbuf, t_sym, t_dom, nrec, hits)
224 bk_w(" open_contracts_indexed=" as *u8); bk_num(ncontract); bk_w("\n" as *u8)
225 bk_w(" contradictions=" as *u8); bk_num(hits[0]); bk_w("\n" as *u8)
226 if hits[0] == 0 {
227 bk_w(" none found. SCOPE: this compares SYMBOL FIELDS only. The defect that motivated it lived in\n" as *u8)
228 bk_w(" a plan LOG ROW, which no field carries, so a zero here does NOT mean the boards agree in\n" as *u8)
229 bk_w(" prose -- it means no symbol is claimed both open and shipped.\n" as *u8)
230 }
231 return 0
232}