feat: add GitHub Actions for CI verification workflow

[astefano]

Summary

Add reusable GitHub Actions workflows and composite actions for integrating verilib into any project's CI pipeline:

• Verus projects: full verification pipeline (create -> atomize -> specify -> verify) with check/generate modes
• Pure Rust projects: atomization only (atomize with rust-analyzer)
• Deploy: both workflows support an optional deploy step via verilib-cli reclone to trigger backend re-processing

Note on deploy: reclone is a stopgap -- it tells the backend to re-process from scratch rather than uploading the .verilib/ artifacts the CI just generated. A proper solution will use verilib-cli deploy once it's wired into the CLI (#36).

Files

File	Description
action/action.yml	Verus composite action (check/generate modes)
action/rust/action.yml	Pure Rust composite action (atomize only)
action/deploy/action.yml	Deploy composite action (reclone to backend)
.github/workflows/verilib-verify.yml	Reusable workflow for Verus projects
.github/workflows/verilib-atomize.yml	Reusable workflow for pure Rust projects
docs/GITHUB_ACTIONS_DESIGN.md	Design rationale and architecture decisions

Quick start

Verus project

jobs:
  verify:
    uses: beneficial-ai-foundation/verilib-cli/.github/workflows/verilib-verify.yml@v1
    with:
      project-path: .
      deploy-enabled: true
      repo-id: '42'
    secrets:
      VERILIB_API_KEY: ${{ secrets.VERILIB_API_KEY }}

See action/README.md for full details on modes, inputs, outputs, and what commands run.

Pure Rust project

jobs:
  atomize:
    uses: beneficial-ai-foundation/verilib-cli/.github/workflows/verilib-atomize.yml@v1
    with:
      project-path: .
      deploy-enabled: true
      repo-id: '42'
    secrets:
      VERILIB_API_KEY: ${{ secrets.VERILIB_API_KEY }}

See action/rust/README.md for full details.

Related issues

• Clean up dead code suppressed with #[allow(dead_code)] #36 -- Wire up verilib-cli deploy to replace reclone stopgap
• Add GitHub Actions workflow for pure Rust projects (atomize-only) #38 -- Add separate workflow for pure Rust projects (closes)

[Copilot]

Pull request overview

This pull request introduces GitHub Actions integration for verilib-cli, enabling Verus projects to integrate verification workflows into their CI/CD pipelines. The implementation provides a composite action with two modes (check and generate) and a reusable workflow that automatically selects the appropriate mode based on the triggering event. The design is well-documented with comprehensive rationale and acknowledges that the deploy functionality is not yet available.

Changes:

• Added composite GitHub Action supporting check mode (PR validation) and generate mode (full pipeline execution)
• Created reusable workflow for easy integration into Verus projects
• Documented design decisions, architecture, and implementation status
• Added placeholder for future deploy action (pending CLI command integration)

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 27 comments.

Show a summary per file

File	Description
docs/GITHUB_ACTIONS_DESIGN.md	Comprehensive design document explaining architecture decisions, workflow patterns, and implementation status
action/action.yml	Main composite action with auto-detection of versions, tool installation, and dual-mode operation
action/README.md	User-facing documentation with usage examples and input/output specifications
.github/workflows/verilib-verify.yml	Reusable workflow template for external Verus projects with automatic mode selection
action/deploy/README.md	Placeholder documentation for future deploy action functionality

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 5 out of 5 changed files in this pull request and generated 17 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[astefano]

Copilot Review Triage

Fixed (commit d423785)

Comment	Fix
Trailing whitespace in action.yml	Stripped all trailing whitespace
probe-verus always reinstalls with --force	Added cache check (command -v) like verus-analyzer/scip
verilib-cli always reinstalls with --force	Added cache check (command -v) like verus-analyzer/scip
uv install doesn't verify success	Added command -v check after install

Already addressed in prior commits

