Nightly #39
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: Nightly | |
| on: | |
| schedule: | |
| - cron: "0 4 * * *" # 4:00 UTC daily | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.workflow }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| jobs: | |
| full-test: | |
| name: Full test suite | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 45 | |
| env: | |
| CARGO_TARGET_DIR: target/ci-nightly | |
| CARGO_INCREMENTAL: '0' | |
| steps: | |
| - name: Harden runner | |
| uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0 | |
| with: | |
| egress-policy: audit | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7 | |
| with: | |
| persist-credentials: false | |
| - name: Setup Rust toolchain | |
| uses: dtolnay/rust-toolchain@4be7066ada62dd38de10e7b70166bc74ed198c30 # stable | |
| with: | |
| components: clippy, rustfmt | |
| - name: Cache dependencies | |
| uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2 | |
| with: | |
| shared-key: ci-nightly | |
| - name: Install system dependencies (Linux) | |
| if: runner.os == 'Linux' | |
| run: sudo apt-get install -y protobuf-compiler libz3-dev z3 ripgrep | |
| env: | |
| DEBIAN_FRONTEND: noninteractive | |
| - name: Set Linux Z3 paths | |
| if: runner.os == 'Linux' | |
| run: | | |
| { | |
| echo "Z3_SYS_Z3_HEADER=/usr/include/z3.h" | |
| echo "CPATH=/usr/include" | |
| echo "LIBRARY_PATH=/usr/lib/x86_64-linux-gnu" | |
| } >> "$GITHUB_ENV" | |
| - name: Format check | |
| run: cargo fmt --check --all | |
| - name: Clippy | |
| run: cargo clippy --workspace --locked -- -D warnings | |
| - name: Full test suite | |
| run: cargo test --workspace --locked | |
| - name: Build compiler | |
| run: cargo build --locked --bin assura | |
| - name: E2E check all demos | |
| run: | | |
| for demo in demos/*.assura; do | |
| # Audit demos have intentional counterexamples (real CVE models); skip them | |
| case "$demo" in *-audit*|*audit-*) echo "=== Skipping audit demo $demo ==="; continue;; esac | |
| echo "=== Checking $demo ===" | |
| cargo run --bin assura -- check "$demo" | |
| done | |
| - name: E2E check all examples | |
| run: | | |
| failed=0 | |
| for example in $(find examples -name '*.assura' | sort); do | |
| echo "=== Checking $example ===" | |
| if ! cargo run --bin assura -- check "$example"; then | |
| echo "FAIL: $example" | |
| failed=1 | |
| fi | |
| done | |
| exit $failed | |
| - name: Codegen validation (demos) | |
| run: | | |
| for demo in demos/*.assura; do | |
| case "$demo" in *-audit*|*audit-*) continue;; esac | |
| echo "=== Building $demo ===" | |
| cargo run --bin assura -- build --no-check "$demo" | |
| # build writes to <input-parent>/generated/ (e.g. demos/generated/) | |
| gen_dir="$(dirname "$demo")/generated" | |
| echo "=== Checking generated Rust for $demo ===" | |
| (cd "$gen_dir" && cargo check) | |
| rm -rf "$gen_dir" | |
| done | |
| no-z3-fallback: | |
| name: No-Z3 fallback | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| steps: | |
| - name: Harden runner | |
| uses: step-security/harden-runner@bf7454d06d71f1098171f2acdf0cd4708d7b5920 # v2.20.0 | |
| with: | |
| egress-policy: audit | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7 | |
| with: | |
| persist-credentials: false | |
| - name: Setup Rust toolchain | |
| uses: dtolnay/rust-toolchain@4be7066ada62dd38de10e7b70166bc74ed198c30 # stable | |
| - name: Cache dependencies | |
| uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2 | |
| with: | |
| shared-key: ci-nightly-no-z3 | |
| - name: Build without Z3 | |
| run: cargo check -p assura-smt --no-default-features --locked |