code wiki / _hdl_build / nx_converge_gate.nx
nx_converge_gate.nx source
↩ module page · 167 lines · 8270 B
1// nx_converge_gate.nx -- proves the convergence controller actually CONTROLS, and refuses rather than
2// spins. It imports the same lib the shipping tool imports, so it grades the code that ships.
3//
4// T1 CONVERGES : lands inside tolerance on targets across the whole reachable range.
5// T2 BOUNDED COST : never exceeds the declared render budget. The budget is the PRODUCT CLAIM --
6// every step is 25-50s of GPU, so an unbounded search is a broken product even
7// if it eventually converges.
8// T3 REFUSES FREE : an unreachable target costs ZERO renders. Refusing after burning a render is
9// not refusing.
10// T4 EARLY EXIT : a first probe already inside tolerance stops immediately (1 render, not a
11// full bisection) -- proves it does not do fixed work regardless of input.
12// T5 BRACKET SANITY : every proposed probe stays inside [CV_MIN,CV_MAX] and the bracket never
13// inverts. A controller that proposes denoise 1300 would silently clamp at the
14// engine and report a wrong cause.
15// T6 DIRECTION : the inversion is correct -- measuring ABOVE target must raise the floor
16// (more denoise), measuring BELOW must lower the ceiling. Getting this
17// backwards still terminates, so only a direction tooth catches it.
18// T7 DETERMINISM : identical inputs produce an identical trajectory (replayable evidence).
19// T8 ORACLE MONOTONE : the grounded oracle is genuinely decreasing across the range -- if it were
20// not, T1 would be proving convergence against a shape the real problem does
21// not have, and the guarantee would be vacuous.
22// expect_exit: 0 license_tier: ORIGINAL
23import "nx_converge_lib.nx"
24
25func gw(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
26func gn(v: i64) -> i64 {
27 let b: *u8 = sys_mmap(28)
28 var m: i64 = v
29 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
30 let t: *u8 = sys_mmap(28)
31 var k: i64 = 0
32 if m == 0 { t[0] = (48 as u8); k = 1 }
33 while m > 0 { t[k] = ((48 + (m % 10)) as u8); m = m / 10; k = k + 1 }
34 var i: i64 = 0
35 while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
36 sys_write(1, b, k)
37 return 0
38}
39
40const G_T1_LO: i64 = 300 // sweep bounds for the convergence tooth (inside the oracle's real range)
41const G_T1_HI: i64 = 950
42const G_T1_STP: i64 = 50
43const G_TOL: i64 = 20
44
45func main() -> i64 {
46 gw("=== nx_converge_gate: does the controller actually control, and refuse instead of spin? ===\n" as *u8)
47 var pass: i64 = 0
48 var total: i64 = 0
49 let d: *i64 = sys_mmap(8)
50 let r: *i64 = sys_mmap(8)
51 let s: *i64 = sys_mmap(8)
52
53 // ---- T1 CONVERGES across the range ----
54 var t: i64 = G_T1_LO
55 var conv: i64 = 0
56 var tried: i64 = 0
57 var worst: i64 = 0
58 while t <= G_T1_HI {
59 let st: i64 = cv_run(t, G_TOL, d, r, s)
60 tried = tried + 1
61 var e: i64 = r[0] - t
62 if e < 0 { e = 0 - e }
63 if st == CV_OK { if e <= G_TOL { conv = conv + 1 } }
64 if s[0] > worst { worst = s[0] }
65 t = t + G_T1_STP
66 }
67 total = total + 1
68 if conv == tried { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
69 gw("T1 CONVERGES: " as *u8); gn(conv); gw("/" as *u8); gn(tried)
70 gw(" targets landed inside tol=" as *u8); gn(G_TOL); gw("\n" as *u8)
71
72 // ---- T2 BOUNDED COST ----
73 total = total + 1
74 if worst <= CV_MAX_STEPS { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
75 gw("T2 BOUNDED COST: worst-case renders=" as *u8); gn(worst)
76 gw(" (budget " as *u8); gn(CV_MAX_STEPS); gw("); each render is 25-50s of GPU\n" as *u8)
77
78 // ---- T3 REFUSES FREE ----
79 let st3: i64 = cv_run(1200, G_TOL, d, r, s)
80 total = total + 1
81 if st3 == CV_UNREACHABLE { if s[0] == 0 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) }
82 gw("T3 REFUSES FREE: target=1200 -> UNREACHABLE at renders=" as *u8); gn(s[0]); gw(" (must be 0)\n" as *u8)
83
84 // ---- T4 EARLY EXIT: first probe is denoise 500 -> oracle 697; target it with a wide tol ----
85 let first_ret: i64 = cv_oracle(cv_first_probe())
86 let st4: i64 = cv_run(first_ret, G_TOL, d, r, s)
87 total = total + 1
88 if st4 == CV_OK { if s[0] == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) }
89 gw("T4 EARLY EXIT: target=" as *u8); gn(first_ret)
90 gw(" (= what probe 1 yields) -> renders=" as *u8); gn(s[0]); gw(" (must be exactly 1)\n" as *u8)
91
92 // ---- T5 BRACKET SANITY: walk a full search checking every proposal ----
93 var lo: i64 = CV_MIN
94 var hi: i64 = CV_MAX
95 var probe: i64 = cv_first_probe()
96 var steps: i64 = 0
97 let st: *i64 = sys_mmap(8)
98 let nlo: *i64 = sys_mmap(8)
99 let nhi: *i64 = sys_mmap(8)
100 st[0] = CV_CONTINUE
101 var sane: i64 = 1
102 while st[0] == CV_CONTINUE {
103 if probe < CV_MIN { sane = 0 }
104 if probe > CV_MAX { sane = 0 }
105 let m: i64 = cv_oracle(probe)
106 steps = steps + 1
107 let nxt: i64 = cv_step(500, 5, lo, hi, probe, m, steps, st, nlo, nhi)
108 if nlo[0] > nhi[0] { sane = 0 }
109 lo = nlo[0]
110 hi = nhi[0]
111 if nxt != CV_DONE { probe = nxt }
112 }
113 total = total + 1
114 if sane == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
115 gw("T5 BRACKET SANITY: every probe within [" as *u8); gn(CV_MIN); gw("," as *u8); gn(CV_MAX)
116 gw("] and bracket never inverted over " as *u8); gn(steps); gw(" steps\n" as *u8)
117
118 // ---- T6 DIRECTION (the inversion) ----
119 let a_lo: *i64 = sys_mmap(8)
120 let a_hi: *i64 = sys_mmap(8)
121 let a_st: *i64 = sys_mmap(8)
122 // measured ABOVE target -> kept too much -> floor must RISE to the probe
123 cv_step(500, 5, 0, 1000, 400, 800, 1, a_st, a_lo, a_hi)
124 let up_ok: i64 = a_lo[0]
125 // measured BELOW target -> kept too little -> ceiling must FALL to the probe
126 cv_step(500, 5, 0, 1000, 600, 300, 1, a_st, a_lo, a_hi)
127 let dn_ok: i64 = a_hi[0]
128 total = total + 1
129 if up_ok == 400 { if dn_ok == 600 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) }
130 gw("T6 DIRECTION: measured>target raises floor to " as *u8); gn(up_ok)
131 gw(" (want 400); measured<target lowers ceiling to " as *u8); gn(dn_ok); gw(" (want 600)\n" as *u8)
132
133 // ---- T7 DETERMINISM ----
134 let d2: *i64 = sys_mmap(8)
135 let r2: *i64 = sys_mmap(8)
136 let s2: *i64 = sys_mmap(8)
137 cv_run(640, G_TOL, d, r, s)
138 cv_run(640, G_TOL, d2, r2, s2)
139 total = total + 1
140 if d[0] == d2[0] { if r[0] == r2[0] { if s[0] == s2[0] { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) }
141 gw("T7 DETERMINISM: two runs agree (denoise=" as *u8); gn(d[0])
142 gw(" retention=" as *u8); gn(r[0]); gw(" renders=" as *u8); gn(s[0]); gw(")\n" as *u8)
143
144 // ---- T8 ORACLE MONOTONE (else the whole guarantee is vacuous) ----
145 var prev: i64 = cv_oracle(CV_MIN)
146 var mono: i64 = 1
147 var x: i64 = CV_MIN
148 while x <= CV_MAX {
149 let v: i64 = cv_oracle(x)
150 if v > prev { mono = 0 }
151 prev = v
152 x = x + 10
153 }
154 total = total + 1
155 if mono == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
156 gw("T8 ORACLE MONOTONE: retention never rises as denoise rises (bisection's precondition holds)\n" as *u8)
157
158 gw("\n=== nx_converge_gate " as *u8); gn(pass); gw("/" as *u8); gn(total)
159 if pass == total {
160 gw(" verdict=GREEN -- the controller lands on target across the range, inside a declared render budget, refuses impossible targets for free, exits early when it is already there, keeps a sane bracket, inverts in the right direction, replays identically, and its precondition (monotonicity) is proven rather than assumed.\n" as *u8)
161 sys_exit(0)
162 return 0
163 }
164 gw(" verdict=RED\n" as *u8)
165 sys_exit(1)
166 return 1
167}