code wiki / (root) / nx_accept_gate.nx

nx_accept_gate.nx source

↩ module page · 388 lines · 29117 B

1// nx_accept_gate.nx -- THE GATE FOR THE THREE-PARTY ACCEPTANCE LEDGER (2026-08-31). 2// 3// Two subjects, one gate: IN-PROCESS over nx_accept_lib + nx_accept_ref_lib (the classifier, its named negatives, 4// the deterministic emitter, the shape ruler) and END-TO-END over the built nx_accept binary (its verbs, its 5// composition of the incumbent writer, its refusals). Everything runs on fixture planes seeded under 6// /tmp/nx_accept_gate/r<usec>/ -- a fresh directory per run, so nothing measured here was inherited from an 7// earlier run and the production planes are never read or written. 8// argv[1] = the subject elf (nx_gate_bite subject mode passes the freshly built one); default 9// buildroot/_build/nx_accept.sov.elf -- the artifact the ship loop just built -- then ./nx_accept.elf. An 10// absent subject SKIPS the end-to-end teeth (a precondition, never a RED); the in-process teeth still run. 11// It also IMPORTS buildroot/runtime/nx_accept_decl.nx, the file `nx_accept emit` regenerates, so every build of 12// this gate is a compile proof of the live emitted declarations. SCOPE, stated: as of THIS gate's build time; 13// the emitted fixture buffer is proven by the shape ruler on every run. 14// license_tier: ORIGINAL No hw writes (Rule 26). 15import "nx_syscalls.nx" 16import "nx_gate_verdict.nx" 17import "nx_tool_run.nx" 18import "nx_store_seed_lib.nx" 19import "nx_accept_lib.nx" 20import "nx_accept_ref_lib.nx" 21import "nx_accept_decl.nx" 22 23const ACG_DIR: *u8 = "/tmp/nx_accept_gate" 24const ACG_RUNPFX: *u8 = "/tmp/nx_accept_gate/r" 25const ACG_SUBJECT_A: *u8 = "buildroot/_build/nx_accept.sov.elf" 26const ACG_SUBJECT_B: *u8 = "nx_accept.elf" 27const ACG_WRITER: *u8 = "nx_store_put.elf" 28const ACG_MODE_DIR: i64 = 493 29const ACG_MODE_FILE: i64 = 420 30const ACG_FLOOR: i64 = 151 // the panel's admitted textured floor (cjc_panel.conf, 2026-08-27) -- the fixture bar 31const ACG_MARGIN: i64 = 49 // fixture percepts sit this far above and below the bar; neither can pass by an off-by-one 32const ACG_TAB: i64 = 9 33const ACG_CAP: i64 = 65536 34const ACG_PATH: i64 = 512 35const ACG_ARGV: i64 = 16 36const ACG_LP: i64 = 16 37const ACG_TMO_MS: i64 = 130000 // the organ's own writer ceiling (nx_seg_store lock ceiling 120 s + margin) 38const ACG_DATE: *u8 = "2026-08-30" 39const ACG_DATE_EARLIER: *u8 = "2026-08-29" 40const ACG_OP: *u8 = "operator" 41const ACG_NONOP: *u8 = "seat-x" 42const ACG_SEAT: *u8 = "seat-fixture" 43const ACG_TIER: *u8 = "textured" 44const ACG_TIER_BAD: *u8 = "photoreal" 45const ACG_WORDS: *u8 = "fixture words" 46const ACG_STAMP: *u8 = "fixturestamp" 47const ACG_FRAME: *u8 = "fixtureframe" 48const ACG_ART_BODY: *u8 = "fixture artifact bytes\n" 49const ACG_EXPECT_SUBJECTS: i64 = 11 50const ACG_EXPECT_AGREED: i64 = 2 51const ACG_EXPECT_ACC_ROWS: i64 = 12 52const ACG_EXPECT_REF_ROWS: i64 = 8 53const ACG_EXPECT_ATT_ROWS: i64 = 8 54const ACG_EXPECT_UNMAPPED: i64 = 1 55const ACG_EXPECT_PLANES: i64 = 3 56const ACG_EXPECT_BOARD_ROWS: i64 = 2 57const ACG_EXPECT_DECLS_AFTER_ATTEST: i64 = 3 58 59func acg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 60func acg_tab(b: *u8, o: i64) -> i64 { b[o] = ACG_TAB as u8; return o + 1 } 61func acg_nl(b: *u8, o: i64) -> i64 { b[o] = AL_NL as u8; return o + 1 } 62func acg_num(v: i64) -> *u8 { let t: *u8 = sys_mmap(AL_NUMCAP); let n: i64 = al_catn(t, 0, v); t[n] = 0 as u8; return t } 63func acg_path(dir: *u8, leaf: *u8) -> *u8 { let p: *u8 = sys_mmap(ACG_PATH); var o: i64 = al_cat(p, 0, dir); p[o] = AL_SLASH as u8; o = o + 1; o = al_cat(p, o, leaf); p[o] = 0 as u8; return p } 64func acg_write(path: *u8, content: *u8) -> i64 { 65 let fd: i64 = sys_openat_wr(path, ACG_MODE_FILE) 66 if fd < 0 { return 0 - 1 } 67 let n: i64 = al_slen(content) 68 var off: i64 = 0 69 while off < n { 70 let r: i64 = sys_write(fd, ((content as i64) + off) as *u8, n - off) 71 if r <= 0 { sys_close(fd); return 0 - 2 } 72 off = off + r 73 } 74 sys_close(fd) 75 return n 76} 77// first offset of needle in b[0..n), -1 when absent 78func acg_find(b: *u8, n: i64, needle: *u8) -> i64 { 79 let nl: i64 = al_slen(needle) 80 if nl == 0 { return 0 - 1 } 81 var i: i64 = 0 82 while i + nl <= n { 83 var m: i64 = 1 84 var j: i64 = 0 85 while j < nl { if b[i + j] != needle[j] { m = 0; j = nl } else { j = j + 1 } } 86 if m == 1 { return i } 87 i = i + 1 88 } 89 return 0 - 1 90} 91func acg_has(b: *u8, n: i64, needle: *u8) -> i64 { if acg_find(b, n, needle) >= 0 { return 1 } return 0 } 92// 7-field row: the accept plane (id subject verdict date actor words targets) and the attest plane 93func acg_row7(b: *u8, o0: i64, f0: *u8, f1: *u8, f2: *u8, f3: *u8, f4: *u8, f5: *u8, f6: *u8) -> i64 { 94 var o: i64 = al_cat(b, o0, f0); o = acg_tab(b, o) 95 o = al_cat(b, o, f1); o = acg_tab(b, o) 96 o = al_cat(b, o, f2); o = acg_tab(b, o) 97 o = al_cat(b, o, f3); o = acg_tab(b, o) 98 o = al_cat(b, o, f4); o = acg_tab(b, o) 99 o = al_cat(b, o, f5); o = acg_tab(b, o) 100 o = al_cat(b, o, f6) 101 return acg_nl(b, o) 102} 103// 8-field referee row: id subject sha composite percept tier date seat 104func acg_row8(b: *u8, o0: i64, f0: *u8, f1: *u8, f2: *u8, f3: *u8, f4: *u8, f5: *u8, f6: *u8, f7: *u8) -> i64 { 105 var o: i64 = al_cat(b, o0, f0); o = acg_tab(b, o) 106 o = al_cat(b, o, f1); o = acg_tab(b, o) 107 o = al_cat(b, o, f2); o = acg_tab(b, o) 108 o = al_cat(b, o, f3); o = acg_tab(b, o) 109 o = al_cat(b, o, f4); o = acg_tab(b, o) 110 o = al_cat(b, o, f5); o = acg_tab(b, o) 111 o = al_cat(b, o, f6); o = acg_tab(b, o) 112 o = al_cat(b, o, f7) 113 return acg_nl(b, o) 114} 115// the book, built exactly the way the organ builds it 116func acg_book(acc: *u8, ref: *u8, att: *u8, conf: *u8, boards: *u8, cfout: *i64, planes_out: *i64, doms: *u8, orgs: *u8) -> *i64 { 117 let bk: *i64 = al_bk_new() 118 planes_out[0] = al_load(bk, acc, ref, att) 119 let cf: *i64 = al_conf_load(conf) 120 cfout[0] = cf as i64 121 let over: *i64 = sys_mmap(ACG_LP) as *i64 122 over[0] = 0 123 planes_out[1] = acr_boards(bk, boards, doms, orgs, over) 124 return bk 125} 126func acg_party_of(bk: *i64, cf: *i64, name: *u8, why: *i64) -> i64 { 127 let si: i64 = al_bk_find_z(bk, name) 128 if si < 0 { return 0 - 1 } 129 return acr_party(bk, cf, si, why) 130} 131// run the subject: argv = [subject, verb, a1..a5, root=<dir>]; captured into out/ol; returns rc 132func acg_run(subject: *u8, rootarg: *u8, verb: *u8, a1: *u8, a2: *u8, a3: *u8, a4: *u8, out: *u8, ol: *i64) -> i64 { 133 let av: *i64 = sys_mmap(8 * ACG_ARGV) as *i64 134 var n: i64 = 0 135 av[n] = subject as i64; n = n + 1 136 av[n] = verb as i64; n = n + 1 137 if (a1 as i64) != 0 { av[n] = a1 as i64; n = n + 1 } 138 if (a2 as i64) != 0 { av[n] = a2 as i64; n = n + 1 } 139 if (a3 as i64) != 0 { av[n] = a3 as i64; n = n + 1 } 140 if (a4 as i64) != 0 { av[n] = a4 as i64; n = n + 1 } 141 av[n] = rootarg as i64; n = n + 1 142 av[n] = 0 143 let tr: *i64 = sys_mmap(ACG_LP) as *i64 144 ol[0] = 0 145 let rc: i64 = tr_run_capture_tr(subject, av, out, ACG_CAP, ol, ACG_TMO_MS, tr) 146 var term: i64 = ol[0] 147 if term < 0 { term = 0 } 148 if term >= ACG_CAP { term = ACG_CAP - 1 } 149 out[term] = 0 as u8 150 return rc 151} 152func acg_nil() -> *u8 { return 0 as *u8 } 153 154func main(argc: i64, argv: *i64) -> i64 { 155 let ctr: *i64 = gv_ctr() 156 gv_head("nx_accept_gate -- three-party agreement derived from the planes, every negative named, emit deterministic, the writer composed and refused where it must be" as *u8) 157 158 // ---------------- SETUP: a fresh run directory, three fixture planes, the panel conf + receipt, a board ---------- 159 sys_mkdir(ACG_DIR, ACG_MODE_DIR) 160 let rundir: *u8 = sys_mmap(ACG_PATH) 161 var ro: i64 = al_cat(rundir, 0, ACG_RUNPFX) 162 ro = al_catn(rundir, ro, sys_now_us()) 163 rundir[ro] = 0 as u8 164 sys_mkdir(rundir, ACG_MODE_DIR) 165 let boards: *u8 = acg_path(rundir, "compare" as *u8) 166 sys_mkdir(boards, ACG_MODE_DIR) 167 let acc: *u8 = acg_path(rundir, "accept-" as *u8) 168 let refp: *u8 = acg_path(rundir, "referee-" as *u8) 169 let att: *u8 = acg_path(rundir, "attest-" as *u8) 170 let conf: *u8 = acg_path(rundir, "cjc_panel.conf" as *u8) 171 let rcpt: *u8 = acg_path(rundir, "receipt.txt" as *u8) 172 let decl: *u8 = acg_path(rundir, "nx_accept_decl.nx" as *u8) 173 let board: *u8 = acg_path(boards, "fixture.matrix" as *u8) 174 let art: *u8 = acg_path(rundir, "artifact.bin" as *u8) 175 let absent: *u8 = acg_path(rundir, "absent.png" as *u8) 176 let rootarg: *u8 = sys_mmap(ACG_PATH) 177 var ra: i64 = al_cat(rootarg, 0, "root=" as *u8) 178 ra = al_cat(rootarg, ra, rundir) 179 rootarg[ra] = 0 as u8 180 gv_puts(" rundir: " as *u8); gv_puts(rundir); gv_puts("\n" as *u8) 181 182 let above: *u8 = acg_num(ACG_FLOOR + ACG_MARGIN) 183 let below: *u8 = acg_num(ACG_FLOOR - ACG_MARGIN) 184 let b: *u8 = sys_mmap(ACG_CAP) 185 // accept plane: 12 rows 186 var o: i64 = 0 187 o = acg_row7(b, o, "op-all" as *u8, "fixture all three" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "gameengine:ga_accept_s_all" as *u8) 188 o = acg_row7(b, o, "op-rev1" as *u8, "fixture revoked" as *u8, "ACCEPT" as *u8, ACG_DATE_EARLIER, ACG_OP, ACG_WORDS, "ga_accept_s_revoked" as *u8) 189 o = acg_row7(b, o, "op-rev2" as *u8, "fixture revoked" as *u8, "REJECT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_revoked" as *u8) 190 o = acg_row7(b, o, "op-re1" as *u8, "fixture reaccepted" as *u8, "REJECT" as *u8, ACG_DATE_EARLIER, ACG_OP, ACG_WORDS, "ga_accept_s_reaccept" as *u8) 191 o = acg_row7(b, o, "op-re2" as *u8, "fixture reaccepted" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_reaccept" as *u8) 192 o = acg_row7(b, o, "op-low" as *u8, "fixture low percept" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_low" as *u8) 193 o = acg_row7(b, o, "op-noref" as *u8, "fixture no referee" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_noref" as *u8) 194 o = acg_row7(b, o, "op-noseat" as *u8, "fixture no seat" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_noseat" as *u8) 195 o = acg_row7(b, o, "seat-nonop" as *u8, "fixture non-operator" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_NONOP, ACG_WORDS, "ga_accept_s_nonop" as *u8) 196 o = acg_row7(b, o, "op-badtier" as *u8, "fixture unadmitted tier" as *u8, "ACCEPT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_badtier" as *u8) 197 o = acg_row7(b, o, "op-rej" as *u8, "fixture rejected" as *u8, "REJECT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "ga_accept_s_rejected" as *u8) 198 o = acg_row7(b, o, "op-unmapped" as *u8, "fixture unmapped" as *u8, "REJECT" as *u8, ACG_DATE, ACG_OP, ACG_WORDS, "gameengine:gpe_garment_draw" as *u8) 199 let accn: i64 = sts_seed(acc, b, o) 200 // referee plane: 8 rows 201 o = 0 202 o = acg_row8(b, o, "ref-all" as *u8, "s_all" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER, ACG_DATE, ACG_SEAT) 203 o = acg_row8(b, o, "ref-rev" as *u8, "s_revoked" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER, ACG_DATE, ACG_SEAT) 204 o = acg_row8(b, o, "ref-re" as *u8, "s_reaccept" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER, ACG_DATE, ACG_SEAT) 205 o = acg_row8(b, o, "ref-low" as *u8, "s_low" as *u8, ACG_FRAME, "GOOD" as *u8, below, ACG_TIER, ACG_DATE, ACG_SEAT) 206 o = acg_row8(b, o, "ref-noseat" as *u8, "s_noseat" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER, ACG_DATE, ACG_SEAT) 207 o = acg_row8(b, o, "ref-nonop" as *u8, "s_nonop" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER, ACG_DATE, ACG_SEAT) 208 o = acg_row8(b, o, "ref-badtier" as *u8, "s_badtier" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER_BAD, ACG_DATE, ACG_SEAT) 209 o = acg_row8(b, o, "ref-rej" as *u8, "s_rejected" as *u8, ACG_FRAME, "GOOD" as *u8, above, ACG_TIER, ACG_DATE, ACG_SEAT) 210 let refn: i64 = sts_seed(refp, b, o) 211 // attest plane: 8 rows (id subject seat stamp words date artifact) 212 o = 0 213 o = acg_row7(b, o, "att-all" as *u8, "s_all" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 214 o = acg_row7(b, o, "att-rev" as *u8, "s_revoked" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 215 o = acg_row7(b, o, "att-re" as *u8, "s_reaccept" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 216 o = acg_row7(b, o, "att-low" as *u8, "s_low" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 217 o = acg_row7(b, o, "att-noref" as *u8, "s_noref" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 218 o = acg_row7(b, o, "att-nonop" as *u8, "s_nonop" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 219 o = acg_row7(b, o, "att-badtier" as *u8, "s_badtier" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 220 o = acg_row7(b, o, "att-rej" as *u8, "s_rejected" as *u8, ACG_SEAT, ACG_STAMP, ACG_WORDS, ACG_DATE, art) 221 let attn: i64 = sts_seed(att, b, o) 222 // conf + receipt (the ONLY source of the floor), a board with one right and one wrong organ file, an artifact 223 o = al_cat(b, 0, "floor_percept_" as *u8); o = al_cat(b, o, ACG_TIER); o = al_cat(b, o, "=" as *u8); o = al_catn(b, o, ACG_FLOOR) 224 o = al_cat(b, o, "\nreceipt=" as *u8); o = al_cat(b, o, rcpt); o = acg_nl(b, o); b[o] = 0 as u8 225 let wconf: i64 = acg_write(conf, b) 226 let wrcpt: i64 = acg_write(rcpt, "admitted=1\ntiers=clay,textured,photoreal\ntiers_admitted=textured\n" as *u8) 227 o = al_cat(b, 0, "@cols a|b\nACCEPTANCE: fixture right file|" as *u8); o = al_cat(b, o, AL_DECL_ROW); o = al_cat(b, o, "|_ABSENT_:ga_accept_s_board|0|1|1|note\n" as *u8) 228 o = al_cat(b, o, "ACCEPTANCE: fixture wrong file|runtime/nx_accept_gate.nx|_ABSENT_:ga_accept_s_wrongorgan|0|1|1|note\n" as *u8); b[o] = 0 as u8 229 let wboard: i64 = acg_write(board, b) 230 let wart: i64 = acg_write(art, ACG_ART_BODY) 231 gv_puts(" seeded: accept=" as *u8); gv_num(accn); gv_puts(" referee=" as *u8); gv_num(refn); gv_puts(" attest=" as *u8); gv_num(attn) 232 gv_puts(" conf=" as *u8); gv_num(wconf); gv_puts("B receipt=" as *u8); gv_num(wrcpt); gv_puts("B board=" as *u8); gv_num(wboard); gv_puts("B artifact=" as *u8); gv_num(wart); gv_puts("B\n" as *u8) 233 var setup: i64 = 0 234 if accn == ACG_EXPECT_ACC_ROWS { if refn == ACG_EXPECT_REF_ROWS { if attn == ACG_EXPECT_ATT_ROWS { if wconf > 0 { if wrcpt > 0 { if wboard > 0 { if wart > 0 { setup = 1 } } } } } } } 235 gv_need("the /tmp fixture planes, conf, receipt, board and artifact could be written" as *u8, setup, ctr) 236 237 // ---------------- IN-PROCESS: the book ----------------------------------------------------------------------- 238 let cfp: *i64 = sys_mmap(ACG_LP) as *i64 239 let pl: *i64 = sys_mmap(ACG_LP) as *i64 240 let doms: *u8 = sys_mmap(AL_NAMEW * AL_MAX_SUBJ) 241 let orgs: *u8 = sys_mmap(AL_ORGW * AL_MAX_SUBJ) 242 let bk: *i64 = acg_book(acc, refp, att, conf, boards, cfp, pl, doms, orgs) 243 let cf: *i64 = cfp[0] as *i64 244 gv_puts(" book: planes=" as *u8); gv_num(pl[0]); gv_puts(" board_rows=" as *u8); gv_num(pl[1]); gv_puts(" subjects=" as *u8); gv_num(bk[AL_B_N]) 245 gv_puts(" unmapped=" as *u8); gv_num(bk[AL_B_UNMAPPED]); gv_puts(" malformed=" as *u8); gv_num(bk[AL_B_MALFORMED]); gv_puts(" badname=" as *u8); gv_num(bk[AL_B_BADNAME]); gv_puts("\n" as *u8) 246 gv_check("fixture-all-three-planes-resolved" as *u8, acg_eq(pl[0], ACG_EXPECT_PLANES), ctr) 247 gv_check("fixture-conf-and-receipt-read-and-admitted" as *u8, acg_eq(cf[AL_C_CONF_OK] + cf[AL_C_RCPT_OK] + cf[AL_C_ADMITTED], 3), ctr) 248 gv_check("fixture-board-rows-seen" as *u8, acg_eq(pl[1], ACG_EXPECT_BOARD_ROWS), ctr) 249 gv_check("fixture-book-reached-every-subject-planes-plus-board" as *u8, acg_eq(bk[AL_B_N], ACG_EXPECT_SUBJECTS), ctr) 250 gv_check("fixture-no-row-was-malformed-or-badly-named" as *u8, acg_eq(bk[AL_B_MALFORMED] + bk[AL_B_BADNAME], 0), ctr) 251 gv_check("unmapped-operator-row-is-counted-once-and-creates-no-subject" as *u8, acg_eq(bk[AL_B_UNMAPPED], ACG_EXPECT_UNMAPPED) * acg_eq(al_bk_find_z(bk, "gpe_garment_draw" as *u8), 0 - 1), ctr) 252 let out: *u8 = sys_mmap(ACG_CAP) 253 let oo: *i64 = sys_mmap(ACG_LP) as *i64 254 oo[0] = 0 255 let unamed: i64 = acr_unmapped(bk[AL_B_ACC_PATH] as *u8, out, oo, ACG_CAP) 256 gv_check("unmapped-rows-named-agree-with-the-count-and-carry-the-remedy" as *u8, acg_eq(unamed, bk[AL_B_UNMAPPED]) * acg_has(out, oo[0], "UNMAPPED id=op-unmapped verdict=REJECT actor=operator targets=gameengine:gpe_garment_draw governs=NOTHING remedy=" as *u8), ctr) 257 258 // ---------------- IN-PROCESS: the three-party rule and every named negative --------------------------------- 259 let why: *i64 = sys_mmap(8 * ACR_WHY_WORDS) as *i64 260 gv_check("agreed-needs-all-three-signatures" as *u8, acg_eq(acg_party_of(bk, cf, "s_all" as *u8, why), ACR_P_AGREED), ctr) 261 gv_check("reject-after-accept-revokes-named-OPERATOR-REJECT" as *u8, acg_eq(acg_party_of(bk, cf, "s_revoked" as *u8, why), ACR_P_OP_REJECT), ctr) 262 gv_check("accept-after-reject-restores-agreement-order-is-load-bearing" as *u8, acg_eq(acg_party_of(bk, cf, "s_reaccept" as *u8, why), ACR_P_AGREED), ctr) 263 let plow: i64 = acg_party_of(bk, cf, "s_low" as *u8, why) 264 gv_check("referee-GOOD-word-below-the-floor-is-REFEREE-BELOW-BAND-not-agreed" as *u8, acg_eq(plow, ACR_P_REF_BELOW) * acg_eq(why[AL_WHY_FLOOR], ACG_FLOOR), ctr) 265 gv_check("referee-missing-named" as *u8, acg_eq(acg_party_of(bk, cf, "s_noref" as *u8, why), ACR_P_REF_MISSING), ctr) 266 gv_check("seat-missing-named" as *u8, acg_eq(acg_party_of(bk, cf, "s_noseat" as *u8, why), ACR_P_SEAT_MISSING), ctr) 267 gv_check("neg-control-an-ACCEPT-by-a-non-operator-actor-is-OPERATOR-MISSING" as *u8, acg_eq(acg_party_of(bk, cf, "s_nonop" as *u8, why), ACR_P_OP_MISSING), ctr) 268 gv_check("referee-row-on-an-unadmitted-tier-named-REFEREE-TIER-UNADMITTED" as *u8, acg_eq(acg_party_of(bk, cf, "s_badtier" as *u8, why), ACR_P_REF_TIER), ctr) 269 gv_check("plain-reject-with-referee-and-seat-present-is-OPERATOR-REJECT" as *u8, acg_eq(acg_party_of(bk, cf, "s_rejected" as *u8, why), ACR_P_OP_REJECT), ctr) 270 gv_check("board-subject-with-no-rows-is-OPERATOR-MISSING-not-absent" as *u8, acg_eq(acg_party_of(bk, cf, "s_board" as *u8, why), ACR_P_OP_MISSING), ctr) 271 let sib: i64 = al_bk_find_z(bk, "s_board" as *u8) 272 let siw: i64 = al_bk_find_z(bk, "s_wrongorgan" as *u8) 273 var lb: i64 = 0 274 var lw: i64 = 0 275 if sib >= 0 { lb = acr_status_line(bk, cf, sib, ((doms as i64) + sib * AL_NAMEW) as *u8, ((orgs as i64) + sib * AL_ORGW) as *u8, out, 0, ACG_CAP) } 276 let boardline_ok: i64 = acg_has(out, lb, " board=fixture organ=runtime/nx_accept_decl.nx organ_row=OK" as *u8) 277 if siw >= 0 { lw = acr_status_line(bk, cf, siw, ((doms as i64) + siw * AL_NAMEW) as *u8, ((orgs as i64) + siw * AL_ORGW) as *u8, out, 0, ACG_CAP) } 278 let wrongline: i64 = acg_has(out, lw, " organ_row=WRONG-FILE-cannot-flip" as *u8) 279 gv_check("board-row-naming-the-declaration-file-reads-organ_row-OK" as *u8, boardline_ok, ctr) 280 gv_bite("neg-control-board-row-naming-another-file-is-flagged-cannot-flip" as *u8, wrongline, 1 - boardline_ok, ctr) 281 282 // ---------------- IN-PROCESS: the emitter --------------------------------------------------------------------- 283 let e1: *u8 = sys_mmap(AL_DECL_CAP) 284 let e2: *u8 = sys_mmap(AL_DECL_CAP) 285 let n1: i64 = al_emit_buf(bk, cf, e1, AL_DECL_CAP) 286 let n2: i64 = al_emit_buf(bk, cf, e2, AL_DECL_CAP) 287 var same: i64 = 0 288 if n1 == n2 { if n1 > 0 { same = 1; var k: i64 = 0; while k < n1 { if e1[k] != e2[k] { same = 0; k = n1 } else { k = k + 1 } } } } 289 gv_puts(" emit: bytes=" as *u8); gv_num(n1); gv_puts(" decls=" as *u8); gv_num(al_count_decls(e1, n1)); gv_puts(" shape=" as *u8); gv_num(acr_decl_shape(e1, n1)); gv_puts("\n" as *u8) 290 gv_check("emit-declares-exactly-the-agreed-set-count" as *u8, acg_eq(al_count_decls(e1, n1), ACG_EXPECT_AGREED), ctr) 291 gv_check("emit-declares-the-two-agreed-subjects" as *u8, acr_declares(e1, n1, "s_all" as *u8) * acr_declares(e1, n1, "s_reaccept" as *u8), ctr) 292 gv_check("emit-declares-none-of-the-not-agreed-subjects" as *u8, acg_eq(acr_declares(e1, n1, "s_revoked" as *u8) + acr_declares(e1, n1, "s_low" as *u8) + acr_declares(e1, n1, "s_noref" as *u8) + acr_declares(e1, n1, "s_noseat" as *u8) + acr_declares(e1, n1, "s_nonop" as *u8) + acr_declares(e1, n1, "s_badtier" as *u8) + acr_declares(e1, n1, "s_rejected" as *u8) + acr_declares(e1, n1, "s_board" as *u8), 0), ctr) 293 let pa: i64 = acg_find(e1, n1, "func ga_accept_s_all(" as *u8) 294 let pr: i64 = acg_find(e1, n1, "func ga_accept_s_reaccept(" as *u8) 295 var sorted: i64 = 0 296 if pa >= 0 { if pr > pa { sorted = 1 } } 297 gv_check("emit-orders-declarations-by-name-not-by-plane-order" as *u8, sorted, ctr) 298 gv_check("emit-is-byte-identical-on-a-second-derivation" as *u8, same, ctr) 299 gv_check("emit-carries-the-derived-artefact-marker-in-its-head" as *u8, acg_has(e1, n1, "NX-DERIVED" as *u8), ctr) 300 gv_check("emit-every-code-line-is-the-one-compilable-declaration-form" as *u8, acg_eq(acr_decl_shape(e1, n1), ACG_EXPECT_AGREED), ctr) 301 // shape ruler neg-controls: a wrong return value and a missing keyword must both be refused 302 var t: i64 = al_catsl(e2, 0, e1, 0, n1) 303 t = al_cat(e2, t, "func ga_accept_s_low() -> i64 { return 0 }\n" as *u8) 304 let shape_bad1: i64 = acr_decl_shape(e2, t) 305 t = al_catsl(e2, 0, e1, 0, n1) 306 t = al_cat(e2, t, "ga_accept_evil() -> i64 { return 1 }\n" as *u8) 307 let shape_bad2: i64 = acr_decl_shape(e2, t) 308 var badfires: i64 = 0 309 if shape_bad1 < 0 { if shape_bad2 < 0 { badfires = 1 } } 310 var goodsilent: i64 = 0 311 if acr_decl_shape(e1, n1) == ACG_EXPECT_AGREED { goodsilent = 1 } 312 gv_bite("neg-control-shape-ruler-refuses-a-wrong-return-and-a-missing-keyword" as *u8, badfires, 1 - goodsilent, ctr) 313 // decl-verify: identical after an atomic write, convicted after a hand-added declaration 314 let wr: i64 = al_write_atomic(decl, e1, n1) 315 let dv_clean: i64 = al_decl_verify(bk, cf, decl) 316 t = al_catsl(e2, 0, e1, 0, n1) 317 t = al_cat(e2, t, "func ga_accept_s_low() -> i64 { return 1 }\n" as *u8) 318 al_write_atomic(decl, e2, t) 319 let dv_tampered: i64 = al_decl_verify(bk, cf, decl) 320 al_write_atomic(decl, e1, n1) 321 gv_check("decl-file-written-atomically-reads-back-IDENTICAL" as *u8, acg_eq(wr, 0) * acg_eq(dv_clean, AL_DV_IDENTICAL), ctr) 322 gv_bite("neg-control-decl-verify-convicts-a-hand-added-declaration" as *u8, acg_eq(dv_tampered, AL_DV_DIFFERS), 1 - acg_eq(dv_clean, AL_DV_IDENTICAL), ctr) 323 let sha_inproc: *u8 = sys_mmap(ACR_HEXCAP) 324 acr_sha256_buf(e1, n1, sha_inproc) 325 326 // ---------------- END-TO-END: the built subject on the same fixtures ------------------------------------------- 327 var subject: *u8 = ACG_SUBJECT_A 328 if argc >= 2 { subject = argv[1] as *u8 } 329 var sfd: i64 = sys_openat_rd(subject) 330 if sfd < 0 { if argc < 2 { subject = ACG_SUBJECT_B; sfd = sys_openat_rd(subject) } } 331 var have_subject: i64 = 0 332 if sfd >= 0 { sys_close(sfd); have_subject = 1 } 333 gv_puts(" subject: " as *u8); gv_puts(subject); gv_puts(" present=" as *u8); gv_num(have_subject); gv_puts("\n" as *u8) 334 if gv_need("the nx_accept subject elf is readable (argv[1], else buildroot/_build/nx_accept.sov.elf, else ./nx_accept.elf)" as *u8, have_subject, ctr) == 1 { 335 let ol: *i64 = sys_mmap(ACG_LP) as *i64 336 let sha_file: *u8 = sys_mmap(ACR_HEXCAP) 337 // emit twice: written then unchanged, and the file is the in-process derivation byte for byte 338 al_write_atomic(decl, e2, 0) 339 let r1: i64 = acg_run(subject, rootarg, "emit" as *u8, acg_nil(), acg_nil(), acg_nil(), acg_nil(), out, ol) 340 let w1: i64 = acg_has(out, ol[0], "ACCEPT-EMIT WRITTEN" as *u8) 341 acr_sha256_file(decl, sha_file) 342 gv_check("emit-verb-writes-the-in-process-derivation-byte-for-byte" as *u8, acg_eq(r1, 0) * w1 * al_streq(sha_file, sha_inproc), ctr) 343 let r2: i64 = acg_run(subject, rootarg, "emit" as *u8, acg_nil(), acg_nil(), acg_nil(), acg_nil(), out, ol) 344 let u2: i64 = acg_has(out, ol[0], "ACCEPT-EMIT UNCHANGED" as *u8) 345 acr_sha256_file(decl, sha_file) 346 gv_check("emit-verb-is-idempotent-second-run-UNCHANGED-same-bytes" as *u8, acg_eq(r2, 0) * u2 * al_streq(sha_file, sha_inproc), ctr) 347 // status names the band and the floor 348 let r3: i64 = acg_run(subject, rootarg, "status" as *u8, "s_low" as *u8, acg_nil(), acg_nil(), acg_nil(), out, ol) 349 gv_check("status-verb-names-REFEREE-BELOW-BAND-and-the-floor-it-used" as *u8, acg_eq(r3, ACR_EXIT_NOT_AGREED) * acg_has(out, ol[0], " missing=REFEREE-BELOW-BAND " as *u8) * acg_has(out, ol[0], " floor=151 " as *u8), ctr) 350 let r3b: i64 = acg_run(subject, rootarg, "status" as *u8, "s_all" as *u8, acg_nil(), acg_nil(), acg_nil(), out, ol) 351 gv_check("status-verb-exit-0-and-AGREED-for-the-agreed-subject" as *u8, acg_eq(r3b, ACR_EXIT_AGREED) * acg_has(out, ol[0], "verdict=AGREED" as *u8), ctr) 352 let r3c: i64 = acg_run(subject, rootarg, "status" as *u8, "s_nobody" as *u8, acg_nil(), acg_nil(), acg_nil(), out, ol) 353 gv_check("status-verb-third-state-UNKNOWN-SUBJECT-for-a-name-no-plane-or-board-carries" as *u8, acg_eq(r3c, ACR_EXIT_UNKNOWN) * acg_has(out, ol[0], "verdict=UNKNOWN-SUBJECT" as *u8), ctr) 354 // list partition 355 let r4: i64 = acg_run(subject, rootarg, "list" as *u8, acg_nil(), acg_nil(), acg_nil(), acg_nil(), out, ol) 356 gv_check("list-verb-partition-subjects-agreed-not_agreed-and-unmapped-both-counters" as *u8, acg_eq(r4, 0) * acg_has(out, ol[0], "ACCEPT-LEDGER subjects=11 agreed=2 not_agreed=9 planes=3/3 acc_rows=12 unmapped=1 unmapped_named=1 ref_rows=8 att_rows=8" as *u8), ctr) 357 // NEG-CONTROL: there is no verb that writes the operator plane 358 let r5: i64 = acg_run(subject, rootarg, "accept" as *u8, "s_all" as *u8, "ACCEPT" as *u8, acg_nil(), acg_nil(), out, ol) 359 let bk2: *i64 = acg_book(acc, refp, att, conf, boards, cfp, pl, doms, orgs) 360 gv_check("neg-control-organ-has-no-verb-that-writes-accept-usage-exit-and-plane-unchanged" as *u8, acg_eq(r5, ACR_EXIT_USAGE) * acg_eq(bk2[AL_B_ACC_ROWS], ACG_EXPECT_ACC_ROWS) * acg_eq(al_count_accepted(bk2, cfp[0] as *i64), ACG_EXPECT_AGREED), ctr) 361 // writer composition: attest lands a row through nx_store_put and the subject becomes AGREED 362 let welf: *u8 = sys_mmap(ACG_PATH) 363 let have_writer: i64 = ep_artifact_path(welf, ACG_WRITER) 364 if gv_need("nx_store_put.elf resolves (the writer the attest and referee verbs compose)" as *u8, have_writer, ctr) == 1 { 365 let r6: i64 = acg_run(subject, rootarg, "attest" as *u8, "s_noseat" as *u8, ACG_SEAT, ACG_WORDS, art, out, ol) 366 let bk3: *i64 = acg_book(acc, refp, att, conf, boards, cfp, pl, doms, orgs) 367 let cf3: *i64 = cfp[0] as *i64 368 gv_check("attest-verb-composes-the-writer-and-completes-the-third-signature" as *u8, acg_eq(r6, 0) * acg_has(out, ol[0], "verdict=ATTESTED" as *u8) * acg_eq(bk3[AL_B_ATT_ROWS], ACG_EXPECT_ATT_ROWS + 1) * acg_eq(acg_party_of(bk3, cf3, "s_noseat" as *u8, why), ACR_P_AGREED), ctr) 369 let r7: i64 = acg_run(subject, rootarg, "emit" as *u8, acg_nil(), acg_nil(), acg_nil(), acg_nil(), out, ol) 370 let dl: *i64 = sys_mmap(ACG_LP) as *i64 371 let db: *u8 = sys_read_file(decl, dl) 372 var dcount: i64 = 0 - 1 373 if (db as i64) != 0 { dcount = al_count_decls(db, dl[0]) } 374 gv_check("emit-tracks-the-planes-a-new-signature-adds-exactly-one-declaration" as *u8, acg_eq(r7, 0) * acg_has(out, ol[0], "ACCEPT-EMIT WRITTEN" as *u8) * acg_eq(dcount, ACG_EXPECT_DECLS_AFTER_ATTEST), ctr) 375 // refusals: unadmitted tier, unreadable capture, unreadable artifact -- no row written for any of them 376 let r8: i64 = acg_run(subject, rootarg, "referee" as *u8, "s_all" as *u8, conf, ACG_TIER_BAD, ACG_SEAT, out, ol) 377 let bk4: *i64 = acg_book(acc, refp, att, conf, boards, cfp, pl, doms, orgs) 378 gv_check("neg-control-referee-refuses-an-unadmitted-tier-by-name-and-writes-no-row" as *u8, acg_eq(r8, ACR_EXIT_REFUSED) * acg_has(out, ol[0], "REFUSED TIER-UNADMITTED" as *u8) * acg_eq(bk4[AL_B_REF_ROWS], ACG_EXPECT_REF_ROWS), ctr) 379 let r9: i64 = acg_run(subject, rootarg, "referee" as *u8, "s_all" as *u8, absent, ACG_TIER, ACG_SEAT, out, ol) 380 let bk5: *i64 = acg_book(acc, refp, att, conf, boards, cfp, pl, doms, orgs) 381 gv_check("neg-control-referee-refuses-an-unreadable-capture-and-writes-no-row" as *u8, acg_eq(r9, ACR_EXIT_REFUSED) * acg_has(out, ol[0], "REFUSED capture-unreadable" as *u8) * acg_eq(bk5[AL_B_REF_ROWS], ACG_EXPECT_REF_ROWS), ctr) 382 let r10: i64 = acg_run(subject, rootarg, "attest" as *u8, "s_noref" as *u8, ACG_SEAT, ACG_WORDS, absent, out, ol) 383 let bk6: *i64 = acg_book(acc, refp, att, conf, boards, cfp, pl, doms, orgs) 384 gv_check("neg-control-attest-refuses-an-unreadable-artifact-and-writes-no-row" as *u8, acg_eq(r10, ACR_EXIT_REFUSED) * acg_has(out, ol[0], "REFUSED artifact-unreadable" as *u8) * acg_eq(bk6[AL_B_ATT_ROWS], ACG_EXPECT_ATT_ROWS + 1), ctr) 385 } 386 } 387 return gv_verdict("ACCEPT-GATE" as *u8, ctr, "three-party agreement is derived, never declared; every negative is named; emit is deterministic; the writer is composed and refused where it must be" as *u8) 388}