fix(actuator): validate reference timing calculations

Reject invalid DShot and PWM timer domains and widen arming-duration
calculations before composing their results.

Validation: actuator tests, strict Clippy and five Kani component proofs.

firmware/Cargo.toml

@@ -38,6 +38,7 @@ rust-version = "1.90"
 
 [workspace.lints.rust]
 unsafe_op_in_unsafe_fn = "deny"
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
 
 [workspace.lints.clippy]
 undocumented_unsafe_blocks = "deny"

firmware/libs/kaptan-actuator/src/dshot.rs

@@ -18,15 +18,12 @@ impl Config {
         rate: Rate,
         armed_idle_throttle: Throttle,
         arming_duration: ArmingDuration,
-    ) -> Option<Self> {
+    ) -> Self {
-        if rate.frames_for_millis(arming_duration.milliseconds()) == 0 {
+        Self {
-            return None;
-        }
-        Some(Self {
             rate,
             armed_idle_throttle,
             arming_duration,
-        })
+        }
     }
 
     pub const fn rate(self) -> Rate {
@@ -62,17 +59,6 @@ impl Rate {
     pub const fn timer_base_hz(self) -> u32 {
         self.hertz() * 20
     }
-
-    pub const fn output_rate_hz(self) -> u32 {
-        match self {
-            Self::Dshot150 => 4_000,
-            Self::Dshot300 | Self::Dshot600 => 8_000,
-        }
-    }
-
-    pub const fn frames_for_millis(self, milliseconds: u16) -> u16 {
-        ((self.output_rate_hz() * milliseconds as u32) / 1_000) as u16
-    }
 }
 
 #[derive(Clone, Copy, Debug, Eq, PartialEq)]
@@ -83,10 +69,12 @@ pub struct Timing {
 }
 
 impl Timing {
+    /// Rounds to the nearest symbol tick, with half ticks rounded up.
+    /// Rejects clocks whose symbol period cannot fit 3..=65,535 ticks.
     pub const fn from_timer_clock(timer_hz: u32, rate: Rate) -> Option<Self> {
-        let symbol_hz = rate.hertz();
+        let symbol_hz = rate.hertz() as u64;
-        let ticks = (timer_hz + symbol_hz / 2) / symbol_hz;
+        let ticks = (timer_hz as u64 + symbol_hz / 2) / symbol_hz;
-        if ticks < 3 || ticks > u16::MAX as u32 {
+        if ticks < 3 || ticks > u16::MAX as u64 {
             return None;
         }
         let bit_ticks = ticks as u16;
@@ -214,8 +202,7 @@ pub const fn symbols(packet: u16, zero_high: u16, one_high: u16) -> [u16; FRAME_
 
 #[cfg(test)]
 mod tests {
-    use super::{ArmSequence, Config, FrameValue, Rate, Throttle, Timing, packet, symbols};
+    use super::{ArmSequence, FrameValue, Rate, Throttle, Timing, packet, symbols};
-    use crate::ArmingDuration;
 
     #[test]
     fn packet_matches_standard_dshot_vectors() {
@@ -250,9 +237,33 @@ mod tests {
     }
 
     #[test]
-    fn requires_an_arming_interval_with_frames() {
+    fn timer_clock_boundaries_do_not_overflow_or_clamp() {
-        let duration = ArmingDuration::from_millis(2_000).unwrap();
+        for (rate, maximum_profile) in [
-        let throttle = Throttle::new(300).unwrap();
+            (Rate::Dshot150, (28_633, 10_022, 20_043)),
-        assert!(Config::new(Rate::Dshot600, throttle, duration).is_some());
+            (Rate::Dshot300, (14_317, 5_011, 10_022)),
+            (Rate::Dshot600, (7_158, 2_505, 5_011)),
+        ] {
+            assert!(Timing::from_timer_clock(0, rate).is_none());
+            let first_supported = rate.hertz() * 5 / 2;
+            assert!(Timing::from_timer_clock(first_supported - 1, rate).is_none());
+            let minimum = Timing::from_timer_clock(first_supported, rate).unwrap();
+            assert_eq!(
+                (
+                    minimum.bit_ticks(),
+                    minimum.zero_high_ticks(),
+                    minimum.one_high_ticks()
+                ),
+                (3, 1, 2)
+            );
+            let maximum = Timing::from_timer_clock(u32::MAX, rate).unwrap();
+            assert_eq!(
+                (
+                    maximum.bit_ticks(),
+                    maximum.zero_high_ticks(),
+                    maximum.one_high_ticks()
+                ),
+                maximum_profile
+            );
+        }
     }
 }

firmware/libs/kaptan-actuator/src/kani_proofs.rs

@@ -0,0 +1,121 @@
+//! Integer wire and timing contracts.
+
+use super::dshot::{FrameValue, Rate, Throttle, Timing, symbols};
+
+fn any_rate() -> Rate {
+    match kani::any::<u8>() {
+        0 => Rate::Dshot150,
+        1 => Rate::Dshot300,
+        _ => Rate::Dshot600,
+    }
+}
+
+#[kani::proof]
+fn dshot_frame_preserves_payload_and_checksum() {
+    let raw: u16 = kani::any();
+    let stop: bool = kani::any();
+    let frame = if stop {
+        FrameValue::Stop
+    } else {
+        let Some(throttle) = Throttle::new(raw) else {
+            assert!(!(48..=2_047).contains(&raw));
+            return;
+        };
+        assert!((48..=2_047).contains(&raw));
+        FrameValue::Throttle(throttle)
+    };
+    let packet = frame.packet();
+    assert_eq!(packet >> 5, if stop { 0 } else { raw });
+    assert_eq!(packet & 0x10, 0);
+    assert_eq!(
+        (packet ^ (packet >> 4) ^ (packet >> 8) ^ (packet >> 12)) & 0xf,
+        0
+    );
+    kani::cover!(stop);
+    kani::cover!(!stop && raw == 48);
+    kani::cover!(!stop && raw == 2_047);
+}
+
+#[kani::proof]
+#[kani::unwind(17)]
+fn dshot_symbols_round_trip_and_end_low() {
+    let packet: u16 = kani::any();
+    let zero: u16 = kani::any();
+    let one: u16 = kani::any();
+    let encoded = symbols(packet, zero, one);
+    let mut decoded = 0_u16;
+    for symbol in &encoded[..16] {
+        assert!(*symbol == zero || *symbol == one);
+        decoded = (decoded << 1) | u16::from(*symbol == one);
+        if zero == one {
+            assert_eq!(*symbol, zero);
+        }
+    }
+    if zero != one {
+        assert_eq!(decoded, packet);
+    }
+    assert_eq!(encoded[16], 0);
+    assert_eq!(encoded[17], 0);
+    // Equal levels are legal arguments. The framing function does not claim
+    // that every caller-supplied pair is physically distinguishable.
+    kani::cover!(zero == one);
+    kani::cover!(zero != one && packet != 0 && packet != u16::MAX);
+}
+
+#[kani::proof]
+fn dshot_timer_rounding_keeps_compares_inside_period() {
+    let rate = any_rate();
+    let timer_hz: u32 = kani::any();
+    let timing = Timing::from_timer_clock(timer_hz, rate);
+    let requested = u64::from(timer_hz);
+    let symbol_hz = u64::from(rate.hertz());
+    if let Some(timing) = timing {
+        let represented = u64::from(timing.bit_ticks()) * symbol_hz;
+        // Nearest period, with half-symbol ties rounded upward.
+        assert!(2 * represented <= 2 * requested + symbol_hz);
+        assert!(2 * represented + symbol_hz > 2 * requested);
+        assert!(timing.zero_high_ticks() > 0);
+        assert!(timing.zero_high_ticks() < timing.one_high_ticks());
+        assert!(timing.one_high_ticks() < timing.bit_ticks());
+    } else {
+        // At all supported DShot rates u32::MAX still fits a u16 period.
+        // Therefore refusal is exactly below the minimum three-tick period.
+        assert!(2 * requested < 5 * symbol_hz);
+    }
+    kani::cover!(timing.is_none());
+    kani::cover!(timing.is_some() && timer_hz == u32::MAX);
+}
+
+#[kani::proof]
+fn arming_duration_product() {
+    let milliseconds: u16 = kani::any();
+    let cadence_hz: u32 = kani::any();
+    let Some(duration) = super::ArmingDuration::from_millis(milliseconds) else {
+        assert!(milliseconds == 0 || milliseconds > 8_000);
+        return;
+    };
+    assert_eq!(duration.milliseconds(), milliseconds);
+    assert!((1..=8_000).contains(&milliseconds));
+    let requested = u64::from(duration.milliseconds()) * u64::from(cadence_hz);
+    assert!(requested <= 8_000 * u64::from(u32::MAX));
+    assert_eq!(requested == 0, cadence_hz == 0);
+    kani::cover!(milliseconds == 1 && cadence_hz == 0);
+    kani::cover!(milliseconds == 8_000 && cadence_hz == u32::MAX);
+}
+
+#[kani::proof]
+fn arming_frame_count() {
+    let requested: u64 = kani::any();
+    let frames = super::frame_count(requested);
+    if let Some(frames) = frames {
+        let frames = u64::from(frames);
+        assert!(requested != 0 && frames != 0);
+        assert!(frames * 1_000 >= requested);
+        assert!((frames - 1) * 1_000 < requested);
+    } else {
+        assert!(requested == 0 || requested > u64::from(u16::MAX) * 1_000);
+    }
+    kani::cover!(requested == 0 && frames.is_none());
+    kani::cover!(frames.is_some() && requested % 1_000 != 0);
+    kani::cover!(requested == u64::MAX && frames.is_none());
+}

firmware/libs/kaptan-actuator/src/lib.rs

@@ -1,16 +1,16 @@
-//! Protocol-neutral physical-motor protocol reference.
+//! DShot/PWM framing and local arming sequences.
 //!
-//! This crate deliberately remains in the workspace for future, separately
+//! This reference crate grants no peripheral access or flight authority and is
-//! reviewed physical-flight work. No checked-in board platform links it, and
+//! not linked by the current board images.
-//! its types model DShot/PWM framing and
-//! local arming sequences only; they grant neither peripheral access nor
-//! flight authority.
 
 #![no_std]
 
 pub mod dshot;
 pub mod pwm;
 
+#[cfg(kani)]
+mod kani_proofs;
+
 #[derive(Clone, Copy, Debug, Eq, PartialEq)]
 pub struct ArmingDuration(u16);
 
@@ -26,6 +26,18 @@ impl ArmingDuration {
     pub const fn milliseconds(self) -> u16 {
         self.0
     }
+
+    /// Minimum frame count at the caller's periodic dispatch cadence.
+    pub const fn frames_at(self, cadence_hz: u32) -> Option<u16> {
+        frame_count(self.0 as u64 * cadence_hz as u64)
+    }
+}
+
+const fn frame_count(requested: u64) -> Option<u16> {
+    if requested == 0 || requested > u16::MAX as u64 * 1_000 {
+        return None;
+    }
+    Some((requested as u32).div_ceil(1_000) as u16)
 }
 
 #[derive(Clone, Copy, Debug, Eq, PartialEq)]
@@ -33,3 +45,23 @@ pub enum MotorProtocol {
     Pwm(pwm::Config),
     Dshot(dshot::Config),
 }
+
+#[cfg(test)]
+mod tests {
+    use super::ArmingDuration;
+
+    #[test]
+    fn frame_count_uses_dispatch_cadence() {
+        let duration = ArmingDuration::from_millis(8_000).unwrap();
+        assert_eq!(duration.frames_at(0), None);
+        assert_eq!(duration.frames_at(4_000), Some(32_000));
+        assert_eq!(duration.frames_at(8_000), Some(64_000));
+        assert_eq!(duration.frames_at(8_191), Some(65_528));
+        assert_eq!(duration.frames_at(8_192), None);
+        assert_eq!(duration.frames_at(u32::MAX), None);
+        assert_eq!(
+            ArmingDuration::from_millis(1).unwrap().frames_at(333),
+            Some(1)
+        );
+    }
+}

firmware/libs/kaptan-actuator/src/pwm.rs

@@ -66,16 +66,22 @@ impl Rate {
         self.0
     }
 
+    /// Returns an integral period representable by a 16-bit microsecond timer.
+    /// Rates with fractional periods or periods above 65,535 µs are unsupported.
     pub const fn period_microseconds(self) -> Option<u16> {
-        if 1_000_000 % self.0 as u32 == 0 {
+        let period = 1_000_000 / self.0 as u32;
-            Some((1_000_000 / self.0 as u32) as u16)
+        if 1_000_000 % self.0 as u32 == 0 && period <= u16::MAX as u32 {
+            Some(period as u16)
         } else {
             None
         }
     }
 
+    /// Rounds up so the frames last at least the requested duration.
     pub const fn frames_for_millis(self, milliseconds: u16) -> u16 {
-        ((self.0 as u32 * milliseconds as u32) / 1_000) as u16
+        // Rate is at most 500 Hz. The product is at most 32,767,500 and
+        // the rounded-up result at most 32,768 for every u16 duration.
+        (self.0 as u32 * milliseconds as u32).div_ceil(1_000) as u16
     }
 }
 
@@ -184,4 +190,59 @@ mod tests {
         assert!(Config::new(Rate::new(333).unwrap(), minimum, idle, duration).is_none());
         assert!(Config::new(rate, idle, minimum, duration).is_none());
     }
+
+    #[test]
+    fn timer_period_support_is_exact_over_the_entire_rate_domain() {
+        let duration = ArmingDuration::from_millis(1).unwrap();
+        let minimum = PulseWidth::new(1_000).unwrap();
+        let idle = PulseWidth::new(1_100).unwrap();
+        for hertz in 0..=u16::MAX {
+            let Some(rate) = Rate::new(hertz) else {
+                assert!(hertz == 0 || hertz > 500);
+                continue;
+            };
+            // Divisors of 10^6 in 1..=500 whose quotient fits u16.
+            let supported = matches!(
+                hertz,
+                16 | 20
+                    | 25
+                    | 32
+                    | 40
+                    | 50
+                    | 64
+                    | 80
+                    | 100
+                    | 125
+                    | 160
+                    | 200
+                    | 250
+                    | 320
+                    | 400
+                    | 500
+            );
+            assert_eq!(rate.period_microseconds().is_some(), supported);
+            assert_eq!(
+                Config::new(rate, minimum, idle, duration).is_some(),
+                supported
+            );
+            if let Some(period) = rate.period_microseconds() {
+                assert_eq!(u64::from(period) * u64::from(hertz), 1_000_000);
+            }
+        }
+    }
+
+    #[test]
+    fn every_rate_and_duration_uses_the_least_sufficient_frame_count() {
+        // All accepted rates and every public u16 duration, including values
+        // beyond ArmingDuration's 8-second configuration limit.
+        for hertz in 1..=500 {
+            let rate = Rate::new(hertz).unwrap();
+            for milliseconds in 0..=u16::MAX {
+                let frames = u64::from(rate.frames_for_millis(milliseconds));
+                let requested = u64::from(hertz) * u64::from(milliseconds);
+                assert!(frames * 1_000 >= requested);
+                assert!(frames == 0 || (frames - 1) * 1_000 < requested);
+            }
+        }
+    }
 }