Skip to content

INVARIANTS.md

Latest commit

 

History

History
484 lines (361 loc) · 22.2 KB

INVARIANTS.md

File metadata and controls

484 lines (361 loc) · 22.2 KB

Vault Balance Invariant

Invariant: For every reachable state of the CalloraVault contract, the stored balance in VaultMeta.balance is always greater than or equal to 0 and less than or equal to i128::MAX.

  • Storage field: VaultMeta.balance : i128
  • Accessors:
    • get_meta(env: Env) -> VaultMeta
    • balance(env: Env) -> i128
  • Guarantee: Any value returned by get_meta(env).balance or balance(env) is never negative and cannot overflow the i128 numeric boundary. Any operation that would cause an overflow (e.g., deposit past i128::MAX) will panic and revert the transaction.

This document lists all functions that can change the stored balance and the pre-/post-conditions that preserve this invariant.

Functions That Modify Balance

Only the following functions mutate VaultMeta.balance:

  • init(env, owner, usdc_token, initial_balance, min_deposit, revenue_pool, max_deduct)
  • deposit(env, from, amount)
  • deduct(env, caller, amount, request_id)
  • batch_deduct(env, caller, items: Vec<DeductItem>)
  • withdraw(env, amount)
  • withdraw_to(env, to, amount)

Helper and view functions such as get_meta, get_max_deduct, get_revenue_pool, get_admin, and balance do not modify balance.

init

Effect on balance

  • Sets VaultMeta.balance to initial_balance.unwrap_or(0).

Pre-conditions

  • Vault is not already initialized:
    • !env.storage().instance().has(MetaKey)
  • initial_balance.unwrap_or(0) >= 0
  • max_deduct.unwrap_or(DEFAULT_MAX_DEDUCT) > 0
  • The on-ledger USDC balance already covers the requested internal starting balance:
    • usdc.balance(current_contract_address) >= initial_balance.unwrap_or(0)

Post-conditions

  • VaultMeta.balance == initial_balance.unwrap_or(0)
  • VaultMeta.balance >= 0 (because initial_balance.unwrap_or(0) is explicitly checked to be non-negative before storage is written).

deposit

Effect on balance

  • Increases VaultMeta.balance by amount:
    • balance' = balance + amount

Pre-conditions

  • Caller is authorized:
    • from.require_auth()
  • Vault is initialized (via get_meta and USDC address lookup).
  • Vault is not paused:
    • is_paused(env) == false (deposit aborts with "vault is paused" if paused).
  • Amount satisfies the minimum deposit:
    • amount >= meta.min_deposit
  • USDC transfer-from must succeed:
    • Token contract must allow current_contract_address to transfer amount from from to current_contract_address.

Post-conditions

  • VaultMeta.balance' = balance + amount
  • Because amount >= 0 in practice (negative amounts are not useful and would fail at the token layer) and balance is already non-negative, we maintain:
    • VaultMeta.balance' >= 0

deduct

Effect on balance

  • Decreases VaultMeta.balance by amount:
    • balance' = balance - amount

