test: verify conversion arithmetic invariants

[hpmaxi]

Summary

Ref #79

Before the audit, the conversion arithmetic should be checked by more than the example tests written alongside it. Property tests run the real rounding helper over wide ranges and check the wind-down accumulator across rounds.

Changes

• Round trips never create value, in either direction.
• The floor is tight, and conversions are monotonic in amount and price.
• Wind-down payouts never exceed what the accumulator credited, across rounds and claim orders.
• Negative control: ceiling division creates value.

Deviations

• Kani was considered and dropped: on overflow the helper uses the host's I256, which Kani cannot model.

Acceptance criteria

#79 has none by design; this covers the conversion-arithmetic candidate with property tests instead of Kani.

Test plan

Automated tests

1. nix develop -c cargo test -p async-vault — 213 passed.
2. nix develop -c cargo clippy -p async-vault --all-targets -- -D warnings — clean.

Manual verification

None.

Breaking changes

None.

Checklist

• Self-reviewed my own diff
• Tests added or updated
• Docs updated (if applicable)
• No unrelated changes bundled in

Screenshots

None.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
strata-vault-kit-app	Ready	Preview	Sep 25, 2026 3:31pm UTC

[luchobonatti]

The proptests over checked_mul_div_floor are welcome and everything is green. My doubts are the Kani part: --features kani does not build, the harnesses sit inside mod test where cargo kani cannot see them, and they check a hand-written i128 formula rather than the helper. Was it run? Would you also fill in the PR template?

[hpmaxi]

It was not run: Kani is not in the devshell and --features kani did not build. Removed, template filled in.

[luchobonatti]

Kani removed rather than patched, and the reasoning is better than my suggestion. The wind-down property now follows the real accumulator. 213 tests, clippy and fmt clean.