nx_nofloat_propose_chat_gate.nx source
↩ module page · 205 lines · 10650 B
1// nx_nofloat_propose_chat_gate.nx -- PROPOSE->VERIFY rung 3 (2026-07-15): a BETTER PROPOSER on the SAME
2// RULER. The raw 3-shot completion proposer measured solve-rate 1/10 on the 10-question inversion ruler
3// (nx_nofloat_propose_solve_gate -- the model pattern-copies instead of inverting). This gate asks the SAME
4// 10 questions through the serve's CHATML path (gp[12]=1: <|im_start|>user ... <|im_start|>assistant -- the
5// instruct-tuned surface, natural-language question + answer-format instruction) and measures whether the
6// prompting MODE alone moves the solve-rate. Same kernel, same questions, same teeth => the delta is the
7// prompting mode's, honestly. Teeth stay model-IQ-independent (the RATE is data, not a tooth):
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 (in-grammar: x+1, stepping to x-1 at the operand caps) REFUTED
11// T4 NEG-CONTROL: the LIVE unsolvable chat question ('2 times what number equals 9?') can NEVER certify
12// T5 determinism: re-running Q1 reproduces BYTE-IDENTICAL text (greedy no-float exceed, chat path included)
13// INSTRUMENT v2 (2026-07-15, after the 1.5B first-light): max_new 8->24 (EOS-complete -- chattier models
14// were TRUNCATED mid-sentence: 'The number is 7 - 3' cut before the result) + LAST-integer extraction
15// (pvl_last_uint -- the answer position in sentence replies; first-int grabbed operands). Applied uniformly
16// to every model on this instrument; v1 numbers (0.5B 3/10, first-int, max_new=8) stay banked as v1.
17// argv[1] = optional gguf path. Requires the gguf. Heavy: ~2-8 min (model-size dependent). Return from
18// main (pool reap), never sys_exit. No hw writes (Rule 26). expect_exit: 0 license_tier: ORIGINAL
19import "nx_syscalls.nx"
20import "nx_propose_verify_lib.nx"
21import "nx_gate_verdict.nx"
22
23func main(argc: i64, argv: *i64) -> i64 {
24 af_w("=== NX-NOFLOAT-PROPOSE-CHAT -- the SAME solve ruler, ChatML proposer (baseline raw 3-shot = 1/10) ===\n" as *u8)
25 // argv[1] = optional gguf path (default = the 0.5B seat) -- the SAME ruler measures ANY model the
26 // arch-config serve core can load (the 1.5B-on-the-ruler rung rides this).
27 var mpath: *u8 = "/home/elderwesto/nx_stage/nx_real_model.gguf" as *u8
28 if argc >= 2 { mpath = argv[1] as *u8 }
29 // argv[2] = max_new override (diagnostic: isolates whether the generation budget can EVER change early
30 // tokens -- under greedy it must not; a cross-binary divergence showed up 07-15 and this is the probe).
31 var mnew: i64 = 24
32 if argc >= 3 {
33 let ms: *u8 = argv[2] as *u8
34 var mi: i64 = 0
35 var mv: i64 = 0
36 while ms[mi] != (0 as u8) { let mc: i64 = ms[mi] as i64; if mc >= 48 { if mc <= 57 { mv = mv * 10 + (mc - 48) } } mi = mi + 1 }
37 if mv >= 1 { mnew = mv }
38 }
39 af_w("[model] " as *u8); af_w(mpath); af_w("\n" as *u8)
40 let t0: i64 = sys_now_ms()
41 let rc: i64 = nsv_init(mpath)
42 let t1: i64 = sys_now_ms()
43 af_w("[init] rc=" as *u8); af_n(rc); af_w(" (" as *u8); af_n(t1 - t0); af_w(" ms)\n" as *u8)
44 if rc != 0 { af_w("NX-NOFLOAT-PROPOSE-CHAT-GATE verdict=RED (model init failed)\n" as *u8); return 1 }
45
46 // THE RULER: the identical 10 solve questions from nx_nofloat_propose_solve_gate.
47 let qk: *i64 = sys_mmap(10 * 8) as *i64
48 let qc: *i64 = sys_mmap(10 * 8) as *i64
49 let qo: *i64 = sys_mmap(10 * 8) as *i64
50 let qs: *i64 = sys_mmap(10 * 8) as *i64
51 qk[0] = 3; qc[0] = 7; qo[0] = 1; qs[0] = 1
52 qk[1] = 5; qc[1] = 12; qo[1] = 1; qs[1] = 1
53 qk[2] = 2; qc[2] = 11; qo[2] = 1; qs[2] = 1
54 qk[3] = 4; qc[3] = 9; qo[3] = 1; qs[3] = 2
55 qk[4] = 6; qc[4] = 14; qo[4] = 1; qs[4] = 2
56 qk[5] = 3; qc[5] = 15; qo[5] = 1; qs[5] = 2
57 qk[6] = 4; qc[6] = 12; qo[6] = 2; qs[6] = 1
58 qk[7] = 5; qc[7] = 25; qo[7] = 2; qs[7] = 1
59 qk[8] = 3; qc[8] = 18; qo[8] = 2; qs[8] = 2
60 qk[9] = 2; qc[9] = 8; qo[9] = 2; qs[9] = 2
61
62 let pbuf: *u8 = sys_mmap(2048)
63 let tx: *u8 = sys_mmap(4096)
64 let mt: *i64 = sys_mmap(8 * 8) as *i64
65 let pres: *i64 = sys_mmap(16) as *i64
66 let cbuf: *u8 = sys_mmap(256)
67 let wbuf: *u8 = sys_mmap(256)
68 let prm: *i64 = sys_mmap(4 * 8) as *i64
69 let q0sav: *u8 = sys_mmap(4096)
70 var q0len: i64 = 0 - 1
71
72 var parseable: i64 = 0
73 var certified: i64 = 0
74 var refuted: i64 = 0
75 var unsup: i64 = 0
76 var kfail: i64 = 0
77 var genfail: i64 = 0
78 var sviol: i64 = 0
79 var t3ok: i64 = 0
80 var i: i64 = 0
81 while i < 10 {
82 let k: i64 = qk[i]
83 let c: i64 = qc[i]
84 let op: i64 = qo[i]
85 let slot: i64 = qs[i]
86 var truex: i64 = 0
87 if op == 1 { truex = c - k } else { truex = c / k }
88 let off: i64 = pvl_prompt_solve_chat(pbuf, k, c, op, slot)
89 let l: i64 = pvl_generate_chat(pbuf, off, tx, mt, mnew)
90 af_w("\nQ" as *u8); af_n(i + 1); af_w(": '" as *u8)
91 sys_write(1, pbuf, off)
92 af_w("' (true x " as *u8); af_n(truex); af_w(", " as *u8); af_n(mt[2]); af_w(" ms) gen='" as *u8)
93 var show: i64 = l
94 if show > 40 { show = 40 }
95 if show > 0 { sys_write(1, tx, show) }
96 af_w("'\n" as *u8)
97 if l < 1 { genfail = genfail + 1 } else {
98 if i == 0 {
99 q0len = l
100 var ci: i64 = 0
101 while ci < l { q0sav[ci] = tx[ci]; ci = ci + 1 }
102 }
103 if pvl_last_uint(tx, l, pres) == 1 {
104 parseable = parseable + 1
105 let p: i64 = pres[1]
106 var wrong: i64 = 0
107 if p != truex { wrong = 1 }
108 if slot == 1 { prm[0] = p; prm[1] = k } else { prm[0] = k; prm[1] = p }
109 prm[2] = op
110 prm[3] = c
111 let cl: i64 = pvl_claim(cbuf, prm)
112 let code: i64 = af_decide(cbuf, 1)
113 if code == 1 { certified = certified + 1; if wrong == 1 { sviol = sviol + 1 } }
114 if code == 2 { refuted = refuted + 1; if wrong == 0 { sviol = sviol + 1 } }
115 if code == 3 { unsup = unsup + 1 }
116 if code < 0 { kfail = kfail + 1 }
117 }
118 }
119 // T3 per-question NEG-CONTROL: wrong-by-one, kept in-grammar (x+1 -> x-1 at the operand caps)
120 var wrongx: i64 = truex + 1
121 if op == 1 { if wrongx > 12 { wrongx = truex - 1 } } else { if wrongx > 6 { wrongx = truex - 1 } }
122 if slot == 1 { prm[0] = wrongx; prm[1] = k } else { prm[0] = k; prm[1] = wrongx }
123 prm[2] = op
124 prm[3] = c
125 let wl: i64 = pvl_claim(wbuf, prm)
126 if af_decide(wbuf, 0) == 2 { t3ok = t3ok + 1 }
127 i = i + 1
128 }
129
130 // T4 NEG-CONTROL: LIVE unsolvable through the chat path -- whatever the model proposes must NOT certify
131 af_w("\n[neg-controls]\n" as *u8)
132 let off9: i64 = pvl_prompt_solve_chat(pbuf, 2, 9, 2, 2)
133 let l9: i64 = pvl_generate_chat(pbuf, off9, tx, mt, mnew)
134 var live_ok: i64 = 1
135 var live_p: i64 = 0 - 1
136 if l9 > 0 { if pvl_last_uint(tx, l9, pres) == 1 {
137 live_p = pres[1]
138 prm[0] = 2
139 prm[1] = live_p
140 prm[2] = 2
141 prm[3] = 9
142 let l9c: i64 = pvl_claim(cbuf, prm)
143 let code9: i64 = af_decide(cbuf, 1)
144 if code9 == 1 { live_ok = 0 }
145 } }
146 af_w(" live unsolvable '2 times what number equals 9?' -> model proposed " as *u8)
147 if live_p >= 0 { af_n(live_p) } else { af_w("(no parse)" as *u8) }
148 af_w(" certified=" as *u8); af_n(1 - live_ok); af_w(" (must be 0)\n" as *u8)
149
150 // T5 determinism: re-run Q1 -> byte-identical generated text
151 let off5: i64 = pvl_prompt_solve_chat(pbuf, 3, 7, 1, 1)
152 let l5: i64 = pvl_generate_chat(pbuf, off5, tx, mt, mnew)
153 var det: i64 = 0
154 if l5 > 0 { if l5 == q0len {
155 var eq: i64 = 1
156 var ei: i64 = 0
157 while ei < l5 { if tx[ei] != q0sav[ei] { eq = 0; ei = l5 } else { ei = ei + 1 } }
158 det = eq
159 } }
160
161 // ---- the MEASUREMENT (vs the raw baseline) + the teeth ----
162 af_w("\nMEASURED SOLVE-RATE (CHATML v2 greedy i32, EOS-complete + last-int, same ruler): parseable " as *u8); af_n(parseable)
163 af_w("/10 kernel-CERTIFIED " as *u8); af_n(certified)
164 af_w("/10 kernel-REFUTED " as *u8); af_n(refuted)
165 af_w("/10 (wrong but CAUGHT) unsupported " as *u8); af_n(unsup)
166 af_w(" genfail " as *u8); af_n(genfail)
167 af_w(" kernelfail " as *u8); af_n(kfail)
168 af_w("\n BASELINES same ruler: 0.5B raw 3-shot 1/10 ยท 0.5B chat-v1 (first-int, max_new 8) 3/10\n\n" as *u8)
169
170 var pass: i64 = 0
171 var ttl: i64 = 0
172 ttl = ttl + 1
173 let ok1a: i64 = (parseable >= 8) as i64
174 let ok1b: i64 = (genfail == 0) as i64
175 let ok1c: i64 = (kfail == 0) as i64
176 var ok1: i64 = ok1a & ok1b
177 ok1 = ok1 & ok1c
178 af_w(" T1 mechanism live (parseable>=8, zero gen/kernel failures): " as *u8)
179 if ok1 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
180 ttl = ttl + 1
181 let ok2: i64 = (sviol == 0) as i64
182 af_w(" T2 soundness cross-check (kernel verdict == independent arithmetic, 0 violations): " as *u8)
183 if ok2 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
184 ttl = ttl + 1
185 let ok3: i64 = (t3ok == 10) as i64
186 af_w(" T3 NEG-CONTROL all 10 wrong-by-one instantiations REFUTED: " as *u8)
187 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) }
188 ttl = ttl + 1
189 af_w(" T4 NEG-CONTROL live unsolvable never certifies (chat path): " as *u8)
190 if live_ok == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
191 ttl = ttl + 1
192 af_w(" T5 determinism: Q1 re-run byte-identical (greedy no-float, chat path): " as *u8)
193 if det == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
194
195 af_w("NX-NOFLOAT-PROPOSE-CHAT-GATE passed " as *u8); af_n(pass); af_w("/" as *u8); af_n(ttl)
196 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
197 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
198 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
199 let ctr__dry: *i64 = gv_ctr()
200 ctr__dry[0] = pass
201 ctr__dry[1] = ttl
202 let rc__dry: i64 = gv_verdict("NOFLOAT-PROPOSE-CHAT-GATE" as *u8, ctr__dry, "same ruler, chat proposer: the rate is the data; wrong proposals still cannot certify)" as *u8)
203 sys_exit(rc__dry)
204 return rc__dry
205}