nx_nofloat_propose_verify_gate.nx source
↩ module page · 179 lines · 8878 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"
22
23func main() -> i64 {
24 af_w("=== NX-NOFLOAT-PROPOSE-VERIFY -- the no-float Qwen PROPOSES, the LCF kernel DISPOSES ===\n" as *u8)
25 let t0: i64 = sys_now_ms()
26 let rc: i64 = nsv_init("/home/elderwesto/nx_stage/nx_real_model.gguf" as *u8)
27 let t1: i64 = sys_now_ms()
28 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)
29 if rc != 0 { af_w("NX-NOFLOAT-PROPOSE-VERIFY-GATE verdict=RED (model init failed)\n" as *u8); return 1 }
30
31 // the 12 questions (verifier grammar caps: plus operands <=12, times <=6; none appear in the few-shot examples)
32 let qa: *i64 = sys_mmap(12 * 8) as *i64
33 let qb: *i64 = sys_mmap(12 * 8) as *i64
34 let qo: *i64 = sys_mmap(12 * 8) as *i64
35 qa[0] = 2; qb[0] = 3; qo[0] = 1
36 qa[1] = 7; qb[1] = 5; qo[1] = 1
37 qa[2] = 4; qb[2] = 4; qo[2] = 1
38 qa[3] = 9; qb[3] = 3; qo[3] = 1
39 qa[4] = 6; qb[4] = 7; qo[4] = 1
40 qa[5] = 8; qb[5] = 4; qo[5] = 1
41 qa[6] = 12; qb[6] = 11; qo[6] = 1
42 qa[7] = 5; qb[7] = 9; qo[7] = 1
43 qa[8] = 3; qb[8] = 4; qo[8] = 2
44 qa[9] = 2; qb[9] = 6; qo[9] = 2
45 qa[10] = 5; qb[10] = 5; qo[10] = 2
46 qa[11] = 6; qb[11] = 6; qo[11] = 2
47
48 let pbuf: *u8 = sys_mmap(2048)
49 let tx: *u8 = sys_mmap(4096)
50 let mt: *i64 = sys_mmap(8 * 8) as *i64
51 let pres: *i64 = sys_mmap(16) as *i64
52 let cbuf: *u8 = sys_mmap(256)
53 let wbuf: *u8 = sys_mmap(256)
54 let prm: *i64 = sys_mmap(4 * 8) as *i64
55 let q0sav: *u8 = sys_mmap(4096)
56 var q0len: i64 = 0 - 1
57
58 var parseable: i64 = 0
59 var certified: i64 = 0
60 var refuted: i64 = 0
61 var unsup: i64 = 0
62 var kfail: i64 = 0
63 var genfail: i64 = 0
64 var sviol: i64 = 0
65 var t3ok: i64 = 0
66 var i: i64 = 0
67 while i < 12 {
68 let a: i64 = qa[i]
69 let b: i64 = qb[i]
70 let op: i64 = qo[i]
71 var truth: i64 = 0
72 if op == 1 { truth = a + b } else { truth = a * b }
73 let off: i64 = pvl_prompt_complete(pbuf, a, b, op)
74 let l: i64 = pvl_generate(pbuf, off, tx, mt, 5)
75 af_w("\nQ" as *u8); af_n(i + 1); af_w(": " as *u8); af_n(a)
76 if op == 1 { af_w(" plus " as *u8) } else { af_w(" times " as *u8) }
77 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)
78 var show: i64 = l
79 if show > 40 { show = 40 }
80 if show > 0 { sys_write(1, tx, show) }
81 af_w("'\n" as *u8)
82 if l < 1 { genfail = genfail + 1 } else {
83 if i == 0 {
84 q0len = l
85 var ci: i64 = 0
86 while ci < l { q0sav[ci] = tx[ci]; ci = ci + 1 }
87 }
88 if pvl_first_uint(tx, l, pres) == 1 {
89 parseable = parseable + 1
90 let p: i64 = pres[1]
91 var wrong: i64 = 0
92 if p != truth { wrong = 1 }
93 prm[0] = a
94 prm[1] = b
95 prm[2] = op
96 prm[3] = p
97 let cl: i64 = pvl_claim(cbuf, prm)
98 let code: i64 = af_decide(cbuf, 1)
99 if code == 1 { certified = certified + 1; if wrong == 1 { sviol = sviol + 1 } }
100 if code == 2 { refuted = refuted + 1; if wrong == 0 { sviol = sviol + 1 } }
101 if code == 3 { unsup = unsup + 1 }
102 if code < 0 { kfail = kfail + 1 }
103 }
104 }
105 // T3 per-question NEG-CONTROL: the wrong-by-one proposal must be REFUTED by the kernel
106 prm[0] = a
107 prm[1] = b
108 prm[2] = op
109 prm[3] = truth + 1
110 let wl: i64 = pvl_claim(wbuf, prm)
111 if af_decide(wbuf, 0) == 2 { t3ok = t3ok + 1 }
112 i = i + 1
113 }
114
115 // T4 NEG-CONTROLS: corrupted-proposer shapes -- a word where the number goes, and an out-of-range
116 // number -- must land UNSUPPORTED (honest refusal), never certified.
117 af_w("\n[neg-controls]\n" as *u8)
118 let g1: i64 = af_decide("7 plus 4 equals banana" as *u8, 1)
119 let g2: i64 = af_decide("7 plus 4 equals 999999" as *u8, 1)
120
121 // T5 determinism: re-run Q1 (same prompt, greedy) -> byte-identical generated text
122 let off5: i64 = pvl_prompt_complete(pbuf, 2, 3, 1)
123 let l5: i64 = pvl_generate(pbuf, off5, tx, mt, 5)
124 var det: i64 = 0
125 if l5 > 0 { if l5 == q0len {
126 var eq: i64 = 1
127 var ei: i64 = 0
128 while ei < l5 { if tx[ei] != q0sav[ei] { eq = 0; ei = l5 } else { ei = ei + 1 } }
129 det = eq
130 } }
131
132 // ---- the MEASUREMENT (data, honestly reported) + the teeth ----
133 af_w("\nMEASURED PROPOSE-RATE (0.5B base, 3-shot greedy i32): parseable " as *u8); af_n(parseable)
134 af_w("/12 kernel-CERTIFIED " as *u8); af_n(certified)
135 af_w("/12 kernel-REFUTED " as *u8); af_n(refuted)
136 af_w("/12 (wrong but CAUGHT) unsupported " as *u8); af_n(unsup)
137 af_w(" genfail " as *u8); af_n(genfail)
138 af_w(" kernelfail " as *u8); af_n(kfail)
139 af_w("\n\n" as *u8)
140
141 var pass: i64 = 0
142 var ttl: i64 = 0
143 ttl = ttl + 1
144 let ok1a: i64 = (parseable >= 8) as i64
145 let ok1b: i64 = (genfail == 0) as i64
146 let ok1c: i64 = (kfail == 0) as i64
147 var ok1: i64 = ok1a & ok1b
148 ok1 = ok1 & ok1c
149 af_w(" T1 mechanism live (parseable>=8, zero gen/kernel failures): " as *u8)
150 if ok1 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
151 ttl = ttl + 1
152 let ok2: i64 = (sviol == 0) as i64
153 af_w(" T2 soundness cross-check (kernel verdict == independent arithmetic, 0 violations): " as *u8)
154 if ok2 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
155 ttl = ttl + 1
156 let ok3: i64 = (t3ok == 12) as i64
157 af_w(" T3 NEG-CONTROL all 12 wrong-by-one proposals REFUTED: " as *u8)
158 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) }
159 ttl = ttl + 1
160 let ok4a: i64 = (g1 == 3) as i64
161 let ok4b: i64 = (g2 == 3) as i64
162 let ok4: i64 = ok4a & ok4b
163 af_w(" T4 NEG-CONTROL garbage proposals UNSUPPORTED (never certified): " as *u8)
164 if ok4 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
165 ttl = ttl + 1
166 af_w(" T5 determinism: Q1 re-run byte-identical (greedy no-float): " as *u8)
167 if det == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
168
169 af_w("NX-NOFLOAT-PROPOSE-VERIFY-GATE passed " as *u8); af_n(pass); af_w("/" as *u8); af_n(ttl)
170 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
171 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
172 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
173 let ctr__dry: *i64 = gv_ctr()
174 ctr__dry[0] = pass
175 ctr__dry[1] = ttl
176 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)
177 sys_exit(rc__dry)
178 return rc__dry
179}