nx_propose_verify.nx source
↩ module page · 198 lines · 10135 B
1// nx_propose_verify.nx -- ORGAN: the PROPOSE->VERIFY capability as a reusable CLI (2026-07-15). The
2// sovereign no-float Qwen PROPOSES an answer; the LCF-kernel autoformalization verifier CERTIFIES or
3// REFUTES it -- nothing unverified is ever trusted (the autonomous-building safety primitive, now an organ).
4// Accepted question forms (space-tokenized; digits or number-words zero..twelve):
5// solve-form : "what plus 3 equals 7" / "3 plus what equals 7" (also times; x works for what)
6// completion form: "6 plus 7 equals what" (model proposes the result)
7// full claim : "2 plus 2 equals 4" (pass-through: kernel verdict only, no model, no init cost)
8// Modes: argv[1] = one question (argv[2] = optional gguf path); no-arg = self-battery (expect_exit 0).
9// Exit codes: 0 CERTIFIED · 2 REFUTED · 3 UNSUPPORTED · 5 NO-PROPOSAL · 1 infra failure.
10// Battery teeth are model-IQ-INDEPENDENT: proposals parse + verdicts SOUND (kernel == independent
11// arithmetic), the unsolvable question never certifies, pass-through true/false/garbage honest.
12// Requires the gguf only for model routes. Return from main (pool reap), never sys_exit. No hw writes
13// (Rule 26). expect_exit: 0 license_tier: ORIGINAL
14import "nx_syscalls.nx"
15import "nx_propose_verify_lib.nx"
16
17// write s[0,min(n,cap)) to stdout
18func pvx_show(s: *u8, n: i64, cap: i64) -> i64 {
19 var m: i64 = n
20 if m > cap { m = cap }
21 if m > 0 { sys_write(1, s, m) }
22 return 0
23}
24
25// copy src minus its LAST space-separated token into body (trailing space kept), the last token into last.
26// Returns 1 if src had >= 2 tokens.
27func pvx_strip_last(src: *u8, body: *u8, last: *u8) -> i64 {
28 var n: i64 = 0
29 while src[n] != (0 as u8) { n = n + 1 }
30 while n > 0 { if src[n - 1] == (32 as u8) { n = n - 1 } else { break } }
31 if n == 0 { return 0 }
32 var ts: i64 = n
33 while ts > 0 { if src[ts - 1] != (32 as u8) { ts = ts - 1 } else { break } }
34 if ts == 0 { return 0 }
35 var i: i64 = 0
36 while i < ts { body[i] = src[i]; i = i + 1 }
37 body[ts] = 0 as u8
38 var j: i64 = 0
39 while ts + j < n { last[j] = src[ts + j]; j = j + 1 }
40 last[j] = 0 as u8
41 return 1
42}
43
44// route a question: 1 = solve-form (unknown in a/b slot) · 2 = completion form ("a op b equals what") ·
45// 3 = full concrete claim (pass-through) · 0 = unsupported. res receives the af_parse result
46// (for route 2: the parse of the question with the trailing what/x replaced by 0, so a/op/b are real).
47func pvx_route(q: *u8, res: *i64) -> i64 {
48 if af_parse(q, res) == 1 {
49 if res[5] != 0 { return 1 }
50 return 3
51 }
52 let body: *u8 = sys_mmap(512)
53 let last: *u8 = sys_mmap(64)
54 if pvx_strip_last(q, body, last) != 1 { return 0 }
55 var isw: i64 = 0
56 if af_streq(last, "what" as *u8) == 1 { isw = 1 }
57 if af_streq(last, "x" as *u8) == 1 { isw = 1 }
58 if isw == 0 { return 0 }
59 let tmpq: *u8 = sys_mmap(600)
60 var o: i64 = 0
61 o = nsv_cat(tmpq, o, body)
62 o = nsv_cat(tmpq, o, "0" as *u8)
63 if af_parse(tmpq, res) != 1 { return 0 }
64 if res[5] != 0 { return 0 }
65 if res[3] != 1 { return 0 }
66 if res[1] == 0 { return 0 }
67 return 2
68}
69
70// run ONE question end-to-end (caller must nsv_init first for model routes). out = [proposal_found,
71// proposal_value, route]. Returns the kernel verdict on the (instantiated) claim: 1 PROVED / 2 REFUTED /
72// 3 UNSUPPORTED / 6 NO-PROPOSAL / -1 kernel failure.
73func pvx_case(q: *u8, out: *i64) -> i64 {
74 let res: *i64 = sys_mmap(48) as *i64
75 let route: i64 = pvx_route(q, res)
76 out[0] = 0
77 out[1] = 0 - 1
78 out[2] = route
79 if route == 0 {
80 af_w(" [UNSUPPORTED] " as *u8); af_w(q); af_w(" (not a claim, solve-form, or completion question)\n" as *u8)
81 return 3
82 }
83 if route == 3 { return af_decide(q, 1) }
84 let pb: *u8 = sys_mmap(2048)
85 let tx: *u8 = sys_mmap(4096)
86 let mt: *i64 = sys_mmap(8 * 8) as *i64
87 let pres: *i64 = sys_mmap(16) as *i64
88 var plen: i64 = 0
89 var kslot: i64 = 0
90 var kknown: i64 = 0
91 if route == 1 {
92 if res[5] == 1 { kslot = 1; kknown = res[2] } else { kslot = 2; kknown = res[0] }
93 plen = pvl_prompt_solve(pb, kknown, res[4], res[1], kslot)
94 } else {
95 plen = pvl_prompt_complete(pb, res[0], res[2], res[1])
96 }
97 let l: i64 = pvl_generate(pb, plen, tx, mt, 5)
98 if l < 1 {
99 af_w(" [NO-PROPOSAL] " as *u8); af_w(q); af_w(" (generation failed)\n" as *u8)
100 return 6
101 }
102 if pvl_first_uint(tx, l, pres) != 1 {
103 af_w(" [NO-PROPOSAL] " as *u8); af_w(q); af_w(" (no integer in gen='" as *u8); pvx_show(tx, l, 40); af_w("')\n" as *u8)
104 return 6
105 }
106 out[0] = 1
107 let p: i64 = pres[1]
108 out[1] = p
109 af_w(" [PROPOSED ] " as *u8); af_w(q); af_w(" -> " as *u8); af_n(p)
110 af_w(" (model " as *u8); af_n(mt[2]); af_w(" ms, gen='" as *u8); pvx_show(tx, l, 24); af_w("')\n" as *u8)
111 let prm: *i64 = sys_mmap(4 * 8) as *i64
112 let cbuf: *u8 = sys_mmap(256)
113 if route == 1 {
114 if kslot == 1 { prm[0] = p; prm[1] = kknown } else { prm[0] = kknown; prm[1] = p }
115 prm[2] = res[1]
116 prm[3] = res[4]
117 } else {
118 prm[0] = res[0]
119 prm[1] = res[2]
120 prm[2] = res[1]
121 prm[3] = p
122 }
123 let cl: i64 = pvl_claim(cbuf, prm)
124 return af_decide(cbuf, 1)
125}
126
127func main(argc: i64, argv: *i64) -> i64 {
128 var mpath: *u8 = "/home/elderwesto/nx_stage/nx_real_model.gguf" as *u8
129 if argc >= 3 { mpath = argv[2] as *u8 }
130 if argc >= 2 {
131 let q: *u8 = argv[1] as *u8
132 let res: *i64 = sys_mmap(48) as *i64
133 let route: i64 = pvx_route(q, res)
134 if route == 1 { let rc: i64 = nsv_init(mpath); if rc != 0 { af_w("[init] model init failed\n" as *u8); return 1 } }
135 if route == 2 { let rc2: i64 = nsv_init(mpath); if rc2 != 0 { af_w("[init] model init failed\n" as *u8); return 1 } }
136 let out: *i64 = sys_mmap(3 * 8) as *i64
137 let code: i64 = pvx_case(q, out)
138 af_w("VERDICT: " as *u8)
139 if code == 1 { af_w("CERTIFIED (kernel-checked derivation)\n" as *u8); return 0 }
140 if code == 2 { af_w("REFUTED (wrong -- caught by the kernel)\n" as *u8); return 2 }
141 if code == 3 { af_w("UNSUPPORTED\n" as *u8); return 3 }
142 if code == 6 { af_w("NO-PROPOSAL\n" as *u8); return 5 }
143 af_w("KERNEL-FAILURE\n" as *u8)
144 return 1
145 }
146 // ---- no-arg self-battery (model-IQ-independent teeth) ----
147 af_w("=== NX-PROPOSE-VERIFY organ battery -- model proposes, LCF kernel disposes ===\n" as *u8)
148 let t0: i64 = sys_now_ms()
149 let rc: i64 = nsv_init(mpath)
150 let t1: i64 = sys_now_ms()
151 af_w("[init] rc=" as *u8); af_n(rc); af_w(" (" as *u8); af_n(t1 - t0); af_w(" ms)\n" as *u8)
152 if rc != 0 { af_w("NX-PROPOSE-VERIFY verdict=RED (model init failed)\n" as *u8); return 1 }
153 let o1: *i64 = sys_mmap(3 * 8) as *i64
154 let o2: *i64 = sys_mmap(3 * 8) as *i64
155 let o3: *i64 = sys_mmap(3 * 8) as *i64
156 let o4: *i64 = sys_mmap(3 * 8) as *i64
157 let o5: *i64 = sys_mmap(3 * 8) as *i64
158 // B1 completion form: the model proposes the RESULT
159 let c1: i64 = pvx_case("6 plus 7 equals what" as *u8, o1)
160 // B2/B3 solve-forms, both unknown slots: the model INVERTS
161 let c2: i64 = pvx_case("what plus 3 equals 7" as *u8, o2)
162 let c3: i64 = pvx_case("3 times what equals 18" as *u8, o3)
163 // B4 LIVE unsolvable: whatever the model proposes, the kernel must not certify (2x=9 has no integer x)
164 let c4: i64 = pvx_case("2 times what equals 9" as *u8, o4)
165 // B5/B6/B7 pass-through: true claim / false claim / out-of-grammar (kernel-only, deterministic)
166 let c5: i64 = pvx_case("2 plus 2 equals 4" as *u8, o5)
167 let c6: i64 = pvx_case("2 plus 2 equals 5" as *u8, o5)
168 let c7: i64 = pvx_case("the moon is made of cheese" as *u8, o5)
169 // soundness: certified IFF the proposal equals the independently computed answer
170 var s1: i64 = 0
171 if o1[0] == 1 { if ((c1 == 1) as i64) == ((o1[1] == 13) as i64) { s1 = 1 } }
172 var s2: i64 = 0
173 if o2[0] == 1 { if ((c2 == 1) as i64) == ((o2[1] == 4) as i64) { s2 = 1 } }
174 var s3: i64 = 0
175 if o3[0] == 1 { if ((c3 == 1) as i64) == ((o3[1] == 6) as i64) { s3 = 1 } }
176 let s4: i64 = (c4 != 1) as i64
177 let s5: i64 = (c5 == 1) as i64
178 let s6: i64 = (c6 == 2) as i64
179 let s7: i64 = (c7 == 3) as i64
180 var cert: i64 = 0
181 if c1 == 1 { cert = cert + 1 }
182 if c2 == 1 { cert = cert + 1 }
183 if c3 == 1 { cert = cert + 1 }
184 af_w("\n data: certified " as *u8); af_n(cert); af_w("/3 solvable questions (model quality, reported not gated)\n" as *u8)
185 var pass: i64 = 0
186 var ttl: i64 = 0
187 ttl = ttl + 1; af_w(" B1 completion-form proposal parsed + verdict SOUND: " as *u8); if s1 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
188 ttl = ttl + 1; af_w(" B2 solve-form (unknown first) parsed + SOUND: " as *u8); if s2 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
189 ttl = ttl + 1; af_w(" B3 solve-form (unknown second, times) parsed + SOUND: " as *u8); if s3 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
190 ttl = ttl + 1; af_w(" B4 NEG-CONTROL live unsolvable never certifies: " as *u8); if s4 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
191 ttl = ttl + 1; af_w(" B5 pass-through true claim CERTIFIED: " as *u8); if s5 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
192 ttl = ttl + 1; af_w(" B6 NEG-CONTROL pass-through false claim REFUTED: " as *u8); if s6 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
193 ttl = ttl + 1; af_w(" B7 out-of-grammar honest UNSUPPORTED: " as *u8); if s7 == 1 { pass = pass + 1; af_w("PASS\n" as *u8) } else { af_w("FAIL\n" as *u8) }
194 af_w("NX-PROPOSE-VERIFY passed " as *u8); af_n(pass); af_w("/" as *u8); af_n(ttl)
195 if pass == ttl { af_w(" verdict=GREEN (the propose->verify organ: proposals verified, wrongs caught, honesty intact)\n" as *u8); return 0 }
196 af_w(" verdict=RED\n" as *u8)
197 return 1
198}