Rust: pure pump state machine with proptest + Kani (#84) - #242
Open
leynos wants to merge 4 commits into
Open
Conversation
pump_stream_files_readwrite drove real descriptor I/O and inlined its own byte-total accounting and writer_open latch, with no seam for scripted verification (issue #84). Extract that control flow into a pure, io::Error-free state machine in src/pump_machine.rs: step advances a PumpState given a ReadEvent (Chunk/Eof) and, when a write is performed, a WriteEvent (Complete / Closed). pump_stream_files_readwrite now drives the machine, translating real I/O into events via a new classify_write helper and propagating fatal PumpErrors out of band so they never reach the machine. The now-redundant io_utils::handle_write_result is removed (its coverage moves to classify_write tests plus the machine's property tests). Verification: - proptest folds random event scripts through step, asserting the total is monotonic, the writer never reopens once a broken pipe latches it closed, a closed writer drains without accruing bytes, and the loop stops exactly on Eof. - Kani proves the same invariants over unbounded byte counts and arbitrary starting states (src/pump_machine_kani_proofs.rs, #[cfg(kani)], outside the commit gate): 6/6 harnesses VERIFICATION SUCCESSFUL. Existing pump/consume tests are unchanged and still pass, confirming the refactor preserves behaviour. Documents the machine in the developers guide. Closes #84 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
Reviewer's GuideExtracts the read/write pump loop control flow into a pure state machine ( Sequence diagram for pump_stream_files_readwrite driving the pure pump_machinesequenceDiagram
participant PumpLoop as pump_stream_files_readwrite
participant Reader as Reader
participant Writer as Writer
participant IOUtils as io_utils
participant PumpState as PumpState
participant Machine as pump_machine
PumpLoop->>PumpState: start()
loop each_iteration
PumpLoop->>IOUtils: read_stream(reader, buffer)
IOUtils-->>PumpLoop: read_len
alt read_len == 0
PumpLoop->>Machine: step(state, ReadEvent::Eof, None)
Machine-->>PumpLoop: Flow::Stop
PumpLoop-->>PumpLoop: break loop
else read_len > 0
PumpLoop-->>PumpLoop: read = ReadEvent::Chunk
alt state.writer_open()
PumpLoop->>Writer: classify_write(writer, chunk)
Writer->>IOUtils: handle_write(writer, chunk)
IOUtils-->>Writer: WriteOutcome
Writer-->>PumpLoop: WriteEvent
PumpLoop->>Machine: step(state, ReadEvent::Chunk, Some(WriteEvent))
Machine-->>PumpLoop: Flow::Continue
else writer_closed
PumpLoop->>Machine: step(state, ReadEvent::Chunk, None)
Machine-->>PumpLoop: Flow::Continue
end
end
end
PumpLoop->>PumpState: total_written()
PumpState-->>PumpLoop: total_bytes
PumpLoop-->>PumpLoop: record tracing and return total_bytes
File-Level Changes
Assessment against linked issues
Possibly linked issues
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
WalkthroughThe fallback read/write path now uses a pure event-driven state machine. Descriptor outcomes are classified into events, the pump tracks writer closure and bytes written, and proptest, Kani, integration tests, and developer documentation cover the resulting behaviour. ChangesRead/write fallback pump
Sequence Diagram(s)sequenceDiagram
participant Reader
participant pump_stream_files_readwrite
participant classify_write
participant pump_machine
Reader->>pump_stream_files_readwrite: read chunk or EOF
pump_stream_files_readwrite->>classify_write: classify chunk write
classify_write-->>pump_stream_files_readwrite: WriteEvent or PumpError
pump_stream_files_readwrite->>pump_machine: step with read and write events
pump_machine-->>pump_stream_files_readwrite: updated state and Flow
Possibly related PRs
Suggested labels: Suggested reviewers: Poem
Caution Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional.
❌ Failed checks (1 error, 1 warning)
✅ Passed checks (18 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![codescene-access[bot]](https://avatars.githubusercontent.com/in/3755875?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 35c23b6c79
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
CodeScene flagged broken_pipe_latches_closed_and_counts_accepted_bytes and completed_write_keeps_open_and_counts_bytes as structurally similar. Fold them into write_counts_bytes_and_latches_by_variant, which drives an arbitrary WriteEvent and proves both invariants at once: either outcome counts its accepted bytes, and only a completed write keeps the writer open. Kani still verifies (5/5 harnesses SUCCESSFUL); code health 10.0. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Two review findings on the pump state machine: - lib.rs had grown to 402 lines, over the 400-line maximum in AGENTS.md. Move classify_write into io_utils, which already owns handle_write, WriteOutcome, and the non-fatal error partition it collapses, so the write boundary's final step sits with the rest of that boundary. lib.rs drops to 388 lines; io_utils/mod.rs (335) and pump_machine.rs (242) stay well inside the cap. - AGENTS.md requires function documentation to demonstrate usage and outcome. Add worked examples to pump_machine::step (a completed write, then a broken pipe latching closed, draining, and stopping on EOF) and to classify_write (complete versus latched-closed after the reader hangs up). Behaviour is unchanged: nextest 59/59 and Kani 5/5 harnesses still pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Owner
Author
|
@coderabbitai Has this now been resolved in the latest commit? Please use codegraph analysis to determine your answer. If this comment is now resolved, please mark it as such using the API. Otherwise, please provide an AI agent prompt for the remaining work to be done to address this comment. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo '=== PR head and changed files ==='
gh pr view 242 --repo leynos/cuprum --json headRefName,headRefOid,files --jq '{headRefName, headRefOid, files: [.files[].path]}'
echo '=== Relevant Rust file map ==='
fd -t f -e rs . rust/cuprum-rust | sort
echo '=== Symbol outlines ==='
for f in rust/cuprum-rust/src/lib.rs rust/cuprum-rust/src/lib_tests.rs rust/cuprum-rust/src/pump_machine.rs; do
if [ -f "$f" ]; then
echo "--- $f ---"
ast-grep outline "$f" --items all || true
fi
done
echo '=== State-machine and classification references ==='
rg -n -C 5 -P '\b(step|drive|drive_step|classify_write|ReadEvent|WriteEvent|WriteOutcome|PumpState)\b' \
rust/cuprum-rust/src/lib.rs \
rust/cuprum-rust/src/lib_tests.rs \
rust/cuprum-rust/src/pump_machine.rs 2>/dev/null || true
echo '=== CodeRabbit review threads ==='
gh api graphql -F owner=leynos -F name=cuprum -F number=242 -f query='
query($owner: String!, $name: String!, $number: Int!) {
repository(owner: $owner, name: $name) {
pullRequest(number: $number) {
reviewThreads(first: 100) {
nodes {
id
isResolved
path
line
comments(first: 20) {
nodes { author { login } body url }
}
}
}
}
}
}' --jq '.data.repository.pullRequest.reviewThreads.nodes[]
| select(any(.comments.nodes[]?; .author.login == "coderabbitai"))
| {id,isResolved,path,line,comments:[.comments.nodes[] | {author:.author.login,body,url}]}'Length of output: 56356 🏁 Script executed: #!/bin/bash
set -euo pipefail
echo '=== io_utils structure and relevant test symbols ==='
ast-grep outline rust/cuprum-rust/src/io_utils/mod.rs --items all
ast-grep outline rust/cuprum-rust/src/io_utils/tests.rs --items all
echo '=== All direct classify_write calls and tests ==='
rg -n -C 8 -P '\bclassify_write\s*\(' rust/cuprum-rust/src
echo '=== Non-fatal write fixtures and assertions ==='
rg -n -C 8 -P '(NonFatalShortWrite|BrokenPipe|ConnectionReset|WriteEvent::Closed|map_short_write_error|write_all_.*_with)' \
rust/cuprum-rust/src/io_utils rust/cuprum-rust/src/lib_tests.rs
echo '=== Production callers of state transition APIs ==='
rg -n -C 5 -P '\b(step|drive_step|drive)\s*\(' rust/cuprum-rust/src \
-g '!rust/cuprum-rust/src/pump_machine_kani_proofs.rs'
echo '=== Exact matching CodeRabbit review threads ==='
gh api graphql -F owner=leynos -F name=cuprum -F number=242 -f query='
query($owner: String!, $name: String!, $number: Int!) {
repository(owner: $owner, name: $name) {
pullRequest(number: $number) {
reviewThreads(first: 100) {
nodes {
id isResolved path line
comments(first: 30) { nodes { author { login } body url } }
}
}
}
}
}' --jq '
.data.repository.pullRequest.reviewThreads.nodes[]
| select(any(.comments.nodes[]?;
.author.login == "coderabbitai"
and (
(.body | contains("non-fatal short write"))
or (.body | contains("construction of `ReadEvent`/`WriteEvent`"))
or (.body | contains("contract that `step` should only receive"))
)
))
| {id,isResolved,path,line,comments:[.comments.nodes[] | {author:.author.login,body,url}]}'Length of output: 47595
Use this AI agent prompt: |
Collaborator
|
@coderabbitai review |
✅ Action performedReview finished.
|
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@rust/cuprum-rust/src/io_utils/mod.rs`:
- Line 12: Update write_all_unix_with to remove the unreachable Err(err) if
err.is_nonfatal_write() branch, since these errors are already converted to
WriteOutcome::NonFatalShortWrite. Add coverage for the
Ok(WriteOutcome::NonFatalShortWrite) handling path in both zero-byte and
positive-byte scenarios.
In `@rust/cuprum-rust/src/lib_tests.rs`:
- Around line 187-211: Add direct tests for the non-fatal short-write branch of
classify_write, covering WriteEvent::Closed with both zero and positive accepted
byte counts. Construct a writer or pipe scenario that causes a short write, then
assert the returned Closed event preserves the accepted byte count, while
keeping the existing Complete and fatal PumpError::Io coverage unchanged.
In `@rust/cuprum-rust/src/lib.rs`:
- Around line 296-323: Replace the manual read/write event construction in the
loop with the production drive_step-style helper exported from pump_machine.
Move ownership of the “write only for chunks while the writer is open”
precondition into that helper, and update the test-only drive helper to reuse it
so runtime and property-test behavior share the same path.
In `@rust/cuprum-rust/src/pump_machine.rs`:
- Around line 120-133: Extract a production drive_step API near step that
encodes the valid write-transition precondition, invoking the supplied write
operation only for an open writer receiving ReadEvent::Chunk and rejecting or
preventing writes for EOF or a latched-closed writer. Update
pump_stream_files_readwrite and the test drive helper to use drive_step, so
invariants_hold_across_iterations and writes_stop_after_broken_pipe exercise the
same transition contract instead of reimplementing it.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 7bf48634-692d-4d27-83e0-655f53e188fc
📒 Files selected for processing (7)
docs/developers-guide.mdrust/cuprum-rust/src/io_utils/mod.rsrust/cuprum-rust/src/io_utils/tests.rsrust/cuprum-rust/src/lib.rsrust/cuprum-rust/src/lib_tests.rsrust/cuprum-rust/src/pump_machine.rsrust/cuprum-rust/src/pump_machine_kani_proofs.rs
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
leynos/shared-actions(auto-detected)leynos/pylint-pypy-shim(auto-detected)leynos/whitaker(auto-detected)
| use std::io; | ||
|
|
||
| use crate::errors::PumpError; | ||
| use crate::pump_machine::WriteEvent; |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
rg -n -A 15 'fn write_all_unix\b' rust/cuprum-rust/src/io_utils/mod.rs
rg -n -A 10 'fn handle_write\b' rust/cuprum-rust/src/io_utils/mod.rs
rg -n 'is_nonfatal_write|map_short_write_error' rust/cuprum-rust/src/io_utils/mod.rsRepository: leynos/cuprum
Length of output: 1540
🏁 Script executed:
#!/bin/bash
sed -n '110,210p' rust/cuprum-rust/src/io_utils/mod.rs
printf '\n---\n'
sed -n '235,340p' rust/cuprum-rust/src/io_utils/mod.rs
printf '\n---\n'
rg -n -A 6 -B 6 'WriteEvent::Closed|NonFatalShortWrite|is_nonfatal_write|map_short_write_error' rust/cuprum-rust/src/io_utils/mod.rsRepository: leynos/cuprum
Length of output: 10447
🏁 Script executed:
#!/bin/bash
rg -n -A 8 -B 8 'fn (write_all_unix_with|write_all_windows|classify_write|handle_write)\b' rust/cuprum-rust/src/io_utils/mod.rs
printf '\n--- TESTS ---\n'
rg -n -A 6 -B 6 'short write|BrokenPipe|ConnectionReset|WriteEvent::Closed|NonFatalShortWrite' rust/cuprum-rust/src/io_utils/mod.rsRepository: leynos/cuprum
Length of output: 5499
🏁 Script executed:
#!/bin/bash
sed -n '235,335p' rust/cuprum-rust/src/io_utils/mod.rsRepository: leynos/cuprum
Length of output: 3710
Remove the dead non-fatal Err branch and add NonFatalShortWrite coverage rust/cuprum-rust/src/io_utils/mod.rs:158-162
write_all_unix_with already folds broken-pipe and connection-reset errors into WriteOutcome::NonFatalShortWrite, so Err(err) if err.is_nonfatal_write() never fires here. Delete that branch, and add tests for the Ok(WriteOutcome::NonFatalShortWrite) arm with both zero-byte and positive-byte cases.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@rust/cuprum-rust/src/io_utils/mod.rs` at line 12, Update write_all_unix_with
to remove the unreachable Err(err) if err.is_nonfatal_write() branch, since
these errors are already converted to WriteOutcome::NonFatalShortWrite. Add
coverage for the Ok(WriteOutcome::NonFatalShortWrite) handling path in both
zero-byte and positive-byte scenarios.
Comment on lines
+187
to
+211
| #[rstest] | ||
| fn classify_write_reports_a_completed_write() { | ||
| let (read_end, mut write_end) = make_pipe(); | ||
|
|
||
| let event = match classify_write(&mut write_end, b"chunk") { | ||
| Ok(event) => event, | ||
| Err(err) => panic!("write to an open pipe failed: {err:?}"), | ||
| }; | ||
|
|
||
| assert_eq!(event, WriteEvent::Complete { bytes: 5 }); | ||
| // Keep the read end open until after the write so the pipe never breaks. | ||
| drop(read_end); | ||
| } | ||
|
|
||
| #[rstest] | ||
| fn classify_write_propagates_a_fatal_error() { | ||
| // Writing to the read end of a pipe is a fatal `EBADF`, which must | ||
| // propagate rather than latch the writer closed. | ||
| let (mut read_end, _write_end) = make_pipe(); | ||
|
|
||
| match classify_write(&mut read_end, b"chunk") { | ||
| Ok(event) => panic!("expected a fatal write error, got {event:?}"), | ||
| Err(err) => assert!(matches!(err, PumpError::Io(_))), | ||
| } | ||
| } |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟠 Major | 🏗️ Heavy lift
Add the missing WriteEvent::Closed coverage for classify_write.
Both new tests are sound, but they only exercise Complete and the fatal Err path — the non-fatal short-write outcome (WriteEvent::Closed, zero and positive accepted bytes) still has no direct test, which is exactly the gap the PR calls out as unresolved. See the io_utils/mod.rs comment on classify_write for the branch these tests should target.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@rust/cuprum-rust/src/lib_tests.rs` around lines 187 - 211, Add direct tests
for the non-fatal short-write branch of classify_write, covering
WriteEvent::Closed with both zero and positive accepted byte counts. Construct a
writer or pipe scenario that causes a short write, then assert the returned
Closed event preserves the accepted byte count, while keeping the existing
Complete and fatal PumpError::Io coverage unchanged.
Comment on lines
+296
to
+323
| let mut state = PumpState::start(); | ||
|
|
||
| loop { | ||
| let read_len = read_stream(reader, &mut buffer)?; | ||
| if read_len == 0 { | ||
| let read = if read_len == 0 { | ||
| ReadEvent::Eof | ||
| } else { | ||
| ReadEvent::Chunk | ||
| }; | ||
|
|
||
| // Write only when a chunk arrives while the writer is open; a closed | ||
| // writer just drains the reader. Fatal writes propagate the real error | ||
| // and never reach the pure state machine. | ||
| let write = if read == ReadEvent::Chunk && state.writer_open() { | ||
| let chunk = buffer | ||
| .get(..read_len) | ||
| .ok_or(PumpError::BufferRangeExceeded)?; | ||
| Some(classify_write(writer, chunk)?) | ||
| } else { | ||
| None | ||
| }; | ||
|
|
||
| if step(&mut state, read, write) == Flow::Stop { | ||
| break; | ||
| } | ||
| if !writer_open { | ||
| continue; | ||
| } | ||
|
|
||
| let chunk = buffer | ||
| .get(..read_len) | ||
| .ok_or(PumpError::BufferRangeExceeded)?; | ||
|
|
||
| writer_open = handle_write_result(writer, chunk, &mut total_written)?; | ||
| } | ||
|
|
||
| let total_written = state.total_written(); |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟠 Major | 🏗️ Heavy lift
Loop hand-constructs pump events instead of calling a production driving helper.
This mirrors the gap flagged in pump_machine.rs: the "write iff ReadEvent::Chunk and the writer is open" rule (line 309) is duplicated here and in the pump module's test-only drive helper, rather than owned by one production entry point. Route this loop through a drive_step-style helper exported from pump_machine so the precondition lives in a single place and both runtime code and property tests exercise it identically.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@rust/cuprum-rust/src/lib.rs` around lines 296 - 323, Replace the manual
read/write event construction in the loop with the production drive_step-style
helper exported from pump_machine. Move ownership of the “write only for chunks
while the writer is open” precondition into that helper, and update the
test-only drive helper to reuse it so runtime and property-test behavior share
the same path.
Comment on lines
+120
to
+133
| pub(crate) fn step(state: &mut PumpState, read: ReadEvent, write: Option<WriteEvent>) -> Flow { | ||
| match read { | ||
| ReadEvent::Eof => Flow::Stop, | ||
| ReadEvent::Chunk => { | ||
| if state.writer_open { | ||
| if let Some(event) = write { | ||
| apply_write(state, event); | ||
| } | ||
| } | ||
| // A closed writer drains the reader: the state is left unchanged. | ||
| Flow::Continue | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟠 Major | 🏗️ Heavy lift
Narrow step's precondition instead of proving around it.
step accepts write: Option<WriteEvent> unconditionally but only honours it when read == ReadEvent::Chunk && state.writer_open; feed it Some(write) alongside ReadEvent::Eof, or while the writer has already latched closed, and it silently drops the value instead of rejecting the call. The Kani proofs (closed_writer_drains_without_writing, loop_stops_exactly_on_eof) only confirm that misuse is currently harmless — they don't stop a future caller from constructing an invalid combination undetected.
The test module compounds this: drive (lines 158-161) re-implements the "write iff an open Chunk" rule as a test-only wrapper rather than routing through a production API that encodes it, so invariants_hold_across_iterations and writes_stop_after_broken_pipe never exercise the real transition contract that pump_stream_files_readwrite relies on.
Extract a production drive_step here that owns the rule (e.g. taking a closure that only runs — and only may run — when a write is warranted) so the fallback loop in rust/cuprum-rust/src/lib.rs and the property tests both drive the machine through the same narrowed entry point.
Also applies to: 158-161
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@rust/cuprum-rust/src/pump_machine.rs` around lines 120 - 133, Extract a
production drive_step API near step that encodes the valid write-transition
precondition, invoking the supplied write operation only for an open writer
receiving ReadEvent::Chunk and rejecting or preventing writes for EOF or a
latched-closed writer. Update pump_stream_files_readwrite and the test drive
helper to use drive_step, so invariants_hold_across_iterations and
writes_stop_after_broken_pipe exercise the same transition contract instead of
reimplementing it.
Four review findings, all valid in substance. classify_write carried an Err(err) if err.is_nonfatal_write() arm that cannot be reached: map_short_write_error already converts broken-pipe and connection-reset failures into Ok(WriteOutcome::NonFatalShortWrite), and every other error escaping handle_write — WriteZero, LengthOverflow, BufferRangeExceeded, and the fatal partition — reports false from is_nonfatal_write. Remove it, and split the pure mapping into classify_write_outcome so the NonFatalShortWrite path can be covered for both a zero and a positive accepted byte count without contriving a partial write against a real descriptor. The finding placed this in write_all_unix_with, which has no such arm; the substance applies to classify_write. The write precondition — a chunk read while the writer is still open — was written out twice, once in the pump loop and once in the property tests' drive helper, so the properties exercised their own copy rather than the production path. Add drive_step next to step, which owns that precondition and invokes the supplied write only when the transition permits one; both the loop and the tests now go through it. That extraction needed its own coverage, and finding it took a mutation check: step independently ignores a write it is handed, so a drive_step that dropped the precondition leaves the resulting state identical and differs only in performing a spurious write. The first mutation therefore survived. The tests now assert whether the write operation ran rather than only its effect — three focused cases plus an invocation clause folded into the main property — and both mutations (dropping the writer_open guard, and writing on EOF) now fail. Kani still verifies 5/5 harnesses, nextest is 66/66, and the developers guide records why the invocation is what must be asserted. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Collaborator
|
All four findings fixed in 5c65637. All were valid in substance; one was mis-anchored, and one turned out to need more than it asked for. 1. The unreachable non-fatal
|
| Command | Outcome |
|---|---|
cargo nextest run |
66/66 passed (was 59) |
cargo kani (5 harnesses) |
5/5 VERIFICATION:- SUCCESSFUL |
make check-fmt |
pass |
make lint |
pass (clippy -D warnings, cargo doc -D warnings, ruff, interrogate, pylint) |
make typecheck |
pass |
make test |
pass — full Python suite plus nextest 66/66 |
make markdownlint / make nixie |
pass |
lib.rs is 387 lines, still inside the 400-line cap. The developers guide now records why the invocation is the thing to assert, so the next person changing drive_step does not have to rediscover it by mutation.
There was a problem hiding this comment.
Gates Failed
(1 new file with code health below 10.00)
(1 file with Code Duplication)
Our agent can fix these. Install it.
Gates Passed
Reason for failure
| New code is healthy | Violations | Code Health Impact | |
|---|---|---|---|
| pump_machine.rs | 1 rule | 9.39 | Suppress |
| Enforce advisory code health rules | Violations | Code Health Impact | |
|---|---|---|---|
| pump_machine.rs | 1 advisory rule | 9.39 | Suppress |
Quality Gate Profile: Pay Down Tech Debt
Install CodeScene MCP: safeguard and uplift AI-generated code. Catch issues early with our IDE extension and CLI tool.
Comment on lines
+213
to
+225
| fn drive_step_skips_the_write_at_eof() { | ||
| let mut state = PumpState::start(); | ||
|
|
||
| let (flow, invoked) = drive_counting( | ||
| &mut state, | ||
| ReadEvent::Eof, | ||
| WriteEvent::Complete { bytes: 4 }, | ||
| ); | ||
|
|
||
| assert_eq!(flow, Flow::Stop); | ||
| assert!(!invoked, "EOF must not attempt a write"); | ||
| assert_eq!(state.total_written(), 0, "EOF must accrue no bytes"); | ||
| } |
There was a problem hiding this comment.
❌ New issue: Code Duplication
The module contains 2 functions with similar structure: tests.drive_step_performs_the_write_for_a_chunk_while_open,tests.drive_step_skips_the_write_at_eof
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
pump_stream_files_readwritedrove real descriptor I/O and inlined its own byte-total accounting andwriter_openlatch, with no seam for scripted verification. This extracts that control flow into a pure,io::Error-free state machine and verifies it with proptest and Kani, as #84 requested.Design
src/pump_machine.rs(pure — no descriptors, noio::Error):ReadEvent—Chunk/EofWriteEvent—Complete { bytes }/Closed { bytes }(the non-fatal broken-pipe latch)PumpState { total_written, writer_open }step(&mut PumpState, ReadEvent, Option<WriteEvent>) -> Flowpump_stream_files_readwritenow drives the machine: it translates real I/O into events via a newclassify_writehelper and propagates fatalPumpErrors out of band, so they never reach the machine. The now-redundantio_utils::handle_write_resultis removed; its coverage moves to twoclassify_writetests plus the machine's property tests.Verification (all four #84 goals)
proptest (
cargo nextest) folds random event scripts throughstep:EofKani (
src/pump_machine_kani_proofs.rs,#[cfg(kani)]— outside the commit gate) proves the same invariants over unbounded byte counts and arbitrary starting states, plus fatal-write accounting:Fatal-error propagation (the fourth goal) is realised by the loop's early
?return and covered byclassify_write_propagates_a_fatal_errorand the existingio_utilswrite tests.Behaviour preserved
Every existing pump/consume test is unchanged and still passes — the refactor is behaviour-preserving, only relocating the decision logic behind a verifiable seam.
Validation
Full gates green:
make check-fmt,make lint(clippy-D warnings, interrogate 100%, pylint 10.00/10),make test(pytest 755 passed/47 skipped; Rust nextest 59/59),make markdownlint,make nixie. Kani verified separately: 6/6 harnesses SUCCESSFUL.Closes #84
🤖 Generated with Claude Code
Summary by Sourcery
Extract the read/write pump loop control flow into a pure state machine and drive it from the existing I/O-based pump implementation, with property-based and model-checking verification.
Enhancements:
Documentation:
Tests: