feat: add GitHub Actions for CI verification workflow

.github/workflows/verilib-atomize.yml

@@ -0,0 +1,100 @@
+# Reusable workflow for verilib atomization of pure Rust projects
+#
+# Usage in any Rust project:
+#
+#   jobs:
+#     atomize:
+#       uses: beneficial-ai-foundation/verilib-cli/.github/workflows/verilib-atomize.yml@v1
+#       with:
+#         project-path: .
+#       secrets:
+#         VERILIB_API_KEY: ${{ secrets.VERILIB_API_KEY }}
+
+name: verilib Atomize
+
+on:
+  workflow_call:
+    inputs:
+      project-path:
+        description: 'Path to the Rust project'
+        required: false
+        type: string
+        default: '.'
+      deploy-enabled:
+        description: 'Enable deployment to verilib backend after atomization (requires VERILIB_API_KEY secret and repo-id)'
+        required: false
+        type: boolean
+        default: false
+      repo-id:
+        description: 'Verilib repository ID (used for deploy; optional if .verilib/config.json is in repo)'
+        required: false
+        type: string
+        default: ''
+    secrets:
+      VERILIB_API_KEY:
+        description: 'API key for verilib backend (required when deploy-enabled is true)'
+        required: false
+    outputs:
+      atoms-path:
+        description: 'Path to generated atoms.json'
+        value: ${{ jobs.atomize.outputs.atoms-path }}
+
+jobs:
+  atomize:
+    name: Atomize
+    runs-on: ubuntu-latest
+    outputs:
+      atoms-path: ${{ steps.verilib.outputs.atoms-path }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Run verilib atomize
+        id: verilib
+        uses: ./action/rust
+        with:
+          project-path: ${{ inputs.project-path }}
+
+      - name: Create summary
+        run: |
+          echo "## Atomization Results" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          ATOMS_PATH="${{ steps.verilib.outputs.atoms-path }}"
+          if [ -n "$ATOMS_PATH" ] && [ -f "$ATOMS_PATH" ]; then
+            ATOM_COUNT=$(jq 'length' "$ATOMS_PATH")
+            echo "**Atoms generated: ${ATOM_COUNT}**" >> $GITHUB_STEP_SUMMARY
+          else
+            echo "No atoms.json generated." >> $GITHUB_STEP_SUMMARY
+          fi
+
+      - name: Upload verilib artifacts
+        if: github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master')
+        uses: actions/upload-artifact@v4
+        with:
+          name: verilib-atoms
+          path: ${{ inputs.project-path }}/.verilib/atoms.json
+          retention-days: 30
+
+  # NOTE: This deploy job currently uses `verilib-cli reclone`, which tells the
+  # backend to re-clone and re-process the repo from scratch. This is a stopgap:
+  # it does NOT upload the .verilib/ artifacts generated by the atomize job above.
+  # A proper solution will use `verilib-cli deploy` (once wired into the CLI) to
+  # upload the generated artifacts directly, avoiding redundant server-side work.
+  # See: https://github.com/Beneficial-AI-Foundation/verilib-cli/issues/36
+  deploy:
+    name: Deploy to verilib
+    needs: atomize
+    if: |
+      inputs.deploy-enabled &&
+      github.event_name == 'push' &&
+      (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master')
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Deploy to verilib backend
+        uses: ./action/deploy
+        with:
+          api-key: ${{ secrets.VERILIB_API_KEY }}
+          repo-id: ${{ inputs.repo-id }}

.github/workflows/verilib-verify.yml

@@ -0,0 +1,128 @@
+# Reusable workflow for verilib verification
+#
+# Usage in any Verus project:
+#
+#   jobs:
+#     verify:
+#       uses: beneficial-ai-foundation/verilib-cli/.github/workflows/verilib-verify.yml@v1
+#       with:
+#         project-path: .
+#       secrets:
+#         VERILIB_API_KEY: ${{ secrets.VERILIB_API_KEY }}
+
+name: verilib Verify
+
+on:
+  workflow_call:
+    inputs:
+      project-path:
+        description: 'Path to the Verus project'
+        required: false
+        type: string
+        default: '.'
+      verus-version:
+        description: 'Verus version (default: auto-detect from Cargo.toml)'
+        required: false
+        type: string
+        default: ''
+      rust-version:
+        description: 'Rust toolchain version (default: auto-detect from Cargo.toml)'
+        required: false
+        type: string
+        default: ''
+      functions-to-track:
+        description: 'Path to functions_to_track.csv'
+        required: false
+        type: string
+        default: ''
+      deploy-enabled:
+        description: 'Enable deployment to verilib backend after verification (requires VERILIB_API_KEY secret and repo-id)'
+        required: false
+        type: boolean
+        default: false
+      repo-id:
+        description: 'Verilib repository ID (used for deploy; optional if .verilib/config.json is in repo)'
+        required: false
+        type: string
+        default: ''
+    secrets:
+      VERILIB_API_KEY:
+        description: 'API key for verilib backend (required when deploy-enabled is true)'
+        required: false
+    outputs:
+      verified-count:
+        description: 'Number of functions verified'
+        value: ${{ jobs.verify.outputs.verified-count }}
+      total-functions:
+        description: 'Total number of tracked functions'
+        value: ${{ jobs.verify.outputs.total-functions }}
+
+jobs:
+  verify:
+    name: Verify
+    runs-on: ubuntu-latest
+    outputs:
+      verified-count: ${{ steps.verilib.outputs.verified-count }}
+      total-functions: ${{ steps.verilib.outputs.total-functions }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Run verilib verification
+        id: verilib
+        uses: ./action
+        with:
+          project-path: ${{ inputs.project-path }}
+          # On push to main/master: generate mode
+          # On PR: check mode
+          mode: ${{ github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master') ? 'generate' : 'check' }}
+          verus-version: ${{ inputs.verus-version }}
+          rust-version: ${{ inputs.rust-version }}
+          functions-to-track: ${{ inputs.functions-to-track }}
+
+      - name: Create summary
+        run: |
+          echo "## Verification Results" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "| Metric | Value |" >> $GITHUB_STEP_SUMMARY
+          echo "|--------|-------|" >> $GITHUB_STEP_SUMMARY
+          echo "| Verified | ${{ steps.verilib.outputs.verified-count }} |" >> $GITHUB_STEP_SUMMARY
+          echo "| Total | ${{ steps.verilib.outputs.total-functions }} |" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          if [ "${{ steps.verilib.outputs.total-functions }}" -gt 0 ]; then
+            PERCENT=$(( ${{ steps.verilib.outputs.verified-count }} * 100 / ${{ steps.verilib.outputs.total-functions }} ))
+            echo "**Coverage: ${PERCENT}%**" >> $GITHUB_STEP_SUMMARY
+          fi
+
+      - name: Upload verilib artifacts
+        if: github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master')
+        uses: actions/upload-artifact@v4
+        with:
+          name: verilib-results
+          # Use the archive to avoid issues with special characters in filenames
+          path: ${{ steps.verilib.outputs.results-archive }}
+          retention-days: 30
+
+  # NOTE: This deploy job currently uses `verilib-cli reclone`, which tells the
+  # backend to re-clone and re-process the repo from scratch. This is a stopgap:
+  # it does NOT upload the .verilib/ artifacts generated by the verify job above.
+  # A proper solution will use `verilib-cli deploy` (once wired into the CLI) to
+  # upload the generated artifacts directly, avoiding redundant server-side work.
+  # See: https://github.com/Beneficial-AI-Foundation/verilib-cli/issues/36
+  deploy:
+    name: Deploy to verilib
+    needs: verify
+    if: |
+      inputs.deploy-enabled &&
+      github.event_name == 'push' &&
+      (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/master')
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Deploy to verilib backend
+        uses: ./action/deploy
+        with:
+          api-key: ${{ secrets.VERILIB_API_KEY }}
+          repo-id: ${{ inputs.repo-id }}

action/README.md

@@ -0,0 +1,124 @@
+# verilib-cli GitHub Action
+
+A GitHub Action to run the verilib verification workflow on Verus projects.
+
+## Features
+
+- Auto-detects Verus and Rust versions from `Cargo.toml`
+- Installs all required tooling (Verus, verus-analyzer, scip, probe-verus, verilib-cli)
+- Two modes: `check` (PR validation) and `generate` (full pipeline)
+- Caches installations for faster subsequent runs
+- Outputs verification statistics
+
+## Usage
+
+### Check Mode (for PRs)
+
+Validates that the project passes all verification checks without modifying files:
+
+```yaml
+- uses: beneficial-ai-foundation/verilib-cli/action@v1
+  with:
+    project-path: .
+    mode: check
+```
+
+This runs:
+- `verilib-cli atomize --check-only` - Fail if stubs out of sync
+- `verilib-cli specify --check-only` - Fail if specs missing certs
+- `verilib-cli verify --check-only` - Fail if any verification failures
+
+### Generate Mode (for main branch)
+
+Runs the full pipeline and generates/updates all verilib files:
+
+```yaml
+- uses: beneficial-ai-foundation/verilib-cli/action@v1
+  with:
+    project-path: .
+    mode: generate
+```
+
+This runs:
+- `verilib-cli create` - Initialize structure files
+- `verilib-cli atomize --update-stubs` - Enrich with SCIP data
+- `verilib-cli specify` - Certify all specifications
+- `verilib-cli verify` - Run Verus verification
+
+## Inputs
+
+| Input | Required | Default | Description |
+|-------|----------|---------|-------------|
+| `project-path` | Yes | `.` | Path to the Verus project directory |
+| `mode` | Yes | `check` | Mode: `check` or `generate` |
+| `verus-version` | No | auto-detect | Verus version (e.g., `1.85.0`) |
+| `rust-version` | No | auto-detect | Rust toolchain version |
+| `functions-to-track` | No | `functions_to_track.csv` | Path to functions CSV (for generate mode) |
+| `token` | No | `github.token` | GitHub token for API calls |
+
+## Outputs
+
+| Output | Description |
+|--------|-------------|
+| `verified-count` | Number of functions verified |
+| `total-functions` | Total number of tracked functions |
+| `results-path` | Path to `.verilib/` directory |
+| `results-archive` | Path to archived results (`verilib-results.tar.gz`) - use this for artifact upload |
+
+> **Note**: Use `results-archive` instead of `results-path` for artifact uploads. Function signatures may contain characters like `<` and `>` that are invalid for GitHub artifact paths.
+
+## Auto-Detection
+
+If `verus-version` or `rust-version` are not provided, the action looks for them in your project's `Cargo.toml`:
+
+```toml
+[package.metadata.verus]
+release = "1.85.0"
+rust-version = "nightly-2025-01-01"
+```
+
+## Complete Example
+
+```yaml
+name: Verification
+
+on:
+  pull_request:
+  push:
+    branches: [main]
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: beneficial-ai-foundation/verilib-cli/action@v1
+        id: verify
+        with:
+          project-path: .
+          mode: ${{ github.event_name == 'push' && 'generate' || 'check' }}
+
+      - name: Summary
+        run: |
+          echo "## Verification Results" >> $GITHUB_STEP_SUMMARY
+          echo "Verified: ${{ steps.verify.outputs.verified-count }} / ${{ steps.verify.outputs.total-functions }}" >> $GITHUB_STEP_SUMMARY
+
+      # Upload artifacts on main branch for future deploy
+      - uses: actions/upload-artifact@v4
+        if: github.ref == 'refs/heads/main'
+        with:
+          name: verilib-results
+          path: ${{ steps.verify.outputs.results-archive }}
+```
+
+## Requirements
+
+- Linux runner (ubuntu-latest recommended)
+- Project must be a valid Verus/Rust project
+- `functions_to_track.csv` required for generate mode
+- You must either provide versions via inputs or include `[package.metadata.verus]` in Cargo.toml; if neither is provided, the action will fail with an error during setup.
+
+## License
+
+MIT