code wiki / (root) / nx_comparewatch_census_gate.nx

nx_comparewatch_census_gate.nx source

↩ module page · 119 lines · 8489 B

1// nx_comparewatch_census_gate.nx -- proves the /compare watch-plane census parsers (2026-08-29). 2// Composes nx_comparewatch_lib IN-PROCESS on fixtures CONSTRUCTED AT RUNTIME (tab bytes written as 9, 3// never embedded in source literals -- the lexer hazard, and also so no source scanner ever finds a 4// fixture row pretending to be data). No filesystem, no seg-store, no fork: every rule is decidable. 5// 6// THE LOAD-BEARING TOOTH is the production trap this whole organ exists for: a LANDED row whose LABEL 7// carries the literal token "OPEN:" (measured live: legalpractice_of_import). A substring ruler counts 8// that row OPEN; the positional ruler must not. The fixture ASSERTS it contains the trap token before 9// asserting the verdict, so a fixture that drifted could never pass vacuously. 10// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 11import "nx_syscalls.nx" 12import "nx_gate_verdict.nx" 13import "nx_comparewatch_lib.nx" 14 15const CWG_BUF: i64 = 1024 16const CWG_TAB: i64 = 9 17 18func cwg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 19func cwg_cat(b: *u8, o: i64, s: *u8) -> i64 { var i: i64 = 0; var p: i64 = o; while s[i] != (0 as u8) { b[p] = s[i]; p = p + 1; i = i + 1 } return p } 20func cwg_tab(b: *u8, o: i64) -> i64 { b[o] = CWG_TAB as u8; return o + 1 } 21// one 6-field plane row: id, domain, label, organ, symbol, status -- tabs constructed, never quoted. 22func cwg_row(b: *u8, id: *u8, dom: *u8, label: *u8, org: *u8, sym: *u8, status: *u8) -> i64 { 23 var o: i64 = cwg_cat(b, 0, id) 24 o = cwg_tab(b, o); o = cwg_cat(b, o, dom) 25 o = cwg_tab(b, o); o = cwg_cat(b, o, label) 26 o = cwg_tab(b, o); o = cwg_cat(b, o, org) 27 o = cwg_tab(b, o); o = cwg_cat(b, o, sym) 28 o = cwg_tab(b, o); o = cwg_cat(b, o, status) 29 return o 30} 31func cwg_contains(b: *u8, n: i64, needle: *u8) -> i64 { 32 let nl: i64 = cwg_slen(needle) 33 if nl == 0 { return 1 } 34 if n < nl { return 0 } 35 var i: i64 = 0 36 while i <= n - nl { 37 var m: i64 = 1 38 var c: i64 = 0 39 while c < nl { if b[i + c] != needle[c] { m = 0; c = nl } else { c = c + 1 } } 40 if m == 1 { return 1 } 41 i = i + 1 42 } 43 return 0 44} 45 46func main(argc: i64, argv: *i64) -> i64 { 47 gv_head("nx_comparewatch_census_gate -- status is POSITIONAL, exact-length, and unknowns get their own bucket" as *u8) 48 let c: *i64 = gv_ctr() 49 let b: *u8 = sys_mmap(CWG_BUF) 50 51 // ---- plain verdicts ------------------------------------------------------------------------ 52 var n: i64 = cwg_row(b, "id1" as *u8, "mydomain" as *u8, "LIVE: a label" as *u8, "runtime/x.nx" as *u8, "sym_a" as *u8, "OPEN" as *u8) 53 gv_check("open-row-reads-OPEN" as *u8, cw_status_code(b, n) == CW_OPEN, c) 54 n = cwg_row(b, "id2" as *u8, "mydomain" as *u8, "LIVE: b label" as *u8, "runtime/x.nx" as *u8, "sym_b" as *u8, "LANDED" as *u8) 55 gv_check("landed-row-reads-LANDED" as *u8, cw_status_code(b, n) == CW_LANDED, c) 56 57 // ---- THE PRODUCTION TRAP: "OPEN:" inside a LANDED row's label ------------------------------- 58 n = cwg_row(b, "legalpractice_of_import" as *u8, "legalpractice" as *u8, "OPEN: Google Docs and any Word file brought in by upload" as *u8, "runtime/nx_office_daemon.nx" as *u8, "of_import" as *u8, "LANDED" as *u8) 59 gv_check("fixture-reached-the-condition-label-carries-the-OPEN-colon-token" as *u8, cwg_contains(b, n, "OPEN:" as *u8) == 1, c) 60 gv_check("neg-control-landed-row-with-OPEN-in-prose-reads-LANDED-not-OPEN" as *u8, cw_status_code(b, n) == CW_LANDED, c) 61 // and the substring-control that PROVES the fixture discriminates the two rulers: a substring scan 62 // finds "OPEN" in this row, so any implementation equivalent to one would have failed the tooth above. 63 gv_check("substring-control-FIRES-on-the-same-fixture" as *u8, cwg_contains(b, n, "OPEN" as *u8) == 1, c) 64 65 // ---- exactness + unknown bucket ------------------------------------------------------------- 66 n = cwg_row(b, "id3" as *u8, "d" as *u8, "l" as *u8, "o" as *u8, "s" as *u8, "PENDING" as *u8) 67 gv_check("neg-control-unknown-status-lands-in-OTHER-never-a-known-bucket" as *u8, cw_status_code(b, n) == CW_OTHER, c) 68 n = cwg_row(b, "id4" as *u8, "d" as *u8, "l" as *u8, "o" as *u8, "s" as *u8, "OPENX" as *u8) 69 gv_check("neg-control-OPENX-is-not-OPEN (exact length)" as *u8, cw_status_code(b, n) == CW_OTHER, c) 70 n = cwg_row(b, "id5" as *u8, "d" as *u8, "l" as *u8, "o" as *u8, "s" as *u8, "LANDED2" as *u8) 71 gv_check("neg-control-LANDED2-is-not-LANDED (exact length)" as *u8, cw_status_code(b, n) == CW_OTHER, c) 72 73 // trailing newline / CR trimmed before the compare 74 n = cwg_row(b, "id6" as *u8, "d" as *u8, "l" as *u8, "o" as *u8, "s" as *u8, "OPEN" as *u8) 75 b[n] = 10 as u8 76 gv_check("trailing-newline-is-trimmed-before-the-compare" as *u8, cw_status_code(b, n + 1) == CW_OPEN, c) 77 n = cwg_row(b, "id7" as *u8, "d" as *u8, "l" as *u8, "o" as *u8, "s" as *u8, "LANDED" as *u8) 78 b[n] = 13 as u8 79 b[n + 1] = 10 as u8 80 gv_check("trailing-CRLF-is-trimmed-before-the-compare" as *u8, cw_status_code(b, n + 2) == CW_LANDED, c) 81 82 // a row with NO tab has no final field: MALFORMED, its own bucket 83 let m0: i64 = cwg_cat(b, 0, "just prose with the word OPEN in it" as *u8) 84 gv_check("neg-control-tabless-row-is-MALFORMED-not-OPEN" as *u8, cw_status_code(b, m0) == CW_MALFORMED, c) 85 86 // ---- field extraction ----------------------------------------------------------------------- 87 n = cwg_row(b, "id8" as *u8, "mydomain" as *u8, "l" as *u8, "o" as *u8, "s" as *u8, "OPEN" as *u8) 88 let f2: *i64 = sys_mmap(16) as *i64 89 var fok: i64 = 0 90 if cw_field(b, n, 1, f2) == 1 { if cw_field_eq(b, f2[0], f2[1], "mydomain" as *u8) == 1 { fok = 1 } } 91 gv_check("domain-is-field-1-extracted-by-position" as *u8, fok == 1, c) 92 gv_check("neg-control-field-9-of-a-6-field-row-refuses" as *u8, cw_field(b, n, 9, f2) == 0, c) 93 94 // ---- key parsing ---------------------------------------------------------------------------- 95 gv_check("key-q17-parses-to-17" as *u8, cw_key_idx("q:17" as *u8, 4) == 17, c) 96 gv_check("key-qn-is-the-declared-count-sentinel" as *u8, cw_key_idx("q:n" as *u8, 3) == CW_KEY_COUNT, c) 97 gv_check("neg-control-q1x-refuses-as-FOREIGN" as *u8, cw_key_idx("q:1x" as *u8, 4) == CW_KEY_FOREIGN, c) 98 gv_check("neg-control-alien-key-refuses-as-FOREIGN" as *u8, cw_key_idx("zz:3" as *u8, 4) == CW_KEY_FOREIGN, c) 99 gv_check("neg-control-bare-q-colon-refuses" as *u8, cw_key_idx("q:" as *u8, 2) == CW_KEY_FOREIGN, c) 100 gv_check("declared-count-945-parses" as *u8, cw_parse_count("945" as *u8, 3) == 945, c) 101 gv_check("neg-control-unparseable-count-is-minus-1-never-zero" as *u8, cw_parse_count("94x" as *u8, 3) == (0 - 1), c) 102 103 // ---- last-version-wins apply + bounds ------------------------------------------------------- 104 let stA: *i64 = sys_mmap(8 * 16) as *i64 105 let dmB: *u8 = sys_mmap(16 * 16) 106 gv_check("apply-first-version-lands" as *u8, cw_apply(stA, dmB, 16, 16, 3, CW_OPEN, "alpha" as *u8, 5) == 1, c) 107 cw_apply(stA, dmB, 16, 16, 3, CW_LANDED, "beta" as *u8, 4) 108 var lastwins: i64 = 0 109 if stA[3] == CW_LANDED { if dmB[3 * 16] == (98 as u8) { lastwins = 1 } } // 'b' of beta 110 gv_check("apply-LAST-version-wins-status-and-domain-both-overwritten" as *u8, lastwins == 1, c) 111 gv_check("neg-control-apply-refuses-out-of-range-idx" as *u8, cw_apply(stA, dmB, 16, 16, 99, CW_OPEN, "x" as *u8, 1) == 0, c) 112 gv_check("neg-control-apply-refuses-negative-idx" as *u8, cw_apply(stA, dmB, 16, 16, 0 - 4, CW_OPEN, "x" as *u8, 1) == 0, c) 113 // domain longer than the slot is TRUNCATED, never overrun: slot width 16 -> 15 chars + NUL 114 cw_apply(stA, dmB, 16, 16, 5, CW_OPEN, "aaaaaaaaaaaaaaaaaaaaaaaa" as *u8, 24) 115 gv_check("overlong-domain-truncates-with-NUL-inside-the-slot" as *u8, dmB[5 * 16 + 15] == (0 as u8), c) 116 117 return gv_verdict("nx_comparewatch_census_gate" as *u8, c, 118 "Watch-plane status is decided by the FINAL tab field with exact-length compares -- the measured production row whose LANDED label carries the token OPEN: reads LANDED, and the substring-control fires on the same fixture to prove it discriminates. Unknown statuses and tabless rows get their own buckets, keys parse strictly with q:n as the declared-count sentinel, an unparseable count is -1 never zero, and the last-version-wins apply overwrites both status and domain while refusing out-of-range rows." as *u8) 119}