nx_texm_ship_gate.nx source
↩ module page · 166 lines · 8158 B
1// nx_texm_ship_gate.nx -- THE GATE FOR THE DERIVED SHIP RESOLUTION.
2//
3// SUBJECT: the nx_nxa_texm ELF, ship mode, forked for real. tex_res_floor stays the MEASURED bar;
4// ship mode DERIVES the largest power-of-two rung whose measured bytes*cast_size fit a declared
5// texture budget, and REFUSES when the budget is unsourced/absent or nothing fits. This gate
6// proves the derivation RESPONDS to its inputs (budget and cast size) and abstains when it cannot
7// decide -- never silently defaulting.
8//
9// EVERY BUDGET FIXTURE IS WRITTEN AT RUNTIME under /tmp/nx_texm_ship_gate/ and passed to the
10// organ via its conf-path OVERRIDE (4th arg), so the gate never mutates the tracked production
11// budget conf -- a gate that shares a fixture with a production conf reports on the fixture. The
12// override arg exists precisely so this test is clean.
13//
14// ALL FIXTURES SELECT 512 OR REFUSE, ON PURPOSE: a 512 bake is fast and a refusal skips the bake
15// entirely, so the gate finishes inside any caller deadline. A budget that selected 2048/4096
16// would derive correctly but bake slowly -- correctness is proven by the 512 case plus the
17// discrimination pairs, not by paying for a large bake.
18//
19// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
20import "nx_syscalls.nx"
21import "nx_gate_verdict.nx"
22import "nx_tool_run.nx"
23
24const SG_SUBJECT_DEFAULT: *u8 = "/volume1/homes/elderwesto/nishihost/_offc/nx_nxa_texm.elf"
25// a real TEXC-bearing input, needed only by the one derive-and-bake tooth; refusals never read it
26const SG_INPUT: *u8 = "/volume1/homes/elderwesto/nishihost/sites/nishifamily/world/ref9d.nxa"
27
28// nx_nxa_texm exit contract, restated so a change to it breaks this gate loudly
29const SG_TXM_OK: i64 = 0
30const SG_TXM_BAD: i64 = 3
31
32const SG_CAPCAP: i64 = 262144
33const SG_ARGVN: i64 = 8
34const SG_MODEDIR: i64 = 493
35const SG_ARGV_BYTES: i64 = 64
36
37const SG_DIR: *u8 = "/tmp/nx_texm_ship_gate"
38const SG_OUT: *u8 = "/tmp/nx_texm_ship_gate/o.nxa"
39const SG_FIT512: *u8 = "/tmp/nx_texm_ship_gate/fit512.conf"
40const SG_TIGHT: *u8 = "/tmp/nx_texm_ship_gate/tight.conf"
41const SG_BIGCAST: *u8 = "/tmp/nx_texm_ship_gate/bigcast.conf"
42const SG_UNSRC: *u8 = "/tmp/nx_texm_ship_gate/unsourced.conf"
43
44// measured ladder rows shared by every fixture. budget=2000000/cast=12 admits 512 (148080*12=
45// 1776960) but not 1024 (846904*12=10162848). budget=1000000 admits nothing (below 512's cost).
46// budget=2000000/cast=100 admits nothing (512 costs 148080*100=14808000). UNSOURCED refuses.
47const SG_FIT512_C: *u8 = "res_bytes_512 148080\nres_bytes_1024 846904\nres_bytes_2048 5774640\nres_bytes_4096 31563984\ncast_size 12\ntexture_budget_bytes 2000000\n"
48const SG_TIGHT_C: *u8 = "res_bytes_512 148080\nres_bytes_1024 846904\nres_bytes_2048 5774640\nres_bytes_4096 31563984\ncast_size 12\ntexture_budget_bytes 1000000\n"
49const SG_BIGCAST_C: *u8 = "res_bytes_512 148080\nres_bytes_1024 846904\nres_bytes_2048 5774640\nres_bytes_4096 31563984\ncast_size 100\ntexture_budget_bytes 2000000\n"
50const SG_UNSRC_C: *u8 = "res_bytes_512 148080\nres_bytes_1024 846904\nres_bytes_2048 5774640\nres_bytes_4096 31563984\ncast_size 12\ntexture_budget_bytes UNSOURCED\n"
51
52const SG_SHIP: *u8 = "ship"
53
54func sg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
55
56func sg_write(path: *u8, content: *u8) -> i64 {
57 let n: i64 = sg_slen(content)
58 let fd: i64 = sys_openat_wr(path, MODE_0644)
59 if fd < 0 { return 0 - 1 }
60 let wr: i64 = sys_write(fd, content, n)
61 sys_close(fd)
62 if wr != n { return 0 - 1 }
63 return n
64}
65func sg_exists(path: *u8) -> i64 {
66 let lp: *i64 = sys_mmap(16) as *i64
67 let b: *u8 = sys_read_file(path, lp)
68 if (b as i64) == 0 { return 0 }
69 if lp[0] <= 0 { return 0 }
70 return 1
71}
72// fork the subject in ship mode with an override budget conf; returns child exit code
73func sg_ship(subject: *u8, budgetconf: *u8, out: *u8, olen: *i64) -> i64 {
74 let av: *i64 = sys_mmap(SG_ARGV_BYTES) as *i64
75 av[0] = subject as i64
76 av[1] = SG_INPUT as i64
77 av[2] = out as i64
78 av[3] = SG_SHIP as i64
79 av[4] = budgetconf as i64
80 av[5] = 0
81 let cap: *u8 = sys_mmap(SG_CAPCAP)
82 return tr_run_capture(subject, av, cap, SG_CAPCAP, olen)
83}
84
85
86func main(argc: i64, argv: *i64) -> i64 {
87 let ctr: *i64 = gv_ctr()
88 gv_head("nx_texm_ship gate -- the ship resolution is DERIVED from a budget, and it responds to its inputs" as *u8)
89 var subject: *u8 = SG_SUBJECT_DEFAULT
90 if argc >= 2 { subject = argv[1] as *u8 }
91 gv_puts(" subject: " as *u8)
92 gv_puts(subject)
93 gv_puts("\n\n" as *u8)
94
95 // ---- SETUP: scratch, remove prior output, write the four budget fixtures ----
96 sys_mkdir(SG_DIR, SG_MODEDIR)
97 sys_unlinkat(SG_OUT)
98 sg_write(SG_FIT512, SG_FIT512_C)
99 sg_write(SG_TIGHT, SG_TIGHT_C)
100 sg_write(SG_BIGCAST, SG_BIGCAST_C)
101 sg_write(SG_UNSRC, SG_UNSRC_C)
102 // ANTI-VACUITY: assert the fixtures reached the condition (exist, non-empty) AND the prior
103 // output is gone, before asserting any outcome. A gate that measured against absent fixtures
104 // would report on nothing.
105 var setup: i64 = 0
106 if sg_exists(SG_FIT512) == 1 { if sg_exists(SG_TIGHT) == 1 { if sg_exists(SG_BIGCAST) == 1 { if sg_exists(SG_UNSRC) == 1 { if sg_exists(SG_OUT) == 0 { setup = 1 } } } } }
107 gv_check("setup-four-budget-fixtures-written-and-output-cleared (idempotent, anti-vacuity)" as *u8, setup, ctr)
108
109 let olen: *i64 = sys_mmap(16) as *i64
110
111 // ---- T1: an ADEQUATE budget derives (and bakes at the derived 512) ----
112 let rc_fit: i64 = sg_ship(subject, SG_FIT512, SG_OUT, olen)
113 gv_puts(" [T1] fit512 budget rc=" as *u8)
114 gv_num(rc_fit)
115 gv_puts("\n" as *u8)
116 var t1: i64 = 0
117 if rc_fit == SG_TXM_OK { t1 = 1 }
118 gv_check("adequate-budget-derives-a-rung-and-bakes (exit OK)" as *u8, t1, ctr)
119
120 // ---- T2: a TIGHTER budget (below the smallest rung's cost) fits NOTHING and REFUSES ----
121 let rc_tight: i64 = sg_ship(subject, SG_TIGHT, SG_OUT, olen)
122 gv_puts(" [T2] tight budget rc=" as *u8)
123 gv_num(rc_tight)
124 gv_puts("\n" as *u8)
125 var t2: i64 = 0
126 if rc_tight == SG_TXM_BAD { t2 = 1 }
127 gv_check("budget-below-the-smallest-rung-refuses (no silent default)" as *u8, t2, ctr)
128
129 // ---- bite(T1,T2): the derivation RESPONDS to the budget -- adequate derives, tight refuses.
130 var b_bad: i64 = 0
131 if rc_tight == SG_TXM_BAD { b_bad = 1 }
132 var b_good: i64 = 1
133 if rc_fit == SG_TXM_OK { b_good = 0 }
134 gv_bite("neg-control-tight-budget-refuses-and-adequate-budget-derives" as *u8, b_bad, b_good, ctr)
135
136 // ---- T3: raising CAST_SIZE at the same budget moves the outcome (derive -> refuse). This is
137 // the 'change the cast size, watch ship_res move' tooth: the derivation reads cast_size, not
138 // just the budget.
139 let rc_cast: i64 = sg_ship(subject, SG_BIGCAST, SG_OUT, olen)
140 gv_puts(" [T3] same budget, cast_size 12->100 rc=" as *u8)
141 gv_num(rc_cast)
142 gv_puts("\n" as *u8)
143 var t3: i64 = 0
144 if rc_cast == SG_TXM_BAD { t3 = 1 }
145 gv_check("raising-cast_size-moves-the-outcome (ship_res responds to cast, not budget alone)" as *u8, t3, ctr)
146
147 // ---- T4: an UNSOURCED budget refuses -- the whole point of the file, and its production state.
148 let rc_uns: i64 = sg_ship(subject, SG_UNSRC, SG_OUT, olen)
149 gv_puts(" [T4] unsourced budget rc=" as *u8)
150 gv_num(rc_uns)
151 gv_puts("\n" as *u8)
152 var t4: i64 = 0
153 if rc_uns == SG_TXM_BAD { t4 = 1 }
154 gv_check("unsourced-budget-refuses (never derive against a budget nobody set)" as *u8, t4, ctr)
155
156 // ---- T5: the subject actually RAN. A negative sentinel or 127 would make every exit-code
157 // tooth above compare against a number the subject never produced.
158 var ran: i64 = 1
159 if rc_fit < 0 { ran = 0 }
160 if rc_fit == 127 { ran = 0 }
161 gv_check("neg-control-subject-actually-executed (not 127, not a harness sentinel)" as *u8, ran, ctr)
162
163 let rc: i64 = gv_verdict("TEXM-SHIP" as *u8, ctr, "ship resolution is derived from a measured ladder and a budget, and responds to both budget and cast size" as *u8)
164 sys_exit(rc)
165 return rc
166}