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-<U64> 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

@@ -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-<U64>`
+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;

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": [

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> {
+    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<RationalNs> {
-        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<RationalNs> {
-        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");

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"
+    );
+}

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");