code wiki / (root) / nx_safety.nx

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}