Pre-conditions

  • Caller is authorized:
    • caller.require_auth()
  • Vault is initialized and not paused.
  • Amount constraints:
    • amount > 0
    • amount <= get_max_deduct(env)
  • Sufficient balance:
    • meta.balance >= amount
  • Settlement configured (Issue #263):
    • StorageKey::Settlement is present — i.e. set_settlement has been called.
    • If absent, the call panics with "settlement address not set" before any balance mutation, guaranteeing no partial state update.

Post-conditions

  • VaultMeta.balance' = balance - amount
  • Because of the meta.balance >= amount assertion and amount > 0, we have:
    • VaultMeta.balance' >= 0
  • The on-ledger USDC decrease at the vault equals the internal balance decrease (both equal amount), because the deducted USDC is always transferred to the settlement address.

batch_deduct

Effect on balance

  • Total change: balance' = balance - sum_i(amount_i).

Pre-conditions

  • Caller is authorized: caller.require_auth()
  • Vault is initialized and not paused.
  • 1 <= items.len() <= MAX_BATCH_SIZE (50)
  • The explicit batch cap is a practical Soroban resource bound: it limits looped validation work, transfer/event overhead, and invocation footprint in one call. Tune this cap conservatively if production workloads approach network CPU or budget limits.
  • For every item: item.amount > 0 and item.amount <= get_max_deduct(env)
  • Cumulative deductions do not exceed balance:
    • Validated in a single pass before any state is written.
  • Settlement configured (Issue #263): StorageKey::Settlement is present; missing settlement causes "settlement address not set" panic before any state write, so the batch is atomically reverted.

Post-conditions

  • VaultMeta.balance' = balance - sum_i(amount_i) >= 0
  • If any pre-condition fails, the call panics before storage is written — no partial balance update is possible.
  • One deduct event is emitted per item, only on success, after state is written.

withdraw

Effect on balance

  • Decreases VaultMeta.balance by amount:
    • balance' = balance - amount

Pre-conditions

  • Vault is initialized.
  • Only the owner may withdraw:
    • meta.owner.require_auth()
  • Amount constraints:
    • amount > 0
    • meta.balance >= amount

Post-conditions

  • VaultMeta.balance' = balance - amount
  • From meta.balance >= amount and amount > 0:
    • VaultMeta.balance' >= 0

withdraw_to

Effect on balance

  • Decreases VaultMeta.balance by amount:
    • balance' = balance - amount

Pre-conditions

  • Vault is initialized.
  • Only the owner may withdraw:
    • meta.owner.require_auth()
  • Amount constraints:
    • amount > 0
    • meta.balance >= amount

Post-conditions

  • VaultMeta.balance' = balance - amount
  • From meta.balance >= amount and amount > 0:
    • VaultMeta.balance' >= 0

How Tests Support the Invariant

The test suite in contracts/vault/src/test.rs provides practical evidence for the non-negative balance invariant:

  • Deterministic fuzz test (fuzz_deposit_and_deduct):
    • Randomly mixes deposits and deducts, asserting after each step that:
      • balance() >= 0
      • balance() matches a locally tracked expected value.
  • Batch deduct tests:
    • batch_deduct_success, batch_deduct_all_succeed, batch_deduct_all_revert, and batch_deduct_revert_preserves_balance all verify that:
      • Successful batches leave balance consistent with expectations.
      • Failing batches revert without corrupting balance.
  • Withdraw tests:
    • withdraw_owner_success, withdraw_exact_balance, and withdraw_exceeds_balance_fails ensure that:
      • Withdrawals are only allowed up to the current balance.
      • Over-withdraw attempts panic before balance can become negative.

Together with the explicit pre-/post-conditions above, these tests help auditors and maintainers validate that VaultMeta.balance is always non-negative in all reachable states.

Settlement Developer Credit Invariant

Invariant: For every reachable state of CalloraSettlement, every credited developer balance stored under DEVELOPER_BALANCES_KEY is always greater than or equal to 0.

This document lists all functions that can change credited developer balances and the pre-/post-conditions that preserve this invariant.

Functions That Modify Credited Developer Balances

Only the following functions mutate the developer-balance map in the settlement contract:

Helper and admin functions such as get_developer_balance, get_all_developer_balances, get_admin, get_vault, get_global_pool, set_admin, and set_vault do not modify credited developer balances.

init

Effect on credited balances

  • Stores an empty Map<Address, i128> at DEVELOPER_BALANCES_KEY.

Pre-conditions

  • Settlement contract is not already initialized:
    • !env.storage().instance().has(ADMIN_KEY)

Post-conditions

  • The credited-balance map is empty.
  • Therefore every stored developer balance is vacuously non-negative.

receive_payment

Effect on credited balances

  • If to_pool == false, increases the selected developer balance by amount:
    • developer_balance' = developer_balance + amount
  • If to_pool == true, the developer-balance map is unchanged.

Pre-conditions

  • Caller passes the settlement authorization gate:
  • Positive credit amount:
    • amount > 0
  • If to_pool == false, a developer address must be supplied:
    • developer.is_some()

Post-conditions

  • For the to_pool == false branch:
    • developer_balance' = developer_balance + amount
    • Because developer_balance >= 0 by the inductive hypothesis and amount > 0, we maintain:
      • developer_balance' > developer_balance >= 0
  • All other developers' balances are unchanged.
  • For the to_pool == true branch, the developer-balance map is unchanged, so the invariant is preserved.
  • If any pre-condition fails, the call reverts and the original credited balances are preserved.

How Tests Support the Invariant

The test suite in contracts/settlement/src/test.rs provides practical evidence for the non-negative credited-balance invariant:

  • Developer credit test (test_receive_payment_to_developer):
    • Verifies that a positive settlement credit creates a positive developer balance while leaving the global pool unchanged.
  • Accumulation test (test_receive_multiple_payments_accumulate):
    • Verifies repeated credits to the same developer are additive and remain non-negative.
  • Missing developer guard (test_receive_payment_pool_false_no_developer):
    • Verifies the contract rejects the only branch that could otherwise write an ill-formed developer credit.
  • Authorization and amount guards (test_receive_payment_unauthorized, test_receive_payment_zero_amount):
    • Verify unauthorized or zero-amount calls revert before credited balances can be corrupted.

Together with the explicit pre-/post-conditions above, these tests help auditors and maintainers validate that settlement developer credits are always non-negative in all reachable states.

Settlement Global Pool Accounting Invariant

Invariant: For every reachable state of CalloraSettlement, GlobalPool.total_balance is always greater than or equal to 0, and equals the initial 0 plus the sum of all successful receive_payment(..., to_pool = true, ...) credits since initialization.

This invariant is intentionally about internal accounting state. The current settlement contract only records credits; it does not implement a debit path from GlobalPool.total_balance, so this field is a monotonic accounting counter rather than a proof of withdrawable USDC.

Functions That Modify Global Pool Accounting

Only the following functions mutate GlobalPool:

Helper and admin functions such as get_global_pool, get_developer_balance, get_all_developer_balances, set_admin, and set_vault do not modify global-pool accounting.

init

Effect on global pool accounting

  • Stores:
    • GlobalPool { total_balance: 0, last_updated: env.ledger().timestamp() }

Pre-conditions

  • Settlement contract is not already initialized:
    • !env.storage().instance().has(ADMIN_KEY)

Post-conditions

  • GlobalPool.total_balance == 0
  • GlobalPool.last_updated equals the current ledger timestamp at initialization.
  • Because the initialized pool balance is 0, the non-negativity and additive-accounting invariants both hold.

receive_payment

Effect on global pool accounting

  • If to_pool == true, increases GlobalPool.total_balance by amount:
    • total_balance' = total_balance + amount
  • If to_pool == false, GlobalPool is unchanged.

Pre-conditions

Post-conditions

  • For the to_pool == true branch:
    • total_balance' = total_balance + amount
    • last_updated' = env.ledger().timestamp()
    • Because total_balance >= 0 by the inductive hypothesis and amount > 0, we maintain:
      • total_balance' > total_balance >= 0
  • For the to_pool == false branch:
    • GlobalPool.total_balance' = GlobalPool.total_balance
    • GlobalPool.last_updated' = GlobalPool.last_updated
  • If any pre-condition fails, the call reverts and the original global-pool accounting is preserved.

How Tests Support the Invariant

The test suite in contracts/settlement/src/test.rs provides practical evidence for the global-pool accounting invariant:

  • Initialization test (test_settlement_initialization):
    • Verifies that get_global_pool().total_balance starts at 0.
  • Pool credit test (test_receive_payment_to_pool):
    • Verifies a successful pool credit increments total_balance by the credited amount.
  • Developer credit isolation test (test_receive_payment_to_developer):
    • Verifies developer-directed credits do not mutate GlobalPool.total_balance.
  • Admin caller path (test_admin_can_receive_payment):
    • Verifies the admin can use the same guarded credit path and the accounting update remains additive.
  • Authorization and amount guards (test_receive_payment_unauthorized, test_receive_payment_zero_amount):
    • Verify invalid calls revert before GlobalPool can be modified.

Together with the explicit pre-/post-conditions above, these tests help auditors and maintainers validate that settlement global-pool accounting remains non-negative and additive in all reachable states.

Cross-Contract Authorization Invariant

Invariant: Only explicitly authorized principals may route funds out of the vault, credit settlement balances, reconfigure downstream contract addresses, or distribute USDC from the revenue pool.

This invariant is the authorization counterpart to the accounting invariants above: balances remain meaningful only if state-changing entry points are reachable by the intended principals.

Functions That Enforce Authorization Constraints

The following functions are the relevant state-changing gates across the vault, settlement, and revenue-pool flow:

Pure accessors such as get_admin, get_vault, get_global_pool, get_admin, and balance do not weaken the authorization invariant because they are read-only.

Vault routing entry points

Effect on authorization-sensitive state

  • deduct and batch_deduct are the only paths that route funds from the vault to a configured settlement or revenue-pool contract.
  • set_settlement is the configuration entry point that changes where settlement-directed deductions are sent.

Pre-conditions

  • deduct / batch_deduct:
    • caller.require_auth()
    • Caller is the vault owner or the stored authorized_caller.
  • set_settlement:
    • caller.require_auth()
    • caller == get_admin(env)

Post-conditions

  • Unauthorized callers cannot trigger downstream fund routing from the vault.
  • Unauthorized callers cannot repoint the settlement destination used by the vault.

Settlement entry points

Effect on authorization-sensitive state

  • receive_payment is the only settlement entry point that mutates developer credits or global-pool accounting.
  • set_admin and set_vault mutate the principals allowed to administer or feed settlement accounting.

Pre-conditions

  • receive_payment:
  • set_admin / set_vault:
    • caller.require_auth()
    • caller == get_admin(env)

Post-conditions

  • No address other than the configured vault or current settlement admin can create accounting entries.
  • No address other than the current settlement admin can rotate settlement admin or vault authority.

Revenue-pool entry points

Effect on authorization-sensitive state

Pre-conditions

  • init:
    • admin.require_auth()
    • The contract is not already initialized.
  • set_admin, receive_payment, distribute, batch_distribute:
    • Caller authenticates with caller.require_auth()
    • caller == get_admin(env)
  • distribute / batch_distribute also require:
    • Positive amount(s)
    • Sufficient on-contract USDC balance before transfer
  • batch_distribute additionally requires:
    • 1 <= payments.len() <= MAX_BATCH_SIZE (50)

Post-conditions

  • No address other than the current revenue-pool admin can emit administrative payment events or move USDC out of the revenue pool.
  • Failed authorization checks revert before any payout or admin rotation occurs.

How Tests Support the Invariant

The settlement, vault, and revenue-pool test suites provide practical evidence for the authorization invariant:

  • Settlement authorization tests (test_receive_payment_unauthorized, test_set_admin_unauthorized, test_set_vault_unauthorized in contracts/settlement/src/test.rs):
    • Verify unauthorized callers cannot mutate settlement accounting or configuration.
  • Revenue-pool authorization tests (distribute_unauthorized_panics, set_admin_unauthorized_panics in contracts/revenue_pool/src/test.rs):
    • Verify unauthorized callers cannot distribute funds or rotate revenue-pool control.
  • Vault routing authorization test (set_settlement_unauthorized_panics in contracts/vault/src/test.rs):
    • Verifies unauthorized callers cannot change the vault's settlement destination.

Together with the explicit pre-/post-conditions above, these tests help auditors and maintainers validate that cross-contract routing, accounting, and payout actions remain reachable only by the intended principals.