From b6ec75e968c3726d5bdd3a894c407419adbaec02 Mon Sep 17 00:00:00 2001 From: leynos Date: Wed, 16 Sep 2026 18:19:51 +0200 Subject: [PATCH 1/2] Fix newly reachable const lint findings Keep the pump state-machine helpers const-safe on Rust 1.85 and retain the byte-exact privacy diagnostic after its signature changes. --- rust/cuprum-native-io/src/fd_ownership_model.rs | 4 ++-- rust/cuprum-streams/src/io_utils/tracing_tests.rs | 2 +- rust/cuprum-streams/src/pump_machine.rs | 4 ++-- .../tests/ui/fail/pump_transition_unreachable.stderr | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/rust/cuprum-native-io/src/fd_ownership_model.rs b/rust/cuprum-native-io/src/fd_ownership_model.rs index 67b2c8359..205f46074 100644 --- a/rust/cuprum-native-io/src/fd_ownership_model.rs +++ b/rust/cuprum-native-io/src/fd_ownership_model.rs @@ -26,8 +26,8 @@ impl CloseLog { } /// Number of closes recorded so far. - pub(crate) fn closes(&self) -> u32 { - self.closes.get() + pub(crate) const fn closes(self) -> u32 { + self.closes.into_inner() } fn record_close(&self) { diff --git a/rust/cuprum-streams/src/io_utils/tracing_tests.rs b/rust/cuprum-streams/src/io_utils/tracing_tests.rs index ee766e08f..bbaa1701d 100644 --- a/rust/cuprum-streams/src/io_utils/tracing_tests.rs +++ b/rust/cuprum-streams/src/io_utils/tracing_tests.rs @@ -79,7 +79,7 @@ fn error_filter_keeps_ordinary_fatal_write_context() { let outcome = write_all_unix_with(b"payload", |_chunk| { Err(io::Error::from(io::ErrorKind::Other)) }); - assert!(outcome.is_err(), "a non-nonfatal write error is fatal",); + assert!(outcome.is_err(), "a non-nonfatal write error is fatal"); }); assert!( diff --git a/rust/cuprum-streams/src/pump_machine.rs b/rust/cuprum-streams/src/pump_machine.rs index 467b2e054..ef9c3f4d4 100644 --- a/rust/cuprum-streams/src/pump_machine.rs +++ b/rust/cuprum-streams/src/pump_machine.rs @@ -164,7 +164,7 @@ pub(crate) fn advance( /// child module and shows the compiler refusing an attempt to build a /// transition and apply it from the parent. Widening either item, even to /// `pub(crate)`, makes that case fail. -fn step(state: &mut PumpState, transition: Transition) -> Flow { +const fn step(state: &mut PumpState, transition: Transition) -> Flow { match transition { Transition::Eof => Flow::Stop, Transition::Drained => Flow::Continue, @@ -175,7 +175,7 @@ fn step(state: &mut PumpState, transition: Transition) -> Flow { } } /// Apply a write outcome to the running total and the `writer_open` latch. -fn apply_write(state: &mut PumpState, write: WriteEvent) { +const fn apply_write(state: &mut PumpState, write: WriteEvent) { match write { WriteEvent::Complete { bytes } => { state.total_written = state.total_written.saturating_add(bytes); diff --git a/rust/cuprum-streams/tests/ui/fail/pump_transition_unreachable.stderr b/rust/cuprum-streams/tests/ui/fail/pump_transition_unreachable.stderr index 3206d48f4..6adb8937d 100644 --- a/rust/cuprum-streams/tests/ui/fail/pump_transition_unreachable.stderr +++ b/rust/cuprum-streams/tests/ui/fail/pump_transition_unreachable.stderr @@ -21,5 +21,5 @@ error[E0603]: function `step` is private note: the function `step` is defined here --> tests/ui/fail/../../../src/pump_machine.rs | - | fn step(state: &mut PumpState, transition: Transition) -> Flow { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | const fn step(state: &mut PumpState, transition: Transition) -> Flow { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ From a10602e5a04edc2e8fff34f065bd182c73eba03d Mon Sep 17 00:00:00 2001 From: leynos Date: Sat, 19 Sep 2026 01:06:54 +0200 Subject: [PATCH 2/2] Document the const accessors in the ownership model CodeRabbit's pre-merge walkthrough withheld the Developer Documentation check because the const work changed a crate-visible API without a guide entry. Record why `CloseLog::closes` consumes its log and why the pump helpers are `const`, so the next reader does not mistake either for an ownership or visibility change. The workspace denies `missing_const_for_fn`, so an accessor with no reason to run at runtime must be `const`. `Cell::get` is not const-stable on the pinned Rust 1.85.0 toolchain, while `Cell::into_inner` is, and reaching it requires taking `self` by value. `CloseLog` stays `pub(crate)` inside a `#[cfg(any(test, kani))]` module and every caller reads the log once as its final use, so the model's unit tests and Kani proofs keep their call sites. `const` on `pump_machine::step` and `apply_write` qualifies how a function may be called, not who may call it, so neither helper widens its visibility and the pump contract is unchanged. The compile-fail case that pins that encapsulation boundary still fails if either item is widened, even to `pub(crate)`; only its quoted definition line moved. --- docs/developers-guide.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/docs/developers-guide.md b/docs/developers-guide.md index c835c689b..9bafd757d 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -2549,6 +2549,34 @@ document. Active verification tracking and the distinction between model evidence and real OS effects lives in [Rust boundary verification](rust-boundary-verification.md) and issue `#89`. +### Const accessors in the test and Kani ownership model + +`CloseLog` in `rust/cuprum-native-io/src/fd_ownership_model.rs` counts modelled +closes for the bounded model, and its accessor is +`const fn closes(self) -> u32`. Both details of that signature follow from the +workspace's Rust 1.85.0 toolchain rather than from an ownership decision. + +The workspace denies `missing_const_for_fn`, so an accessor with no reason to +run at runtime must be `const`. `Cell::get` is not const-stable on 1.85; the +compiler reports that `Cell::::get` is not yet stable as a const fn. +`Cell::into_inner` is const-stable, and it consumes the cell, so reaching it +requires taking `self` by value. The consuming receiver is therefore what keeps +the accessor `const` on that toolchain. It is not a new ownership rule: +`CloseLog` stays `pub(crate)` inside a `#[cfg(any(test, kani))]` module, and +each caller reads the log once as its final use, so the model's unit tests and +`fd_ownership_kani_proofs.rs` keep their existing call sites. This remains an +internal test-and-proof helper rather than a supported API. + +The pump helpers `step` and `apply_write` in +`rust/cuprum-streams/src/pump_machine.rs` take `const fn` for the same lint +reason. `const` qualifies how a function may be called, not who may call it, so +neither helper widens its visibility and the pump contract is unchanged. The +compile-fail case `tests/ui/fail/pump_transition_unreachable.rs` still pins the +encapsulation boundary: it fails if either item is widened, even to +`pub(crate)`. Because the committed `.stderr` fixture quotes the definition +line, the added keyword changed that expectation; the private-function +diagnostic it asserts is the same. + ### Native boundary verification The boundary checks have dedicated Makefile targets so the normal Rust