code wiki / (root) / nx_mcu_ready.nx

nx_mcu_ready.nx source

↩ module page · 104 lines · 7246 B

1// nx_mcu_ready.nx -- THE HARDWARE-TEST CHOKEPOINT: composes the two independent questions a board must 2// answer before anyone plugs one in. 3// 4// 1. DOES IT FIT? nx_mcu_fit -- core->SRAM, weights+table->flash, KV->PSRAM, refusing UNMEASURED. 5// 2. IS IT SAFE? nx_mcu_brick -- eFuse burns refused as a class; flash permitted only while the 6// mask-ROM UART recovery path is intact. 7// 8// ★SAFETY DOMINATES, ALWAYS. A config that fits perfectly is still REFUSED if the write is irreversible. 9// The reverse is not symmetric: a safe write that does not fit is merely a sizing problem, recoverable by 10// choosing a smaller model. An unsafe write that fits is a DEAD BOARD. So the composition is deliberately 11// NOT a symmetric AND -- when both fail, the reported blocker is SAFETY, because that is the one the 12// operator must never work around. 13// 14// WHY A SEPARATE ORGAN RATHER THAN A FLAG ON EITHER. Both inputs already exist and are gated (nx_mcu_fit 15// 13/13, nx_neverbrick_gate 9/9). What did not exist was a SINGLE CALL a bring-up path can route through, 16// and per the adoption law a capability proven only inside its own gate IS the baseline. This is the wire. 17// 18// FIRST- vs THIRD-PARTY: identical logic, different data. A first-party board is a row in mcu_targets.conf 19// we have benched; a third-party board is a row we have NOT, so its fields are -1 and nx_mcu_fit REFUSES 20// with UNMEASURED. That refusal is the correct answer for an unknown board -- it returns a work order 21// ("bench these fields") rather than a guess, which is exactly what makes third-party testing safe. 22// license_tier: ORIGINAL No hw writes (Rule 26). 23import "nx_syscalls.nx" 24import "nx_mcu_fit.nx" 25import "nx_mcu_brick.nx" 26 27// ★RETRACTED 2026-08-06 -- THERE WAS NEVER A COMPILER DEFECT, AND THIS COMMENT USED TO SAY THERE WAS. 28// Debts 1785529609 + 1785530065 (both sev-9, both EATEN) blamed nx_cc for miscompiling `==`. The real 29// cause was one character in rdy_reason below: its FIRST branch read `if v != RDY_READY`. That alone 30// reproduces EVERY observation in both rows under BOTH const sets, with no codegen defect whatsoever -- 31// and it was an ESCAPED nx_gate_bite phase-1 mutant (`==` -> `!=` is literally that tool's operator 1), 32// stranded here when a run died inside its mutation window. nx_gate_bite now keeps a write-ahead pristine 33// sidecar so that can no longer happen. 34// ★THE CONTROL THAT SETTLES IT WAS ALWAYS IN THIS FILE: rdy_probe -- same module, same two imports, same 35// named consts, same long literals -- printed P/Q/R/S CORRECTLY in the same binary on the same run. It 36// differs from rdy_reason in exactly one character, so const collision, import count, module-vs-main and 37// literal length were all held CONSTANT and refuted. Verified by execution: 8/10 RED -> 10/10 GREEN on 38// that one byte. ★★A DIFFERENTIAL PROBE HAND-COPIED FROM ITS SUBJECT IS ONLY EVIDENCE IF THE COPY IS 39// PROVEN CHARACTER-IDENTICAL -- this one silently CORRECTED the bug while being copied, and so exonerated 40// the innocent for four rounds. 41// The 100..103 offsets are therefore NOT load-bearing (0..3 was never the problem); they are kept only 42// because changing them now would be an unrelated edit to a Rule-26 chokepoint. rdy_probe is kept as the 43// standing control -- it is what makes any future claim of a codegen defect here falsifiable in one run. 44const RDY_READY: i64 = 100 45const RDY_BLOCKED_FIT: i64 = 101 46const RDY_BLOCKED_SAFETY: i64 = 102 47const RDY_BLOCKED_BOTH: i64 = 103 48 49func rdy_reason(v: i64) -> *u8 { 50 if v == RDY_READY { return "READY -- fits the target and the write is reversible" as *u8 } 51 if v == RDY_BLOCKED_FIT { return "BLOCKED blocker=FIT (safe to write, but the model does not fit)" as *u8 } 52 if v == RDY_BLOCKED_SAFETY { return "BLOCKED blocker=SAFETY (fits, but the write is NOT reversible -- Rule 26)" as *u8 } 53 return "BLOCKED blocker=SAFETY+FIT (unsafe AND does not fit; safety is the one that must never be worked around)" as *u8 54} 55 56// THE CHOKEPOINT. Every MCU bring-up path routes through this and proceeds only on RDY_READY. 57func rdy_check(sram_kb: i64, psram_mb: i64, flash_mb: i64, 58 core_bytes: i64, flash_bytes: i64, psram_bytes: i64, 59 ns: *u8, dl_state: i64) -> i64 { 60 let fit: i64 = mf_admit(sram_kb, psram_mb, flash_mb, core_bytes, flash_bytes, psram_bytes) 61 let safe: i64 = nb_verdict(ns, dl_state) 62 var fit_bad: i64 = 0 63 if fit != MF_FIT { fit_bad = 1 } 64 var safe_bad: i64 = 0 65 if safe != NB_GREEN { safe_bad = 1 } 66 if safe_bad == 1 { 67 if fit_bad == 1 { return RDY_BLOCKED_BOTH } 68 return RDY_BLOCKED_SAFETY 69 } 70 if fit_bad == 1 { return RDY_BLOCKED_FIT } 71 return RDY_READY 72} 73 74// FINAL REPRO PROBE for debt 1785531316. A brand-new, trivially simple 4-branch dispatch placed INSIDE 75// this module -- the one that imports nx_mcu_fit AND nx_mcu_brick. The standalone nx_eqprobe has the 76// identical shape but lives in a MAIN file and dispatches CORRECTLY (including its 999 no-match case). 77// If this one is ALSO wrong, the trigger is the MODULE (a dispatch inside a module that itself imports 78// non-syscall modules); if it is RIGHT, the defect is specific to rdy_reason and not to the module. 79// Literals are 1 char so nothing else can be blamed. Correct: 0->P 1->Q 2->R 999->S. 80// ROUND 2 OF THIS PROBE. With INTEGER LITERALS (0/1/2) it dispatched CORRECTLY from inside this module, 81// refuting the module hypothesis. The ONLY remaining difference from the broken rdy_reason is that 82// rdy_reason compares against NAMED CONSTS. Switch this probe to the same consts, changing nothing else. 83// nx_eqprobe uses named consts too and is CORRECT -- but its dispatch lives in a MAIN file, not a LIB. 84// So the suspected trigger is the CONJUNCTION: named-const comparison, inside a LIB, that imports other 85// const-declaring modules. Correct: 100->P 101->Q 102->R 999->S. 86// ROUND 3. Named consts in this lib: CORRECT. Short literals in this lib: CORRECT. Long literals in a 87// MAIN file (nx_eqprobe): CORRECT. The one conjunction never tested is LONG LITERALS INSIDE THIS LIB -- 88// which is exactly what the broken rdy_reason is. Same consts, same module; only the literals lengthen. 89// Each still starts with its identifying letter so the P/Q/R/S reading is unchanged. 90func rdy_probe(v: i64) -> *u8 { 91 if v == RDY_READY { return "P -- fits the target and the write is reversible" as *u8 } 92 if v == RDY_BLOCKED_FIT { return "Q blocker=FIT (safe to write, but the model does not fit)" as *u8 } 93 if v == RDY_BLOCKED_SAFETY { return "R blocker=SAFETY (fits, but the write is NOT reversible -- Rule 26)" as *u8 } 94 return "S blocker=SAFETY+FIT (unsafe AND does not fit; safety is the one that must never be worked around)" as *u8 95} 96 97// Is this target benched enough to be trusted at all? A third-party board with UNMEASURED fields is not a 98// failure -- it is a WORK ORDER. Kept separate so a caller can tell "unknown board" from "bad board". 99func rdy_target_measured(sram_kb: i64, psram_mb: i64, flash_mb: i64) -> i64 { 100 if sram_kb == MF_UNMEASURED { return 0 } 101 if psram_mb == MF_UNMEASURED { return 0 } 102 if flash_mb == MF_UNMEASURED { return 0 } 103 return 1 104}