Meta: deferred verification & refactor work from the issue audit

[leynos]

Tracking issue for the eight verification/refactor items reconciled during the July 2026 issue audit but deliberately deferred — each is a larger refactor that needs a fresh context to land well rather than being rushed at the tail of the audit session.

The audit itself resolved 22 of 30 issues (9 closed as already-resolved or not-tractable, 12 across the PRs listed under Blocked by below, and #130 updated and kept open). This meta issue coordinates the remainder.

Deferred work

Each item below needs a production seam extracted first, then the tests/proofs the original issue asked for.

• Hypothesis state-machine tests for _PipelineWaitState / _process_completed_task (cuprum/_pipeline_wait.py) #73 — _pipeline_wait: extract a pure, clock-injected transition method (state, completed_idx, exit_code) -> decision, then add a Hypothesis RuleBasedStateMachine proving first-failure-wins, timing-slot population, and correct termination decisions.
• Hypothesis fault-injection tests for _pipeline_streams dispatch/fd lifecycle (cuprum/_pipeline_streams.py) #74 — _pipeline_streams: introduce an FD-state object + context manager for the pause/blocking lifecycle, then Hypothesis fault-injection over FD-extraction / os.set_blocking / rust_pump_stream failure points asserting blocking mode is always restored, plus a property over _surface_unexpected_pipe_failures.
• Property-based tests for _handle_subprocess_timeout and _terminate_pipeline_remaining_stages #75 — _subprocess_timeout._handle_subprocess_timeout and _process_lifecycle._terminate_pipeline_remaining_stages: Hypothesis/CrossHair for timeout-payload consistency across both exception arms, and idempotent cleanup with no double-termination.
• Hypothesis stateful tests for metrics/tracing/logging hooks (cuprum/adapters/metrics_adapter.py) #78 — metrics_adapter + logging_adapter: add stateful machines (counters/histograms and log records created exactly when intended across event sequences). Tracing is already done — mirror cuprum/unittests/test_tracing_span_stateful.py; _LabelRecordingCollector in _adapter_test_support.py is a ready collector seam.
• Rust: proptest + Kani state-machine tests for pump_stream_files_readwrite (rust/cuprum-rust/src/lib.rs) #84 — pump_stream_files_readwrite: extract a pure ReadEvent/WriteEvent state machine (deliberately io::Error-free, so it is Kani-tractable unlike the splice/io paths), then proptest monotonic-total / stop-after-broken-pipe / drain-continues / fatal-propagate, plus a bounded Kani harness.
• Simplify tests/helpers/maturin.py: inline pin-collection logic and remove speculative abstractions #97, Simplify tests/helpers/maturin.py: consolidate 12 functions into 2–3 and defer abstraction until second consumer exists #99 — simplify tests/helpers/maturin.py (394 lines / 12 functions → 2–3): inline the pin-reading logic into test_maturin_build.py and drop the speculative platform-normalisation. Python-only, so no contention with the Rust PRs below.
• Rust: snapshot and integration tests for consume_stream UTF-8 replacement output #105 — Rust-level snapshot tests for consume_stream UTF-8 output (ASCII, multi-byte split across buffers, invalid → U+FFFD, incomplete trailing sequence). The four categories are already oracle-tested on the Python boundary (cuprum/unittests/test_rust_streams.py::TestRustConsumeStream); this adds insta/syrupy snapshots and a Rust-level integration test. Touches lib.rs/lib_tests.rs, which are contended by the landed PRs — stack on the latest.

Why Kani could not close #84's siblings

For context: #86/#87/#88/#89 were closed during the audit because their functions carry std::io::Error (whose bit-packed representation makes CBMC symbolic execution non-terminating) or concern OS file-descriptor state Kani has no model for — their behaviours are exhaustively proptest/runtime-verified instead. #84 is different: its extracted state machine is designed to be io::Error-free, so Kani should apply there.

Blocked by

The landed audit PRs (merge these first; #228 is stacked on #227):

• Pin dev pytest below 9.1 until pytest-bdd supports its fixture API (#208) #222 — pin dev pytest <9.1 (Pin pytest below 9.1 until pytest-bdd supports its fixture-registration API #208)
• Property tests for path/git-ref validators and backend resolver (#70, #72) #224 — property tests for path/git-ref validators and backend resolver (Property-based fuzz tests for safe_path / git_ref validators (cuprum/builders/args.py) #70, Property-based tests for _read_backend_env / get_stream_backend (cuprum/_backend.py) #72)
• Property tests for benchmark comparison and folded ranking reducers (#76, #77) #225 — property tests for benchmark comparison and folded ranking reducers (Property-based tests for benchmark comparison / ratchet reducers (benchmarks/comparison_analysis.py) #76, Deeper property-based tests for folded stack summarisation (benchmarks/summarize_folded.py) #77)
• Direct tests for the Unix write loop, error taxonomy, and stream handle (#85, #104) #227 — direct tests for the Unix write loop, error taxonomy, and stream handle (Rust: proptest tests for handle_write_result / is_nonfatal_write_error (rust/cuprum-rust/src/io_utils.rs) #85, Rust: unit and behavioural tests for read_stream, write_all_unix, StreamHandle, and overflow paths #104)
• Add tracing instrumentation to io_utils read/write loops (#106) #228 — tracing instrumentation for io_utils read/write loops (Rust: add tracing instrumentation to io_utils read_stream and write_all_unix loops #106) (stacked on Direct tests for the Unix write loop, error taxonomy, and stream handle (#85, #104) #227)
• Add buffer-size cap and Python/Rust boundary property tests (#82, #90) #229 — buffer-size cap and Python/Rust boundary property tests (Rust: proptest boundary tests for validate_buffer_size (rust/cuprum-rust/src/lib.rs) #82, Rust: proptest at Python/Rust boundary for rust_pump_stream / rust_consume_stream (rust/cuprum-rust/src/lib.rs) #90)
• Symbolic Kani proofs for UTF-8 decode bounds and unsafe prefix (#80, #81) #230 — symbolic Kani proofs for UTF-8 decode bounds and unsafe prefix (Rust: Kani harness for handle_utf8_error / handle_incomplete_sequence (rust/cuprum-rust/src/utf8.rs) #80, Rust: Kani verification for append_valid_prefix unsafe block (rust/cuprum-rust/src/utf8.rs) #81)

Reference

A full per-issue reconciliation (findings, current-code locations, and implementation notes) was recorded at /tmp/cuprum-audit-progress.md during the audit session.

[coderabbitai]

🔗 Related PRs

#134 - Make _get_stage_stream_fds the canonical pipeline stdio policy (#112) [merged]
#136 - Apply assorted consistency and dead-code cleanups (#129) [merged]
#144 - Fix Command-Query Separation violations (#118) [merged]
#153 - Share one canonical stream-drain loop across consume variants (#115) [merged]
#160 - Unify the splice loop and fix drain_reader EINTR handling (#124) [merged]

---

📝 Issue Planner

_{Check the box below or use the @coderabbitai plan command to generate an implementation plan and prompts that you can use with your favorite coding assistant.}

• Create Plan

---

🧪 Issue enrichment is currently in open beta.

You can configure auto-planning by selecting labels in the issue_enrichment configuration.

To disable automatic issue enrichment, add the following to your .coderabbit.yaml:

issue_enrichment:
  auto_enrich:
    enabled: false

💬 Have feedback or questions? Drop into our discord!