phantom/.github/workflows/ci.yml at main · v-code01/phantom · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
name: CI

on:
  push:
    branches: [main, "feat/*"]
  pull_request:
    branches: [main]

env:
  RUST_BACKTRACE: 1
  CARGO_TERM_COLOR: always

jobs:
  build-and-test:
    name: Build and test (macOS arm64)
    runs-on: macos-15

    steps:
      - name: Checkout
        uses: actions/checkout@v4

      - name: Install Rust stable
        uses: dtolnay/rust-toolchain@stable
        with:
          components: clippy

      - name: Cache cargo
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target/
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: ${{ runner.os }}-cargo-

      - name: Clippy (deny warnings)
        run: cargo clippy --workspace --all-targets -- -D warnings

      - name: Test (hardware tests excluded)
        run: cargo test --workspace
        # Hardware tests marked #[ignore = "requires Apple Silicon hardware"] are skipped.
        # Run `make test-hardware` on physical M4/M5 Max to include them.

  tla-check:
    name: TLA+ model checker
    runs-on: macos-latest

    steps:
      - name: Checkout
        uses: actions/checkout@v4

      - name: Install Java (TLC dependency)
        uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"

      - name: Download TLA+ tools
        run: |
          curl -L -o tla2tools.jar \
            https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar

      - name: Run TLC model checker
        run: |
          java -jar tla2tools.jar tla/TokenCoherence.tla -config tla/TokenCoherence.cfg

  dafny-check:
    name: Dafny I5 proof
    runs-on: macos-latest

    steps:
      - name: Checkout
        uses: actions/checkout@v4

      - name: Install Dafny
        run: brew install dafny

      - name: Verify I5 invariant
        run: dafny verify dafny/KvInvariant.dfy