nx_loop.nx

nx_loop.nx -- bounded-loop discipline primitive. Per docs/LOOP_DESIGN_RESEARCH.md. Provides the sealed verdict enum + settle helper for the substrate's canonical bounded-loop pattern. Replaces ad-hoc `keep == 1` sentinel-flag style with a structured verdict that distinguishes: NX_LOOP_RUNNING -- loop is still active NX_LOOP_DONE_SUCCESS -- ran to budget, body never asked to stop -- the loop did its full job NX_LOOP_DONE_EXIT -- body asked to exit early (success) NX_LOOP_BUDGET_EXHAUSTED -- budget hit before body finished NX_LOOP_ABORTED -- body asked to abort (hard error) Inspired by NASA JPL Power of 10 Rule 2 (Holzmann 2006: all loops must have a fixed upper bound) + Why3 loop-variants + Idris totality checking. Without a parser-level `bounded` keyword (queued for self-host), this module lets substrate code follow the same DISCIPLINE today with no compiler change. ===== Canonical loop pattern ===== import "nx_loop.nx" let MAX_ITERS: nx_int = 1024 var iter: nx_int = 0 var verdict: nx_int = NX_LOOP_RUNNING while verdict == NX_LOOP_RUNNING && iter < MAX_ITERS { // body here, may set verdict via constants below if early_success_cond { verdict = NX_LOOP_DONE_EXIT } if hard_error_cond { verdict = NX_LOOP_ABORTED } iter = iter + 1 } verdict = nx_loop_settle(verdict, iter, MAX_ITERS) // verdict is now one of {DONE_SUCCESS, DONE_EXIT, // BUDGET_EXHAUSTED, ABORTED} Properties (the four-pillar discipline this primitive enforces): DETECT -- verdict tells you exactly why the loop ended PREVENT -- MAX_ITERS in the loop header makes infinite loops