Merge pull request #93 from quicknode/claude/solana-examples-ci-asm-j… #28
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Kani | |
| # Formal-verification proofs (https://github.com/model-checking/kani) for the | |
| # finance/ example programs. Each <program>/kani-proofs crate models its | |
| # program's pure money-math and lets the Kani model checker prove the invariants | |
| # exhaustively, in the spirit of aeyakovenko/percolator. | |
| # | |
| # WHY THIS RUNS ON A WEEKLY SCHEDULE, NOT ON EVERY PUSH/PR | |
| # ------------------------------------------------------- | |
| # Most of the finance proofs verify NONLINEAR 128-bit arithmetic (constant- | |
| # product curves, mul_div with a symbolic divisor, integer sqrt, pari-mutuel | |
| # payouts, share exchange rates). Kani is a bit-precise model checker: it | |
| # bit-blasts that arithmetic into SAT, and nonlinear / symbolic-divisor terms | |
| # are the worst case for the solver. Even with bounded inputs, individual | |
| # harnesses take tens of seconds and a full crate runs for minutes; the whole | |
| # finance suite is far too slow to gate every push/PR. So the heavy | |
| # `cargo kani` verification runs once a week (and on demand via | |
| # workflow_dispatch), while a fast unit-test job still runs on every push/PR to | |
| # catch model regressions early. See each finance/<program>/kani-proofs/README.md | |
| # for the per-harness bounds and timings. | |
| on: | |
| schedule: | |
| # Mondays at 06:00 UTC. Weekly because the proofs are slow (see header). | |
| - cron: "0 6 * * 1" | |
| workflow_dispatch: {} | |
| # Fast feedback only: the unit-test job below is gated to these events; the | |
| # slow `verify` job is gated to schedule / manual dispatch. | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| types: [opened, synchronize, reopened] | |
| branches: | |
| - main | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| # See https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/ | |
| FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true | |
| jobs: | |
| # Fast feedback on every push/PR: the proof crates compile and their plain | |
| # unit tests pass on stable, independently of the (slow) Kani toolchain. This | |
| # catches model regressions without paying for full verification. | |
| unit-tests: | |
| name: Proof unit tests (${{ matrix.program }}) | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| program: | |
| - escrow | |
| - token-swap | |
| - order-book | |
| - lending | |
| - betting-market | |
| - vault-strategy | |
| - token-fundraiser | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - name: Run unit tests | |
| working-directory: finance/${{ matrix.program }}/kani-proofs | |
| run: cargo test | |
| # The formal verification itself. SLOW (minutes per crate), so it only runs on | |
| # the weekly schedule or when triggered manually — never on push/PR. The | |
| # official Kani action installs the verifier + CBMC toolchain (with caching) | |
| # and runs `cargo kani` in each proof crate; any failed proof fails the job. | |
| verify: | |
| name: Kani proofs (${{ matrix.program }}) | |
| if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| program: | |
| - escrow | |
| - token-swap | |
| - order-book | |
| - lending | |
| - betting-market | |
| - vault-strategy | |
| - token-fundraiser | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Run Kani | |
| uses: model-checking/kani-github-action@v1 | |
| with: | |
| working-directory: finance/${{ matrix.program }}/kani-proofs |