Skip to content

Invariant test: Σ locked_tokens + Σ claimed_tokens + Σ surplus == total_funded #223

Description

@kilodesodiq-arch

Problem Statement. The Soroban contract tracks KEY_TOTAL_LOCKED and KEY_TOTAL_CLAIMED
per token but never asserts the invariant that those totals plus the surplus equal the
total ever funded. A single off-by-one in decrement_locked() or finalize_claim() would
corrupt the ledger silently — and there is no on-chain total_funded storage key, so the
test must reconstruct that aggregate from the EscrowFunded event stream.

Why it matters. Mis-bookkeeping on a humanitarian escrow is what auditors will look at
first. Even a sub-stroop drift compounds through the lifetime of the contract.

Technical Context. app/onchain/contracts/aid_escrow/src/lib.rs keeps two Map<Address, i128> totals. get_total_locked and get_total_claimed are exposed to readers but never
asserted against one another, and the contract emits EscrowFunded { from, token, amount, timestamp } events from fund() and SurplusWithdrawnEvent / PackageRefunded events
elsewhere. Invariant #15 reconstructs total_funded by summing those events in a Soroban
test harness.

Expected Outcome. A proptest!-driven invariant test that exercises
fund → create → claim → fund → create → revoke / refund / withdraw_surplus triples and
asserts

Σ locked(tokens) + Σ claimed(tokens) == Σ EscrowFunded.amount(tokens)
                                    − Σ SurplusWithdrawn.amount(tokens)
                                    − Σ transfers-to-admin (refunded)

Acceptance Criteria.

  • New file app/onchain/contracts/aid_escrow/tests/invariants.rs aggregates events using
    env.events().all() and replays them post-hoc, then runs 100 random sequences.
  • Failure produces a minimal shrunk example identifying which instruction broke it,
    along with a printed event-stream snapshot.
  • The invariant is also asserted at bookkeeping calls (decrement_locked,
    finalize_claim, withdraw_surplus, refund) using unit-level smoke tests.

Implementation Notes. Use proptest as a dev-dependency. Seed proptest! with a
fixed seed in CI for reproducibility. Events are emitted via the contractevent macro —
use env.events().all() (or the equivalent in the chosen SDK) at assertion time.

Files or modules likely to be affected. app/onchain/contracts/aid_escrow/tests/invariants.rs.

Dependencies. None.

Difficulty. Medium
Estimated effort. M



Backlog item #15 from `docs/maintainer-issue-backlog.md.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions