nx_mcu_fit_gate.nx source
↩ module page · 135 lines · 7216 B
1// nx_mcu_fit_gate.nx -- pins the MCU memory-hierarchy admission decision, using the REAL esp32-ai numbers
2// so the gate is about a shipping workload rather than invented ones.
3//
4// Reference config (measured, esp32-ai RESULTS.md 2026-07-21, ESP32-S3 N16R8): 559K-param dense core at
5// 4 bits = 279,500 B against 512 KB internal SRAM; a 14,912,332 B exported model against 16 MB flash;
6// ~3 MB of KV+scratch against 8 MB PSRAM. That config MUST be admitted (T1) or the organ is useless.
7//
8// The two ways this logic goes wrong, both controlled for:
9// - refusing everything (safe-looking, ships nothing): T1/T6/T7 are positive controls.
10// - treating UNMEASURED as room (silently guessing): T5 refuses it, and T6 proves that refusal is
11// SCOPED -- an unmeasured resource nobody asked for must not block a decidable verdict.
12// T9 pins determinism: when two walls are hit at once the reported binding constraint must not wobble.
13// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
14import "nx_syscalls.nx"
15import "nx_gate_verdict.nx"
16import "nx_mcu_fit.nx"
17
18func mfg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
19
20// naive substring: 1 present / 0 absent
21func mfg_has(hay: *u8, needle: *u8) -> i64 {
22 let hn: i64 = mfg_len(hay)
23 let nn: i64 = mfg_len(needle)
24 if nn <= 0 { return 0 }
25 if hn < nn { return 0 }
26 var i: i64 = 0
27 while i <= hn - nn {
28 var j: i64 = 0
29 var ok: i64 = 1
30 while j < nn {
31 if hay[i + j] != needle[j] { ok = 0; j = nn } else { j = j + 1 }
32 }
33 if ok == 1 { return 1 }
34 i = i + 1
35 }
36 return 0
37}
38
39func main() -> i64 {
40 let ctr: *i64 = gv_ctr()
41 gv_head("nx_mcu_fit_gate -- MCU memory-hierarchy admission, pinned to the measured esp32-ai workload" as *u8)
42
43 // the measured ESP32-S3 N16R8 row from mcu_targets.conf
44 let SRAM: i64 = 512
45 let PSRAM: i64 = 8
46 let FLASH: i64 = 16
47 // the measured esp32-ai deployable config
48 let CORE: i64 = 279500
49 let MODEL: i64 = 14912332
50 let KV: i64 = 3145728
51
52 // ---- T1 POS-CONTROL: the real shipping workload is ADMITTED on the real board
53 var t1: i64 = 0
54 if mf_admit(SRAM, PSRAM, FLASH, CORE, MODEL, KV) == MF_FIT { t1 = 1 }
55 gv_check("T1 POS-CONTROL: the measured esp32-ai config FITS the measured S3 N16R8" as *u8, t1, ctr)
56
57 // ---- T2 SRAM wall: a core that cannot live in internal SRAM is refused, and NAMED
58 var t2: i64 = 0
59 if mf_admit(SRAM, PSRAM, FLASH, 2000000, MODEL, KV) == MF_REFUSE_SRAM { t2 = 1 }
60 gv_check("T2 a 2MB dense core is REFUSED with binding=SRAM" as *u8, t2, ctr)
61
62 // ---- T3 FLASH wall
63 var t3: i64 = 0
64 if mf_admit(SRAM, PSRAM, FLASH, CORE, 20000000, KV) == MF_REFUSE_FLASH { t3 = 1 }
65 gv_check("T3 a 20MB model on 16MB flash is REFUSED with binding=FLASH" as *u8, t3, ctr)
66
67 // ---- T4 PSRAM wall
68 var t4: i64 = 0
69 if mf_admit(SRAM, PSRAM, FLASH, CORE, MODEL, 9437184) == MF_REFUSE_PSRAM { t4 = 1 }
70 gv_check("T4 a 9MB KV+scratch on 8MB PSRAM is REFUSED with binding=PSRAM" as *u8, t4, ctr)
71
72 // ---- T5 THE HONESTY TOOTH: an unmeasured SRAM figure must REFUSE, never guess a fit
73 var t5: i64 = 0
74 if mf_admit(0 - 1, PSRAM, FLASH, CORE, MODEL, KV) == MF_REFUSE_UNMEASURED { t5 = 1 }
75 gv_check("T5 UNMEASURED sram_kb REFUSES rather than assuming room (bench it first)" as *u8, t5, ctr)
76
77 // ---- T6 NEG-CONTROL ON T5: that refusal must be SCOPED to resources actually demanded.
78 // A board with no PSRAM measurement is still decidable for a model that needs no PSRAM. Without this,
79 // T5 would pass even if the organ refused every input it ever saw.
80 var t6: i64 = 0
81 if mf_admit(SRAM, 0 - 1, FLASH, CORE, MODEL, 0) == MF_FIT { t6 = 1 }
82 gv_check("T6 NEG-CONTROL: UNMEASURED psram does NOT block a model that demands no PSRAM" as *u8, t6, ctr)
83
84 // ---- T7/T8 the SRAM boundary, exactly. 512KB == 524288 B.
85 var t7: i64 = 0
86 if mf_admit(SRAM, PSRAM, FLASH, 524288, MODEL, KV) == MF_FIT { t7 = 1 }
87 gv_check("T7 a core of exactly 524288 B FITS 512 KB SRAM (boundary is inclusive)" as *u8, t7, ctr)
88
89 var t8: i64 = 0
90 if mf_admit(SRAM, PSRAM, FLASH, 524289, MODEL, KV) == MF_REFUSE_SRAM { t8 = 1 }
91 gv_check("T8 one byte over (524289) is REFUSED -- the boundary is not fudged" as *u8, t8, ctr)
92
93 // ---- T9 DETERMINISM: two walls hit at once must report the same, tightest constraint every time
94 var t9: i64 = 1
95 if mf_admit(SRAM, PSRAM, FLASH, 2000000, 20000000, KV) != MF_REFUSE_SRAM { t9 = 0 }
96 if mf_admit(SRAM, PSRAM, FLASH, 2000000, 20000000, KV) != MF_REFUSE_SRAM { t9 = 0 }
97 gv_check("T9 when SRAM and FLASH both fail, binding=SRAM is reported deterministically" as *u8, t9, ctr)
98
99 // ---- T10 the bit-width arithmetic that sizes a core
100 var t10: i64 = 1
101 if mf_core_bytes(559000, 4) != 279500 { t10 = 0 }
102 if mf_core_bytes(559000, 8) != 559000 { t10 = 0 }
103 if mf_core_bytes(559000, 2) != 139750 { t10 = 0 }
104 gv_check("T10 core sizing: 559K params = 279500 B at 4-bit, 559000 B at 8-bit, 139750 B at 2-bit" as *u8, t10, ctr)
105
106 // ---- T11 DISCRIMINATION: the SAME config must flip FIT->REFUSE when only the TARGET changes.
107 // This is what proves the decision depends on the board and is not a constant.
108 var t11: i64 = 0
109 if mf_admit(SRAM, PSRAM, FLASH, CORE, MODEL, KV) == MF_FIT {
110 if mf_admit(256, PSRAM, 4, CORE, MODEL, KV) == MF_REFUSE_SRAM { t11 = 1 }
111 }
112 gv_check("T11 DISCRIMINATION: the same config FITS the S3 but is REFUSED on a 256KB/4MB target" as *u8, t11, ctr)
113
114 // ---- T12 THE OPERATOR-FACING CONTRACT. A bite run proved codes alone leave the reason strings
115 // unasserted: 4 mutants inside mf_reason survived because nothing here read them. The reason text IS
116 // what a human acts on during bring-up, so it must NAME the constraint it refused for.
117 var t12: i64 = 1
118 if mfg_has(mf_reason(MF_FIT), "FIT" as *u8) != 1 { t12 = 0 }
119 if mfg_has(mf_reason(MF_REFUSE_SRAM), "binding=SRAM" as *u8) != 1 { t12 = 0 }
120 if mfg_has(mf_reason(MF_REFUSE_FLASH), "binding=FLASH" as *u8) != 1 { t12 = 0 }
121 if mfg_has(mf_reason(MF_REFUSE_PSRAM), "binding=PSRAM" as *u8) != 1 { t12 = 0 }
122 if mfg_has(mf_reason(MF_REFUSE_UNMEASURED), "binding=UNMEASURED" as *u8) != 1 { t12 = 0 }
123 gv_check("T12 every reason string NAMES the constraint it refused for (the bring-up contract)" as *u8, t12, ctr)
124
125 // ---- T13 NEG-CONTROL on T12's reader: the reasons must be DISTINCT, and mfg_has must discriminate.
126 // If mfg_has returned 1 unconditionally, or every reason were the same blob, T12 would be vacuous.
127 var t13: i64 = 1
128 if mfg_has(mf_reason(MF_REFUSE_SRAM), "binding=FLASH" as *u8) != 0 { t13 = 0 }
129 if mfg_has(mf_reason(MF_REFUSE_FLASH), "binding=PSRAM" as *u8) != 0 { t13 = 0 }
130 if mfg_has(mf_reason(MF_FIT), "binding=" as *u8) != 0 { t13 = 0 }
131 gv_check("T13 NEG-CONTROL: reasons are distinct -- the SRAM reason does NOT name FLASH" as *u8, t13, ctr)
132
133 let rc: i64 = gv_verdict("MCU-FIT" as *u8, ctr, "admission is target-dependent, boundary-exact, deterministic, and refuses UNMEASURED instead of guessing" as *u8)
134 return rc
135}