nx_nofloat_propose_verify_gate.nx source
↩ module page · 180 lines · 8934 B
1// nx_nofloat_propose_verify_gate.nx -- THE PROPOSE->VERIFY LOOP, rung 1 (2026-07-15). The sovereign no-float
2// Qwen2.5-0.5B PROPOSES arithmetic answers (greedy i32 few-shot completion through the SERVE core -- the exact
3// production generator behind /gen); the LCF-kernel autoformalization verifier CERTIFIES or REFUTES every
4// proposal (af_decide -- a wrong proposal CANNOT certify, soundness by construction). This is the
5// autonomous-building safety primitive: generator proposes, sound checker disposes, nothing unverified is
6// trusted. The generator's propose-rate is REPORTED as measured data; the gate's TEETH are the mechanism
7// invariants, which do not depend on model IQ:
8// T1 mechanism live: >=8/12 proposals parse as integers; zero generation or kernel failures
9// T2 soundness cross-check: kernel verdict == independent in-gate arithmetic on EVERY parsed proposal
10// (certified-and-wrong = 0 AND refuted-and-correct = 0)
11// T3 NEG-CONTROL: all 12 deliberately-wrong proposals (truth+1) REFUTED by the kernel
12// T4 NEG-CONTROL: corrupted-proposer outputs (word token / out-of-range number) land UNSUPPORTED, never certified
13// T5 determinism: re-running Q1 reproduces BYTE-IDENTICAL text (greedy no-float exceed)
14// 2026-07-15 consolidation: templating/generation/parse/claim now ride nx_propose_verify_lib (single source
15// of truth shared with the organ nx_propose_verify + the solve probe) -- prompts byte-identical to the
16// original inline version, so the measured 12/12 must reproduce (that reproduction = the migration proof).
17// Requires /home/elderwesto/nx_stage/nx_real_model.gguf. Heavy: ~2-3 min. Return from main (pool reap),
18// 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() -> i64 {
25 af_w("=== NX-NOFLOAT-PROPOSE-VERIFY -- the no-float Qwen PROPOSES, the LCF kernel DISPOSES ===\n" as *u8)
26 let t0: i64 = sys_now_ms()
27 let rc: i64 = nsv_init(sp_guarded("NOFLOAT-PROPOSE-VERIFY-GATE" as *u8, "nx_real_model.gguf" as *u8))
28 let t1: i64 = sys_now_ms()
29 af_w("[init] rc=" as *u8); af_n(rc); af_w(" (" as *u8); af_n(t1 - t0); af_w(" ms: model + caches)\n" as *u8)
30 if rc != 0 { af_w("NX-NOFLOAT-PROPOSE-VERIFY-GATE verdict=RED (model init failed)\n" as *u8); return 1 }
31
32 // the 12 questions (verifier grammar caps: plus operands <=12, times <=6; none appear in the few-shot examples)
33 let qa: *i64 = sys_mmap(12 * 8) as *i64
34 let qb: *i64 = sys_mmap(12 * 8) as *i64
35 let qo: *i64 = sys_mmap(12 * 8) as *i64
36 qa[0] = 2; qb[0] = 3; qo[0] = 1
37 qa[1] = 7; qb[1] = 5; qo[1] = 1
38 qa[2] = 4; qb[2] = 4; qo[2] = 1
39 qa[3] = 9; qb[3] = 3; qo[3] = 1
40 qa[4] = 6; qb[4] = 7; qo[4] = 1
41 qa[5] = 8; qb[5] = 4; qo[5] = 1
42 qa[6] = 12; qb[6] = 11; qo[6] = 1
43 qa[7] = 5; qb[7] = 9; qo[7] = 1
44 qa[8] = 3; qb[8] = 4; qo[8] = 2
45 qa[9] = 2; qb[9] = 6; qo[9] = 2
46 qa[10] = 5; qb[10] = 5; qo[10] = 2
47 qa[11] = 6; qb[11] = 6; qo[11] = 2
48
49 let pbuf: *u8 = sys_mmap(2048)
50 let tx: *u8 = sys_mmap(4096)
51 let mt: *i64 = sys_mmap(8 * 8) as *i64
52 let pres: *i64 = sys_mmap(16) as *i64
53 let cbuf: *u8 = sys_mmap(256)
54 let wbuf: *u8 = sys_mmap(256)
55 let prm: *i64 = sys_mmap(4 * 8) as *i64
56 let q0sav: *u8 = sys_mmap(4096)
57 var q0len: i64 = 0 - 1
58
59 var parseable: i64 = 0
60 var certified: i64 = 0
61 var refuted: i64 = 0
62 var unsup: i64 = 0
63 var kfail: i64 = 0
64 var genfail: i64 = 0
65 var sviol: i64 = 0
66 var t3ok: i64 = 0
67 var i: i64 = 0
68 while i < 12 {
69 let a: i64 = qa[i]
70 let b: i64 = qb[i]
71 let op: i64 = qo[i]
72 var truth: i64 = 0
73 if op == 1 { truth = a + b } else { truth = a * b }
74 let off: i64 = pvl_prompt_complete(pbuf, a, b, op)
75 let l: i64 = pvl_generate(pbuf, off, tx, mt, 5)
76 af_w("\nQ" as *u8); af_n(i + 1); af_w(": " as *u8); af_n(a)
77 if op == 1 { af_w(" plus " as *u8) } else { af_w(" times " as *u8) }
78 af_n(b); af_w(" (truth " as *u8); af_n(truth); af_w(", " as *u8); af_n(mt[2]); af_w(" ms) gen='" as *u8)
79 var show: i64 = l
80 if show > 40 { show = 40 }
81 if show > 0 { sys_write(1, tx, show) }
82 af_w("'\n" as *u8)
83 if l < 1 { genfail = genfail + 1 } else {
84 if i == 0 {
85 q0len = l
86 var ci: i64 = 0
87 while ci < l { q0sav[ci] = tx[ci]; ci = ci + 1 }
88 }
89 if pvl_first_uint(tx, l, pres) == 1 {
90 parseable = parseable + 1
91 let p: i64 = pres[1]
92 var wrong: i64 = 0
93 if p != truth { wrong = 1 }
94 prm[0] = a
95 prm[1] = b
96 prm[2] = op
97 prm[3] = p
98 let cl: i64 = pvl_claim(cbuf, prm)
99 let code: i64 = af_decide(cbuf, 1)
100 if code == 1 { certified = certified + 1; if wrong == 1 { sviol = sviol + 1 } }
101 if code == 2 { refuted = refuted + 1; if wrong == 0 { sviol = sviol + 1 } }
102 if code == 3 { unsup = unsup + 1 }
103 if code < 0 { kfail = kfail + 1 }
104 }
105 }
106 // T3 per-question NEG-CONTROL: the wrong-by-one proposal must be REFUTED by the kernel
107 prm[0] = a
108 prm[1] = b
109 prm[2] = op
110 prm[3] = truth + 1
111 let wl: i64 = pvl_claim(wbuf, prm)
112 if af_decide(wbuf, 0) == 2 { t3ok = t3ok + 1 }
113 i = i + 1
114 }
115
116 // T4 NEG-CONTROLS: corrupted-proposer shapes -- a word where the number goes, and an out-of-range
117 // number -- must land UNSUPPORTED (honest refusal), never certified.
118 af_w("\n[neg-controls]\n" as *u8)
119 let g1: i64 = af_decide("7 plus 4 equals banana" as *u8, 1)
120 let g2: i64 = af_decide("7 plus 4 equals 999999" as *u8, 1)
121
122 // T5 determinism: re-run Q1 (same prompt, greedy) -> byte-identical generated text
123 let off5: i64 = pvl_prompt_complete(pbuf, 2, 3, 1)
124 let l5: i64 = pvl_generate(pbuf, off5, tx, mt, 5)
125 var det: i64 = 0
126 if l5 > 0 { if l5 == q0len {
127 var eq: i64 = 1
128 var ei: i64 = 0
129 while ei < l5 { if tx[ei] != q0sav[ei] { eq = 0; ei = l5 } else { ei = ei + 1 } }
130 det = eq
131 } }
132
133 // ---- the MEASUREMENT (data, honestly reported) + the teeth ----
134 af_w("\nMEASURED PROPOSE-RATE (0.5B base, 3-shot greedy i32): parseable " as *u8); af_n(parseable)
135 af_w("/12 kernel-CERTIFIED " as *u8); af_n(certified)
136 af_w("/12 kernel-REFUTED " as *u8); af_n(refuted)
137 af_w("/12 (wrong but CAUGHT) unsupported " as *u8); af_n(unsup)
138 af_w(" genfail " as *u8); af_n(genfail)
139 af_w(" kernelfail " as *u8); af_n(kfail)
140 af_w("\n\n" as *u8)
141
142 var pass: i64 = 0
143 var ttl: i64 = 0
144 ttl = ttl + 1
145 let ok1a: i64 = (parseable >= 8) as i64
146 let ok1b: i64 = (genfail == 0) as i64
147 let ok1c: i64 = (kfail == 0) as i64
148 var ok1: i64 = ok1a & ok1b
149 ok1 = ok1 & ok1c
150 af_w(" T1 mechanism live (parseable>=8, zero gen/kernel failures): " as *u8)
151 if ok1 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
152 ttl = ttl + 1
153 let ok2: i64 = (sviol == 0) as i64
154 af_w(" T2 soundness cross-check (kernel verdict == independent arithmetic, 0 violations): " as *u8)
155 if ok2 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
156 ttl = ttl + 1
157 let ok3: i64 = (t3ok == 12) as i64
158 af_w(" T3 NEG-CONTROL all 12 wrong-by-one proposals REFUTED: " as *u8)
159 if ok3 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL (" as *u8); af_n(t3ok); af_w("/12)\n" as *u8) }
160 ttl = ttl + 1
161 let ok4a: i64 = (g1 == 3) as i64
162 let ok4b: i64 = (g2 == 3) as i64
163 let ok4: i64 = ok4a & ok4b
164 af_w(" T4 NEG-CONTROL garbage proposals UNSUPPORTED (never certified): " as *u8)
165 if ok4 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
166 ttl = ttl + 1
167 af_w(" T5 determinism: Q1 re-run byte-identical (greedy no-float): " as *u8)
168 if det == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
169
170 af_w("NX-NOFLOAT-PROPOSE-VERIFY-GATE passed " as *u8); af_n(pass); af_w("/" as *u8); af_n(ttl)
171 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
172 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
173 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
174 let ctr__dry: *i64 = gv_ctr()
175 ctr__dry[0] = pass
176 ctr__dry[1] = ttl
177 let rc__dry: i64 = gv_verdict("NOFLOAT-PROPOSE-VERIFY-GATE" as *u8, ctr__dry, "propose->verify loop sound: the model proposes, the kernel disposes, wrong proposals cannot certify)" as *u8)
178 sys_exit_group(rc__dry)
179 return rc__dry
180}