nx_nofloat_propose_solve_gate.nx source
↩ module page · 210 lines · 11442 B
1// nx_nofloat_propose_solve_gate.nx -- PROPOSE->VERIFY rung 2 (2026-07-15): SOLVE-FORMS. Rung 1 proved the
2// loop on completions ("6 plus 7 equals ?" -> 12/12 kernel-certified); this rung asks the model to INVERT the
3// operation -- "what plus 3 equals 7?" -> the no-float Qwen PROPOSES the unknown x, and the LCF kernel
4// certifies the INSTANTIATED claim ("4 plus 3 equals 7") through a full Peano derivation. Wrong x cannot
5// certify (kernel soundness); the model's solve-rate is REPORTED as measured data (first measured run:
6// 1/10 -- inversion is beyond the 0.5B's 3-shot ability; every wrong proposal was kernel-CAUGHT). Teeth stay
7// model-IQ-independent:
8// T1 mechanism live: >=8/10 proposals parse as integers; zero generation or kernel failures
9// T2 soundness cross-check: kernel verdict on the instantiation == independent in-gate arithmetic (0 violations)
10// T3 NEG-CONTROL: all 10 wrong-by-one instantiations (kept IN-GRAMMAR: x+1, stepping to x-1 at the operand
11// caps plus<=12/times<=6 -- first run taught that x+1 can land UNSUPPORTED instead of REFUTED) REFUTED
12// T4 NEG-CONTROL unsolvable honesty: kernel solve-form 'what times 4 equals 13' -> NO-SOLUTION; its nearest
13// instantiations REFUTED; and the LIVE model asked '2 times what equals 9?' can NEVER certify (2x=9 has
14// no integer solution -- whatever the model proposes, the kernel must catch it)
15// T5 determinism: re-running Q1 reproduces BYTE-IDENTICAL text (greedy no-float exceed)
16// 2026-07-15 consolidation: templating/generation/parse/claim now ride nx_propose_verify_lib (single source
17// of truth shared with the organ nx_propose_verify + the completion probe) -- prompts byte-identical, so the
18// measured numbers must reproduce (that reproduction = the migration proof).
19// Requires /home/elderwesto/nx_stage/nx_real_model.gguf. Heavy: ~2-4 min. Return from main (pool reap),
20// never sys_exit. No hw writes (Rule 26). expect_exit: 0 license_tier: ORIGINAL
21import "nx_syscalls.nx"
22import "nx_propose_verify_lib.nx"
23import "nx_gate_verdict.nx"
24import "nx_stage_path.nx"
25
26func main() -> i64 {
27 af_w("=== NX-NOFLOAT-PROPOSE-SOLVE -- solve-forms: the model INVERTS, the LCF kernel certifies the instantiation ===\n" as *u8)
28 let t0: i64 = sys_now_ms()
29 let rc: i64 = nsv_init(sp_guarded("NOFLOAT-PROPOSE-SOLVE-GATE" as *u8, "nx_real_model.gguf" as *u8))
30 let t1: i64 = sys_now_ms()
31 af_w("[init] rc=" as *u8); af_n(rc); af_w(" (" as *u8); af_n(t1 - t0); af_w(" ms)\n" as *u8)
32 if rc != 0 { af_w("NX-NOFLOAT-PROPOSE-SOLVE-GATE verdict=RED (model init failed)\n" as *u8); return 1 }
33
34 // 10 solve questions: known k, target c, op (1 plus|2 times), slot (1 = unknown first, 2 = unknown second).
35 // true x = c-k (plus) or c/k (times). All inside the verifier grammar caps; none appear in the few-shot examples.
36 let qk: *i64 = sys_mmap(10 * 8) as *i64
37 let qc: *i64 = sys_mmap(10 * 8) as *i64
38 let qo: *i64 = sys_mmap(10 * 8) as *i64
39 let qs: *i64 = sys_mmap(10 * 8) as *i64
40 qk[0] = 3; qc[0] = 7; qo[0] = 1; qs[0] = 1 // what plus 3 equals 7 -> 4
41 qk[1] = 5; qc[1] = 12; qo[1] = 1; qs[1] = 1 // what plus 5 equals 12 -> 7
42 qk[2] = 2; qc[2] = 11; qo[2] = 1; qs[2] = 1 // what plus 2 equals 11 -> 9
43 qk[3] = 4; qc[3] = 9; qo[3] = 1; qs[3] = 2 // 4 plus what equals 9 -> 5
44 qk[4] = 6; qc[4] = 14; qo[4] = 1; qs[4] = 2 // 6 plus what equals 14 -> 8
45 qk[5] = 3; qc[5] = 15; qo[5] = 1; qs[5] = 2 // 3 plus what equals 15 -> 12
46 qk[6] = 4; qc[6] = 12; qo[6] = 2; qs[6] = 1 // what times 4 equals 12 -> 3
47 qk[7] = 5; qc[7] = 25; qo[7] = 2; qs[7] = 1 // what times 5 equals 25 -> 5
48 qk[8] = 3; qc[8] = 18; qo[8] = 2; qs[8] = 2 // 3 times what equals 18 -> 6
49 qk[9] = 2; qc[9] = 8; qo[9] = 2; qs[9] = 2 // 2 times what equals 8 -> 4
50
51 let pbuf: *u8 = sys_mmap(2048)
52 let tx: *u8 = sys_mmap(4096)
53 let mt: *i64 = sys_mmap(8 * 8) as *i64
54 let pres: *i64 = sys_mmap(16) as *i64
55 let cbuf: *u8 = sys_mmap(256)
56 let wbuf: *u8 = sys_mmap(256)
57 let prm: *i64 = sys_mmap(4 * 8) as *i64
58 let q0sav: *u8 = sys_mmap(4096)
59 var q0len: i64 = 0 - 1
60
61 var parseable: i64 = 0
62 var certified: i64 = 0
63 var refuted: i64 = 0
64 var unsup: i64 = 0
65 var kfail: i64 = 0
66 var genfail: i64 = 0
67 var sviol: i64 = 0
68 var t3ok: i64 = 0
69 var i: i64 = 0
70 while i < 10 {
71 let k: i64 = qk[i]
72 let c: i64 = qc[i]
73 let op: i64 = qo[i]
74 let slot: i64 = qs[i]
75 var truex: i64 = 0
76 if op == 1 { truex = c - k } else { truex = c / k }
77 let off: i64 = pvl_prompt_solve(pbuf, k, c, op, slot)
78 let l: i64 = pvl_generate(pbuf, off, tx, mt, 5)
79 af_w("\nQ" as *u8); af_n(i + 1); af_w(": " as *u8)
80 if slot == 1 { af_w("what " as *u8) } else { af_n(k); af_w(" " as *u8) }
81 if op == 1 { af_w("plus " as *u8) } else { af_w("times " as *u8) }
82 if slot == 1 { af_n(k) } else { af_w("what" as *u8) }
83 af_w(" equals " as *u8); af_n(c)
84 af_w(" (true x " as *u8); af_n(truex); af_w(", " as *u8); af_n(mt[2]); af_w(" ms) gen='" as *u8)
85 var show: i64 = l
86 if show > 40 { show = 40 }
87 if show > 0 { sys_write(1, tx, show) }
88 af_w("'\n" as *u8)
89 if l < 1 { genfail = genfail + 1 } else {
90 if i == 0 {
91 q0len = l
92 var ci: i64 = 0
93 while ci < l { q0sav[ci] = tx[ci]; ci = ci + 1 }
94 }
95 if pvl_first_uint(tx, l, pres) == 1 {
96 parseable = parseable + 1
97 let p: i64 = pres[1]
98 var wrong: i64 = 0
99 if p != truex { wrong = 1 }
100 if slot == 1 { prm[0] = p; prm[1] = k } else { prm[0] = k; prm[1] = p }
101 prm[2] = op
102 prm[3] = c
103 let cl: i64 = pvl_claim(cbuf, prm)
104 let code: i64 = af_decide(cbuf, 1)
105 if code == 1 { certified = certified + 1; if wrong == 1 { sviol = sviol + 1 } }
106 if code == 2 { refuted = refuted + 1; if wrong == 0 { sviol = sviol + 1 } }
107 if code == 3 { unsup = unsup + 1 }
108 if code < 0 { kfail = kfail + 1 }
109 }
110 }
111 // T3 per-question NEG-CONTROL: instantiate with a wrong-by-one value KEPT IN-GRAMMAR -> the kernel
112 // must REFUTE. (First run taught this: true-x+1 can exceed the verifier operand caps -- plus <=12,
113 // times <=6 -- landing UNSUPPORTED not REFUTED. Step DOWN to x-1 there: still wrong, still parseable;
114 // k+(x±1)=c±1 != c and k*(x±1)=c±k != c, so the control claim is false by construction.)
115 var wrongx: i64 = truex + 1
116 if op == 1 { if wrongx > 12 { wrongx = truex - 1 } } else { if wrongx > 6 { wrongx = truex - 1 } }
117 if slot == 1 { prm[0] = wrongx; prm[1] = k } else { prm[0] = k; prm[1] = wrongx }
118 prm[2] = op
119 prm[3] = c
120 let wl: i64 = pvl_claim(wbuf, prm)
121 if af_decide(wbuf, 0) == 2 { t3ok = t3ok + 1 }
122 i = i + 1
123 }
124
125 // T4 NEG-CONTROLS: unsolvable honesty, kernel side + LIVE model side.
126 af_w("\n[neg-controls]\n" as *u8)
127 let s1: i64 = af_decide("what times 4 equals 13" as *u8, 1) // kernel: NO-SOLUTION (5)
128 let c1: i64 = af_decide("3 times 4 equals 13" as *u8, 1) // REFUTED (2)
129 let c2: i64 = af_decide("4 times 4 equals 13" as *u8, 1) // REFUTED (2)
130 // LIVE: ask the model the unsolvable '2 times what equals 9?' -- whatever it proposes must NOT certify
131 let off9: i64 = pvl_prompt_solve(pbuf, 2, 9, 2, 2)
132 let l9: i64 = pvl_generate(pbuf, off9, tx, mt, 5)
133 var live_ok: i64 = 1
134 var live_p: i64 = 0 - 1
135 if l9 > 0 { if pvl_first_uint(tx, l9, pres) == 1 {
136 live_p = pres[1]
137 prm[0] = 2
138 prm[1] = live_p
139 prm[2] = 2
140 prm[3] = 9
141 let l9c: i64 = pvl_claim(cbuf, prm)
142 let code9: i64 = af_decide(cbuf, 1)
143 if code9 == 1 { live_ok = 0 }
144 } }
145 af_w(" live unsolvable '2 times what equals 9?' -> model proposed " as *u8)
146 if live_p >= 0 { af_n(live_p) } else { af_w("(no parse)" as *u8) }
147 af_w(" certified=" as *u8); af_n(1 - live_ok); af_w(" (must be 0)\n" as *u8)
148
149 // T5 determinism: re-run Q1 -> byte-identical generated text
150 let off5: i64 = pvl_prompt_solve(pbuf, 3, 7, 1, 1)
151 let l5: i64 = pvl_generate(pbuf, off5, tx, mt, 5)
152 var det: i64 = 0
153 if l5 > 0 { if l5 == q0len {
154 var eq: i64 = 1
155 var ei: i64 = 0
156 while ei < l5 { if tx[ei] != q0sav[ei] { eq = 0; ei = l5 } else { ei = ei + 1 } }
157 det = eq
158 } }
159
160 // ---- the MEASUREMENT + the teeth ----
161 af_w("\nMEASURED SOLVE-RATE (0.5B base, 3-shot greedy i32, inversion): parseable " as *u8); af_n(parseable)
162 af_w("/10 kernel-CERTIFIED " as *u8); af_n(certified)
163 af_w("/10 kernel-REFUTED " as *u8); af_n(refuted)
164 af_w("/10 (wrong but CAUGHT) unsupported " as *u8); af_n(unsup)
165 af_w(" genfail " as *u8); af_n(genfail)
166 af_w(" kernelfail " as *u8); af_n(kfail)
167 af_w("\n\n" as *u8)
168
169 var pass: i64 = 0
170 var ttl: i64 = 0
171 ttl = ttl + 1
172 let ok1a: i64 = (parseable >= 8) as i64
173 let ok1b: i64 = (genfail == 0) as i64
174 let ok1c: i64 = (kfail == 0) as i64
175 var ok1: i64 = ok1a & ok1b
176 ok1 = ok1 & ok1c
177 af_w(" T1 mechanism live (parseable>=8, zero gen/kernel failures): " as *u8)
178 if ok1 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
179 ttl = ttl + 1
180 let ok2: i64 = (sviol == 0) as i64
181 af_w(" T2 soundness cross-check (kernel verdict == independent arithmetic, 0 violations): " as *u8)
182 if ok2 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
183 ttl = ttl + 1
184 let ok3: i64 = (t3ok == 10) as i64
185 af_w(" T3 NEG-CONTROL all 10 wrong-by-one instantiations REFUTED: " as *u8)
186 if ok3 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL (" as *u8); af_n(t3ok); af_w("/10)\n" as *u8) }
187 ttl = ttl + 1
188 let ok4a: i64 = (s1 == 5) as i64
189 let ok4b: i64 = (c1 == 2) as i64
190 let ok4c: i64 = (c2 == 2) as i64
191 var ok4: i64 = ok4a & ok4b
192 ok4 = ok4 & ok4c
193 ok4 = ok4 & live_ok
194 af_w(" T4 NEG-CONTROL unsolvable honest (kernel NO-SOLUTION + instantiations REFUTED + live never certifies): " as *u8)
195 if ok4 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
196 ttl = ttl + 1
197 af_w(" T5 determinism: Q1 re-run byte-identical (greedy no-float): " as *u8)
198 if det == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
199
200 af_w("NX-NOFLOAT-PROPOSE-SOLVE-GATE passed " as *u8); af_n(pass); af_w("/" as *u8); af_n(ttl)
201 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
202 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
203 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
204 let ctr__dry: *i64 = gv_ctr()
205 ctr__dry[0] = pass
206 ctr__dry[1] = ttl
207 let rc__dry: i64 = gv_verdict("NOFLOAT-PROPOSE-SOLVE-GATE" as *u8, ctr__dry, "solve-forms: the model inverts, the kernel certifies the instantiation; wrong x cannot certify)" as *u8)
208 sys_exit_group(rc__dry)
209 return rc__dry
210}