From f372181d35b326233eb38efba4f9d962f1b10935 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 4 Oct 2026 19:57:21 -0700 Subject: [PATCH 1/5] feat(numeric): adopt checked Bunny Q32.32 foundation Pin Bunny 0.6.0, define the normative checked profile, expose the compiler numeric API through the public facade, and align Rust 1.96 policy. Keep integer semantics and source/Core/Target capabilities unchanged. Refs #224 --- .github/workflows/ci.yml | 4 +- CHANGELOG.md | 7 + Cargo.lock | 7 + Cargo.toml | 2 +- crates/edict-syntax/Cargo.toml | 1 + crates/edict-syntax/src/lib.rs | 1 + crates/edict-syntax/src/numeric.rs | 103 +++++++++++++ crates/edict/src/lib.rs | 17 +++ crates/edict/tests/numeric_foundation.rs | 140 ++++++++++++++++++ docs/README.md | 2 + docs/REQUIREMENTS.md | 1 + docs/SPEC_edict-language-v1.md | 61 ++++++++ docs/topics/README.md | 2 + docs/topics/numeric-foundation/README.md | 56 +++++++ docs/topics/numeric-foundation/test-plan.md | 33 +++++ docs/topics/public-rust-api/README.md | 7 +- docs/topics/public-rust-api/test-plan.md | 2 + docs/topics/rust-standards/README.md | 6 +- docs/topics/rust-standards/test-plan.md | 4 +- .../jedit-state-read.Dockerfile | 2 +- xtask/src/tests.rs | 10 +- 21 files changed, 453 insertions(+), 15 deletions(-) create mode 100644 crates/edict-syntax/src/numeric.rs create mode 100644 crates/edict/tests/numeric_foundation.rs create mode 100644 docs/topics/numeric-foundation/README.md create mode 100644 docs/topics/numeric-foundation/test-plan.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c6c6a17f..32bfafac 100644 --- a/.github/workflows/ci.yml +++ b/.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: diff --git a/CHANGELOG.md b/CHANGELOG.md index cd40892f..21d7d2d2 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/Cargo.lock b/Cargo.lock index bacb208d..848916e3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -85,6 +85,12 @@ dependencies = [ "allocator-api2", ] +[[package]] +name = "bunny-num" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2d5c3288a3b7dcf4517c717a864c648777af349a15c86e25db48f86ec099f864" + [[package]] name = "cap-fs-ext" version = "4.0.3" @@ -438,6 +444,7 @@ dependencies = [ name = "edict-syntax" version = "0.11.0-alpha.1" dependencies = [ + "bunny-num", "serde", "serde_json", "sha2", diff --git a/Cargo.toml b/Cargo.toml index b2e7106e..f8c8bb58 100644 --- a/Cargo.toml +++ b/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] diff --git a/crates/edict-syntax/Cargo.toml b/crates/edict-syntax/Cargo.toml index f55bb23e..d42ff2fd 100644 --- a/crates/edict-syntax/Cargo.toml +++ b/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" diff --git a/crates/edict-syntax/src/lib.rs b/crates/edict-syntax/src/lib.rs index 7323475c..0dc1d1c5 100644 --- a/crates/edict-syntax/src/lib.rs +++ b/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; diff --git a/crates/edict-syntax/src/numeric.rs b/crates/edict-syntax/src/numeric.rs new file mode 100644 index 00000000..d4aa0841 --- /dev/null +++ b/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.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.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.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.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 { + if rhs.raw() == 0 { + return Err(NumericError::DivisionByZero); + } + self.0 + .checked_div(rhs.0) + .map(Self) + .ok_or(NumericError::Overflow) + } +} diff --git a/crates/edict/src/lib.rs b/crates/edict/src/lib.rs index 169d8207..5bdf045a 100644 --- a/crates/edict/src/lib.rs +++ b/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}; +} diff --git a/crates/edict/tests/numeric_foundation.rs b/crates/edict/tests/numeric_foundation.rs new file mode 100644 index 00000000..0ffe8f6f --- /dev/null +++ b/crates/edict/tests/numeric_foundation.rs @@ -0,0 +1,140 @@ +//! Literal raw vectors for the public checked numeric foundation. +use edict::numeric::{NumericError, Q32_32}; + +fn raw(value: Result) -> Result { + value.map(Q32_32::raw) +} + +#[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 [ + (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) + ); + } +} diff --git a/docs/README.md b/docs/README.md index e21739b8..bb91b3ce 100644 --- a/docs/README.md +++ b/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 diff --git a/docs/REQUIREMENTS.md b/docs/REQUIREMENTS.md index fd69cf5b..98764918 100644 --- a/docs/REQUIREMENTS.md +++ b/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 | diff --git a/docs/SPEC_edict-language-v1.md b/docs/SPEC_edict-language-v1.md index dd3f1584..dae1cbe5 100644 --- a/docs/SPEC_edict-language-v1.md +++ b/docs/SPEC_edict-language-v1.md @@ -1697,6 +1697,67 @@ and no authored type arguments. Other operand families, including String's specified Unicode-scalar specialization, remain unsupported by this lowering; they must not be silently measured in byte units instead. +### Fixed-Point Numeric Authority + +Bunny is the normative authority for Edict fixed-point arithmetic +(`EDICT-LANG-FIXED-NUMERIC-001`). Edict's integration profile +`bunny.q32_32.checked/v1` selects the **checked** Q32.32 subset of +[`bunny-num` 0.6.0's Numeric Constitution](https://github.com/flyingrobots/bunny/blob/9bf43600d08ff8e2a0ab888713948b409e386513/docs/NUMERIC_CONSTITUTION.md). +The dependency is pinned exactly; an unreviewed newer Bunny release does not +change this profile. This Edict integration identifier is distinct from Bunny's +SDL scalar profile name `q32.32`. + +The adopted rules are: + +- A value has one signed two's-complement raw `i64`; its mathematical value is + `raw / 2^32`. Raw construction and extraction preserve bits. Equality and + ordering compare raw values exactly, without epsilon. +- Addition, subtraction and negation use exact raw arithmetic and reject when + the result is outside `i64`. +- Multiplication and division use Bunny's `i128` intermediates, round to the + nearest Q32.32 value with ties to even for either sign, then reject an + out-of-range **rounded** result. Quantization may legitimately turn a small + nonzero mathematical result into zero. +- A zero divisor is a distinct domain failure, including `0 / 0`. Checked + failure must be explicit; it cannot become saturation, wrapping or a panic. +- Saturating operators, square root and floating-point conversion APIs are + outside this adopted subset. No host float participates in canonical math. + A future explicit float-ingress boundary must reject non-finite or + out-of-range input using Bunny's validated conversion policy; its rounding + and failure behavior require separate conformance evidence. + +This does not reinterpret `I32`, `I64`, `U32` or `U64` as fixed-point values. +Their exact domains, canonical identity, range proofs and signed division's +truncation-toward-zero rule remain unchanged. There is no implicit conversion +between an integer and this fixed-point domain. + +The current implementation exposes only a checked Rust numeric foundation for +compiler consumers. It adds no fixed-point source type, literal, prelude +operation, Core value tag, Target instruction, or provider capability. Existing +integer artifact tags cannot be used as unmarked fixed-point encodings. + +Before a future compiler fold or target implementation can claim this profile, +its accepted representation and capability must be explicit and hash-bound. +Compiler and runtime conformance must agree on literal raw-result vectors, +structured failures and canonical artifact bytes. Bunny's generated +[`i64-le-q32.32` wire profile](https://github.com/flyingrobots/bunny/blob/9bf43600d08ff8e2a0ab888713948b409e386513/generated/bunny-graphics.manifest.json) +is an eight-byte little-endian raw representation; it is not an existing Edict +canonical-CBOR fixed-point tag. A future Edict schema must specify how it binds +this raw representation and the profile identity without silently repurposing +integer values. No such wire extension is implemented by this foundation. + +A dependency/profile upgrade requires review of results, failures and encoding +compatibility, with compiler/runtime conformance rerun before adoption. A +changed arithmetic or identity contract requires an explicit profile/version +transition; changing a manifest alone is not that transition. + +| Relationship | Targets | +| --- | --- | +| `refines` | [Core types](#core-types), [Integer safety](#integer-safety) | +| `supersedes` | none | +| `depends_on` | [Pinned Bunny Numeric Constitution](https://github.com/flyingrobots/bunny/blob/9bf43600d08ff8e2a0ab888713948b409e386513/docs/NUMERIC_CONSTITUTION.md) | +| `related` | [Numeric foundation](./topics/numeric-foundation/README.md), [Core IR](./topics/core-ir/README.md), [Target profiles](./topics/target-profiles/README.md) | + ### Compound Types - record types; diff --git a/docs/topics/README.md b/docs/topics/README.md index 99b06d31..9aee33cd 100644 --- a/docs/topics/README.md +++ b/docs/topics/README.md @@ -61,6 +61,8 @@ cargo xtask verify reference, request-only profile, and canonical manifest-validation boundary. - [Lowerability](./lowerability/README.md): typed v1 lowering requirements, target-profile facts, and direct-only support classification. +- [Numeric Foundation](./numeric-foundation/README.md): checked Bunny Q32.32 + arithmetic for compiler consumers, with explicit source and artifact limits. - [Obstruction Strands](./obstruction-strands/README.md): current terminal and preserved-obstruction source/Core boundary plus planned Target IR/runtime verification ledger. diff --git a/docs/topics/numeric-foundation/README.md b/docs/topics/numeric-foundation/README.md new file mode 100644 index 00000000..ee51e719 --- /dev/null +++ b/docs/topics/numeric-foundation/README.md @@ -0,0 +1,56 @@ +# Numeric Foundation + +The compiler library exposes a checked Q32.32 numeric API backed by exact +`bunny-num = "=0.6.0"`. The normative owner is the language specification's +[fixed-point numeric authority](../../SPEC_edict-language-v1.md#fixed-point-numeric-authority). +Bunny owns the arithmetic implementation; Edict selects its checked subset and +provides stable failures. [NUMERIC-REQ-001] [NUMERIC-REQ-002] + +## Public boundary + +`edict::numeric` exports `Q32_32`, `NumericError`, and `Q32_32_PROFILE`. +`edict_syntax::numeric` provides the same implementation to compiler consumers. +The profile value is `bunny.q32_32.checked/v1`; it is Edict's integration label, +not a new name for Bunny's SDL `q32.32` scalar profile. + +| API | Contract | +| --- | --- | +| `Q32_32::from_raw` / `raw` | Preserve every raw signed i64 bit pattern, without integer scaling. | +| Equality / ordering | Compare raw values exactly. | +| `checked_add`, `checked_sub`, `checked_neg` | Return the exact result or `NumericError::Overflow`. | +| `checked_mul`, `checked_div` | Use Bunny's wide intermediate, ties-to-even quantization, then reject an out-of-range rounded result as `Overflow`. | +| Division by zero | Return `NumericError::DivisionByZero`, including zero divided by zero. | + +The wrapper keeps Bunny's representation private and exposes no saturating +arithmetic traits or float conversions. Tiny nonzero products and quotients +may round to zero successfully. Expected raw values in the +[consumer tests](../../../crates/edict/tests/numeric_foundation.rs) are literal +oracles, not values calculated through Bunny. [NUMERIC-REQ-002] + +## Compatibility and implementation limits + +Existing integer semantics and canonical artifacts retain their meaning. +There is no automatic integer/fixed-point coercion. This library API is a +foundation for compiler consumers, not an implemented source-language folding +pass. Source fixed-point syntax, Core/Target tags and runtime execution are not +added by it. [NUMERIC-REQ-003] + +Bunny's raw wire profile is eight-byte little-endian i64. Edict has no fixed-point +canonical-CBOR tag today. Future source lowering, encoding and runtime support +must satisfy the specification's explicit representation, capability and +conformance obligations before claiming this profile. Dependency upgrades must +review raw results, failures and identity compatibility; an exact manifest pin +must not float implicitly. The checked subset does not adopt every API Bunny +exports, and this foundation grants no application or provider authority. + +## Ownership relationships + +The specification owns the numeric law; this shelf owns the implementation +boundary and its verification map. + +| Relationship | Targets | +| --- | --- | +| `refines` | [Fixed-point numeric authority](../../SPEC_edict-language-v1.md#fixed-point-numeric-authority) | +| `supersedes` | none | +| `depends_on` | [Pinned Bunny Numeric Constitution](https://github.com/flyingrobots/bunny/blob/9bf43600d08ff8e2a0ab888713948b409e386513/docs/NUMERIC_CONSTITUTION.md) | +| `related` | [Public Rust API](../public-rust-api/README.md), [Rust standards](../rust-standards/README.md), [Test plan](./test-plan.md) | diff --git a/docs/topics/numeric-foundation/test-plan.md b/docs/topics/numeric-foundation/test-plan.md new file mode 100644 index 00000000..af130c68 --- /dev/null +++ b/docs/topics/numeric-foundation/test-plan.md @@ -0,0 +1,33 @@ +# Numeric Foundation Test Plan + +## Scope + +The checked compiler numeric API and normative Bunny Q32.32 profile. Source +syntax, Core fixed-point values, folding source programs, Target instructions, +and runtime admission remain outside this implementation. + +## Requirements + +| ID | Status | Requirement | Source | +| --- | --- | --- | --- | +| NUMERIC-REQ-001 | implemented | The public Edict numeric API delegates Q32.32 arithmetic to exact Bunny 0.6.0 and preserves every supplied raw i64 bit pattern. | docs/SPEC_edict-language-v1.md | +| NUMERIC-REQ-002 | implemented | Checked addition, subtraction, multiplication, division and negation return exact raw results or stable Overflow/DivisionByZero failures, with multiplication and division rounding ties to even before range checking. | docs/SPEC_edict-language-v1.md | +| NUMERIC-REQ-003 | implemented | Existing exact integer domains and canonical Core artifacts remain unchanged; fixed-point support introduces no implicit integer conversion. | docs/SPEC_edict-language-v1.md | + +## Test Cases + +| ID | Status | Category | Requirement | Oracle | Evidence | Fixtures | Notes | +| --- | --- | --- | --- | --- | --- | --- | --- | +| NUMERIC-TP-001 | implemented | Public API | NUMERIC-REQ-001 | Literal zero, extrema and signed fractional raw values round-trip through facade-only imports and retain exact ordering. | raw_values_preserve_bits_and_order | crates/edict/tests/numeric_foundation.rs | No float ingress or artifact encoding claim. | +| NUMERIC-TP-002 | implemented | Arithmetic boundaries | NUMERIC-REQ-002 | Literal add/sub/neg results include exact endpoints; one-unit overflow and minimum negation return Overflow. | checked_linear_operations_preserve_exact_boundaries | crates/edict/tests/numeric_foundation.rs | Expected values do not call Bunny. | +| NUMERIC-TP-003 | implemented | Rounding | NUMERIC-REQ-002 | Positive and negative multiplication/division below, above and exactly halfway round to literal ties-even raw results, including underflow to zero. | multiplication_uses_signed_ties_to_even, division_uses_signed_ties_to_even | crates/edict/tests/numeric_foundation.rs | Native integer division retains its separate truncation rule. | +| NUMERIC-TP-004 | implemented | Structured refusal | NUMERIC-REQ-002 | Multiplication/division overflow return Overflow; zero divisors return DivisionByZero for zero, signed and endpoint dividends. | checked_products_and_quotients_refuse_invalid_results | crates/edict/tests/numeric_foundation.rs | No panic, saturation or wrapping. | +| NUMERIC-TP-005 | implemented | Compatibility | NUMERIC-REQ-003 | Existing integer-domain and canonical-golden tests retain exact accepted domains and artifacts. | fixed_width_integer_types_and_suffixes_preserve_exact_domains, signed_fixed_width_minima_preserve_exact_domains, out_of_range_u64_and_cross_width_values_reject_before_core, canonical_core_rejects_values_outside_their_declared_integer_domain | crates/edict-syntax/tests/operation_prerequisites.rs | Existing behavioral oracles; no new integer implementation. | + +## Known Gaps + +- Source fixed-point types, literals, operations and constant folding are not + implemented. Core/Target representation and provider/runtime conformance need + separately verified, hash-bound contracts before source support can claim them. +- This API has no floating-point ingress, decimal parser or canonical artifact + encoder. Raw host values alone carry no package or execution authority. diff --git a/docs/topics/public-rust-api/README.md b/docs/topics/public-rust-api/README.md index c64a1081..cd35c248 100644 --- a/docs/topics/public-rust-api/README.md +++ b/docs/topics/public-rust-api/README.md @@ -26,6 +26,11 @@ and verified projections. Diagnostic spans are available under `diagnostic`. These are explicit type exports; implementation modules remain private to the facade boundary. [PUBRUST-REQ-001] +The `numeric` namespace exposes the checked Bunny Q32.32 foundation described +in its [owning shelf](../numeric-foundation/README.md). It evaluates raw values +without exposing saturating traits or claiming fixed-point source/IR support. +[PUBRUST-REQ-005] + ## Decision relationships This current public-API boundary depends on the contracts implemented by its @@ -36,7 +41,7 @@ continues to serve repository consumers. | --- | --- | | `refines` | none | | `supersedes` | none | -| `depends_on` | [Syntax](../syntax/README.md), [Semantic validation](../semantic-validation/README.md), [Core IR](../core-ir/README.md), [Target IR](../target-ir/README.md), [Result projections](../result-projections/README.md) | +| `depends_on` | [Syntax](../syntax/README.md), [Semantic validation](../semantic-validation/README.md), [Core IR](../core-ir/README.md), [Target IR](../target-ir/README.md), [Result projections](../result-projections/README.md), [Numeric foundation](../numeric-foundation/README.md) | | `related` | [Rust standards](../rust-standards/README.md), [Release process](../release-process/README.md), [CLI](../cli/README.md) | The relationship table follows the diff --git a/docs/topics/public-rust-api/test-plan.md b/docs/topics/public-rust-api/test-plan.md index 4c3b9e96..9eb193ba 100644 --- a/docs/topics/public-rust-api/test-plan.md +++ b/docs/topics/public-rust-api/test-plan.md @@ -26,6 +26,7 @@ Out of scope: | PUBRUST-REQ-002 | planned | The facade's package inventory is explicit, reproducible, and remains non-publishing until a separately approved publication policy exists. | issue #189 | | PUBRUST-REQ-003 | planned | A clean external consumer can compile against the facade without an undocumented repository-relative dependency. | issue #189 | | PUBRUST-REQ-004 | implemented | Release preparation advances the facade package version and exact implementation dependency together. | xtask/src/release_prep.rs | +| PUBRUST-REQ-005 | implemented | The facade exposes the checked numeric foundation without leaking Bunny saturating operators or implying source/IR support. | docs/SPEC_edict-language-v1.md | ## Test Cases @@ -37,6 +38,7 @@ Out of scope: | PUBRUST-TP-004 | planned | External consumer | PUBRUST-REQ-003 | The project compiles and runs without a sibling Edict checkout. | release-engineering external-consumer check | - | Requires packaged implementation dependencies or a sealed local registry before publication. | | PUBRUST-TP-005 | implemented | Release preparation | PUBRUST-REQ-004 | Cargo resolves the requested facade and implementation versions with the prepared lockfile. | release_prep_keeps_facade_exact_dependency_resolvable | xtask/src/tests.rs | Offline temporary workspace; no registry publication. | | PUBRUST-TP-006 | implemented | Consumer model closure | PUBRUST-REQ-001 | A consumer using only facade imports constructs Core, Target IR, and projection values, names decoded values and verified projections, and reads diagnostic spans. | facade_consumer_constructs_and_verifies_artifacts, facade_consumer_names_diagnostic_spans | crates/edict/tests/artifact_models.rs | The integration test is a separate consumer crate; it uses no implementation imports. | +| PUBRUST-TP-007 | implemented | Numeric consumer | PUBRUST-REQ-005 | A facade-only consumer evaluates literal Q32.32 vectors and distinguishes overflow from division by zero. | raw_values_preserve_bits_and_order, checked_linear_operations_preserve_exact_boundaries, multiplication_uses_signed_ties_to_even, division_uses_signed_ties_to_even, checked_products_and_quotients_refuse_invalid_results | crates/edict/tests/numeric_foundation.rs | No direct Bunny import or fixed-point source/artifact claim. | ## Known Gaps diff --git a/docs/topics/rust-standards/README.md b/docs/topics/rust-standards/README.md index 2fe29258..89917488 100644 --- a/docs/topics/rust-standards/README.md +++ b/docs/topics/rust-standards/README.md @@ -20,10 +20,10 @@ That gate runs formatting, Clippy with warnings as errors, workspace tests, workspace doctests, Core golden checks, topic contract checks, and whitespace checks. [RUST-REQ-001] -Every workspace package inherits the minimum supported Rust version `1.95`, so +Every workspace package inherits the minimum supported Rust version `1.96`, so published Cargo metadata and local resolver behavior agree with the workspace -policy. CI runs the complete format, Clippy, test, and provider-component -fixture matrix on exact Rust `1.95.0` and on stable; an xtask guard checks Cargo +policy. The pinned Bunny 0.6.0 numeric dependency requires this minimum. CI runs +the complete format, Clippy, test, and provider-component fixture matrix on exact Rust `1.96.0` and on stable; an xtask guard checks Cargo metadata and the CI toolchain declarations together. [RUST-REQ-009] ## Safety diff --git a/docs/topics/rust-standards/test-plan.md b/docs/topics/rust-standards/test-plan.md index 0e0d6b30..e6063893 100644 --- a/docs/topics/rust-standards/test-plan.md +++ b/docs/topics/rust-standards/test-plan.md @@ -34,7 +34,7 @@ Out of scope: | RUST-REQ-006 | planned | Library-code footgun lints for `unwrap`, `expect`, `panic`, `todo`, `unimplemented`, debug macros, and direct stdout/stderr should become deny-level after scoped test and `xtask` allowances exist. | docs/topics/rust-standards/README.md | | RUST-REQ-007 | implemented | CI pins cargo-deny and checks the root plus provider fixture guest lockfiles for advisories, yanked crates, reviewed licenses, dependency bans, and allowed sources. | deny.toml, .github/workflows/ci.yml | | RUST-REQ-008 | planned | Parser, lexer, decoder, and authority-facts fuzz targets should be added as the language surface grows. | docs/topics/rust-standards/README.md | -| RUST-REQ-009 | implemented | The workspace declares Rust `1.95` as its MSRV, and CI runs the complete formatting, lint, and test matrix on exact Rust `1.95.0` plus stable. | Cargo.toml, .github/workflows/ci.yml | +| RUST-REQ-009 | implemented | The workspace declares Rust `1.96` as its MSRV, and CI runs the complete formatting, lint, and test matrix on exact Rust `1.96.0` plus stable. | Cargo.toml, .github/workflows/ci.yml | ## Fixtures @@ -57,7 +57,7 @@ Out of scope: | RUST-TP-006 | planned | Lint ratchet | RUST-REQ-006 | Add scoped lint allowances and then deny library-code footgun lints. | - | - | Planned cleanup slice. | | RUST-TP-007 | implemented | Dependency gate | RUST-REQ-007 | CI installs pinned cargo-deny and checks both root and provider fixture guest lockfiles under the reviewed advisory, license, ban, and source policy. | cargo_deny_supply_chain_gate_covers_root_and_fixture_guest | deny.toml, .github/workflows/ci.yml, Cargo.lock, fixtures/providers/components/guests/Cargo.lock | This gate does not publish crates. | | RUST-TP-008 | planned | Fuzzing | RUST-REQ-008 | Add fuzz targets for parser/decoder surfaces. | - | - | Planned hardening slice. | -| RUST-TP-009 | implemented | MSRV guard | RUST-REQ-009 | Cargo metadata reports Rust 1.95 for every workspace package, and the exact CI toolchain label agrees. | workspace_msrv_matches_the_ci_toolchain | Cargo.toml, crates/edict-cli/Cargo.toml, crates/edict-provider-host-wasmtime/Cargo.toml, crates/edict-provider-schema/Cargo.toml, crates/edict-syntax/Cargo.toml, xtask/Cargo.toml, .github/workflows/ci.yml | Required by the isolated Wasmtime 48 provider host. | +| RUST-TP-009 | implemented | MSRV guard | RUST-REQ-009 | Cargo metadata reports Rust 1.96 for every workspace package, and the exact CI toolchain label agrees. | workspace_msrv_matches_the_ci_toolchain | Cargo.toml, crates/edict-cli/Cargo.toml, crates/edict-provider-host-wasmtime/Cargo.toml, crates/edict-provider-schema/Cargo.toml, crates/edict-syntax/Cargo.toml, xtask/Cargo.toml, .github/workflows/ci.yml | Required by the pinned Bunny 0.6.0 numeric dependency. | ## Determinism Obligations diff --git a/scripts/consumer-witnesses/jedit-state-read.Dockerfile b/scripts/consumer-witnesses/jedit-state-read.Dockerfile index 7462059b..fce0cf31 100644 --- a/scripts/consumer-witnesses/jedit-state-read.Dockerfile +++ b/scripts/consumer-witnesses/jedit-state-read.Dockerfile @@ -1,4 +1,4 @@ -FROM rust:1.95.0-bookworm +FROM rust:1.96.0-bookworm RUN apt-get update && apt-get install -y --no-install-recommends python3 \ && rm -rf /var/lib/apt/lists/* WORKDIR /edict diff --git a/xtask/src/tests.rs b/xtask/src/tests.rs index 9a3f6543..95613128 100644 --- a/xtask/src/tests.rs +++ b/xtask/src/tests.rs @@ -2003,17 +2003,17 @@ fn workspace_msrv_matches_the_ci_toolchain() { checked_members += 1; assert_eq!( package["rust_version"].as_str(), - Some("1.95"), - "workspace package {} must inherit Rust 1.95", + Some("1.96"), + "workspace package {} must inherit Rust 1.96", package["name"].as_str().expect("package name") ); } } assert_eq!(checked_members, workspace_members.len()); assert!( - workflow.contains("rust-version: \"1.95.0\"") - && workflow.contains("rust-label: \"msrv 1.95.0\""), - "CI must exercise the exact Rust 1.95.0 MSRV" + workflow.contains("rust-version: \"1.96.0\"") + && workflow.contains("rust-label: \"msrv 1.96.0\""), + "CI must exercise the exact Rust 1.96.0 MSRV" ); } From 829fe01958204fd84e5cc700f40651004e8f0292 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 4 Oct 2026 20:03:59 -0700 Subject: [PATCH 2/5] test: refresh provider fixture source binding for Bunny dependency --- fixtures/providers/components/inventory.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/fixtures/providers/components/inventory.json b/fixtures/providers/components/inventory.json index 45cf2e8e..e42104b6 100644 --- a/fixtures/providers/components/inventory.json +++ b/fixtures/providers/components/inventory.json @@ -7,5 +7,5 @@ "malformed-lowerer": "sha256:dfcd171918373d18b9dff16778e98b7618eeb4ac85976dd7134b9e201562f41b", "verifier": "sha256:e889007a621d05820261eeb9fd69ce555f5761dbdbf82c6e9f55220ea529776d" }, - "sourceDigest": "sha256:d3148b4eaf86909eef55e52101d4d0b3fec4889833ab26ca481f134dba42c050" + "sourceDigest": "sha256:d81471e45b02ff2eae8e00125d765517d89c10b551c9593002ffee6f345e2fca" } From ec497c53645aece37b3cd7b423b6f4a026331255 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 4 Oct 2026 21:34:08 -0700 Subject: [PATCH 3/5] test: pin the public checked numeric profile identity --- crates/edict/tests/numeric_foundation.rs | 7 ++++++- docs/topics/numeric-foundation/test-plan.md | 2 +- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/crates/edict/tests/numeric_foundation.rs b/crates/edict/tests/numeric_foundation.rs index 0ffe8f6f..46f79665 100644 --- a/crates/edict/tests/numeric_foundation.rs +++ b/crates/edict/tests/numeric_foundation.rs @@ -1,10 +1,15 @@ //! Literal raw vectors for the public checked numeric foundation. -use edict::numeric::{NumericError, Q32_32}; +use edict::numeric::{NumericError, Q32_32, Q32_32_PROFILE}; fn raw(value: Result) -> Result { 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]; diff --git a/docs/topics/numeric-foundation/test-plan.md b/docs/topics/numeric-foundation/test-plan.md index af130c68..8742fe07 100644 --- a/docs/topics/numeric-foundation/test-plan.md +++ b/docs/topics/numeric-foundation/test-plan.md @@ -18,7 +18,7 @@ and runtime admission remain outside this implementation. | ID | Status | Category | Requirement | Oracle | Evidence | Fixtures | Notes | | --- | --- | --- | --- | --- | --- | --- | --- | -| NUMERIC-TP-001 | implemented | Public API | NUMERIC-REQ-001 | Literal zero, extrema and signed fractional raw values round-trip through facade-only imports and retain exact ordering. | raw_values_preserve_bits_and_order | crates/edict/tests/numeric_foundation.rs | No float ingress or artifact encoding claim. | +| NUMERIC-TP-001 | implemented | Public API | NUMERIC-REQ-001 | The facade profile equals literal bunny.q32_32.checked/v1; zero, extrema and signed fractional raw values round-trip through facade-only imports and retain exact ordering. | public_numeric_profile_has_the_normative_identity, raw_values_preserve_bits_and_order | crates/edict/tests/numeric_foundation.rs | No float ingress or artifact encoding claim. | | NUMERIC-TP-002 | implemented | Arithmetic boundaries | NUMERIC-REQ-002 | Literal add/sub/neg results include exact endpoints; one-unit overflow and minimum negation return Overflow. | checked_linear_operations_preserve_exact_boundaries | crates/edict/tests/numeric_foundation.rs | Expected values do not call Bunny. | | NUMERIC-TP-003 | implemented | Rounding | NUMERIC-REQ-002 | Positive and negative multiplication/division below, above and exactly halfway round to literal ties-even raw results, including underflow to zero. | multiplication_uses_signed_ties_to_even, division_uses_signed_ties_to_even | crates/edict/tests/numeric_foundation.rs | Native integer division retains its separate truncation rule. | | NUMERIC-TP-004 | implemented | Structured refusal | NUMERIC-REQ-002 | Multiplication/division overflow return Overflow; zero divisors return DivisionByZero for zero, signed and endpoint dividends. | checked_products_and_quotients_refuse_invalid_results | crates/edict/tests/numeric_foundation.rs | No panic, saturation or wrapping. | From eff58d06cf24e0646079dcba674a42fde04e9c29 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 4 Oct 2026 21:35:45 -0700 Subject: [PATCH 4/5] test: witness rounding before fixed-point overflow checks --- crates/edict/tests/numeric_foundation.rs | 3 +++ docs/topics/numeric-foundation/test-plan.md | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/crates/edict/tests/numeric_foundation.rs b/crates/edict/tests/numeric_foundation.rs index 46f79665..5305bc13 100644 --- a/crates/edict/tests/numeric_foundation.rs +++ b/crates/edict/tests/numeric_foundation.rs @@ -69,6 +69,9 @@ fn checked_linear_operations_preserve_exact_boundaries() { #[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), diff --git a/docs/topics/numeric-foundation/test-plan.md b/docs/topics/numeric-foundation/test-plan.md index 8742fe07..f0722860 100644 --- a/docs/topics/numeric-foundation/test-plan.md +++ b/docs/topics/numeric-foundation/test-plan.md @@ -20,7 +20,7 @@ and runtime admission remain outside this implementation. | --- | --- | --- | --- | --- | --- | --- | --- | | NUMERIC-TP-001 | implemented | Public API | NUMERIC-REQ-001 | The facade profile equals literal bunny.q32_32.checked/v1; zero, extrema and signed fractional raw values round-trip through facade-only imports and retain exact ordering. | public_numeric_profile_has_the_normative_identity, raw_values_preserve_bits_and_order | crates/edict/tests/numeric_foundation.rs | No float ingress or artifact encoding claim. | | NUMERIC-TP-002 | implemented | Arithmetic boundaries | NUMERIC-REQ-002 | Literal add/sub/neg results include exact endpoints; one-unit overflow and minimum negation return Overflow. | checked_linear_operations_preserve_exact_boundaries | crates/edict/tests/numeric_foundation.rs | Expected values do not call Bunny. | -| NUMERIC-TP-003 | implemented | Rounding | NUMERIC-REQ-002 | Positive and negative multiplication/division below, above and exactly halfway round to literal ties-even raw results, including underflow to zero. | multiplication_uses_signed_ties_to_even, division_uses_signed_ties_to_even | crates/edict/tests/numeric_foundation.rs | Native integer division retains its separate truncation rule. | +| NUMERIC-TP-003 | implemented | Rounding | NUMERIC-REQ-002 | Positive and negative multiplication/division below, above and exactly halfway round to literal ties-even raw results, including underflow to zero and an exact product above i64::MAX that rounds back into range. | multiplication_uses_signed_ties_to_even, division_uses_signed_ties_to_even | crates/edict/tests/numeric_foundation.rs | Native integer division retains its separate truncation rule. | | NUMERIC-TP-004 | implemented | Structured refusal | NUMERIC-REQ-002 | Multiplication/division overflow return Overflow; zero divisors return DivisionByZero for zero, signed and endpoint dividends. | checked_products_and_quotients_refuse_invalid_results | crates/edict/tests/numeric_foundation.rs | No panic, saturation or wrapping. | | NUMERIC-TP-005 | implemented | Compatibility | NUMERIC-REQ-003 | Existing integer-domain and canonical-golden tests retain exact accepted domains and artifacts. | fixed_width_integer_types_and_suffixes_preserve_exact_domains, signed_fixed_width_minima_preserve_exact_domains, out_of_range_u64_and_cross_width_values_reject_before_core, canonical_core_rejects_values_outside_their_declared_integer_domain | crates/edict-syntax/tests/operation_prerequisites.rs | Existing behavioral oracles; no new integer implementation. | From 4fe28c5323b92de1b4086bc5271bb7be7ce45518 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 4 Oct 2026 22:02:25 -0700 Subject: [PATCH 5/5] Fix: align source build prerequisite with Bunny MSRV --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0812ef9a..cf9258d6 100644 --- a/README.md +++ b/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: