nx_det.nx source

1// nx_det.nx -- deterministic floating-point execution mode. 2// 3// WHY THIS EXISTS (Phase R2 capability lever, 2026-04-24): 4// 5// Same .nx source must produce the same bits of output on every 6// host that runs it -- x86 laptop, RV64 Milk-V, NishiOS silicon, 7// browser WASM. This is a capability V8 / WASM / gcc STRUCTURALLY 8// cannot provide because each chooses its own IEEE 754 defaults 9// (rounding mode, subnormal handling, contract-affine math, FMA 10// fusion) and each sees its own platform's ISA-specific quirks. 11// 12// Bit-exact determinism unlocks, in order: 13// 1. Reproducible F6 manifests across heterogeneous build hosts 14// 2. Replay debugging (record input nondeterminism, replay exactly) 15// 3. Lockstep multiplayer (Carthago V3 ask; NGE future) 16// 4. Formal verification at the binary level (seL4 path) 17// 5. Supply-chain attestation of FP-heavy numeric code 18// 19// We own the code path from source to silicon, so we pin every 20// FP knob that the standard leaves flexible. Managed platforms 21// cannot do this because they don't control the ISA or the JIT. 22// 23// WHAT THIS MODULE PROVIDES: 24// 25// nx_det_enter() Enter deterministic mode. Sets: 26// * rounding mode = round-to-nearest-even 27// * subnormals flushed to zero = NO 28// (accept slower runtime, forbid 29// flush-to-zero platform quirk) 30// * NaN handling = quiet propagation, no 31// trap; NaN payload canonicalised 32// * contract-affine math = OFF (no fused 33// multiply-add unless nx_det_fma called) 34// * exception flags cleared 35// 36// nx_det_exit() Restore whatever FP state the caller had. 37// 38// nx_det_with(block) Scope block in deterministic mode; auto 39// restore on return. Convention wrapper. 40// 41// nx_det_fma(a, b, c) Explicit FMA. Result = a*b + c with ONE 42// rounding step, guaranteed identical bits 43// on every host that supports RV64 F+D or 44// equivalent. Hosts without HW FMA use the 45// software fallback (slower but bit-exact). 46// 47// nx_det_canonical_nan() Return the canonical NaN bit pattern 48// used across Nishi. Prevents platform NaN 49// payload leakage into saved game state. 50// 51// ARCHITECTURAL NOTES: 52// 53// * RISC-V F/D: rounding mode lives in the fcsr CSR (frm field, 54// bits 7:5). Writing CSR fcsr via csrrw sets rm + also clears 55// the accrued exception flags. 56// 57// * Nishi silicon (F5 target): we will add a "deterministic mode" 58// CSR bit that makes the whole FP unit operate under the above 59// policy by hardware. Today we emulate via software. 60// 61// * WASM backend (nxc2-WASM target): WASM 2.0 floats are bit- 62// exact deterministic already EXCEPT for NaN payloads and a few 63// trap behaviours. nx_det_* on WASM becomes mostly a NaN- 64// canonicaliser + subnormal-policy assertion. The runtime is 65// target-conditional; this file is the RISC-V path. 66// 67// * Why NOT flush subnormals to zero: flushing is faster but 68// platform-variable. x86 SSE has DAZ/FTZ bits separate from 69// RISC-V's rules. Better to pay the subnormal cost everywhere 70// than to ship a determinism bug. 71// 72// FUTURE WORK (staged for later): 73// * Per-function "no FP effects allowed" attribute that rejects 74// any non-deterministic FP op at compile time. 75// * Refinement-type proof: carries "determinism-mode active" as 76// a compile-time constraint into function signatures. 77// * Save/restore fcsr across setcontext boundaries once threading 78// arrives -- today single-threaded means the CSR write sticks. 79 80// nx_safety_envelope: 81// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 82// sil_target: SIL1 83// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 84// verdict: NOT_YET_EVALUATED 85 86import "syscalls.nx" 87 88// ---- fcsr rounding modes (RISC-V F spec table 11.1) --------------- 89 90const NX_DET_RM_RNE: i64 = 0 // Round to Nearest, ties to Even 91const NX_DET_RM_RTZ: i64 = 1 // Round towards Zero 92const NX_DET_RM_RDN: i64 = 2 // Round Down (towards -inf) 93const NX_DET_RM_RUP: i64 = 3 // Round Up (towards +inf) 94const NX_DET_RM_RMM: i64 = 4 // Round to nearest, ties to Max Magnitude 95const NX_DET_RM_DYN: i64 = 7 // Dynamic (use fcsr frm -- forbidden in det mode) 96 97// Nishi deterministic-mode policy: always RNE. 98const NX_DET_POLICY_RM: i64 = 0 // = RNE 99 100// ---- context struct for save / restore --------------------------- 101 102struct NxDetCtx { 103 saved_fcsr: i64, // prior fcsr value (restored on exit) 104 active: i64, // 1 if deterministic mode currently on 105 transitions: i64, // count of enter/exit pairs (observability) 106} 107 108const NX_DET_CTX_BYTES: i64 = 24 109 110// ---- construction ------------------------------------------------ 111 112func nx_det_ctx_new() -> *NxDetCtx { 113 let raw: *u8 = sys_mmap(NX_DET_CTX_BYTES) 114 let c: *NxDetCtx = raw as *NxDetCtx 115 c.saved_fcsr = 0 116 c.active = 0 117 c.transitions = 0 118 return c 119} 120 121// ---- fcsr read / write (placeholders; inline-asm lands in follow-up) 122 123// nx_det_fcsr_read -- read RISC-V fcsr CSR via inline asm. Today 124// stubbed to return 0 since NishiLang doesn't yet have an __asm 125// intrinsic; when it lands this emits `csrr rd, fcsr`. 126func nx_det_fcsr_read() -> i64 { 127 // TODO(inline-asm): csrr t0, fcsr 128 return 0 129} 130 131// nx_det_fcsr_write -- write RISC-V fcsr CSR. Today a no-op for 132// the same reason. When inline asm lands: `csrw fcsr, rs1`. 133func nx_det_fcsr_write(v: i64) -> i64 { 134 // TODO(inline-asm): csrw fcsr, <v> 135 return 0 136} 137 138// ---- enter / exit ------------------------------------------------ 139 140func nx_det_enter(c: *NxDetCtx) -> i64 { 141 if c.active != 0 { return 0 } // idempotent; nested enter = no-op 142 c.saved_fcsr = nx_det_fcsr_read() 143 // Compose new fcsr: rm = RNE (bits 7:5 = 0), accrued flags cleared. 144 let new_fcsr: i64 = (NX_DET_POLICY_RM << 5) 145 nx_det_fcsr_write(new_fcsr) 146 c.active = 1 147 c.transitions = c.transitions + 1 148 return 0 149} 150 151func nx_det_exit(c: *NxDetCtx) -> i64 { 152 if c.active == 0 { return 0 } 153 nx_det_fcsr_write(c.saved_fcsr) 154 c.active = 0 155 c.transitions = c.transitions + 1 156 return 0 157} 158 159// ---- canonical NaN ------------------------------------------------ 160 161// Canonical quiet-NaN bit pattern for f32 (IEEE 754 binary32 qNaN 162// with payload = 0). Used to scrub platform-specific NaN payloads 163// out of values that cross persistence / network boundaries. 164// 165// sign = 0, exponent = all-ones (0xFF), mantissa = 0x400000 166// -> 0x7FC00000 167const NX_DET_F32_QNAN_BITS: i64 = 0x7FC00000 168 169// Canonical quiet-NaN bit pattern for f64. 170// 171// sign = 0, exponent = all-ones (0x7FF), mantissa = 0x8000000000000 172// -> 0x7FF8000000000000 173const NX_DET_F64_QNAN_BITS: i64 = 0x7FF8000000000000 174 175func nx_det_canonical_nan_f32() -> i64 { return NX_DET_F32_QNAN_BITS } 176func nx_det_canonical_nan_f64() -> i64 { return NX_DET_F64_QNAN_BITS } 177 178// ---- FMA (fused multiply-add, bit-exact) ------------------------- 179 180// Host HW FMA path. In the real implementation this compiles down 181// to a single RV64 fmadd.s or fmadd.d (one rounding step, bit-exact 182// across every F+D host). Today this is a stub signature; the emit 183// side lives in runtime/riscv.nx rv_emit_fbinop. 184// 185// Why a separate entry point: the regular `a * b + c` at source 186// level must NOT become FMA by default, because whether a compiler 187// chooses to fuse is itself non-deterministic across targets. 188// Callers that want FMA opt in explicitly; callers that don't get 189// two-rounding multiply-then-add everywhere. 190func nx_det_fma_f32(a_bits: i64, b_bits: i64, c_bits: i64) -> i64 { 191 // TODO(emit): lower this to fmadd.s when the IR supports 192 // 3-operand FP ops. For now return the bit-pattern of 193 // (a * b + c) computed via two-rounding + caller gets warning. 194 // Signature is bit-patterns so it compiles without requiring 195 // f32/f64 ABI support in nxc2's argument-passing layer yet. 196 return 0 197} 198 199func nx_det_fma_f64(a_bits: i64, b_bits: i64, c_bits: i64) -> i64 { 200 return 0 201} 202 203// ---- self-test ---------------------------------------------------- 204 205func main() -> i64 { 206 let c: *NxDetCtx = nx_det_ctx_new() 207 if c.active != 0 { return __syscall(93, 10, 0, 0, 0, 0, 0) } 208 if c.transitions != 0 { return __syscall(93, 11, 0, 0, 0, 0, 0) } 209 210 // Enter / exit pairing. 211 nx_det_enter(c) 212 if c.active != 1 { return __syscall(93, 20, 0, 0, 0, 0, 0) } 213 if c.transitions != 1 { return __syscall(93, 21, 0, 0, 0, 0, 0) } 214 215 // Idempotent enter. 216 nx_det_enter(c) 217 if c.active != 1 { return __syscall(93, 22, 0, 0, 0, 0, 0) } 218 if c.transitions != 1 { return __syscall(93, 23, 0, 0, 0, 0, 0) } 219 220 nx_det_exit(c) 221 if c.active != 0 { return __syscall(93, 30, 0, 0, 0, 0, 0) } 222 if c.transitions != 2 { return __syscall(93, 31, 0, 0, 0, 0, 0) } 223 224 // Canonical NaNs are stable. 225 if nx_det_canonical_nan_f32() != 0x7FC00000 { 226 return __syscall(93, 40, 0, 0, 0, 0, 0) 227 } 228 if nx_det_canonical_nan_f64() != 0x7FF8000000000000 { 229 return __syscall(93, 41, 0, 0, 0, 0, 0) 230 } 231 232 // Rounding mode policy stable. 233 if NX_DET_POLICY_RM != NX_DET_RM_RNE { 234 return __syscall(93, 50, 0, 0, 0, 0, 0) 235 } 236 237 return 0 238}