test(postage): add property-style invariant tests and contract docume…#1580
Merged
kryputh merged 2 commits intoJul 20, 2026
Merged
Conversation
TheDEV111
force-pushed
the
feature/postage-invariant-tests
branch
from
July 19, 2026 17:03
4e9d667 to
66ae2fb
Compare
Contributor
Author
|
@kryputh edits were made to this closed PR |
Collaborator
|
@TheDEV111 fix conflict |
Contributor
Author
|
@kryputh pls merge |
3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
closes #1395
📝 Overview
This PR improves the Soroban Postage contract in lib.rs by introducing property-style invariant tests and complete contract-facing Rust documentation.
These changes strengthen reliability and ledger integration safety by verifying mathematical balance conservation, fee calculations, deadline ordering, and terminal state machine transitions across parameter combinations.
──────
🚀 Key Changes
1. Property-Style Invariant Test Suite
Added property-style invariant tests covering contract boundary conditions and state transitions:
• Token Balance Conservation Invariant (invariant_token_balance_conservation_across_lifecycle_paths)
• Verifies that for any deposit amount and fee rate in 0..=10,000 bps, the total token supply across sender, recipient, treasury, and contract remains strictly constant throughout the escrow lifecycle.
• Asserts contract_balance == amount during pending status and contract_balance == 0 post-settlement.
• Fee Calculation & Split Bounds Invariant (invariant_fee_calculation_and_split_bounds)
• Evaluates fee calculations across a broad matrix of amounts (0 to i128::MAX / 20,000) and fee basis points (0 to 10,000 bps).
• Validates properties:
• 0 <= fee <= gross_amount
• recipient_amount >= 0
• recipient_amount + fee == gross_amount
• Boundary guarantees for fee_bps == 0 (zero fee) and fee_bps == 10,000 (100% fee).
• State Transition & Single Terminal State Invariant (invariant_state_transitions_reach_unique_terminal_state)
• Asserts that every escrow reaches exactly one terminal state (Settled, Refunded, or Reclaimed).
• Verifies that once a terminal state is reached, all further resolution or transition calls (settle, refund, reclaim, expire, dispute) permanently fail with Error::AlreadyResolved.
• Deadline Ordering & Reclaim Boundary Invariant (invariant_deadline_ordering_and_reclaim_boundaries)
• Asserts strict time monotonicity: created_at < expires_at <= dispute_until == reclaimable_at.
• Verifies that reclaim strictly fails with NotExpired before the reclaimable boundary (t < reclaimable_at) and succeeds at or after the boundary (t >= reclaimable_at).
• Initialization Preconditions & Boundary Invariant (invariant_initialization_preconditions)
• Tests input validation guards during contract initialization:
• minimum < 0 → Error::InvalidAmount
• fee_bps > 10,000 → Error::InvalidFee
• expiry_seconds == 0 → Error::InvalidWindow
• Re-initialization → Error::AlreadyInitialized
──────
2. Contract Documentation & DX
• Added module-level (//!) rustdoc documentation explaining Postage escrow rules and lifecycle transitions.
• Added item-level (///) rustdoc documentation for all public structs, enums, errors, and contract implementation methods (initialize, config, minimum, quote, submit, expire, settle, refund, dispute, reclaim, get).
──────
✅ Acceptance Criteria Checklist
[✓] Property-style invariant tests: Covered balance conservation, fee split bounds, state machine monotonicity, and deadline boundaries.
[✓] Existing tests pass: All 22 pre-existing unit tests plus 5 new property invariant test suites pass (27 total tests in stealth-postage).
[✓] Contract-facing behavior documented: Added rustdoc comments to all public types and entrypoints.
[✓] Backward compatibility: Public contract interface, method signatures, storage layout, and event payloads remain untouched.