Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 12 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -42,10 +42,19 @@ jobs:
- uses: dtolnay/rust-toolchain@stable
with:
components: rustfmt
# Pre-existing cFS crates emit rustfmt deltas; v0.1 tolerates
# them while v0.2 cleans the workspace up.
# `Format` is a REQUIRED status check. It carried `continue-on-error: true`
# from d30a5e3 (2026-05-18, the v0.1.0 release) until v1.139 — so for its
# entire life it could not report failure, and it was promoted to required
# while in that state. The comment that stood here said "v0.1 tolerates
# them while v0.2 cleans the workspace up"; we were at v1.138.
#
# The mask WAS hiding a live violation. On main 3ec4a2f this step logged
# 893 `Diff in` hunks and `exit code 1` while the job reported success —
# and the jobs API reports a continue-on-error step as `success` too, so
# only the log tells. An earlier note here blamed local-vs-CI rustfmt
# divergence; there was none: a local `cargo fmt --all` passes this check.
# Run it. (#409)
- run: cargo fmt --all -- --check
continue-on-error: true

clippy:
name: Clippy
Expand Down
60 changes: 60 additions & 0 deletions artifacts/verification/FV-RELAY-VGATE-004.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
artifacts:
- id: FV-RELAY-VGATE-004
type: sw-verification
title: "VGATE-P04 — the required Format gate can report failure again (v1.139)"
status: implemented
release: falcon-v1.139.0
description: >
Partial verification of SWREQ-RELAY-VGATE-P04, for one instance of the
defect class it names: a gate that is wired, cited and required, and
cannot execute a failing verdict.

WHAT WAS WRONG. `Format` is one of the required status checks on `main`.
Its only substantive step carried `continue-on-error: true`, so a failing
`cargo fmt --all -- --check` left the job conclusion `success`. It was
structurally incapable of going red, and it was promoted to a REQUIRED
context while in that state.

`git log -S` dates the flag to d30a5e3 (2026-05-18) — the v0.1.0 release.
It was inert for its entire life, roughly 137 releases. The comment beside
it read "v0.1 tolerates them while v0.2 cleans the workspace up"; the repo
was at v1.138 when this was found.

WHAT THE MASK WAS HIDING — a live violation, not merely lost potency.
CI's own rustfmt on main 3ec4a2f (job 104933185124) logged 893 `Diff in`
hunks and `Process completed with exit code 1`, and the job reported
`success`. The jobs API reported the step as `success` as well:
continue-on-error rewrites a failed step's conclusion, and only the log
shows the failure. This change's 106-file reformat is the debt the mask
hid.

A CORRECTION, KEPT BECAUSE IT IS THE SAME ERROR. The first draft of this
artifact said the opposite: that CI's rustfmt reported success on every
recent run, and that ~891 local hunks were "the known local-vs-CI rustfmt
divergence". That draft read the masked JOB conclusion as the STEP
result — the exact confusion the mask produces. There was no divergence:
the reformat generated by a local `cargo fmt --all` passed this change's
unmasked check, and the months-old "divergence" belief had the same root.

WHY IT BELONGS TO VGATE-P04. Branch protection asserts that a set of
checks gates `main`. An assessor reading that list would conclude
formatting is enforced. It was not, and had not been since the first
release. That is the same shape as a verification track that cannot run:
wired correctly, cited correctly, and incapable of saying no.

