Standardize checked fixed-point math on Bunny

.github/workflows/ci.yml

@@ -20,8 +20,8 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - rust-version: "1.95.0"
-            rust-label: "msrv 1.95.0"
+          - rust-version: "1.96.0"
+            rust-label: "msrv 1.96.0"
           - rust-version: stable
             rust-label: "stable"
     steps:

CHANGELOG.md

@@ -10,6 +10,13 @@ versions still track specification maturity rather than a released product.
 
 ### Changed
 
+- Adopted pinned Bunny 0.6.0 as the normative checked Q32.32 numeric foundation
+  and exposed raw fixed-point evaluation through the Rust facade, with explicit
+  overflow and division-by-zero failures. Existing integer semantics and Core
+  artifacts are unchanged; fixed-point source syntax and Target instructions
+  remain unsupported. The workspace, CI and current-source consumer witness
+  now require Rust 1.96 for the dependency.
+
 - Added bounded raw-byte `+`, preserving operand order and exact coordinates in
   Core and Target with a checked sum of operand maxima. Overflow, narrowing,
   wrong operand families and forged Target calls fail closed. This generic

Cargo.toml

@@ -13,7 +13,7 @@ resolver = "2"
 edition = "2021"
 license = "Apache-2.0"
 repository = "https://github.com/flyingrobots/edict"
-rust-version = "1.95"
+rust-version = "1.96"
 
 # Maximize strictness (flyingrobots house rule): no unsafe, warnings are errors.
 [workspace.lints.rust]

README.md

@@ -474,7 +474,7 @@ That's the gap Edict fills.
 ## Build & Run
 
 Edict is not on crates.io yet (the alpha train keeps `publish = false`), so build
-from source. Requires Rust 1.85+.
+from source. Requires Rust 1.96+.
 
 Build the CLI:
 

crates/edict-syntax/Cargo.toml

@@ -12,6 +12,7 @@ publish = false
 workspace = true
 
 [dependencies]
+bunny-num = "=0.6.0"
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"
 sha2 = "0.10.9"

crates/edict-syntax/src/lib.rs

@@ -80,6 +80,7 @@ pub mod lawpack;
 pub mod lawpack_adapter;
 pub mod lawpack_authoring;
 pub mod lowerability;
+pub mod numeric;
 pub mod parser;
 pub mod provider;
 pub mod provider_invocation;

crates/edict-syntax/src/numeric.rs

