nx_mcu_ready_gate.nx source
↩ module page · 156 lines · 9562 B
1// nx_mcu_ready_gate.nx -- pins the hardware-test chokepoint, using the MEASURED esp32-ai workload on the
2// MEASURED S3 N16R8 row so the gate is about a real bring-up, not invented numbers.
3//
4// The composition has one asymmetry that must never silently invert, and T4/T5 exist to pin it:
5// SAFETY DOMINATES FIT. A config that fits perfectly is still refused when the write is irreversible,
6// and when BOTH fail the reported blocker is SAFETY -- because a sizing problem is recoverable by picking
7// a smaller model, whereas an unsafe write is a dead board. A symmetric AND would report either, and an
8// operator reading "blocker=FIT" would go shrink the model and then flash an unrecoverable board.
9//
10// T7 is the third-party case and the reason this organ exists: an UNBENCHED board must come back BLOCKED,
11// never READY -- a work order, not a guess.
12// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
13import "nx_syscalls.nx"
14import "nx_gate_verdict.nx"
15import "nx_mcu_ready.nx"
16
17func mrg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
18func mrg_has(hay: *u8, needle: *u8) -> i64 {
19 let hn: i64 = mrg_len(hay)
20 let nn: i64 = mrg_len(needle)
21 if nn <= 0 { return 0 }
22 if hn < nn { return 0 }
23 var i: i64 = 0
24 while i <= hn - nn {
25 var j: i64 = 0
26 var ok: i64 = 1
27 while j < nn {
28 if hay[i + j] != needle[j] { ok = 0; j = nn } else { j = j + 1 }
29 }
30 if ok == 1 { return 1 }
31 i = i + 1
32 }
33 return 0
34}
35
36func main() -> i64 {
37 let ctr: *i64 = gv_ctr()
38 gv_head("nx_mcu_ready_gate -- MCU hardware-test chokepoint: fit AND never-brick, safety dominating" as *u8)
39
40 // measured ESP32-S3 N16R8 + the measured esp32-ai deployable config
41 let SRAM: i64 = 512
42 let PSRAM: i64 = 8
43 let FLASH: i64 = 16
44 let CORE: i64 = 279500
45 let MODEL: i64 = 14912332
46 let KV: i64 = 3145728
47
48 // ---- T1 POS-CONTROL: the real workload on the real board with recovery intact is READY
49 var t1: i64 = 0
50 if rdy_check(SRAM, PSRAM, FLASH, CORE, MODEL, KV, "flash" as *u8, NB_DL_INTACT) == RDY_READY { t1 = 1 }
51 gv_check("T1 POS-CONTROL: measured esp32-ai config on measured S3, recovery intact -> READY" as *u8, t1, ctr)
52
53 // ---- T2 a fitting config becomes BLOCKED the moment the write stops being reversible
54 var t2: i64 = 0
55 if rdy_check(SRAM, PSRAM, FLASH, CORE, MODEL, KV, "flash" as *u8, NB_DL_BURNED) == RDY_BLOCKED_SAFETY { t2 = 1 }
56 gv_check("T2 the SAME fitting config is BLOCKED once download mode is burned (blocker=SAFETY)" as *u8, t2, ctr)
57
58 // ---- T3 an eFuse write is refused even though nothing about the model changed
59 var t3: i64 = 0
60 if rdy_check(SRAM, PSRAM, FLASH, CORE, MODEL, KV, "efuse" as *u8, NB_DL_INTACT) == RDY_BLOCKED_SAFETY { t3 = 1 }
61 gv_check("T3 an eFuse-namespace write is BLOCKED regardless of fit (OTP is OTP)" as *u8, t3, ctr)
62
63 // ---- T4 a too-big model on a safe write reports FIT, not SAFETY
64 var t4: i64 = 0
65 if rdy_check(SRAM, PSRAM, FLASH, 2000000, MODEL, KV, "flash" as *u8, NB_DL_INTACT) == RDY_BLOCKED_FIT { t4 = 1 }
66 gv_check("T4 an oversized core on a SAFE write reports blocker=FIT (a sizing problem, recoverable)" as *u8, t4, ctr)
67
68 // ---- T5 THE ASYMMETRY: when BOTH fail, the blocker reported is SAFETY, never FIT.
69 // If this inverted, an operator would shrink the model and then flash an unrecoverable board.
70 var t5: i64 = 0
71 if rdy_check(SRAM, PSRAM, FLASH, 2000000, MODEL, KV, "efuse" as *u8, NB_DL_INTACT) == RDY_BLOCKED_BOTH { t5 = 1 }
72 gv_check("T5 ASYMMETRY: when fit AND safety both fail, the verdict names SAFETY+FIT, not FIT alone" as *u8, t5, ctr)
73
74 // ---- T6 NEG-CONTROL on T5's reader: BOTH must be a DISTINCT code from either single blocker,
75 // or the asymmetry is unobservable and T5 proves nothing.
76 var t6: i64 = 1
77 if RDY_BLOCKED_BOTH == RDY_BLOCKED_FIT { t6 = 0 }
78 if RDY_BLOCKED_BOTH == RDY_BLOCKED_SAFETY { t6 = 0 }
79 if RDY_READY == RDY_BLOCKED_FIT { t6 = 0 }
80 gv_check("T6 NEG-CONTROL: READY / FIT / SAFETY / BOTH are four DISTINCT codes" as *u8, t6, ctr)
81
82 // ---- T7 THIRD-PARTY BOARD: unbenched target must never come back READY
83 var t7: i64 = 0
84 if rdy_check(0 - 1, 0 - 1, 0 - 1, CORE, MODEL, KV, "flash" as *u8, NB_DL_INTACT) != RDY_READY { t7 = 1 }
85 gv_check("T7 THIRD-PARTY: an UNBENCHED target is never READY (returns a work order, not a guess)" as *u8, t7, ctr)
86
87 // ---- T8 and we can tell 'unknown board' apart from 'bad board'
88 var t8: i64 = 1
89 if rdy_target_measured(SRAM, PSRAM, FLASH) != 1 { t8 = 0 }
90 if rdy_target_measured(0 - 1, PSRAM, FLASH) != 0 { t8 = 0 }
91 if rdy_target_measured(SRAM, 0 - 1, FLASH) != 0 { t8 = 0 }
92 if rdy_target_measured(SRAM, PSRAM, 0 - 1) != 0 { t8 = 0 }
93 gv_check("T8 a benched target reads MEASURED; any UNMEASURED field marks the board unknown" as *u8, t8, ctr)
94
95 // DIAGNOSTIC: print what rdy_reason actually returns. T9/T10 flipped between two runs of nearly
96 // identical binaries while the teeth are pure string compares, so the strings themselves are suspect.
97 // Measure, do not guess.
98 // ISOLATION TEST: hoist each call result into a temp instead of NESTING it inside another call.
99 // Every failing site so far nests (gv_puts(rdy_reason(x)), mrg_has(rdy_reason(x), ...)); every passing
100 // tooth T1-T8 calls rdy_check() directly and compares to a constant, never nesting. If hoisting fixes
101 // the dispatch, the defect is nested-call-as-argument, not rdy_reason.
102 // DISCRIMINATING PROBE: 999 matches NO branch. If == compiles correctly, 999 must return the LAST
103 // (fallthrough) string. If == is being emitted as >, 999 returns the FIRST string, because 999 > 100.
104 // The observed pattern (100->last, 101->first, 102->first) fits > exactly, under BOTH the old 0..3
105 // constants and the new 100..103 ones. This probe separates the two explanations in one line.
106 // TIGHTEST A/B: call the KNOWN-GOOD mf_reason (from nx_mcu_fit.nx, which imports only nx_syscalls)
107 // and the BROKEN rdy_reason (from nx_mcu_ready.nx, which imports TWO modules) IN THE SAME BINARY.
108 // The standalone repro nx_eqprobe already refuted ==-as->, import count, and literal length, and it
109 // put its dispatch in the MAIN file. rdy_reason lives in an imported module that itself imports.
110 // If mf_reason is right here while rdy_reason is wrong, the trigger is the MODULE, not the shape.
111 // FINAL REPRO: rdy_probe is a BRAND-NEW trivial 4-branch dispatch living inside nx_mcu_ready.nx.
112 // Same shape as nx_eqprobe's eq_pick, which is CORRECT in a main file. Only the module differs.
113 let p0: *u8 = rdy_probe(RDY_READY)
114 let p1: *u8 = rdy_probe(RDY_BLOCKED_FIT)
115 let p2: *u8 = rdy_probe(RDY_BLOCKED_SAFETY)
116 let p9: *u8 = rdy_probe(999)
117 gv_puts(" [repro] rdy_probe(0)=" as *u8); gv_puts(p0); gv_puts(" (want P) (1)=" as *u8); gv_puts(p1); gv_puts(" (want Q) (2)=" as *u8); gv_puts(p2); gv_puts(" (want R) (999)=" as *u8); gv_puts(p9); gv_puts(" (want S)\n" as *u8)
118
119 let m_fit: *u8 = mf_reason(MF_FIT)
120 let m_sram: *u8 = mf_reason(MF_REFUSE_SRAM)
121 let m_probe: *u8 = mf_reason(999)
122 gv_puts(" [ab] mf_reason(MF_FIT) = " as *u8); gv_puts(m_fit); gv_puts("\n" as *u8)
123 gv_puts(" [ab] mf_reason(MF_REFUSE_SRAM)= " as *u8); gv_puts(m_sram); gv_puts("\n" as *u8)
124 gv_puts(" [ab] mf_reason(999, no match) = " as *u8); gv_puts(m_probe); gv_puts("\n" as *u8)
125
126 let r_probe: *u8 = rdy_reason(999)
127 gv_puts(" [diag] reason(999, matches NO branch) = " as *u8); gv_puts(r_probe); gv_puts("\n" as *u8)
128 let r_ready: *u8 = rdy_reason(RDY_READY)
129 let r_fit: *u8 = rdy_reason(RDY_BLOCKED_FIT)
130 let r_safety: *u8 = rdy_reason(RDY_BLOCKED_SAFETY)
131 gv_puts(" [diag] reason(READY) = " as *u8); gv_puts(r_ready); gv_puts("\n" as *u8)
132 gv_puts(" [diag] reason(FIT) = " as *u8); gv_puts(r_fit); gv_puts("\n" as *u8)
133 gv_puts(" [diag] reason(SAFETY) = " as *u8); gv_puts(r_safety); gv_puts("\n" as *u8)
134
135 // ---- T9 the operator-facing reason NAMES its blocker (the bring-up contract)
136 var t9: i64 = 1
137 if mrg_has(r_ready, "READY" as *u8) != 1 { t9 = 0 }
138 if mrg_has(r_fit, "blocker=FIT" as *u8) != 1 { t9 = 0 }
139 if mrg_has(r_safety, "blocker=SAFETY" as *u8) != 1 { t9 = 0 }
140 gv_check("T9 every reason NAMES its blocker (what a human acts on during bring-up)" as *u8, t9, ctr)
141
142 // ---- T10 NEG-CONTROL on T9's reader: the FIT reason must NOT claim SAFETY, or the strings are a blob
143 var t10: i64 = 1
144 if mrg_has(r_fit, "blocker=SAFETY" as *u8) != 0 { t10 = 0 }
145 if mrg_has(r_ready, "BLOCKED" as *u8) != 0 { t10 = 0 }
146 gv_check("T10 NEG-CONTROL: the FIT reason does NOT name SAFETY; READY does not say BLOCKED" as *u8, t10, ctr)
147
148 gv_verdict("MCU-READY" as *u8, ctr, "fit and never-brick composed at one chokepoint; safety dominates; an unbenched third-party board is never READY" as *u8)
149 // Derive the exit code from the counters DIRECTLY rather than trusting a helper's return convention.
150 // Found by nx_gate_bite: this gate printed 'verdict=GREEN' while exiting NON-ZERO, so the biter refused
151 // it as UNCONTROLLED. nx_job_run hides child exit codes (debt 1785526584), so stdout looked perfect and
152 // the mismatch was invisible -- I hit the exact trap I had filed hours earlier.
153 // An exit code is the one signal every runner can read; it must not depend on a convention.
154 if ctr[0] == ctr[1] { return 0 }
155 return 1
156}