diff --git a/quon_qec/src/family.rs b/quon_qec/src/family.rs index 2577b2c..35bdc2e 100644 --- a/quon_qec/src/family.rs +++ b/quon_qec/src/family.rs @@ -90,48 +90,90 @@ pub fn atoms_per_logical(family: &CodeFamily) -> Result { } /// `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) + spec(fn(d: u32) -> Result) )] pub fn surface_n(distance: u32) -> Result { 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) + spec(fn(d: u32) -> Result) )] pub fn repetition_n(distance: u32) -> Result { 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) + 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 { 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 diff --git a/quon_qec/src/qldpc.rs b/quon_qec/src/qldpc.rs index bf0281b..ff6594e 100644 --- a/quon_qec/src/qldpc.rs +++ b/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 { + // `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