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