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
28 changes: 28 additions & 0 deletions docs/developers-guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -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::<T>::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
Expand Down
4 changes: 2 additions & 2 deletions rust/cuprum-native-io/src/fd_ownership_model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
2 changes: 1 addition & 1 deletion rust/cuprum-streams/src/io_utils/tracing_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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!(
Expand Down
4 changes: 2 additions & 2 deletions rust/cuprum-streams/src/pump_machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ pub(crate) fn advance<E>(
/// 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,
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Loading