code wiki / _hdl_build / nx_converge_gate.nx
nx_converge_gate.nx source
↩ module page · 169 lines · 8549 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"
24import "nx_gate_verdict.nx"
25
26func gw(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
27func gn(v: i64) -> i64 {
28 let b: *u8 = sys_mmap(28)
29 var m: i64 = v
30 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
31 let t: *u8 = sys_mmap(28)
32 var k: i64 = 0
33 if m == 0 { t[0] = (48 as u8); k = 1 }
34 while m > 0 { t[k] = ((48 + (m % 10)) as u8); m = m / 10; k = k + 1 }
35 var i: i64 = 0
36 while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
37 sys_write(1, b, k)
38 return 0
39}
40
41const G_T1_LO: i64 = 300 // sweep bounds for the convergence tooth (inside the oracle's real range)
42const G_T1_HI: i64 = 950
43const G_T1_STP: i64 = 50
44const G_TOL: i64 = 20
45
46func main() -> i64 {
47 gw("=== nx_converge_gate: does the controller actually control, and refuse instead of spin? ===\n" as *u8)
48 var pass: i64 = 0
49 var total: i64 = 0
50 let d: *i64 = sys_mmap(8)
51 let r: *i64 = sys_mmap(8)
52 let s: *i64 = sys_mmap(8)
53
54 // ---- T1 CONVERGES across the range ----
55 var t: i64 = G_T1_LO
56 var conv: i64 = 0
57 var tried: i64 = 0
58 var worst: i64 = 0
59 while t <= G_T1_HI {
60 let st: i64 = cv_run(t, G_TOL, d, r, s)
61 tried = tried + 1
62 var e: i64 = r[0] - t
63 if e < 0 { e = 0 - e }
64 if st == CV_OK { if e <= G_TOL { conv = conv + 1 } }
65 if s[0] > worst { worst = s[0] }
66 t = t + G_T1_STP
67 }
68 total = total + 1
69 if conv == tried { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
70 gw("T1 CONVERGES: " as *u8); gn(conv); gw("/" as *u8); gn(tried)
71 gw(" targets landed inside tol=" as *u8); gn(G_TOL); gw("\n" as *u8)
72
73 // ---- T2 BOUNDED COST ----
74 total = total + 1
75 if worst <= CV_MAX_STEPS { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
76 gw("T2 BOUNDED COST: worst-case renders=" as *u8); gn(worst)
77 gw(" (budget " as *u8); gn(CV_MAX_STEPS); gw("); each render is 25-50s of GPU\n" as *u8)
78
79 // ---- T3 REFUSES FREE ----
80 let st3: i64 = cv_run(1200, G_TOL, d, r, s)
81 total = total + 1
82 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) }
83 gw("T3 REFUSES FREE: target=1200 -> UNREACHABLE at renders=" as *u8); gn(s[0]); gw(" (must be 0)\n" as *u8)
84
85 // ---- T4 EARLY EXIT: first probe is denoise 500 -> oracle 697; target it with a wide tol ----
86 let first_ret: i64 = cv_oracle(cv_first_probe())
87 let st4: i64 = cv_run(first_ret, G_TOL, d, r, s)
88 total = total + 1
89 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) }
90 gw("T4 EARLY EXIT: target=" as *u8); gn(first_ret)
91 gw(" (= what probe 1 yields) -> renders=" as *u8); gn(s[0]); gw(" (must be exactly 1)\n" as *u8)
92
93 // ---- T5 BRACKET SANITY: walk a full search checking every proposal ----
94 var lo: i64 = CV_MIN
95 var hi: i64 = CV_MAX
96 var probe: i64 = cv_first_probe()
97 var steps: i64 = 0
98 let st: *i64 = sys_mmap(8)
99 let nlo: *i64 = sys_mmap(8)
100 let nhi: *i64 = sys_mmap(8)
101 st[0] = CV_CONTINUE
102 var sane: i64 = 1
103 while st[0] == CV_CONTINUE {
104 if probe < CV_MIN { sane = 0 }
105 if probe > CV_MAX { sane = 0 }
106 let m: i64 = cv_oracle(probe)
107 steps = steps + 1
108 let nxt: i64 = cv_step(500, 5, lo, hi, probe, m, steps, st, nlo, nhi)
109 if nlo[0] > nhi[0] { sane = 0 }
110 lo = nlo[0]
111 hi = nhi[0]
112 if nxt != CV_DONE { probe = nxt }
113 }
114 total = total + 1
115 if sane == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
116 gw("T5 BRACKET SANITY: every probe within [" as *u8); gn(CV_MIN); gw("," as *u8); gn(CV_MAX)
117 gw("] and bracket never inverted over " as *u8); gn(steps); gw(" steps\n" as *u8)
118
119 // ---- T6 DIRECTION (the inversion) ----
120 let a_lo: *i64 = sys_mmap(8)
121 let a_hi: *i64 = sys_mmap(8)
122 let a_st: *i64 = sys_mmap(8)
123 // measured ABOVE target -> kept too much -> floor must RISE to the probe
124 cv_step(500, 5, 0, 1000, 400, 800, 1, a_st, a_lo, a_hi)
125 let up_ok: i64 = a_lo[0]
126 // measured BELOW target -> kept too little -> ceiling must FALL to the probe
127 cv_step(500, 5, 0, 1000, 600, 300, 1, a_st, a_lo, a_hi)
128 let dn_ok: i64 = a_hi[0]
129 total = total + 1
130 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) }
131 gw("T6 DIRECTION: measured>target raises floor to " as *u8); gn(up_ok)
132 gw(" (want 400); measured<target lowers ceiling to " as *u8); gn(dn_ok); gw(" (want 600)\n" as *u8)
133
134 // ---- T7 DETERMINISM ----
135 let d2: *i64 = sys_mmap(8)
136 let r2: *i64 = sys_mmap(8)
137 let s2: *i64 = sys_mmap(8)
138 cv_run(640, G_TOL, d, r, s)
139 cv_run(640, G_TOL, d2, r2, s2)
140 total = total + 1
141 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) }
142 gw("T7 DETERMINISM: two runs agree (denoise=" as *u8); gn(d[0])
143 gw(" retention=" as *u8); gn(r[0]); gw(" renders=" as *u8); gn(s[0]); gw(")\n" as *u8)
144
145 // ---- T8 ORACLE MONOTONE (else the whole guarantee is vacuous) ----
146 var prev: i64 = cv_oracle(CV_MIN)
147 var mono: i64 = 1
148 var x: i64 = CV_MIN
149 while x <= CV_MAX {
150 let v: i64 = cv_oracle(x)
151 if v > prev { mono = 0 }
152 prev = v
153 x = x + 10
154 }
155 total = total + 1
156 if mono == 1 { pass = pass + 1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) }
157 gw("T8 ORACLE MONOTONE: retention never rises as denoise rises (bisection's precondition holds)\n" as *u8)
158
159 gw("\n=== nx_converge_gate " as *u8); gn(pass); gw("/" as *u8); gn(total)
160 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
161 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
162 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
163 let ctr__dry: *i64 = gv_ctr()
164 ctr__dry[0] = pass
165 ctr__dry[1] = total
166 let rc__dry: i64 = gv_verdict("CONVERGE-GATE" as *u8, ctr__dry, "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 " as *u8)
167 sys_exit(rc__dry)
168 return rc__dry
169}