[jdjioe5-cpu]

Closes #27

What and why

Extends \contracts/kinlock/tests/properties.rs:check_invariants()\ so that Invariants 5, 6, and 8 are asserted directly after every step in the property testing harness, rather than being checked only through operation gates. Proves through deliberate fault mutations that each new assertion catches broken contract gates with explicit diagnostics, while leaving \src/\ completely untouched.

Changes

• \contracts/kinlock/tests/properties.rs:
  • Added direct assertion for Invariant 5 in \check_invariants(): loops over all locks; for non-Open locks or illegal tranches (unreleased with
    ow < t.unlock_at,
    ow >= lock.expires_at, \ .released, or payee not \Active), calling \ ry_release\ is asserted to return \Err.
  • Added direct assertion for Invariant 6 in \check_invariants(): for non-Open locks or locks where !refund_allowed(lock.id)\ (
    ow < lock.expires_at, payee != \Revoked, payee not \Suspended\ past 14-day grace), calling \ ry_refund\ is asserted to return \Err.
  • Added direct assertion for Invariant 8 in \check_invariants(): when \lock.state == LockState::Open, temporarily enables \paused_new_locks\ and asserts that pause never causes \ ry_release\ or \ ry_refund\ on existing locks to fail with \Error::PausedNewLocks, then immediately restores pause state.
  • Documented \M1-38\ and direct assertions in module-level doc comments.
• \README.md: Clarified property test suite coverage accurately (invariants 1–9 asserted directly in \check_invariants(), invariant 10 asserted across each operation failure).
• \ROADMAP.md: Updated \M1-38\ from \TODO\ to \DONE, updated Section 3 Progress snapshot, updated \Last updated\ date to 2026-10-17, and added Section 17 Changelog entry.

Hard rules / invariants touched

5, 6, 8 (from \ARCHITECTURE.md\ §4.6)

Tests

1. Verification commands executed locally:

• \cargo fmt --all -- --check: Exit code 0 (clean).
• \cargo clippy --all-targets -- -D warnings: Exit code 0 (clean, 0 warnings).
• \stellar contract build: Exit code 0 (\ arget\wasm32v1-none\release\kinlock.wasm, 23,780 bytes, hash: \5a8c6b230ab2c5a8c977e8a0b0a478d067a76f1ea58a9d80f1b739900c895558).
• \cargo test --workspace: Exit code 0.
  • 107/107 unit tests passed (\inished in 0.47s).
  • \ ests/properties.rs\ passed 64 proptest cases (\inished in 66.75s).
  • \ ests/budget.rs\ and \ ests/integration.rs\ passed.

2. Deliberate Mutation Proofs (Demonstration that assertions catch broken gates):

1. Invariant 5: Commented out \if now < tranche.unlock_at { return Err(Error::TrancheNotUnlocked); }\ in \src/vault.rs:release.
   • Result: caught immediately at first step:
     \Test failed: invariant 5 violated: release(1, 1) succeeded when illegal at now=1000000 (unlock_at=1086400, expires_at=1864000, released=false, payee_status=Active) at contracts\kinlock\tests\properties.rs:778.\
2. Invariant 6: Changed \match payee.status\ in \src/vault.rs:refund\ to allow active payees before expiry.
   • Result: caught immediately:
     \Test failed: invariant 6 violated: refund(1) succeeded when illegal at now=1000000 (expires_at=1864000, payee_status=Active) at contracts\kinlock\tests\properties.rs:804.\
3. Invariant 8: Injected \if cfg.paused_new_locks { return Err(Error::PausedNewLocks); }\ into \src/vault.rs:release.
   • Result: caught immediately:
     \Test failed: assertion failed: (left != right) left: PausedNewLocks, right: PausedNewLocks: invariant 8 violated: pause blocked release for lock 1 at contracts\kinlock\tests\properties.rs:828.\

All mutations were reverted; \git diff --stat contracts/kinlock/src/\ is completely empty.

Docs / ADR

\README.md\ and \ROADMAP.md\ updated.

Roadmap

\M1-38\ marked \DONE. Changelog entry added: yes.

Assumptions and open questions

None.