feat(verus): verified StaticVec proofs pass via Bazel — 13 verified, … #362

Workflow file for this run

	name: Rust CI

	on:
	push:
	branches: [ main ]
	pull_request:
	branches: [ main ]
	workflow_dispatch: # Allows manual triggering
	inputs:
	run_extended_analysis: # Input to specifically trigger Kani/Miri
	description: 'Run Kani and Miri extended static analysis?'
	required: false
	default: false # Boolean false, not string
	type: boolean

	permissions:
	contents: read
	issues: write
	pull-requests: write
	actions: read
	checks: write

	env:
	CARGO_TERM_COLOR: always
	# RUST_LOG: "info,cargo_kiln=debug,dagger_sdk=debug" # Optional: for more detailed Dagger logs

	jobs:
	ci_checks_and_docs:
	name: CI Checks & Docs
	runs-on: ubuntu-latest
	# This job runs on push, PR, and all manual triggers (regardless of input)
	steps:
	- uses: actions/checkout@v5
	- name: Cargo Cache
	uses: actions/cache@v5
	with:
	path: \|
	~/.cargo/bin/
	~/.cargo/registry/index/
	~/.cargo/registry/cache/
	~/.cargo/git/db/
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	- name: Dagger Engine Cache
	uses: actions/cache@v5
	with:
	path: ~/.cache/dagger
	key: ${{ runner.os }}-dagger-engine
	- uses: actions-rs/toolchain@v1
	with:
	profile: minimal
	toolchain: stable # Or match your rust-toolchain.toml for building cargo-kiln
	override: true
	- name: Install and setup cargo-kiln with all tools
	run: \|
	cargo build --package cargo-kiln # Ensures cargo-kiln and its direct deps are built/cached
	cargo install --path cargo-kiln --force # Install cargo-kiln for use in subsequent steps
	cargo-kiln setup --all # Setup all development tools automatically
	- name: Run CI Integrity Checks (lint, fmt, deny, spell, headers, etc.)
	run: cargo-kiln verify --detailed
	- name: Setup Java for PlantUML (if CheckDocsStrict Dagger pipeline needs it from host - unlikely)
	uses: actions/setup-java@v5
	if: false # Assuming Dagger pipeline for docs is self-contained
	with:
	distribution: 'temurin'
	java-version: '17'
	- name: Install Python & PlantUML (if CheckDocsStrict Dagger pipeline needs them - unlikely)
	if: false # Assuming Dagger pipeline for docs is self-contained
	run: \|
	sudo apt-get update && sudo apt-get install -y python3-pip plantuml
	pip3 install -r docs/source/requirements.txt
	- name: Run Strict Documentation Check
	run: cargo-kiln docs --private
	- name: Initialize Requirements File (if missing)
	run: cargo-kiln verify --asil c # Requirements initialization is handled automatically
	- name: Run Requirements Verification
	run: cargo-kiln verify --asil c --detailed
	- name: Generate Safety Summary for Documentation
	run: cargo-kiln verify --asil c --detailed # Safety summary is generated automatically

	code_quality:
	name: Code Quality Checks
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v5
	- uses: actions-rs/toolchain@v1
	with:
	profile: minimal
	toolchain: stable
	override: true
	components: rustfmt, clippy
	- name: Install and setup cargo-kiln
	run: \|
	cargo build --package cargo-kiln
	cargo install --path cargo-kiln --force
	cargo-kiln setup --check # Verify tools are available
	- name: Check for test files in src/
	run: cargo-kiln validate --check-test-files
	- name: Check module documentation coverage
	run: cargo-kiln validate --check-docs
	- name: Check code formatting
	run: cargo fmt --all -- --check
	continue-on-error: true # Temporarily allow failures due to rustfmt crash bug
	- name: Run clippy checks
	# Note: Using --lib --bins only (not --all-targets) to skip examples/tests that have outdated API
	# continue-on-error: true due to occasional compiler panics in CI environment
	run: cargo clippy --workspace --lib --bins -- -D warnings
	continue-on-error: true
	- name: Check for WASI stub implementations in engine (architectural invariant)
	run: \|
	# Engine must NOT contain hardcoded WASI function implementations
	# Per CLAUDE.md: Engine has ZERO WASI-specific stub code - all dispatch goes through kiln-wasi
	# Pattern matches: match arms like ("wasi:cli/stdout", "get-stdout") => { ... }
	if grep -nE '^\s*\("wasi:' kiln-runtime/src/stackless/engine.rs; then
	echo "ERROR: Hardcoded WASI function implementations found in engine.rs"
	echo "All WASI dispatch must go through kiln-wasi/src/dispatcher.rs"
	echo "Engine should only use WasiDispatcher, not implement WASI functions directly"
	exit 1
	fi
	echo "Engine architecture check passed - no hardcoded WASI stubs in engine"

	core_tests_and_analysis:
	name: Core Tests, Analysis & Coverage
	runs-on: ubuntu-latest
	# This job runs on push, PR, and all manual triggers (regardless of input)
	steps:
	- uses: actions/checkout@v5
	- name: Cargo Cache
	uses: actions/cache@v5
	with:
	path: \|
	~/.cargo/bin/
	~/.cargo/registry/index/
	~/.cargo/registry/cache/
	~/.cargo/git/db/
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	- name: Dagger Engine Cache
	uses: actions/cache@v5
	with:
	path: ~/.cache/dagger
	key: ${{ runner.os }}-dagger-engine
	- uses: actions-rs/toolchain@v1
	with:
	profile: minimal
	toolchain: stable # For cargo-kiln. Nightly for UDeps should be handled internally.
	override: true
	components: llvm-tools-preview # For coverage
	- name: Install and setup cargo-kiln with tools
	run: \|
	cargo build --package cargo-kiln
	cargo install --path cargo-kiln --force
	cargo-kiln setup --all # Setup all required tools for testing and analysis
	- name: Run Tests
	run: cargo-kiln test
	- name: Run Code Validation Checks
	run: cargo-kiln validate --all
	- name: Check Unused Dependencies
	run: cargo-kiln check --strict
	- name: Run Security Audit
	run: cargo-kiln verify --asil c
	- name: Run Coverage Tests
	run: cargo-kiln coverage --html # This should produce lcov.info and junit.xml
	- name: Run Basic Safety Checks
	run: \|
	cargo test -p kiln-foundation asil_testing -- --nocapture \|\| true
	cargo-kiln verify --asil c \|\| true
	- name: Upload coverage reports to Codecov
	uses: codecov/codecov-action@v5
	with:
	token: ${{ secrets.CODECOV_TOKEN }}
	files: \|
	./target/coverage/lcov.info
	./target/coverage/cobertura.xml
	fail_ci_if_error: true
	- name: Upload test results to Codecov (JUnit)
	if: ${{ !cancelled() }}
	uses: codecov/test-results-action@v1
	with:
	token: ${{ secrets.CODECOV_TOKEN }}
	files: ./target/coverage/junit.xml # Ensure this path is correct

	safety_verification:
	name: SCORE-Inspired Safety Verification
	runs-on: ubuntu-latest
	# Run safety verification on all pushes and PRs
	steps:
	- uses: actions/checkout@v5
	- name: Cargo Cache
	uses: actions/cache@v5
	with:
	path: \|
	~/.cargo/bin/
	~/.cargo/registry/index/
	~/.cargo/registry/cache/
	~/.cargo/git/db/
	target/
	key: ${{ runner.os }}-cargo-safety-${{ hashFiles('**/Cargo.lock') }}
	- uses: actions-rs/toolchain@v1
	with:
	profile: minimal
	toolchain: stable
	override: true
	- name: Install and setup cargo-kiln for safety verification
	run: \|
	cargo build --package cargo-kiln
	cargo install --path cargo-kiln --force
	cargo-kiln setup --check # Verify required tools for safety verification
	- name: Check Requirements File
	run: cargo-kiln verify --asil c
	continue-on-error: true
	- name: Initialize Requirements if Missing
	run: cargo-kiln verify --asil c # Requirements are initialized automatically
	if: failure() # Only run if check-requirements failed
	- name: Run ASIL Test Suite
	run: cargo test -p kiln-foundation asil_testing -- --nocapture
	continue-on-error: true
	- name: Generate Comprehensive Safety Report (JSON)
	run: cargo-kiln verify --asil d --detailed > safety-verification-full.json
	- name: Generate Comprehensive Safety Report (HTML)
	run: cargo-kiln verify --asil d --detailed # HTML report generated automatically
	- name: Generate Safety Dashboard
	run: cargo-kiln verify --asil d --detailed # Dashboard included in detailed verification
	- name: Upload Safety Artifacts
	uses: actions/upload-artifact@v6
	with:
	name: safety-verification-artifacts
	path: \|
	safety-verification-full.json
	safety-verification-report.html
	docs/source/_generated_safety_summary.rst
	retention-days: 90
	- name: Safety Verification Gate
	run: cargo-kiln verify --asil d

	extended_static_analysis:
	name: Extended Static Analysis (Miri, Kani)
	runs-on: ubuntu-latest
	# Only run this job if the workflow was manually dispatched AND the input was true
	if: github.event_name == 'workflow_dispatch' && github.event.inputs.run_extended_analysis == true # Compare to boolean true
	needs: [ci_checks_and_docs, core_tests_and_analysis, safety_verification] # Optional: wait for other jobs
	steps:
	- uses: actions/checkout@v5
	- name: Cargo Cache
	uses: actions/cache@v5
	with:
	path: \|
	~/.cargo/bin/
	~/.cargo/registry/index/
	~/.cargo/registry/cache/
	~/.cargo/git/db/
	target/
	key: ${{ runner.os }}-cargo-extended-${{ hashFiles('**/Cargo.lock') }}
	- name: Dagger Engine Cache
	uses: actions/cache@v5
	with:
	path: ~/.cache/dagger
	key: ${{ runner.os }}-dagger-engine-extended
	- uses: actions-rs/toolchain@v1
	with:
	profile: minimal
	# Kani/Miri might need nightly or specific stable. Adjust as needed.
	# The cargo-kiln should ideally manage this internally.
	toolchain: stable # Or nightly if Kani/Miri need it directly for cargo-kiln compilation
	override: true
	# Add components if they can be installed via rustup and cargo-kiln doesn't handle it
	# components: miri, kani # (kani might need manual install steps)
	- name: Install and setup cargo-kiln for extended analysis
	run: \|
	cargo build --package cargo-kiln
	cargo install --path cargo-kiln --force
	cargo-kiln setup --all # Setup all tools including Kani and Miri
	# Run advanced static analysis
	- name: Run Miri Checks
	run: cargo-kiln verify --asil d --no-kani
	- name: Run Kani Checks
	run: cargo-kiln kani-verify --asil-profile d --verbose

	# Coverage job is still Linux-only as tarpaulin only supports Linux
	coverage:
	name: Code Coverage
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v5
	- uses: actions/cache@v5
	with:
	path: \|
	~/.cargo/bin/
	~/.cargo/registry/index/
	~/.cargo/registry/cache/
	~/.cargo/git/db/
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	- uses: dtolnay/rust-toolchain@stable
	with:
	components: llvm-tools-preview
	- name: Setup Rust targets
	run: rustup target add wasm32-unknown-unknown wasm32-wasip1 wasm32-wasip2 \|\| true
	- name: Install cargo-kiln
	run: cargo install --path cargo-kiln --force
	- name: Run coverage tests
	run: cargo-kiln coverage --html
	- name: Upload coverage reports to Codecov
	uses: codecov/codecov-action@v5
	with:
	token: ${{ secrets.CODECOV_TOKEN }}
	file: target/llvm-cov/lcov.info
	fail_ci_if_error: false

	audit:
	name: Security Audit (${{ matrix.os }})
	strategy:
	fail-fast: false # Don't stop all jobs if one fails
	matrix:
	os: [ubuntu-latest, macos-latest, windows-latest]
	include:
	- os: windows-latest
	continue-on-error: true # Allow Windows to fail without stopping the workflow
	runs-on: ${{ matrix.os }}
	continue-on-error: ${{ matrix.continue-on-error \|\| false }}
	steps:
	- uses: actions/checkout@v5
	- uses: actions-rs/audit-check@v1
	with:
	token: ${{ secrets.GITHUB_TOKEN }}

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(verus): verified StaticVec proofs pass via Bazel — 13 verified, … #362

Workflow file

feat(verus): verified StaticVec proofs pass via Bazel — 13 verified, … #362

Uh oh!

Workflow file for this run