code wiki / _hdl_build / nx_self_repair_cycle_test.nx
nx_self_repair_cycle_test.nx
buildroot/runtime/_hdl_build/nx_self_repair_cycle_test.nx
about
nx_self_repair_cycle_test.nx -- the self-build cycle UPGRADED to self-REPAIR,
drawing on the growable RESEARCHER knowledge base (nx_research_basis).
Cardinal #25: when a proposal is bad, REWRITE it better -- don't just filter it.
On UNSOUND, the loop: (1) diagnoses the failure (counterexample = WHY, CEGIS),
(2) the RESEARCHER consults the basis for a modern, CITED alternative,
(3) the VERIFIER re-proves the alternative 1:1, (4) ABSORBS the repaired
capability -- and ESCALATES (hard no) ONLY when the basis has no alternative.
Star case (real, verified both ways): `(mul x 2^k) == (shl x k)` is UNSOUND at
the k>=W boundary; the basis's research-grounded fix is the k<W validity guard
(egg POPL21; Hacker's Delight). Guarded, it is sound for all k<W, all x.
Known answer: 2 unsound proposals -> 1 REPAIRED+ABSORBED + 1 ESCALATED. exit 0.
dependencies 3 imports · 0 importers
imports: nx_rule_soundness.nxnx_crew_council.nxnx_research_basis.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 20 | const SR_W: i64 = 8 |
functions
| 23 | func sr_repair_lookup(id: i64, fix_out: *i64, cite_out: *i64) -> i64 |
| 34 | func sr_mulpow2_unguarded_sound() -> i64 |
| 44 | func sr_mulpow2_guarded_sound(vals: *i64, cells: *NxGsimCell, g: *NxGsim, |
| 59 | func main() -> i64 |