Repository navigation
audit: use tla+ to formally verify transaction graphs #1005
Workflow file for this run
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: Cargo Build & Test | |
| on: | |
| push: | |
| branches: | |
| - main | |
| - dev | |
| tags: | |
| - v[0-9]+.* | |
| pull_request: | |
| branches: | |
| - main | |
| - dev | |
| - gc-v2 | |
| env: | |
| CARGO_TERM_COLOR: always | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| fmt: | |
| name: Rustfmt | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions-rs/toolchain@v1 | |
| timeout-minutes: 30 | |
| with: | |
| profile: minimal | |
| toolchain: stable | |
| override: true | |
| - run: rustup component add rustfmt | |
| - uses: actions-rs/cargo@v1 | |
| with: | |
| command: fmt | |
| args: --all -- --check | |
| clippy: | |
| name: Clippy | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions-rs/toolchain@v1 | |
| timeout-minutes: 30 | |
| with: | |
| profile: minimal | |
| toolchain: nightly-2025-12-11 | |
| override: true | |
| components: clippy | |
| - run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh | |
| - name: Install Dependencies | |
| run: sudo apt update && sudo apt install protobuf-compiler | |
| - run: | | |
| source ~/.zkm-toolchain/env | |
| cargo clippy --all-targets -- -D warnings | |
| test: | |
| name: Cargo Test | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - nightly-2025-12-11 | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Install Ziren toolchain | |
| run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh | |
| - name: Install Dependencies | |
| run: sudo apt update && sudo apt install protobuf-compiler | |
| - name: Launch the Regtest | |
| run: cd scripts && docker compose up -d | |
| - name: Run all unit tests | |
| run: | | |
| set -e | |
| source ~/.zkm-toolchain/env | |
| cargo test -r --all --all-targets | |
| tla-plus: | |
| name: TLA+ Formal Verification | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions/setup-java@v4 | |
| with: | |
| distribution: temurin | |
| java-version: "21" | |
| - name: Download TLA+ tools | |
| run: | | |
| mkdir -p ~/.local/share/tlaplus | |
| curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \ | |
| https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar | |
| # These model the CURRENT code and must always pass. A failure here is | |
| # a real regression - see README.md's "Formal verification (TLA+)" | |
| # section for what each spec covers. | |
| - name: Run current-code specs (must pass) | |
| working-directory: node/tla | |
| run: | | |
| set -e | |
| JAR=~/.local/share/tlaplus/tla2tools.jar | |
| java -jar "$JAR" -config GraphLifecycleCoreOnly.cfg GraphLifecycle.tla | |
| java -jar "$JAR" -config GraphLifecycleFixed.cfg GraphLifecycle.tla | |
| java -jar "$JAR" -config GraphLifecycleFineGrainedFixed.cfg GraphLifecycleFineGrainedFixed.tla | |
| java -jar "$JAR" -config InstancePresignedFixed.cfg InstancePresigned.tla | |
| java -jar "$JAR" -config Take2DisproveRace.cfg Take2DisproveRace.tla | |
| # These model PRE-FIX behavior and are permanent regression artifacts - | |
| # they are expected to keep failing forever. If one of these starts | |
| # passing, either the bug config or the spec itself silently changed | |
| # meaning and no longer demonstrates the bug it's supposed to. | |
| - name: Confirm pre-fix specs still fail (regression artifacts) | |
| working-directory: node/tla | |
| run: | | |
| JAR=~/.local/share/tlaplus/tla2tools.jar | |
| status=0 | |
| for pair in \ | |
| "GraphLifecycle.cfg:GraphLifecycle.tla" \ | |
| "GraphLifecycleFineGrained.cfg:GraphLifecycleFineGrained.tla" \ | |
| "InstancePresignedBug.cfg:InstancePresigned.tla" \ | |
| ; do | |
| cfg="${pair%%:*}"; tla="${pair##*:}" | |
| if java -jar "$JAR" -config "$cfg" "$tla" | grep -q "Model checking completed. No error has been found."; then | |
| echo "::error::$tla / $cfg was expected to keep failing (pre-fix regression artifact) but passed - it no longer demonstrates the bug" | |
| status=1 | |
| fi | |
| done | |
| exit $status |