Comment	Status
Deploy job commented out / inputs unused	Uncommented in 568602e — deploy job now active
UUOC with jq (cat | jq)	Already fixed — current code passes file directly to jq
Missing set -euo pipefail	Already present on line 66
Archive name uniqueness	Already uses $RANDOM/timestamps (from a8c5c74)
Design doc: deploy not wired	Updated in 568602e

Won't fix (incorrect or not applicable)

• ${{ github.token }} invalid as default: This is valid in composite actions (docs).
• Bearer vs token auth for GitHub API: Authorization: Bearer works with GITHUB_TOKEN and is the recommended format.
• Division by zero in coverage %: The arithmetic is inside if [ "$total" -gt 0 ], so it only runs when safe.
• Ternary expression clarity: The suggestion is identical to the existing code.
• sudo mv to /usr/local/bin: Standard practice on GitHub-hosted runners; all steps already run sudo apt-get for other installs.
• Platform-specific downloads: README documents "Linux runner (ubuntu-latest recommended)" as a requirement.
• Auto-certify all specs in CI: Intentional design for generate mode — CI has no interactive terminal.
• ./action reference in reusable workflow: Correct — reusable workflows resolve ./ relative to their own repo.
• Check CLI utilities (jq, wget, etc.): Standard on ubuntu-latest; documented in requirements.
• Cache key version conflicts: Key includes verus version + Cargo.lock hash, providing reasonable invalidation.

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated 8 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 10 out of 10 changed files in this pull request and generated 12 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 10 out of 10 changed files in this pull request and generated 15 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[astefano]

Copilot Review Triage (Rounds 3–5)

Fixed (this commit)

Comment	Fix
github.event_name checks in reusable workflows (deploy conditions, artifact upload, auto mode detection)	Replaced with github.ref checks — event_name is always workflow_call inside reusable workflows
Feature branch refs @la/create_github_actions	Updated to @main in both verilib-verify.yml and verilib-atomize.yml
scip installed to /usr/local/bin (not cached)	Now installed to ~/.cargo/bin (covered by actions/cache) in both action.yml and rust/action.yml
dtolnay/rust-toolchain@master unpinned	Changed to @stable
Version detection errors when inputs provided	Now skips Cargo.toml metadata discovery when both verus-version and rust-version inputs are provided
repo-id marked required: true in deploy action	Changed to required: false with runtime validation — fails with clear error if neither repo-id input nor .verilib/config.json provides a repo ID
--force in deploy action cargo install	Removed; cache check (command -v) handles this
Secret name typo VERRILIB_CLI_AUTH_KEY in test-deploy.yml	Fixed to VERILIB_API_KEY
functions-to-track listed in README but not in action.yml	Removed from README inputs table and requirements
results-archive output description in README	Updated to reflect actual naming (includes run ID and timestamp)

Won't fix (incorrect or not applicable)

• Hyphenated output names in expressions (verified-count, total-functions, results-archive, atoms-path): GitHub Actions property dereference syntax supports hyphens in property names with dot notation. The - is only an operator in arithmetic contexts, not in property access.
• ${{ github.token }} invalid as default: Valid in composite actions per docs.
• Bearer auth format: Correct for GITHUB_TOKEN per REST API docs.
• ./action in reusable workflows: Workflows already use beneficial-ai-foundation/verilib-cli/action@ref (full path), not ./action.
• Unpinned cargo install for probe-verus/verilib-cli: No stable release tags exist yet; will pin when tagging releases.
• verus-analyzer from releases/latest: The action uses the verus version tag from steps.versions.outputs.verus_version when available.
• Platform-specific downloads: README documents "Linux runner (ubuntu-latest recommended)" as a requirement.
• Auto-certify specs in CI: Intentional — CI has no interactive terminal; generate mode is designed for automated pipelines.
• test-deploy.yml temporary: Intentional; workflow_dispatch only, will remove after integration testing.
• functions_to_track.csv required: verilib-cli create generates tracked_functions.csv via probe-verus tracked-csv; external CSV not required.
• Division by zero: Already gated by if [ "$total" -gt 0 ].
• CLI utilities check (jq, wget, etc.): Standard on ubuntu-latest; documented in requirements.

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated 7 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The deploy step here also uses @main, which defeats pinning for consumers of the reusable workflow. Please pin this to the same ref as the workflow release (e.g., @v1) or keep it otherwise in lockstep with the workflow ref.

