test(contract): add fuzz invariants for escrow, expiry, and balance accounting

[arisu6804]

Problem

Example tests do not cover combinations of expiry, refunds, partial settlement, and large amounts.

Objective

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

Implementation scope

• Generate lifecycle sequences and assert escrow conservation, monotonic status, safe expiry, and checked arithmetic.

Acceptance criteria

• Fuzz failures are reproducible; all lifecycle paths participate; invariants remain enabled in CI.

Required validation

• Deterministic fuzz tests 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 as well. I already applied to #190, and I want to be explicit that these two are the same job seen from both sides: #190 defines the conservation invariant, this one proves it holds under generated sequences. If you would rather give them to different people that is fine, but they are cheaper together than apart, because the property suite is what tells you the centralized accounting actually covers every path.

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

Direct evidence: I shipped four property-test PRs to another Soroban contract this week, all green:

• Disciplr-Contracts#416: isolation across several escrows driven to different terminal states, asserting the contract holds exactly the escrow still open and nothing more. That is your conservation invariant, written as a test.
• Disciplr-Contracts#417: boundary properties, where the notable part is that the previous suite asserted is_err() and therefore could not distinguish a bounds rejection from an insufficient-balance failure. A regression widening the bounds would have stayed green.
• #414 and #415: a security guard and negative authorization coverage using scoped mock_auths instead of mock_all_auths, since the latter authorizes everybody and can never observe a rejection.

On your acceptance criteria, two notes:

"Fuzz failures include reproducible seeds" means the proptest regression file has to be committed, not just generated. Otherwise the minimized fixtures you ask for die with the CI runner. I would commit it and say so in the PR.

"All mutation paths participate" is the part that decides whether this suite is worth anything. Generating isolated calls finds almost nothing; the bugs live in ordering. For escrow and expiry that means sequences like refund after partial release, expiry firing between two calls, and recovery on an already-refunded entry. I would generate lifecycle sequences and assert the conservation identity after every step, not only at the end, since that is what separates a real accounting drift from a single wrong call.

Happy to answer anything before you assign.

[Opulencechuks]

I am confident that I can implement this issue having worked on similar issues in the past

[grantfox-oss]

🦊 GrantFox — @Opulencechuks has been assigned to this issue as part of the Third Campaign campaign!

Next steps:

1. Open a Pull Request referencing this issue (e.g., Closes #192)
2. Your PR will be reviewed by the RemitFlow maintainers

Good luck! Track your progress on GrantFox.