The Determinism Contract

MIND is deterministic. The same source code, the same inputs, the same compiler/runtime version, and the same target settings produce the same output — every time, on every conforming implementation.

This is not a claim that every mathematical question has one truth. It is a claim that the language defines one exact behaviour for every operation and never leaves the result to accident — to undefined behaviour, backend quirks, hidden global state, race conditions, or the order a parallel runtime happens to execute in.

Every questionable operation falls into exactly one bucket:

  • define — the spec picks one rule; the operation always produces that result.
  • reject — a compile error or a defined domain error.
  • mark non-deterministic — explicitly opted into a fast / unordered mode the spec labels non-deterministic.

The forbidden fourth bucket — “sometimes 1, sometimes 0, sometimes NaN, depending on backend / GPU / optimization level” — does not exist in MIND.

Status, honestly: ✅ shipped means implemented and gated in CI today. 📋 specified — enforcement in progress means the rule is fixed by this contract and we are working towards full enforcement. We do not claim a behaviour is enforced before it is.

Verifiable, not promised

Determinism in MIND is checkable. Each artifact embeds an evidence chain whose trace_hash = SHA-256 of the canonical mic@3 bytes. Identical (source, inputs, version, target) ⇒ identical trace_hash. mindc verify ./artifact confirms it without trusting the build host. ✅ shipped

A plain verify reports; a consumer that needs a guarantee opts into a fail-closed gate. Each of these exits non-zero rather than passing quietly ✅ shipped:

  • --require-strict-fp — rejects unless the artifact’s FP-contract mode is strict (no FMA-contraction, no f32 reduction reassociation). Fails closed on relaxed, on unknown, and on an unattested artifact.
  • --require-deterministic — rejects unless the artifact calls no PRNG / wall-clock / stdin builtin.
  • --require-signed / --signer-pubkey <hex> — rejects an unsigned artifact, or one signed by a key outside a pinned allowlist.
  • --json — one stable receipt shape on every exit path; a property that could not be established is an explicit null/false, never a missing key.

Both mode fields are re-derived from the hashed mic@3 body, not read out of the metadata epilogue — so on an unsigned artifact a forged deterministic or strict label cannot pass. ✅ shipped

Verification is honest about its own limits. trace_hash covers the IR body, so an unsigned artifact is tamper-evident at tier 1 (IR body attested) while its provenance fields are not authenticatedat tier 2. The signing engine ships — the production scheme is post-quantum: ML-DSA-87 (FIPS-204) AND SLH-DSA-SHAKE-256s (FIPS-205), both legs required, compiled in via the evidence-mldsa and evidence-slhdsa build features (off by default). Ed25519 and the older Ed25519 / ML-DSA-65 hybrid are retired from signing and trust verification and survive only as legacy read tags that are not PQC-compliant. Signing is opt-in via an operator-supplied key seed and never enabled by default; an unsigned artifact stays byte-identical to the pre-signing encoder, with no IR-version bump. See Security.

1. Integer semantics ✅ shipped

Fully deterministic and byte-identical across substrates.

  • x / 0 = 0 and x % 0 = 0 — defined; no trap, no UB.
  • INT_MIN / -1 = INT_MIN — defined; no overflow trap.
  • Integer overflow wraps two’s-complement — identical on x86 and ARM.
  • Oversized shift (count ≥ bit-width) is given a defined result, never UB.
  • Condition truthiness: if c tests c != 0 — the whole value, not the low bit.

2. Floating-point semantics

MIND follows IEEE 754 and pins every edge case. The Q16.16 fixed-point tier is fully deterministic and byte-identical across substrates today ✅ shipped.

Strict floating-point output identity is gated for three committed workloads on x86_64 AVX2 and ARM64 NEON: the scalar f64 chain, length-4093 f32 dot, and 64×64 f32 matrix-vector product. Their exact output hashes and arithmetic sequences are documented in RFC 0015 section 5A. ✅ shippedThe Lorenz visualization illustrates sensitivity to floating-point evaluation order; it is separate from that committed fixture corpus. The earlier x86/GPU demonstration has no reproducible receipt linked here and is not evidence of supported GPU identity. Wider input coverage, transcendentals, and GPU workloads need their own validation. 📋 specified — enforcement in progress

The remaining IEEE edge cases are fixed by this contract 📋 specified — enforcement in progress:

  • 1.0 / 0.0 = +Inf, -1.0 / 0.0 = -Inf, 0.0 / 0.0 = NaN (IEEE).
  • sqrt(-1.0) = NaN (IEEE); strict_domain → a defined domain error.
  • NaN comparisons are all false except !=; min/max/sort use a defined total order (NaN sorts last) so results are deterministic.
  • Rounding is round-to-nearest-even (IEEE default), fixed.

0^0 — worked example

0^0is the canonical “vague” case. MIND removes the vagueness by choosing the function, not the mood:

pow(0, 0)        // 1     — integer / exact arithmetic, deterministic
pow(0.0, 0.0)    // 1.0   — IEEE pow, deterministic (x^0 == 1 for all x)
powr(0.0, 0.0)   // NaN   — IEEE powr (real power), deterministic
limit_form(0^0)  //        indeterminate — symbolic/calculus, not a runtime number