[Copilot]

The Cargo.toml metadata discovery only checks the root and one level of subdirectories ($PROJECT_PATH/*/Cargo.toml), but many workspaces nest members deeper (e.g., crates/foo/Cargo.toml). This can incorrectly error even when [package.metadata.verus] exists. Consider using find (bounded depth) or parsing the workspace members list to locate the correct Cargo.toml reliably.

[Copilot]

probe-verus is installed from a moving git target (cargo install --git ...) and is then reused from ~/.cargo/bin if present. This can produce non-reproducible runs where a workflow pinned to a tag ends up using whatever probe-verus happened to be cached. Pin the install to a specific ref/tag/sha (and incorporate it into the cache key) or add a version check + reinstall when it doesn’t match the expected version.

Suggested change

	run: |
	if command -v probe-verus &> /dev/null; then
	echo "probe-verus already installed (from cache)"
	probe-verus --version
	else
	echo "Installing probe-verus..."
	cargo install --git https://github.com/Beneficial-AI-Foundation/probe-verus
	probe-verus --version || echo "probe-verus installed"
	fi
	env:
	PROBE_VERUS_VERSION: "0.1.0"
	run: |
	echo "Expected probe-verus version: $PROBE_VERUS_VERSION"
	if command -v probe-verus &> /dev/null; then
	INSTALLED_PROBE_VERUS_VERSION=$(probe-verus --version | awk '{print $NF}')
	echo "probe-verus already installed (from cache): $INSTALLED_PROBE_VERUS_VERSION"
	if [ "$INSTALLED_PROBE_VERUS_VERSION" != "$PROBE_VERUS_VERSION" ]; then
	echo "probe-verus version mismatch (expected $PROBE_VERUS_VERSION, found $INSTALLED_PROBE_VERUS_VERSION); reinstalling..."
	cargo install --git https://github.com/Beneficial-AI-Foundation/probe-verus --tag "v$PROBE_VERUS_VERSION" --force
	else
	echo "probe-verus version matches expected version ($PROBE_VERUS_VERSION)"
	fi
	else
	echo "Installing probe-verus..."
	cargo install --git https://github.com/Beneficial-AI-Foundation/probe-verus --tag "v$PROBE_VERUS_VERSION"
	fi
	probe-verus --version || echo "probe-verus installed"

[Copilot]

This action installs probe-verus from an unpinned git source and then skips installation if it’s already present in the cached ~/.cargo/bin. That can make runs non-reproducible (especially when consumers pin the action version) and can lead to subtle incompatibilities. Pin to a specific ref/tag/sha (and include it in the cache key) or check the installed version and force reinstall when it differs.

[Copilot]

verilib-cli is installed from the repo’s default branch via cargo install --git ...verilib-cli and then reused from cache if present. This breaks version pinning: a workflow/action pinned to a tag/sha can still execute a different verilib-cli than intended (or a stale cached one). Prefer installing from the action checkout (via $GITHUB_ACTION_PATH) or pin the git ref/tag/sha explicitly and ensure the cache key enforces that version.

[Copilot]

Same versioning/reproducibility concern as the other actions: verilib-cli is installed from an unpinned git source and then reused if present in cached ~/.cargo/bin, which can cause deploy runs to use a different CLI version than the action/workflow version a consumer pinned. Prefer installing from the action’s own checkout (via $GITHUB_ACTION_PATH) or pin the git ref/tag/sha and make the cache key include it (or force reinstall when mismatched).

[Copilot]

Same issue as the verify job: the deploy job uses beneficial-ai-foundation/verilib-cli/action/deploy@main, so consumers pinning this reusable workflow to a tag/sha will still execute whatever is currently on main. Please pin this to the same ref as the reusable workflow release (e.g., @v1) or otherwise keep the action reference in lockstep with the workflow ref.