ci: pilot bounded ESBMC verification

.github/CODEOWNERS

@@ -0,0 +1,5 @@
+# Formal policy and its execution boundary require explicit pilot ownership.
+/formal/ @dusterbloom
+/scripts/formal*.py @dusterbloom
+/scripts/formal*.sh @dusterbloom
+/.github/workflows/formal*.yml @dusterbloom

.github/workflows/ci.yml

@@ -79,12 +79,16 @@ jobs:
             -DCMAKE_BUILD_TYPE=Release
           cmake --build build --target \
             test_dflash test_generate test_flash_attn_sparse test_server_unit \
+            test_prefix_cache_state test_full_prefix_cache_state test_spec_commit \
+            test_kvflash_residency_map \
             test_deepseek4_unit -j$(nproc)
 
       - name: Run C++ server unit tests
         run: |
           cd server/build
-          ctest --output-on-failure -R "server_unit|deepseek4_unit" --no-tests=error
+          ctest --output-on-failure \
+            -R "server_unit|prefix_cache_state|spec_commit|kvflash_residency_map|deepseek4_unit" \
+            --no-tests=error
 
       - name: Populate venv with cu128 torch + setuptools
         # First pass: install the workspace's default deps. dflash declares

.github/workflows/formal-ai.yml

@@ -0,0 +1,370 @@
+name: Formal AI Candidate
+
+on:
+  workflow_run:
+    workflows: ["Formal Verification"]
+    types: [completed]
+  workflow_dispatch:
+    inputs:
+      run_id:
+        description: Formal Verification workflow run ID
+        required: true
+        type: string
+
+permissions:
+  actions: read
+  contents: read
+
+concurrency:
+  group: formal-ai-${{ github.event.workflow_run.id || inputs.run_id }}
+  cancel-in-progress: false
+
+jobs:
+  inspect:
+    name: inspect-deterministic-result
+    runs-on: ubuntu-latest
+    outputs:
+      run_id: ${{ steps.source.outputs.run_id }}
+      authorized: ${{ steps.report.outputs.authorized }}
+      has_counterexample: ${{ steps.report.outputs.has_counterexample }}
+      has_coverage_gap: ${{ steps.report.outputs.has_coverage_gap }}
+      head_repository: ${{ steps.report.outputs.head_repository }}
+      head_sha: ${{ steps.report.outputs.head_sha }}
+    steps:
+      - id: source
+        name: Resolve deterministic run
+        shell: bash
+        run: |
+          if [[ "$GITHUB_EVENT_NAME" == "workflow_dispatch" ]]; then
+            echo "run_id=${{ inputs.run_id }}" >> "$GITHUB_OUTPUT"
+            echo "manual=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "run_id=${{ github.event.workflow_run.id }}" \
+              >> "$GITHUB_OUTPUT"
+            echo "manual=false" >> "$GITHUB_OUTPUT"
+          fi
+
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4
+        with:
+          name: formal-results
+          path: incoming
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          run-id: ${{ steps.source.outputs.run_id }}
+
+      - id: report
+        name: Authenticate source and classify evidence
+        env:
+          MANUAL_DISPATCH: ${{ steps.source.outputs.manual }}
+          EXPECTED_REPOSITORY: ${{ github.repository }}
+        shell: bash
+        run: |
+          python3 -c '
+          import json
+          import os
+          import re
+          from pathlib import Path
+
+          def exactly_one(name):
+              matches = list(Path("incoming").rglob(name))
+              if len(matches) != 1:
+                  raise SystemExit(
+                      f"expected one {name}, found {len(matches)}"
+                  )
+              return matches[0]
+
+          source = json.loads(
+              exactly_one("source.json").read_text(encoding="utf-8")
+          )
+          report = json.loads(
+              exactly_one("report.json").read_text(encoding="utf-8")
+          )
+          expected = os.environ["EXPECTED_REPOSITORY"]
+          sha = re.compile(r"^[0-9a-f]{40}$")
+          if source.get("repository") != expected:
+              raise SystemExit("formal source repository mismatch")
+          if not sha.fullmatch(source.get("base_sha", "")):
+              raise SystemExit("formal source has invalid base SHA")
+          if not sha.fullmatch(source.get("head_sha", "")):
+              raise SystemExit("formal source has invalid head SHA")
+          if report.get("base_sha") != source["base_sha"]:
+              raise SystemExit("formal report base SHA mismatch")
+          if report.get("head_sha") != source["head_sha"]:
+              raise SystemExit("formal report head SHA mismatch")
+          head_repository = source.get("head_repository")
+          if not isinstance(head_repository, str):
+              raise SystemExit("formal source has invalid head repository")
+
+          statuses = {
+              item.get("status") for item in report.get("results", [])
+          }
+          failures = list(
+              Path("incoming").rglob("failure-bundle-*.tar.gz")
+          )
+          gaps = list(
+              Path("incoming").rglob("coverage-gap-bundle-*.tar.gz")
+          )
+          has_counterexample = (
+              "counterexample" in statuses and bool(failures)
+          )
+          has_coverage_gap = "coverage_gap" in statuses and bool(gaps)
+          manual = os.environ["MANUAL_DISPATCH"] == "true"
+          authorized = manual or head_repository == expected
+
+          values = {
+              "authorized": str(authorized).lower(),
+              "has_counterexample": str(has_counterexample).lower(),
+              "has_coverage_gap": str(has_coverage_gap).lower(),
+              "head_repository": head_repository,
+              "head_sha": source["head_sha"],
+          }
+          with open(
+              os.environ["GITHUB_OUTPUT"], "a", encoding="utf-8"
+          ) as output:
+              for key, value in values.items():
+                  output.write(f"{key}={value}\n")
+          '
+
+  repair-candidate:
+    name: approval-only-repair
+    needs: inspect
+    if: >-
+      needs.inspect.outputs.authorized == 'true' &&
+      needs.inspect.outputs.has_counterexample == 'true'
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    environment: formal-ai
+    steps:
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4
+        with:
+          name: formal-results
+          path: incoming
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          run-id: ${{ needs.inspect.outputs.run_id }}
+
+      - id: propose
+        name: Generate bounded repair without executing it
+        continue-on-error: true
+        env:
+          OPENAI_API_KEY: ${{ secrets.ZAI_API_KEY || secrets.OPENAI_API_KEY }}
+          OPENAI_API_BASE: ${{ vars.FORMAL_AI_BASE_URL || 'https://api.z.ai/api/paas/v4/' }}
+          FORMAL_AI_MODEL: ${{ vars.FORMAL_AI_MODEL || 'openai:glm-5' }}
+          REPAIR_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597
+        run: |
+          bundle="$(
+            find incoming -type f -name "failure-bundle-*.tar.gz" \
+              -print -quit
+          )"
+          if [[ -z "$bundle" ]]; then
+            echo "No failure bundle was present." >&2
+            exit 21
+          fi
+          mkdir -p proposed
+          bundle_relative="${bundle#incoming/}"
+          docker run --rm \
+            --read-only \
+            --cap-drop ALL \
+            --security-opt no-new-privileges \
+            --pids-limit 512 \
+            --memory 6g \
+            --cpus 2 \
+            --user "$(id -u):$(id -g)" \
+            --tmpfs /tmp:rw,nosuid,nodev,size=1g \
+            --env OPENAI_API_KEY \
+            --env OPENAI_API_BASE \
+            --env XDG_CACHE_HOME=/tmp/cache \
+            --env XDG_CONFIG_HOME=/tmp/config \
+            --volume "$GITHUB_WORKSPACE/incoming:/input:ro" \
+            --volume "$GITHUB_WORKSPACE/proposed:/output:rw" \
+            "$REPAIR_IMAGE" propose \
+            --bundle "/input/$bundle_relative" \
+            --model "$FORMAL_AI_MODEL" \
+            --out /output
+
+      - id: validate
+        name: Reverify repair without network or credentials
+        if: steps.propose.outcome == 'success'
+        continue-on-error: true
+        env:
+          REPAIR_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597
+        run: |
+          bundle="$(
+            find incoming -type f -name "failure-bundle-*.tar.gz" \
+              -print -quit
+          )"
+          bundle_relative="${bundle#incoming/}"
+          mkdir -p candidate
+          if [[ -f proposed/diagnosis.md ]]; then
+            cp proposed/diagnosis.md candidate/diagnosis.md
+          fi
+          docker run --rm \
+            --network none \
+            --read-only \
+            --cap-drop ALL \
+            --security-opt no-new-privileges \
+            --pids-limit 512 \
+            --memory 6g \
+            --cpus 2 \
+            --user "$(id -u):$(id -g)" \
+            --tmpfs /tmp:rw,exec,nosuid,nodev,size=1g \
+            --volume "$GITHUB_WORKSPACE/incoming:/input:ro" \
+            --volume "$GITHUB_WORKSPACE/proposed:/proposal:ro" \
+            --volume "$GITHUB_WORKSPACE/candidate:/output:rw" \
+            "$REPAIR_IMAGE" validate \
+            --bundle "/input/$bundle_relative" \
+            --patch /proposal/candidate.patch \
+            --out /output
+
+      - name: Publish advisory repair summary
+        if: always()
+        run: |
+          {
+            echo "# Formal AI repair candidate"
+            echo
+            echo "This lane is advisory and cannot write to the repository."
+            echo "Proposal: \`${{ steps.propose.outcome }}\`"
+            echo "Secretless validation: \`${{ steps.validate.outcome }}\`"
+          } >> "$GITHUB_STEP_SUMMARY"
+
+      - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        if: always()
+        with:
+          name: formal-ai-repair-${{ needs.inspect.outputs.run_id }}
+          path: candidate/
+          if-no-files-found: warn
+          retention-days: 14
+
+  contract-candidate:
+    name: approval-only-contract
+    needs: inspect
+    if: >-
+      needs.inspect.outputs.authorized == 'true' &&
+      needs.inspect.outputs.has_coverage_gap == 'true'
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    environment: formal-ai
+    steps:
+      - name: Checkout exact head without credentials
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        with:
+          repository: ${{ needs.inspect.outputs.head_repository }}
+          ref: ${{ needs.inspect.outputs.head_sha }}
+          path: head
+          fetch-depth: 0
+          persist-credentials: false
+
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4
+        with:
+          name: formal-results
+          path: incoming
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          run-id: ${{ needs.inspect.outputs.run_id }}
+
+      - id: propose
+        name: Draft bounded contracts without executing them
+        continue-on-error: true
+        env:
+          OPENAI_API_KEY: ${{ secrets.ZAI_API_KEY || secrets.OPENAI_API_KEY }}
+          OPENAI_API_BASE: ${{ vars.FORMAL_AI_BASE_URL || 'https://api.z.ai/api/paas/v4/' }}
+          FORMAL_AI_MODEL: ${{ vars.FORMAL_AI_MODEL || 'openai:glm-5' }}
+          REPAIR_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597
+        run: |
+          mkdir -p proposed
+          successes=0
+          while IFS= read -r bundle; do
+            key="$(basename "$bundle" .tar.gz)"
+            bundle_relative="${bundle#incoming/}"
+            mkdir -p "proposed/$key"
+            if docker run --rm \
+              --read-only \
+              --cap-drop ALL \
+              --security-opt no-new-privileges \
+              --pids-limit 512 \
+              --memory 6g \
+              --cpus 2 \
+              --user "$(id -u):$(id -g)" \
+              --tmpfs /tmp:rw,nosuid,nodev,size=1g \
+              --env OPENAI_API_KEY \
+              --env OPENAI_API_BASE \
+              --env XDG_CACHE_HOME=/tmp/cache \
+              --env XDG_CONFIG_HOME=/tmp/config \
+              --volume "$GITHUB_WORKSPACE/incoming:/input:ro" \
+              --volume "$GITHUB_WORKSPACE/proposed/$key:/output:rw" \
+              "$REPAIR_IMAGE" propose-contract \
+              --bundle "/input/$bundle_relative" \
+              --model "$FORMAL_AI_MODEL" \
+              --out /output;
+            then
+              successes=$((successes + 1))
+            fi
+          done < <(
+            find incoming -type f \
+              -name "coverage-gap-bundle-*.tar.gz" |
+              sort |
+              head -4
+          )
+          [[ "$successes" -gt 0 ]]
+
+      - id: validate
+        name: Validate draft contracts without network or credentials
+        if: steps.propose.outcome == 'success'
+        continue-on-error: true
+        env:
+              REPAIR_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597
+        run: |
+          mkdir -p candidate
+          ready=0
+          while IFS= read -r bundle; do
+            key="$(basename "$bundle" .tar.gz)"
+            bundle_relative="${bundle#incoming/}"
+            [[ -d "proposed/$key" ]] || continue
+            mkdir -p "candidate/$key"
+            if docker run --rm \
+              --network none \
+              --read-only \
+              --cap-drop ALL \
+              --security-opt no-new-privileges \
+              --pids-limit 512 \
+              --memory 6g \
+              --cpus 2 \
+              --user "$(id -u):$(id -g)" \
+              --tmpfs /tmp:rw,exec,nosuid,nodev,size=1g \
+              --volume "$GITHUB_WORKSPACE/incoming:/input:ro" \
+              --volume "$GITHUB_WORKSPACE/proposed/$key:/proposal:ro" \
+              --volume "$GITHUB_WORKSPACE/head:/workspace:ro" \
+              --volume "$GITHUB_WORKSPACE/candidate/$key:/output:rw" \
+              "$REPAIR_IMAGE" validate-contract \
+              --bundle "/input/$bundle_relative" \
+              --proposal-dir /proposal \
+              --workspace /workspace \
+              --out /output;
+            then
+              cp "proposed/$key/proposal.json" "candidate/$key/"
+              cp "proposed/$key/contract.cpp" "candidate/$key/"
+              ready=$((ready + 1))
+            fi
+          done < <(
+            find incoming -type f \
+              -name "coverage-gap-bundle-*.tar.gz" |
+              sort |
+              head -4
+          )
+          [[ "$ready" -gt 0 ]]
+
+      - name: Publish advisory contract summary
+        if: always()
+        run: |
+          {
+            echo "# Formal AI contract proposals"
+            echo
+            echo "AI proposals are advisory and never satisfy the gate."
+            echo "Proposal: \`${{ steps.propose.outcome }}\`"
+            echo "Secretless validation: \`${{ steps.validate.outcome }}\`"
+          } >> "$GITHUB_STEP_SUMMARY"
+
+      - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        if: always()
+        with:
+          name: formal-ai-contract-${{ needs.inspect.outputs.run_id }}
+          path: candidate/
+          if-no-files-found: warn
+          retention-days: 14