pow(0,0) = 1 matches the empty-product convention and every mainstream language, and keeps polynomial / tensor x^0 well-behaved. powr is the honestly-NaN real power. Both are deterministic — you pick which one. Mathematically honest and never an accident. 📋 specified — enforcement in progress

3. The backend must not change meaning

Two execution tiers. The contract is bit-identity, never “within tolerance” — tolerance-equal is a correctness-testing notion, not a determinism guarantee.

  • Strict tier (default). Committed integer, Q16.16, and three strict f32/f64 fixtures have matching computational output hashes on x86 AVX2 and ARM NEON. ✅ shipped Fixed operation and accumulation order preserve the admitted arithmetic contract. The fixture corpus does not prove every floating-point program or input, and it contains no GPU CI arm. General reductions, transcendentals, and additional substrates remain explicit validation work. 📋 specified — enforcement in progress
  • Fast tier (opt-in). Explicitly labelled non-deterministic; results may differ by substrate. You opt into it — you never get it by accident.

GPU and accelerator execution (CUDA, Metal, ROCm, WebGPU) ships in the commercial mind-runtime; bit-identical determinism across those substrates is on the roadmap. The open-source mindc emits for the CPU.

4. Parallel execution must not randomise results

For floating-point, (a + b) + c != a + (b + c). A parallel runtime that reorders a reduction can change the result. MIND’s rule: strict is the default (defined reduction order / stable kernel, reproducible regardless of thread or lane count); fast is opt-in and labelled non-deterministic.

sum(x)                 // strict: defined reduction order, reproducible
sum(x, mode = "fast")  // explicitly non-deterministic

Fixed-reduction-order kernels are the active work. 📋 specified — enforcement in progress

5. Compiler optimizations cannot change observable behaviour

  • strict_math (default). No x * 0 → 0 (because NaN * 0 = NaN, Inf * 0 = NaN), no reassociation, no FMA-contraction. NaN, Inf, and rounding are preserved exactly.
  • fast_math (opt-in). Permits those rewrites; the spec labels the result non-deterministic.

The native-ELF backend emits an image that is a pure function of the IR — there is no external toolchain whose -ffast-math can leak in. ✅ shipped The strict_math / fast_math surface is being finalised. 📋 specified — enforcement in progress

#[collapse] — an optimization that proves it preserves behaviour ✅ shipped

The sharpest form of “an optimization cannot change observable behaviour” is one that carries its own proof. A #[collapse] annotation on a counted forloop replaces the whole loop with its exact closed form at compile time — O(n) becomes O(1) — and the result is bit-identical to running the loop. It is a prove-or-fail contract: a loop the compiler cannot prove collapsible is a compile error (E2201–E2215), never a silent constant.

  • acc = acc + (A*i + B) → the ring-exact Gauss sum in Z/2^64.
  • acc = acc * R → acc * Rⁿ via a fixed 64-step square-and-multiply.
  • x = f(x) → the bit-exact fixed point of a Q16.16 contraction. The fold evaluates the program’s own function bodies, so collapse == loop holds by construction: a program that redefines the map differently is rejected, not miscompiled.

Because every collapse is exact integer / Q16.16 arithmetic with no float reassociation, the folded constant is byte-identical across x86, ARM, and mic@3— it moves no cross-substrate canary. Each fold also records a receipt in the evidence MAP outside the trace_hash preimage, and mindc verify independently re-derives the constant by exact integer arithmetic, failing on a forged constant or tampered parameters. ✅ shipped This requires a determinism contract on the arithmetic itself; a float compiler cannot do it.

6. Randomness must be explicit

There is no implicit rand() reading hidden global state. Randomness is always seeded and explicit:

let rng = Random(seed = 42)
let x   = rng.normal(shape = [1024])   // same seed => same tensor, every run

The generator is counter-based (Philox / Threefry), keyed by (seed, element_index). Because each element’s draw is a stateless function of its index, parallel generation is reproducible regardless of execution order, and the result is identical across substrates. This is the basis of MIND’s reproducible-across-hardware randn. 📋 specified — enforcement in progress

Non-determinism never leaks untraced ✅ shipped

MIND is a systems language, so it cancompile a genuinely non-deterministic program — an unseeded PRNG draw, a wall-clock read, a stdin read. Such a program is neither silently accepted nor silently rejected. It is a traced, attested opt-in across three layers:

  • Build gate. Emitting a runnable or attested artifact from such a program is rejected fail-loud, naming the offending builtin and pointing at the seeded Random(seed = 42) API — unless you pass --allow-nondeterministic.
  • Honest attestation. With the flag the program compiles, and its evidence_chain.determinism field — derived from the IR — declares nondeterministic. The flag authorises the build; it never touches the label.
  • Verify re-derivation. mindc verify re-derives the mode from the hashed body and fails closed if the stored field disagrees, so a forged deterministic label cannot pass on an unsigned artifact.

The classifier is machine-checked, not a prose list: every __mind_* primitive carries its determinism class on the same registry row as its name, so a newly added clock or entropy primitive cannot be admitted as deterministic by omission.

In one sentence

MIND does not depend on undefined behaviour, backend quirks, hidden randomness, race conditions, or accidental execution order. Every questionable case is either precisely defined, explicitly rejected, or explicitly marked non-deterministic — and the result is verifiable through the artifact’s trace_hash.

The normative source is determinism.md in star-ga/mind-spec.