fix: strengthen QEC sizing and distance contracts with Flux (#412)

quon_qec/src/family.rs

@@ -90,48 +90,90 @@ pub fn atoms_per_logical(family: &CodeFamily) -> Result<u32, QecError> {
 }
 
 /// `N(d) = 2d² − 1` for odd `d ≥ 3` (architecture_model.md §10.1).
+///
+/// The refined spec proves the successful (`Ok`) result equals the closed-form
+/// `2*d*d − 1`. The body rejects out-of-domain distances first, then rejects
+/// any `d > 46340` — the largest odd `d` with `2*d*d <= u32::MAX` (since
+/// `2·46341² > u32::MAX`) — before the unchecked multiplication, so the `Ok`
+/// path never wraps. Flux discharges the `Ok` postcondition from the
+/// primitive-arithmetic refinement (no `trusted` body, no empty `Result<_, _>`
+/// spec).
 #[cfg_attr(
     feature = "flux",
-    spec(fn(d: u32) -> Result<u32, QecError>)
+    spec(fn(d: u32) -> Result<u32{v: v == 2 * d * d - 1}, QecError>)
 )]
 pub fn surface_n(distance: u32) -> Result<u32, QecError> {
     if distance < 3 || distance.is_multiple_of(2) {
         return Err(QecError::InvalidSurfaceDistance { distance });
     }
-    let d2 = distance
-        .checked_mul(distance)
-        .ok_or(QecError::AtomCountOverflow)?;
-    let two_d2 = d2.checked_mul(2).ok_or(QecError::AtomCountOverflow)?;
-    two_d2.checked_sub(1).ok_or(QecError::AtomCountOverflow)
+    // `2*d*d` overflows `u32` once `d > 46340` (2·46341² > u32::MAX). Reject
+    // before the unchecked multiplication so the `Ok` path never wraps.
+    if distance > 46340 {
+        return Err(QecError::AtomCountOverflow);
+    }
+    Ok(2 * distance * distance - 1)
 }
 
 /// `N(d) = 2d − 1` for `d ≥ 2` (architecture_model.md §10.2).
+///
+/// The refined spec proves the successful (`Ok`) result equals the closed-form
+/// `2*d − 1`. With overflow checking enabled, the body rejects `d < 2` and
+/// `d > u32::MAX/2` (where `2*d` would overflow) before the unchecked
+/// arithmetic, so Flux proves both the `Ok` postcondition and the absence of
+/// overflow/underflow (no `trusted` body, no empty `Result<_, _>` spec).
+#[cfg_attr(feature = "flux", opts(check_overflow = "strict"))]
 #[cfg_attr(
     feature = "flux",
-    spec(fn(d: u32) -> Result<u32, QecError>)
+    spec(fn(d: u32) -> Result<u32{v: v == 2 * d - 1}, QecError>)
 )]
 pub fn repetition_n(distance: u32) -> Result<u32, QecError> {
     if distance < 2 {
         return Err(QecError::InvalidRepetitionDistance { distance });
     }
-    let two_d = distance.checked_mul(2).ok_or(QecError::AtomCountOverflow)?;
-    two_d.checked_sub(1).ok_or(QecError::AtomCountOverflow)
+    // `2*d` overflows `u32` once `d > u32::MAX / 2`. Reject before the
+    // unchecked multiplication so the `Ok` path never wraps.
+    if distance > u32::MAX / 2 {
+        return Err(QecError::AtomCountOverflow);
+    }
+    Ok(2 * distance - 1)
 }
 
-/// Ceiling division `(numerator + denominator - 1) / denominator`.
+/// Ceiling division `(numerator + denominator - 1) / denominator`
+/// (architecture_model.md §10.3–§10.4).
+///
+/// The refined spec proves the successful (`Ok`) result is the mathematical
+/// ceiling `⌈numerator / denominator⌉ = (numerator + denominator − 1) /
+/// denominator` for any nonzero denominator. With overflow checking enabled,
+/// the body rejects a zero denominator and any `numerator + denominator` that
+/// would overflow `u32` before the unchecked arithmetic, so Flux proves the
+/// `Ok` postcondition and the absence of overflow/underflow (no `trusted`
+/// body, no empty `Result<_, _>` spec).
+#[cfg_attr(feature = "flux", opts(check_overflow = "strict"))]
 #[cfg_attr(
     feature = "flux",
-    spec(fn(numerator: u32, denominator: u32{v: v > 0}) -> Result<u32, QecError>)
+    spec(
+        fn(numerator: u32, denominator: u32{denominator > 0}) -> Result<
+            u32{v: v == (numerator + denominator - 1) / denominator},
+            QecError
+        >
+    )
 )]
+// The `(numerator + denominator - 1) / denominator` form is deliberate: Flux
+// discharges the `Ok` postcondition from the primitive `/` refinement, but has
+// no refined spec for `u32::div_ceil`, so the clippy-suggested rewrite would
+// break refinement checking. Keep the form and silence the lint.
+#[allow(clippy::manual_div_ceil)]
 pub fn ceil_div(numerator: u32, denominator: u32) -> Result<u32, QecError> {
     if denominator == 0 {
         return Err(QecError::ZeroLogicalDimension);
     }
-    let sum = numerator
-        .checked_add(denominator)
-        .ok_or(QecError::AtomCountOverflow)?;
-    let adjusted = sum.checked_sub(1).ok_or(QecError::AtomCountOverflow)?;
-    Ok(adjusted / denominator)
+    // `numerator + denominator` overflows `u32` once `numerator > u32::MAX -
+    // denominator`. Reject before the unchecked addition so the `Ok` path
+    // never wraps.
+    if numerator > u32::MAX - denominator {
+        return Err(QecError::AtomCountOverflow);
+    }
+    Ok((numerator + denominator - 1) / denominator)
 }
 
 /// Negative compile fixture (issue #411): `ceil_div`'s Flux precondition