@@ -0,0 +1,103 @@
+//! Checked fixed-point arithmetic for compiler consumers.
+//!
+//! Bunny 0.6.0 owns the arithmetic. This module selects its checked Q32.32
+//! subset without exposing saturating operators or floating-point conversions.
+//! It does not add source syntax, a Core value tag, or Target instructions.
+
+use bunny_num::FixedQ32_32;
+
+/// Edict's checked integration profile, distinct from Bunny's SDL `q32.32` name.
+pub const Q32_32_PROFILE: &str = "bunny.q32_32.checked/v1";
+
+/// Stable failures from checked fixed-point evaluation.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum NumericError {
+    /// The exact add/sub/neg result, or rounded mul/div result, exceeds i64.
+    Overflow,
+    /// Division has a zero raw divisor, including zero divided by zero.
+    DivisionByZero,
+}
+
+/// A signed Q32.32 value whose mathematical value is `raw / 2^32`.
+///
+/// Every raw i64 is valid. Equality and ordering compare raw values exactly.
+/// The Bunny representation stays private so callers cannot accidentally use
+/// its saturating arithmetic operators through this checked API.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct Q32_32(FixedQ32_32);
+
+impl Q32_32 {
+    /// Preserves the supplied raw bits exactly, without integer scaling.
+    #[must_use]
+    pub const fn from_raw(raw: i64) -> Self {
+        Self(FixedQ32_32::from_raw(raw))
+    }
+
+    /// Returns the exact signed raw representation, not a whole-number cast.
+    #[must_use]
+    pub const fn raw(self) -> i64 {
+        self.0.raw()
+    }
+
+    /// Adds two raw values exactly through Bunny's checked arithmetic.
+    ///
+    /// # Errors
+    /// Returns [`NumericError::Overflow`] when the exact sum cannot fit.
+    pub fn checked_add(self, rhs: Self) -> Result<Self, NumericError> {
+        self.0
+            .checked_add(rhs.0)
+            .map(Self)
+            .ok_or(NumericError::Overflow)
+    }
+
+    /// Subtracts two raw values exactly through Bunny's checked arithmetic.
+    ///
+    /// # Errors
+    /// Returns [`NumericError::Overflow`] when the exact difference cannot fit.
+    pub fn checked_sub(self, rhs: Self) -> Result<Self, NumericError> {
+        self.0
+            .checked_sub(rhs.0)
+            .map(Self)
+            .ok_or(NumericError::Overflow)
+    }
+
+    /// Negates a raw value exactly through Bunny's checked arithmetic.
+    ///
+    /// # Errors
+    /// Returns [`NumericError::Overflow`] for the minimum raw i64 value.
+    pub fn checked_neg(self) -> Result<Self, NumericError> {
+        self.0.checked_neg().map(Self).ok_or(NumericError::Overflow)
+    }
+
+    /// Multiplies with Bunny's wide intermediate and ties-to-even rounding.
+    ///
+    /// Quantization precedes the range check; a tiny nonzero product may round
+    /// to zero successfully.
+    ///
+    /// # Errors
+    /// Returns [`NumericError::Overflow`] when the rounded raw result cannot fit.
+    pub fn checked_mul(self, rhs: Self) -> Result<Self, NumericError> {
+        self.0
+            .checked_mul(rhs.0)
+            .map(Self)
+            .ok_or(NumericError::Overflow)
+    }
+
+    /// Divides with Bunny's wide intermediate and ties-to-even rounding.
+    ///
+    /// Quantization precedes the range check; this is distinct from the
+    /// truncation-toward-zero rule for Edict's exact signed integer division.
+    ///
+    /// # Errors
+    /// Returns [`NumericError::DivisionByZero`] for a zero divisor, or
+    /// [`NumericError::Overflow`] when the rounded raw quotient cannot fit.
+    pub fn checked_div(self, rhs: Self) -> Result<Self, NumericError> {
+        if rhs.raw() == 0 {
+            return Err(NumericError::DivisionByZero);
+        }
+        self.0
+            .checked_div(rhs.0)
+            .map(Self)
+            .ok_or(NumericError::Overflow)
+    }
+}

crates/edict/src/lib.rs

@@ -51,3 +51,20 @@ pub mod artifact {
         VerifiedResultProjection,
     };
 }
+
+/// Checked Bunny Q32.32 arithmetic for compiler consumers.
+///
+/// This API evaluates raw fixed-point values. It does not imply source-language
+/// fixed-point syntax or a corresponding Core/Target artifact representation.
+///
+/// ```
+/// use edict::numeric::{NumericError, Q32_32};
+///
+/// let one = Q32_32::from_raw(4_294_967_296);
+/// let half = Q32_32::from_raw(2_147_483_648);
+/// assert_eq!(one.checked_mul(half).map(Q32_32::raw), Ok(2_147_483_648));
+/// assert_eq!(one.checked_div(Q32_32::from_raw(0)), Err(NumericError::DivisionByZero));
+/// ```
+pub mod numeric {
+    pub use edict_syntax::numeric::{NumericError, Q32_32, Q32_32_PROFILE};
+}

crates/edict/tests/numeric_foundation.rs

