nx_research_basis.nx source

1// nx_research_basis.nx -- the RESEARCHER leg as a real, growable, CITED knowledge 2// base of research-grounded repairs. When the Verifier finds a proposal unsound, 3// the loop consults this basis for a modern, literature-backed alternative (the 4// soundness-restoring fix) instead of a hard no. Data-driven (Cardinal #11) and 5// every entry carries its citation (Cardinal #4: verified facts, real research). 6// The loop GROWS this basis as it learns more fixes; today's seed = 8 canonical 7// failure->fix patterns from compiler / hardware / numerics / power research 8// (the last three added 2026-06-03: energy-proxy, register-allocation, and the 9// battery-attribution caveat that grounded this session's efficiency-triangle work). 10// license_tier: ORIGINAL (the FACTS/citations are concepts, not copied text) 11 12import "nx_syscalls.nx" 13 14const RB_NONE: i64 = 0 15const RB_STRENGTH_SHIFT: i64 = 1 // mul x 2^k -> shl x k 16const RB_DIV_CONST: i64 = 2 // x / c (invariant divisor) 17const RB_MIDPOINT_OVF: i64 = 3 // (a+b)/2 overflow 18const RB_FP_REASSOC: i64 = 4 // (a+b)+c == a+(b+c) for floats 19const RB_SIGNED_SHR_DIV: i64 = 5 // signed x / 2^k via shift 20const RB_ENERGY_PROXY: i64 = 6 // energy == cycles (ignores switching activity) 21const RB_REGALLOC: i64 = 7 // stack-machine codegen spills every value 22const RB_SENSOR_ATTR: i64 = 8 // battery power == CPU energy (false on AC) 23const RB_N: i64 = 8 24 25func rb_has(id: i64) -> i64 { 26 if id < 1 { return 0 } 27 if id > RB_N { return 0 } 28 return 1 29} 30 31// the UNSOUND form the Generator might naively propose. 32func rb_unsound_form(id: i64) -> *u8 { 33 if id == RB_STRENGTH_SHIFT { return "(mul x 2^k) == (shl x k) [unguarded]" as *u8 } 34 if id == RB_DIV_CONST { return "(div x c) == (mulhi x recip) >> s [naive reciprocal]" as *u8 } 35 if id == RB_MIDPOINT_OVF { return "mid = (a + b) / 2 [a+b overflows]" as *u8 } 36 if id == RB_FP_REASSOC { return "(a + b) + c == a + (b + c) [floats]" as *u8 } 37 if id == RB_SIGNED_SHR_DIV { return "(sdiv x 2^k) == (x >> k) [signed, negatives]" as *u8 } 38 if id == RB_ENERGY_PROXY { return "energy == cycle count [ignores switching activity]" as *u8 } 39 if id == RB_REGALLOC { return "stack-machine codegen spills every value [~2x compute tax vs C]" as *u8 } 40 if id == RB_SENSOR_ATTR { return "battery power_now == CPU energy [false while on AC/charging]" as *u8 } 41 return "?" as *u8 42} 43 44// the RESEARCH-GROUNDED fix (the soundness-restoring alternative). 45func rb_fix(id: i64) -> *u8 { 46 if id == RB_STRENGTH_SHIFT { return "add the k<W validity guard (conditional rewrite)" as *u8 } 47 if id == RB_DIV_CONST { return "Granlund-Montgomery magic constant + correction shift/add" as *u8 } 48 if id == RB_MIDPOINT_OVF { return "mid = a + (b - a) / 2 (overflow-safe)" as *u8 } 49 if id == RB_FP_REASSOC { return "guard exact/integer only; floats need round-to-nearest / no-fast-math" as *u8 } 50 if id == RB_SIGNED_SHR_DIV { return "add the negative rounding bias: (x + ((x>>(W-1)) & (2^k - 1))) >> k" as *u8 } 51 if id == RB_ENERGY_PROXY { return "dynamic energy ~ switching activity (a*C*V^2*f); count gate TOGGLES; measure real via RAPL/fuel-gauge" as *u8 } 52 if id == RB_REGALLOC { return "register allocation: linear-scan / graph-coloring keeps live values in registers (the keystone lever)" as *u8 } 53 if id == RB_SENSOR_ATTR { return "attribute energy only while DISCHARGING; on AC the adapter powers the CPU; integrate power_now x time" as *u8 } 54 return "?" as *u8 55} 56 57// the CITATION (modern/canonical research the fix is grounded in -- REAL sources, 58// Cardinal #4: verified facts only, never an invented reference). 59func rb_citation(id: i64) -> *u8 { 60 if id == RB_STRENGTH_SHIFT { return "egg (Willsey et al., POPL 2021); Warren, Hacker's Delight 2e ch.10" as *u8 } 61 if id == RB_DIV_CONST { return "Granlund & Montgomery, PLDI 1994; Hacker's Delight ch.10" as *u8 } 62 if id == RB_MIDPOINT_OVF { return "Bloch, 'Nearly All Binary Searches Are Broken', Google Research 2006" as *u8 } 63 if id == RB_FP_REASSOC { return "Goldberg, 'What Every CS Should Know About FP', ACM CSUR 1991" as *u8 } 64 if id == RB_SIGNED_SHR_DIV { return "Warren, Hacker's Delight 2e sec.10-1; Granlund-Montgomery" as *u8 } 65 if id == RB_ENERGY_PROXY { return "Weste & Harris, CMOS VLSI Design 4e, 2010 (P=a*C*V^2*f); Najm, IEEE TVLSI 1994 (power-estimation survey)" as *u8 } 66 if id == RB_REGALLOC { return "Poletto & Sarkar, ACM TOPLAS 1999 (linear scan); Chaitin, SIGPLAN 1982 (graph coloring); Erbsen et al. (fiat-crypto), IEEE S&P 2019" as *u8 } 67 if id == RB_SENSOR_ATTR { return "Linux power_supply class (Documentation/power/power_supply_class.rst); Khan et al., ACM TOMPECS 2018 (RAPL in Action); Intel SDM Vol.3B (RAPL MSRs)" as *u8 } 68 return "?" as *u8 69}