From 7d14bd0dd1cf4a2293c00c185573fd4a7fc364ae Mon Sep 17 00:00:00 2001 From: Codex Date: Fri, 11 Sep 2026 05:50:45 -0700 Subject: [PATCH] Add exact analysis numbers units and bounded request work --- .gitattributes | 1 + Cargo.lock | 22 + crates/oa-core/Cargo.toml | 3 + crates/oa-core/src/analysis_numeric.rs | 103 +++ .../oa-core/src/analysis_numeric/dimension.rs | 107 +++ crates/oa-core/src/analysis_numeric/exact.rs | 469 ++++++++++ .../fixtures/r7-literal-boundaries.json | 32 + crates/oa-core/src/analysis_numeric/meter.rs | 240 ++++++ .../oa-core/src/analysis_numeric/quantity.rs | 378 ++++++++ crates/oa-core/src/analysis_numeric/tests.rs | 804 ++++++++++++++++++ crates/oa-core/src/lib.rs | 1 + harness/DECISIONS.md | 38 + ...nalysis-numeric-implementation-20260911.md | 156 ++++ ...elease-analysis-numeric-review-20260911.md | 82 ++ ...is-production-integration-plan-20260911.md | 126 +++ 15 files changed, 2562 insertions(+) create mode 100644 crates/oa-core/src/analysis_numeric.rs create mode 100644 crates/oa-core/src/analysis_numeric/dimension.rs create mode 100644 crates/oa-core/src/analysis_numeric/exact.rs create mode 100644 crates/oa-core/src/analysis_numeric/fixtures/r7-literal-boundaries.json create mode 100644 crates/oa-core/src/analysis_numeric/meter.rs create mode 100644 crates/oa-core/src/analysis_numeric/quantity.rs create mode 100644 crates/oa-core/src/analysis_numeric/tests.rs create mode 100644 harness/release-analysis-numeric-implementation-20260911.md create mode 100644 harness/release-analysis-numeric-review-20260911.md create mode 100644 harness/release-analysis-production-integration-plan-20260911.md diff --git a/.gitattributes b/.gitattributes index b6e8e341..639a64f6 100644 --- a/.gitattributes +++ b/.gitattributes @@ -23,6 +23,7 @@ harness/history/2026-09-10-ledgers-before-continuation-refresh/** -text harness/history/2026-09-10-ledgers-before-second-consolidation/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol harness/experiments/textual-authoring-20260911-local/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol crates/oa-desktop/src/recovery/fixtures/*.json -text +crates/oa-core/src/analysis_numeric/fixtures/** -text whitespace=cr-at-eol harness/fixtures/source7-native/** -text harness/fixtures/basic-editing/** -text harness/fixtures/scenario-authoring/base/** -text whitespace=cr-at-eol diff --git a/Cargo.lock b/Cargo.lock index b3bda78b..9ac4d639 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2107,6 +2107,25 @@ dependencies = [ "jni-sys 0.3.1", ] +[[package]] +name = "num-bigint" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93e7820bc0a80a0238e650327316f929ba18d5be054b647490a3a6a339f3e7c0" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-integer" +version = "0.1.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7ce2d95d4b3734dc35aa2f45e1aa22cd416814592a4f9d9205e11affd5b8e10b" +dependencies = [ + "num-traits", +] + [[package]] name = "num-traits" version = "0.2.19" @@ -2153,6 +2172,9 @@ name = "oa-core" version = "0.2.0" dependencies = [ "libc", + "num-bigint", + "num-integer", + "num-traits", "same-file", "serde", "serde_json", diff --git a/crates/oa-core/Cargo.toml b/crates/oa-core/Cargo.toml index df5452b5..fdc86b2a 100644 --- a/crates/oa-core/Cargo.toml +++ b/crates/oa-core/Cargo.toml @@ -12,6 +12,9 @@ uuid.workspace = true thiserror.workspace = true tempfile = "3" same-file = "1" +num-bigint = "0.5.1" +num-integer = "0.1.47" +num-traits = "0.2.19" [target.'cfg(target_os = "linux")'.dependencies] libc = "0.2" diff --git a/crates/oa-core/src/analysis_numeric.rs b/crates/oa-core/src/analysis_numeric.rs new file mode 100644 index 00000000..78a56dbd --- /dev/null +++ b/crates/oa-core/src/analysis_numeric.rs @@ -0,0 +1,103 @@ +//! Exact numeric foundation for analysis; no model, expression, or package resolver. +//! +//! Values use reduced rational coordinates. All nontrivial arithmetic takes one +//! request-local [WorkMeter]. The future evaluator must also charge *expanded* +//! expression/call/property/list/target visits and retain the same logical walk on +//! cache hits. Stored AST size is not a dynamic execution limit. +//! +//! Approximate engineering functions/irrational unit scales require a subsequent +//! explicit numeric profile; rationals do not implement degree/radian conversion +//! or transcendental mathematics. + +mod dimension; +mod exact; +mod meter; +mod quantity; + +pub use dimension::{Dimension, DimensionAxis}; +pub use exact::{Exact, ExactWire}; +pub use meter::{ + EvaluationStep, NumericOperation, WorkExhaustion, WorkLimits, WorkMeter, WorkResource, + WorkSite, WorkUsage, +}; +pub use quantity::{NumericType, NumericValue, ResolvedKind, Unit}; + +use serde::{Deserialize, Serialize}; +use thiserror::Error; + +/// Profile identity includes the accounting rules, not crate-internal timing. +pub const WORK_PROFILE: &str = "Q1-logical-work-1"; +pub const MAX_COMPONENT_BITS: u64 = 4096; +/// Cross products require 8192 bits; their sum can require one additional bit. +pub const MAX_INTERMEDIATE_BITS: u64 = 8193; +pub const MAX_COMPONENT_DIGITS: usize = 1234; +pub const MAX_DECIMAL_EXPONENT: i32 = 128; +pub const MAX_INTEGER_POWER: i8 = 16; +/// Includes ratio punctuation/whitespace without permitting unbounded scanning. +pub const MAX_LITERAL_BYTES: usize = 2 * MAX_COMPONENT_DIGITS + 32; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum NumberComponent { + Numerator, + Denominator, +} + +#[derive(Debug, Clone, PartialEq, Eq, Error, Serialize, Deserialize)] +pub enum NumericLimit { + #[error("request work exhausted: {0}")] + Work(WorkExhaustion), + #[error("{component:?} uses {bits} bits, above the {limit}-bit {stage} limit")] + Bits { + component: NumberComponent, + bits: u64, + limit: u64, + stage: String, + }, +} + +#[derive(Debug, Clone, PartialEq, Eq, Error, Serialize, Deserialize)] +pub enum NumericError { + #[error("numeric limit: {0}")] + Limit(NumericLimit), + #[error("invalid numeric literal")] + InvalidLiteral, + #[error("numeric literal exceeds its digit or byte limit")] + LiteralTooLong, + #[error("decimal exponent is outside -128 through 128")] + DecimalExponent, + #[error("wire rational is not in canonical reduced form")] + NonCanonicalWire, + #[error("rational denominator is zero")] + ZeroDenominator, + #[error("division by zero")] + DivisionByZero, + #[error("zero to the power zero is undefined in this profile")] + ZeroPowerZero, + #[error("integer power is outside -16 through 16")] + IntegerPower, + #[error("dimension exponent at {axis:?} is outside -32 through 32: {value}")] + DimensionExponent { axis: DimensionAxis, value: i32 }, + #[error("unit scale must be strictly positive")] + UnitScale, + #[error("a linear unit must have zero offset")] + LinearOffset, + #[error("an affine point must have a distinct linear difference kind")] + DifferenceKind, + #[error("numeric kinds or dimensions are incompatible")] + IncompatibleTypes, + #[error("operation is not defined for affine points")] + AffineOperation, + #[error("AsKind requires an anonymous matching dimension and a linear target")] + KindAssertion, + #[error("request work limits exceed the provisional reference ceilings")] + InvalidWorkLimits, +} + +impl NumericError { + pub fn is_terminal_work_exhaustion(&self) -> bool { + matches!(self, Self::Limit(NumericLimit::Work(_))) + } +} + +#[cfg(test)] +mod tests; diff --git a/crates/oa-core/src/analysis_numeric/dimension.rs b/crates/oa-core/src/analysis_numeric/dimension.rs new file mode 100644 index 00000000..d6f6f524 --- /dev/null +++ b/crates/oa-core/src/analysis_numeric/dimension.rs @@ -0,0 +1,107 @@ +use super::NumericError; +use serde::{Deserialize, Serialize}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum DimensionAxis { + Length, + Mass, + Time, + ElectricCurrent, + Temperature, + Amount, + LuminousIntensity, +} + +impl DimensionAxis { + pub const ALL: [Self; 7] = [ + Self::Length, + Self::Mass, + Self::Time, + Self::ElectricCurrent, + Self::Temperature, + Self::Amount, + Self::LuminousIntensity, + ]; +} + +/// SI base-dimension vector in DimensionAxis::ALL order, each entry -32..=32. +/// This is a dimension, never a nominal quantity-kind compatibility proof. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[serde(try_from = "[i16; 7]", into = "[i16; 7]")] +pub struct Dimension([i16; 7]); + +impl Dimension { + pub const ZERO: Self = Self([0; 7]); + + pub fn new(exponents: [i16; 7]) -> Result { + for (index, value) in exponents.iter().copied().enumerate() { + if !(-32..=32).contains(&value) { + return Err(NumericError::DimensionExponent { + axis: DimensionAxis::ALL[index], + value: i32::from(value), + }); + } + } + Ok(Self(exponents)) + } + + pub fn exponents(self) -> [i16; 7] { + self.0 + } + + pub fn is_dimensionless(self) -> bool { + self == Self::ZERO + } + + pub fn checked_product(self, rhs: Self) -> Result { + self.combine(rhs, 1) + } + + pub fn checked_quotient(self, rhs: Self) -> Result { + self.combine(rhs, -1) + } + + pub fn checked_power(self, exponent: i8) -> Result { + if !(-super::MAX_INTEGER_POWER..=super::MAX_INTEGER_POWER).contains(&exponent) { + return Err(NumericError::IntegerPower); + } + let mut output = [0; 7]; + for (index, value) in self.0.iter().enumerate() { + output[index] = Self::checked_exponent(index, i32::from(*value) * i32::from(exponent))?; + } + Ok(Self(output)) + } + + fn combine(self, rhs: Self, sign: i32) -> Result { + let mut output = [0; 7]; + for (index, value) in self.0.iter().enumerate() { + output[index] = + Self::checked_exponent(index, i32::from(*value) + sign * i32::from(rhs.0[index]))?; + } + Ok(Self(output)) + } + + fn checked_exponent(index: usize, value: i32) -> Result { + if !(-32..=32).contains(&value) { + return Err(NumericError::DimensionExponent { + axis: DimensionAxis::ALL[index], + value, + }); + } + Ok(value as i16) + } +} + +impl TryFrom<[i16; 7]> for Dimension { + type Error = NumericError; + + fn try_from(value: [i16; 7]) -> Result { + Self::new(value) + } +} + +impl From for [i16; 7] { + fn from(value: Dimension) -> Self { + value.0 + } +} diff --git a/crates/oa-core/src/analysis_numeric/exact.rs b/crates/oa-core/src/analysis_numeric/exact.rs new file mode 100644 index 00000000..7075e6be --- /dev/null +++ b/crates/oa-core/src/analysis_numeric/exact.rs @@ -0,0 +1,469 @@ +use super::meter::{normalization_cost, parse_cost, product_cost, sum_cost, words}; +use super::{ + MAX_COMPONENT_BITS, MAX_COMPONENT_DIGITS, MAX_DECIMAL_EXPONENT, MAX_INTEGER_POWER, + MAX_INTERMEDIATE_BITS, MAX_LITERAL_BYTES, NumberComponent, NumericError, NumericLimit, + NumericOperation, WorkLimits, WorkMeter, +}; +use num_bigint::BigInt; +use num_integer::Integer; +use num_traits::{One, Signed, Zero}; +use serde::{Deserialize, Serialize}; +use std::cmp::Ordering; + +/// The interchange representation deliberately does not use num-bigint's serde +/// format or JSON numeric values. Duplicate/missing/unknown fields reject. +/// Its derived decoder allocates String fields before numeric validation; a +/// transport/document adapter must bound the encoded envelope and decoded text. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[serde(deny_unknown_fields)] +pub struct ExactWire { + pub numerator: String, + pub denominator: String, +} + +/// Reduced rational with positive denominator and <=4096-bit components. +/// +/// There are no unmetered arithmetic/ordering traits. Eq is structural equality +/// of already normalized bounded values, not an expression comparison API. +/// Standalone serde admission bounds the subsequent BigInt validation, not the +/// preceding String decoding. Document adapters must bound encoded/decoded input +/// and aggregate admission work. Evaluation uses one explicit WorkMeter. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[serde(try_from = "ExactWire", into = "ExactWire")] +pub struct Exact { + numerator: BigInt, + denominator: BigInt, +} + +impl Exact { + pub fn from_integer(value: i64) -> Self { + Self { + numerator: BigInt::from(value), + denominator: BigInt::one(), + } + } + + pub fn is_zero(&self) -> bool { + self.numerator.is_zero() + } + + pub fn is_positive(&self) -> bool { + self.numerator.is_positive() + } + + pub fn component_bits(&self) -> (u64, u64) { + (self.numerator.bits(), self.denominator.bits()) + } + + pub fn to_wire(&self) -> ExactWire { + ExactWire { + numerator: self.numerator.to_string(), + denominator: self.denominator.to_string(), + } + } + + /// Canonical *literal* spelling, not a generic expression formatter. + /// Negative literal nodes use ratio(-n,d), even when d=1. A leading minus + /// belongs to the future expression parser's UnaryNegate node instead. + pub fn canonical_literal(&self) -> String { + if self.denominator.is_one() && !self.numerator.is_negative() { + self.numerator.to_string() + } else { + format!("ratio({}, {})", self.numerator, self.denominator) + } + } + + pub fn from_wire(wire: &ExactWire, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + let n_digits = wire_digits(&wire.numerator, true)?; + let d_digits = wire_digits(&wire.denominator, false)?; + let n_bound = decimal_bits(n_digits.len()); + let d_bound = decimal_bits(d_digits.len()); + meter.numeric( + NumericOperation::ParseWire, + parse_cost(n_digits.len(), n_bound) + + parse_cost(d_digits.len(), d_bound) + + normalization_cost(n_bound, d_bound), + )?; + let numerator = parse_integer(&wire.numerator)?; + let denominator = parse_integer(&wire.denominator)?; + Self::check_bits(&numerator, &denominator, MAX_COMPONENT_BITS, "wire")?; + if denominator.is_zero() { + return Err(NumericError::ZeroDenominator); + } + if !numerator.gcd(&denominator).is_one() { + return Err(NumericError::NonCanonicalWire); + } + Ok(Self { + numerator, + denominator, + }) + } + + /// Reads one unsigned decimal/integer atom or a ratio(n,d) literal only. + /// It does not parse expressions, unary operators, units, calls or names. + /// Source ratios/decimals may reduce; wire values must already be canonical. + pub fn parse_literal(source: &str, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + if source.len() > MAX_LITERAL_BYTES { + return Err(NumericError::LiteralTooLong); + } + let source = trim_ascii(source); + if let Some(body) = source.strip_prefix("ratio(") { + let body = body.strip_suffix(')').ok_or(NumericError::InvalidLiteral)?; + let (n, d) = body.split_once(',').ok_or(NumericError::InvalidLiteral)?; + return Self::parse_ratio(trim_ascii(n), trim_ascii(d), meter); + } + Self::parse_decimal(source, meter) + } + + fn parse_ratio(n: &str, d: &str, meter: &mut WorkMeter) -> Result { + let n_digits = source_integer_digits(n, true)?; + let d_digits = source_integer_digits(d, false)?; + let n_bound = decimal_bits(n_digits.len()); + let d_bound = decimal_bits(d_digits.len()); + Self::check_estimates(n_bound, d_bound)?; + meter.numeric( + NumericOperation::ParseLiteral, + parse_cost(n_digits.len(), n_bound) + + parse_cost(d_digits.len(), d_bound) + + normalization_cost(n_bound, d_bound), + )?; + Self::normalize_precharged(parse_integer(n)?, parse_integer(d)?) + } + + fn parse_decimal(source: &str, meter: &mut WorkMeter) -> Result { + let mut parts = source.split(['e', 'E']); + let mantissa = parts.next().ok_or(NumericError::InvalidLiteral)?; + let exponent = match parts.next() { + Some(text) => parse_exponent(text)?, + None => 0, + }; + if parts.next().is_some() { + return Err(NumericError::InvalidLiteral); + } + let (whole, fraction) = match mantissa.split_once('.') { + Some((whole, fraction)) if !fraction.is_empty() => (whole, fraction), + Some(_) => return Err(NumericError::InvalidLiteral), + None => (mantissa, ""), + }; + source_integer_digits(whole, false)?; + if !fraction.bytes().all(|byte| byte.is_ascii_digit()) { + return Err(NumericError::InvalidLiteral); + } + let digit_count = whole.len() + fraction.len(); + if digit_count > MAX_COMPONENT_DIGITS { + return Err(NumericError::LiteralTooLong); + } + let adjustment = exponent - fraction.len() as i32; + let power = adjustment.unsigned_abs(); + let mantissa_bound = decimal_bits(digit_count); + let scale_bound = decimal_bits(power as usize + 1); + let (n_bound, d_bound) = if adjustment >= 0 { + (mantissa_bound + scale_bound, 1) + } else { + (mantissa_bound, scale_bound) + }; + Self::check_estimates(n_bound, d_bound)?; + // Fixed logical allowance for constructing 10^power; independent of + // num-bigint's selected multiplication/exponentiation implementation. + let power_steps = 1 + 2 * u64::from(u32::BITS - power.leading_zeros()); + meter.numeric( + NumericOperation::ParseLiteral, + parse_cost(digit_count, mantissa_bound) + + power_steps * product_cost(scale_bound, scale_bound) + + product_cost(mantissa_bound, scale_bound) + + normalization_cost(n_bound, d_bound), + )?; + let digits = format!("{whole}{fraction}"); + let mut numerator = parse_integer(&digits)?; + let scale = BigInt::from(10_u8).pow(power); + let denominator = if adjustment >= 0 { + numerator *= scale; + BigInt::one() + } else { + scale + }; + Self::normalize_precharged(numerator, denominator) + } + + pub fn add(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + self.add_or_subtract(rhs, false, meter) + } + + pub fn subtract(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + self.add_or_subtract(rhs, true, meter) + } + + fn add_or_subtract( + &self, + rhs: &Self, + subtract: bool, + meter: &mut WorkMeter, + ) -> Result { + let (a, b) = self.component_bits(); + let (c, d) = rhs.component_bits(); + let left_bound = a + d; + let right_bound = c + b; + let n_bound = left_bound.max(right_bound) + 1; + let d_bound = b + d; + Self::check_estimates(n_bound, d_bound)?; + meter.numeric( + if subtract { + NumericOperation::Subtract + } else { + NumericOperation::Add + }, + product_cost(a, d) + + product_cost(c, b) + + sum_cost(left_bound, right_bound) + + product_cost(b, d) + + normalization_cost(n_bound, d_bound), + )?; + let left = &self.numerator * &rhs.denominator; + let right = &rhs.numerator * &self.denominator; + let numerator = if subtract { left - right } else { left + right }; + let denominator = &self.denominator * &rhs.denominator; + Self::normalize_precharged(numerator, denominator) + } + + pub fn multiply(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + let (a, b) = self.component_bits(); + let (c, d) = rhs.component_bits(); + Self::check_estimates(a + c, b + d)?; + meter.numeric( + NumericOperation::Multiply, + product_cost(a, c) + product_cost(b, d) + normalization_cost(a + c, b + d), + )?; + Self::normalize_precharged( + &self.numerator * &rhs.numerator, + &self.denominator * &rhs.denominator, + ) + } + + pub fn divide(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + let (a, b) = self.component_bits(); + let (c, d) = rhs.component_bits(); + Self::check_estimates(a + d, b + c)?; + meter.numeric( + NumericOperation::Divide, + product_cost(a, d) + product_cost(b, c) + normalization_cost(a + d, b + c), + )?; + if rhs.is_zero() { + return Err(NumericError::DivisionByZero); + } + Self::normalize_precharged( + &self.numerator * &rhs.denominator, + &self.denominator * &rhs.numerator, + ) + } + + pub fn compare(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + let (a, b) = self.component_bits(); + let (c, d) = rhs.component_bits(); + Self::check_estimates((a + d).max(c + b), 1)?; + meter.numeric( + NumericOperation::Compare, + product_cost(a, d) + product_cost(c, b) + sum_cost(a + d, c + b), + )?; + Ok((&self.numerator * &rhs.denominator).cmp(&(&rhs.numerator * &self.denominator))) + } + + pub fn negated(&self, meter: &mut WorkMeter) -> Result { + meter.numeric(NumericOperation::Negate, self.copy_cost())?; + Ok(Self { + numerator: -&self.numerator, + denominator: self.denominator.clone(), + }) + } + + pub fn absolute(&self, meter: &mut WorkMeter) -> Result { + meter.numeric(NumericOperation::Absolute, self.copy_cost())?; + Ok(Self { + numerator: self.numerator.abs(), + denominator: self.denominator.clone(), + }) + } + + pub fn reciprocal(&self, meter: &mut WorkMeter) -> Result { + meter.numeric(NumericOperation::Reciprocal, self.copy_cost())?; + if self.is_zero() { + return Err(NumericError::DivisionByZero); + } + Ok(Self { + numerator: if self.numerator.is_negative() { + -&self.denominator + } else { + self.denominator.clone() + }, + denominator: self.numerator.abs(), + }) + } + + /// Fixed left-to-right repeated multiplication, at most 16 multiplications. + /// Each reduced stage obeys the same component bound; no large power is + /// allocated and subsequently discarded after discovering it is oversized. + pub fn power(&self, exponent: i8, meter: &mut WorkMeter) -> Result { + meter.numeric(NumericOperation::Power, self.copy_cost())?; + if !(-MAX_INTEGER_POWER..=MAX_INTEGER_POWER).contains(&exponent) { + return Err(NumericError::IntegerPower); + } + if self.is_zero() && exponent == 0 { + return Err(NumericError::ZeroPowerZero); + } + let factor = if exponent < 0 { + self.reciprocal(meter)? + } else { + self.clone() + }; + let mut value = Self::from_integer(1); + for _ in 0..exponent.unsigned_abs() { + value = value.multiply(&factor, meter)?; + } + Ok(value) + } + + pub(super) fn copy_cost(&self) -> u64 { + let (n, d) = self.component_bits(); + 1 + words(n) + words(d) + } + + fn normalize_precharged( + mut numerator: BigInt, + mut denominator: BigInt, + ) -> Result { + Self::check_bits( + &numerator, + &denominator, + MAX_INTERMEDIATE_BITS, + "intermediate", + )?; + if denominator.is_zero() { + return Err(NumericError::ZeroDenominator); + } + if denominator.is_negative() { + numerator = -numerator; + denominator = -denominator; + } + let gcd = numerator.gcd(&denominator); + numerator /= &gcd; + denominator /= gcd; + Self::check_bits(&numerator, &denominator, MAX_COMPONENT_BITS, "reduced")?; + Ok(Self { + numerator, + denominator, + }) + } + + fn check_estimates(n: u64, d: u64) -> Result<(), NumericError> { + Self::check_bit_count( + n, + NumberComponent::Numerator, + MAX_INTERMEDIATE_BITS, + "predicted", + )?; + Self::check_bit_count( + d, + NumberComponent::Denominator, + MAX_INTERMEDIATE_BITS, + "predicted", + ) + } + + fn check_bits(n: &BigInt, d: &BigInt, limit: u64, stage: &str) -> Result<(), NumericError> { + Self::check_bit_count(n.bits(), NumberComponent::Numerator, limit, stage)?; + Self::check_bit_count(d.bits(), NumberComponent::Denominator, limit, stage) + } + + fn check_bit_count( + bits: u64, + component: NumberComponent, + limit: u64, + stage: &str, + ) -> Result<(), NumericError> { + if bits > limit { + return Err(NumericError::Limit(NumericLimit::Bits { + component, + bits, + limit, + stage: stage.to_owned(), + })); + } + Ok(()) + } +} + +impl TryFrom for Exact { + type Error = NumericError; + + fn try_from(value: ExactWire) -> Result { + // BigInt validation is bounded after ExactWire strings have decoded. + // The adapter owns envelope/text/aggregate admission bounds and must not + // reset evaluation meters. + Self::from_wire(&value, &mut WorkMeter::new(WorkLimits::REFERENCE)) + } +} + +impl From for ExactWire { + fn from(value: Exact) -> Self { + value.to_wire() + } +} + +fn trim_ascii(text: &str) -> &str { + text.trim_matches(|ch: char| ch.is_ascii_whitespace()) +} + +fn source_integer_digits(text: &str, signed: bool) -> Result<&str, NumericError> { + let digits = if signed { + text.strip_prefix('-').unwrap_or(text) + } else { + text + }; + if digits.len() > MAX_COMPONENT_DIGITS { + return Err(NumericError::LiteralTooLong); + } + if digits.is_empty() || !digits.bytes().all(|byte| byte.is_ascii_digit()) { + return Err(NumericError::InvalidLiteral); + } + Ok(digits) +} + +fn wire_digits(text: &str, signed: bool) -> Result<&str, NumericError> { + let digits = source_integer_digits(text, signed).map_err(|error| match error { + NumericError::LiteralTooLong => error, + _ => NumericError::NonCanonicalWire, + })?; + if (digits.len() > 1 && digits.starts_with('0')) || (text.starts_with('-') && digits == "0") { + return Err(NumericError::NonCanonicalWire); + } + Ok(digits) +} + +fn parse_integer(text: &str) -> Result { + BigInt::parse_bytes(text.as_bytes(), 10).ok_or(NumericError::InvalidLiteral) +} + +fn parse_exponent(text: &str) -> Result { + let (negative, digits) = if let Some(digits) = text.strip_prefix('-') { + (true, digits) + } else { + (false, text.strip_prefix('+').unwrap_or(text)) + }; + if digits.is_empty() || !digits.bytes().all(|byte| byte.is_ascii_digit()) { + return Err(NumericError::InvalidLiteral); + } + let mut value = 0_i32; + for digit in digits.bytes() { + value = value * 10 + i32::from(digit - b'0'); + if value > MAX_DECIMAL_EXPONENT { + return Err(NumericError::DecimalExponent); + } + } + Ok(if negative { -value } else { value }) +} + +fn decimal_bits(digits: usize) -> u64 { + // 3.322 exceeds log2(10); dimensions are bounded before this conversion. + (digits as u64 * 3322).div_ceil(1000).max(1) +} diff --git a/crates/oa-core/src/analysis_numeric/fixtures/r7-literal-boundaries.json b/crates/oa-core/src/analysis_numeric/fixtures/r7-literal-boundaries.json new file mode 100644 index 00000000..9c8aa284 --- /dev/null +++ b/crates/oa-core/src/analysis_numeric/fixtures/r7-literal-boundaries.json @@ -0,0 +1,32 @@ +[ + { + "canonical_source": "1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "expression": { + "Number": { + "denominator": "1", + "numerator": "1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + } + }, + "name": "ten_to_300" + }, + { + "canonical_source": "ratio(1, 522194440706576253345876355358312191289982124523691890192116741641976953985778728424413405967498779170445053357219631418993786719092896803631618043925682638972978488271854999170180795067191859157214035005927973113188159419698856372836167342172293308748403954352901852035642024370059304557233988891799014503343469488440893892973452815095130470299789726716411734651513348221529512507986199933857107770846917779942645743159118957217248367043905936319748237550094520674504208530837546834166925275516486044134775384991808184705966507606898412918594045916828375610659246423184062775112999150206172392431297837246097308511903252956622805412865917690043804311051417135098849101156584508839003337597742539960818209685142687562392007453579567729991395256699805775897135553415567045292136442139895777424891477161767258532611634530697452993846501061481697843891439474220308003706472837459911525285821188577408160690315522951458068463354171428220365223949985950890732881736611925133626529949897998045399734600887312408859224933727829625089164535236559716582775403784110923285873186648442456409760158728501220463308455437074192539205964902261490928669488824051563042951500651206733594863336608245755565801460390869016718045121902354170201577095168)", + "expression": { + "Number": { + "denominator": "522194440706576253345876355358312191289982124523691890192116741641976953985778728424413405967498779170445053357219631418993786719092896803631618043925682638972978488271854999170180795067191859157214035005927973113188159419698856372836167342172293308748403954352901852035642024370059304557233988891799014503343469488440893892973452815095130470299789726716411734651513348221529512507986199933857107770846917779942645743159118957217248367043905936319748237550094520674504208530837546834166925275516486044134775384991808184705966507606898412918594045916828375610659246423184062775112999150206172392431297837246097308511903252956622805412865917690043804311051417135098849101156584508839003337597742539960818209685142687562392007453579567729991395256699805775897135553415567045292136442139895777424891477161767258532611634530697452993846501061481697843891439474220308003706472837459911525285821188577408160690315522951458068463354171428220365223949985950890732881736611925133626529949897998045399734600887312408859224933727829625089164535236559716582775403784110923285873186648442456409760158728501220463308455437074192539205964902261490928669488824051563042951500651206733594863336608245755565801460390869016718045121902354170201577095168", + "numerator": "1" + } + }, + "name": "one_over_two_to_4095" + }, + { + "canonical_source": "ratio(-1044388881413152506691752710716624382579964249047383780384233483283953907971557456848826811934997558340890106714439262837987573438185793607263236087851365277945956976543709998340361590134383718314428070011855946226376318839397712745672334684344586617496807908705803704071284048740118609114467977783598029006686938976881787785946905630190260940599579453432823469303026696443059025015972399867714215541693835559885291486318237914434496734087811872639496475100189041349008417061675093668333850551032972088269550769983616369411933015213796825837188091833656751221318492846368125550225998300412344784862595674492194617023806505913245610825731835380087608622102834270197698202313169017678006675195485079921636419370285375124784014907159135459982790513399611551794271106831134090584272884279791554849782954323534517065223269061394905987693002122963395687782878948440616007412945674919823050571642377154816321380631045902916136926708342856440730447899971901781465763473223850267253059899795996090799469201774624817718449867455659250178329070473119433165550807568221846571746373296884912819520317457002440926616910874148385078411929804522981857338977648103126085903001302413467189726673216491511131602920781738033436090243804708340403154190335, 1)", + "expression": { + "Number": { + "denominator": "1", + "numerator": "-1044388881413152506691752710716624382579964249047383780384233483283953907971557456848826811934997558340890106714439262837987573438185793607263236087851365277945956976543709998340361590134383718314428070011855946226376318839397712745672334684344586617496807908705803704071284048740118609114467977783598029006686938976881787785946905630190260940599579453432823469303026696443059025015972399867714215541693835559885291486318237914434496734087811872639496475100189041349008417061675093668333850551032972088269550769983616369411933015213796825837188091833656751221318492846368125550225998300412344784862595674492194617023806505913245610825731835380087608622102834270197698202313169017678006675195485079921636419370285375124784014907159135459982790513399611551794271106831134090584272884279791554849782954323534517065223269061394905987693002122963395687782878948440616007412945674919823050571642377154816321380631045902916136926708342856440730447899971901781465763473223850267253059899795996090799469201774624817718449867455659250178329070473119433165550807568221846571746373296884912819520317457002440926616910874148385078411929804522981857338977648103126085903001302413467189726673216491511131602920781738033436090243804708340403154190335" + } + }, + "name": "negative_4096_bit_bound" + } +] diff --git a/crates/oa-core/src/analysis_numeric/meter.rs b/crates/oa-core/src/analysis_numeric/meter.rs new file mode 100644 index 00000000..4a3a0486 --- /dev/null +++ b/crates/oa-core/src/analysis_numeric/meter.rs @@ -0,0 +1,240 @@ +use super::{NumericError, NumericLimit}; +use serde::{Deserialize, Serialize}; +use thiserror::Error; + +/// Every event is charged once per dynamic occurrence, before entering it. +/// +/// A Call expression therefore charges Expression and CalculationEntry; a +/// Property read charges Expression and PropertyBinding. List element visits +/// are additional to evaluation of their expressions. Only executed branches +/// are charged. Targets are sorted by category (properties, then checks), then +/// stable UUID bytes, by the integrating evaluator. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum EvaluationStep { + Target, + Expression, + CalculationEntry, + PropertyBinding, + ListElement, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum NumericOperation { + ParseWire, + ParseLiteral, + Add, + Subtract, + Multiply, + Divide, + Compare, + Negate, + Absolute, + Reciprocal, + Power, + KindAssertion, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum WorkResource { + DynamicEvents, + NumericUnits, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum WorkSite { + Evaluation(EvaluationStep), + Numeric(NumericOperation), +} + +/// Failed reservations consume no partial charge. The first failure is latched. +#[derive(Debug, Clone, PartialEq, Eq, Error, Serialize, Deserialize)] +#[error("{resource:?}: used {used}, requested {requested}, limit {limit}, at {site:?}")] +pub struct WorkExhaustion { + pub resource: WorkResource, + pub used: u64, + pub requested: u64, + pub limit: u64, + pub site: WorkSite, +} + +/// Provisional calibration ceilings, not measured execution-time guarantees. +/// +/// Effective limits, profile identity, capture, targets and context must all be +/// recorded in request/result/frozen identity. A caller may lower these ceilings. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(try_from = "WorkLimitsWire", into = "WorkLimitsWire")] +pub struct WorkLimits { + dynamic_events: u64, + numeric_units: u64, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(deny_unknown_fields)] +struct WorkLimitsWire { + dynamic_events: u64, + numeric_units: u64, +} + +impl WorkLimits { + pub const REFERENCE: Self = Self { + dynamic_events: 1_000_000, + numeric_units: 50_000_000, + }; + + pub fn new(dynamic_events: u64, numeric_units: u64) -> Result { + if dynamic_events > Self::REFERENCE.dynamic_events + || numeric_units > Self::REFERENCE.numeric_units + { + return Err(NumericError::InvalidWorkLimits); + } + Ok(Self { + dynamic_events, + numeric_units, + }) + } + + pub fn dynamic_events(self) -> u64 { + self.dynamic_events + } + + pub fn numeric_units(self) -> u64 { + self.numeric_units + } +} + +impl TryFrom for WorkLimits { + type Error = NumericError; + + fn try_from(value: WorkLimitsWire) -> Result { + Self::new(value.dynamic_events, value.numeric_units) + } +} + +impl From for WorkLimitsWire { + fn from(value: WorkLimits) -> Self { + Self { + dynamic_events: value.dynamic_events, + numeric_units: value.numeric_units, + } + } +} + +#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize, Deserialize)] +#[serde(deny_unknown_fields)] +pub struct WorkUsage { + pub dynamic_events: u64, + pub numeric_units: u64, +} + +/// Intentionally neither Clone nor Default: pass the same mutable meter through +/// every target, numeric operation and expanded call in one evaluation request. +/// +/// Exhaustion is terminal. Integrators must stop traversing siblings/targets and +/// mark already collected causes as incomplete. Replaying an aggregate cache +/// cost is insufficient if it changes the exact exhaustion location; initially +/// retain logical traversal even when numerical values come from a cache. +#[derive(Debug)] +pub struct WorkMeter { + limits: WorkLimits, + usage: WorkUsage, + exhausted: Option, +} + +impl WorkMeter { + pub fn new(limits: WorkLimits) -> Self { + Self { + limits, + usage: WorkUsage::default(), + exhausted: None, + } + } + + pub fn limits(&self) -> WorkLimits { + self.limits + } + + pub fn usage(&self) -> WorkUsage { + self.usage + } + + pub fn exhaustion(&self) -> Option<&WorkExhaustion> { + self.exhausted.as_ref() + } + + pub fn ensure_active(&self) -> Result<(), NumericError> { + match &self.exhausted { + Some(failure) => Err(NumericError::Limit(NumericLimit::Work(failure.clone()))), + None => Ok(()), + } + } + + pub fn visit(&mut self, step: EvaluationStep) -> Result<(), NumericError> { + self.reserve(WorkResource::DynamicEvents, 1, WorkSite::Evaluation(step)) + } + + pub(super) fn numeric( + &mut self, + operation: NumericOperation, + units: u64, + ) -> Result<(), NumericError> { + self.reserve( + WorkResource::NumericUnits, + units, + WorkSite::Numeric(operation), + ) + } + + fn reserve( + &mut self, + resource: WorkResource, + requested: u64, + site: WorkSite, + ) -> Result<(), NumericError> { + self.ensure_active()?; + let (used, limit) = match resource { + WorkResource::DynamicEvents => (self.usage.dynamic_events, self.limits.dynamic_events), + WorkResource::NumericUnits => (self.usage.numeric_units, self.limits.numeric_units), + }; + // Subtraction is safe: only successful reservations update usage. + if requested > limit - used { + let failure = WorkExhaustion { + resource, + used, + requested, + limit, + site, + }; + self.exhausted = Some(failure.clone()); + return Err(NumericError::Limit(NumericLimit::Work(failure))); + } + match resource { + WorkResource::DynamicEvents => self.usage.dynamic_events += requested, + WorkResource::NumericUnits => self.usage.numeric_units += requested, + } + Ok(()) + } +} + +// Logical 64-bit words are platform independent. These are deterministic +// accounting weights, not a claim about num-bigint's internal algorithm/timing. +pub(super) fn words(bits: u64) -> u64 { + bits.max(1).div_ceil(64) +} + +pub(super) fn product_cost(a_bits: u64, b_bits: u64) -> u64 { + 1 + words(a_bits) * words(b_bits) +} + +pub(super) fn sum_cost(a_bits: u64, b_bits: u64) -> u64 { + 1 + words(a_bits.max(b_bits)) +} + +pub(super) fn normalization_cost(n_bits: u64, d_bits: u64) -> u64 { + let width = words(n_bits.max(d_bits)); + // 64*w² for GCD plus 2*w² for the two quotient operations. + 1 + 66 * width * width +} + +pub(super) fn parse_cost(digits: usize, estimated_bits: u64) -> u64 { + 1 + digits as u64 * words(estimated_bits) +} diff --git a/crates/oa-core/src/analysis_numeric/quantity.rs b/crates/oa-core/src/analysis_numeric/quantity.rs new file mode 100644 index 00000000..7213e5ba --- /dev/null +++ b/crates/oa-core/src/analysis_numeric/quantity.rs @@ -0,0 +1,378 @@ +use super::{Dimension, Exact, MAX_INTEGER_POWER, NumericError, NumericOperation, WorkMeter}; +use std::cmp::Ordering; + +/// K is supplied by the common resolver's verified nominal compatibility +/// relation. It is not inferred from dimension/name/symbol/archive bytes here. +/// Coordinate basis/algebra/difference-kind closure must be part of that proof. +/// Exact definition references and pins remain the caller's provenance. +/// K must be a bounded, cheap-to-clone/compare verified handle. Constructing or +/// comparing an unbounded rooted contract graph is resolver admission work and +/// must not be hidden inside K's Clone/Eq implementations. Rust trait bounds do +/// not enforce this resource contract. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ResolvedKind { + key: K, + dimension: Dimension, + difference: Option, +} + +impl ResolvedKind { + pub fn linear(key: K, dimension: Dimension) -> Self { + Self { + key, + dimension, + difference: None, + } + } + + pub fn key(&self) -> &K { + &self.key + } + + pub fn dimension(&self) -> Dimension { + self.dimension + } + + pub fn is_affine(&self) -> bool { + self.difference.is_some() + } +} + +impl ResolvedKind { + pub fn affine(key: K, difference: &Self) -> Result { + if difference.is_affine() || key == difference.key { + return Err(NumericError::DifferenceKind); + } + Ok(Self { + key, + dimension: difference.dimension, + difference: Some(difference.key.clone()), + }) + } + + pub fn difference_kind(&self) -> Option { + self.difference + .as_ref() + .map(|key| Self::linear(key.clone(), self.dimension)) + } +} + +/// Canonical coordinate = magnitude * scale + offset. +/// Unit symbols and display preferences are outside this numeric representation. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Unit { + kind: ResolvedKind, + scale: Exact, + offset: Exact, +} + +impl Unit { + pub fn new(kind: ResolvedKind, scale: Exact, offset: Exact) -> Result { + if !scale.is_positive() { + return Err(NumericError::UnitScale); + } + if !kind.is_affine() && !offset.is_zero() { + return Err(NumericError::LinearOffset); + } + Ok(Self { + kind, + scale, + offset, + }) + } + + pub fn kind(&self) -> &ResolvedKind { + &self.kind + } + + pub fn scale(&self) -> &Exact { + &self.scale + } + + pub fn offset(&self) -> &Exact { + &self.offset + } + + /// Fixed multiply-then-add path. Each reduced arithmetic stage is bounded. + /// A mathematically cancelling wider intermediate still reports NumericLimit; + /// replacing this path with a fused operation requires a new work profile. + pub fn to_canonical( + &self, + magnitude: &Exact, + meter: &mut WorkMeter, + ) -> Result { + magnitude + .multiply(&self.scale, meter)? + .add(&self.offset, meter) + } + + /// Fixed subtract-then-divide path; never rounds a coordinate. + pub fn from_canonical( + &self, + coordinate: &Exact, + meter: &mut WorkMeter, + ) -> Result { + coordinate + .subtract(&self.offset, meter)? + .divide(&self.scale, meter) + } + + pub fn convert( + &self, + magnitude: &Exact, + target: &Self, + meter: &mut WorkMeter, + ) -> Result { + meter.ensure_active()?; + if self.kind != target.kind { + return Err(NumericError::IncompatibleTypes); + } + target.from_canonical(&self.to_canonical(magnitude, meter)?, meter) + } +} + +/// Internal numerical types. Boolean/list/check semantics belong to the common +/// expression evaluator. Anonymous zero dimension normalizes to Number. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum NumericType { + Number, + Named(ResolvedKind), + Anonymous(Dimension), +} + +impl NumericType { + pub fn dimension(&self) -> Dimension { + match self { + Self::Number => Dimension::ZERO, + Self::Named(kind) => kind.dimension, + Self::Anonymous(dimension) => *dimension, + } + } + + pub fn is_affine(&self) -> bool { + matches!(self, Self::Named(kind) if kind.is_affine()) + } + + fn anonymous(dimension: Dimension) -> Self { + if dimension.is_dimensionless() { + Self::Number + } else { + Self::Anonymous(dimension) + } + } + + fn normalized(self) -> Self { + match self { + Self::Anonymous(dimension) => Self::anonymous(dimension), + other => other, + } + } +} + +/// A canonical rational coordinate with an internal numerical type. +/// +/// Derived Eq compares stored representation. Formal equality/ordering must call +/// compare(), which rejects mismatched nominal kinds instead of treating them +/// as a false predicate. Public property output must still check its declared +/// type and anchor the result to that declaration's exact definition reference. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct NumericValue { + value_type: NumericType, + coordinate: Exact, +} + +impl NumericValue { + pub fn new(value_type: NumericType, coordinate: Exact) -> Self { + Self { + value_type: value_type.normalized(), + coordinate, + } + } + + pub fn number(coordinate: Exact) -> Self { + Self::new(NumericType::Number, coordinate) + } + + pub fn from_unit( + magnitude: &Exact, + unit: &Unit, + meter: &mut WorkMeter, + ) -> Result { + meter.ensure_active()?; + Ok(Self::new( + NumericType::Named(unit.kind.clone()), + unit.to_canonical(magnitude, meter)?, + )) + } + + pub fn value_type(&self) -> &NumericType { + &self.value_type + } + + pub fn coordinate(&self) -> &Exact { + &self.coordinate + } + + pub fn display_in(&self, unit: &Unit, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + if !matches!(&self.value_type, NumericType::Named(kind) if kind == &unit.kind) { + return Err(NumericError::IncompatibleTypes); + } + unit.from_canonical(&self.coordinate, meter) + } + + pub fn add(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + let output = self.additive_type(rhs, false)?; + Ok(Self::new( + output, + self.coordinate.add(&rhs.coordinate, meter)?, + )) + } + + pub fn subtract(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + let output = self.additive_type(rhs, true)?; + Ok(Self::new( + output, + self.coordinate.subtract(&rhs.coordinate, meter)?, + )) + } + + fn additive_type(&self, rhs: &Self, subtract: bool) -> Result, NumericError> { + use NumericType::{Anonymous, Named, Number}; + match (&self.value_type, &rhs.value_type) { + (Number, Number) => Ok(Number), + (Anonymous(left), Anonymous(right)) if left == right => Ok(Anonymous(*left)), + (Named(left), Named(right)) => match (&left.difference, &right.difference) { + (None, None) if left == right => Ok(Named(left.clone())), + (Some(difference), Some(_)) if subtract && left == right => Ok(Named( + ResolvedKind::linear(difference.clone(), left.dimension), + )), + (Some(difference), None) + if difference == &right.key && left.dimension == right.dimension => + { + Ok(Named(left.clone())) + } + (None, Some(difference)) + if !subtract + && difference == &left.key + && left.dimension == right.dimension => + { + Ok(Named(right.clone())) + } + _ => Err(NumericError::IncompatibleTypes), + }, + _ => Err(NumericError::IncompatibleTypes), + } + } + + pub fn multiply(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + let output = self.multiplicative_type(rhs, false)?; + Ok(Self::new( + output, + self.coordinate.multiply(&rhs.coordinate, meter)?, + )) + } + + pub fn divide(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + let output = self.multiplicative_type(rhs, true)?; + Ok(Self::new( + output, + self.coordinate.divide(&rhs.coordinate, meter)?, + )) + } + + fn multiplicative_type( + &self, + rhs: &Self, + divide: bool, + ) -> Result, NumericError> { + use NumericType::Number; + if self.value_type.is_affine() || rhs.value_type.is_affine() { + return Err(NumericError::AffineOperation); + } + match (&self.value_type, &rhs.value_type) { + (Number, Number) => Ok(Number), + (_, Number) => Ok(self.value_type.clone()), + (Number, _) if !divide => Ok(rhs.value_type.clone()), + _ => { + let left = self.value_type.dimension(); + let right = rhs.value_type.dimension(); + let dimension = if divide { + left.checked_quotient(right)? + } else { + left.checked_product(right)? + }; + Ok(NumericType::anonymous(dimension)) + } + } + } + + pub fn negated(&self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + if self.value_type.is_affine() { + return Err(NumericError::AffineOperation); + } + Ok(Self::new( + self.value_type.clone(), + self.coordinate.negated(meter)?, + )) + } + + pub fn absolute(&self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + if self.value_type.is_affine() { + return Err(NumericError::AffineOperation); + } + Ok(Self::new( + self.value_type.clone(), + self.coordinate.absolute(meter)?, + )) + } + + pub fn power(&self, exponent: i8, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + if !(-MAX_INTEGER_POWER..=MAX_INTEGER_POWER).contains(&exponent) { + return Err(NumericError::IntegerPower); + } + if self.value_type.is_affine() { + return Err(NumericError::AffineOperation); + } + let output = match exponent { + 0 => NumericType::Number, + 1 => self.value_type.clone(), + _ => NumericType::anonymous(self.value_type.dimension().checked_power(exponent)?), + }; + Ok(Self::new(output, self.coordinate.power(exponent, meter)?)) + } + + pub fn compare(&self, rhs: &Self, meter: &mut WorkMeter) -> Result { + meter.ensure_active()?; + if self.value_type != rhs.value_type { + return Err(NumericError::IncompatibleTypes); + } + self.coordinate.compare(&rhs.coordinate, meter) + } + + pub fn as_kind( + &self, + target: &ResolvedKind, + meter: &mut WorkMeter, + ) -> Result { + meter.ensure_active()?; + if target.is_affine() + || matches!(self.value_type, NumericType::Named(_)) + || self.value_type.dimension() != target.dimension + { + return Err(NumericError::KindAssertion); + } + meter.numeric(NumericOperation::KindAssertion, self.coordinate.copy_cost())?; + Ok(Self::new( + NumericType::Named(target.clone()), + self.coordinate.clone(), + )) + } +} diff --git a/crates/oa-core/src/analysis_numeric/tests.rs b/crates/oa-core/src/analysis_numeric/tests.rs new file mode 100644 index 00000000..d30c8ea4 --- /dev/null +++ b/crates/oa-core/src/analysis_numeric/tests.rs @@ -0,0 +1,804 @@ +use super::*; +use num_bigint::BigInt; +use num_traits::One; +use std::cmp::Ordering; + +fn meter() -> WorkMeter { + WorkMeter::new(WorkLimits::REFERENCE) +} + +fn exact(n: impl ToString, d: impl ToString) -> Exact { + Exact::from_wire( + &ExactWire { + numerator: n.to_string(), + denominator: d.to_string(), + }, + &mut meter(), + ) + .unwrap() +} + +fn source(text: &str) -> Exact { + Exact::parse_literal(text, &mut meter()).unwrap() +} + +fn assert_fraction(value: &Exact, n: impl ToString, d: impl ToString) { + assert_eq!( + value.to_wire(), + ExactWire { + numerator: n.to_string(), + denominator: d.to_string(), + } + ); +} + +// Independent bounded i128 oracle. It does not call the production Exact/GCD +// implementation when deriving expected arithmetic or ordering. +fn small_fraction(mut n: i128, mut d: i128) -> (i128, i128) { + assert_ne!(d, 0); + if d < 0 { + n = -n; + d = -d; + } + let (mut a, mut b) = (n.abs(), d); + while b != 0 { + (a, b) = (b, a % b); + } + (n / a, d / a) +} + +#[test] +fn arithmetic_matches_independent_small_integer_oracle() { + for a in [-5_i128, -2, 0, 1, 4] { + for b in [1_i128, 2, 3, 7] { + for c in [-5_i128, -2, 0, 1, 4] { + for d in [1_i128, 2, 3, 7] { + let (an, ad) = small_fraction(a, b); + let (bn, bd) = small_fraction(c, d); + let left = exact(an, ad); + let right = exact(bn, bd); + let mut work = meter(); + let (n, den) = small_fraction(a * d + c * b, b * d); + assert_fraction(&left.add(&right, &mut work).unwrap(), n, den); + let (n, den) = small_fraction(a * d - c * b, b * d); + assert_fraction(&left.subtract(&right, &mut work).unwrap(), n, den); + let (n, den) = small_fraction(a * c, b * d); + assert_fraction(&left.multiply(&right, &mut work).unwrap(), n, den); + if c != 0 { + let (n, den) = small_fraction(a * d, b * c); + assert_fraction(&left.divide(&right, &mut work).unwrap(), n, den); + } else { + assert_eq!( + left.divide(&right, &mut work), + Err(NumericError::DivisionByZero) + ); + } + assert_eq!( + left.compare(&right, &mut work).unwrap(), + (a * d).cmp(&(c * b)) + ); + } + } + } + } +} + +#[test] +fn decimals_are_exact_and_source_ratios_reduce() { + assert_fraction( + &source("0.1").add(&source("0.2"), &mut meter()).unwrap(), + 3, + 10, + ); + assert_fraction(&source("0.50"), 1, 2); + assert_fraction(&source("12.50e-2"), 1, 8); + assert_fraction(&source("1e+3"), 1000, 1); + assert_fraction(&source("0001.2500"), 5, 4); + assert_fraction(&source(" ratio( -6, 8 ) "), -3, 4); + assert_fraction(&source("ratio(-0, 27)"), 0, 1); + assert_eq!(source("0.5").canonical_literal(), "ratio(1, 2)"); + assert_eq!(source("42").canonical_literal(), "42"); +} + +#[test] +fn powers_and_signs_have_explicit_domains() { + let x = exact(-2, 3); + assert_fraction(&x.power(3, &mut meter()).unwrap(), -8, 27); + assert_fraction(&x.power(-3, &mut meter()).unwrap(), -27, 8); + assert_fraction(&x.power(0, &mut meter()).unwrap(), 1, 1); + assert_fraction(&x.absolute(&mut meter()).unwrap(), 2, 3); + assert_fraction(&x.negated(&mut meter()).unwrap(), 2, 3); + assert_fraction(&x.reciprocal(&mut meter()).unwrap(), -3, 2); + let zero = Exact::from_integer(0); + assert_eq!( + zero.power(0, &mut meter()), + Err(NumericError::ZeroPowerZero) + ); + assert_eq!( + zero.power(-1, &mut meter()), + Err(NumericError::DivisionByZero) + ); + assert_eq!(x.power(17, &mut meter()), Err(NumericError::IntegerPower)); + assert_eq!( + x.power(i8::MIN, &mut meter()), + Err(NumericError::IntegerPower) + ); +} + +#[test] +fn canonical_wire_rejects_both_component_noncanonical_forms() { + for (n, d) in [ + ("+1", "1"), + ("01", "1"), + ("-0", "1"), + ("1", "+1"), + ("1", "-1"), + ("1", "01"), + ("2", "4"), + ("0", "3"), + ("", "1"), + ("1", ""), + ("1.0", "1"), + ("1", "1.0"), + ("1e1", "1"), + ("1", "1e1"), + (" 1", "1"), + ("1", "1 "), + ] { + assert!( + Exact::from_wire( + &ExactWire { + numerator: n.into(), + denominator: d.into() + }, + &mut meter(), + ) + .is_err(), + "accepted {n}/{d}" + ); + } + assert_eq!( + Exact::from_wire( + &ExactWire { + numerator: "1".into(), + denominator: "0".into() + }, + &mut meter() + ), + Err(NumericError::ZeroDenominator) + ); + assert_fraction(&exact(0, 1), 0, 1); + assert_fraction(&exact(-1, 2), -1, 2); +} + +#[test] +fn serde_uses_closed_canonical_string_wire() { + let value = exact(-3, 7); + let encoded = serde_json::to_value(&value).unwrap(); + assert_eq!( + encoded, + serde_json::json!({"numerator":"-3","denominator":"7"}) + ); + assert_eq!(serde_json::from_value::(encoded).unwrap(), value); + for invalid in [ + r#"{"numerator":1,"denominator":"2"}"#, + r#"{"numerator":"1","denominator":2}"#, + r#"{"numerator":"1","denominator":"2","other":0}"#, + r#"{"numerator":"1","numerator":"2","denominator":"3"}"#, + r#"{"numerator":"1"}"#, + r#"{"numerator":"2","denominator":"4"}"#, + ] { + assert!(serde_json::from_str::(invalid).is_err(), "{invalid}"); + } +} + +#[test] +fn literal_reader_does_not_fold_expression_unary_minus() { + assert_eq!( + Exact::parse_literal("-2", &mut meter()), + Err(NumericError::InvalidLiteral) + ); + let negative_literal = source("ratio(-2, 1)"); + assert_eq!(negative_literal.canonical_literal(), "ratio(-2, 1)"); + assert_eq!(source("2").negated(&mut meter()).unwrap(), negative_literal); + // Equality of coordinates does not claim AST equality. The expression + // parser must preserve UnaryNegate independently of its operand literal. + assert_eq!(source("2").canonical_literal(), "2"); +} + +#[test] +fn literal_syntax_and_decimal_exponent_are_bounded() { + for invalid in [ + "", + "-", + "+1", + ".5", + "1.", + "1.2.3", + "1e", + "1ee2", + "1e+-2", + "1_000", + "NaN", + "Infinity", + "1/2", + "ratio(1)", + "ratio(1,2,3)", + "ratio(1,-2)", + "ratio(+1,2)", + "ratio(1,2) + 1", + "１２", + ] { + assert!( + Exact::parse_literal(invalid, &mut meter()).is_err(), + "{invalid}" + ); + } + for invalid in ["1e129", "1e-129", "1e9999999999999999999999"] { + assert_eq!( + Exact::parse_literal(invalid, &mut meter()), + Err(NumericError::DecimalExponent) + ); + } + assert!(Exact::parse_literal("1e128", &mut meter()).is_ok()); + assert!(Exact::parse_literal("1e-128", &mut meter()).is_ok()); + assert_eq!( + Exact::parse_literal(&"1".repeat(MAX_COMPONENT_DIGITS + 1), &mut meter()), + Err(NumericError::LiteralTooLong) + ); + assert_eq!( + Exact::parse_literal(&" ".repeat(MAX_LITERAL_BYTES + 1), &mut meter()), + Err(NumericError::LiteralTooLong) + ); +} + +#[test] +fn full_independent_r7_packets_round_trip_as_literals_and_wire() { + let packets: serde_json::Value = + serde_json::from_str(include_str!("fixtures/r7-literal-boundaries.json")).unwrap(); + for packet in packets.as_array().unwrap() { + let wire: ExactWire = + serde_json::from_value(packet["expression"]["Number"].clone()).unwrap(); + let expected = Exact::from_wire(&wire, &mut meter()).unwrap(); + let spelling = packet["canonical_source"].as_str().unwrap(); + assert_eq!(expected.canonical_literal(), spelling); + assert_eq!( + Exact::parse_literal(spelling, &mut meter()).unwrap(), + expected + ); + let serialized = serde_json::to_string(&expected).unwrap(); + assert_eq!( + serde_json::from_str::(&serialized).unwrap(), + expected + ); + assert_eq!(expected.to_wire(), wire); + } +} + +#[test] +fn full_8193_bit_sum_intermediate_can_reduce_to_admitted_value() { + // N=(2^4096)-1, D=N-1. gcd(N,D)=1 and D is even. + // N/D + N/D = N/(D/2), although its un-reduced numerator needs 8193 bits. + let n = (BigInt::one() << 4096_usize) - 1_u8; + let d = &n - 1_u8; + let value = exact(&n, &d); + let result = value.add(&value, &mut meter()).unwrap(); + assert_fraction(&result, &n, &d / 2_u8); +} + +#[test] +fn cross_products_cancel_before_reduced_component_limit() { + let n = BigInt::one() << 4095_usize; + let d = &n - 1_u8; + let left = exact(&n, &d); + let right = exact(&d, &n); + assert_fraction(&left.multiply(&right, &mut meter()).unwrap(), 1, 1); + assert_fraction( + &left + .add(&left.negated(&mut meter()).unwrap(), &mut meter()) + .unwrap(), + 0, + 1, + ); +} + +#[test] +fn both_reduced_component_overflows_are_reported() { + let n = BigInt::one() << 4095_usize; + let mut work = meter(); + let failure = exact(&n, 1) + .multiply(&Exact::from_integer(2), &mut work) + .unwrap_err(); + assert!(matches!( + failure, + NumericError::Limit(NumericLimit::Bits { + component: NumberComponent::Numerator, + bits: 4097, + .. + }) + )); + assert!(work.exhaustion().is_none()); + let failure = exact(1, &n) + .divide(&Exact::from_integer(2), &mut work) + .unwrap_err(); + assert!(matches!( + failure, + NumericError::Limit(NumericLimit::Bits { + component: NumberComponent::Denominator, + bits: 4097, + .. + }) + )); + // Value overflow is a nonterminal supported-operation failure; fuel + // exhaustion, in contrast, terminates the entire request. + assert_fraction(&source("1").add(&source("1"), &mut work).unwrap(), 2, 1); +} + +#[test] +fn wire_rejects_4097_bits_before_gcd_can_reduce_them() { + let oversized = (BigInt::one() << 4096_usize).to_string(); + for wire in [ + ExactWire { + numerator: oversized.clone(), + denominator: "1".into(), + }, + ExactWire { + numerator: "1".into(), + denominator: oversized.clone(), + }, + ExactWire { + numerator: oversized.clone(), + denominator: oversized, + }, + ] { + assert!(matches!( + Exact::from_wire(&wire, &mut meter()), + Err(NumericError::Limit(NumericLimit::Bits { stage, .. })) if stage == "wire" + )); + } +} + +#[test] +fn numeric_precharge_precedes_big_integer_result_allocation() { + let n = BigInt::one() << 4095_usize; + let left = exact(&n, 1); + let mut work = WorkMeter::new(WorkLimits::new(10, 0).unwrap()); + let failure = left + .multiply(&Exact::from_integer(2), &mut work) + .unwrap_err(); + assert!(failure.is_terminal_work_exhaustion()); + assert_eq!(work.usage().numeric_units, 0); + assert!(matches!( + work.exhaustion().unwrap().site, + WorkSite::Numeric(NumericOperation::Multiply) + )); + // With available fuel the same operation reaches the 4097-bit result check. + assert!(matches!( + left.multiply(&Exact::from_integer(2), &mut meter()), + Err(NumericError::Limit(NumericLimit::Bits { .. })) + )); + let too_wide_wire = ExactWire { + numerator: (BigInt::one() << 4096_usize).to_string(), + denominator: "1".into(), + }; + let mut parse_work = WorkMeter::new(WorkLimits::new(0, 0).unwrap()); + assert!( + Exact::from_wire(&too_wide_wire, &mut parse_work) + .unwrap_err() + .is_terminal_work_exhaustion() + ); +} + +#[test] +fn provisional_limits_and_effective_limits_round_trip() { + let limits = WorkLimits::new(500, 2000).unwrap(); + let encoded = serde_json::to_value(limits).unwrap(); + assert_eq!( + encoded, + serde_json::json!({"dynamic_events":500,"numeric_units":2000}) + ); + assert_eq!( + serde_json::from_value::(encoded).unwrap(), + limits + ); + assert_eq!( + WorkLimits::new(1_000_001, 0), + Err(NumericError::InvalidWorkLimits) + ); + assert_eq!( + WorkLimits::new(0, 50_000_001), + Err(NumericError::InvalidWorkLimits) + ); + assert!( + serde_json::from_str::(r#"{"dynamic_events":1000001,"numeric_units":0}"#) + .is_err() + ); +} + +#[test] +fn exact_accounting_boundary_and_terminal_failure_are_stable() { + // One-word addition: three products at 2, one sum at 2, + // normalization at 67 => 75 logical numeric units. + let mut work = WorkMeter::new(WorkLimits::new(4, 75).unwrap()); + assert_fraction(&exact(1, 2).add(&exact(1, 3), &mut work).unwrap(), 5, 6); + assert_eq!(work.usage().numeric_units, 75); + assert!(work.exhaustion().is_none()); + let first = Exact::from_integer(1).negated(&mut work).unwrap_err(); + let at_failure = work.usage(); + assert_eq!( + work.exhaustion().unwrap(), + &WorkExhaustion { + resource: WorkResource::NumericUnits, + used: 75, + requested: 3, + limit: 75, + site: WorkSite::Numeric(NumericOperation::Negate), + } + ); + assert_eq!(work.visit(EvaluationStep::Target).unwrap_err(), first); + assert_eq!( + Exact::from_integer(1) + .divide(&Exact::from_integer(0), &mut work) + .unwrap_err(), + first + ); + assert_eq!( + work.numeric(NumericOperation::Compare, 0).unwrap_err(), + first + ); + assert_eq!(work.usage(), at_failure); +} + +#[test] +fn zero_cost_and_maximum_reservation_do_not_underflow_or_reactivate() { + let mut work = WorkMeter::new(WorkLimits::new(0, 0).unwrap()); + work.numeric(NumericOperation::Compare, 0).unwrap(); + let failure = work + .numeric(NumericOperation::Multiply, u64::MAX) + .unwrap_err(); + assert!(failure.is_terminal_work_exhaustion()); + assert_eq!(work.usage(), WorkUsage::default()); + assert_eq!( + work.numeric(NumericOperation::Compare, 0).unwrap_err(), + failure + ); + let mut dynamic = WorkMeter::new(WorkLimits::new(0, 5).unwrap()); + assert!(dynamic.visit(EvaluationStep::Target).is_err()); + assert_eq!(dynamic.usage(), WorkUsage::default()); +} + +#[test] +fn multiple_targets_share_one_aggregate_meter() { + let mut work = WorkMeter::new(WorkLimits::new(3, 50).unwrap()); + work.visit(EvaluationStep::Target).unwrap(); + work.visit(EvaluationStep::Expression).unwrap(); + work.visit(EvaluationStep::Target).unwrap(); + let failure = work.visit(EvaluationStep::Expression).unwrap_err(); + assert!(failure.is_terminal_work_exhaustion()); + assert_eq!(work.usage().dynamic_events, 3); +} + +// A direct bounded call-tree workload, not an expression interpreter/dialect. +fn expanded_calls( + depth: u8, + x: u64, + work: &mut WorkMeter, + entered: &mut u64, +) -> Result { + work.visit(EvaluationStep::CalculationEntry)?; + *entered += 1; + if depth == 0 { + return Ok(x); + } + let left = expanded_calls(depth - 1, 2 * x, work, entered)?; + let right = expanded_calls(depth - 1, 2 * x + 1, work, entered)?; + Ok(left + right) +} + +#[test] +fn c1_expanded_call_witness_terminates_at_dynamic_limit() { + let mut work = WorkMeter::new(WorkLimits::new(10_000, 0).unwrap()); + let mut entered = 0; + let failure = expanded_calls(30, 0, &mut work, &mut entered).unwrap_err(); + assert!(failure.is_terminal_work_exhaustion()); + assert_eq!(entered, 10_000); + assert_eq!(work.usage().dynamic_events, 10_000); + assert_eq!( + work.exhaustion().unwrap().site, + WorkSite::Evaluation(EvaluationStep::CalculationEntry) + ); + // Nearby finite control: 63 invocations, leaves 0..31, sum 496. + let mut bounded = WorkMeter::new(WorkLimits::new(63, 0).unwrap()); + let mut entered = 0; + assert_eq!( + expanded_calls(5, 0, &mut bounded, &mut entered).unwrap(), + 496 + ); + assert_eq!(entered, 63); + assert!(bounded.exhaustion().is_none()); +} + +fn dim(value: [i16; 7]) -> Dimension { + Dimension::new(value).unwrap() +} + +fn linear(key: &str, dimension: Dimension) -> ResolvedKind { + ResolvedKind::linear(key.to_owned(), dimension) +} + +fn named(n: i64, kind: &ResolvedKind) -> NumericValue { + NumericValue::new(NumericType::Named(kind.clone()), Exact::from_integer(n)) +} + +#[test] +fn dimensions_use_checked_seven_axis_integer_algebra() { + let length = dim([1, 0, 0, 0, 0, 0, 0]); + let mass = dim([0, 1, 0, 0, 0, 0, 0]); + let time = dim([0, 0, 1, 0, 0, 0, 0]); + assert_eq!( + mass.checked_product(length) + .unwrap() + .checked_quotient(time.checked_power(2).unwrap()) + .unwrap(), + dim([1, 1, -2, 0, 0, 0, 0]) + ); + assert!(time.checked_quotient(time).unwrap().is_dimensionless()); + assert!(matches!( + dim([32, 0, 0, 0, 0, 0, 0]).checked_product(length), + Err(NumericError::DimensionExponent { + axis: DimensionAxis::Length, + value: 33 + }) + )); + assert!(dim([0, 0, -32, 0, 0, 0, 0]).checked_quotient(time).is_err()); + assert!(length.checked_power(i8::MIN).is_err()); + assert!(Dimension::new([33, 0, 0, 0, 0, 0, 0]).is_err()); + assert_eq!( + serde_json::to_value(time).unwrap(), + serde_json::json!([0, 0, 1, 0, 0, 0, 0]) + ); + for invalid in ["[0,0,33,0,0,0,0]", "[0,0,1]", "[0,0,1,0,0,0,0,0]"] { + assert!(serde_json::from_str::(invalid).is_err()); + } +} + +#[test] +fn duration_unit_coordinates_are_exact_and_nominal() { + let duration = linear("duration", dim([0, 0, 1, 0, 0, 0, 0])); + let s = Unit::new(duration.clone(), source("1"), source("0")).unwrap(); + let ms = Unit::new(duration.clone(), source("0.001"), source("0")).unwrap(); + assert_fraction(&ms.convert(&source("750"), &s, &mut meter()).unwrap(), 3, 4); + let receive = NumericValue::from_unit(&source("750"), &ms, &mut meter()).unwrap(); + let dispatch = NumericValue::from_unit(&source("1"), &s, &mut meter()).unwrap(); + let total = receive.add(&dispatch, &mut meter()).unwrap(); + assert_fraction(total.coordinate(), 7, 4); + assert_fraction(&total.display_in(&ms, &mut meter()).unwrap(), 1750, 1); + let different = Unit::new( + linear("different-kind", duration.dimension()), + source("1"), + source("0"), + ) + .unwrap(); + assert_eq!( + ms.convert(&source("750"), &different, &mut meter()), + Err(NumericError::IncompatibleTypes) + ); + let inconsistent = Unit::new( + linear("duration", dim([1, 0, 0, 0, 0, 0, 0])), + source("1"), + source("0"), + ) + .unwrap(); + assert!( + ms.convert(&source("1"), &inconsistent, &mut meter()) + .is_err() + ); + assert!(Unit::new(duration.clone(), source("0"), source("0")).is_err()); + assert!(Unit::new(duration.clone(), source("ratio(-1,1)"), source("0")).is_err()); + assert_eq!( + Unit::new(duration, source("1"), source("1")).unwrap_err(), + NumericError::LinearOffset + ); +} + +#[test] +fn affine_point_and_difference_arithmetic_has_distinct_kinds() { + let interval = linear("temperature-difference", dim([0, 0, 0, 0, 1, 0, 0])); + let point = ResolvedKind::affine("temperature-point".to_owned(), &interval).unwrap(); + let celsius = Unit::new(point.clone(), source("1"), source("273.15")).unwrap(); + let fahrenheit = Unit::new( + point.clone(), + source("ratio(5,9)"), + source("ratio(45967,180)"), + ) + .unwrap(); + let kelvin_interval = Unit::new(interval.clone(), source("1"), source("0")).unwrap(); + assert_fraction( + &celsius + .convert(&source("0"), &fahrenheit, &mut meter()) + .unwrap(), + 32, + 1, + ); + assert_fraction( + &fahrenheit + .convert(&source("70"), &celsius, &mut meter()) + .unwrap(), + 190, + 9, + ); + let p20 = NumericValue::from_unit(&source("20"), &celsius, &mut meter()).unwrap(); + let p10 = NumericValue::from_unit(&source("10"), &celsius, &mut meter()).unwrap(); + let difference = p20.subtract(&p10, &mut meter()).unwrap(); + assert_eq!( + difference.value_type(), + &NumericType::Named(interval.clone()) + ); + assert_fraction( + &difference + .display_in(&kelvin_interval, &mut meter()) + .unwrap(), + 10, + 1, + ); + let delta5 = named(5, &interval); + let p25 = p20.add(&delta5, &mut meter()).unwrap(); + assert_fraction(&p25.display_in(&celsius, &mut meter()).unwrap(), 25, 1); + assert_eq!(delta5.add(&p20, &mut meter()).unwrap(), p25); + assert!(p20.add(&p10, &mut meter()).is_err()); + assert!(delta5.subtract(&p20, &mut meter()).is_err()); + assert_eq!( + p20.power(1, &mut meter()), + Err(NumericError::AffineOperation) + ); + assert_eq!( + p20.negated(&mut meter()), + Err(NumericError::AffineOperation) + ); + assert_eq!(p20.compare(&p10, &mut meter()).unwrap(), Ordering::Greater); + assert!(p20.display_in(&kelvin_interval, &mut meter()).is_err()); + assert!(ResolvedKind::affine(interval.key().clone(), &interval).is_err()); + assert!(ResolvedKind::affine("other".to_owned(), &point).is_err()); +} + +#[test] +fn affine_conversion_rejects_a_wider_stage_even_when_the_final_value_would_fit() { + // A fused coordinate calculation 2*m-m equals m, where m=2^4095 fits. + // The fixed multiply stage produces 2^4096, so it must fail before offset + // cancellation. The inverse path likewise rejects (m-(-m))/2 at subtraction. + let large = BigInt::one() << 4095_usize; + let magnitude = exact(&large, 1); + let interval = linear("temperature-interval", dim([0, 0, 0, 0, 1, 0, 0])); + let point = ResolvedKind::affine("temperature-point".to_owned(), &interval).unwrap(); + let unit = Unit::new(point, Exact::from_integer(2), exact(-&large, 1)).unwrap(); + let mut work = meter(); + for outcome in [ + unit.to_canonical(&magnitude, &mut work), + unit.from_canonical(&magnitude, &mut work), + ] { + assert!(matches!( + outcome, + Err(NumericError::Limit(NumericLimit::Bits { + component: NumberComponent::Numerator, + bits: 4097, + limit: MAX_COMPONENT_BITS, + .. + })) + )); + } + assert!(work.exhaustion().is_none()); + let half = exact(&large >> 1_usize, 1); + assert_fraction(&unit.to_canonical(&half, &mut work).unwrap(), 0, 1); + assert_eq!( + unit.from_canonical(&Exact::from_integer(0), &mut work) + .unwrap(), + half + ); +} + +#[test] +fn r6_anonymous_compound_energy_needs_one_outer_assertion() { + let force = linear("force", dim([1, 1, -2, 0, 0, 0, 0])); + let length = linear("length", dim([1, 0, 0, 0, 0, 0, 0])); + let energy = linear("energy", dim([2, 1, -2, 0, 0, 0, 0])); + let a = named(3, &force) + .multiply(&named(4, &length), &mut meter()) + .unwrap(); + let b = named(2, &force) + .multiply(&named(7, &length), &mut meter()) + .unwrap(); + assert_eq!(a.value_type(), &NumericType::Anonymous(energy.dimension())); + let sum = a.add(&b, &mut meter()).unwrap(); + let result = sum.as_kind(&energy, &mut meter()).unwrap(); + assert_fraction(result.coordinate(), 26, 1); + assert_eq!(result.value_type(), &NumericType::Named(energy.clone())); + assert_eq!(a.compare(&b, &mut meter()).unwrap(), Ordering::Less); + assert!(result.add(&sum, &mut meter()).is_err()); + assert_eq!( + result.as_kind(&energy, &mut meter()), + Err(NumericError::KindAssertion) + ); +} + +#[test] +fn anonymous_product_then_quotient_closes_and_preserves_scaling() { + let mass = linear("mass", dim([0, 1, 0, 0, 0, 0, 0])); + let length = linear("length", dim([1, 0, 0, 0, 0, 0, 0])); + let time = linear("duration", dim([0, 0, 1, 0, 0, 0, 0])); + let momentum = linear("momentum", dim([1, 1, -1, 0, 0, 0, 0])); + let result = named(2, &mass) + .multiply(&named(3, &length), &mut meter()) + .unwrap() + .divide(&named(2, &time), &mut meter()) + .unwrap() + .as_kind(&momentum, &mut meter()) + .unwrap(); + assert_fraction(result.coordinate(), 3, 1); + let scalar = NumericValue::number(source("2")); + let scaled = scalar.multiply(&named(3, &time), &mut meter()).unwrap(); + assert_eq!(scaled.value_type(), &NumericType::Named(time.clone())); + assert_fraction(scaled.coordinate(), 6, 1); + assert_eq!( + named(3, &time) + .divide(&scalar, &mut meter()) + .unwrap() + .value_type(), + &NumericType::Named(time.clone()) + ); + assert_eq!( + scalar + .divide(&named(3, &time), &mut meter()) + .unwrap() + .value_type(), + &NumericType::Anonymous(dim([0, 0, -1, 0, 0, 0, 0])) + ); +} + +#[test] +fn nominal_kinds_survive_comparison_but_explicit_quotients_can_erase_dimension() { + let energy = linear("energy", dim([2, 1, -2, 0, 0, 0, 0])); + let torque = linear("torque", energy.dimension()); + let left = named(7, &energy); + let right = named(7, &torque); + assert!(left.add(&right, &mut meter()).is_err()); + assert!(left.compare(&right, &mut meter()).is_err()); + let ratio = left.divide(&right, &mut meter()).unwrap(); + assert_eq!(ratio.value_type(), &NumericType::Number); + assert_fraction(ratio.coordinate(), 1, 1); + let named_ratio = linear("chosen-ratio", Dimension::ZERO); + let asserted = ratio.as_kind(&named_ratio, &mut meter()).unwrap(); + assert_eq!( + asserted.value_type(), + &NumericType::Named(named_ratio.clone()) + ); + assert!(asserted.add(&ratio, &mut meter()).is_err()); + assert_eq!( + NumericValue::::new(NumericType::Anonymous(Dimension::ZERO), source("1")), + NumericValue::number(source("1")) + ); +} + +#[test] +fn numerical_power_types_and_dimension_overflow_are_checked() { + let length = linear("length", dim([1, 0, 0, 0, 0, 0, 0])); + let value = named(2, &length); + assert_eq!( + value.power(0, &mut meter()).unwrap().value_type(), + &NumericType::Number + ); + assert_eq!( + value.power(1, &mut meter()).unwrap().value_type(), + value.value_type() + ); + assert_eq!( + value.power(-2, &mut meter()).unwrap().value_type(), + &NumericType::Anonymous(dim([-2, 0, 0, 0, 0, 0, 0])) + ); + let large_dimension = linear("large-dimension", dim([32, 0, 0, 0, 0, 0, 0])); + assert!( + named(1, &large_dimension) + .multiply(&value, &mut meter()) + .is_err() + ); + assert!(named(1, &large_dimension).power(2, &mut meter()).is_err()); +} diff --git a/crates/oa-core/src/lib.rs b/crates/oa-core/src/lib.rs index 7197328c..7934fd65 100644 --- a/crates/oa-core/src/lib.rs +++ b/crates/oa-core/src/lib.rs @@ -1,4 +1,5 @@ //! Framework-independent OA/SA model, transactional commands and editing services. +pub mod analysis_numeric; pub mod data; pub mod language; pub mod model; diff --git a/harness/DECISIONS.md b/harness/DECISIONS.md index 9e39b186..91c86012 100644 --- a/harness/DECISIONS.md +++ b/harness/DECISIONS.md @@ -376,3 +376,41 @@ The exact numeric foundation is the next bounded core implementation. Ordinary engineering approximations, a complete low-noise text workflow, two-project library maintenance and native/API/source parity remain required release work. An exact-only slice cannot complete the user's first release. + +## Analysis production staging — 2026-09-11 + +Root accepts the concrete [production integration sequence](release-analysis-production-integration-plan-20260911.md). +Allocate schema8 to the next coherent production analysis integration. Start with +the actual Project's neutral definition catalog, three analysis element kinds, +typed expressions and a closed Local definition-reference environment. Imported +references will be admitted only with the real package environment; no placeholder +resolver, guessed pin, implicit type compatibility or competing package format. +This stages implementation and does not defer the required maintained libraries. + +The first useful gate is the complete persisted/source-authored response budget, +shared two-parameter calculation and check: baseline7/4 seconds versus degraded9/4, +with explicit request context and the same core result through CLI and REST. +Required property fields cannot come from generic factory guesses. Existing +descriptive expressions/unit labels retain their exact old meaning and bytes. +Freeze older top-level wire DTOs before making definitions required in schema8; +reject new fields/constructors in older versions instead of silently dropping them. +Global, scoped parameter, imported and historical identities remain distinct. + +Implement pure static numeric type helpers once and reuse them for admission and +runtime. Validate every effective case graph and unused branch before accepting a +candidate; deleting dependencies requires explicit same-batch repair. Numeric +domain failure is not a static type failure. Full evaluator traversal and actual +C1 input, provenance, terminal incomplete causes and immutable replay are required +before claiming evaluated engineering behavior. Until explicit analysis review/ +transition facets exist, those entry points must reject unsupported analysis with +a clear capability error, including manual-trace paths that could otherwise appear +to reconcile headers alone. + +Logical expression depth128 must be reconciled with bounded actual JSON/source +decoding; do not simply disable recursion limits. Raw byte, decoded string and +aggregate literal/graph/case-admission limits are separate from evaluation fuel. +Concrete decoder/admission ceilings remain subject to bounded boundary and timing +experiments; the implementer must surface those choices before locking the profile. +The current local numeric gate runs against frozen root source. New core contract +work proceeds in an isolated checkout, preserving root's Cargo/native leases and +the other hosts' CLI, staged-source and B4 ownership. diff --git a/harness/release-analysis-numeric-implementation-20260911.md b/harness/release-analysis-numeric-implementation-20260911.md new file mode 100644 index 00000000..0b58bf14 --- /dev/null +++ b/harness/release-analysis-numeric-implementation-20260911.md @@ -0,0 +1,156 @@ +# Exact analysis numeric foundation: implementation handoff + +Codex-956atf /root/requirements_delta, 2026-09-11. Root ratified the property-base/shared-check/full-capture, R6/R7 and nominal compatibility architecture after [independent review C1](release-refined-contracts-review-20260911.md). This bounded production lease owns only new crates/oa-core/src/analysis_numeric.rs, its analysis_numeric/ files, and this report. Root retains Cargo, dependency/lock changes, module declaration, production adapters, integration tests, ledgers and release publication. + +Read Gitea through #170 before implementation, coordinated ownership in #171, read Wiki Home and fetched updated AGENTS.md blob d93cddacdd45341abb7bbea1d3e3fd4493484d9e through Gitea. Resumed coordination through #195, including the independent numeric review lease #191. The new coordinated milestone-prerelease requirement belongs to root's release ownership; an undeclared numeric module is not an independently runnable milestone. + +## Status and integration needs + +**Written, not yet compiled or executed:** reusable exact rational arithmetic, literal/wire admission and formatting, bounded dimensions, nominal numerical scalar operations, affine/linear unit coordinates, request-local work accounting, and 26 Rust test functions. The module is deliberately not declared in lib.rs, so current builds cannot accidentally claim these tests or semantics. Standalone rustfmt completed successfully on the owned module tree; no Cargo, rustc, native application, current Project/source/API, prior frozen evidence, commit or push work occurred. + +Root approved these exact dependency choices. Add them to oa-core directly or via workspace dependencies according to the integration convention, and resolve/preserve the lock with the sole Cargo writer: + +~~~toml +num-bigint = "0.5.1" +num-integer = "0.1.47" +num-traits = "0.2.19" +~~~ + +Use their default std features; no rand, num-bigint serde, floating libm or num-rational dependency is needed. Existing serde/serde_json/thiserror supply wire and diagnostic support. The maintained [num-bigint manifest](https://docs.rs/crate/num-bigint/0.5.1/source/Cargo.toml) identifies 0.5.1, Rust 1.60, num-integer ^0.1.46 and num-traits ^0.2.18; this fits the workspace's Rust 1.90 minimum. [num-integer](https://docs.rs/crate/num-integer/0.1.47) supplies Integer/GCD and [num-traits](https://docs.rs/crate/num-traits/0.2.19) supplies the basic numeric traits. num-traits 0.2.19 was already present transitively in the inspected lock. These are primary crate-maintainer sources, inspected before choosing the APIs; the standard [BigInt API](https://docs.rs/num-bigint/0.5.1/num_bigint/struct.BigInt.html) supplies bit counts, parsing and integer operations. Big integer arithmetic/GCD is not reimplemented here. + +Root's proposed first execution gate is: + +~~~text +cargo test --locked -p oa-core analysis_numeric::tests -- --test-threads=1 +cargo clippy --locked -p oa-core --all-targets -- -D warnings +~~~ + +These commands have **not** run for this implementation. Root must add the dependencies and declare pub mod analysis_numeric first. A successful existing desktop suite while this module is undeclared provides no numeric validation. The independent correctness review is read-only and also does not execute these tests. + +## Public boundary + +| Type/API | Responsibility | +| --- | --- | +| Exact / ExactWire | Private normalized BigInt numerator and positive denominator; explicit canonical decimal-string wire. No unmetered Add/Div/Ord traits. | +| Exact::from_wire / parse_literal | Canonical wire admission or one exact source atom with explicit shared caller meter. No expression parser, names, unit resolver or evaluation context. | +| Exact arithmetic methods | Metered add/subtract/multiply/divide/compare/negate/abs/reciprocal/bounded integer power. | +| WorkLimits / WorkMeter / WorkUsage | One explicit request-local dynamic and numeric budget; read-only usage/limits; terminal first exhaustion. No Clone/Default on the meter. | +| Dimension | Validated seven-component integer vector, checked products/quotients/powers; dimension equality is not kind equality. | +| ResolvedKind | Resolver-supplied verified nominal key with dimension and optional distinct linear difference kind. No package lookup or compatibility cache. | +| Unit | Positive exact scale; affine offset or zero linear offset; exact canonical coordinate conversion. | +| NumericType / NumericValue | Internal Number, named linear/point, or anonymous dimension with R6 numerical operations. Boolean, list, property, call/check and AST semantics remain the common evaluator's responsibility. | +| NumericError / NumericLimit | Classified syntax/canonical/domain/type/dimension and magnitude/work-limit failures. Fuel exhaustion is detectably terminal; a component bit failure is not. | + +Public Eq on stored bounded values means representation equality; expression equality must call the metered compare operation, which rejects incompatible kinds. A false predicate is not represented by a numeric error. The integrating evaluator maps a valid comparison to Boolean and maps supported numeric failures into Failed/Unresolved. It must still distinguish those from Missing inputs and admission/type rejection. + +K is the common resolver's verified same-origin contract key. This module neither derives K from dimensional equality nor mistakes a digest/name for compatibility. ResolvedKind comparison also checks dimension/algebra/difference key, so accidentally supplying the same key with different dimensions does not make two units convertible. The resolver still owns proof of the coherent coordinate basis. Exact definition references, package pins and declared-output anchoring remain model/report provenance outside this numerical value. + +K must be a bounded handle with cheap Clone/Eq, such as an admitted internal identifier into a verified environment. A rooted contract graph must not be stored directly in K and recursively cloned/compared during arithmetic. Proof construction, archive reading and its work accounting belong to resolver admission. The generic Rust bounds cannot enforce that integration precondition. Numeric precharges cover the BigInt work, not arbitrary user-defined Clone/Eq implementations. NumericValue::from_unit checks terminal exhaustion before copying its key; display_in compares the existing key by reference. + +## Exact number and admission policy + +Every admitted Exact has a nonzero positive denominator, gcd(n,d)=1, at most 4096 magnitude bits per component, and zero represented as 0/1. BigInts are private, so clients cannot mutate an admitted denominator or inject a wider coordinate. The bounded i64 constructor only creates an exact small integer; all nontrivial arithmetic is metered. + +Wire fields are required strings. Leading plus/zeroes, negative zero, negative denominator, whitespace, exponents, decimal fractions, unreduced ratios and JSON numeric tokens reject. Numerator and denominator each enforce the digit limit, actual bit count and canonical grammar. An oversized but reducible wire pair still rejects; wire input is already required to be normalized. Duplicate and unknown fields reject through the closed Serde record. + +Source admission reads only an unsigned decimal/integer or ratio(signed_integer, unsigned_integer) atom. It does not parse arithmetic, names or units. Whole source-atom bytes are capped at 2500; mantissa or ratio-component digits at 1234; decimal exponent magnitude at 128. Decimal mantissas require digits on both sides of a present dot. Source ratios/decimals may reduce, preserving distinctions such as accepted ratio(2,4) versus rejected unreduced wire. Ratio denominator zero rejects. No numeric input passes through f64. + +Canonical nonnegative integer literals print as integers; other literals print ratio(n,d). **A negative literal always prints ratio(-n,d), including d=1.** A leading expression minus is not accepted by this literal reader and belongs to the future UnaryNegate AST. This preserves the R7 negative-literal distinction without constant-folding an expression. The complete copied R7 packet contains 10^300, 1/(2^4095), and -(2^4096-1) as full wire strings with full expected literal spellings. + +Standalone Exact Serde conversion performs bounded canonical BigInt validation using a fresh per-literal admission meter, **after the derived ExactWire decoder has allocated its String fields**. It does not bound untrusted JSON string allocation or aggregate whole-document admission. A model/source/REST adapter must bound the encoded envelope and decoded strings, use a bounded visitor where needed, and cap aggregate admission work. The explicit metered entry points can accumulate literal parsing work after text admission. The evaluator must not deserialize repeatedly while interpreting dynamic calls or reset its meter per literal/target. No current Project/REST adapter is changed by this lease. + +## Bounded arithmetic and conversion + +Each binary arithmetic method computes safe intermediate bit estimates and reserves its complete logical numeric charge before constructing cross products or running GCD. Two 4096-bit components multiply to at most 8192 bits; adding two such numerator terms can require 8193. Those bounded raw values normalize before applying the 4096-bit **reduced result** limit. Raw cancellation is therefore permitted: the tests include an 8193-bit sum numerator that reduces back to an admitted rational, and two approximately 8192-bit products that cancel to one. + +Source decimal parsing bounds digit count/exponent before parsing or allocating a power of ten. It reserves parse, scale-construction, multiplication and normalization work using safe decimal-to-binary estimates; no arbitrarily long exponent can trigger an enormous BigInt. Canonical wire validation similarly reserves before BigInt parsing/GCD. The bit estimate uses ceil(3.322 * decimal_digits), an integer-only upper estimate, not a conversion through floating point. + +Powers admit syntactic integer exponents -16..16. They use a fixed initial reservation, optional reciprocal, and left-to-right repeated multiplication, with each reduced stage bounded. They never allocate a 65536-bit power and discard it afterward. Division by zero/zero to a negative power fail; 0^0 is the explicit domain failure. A later rational expression that could mathematically cancel an earlier overflowing reduced stage does not erase that NumericLimit. + +Unit coordinate conversion is deliberately the fixed path magnitude*scale then +offset; reverse conversion is coordinate-offset then /scale. Every reduced stage must fit the Exact bound. **A wider intermediate that would cancel in a later conversion stage still fails.** A fused conversion with different limit/work behavior would require an explicit revised profile. This is a practical bound at extreme magnitudes, not a rounding rule; ordinary supported conversions remain exact. + +Linear units require positive scale and zero offset. An affine point kind has a distinct linear difference kind of the same dimension; the constructor derives that dimension from the validated linear difference kind and rejects point-as-difference or equal point/difference key. Tests use exact Celsius/Fahrenheit point coordinates and separate Kelvin interval units. Point-minus-point yields that interval kind, point plus/minus its interval yields the point, and interval+point is supported. Point+point, interval-point, point scaling/negation/abs/power reject. Comparison requires the same full type. + +R6 numerical products/quotients yield anonymous dimensions when both operands are non-Number linear quantities, with A(0) immediately normalized to Number. Number scaling preserves the other linear type; Number/quantity yields an anonymous inverse. Anonymous add/subtract/compare requires equal dimensions. Named add/subtract/compare requires compatible nominal kinds. Explicit AsKind accepts only a matching anonymous dimension or Number for a named dimensionless kind, never a named-to-named coercion or affine target. The force-distance sum test requires one outer Energy assertion and expects 26 canonical joules. + +## C1 work contract and precise weights + +The accounting profile is Q1-logical-work-1. Root approved implementing **provisional** reference ceilings of 1,000,000 dynamic events and 50,000,000 numeric work units. These constants still require measured bounded/worst-case calibration before a published stable profile. They are not wall-clock guarantees. Callers can lower either ceiling, including to zero, but cannot raise them through WorkLimits. The effective limits must travel in request/result/freeze identity; comparison of replay or caches requires identical limits as well as capture, context, targets and profile. + +The one mutable meter is shared by all outputs and recursive evaluation. Dynamic events are explicit: + +- Target before each requested output. +- Expression before every dynamically visited expression occurrence. +- CalculationEntry before every function body entry, additional to its Call expression. +- PropertyBinding before each selected effective property binding, additional to its Property expression. +- ListElement before each visited item, additional to that item's expression. + +Charge only executed dynamic branches; statically checking both branches is a separate admission rule. The future evaluator must sort targets by category (properties, then checks) and UUID bytes, use the agreed operand/argument order, and preserve the same logical traversal/cost on cache hits. There is no implementation of an AST/cache here and no cache-parity execution claim. A shortcut that skips charges or uses a different effective budget is invalid; full report reuse must include the complete request identity. + +Let W(b)=ceil(max(b,1)/64), using logical 64-bit words on every target platform. Numeric costs are fixed functions of bounded input/estimated intermediate sizes: + +| Primitive plan | Numeric work units | +| --- | --- | +| Product/division allowance P(a,b) | 1 + W(a)*W(b) | +| Sum/comparison allowance S(a,b) | 1 + W(max(a,b)) | +| Normalization allowance G(n,d) | 1 + 66*W(max(n,d))^2 (64 parts GCD, two parts quotient) | +| Digit parsing D(k,b) | 1 + k*W(b) | +| Copy/sign/reciprocal C(n,d) | 1 + W(n) + W(d) | + +These are conservative **logical weights**, not a claim about a crate's GCD complexity or algorithm. They remain independent of actual GCD iteration counts and internal multiplication optimizations. All cost inputs are bounded before these integer formulas; actual arithmetic cannot overflow their u64 computation. + +For left component bits (a,b) and right (c,d), exact operation reservations are: + +| Method | Complete reservation before its BigInt work | +| --- | --- | +| add/subtract | P(a,d)+P(c,b)+S(a+d,c+b)+P(b,d)+G(max(a+d,c+b)+1,b+d) | +| multiply | P(a,c)+P(b,d)+G(a+c,b+d) | +| divide | P(a,d)+P(b,c)+G(a+d,b+c), then the zero-domain check | +| compare | P(a,d)+P(c,b)+S(a+d,c+b) | +| negate/abs/reciprocal | C(a,b), then the reciprocal zero-domain check where relevant | +| power | C(a,b), optional reciprocal charge, then the fixed sequence of bounded multiply charges | +| AsKind | C(a,b), after the type check | +| wire/ratio parsing | D(n_digits,n_est)+D(d_digits,d_est)+G(n_est,d_est) | +| decimal parsing | D(mantissa_digits,m_est) + (1+2*bit_length(abs(adjustment)))*P(scale_est,scale_est) + P(m_est,scale_est) + G(n_est,d_est) | + +Decimal adjustment is exponent minus fractional-digit count; scale_est estimates 10^abs(adjustment). These rules intentionally charge a fixed plan even when a sign/zero/identity shortcut could be faster. A one-word rational add costs exactly 75 numeric units; the boundary test independently checks that value. + +The meter reserves atomically. A reservation that exceeds remaining fuel consumes no partial charge and latches its first WorkExhaustion (resource, prior usage, attempted charge, limit, operation/event). Further operations, even zero-cost reservations or unrelated target visits, return that same terminal failure without changing usage or traversing more children. The integrating evaluator must stop and label collected causes **incomplete**. It may not keep traversing siblings to make strict missing/failure cause lists exhaustive. + +Component bit-limit errors are distinct nonterminal supported-operation failures: the prepaid bounded operation has finished and another independent output may still be evaluated with remaining fuel. Domain/type/admission classification remains the evaluator/adapter's responsibility. + +## Authored tests and evidence limits + +The 26 test functions are authored in analysis_numeric/tests.rs. They currently cover: + +| Area | Independent expectations / negative controls | +| --- | --- | +| Basic exact arithmetic | 400 small rational operand pairs checked against an independent i128 Euclidean-normalization oracle for add/subtract/multiply/divide/order; explicit zero divisors. | +| Decimal/power/sign domain | 0.1+0.2=3/10, reduced source ratios, decimal exponents, positive/negative powers, abs/reciprocal, 0^0 and exponent rejection. | +| Strict wire/literal boundaries | Both numerator/denominator grammar, leading zero/plus/negative zero, unreduced/zero denominator, JSON numeric fields, duplicate/unknown/missing fields; source atom rejects expression minus/arithmetic. | +| R7 | Exact full copied packets and expected canonical source/wire; negative literal remains signed ratio. This does not execute the future expression AST parser. | +| Magnitude/preallocation | 8193-bit cancelling sum; wide cancelling products; numerator and denominator 4097-bit failures; zero numeric budget yields fuel exhaustion before a result allocation/bit check; forward/reverse affine stages reject 4097-bit intermediates despite a mathematically fitting final coordinate, with fitting conversion controls. | +| Meter | Exact 75-unit add boundary; zero-cost reservation; u64::MAX request without underflow; terminal first failure; effective limits serialize; shared target budget. | +| C1 | A direct depth-30 call-tree workload stops after 10,000 entered calls; a depth-5 control permits exactly 63 calls and returns 496. This is a meter workload, not a second expression dialect or actual Studio evaluation. | +| Dimensions/kinds/units | Checked seven-axis limits; same-dimension different nominal kinds reject addition/comparison/conversion; same key/different dimension also rejects; exact duration and Celsius/Fahrenheit conversions. | +| R6 | Anonymous compound energy sum/compare, product-then-quotient momentum, Number scaling/inverse, dimensionless normalization/explicit kind, affine point/interval rejection and power types. | + +Executed by this worker: the source fixture was copied byte-for-byte from the frozen independently reviewed R7 packet (SHA256 3B959DEC5E100A6F03817F5314BEF497347BA579EBD235476516D4BD83399181); standalone rustfmt succeeded. **No test pass, compile pass, Clippy pass, benchmark or source/model/REST/GUI parity is claimed.** Root's independent review and serialized execution are the next evidence. + +The future vertical integration must add the actual expression traversal/meter propagation, type-check all operands including thresholds/unused branches, obey terminal cause incompleteness, record effective work limits, and test identical cold/warm/source/REST/frozen outcomes. The current R6 result-type helpers are internal to NumericValue; the AST checker should extract/reuse pure NumericType helpers, rather than evaluate dummy coordinates or duplicate the algebra. Number/Number has a valid result type even when a runtime denominator happens to be zero. Integration must also close encoded/decoded input and aggregate admission bounds, bounded resolver keys, nonempty pinned freeze and source AST round-trip. Approximate unit scales and ordinary engineering transcendental functions remain a mandatory subsequent capability; this exact module does not complete the release objective. + +## Frozen source inventory + +Final standalone rustfmt --edition 2024 --check succeeded. A scoped text scan found zero trailing-whitespace lines and counted 26 test functions. The numeric module/dependencies remain absent from lib.rs and inspected manifests. This inventory describes local, uncommitted files awaiting root's integration and execution: + +| Workspace-relative file | SHA256 | +| --- | --- | +| crates/oa-core/src/analysis_numeric.rs | 6C88EEF3119162AEB6C07B9E75812C3AF9FBFE75554B0503AD00F103CB478408 | +| crates/oa-core/src/analysis_numeric/dimension.rs | D4AD8E5307A1620E31791D724A0E31FDBA860D00DC83E3E1F2209D9C5E22A340 | +| crates/oa-core/src/analysis_numeric/exact.rs | 4EB8CB0F66B10E5DA204899AF82EE26ADFEC74BAB47B1A6C9842B5488EE04C4D | +| crates/oa-core/src/analysis_numeric/fixtures/r7-literal-boundaries.json | 3B959DEC5E100A6F03817F5314BEF497347BA579EBD235476516D4BD83399181 | +| crates/oa-core/src/analysis_numeric/meter.rs | 1F7174BEB992935B4C399ACDEF91114AF73FAF041070FEAB968455AC827E8EE4 | +| crates/oa-core/src/analysis_numeric/quantity.rs | EAD5142D6EEEA8F99399D57E02D8F7D819980923DE76387CD454694D6A747AEE | +| crates/oa-core/src/analysis_numeric/tests.rs | 323CE82FC057D36F44463569FD8EA324C7D700FDDFBF32BCE15E04BD2A66970B | + +The SHA256 of the seven sorted path + TAB + uppercase hash + LF inventory lines, UTF-8 without BOM, is E4C2E20476FD21228F58741E8E537C01530B4C995DA47C5A714B407FD7086FD0. The report is excluded from that digest to avoid self-reference. Independent reviewer /root/semantics_critic reported no confirmed arithmetic/type/meter blocker in the read-only review; its final report and root's compiled tests remain separately owned evidence. diff --git a/harness/release-analysis-numeric-review-20260911.md b/harness/release-analysis-numeric-review-20260911.md new file mode 100644 index 00000000..45dc2136 --- /dev/null +++ b/harness/release-analysis-numeric-review-20260911.md @@ -0,0 +1,82 @@ +# Independent numeric foundation review + +Codex-956atf `/root/semantics_critic`, 2026-09-11. Root assigned read-only review of `crates/oa-core/src/analysis_numeric.rs` and its module tree. Read the ratified decision in `harness/DECISIONS.md:323`, the refined baseline contract and C1 review, all implementation/tests, and the implementation handoff. Coordinated with requirements_delta; Gitea ownership is issue #1 comment 191. Owned only this report. No production, prior report, Git, Cargo, compiler or native changes; no tests executed by this reviewer. + +**Source-review conclusion:** no confirmed arithmetic, rational canonicalization, affine/linear type or meter-latching defect was found in the reviewed foundation. It is suitable for root's compilation and focused test gates. This conclusion does not certify those unexecuted gates. Three concrete integration boundaries below must remain explicit; the numeric meter alone does not make arbitrary deserialization, arbitrary generic key implementations or an uncharged evaluator bounded. + +## Exact arithmetic and type rules checked + +- `exact.rs:76` validates both wire components before BigInt parsing, enforces actual component bits, positive nonzero denominator and reduced canonical form. Signed numerator, forbidden negative zero/leading zeros, zero as 0/1 and duplicate/missing/unknown wire fields are handled consistently. Source ratios/decimals may reduce; wire values may not rely on later reduction. +- `exact.rs:106` bounds the borrowed source atom before scanning; mantissa/component digits and exponent are separately bounded. Decimal scale construction is precharged before allocation. Unsigned source atoms and signed ratio numerators preserve the R7 distinction between a negative literal and an expression UnaryNegate. The full copied R7 fixture is byte-identical to the previously audited packet. +- `exact.rs:198`, `:230`, `:244` and `:331` allow bounded cross products and an 8,193-bit raw sum numerator, normalize them, then enforce the 4,096-bit reduced result. The estimates cover each corresponding operation. They neither reject every reducible 8,192-bit intermediate nor permit an unbounded intermediate. Denominator sign normalization, zero normalization, reciprocal and sign rules are consistent. Bounded repeated power checks exponent range and zero-domain cases before the loop. +- `quantity.rs:242` distinguishes linear kinds, affine points and their difference kinds. Point-minus-point returns the declared interval kind; point plus/minus its interval and interval-plus-point are allowed; point-plus-point, interval-minus-point and point scaling/negation/power reject. Nominal equality includes dimension/algebra/difference identity, while the external resolver still owns coordinate-basis proof. +- `quantity.rs:288`, `:336` and `:360` match R6: Number scaling preserves the other linear type; two non-Number linear factors produce anonymous dimensions; A(0) normalizes to Number; powers have the prescribed result types; AsKind rejects named-to-named and affine assertions. Formal compare rejects differing types rather than silently returning false. +- `meter.rs:187` atomically reserves against private validated limits, consumes no partial failed charge and latches the first exhaustion. Further numeric/dynamic reservations return the same failure. The arithmetic paths precharge before BigInt products/GCD and do not expose unmetered Add/Div/Ord implementations. Component bit-limit failures correctly remain nonterminal while fuel exhaustion is terminal. + +## Boundary N1: JSON decoding precedes the per-literal numeric limit + +**Locations:** `exact.rs:17–22`, `:31–32`, `:76–87`, `:396–402`; implementation report's admission section. + +`Exact` deserialization first creates an `ExactWire` containing two owned `String`s, then calls `from_wire` with a fresh admission meter. A numerator string with one million digits is eventually rejected by the digit limit, but that limit is not a bound on the JSON decoder's earlier string allocation/scan. An escaped JSON string can also require decoder scratch storage. Repeating valid literals restarts the standalone per-value meter, so it does not consume one shared admission budget. + +Reproducible source-derived example, not executed here: + +```rust +let input = format!( + r#"{{"numerator":"{}","denominator":"1"}}"#, + "1".repeat(1_000_000), +); +let rejected = serde_json::from_str::(&input); +// Rejection is expected, but ExactWire's String decoding came first. +``` + +**Required before untrusted adapter integration:** bound raw body/file/envelope bytes before Serde, bound the document's total admitted literal/graph work, and use one supplied meter for aggregated numeric admission. A bounded field visitor can reduce owned-string copying but is not a substitute for raw parser/input bounds. Do not deserialize numbers anew while evaluating every dynamic call. The existing server already has 8 MiB request limits (`oa-server/src/lib.rs:65`, `store.rs:20`) and bounded envelope reads (`store.rs:316`); preserve the equivalent common rule for local source/recovery/frozen replay. + +This is not an existing REST vulnerability: no numeric model/API adapter is introduced by this module. The narrower valid guarantee is precharged, bounded **BigInt parsing and arithmetic on length-checked components**, not bounded arbitrary JSON decoding by `Exact` alone. The author corrected the initially broader wording in Exact/ExactWire documentation and the handoff; final readback confirms the encoded/decoded input and aggregate admission preconditions are explicit. The documentation finding is closed; adapters must implement the preconditions. + +## Boundary N2: generic kind-key work is outside numeric accounting + +**Locations:** `quantity.rs:8`, `:41`, `:126–130`, `:196–205`, `:216–229`, `:242–263`, `:314–332`. + +`K: Clone + Eq` is deliberately supplied by the resolver. Those trait bounds do not enforce bounded storage or cheap copying/equality. `NumericValue::from_unit` clones `unit.kind` while evaluating its first constructor argument, before the later coordinate conversion reserves numeric work. Additive type selection and several unary/display paths also clone or compare keys outside that reservation. + +For example, supply a `String` key containing one million characters, a valid linear unit, and an active meter with zero numeric units. Calling `NumericValue::from_unit` clones that key before the multiply reports work exhaustion. A counter-bearing custom Clone would expose the same ordering without allocating a large key. This does not disprove the BigInt precharge; it identifies its boundary. + +**Required resolver integration choice:** K must be a bounded inexpensive verified handle, such as a compact interned contract identity, with construction/proof-graph limits enforced outside the numeric engine. Do not instantiate K as an unbounded owned canonical graph or equate arbitrary strings merely because their spelling matches. Exact package pins and declared output references remain separate provenance. The author has now documented this caller precondition on ResolvedKind and in the handoff. Final readback also confirms `from_unit` checks already-latched exhaustion before cloning, and `display_in` now compares its existing key by reference. An active zero-budget meter has not latched yet, so the cheap-key requirement remains necessary. No replacement of the generic foundation or verification of hostile Rust trait implementations is requested. + +Related public constructors are trusted assembly APIs: `ResolvedKind::linear`, `NumericValue::new`, and raw `NumericType` variants do not prove package origin or independently validate the declared output contract. A caller can intentionally take a coordinate from one kind and construct a new value with another kind. Actual source/REST inputs must pass the common resolver/type checker rather than treating these constructors as checked casts. Stored representation Eq is likewise not the formal comparison API. `NumericValue::new` normalizes A(0); a future type checker must normalize its standalone types too. + +## Boundary N3: the meter is ready; full evaluator determinism is not yet implemented + +**Locations:** `meter.rs:5–11`, `:129–135`, `:171`; `tests.rs:482–518`. + +The C1 test explicitly charges CalculationEntry in a direct recursive workload, stops after 10,000 entries, and has a 63-entry successful control. This is a useful bounded test of the new meter. It is not execution of the actual 333-node expression graph, target sorting, source locations, strict nonvalue collection, property-context selection or a cache. The entire evaluator must charge Expression/CalculationEntry/PropertyBinding/ListElement/Target visits before entering them, share the same meter across outputs, and preserve the same logical numeric and visit sequence on cache hits. + +Neither the meter nor numeric helpers carry an AST/source location; WorkSite identifies an event/operation. The evaluator must capture the first failing expression's location and stop immediately, retaining only collected causes and marking them incomplete. Wrapping the latched error later with a different current location would break the promised stable origin even though WorkExhaustion itself remained equal. Effective limits, profile, document capture, targets and context must participate in report/freeze/cache identity. The 1,000,000/50,000,000 ceilings are explicitly provisional and do not claim calibrated wall-clock limits. + +**Before adding the expression adapter**, expose/reuse pure result-type helpers instead of duplicating the R6 table. Current additive/multiplicative type helpers are private methods on NumericValue. Admission must determine that Number/Number has type Number without calling a numeric divide on dummy zero coordinates, and must accept a well-typed `0^0` expression whose evaluation subsequently fails. Dummy-value execution would incorrectly turn runtime domain failures into save/type errors. This is a next-step integration requirement, not a defect in the present value arithmetic. + +## Focused remaining validation + +Root must compile the declared module with resolved dependencies and run its authored tests and strict lint. Final readback contains 26 test functions, including a 400-pair independent small-rational oracle, full R7 packets, wide cancelling intermediates, both reduced overflow components, the 75-unit exact charge boundary, aggregate target reservations, C1's bounded call tree and representative nominal/affine/R6 cases. No pass count is inferred from reading them. + +One review-requested addition is now authored; one narrow gap remains: + +1. **Staged affine conversion failure now covered in authored test `tests.rs:665`.** Let N=`2^4095`, use an affine unit with scale 2 and offset -N. Forward conversion of magnitude N has mathematical final coordinate N, but its first multiply produces `2^4096` and must return the documented 4,097-bit NumericLimit. Reverse conversion of coordinate N must likewise fail during subtraction before division by 2. The author added both failures, nonterminal bit-limit checking and fitting controls `to_canonical(N/2)=0` / `from_canonical(0)=N/2`; these were independently read back, not executed. A future fused optimization must not silently change the chosen reduced-stage limits. +2. **Exercise terminal precedence through wrappers.** Exhaust one meter, then call a wrong-kind Unit conversion, NumericValue compare/power/AsKind and valid literal parsing. Each must return the original latched exhaustion with unchanged usage and no further arithmetic, rather than a new type/domain/literal error. Current tests cover this property directly for Exact arithmetic and meter reservations; wrapper paths were checked by source inspection only. + +Cold/warm cache equality, real C1 source/API/frozen replay, complete static typing (including unused threshold operands), raw input allocation bounds, aggregate admission and ordinary approximate engineering mathematics remain integration gates. The foundation does not claim to implement those adapters. No change to the ratified property-base, case or exact-pin architecture is indicated by this review. + +## Exact final readback + +SHA-256 hashes below identify the reviewed code after the author's bounded corrections and explicit source freeze. Paths are relative to `crates/oa-core/src/`. The author reported standalone rustfmt/whitespace success and 26 authored tests, without compilation or execution; this reviewer independently read the final source and hashes. + +| File | SHA-256 | +| --- | --- | +| `analysis_numeric.rs` | `6C88EEF3119162AEB6C07B9E75812C3AF9FBFE75554B0503AD00F103CB478408` | +| `analysis_numeric/dimension.rs` | `D4AD8E5307A1620E31791D724A0E31FDBA860D00DC83E3E1F2209D9C5E22A340` | +| `analysis_numeric/exact.rs` | `4EB8CB0F66B10E5DA204899AF82EE26ADFEC74BAB47B1A6C9842B5488EE04C4D` | +| `analysis_numeric/meter.rs` | `1F7174BEB992935B4C399ACDEF91114AF73FAF041070FEAB968455AC827E8EE4` | +| `analysis_numeric/quantity.rs` | `EAD5142D6EEEA8F99399D57E02D8F7D819980923DE76387CD454694D6A747AEE` | +| `analysis_numeric/tests.rs` | `323CE82FC057D36F44463569FD8EA324C7D700FDDFBF32BCE15E04BD2A66970B` | +| `analysis_numeric/fixtures/r7-literal-boundaries.json` | `3B959DEC5E100A6F03817F5314BEF497347BA579EBD235476516D4BD83399181` | diff --git a/harness/release-analysis-production-integration-plan-20260911.md b/harness/release-analysis-production-integration-plan-20260911.md new file mode 100644 index 00000000..0b28cb55 --- /dev/null +++ b/harness/release-analysis-production-integration-plan-20260911.md @@ -0,0 +1,126 @@ +# Production analysis integration: next vertical slice + +Codex-956atf /root/requirements_delta, 2026-09-11. Read-only investigation after numeric freeze #201 and review #203; ownership coordinated in Gitea #210. This report is the only new file. Root has declared the numeric module and owns its first Cargo gate; this worker has not compiled, executed, or changed production code. The B/property-base, shared-check, R6/R7 and complete-capture architecture is ratified. This plan stages its implementation in the existing application, not an alternate Project or interpreter. + +**Recommended next gate: author the complete response-budget model in real source, admit/persist it through the existing command/source boundary, and evaluate the same property and shared check through core, CLI and REST under explicit ModelBaseline and Case contexts.** Include the reusable two-parameter calculation: otherwise the first example misses the captured-definition and scoped-reference boundaries that determine the architecture. The existing complete UUID fixture is [active.arcadia.proposed](experiments/analysis-baseline-20260911/active.arcadia.proposed); its current suffix and explanatory text correctly say that it is not implemented source. Promote a newly implemented version into a production example/test fixture, leaving that frozen evidence unchanged. + +## Existing boundaries and required changes + +| Actual code | Consequence for the implementation | +| --- | --- | +| [model.rs:9](../crates/oa-core/src/model.rs#L9), [model.rs:229](../crates/oa-core/src/model.rs#L229), [model.rs:593](../crates/oa-core/src/model.rs#L593), [model.rs:1621](../crates/oa-core/src/model.rs#L1621) | Schema 7, closed Element/SharedBody and five Project UUID maps are authoritative. Add three analysis element kinds and one neutral definition map. ModelBaseline is a selector, not a sixth kind or record. | +| [session.rs:170](../crates/oa-core/src/session.rs#L170) and [store.rs:146](../crates/oa-server/src/store.rs#L146) | Clone/apply/finish deletions/validate and identity correspondence already exist; PreparedProject also updates and recompiles source. Extend these operations instead of making evaluator mutations or a separate save path. | +| [references.rs:17](../crates/oa-core/src/references.rs#L17), [references.rs:206](../crates/oa-core/src/references.rs#L206), [references.rs:392](../crates/oa-core/src/references.rs#L392) | Live reference visitors and cleanup have explicit policies. Expr dependencies, override keys and definitions need typed visitors; cleanup must not prune an operand or override and change its meaning. | +| [language.rs:273](../crates/oa-core/src/language.rs#L273), [language.rs:761](../crates/oa-core/src/language.rs#L761), [language.rs:811](../crates/oa-core/src/language.rs#L811), [language.rs:1297](../crates/oa-core/src/language.rs#L1297) | Declarations and source values are finite. Current references/enums are recognized by field-name lists; number tokens become serde_json::Value; typed values stop at depth 64. These mechanisms alone cannot represent exact R7 literals, scoped parameters, call argument keys or override references. | +| [source_project.rs:92](../crates/oa-core/src/source_project.rs#L92), [source_project.rs:286](../crates/oa-core/src/source_project.rs#L286), [source_project.rs:780](../crates/oa-core/src/source_project.rs#L780), [source_project.rs:1662](../crates/oa-core/src/source_project.rs#L1662) | Compilation stabilizes identities and indexes returned bytes. Updating preserves token trivia and file ownership. Add definition record classification, scoped parameter identity/token locations and typed expression locations; add definitions to canonical module ownership/order. | +| [persistence.rs:130](../crates/oa-core/src/persistence.rs#L130) and [source_migration.rs:4](../crates/oa-core/src/source_project/source_migration.rs#L4) | Existing readers migrate versions explicitly. A new required Project field needs a frozen V7 envelope reader/adapter, not a serde default that makes omission valid in the new schema. Source migration must retain prior comments/modules/history and change only required tokens. | +| [semantic/types.rs:81](../crates/oa-core/src/semantic/types.rs#L81), [semantic/historical.rs:6](../crates/oa-core/src/semantic/historical.rs#L6), [history_fields.rs:29](../crates/oa-desktop/src/forms/history_fields.rs#L29) | OA/SA review is a closed typed facet vocabulary; historical references have a separate walker. The desktop history editor reads docs/openapi.json shapes. Snapshot undo already retains the actual Project/source; reviewed semantic history needs deliberate analysis facets before claiming parity. | +| [transitions.rs:203](../crates/oa-core/src/transitions.rs#L203), [transitions.rs:889](../crates/oa-core/src/transitions.rs#L889), [validation.rs:2624](../crates/oa-core/src/validation.rs#L2624) | Merely adding a same-kind mapping can clone an analysis body and remap the wrong reference domain. Manual traces already admit arbitrary semantic endpoints. Explicit analysis selection/remapping and review guards are needed. | +| [routes.rs:29](../crates/oa-server/src/routes.rs#L29), [store.rs:20](../crates/oa-server/src/store.rs#L20), [lib.rs:192](../crates/oa-server/src/lib.rs#L192), [oa-cli/lib.rs:25](../crates/oa-cli/src/lib.rs#L25) | REST has worker slots, bounded bodies, accepted snapshots and ETags; CLI has actual Check/Stabilize/RenameAlias. Add evaluation adapters there. No GUI initialization, ad hoc local web service or second executable is needed. | + +## Persistent types and trusted runtime boundary + +Place the common persistent types under new oa-core analysis/types.rs and use them directly from model.rs, source and API schemas. All records/enums remain closed, with duplicate UUID-map keys rejected by an equivalent of unique_id_map. + +~~~rust +// Existing Project, not a wrapper model: +definitions: BTreeMap + +struct Definition { id: Id, alias: String, name: String, + description: String, body: DefinitionBody } +enum DefinitionBody { QuantityKind(QuantityKindDefinition), + Unit(UnitDefinition), Calculation(CalculationDefinition) } +enum Binding { Unbound, Expression(Expr) } +enum AnalysisSubject { Element(Id), Relation(Id) } +enum BaselineBase { ModelBaseline } +enum EvaluationContext { ModelBaseline, Case(Id) } + +// SharedBody variants; existing Element header supplies identity and layer: +EngineeringProperty { subject: AnalysisSubject, value_type: AnalysisType, + display_unit: Option, base: Binding } +AnalysisCase { subject: Option, base: BaselineBase, + overrides: BTreeMap } +AnalysisCheck { subject: Option, + documented_constraint: Option, predicate: Binding } +~~~ + +Use the ratified Expr tree directly: Boolean, Number(Exact), Quantity(magnitude/unit), Property, Parameter, List, Unary, Binary, If, Call, Sum with explicit initial, Power with integer exponent, and AsKind. Do not accept an uninterpreted formula string or serialize an experimental evaluator's AST. AnalysisType remains scalar Boolean/Number/Quantity or a finite flat list of one scalar type. Calculation parameters have stable scoped ParameterIds, names and AnalysisTypes; arguments map those IDs, and the body is a Binding. Calls are pure and cannot capture architectural properties. UnitDefinition retains exact scale/offset, kind reference and display symbol; quantity kinds retain checked dimensions, linear/affine algebra and the explicit difference-kind reference. + +Existing DataType/DataField unit strings, DataValue defaults, Constraint.expression, message annotation expressions, scenario conditions and state/event text retain their current meaning and wire/source bytes. Migration does not resolve their words into new units, parse them as Expr, or use them as property defaults. A formal check may explicitly link a descriptive Constraint, but only its own typed predicate is evaluated. Any future adapter between exact analysis values and existing i64/f64 payload values is a separate explicit checked operation. + +All three element kinds are layer roots. Required base/type/subject fields are genuinely required: current source factory-default merging must not invent a property subject, Number type or base. Use CreateElement for complete typed records and a dedicated source branch. Generic Add/AddElement should reject kinds requiring an explicit contract until their authoring UI supplies one; audit ElementBody::new/make_element consumers so no new Kind option reaches an unwrap with no valid factory value. Case/check can explicitly author a subjectless record, and Unbound remains a valid incomplete binding. + +Extend Project.identities/contains/named/fresh_alias with local definitions; layer_of(definition) stays None. Parameters are unique only inside their calculation and never enter that global identity set. Local definition reidentification changes actual Local references; parameter rename preserves ParameterId and edits parameter declaration/use and named-call tokens. Never apply a generic UUID visitor to parameter IDs, imported members, quantity coordinates or frozen historical capsules. + +The first example needs only local definitions. Recommended staging decision for root: admit a closed local definition environment first, using DefinitionRef::Local(Id); add the actual Imported form with the coordinated production package environment, not a placeholder resolver that accepts missing pins. This is a local first gate, not fulfillment of reusable-library or nonempty pinned-freeze requirements. If package production types land first, share their exact DefinitionRef and reject absent/corrupt imported environments at admission. Do not create a competing package format here. Root must coordinate the next schema number with that integration; 8 is available in inspected source but remains a proposal until allocated. + +The resolver constructs a private ResolvedAnalysis view over the accepted Project and a bounded table of verified kinds/units/calculations. Numeric K should be a cheap private KindHandle index, not a cloned definition graph. Store exact declared refs separately for public output/provenance. No user can construct a trusted resolved environment merely by filling public CompiledSourceProject fields; its constructor performs shared admission, or consumes an owning component's validated capture. Typed models and source span indexes remain separate: Expr nodes use stable owner/field/child paths for diagnostics, with source locations derived from the compiled bytes. + +## Mandatory ordering inside the core + +1. Extract pure numeric result-type functions from NumericValue into NumericType: additive, multiplicative, unary, power, comparison compatibility and AsKind. Runtime NumericValue delegates to those same functions. Boolean/list rules wrap this algebra in analysis/typecheck.rs. A valid Number/Number type must not require evaluating a dummy zero divisor. Anonymous zero dimensions normalize to Number; declared result boundaries still require explicit nominal kinds. +2. Resolve definitions and check their kinds, dimensions, coordinate basis and pure call graph. Enforce exact named parameter sets, result types and all expression branches, including unused If branches and short-circuit operands. Check every property/check/case reference against its actual layer and record kind. Same-dimensional named kinds remain distinct without verified nominal equivalence. +3. Build the complete baseline dependency graph and every stored case's effective graph. An absent override uses the property's base; present Unbound masks it. An inherited formula resolves all subsequent Property reads in the originally requested case. Check baseline-induced case cycles before any candidate is accepted. Do not calculate values during model admission merely to find types or cycles. +4. Implement the sole evaluator over those admitted Expr nodes. Pass one WorkMeter through every requested target, expression occurrence, call entry, property binding and list element. Use fixed target and argument order, the ratified short-circuit rules, and classified Value/Missing/Failed outcomes; checks map Boolean true/false to Satisfied/Violated and other outcomes to Unresolved. Terminal work exhaustion ends traversal and marks causes incomplete. Initially perform the same logical work without a node-value cache; no optimization is required for first usefulness. +5. Return exact canonical coordinates, declared type anchoring, requested context/targets/profile/effective limits, capture identity, work usage and located Base/CaseOverride provenance for every consulted binding. No result is written back into a base, case, DataValue or history as an evaluator side effect. + +Add CreateDefinition/EditDefinition and the three ratified narrow commands SetAnalysisBase, SetAnalysisOverride and ClearAnalysisOverride. Existing Rename/Describe/SetAlias/Reidentify/Delete must recognize definitions. Clear removes one override key and is an exact no-op if absent; it is not a persisted Binding variant. Existing CreateElement/EditElement/Batch already cover shared checks and complete property/case records. Deleting a referenced property/definition/subject must leave the candidate invalid unless that same batch explicitly repairs or removes its analysis users. Reuse final-candidate validation instead of silently applying the existing optional-reference/list cleanup to these fields. + +## Source authoring, persistence and public calls + +Add one typed adapter, language/analysis_source.rs, invoked only for the new declarations and typed analysis fields. It lowers directly into the real Expr/Definition/SharedBody types and writes those same types. Retain existing declaration headers, explicit IDs, include handling, stable file ownership and ordinary comments. Use the complete fixture's readable forms: quantity_kind/unit/calculation; oa_property/oa_analysis/oa_check (and SA counterparts); base/predicate infix expressions, exact ratio atoms, explicit unit suffixes, scoped $parameters and named call arguments. These are proposed production grammar additions, not descriptions of implemented source7. + +The adapter must preserve raw numeric lexemes for Exact::parse_literal; never route them through serde_json::Number. Negative literal nodes print signed ratio, while unary minus stays a distinct Expr node. Scoped parameter declarations/argument keys and override keys need typed source syntax/identity handling; adding their field names to reference_field is insufficient. Extend tolerant highlighting and actual edit_declarations/SyntaxUpdate parsing too, not just compile/format. On alias-only edits, preserve expression spacing/comments and decimal spelling while changing only affected tokens. Add nested expression source locations so a fuel failure can identify the actual call or operator rather than only the enclosing base field. + +Migration: freeze a V7 top-level DTO with the old required maps, adapt it to an empty definitions catalog and current schema, and reject new analysis constructors/fields in all earlier versions, including explicit empty/null attempts. Do not default away missing definitions or Binding fields in native new-schema input. The V5/V6 decode branches also currently deserialize through Project; route them through an appropriate frozen top-level DTO before their existing migration logic, and update all older-adapter Project constructors. The existing source upgrade should preserve old semantic baseline bytes and authored modules; ordinary schema7 models acquire no analysis assumptions. + +Use new pure read endpoints POST /api/v1/projects/{id}/analysis/evaluate and /analysis/freeze, plus a private-capture replay endpoint when capture support is complete. The request must carry context, targets, numeric_profile and work_limits; the hosted envelope also requires an exact requested revision. Reuse the existing revision-check and captured ETag response convention. A valid false/Missing/Failed evaluation returns HTTP 200 with its typed result; malformed request is 400, unavailable revision follows the existing conflict policy, and invalid semantic target/type is 422. Evaluation does not increment revision or keep the store mutex while doing arithmetic. Existing store.get already clones an accepted StoredProject for worker work. + +Add a CLI evaluate operation consuming a request JSON file with the identical core request, rather than a second formula language or implicit current context. Existing source Check/Stabilize/RenameAlias remain the authoring workflow. If disk source still needs identity stabilization/migration, first evaluation should require the explicit existing stabilization/save step so repeated evaluations do not invent new local identities. A CLI capture records its actual source/document digest; it must not invent a hosted ETag or a persisted local revision counter. The native Document already has accepted snapshot/revision/history and can later call the same evaluator without applying a pending editor. + +## Admission, capture, history and transition boundaries + +Retain current transport caps: REST 8 MiB model/body, 8 MiB serialized source bundle, 5,000 graph objects, 20,000 records and 50,000 ordered references; CLI currently allows 64 MiB source with its separate graph/record caps. Count definitions and parameters in record budgets, and count Expr nodes, argument/override entries and list members across the entire admitted document, not separately per included file or target. The ratified expression limits are depth 128, 65,536 stored nodes per closure, list length 1,024 and call depth 32. Also impose a deterministic aggregate admission-work budget for traversing all case-effective graphs, so many small cases cannot multiply validation work without charge. Its exact ceiling requires root's bounded measurements; keep that admission policy separate from per-evaluation WorkLimits. + +Raw byte bounds must precede JSON/String allocation; decoded exact components are capped before BigInt allocation. Native new-schema JSON, command bodies and source need the same aggregate literal-admission meter; derived per-Exact Serde alone does not supply it. The existing source value-depth 64 and JSON decoding recursion behavior must be reconciled with a logical Expr depth of 128 through bounded typed readers and explicit positive boundary tests. Do not silently reduce the ratified profile or disable decoder limits without a replacement bound. Effective evaluation limits/profile are recorded in request/result/capture identity; the numeric module's provisional ceilings are not calibrated timing guarantees. + +There is no production PortableDocument type in the inspected core. Add a shared capture type containing the actual Project plus exact SourceBundle, and later the common package environment's pins and exact archive bytes. Reopening verifies captured source compilation equals the captured Project, exact capsule digest, full local-definition inventory and redundant effective-binding/check manifests. This is a private immutable namespace and never goes through live Reidentify. Whole-document local capture must include unused definitions and other cases; a result or reachable-value subset is insufficient. Bound encoded envelope, decoded bytes, records and manifest entries before allocation, with any route-specific larger freeze ceiling explicit. Nonempty pinned offline replay/tamper rejection is a separate mandatory gate once the real library environment exists; an empty local example cannot prove it. + +Snapshot undo/redo in Session and desktop Document automatically includes new typed fields once source updates are correct. OA/SA reviewed history is different: add explicit typed Property/Case/Check facets and historical Expr/reference walkers together with their schema descriptors when analysis transitions are implemented. Do not reuse live resolution for deleted historical refs, or reinterpret existing ConstraintFacet::Expression text. Until that support lands, reject analysis requests in semantic review/transition entry points with an explicit capability error; adding Kind mappings alone is unsafe, and manual traces must not produce a misleading header-only semantic-success result. Ordinary descriptive manual trace storage can remain descriptive. The subsequent transition slice needs explicit AnalysisSelection, whole selected cases, remapped subject/property/check IDs, unchanged neutral definition identities and explicit inclusion/omission; it must not inverse-pull every unrelated case mentioning a property. + +## Proposed file ownership and sequence + +These are proposed implementation leases, not permission for concurrent edits yet. Root retains manifests, lib.rs declarations, shared integration hooks and Cargo; each existing file has one writer at a time. + +| Order / owner role | Concrete files | Exit evidence | +| --- | --- | --- | +| 0. Root + numeric owner, renewed lease | analysis_numeric/quantity.rs and tests.rs only after current freeze gate | Pure type helpers agree with runtime R6; terminal-wrapper controls; existing numeric tests stay passing. | +| 1. Core contract owner | new analysis.rs, analysis/types.rs, analysis/references.rs, analysis/admission.rs; model.rs, session.rs, references.rs, validation.rs, persistence.rs; new migration_v7.rs | Actual Project JSON round-trip, unique IDs/keys, explicit bases, transactions/deletion, old-schema rejection/migration. Root applies lib.rs hook. | +| 2. Source owner | language.rs, new language/analysis_source.rs, source_project.rs, source_project/source_structure.rs, source_project/source_migration.rs; new crates/oa-core/tests/analysis_source.rs; new examples/analysis/response-budget/ | Entire real fixture, fresh-ID stabilization, parameter rename, aliases/includes/comments, R7 literal AST equality, exact command-source correspondence. | +| 3. Evaluator owner after types fixed | new analysis/resolve.rs, analysis/typecheck.rs, analysis/evaluate.rs, analysis/tests.rs; shared analysis.rs glue stays with contract owner | Actual shared Expr traversal, B effective graphs, R6/R7 outcomes, actual C1 exponential-call witness bounded across all targets, origins and incomplete causes. | +| 4. API/CLI owner after core callable | routes.rs, new routes/analysis.rs, minimal store.rs snapshot hook if needed; oa-cli/src/lib.rs/main.rs and CLI tests; new oa-server/tests/http/analysis.rs plus test registration | Same accepted source/JSON report via CLI and HTTP; revision races, no save on Evaluate, body/admission limits. | +| 4. Same API/schema owner | docs/openapi.json, oa-server/tests/semantic_schema.py, docs/api.rst, docs/language.rst, docs/source-cli.md and generated HTML | Closed schemas/required fields/commands/request/outcome match actual Serde; schema fixtures and documented grammar compile. Coordinate peer language-doc ownership before touching them. | +| 5. Capture owner | new analysis/capture.rs and capture tests; API/CLI adapters under their current owner | Whole local snapshot replay after live source/definition changes; tampered capsule/manifests reject. Then integrate real package pins/bytes and nonempty offline controls. | +| 6. History/transition + native authoring owners | semantic/types.rs/catalog.rs/historical.rs/mutate.rs/review.rs, transitions.rs and new transitions/analysis.rs; descriptor/API owner updates schema; desktop analysis/forms/document hooks | Explicit OA/SA analysis selection and historical parity; then native base/override/check/context authoring, source equality, undo/reopen and stale result handling. | + +Steps 1–4 form the first useful source-authored persisted evaluation gate; step 5 supplies reproducible export, and step 6 closes existing transition/native workflows. They are implementation sequencing, not a narrowed release objective. Approximate engineering functions/irrational unit scales, real reusable libraries and dense full-model textual usability remain required. + +## First acceptance fixture and falsifiers + +Use the frozen fixture's actual identities and independent expected model, never an evaluator-generated expected Project. Model 4210b9f2-7046-47f0-aa3b-153f626a579d has local Duration, second/millisecond and combine definitions; four properties; degraded and unmeasured cases; one shared check. Requested total is bd5b68e8-65fc-4e35-9071-a73061316a4b and check is bac0de99-9d2f-4e53-9158-d424ecac61bf. The degraded case is 38036c65-16d4-449c-837b-91eb141c1d93; unmeasured is 99d3e09a-0ec3-4194-9dd4-9f3de6625cde. + +| Transaction/request | Required real observation | +| --- | --- | +| Source import/save/reopen; evaluate ModelBaseline | 750 ms + 1 s = 7/4 seconds; shared check Satisfied against 2 s. Equivalent JSON produces the same persistent AST. | +| Evaluate degraded | 1250 ms + 1 s = 9/4 seconds; the same check ID is Violated. Total formula origin is Base, receive-time origin is this case's override. | +| Evaluate unmeasured; then ClearAnalysisOverride | Missing receive-time/Unresolved check; clearing restores 7/4 and Satisfied. Setting Unbound and clearing must remain distinct commands/source edits. | +| Edit threshold property once | Both contexts use the same check and new threshold unless that property is explicitly overridden. No predicate copies are rewritten. | +| Baseline edit causing only a case-effective cycle; invalid unused branch | Entire transaction/source admission rejects; prior model, comments, revision and undo remain unchanged. | +| Rename receive_time alias and calculation parameter a; Reidentify local definition | Persistent IDs stay stable for renames; exact typed refs/argument tokens change appropriately; unrelated comments, historical strings and ParameterIds are untouched by ordinary global reidentification. | +| Delete a used property/definition/subject without repair; repair in same batch | First rejects; second admits once. No automatic dropping of an override or conversion to Unbound. | +| Full R7 atoms, affine and anonymous energy expressions | Source/JSON retain exact literal AST and runtime R6 types; no f64 conversion, dimension-only nominal matching or dummy-value type checking. | +| Real C1 call tree, multiple targets, identical repeat | Actual Expr evaluator stops at the same first location/work usage with incomplete causes and no later visits. Cold/warm policy cannot change effective limits or outcome. | +| HTTP expected revision changes before capture | Existing revision conflict; evaluation never acts on a different accepted snapshot than the reported revision/ETag. | +| Whole local freeze then edit live dispatch and combine | Frozen degraded stays 9/4 with old exact sources/definitions while the live result changes. Missing captured content or a tampered redundant manifest rejects. | + +Root's remaining staging ratifications are narrow: allocate the schema number; choose whether the real package environment precedes this local fixture or follows it; approve concrete decoder/admission limits after bounded tests. The selected B/R6/R7 semantics do not need another architecture comparison before production work.