From 57de8126d538083fc908757462f718b6ccdf94d9 Mon Sep 17 00:00:00 2001 From: acamilo Date: Tue, 22 Sep 2026 13:12:59 +0000 Subject: [PATCH] fix(session-types): check the rational addition, and hold the schema set to the readers list Two fixes from the independent review of f043cd7. RationalNs::checked_add cross-multiplied into u128 and then added without a check. Each product fits, but their sum does not: two reduced fractions near the U64 maximum add to about 2^129, which panics in debug and wraps in release, after which the reduction returns a confidently wrong rational. Every multiplication and the addition now go through a checked path, as ipc-v1 section 2 requires, with a fixture row and a test that reaches the overflow rather than the "does not fit U64" reduction limit. The schema-set test checked fourteen hardcoded type names, so a new payload type could have shipped outside contractDigest. It now iterates the readers own list, all fifty of them. Also amends ipc-v1 section 5, dated: Worker.Acknowledge carries req- request ids, not arbitrary Ids, because the serial watermark rule in that same section cannot reject reuse after acknowledgment unless the acknowledged id carries its serial. --- docs/design/session-framework/ipc-v1.md | 5 +++ .../fly-session-types/fixtures/rational.json | 24 ++++++++++++++ .../crates/fly-session-types/src/scalar.rs | 30 +++++++++++++----- .../fly-session-types/tests/rational.rs | 19 ++++++++++++ .../fly-session-types/tests/schema_set.rs | 31 ++++++++----------- 5 files changed, 83 insertions(+), 26 deletions(-) diff --git a/docs/design/session-framework/ipc-v1.md b/docs/design/session-framework/ipc-v1.md index 98778f9..083a6ce 100644 --- a/docs/design/session-framework/ipc-v1.md +++ b/docs/design/session-framework/ipc-v1.md @@ -154,6 +154,11 @@ Lifecycle/capture replies are retained until Worker.Acknowledge: not another consumer's bus delivery. Already released/unknown IDs are ignored. Serial watermarks reject reuse after acknowledgment without an unbounded tombstone list. +**Amendment, 2026-09-22 (CONTRACT-01):** those ids are domain request ids in the `req-` +serial form, not arbitrary `Id`s. The serial watermark rule in the sentence above cannot reject +reuse after acknowledgment unless the acknowledged id carries its serial, so a bus callId or a +bare `Id` is refused there. + Bound unacknowledged lifecycle replies at 16, then BUSY before application. Status and Acknowledge use a cache of their last 16 replies; current/previous step records have their separate finite retention. Caches containing big artifacts consume bus owner/byte budgets; diff --git a/services/flysim/crates/fly-session-types/fixtures/rational.json b/services/flysim/crates/fly-session-types/fixtures/rational.json index f32a9ce..17b3634 100644 --- a/services/flysim/crates/fly-session-types/fixtures/rational.json +++ b/services/flysim/crates/fly-session-types/fixtures/rational.json @@ -135,6 +135,18 @@ "denominator": "2" }, "error": "reduced value does not fit U64" + }, + { + "a": { + "numerator": "18446744073709551615", + "denominator": "18446744073709551614" + }, + "b": { + "numerator": "18446744073709551613", + "denominator": "18446744073709551611" + }, + "error": "the cross-multiplied numerators sum past 2^128", + "reason": "two reduced fractions near the U64 maximum: every multiplication fits u128, their sum does not, and the arithmetic must refuse rather than wrap" } ], "subtract": [ @@ -176,6 +188,18 @@ "denominator": "2" }, "error": "subtraction would be negative" + }, + { + "a": { + "numerator": "18446744073709551615", + "denominator": "18446744073709551614" + }, + "b": { + "numerator": "1", + "denominator": "18446744073709551611" + }, + "error": "the reduced difference does not fit U64", + "reason": "large denominators reach the reduction limit rather than the subtraction one" } ], "multiply": [ diff --git a/services/flysim/crates/fly-session-types/src/scalar.rs b/services/flysim/crates/fly-session-types/src/scalar.rs index 7bfc24d..0fdc030 100644 --- a/services/flysim/crates/fly-session-types/src/scalar.rs +++ b/services/flysim/crates/fly-session-types/src/scalar.rs @@ -302,6 +302,14 @@ fn gcd(a: u64, b: u64) -> u64 { a } +/// One checked `u64` x `u64` product. The product itself always fits `u128`; the function +/// exists so every multiplication in the arithmetic below goes through one checked path. +fn mul(a: u64, b: u64) -> Result { + u128::from(a) + .checked_mul(u128::from(b)) + .ok_or_else(|| wire_err("RationalNs: multiplication overflowed")) +} + fn gcd128(a: u128, b: u128) -> u128 { let (mut a, mut b) = (a, b); while b != 0 { @@ -357,20 +365,26 @@ impl RationalNs { Ok(()) } + /// Cross-multiplication of two `U64` pairs fits `u128`, but their *sum* does not: two + /// reduced fractions near the `U64` maximum add to about 2^129. Every step is checked, as + /// ipc-v1 section 2 requires; nothing here may wrap in release and panic in debug. pub fn checked_add(&self, other: &RationalNs) -> Result { - let n = u128::from(self.numerator) * u128::from(other.denominator) - + u128::from(other.numerator) * u128::from(self.denominator); - let d = u128::from(self.denominator) * u128::from(other.denominator); + let left = mul(self.numerator, other.denominator)?; + let right = mul(other.numerator, self.denominator)?; + let n = left + .checked_add(right) + .ok_or_else(|| wire_err("RationalNs: addition overflowed"))?; + let d = mul(self.denominator, other.denominator)?; RationalNs::reduced(n, d) } pub fn checked_sub(&self, other: &RationalNs) -> Result { - let left = u128::from(self.numerator) * u128::from(other.denominator); - let right = u128::from(other.numerator) * u128::from(self.denominator); + let left = mul(self.numerator, other.denominator)?; + let right = mul(other.numerator, self.denominator)?; if right > left { return err("RationalNs: subtraction would be negative"); } - let d = u128::from(self.denominator) * u128::from(other.denominator); + let d = mul(self.denominator, other.denominator)?; RationalNs::reduced(left - right, d) } @@ -385,8 +399,8 @@ impl RationalNs { /// `self - ticks * tick`, which is always `>= 0` and `< tick`. pub fn divide_floor(&self, tick: &RationalNs) -> Result<(u64, RationalNs)> { tick.require_positive("RationalNs::divide_floor tick")?; - let n = u128::from(self.numerator) * u128::from(tick.denominator); - let d = u128::from(self.denominator) * u128::from(tick.numerator); + let n = mul(self.numerator, tick.denominator)?; + let d = mul(self.denominator, tick.numerator)?; let ticks = n / d; if ticks > u128::from(u64::MAX) { return err("RationalNs: tick count does not fit U64"); diff --git a/services/flysim/crates/fly-session-types/tests/rational.rs b/services/flysim/crates/fly-session-types/tests/rational.rs index e73341a..3781a88 100644 --- a/services/flysim/crates/fly-session-types/tests/rational.rs +++ b/services/flysim/crates/fly-session-types/tests/rational.rs @@ -138,3 +138,22 @@ fn reduction_refuses_a_result_that_does_not_fit_u64() { big ); } + +/// The review case: cross-multiplying two reduced fractions near the `U64` maximum fits +/// `u128`, but adding the two products does not. Unchecked, that panics in debug and wraps in +/// release, after which the reduction returns a confidently wrong rational. +#[test] +fn adding_two_fractions_near_the_u64_maximum_is_refused_not_wrapped() { + let left = RationalNs::new(u64::MAX, u64::MAX - 1).expect("consecutive integers are coprime"); + let right = RationalNs::new(u64::MAX - 2, u64::MAX - 4).expect("two odd numbers differing by 2"); + let outcome = left.checked_add(&right); + let message = outcome.expect_err("the sum reaches about 2^129").0; + assert!( + message.contains("overflow"), + "the failure names the overflow rather than the reduction: {message}" + ); + assert!( + left.checked_add(&RationalNs::ZERO).is_ok(), + "the checked path still adds ordinary operands" + ); +} diff --git a/services/flysim/crates/fly-session-types/tests/schema_set.rs b/services/flysim/crates/fly-session-types/tests/schema_set.rs index 5943def..179ed34 100644 --- a/services/flysim/crates/fly-session-types/tests/schema_set.rs +++ b/services/flysim/crates/fly-session-types/tests/schema_set.rs @@ -3,6 +3,9 @@ use fly_session_types::{canonical, fixtures, schema}; use serde_json::Value; +#[allow(dead_code, reason = "this file uses the readers' type list, not the readers")] +mod common; + #[path = "../examples/update_fixtures.rs"] #[allow(dead_code, reason = "the example's main is not used by the test that reuses its writers")] mod updater; @@ -104,6 +107,8 @@ fn the_contract_digest_changes_when_a_schema_changes() { } } +/// Every type the crate can read is declared in the schema set, so a new payload type cannot +/// ship outside `contractDigest`. The list is the readers' own, not a copy of it. #[test] fn the_schema_set_names_every_type_the_crate_reads() { let set = schema::schema_set(); @@ -113,24 +118,14 @@ fn the_schema_set_names_every_type_the_crate_reads() { .iter() .map(|t| t["name"].as_str().expect("name")) .collect(); - for expected in [ - "Scope", - "RationalNs", - "TypedValue", - "SessionRpcRequest", - "SessionRpcFailure", - "PrepareParams", - "StepResult", - "ViewRef", - "AudioRef", - "CaptureResult", - "SessionDescriptor", - "CommittedSnapshot", - "TraceBehaviour", - "TraceOperational", - ] { - assert!(names.contains(&expected), "the schema set must name {expected}"); - } + let missing: Vec<&&str> = common::READABLE_TYPES + .iter() + .filter(|expected| !names.contains(*expected)) + .collect(); + assert!( + missing.is_empty(), + "every readable type must be in the schema set; missing {missing:?}" + ); let mut sorted = names.clone(); sorted.sort_unstable(); assert_eq!(names, sorted, "the rendered set is sorted by type name");