topic: regalloc
16 modules sharing the regalloc name family (derived from the tree's prefix discipline).
The 'regalloc' topic family in the Nishi sovereign ecosystem focuses on register allocation techniques and their verification within the NishiLang framework. It includes modules like _regalloc_lf_repro, which provides a reproducible test case for linear-scan register allocation, and nx_regalloc_linscan, which implements a provable linear-scan allocator with bits-up optimization. The nx_regalloc_interp module ensures execution-equivalence between original and allocated code, validating correctness through formal verification.
auto-narrated by the local model from this topic's module headers; links verified against the wiki index.
narrated overview -- maintained by the narration lane, module links verified against this wiki.
| module | description | lines | funcs |
|---|---|---|---|
| _regalloc_lf_repro.nx | candidate TEN-SECOND repro for LM-REGALLOC: the | 54 | 5 |
| nx_regalloc.nx | linear-scan register allocator, in NishiLang. | 1112 | 23 |
| nx_regalloc_absorb_governed_test.nx | the LOOP governs absorbing the allocator | 113 | 5 |
| nx_regalloc_calls.nx | the G1 register allocator's KEYSTONE capability: correct | 142 | 5 |
| nx_regalloc_calls_test.nx | PROVE the G1 allocator's live-across-call capability, with | 110 | 7 |
| nx_regalloc_exec_test.nx | PROVE register-allocated execution is 1:1 with the | 112 | 4 |
| nx_regalloc_interp.nx | EXECUTION-equivalence verifier for register allocation. | 85 | 4 |
| nx_regalloc_linscan.nx | linear-scan register allocation, bits-up + PROVABLE. | 143 | 5 |
| nx_regalloc_linscan_test.nx | prove the register allocator on two IRs: | 95 | 4 |
| nx_regalloc_liveness_diag.nx | BITS-UP DIAGNOSTIC for the disabled | 99 | 1 |
| nx_regalloc_race_kernel_test.nx | point the proven allocator at the EXACT hot | 83 | 3 |
| nx_regalloc_soundness_test.nx | BITS-UP soundness proof for the allocator | 164 | 1 |
| regalloc.nx | alias stub. | 24 | 0 |
| regalloc_evict_test.nx | proves the Poletto-Sarkar spill-at- | 95 | 1 |
| regalloc_fpr_evict_test.nx | proves linear_scan_fpr's eviction | 78 | 1 |
| regalloc_test.nx | self-test for regalloc.nx. | 57 | 1 |