From fb1b8af2d1279cfc943b177990d69f39a6f884f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Onur=20=C3=96zkan?= Date: Sat, 7 Nov 2026 18:12:11 +0300 Subject: [PATCH] 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 | 1 + firmware/libs/kaptan-actuator/src/dshot.rs | 63 +++++---- .../libs/kaptan-actuator/src/kani_proofs.rs | 121 ++++++++++++++++++ firmware/libs/kaptan-actuator/src/lib.rs | 44 ++++++- firmware/libs/kaptan-actuator/src/pwm.rs | 67 +++++++++- 5 files changed, 261 insertions(+), 35 deletions(-) create mode 100644 firmware/libs/kaptan-actuator/src/kani_proofs.rs diff --git a/firmware/Cargo.toml b/firmware/Cargo.toml index 74c66cd..83e3784 100644 --- a/firmware/Cargo.toml +++ b/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" diff --git a/firmware/libs/kaptan-actuator/src/dshot.rs b/firmware/libs/kaptan-actuator/src/dshot.rs index 1ca0be1..3132a64 100644 --- a/firmware/libs/kaptan-actuator/src/dshot.rs +++ b/firmware/libs/kaptan-actuator/src/dshot.rs @@ -18,15 +18,12 @@ impl Config { rate: Rate, armed_idle_throttle: Throttle, arming_duration: ArmingDuration, - ) -> Option { - if rate.frames_for_millis(arming_duration.milliseconds()) == 0 { - return None; - } - Some(Self { + ) -> Self { + 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 { - let symbol_hz = rate.hertz(); - let ticks = (timer_hz + symbol_hz / 2) / symbol_hz; - if ticks < 3 || ticks > u16::MAX as u32 { + let symbol_hz = rate.hertz() as u64; + let ticks = (timer_hz as u64 + symbol_hz / 2) / symbol_hz; + 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 crate::ArmingDuration; + use super::{ArmSequence, FrameValue, Rate, Throttle, Timing, packet, symbols}; #[test] fn packet_matches_standard_dshot_vectors() { @@ -250,9 +237,33 @@ mod tests { } #[test] - fn requires_an_arming_interval_with_frames() { - let duration = ArmingDuration::from_millis(2_000).unwrap(); - let throttle = Throttle::new(300).unwrap(); - assert!(Config::new(Rate::Dshot600, throttle, duration).is_some()); + fn timer_clock_boundaries_do_not_overflow_or_clamp() { + for (rate, maximum_profile) in [ + (Rate::Dshot150, (28_633, 10_022, 20_043)), + (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 + ); + } } } diff --git a/firmware/libs/kaptan-actuator/src/kani_proofs.rs b/firmware/libs/kaptan-actuator/src/kani_proofs.rs new file mode 100644 index 0000000..e65cc2b --- /dev/null +++ b/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::() { + 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()); +} diff --git a/firmware/libs/kaptan-actuator/src/lib.rs b/firmware/libs/kaptan-actuator/src/lib.rs index 982e6ab..d3f5022 100644 --- a/firmware/libs/kaptan-actuator/src/lib.rs +++ b/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 -//! reviewed physical-flight work. No checked-in board platform links it, and -//! its types model DShot/PWM framing and -//! local arming sequences only; they grant neither peripheral access nor -//! flight authority. +//! This reference crate grants no peripheral access or flight authority and is +//! not linked by the current board images. #![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 { + frame_count(self.0 as u64 * cadence_hz as u64) + } +} + +const fn frame_count(requested: u64) -> Option { + 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) + ); + } +} diff --git a/firmware/libs/kaptan-actuator/src/pwm.rs b/firmware/libs/kaptan-actuator/src/pwm.rs index 41665a4..ff90c2e 100644 --- a/firmware/libs/kaptan-actuator/src/pwm.rs +++ b/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 { - if 1_000_000 % self.0 as u32 == 0 { - Some((1_000_000 / self.0 as u32) as u16) + let period = 1_000_000 / self.0 as u32; + 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); + } + } + } }