code wiki / (root) / nx_pageref_gate.nx

nx_pageref_gate.nx source

↩ module page · 201 lines · 13320 B

1// nx_pageref_gate.nx -- the IN-PROCESS referee for nx_pageref_lib: the asset-reference vocabulary and the 2// 404-fallback extension class. In-process ON PURPOSE -- the sibling nx_page_verify_gate proves the 3// DEPLOYED verifier end-to-end over the real edge, and a gate that fork/execs a deployed elf cannot be 4// mutation-proven. This one imports the lib, so nx_gate_bite can substitute a mutant and watch it die. 5// 6// EVERY ORACLE BELOW IS A HAND-WRITTEN LITERAL, NEVER A SECOND CALL INTO THE LIB. A tooth that calls the 7// same function on both sides of its comparison cannot fail: it agrees with a mutant as readily as with 8// the truth. The skip lengths (5 for src plus its quote, 10 for data-glb plus its quote) and the 9// extension indices are typed out here independently of pr_len and pr_binext. 10// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 11import "nx_syscalls.nx" 12import "nx_gate_verdict.nx" 13import "nx_pageref_lib.nx" 14 15// hand-written oracles -- what this gate is entitled to know without asking the subject 16const PRG_SKIP_SRC: i64 = 5 // src= plus its opening quote 17const PRG_SKIP_DATAGLB: i64 = 10 // data-glb= plus its opening quote 18const PRG_ATTR_SRC: i64 = 0 19const PRG_ATTR_DATAGLB: i64 = 1 20const PRG_QUOTE_DQ: i64 = 34 21const PRG_QUOTE_SQ: i64 = 39 22const PRG_MISS: i64 = 0 - 1 23const PRG_EXT_PNG: i64 = 0 24const PRG_EXT_JS: i64 = 3 25const PRG_EXT_GLB: i64 = 4 26const PRG_EXT_VRM: i64 = 5 27const PRG_EXT_WASM: i64 = 6 28const PRG_EXT_NXDV: i64 = 7 29const PRG_EXT_NXA: i64 = 8 30// declared assets (2026-09-05): a meta row named nishi-<kind> promises a script-fetched artifact 31const PRG_ATTR_DECLARED: i64 = 2 32const PRG_SKIP_CONTENT: i64 = 9 // content= plus its opening quote 33const PRG_OFF_META_ATTR: i64 = 23 // <meta name="nishi-nxa" is 22 bytes; the space puts content= at 23 34const PRG_OFF_DESC_ATTR: i64 = 25 // <meta name="description" is 24 bytes; the space puts content= at 25 35const PRG_OFF_DIV_ATTR: i64 = 16 // <div data-x="1" is 15 bytes; the space puts content= at 16 36// fixture offsets, counted by hand from the fixture text so fixture and subject can disagree freely 37const PRG_OFF_IMG_ATTR: i64 = 5 // the five bytes of an img tag opening put src= at 5 38const PRG_OFF_CANV_ATTR: i64 = 8 // the eight bytes of a canvas tag opening put data-glb= at 8 39const PRG_CH_s: i64 = 115 40const PRG_CH_d: i64 = 100 41const PRG_CH_o: i64 = 111 42const PRG_CH_c: i64 = 99 43const PRG_LT: i64 = 60 44const PRG_BANG: i64 = 33 45const PRG_OUT_SLOTS: i64 = 2 46const PRG_WORD_BYTES: i64 = 8 47const PRG_BIN_BYTES: i64 = 8 48const PRG_DOCT_BYTES: i64 = 5 49const PRG_WASM_B1: i64 = 97 // a 50const PRG_WASM_B2: i64 = 115 // s 51const PRG_WASM_B3: i64 = 109 // m 52 53// the gate's own comparator. gv_check wants a condition that is EXACTLY 1, and spelling that here rather 54// than leaning on the comparison operator's return shape keeps every tooth's truth value explicit. 55func prg_is(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 56 57func prg_declared(f: *u8) -> i64 { 58 let n: i64 = pr_len(f) 59 let out: *i64 = sys_mmap(PRG_OUT_SLOTS*PRG_WORD_BYTES) as *i64 60 var i: i64 = 0 61 var found: i64 = PRG_MISS 62 while i < n { 63 if pr_starts(f,n,i,"content=" as *u8) == 1 { found = pr_declared_hit(f,n,i,out); break } 64 i = i+1 65 } 66 sys_munmap(out as *u8,PRG_OUT_SLOTS*PRG_WORD_BYTES) 67 return found 68} 69 70func main() -> i64 { 71 let ctr: *i64 = gv_ctr() 72 gv_head("nx_pageref_gate (the asset-reference vocabulary: what a page promises the browser will fetch)" as *u8) 73 74 let out: *i64 = sys_mmap(PRG_OUT_SLOTS * PRG_WORD_BYTES) as *i64 75 76 let f_dq: *u8 = "<img src=\"a.png\">" as *u8 77 let f_sq: *u8 = "<img src='a.png'>" as *u8 78 let f_gdq: *u8 = "<canvas data-glb=\"/x.glb\" data-mode=\"turn\"></canvas>" as *u8 79 let f_gsq: *u8 = "<canvas data-glb='/x.glb'></canvas>" as *u8 80 let f_foo: *u8 = "<div data-foo=\"x\"></div>" as *u8 81 let f_bare: *u8 = "<img src=a.png>" as *u8 82 83 // ---- ANTI-VACUITY FIRST. Prove each fixture actually reached the condition the outcome teeth are 84 // about: an outcome asserted over a fixture that never held the attribute is a green about nothing. 85 // These read the raw byte, so they cannot be satisfied by the matcher under test. 86 gv_check("fixture-img-really-carries-an-attribute-byte-at-the-offset-under-test" as *u8, 87 prg_is(f_dq[PRG_OFF_IMG_ATTR] as i64, PRG_CH_s), ctr) 88 gv_check("fixture-canvas-really-carries-an-attribute-byte-at-the-offset-under-test" as *u8, 89 prg_is(f_gdq[PRG_OFF_CANV_ATTR] as i64, PRG_CH_d), ctr) 90 91 // ---- THE INCUMBENT VOCABULARY, PRESERVED. src= in both quote styles must keep resolving exactly as 92 // it did, or this change bought coverage by losing coverage. 93 let h1: i64 = pr_attr_hit(f_dq, pr_len(f_dq), PRG_OFF_IMG_ATTR, out) 94 gv_check("src-double-quote-resolves-to-the-src-attribute" as *u8, prg_is(h1, PRG_ATTR_SRC), ctr) 95 gv_check("src-double-quote-skips-past-attribute-and-quote" as *u8, prg_is(out[0], PRG_SKIP_SRC), ctr) 96 gv_check("src-double-quote-closes-on-a-double-quote" as *u8, prg_is(out[1], PRG_QUOTE_DQ), ctr) 97 98 let h2: i64 = pr_attr_hit(f_sq, pr_len(f_sq), PRG_OFF_IMG_ATTR, out) 99 gv_check("src-single-quote-resolves-to-the-src-attribute" as *u8, prg_is(h2, PRG_ATTR_SRC), ctr) 100 gv_check("src-single-quote-closes-on-a-single-quote" as *u8, prg_is(out[1], PRG_QUOTE_SQ), ctr) 101 102 // ---- THE NEW COVERAGE. data-glb= is the attribute nx_asset_page emits for every mesh panel, and the 103 // verifier's extractor had never heard of it, so four mesh refs per /exceed page were acquitted 104 // without ever being fetched. 105 let h3: i64 = pr_attr_hit(f_gdq, pr_len(f_gdq), PRG_OFF_CANV_ATTR, out) 106 gv_check("data-glb-double-quote-resolves-to-the-mesh-attribute" as *u8, prg_is(h3, PRG_ATTR_DATAGLB), ctr) 107 gv_check("data-glb-double-quote-skips-past-attribute-and-quote" as *u8, prg_is(out[0], PRG_SKIP_DATAGLB), ctr) 108 gv_check("data-glb-double-quote-closes-on-a-double-quote" as *u8, prg_is(out[1], PRG_QUOTE_DQ), ctr) 109 110 let h4: i64 = pr_attr_hit(f_gsq, pr_len(f_gsq), PRG_OFF_CANV_ATTR, out) 111 gv_check("data-glb-single-quote-resolves-to-the-mesh-attribute" as *u8, prg_is(h4, PRG_ATTR_DATAGLB), ctr) 112 gv_check("data-glb-single-quote-closes-on-a-single-quote" as *u8, prg_is(out[1], PRG_QUOTE_SQ), ctr) 113 114 // ---- NEGATIVE CONTROLS on the vocabulary. A table that matched everything would pass every tooth 115 // above and be worthless: these are the inputs it MUST decline. 116 let n1: i64 = pr_attr_hit(f_foo, pr_len(f_foo), PRG_OFF_IMG_ATTR, out) 117 gv_check("neg-control-an-unrelated-data-attribute-is-not-an-asset-ref" as *u8, prg_is(n1, PRG_MISS), ctr) 118 let n2: i64 = pr_attr_hit(f_bare, pr_len(f_bare), PRG_OFF_IMG_ATTR, out) 119 gv_check("neg-control-an-unquoted-attribute-is-left-to-the-callers-bare-branch" as *u8, prg_is(n2, PRG_MISS), ctr) 120 121 // ---- DECLARED ASSETS (2026-09-05). A page names the artifact its script will fetch in a meta row; the verifier 122 // used to acquit /world/rigview having fetched one advert PNG while the 1.7 MB rig it declares went unchecked. 123 let f_meta: *u8 = "<meta name=\"nishi-nxa\" content=\"/world/ref9d.nxa\">" as *u8 124 let f_desc: *u8 = "<meta name=\"description\" content=\"a page\">" as *u8 125 let f_divc: *u8 = "<div data-x=\"1\" content=\"/a\"></div>" as *u8 126 gv_check("fixture-meta-really-carries-content-at-the-offset-under-test" as *u8, prg_is(f_meta[PRG_OFF_META_ATTR] as i64, PRG_CH_c), ctr) 127 let h5: i64 = pr_declared_hit(f_meta, pr_len(f_meta), PRG_OFF_META_ATTR, out) 128 gv_check("meta-nishi-content-resolves-to-the-declared-asset-class" as *u8, prg_is(h5, PRG_ATTR_DECLARED), ctr) 129 gv_check("meta-nishi-content-skips-past-attribute-and-quote" as *u8, prg_is(out[0], PRG_SKIP_CONTENT), ctr) 130 gv_check("meta-nishi-content-closes-on-a-double-quote" as *u8, prg_is(out[1], PRG_QUOTE_DQ), ctr) 131 let n3: i64 = pr_declared_hit(f_desc, pr_len(f_desc), PRG_OFF_DESC_ATTR, out) 132 gv_check("neg-control-a-description-meta-is-not-a-declared-asset" as *u8, prg_is(n3, PRG_MISS), ctr) 133 let n4: i64 = pr_declared_hit(f_divc, pr_len(f_divc), PRG_OFF_DIV_ATTR, out) 134 gv_check("neg-control-a-content-attribute-outside-a-meta-tag-is-not-a-declared-asset" as *u8, prg_is(n4, PRG_MISS), ctr) 135 let n5: i64 = pr_attr_hit(f_meta, pr_len(f_meta), PRG_OFF_META_ATTR, out) 136 gv_check("neg-control-the-plain-attribute-table-still-declines-content (the declared rule is a separate door)" as *u8, prg_is(n5, PRG_MISS), ctr) 137 gv_check("ext-nxa-classified" as *u8, prg_is(pr_ext_class("/world/ref9d.nxa" as *u8), PRG_EXT_NXA), ctr) 138 139 // ---- THE EXTENSION CLASS. The incumbent four must survive; the four that make an /exceed page are new. 140 gv_check("ext-png-still-classified" as *u8, prg_is(pr_ext_class("/a/b.png" as *u8), PRG_EXT_PNG), ctr) 141 gv_check("ext-js-still-classified" as *u8, prg_is(pr_ext_class("/a/b.js" as *u8), PRG_EXT_JS), ctr) 142 gv_check("ext-glb-classified" as *u8, prg_is(pr_ext_class("/a/b.glb" as *u8), PRG_EXT_GLB), ctr) 143 gv_check("ext-vrm-classified" as *u8, prg_is(pr_ext_class("/a/b.vrm" as *u8), PRG_EXT_VRM), ctr) 144 gv_check("ext-wasm-classified" as *u8, prg_is(pr_ext_class("/a/b.wasm" as *u8), PRG_EXT_WASM), ctr) 145 gv_check("ext-nxdv-classified" as *u8, prg_is(pr_ext_class("/a/b.nxdv" as *u8), PRG_EXT_NXDV), ctr) 146 147 gv_check("neg-control-html-is-not-in-the-must-not-answer-html-class" as *u8, 148 prg_is(pr_ext_class("/a/b.html" as *u8), PRG_MISS), ctr) 149 gv_check("neg-control-extension-match-is-exact-not-a-prefix-at-the-dot" as *u8, 150 prg_is(pr_ext_class("/a/b.glbx" as *u8), PRG_MISS), ctr) 151 gv_check("neg-control-a-url-with-no-dot-has-no-extension-class" as *u8, 152 prg_is(pr_ext_class("/a/bglb" as *u8), PRG_MISS), ctr) 153 154 // ---- THE 404-FALLBACK VERDICT, BITE-PROVEN BOTH WAYS. A 200 carrying an error page where a mesh was 155 // promised is the whole failure this class exists to name, and a rule that fired on real glTF bytes 156 // would be worse than no rule at all. 157 let html: *u8 = "<html><body>404</body></html>" as *u8 158 let gltf: *u8 = "glTF binary payload follows" as *u8 159 // the doctype fixture is assembled byte-wise: the character that opens a doctype declaration is the 160 // one the nx_cc lexer refuses inside a string literal, and building it here also proves the rule is 161 // structural rather than a match against one spelling. 162 let doct: *u8 = sys_mmap(PRG_DOCT_BYTES) 163 doct[0] = PRG_LT as u8 164 doct[1] = PRG_BANG as u8 165 doct[2] = PRG_CH_d as u8 166 doct[3] = PRG_CH_o as u8 167 doct[4] = PRG_CH_c as u8 168 169 gv_bite("fallback-a-glb-that-answers-html-is-broken" as *u8, 170 pr_is_fallback("/x.glb" as *u8, html, pr_len(html)), 171 pr_is_fallback("/x.glb" as *u8, gltf, pr_len(gltf)), ctr) 172 gv_bite("fallback-a-doctype-body-counts-the-same-as-an-html-element" as *u8, 173 pr_is_fallback("/x.vrm" as *u8, doct, PRG_DOCT_BYTES), 174 pr_is_fallback("/x.vrm" as *u8, gltf, pr_len(gltf)), ctr) 175 gv_bite("neg-control-fallback-needs-BOTH-an-artifact-extension-and-an-html-body" as *u8, 176 pr_is_fallback("/x.wasm" as *u8, html, pr_len(html)), 177 pr_is_fallback("/x.html" as *u8, html, pr_len(html)), ctr) 178 179 // a real wasm body begins with a NUL, which no string literal can carry -- assembled at runtime so the 180 // good side of this control is the actual wire shape and not a stand-in for it. 181 let wasm: *u8 = sys_mmap(PRG_BIN_BYTES) 182 wasm[0] = 0 as u8 183 wasm[1] = PRG_WASM_B1 as u8 184 wasm[2] = PRG_WASM_B2 as u8 185 wasm[3] = PRG_WASM_B3 as u8 186 gv_check("neg-control-real-wasm-magic-is-not-an-html-body" as *u8, 187 prg_is(pr_body_is_html(wasm, PRG_BIN_BYTES), 0), ctr) 188 gv_check("neg-control-an-empty-body-is-not-an-html-body" as *u8, 189 prg_is(pr_body_is_html(html, 0), 0), ctr) 190 191 let f_game: *u8 = "<meta name=\"nishi-game\" content=\"nx_desktop_craft\">" as *u8 192 let f_release: *u8 = "<meta name=\"nishi-release\" content=\"496ac57a773aebeed3d68d347cc0b7841ca0cfa4b04bb3bfe851dcd129a75a05\">" as *u8 193 gv_check("game-identity-is-not-an-asset",prg_declared(f_game)==PRG_MISS,ctr) 194 gv_check("release-digest-is-not-an-asset",prg_declared(f_release)==PRG_MISS,ctr) 195 gv_check("wasm-declaration-remains-an-asset",prg_declared("<meta name=\"nishi-wasm\" content=\"/releases/beach.wasm\">" as *u8)==PRG_ATTR_DECLARED,ctr) 196 gv_check("generic-asset-allows-extensionless-resource",prg_declared("<meta name='nishi-asset' content='/api/resource/scene'>" as *u8)==PRG_ATTR_DECLARED,ctr) 197 gv_check("asset-type-is-exact-not-prefix",prg_declared("<meta name='nishi-nxa-extra' content='/a'>" as *u8)==PRG_MISS,ctr) 198 gv_check("nxa-single-quote-remains-an-asset",prg_declared("<meta name='nishi-nxa' content='/world/ref9d.nxa'>" as *u8)==PRG_ATTR_DECLARED,ctr) 199 return gv_verdict("nx_pageref_gate" as *u8, ctr, 200 "the asset-reference vocabulary is one table, read by the verifier and by this gate, so a reference class cannot be known to one and unknown to the other" as *u8) 201}