name: CI & Formal Verification
'on':
push:
branches: ["main", "fix/**", "feat/**"]
pull_request:
branches: ["**"]
env:
CARGO_TERM_COLOR: always
RUSTFLAGS: "-D warnings"
permissions:
contents: read
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
version-bump-check:
name: Enforce Semantic Version Bump & CHANGELOG on PRs
runs-on: ubuntu-latest
permissions:
contents: read
if: github.event_name == 'pull_request'
steps:
- name: Checkout repository with full history
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
fetch-depth: 0
persist-credentials: false
- name: Verify Semantic Version Bump & CHANGELOG Entry
run: |
chmod +x ./scripts/check_version_bump.sh
./scripts/check_version_bump.sh
fmt-and-clippy:
name: Code Formatting & Strict Clippy Safety Guards
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Setup Rust toolchain
uses: dtolnay/rust-toolchain@4360b52568e2003a75bf9bc1d59f33a8e3fc893c with:
components: rustfmt, clippy
- name: Cargo Cache
uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 with:
path: |
~/.cargo/bin/
~/.cargo/registry/index/
~/.cargo/registry/cache/
~/.cargo/git/db/
target/
key: ${{ runner.os }}-cargo-lint-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-lint-
- name: Check code formatting
run: cargo fmt --all -- --check
- name: Check clippy lints
run: cargo clippy --all-targets --all-features -- -D warnings
test:
name: Full Test Suite, RFC Vectors & Spec Drift Verification
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Setup Rust toolchain
uses: dtolnay/rust-toolchain@4360b52568e2003a75bf9bc1d59f33a8e3fc893c
- name: Cargo Cache
uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 with:
path: |
~/.cargo/bin/
~/.cargo/registry/index/
~/.cargo/registry/cache/
~/.cargo/git/db/
target/
key: ${{ runner.os }}-cargo-test-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-test-
- name: Run all tests
run: cargo test --all-targets --all-features
- name: Run documentation tests
run: cargo test --doc --all-features
- name: "Run tests with default features (packaging contract: default = [])"
run: cargo test --all-targets
- name: Verify ATProto Lexicon & RFC Schema Synchronization
run: |
chmod +x ./scripts/sync_specs.sh
./scripts/sync_specs.sh --verify
coverage:
name: Code Coverage (cargo-llvm-cov ≥ 80%)
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Setup Rust toolchain
uses: dtolnay/rust-toolchain@4360b52568e2003a75bf9bc1d59f33a8e3fc893c with:
components: llvm-tools-preview
- name: Install cargo-llvm-cov
uses: taiki-e/install-action@1ed6d7be6168f6c9046541087ff549b6bc581fdf with:
tool: cargo-llvm-cov
- name: Measure coverage with 80% gate
run: cargo llvm-cov --all-features --fail-under-lines 80
security-audit:
name: Supply Chain & License Audit (cargo-deny)
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Run cargo-deny security checks
uses: EmbarkStudios/cargo-deny-action@b66acf5e9fe20f8aba065be86778a8a4c846f902
msrv:
name: MSRV (1.88) Library Build
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Install Rust 1.88 toolchain
run: rustup toolchain install 1.88.0 --profile minimal
- name: Check library on MSRV (locked deps, all features)
run: cargo +1.88.0 check --locked --lib --all-features
kani:
name: Kani Bounded Model Checking
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Run Kani Proofs
uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f with:
command: 'cargo-kani'
kani-version: '0.67.0'
args: '-Z source-coverage --harness proof_ --coverage | tee kani_output.txt'
- name: Gate on Kani cover satisfaction (anti-vacuity, fail-closed)
run: |
if ! ls kani_output.txt >/dev/null 2>&1; then
echo "::error::kani_output.txt missing — Kani did not run; failing closed"
exit 1
fi
# NOTE: CBMC's internal solver lines ("SAT checker: instance is
# UNSATISFIABLE") are NORMAL for successful proofs — they mean no
# assertion-violation trace exists. Only a cover property's own
# status line ("\t - Status: UNSATISFIABLE") indicates an
# unreachable cover.
if grep -E $'^[[:space:]]*-[[:space:]]Status: UNSATISFIABLE' kani_output.txt; then
echo "::error::Kani cover property UNSATISFIABLE (vacuous-proof risk)"
exit 1
fi
if ! grep -qE "successfully verified harnesses" kani_output.txt; then
echo "::error::Kani summary missing (fail-closed)"
exit 1
fi
echo "All Kani cover properties satisfied."
verus:
name: Verus Deductive Verification
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Run Verus Verification
run: bash scripts/run_verus.sh
publish:
name: Auto-Publish to Crates.io & Create GitHub Release
runs-on: ubuntu-latest
needs: [fmt-and-clippy, test, coverage, security-audit, msrv, kani, verus]
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
permissions:
contents: write
checks: read
steps:
- name: Checkout repository
uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 with:
persist-credentials: false
- name: Setup Rust toolchain
uses: dtolnay/rust-toolchain@4360b52568e2003a75bf9bc1d59f33a8e3fc893c
- name: Extract Current Version & Name
id: pkg_info
run: |
VERSION=$(grep -m1 '^[[:space:]]*version[[:space:]]*=' Cargo.toml | awk -F'"' '{print $2}')
NAME=$(grep -m1 '^[[:space:]]*name[[:space:]]*=' Cargo.toml | awk -F'"' '{print $2}')
echo "version=${VERSION}" >> $GITHUB_OUTPUT
echo "name=${NAME}" >> $GITHUB_OUTPUT
echo "Detected package: ${NAME} v${VERSION}"
- name: Check if Version Already Published on Crates.io
id: check_published
run: |
HTTP_STATUS=$(curl -s -o /dev/null -w "%{http_code}" -H "User-Agent: skyauth-release-check" "https://crates.io/api/v1/crates/${{ steps.pkg_info.outputs.name }}/${{ steps.pkg_info.outputs.version }}" || echo "000")
if [ "$HTTP_STATUS" -eq 200 ]; then
echo "published=true" >> $GITHUB_OUTPUT
echo "Version ${{ steps.pkg_info.outputs.version }} is already published on crates.io."
else
echo "published=false" >> $GITHUB_OUTPUT
echo "Version ${{ steps.pkg_info.outputs.version }} is NOT published on crates.io yet."
fi
- name: Wait for required CodeQL security scans on this commit
if: steps.check_published.outputs.published == 'false'
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
run: |
contexts=("CodeQL Static Security Scan (rust)" "CodeQL Static Security Scan (actions)")
deadline=$(( $(date +%s) + 900 ))
while :; do
# M8 fix: CodeQL creates CHECK RUNS, not commit statuses — the status
# endpoint was always empty for these contexts (verified during the
# review: status endpoint returned none while the Checks API showed
# both jobs). Poll check-runs instead.
json=$(gh api "repos/${GITHUB_REPOSITORY}/commits/${GITHUB_SHA}/check-runs" -H "Accept: application/vnd.github+json")
all_ok=true
for c in "${contexts[@]}"; do
state=$(jq -r --arg c "$c" '[.check_runs[] | select(.name == $c)][0].conclusion // "missing"' <<<"$json")
case "$state" in
success) ;;
missing|pending|null) all_ok=false ;;
*)
echo "::error::Required check '${c}' concluded with state '${state}'; refusing to publish"
exit 1
;;
esac
done
if $all_ok; then
echo "All required CodeQL scans succeeded on commit ${GITHUB_SHA}."
exit 0
fi
if [ "$(date +%s)" -ge "$deadline" ]; then
echo "::error::Timed out waiting for required CodeQL scans; refusing to publish"
exit 1
fi
echo "Waiting for required CodeQL scans..."
sleep 15
done
- name: Validate package before publish
if: steps.check_published.outputs.published == 'false'
run: cargo publish --dry-run --allow-dirty
- name: Publish to Crates.io
if: steps.check_published.outputs.published == 'false'
env:
CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN }}
run: |
# Secrets are not accessible in `if:` conditions, so the token
# presence check must live here; fail the job rather than silently
# skipping so a missing secret is visible in the required checks.
if [ -z "${CARGO_REGISTRY_TOKEN}" ]; then
echo "::error::CARGO_REGISTRY_TOKEN secret is not configured; cannot publish"
exit 1
fi
echo "Publishing ${{ steps.pkg_info.outputs.name }} v${{ steps.pkg_info.outputs.version }} to crates.io..."
cargo publish --allow-dirty --token "${CARGO_REGISTRY_TOKEN}"
- name: Create or Update GitHub Release Tag
if: steps.check_published.outputs.published == 'false'
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
TAG_NAME: "v${{ steps.pkg_info.outputs.version }}"
run: |
if ! gh release view "${TAG_NAME}" >/dev/null 2>&1; then
echo "Creating GitHub Release ${TAG_NAME}..."
gh release create "${TAG_NAME}" \
--target "${GITHUB_SHA}" \
--title "${TAG_NAME} - Production Release" \
--notes-file CHANGELOG.md
else
echo "GitHub Release ${TAG_NAME} already exists."
fi