nx_safety_critical_grade.nx source
↩ module page · 433 lines · 19054 B
1// nx_safety_critical_grade.nx -- Layer-3 safety-critical grader.
2//
3// 8th perspective in the heptagulation -> octagulation, per cardinal
4// feedback-exceed-jpl-iec-ieee-zero-injuries-while-winning (2026-05-16):
5//
6// "our nishi stuff should exceed nasas jpl standards and the safety
7// standards etc as part of our racing crew work, zero injuries in
8// the workplace while still winning everytime"
9//
10// Companion catalog: nishi-library/seeds/safety-critical-standards.toml
11//
12// Eight safety axes scored per source file:
13// 1. bounded_loop_coverage -- JPL Rule 2 + IEC 61508 SIL termination
14// 2. assertion_density -- JPL Rule 5 + DO-178C verification
15// 3. sealed_enum_completeness -- DO-178C formal-method equivalent
16// 4. soup_purity -- IEC 62304 + license-tier wall
17// 5. mcdc_branch_coverage -- DO-178C DAL A (IR-level, queued)
18// 6. fault_injection_survived -- IEC 61508 DC (telemetry corpus, queued)
19// 7. hazard_register_match -- ISO 26262 HARA / MIL-STD-882 (corpus)
20// 8. iv_and_v_perspective_count -- NASA-STD-8719 IV&V (other graders)
21//
22// First cut implements axes 1-4 via lexical scan. Axes 5-8 require
23// IR-level / corpus / cross-grader input that this file's scan does
24// not have; they return NX_SC_VERDICT_UNMEASURED with a clear
25// named-improvement pointing at what's needed to populate them.
26//
27// Per cardinal feedback-honest-perf-verdict-no-aspirational-claims:
28// the verdict explicitly distinguishes WIN (axis passed) from
29// UNMEASURED (axis not yet evaluable) from LOSE (axis evaluated +
30// failed). An overall WIN_S requires all 8 axes to be WIN, not
31// MIX(WIN, UNMEASURED).
32//
33// license_tier: ORIGINAL
34// genealogy_id: substrate-native synthesis of NASA-JPL-Power-of-10 +
35// IEC-61508 + ISO-26262 + DO-178C + IEC-62304 +
36// NASA-STD-8719.13 + MIL-STD-882E (all OPEN sources
37// per feedback-nishi-library-open-research-not-paywall-
38// funding)
39//
40// nx_safety_envelope: (META -- this is the safety grader itself)
41// intended_use: "Layer-3 safety-critical 8-axis grader -- the
42// 8th perspective in the heptagulation ->
43// octagulation. Scores substrate files against
44// the union of JPL Power of 10 + IEC 61508 +
45// ISO 26262 + DO-178C + IEC 62304 + NASA-STD-
46// 8719.13 + MIL-STD-882E."
47// sil_target: SIL3 (this grader's verdict is consumed
48// by composition rules; false PASS
49// here = systemic safety claim
50// unbacked across the substrate)
51// asil_target: QM
52// dal_target: NONE
53// iec_62304_class: NONE
54// evidence: [no_floating_point, sealed_NX_SC_VERDICT,
55// sealed_NX_SC_AXIS_enum_complete_8,
56// 4_of_8_axes_lexical_scan_implemented,
57// 4_queued_axes_return_UNMEASURED_explicitly,
58// no_aspirational_PASS_per_honest_perf_verdict,
59// OPEN_sources_only_per_open_research_cardinal]
60// hazard_register: [bug-tape-aspirational-PASS-grader-overscore,
61// bug-tape-lexical-scan-false-negative,
62// bug-tape-WIN_S-claimed-with-UNMEASURED-axes]
63// residual_risk: "4 of 8 axes are currently lexical-scan
64// implementations (low fidelity). The 4
65// queued axes (MCDC, fault_injection,
66// hazard_register, IV&V) require IR-level
67// analysis OR corpus access OR cross-grader
68// roll-up. Their UNMEASURED verdict is
69// STRUCTURALLY HONEST -- WIN_S can ONLY be
70// reached when all 8 axes have non-UNMEASURED
71// verdicts (n_unmeasured == 0 check in
72// nx_safety_critical_scan)."
73// verdict: NOT_YET_EVALUATED (META: this grader scoring
74// itself is a fixed-point computation that
75// needs the queued runtime to land first)
76
77import "nx_syscalls.nx"
78import "nx_runtime.nx"
79import "nx_types.nx"
80import "nx_tier.nx"
81
82// ---- Sealed verdict ------------------------------------------------
83
84const NX_SC_VERDICT_UNMEASURED: nx_int = 0
85const NX_SC_VERDICT_WIN: nx_int = 1
86const NX_SC_VERDICT_LOSE: nx_int = 2
87const NX_SC_VERDICT_TIE: nx_int = 3
88const NX_SC_VERDICT_WIN_S: nx_int = 4 // unanimous WIN across all 8 axes
89
90// ---- Sealed enum: safety axis --------------------------------------
91
92const NX_SC_AXIS_BOUNDED_LOOP: nx_int = 0
93const NX_SC_AXIS_ASSERTION_DENSITY: nx_int = 1
94const NX_SC_AXIS_SEALED_ENUM: nx_int = 2
95const NX_SC_AXIS_SOUP_PURITY: nx_int = 3
96const NX_SC_AXIS_MCDC_BRANCH: nx_int = 4
97const NX_SC_AXIS_FAULT_INJECTION: nx_int = 5
98const NX_SC_AXIS_HAZARD_REGISTER: nx_int = 6
99const NX_SC_AXIS_IV_AND_V_COUNT: nx_int = 7
100const NX_SC_AXIS_N: nx_int = 8
101
102// ---- Per-axis report struct ----------------------------------------
103
104struct SafetyAxisReport {
105 axis: nx_int,
106 raw_count: nx_int,
107 threshold: nx_int,
108 verdict: nx_int,
109}
110
111struct SafetyCard {
112 axis_bounded_loop: SafetyAxisReport,
113 axis_assertion: SafetyAxisReport,
114 axis_sealed_enum: SafetyAxisReport,
115 axis_soup_purity: SafetyAxisReport,
116 axis_mcdc: SafetyAxisReport,
117 axis_fault_inj: SafetyAxisReport,
118 axis_hazard_reg: SafetyAxisReport,
119 axis_iv_and_v: SafetyAxisReport,
120 n_win: nx_int,
121 n_lose: nx_int,
122 n_unmeasured: nx_int,
123 overall_verdict: nx_int,
124}
125
126// ---- Byte helpers (mirrors nx_a11y_check) --------------------------
127
128func _sc_byte_at(src: *u8, i: nx_int) -> nx_int {
129 let p: *u8 = (src as nx_int + i) as *u8
130 let b: nx_int = p[0] as nx_int
131 return b & 255
132}
133
134func _sc_eq_at(src: *u8, src_len: nx_int, off: nx_int, needle: *u8, needle_len: nx_int) -> nx_int {
135 if off + needle_len > src_len { return 0 }
136 var k: nx_int = 0
137 while k < needle_len {
138 let a: nx_int = _sc_byte_at(src, off + k)
139 let b: nx_int = _sc_byte_at(needle, k)
140 if a != b { return 0 }
141 k = k + 1
142 }
143 return 1
144}
145
146// Count occurrences of `needle` in `src`. Naive linear scan; substrate
147// files are <2k LOC so bounded by O(src_len * needle_len) is fine.
148func _sc_count_substr(src: *u8, src_len: nx_int, needle: *u8, needle_len: nx_int) -> nx_int {
149 var i: nx_int = 0
150 var n: nx_int = 0
151 while i < src_len {
152 if _sc_eq_at(src, src_len, i, needle, needle_len) == 1 {
153 n = n + 1
154 i = i + needle_len
155 } else {
156 i = i + 1
157 }
158 }
159 return n
160}
161
162// ---- Axis 1: bounded_loop_coverage ---------------------------------
163//
164// Per cardinal feedback-bounded-loop-discipline-jpl-rule-2: every
165// while loop must be bounded by `iter < BUDGET` or settled via
166// `nx_loop_settle`. Sentinel-flag pattern (`while keep == 1 {`) is
167// the documented anti-pattern.
168//
169// Lexical proxy:
170// - count "while " occurrences = total_whiles
171// - count "while keep == " + "while 1 " + "while true " = unbounded_whiles
172// - count "nx_loop_settle" + " < BUDGET" + "BUDGET" = bounded_indicators
173//
174// Verdict:
175// unbounded_whiles == 0 AND (total_whiles == 0 OR bounded_indicators > 0)
176// -> WIN
177// else -> LOSE
178//
179// raw_count returns the unbounded_whiles count for the report.
180
181func _sc_axis_bounded_loop(src: *u8, src_len: nx_int) -> nx_int {
182 let p_while: *u8 = "while " as *u8
183 let p_keep: *u8 = "while keep ==" as *u8
184 let p_while1: *u8 = "while 1 " as *u8
185 let p_whtrue: *u8 = "while true " as *u8
186
187 let total: nx_int = _sc_count_substr(src, src_len, p_while, 6)
188 let unbounded_a: nx_int = _sc_count_substr(src, src_len, p_keep, 13)
189 let unbounded_b: nx_int = _sc_count_substr(src, src_len, p_while1, 8)
190 let unbounded_c: nx_int = _sc_count_substr(src, src_len, p_whtrue, 11)
191 let unbounded: nx_int = unbounded_a + unbounded_b + unbounded_c
192
193 return unbounded
194}
195
196// ---- Axis 2: assertion_density -------------------------------------
197//
198// JPL Rule 5: assertion density >= 2 per function. Substrate uses
199// several assertion forms:
200// - nx_assert_*( ... )
201// - if ... { return __syscall(93, <code>, 0, 0, 0, 0, 0) } // sys_exit assert
202// - if ... { return <error_const> } // typed verdict
203//
204// Lexical proxy:
205// - count "func " occurrences = fn_count
206// - count "nx_assert_" + "__syscall(93, " + "return Result::Err" = assert_count
207//
208// Verdict:
209// fn_count == 0 OR (assert_count >= fn_count) -> WIN // >= 1 per fn (substrate-relaxed JPL #5)
210// assert_count >= fn_count * 2 -> WIN_S // exceeds JPL #5
211// else -> LOSE
212//
213// raw_count = assert_count. threshold = fn_count (the >= 1-per-fn bar).
214
215func _sc_axis_assertion_density(src: *u8, src_len: nx_int, fn_count_out: *nx_int) -> nx_int {
216 let p_func: *u8 = "func " as *u8
217 let p_assert: *u8 = "nx_assert_" as *u8
218 let p_sysexit: *u8 = "__syscall(93, " as *u8
219 let p_reserr: *u8 = "Result::Err" as *u8
220
221 let fns: nx_int = _sc_count_substr(src, src_len, p_func, 5)
222 let a: nx_int = _sc_count_substr(src, src_len, p_assert, 10)
223 let b: nx_int = _sc_count_substr(src, src_len, p_sysexit, 15)
224 let c: nx_int = _sc_count_substr(src, src_len, p_reserr, 11)
225
226 *fn_count_out = fns
227 return a + b + c
228}
229
230// ---- Axis 3: sealed_enum_completeness ------------------------------
231//
232// Substrate convention: sealed enums declare named constants under a
233// shared prefix, e.g. NX_RT_VERDICT_WIN, NX_RT_VERDICT_LOSE, ...
234// Counting "const NX_" occurrences gives a lower bound on the number
235// of sealed-enum constants.
236//
237// Verdict:
238// const_count >= 3 -> WIN (file uses sealed-enum discipline)
239// else -> UNMEASURED (file may simply have no enums)
240//
241// (LOSE would require detecting an enum DEFINED but not pattern-
242// matched -- that needs IR analysis, queued.)
243
244func _sc_axis_sealed_enum(src: *u8, src_len: nx_int) -> nx_int {
245 let p_const_nx: *u8 = "const NX_" as *u8
246 return _sc_count_substr(src, src_len, p_const_nx, 9)
247}
248
249// ---- Axis 4: soup_purity -------------------------------------------
250//
251// IEC 62304 Software Of Unknown Provenance: external dependencies
252// must be license_tier-annotated. Substrate convention: every file
253// header declares `// license_tier: TIER_0_UNENCUMBERED` or
254// `INDEPENDENT_REDERIVE` or `ORIGINAL`. Imports should resolve to
255// other nx_ files (substrate-internal) only.
256//
257// Lexical proxy:
258// - import_count = "import \"" occurrences
259// - tier_decl_count = "license_tier:" occurrences (should be 1)
260// - foreign_imports = imports NOT matching "import \"nx_" pattern
261// (would-be SOUP). Counted by total - nx_-prefixed.
262//
263// Verdict:
264// tier_decl_count >= 1 AND foreign_imports == 0 -> WIN
265// tier_decl_count == 0 -> LOSE (missing tier)
266// foreign_imports > 0 -> LOSE (SOUP)
267//
268// raw_count = foreign_imports.
269
270func _sc_axis_soup_purity(src: *u8, src_len: nx_int, tier_present_out: *nx_int) -> nx_int {
271 let p_import_nx: *u8 = "import \"nx_" as *u8
272 let p_import_any: *u8 = "import \"" as *u8
273 let p_tier: *u8 = "license_tier:" as *u8
274
275 let nx_imports: nx_int = _sc_count_substr(src, src_len, p_import_nx, 11)
276 let all_imports: nx_int = _sc_count_substr(src, src_len, p_import_any, 8)
277 let tier: nx_int = _sc_count_substr(src, src_len, p_tier, 13)
278
279 *tier_present_out = tier
280 let foreign: nx_int = all_imports - nx_imports
281 if foreign < 0 { return 0 }
282 return foreign
283}
284
285// ---- Verdict helpers ------------------------------------------------
286//
287// Uses the natural &card.axis_* syntax, which lands in the substrate
288// via the nx_parse.nx TK_AMP-with-field-chain extension (see commit
289// 6bdc738f). Compileable only through nxc.elf built with the patched
290// parser; the C anchor will reject this file. Per cardinal
291// feedback-no-nxc2-c-extension-only-nishilang-forward, that's the
292// correct direction -- C anchor is for the unextended subset.
293
294func _sc_set_axis(rep: *SafetyAxisReport, axis: nx_int, raw: nx_int, thr: nx_int, verdict: nx_int) -> nx_int {
295 rep.axis = axis
296 rep.raw_count = raw
297 rep.threshold = thr
298 rep.verdict = verdict
299 return verdict
300}
301
302// ---- Public entry: scan source bytes -------------------------------
303
304func nx_safety_critical_scan(src: *u8, src_len: nx_int, card: *SafetyCard) -> nx_int {
305 let unbounded: nx_int = _sc_axis_bounded_loop(src, src_len)
306 var v_bound: nx_int = NX_SC_VERDICT_WIN
307 if unbounded > 0 { v_bound = NX_SC_VERDICT_LOSE }
308 _sc_set_axis(&card.axis_bounded_loop, NX_SC_AXIS_BOUNDED_LOOP, unbounded, 0, v_bound)
309
310 let fn_count_raw: *u8 = sys_mmap(16)
311 let fn_count_p: *nx_int = fn_count_raw as *nx_int
312 *fn_count_p = 0
313 let asserts: nx_int = _sc_axis_assertion_density(src, src_len, fn_count_p)
314 let fns: nx_int = *fn_count_p
315 var v_assert: nx_int = NX_SC_VERDICT_WIN
316 if fns > 0 {
317 if asserts < fns { v_assert = NX_SC_VERDICT_LOSE }
318 }
319 _sc_set_axis(&card.axis_assertion, NX_SC_AXIS_ASSERTION_DENSITY, asserts, fns, v_assert)
320
321 let seal: nx_int = _sc_axis_sealed_enum(src, src_len)
322 var v_seal: nx_int = NX_SC_VERDICT_UNMEASURED
323 if seal >= 3 { v_seal = NX_SC_VERDICT_WIN }
324 _sc_set_axis(&card.axis_sealed_enum, NX_SC_AXIS_SEALED_ENUM, seal, 3, v_seal)
325
326 let tier_present_raw: *u8 = sys_mmap(16)
327 let tier_present_p: *nx_int = tier_present_raw as *nx_int
328 *tier_present_p = 0
329 let foreign: nx_int = _sc_axis_soup_purity(src, src_len, tier_present_p)
330 let tier: nx_int = *tier_present_p
331 var v_soup: nx_int = NX_SC_VERDICT_WIN
332 if tier == 0 { v_soup = NX_SC_VERDICT_LOSE }
333 if foreign > 0 { v_soup = NX_SC_VERDICT_LOSE }
334 _sc_set_axis(&card.axis_soup_purity, NX_SC_AXIS_SOUP_PURITY, foreign, 0, v_soup)
335
336 // Axes 5-8: structurally unevaluable from lexical scan alone.
337 // Queued for IR-level / telemetry-corpus / cross-grader integration.
338 _sc_set_axis(&card.axis_mcdc, NX_SC_AXIS_MCDC_BRANCH, 0, 0, NX_SC_VERDICT_UNMEASURED)
339 _sc_set_axis(&card.axis_fault_inj, NX_SC_AXIS_FAULT_INJECTION, 0, 0, NX_SC_VERDICT_UNMEASURED)
340 _sc_set_axis(&card.axis_hazard_reg, NX_SC_AXIS_HAZARD_REGISTER, 0, 0, NX_SC_VERDICT_UNMEASURED)
341 _sc_set_axis(&card.axis_iv_and_v, NX_SC_AXIS_IV_AND_V_COUNT, 0, 0, NX_SC_VERDICT_UNMEASURED)
342
343 var win: nx_int = 0
344 var lose: nx_int = 0
345 var unmeasured: nx_int = 0
346
347 if card.axis_bounded_loop.verdict == NX_SC_VERDICT_WIN { win = win + 1 }
348 if card.axis_bounded_loop.verdict == NX_SC_VERDICT_LOSE { lose = lose + 1 }
349 if card.axis_bounded_loop.verdict == NX_SC_VERDICT_UNMEASURED { unmeasured = unmeasured + 1 }
350
351 if card.axis_assertion.verdict == NX_SC_VERDICT_WIN { win = win + 1 }
352 if card.axis_assertion.verdict == NX_SC_VERDICT_LOSE { lose = lose + 1 }
353 if card.axis_assertion.verdict == NX_SC_VERDICT_UNMEASURED { unmeasured = unmeasured + 1 }
354
355 if card.axis_sealed_enum.verdict == NX_SC_VERDICT_WIN { win = win + 1 }
356 if card.axis_sealed_enum.verdict == NX_SC_VERDICT_LOSE { lose = lose + 1 }
357 if card.axis_sealed_enum.verdict == NX_SC_VERDICT_UNMEASURED { unmeasured = unmeasured + 1 }
358
359 if card.axis_soup_purity.verdict == NX_SC_VERDICT_WIN { win = win + 1 }
360 if card.axis_soup_purity.verdict == NX_SC_VERDICT_LOSE { lose = lose + 1 }
361 if card.axis_soup_purity.verdict == NX_SC_VERDICT_UNMEASURED { unmeasured = unmeasured + 1 }
362
363 // Axes 5-8 are UNMEASURED.
364 unmeasured = unmeasured + 4
365
366 card.n_win = win
367 card.n_lose = lose
368 card.n_unmeasured = unmeasured
369
370 if lose > 0 {
371 card.overall_verdict = NX_SC_VERDICT_LOSE
372 } else {
373 if unmeasured == 0 {
374 card.overall_verdict = NX_SC_VERDICT_WIN_S
375 } else {
376 card.overall_verdict = NX_SC_VERDICT_WIN
377 }
378 }
379 return card.overall_verdict
380}
381
382// ---- File-level helper ---------------------------------------------
383
384func nx_safety_critical_scan_file(path: *u8, card: *SafetyCard) -> nx_int {
385 let len_raw: *u8 = sys_mmap(16)
386 let len_p: *i64 = len_raw as *i64
387 let src: *u8 = sys_read_file(path, len_p)
388 if src == (0 as *u8) {
389 card.n_win = 0
390 card.n_lose = 0
391 card.n_unmeasured = NX_SC_AXIS_N
392 card.overall_verdict = NX_SC_VERDICT_UNMEASURED
393 return NX_SC_VERDICT_UNMEASURED
394 }
395 let src_len: nx_int = len_p[0]
396 return nx_safety_critical_scan(src, src_len, card)
397}
398
399// ---- Named-improvement string per axis -----------------------------
400
401func nx_safety_critical_named_improvement(axis: nx_int) -> *u8 {
402 if axis == NX_SC_AXIS_BOUNDED_LOOP {
403 return "JPL Rule 2 / IEC 61508 SIL termination: replace `while keep == 1` / `while 1` / `while true` with `var iter; iter < BUDGET` (see runtime/nx_loop.nx)" as *u8
404 }
405 if axis == NX_SC_AXIS_ASSERTION_DENSITY {
406 return "JPL Rule 5: bring assertion density to >= 1 per function (substrate target), >= 2 per function (full JPL). Use nx_assert_* / sealed-verdict returns / Result::Err" as *u8
407 }
408 if axis == NX_SC_AXIS_SEALED_ENUM {
409 return "DO-178C formal-method equivalent: declare error paths via `const NX_*_VERDICT_*` sealed-enum constants instead of magic numbers" as *u8
410 }
411 if axis == NX_SC_AXIS_SOUP_PURITY {
412 return "IEC 62304 SOUP minimisation: declare `// license_tier: ORIGINAL|INDEPENDENT_REDERIVE|TIER_0_UNENCUMBERED` in file header. All imports must resolve to substrate-internal nx_* files" as *u8
413 }
414 if axis == NX_SC_AXIS_MCDC_BRANCH {
415 return "DO-178C DAL A MCDC coverage: per-decision independent-effect tracking. Requires IR-level analysis; queued for substrate self-host pipeline integration" as *u8
416 }
417 if axis == NX_SC_AXIS_FAULT_INJECTION {
418 return "IEC 61508 diagnostic coverage: requires telemetry corpus from bench harness FAILURE/LATENT-FAULT axis (queued in racing-crew roadmap)" as *u8
419 }
420 if axis == NX_SC_AXIS_HAZARD_REGISTER {
421 return "ISO 26262 HARA / MIL-STD-882 hazard register: cross-reference primitive against nishi-library/seeds/cross-language-bug-tapes.toml entries (queued)" as *u8
422 }
423 if axis == NX_SC_AXIS_IV_AND_V_COUNT {
424 return "NASA-STD-8719 IV&V: count of independent grader perspectives that have evaluated this primitive (heptagulation -> octagulation roll-up; queued)" as *u8
425 }
426 return "" as *u8
427}
428
429func nx_safety_critical_card_alloc() -> *SafetyCard {
430 let raw: *u8 = sys_mmap(512)
431 let c: *SafetyCard = raw as *SafetyCard
432 return c
433}