Repository navigation
audit: use tla+ to formally verify transaction graphs #1009
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 | |
| # This audit pass proves bugs exist in CURRENT code and proves correct | |
| # fix designs for them - the fixes are NOT yet applied to the Rust code | |
| # (see node/README.md's "Known gap" sections). These configs model the | |
| # verified fix designs (or a baseline that was never buggy) and must | |
| # always pass. See root README.md's "Formal verification (TLA+)" | |
| # section for what each spec covers. | |
| - name: Run baseline + proposed-fix 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 | |
| java -jar "$JAR" -config MultiActorRace.cfg MultiActorRace.tla | |
| # These model the CURRENT, unfixed code and are expected to keep | |
| # failing until the corresponding fix design above is actually applied | |
| # to the Rust source - that failure is a real, live issue, not a | |
| # historical artifact. If one of these starts passing without a | |
| # matching code change, either the bug config or the spec itself | |
| # silently changed meaning and no longer demonstrates the bug it's | |
| # supposed to. | |
| - name: Confirm known-bug specs still fail (fix not yet applied) | |
| 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 (bug not yet fixed in code) but passed - either the fix was applied (update this config's status) or the spec no longer demonstrates the bug" | |
| status=1 | |
| fi | |
| done | |
| exit $status |