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