nx_loop.nx source
↩ module page · 350 lines · 13053 B
1// nx_loop.nx -- bounded-loop discipline primitive.
2//
3// Per docs/LOOP_DESIGN_RESEARCH.md. Provides the sealed verdict
4// enum + settle helper for the substrate's canonical bounded-loop
5// pattern. Replaces ad-hoc `keep == 1` sentinel-flag style with a
6// structured verdict that distinguishes:
7//
8// NX_LOOP_RUNNING -- loop is still active
9// NX_LOOP_DONE_SUCCESS -- ran to budget, body never asked to
10// stop -- the loop did its full job
11// NX_LOOP_DONE_EXIT -- body asked to exit early (success)
12// NX_LOOP_BUDGET_EXHAUSTED -- budget hit before body finished
13// NX_LOOP_ABORTED -- body asked to abort (hard error)
14//
15// Inspired by NASA JPL Power of 10 Rule 2 (Holzmann 2006: all loops
16// must have a fixed upper bound) + Why3 loop-variants + Idris totality
17// checking. Without a parser-level `bounded` keyword (queued for
18// self-host), this module lets substrate code follow the same
19// DISCIPLINE today with no compiler change.
20//
21// ===== Canonical loop pattern =====
22//
23// import "nx_loop.nx"
24//
25// let MAX_ITERS: nx_int = 1024
26// var iter: nx_int = 0
27// var verdict: nx_int = NX_LOOP_RUNNING
28// while verdict == NX_LOOP_RUNNING && iter < MAX_ITERS {
29// // body here, may set verdict via constants below
30// if early_success_cond { verdict = NX_LOOP_DONE_EXIT }
31// if hard_error_cond { verdict = NX_LOOP_ABORTED }
32// iter = iter + 1
33// }
34// verdict = nx_loop_settle(verdict, iter, MAX_ITERS)
35// // verdict is now one of {DONE_SUCCESS, DONE_EXIT,
36// // BUDGET_EXHAUSTED, ABORTED}
37//
38// Properties (the four-pillar discipline this primitive enforces):
39// DETECT -- verdict tells you exactly why the loop ended
40// PREVENT -- MAX_ITERS in the loop header makes infinite loops
41// structurally impossible (JPL Rule 2)
42// DIAGNOSE -- BUDGET_EXHAUSTED vs DONE_SUCCESS distinguishes
43// "couldn't finish" from "didn't need early exit"
44// REPAIR -- caller can branch on verdict to retry, escalate,
45// or log per the situation
46//
47// genealogy_id: nasa_jpl_power_of_10_rule_2_holzmann_2006 +
48// hoare_1969_axiomatic_basis +
49// why3_loop_variants_filliatre_2013 +
50// idris_totality_brady_2013
51// lineage_id: substrate_loop_discipline_v1
52
53// nx_safety_envelope:
54// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
55// sil_target: SIL1
56// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
57// verdict: NOT_YET_EVALUATED
58
59import "nx_tier.nx"
60import "nx_syscalls.nx"
61import "nx_clock.nx"
62
63// ===== Sealed-enum: LoopVerdict ===================================
64
65const NX_LOOP_RUNNING: nx_int = 0
66const NX_LOOP_DONE_SUCCESS: nx_int = 1
67const NX_LOOP_DONE_EXIT: nx_int = 2
68const NX_LOOP_BUDGET_EXHAUSTED: nx_int = 3
69const NX_LOOP_ABORTED: nx_int = 4
70const NX_LOOP_N_VERDICTS: nx_int = 5
71
72func nx_loop_verdict_is_valid(v: nx_int) -> nx_int {
73 if v < 0 { return 0 }
74 if v >= NX_LOOP_N_VERDICTS { return 0 }
75 return 1
76}
77
78// ===== Verdict predicates =========================================
79//
80// Convenience: callers should check "did the loop succeed" without
81// caring whether it was early-exit or ran-the-full-budget-cleanly.
82
83func nx_loop_is_success(v: nx_int) -> nx_int {
84 if v == NX_LOOP_DONE_SUCCESS { return 1 }
85 if v == NX_LOOP_DONE_EXIT { return 1 }
86 return 0
87}
88
89func nx_loop_is_failure(v: nx_int) -> nx_int {
90 if v == NX_LOOP_BUDGET_EXHAUSTED { return 1 }
91 if v == NX_LOOP_ABORTED { return 1 }
92 return 0
93}
94
95// ===== Settle: post-loop verdict resolution =======================
96//
97// Run this once after the while-loop exits. It converts the
98// transient NX_LOOP_RUNNING state into a final terminal verdict by
99// distinguishing two cases:
100//
101// * loop exited with verdict already set (body called mark-exit
102// or mark-abort) -- preserve that verdict
103// * loop fell out because iter reached max_iters without the body
104// setting a verdict -- this is the budget-exhaustion case
105//
106// If the loop body NEVER intended early exit (e.g. simple counted
107// loop), the natural exit is "ran full budget cleanly" which IS the
108// success case for that loop shape. We disambiguate by looking at
109// whether iter == max_iters: yes = full-budget-success, no = early
110// exit signaled by zeroing verdict, etc. In practice the user
111// either uses early-exit (mark-exit before iter == max_iters) or
112// doesn't (verdict stays RUNNING, iter hits max_iters cleanly).
113
114func nx_loop_settle(verdict_in: nx_int, iter: nx_int, max_iters: nx_int) -> nx_int {
115 if verdict_in == NX_LOOP_DONE_EXIT { return NX_LOOP_DONE_EXIT }
116 if verdict_in == NX_LOOP_ABORTED { return NX_LOOP_ABORTED }
117 // Still in RUNNING means we fell out via the header. Did we
118 // hit max_iters? If yes, it depends on whether the loop was
119 // counted-only (max_iters is the intended end) or budget-only.
120 // For canonical use, hitting iter == max_iters from RUNNING is
121 // DONE_SUCCESS for counted loops and BUDGET_EXHAUSTED for
122 // budget-protected loops. We default to BUDGET_EXHAUSTED
123 // because it's the safer outcome: caller MUST handle it; if
124 // they expected success, they can downcast.
125 if iter >= max_iters { return NX_LOOP_BUDGET_EXHAUSTED }
126 // Fell out for some other reason -- shouldn't happen if the
127 // canonical header is `verdict == RUNNING && iter < max`, but
128 // be defensive.
129 return NX_LOOP_DONE_SUCCESS
130}
131
132// ===== Counted-loop helper: alternative settle for simple cases ===
133//
134// When the loop's intent is "do exactly N iterations, no early
135// exit", the natural verdict is DONE_SUCCESS not BUDGET_EXHAUSTED.
136// Use this settle variant for counted loops where reaching the end
137// is the goal, not a failure.
138
139func nx_loop_settle_counted(verdict_in: nx_int, iter: nx_int, n_required: nx_int) -> nx_int {
140 if verdict_in == NX_LOOP_DONE_EXIT { return NX_LOOP_DONE_EXIT }
141 if verdict_in == NX_LOOP_ABORTED { return NX_LOOP_ABORTED }
142 if iter >= n_required { return NX_LOOP_DONE_SUCCESS }
143 return NX_LOOP_BUDGET_EXHAUSTED
144}
145
146// ===== V2 FRAME API: structural four-pillar primitive =============
147//
148// Per [[feedback-loop-discipline-cardinal-2026-05-21]]: the V1
149// manual pattern `while v == RUNNING && i < N` is STILL a manual flag
150// check in the header. V2 collapses bound + watchdog + verdict into
151// one function call so the call site reads as `while nx_loop_step(lp)`.
152// No `==` flag in the header, no manual iter++ in the body.
153//
154// Four-pillar contract:
155// LOG NxLoopFrame.iters increments per step
156// PREVENT nx_loop_begin(max_iters) -- bound is non-optional
157// MONITOR nx_loop_begin_watchdog(max, deadline_ns, no_progress)
158// -- wall-time + stall detection
159// REACTIVE NxLoopVerdict.kind sealed enum: NX_LV_NORMAL /
160// NX_LV_BOUND_EXHAUSTED / NX_LV_TIMED_OUT / NX_LV_STALLED
161//
162// Canonical usage:
163//
164// let lp: *NxLoopFrame = nx_loop_begin(MAX_ITERS)
165// while nx_loop_step(lp) == 1 {
166// // body
167// if done_cond { nx_loop_break(lp) }
168// if progress { nx_loop_mark_progress(lp) }
169// }
170// let v: NxLoopVerdict = nx_loop_finish(lp)
171// // case v.kind ...
172//
173// Research synthesis (see docs/NISHI_LOOP_PRIMITIVE_DESIGN.md):
174// no other language ships all four pillars in one primitive --
175// Rust/Zig bound + iterator, Idris/Coq termination proofs,
176// Eiffel/Dafny decrease clauses; none have watchdog + sealed
177// verdict in one structural API.
178
179// V2 verdict kinds (independent of V1 enum since semantics differ).
180const NX_LV_NORMAL: i64 = 1 // body broke OR predicate matched
181const NX_LV_BOUND_EXHAUSTED: i64 = 2 // hit declared max_iters
182const NX_LV_TIMED_OUT: i64 = 3 // wall-time watchdog fired
183const NX_LV_STALLED: i64 = 4 // no progress for max_no_progress iters
184
185struct NxLoopFrame {
186 iters: i64,
187 max_iters: i64,
188 deadline_ns: i64,
189 last_progress_iter: i64,
190 max_no_progress: i64,
191 break_requested: i64,
192 verdict_kind: i64,
193 reason: i64,
194}
195
196struct NxLoopVerdict {
197 kind: i64,
198 iters: i64,
199 reason: i64,
200}
201
202func nx_loop_begin(max_iters: i64) -> *NxLoopFrame {
203 let raw: *u8 = sys_mmap(64)
204 let lp: *NxLoopFrame = raw as *NxLoopFrame
205 lp.iters = 0
206 lp.max_iters = max_iters
207 lp.deadline_ns = 0
208 lp.last_progress_iter = 0
209 lp.max_no_progress = 0
210 lp.break_requested = 0
211 lp.verdict_kind = 0
212 lp.reason = 0
213 return lp
214}
215
216func nx_loop_begin_watchdog(max_iters: i64, max_wall_ns: i64, max_no_progress: i64) -> *NxLoopFrame {
217 let lp: *NxLoopFrame = nx_loop_begin(max_iters)
218 if max_wall_ns > 0 {
219 let now: i64 = nx_clock_monotonic_ns()
220 lp.deadline_ns = now + max_wall_ns
221 }
222 lp.max_no_progress = max_no_progress
223 return lp
224}
225
226// Returns 1 to continue, 0 to exit (seals the verdict_kind on exit).
227func nx_loop_step(lp: *NxLoopFrame) -> i64 {
228 if lp.break_requested != 0 {
229 if lp.verdict_kind == 0 { lp.verdict_kind = NX_LV_NORMAL }
230 return 0
231 }
232 if lp.iters >= lp.max_iters {
233 if lp.verdict_kind == 0 { lp.verdict_kind = NX_LV_BOUND_EXHAUSTED }
234 return 0
235 }
236 if lp.deadline_ns != 0 {
237 let now: i64 = nx_clock_monotonic_ns()
238 if now >= lp.deadline_ns {
239 if lp.verdict_kind == 0 { lp.verdict_kind = NX_LV_TIMED_OUT }
240 return 0
241 }
242 }
243 if lp.max_no_progress > 0 {
244 let since: i64 = lp.iters - lp.last_progress_iter
245 if since >= lp.max_no_progress {
246 if lp.verdict_kind == 0 { lp.verdict_kind = NX_LV_STALLED }
247 return 0
248 }
249 }
250 lp.iters = lp.iters + 1
251 return 1
252}
253
254func nx_loop_break(lp: *NxLoopFrame) -> i64 {
255 lp.break_requested = 1
256 return 0
257}
258
259func nx_loop_break_with(lp: *NxLoopFrame, reason: i64) -> i64 {
260 lp.break_requested = 1
261 lp.reason = reason
262 return 0
263}
264
265func nx_loop_mark_progress(lp: *NxLoopFrame) -> i64 {
266 lp.last_progress_iter = lp.iters
267 return 0
268}
269
270// Returns the frame pointer itself so the caller can read .verdict_kind,
271// .iters, .reason directly. Returning a NxLoopVerdict struct by value
272// is not yet reliable in the C bootstrap path; the frame fields are
273// the source of truth post-step anyway.
274func nx_loop_finish(lp: *NxLoopFrame) -> *NxLoopFrame {
275 return lp
276}
277
278func nx_loop_was_normal(lp: *NxLoopFrame) -> i64 {
279 if lp.verdict_kind == NX_LV_NORMAL { return 1 }
280 return 0
281}
282
283// ===== Self-test ==================================================
284//
285// Verifies the verdict transitions on three canonical shapes:
286// (a) Counted loop that runs to completion: SUCCESS.
287// (b) Budget loop where body never exits before budget: EXHAUSTED.
288// (c) Body exits early via DONE_EXIT: that verdict preserved.
289// (d) Body aborts via ABORTED: that verdict preserved.
290
291func main() -> i64 {
292 // --- (a) Counted loop, runs to end ---
293 let N1: nx_int = 10
294 var i1: nx_int = 0
295 var v1: nx_int = NX_LOOP_RUNNING
296 while v1 == NX_LOOP_RUNNING && i1 < N1 {
297 i1 = i1 + 1
298 }
299 let r1: nx_int = nx_loop_settle_counted(v1, i1, N1)
300 if r1 != NX_LOOP_DONE_SUCCESS { return 10 }
301 if nx_loop_is_success(r1) != 1 { return 11 }
302
303 // --- (b) Budget loop, body never exits ---
304 let N2: nx_int = 5
305 var i2: nx_int = 0
306 var v2: nx_int = NX_LOOP_RUNNING
307 while v2 == NX_LOOP_RUNNING && i2 < N2 {
308 // body that never sets verdict
309 i2 = i2 + 1
310 }
311 let r2: nx_int = nx_loop_settle(v2, i2, N2)
312 if r2 != NX_LOOP_BUDGET_EXHAUSTED { return 20 }
313 if nx_loop_is_failure(r2) != 1 { return 21 }
314
315 // --- (c) Early DONE_EXIT preserved ---
316 let N3: nx_int = 100
317 var i3: nx_int = 0
318 var v3: nx_int = NX_LOOP_RUNNING
319 while v3 == NX_LOOP_RUNNING && i3 < N3 {
320 if i3 == 3 { v3 = NX_LOOP_DONE_EXIT }
321 i3 = i3 + 1
322 }
323 let r3: nx_int = nx_loop_settle(v3, i3, N3)
324 if r3 != NX_LOOP_DONE_EXIT { return 30 }
325 if i3 != 4 { return 31 } // 0,1,2,3 then exit set, increment, header rejects
326 if nx_loop_is_success(r3) != 1 { return 32 }
327
328 // --- (d) ABORTED preserved ---
329 let N4: nx_int = 100
330 var i4: nx_int = 0
331 var v4: nx_int = NX_LOOP_RUNNING
332 while v4 == NX_LOOP_RUNNING && i4 < N4 {
333 if i4 == 7 { v4 = NX_LOOP_ABORTED }
334 i4 = i4 + 1
335 }
336 let r4: nx_int = nx_loop_settle(v4, i4, N4)
337 if r4 != NX_LOOP_ABORTED { return 40 }
338 if nx_loop_is_failure(r4) != 1 { return 41 }
339
340 // --- (e) Verdict-range gate ---
341 var k: nx_int = 0
342 while k < NX_LOOP_N_VERDICTS {
343 if nx_loop_verdict_is_valid(k) != 1 { return 50 + k }
344 k = k + 1
345 }
346 if nx_loop_verdict_is_valid(NX_LOOP_N_VERDICTS) != 0 { return 60 }
347 if nx_loop_verdict_is_valid(0 - 1) != 0 { return 61 }
348
349 return 0
350}