NOT CLAIMED: this artifact covers the Format gate only. The other
instances VGATE-P04 names — the Verus track that cannot find core/std
(#405), the Verus PR trigger filtered on Lean paths (#418), and the
verification gate's missing main backstop (#410) — are open.
tags: [verification, relay, verification-gate, ci, v1.139]
fields:
method: automated-test
steps:
# The flag is gone. A grep is the right assertion here: the property IS
# the absence of a line in the workflow definition.
- run: "! grep -A1 'cargo fmt --all' .github/workflows/ci.yml | grep -q 'continue-on-error'"
# ...and the step still exists, so the fix cannot be 'delete the check'.
- run: "grep -q 'cargo fmt --all -- --check' .github/workflows/ci.yml"
links:
- type: verifies
target: SWREQ-RELAY-VGATE-P04
45 changes: 38 additions & 7 deletions benches/cascade-throughput/benches/cascade_throughput.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,22 @@ const ACCEL: [f32; 3] = [0.15, -0.09, -9.79];
const DT: f32 = 0.001; // 1 kHz rate loop

fn ts_rate(ms: u64) -> RateTime {
RateTime { seconds: ms / 1000, fraction: ((ms % 1000) * (1u64 << 32) / 1000) as u32 }
RateTime {
seconds: ms / 1000,
fraction: ((ms % 1000) * (1u64 << 32) / 1000) as u32,
}
}
fn ts_att(ms: u64) -> AttTime {
AttTime { seconds: ms / 1000, fraction: ((ms % 1000) * (1u64 << 32) / 1000) as u32 }
AttTime {
seconds: ms / 1000,
fraction: ((ms % 1000) * (1u64 << 32) / 1000) as u32,
}
}
fn ts_pos(ms: u64) -> PosTime {
PosTime { seconds: ms / 1000, fraction: ((ms % 1000) * (1u64 << 32) / 1000) as u32 }
PosTime {
seconds: ms / 1000,
fraction: ((ms % 1000) * (1u64 << 32) / 1000) as u32,
}
}

/// IEKF — one propagate step at the rate-loop dt. The estimator is the heaviest
Expand All @@ -52,7 +61,13 @@ fn bench_iekf(c: &mut Criterion) {
let mut t = 0u64;
b.iter(|| {
t = t.wrapping_add(1);
ekf.propagate(black_box(Imu { gyro: GYRO, accel: ACCEL }), black_box(DT));
ekf.propagate(
black_box(Imu {
gyro: GYRO,
accel: ACCEL,
}),
black_box(DT),
);
black_box(ekf.state())
})
});
Expand Down Expand Up @@ -106,7 +121,11 @@ fn bench_rate(c: &mut Criterion) {
let mut ms = 0u64;
b.iter(|| {
ms = ms.wrapping_add(1); // 1 kHz
black_box(pid.tick(black_box(ts_rate(ms)), black_box(GYRO), black_box([0.0, 0.0, 0.0])))
black_box(pid.tick(
black_box(ts_rate(ms)),
black_box(GYRO),
black_box([0.0, 0.0, 0.0]),
))
})
});
}
Expand Down Expand Up @@ -138,10 +157,22 @@ fn bench_full_cascade(c: &mut Criterion) {
b.iter(|| {
ms = ms.wrapping_add(1);
// 1. estimator
ekf.propagate(black_box(Imu { gyro: GYRO, accel: ACCEL }), DT);
ekf.propagate(
black_box(Imu {
gyro: GYRO,
accel: ACCEL,
}),
DT,
);
let st = ekf.state();
// 2. position -> attitude setpoint
let att_sp = pos.tick(ts_pos(ms), [0.3, -0.2, -4.8], [0.05, -0.03, 0.01], [1.0, 0.0, 0.0, 0.0], sp);
let att_sp = pos.tick(
ts_pos(ms),
[0.3, -0.2, -4.8],
[0.05, -0.03, 0.01],
[1.0, 0.0, 0.0, 0.0],
sp,
);
// 3. attitude -> rate setpoint
let rate_sp = att.tick(ts_att(ms), att_sp.quaternion, [1.0, 0.0, 0.0, 0.0]);
// 4. rate -> torque
Expand Down
13 changes: 4 additions & 9 deletions benches/engine-throughput/benches/engine_throughput.rs
Original file line number Diff line number Diff line change
Expand Up @@ -124,20 +124,15 @@ fn bench_cfdp(c: &mut Criterion) {

let mut table = TransactionTable::new();
let txn = table
.begin_send(/* file_size */ 65_536, /* max_retransmit */ 1_000_000)
.begin_send(
/* file_size */ 65_536, /* max_retransmit */ 1_000_000,
)
.expect("transaction slot available");

c.bench_function("cfdp/process_nak__retransmit_event", |b| {
b.iter(|| black_box(table.process_nak(black_box(txn), black_box(1024), black_box(512))))
});
}

criterion_group!(
engines,
bench_lc,
bench_sch,
bench_sc,
bench_hs,
bench_cfdp
);
criterion_group!(engines, bench_lc, bench_sch, bench_sc, bench_hs, bench_cfdp);
criterion_main!(engines);
64 changes: 53 additions & 11 deletions crates/falcon-baromag/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,10 @@ pub mod mag {
pub fn init(&mut self) -> Result<(), DriverError> {
let id = self.bus.read_reg(REG_WHO_AM_I);
if id != WHO_AM_I_VALUE {
return Err(DriverError::WrongIdentity { got: id, want: WHO_AM_I_VALUE });
return Err(DriverError::WrongIdentity {
got: id,
want: WHO_AM_I_VALUE,
});
}
self.bus.write_reg(REG_CNTL1, MODE_CONTINUOUS);
Ok(())
Expand Down Expand Up @@ -133,7 +136,10 @@ pub mod mag {

/// Wrap an I2C bus at the default address.
pub fn new(i2c: I) -> Self {
Self { i2c, addr: Self::DEFAULT_ADDR }
Self {
i2c,
addr: Self::DEFAULT_ADDR,
}
}

/// Wrap an I2C bus at an explicit address.
Expand Down Expand Up @@ -202,7 +208,11 @@ pub mod baro {
// Nominal scales: BMP388 raw is ~24-bit over the sensor range; these
// map a mid-range raw to ~standard sea-level pressure. Replaced by
// the per-chip NVM trim at calibration time.
Self { p_scale: 0.012_5, t_scale: 0.005, t_offset: 0.0 }
Self {
p_scale: 0.012_5,
t_scale: 0.005,
t_offset: 0.0,
}
}
}

Expand All @@ -215,7 +225,10 @@ pub mod baro {
impl<B: RegBus> Bmp388<B> {
/// Wrap a bus with the default calibration.
pub fn new(bus: B) -> Self {
Self { bus, cal: BaroCal::default() }
Self {
bus,
cal: BaroCal::default(),
}
}

/// Wrap a bus with an explicit calibration.
Expand All @@ -227,7 +240,10 @@ pub mod baro {
pub fn init(&mut self) -> Result<(), DriverError> {
let id = self.bus.read_reg(REG_CHIP_ID);
if id != CHIP_ID_VALUE {
return Err(DriverError::WrongIdentity { got: id, want: CHIP_ID_VALUE });
return Err(DriverError::WrongIdentity {
got: id,
want: CHIP_ID_VALUE,
});
}
self.bus.write_reg(REG_PWR_CTRL, PWR_PRESS_TEMP_NORMAL);
Ok(())
Expand Down Expand Up @@ -270,7 +286,11 @@ pub mod baro {

/// Wrap an I2C bus at the default address + default calibration.
pub fn new(i2c: I) -> Self {
Self { i2c, addr: Self::DEFAULT_ADDR, cal: BaroCal::default() }
Self {
i2c,
addr: Self::DEFAULT_ADDR,
cal: BaroCal::default(),
}
}

/// Wrap an I2C bus at an explicit address + calibration.
Expand Down Expand Up @@ -349,13 +369,23 @@ mod tests {
let mut bus = MockBus::new();
bus.set(0x00, 0xAB);
let mut m = Ist8310::new(bus);
assert_eq!(m.init(), Err(DriverError::WrongIdentity { got: 0xAB, want: 0x10 }));
assert_eq!(
m.init(),
Err(DriverError::WrongIdentity {
got: 0xAB,
want: 0x10
})
);
}

#[test]
fn flat_heading_cardinal() {
// field pointing +Y (east) ⇒ heading +π/2.
let h = flat_heading(MagField { x_ut: 0.0, y_ut: 10.0, z_ut: 0.0 });
let h = flat_heading(MagField {
x_ut: 0.0,
y_ut: 10.0,
z_ut: 0.0,
});
assert!((h - core::f32::consts::FRAC_PI_2).abs() < 1e-4);
}

Expand Down Expand Up @@ -383,7 +413,13 @@ mod tests {
let mut bus = MockBus::new();
bus.set(0x00, 0x99);
let mut b = Bmp388::new(bus);
assert_eq!(b.init(), Err(DriverError::WrongIdentity { got: 0x99, want: 0x50 }));
assert_eq!(
b.init(),
Err(DriverError::WrongIdentity {
got: 0x99,
want: 0x50
})
);
}

// ── async hardware path (embedded-hal-async I2c) ─────────────────────────
Expand Down Expand Up @@ -477,9 +513,15 @@ mod tests {
/// The async paths are fallible: an I2C transport error propagates as Err.
#[test]
fn baromag_async_propagates_transport_error() {
let mut mag = Ist8310I2c::new(MockI2c { block: [0; 6], fail: true });
let mut mag = Ist8310I2c::new(MockI2c {
block: [0; 6],
fail: true,
});
assert!(block_on(mag.read_field()).is_err());
let mut baro = Bmp388I2c::new(MockI2c { block: [0; 6], fail: true });
let mut baro = Bmp388I2c::new(MockI2c {
block: [0; 6],
fail: true,
});
assert!(block_on(baro.read()).is_err());
}

Expand Down
13 changes: 9 additions & 4 deletions crates/falcon-core/plain/src/blackbox_backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

use crate::{FlightBackend, ImuSample, NavState};
use relay_iekf::Vec3;
use relay_log::blackbox::{BlackboxWriter, BlockLog, TickRecord, TICK_MAX};
use relay_log::blackbox::{BlackboxWriter, BlockLog, TICK_MAX, TickRecord};

/// Wraps a live backend; call [`LoggingBackend::finish_tick`] after each
/// `FlightCore::step` with the estimator state to seal that tick's record.
Expand Down Expand Up @@ -102,8 +102,10 @@ impl<B: FlightBackend, L: BlockLog> FlightBackend for LoggingBackend<'_, B, L> {
}
fn read_gnss_dual(
&mut self,
) -> Option<(Option<falcon_gnss_ubx::dual::NedFix>, Option<falcon_gnss_ubx::dual::NedFix>)>
{
) -> Option<(
Option<falcon_gnss_ubx::dual::NedFix>,
Option<falcon_gnss_ubx::dual::NedFix>,
)> {
// Forwarded, NOT logged: the TickRecord carries the SELECTED position
// (what the estimator consumed); per-receiver raw lanes are part of
// the schema-v2 slice (#277).
Expand Down Expand Up @@ -160,7 +162,10 @@ impl<'a> ReplayBackend<'a> {
impl FlightBackend for ReplayBackend<'_> {
fn read_imu(&mut self) -> ImuSample {
let t = &self.ticks[self.at.min(self.ticks.len() - 1)];
ImuSample { accel: t.accel, gyro: t.gyro }
ImuSample {
accel: t.accel,
gyro: t.gyro,
}
}
fn read_position(&mut self) -> Option<Vec3> {
self.ticks.get(self.at).and_then(|t| t.pos)
Expand Down
Loading
Loading