nx_win_ledger.nx source
↩ module page · 324 lines · 13630 B
1// nx_win_ledger.nx -- the WIN-LEDGER organ (ADDITIVE; no main, no shared edits).
2//
3// REASON TO EXIST (operator's mandate): a "win" is not a win until it is
4// EXPLAINED (why, cited), PROVEN (a repro gate with a known answer), and
5// FALSIFIABLE (an explicit assumptions[] list, so a bad assumption is
6// catchable). This organ is the bookkeeping layer for those wins, recorded
7// ADDITIVELY over the hash-chained nx_journal_log (which itself stores its
8// payloads content-addressed in nx_blob_store -- the snapshot/attest
9// substrate). A re-verify RE-RUNS a recorded win's repro and asserts the
10// expected known answer -> HOLDS; a regression / broken assumption / a
11// deliberately-wrong expected FAILS LOUD -> REFUTED. The status downgrade is
12// the whole point: the ledger must be able to flip a stale win to REFUTED.
13//
14// SOVEREIGNTY: the re-gate path mirrors nx_gate_runner exactly -- compile the
15// repro *_test.nx via the PINNED nx_cc_known_good.elf (NEVER the active,
16// possibly-poisoned compiler; cf. the g1 regalloc miscompile history), then
17// as + ld, then run capturing stdout, and substring-match the expected
18// known-answer. We capture STDOUT (not just the exit code) so the ledger
19// catches a regression where the gate still exits 0 but emits a DIFFERENT
20// answer -- and so a deliberately-wrong expected string genuinely flips to
21// REFUTED.
22//
23// ADDITIVE: this is a NEW file. It does NOT edit nx_warden_lib / nx_gate_runner
24// / nx_conductor / nx_eqsat. It REUSES, concept-not-copy:
25// * nx_blob_store.nx -- content-addressed snapshot substrate (under journal)
26// * nx_journal_log.nx -- hash-chained append-only win record store
27// * nx_syscalls.nx -- raw fork/exec/wait + file I/O (NOT copied; imported)
28// license_tier: ORIGINAL
29
30import "nx_syscalls.nx"
31import "nx_blob_store.nx"
32import "nx_journal_log.nx"
33
34// ===== Constants =================================================
35
36// Build oracles -- the EXACT pinned known-good re-gate path (mirrors
37// nx_gate_runner GR_CC/GR_AS/GR_LD; the pinned compiler is the single most
38// important correctness decision given the active-compiler miscompile history).
39const WL_CC: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/_offc/nx_cc_known_good.elf"
40const WL_AS: *u8 = "/usr/bin/as"
41const WL_LD: *u8 = "/usr/bin/ld"
42
43// Scratch paths carry a unique tag to avoid concurrent-tick collision with
44// nx_gate_runner's fixed /tmp/nx_gr.* paths (the design's open follow-up).
45const WL_S: *u8 = "/tmp/nx_winl.s"
46const WL_O: *u8 = "/tmp/nx_winl.o"
47const WL_ELF: *u8 = "/tmp/nx_winl.elf"
48const WL_OUT: *u8 = "/tmp/nx_winl.out"
49const WL_MODE: i64 = 420
50
51// Status enum for a win record.
52const WL_STATUS_UNVERIFIED: i64 = 0
53const WL_STATUS_HOLDS: i64 = 1
54const WL_STATUS_REFUTED: i64 = 2
55const WL_STATUS_SUPERSEDED: i64 = 3
56
57// Build-stage failures from the re-gate (distinct from a gate that ran and
58// produced the wrong answer -- the design demands we distinguish 'gate ran and
59// FAILED' from 'gate failed to BUILD').
60const WL_BUILD_CC_FAIL: i64 = 0 - 1
61const WL_BUILD_AS_FAIL: i64 = 0 - 2
62const WL_BUILD_LD_FAIL: i64 = 0 - 3
63
64// Journal schema ids for the additive win records.
65const WL_SCHEMA_RECORD: i64 = 9001 // a win was recorded
66const WL_SCHEMA_HOLDS: i64 = 9002 // re-verify confirmed HOLDS
67const WL_SCHEMA_REFUTED: i64 = 9003 // re-verify FAILED LOUD -> REFUTED
68
69// Capacity for the assumptions[] list on one record.
70const WL_MAX_ASSUMPTIONS: i64 = 16
71
72// Canaries (distinct from blob_store / journal_log canaries).
73const WL_CANARY_PRE: i64 = 0x4E5857494E4C5052 // "NXWINLPR"
74const WL_CANARY_POST: i64 = 0x4E5857494E4C4550 // "NXWINLEP"
75
76// ===== Win record ===============================================
77// The operator's win-record schema. Strings are *u8 (NishiLang string
78// literals). assumptions[] is an array of *u8 + a count -- every assumption
79// is EXPLICIT and FALSIFIABLE so a bad one is catchable.
80
81struct NxWinRecord {
82 canary_pre: i64,
83 claim: *u8, // what we claim we did
84 exceed_axis: *u8, // the dimension on which we exceed (or "meet")
85 why: *u8, // explanation + cited source_id / url
86 repro_gate: *u8, // absolute path to a *_test.nx repro gate
87 expected: *u8, // expected KNOWN ANSWER (substring of gate stdout)
88 n_assumptions: i64,
89 assumptions: *i64, // *i64 array of *u8 (each a falsifiable assumption)
90 status: i64, // WL_STATUS_*
91 canary_post: i64,
92}
93
94// ===== Win ledger (additive over the journal) ====================
95struct NxWinLedger {
96 canary_pre: i64,
97 store: *NxBlobStore,
98 log: *NxJournalLog,
99 canary_post: i64,
100}
101
102// ===== Small helpers ============================================
103
104func _wl_strlen(s: *u8) -> i64 {
105 if (s as i64) == 0 { return 0 }
106 var n: i64 = 0
107 while s[n] != 0 as u8 { n = n + 1 }
108 return n
109}
110
111// substring scan: does haystack contain needle? 1/0. (Reuses the same shape
112// as nx_warden_lib's w_contains -- concept, not a shared edit.)
113func _wl_contains(hay: *u8, needle: *u8) -> i64 {
114 let hn: i64 = _wl_strlen(hay)
115 let nn: i64 = _wl_strlen(needle)
116 if nn == 0 { return 1 }
117 if nn > hn { return 0 }
118 var i: i64 = 0
119 while i <= hn - nn {
120 var j: i64 = 0
121 var matched: i64 = 1
122 while j < nn {
123 if hay[i + j] != needle[j] { matched = 0; j = nn } else { j = j + 1 }
124 }
125 if matched == 1 { return 1 }
126 i = i + 1
127 }
128 return 0
129}
130
131// ===== Construction =============================================
132
133// A record starts UNVERIFIED with an empty assumptions list.
134func nx_win_record_new(
135 claim: *u8, exceed_axis: *u8, why: *u8,
136 repro_gate: *u8, expected: *u8
137) -> *NxWinRecord {
138 let r: *NxWinRecord = (sys_mmap(96)) as *NxWinRecord
139 r.canary_pre = WL_CANARY_PRE
140 r.canary_post = WL_CANARY_POST
141 r.claim = claim
142 r.exceed_axis = exceed_axis
143 r.why = why
144 r.repro_gate = repro_gate
145 r.expected = expected
146 r.n_assumptions = 0
147 r.assumptions = (sys_mmap(WL_MAX_ASSUMPTIONS * 8)) as *i64
148 var i: i64 = 0
149 while i < WL_MAX_ASSUMPTIONS { r.assumptions[i] = 0; i = i + 1 }
150 r.status = WL_STATUS_UNVERIFIED
151 return r
152}
153
154func nx_win_record_is_valid(r: *NxWinRecord) -> i64 {
155 if (r as i64) == 0 { return 0 }
156 if r.canary_pre != WL_CANARY_PRE { return 0 }
157 if r.canary_post != WL_CANARY_POST { return 0 }
158 if (r.repro_gate as i64) == 0 { return 0 }
159 if (r.expected as i64) == 0 { return 0 }
160 if r.n_assumptions < 0 { return 0 }
161 if r.n_assumptions > WL_MAX_ASSUMPTIONS { return 0 }
162 return 1
163}
164
165// Add an EXPLICIT, FALSIFIABLE assumption to the record. Returns the new
166// count, or -1 if the record is invalid / full.
167func nx_win_record_add_assumption(r: *NxWinRecord, assumption: *u8) -> i64 {
168 if nx_win_record_is_valid(r) != 1 { return -1 }
169 if (assumption as i64) == 0 { return -1 }
170 if r.n_assumptions >= WL_MAX_ASSUMPTIONS { return -1 }
171 r.assumptions[r.n_assumptions] = assumption as i64
172 r.n_assumptions = r.n_assumptions + 1
173 return r.n_assumptions
174}
175
176func nx_win_record_assumption(r: *NxWinRecord, idx: i64) -> *u8 {
177 if nx_win_record_is_valid(r) != 1 { return 0 as *u8 }
178 if idx < 0 { return 0 as *u8 }
179 if idx >= r.n_assumptions { return 0 as *u8 }
180 return (r.assumptions[idx]) as *u8
181}
182
183// ===== Ledger construction (additive over journal/blob) =========
184func nx_win_ledger_new() -> *NxWinLedger {
185 let L: *NxWinLedger = (sys_mmap(48)) as *NxWinLedger
186 L.canary_pre = WL_CANARY_PRE
187 L.canary_post = WL_CANARY_POST
188 L.store = nx_blob_store_new()
189 L.log = nx_journal_log_new(L.store)
190 return L
191}
192
193func nx_win_ledger_is_valid(L: *NxWinLedger) -> i64 {
194 if (L as i64) == 0 { return 0 }
195 if L.canary_pre != WL_CANARY_PRE { return 0 }
196 if L.canary_post != WL_CANARY_POST { return 0 }
197 if nx_blob_store_is_valid(L.store) != 1 { return 0 }
198 if nx_journal_log_is_valid(L.log) != 1 { return 0 }
199 return 1
200}
201
202func nx_win_ledger_count(L: *NxWinLedger) -> i64 {
203 if nx_win_ledger_is_valid(L) != 1 { return -1 }
204 return nx_journal_log_count(L.log)
205}
206
207// ===== Record a win (ADDITIVE append over the hash-chained journal) =====
208// Stores the claim bytes as the journal payload (content-addressed in the
209// blob store), schema-tagged WL_SCHEMA_RECORD. Returns the new seq_no, or a
210// negative journal verdict. The journal entry is the falsifiable trail: it
211// exists BEFORE any re-verify runs.
212func nx_win_ledger_record(L: *NxWinLedger, r: *NxWinRecord) -> i64 {
213 if nx_win_ledger_is_valid(L) != 1 { return 0 - NX_JOURNAL_TAMPER }
214 if nx_win_record_is_valid(r) != 1 { return 0 - NX_JOURNAL_BAD_INPUT }
215 let claim: *u8 = r.claim
216 let clen: i64 = _wl_strlen(claim)
217 return nx_journal_log_append(L.log, claim, clen, WL_SCHEMA_RECORD)
218}
219
220// ===== Re-gate: compile (pinned) + as + ld + run, capture stdout =====
221
222// fork+exec `path` with argv/envp; child stdout -> out_path if non-null else
223// /dev/null, stderr -> /dev/null. Blocking wait; returns child exit code.
224// (Same shape as nx_gate_runner.gr_run -- concept reused, no shared edit.)
225func _wl_run(path: *u8, argv: *i64, envp: *i64, out_path: *u8) -> i64 {
226 let pid: i64 = sys_fork()
227 if pid == 0 {
228 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0)
229 if (out_path as i64) != 0 {
230 let ofd: i64 = sys_openat_wr(out_path, WL_MODE)
231 if ofd >= 0 { sys_dup3(ofd, 1, 0) }
232 }
233 if (out_path as i64) == 0 { if dn >= 0 { sys_dup3(dn, 1, 0) } }
234 if dn >= 0 { sys_dup3(dn, 2, 0) }
235 sys_execve(path, argv, envp)
236 sys_exit(127)
237 }
238 let st: *i64 = sys_mmap(16) as *i64
239 sys_wait4(pid, st, 0)
240 return wait_exit_code(st[0])
241}
242
243// Compile + assemble + link the repro gate (PINNED known-good compiler), run
244// it capturing stdout into WL_OUT. Returns the gate's exit code (>=0 = it ran;
245// 0 = the gate self-asserted PASS), or a negative WL_BUILD_*_FAIL stage code
246// if a BUILD oracle failed (so callers distinguish 'ran+failed' from
247// 'failed to build').
248func nx_win_regate(testnx: *u8) -> i64 {
249 let envp: *i64 = sys_mmap(8) as *i64; envp[0] = 0
250 // 1. compile: cc testnx > WL_S (PINNED -- never the active compiler)
251 let a1: *i64 = sys_mmap(32) as *i64
252 a1[0] = WL_CC as i64; a1[1] = testnx as i64; a1[2] = 0
253 if _wl_run(WL_CC, a1, envp, WL_S) != 0 { return WL_BUILD_CC_FAIL }
254 // 2. assemble: as WL_S -o WL_O
255 let a2: *i64 = sys_mmap(40) as *i64
256 a2[0] = WL_AS as i64; a2[1] = WL_S as i64; a2[2] = ("-o" as *u8) as i64; a2[3] = WL_O as i64; a2[4] = 0
257 if _wl_run(WL_AS, a2, envp, 0 as *u8) != 0 { return WL_BUILD_AS_FAIL }
258 // 3. link: ld -o WL_ELF WL_O
259 let a3: *i64 = sys_mmap(40) as *i64
260 a3[0] = WL_LD as i64; a3[1] = ("-o" as *u8) as i64; a3[2] = WL_ELF as i64; a3[3] = WL_O as i64; a3[4] = 0
261 if _wl_run(WL_LD, a3, envp, 0 as *u8) != 0 { return WL_BUILD_LD_FAIL }
262 // 4. run the gate, capturing stdout into WL_OUT; exit code is the verdict.
263 let a4: *i64 = sys_mmap(16) as *i64
264 a4[0] = WL_ELF as i64; a4[1] = 0
265 return _wl_run(WL_ELF, a4, envp, WL_OUT)
266}
267
268// ===== Re-verify: re-run the repro, assert expected -> HOLDS / REFUTED =====
269// Re-runs the recorded win's repro gate, reads the captured stdout, and asserts
270// the expected KNOWN ANSWER appears in it. On match -> HOLDS. On any failure
271// (build oracle failed, gate exited non-zero, OR stdout lacks the expected
272// answer) -> REFUTED (FAIL LOUD). The record's status field is MUTATED to the
273// verdict (the additive history is journaled separately by record_and_verify).
274// Returns the new status (WL_STATUS_HOLDS / WL_STATUS_REFUTED), or -1 on bad
275// input.
276func nx_win_reverify(r: *NxWinRecord) -> i64 {
277 if nx_win_record_is_valid(r) != 1 { return -1 }
278
279 let rc: i64 = nx_win_regate(r.repro_gate)
280 // A build oracle failed (negative) OR the gate ran but exited non-zero:
281 // either way the repro did not reproduce -> REFUTED.
282 if rc != 0 {
283 r.status = WL_STATUS_REFUTED
284 return WL_STATUS_REFUTED
285 }
286
287 // The gate ran and self-asserted PASS. Now the LEDGER's own assertion:
288 // does the captured stdout actually contain the expected known answer?
289 // This is what catches a deliberately-wrong expected (and a silent
290 // answer-regression that still exits 0).
291 let out_len: *i64 = sys_mmap(8) as *i64
292 let out_bytes: *u8 = sys_read_file(WL_OUT, out_len)
293 if (out_bytes as i64) == 0 {
294 r.status = WL_STATUS_REFUTED
295 return WL_STATUS_REFUTED
296 }
297 if _wl_contains(out_bytes, r.expected) != 1 {
298 r.status = WL_STATUS_REFUTED
299 return WL_STATUS_REFUTED
300 }
301
302 r.status = WL_STATUS_HOLDS
303 return WL_STATUS_HOLDS
304}
305
306// ===== Record + re-verify in one shot (the load-bearing entry point) =====
307// Records the win additively, re-verifies it, and journals the verdict
308// (HOLDS / REFUTED) as a SECOND additive entry -- so the hash-chained history
309// carries both 'a win was claimed' and 'how it re-verified'. Returns the
310// re-verify status.
311func nx_win_ledger_record_and_verify(L: *NxWinLedger, r: *NxWinRecord) -> i64 {
312 if nx_win_ledger_is_valid(L) != 1 { return -1 }
313 if nx_win_record_is_valid(r) != 1 { return -1 }
314 nx_win_ledger_record(L, r)
315 let status: i64 = nx_win_reverify(r)
316 let claim: *u8 = r.claim
317 let clen: i64 = _wl_strlen(claim)
318 if status == WL_STATUS_HOLDS {
319 nx_journal_log_append(L.log, claim, clen, WL_SCHEMA_HOLDS)
320 } else {
321 nx_journal_log_append(L.log, claim, clen, WL_SCHEMA_REFUTED)
322 }
323 return status
324}