quon_qec/src/qldpc.rs

@@ -17,6 +17,8 @@
 //!
 //! Unsupported features fail clearly with actionable diagnostics.
 
+#[cfg(feature = "flux")]
+use flux_rs::attrs::*;
 use serde::{Deserialize, Serialize};
 use thiserror::Error;
 
@@ -321,36 +323,46 @@ pub fn toy_5qubit_graph() -> ParityCheckGraph {
 }
 
 /// A simple toy repetition code for testing.
-pub fn toy_repetition_graph(distance: u32) -> ParityCheckGraph {
-    // A repetition code needs `distance >= 1` so `distance - 1` (the check
-    // count) cannot underflow. The degenerate `distance == 0` case is an
-    // empty code; handling it here keeps the subtraction total *and* lets
-    // Flux prove the arithmetic is safe (it sees `distance >= 1` past this
-    // guard).
+///
+/// A repetition code of distance `d` carries `d` data qubits and `d − 1`
+/// parity checks. The `d − 1` check count underflows for `d == 0`, so this
+/// constructor requires a valid nonzero distance and returns
+/// [`QldpcError::InvalidDistance`] for `d == 0` rather than building a
+/// degenerate empty graph. Overflow checking is enabled so Flux proves the
+/// `d − 1` subtraction (and the per-check `i + 1` index) never underflows or
+/// overflows on the `Ok` path — there is no `trusted` body and no empty
+/// `Result<_, _>` spec; the contract is discharged by the body-level
+/// arithmetic checks under the `distance >= 1` guard.
+#[cfg_attr(feature = "flux", opts(check_overflow = "strict"))]
+pub fn toy_repetition_graph(distance: u32) -> Result<ParityCheckGraph, QldpcError> {
+    // `distance - 1` (the check count) underflows for `distance == 0`. Reject
+    // the invalid distance so Flux sees `distance >= 1` on the `Ok` path and
+    // the subtraction is total.
     if distance == 0 {
-        return ParityCheckGraph {
-            n_data: 0,
-            n_checks: 0,
-            distance: 0,
-            checks: Vec::new(),
-        };
+        return Err(QldpcError::InvalidDistance { distance: 0 });
     }
     let n_data = distance;
     let n_checks = distance - 1;
     let mut checks = Vec::new();
-    for i in 0..n_checks {
+    // A `while` loop (rather than `for i in 0..n_checks`) exposes the
+    // `i < n_checks` bound to Flux so strict overflow checking can prove the
+    // per-check `i + 1` data-qubit index never overflows (`n_checks = d - 1`,
+    // so `i + 1 <= d - 1 < u32::MAX`).
+    let mut i = 0u32;
+    while i < n_checks {
         checks.push(ParityCheck {
             check_id: i,
             basis: CheckBasis::Z,
             data_qubits: vec![i, i + 1],
         });
+        i += 1;
     }
-    ParityCheckGraph {
+    Ok(ParityCheckGraph {
         n_data,
         n_checks,
         distance,
         checks,
-    }
+    })
 }
 
 /// Unsupported features that fail clearly.
@@ -379,13 +391,24 @@ mod tests {
 
     #[test]
     fn toy_repetition_graph_validates() {
-        let graph = toy_repetition_graph(5);
+        let graph = toy_repetition_graph(5).expect("valid distance");
         graph.validate().expect("valid");
         assert_eq!(graph.n_data, 5);
         assert_eq!(graph.n_checks, 4);
         assert_eq!(graph.max_check_weight(), 2);
     }
 
+    #[test]
+    fn toy_repetition_graph_rejects_zero_distance() {
+        // distance == 0 would underflow the `distance - 1` check count; the
+        // constructor must reject it with InvalidDistance rather than build a
+        // degenerate graph (issue #412).
+        assert_eq!(
+            toy_repetition_graph(0),
+            Err(QldpcError::InvalidDistance { distance: 0 })
+        );
+    }
+
     #[test]
     fn rejects_empty_code() {
         let graph = ParityCheckGraph {
@@ -455,7 +478,7 @@ mod tests {
 
     #[test]
     fn resource_estimate_repetition() {
-        let graph = toy_repetition_graph(5);
+        let graph = toy_repetition_graph(5).expect("valid distance");
         let est = QldpcResourceEstimate::estimate(&graph, 2, 5).expect("estimate");
         assert_eq!(est.max_check_weight, 2);
         assert_eq!(est.edge_count, 8); // 4 checks × 2 data
@@ -479,7 +502,7 @@ mod tests {
 
     #[test]
     fn syndrome_rounds_generate_correct_cnots() {
-        let graph = toy_repetition_graph(5);
+        let graph = toy_repetition_graph(5).expect("valid distance");
         let rounds = generate_syndrome_rounds(&graph, 2).expect("rounds");
         assert_eq!(rounds.len(), 2);
         // Each round has 4 checks × 2 data = 8 CNOTs