@@ -0,0 +1,148 @@
+//! Literal raw vectors for the public checked numeric foundation.
+use edict::numeric::{NumericError, Q32_32, Q32_32_PROFILE};
+
+fn raw(value: Result<Q32_32, NumericError>) -> Result<i64, NumericError> {
+    value.map(Q32_32::raw)
+}
+
+#[test]
+fn public_numeric_profile_has_the_normative_identity() {
+    assert_eq!(Q32_32_PROFILE, "bunny.q32_32.checked/v1");
+}
+
+#[test]
+fn raw_values_preserve_bits_and_order() {
+    let values = [i64::MIN, -4_294_967_296, -1, 0, 1, 4_294_967_296, i64::MAX];
+    for value in values {
+        assert_eq!(Q32_32::from_raw(value).raw(), value);
+    }
+    for pair in values.windows(2) {
+        assert!(Q32_32::from_raw(pair[0]) < Q32_32::from_raw(pair[1]));
+    }
+}
+
+#[test]
+fn checked_linear_operations_preserve_exact_boundaries() {
+    for (left, right, expected) in [
+        (0, 0, 0),
+        (4_294_967_296, -1, 4_294_967_295),
+        (i64::MAX - 1, 1, i64::MAX),
+        (i64::MIN + 1, -1, i64::MIN),
+    ] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_add(Q32_32::from_raw(right))),
+            Ok(expected)
+        );
+    }
+    for (left, right, expected) in [
+        (0, 0, 0),
+        (4_294_967_296, 1, 4_294_967_295),
+        (i64::MAX - 1, -1, i64::MAX),
+        (i64::MIN + 1, 1, i64::MIN),
+    ] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_sub(Q32_32::from_raw(right))),
+            Ok(expected)
+        );
+    }
+    for (left, right) in [(i64::MAX, 1), (i64::MIN, -1)] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_add(Q32_32::from_raw(right))),
+            Err(NumericError::Overflow)
+        );
+    }
+    for (left, right) in [(i64::MAX, -1), (i64::MIN, 1)] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_sub(Q32_32::from_raw(right))),
+            Err(NumericError::Overflow)
+        );
+    }
+    for (value, expected) in [(0, 0), (1, -1), (-1, 1), (i64::MAX, -i64::MAX)] {
+        assert_eq!(raw(Q32_32::from_raw(value).checked_neg()), Ok(expected));
+    }
+    assert_eq!(
+        raw(Q32_32::from_raw(i64::MIN).checked_neg()),
+        Err(NumericError::Overflow)
+    );
+}
+
+#[test]
+fn multiplication_uses_signed_ties_to_even() {
+    for (left, right, expected) in [
+        // Exact scaled product = i64::MAX + 8_365_928 / 2^32.
+        // The fractional remainder rounds down before the range check.
+        (199_032_858_228_936, 199_032_871_303_925, i64::MAX),
+        (1, 2_147_483_647, 0),
+        (1, 2_147_483_648, 0),
+        (1, 2_147_483_649, 1),
+        (3, 2_147_483_648, 2),
+        (5, 2_147_483_648, 2),
+        (-1, 2_147_483_647, 0),
+        (-1, 2_147_483_648, 0),
+        (-1, 2_147_483_649, -1),
+        (-3, 2_147_483_648, -2),
+        (-5, 2_147_483_648, -2),
+        (3, -2_147_483_648, -2),
+        (-3, -2_147_483_648, 2),
+        (i64::MAX, 4_294_967_296, i64::MAX),
+        (i64::MIN, 4_294_967_296, i64::MIN),
+    ] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_mul(Q32_32::from_raw(right))),
+            Ok(expected),
+            "{left} * {right}"
+        );
+    }
+}
+
+#[test]
+fn division_uses_signed_ties_to_even() {
+    for (left, right, expected) in [
+        (1, 8_589_934_593, 0),
+        (1, 8_589_934_592, 0),
+        (1, 8_589_934_591, 1),
+        (3, 8_589_934_592, 2),
+        (5, 8_589_934_592, 2),
+        (-1, 8_589_934_593, 0),
+        (-1, 8_589_934_592, 0),
+        (-1, 8_589_934_591, -1),
+        (-3, 8_589_934_592, -2),
+        (-5, 8_589_934_592, -2),
+        (3, -8_589_934_592, -2),
+        (-3, -8_589_934_592, 2),
+        (i64::MAX, 4_294_967_296, i64::MAX),
+        (i64::MIN, 4_294_967_296, i64::MIN),
+    ] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_div(Q32_32::from_raw(right))),
+            Ok(expected),
+            "{left} / {right}"
+        );
+    }
+}
+
+#[test]
+fn checked_products_and_quotients_refuse_invalid_results() {
+    for (left, right) in [
+        (i64::MAX, 8_589_934_592),
+        (i64::MIN, 8_589_934_592),
+        (i64::MIN, -4_294_967_296),
+    ] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_mul(Q32_32::from_raw(right))),
+            Err(NumericError::Overflow)
+        );
+    }
+    for (left, right) in [(i64::MAX, 1), (i64::MIN, 1), (i64::MIN, -4_294_967_296)] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_div(Q32_32::from_raw(right))),
+            Err(NumericError::Overflow)
+        );
+    }
+    for left in [i64::MIN, -1, 0, 1, i64::MAX] {
+        assert_eq!(
+            raw(Q32_32::from_raw(left).checked_div(Q32_32::from_raw(0))),
+            Err(NumericError::DivisionByZero)
+        );
+    }
+}

