nx_safety.nx source
↩ module page · 233 lines · 9343 B
1// nx_safety.nx -- SafetyEnvelope as a native NishiLang construct.
2//
3// Per cardinal feedback-safety-envelope-native-language-feature
4// (user 2026-05-16: "just make it metaprogramming or whatever and
5// part of what nishilang does natively"), the safety envelope is
6// a STRUCTURED DATA TYPE, not a comment-block convention. Every
7// substrate module declares:
8//
9// import "nx_safety.nx"
10//
11// const _SAFETY_ENVELOPE: SafetyEnvelope = SafetyEnvelope {
12// sil_target: SIL_2,
13// asil_target: ASIL_QM,
14// dal_target: DAL_B,
15// iec_62304_class: IEC_62304_NONE,
16// evidence_ids: [EVID_NO_FP, EVID_SEALED_ENUM] as *i64,
17// n_evidence_ids: 2,
18// hazard_ids: [HAZ_CACHE_TIMING_AES] as *i64,
19// n_hazard_ids: 1,
20// residual_risk: "S-box cache-timing per Bernstein 2005" as *u8,
21// residual_risk_len: 38,
22// verdict: NX_VERDICT_NOT_YET_EVALUATED,
23// }
24//
25// The grader (nx_safety_critical_grade.nx) consumes the const
26// directly -- typed introspection, no comment scan. Future
27// compilers extend this via NishiLang's existing struct/const
28// machinery without parser changes.
29//
30// Companion catalog: nishi-library/seeds/safety-critical-standards.toml
31//
32// license_tier: ORIGINAL
33// genealogy_id: substrate-native synthesis of IEC 61508 / ISO 26262 /
34// DO-178C / IEC 62304 / NASA-STD-8719.13 / MIL-STD-882E
35// + NASA JPL Power of 10
36
37import "nx_syscalls.nx"
38
39// ===== Sealed enums =================================================
40
41// IEC 61508 Safety Integrity Levels. SIL4 = highest target on
42// E/E/PE systems. SIL_NONE = primitive does not claim a SIL.
43const SIL_NONE: i64 = 0
44const SIL_1: i64 = 1
45const SIL_2: i64 = 2
46const SIL_3: i64 = 3
47const SIL_4: i64 = 4
48
49// ISO 26262 Automotive Safety Integrity Levels. ASIL_QM = below
50// the safety-relevant threshold (quality-managed). ASIL_D = highest.
51const ASIL_QM: i64 = 0
52const ASIL_A: i64 = 1
53const ASIL_B: i64 = 2
54const ASIL_C: i64 = 3
55const ASIL_D: i64 = 4
56
57// DO-178C Software Development Assurance Levels. DAL_E = no
58// effect (lowest rigor); DAL_A = catastrophic (highest rigor).
59const DAL_NONE: i64 = 0
60const DAL_E: i64 = 1
61const DAL_D: i64 = 2
62const DAL_C: i64 = 3
63const DAL_B: i64 = 4
64const DAL_A: i64 = 5
65
66// IEC 62304 medical-device software safety classes. A = no injury
67// possible; C = death or serious injury possible.
68const IEC_62304_NONE: i64 = 0
69const IEC_62304_A: i64 = 1
70const IEC_62304_B: i64 = 2
71const IEC_62304_C: i64 = 3
72
73// Sealed-enum grader verdict. Substrate consumers (graders, bench
74// harness, racing-crew telemetry) read this field. WIN_S_UNANIMOUS
75// requires all 8 grader axes PASS + zero UNMEASURED.
76const NX_VERDICT_NOT_YET_EVALUATED: i64 = 0
77const NX_VERDICT_PASS: i64 = 1
78const NX_VERDICT_FAIL: i64 = 2
79const NX_VERDICT_WIN_S_UNANIMOUS: i64 = 3
80
81// ===== Canonical evidence-id tokens =================================
82//
83// The substrate's standard set of evidence types a primitive can
84// claim. Each ID corresponds to a verifiable property; the grader
85// validates by running the corresponding check. When new evidence
86// types ship, add a const here + extend the grader's dispatch
87// table.
88
89const EVID_NO_FP: i64 = 1 // no floating-point arithmetic
90const EVID_SEALED_ENUM_COMPLETE: i64 = 2 // all verdict paths sealed-enum
91const EVID_BOUNDED_LOOPS: i64 = 3 // JPL Rule 2: every while bounded
92const EVID_NO_RECURSION: i64 = 4 // JPL Rule 1
93const EVID_ASSERTION_DENSITY: i64 = 5 // JPL Rule 5: >=2/fn
94const EVID_BIT_EQUAL_REPRODUCIBLE: i64 = 6 // deterministic across runs
95const EVID_NO_TABLE_LOOKUP_ON_SECRET: i64 = 7 // constant-time crypto
96const EVID_CONSTANT_TIME_BY_DESIGN: i64 = 8 // no secret-dep branches
97const EVID_KAT_VERIFIED: i64 = 9 // known-answer-test pass
98const EVID_LICENSE_TIER_ORIGINAL: i64 = 10 // original work
99const EVID_LICENSE_TIER_INDEPENDENT_REDERIVE: i64 = 11
100const EVID_LICENSE_TIER_TIER_0_UNENCUMBERED: i64 = 12
101const EVID_FORMAL_PROOF_THEOREM: i64 = 13 // theorem with full proof
102const EVID_FAULT_INJECTION_SURVIVED: i64 = 14 // chaos test pass
103const EVID_ICL_AUDIT_PASSED: i64 = 15 // capability-claims audit
104const EVID_KIND_ISOLATED: i64 = 16 // no sibling-kind imports
105const EVID_BACKTRACKING_RESISTANCE: i64 = 17 // CSPRNG specific
106const EVID_NONCE_UNIQUENESS_DOC: i64 = 18 // crypto caller-contract documented
107const EVID_FIPS_TEST_VECTORS: i64 = 19 // NIST CAVS / FIPS validated
108const EVID_RFC_TEST_VECTORS: i64 = 20 // RFC appendix vectors validated
109
110// ===== Canonical hazard-id tokens ===================================
111//
112// References to bug-tape entries. Each ID points at an entry in
113// nishi-library/seeds/cross-language-bug-tapes.toml + per-domain
114// catalogs. When a primitive's envelope lists a hazard, it
115// asserts the implementation DEFENDS against that hazard.
116
117const HAZ_CACHE_TIMING_AES_SBOX: i64 = 1
118const HAZ_NONCE_REUSE_DISCLOSURE: i64 = 2
119const HAZ_LENGTH_EXTENSION_HASH: i64 = 3
120const HAZ_PADDING_ORACLE: i64 = 4
121const HAZ_MAC_NONCONSTANT_TIME_COMPARE: i64 = 5
122const HAZ_NULL_DEREF_UNCHECKED: i64 = 6
123const HAZ_INTEGER_OVERFLOW_SILENT: i64 = 7
124const HAZ_INFINITE_LOOP_UNBOUNDED: i64 = 8
125const HAZ_STACK_OVERFLOW_RECURSION: i64 = 9
126const HAZ_USE_AFTER_FREE: i64 = 10
127const HAZ_DOUBLE_FREE: i64 = 11
128const HAZ_RACE_CONDITION_TOCTOU: i64 = 12
129const HAZ_INJECTION_VIA_UNESCAPED: i64 = 13
130const HAZ_XSS_HTML_ATTRIBUTE: i64 = 14
131const HAZ_CSRF_NO_TOKEN: i64 = 15
132const HAZ_DNS_CACHE_POISONING: i64 = 16
133const HAZ_DOWNGRADE_ATTACK: i64 = 17
134const HAZ_SUPPLY_CHAIN_HASH_COLLISION: i64 = 18
135const HAZ_AI_ALIGNMENT_MISUSE: i64 = 19
136const HAZ_SIDE_CHANNEL_FAULT_INJECTION: i64 = 20
137
138// ===== The struct ===================================================
139//
140// Fixed-shape, fixed-stride. All variable-length fields are
141// pointer + length pairs so the const declaration is the SINGLE
142// source of truth for size, with no realloc / heap.
143
144struct SafetyEnvelope {
145 sil_target: i64, // SIL_*
146 asil_target: i64, // ASIL_*
147 dal_target: i64, // DAL_*
148 iec_62304_class: i64, // IEC_62304_*
149 n_evidence_ids: i64,
150 evidence_ids: *i64, // array of EVID_*
151 n_hazard_ids: i64,
152 hazard_ids: *i64, // array of HAZ_*
153 residual_risk_len: i64,
154 residual_risk: *u8, // free-form bytes, length-prefixed
155 verdict: i64, // NX_VERDICT_*
156}
157
158// ===== Helper: query a module's envelope ============================
159//
160// Future graders use this surface to introspect. v1 substrate
161// has no reflection API; callers wire `_SAFETY_ENVELOPE` by name.
162// When the substrate compiler grows reflection (queued), this
163// helper becomes the canonical entry.
164
165// Validate a SafetyEnvelope struct's field values for consistency.
166// Returns 1 on PASS, 0 on FAIL. Used by graders to refuse
167// malformed envelope declarations at audit time.
168func nx_safety_envelope_is_valid(e: *SafetyEnvelope) -> i64 {
169 if e.sil_target < 0 { return 0 }
170 if e.sil_target > 4 { return 0 }
171 if e.asil_target < 0 { return 0 }
172 if e.asil_target > 4 { return 0 }
173 if e.dal_target < 0 { return 0 }
174 if e.dal_target > 5 { return 0 }
175 if e.iec_62304_class < 0 { return 0 }
176 if e.iec_62304_class > 3 { return 0 }
177 if e.verdict < 0 { return 0 }
178 if e.verdict > 3 { return 0 }
179 if e.n_evidence_ids < 0 { return 0 }
180 if e.n_hazard_ids < 0 { return 0 }
181 if e.residual_risk_len < 0 { return 0 }
182 return 1
183}
184
185// ===== Self-test ====================================================
186//
187// Smoke that demonstrates the native declaration pattern + validates
188// it through nx_safety_envelope_is_valid.
189
190func main() -> i64 {
191 let evid_raw: *u8 = sys_mmap(32)
192 let evid: *i64 = evid_raw as *i64
193 evid[0] = EVID_NO_FP
194 evid[1] = EVID_SEALED_ENUM_COMPLETE
195
196 let haz_raw: *u8 = sys_mmap(16)
197 let haz: *i64 = haz_raw as *i64
198 haz[0] = HAZ_NULL_DEREF_UNCHECKED
199
200 let e_raw: *u8 = sys_mmap(128)
201 let e: *SafetyEnvelope = e_raw as *SafetyEnvelope
202 e.sil_target = SIL_2
203 e.asil_target = ASIL_QM
204 e.dal_target = DAL_B
205 e.iec_62304_class = IEC_62304_NONE
206 e.n_evidence_ids = 2
207 e.evidence_ids = evid
208 e.n_hazard_ids = 1
209 e.hazard_ids = haz
210 e.residual_risk_len = 0
211 e.residual_risk = 0 as *u8
212 e.verdict = NX_VERDICT_NOT_YET_EVALUATED
213
214 if nx_safety_envelope_is_valid(e) != 1 {
215 return __syscall(93, 1, 0, 0, 0, 0, 0)
216 }
217
218 // Out-of-range SIL -> fail.
219 e.sil_target = 99
220 if nx_safety_envelope_is_valid(e) != 0 {
221 return __syscall(93, 2, 0, 0, 0, 0, 0)
222 }
223 e.sil_target = SIL_2
224
225 // Out-of-range verdict -> fail.
226 e.verdict = 99
227 if nx_safety_envelope_is_valid(e) != 0 {
228 return __syscall(93, 3, 0, 0, 0, 0, 0)
229 }
230 e.verdict = NX_VERDICT_NOT_YET_EVALUATED
231
232 return 0
233}