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 Strings, 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:

let input = format!(
    r#"{{"numerator":"{}","denominator":"1"}}"#,
    "1".repeat(1_000_000),
);
let rejected = serde_json::from_str::<Exact>(&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:

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.
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`

13 KiB Raw Blame History Unescape Escape