test(contract): add fuzz invariants for vesting and supply accounting

[arisu6804]

Problem

Large combinations of timestamps, rates, top-ups, cancellations, and withdrawals are not covered by examples.

Objective

Deliver a production-quality improvement to vesting and supply property suite that creates measurable value for correctness, security, reliability, performance, or maintainability.

Implementation scope

• Generate valid lifecycle sequences; assert monotonic vesting, no over-withdrawal, cap conservation, and safe invalid input rejection.

Acceptance criteria

• Fuzz failures include reproducible seeds; all mutation paths participate; no invariant is disabled to pass.

Required validation

• Deterministic fuzz runs and minimized regression fixtures.
• Existing tests and CI remain passing.
• Add regression coverage for the original failure mode.
• Do not weaken, delete, or skip unrelated tests to obtain a green build.

PR quality bar

• Keep the PR focused and explain design tradeoffs, compatibility impact, and test evidence.
• Avoid typo-only, documentation-only, cosmetic-only, or unrelated refactor submissions.

Out of scope

• Broad rewrites not required by the acceptance criteria.
• Changes to unrelated services, contracts, or user flows.

[leocagli]

Hi, I would like to take this one.

I am Leo Cagliero, from the Starmaker program, working on Cosmos LATAM and Open Stellar.

Why this one specifically: I just delivered four property-test PRs to another Soroban vault contract, all four green on CI, and they cover the same shape of problem you describe here:

• Disciplr-Contracts#417: amount boundary properties. The part worth mentioning is that the existing suite asserted result.is_err(), which cannot tell a bounds rejection apart from an insufficient-balance failure. A regression that widened the bounds would have stayed green. I made the tests mint generously on purpose and assert the exact typed error, plus a dedicated test that pins that the two failure reasons stay distinguishable.
• Disciplr-Contracts#416: multi-vault isolation, opening several vaults with deliberately different amounts so that any cross-contamination shows up as a wrong number instead of passing by coincidence, and asserting the contract holds exactly the escrow still open.
• #414 and #415: a security guard and negative authorization coverage.

How I would approach yours. The four invariants you list (monotonic vesting, no over-withdrawal, cap conservation, safe rejection of invalid input) are the right set, and I would generate lifecycle sequences rather than isolated calls, since the bugs live in the ordering: top-up after partial withdrawal, cancel between two withdrawals, withdrawal at the exact cliff timestamp.

Two things I would want to pin down with you:

1. Determinism. You ask for reproducible seeds. Proptest writes failures to a regression file that has to be committed, otherwise the "minimized regression fixtures" you ask for do not survive. I would commit that file and say so in the PR.
2. Time. Vesting properties depend on the ledger timestamp, so the generator has to produce timestamp sequences, not just amounts. The monotonicity invariant only means something if time can move in the awkward ways: same timestamp twice, a jump past the whole schedule, a withdrawal at exactly the boundary second.

I would also add one invariant you do not list, if you want it: that the sum of everything withdrawn plus everything still locked equals everything ever deposited, checked after every mutation and not only at the end. That is the one that catches accounting drift rather than a single wrong call.

Happy to answer anything before you assign.