Rust: proptest + Kani state-machine tests for pump_stream_files_readwrite (rust/cuprum-rust/src/lib.rs)

[coderabbitai]

Overview

Add proptest tests (and Kani after refactor) for pump_stream_files_readwrite (rust/cuprum-rust/src/lib.rs, line 209).

Baseline

No Rust-level #[test], proptest, Kani, or Verus coverage currently exists under rust/cuprum-rust.

Justification

The writer-open state latches after non-fatal write errors; fixed tests cover only broad cases. There is no seam for event injection.

Benefit

• Proves total bytes are monotonic
• Proves writes stop after broken pipe
• Proves reader drain continues after writer close
• Proves fatal errors propagate correctly

Cost Trade-Off

Medium-high without seams.

Verifiability Improvement

Extract a pure pump state machine over ReadEvent and WriteEvent to enable scripted verification.

Tool Fit

proptest first; Kani after the pure state-machine seam is added.

Recommended Order

Phase 2 — after event/state seams are extracted.

---

Raised from PR #62 by @leynos.

[coderabbitai]

🔗 Related PRs

leynos/repovec-appliance#23 - Add proptest property tests for Qdrant Quadlet parser and validator (#17) [merged]
leynos/actix-v2a#27 - Add SSE property tests (#18) [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!