nx_glprobe_gate.nx source
↩ module page · 113 lines · 7518 B
1// nx_glprobe_gate.nx -- THE REFEREE FOR THE GL-CONTEXT PROBE RULER (nx_glprobe_lib), 2026-09-02.
2//
3// IN-PROCESS over the lib, deliberately (a gate that forks a deployed .elf reports NOT-REACHED for every
4// mutant). It proves: (1) the classifier separates its four states and is not a constant; (2) ONE TABLE,
5// TWO SURFACES -- every native state name and remedy string is carried verbatim inside the emitted JS, so
6// the page and the MCP caller cannot disagree; (3) the probe never claims a 2d context on the target canvas
7// (the poisoned-canvas class); (4) the bare-refusal detector FIRES on a runtime-assembled bare refusal and
8// stays silent on the diagnosed form (the neg-control pair); (5) every page emitter that acquires a WebGL2
9// context COMPOSES the probe and ships ZERO bare refusals -- emitter sources read from buildroot/runtime,
10// an unreadable emitter degrades to a NAMED SKIP through gv_need, never a green.
11// SCOPE: this does not run a browser; the served page's behaviour under a refusing browser is proven by the
12// 2026-09-02 headless measurements recorded in the lib header, not by this gate.
13// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
14import "nx_gate_verdict.nx"
15import "nx_glprobe_lib.nx"
16
17const GG_EMITTERS: i64 = 4
18const GG_E1: *u8 = "buildroot/runtime/nx_game_page_emit.nx"
19const GG_E2: *u8 = "buildroot/runtime/nx_nxa_rig_emit.nx"
20const GG_E3: *u8 = "buildroot/runtime/nx_nxa_view_emit.nx"
21const GG_E4: *u8 = "buildroot/runtime/nx_nxa_stream_emit.nx"
22const GG_FIX_BYTES: i64 = 256
23
24// runtime-assembled fixtures: the bare form `throw"no webgl2"` and the diagnosed form `throw"no webgl2 (x)"`
25func gg_fixture(buf: *u8, diagnosed: i64) -> i64 {
26 var p: i64 = 0
27 let a: *u8 = "if(g===null)throw" as *u8
28 var k: i64 = 0
29 while a[k] != (0 as u8) { buf[p] = a[k]; p = p + 1; k = k + 1 }
30 let q: *u8 = "\"" as *u8
31 buf[p] = q[0]; p = p + 1
32 let b: *u8 = "no webgl" as *u8
33 k = 0
34 while b[k] != (0 as u8) { buf[p] = b[k]; p = p + 1; k = k + 1 }
35 let two: *u8 = "2" as *u8
36 buf[p] = two[0]; p = p + 1
37 if diagnosed == 1 {
38 let d: *u8 = " (" as *u8
39 buf[p] = d[0]; p = p + 1
40 buf[p] = d[1]; p = p + 1
41 }
42 buf[p] = q[0]; p = p + 1
43 let tail: *u8 = ";" as *u8
44 buf[p] = tail[0]; p = p + 1
45 return p
46}
47
48func gg_emitter(path: *u8, label_read: *u8, label_comp: *u8, label_bare: *u8, ctr: *i64) -> i64 {
49 let lp: *i64 = sys_mmap(16) as *i64
50 let b: *u8 = sys_read_file(path, lp)
51 var readable: i64 = 0
52 if (b as i64) != 0 { if lp[0] > 0 { readable = 1 } }
53 // gv_need: an unreadable subject is a NAMED SKIP, never a silent pass
54 if gv_need(label_read, readable, ctr) == 0 { return 0 }
55 let n: i64 = lp[0]
56 gv_check(label_comp, glp_composes(b, n) == 1, ctr)
57 gv_check(label_bare, glp_bare_count(b, n) == 0, ctr)
58 return 1
59}
60
61func main(argc: i64, argv: *i64) -> i64 {
62 gv_head("nx_glprobe_gate -- the GL-context probe ruler: one table, two surfaces, no bare refusals" as *u8)
63 let ctr: *i64 = gv_ctr()
64 gv_subjects("page emitters that acquire a WebGL2 context" as *u8, GG_EMITTERS, ctr)
65
66 // (1) the classifier separates its states
67 gv_check("gl2-granted-reads-OK" as *u8, glp_classify(1, 0, 0) == GLP_OK, ctr)
68 gv_check("gl2-granted-outranks-every-other-fact" as *u8, glp_classify(1, 1, 1) == GLP_OK, ctr)
69 gv_check("gl1-only-reads-GL1_ONLY" as *u8, glp_classify(0, 1, 0) == GLP_GL1_ONLY, ctr)
70 gv_check("gl1-outranks-gpu-when-both-present" as *u8, glp_classify(0, 1, 1) == GLP_GL1_ONLY, ctr)
71 gv_check("gpu-adapter-without-gl-reads-GPU_NO_GL" as *u8, glp_classify(0, 0, 1) == GLP_GPU_NO_GL, ctr)
72 gv_check("nothing-reads-NO_CONTEXT" as *u8, glp_classify(0, 0, 0) == GLP_NO_CONTEXT, ctr)
73 // anti-vacuity: a classifier that returns one constant passes none of the four above together, but say it
74 gv_check("neg-control-four-states-are-distinct" as *u8, (GLP_OK != GLP_GL1_ONLY) + (GLP_GL1_ONLY != GLP_GPU_NO_GL) + (GLP_GPU_NO_GL != GLP_NO_CONTEXT) + (GLP_OK != GLP_NO_CONTEXT) == 4, ctr)
75 gv_check("state-names-are-distinct-strings" as *u8, glp_find(glp_state_name(GLP_OK), 0, glp_slen(glp_state_name(GLP_OK)), glp_state_name(GLP_NO_CONTEXT)) < 0, ctr)
76
77 // (2) one table, two surfaces: every native string is carried verbatim in the emitted JS
78 let js: *u8 = glp_js()
79 let jn: i64 = glp_slen(js)
80 gv_check("js-defines-nxGlProbe" as *u8, glp_find(js, 0, jn, "function nxGlProbe(" as *u8) >= 0, ctr)
81 gv_check("js-asks-for-webgl2-first" as *u8, glp_find(js, 0, jn, "getContext(\"webgl2\"" as *u8) >= 0, ctr)
82 gv_check("js-carries-state-OK" as *u8, glp_find(js, 0, jn, glp_state_name(GLP_OK)) >= 0, ctr)
83 gv_check("js-carries-state-GL1_ONLY" as *u8, glp_find(js, 0, jn, glp_state_name(GLP_GL1_ONLY)) >= 0, ctr)
84 gv_check("js-carries-state-GPU_NO_GL" as *u8, glp_find(js, 0, jn, glp_state_name(GLP_GPU_NO_GL)) >= 0, ctr)
85 gv_check("js-carries-state-NO_CONTEXT" as *u8, glp_find(js, 0, jn, glp_state_name(GLP_NO_CONTEXT)) >= 0, ctr)
86 gv_check("js-carries-remedy-GL1_ONLY" as *u8, glp_find(js, 0, jn, glp_remedy(GLP_GL1_ONLY)) >= 0, ctr)
87 gv_check("js-carries-remedy-NO-GL" as *u8, glp_find(js, 0, jn, glp_remedy(GLP_NO_CONTEXT)) >= 0, ctr)
88 gv_check("js-publishes-window-__nx_gl" as *u8, glp_find(js, 0, jn, "window.__nx_gl={" as *u8) >= 0, ctr)
89 // (3) the poisoned-canvas guard: the probe must never claim a 2d context on the target canvas
90 gv_check("neg-control-js-never-claims-2d-on-target-canvas" as *u8, glp_find(js, 0, jn, "cv.getContext(\"2d\"" as *u8) < 0, ctr)
91 gv_check("js-probes-webgl1-on-a-fresh-canvas" as *u8, glp_find(js, 0, jn, "createElement(\"canvas\").getContext(\"webgl\")" as *u8) >= 0, ctr)
92
93 // (4) the bare-refusal detector fires on the bare form and not on the diagnosed form
94 let fx: *u8 = sys_mmap(GG_FIX_BYTES)
95 let fn1: i64 = gg_fixture(fx, 0)
96 gv_check("fixture-reached-condition-bare-form-assembled" as *u8, fn1 > 20, ctr)
97 gv_check("neg-control-detector-FIRES-on-a-bare-refusal" as *u8, glp_bare_count(fx, fn1) == 1, ctr)
98 let fy: *u8 = sys_mmap(GG_FIX_BYTES)
99 let fn2: i64 = gg_fixture(fy, 1)
100 gv_check("fixture-reached-condition-diagnosed-form-assembled" as *u8, fn2 == fn1 + 2, ctr)
101 gv_check("detector-silent-on-the-diagnosed-form" as *u8, glp_bare_count(fy, fn2) == 0, ctr)
102 gv_check("detector-silent-on-the-probe-itself" as *u8, glp_bare_count(js, jn) == 0, ctr)
103
104 // (5) every emitter composes the probe and ships zero bare refusals
105 var composed: i64 = 0
106 composed = composed + gg_emitter(GG_E1, "emitter-readable-nx_game_page_emit" as *u8, "composes-probe-nx_game_page_emit" as *u8, "zero-bare-refusals-nx_game_page_emit" as *u8, ctr)
107 composed = composed + gg_emitter(GG_E2, "emitter-readable-nx_nxa_rig_emit" as *u8, "composes-probe-nx_nxa_rig_emit" as *u8, "zero-bare-refusals-nx_nxa_rig_emit" as *u8, ctr)
108 composed = composed + gg_emitter(GG_E3, "emitter-readable-nx_nxa_view_emit" as *u8, "composes-probe-nx_nxa_view_emit" as *u8, "zero-bare-refusals-nx_nxa_view_emit" as *u8, ctr)
109 composed = composed + gg_emitter(GG_E4, "emitter-readable-nx_nxa_stream_emit" as *u8, "composes-probe-nx_nxa_stream_emit" as *u8, "zero-bare-refusals-nx_nxa_stream_emit" as *u8, ctr)
110 gv_check("every-declared-emitter-was-examined" as *u8, composed == GG_EMITTERS, ctr)
111
112 return gv_verdict("nx_glprobe_gate" as *u8, ctr, "one table two surfaces; no bare GL refusal ships from any page emitter" as *u8)
113}