docs/README.md

@@ -64,6 +64,8 @@ The current specification set is:
   participant-neutral bundle and assurance evidence manifest validation.
 - [Fixtures Topic](./topics/fixtures/): shared executable fixture corpus and
   reviewed Core golden artifact contract.
+- [Numeric Foundation](./topics/numeric-foundation/): the checked Bunny Q32.32
+  compiler API and its conformance boundary.
 - [Lawpacks Topic](./topics/lawpacks/): lawpack import, direct-adapter, bundle
   reference, and deferred manifest-validation boundary.
 - [Lowerability Topic](./topics/lowerability/): typed v1 lowering

docs/REQUIREMENTS.md

@@ -110,6 +110,7 @@ but owned by a follow-up issue; no fixtures until its dependency lands).
 | EDICT-OPTIC-TEMPLATE-OWNER-001 | operation-profile optic template has a canonical shape in edict-common.cddl, exported via ABIs | Target/Lawpack | `optic/template/owned` | `optic/template/undefined` | spec |
 | EDICT-OPTIC-APERTURE-REF-001 | `apertureRequirement` is a typed reference (footprintCeiling/abstractFootprintObligation), not a string | Language | `optic/aperture/typed-ref` | `optic/aperture/string` | spec |
 | EDICT-LANG-CAPABILITIES-SPLIT-001 | requiredSourceCapabilities (compiler) vs requiredCoreCapabilities (hash-significant Core field) | Language/Bundle | `lang/caps/split` | `lang/caps/conflated` | spec |
+| EDICT-LANG-FIXED-NUMERIC-001 | Bunny 0.6.0 owns the checked Q32.32 numeric profile; raw arithmetic results and explicit failures are shared compiler/runtime obligations, without implying current source or artifact support | Language | `raw_values_preserve_bits_and_order`; `multiplication_uses_signed_ties_to_even`; `division_uses_signed_ties_to_even` | `checked_products_and_quotients_refuse_invalid_results`; `checked_linear_operations_preserve_exact_boundaries` | spec |
 | EDICT-LANG-INT-SAFETY-001 | Integer arithmetic overflow-safe and total; checked forms or static proof; no wrap/saturate/trap | Language | `lang/int/checked` | `lang/int/unproven-overflow` | spec |
 | EDICT-TARGET-POSTCOND-001 | Target declares `postconditionSupport`; precommit `guarantee` requires it or rejects | Target/Language | `target/postcond/supported` | `target/postcond/unsupported-guarantee` | spec |
 | EDICT-LOWERABILITY-PARTIAL-001 | Lowering is a partial semantics-preserving relation: native/adapted/composite/unsupported; unsupported is a compiler error | Language/Target | `lowering/partial/classified` | `lowering/partial/silent-approx` | spec |