Tier-S: #43 sub — property-correspondence tests (15 → 100, +85)

[hyperpolymath]

Scope (sub-issue of #43)

Expand property-correspondence tests from 15 → 100 (+85).

Each new test mirrors one Lean theorem in FilesystemModel.lean / FileOperations.lean / Composition.lean / CrashConsistency.lean and uses proptest's strategy generators to drive the Rust impl through the same state diagram.

Current state

tests/property_correspondence_tests.rs has 15 tests. The next 85 should cover:

Tier	Count	Source
Operations (mkdir/rmdir/touch/rm)	20	FilesystemModel.lean
Content (read/write/append)	20	FileContentOperations.lean
Composition (sequences/reversibility)	25	Composition.lean
Crash consistency	20	CrashConsistency.lean + #62

Resolution

1. PR per Lean module (~4 PRs).
2. Each test has a docstring // Mirrors Lean theorem: <name> for grep-ability.
3. Don't introduce new proptest! macros without #[allow(unused_doc_comments)] blocks on /// headers (PR fix(clippy): clear 86 errors under -D warnings across impl/rust-cli/ #74 lesson).

References

• Parent: Test + bench dramatic expansion — 736 → 2000+ tests, 3 → 15 benches, 7 → 20 fuzz targets #43
• Mirror-PR pattern: PR feat(rust-cli): secure_delete + audit_log real impls + typed-error refactor + 15-25 prop-tests #72 added 20 prop-correspondence tests; same shape