diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 000000000..a322472e8 --- /dev/null +++ b/.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 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3cfe3e446..6bcfb6bc3 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/.github/workflows/formal-ai.yml b/.github/workflows/formal-ai.yml new file mode 100644 index 000000000..6609e4883 --- /dev/null +++ b/.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 diff --git a/.github/workflows/formal-nightly.yml b/.github/workflows/formal-nightly.yml new file mode 100644 index 000000000..28033543d --- /dev/null +++ b/.github/workflows/formal-nightly.yml @@ -0,0 +1,168 @@ +name: Formal Verification Nightly + +on: + schedule: + - cron: "17 3 * * *" + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: formal-nightly + cancel-in-progress: true + +jobs: + verify-nightly: + name: verify-nightly + runs-on: ubuntu-latest + timeout-minutes: 45 + steps: + - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + with: + fetch-depth: 0 + persist-credentials: false + + - id: plan + name: Generate extended base-approved plan + continue-on-error: true + env: + VERIFIER_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e + REPAIR_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597 + REVISION: ${{ github.sha }} + run: | + readarray -t policy_images < <( + git show "$REVISION:formal/contracts/registry.toml" | + python3 -c ' + import sys + import tomllib + toolchain = tomllib.loads(sys.stdin.read())["toolchain"] + print(toolchain["verifier_image"]) + print(toolchain["repair_image"]) + ' + ) + if [[ "${#policy_images[@]}" -ne 2 ]] || + [[ "${policy_images[0]}" != "$VERIFIER_IMAGE" ]] || + [[ "${policy_images[1]}" != "$REPAIR_IMAGE" ]]; + then + echo "Nightly images do not match trusted policy." >&2 + exit 13 + fi + mkdir -p .formal-plan + docker run --rm \ + --network none \ + --read-only \ + --cap-drop ALL \ + --security-opt no-new-privileges \ + --pids-limit 256 \ + --memory 2g \ + --cpus 1 \ + --user "$(id -u):$(id -g)" \ + --tmpfs /tmp:rw,nosuid,nodev,size=128m \ + --volume "$GITHUB_WORKSPACE:/workspace:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-plan:/plan:rw" \ + --workdir /workspace \ + "$VERIFIER_IMAGE" plan \ + --workspace /workspace \ + --base-policy formal/contracts/registry.toml \ + --base-sha "$REVISION" \ + --head-sha "$REVISION" \ + --mode nightly \ + --out /plan + + - id: formal + name: Run extended generated contracts + if: steps.plan.outcome == 'success' + continue-on-error: true + env: + VERIFIER_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e + run: | + mkdir -p .formal-results + 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=512m \ + --volume "$GITHUB_WORKSPACE:/workspace:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-plan:/plan:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-results:/results:rw" \ + --workdir /workspace \ + "$VERIFIER_IMAGE" verify \ + --plan /plan/plan.json \ + --workspace /workspace \ + --generated-root /plan \ + --out /results + + - id: legacy + name: Run legacy nightly capsules for comparison + continue-on-error: true + env: + VERIFIER_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e + run: | + mkdir -p .formal-legacy-results + 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,nosuid,nodev,size=512m \ + --volume "$GITHUB_WORKSPACE:/workspace:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-legacy-results:/results:rw" \ + --workdir /workspace \ + "$VERIFIER_IMAGE" verify \ + --manifest /workspace/formal/manifest.toml \ + --mode nightly \ + --out /results + + - name: Publish formal summary + if: always() + run: | + if [[ -f .formal-results/summary.md ]]; then + cat .formal-results/summary.md >> "$GITHUB_STEP_SUMMARY" + else + echo "Nightly plan did not produce a summary." \ + >> "$GITHUB_STEP_SUMMARY" + fi + echo "Legacy comparison: \`${{ steps.legacy.outcome }}\`" \ + >> "$GITHUB_STEP_SUMMARY" + + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: always() + with: + name: formal-nightly-results + path: | + .formal-plan/ + .formal-results/ + .formal-legacy-results/ + include-hidden-files: true + if-no-files-found: error + retention-days: 30 + + - name: Enforce extended result + if: >- + steps.plan.outcome != 'success' || + steps.formal.outcome != 'success' + run: exit 1 + + mutation-sensitivity: + name: mutation-sensitivity + needs: verify-nightly + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + with: + fetch-depth: 0 + persist-credentials: false + + - name: Require the historical call-site regression to fail + run: scripts/formal_mutation_test.sh diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml new file mode 100644 index 000000000..306ce3ae5 --- /dev/null +++ b/.github/workflows/formal.yml @@ -0,0 +1,333 @@ +name: Formal Verification + +on: + pull_request_target: + types: [opened, synchronize, reopened] + merge_group: + types: [checks_requested] + push: + branches: [main] + workflow_dispatch: + inputs: + base_sha: + description: Trusted policy/base commit (defaults to head) + required: false + type: string + head_sha: + description: Production commit to verify (defaults to dispatched ref) + required: false + type: string + mode: + description: Verification scope + required: true + default: all + type: choice + options: [pr, all, nightly] + +permissions: + contents: read + +concurrency: + group: formal-${{ github.workflow }}-${{ github.event.pull_request.number || github.event.merge_group.head_sha || github.ref }} + cancel-in-progress: true + +jobs: + verify: + name: verify + runs-on: ubuntu-latest + timeout-minutes: 20 + outputs: + base_sha: ${{ steps.scope.outputs.base_sha }} + head_sha: ${{ steps.scope.outputs.head_sha }} + head_repository: ${{ steps.scope.outputs.head_repository }} + mode: ${{ steps.scope.outputs.mode }} + steps: + - id: scope + name: Resolve trusted policy and production revisions + shell: bash + env: + EVENT_NAME: ${{ github.event_name }} + PR_BASE_SHA: ${{ github.event.pull_request.base.sha }} + PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }} + PR_HEAD_REPOSITORY: ${{ github.event.pull_request.head.repo.full_name }} + GROUP_BASE_SHA: ${{ github.event.merge_group.base_sha }} + GROUP_HEAD_SHA: ${{ github.event.merge_group.head_sha }} + INPUT_BASE_SHA: ${{ inputs.base_sha }} + INPUT_HEAD_SHA: ${{ inputs.head_sha }} + INPUT_MODE: ${{ inputs.mode }} + EVENT_SHA: ${{ github.sha }} + CURRENT_REPOSITORY: ${{ github.repository }} + run: | + case "$EVENT_NAME" in + pull_request_target) + base_sha="$PR_BASE_SHA" + head_sha="$PR_HEAD_SHA" + head_repository="$PR_HEAD_REPOSITORY" + mode=pr + ;; + merge_group) + base_sha="$GROUP_BASE_SHA" + head_sha="$GROUP_HEAD_SHA" + head_repository="$CURRENT_REPOSITORY" + mode=pr + ;; + workflow_dispatch) + head_sha="${INPUT_HEAD_SHA:-$EVENT_SHA}" + base_sha="${INPUT_BASE_SHA:-$head_sha}" + head_repository="$CURRENT_REPOSITORY" + mode="$INPUT_MODE" + ;; + *) + base_sha="$EVENT_SHA" + head_sha="$EVENT_SHA" + head_repository="$CURRENT_REPOSITORY" + mode=all + ;; + esac + if [[ ! "$base_sha" =~ ^[0-9a-f]{40}$ ]] || + [[ ! "$head_sha" =~ ^[0-9a-f]{40}$ ]] || + [[ ! "$head_repository" =~ ^[A-Za-z0-9_.-]+/[A-Za-z0-9_.-]+$ ]]; + then + echo "Refusing malformed formal-verification scope." >&2 + exit 13 + fi + { + echo "base_sha=$base_sha" + echo "head_sha=$head_sha" + echo "head_repository=$head_repository" + echo "mode=$mode" + } >> "$GITHUB_OUTPUT" + + - name: Checkout exact production revision without credentials + uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + with: + repository: ${{ steps.scope.outputs.head_repository }} + ref: ${{ steps.scope.outputs.head_sha }} + fetch-depth: 0 + persist-credentials: false + + - name: Materialize exact trusted base commit + shell: bash + env: + BASE_SHA: ${{ steps.scope.outputs.base_sha }} + HEAD_SHA: ${{ steps.scope.outputs.head_sha }} + BASE_REPOSITORY: ${{ github.repository }} + run: | + actual_head="$(git rev-parse HEAD)" + if [[ "$actual_head" != "$HEAD_SHA" ]]; then + echo "Checkout does not match the requested head SHA." >&2 + exit 13 + fi + if ! git cat-file -e "$BASE_SHA^{commit}" 2>/dev/null; then + git fetch --no-tags --depth=1 \ + "https://github.com/$BASE_REPOSITORY.git" "$BASE_SHA" + fi + git cat-file -e "$BASE_SHA^{commit}" + + - id: plan + name: Generate base-approved verification plan + continue-on-error: true + env: + VERIFIER_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e + REPAIR_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597 + BASE_SHA: ${{ steps.scope.outputs.base_sha }} + HEAD_SHA: ${{ steps.scope.outputs.head_sha }} + MODE: ${{ steps.scope.outputs.mode }} + run: | + readarray -t policy_images < <( + git show "$BASE_SHA:formal/contracts/registry.toml" | + python3 -c ' + import sys + import tomllib + toolchain = tomllib.loads(sys.stdin.read())["toolchain"] + print(toolchain["verifier_image"]) + print(toolchain["repair_image"]) + ' + ) + if [[ "${#policy_images[@]}" -ne 2 ]] || + [[ "${policy_images[0]}" != "$VERIFIER_IMAGE" ]] || + [[ "${policy_images[1]}" != "$REPAIR_IMAGE" ]]; + then + echo "Workflow images do not match trusted base policy." >&2 + exit 13 + fi + mkdir -p .formal-plan + docker run --rm \ + --network none \ + --read-only \ + --cap-drop ALL \ + --security-opt no-new-privileges \ + --pids-limit 256 \ + --memory 2g \ + --cpus 1 \ + --user "$(id -u):$(id -g)" \ + --tmpfs /tmp:rw,nosuid,nodev,size=128m \ + --volume "$GITHUB_WORKSPACE:/workspace:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-plan:/plan:rw" \ + --workdir /workspace \ + "$VERIFIER_IMAGE" plan \ + --workspace /workspace \ + --base-policy formal/contracts/registry.toml \ + --base-sha "$BASE_SHA" \ + --head-sha "$HEAD_SHA" \ + --mode "$MODE" \ + --out /plan + + - id: formal + name: Verify exact generated plan + if: steps.plan.outcome == 'success' + continue-on-error: true + env: + VERIFIER_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e + run: | + mkdir -p .formal-results + 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=512m \ + --volume "$GITHUB_WORKSPACE:/workspace:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-plan:/plan:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-results:/results:rw" \ + --workdir /workspace \ + "$VERIFIER_IMAGE" verify \ + --plan /plan/plan.json \ + --workspace /workspace \ + --generated-root /plan \ + --out /results + + - name: Publish formal summary + if: always() + run: | + if [[ -f .formal-results/summary.md ]]; then + cat .formal-results/summary.md >> "$GITHUB_STEP_SUMMARY" + elif [[ "${{ steps.plan.outcome }}" != "success" ]]; then + echo "Formal planning failed; inspect the plan artifact." \ + >> "$GITHUB_STEP_SUMMARY" + else + echo "Formal verifier did not produce a summary." \ + >> "$GITHUB_STEP_SUMMARY" + fi + + - name: Record trusted workflow source + if: always() + env: + BASE_REPOSITORY: ${{ github.repository }} + HEAD_REPOSITORY: ${{ steps.scope.outputs.head_repository }} + BASE_SHA: ${{ steps.scope.outputs.base_sha }} + HEAD_SHA: ${{ steps.scope.outputs.head_sha }} + EVENT_NAME: ${{ github.event_name }} + run: | + mkdir -p .formal-results + python3 -c ' + import json + import os + from pathlib import Path + fields = { + "repository": os.environ["BASE_REPOSITORY"], + "head_repository": os.environ["HEAD_REPOSITORY"], + "base_sha": os.environ["BASE_SHA"], + "head_sha": os.environ["HEAD_SHA"], + "event": os.environ["EVENT_NAME"], + } + Path(".formal-results/source.json").write_text( + json.dumps(fields, indent=2, sort_keys=True) + "\n", + encoding="utf-8", + ) + ' + + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: always() + with: + name: formal-results + path: | + .formal-plan/ + .formal-results/ + include-hidden-files: true + if-no-files-found: error + retention-days: 14 + + - name: Enforce deterministic result + if: >- + steps.plan.outcome != 'success' || + steps.formal.outcome != 'success' + run: | + echo "The deterministic formal-verification lane did not pass." >&2 + exit 1 + + legacy-shadow: + name: legacy-shadow + needs: verify + if: always() && needs.verify.outputs.head_sha != '' + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout exact production revision without credentials + uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + with: + repository: ${{ needs.verify.outputs.head_repository }} + ref: ${{ needs.verify.outputs.head_sha }} + fetch-depth: 0 + persist-credentials: false + + - name: Materialize comparison base + env: + BASE_SHA: ${{ needs.verify.outputs.base_sha }} + BASE_REPOSITORY: ${{ github.repository }} + run: | + if ! git cat-file -e "$BASE_SHA^{commit}" 2>/dev/null; then + git fetch --no-tags --depth=1 \ + "https://github.com/$BASE_REPOSITORY.git" "$BASE_SHA" + fi + + - id: legacy + name: Run legacy manifest for dual-run comparison + continue-on-error: true + env: + VERIFIER_IMAGE: ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e + BASE_SHA: ${{ needs.verify.outputs.base_sha }} + MODE: ${{ needs.verify.outputs.mode }} + run: | + mkdir -p .formal-legacy-results + 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,nosuid,nodev,size=512m \ + --volume "$GITHUB_WORKSPACE:/workspace:ro" \ + --volume "$GITHUB_WORKSPACE/.formal-legacy-results:/results:rw" \ + --workdir /workspace \ + "$VERIFIER_IMAGE" verify \ + --manifest /workspace/formal/manifest.toml \ + --base-sha "$BASE_SHA" \ + --mode "$MODE" \ + --out /results + + - name: Record advisory comparison + if: always() + run: | + { + echo "# Legacy formal comparison" + echo + echo "This shadow result is advisory during plan migration." + echo "Outcome: \`${{ steps.legacy.outcome }}\`" + } >> "$GITHUB_STEP_SUMMARY" + + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: always() + with: + name: formal-legacy-results + path: .formal-legacy-results/ + include-hidden-files: true + if-no-files-found: warn + retention-days: 14 diff --git a/.gitignore b/.gitignore index 0ff34e9cf..0d1fe703b 100644 --- a/.gitignore +++ b/.gitignore @@ -78,6 +78,7 @@ fix-plan.md # Harness test artifacts .harness-work/ +.formal-results/ health # lucebox host-side generated config + benchmark output diff --git a/formal/FIRST_WAVE_EVIDENCE.md b/formal/FIRST_WAVE_EVIDENCE.md new file mode 100644 index 000000000..312b0265e --- /dev/null +++ b/formal/FIRST_WAVE_EVIDENCE.md @@ -0,0 +1,163 @@ +# First-wave verification evidence + +This file records the local promotion evidence for the first advisory wave. It +does not promote any target or claim proof of the complete Lucebox system. + +## 2026-07-30 PR-bound replay + +The five legacy capsules were run together with ESBMC 8.4.0 using the +repository's pinned verifier image: + +`ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:cb38011acd8dbe5aeb702b6ba981607cf81656667d79461fc74e66d552cabd07` + +| Capsule | Result | Bound and solver | Time | +|---|---:|---|---:| +| `prefix-cache-inline` | passed | capacity 4, Z3, unwind 5 | 7.37 s | +| `prefix-cache-abort-hole` | passed | capacity 4, Z3, unwind 17 | 0.81 s | +| `prefix-cache-full-lifecycle` | passed | capacity 2, Boolector, unwind 5 | 45.35 s | +| `spec-commit-exactness` | passed | width 4, Z3, unwind 17 | 1.02 s | +| `kvflash-residency-map` | passed | four blocks, Boolector, unwind 14 | 89.19 s | + +The new targets' exact properties and exclusions are documented in: + +- [`prefix_cache/FULL_LIFECYCLE_PROPERTIES.md`](prefix_cache/FULL_LIFECYCLE_PROPERTIES.md) +- [`spec_commit/PROPERTIES.md`](spec_commit/PROPERTIES.md) +- [`kvflash/RESIDENCY_MAP_PROPERTIES.md`](kvflash/RESIDENCY_MAP_PROPERTIES.md) + +The broader exact-head native regressions remain part of each deterministic +plan. They cover integration behavior that is intentionally not described as +model checked. + +## 2026-07-30 mutation campaign + +The complete checked-in mutation suite passed against exact source commit +`a0e476bd`. Each case ran in an isolated clone and required the protected +target to conclude with a counterexample: + +| Mutation | Target result | Intended evidence | +|---|---:|---| +| inline free-slot selector bypass | counterexample | exact-head native regression; inline formal control verified | +| full-cache free-slot selector bypass | counterexample | exact-head lifecycle regression; inline and abort-hole controls verified | +| speculative prefix comparison inversion | counterexample in 2.26 s | ESBMC and native regression | +| KVFlash capacity-boundary off-by-one | counterexample in 0.93 s | ESBMC and native regression | + +This establishes sensitivity for the checked-in representative defects. It +does not imply sensitivity to every possible defect in the same production +areas. + +## 2026-07-30 companion 0.3.0 candidate validation and proposed pin + +Companion commit `971fda75b4b6f2da9ff26d1c06bf248472bf96b6` was published +and smoke-tested in +[run 30541259801](https://github.com/dusterbloom/lucebox-esbmc-ai/actions/runs/30541259801). +This branch proposes pinning the resulting post-smoke OCI digests: + +- verifier: + `ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:fd1a08aec947df86f3a441504f65d44ebb3fc05c299e98cdf3249a724446f62e`; +- repair: + `ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:2d77a93c2467641696b1080e00866b22d5f7ab6f4456eeceec35862aa01bdd46`. + +Before the proposed pin transition, the new verifier was run locally as an +explicit candidate override against exact Lucebox head +`84ad08b22e34814f116628a3ea396b7c4efa6bf0`. The authenticated generated plan +and all declared native regressions verified: + +```text +LUCEBOX_FORMAL_IMAGE=ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:fd1a08aec947df86f3a441504f65d44ebb3fc05c299e98cdf3249a724446f62e \ +LUCEBOX_FORMAL_RESULTS=/tmp/lucebox-formal-new-image-candidate \ +./scripts/formal.sh --all +``` + +Mode `all` used base=head=`84ad08b22e34814f116628a3ea396b7c4efa6bf0`. +The resulting `report.json` SHA-256 was +`8613f96727f73739e1072242f4a7e0ea6f98b92172d83061b3eb370268e69ea7`. +The generated plan directory was ephemeral and was not retained. + +## 2026-07-30 separate KVFlash nightly timeout + +Companion commit `8a7e1aae040a9f17a7e7513e7bb29c9495afcedb` adds an authenticated +`nightly_timeout_seconds` target setting. The PR timeout remains 180 seconds; +the KVFlash five-block nightly expansion is set to 240 seconds. The companion +CI suite passed all 49 tests, and the updated images were published and +smoke-tested in [run 30560639772](https://github.com/dusterbloom/lucebox-esbmc-ai/actions/runs/30560639772): + +- verifier: + `ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e`; +- repair: + `ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597`. + +This timeout change provides operational headroom for the nightly proof; it +does not promote KVFlash or relax the per-PR bound. + +The exact-head nightly replay at Lucebox commit `2fe23811868701ec430325817972b1efd0872fbc` +passed both generated and legacy lanes in +[run 30561396096](https://github.com/dusterbloom/lucebox-hub/actions/runs/30561396096). +The generated KVFlash proof took 167.92 seconds and the legacy proof took +181.48 seconds against the 240-second nightly timeout, leaving approximately +58.5 seconds of margin in the slower lane. The artifact hashes are: + +- plan: `d50d74575fae0871a6ac0eb94b2a36946edd4dcf4e6f7ca3f919ded5f5fec6f9`; +- generated report: `f045a24c6c8619091d375c488ae9b7295f5cc1ed197f795c23723fcc606b302e`; +- legacy report: `23a526ceb8f28279be848ef3548919d9247d9e185f715d9b10f515b22e7f1744`. + +| Capsule | Result | Time | +|---|---:|---:| +| `prefix-cache-inline` | verified | 7.27 s | +| `prefix-cache-abort-hole` | verified | 0.96 s | +| `prefix-cache-full-lifecycle` | verified | 45.34 s | +| `spec-commit-exactness` | verified | 1.19 s | +| `kvflash-residency-map` | verified | 87.89 s | + +At proposed-pin commit `b37dae25ea3f4104785ee2163174390fbbb9e0be`, +the normal pinned-image invocation also verified all five capsules with +base=head and mode `all`: + +```text +LUCEBOX_FORMAL_RESULTS=/tmp/lucebox-formal-pin-head \ +./scripts/formal.sh --all +``` + +The resulting `report.json` SHA-256 was +`eb2d633fa0108a94aa82364091714da2f8bbe842c1ff72c588079172512f8052`. +Capsule times were 7.02 s, 0.98 s, 45.21 s, 1.15 s, and 87.34 s in registry +order. The complete `./scripts/formal_mutation_test.sh` campaign then passed +at the same commit: each of the four checked-in defects produced its required +counterexample, while the applicable prefix-cache control capsules remained +verified. + +The companion's +[49-test CI run](https://github.com/dusterbloom/lucebox-esbmc-ai/actions/runs/30538756694) +includes an adversarial regression checking that a head-edited transitive +contract body cannot shadow the authenticated base snapshot while production +headers still resolve from the exact head. + +## 2026-07-30 nightly-bound calibration + +The first hosted nightly-mode bootstrap at exact base=head +`a88ba49251fa657efe1d13938c9280a211d380e6` was intentionally treated as a +calibration run: +[run 30543897953](https://github.com/dusterbloom/lucebox-hub/actions/runs/30543897953). +Both the generated-plan and legacy lanes verified the two inline prefix-cache +targets, four-slot full prefix-cache lifecycle, and width-eight speculative +commit target. The six-block KVFlash target reached its exact 180-second +timeout in both lanes and was reported as inconclusive, not as a +counterexample. + +The generated KVFlash run spent 145.39 seconds in symbolic execution and +produced 83,245 verification conditions before timing out in Boolector. Because +the four-block PR bound already verifies well within the shared timeout, the +advisory nightly bound is calibrated to five blocks rather than loosening the +PR timeout. Five remains a strict coverage expansion and adds a +non-power-of-two pool. It must pass generated, legacy, native, and mutation +checks before it counts as clean soak evidence. + +## Promotion blockers + +The three new targets remain advisory until all of the following are complete: + +1. The companion and Lucebox pin transitions are reviewed and merged into + their protected base branches. +2. The accepted base policy completes a clean PR/nightly soak on the new + digests. +3. Maintainers approve each target's protected contract, bounds, latency, and + ownership in a separate promotion change. diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 000000000..ea13cb7c4 --- /dev/null +++ b/formal/README.md @@ -0,0 +1,161 @@ +# Lucebox formal-verification pilot + +This directory defines proof capsules for the +[`dusterbloom/lucebox-esbmc-ai`](https://github.com/dusterbloom/lucebox-esbmc-ai) +companion runner. + +## Trust boundaries + +The `Formal Verification / verify` check is deterministic: + +- its workflow, registry, templates, bounds, and verifier arguments come from + the exact target-branch base commit, not from the PR being judged; +- it checks out the exact PR head separately and refuses a SHA mismatch; +- its verifier image is pinned by an OCI SHA-256 digest; the registry records + the ESBMC release checksum and the current verifier checks its version + string; +- the Lucebox checkout is mounted read-only; +- only the generated-plan and results directories are writable; +- the container has no network, Linux capabilities, or writable root; +- no model SDK or repository secret is present. + +The `Formal AI Candidate` workflow is separate and advisory: + +- automatic model access is limited to same-repository revisions; a maintainer + may explicitly dispatch a reviewed fork run; +- a secretless job authenticates the deterministic run, source SHA, evidence, + and either a real counterexample or a critical coverage gap; +- the `formal-ai` environment requires approval before model access; +- archive paths, sizes, immutable contract hashes, and mutable patch paths are + validated; +- the credential-bearing proposer never executes generated code; +- generated code is applied, compiled, run, and reverified only in a second + networkless container after the proposer has exited; +- a missing-contract proposal is compiled and checked by ESBMC without + credentials, but remains advisory until reviewed and merged into base policy; +- the lane can only upload artifacts. It cannot commit, comment, push, or open + a pull request. + +Every C/C++ capsule requests ESBMC's native self-contained HTML report. A +counterexample publishes it below `counterexamples//` in the formal +results artifact; CI never renders untrusted report HTML in the job summary. + +## Current capsules + +`prefix-cache-inline` checks the production +`InlinePrefixCacheState` one-entry prepare/confirm/exact-lookup path for +symbolic cache capacity, branch, and prefix depth. Its precise guarantees and +exclusions are in +[`prefix_cache/PROPERTIES.md`](prefix_cache/PROPERTIES.md). + +The abort-hole capsule formally checks the scalar free-slot selector. Its +deterministic plan then compiles and runs the immutable base regression against +the exact head, covering the production prepare/confirm/prepare/abort/prepare +sequence. This catches both a broken selector and a `prepare` call site that +bypasses a correct selector. The formal and native guarantees are separated in +[`prefix_cache/ABORT_HOLE_PROPERTIES.md`](prefix_cache/ABORT_HOLE_PROPERTIES.md). + +The first-wave advisory capsules add: + +- `prefix-cache-full-lifecycle`, which extracts the full snapshot + key/slot/boundary/victim reservation, model-checks its fresh + prepare/invalid-confirm/confirm/lookup/clear trace, and exercises the wider + abort/hole/LRU lifecycle in the exact-head native regression; +- `spec-commit-exactness`, which centralizes the linear speculative-decode + acceptance, optional bonus, budget, and token-selection decision used by + five model families; +- `kvflash-residency-map`, which makes the CPU ownership map authoritative and + model-checks named identity-fill, rejected-eviction rollback, + protected-LRU-eviction, mask, and logical-bound sequences independently of + GPU DMA; recall, explicit page-out, reset, and scored paths remain in the + exact-head native regression. + +Their exact checked properties and exclusions live beside their harnesses. +They remain `advisory` while maintainers review their protected contracts, +bounds, latency, and ownership. The candidate companion image proposed by this +transition contains the authenticated transitive-contract snapshot +implementation. Local candidate and hosted baseline ESBMC evidence is recorded in +[`FIRST_WAVE_EVIDENCE.md`](FIRST_WAVE_EVIDENCE.md). Only behavior explicitly +named by a capsule contract is described as model checked. + +The KVFlash target keeps its four-block PR timeout at 180 seconds while using a +separate 240-second authenticated nightly timeout for the wider five-block +soak. This extra nightly margin does not weaken the per-PR gate. + +## Local use + +Docker will pull the immutable verifier declared in +`contracts/registry.toml`. Local planning requires a committed checkout. + +```bash +./scripts/formal.sh --all +./scripts/formal.sh --nightly +./scripts/formal.sh --base-sha origin/main +./scripts/formal.sh --all --legacy +./scripts/formal_mutation_test.sh +``` + +Set `LUCEBOX_FORMAL_IMAGE` only when deliberately testing a new companion image. +Results are written to `.formal-results/`. +The mutation suite runs four isolated clones. It recreates the historical +inline `prepare` bypass and injects one focused defect into each first-wave +core. Every immutable native regression must fail, every selected formal lane +must conclude with a counterexample, and declared unrelated control targets +must remain verified. + +## Adding an approved contract + +1. Extract a dependency-light production transition boundary; do not verify a + toy reimplementation. +2. Write a deterministic template and property document that distinguish + checked properties from exclusions. +3. Add a deterministic native regression test. +4. Declare the exact symbol/signature, triggers, PR/nightly bounds, mutable + paths, and immutable contract paths in `contracts/registry.toml`. +5. Run both pull-request and nightly bounds locally. +6. Demonstrate mutation sensitivity before marking the entry `required`. +7. Treat invalid contracts, exhausted bounds, timeout, and tool errors as + failures, never as passes. + +## Per-PR contract registry migration + +The current capsules have also been recorded in +[`contracts/registry.toml`](contracts/registry.toml) with deterministic source +templates. This is a dual-run migration: the registry drives the base-locked +plan while `manifest.toml` remains an advisory comparison interface. See +[`contracts/README.md`](contracts/README.md) for the base-branch trust rule, +coverage-gap policy, and local registry validation commands. + +The first registry PR cannot use itself as required base policy. Validate that +bootstrap revision with an `all` workflow dispatch; base-locked PR planning +starts after the registry exists on the protected target branch. + +## AI environment + +Create an approval-protected GitHub environment named `formal-ai`: + +```text +Secret: + ZAI_API_KEY= + +Variables: + FORMAL_AI_MODEL=openai:glm-5 + FORMAL_AI_BASE_URL=https://api.z.ai/api/paas/v4/ +``` + +`OPENAI_API_KEY` may be used instead when the base URL and model are configured +for OpenAI. Model credentials are passed only to proposal containers. + +## Promotion after the proving period + +Leave the check non-required for at least 14 days. Promote +`Formal Verification / verify` to a required fork branch-protection check only +after it has: + +- no unexplained counterexamples or false passes; +- no recurring timeout/tool-error failures; +- stable pull-request latency; +- useful, reproducible artifacts for every failure. + +Promotion in the fork is a separate decision. Upstream contribution should +follow only after the fork data supports the stated value proposition. diff --git a/formal/contracts/README.md b/formal/contracts/README.md new file mode 100644 index 000000000..b9cb69d51 --- /dev/null +++ b/formal/contracts/README.md @@ -0,0 +1,72 @@ +# Approved per-PR formal contracts + +`registry.toml` is the source of truth for the minimal formal boundaries that +may be selected automatically for a pull request. It is intentionally not a +replacement for `../manifest.toml` yet: the manifest continues to drive the +existing deterministic capsule workflow during the dual-run migration. + +Each target records the exact production symbol and signature, approved +template, execution bounds, mutable implementation paths, immutable contract +paths, and paired native regression. Templates use only literal +`{{ID}}`, `{{SYMBOL}}`, `{{SIGNATURE}}`, and optional declared variables. The +planner substitutes those tokens deterministically; it never asks a model to +write a required contract. + +## Trust and migration rules + +For a PR, the planner must read this registry and the selected template blobs +from the merge base (or a protected artifact identified by that base), then +record their hashes in its plan. It must not trust a registry or template that +the PR itself changed. A contract-change PR therefore runs the old approved +contract as the gate and reports its proposed new contract separately until +formal CODEOWNERS approve promotion. + +The promoted entries cover two complementary inline prefix-cache capsules: + +- `prefix-cache-inline` maps to the existing prepare/confirm/lookup harness. +- `prefix-cache-abort-hole` exhaustively checks the bounded scalar free-slot + selector, then runs the immutable base regression against the exact head to + guard the real `prepare`/`abort`/`prepare` integration point. + +Three first-wave entries are registered as advisory while proof latency and +mutation sensitivity are established: + +- `prefix-cache-full-lifecycle` +- `spec-commit-exactness` +- `kvflash-residency-map` + +Their generated wrappers may include shared harness bodies. Every such body is +declared in `contract_paths`. Once accepted into protected base policy, the +candidate companion image materializes those authenticated base-revision blobs +into an isolated include tree before the PR/head production include paths. A +PR therefore cannot weaken a transitive harness include while retaining a +green result. + +The templates intentionally call production code; they are not duplicate +implementations. The legacy harness runs the same transition during the +planner/verifier dual-run so comparison remains meaningful. + +`[[critical_paths]]` lists the cache, snapshot, streaming, and tool-hint state +machines. A changed path in one of those areas that matches no approved target +is an **advisory coverage gap**, never a pass. Paths outside the list are +reported as not applicable by the CI planner. + +An area may also declare advisory `watch_paths` and bounded `include_roots`. +In CI, the companion planner uses watch matches to route suspicious new files +for review, but a match never means that a file is formally covered. The +companion records exact boundary, trigger, include-adjacency, and unmodeled +relationships separately; only a verifier result for a declared target may +use the word `verified`. + +## Local validation + +```bash +python3 scripts/formal_plan.py validate +python3 scripts/formal_plan.py plan \ + --changed-path server/src/server/prefix_cache_state.h +python3 -m unittest formal/contracts/tests/test_formal_plan.py -v +``` + +`emit` is a local fixture aid: it renders selected protected templates into an +output directory and records their hashes. It does not invoke ESBMC or modify +the existing manifest lane. diff --git a/formal/contracts/fixtures/kvflash-change.json b/formal/contracts/fixtures/kvflash-change.json new file mode 100644 index 000000000..ab52f4df4 --- /dev/null +++ b/formal/contracts/fixtures/kvflash-change.json @@ -0,0 +1,5 @@ +{ + "changed_paths": [ + "server/src/common/kvflash_pager.h" + ] +} diff --git a/formal/contracts/fixtures/prefix-cache-change.json b/formal/contracts/fixtures/prefix-cache-change.json new file mode 100644 index 000000000..a4932d2f6 --- /dev/null +++ b/formal/contracts/fixtures/prefix-cache-change.json @@ -0,0 +1,10 @@ +{ + "changed_paths": [ + "server/src/server/prefix_cache_state.h" + ], + "expected_coverage_gaps": [], + "expected_target_ids": [ + "prefix-cache-abort-hole", + "prefix-cache-inline" + ] +} diff --git a/formal/contracts/fixtures/spec-commit-change.json b/formal/contracts/fixtures/spec-commit-change.json new file mode 100644 index 000000000..6c12f2063 --- /dev/null +++ b/formal/contracts/fixtures/spec-commit-change.json @@ -0,0 +1,5 @@ +{ + "changed_paths": [ + "server/src/qwen35/qwen35_backend.cpp" + ] +} diff --git a/formal/contracts/fixtures/uncovered-streaming-change.json b/formal/contracts/fixtures/uncovered-streaming-change.json new file mode 100644 index 000000000..c849c6d24 --- /dev/null +++ b/formal/contracts/fixtures/uncovered-streaming-change.json @@ -0,0 +1,9 @@ +{ + "changed_paths": [ + "server/src/server/sse_emitter.cpp" + ], + "expected_coverage_gaps": [ + "streaming-lifecycle" + ], + "expected_target_ids": [] +} diff --git a/formal/contracts/mutations/kvflash-capacity-off-by-one.patch b/formal/contracts/mutations/kvflash-capacity-off-by-one.patch new file mode 100644 index 000000000..d747135fc --- /dev/null +++ b/formal/contracts/mutations/kvflash-capacity-off-by-one.patch @@ -0,0 +1,8 @@ +diff --git a/server/src/common/kvflash_residency_map.h b/server/src/common/kvflash_residency_map.h +--- a/server/src/common/kvflash_residency_map.h ++++ b/server/src/common/kvflash_residency_map.h +@@ -80,3 +80,3 @@ public: + const int64_t min_chunks = +- (int64_t)cfg.sink_chunks + cfg.tail_window_chunks + 2; ++ (int64_t)cfg.sink_chunks + cfg.tail_window_chunks + 3; + const int64_t min_tokens = min_chunks * cfg.chunk_tokens; diff --git a/formal/contracts/mutations/prefix-cache-bypass-selector.patch b/formal/contracts/mutations/prefix-cache-bypass-selector.patch new file mode 100644 index 000000000..6ba5e2251 --- /dev/null +++ b/formal/contracts/mutations/prefix-cache-bypass-selector.patch @@ -0,0 +1,24 @@ +diff --git a/server/src/server/prefix_cache_state.h b/server/src/server/prefix_cache_state.h +--- a/server/src/server/prefix_cache_state.h ++++ b/server/src/server/prefix_cache_state.h +@@ -186,17 +186,8 @@ public: + result.victim_len = + (int)entries_[(size_t)victim].ids.size(); + result.oldest_len = (int)entries_.front().ids.size(); + } else { +- uint64_t occupied_slots = 0; +- if (capacity_ <= 64) { +- for (const auto & entry : entries_) { +- if (entry.slot >= 0 && entry.slot < 64) { +- occupied_slots |= uint64_t{1} << entry.slot; +- } +- } +- } +- result.slot = select_inline_free_slot( +- next_slot_, capacity_, occupied_slots); +- next_slot_ = (result.slot + 1) % capacity_; ++ result.slot = next_slot_; ++ next_slot_ = (next_slot_ + 1) % capacity_; + has_pending_evict_ = false; + } + return result; diff --git a/formal/contracts/mutations/prefix-cache-full-bypass-free-slot.patch b/formal/contracts/mutations/prefix-cache-full-bypass-free-slot.patch new file mode 100644 index 000000000..5337809d9 --- /dev/null +++ b/formal/contracts/mutations/prefix-cache-full-bypass-free-slot.patch @@ -0,0 +1,14 @@ +diff --git a/server/src/server/prefix_cache_state.h b/server/src/server/prefix_cache_state.h +--- a/server/src/server/prefix_cache_state.h ++++ b/server/src/server/prefix_cache_state.h +@@ -405,9 +405,7 @@ public: + } + } + } +- const int relative = select_inline_free_slot( +- next_relative_slot_, capacity_, occupied); +- if (relative < 0) return result; ++ const int relative = next_relative_slot_; + abs_slot = slot_base_ + relative; + next_relative_slot_ = (relative + 1) % capacity_; + } else { diff --git a/formal/contracts/mutations/spec-commit-invert-prefix-match.patch b/formal/contracts/mutations/spec-commit-invert-prefix-match.patch new file mode 100644 index 000000000..d283ad9c5 --- /dev/null +++ b/formal/contracts/mutations/spec-commit-invert-prefix-match.patch @@ -0,0 +1,10 @@ +diff --git a/server/src/common/spec_commit.h b/server/src/common/spec_commit.h +--- a/server/src/common/spec_commit.h ++++ b/server/src/common/spec_commit.h +@@ -34,5 +34,5 @@ public: + int accepted = 1; // seed + while (accepted < verify_count && +- draft_tokens[accepted] == target_tokens[accepted - 1]) { ++ draft_tokens[accepted] != target_tokens[accepted - 1]) { + ++accepted; + } diff --git a/formal/contracts/registry.toml b/formal/contracts/registry.toml new file mode 100644 index 000000000..8c093b0df --- /dev/null +++ b/formal/contracts/registry.toml @@ -0,0 +1,365 @@ +# Approved minimal-core formal contracts. +# +# This registry is deliberately separate from formal/manifest.toml. The +# latter remains the compatibility manifest for the existing verifier while +# the PR planner uses this file to decide which approved templates may become +# required checks. In CI, the authoritative copy must be read from the PR +# base revision (or an equivalently protected artifact), never from a PR that +# is changing the implementation under review. +schema_version = 1 + +# An edit below is security-relevant: it is a change to the definition of +# formal coverage, not merely a new test. New or changed entries remain +# advisory until reviewed and promoted through the protected-contract path. +[registry] +description = "Approved Lucebox minimal-core contracts for per-PR ESBMC planning" +compatibility_manifest = "formal/manifest.toml" + +[toolchain] +esbmc_version = "8.4" +esbmc_linux_sha256 = "68bb71128e0c3c2db090955e7a302533a8a11a9d898df7f169c22311a0ec5078" +verifier_image = "ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e" +repair_image = "ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597" + +# These are the state-machine areas where an edit without a matched approved +# target is an advisory coverage gap. Keep the list narrow; ordinary server +# implementation edits are not made critical merely by living under server/. +[[critical_paths]] +id = "prefix-cache" +description = "Inline and full prefix-cache slot, reservation, and eviction lifecycle" +paths = [ + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", +] +# These are advisory routing hints, not claims of formal coverage. Exact +# boundaries above and approved target triggers remain authoritative. +watch_paths = [ + "server/src/server/prefix_cache*.h", + "server/src/server/prefix_cache*.cpp", + "server/src/server/*snapshot*.h", + "server/src/server/*snapshot*.cpp", + "server/src/server/*eviction*.h", + "server/src/server/*eviction*.cpp", +] +include_roots = ["server/src"] +policy = "advisory" + +[[critical_paths]] +id = "disk-prefix-cache" +description = "Persistent snapshot load/save/adopt lifecycle" +paths = [ + "server/src/server/disk_prefix_cache.h", + "server/src/server/disk_prefix_cache.cpp", +] + +[[critical_paths]] +id = "request-snapshot-lifecycle" +description = "Request restore, snapshot reservation, confirmation, abort, and cancellation orchestration" +paths = [ + "server/src/server/http_server.cpp", + "server/src/server/http_server.h", +] + +[[critical_paths]] +id = "streaming-lifecycle" +description = "Streaming response state transitions and disconnect cancellation" +paths = [ + "server/src/server/sse_emitter.h", + "server/src/server/sse_emitter.cpp", +] + +[[critical_paths]] +id = "tool-hint-state" +description = "Generation-time tool-hint state machine" +paths = [ + "server/src/server/tool_hint.h", + "server/src/server/tool_hint.cpp", +] + +[[critical_paths]] +id = "spec-commit" +description = "Linear speculative verification and bounded token commit decisions" +paths = [ + "server/src/common/spec_commit.h", + "server/src/common/dflash_spec_decode.cpp", + "server/src/qwen35/qwen35_backend.cpp", + "server/src/qwen35moe/qwen35moe_backend.cpp", + "server/src/laguna/laguna_backend.cpp", + "server/src/gemma4/gemma4_backend.cpp", +] +watch_paths = [ + "server/src/**/*spec*decode*.h", + "server/src/**/*spec*decode*.cpp", + "server/src/**/*backend.cpp", +] +include_roots = ["server/src"] +policy = "advisory" + +[[critical_paths]] +id = "kvflash-residency" +description = "KVFlash logical-chunk ownership, eviction, and slot mapping" +paths = [ + "server/src/common/kvflash_residency_map.h", + "server/src/common/kvflash_pager.h", +] +watch_paths = [ + "server/src/common/*kvflash*.h", + "server/src/common/*kvflash*.cpp", + "server/src/**/*kvflash*.h", + "server/src/**/*kvflash*.cpp", +] +include_roots = ["server/src"] +policy = "advisory" + +[[targets]] +id = "prefix-cache-inline" +policy = "required" +description = "Inline prefix-cache prepare, confirm, exact lookup, and structural invariants" +source_paths = [ + "server/src/server/prefix_cache_state.h", +] +trigger_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/prefix-cache-inline.cpp.in", + "formal/prefix_cache/PROPERTIES.md", + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", + "server/test/test_prefix_cache_state.cpp", +] +symbol = "dflash::common::InlinePrefixCacheState" +signature = "class dflash::common::InlinePrefixCacheState" +template = "formal/contracts/templates/prefix-cache-inline.cpp.in" +entry_function = "main" +include_dirs = ["server/src"] +timeout_seconds = 120 +pr_defines = ["LUCEBOX_FORMAL_MAX_CAP=4"] +nightly_defines = ["LUCEBOX_FORMAL_MAX_CAP=16"] +pr_esbmc_args = [ + "--quiet", + "--z3", + "--unwind", "5", + "--memory-leak-check", + "--overflow-check", +] +nightly_esbmc_args = [ + "--quiet", + "--z3", + "--unwind", "5", + "--memory-leak-check", + "--overflow-check", +] +mutable_paths = ["server/src/server/prefix_cache_state.h"] +contract_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/prefix-cache-inline.cpp.in", + "formal/prefix_cache/PROPERTIES.md", + "server/test/test_prefix_cache_state.cpp", +] + +[[targets]] +id = "prefix-cache-abort-hole" +policy = "required" +description = "Inline prefix-cache free-slot selection after an aborted reservation" +source_paths = [ + "server/src/server/prefix_cache_state.h", +] +trigger_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/prefix-cache-abort-hole.cpp.in", + "formal/contracts/mutations/prefix-cache-bypass-selector.patch", + "formal/prefix_cache/ABORT_HOLE_PROPERTIES.md", + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", + "server/test/test_prefix_cache_state.cpp", +] +symbol = "dflash::common::select_inline_free_slot" +signature = "int(int next_slot, int capacity, uint64_t occupied_slots)" +template = "formal/contracts/templates/prefix-cache-abort-hole.cpp.in" +entry_function = "verify_select_inline_free_slot_contract" +include_dirs = ["server/src"] +timeout_seconds = 120 +pr_defines = ["LUCEBOX_FORMAL_MAX_CAP=4"] +nightly_defines = ["LUCEBOX_FORMAL_MAX_CAP=16"] +pr_esbmc_args = [ + "--quiet", + "--z3", + "--enforce-contract", "verify_select_inline_free_slot_contract", + "--unwind", "17", + "--overflow-check", +] +nightly_esbmc_args = [ + "--quiet", + "--z3", + "--enforce-contract", "verify_select_inline_free_slot_contract", + "--unwind", "17", + "--overflow-check", +] +mutable_paths = ["server/src/server/prefix_cache_state.h"] +contract_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/prefix-cache-abort-hole.cpp.in", + "formal/contracts/mutations/prefix-cache-bypass-selector.patch", + "formal/prefix_cache/ABORT_HOLE_PROPERTIES.md", + "server/test/test_prefix_cache_state.cpp", +] +native_test = "test_prefix_cache_state" +native_test_source = "server/test/test_prefix_cache_state.cpp" + +[[targets]] +id = "prefix-cache-full-lifecycle" +policy = "advisory" +description = "Full prefix-cache fresh boundary/confirm proof with exact-head lifecycle regression" +source_paths = [ + "server/src/server/prefix_cache_state.h", +] +trigger_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/prefix-cache-full-lifecycle.cpp.in", + "formal/contracts/mutations/prefix-cache-full-bypass-free-slot.patch", + "formal/prefix_cache/full_lifecycle_harness_body.h", + "formal/prefix_cache/FULL_LIFECYCLE_PROPERTIES.md", + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", + "server/test/test_full_prefix_cache_state.cpp", +] +symbol = "dflash::common::FullPrefixCacheState" +signature = "class dflash::common::FullPrefixCacheState" +template = "formal/contracts/templates/prefix-cache-full-lifecycle.cpp.in" +entry_function = "main" +include_dirs = ["server/src", "formal"] +timeout_seconds = 120 +pr_defines = ["LUCEBOX_FORMAL_CAP=2"] +nightly_defines = ["LUCEBOX_FORMAL_CAP=4"] +pr_esbmc_args = [ + "--quiet", + "--boolector", + "--unwind", "5", + "--overflow-check", +] +nightly_esbmc_args = [ + "--quiet", + "--boolector", + "--unwind", "5", + "--overflow-check", +] +mutable_paths = ["server/src/server/prefix_cache_state.h"] +contract_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/prefix-cache-full-lifecycle.cpp.in", + "formal/contracts/mutations/prefix-cache-full-bypass-free-slot.patch", + "formal/prefix_cache/full_lifecycle_harness_body.h", + "formal/prefix_cache/FULL_LIFECYCLE_PROPERTIES.md", + "server/test/test_full_prefix_cache_state.cpp", +] +native_test = "test_full_prefix_cache_state" +native_test_source = "server/test/test_full_prefix_cache_state.cpp" + +[[targets]] +id = "spec-commit-exactness" +policy = "advisory" +description = "Linear speculative acceptance, bonus availability, budget clipping, and safe token selection" +source_paths = [ + "server/src/common/spec_commit.h", +] +trigger_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/spec-commit-exactness.cpp.in", + "formal/contracts/mutations/spec-commit-invert-prefix-match.patch", + "formal/spec_commit/spec_commit_harness_body.h", + "formal/spec_commit/PROPERTIES.md", + "server/src/common/spec_commit.h", + "server/src/common/dflash_spec_decode.cpp", + "server/src/qwen35/qwen35_backend.cpp", + "server/src/qwen35moe/qwen35moe_backend.cpp", + "server/src/laguna/laguna_backend.cpp", + "server/src/gemma4/gemma4_backend.cpp", + "server/test/test_spec_commit.cpp", +] +symbol = "dflash::common::SpecCommitDecision" +signature = "class dflash::common::SpecCommitDecision" +template = "formal/contracts/templates/spec-commit-exactness.cpp.in" +entry_function = "main" +include_dirs = ["server/src", "formal"] +timeout_seconds = 120 +pr_defines = ["LUCEBOX_FORMAL_MAX_WIDTH=4"] +nightly_defines = ["LUCEBOX_FORMAL_MAX_WIDTH=8"] +pr_esbmc_args = [ + "--quiet", + "--z3", + "--unwind", "17", + "--memory-leak-check", + "--overflow-check", +] +nightly_esbmc_args = [ + "--quiet", + "--z3", + "--unwind", "17", + "--memory-leak-check", + "--overflow-check", +] +mutable_paths = ["server/src/common/spec_commit.h"] +contract_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/spec-commit-exactness.cpp.in", + "formal/contracts/mutations/spec-commit-invert-prefix-match.patch", + "formal/spec_commit/spec_commit_harness_body.h", + "formal/spec_commit/PROPERTIES.md", + "server/test/test_spec_commit.cpp", +] +native_test = "test_spec_commit" +native_test_source = "server/test/test_spec_commit.cpp" + +[[targets]] +id = "kvflash-residency-map" +policy = "advisory" +description = "KVFlash identity map, callback rollback, protected LRU eviction, logical bounds, and slot masks" +source_paths = [ + "server/src/common/kvflash_residency_map.h", +] +trigger_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/kvflash-residency-map.cpp.in", + "formal/contracts/mutations/kvflash-capacity-off-by-one.patch", + "formal/kvflash/residency_map_harness_body.h", + "formal/kvflash/RESIDENCY_MAP_PROPERTIES.md", + "server/src/common/kvflash_residency_map.h", + "server/src/common/kvflash_pager.h", + "server/test/test_kvflash_residency_map.cpp", + "server/test/test_kvflash.cpp", +] +symbol = "dflash::common::KvFlashResidencyMap" +signature = "class dflash::common::KvFlashResidencyMap" +template = "formal/contracts/templates/kvflash-residency-map.cpp.in" +entry_function = "main" +include_dirs = ["server/src", "formal"] +timeout_seconds = 180 +nightly_timeout_seconds = 240 +pr_defines = ["LUCEBOX_FORMAL_BLOCKS=4"] +nightly_defines = ["LUCEBOX_FORMAL_BLOCKS=5"] +pr_esbmc_args = [ + "--quiet", + "--boolector", + "--unwind", "14", + "--overflow-check", +] +nightly_esbmc_args = [ + "--quiet", + "--boolector", + "--unwind", "14", + "--overflow-check", +] +mutable_paths = ["server/src/common/kvflash_residency_map.h"] +contract_paths = [ + "formal/contracts/registry.toml", + "formal/contracts/templates/kvflash-residency-map.cpp.in", + "formal/contracts/mutations/kvflash-capacity-off-by-one.patch", + "formal/kvflash/residency_map_harness_body.h", + "formal/kvflash/RESIDENCY_MAP_PROPERTIES.md", + "server/test/test_kvflash_residency_map.cpp", +] +native_test = "test_kvflash_residency_map" +native_test_source = "server/test/test_kvflash_residency_map.cpp" diff --git a/formal/contracts/templates/kvflash-residency-map.cpp.in b/formal/contracts/templates/kvflash-residency-map.cpp.in new file mode 100644 index 000000000..cdaac4aa5 --- /dev/null +++ b/formal/contracts/templates/kvflash-residency-map.cpp.in @@ -0,0 +1,3 @@ +// Generated protected wrapper for {{ID}}: {{SIGNATURE}} +#define LUCEBOX_FORMAL_CONTRACT_SYMBOL {{SYMBOL}} +#include "kvflash/residency_map_harness_body.h" diff --git a/formal/contracts/templates/prefix-cache-abort-hole.cpp.in b/formal/contracts/templates/prefix-cache-abort-hole.cpp.in new file mode 100644 index 000000000..74c0e44e8 --- /dev/null +++ b/formal/contracts/templates/prefix-cache-abort-hole.cpp.in @@ -0,0 +1,38 @@ +// Generated from the protected prefix-cache-abort-hole contract template. +// This wrapper delegates directly to the production free-slot selector. + +#include "server/prefix_cache_state.h" + +#include + +#ifndef LUCEBOX_FORMAL_MAX_CAP +#define LUCEBOX_FORMAL_MAX_CAP 4 +#endif + +// Target {{ID}}: {{SIGNATURE}} + +static_assert( + LUCEBOX_FORMAL_MAX_CAP > 0 && LUCEBOX_FORMAL_MAX_CAP < 64); + +int verify_select_inline_free_slot_contract( + int next_slot, int capacity, uint64_t occupied_slots) { + // Model the below-capacity state after an aborted reservation: the cursor + // may name an occupied slot, but at least one in-range slot remains free. + __ESBMC_requires( + capacity > 0 && capacity <= LUCEBOX_FORMAL_MAX_CAP); + __ESBMC_requires(next_slot >= 0 && next_slot < capacity); + __ESBMC_requires((occupied_slots >> capacity) == 0); + __ESBMC_requires( + occupied_slots != ((uint64_t{1} << capacity) - 1)); + + // Slot selection is scalar and must not mutate program state. + __ESBMC_assigns(); + __ESBMC_ensures(__ESBMC_return_value >= 0); + __ESBMC_ensures(__ESBMC_return_value < capacity); + __ESBMC_ensures( + (occupied_slots & + (uint64_t{1} << __ESBMC_return_value)) == 0); + + return {{SYMBOL}}( + next_slot, capacity, occupied_slots); +} diff --git a/formal/contracts/templates/prefix-cache-full-lifecycle.cpp.in b/formal/contracts/templates/prefix-cache-full-lifecycle.cpp.in new file mode 100644 index 000000000..130d28b4b --- /dev/null +++ b/formal/contracts/templates/prefix-cache-full-lifecycle.cpp.in @@ -0,0 +1,3 @@ +// Generated protected wrapper for {{ID}}: {{SIGNATURE}} +#define LUCEBOX_FORMAL_CONTRACT_SYMBOL {{SYMBOL}} +#include "prefix_cache/full_lifecycle_harness_body.h" diff --git a/formal/contracts/templates/prefix-cache-inline.cpp.in b/formal/contracts/templates/prefix-cache-inline.cpp.in new file mode 100644 index 000000000..10b2c924d --- /dev/null +++ b/formal/contracts/templates/prefix-cache-inline.cpp.in @@ -0,0 +1,102 @@ +// Generated from the protected prefix-cache-inline contract template. +// This file intentionally calls the production transition core directly. + +#include "server/prefix_cache_state.h" + +#include +#include +#include + +#ifndef LUCEBOX_FORMAL_MAX_CAP +#define LUCEBOX_FORMAL_MAX_CAP 4 +#endif + +extern "C" unsigned int nondet_uint(); +extern "C" void __ESBMC_assume(bool); + +// Target {{ID}}: {{SIGNATURE}} +using ContractState = {{SYMBOL}}; +using dflash::common::PrefixHash; +using dflash::common::prefix_hash_equal; + +namespace { + +unsigned int bounded(unsigned int upper_exclusive) { + const unsigned int value = nondet_uint(); + __ESBMC_assume(value < upper_exclusive); + return value; +} + +PrefixHash make_key(unsigned int branch, int depth) { + PrefixHash key{}; + key[0] = (uint8_t)depth; + key[1] = (uint8_t)(branch + 1); + return key; +} + +std::vector make_ids(unsigned int branch, int depth) { + std::vector ids; + ids.push_back(7); + if (depth >= 2) ids.push_back((int32_t)(20 + branch)); + if (depth >= 3) ids.push_back((int32_t)(30 + branch)); + return ids; +} + +void assert_invariants(const ContractState & state) { + assert(state.capacity() >= 1); + assert(state.capacity() <= LUCEBOX_FORMAL_MAX_CAP); + assert(state.size() >= 0); + assert(state.size() <= state.capacity()); + assert(state.next_slot() >= 0); + assert(state.next_slot() < state.capacity()); + + const auto & entries = state.entries(); + for (size_t i = 0; i < entries.size(); ++i) { + assert(entries[i].slot >= 0); + assert(entries[i].slot < state.capacity()); + assert(!entries[i].ids.empty()); + assert(entries[i].ids.size() <= 3); + for (size_t j = i + 1; j < entries.size(); ++j) { + assert(entries[i].slot != entries[j].slot); + assert(!prefix_hash_equal(entries[i].hash, entries[j].hash)); + } + } + + if (state.has_pending_eviction()) { + assert(state.contains(state.pending_eviction_key())); + } +} + +} // namespace + +int main() { + const int capacity = (int)bounded(LUCEBOX_FORMAL_MAX_CAP) + 1; + const unsigned int branch = bounded(3); + const int depth = (int)bounded(3) + 1; + ContractState state(capacity); + const PrefixHash key = make_key(branch, depth); + const std::vector ids = make_ids(branch, depth); + + const auto reservation = state.prepare(key, depth); + assert(reservation.slot >= 0); + assert(reservation.slot < capacity); + assert(reservation.target_cut == depth); + assert(!state.has_pending_eviction()); + + const auto confirmed = + state.confirm(reservation.slot, key, depth, ids); + assert(confirmed.accepted); + assert(state.size() == 1); + assert(state.contains(key)); + assert(state.entries()[0].ids.size() == (size_t)depth); + for (int i = 0; i < depth; ++i) { + assert(state.entries()[0].ids[(size_t)i] == ids[(size_t)i]); + } + + const auto found = state.lookup_candidate(key, depth); + assert(found.slot == reservation.slot); + assert(found.prefix_len == depth); + assert(!found.stale_removed); + assert_invariants(state); + return 0; +} diff --git a/formal/contracts/templates/spec-commit-exactness.cpp.in b/formal/contracts/templates/spec-commit-exactness.cpp.in new file mode 100644 index 000000000..b5b0eae02 --- /dev/null +++ b/formal/contracts/templates/spec-commit-exactness.cpp.in @@ -0,0 +1,3 @@ +// Generated protected wrapper for {{ID}}: {{SIGNATURE}} +#define LUCEBOX_FORMAL_CONTRACT_SYMBOL {{SYMBOL}} +#include "spec_commit/spec_commit_harness_body.h" diff --git a/formal/contracts/tests/test_formal_plan.py b/formal/contracts/tests/test_formal_plan.py new file mode 100644 index 000000000..db993b8bf --- /dev/null +++ b/formal/contracts/tests/test_formal_plan.py @@ -0,0 +1,230 @@ +from __future__ import annotations + +import importlib.util +import json +import re +import tempfile +import tomllib +import unittest +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[3] +SCRIPT = ROOT / "scripts" / "formal_plan.py" +REGISTRY = ROOT / "formal" / "contracts" / "registry.toml" + +spec = importlib.util.spec_from_file_location("formal_plan", SCRIPT) +assert spec and spec.loader +formal_plan = importlib.util.module_from_spec(spec) +spec.loader.exec_module(formal_plan) + + +class FormalPlanTest(unittest.TestCase): + def plan_fixture(self, name: str) -> dict: + fixture = json.loads( + (ROOT / "formal" / "contracts" / "fixtures" / name).read_text() + ) + return formal_plan.make_plan(REGISTRY, ROOT, fixture["changed_paths"]) + + def test_registry_is_valid(self) -> None: + registry = formal_plan.load_registry(REGISTRY, ROOT) + self.assertEqual(registry["schema_version"], 1) + self.assertEqual( + [target["id"] for target in registry["targets"]], + [ + "prefix-cache-inline", + "prefix-cache-abort-hole", + "prefix-cache-full-lifecycle", + "spec-commit-exactness", + "kvflash-residency-map", + ], + ) + prefix_area = next( + area + for area in registry["critical_paths"] + if area["id"] == "prefix-cache" + ) + self.assertEqual(prefix_area["policy"], "advisory") + self.assertEqual(prefix_area["include_roots"], ["server/src"]) + self.assertIn( + "server/src/server/*eviction*.h", + prefix_area["watch_paths"], + ) + kvflash_target = next( + target + for target in registry["targets"] + if target["id"] == "kvflash-residency-map" + ) + self.assertEqual(kvflash_target["policy"], "advisory") + self.assertEqual( + kvflash_target["pr_defines"], + ["LUCEBOX_FORMAL_BLOCKS=4"], + ) + self.assertEqual( + kvflash_target["nightly_defines"], + ["LUCEBOX_FORMAL_BLOCKS=5"], + ) + self.assertEqual(kvflash_target["timeout_seconds"], 180) + + def test_registry_and_legacy_manifest_pin_the_same_toolchain(self) -> None: + registry = formal_plan.load_registry(REGISTRY, ROOT) + manifest_path = registry["registry"]["compatibility_manifest"] + manifest = tomllib.loads((ROOT / manifest_path).read_text()) + self.assertEqual(registry["toolchain"], manifest["toolchain"]) + + def test_workflow_image_pins_match_registry_toolchain(self) -> None: + toolchain = formal_plan.load_registry(REGISTRY, ROOT)["toolchain"] + workflows = { + ".github/workflows/formal.yml": { + "VERIFIER_IMAGE": (toolchain["verifier_image"], 3), + "REPAIR_IMAGE": (toolchain["repair_image"], 1), + }, + ".github/workflows/formal-nightly.yml": { + "VERIFIER_IMAGE": (toolchain["verifier_image"], 3), + "REPAIR_IMAGE": (toolchain["repair_image"], 1), + }, + ".github/workflows/formal-ai.yml": { + "REPAIR_IMAGE": (toolchain["repair_image"], 4), + }, + } + assignment_pattern = re.compile( + r"^\s*(VERIFIER_IMAGE|REPAIR_IMAGE):\s*(\S+)\s*$", + re.MULTILINE, + ) + for relative, expected in workflows.items(): + assignments = assignment_pattern.findall((ROOT / relative).read_text()) + self.assertEqual( + {name for name, _ in assignments}, + set(expected), + relative, + ) + for name, (expected_value, expected_count) in expected.items(): + values = [value for actual_name, value in assignments if actual_name == name] + self.assertEqual(len(values), expected_count, f"{relative}: {name}") + self.assertEqual( + values, + [expected_value] * expected_count, + f"{relative}: {name}", + ) + + def test_prefix_cache_fixture_selects_approved_targets(self) -> None: + plan = self.plan_fixture("prefix-cache-change.json") + self.assertEqual( + [target["id"] for target in plan["targets"]], + [ + "prefix-cache-inline", + "prefix-cache-abort-hole", + "prefix-cache-full-lifecycle", + ], + ) + self.assertEqual(plan["coverage_gaps"], []) + + def test_spec_commit_fixture_selects_exactness_target(self) -> None: + plan = self.plan_fixture("spec-commit-change.json") + self.assertEqual( + [target["id"] for target in plan["targets"]], + ["spec-commit-exactness"], + ) + self.assertEqual(plan["coverage_gaps"], []) + + def test_kvflash_fixture_selects_residency_target(self) -> None: + plan = self.plan_fixture("kvflash-change.json") + self.assertEqual( + [target["id"] for target in plan["targets"]], + ["kvflash-residency-map"], + ) + self.assertEqual(plan["coverage_gaps"], []) + + def test_registry_execution_matches_legacy_capsules_during_dual_run(self) -> None: + registry = formal_plan.load_registry(REGISTRY, ROOT) + manifest = tomllib.loads((ROOT / "formal" / "manifest.toml").read_text()) + legacy = {capsule["id"]: capsule for capsule in manifest["capsules"]} + for target in registry["targets"]: + capsule = legacy[target["id"]] + self.assertEqual(target["description"], capsule["description"]) + self.assertEqual(target["entry_function"], capsule["entry_function"]) + self.assertEqual(target["include_dirs"], capsule["include_dirs"]) + self.assertEqual(target["timeout_seconds"], capsule["timeout_seconds"]) + self.assertEqual( + target["nightly_timeout_seconds"], + capsule.get("nightly_timeout_seconds", capsule["timeout_seconds"]), + ) + self.assertEqual(target["pr_defines"], capsule["defines"]) + self.assertEqual(target["nightly_defines"], capsule["nightly_defines"]) + self.assertEqual(target["pr_esbmc_args"], capsule["esbmc_args"]) + self.assertEqual(target["nightly_esbmc_args"], capsule["esbmc_args"]) + self.assertEqual(target["mutable_paths"], capsule["mutable_paths"]) + self.assertEqual(target.get("native_test"), capsule.get("native_test")) + self.assertEqual( + target.get("native_test_source"), + capsule.get("native_test_source"), + ) + + def test_transitive_formal_template_includes_are_protected(self) -> None: + registry = formal_plan.load_registry(REGISTRY, ROOT) + expected_bodies = { + "prefix-cache-full-lifecycle": ( + "formal/prefix_cache/full_lifecycle_harness_body.h" + ), + "spec-commit-exactness": ( + "formal/spec_commit/spec_commit_harness_body.h" + ), + "kvflash-residency-map": ( + "formal/kvflash/residency_map_harness_body.h" + ), + } + for target in registry["targets"]: + template = (ROOT / target["template"]).read_text(encoding="utf-8") + resolved_formal_paths = set() + for included in re.findall(r'#include\s+"([^"]+)"', template): + candidates = [included] + candidates.extend( + str(Path(include_dir) / included) + for include_dir in target["include_dirs"] + ) + resolved_formal_paths.update( + path + for path in candidates + if path.startswith("formal/") and (ROOT / path).is_file() + ) + + if "formal" in target["include_dirs"]: + self.assertTrue(resolved_formal_paths, target["id"]) + if target["id"] in expected_bodies: + self.assertIn( + expected_bodies[target["id"]], + resolved_formal_paths, + target["id"], + ) + for formal_path in resolved_formal_paths: + self.assertIn( + formal_path, + target["contract_paths"], + target["id"], + ) + self.assertIn( + formal_path, + target["trigger_paths"], + target["id"], + ) + + def test_uncovered_critical_path_is_advisory_gap(self) -> None: + plan = self.plan_fixture("uncovered-streaming-change.json") + self.assertEqual(plan["targets"], []) + self.assertEqual(plan["coverage_gaps"][0]["id"], "streaming-lifecycle") + self.assertEqual(plan["coverage_gaps"][0]["policy"], "advisory") + + def test_emit_copies_approved_template_and_records_hash(self) -> None: + plan = self.plan_fixture("prefix-cache-change.json") + with tempfile.TemporaryDirectory() as temporary: + output = Path(temporary) + formal_plan._emit_templates(plan, ROOT, output) + emitted = plan["generated_harnesses"] + self.assertEqual(len(emitted), 3) + for item in emitted: + self.assertTrue((output / item["path"]).is_file()) + self.assertEqual(len(item["sha256"]), 64) + + +if __name__ == "__main__": + unittest.main() diff --git a/formal/kvflash/RESIDENCY_MAP_PROPERTIES.md b/formal/kvflash/RESIDENCY_MAP_PROPERTIES.md new file mode 100644 index 000000000..5d0f14b80 --- /dev/null +++ b/formal/kvflash/RESIDENCY_MAP_PROPERTIES.md @@ -0,0 +1,54 @@ +# KVFlash residency-map contract + +`kvflash-residency-map` checks the dependency-free production +`dflash::common::KvFlashResidencyMap` used by `KvFlashPager`. Pull-request +proofs use four one-token physical blocks; nightly proofs use five, adding a +non-power-of-two pool. ESBMC checks the named identity-fill, failed-eviction, +protected-LRU-eviction, mask, and logical-bound sequences. The exact-head +native regression covers the broader chunk offsets, recall, explicit page-out, +block order, reset, and scored paths. + +The initial six-block nightly bound reached the declared 180-second timeout in +both generated and legacy lanes on GitHub-hosted runners. Five blocks retains a +strict nightly expansion without weakening the shared PR timeout. Six blocks +remains a future harness/solver optimization target rather than claimed proof +coverage. + +## Model-checked guarantees for the named sequences + +- invalid chunk sizes, pool sizes, protection counts, partial blocks, and + eviction-deadlocking pools are rejected, and logical positions are bounded + before vector growth; +- the filled and post-eviction maps satisfy the runtime partial-bijection and + resident/free-complement invariant; +- `acquire` and `slot_of` agree on block and in-block token offsets; +- initial allocation follows identity placement and + `identity_prefix_covers` requires every intersecting prefix chunk to be + resident in its identity block; +- automatic eviction excludes configured sink chunks and the protected append + tail; +- the page-out callback succeeds before ownership transfers to a new chunk; +- a rejected page-out callback preserves the map's logical extent, ownership, + free blocks, append-head policy, and epoch; +- every successful residency change advances the epoch; +- slot-position and slot-validity arrays agree with resident ownership. + +The exact-head native regression additionally covers malformed block orders, +explicit page-out failure, score-independent LRU selection, large and negative +positions, mask values, and runtime representation invariants. + +## Deliberate exclusions + +This capsule does not prove: + +- CUDA/HIP allocation, asynchronous ordering, DMA success, or copied bytes; +- KV tensor shape, stride, numerical values, or attention output; +- host-backing allocation size and lifetime; +- score quality or floating-point ordering in lookahead reselect; +- concurrent access. + +The pager adapter owns device and host storage. Its page-out callback is an +abstract success/failure boundary in this proof; the map cannot roll back +external side effects from a callback that returns false. The production pager +therefore returns false only before DMA, zeroing, or statistic changes. GPU +parity remains a separate native/nightly responsibility. diff --git a/formal/kvflash/residency_map_harness.cpp b/formal/kvflash/residency_map_harness.cpp new file mode 100644 index 000000000..2a8d661a9 --- /dev/null +++ b/formal/kvflash/residency_map_harness.cpp @@ -0,0 +1,2 @@ +#define LUCEBOX_FORMAL_CONTRACT_SYMBOL dflash::common::KvFlashResidencyMap +#include "residency_map_harness_body.h" diff --git a/formal/kvflash/residency_map_harness_body.h b/formal/kvflash/residency_map_harness_body.h new file mode 100644 index 000000000..30ea259c3 --- /dev/null +++ b/formal/kvflash/residency_map_harness_body.h @@ -0,0 +1,157 @@ +// Shared body for generated and legacy KVFlash residency-map harnesses. + +#include "common/kvflash_residency_map.h" + +#include +#include + +#ifndef LUCEBOX_FORMAL_CONTRACT_SYMBOL +#error "LUCEBOX_FORMAL_CONTRACT_SYMBOL must name the production map type" +#endif + +#ifndef LUCEBOX_FORMAL_BLOCKS +#define LUCEBOX_FORMAL_BLOCKS 4 +#endif + +using ContractMap = LUCEBOX_FORMAL_CONTRACT_SYMBOL; +using dflash::common::KvFlashConfig; + +namespace { + +constexpr int kChunkTokens = 1; +constexpr int kPoolTokens = LUCEBOX_FORMAL_BLOCKS; +constexpr int kMaxLogicalTokens = LUCEBOX_FORMAL_BLOCKS + 2; +constexpr uint16_t kF16Zero = 0x0000; +constexpr uint16_t kF16NegInf = 0xFC00; + +bool accept_page_out(void *, int, int) { + return true; +} + +bool reject_page_out(void *, int, int) { + return false; +} + +ContractMap::PreparePageOut accepting() { + return {nullptr, &accept_page_out}; +} + +ContractMap::PreparePageOut rejecting() { + return {nullptr, &reject_page_out}; +} + +KvFlashConfig config() { + KvFlashConfig cfg; + cfg.chunk_tokens = kChunkTokens; + cfg.pool_tokens = kPoolTokens; + cfg.sink_chunks = 1; + cfg.tail_window_chunks = 1; + cfg.max_logical_tokens = kMaxLogicalTokens; + return cfg; +} + +void fill_identity(ContractMap & map) { + for (int chunk = 0; chunk < LUCEBOX_FORMAL_BLOCKS; ++chunk) { + const auto acquired = map.acquire(chunk); + assert(acquired); + assert(acquired.chunk == chunk); + assert(acquired.block == chunk); + assert(acquired.slot == chunk); + assert(map.slot_of(chunk) == chunk); + } + assert(map.resident_blocks() == LUCEBOX_FORMAL_BLOCKS); + assert(map.free_blocks().empty()); + assert(map.is_identity()); + assert(map.identity_prefix_covers(kPoolTokens)); + assert(!map.identity_prefix_covers(kPoolTokens + 1)); + assert(map.invariant_holds()); +} + +} // namespace + +int main() { + static_assert(LUCEBOX_FORMAL_BLOCKS >= 4); + + KvFlashConfig cfg = config(); + assert(ContractMap::valid_config(cfg)); + assert(ContractMap::min_pool_tokens(cfg) <= cfg.pool_tokens); + KvFlashConfig invalid = cfg; + invalid.chunk_tokens = 0; + assert(!ContractMap::valid_config(invalid)); + invalid = cfg; + invalid.max_logical_tokens = cfg.pool_tokens - 1; + assert(!ContractMap::valid_config(invalid)); + + ContractMap map; + assert(map.configure(cfg)); + fill_identity(map); + const uint64_t full_epoch = map.epoch(); + int owners[LUCEBOX_FORMAL_BLOCKS]; + for (int chunk = 0; chunk < LUCEBOX_FORMAL_BLOCKS; ++chunk) { + owners[chunk] = map.block_of(chunk); + } + + // Callback rejection must leave the complete map transition uncommitted. + const auto rejected = + map.acquire(LUCEBOX_FORMAL_BLOCKS, {}, rejecting()); + assert(!rejected); + assert(map.epoch() == full_epoch); + assert(map.n_chunks() == LUCEBOX_FORMAL_BLOCKS); + for (int chunk = 0; chunk < LUCEBOX_FORMAL_BLOCKS; ++chunk) { + assert(map.block_of(chunk) == owners[chunk]); + } + assert(map.invariant_holds()); + + // With one sink and one protected tail, LRU must transfer chunk 1's block + // to the new append head while preserving both protected mappings. + const auto evicted = + map.acquire(LUCEBOX_FORMAL_BLOCKS, {}, accepting()); + assert(evicted); + assert(evicted.changed); + assert(evicted.evicted_chunk == 1); + assert(evicted.block == 1); + assert(evicted.slot == 1); + assert(map.is_resident(0)); + assert(map.block_of(0) == 0); + assert(map.is_resident(LUCEBOX_FORMAL_BLOCKS - 1)); + assert( + map.block_of(LUCEBOX_FORMAL_BLOCKS - 1) == + LUCEBOX_FORMAL_BLOCKS - 1); + assert(!map.is_resident(1)); + assert(map.is_host_backed(1)); + assert(map.block_of(LUCEBOX_FORMAL_BLOCKS) == 1); + assert(map.slot_of(LUCEBOX_FORMAL_BLOCKS) == 1); + assert(map.resident_blocks() == LUCEBOX_FORMAL_BLOCKS); + assert(map.free_blocks().empty()); + assert(map.epoch() == full_epoch + 2); + assert(!map.is_identity()); + assert(map.invariant_holds()); + + int32_t positions[kPoolTokens]; + uint16_t masks[kPoolTokens]; + map.fill_slot_pos(positions); + map.fill_slot_mask(masks); + for (int block = 0; block < LUCEBOX_FORMAL_BLOCKS; ++block) { + assert(masks[block] == kF16Zero); + if (block == 1) { + assert(positions[block] == LUCEBOX_FORMAL_BLOCKS); + } else { + assert(positions[block] == block); + } + } + + // An out-of-range logical position is rejected before sparse growth. + assert(!map.acquire(kMaxLogicalTokens)); + assert(map.slot_of(kMaxLogicalTokens) == -1); + + // The validity mask sentinel is also checked on an empty configured map. + ContractMap empty; + assert(empty.configure(cfg)); + empty.fill_slot_pos(positions); + empty.fill_slot_mask(masks); + for (int slot = 0; slot < kPoolTokens; ++slot) { + assert(positions[slot] == -1); + assert(masks[slot] == kF16NegInf); + } + return 0; +} diff --git a/formal/manifest.toml b/formal/manifest.toml new file mode 100644 index 000000000..504d1ef68 --- /dev/null +++ b/formal/manifest.toml @@ -0,0 +1,209 @@ +schema_version = 1 + +[toolchain] +esbmc_version = "8.4" +esbmc_linux_sha256 = "68bb71128e0c3c2db090955e7a302533a8a11a9d898df7f169c22311a0ec5078" +verifier_image = "ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e" +repair_image = "ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597" + +[[capsules]] +id = "prefix-cache-inline" +description = "Inline prefix-cache prepare, confirm, exact lookup, and structural invariants" +harness = "formal/prefix_cache/prefix_cache_harness.cpp" +entry_function = "main" +include_dirs = ["server/src"] +timeout_seconds = 120 +defines = [ + "LUCEBOX_FORMAL_MAX_CAP=4", +] +nightly_defines = [ + "LUCEBOX_FORMAL_MAX_CAP=16", +] +esbmc_args = [ + "--quiet", + "--z3", + "--unwind", "5", + "--memory-leak-check", + "--overflow-check", +] +trigger_paths = [ + "formal/**", + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", + "server/test/test_prefix_cache_state.cpp", +] +mutable_paths = [ + "server/src/server/prefix_cache_state.h", +] +contract_paths = [ + "formal/manifest.toml", + "formal/prefix_cache/prefix_cache_harness.cpp", + "formal/prefix_cache/PROPERTIES.md", + "server/test/test_prefix_cache_state.cpp", +] + +[[capsules]] +id = "prefix-cache-abort-hole" +description = "Inline prefix-cache free-slot selection after an aborted reservation" +harness = "formal/prefix_cache/abort_hole_harness.cpp" +entry_function = "verify_select_inline_free_slot_contract" +include_dirs = ["server/src"] +timeout_seconds = 120 +defines = [ + "LUCEBOX_FORMAL_MAX_CAP=4", +] +nightly_defines = [ + "LUCEBOX_FORMAL_MAX_CAP=16", +] +esbmc_args = [ + "--quiet", + "--z3", + "--enforce-contract", "verify_select_inline_free_slot_contract", + "--unwind", "17", + "--overflow-check", +] +trigger_paths = [ + "formal/**", + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", + "server/test/test_prefix_cache_state.cpp", +] +mutable_paths = [ + "server/src/server/prefix_cache_state.h", +] +contract_paths = [ + "formal/manifest.toml", + "formal/prefix_cache/abort_hole_harness.cpp", + "formal/contracts/mutations/prefix-cache-bypass-selector.patch", + "formal/prefix_cache/ABORT_HOLE_PROPERTIES.md", + "server/test/test_prefix_cache_state.cpp", +] +native_test = "test_prefix_cache_state" +native_test_source = "server/test/test_prefix_cache_state.cpp" + +[[capsules]] +id = "prefix-cache-full-lifecycle" +description = "Full prefix-cache fresh boundary/confirm proof with exact-head lifecycle regression" +harness = "formal/prefix_cache/full_lifecycle_harness.cpp" +entry_function = "main" +include_dirs = ["server/src", "formal"] +timeout_seconds = 120 +defines = [ + "LUCEBOX_FORMAL_CAP=2", +] +nightly_defines = [ + "LUCEBOX_FORMAL_CAP=4", +] +esbmc_args = [ + "--quiet", + "--boolector", + "--unwind", "5", + "--overflow-check", +] +trigger_paths = [ + "formal/**", + "server/src/server/prefix_cache_state.h", + "server/src/server/prefix_cache.h", + "server/src/server/prefix_cache.cpp", + "server/test/test_full_prefix_cache_state.cpp", +] +mutable_paths = [ + "server/src/server/prefix_cache_state.h", +] +contract_paths = [ + "formal/manifest.toml", + "formal/prefix_cache/full_lifecycle_harness.cpp", + "formal/prefix_cache/full_lifecycle_harness_body.h", + "formal/contracts/mutations/prefix-cache-full-bypass-free-slot.patch", + "formal/prefix_cache/FULL_LIFECYCLE_PROPERTIES.md", + "server/test/test_full_prefix_cache_state.cpp", +] +native_test = "test_full_prefix_cache_state" +native_test_source = "server/test/test_full_prefix_cache_state.cpp" + +[[capsules]] +id = "spec-commit-exactness" +description = "Linear speculative acceptance, bonus availability, budget clipping, and safe token selection" +harness = "formal/spec_commit/spec_commit_harness.cpp" +entry_function = "main" +include_dirs = ["server/src", "formal"] +timeout_seconds = 120 +defines = [ + "LUCEBOX_FORMAL_MAX_WIDTH=4", +] +nightly_defines = [ + "LUCEBOX_FORMAL_MAX_WIDTH=8", +] +esbmc_args = [ + "--quiet", + "--z3", + "--unwind", "17", + "--memory-leak-check", + "--overflow-check", +] +trigger_paths = [ + "formal/**", + "server/src/common/spec_commit.h", + "server/src/common/dflash_spec_decode.cpp", + "server/src/qwen35/qwen35_backend.cpp", + "server/src/qwen35moe/qwen35moe_backend.cpp", + "server/src/laguna/laguna_backend.cpp", + "server/src/gemma4/gemma4_backend.cpp", + "server/test/test_spec_commit.cpp", +] +mutable_paths = [ + "server/src/common/spec_commit.h", +] +contract_paths = [ + "formal/manifest.toml", + "formal/spec_commit/spec_commit_harness.cpp", + "formal/spec_commit/spec_commit_harness_body.h", + "formal/contracts/mutations/spec-commit-invert-prefix-match.patch", + "formal/spec_commit/PROPERTIES.md", + "server/test/test_spec_commit.cpp", +] +native_test = "test_spec_commit" +native_test_source = "server/test/test_spec_commit.cpp" + +[[capsules]] +id = "kvflash-residency-map" +description = "KVFlash identity map, callback rollback, protected LRU eviction, logical bounds, and slot masks" +harness = "formal/kvflash/residency_map_harness.cpp" +entry_function = "main" +include_dirs = ["server/src", "formal"] +timeout_seconds = 180 +nightly_timeout_seconds = 240 +defines = [ + "LUCEBOX_FORMAL_BLOCKS=4", +] +nightly_defines = [ + "LUCEBOX_FORMAL_BLOCKS=5", +] +esbmc_args = [ + "--quiet", + "--boolector", + "--unwind", "14", + "--overflow-check", +] +trigger_paths = [ + "formal/**", + "server/src/common/kvflash_residency_map.h", + "server/src/common/kvflash_pager.h", + "server/test/test_kvflash_residency_map.cpp", + "server/test/test_kvflash.cpp", +] +mutable_paths = [ + "server/src/common/kvflash_residency_map.h", +] +contract_paths = [ + "formal/manifest.toml", + "formal/kvflash/residency_map_harness.cpp", + "formal/kvflash/residency_map_harness_body.h", + "formal/contracts/mutations/kvflash-capacity-off-by-one.patch", + "formal/kvflash/RESIDENCY_MAP_PROPERTIES.md", + "server/test/test_kvflash_residency_map.cpp", +] +native_test = "test_kvflash_residency_map" +native_test_source = "server/test/test_kvflash_residency_map.cpp" diff --git a/formal/prefix_cache/ABORT_HOLE_PROPERTIES.md b/formal/prefix_cache/ABORT_HOLE_PROPERTIES.md new file mode 100644 index 000000000..59c69c079 --- /dev/null +++ b/formal/prefix_cache/ABORT_HOLE_PROPERTIES.md @@ -0,0 +1,33 @@ +# Inline prefix-cache abort-hole allocation contract + +The capsule enforces a native ESBMC function contract around the scalar +`select_inline_free_slot` helper for every bounded cursor and occupancy +pattern. The deterministic plan also compiles and runs an immutable +base-revision regression against the exact PR head. That regression drives the +production `InlinePrefixCacheState` through the historical defect sequence: +commit slot zero, reserve and abort slot one, then call `prepare` again while +the round-robin cursor points at occupied slot zero. + +## Checked properties + +- Scalar selection returns an in-range, unoccupied slot whenever one exists. +- The scalar selector cannot mutate program state. +- ESBMC's default pointer and bounds checks plus integer overflow checks remain + enabled. + +The paired native regression checks that aborting preserves every committed +entry and the replacement `prepare` call reuses the aborted slot. Those +integration assertions are regression-tested rather than described as +model-checked properties. + +## Bounded operating envelope + +The formal capsule covers capacities 1–4 in pull requests and 1–16 in extended +runs. The native regression fixes capacity at two, the smallest state that +reproduces the production call-site defect. `PrefixCache` clamps inline +capacity to 64 slots; the formal capsule does not claim coverage beyond its +declared bound. + +On a contract violation, the deterministic lane publishes ESBMC's native, +self-contained HTML counterexample report alongside the textual trace and +immutable repair bundle. diff --git a/formal/prefix_cache/FULL_LIFECYCLE_PROPERTIES.md b/formal/prefix_cache/FULL_LIFECYCLE_PROPERTIES.md new file mode 100644 index 000000000..92242f10a --- /dev/null +++ b/formal/prefix_cache/FULL_LIFECYCLE_PROPERTIES.md @@ -0,0 +1,45 @@ +# Full prefix-cache lifecycle contract + +`prefix-cache-full-lifecycle` checks the production +`dflash::common::FullPrefixCacheState` used by `PrefixCache` for exact +full-prompt snapshots. Pull-request proofs use capacity two and nightly proofs +use capacity four. ESBMC model-checks the fresh +prepare/invalid-confirm/confirm/lookup/clear sequence for every symbolic +snapshot boundary from one through four. The immutable native regression +covers the wider capacities, abort, hole-reuse, and LRU lifecycle against the +exact head. + +## Model-checked guarantees for the named traces + +- configuration accepts only a non-empty, non-overflowing absolute slot range + that excludes the disk staging slot; +- the fresh reservation owns one in-range non-staging slot; +- prepare binds the effective-prompt snapshot boundary independently of the + raw prompt used as the lookup key; +- confirm succeeds only for the matching key and slot, a still-valid victim, + a positive raw prompt length, and a saved position inside the prepared + effective-prompt boundary; +- a successful fresh confirm installs the requested key and clears the + reservation; +- invalid confirmation leaves the pending reservation and committed ownership + unchanged; +- exact lookup returns the confirmed slot and saved position; +- clear removes every entry and reservation and resets the allocation cursor. + +The exact-head native regression also checks the production sequences for the +capacity-two abort hole, LRU touch and victim selection, victim abort, invalid +reservation inputs, staging-slot exclusion, and independent committed-slot +invalidation. + +## Deliberate exclusions + +This capsule does not prove: + +- hashing collision resistance; +- GPU snapshot creation, restoration, or byte identity; +- the atomic public size mirror or HTTP request orchestration; +- disk-cache staging I/O; +- concurrent access (the production state is daemon-thread owned). + +The `PrefixCache` adapter remains responsible for hashing prompts, invoking +backend snapshot operations, synchronizing its atomic size mirror, and logging. diff --git a/formal/prefix_cache/PROPERTIES.md b/formal/prefix_cache/PROPERTIES.md new file mode 100644 index 000000000..d03b38e26 --- /dev/null +++ b/formal/prefix_cache/PROPERTIES.md @@ -0,0 +1,32 @@ +# Inline prefix-cache verification capsule + +This capsule model-checks the production `InlinePrefixCacheState` transition +core used by `PrefixCache`. + +## Checked properties + +- A fresh reservation returns an in-range slot and the requested depth. +- A valid confirmation creates exactly one committed entry. +- Exact lookup returns the committed slot and prefix length. +- The number of committed entries never exceeds capacity. +- Every committed entry owns one in-range slot. +- The committed token prefix is non-empty and has the confirmed length. +- A fresh reservation does not spuriously create a pending eviction. +- ESBMC's pointer, bounds, memory-leak, and integer checks remain enabled. + +## Bounded operating envelope + +Pull requests cover a symbolic fresh-cache prepare/confirm/lookup path for +capacities 1–4. Extended runs widen the capacity domain to 1–16. Each generated +prefix has one to three tokens and belongs to one of three branches. + +Abort, cancellation, stale lookup, invalid confirmation, clearing, slot reuse, +and prefix-aware eviction are exercised by the immutable native regression +test. They are intentionally not described as model-checked properties in this +first capsule. + +The harness models prefix hashes as collision-free identifiers derived from the +bounded prefix family. It does not prove tokenizer correctness, SHA-1 collision +resistance, cache performance, backend snapshot correctness, or whole-server +behavior. A successful result is a bounded proof for this declared envelope, +not a claim that all Lucebox behavior is formally verified. diff --git a/formal/prefix_cache/abort_hole_harness.cpp b/formal/prefix_cache/abort_hole_harness.cpp new file mode 100644 index 000000000..5ebcb29ee --- /dev/null +++ b/formal/prefix_cache/abort_hole_harness.cpp @@ -0,0 +1,35 @@ +#include "server/prefix_cache_state.h" + +#include + +#ifndef LUCEBOX_FORMAL_MAX_CAP +#define LUCEBOX_FORMAL_MAX_CAP 4 +#endif + +using dflash::common::select_inline_free_slot; + +static_assert( + LUCEBOX_FORMAL_MAX_CAP > 0 && LUCEBOX_FORMAL_MAX_CAP < 64); + +int verify_select_inline_free_slot_contract( + int next_slot, int capacity, uint64_t occupied_slots) { + // Model the below-capacity state after an aborted reservation: the cursor + // may name an occupied slot, but at least one in-range slot remains free. + __ESBMC_requires( + capacity > 0 && capacity <= LUCEBOX_FORMAL_MAX_CAP); + __ESBMC_requires(next_slot >= 0 && next_slot < capacity); + __ESBMC_requires((occupied_slots >> capacity) == 0); + __ESBMC_requires( + occupied_slots != ((uint64_t{1} << capacity) - 1)); + + // Slot selection is scalar and must not mutate program state. + __ESBMC_assigns(); + __ESBMC_ensures(__ESBMC_return_value >= 0); + __ESBMC_ensures(__ESBMC_return_value < capacity); + __ESBMC_ensures( + (occupied_slots & + (uint64_t{1} << __ESBMC_return_value)) == 0); + + return select_inline_free_slot( + next_slot, capacity, occupied_slots); +} diff --git a/formal/prefix_cache/full_lifecycle_harness.cpp b/formal/prefix_cache/full_lifecycle_harness.cpp new file mode 100644 index 000000000..e2567e0a2 --- /dev/null +++ b/formal/prefix_cache/full_lifecycle_harness.cpp @@ -0,0 +1,2 @@ +#define LUCEBOX_FORMAL_CONTRACT_SYMBOL dflash::common::FullPrefixCacheState +#include "full_lifecycle_harness_body.h" diff --git a/formal/prefix_cache/full_lifecycle_harness_body.h b/formal/prefix_cache/full_lifecycle_harness_body.h new file mode 100644 index 000000000..d6f23e479 --- /dev/null +++ b/formal/prefix_cache/full_lifecycle_harness_body.h @@ -0,0 +1,108 @@ +// Shared body for generated and legacy full prefix-cache harnesses. + +#include "server/prefix_cache_state.h" + +#include +#include + +#ifndef LUCEBOX_FORMAL_CONTRACT_SYMBOL +#error "LUCEBOX_FORMAL_CONTRACT_SYMBOL must name the production state type" +#endif + +#ifndef LUCEBOX_FORMAL_CAP +#define LUCEBOX_FORMAL_CAP 2 +#endif + +extern "C" unsigned int nondet_uint(); +extern "C" void __ESBMC_assume(bool); + +using ContractState = LUCEBOX_FORMAL_CONTRACT_SYMBOL; +using dflash::common::PrefixHash; + +namespace { + +constexpr int kSlotBase = 8; +constexpr int kStagingSlot = 63; + +unsigned int bounded(unsigned int upper_exclusive) { + const unsigned int value = nondet_uint(); + __ESBMC_assume(value < upper_exclusive); + return value; +} + +PrefixHash key(uint8_t value) { + PrefixHash result{}; + result[0] = value; + return result; +} + +} // namespace + +int main() { + static_assert(LUCEBOX_FORMAL_CAP > 0); + static_assert(LUCEBOX_FORMAL_CAP <= 8); + static_assert(kSlotBase + LUCEBOX_FORMAL_CAP < kStagingSlot); + + const int expected_snapshot_len = + static_cast(bounded(4)) + 1; + const int saved_pos = + static_cast(bounded( + static_cast(expected_snapshot_len))) + 1; + const PrefixHash first = key(1); + const PrefixHash wrong = key(2); + + ContractState state( + kSlotBase, LUCEBOX_FORMAL_CAP, kStagingSlot); + assert(state.enabled()); + assert(state.capacity() == LUCEBOX_FORMAL_CAP); + assert(state.size() == 0); + + const auto prepared = + state.prepare(first, expected_snapshot_len); + assert(prepared.accepted); + assert(!prepared.reuses_victim); + assert(prepared.slot >= kSlotBase); + assert(prepared.slot < kSlotBase + LUCEBOX_FORMAL_CAP); + assert(prepared.slot != kStagingSlot); + assert(prepared.expected_snapshot_len == expected_snapshot_len); + assert(state.has_pending_reservation()); + assert(state.pending_slot() == prepared.slot); + assert( + state.pending_expected_snapshot_len() == + expected_snapshot_len); + assert(state.size() == 0); + + // Neither a wrong key nor a saved position outside the prepared effective + // boundary may resolve the reservation. + assert(!state.confirm( + prepared.slot, wrong, 1, saved_pos, 1).accepted); + assert(!state.confirm( + prepared.slot, first, 1, expected_snapshot_len + 1, 1).accepted); + assert(state.has_pending_reservation()); + assert(state.size() == 0); + + // Raw prompt length is the lookup-key length and may be shorter than the + // effective/compressed snapshot position. + const auto confirmed = + state.confirm(prepared.slot, first, 1, saved_pos, 2); + assert(confirmed.accepted); + assert(state.size() == 1); + assert(state.contains(first)); + assert(!state.has_pending_reservation()); + + const auto hit = state.lookup(first, 3); + assert(hit.slot == prepared.slot); + assert(hit.cur_ids_len == saved_pos); + assert(state.size() == 1); + + state.clear(); + assert(state.size() == 0); + assert(!state.has_pending_reservation()); + assert(state.next_relative_slot() == 0); + + ContractState overlaps_staging( + kStagingSlot - 1, 2, kStagingSlot); + assert(!overlaps_staging.enabled()); + assert(!overlaps_staging.prepare(first, 1).accepted); + return 0; +} diff --git a/formal/prefix_cache/prefix_cache_harness.cpp b/formal/prefix_cache/prefix_cache_harness.cpp new file mode 100644 index 000000000..d6399add2 --- /dev/null +++ b/formal/prefix_cache/prefix_cache_harness.cpp @@ -0,0 +1,98 @@ +#include "server/prefix_cache_state.h" + +#include +#include +#include + +#ifndef LUCEBOX_FORMAL_MAX_CAP +#define LUCEBOX_FORMAL_MAX_CAP 4 +#endif + +extern "C" unsigned int nondet_uint(); +extern "C" void __ESBMC_assume(bool); + +using dflash::common::InlinePrefixCacheState; +using dflash::common::PrefixHash; +using dflash::common::prefix_hash_equal; + +namespace { + +unsigned int bounded(unsigned int upper_exclusive) { + const unsigned int value = nondet_uint(); + __ESBMC_assume(value < upper_exclusive); + return value; +} + +PrefixHash make_key(unsigned int branch, int depth) { + PrefixHash key{}; + key[0] = (uint8_t)depth; + key[1] = (uint8_t)(branch + 1); + return key; +} + +std::vector make_ids(unsigned int branch, int depth) { + std::vector ids; + ids.push_back(7); + if (depth >= 2) ids.push_back((int32_t)(20 + branch)); + if (depth >= 3) ids.push_back((int32_t)(30 + branch)); + return ids; +} + +void assert_invariants(const InlinePrefixCacheState & state) { + assert(state.capacity() >= 1); + assert(state.capacity() <= LUCEBOX_FORMAL_MAX_CAP); + assert(state.size() >= 0); + assert(state.size() <= state.capacity()); + assert(state.next_slot() >= 0); + assert(state.next_slot() < state.capacity()); + + const auto & entries = state.entries(); + for (size_t i = 0; i < entries.size(); ++i) { + assert(entries[i].slot >= 0); + assert(entries[i].slot < state.capacity()); + assert(!entries[i].ids.empty()); + assert(entries[i].ids.size() <= 3); + for (size_t j = i + 1; j < entries.size(); ++j) { + assert(entries[i].slot != entries[j].slot); + assert(!prefix_hash_equal(entries[i].hash, entries[j].hash)); + } + } + + if (state.has_pending_eviction()) { + assert(state.contains(state.pending_eviction_key())); + } +} + +} // namespace + +int main() { + const int capacity = (int)bounded(LUCEBOX_FORMAL_MAX_CAP) + 1; + const unsigned int branch = bounded(3); + const int depth = (int)bounded(3) + 1; + InlinePrefixCacheState state(capacity); + const PrefixHash key = make_key(branch, depth); + const std::vector ids = make_ids(branch, depth); + + const auto reservation = state.prepare(key, depth); + assert(reservation.slot >= 0); + assert(reservation.slot < capacity); + assert(reservation.target_cut == depth); + assert(!state.has_pending_eviction()); + + const auto confirmed = + state.confirm(reservation.slot, key, depth, ids); + assert(confirmed.accepted); + assert(state.size() == 1); + assert(state.contains(key)); + assert(state.entries()[0].ids.size() == (size_t)depth); + for (int i = 0; i < depth; ++i) { + assert(state.entries()[0].ids[(size_t)i] == ids[(size_t)i]); + } + + const auto found = state.lookup_candidate(key, depth); + assert(found.slot == reservation.slot); + assert(found.prefix_len == depth); + assert(!found.stale_removed); + assert_invariants(state); + return 0; +} diff --git a/formal/spec_commit/PROPERTIES.md b/formal/spec_commit/PROPERTIES.md new file mode 100644 index 000000000..27f6601c5 --- /dev/null +++ b/formal/spec_commit/PROPERTIES.md @@ -0,0 +1,54 @@ +# Speculative-commit exactness contract + +`spec-commit-exactness` checks the dependency-free production decision core +`dflash::common::SpecCommitDecision`. The pull-request bound uses verification +widths and commit budgets up to four; the nightly bound raises both to eight. + +## Model-checked guarantees + +For greedy verification: + +- the accepted count is the longest draft prefix whose tokens are approved by + the preceding target rows; +- the seed token is always accepted and the accepted count stays in + `[1, verify_count]`; +- a target bonus is available exactly when the accepted prefix ends before the + verification width, while `commits_bonus` is true only when the remaining + generation budget can emit it; +- the commit count is non-negative, does not exceed the budget, and is at most + the accepted prefix plus one target bonus; +- every committed token selected by `token_at` is either an accepted draft + token at the same index or the one target token at the first mismatch; +- a negative mismatch target is treated as the no-bonus sentinel, so the + already-verified prefix remains committable; a negative accepted draft token + still cannot be emitted; +- clipped and out-of-range token requests fail instead of reading outside the + draft prefix or returning a unavailable bonus. + +For a model-specific verifier that supplies a precomputed accepted prefix: + +- accepted counts outside `[1, verify_count]` fail closed; +- a strict prefix may declare one non-negative target-selected mismatch token + or omit it when the model-specific verifier reports the negative no-token + sentinel; +- a fully accepted width must not declare a bonus; +- the same budget, bonus, and safe token-selection rules apply as in the + greedy path. + +The immutable native regression is also compiled against the exact PR head. +It exercises greedy match and mismatch decisions, budget clipping, the sampled +verification finalizer, malformed input, and safe materialization. + +## Deliberate exclusions + +This capsule does not prove: + +- target logits, sampling probabilities, or RNG history; +- model-family rollback, KV restore/replay, or feature-cache updates; +- EOS stopping, client cancellation, counters, or emitted network bytes; +- correctness of the draft or target model; +- tree speculative decoding. + +Those effects remain owned by model-family native and GPU tests. Later +capsules can abstract rollback and emission only after their production +orchestration is shared. diff --git a/formal/spec_commit/spec_commit_harness.cpp b/formal/spec_commit/spec_commit_harness.cpp new file mode 100644 index 000000000..309ad1d0f --- /dev/null +++ b/formal/spec_commit/spec_commit_harness.cpp @@ -0,0 +1,2 @@ +#define LUCEBOX_FORMAL_CONTRACT_SYMBOL dflash::common::SpecCommitDecision +#include "spec_commit_harness_body.h" diff --git a/formal/spec_commit/spec_commit_harness_body.h b/formal/spec_commit/spec_commit_harness_body.h new file mode 100644 index 000000000..0f35a03e4 --- /dev/null +++ b/formal/spec_commit/spec_commit_harness_body.h @@ -0,0 +1,137 @@ +// Shared body for the generated and legacy spec-commit exactness harnesses. + +#include "common/spec_commit.h" + +#include +#include + +#ifndef LUCEBOX_FORMAL_CONTRACT_SYMBOL +#error "LUCEBOX_FORMAL_CONTRACT_SYMBOL must name the production decision type" +#endif + +#ifndef LUCEBOX_FORMAL_MAX_WIDTH +#define LUCEBOX_FORMAL_MAX_WIDTH 4 +#endif + +extern "C" unsigned int nondet_uint(); +extern "C" int32_t nondet_int(); +extern "C" void __ESBMC_assume(bool); + +using ContractDecision = LUCEBOX_FORMAL_CONTRACT_SYMBOL; + +static unsigned int bounded(unsigned int upper_exclusive) { + const unsigned int value = nondet_uint(); + __ESBMC_assume(value < upper_exclusive); + return value; +} + +static void assert_safe_tokens( + const ContractDecision & decision, + const int32_t * draft, + int verify_count, + int32_t expected_bonus) { + for (int index = 0; index < decision.commit_count(); ++index) { + int32_t token = nondet_int(); + assert(decision.token_at(index, draft, verify_count, token)); + if (index < decision.accepted_count()) { + assert(token == draft[index]); + } else { + assert(index == decision.accepted_count()); + assert(decision.has_bonus()); + assert(decision.commits_bonus()); + assert(token == expected_bonus); + } + } + + int32_t ignored = nondet_int(); + assert(!decision.token_at(-1, draft, verify_count, ignored)); + assert(!decision.token_at( + decision.commit_count(), draft, verify_count, ignored)); +} + +int main() { + static_assert(LUCEBOX_FORMAL_MAX_WIDTH > 0); + const int verify_count = + static_cast(bounded(LUCEBOX_FORMAL_MAX_WIDTH)) + 1; + const int commit_budget = + static_cast(bounded(LUCEBOX_FORMAL_MAX_WIDTH + 1)); + + int32_t draft[LUCEBOX_FORMAL_MAX_WIDTH]; + int32_t target[LUCEBOX_FORMAL_MAX_WIDTH]; + for (int index = 0; index < verify_count; ++index) { + draft[index] = nondet_int(); + target[index] = nondet_int(); + __ESBMC_assume(draft[index] >= 0); + __ESBMC_assume(target[index] >= 0); + } + + const ContractDecision greedy = ContractDecision::greedy( + draft, verify_count, target, verify_count, + verify_count, commit_budget); + assert(greedy.valid()); + assert(greedy.accepted_count() >= 1); + assert(greedy.accepted_count() <= verify_count); + assert(greedy.commit_count() >= 0); + assert(greedy.commit_count() <= commit_budget); + assert(greedy.commit_count() <= greedy.accepted_count() + 1); + + for (int index = 1; index < greedy.accepted_count(); ++index) { + assert(draft[index] == target[index - 1]); + } + if (greedy.accepted_count() < verify_count) { + assert( + draft[greedy.accepted_count()] != + target[greedy.accepted_count() - 1]); + assert( + greedy.bonus_token() == + target[greedy.accepted_count() - 1]); + } + const bool greedy_bonus_available = + greedy.accepted_count() < verify_count; + const bool greedy_bonus_committed = + greedy_bonus_available && + commit_budget > greedy.accepted_count(); + assert(greedy.has_bonus() == greedy_bonus_available); + assert(greedy.commits_bonus() == greedy_bonus_committed); + assert_safe_tokens( + greedy, draft, verify_count, + target[greedy.accepted_count() - 1]); + + // Exercise the shared finalizer used by sampled/model-specific acceptance. + const int accepted = + static_cast(bounded(static_cast(verify_count))) + 1; + const bool bonus_available = accepted < verify_count; + const int32_t bonus = nondet_int(); + __ESBMC_assume(bonus >= 0); + const ContractDecision precomputed = ContractDecision::precomputed( + accepted, verify_count, bonus_available, bonus, commit_budget); + assert(precomputed.valid()); + assert(precomputed.accepted_count() == accepted); + assert(precomputed.commit_count() >= 0); + assert(precomputed.commit_count() <= commit_budget); + assert(precomputed.commit_count() <= accepted + 1); + assert(precomputed.has_bonus() == bonus_available); + assert( + precomputed.commits_bonus() == + (bonus_available && commit_budget > accepted)); + assert_safe_tokens(precomputed, draft, verify_count, bonus); + + assert(!ContractDecision::precomputed( + 0, verify_count, true, bonus, commit_budget).valid()); + assert(!ContractDecision::precomputed( + verify_count + 1, verify_count, false, bonus, commit_budget).valid()); + assert(!ContractDecision::precomputed( + verify_count, verify_count, true, bonus, commit_budget).valid()); + if (verify_count > 1) { + const ContractDecision sentinel_prefix = + ContractDecision::precomputed( + 1, verify_count, false, -1, commit_budget); + assert(sentinel_prefix.valid()); + assert(sentinel_prefix.accepted_count() == 1); + assert(!sentinel_prefix.has_bonus()); + assert(!sentinel_prefix.commits_bonus()); + assert_safe_tokens( + sentinel_prefix, draft, verify_count, bonus); + } + return 0; +} diff --git a/scripts/formal.sh b/scripts/formal.sh new file mode 100755 index 000000000..750c6f055 --- /dev/null +++ b/scripts/formal.sh @@ -0,0 +1,113 @@ +#!/usr/bin/env bash +set -euo pipefail + +script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +repo_root="$(cd "$script_dir/.." && pwd)" +result_dir="${LUCEBOX_FORMAL_RESULTS:-$repo_root/.formal-results}" +base_sha="" +mode="all" +legacy=false + +while (($#)); do + case "$1" in + --base-sha) + base_sha="${2:?--base-sha requires a commit}" + mode="pr" + shift 2 + ;; + --all) + mode="all" + shift + ;; + --nightly) + mode="nightly" + shift + ;; + --legacy) + legacy=true + shift + ;; + *) + echo "usage: $0 [--base-sha SHA|--all|--nightly] [--legacy]" >&2 + exit 2 + ;; + esac +done + +cd "$repo_root" +if [[ -n "$(git status --short --untracked-files=no)" ]]; then + echo "formal planning requires a committed production checkout" >&2 + exit 2 +fi + +registry_image="$( + python3 -c ' +import pathlib +import tomllib +registry = pathlib.Path("formal/contracts/registry.toml") +print(tomllib.loads(registry.read_text())["toolchain"]["verifier_image"]) +' < /dev/null +)" +verifier_image="${LUCEBOX_FORMAL_IMAGE:-$registry_image}" + +mkdir -p "$result_dir" +result_dir="$(cd "$result_dir" && pwd)" + +container_common=( + --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)" + # The plan verifier compiles the immutable base-native regression here and + # executes it against the read-only head workspace. + --tmpfs /tmp:rw,exec,nosuid,nodev,size=512m + --volume "$repo_root:/workspace:ro" + --workdir /workspace +) + +if [[ "$legacy" == true ]]; then + docker run \ + "${container_common[@]}" \ + --volume "$result_dir:/results:rw" \ + "$verifier_image" verify \ + --manifest /workspace/formal/manifest.toml \ + --base-sha "$base_sha" \ + --mode "$mode" \ + --out /results + exit +fi + +head_sha="$(git rev-parse HEAD)" +if [[ -n "$base_sha" ]]; then + policy_sha="$(git rev-parse "${base_sha}^{commit}")" +else + policy_sha="$head_sha" +fi +plan_dir="$(mktemp -d)" +trap 'rm -rf -- "$plan_dir"' EXIT + +docker run \ + "${container_common[@]}" \ + --volume "$plan_dir:/plan:rw" \ + "$verifier_image" plan \ + --workspace /workspace \ + --base-policy formal/contracts/registry.toml \ + --base-sha "$policy_sha" \ + --head-sha "$head_sha" \ + --mode "$mode" \ + --out /plan + +docker run \ + "${container_common[@]}" \ + --volume "$plan_dir:/plan:ro" \ + --volume "$result_dir:/results:rw" \ + "$verifier_image" verify \ + --plan /plan/plan.json \ + --workspace /workspace \ + --generated-root /plan \ + --out /results diff --git a/scripts/formal_mutation_test.sh b/scripts/formal_mutation_test.sh new file mode 100755 index 000000000..ea0bd1ed6 --- /dev/null +++ b/scripts/formal_mutation_test.sh @@ -0,0 +1,99 @@ +#!/usr/bin/env bash +set -euo pipefail + +script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +repo_root="$(cd "$script_dir/.." && pwd)" + +# id|patch|mutated production path|expected target|base-native source|control target +mutation_cases=( + "prefix-cache-abort-hole|prefix-cache-bypass-selector.patch|server/src/server/prefix_cache_state.h|prefix-cache-abort-hole|server/test/test_prefix_cache_state.cpp|prefix-cache-inline" + "prefix-cache-full-lifecycle|prefix-cache-full-bypass-free-slot.patch|server/src/server/prefix_cache_state.h|prefix-cache-full-lifecycle|server/test/test_full_prefix_cache_state.cpp|prefix-cache-inline" + "spec-commit-exactness|spec-commit-invert-prefix-match.patch|server/src/common/spec_commit.h|spec-commit-exactness|server/test/test_spec_commit.cpp|" + "kvflash-residency-map|kvflash-capacity-off-by-one.patch|server/src/common/kvflash_residency_map.h|kvflash-residency-map|server/test/test_kvflash_residency_map.cpp|" +) + +cd "$repo_root" +if [[ -n "$(git status --short --untracked-files=no)" ]]; then + echo "mutation sensitivity requires a checkout with no tracked changes" >&2 + exit 2 +fi + +base_sha="$(git rev-parse HEAD)" +temporary_root="$(mktemp -d)" +trap 'rm -rf -- "$temporary_root"' EXIT + +for mutation_case in "${mutation_cases[@]}"; do + IFS='|' read -r case_id patch_name mutable_path target_id native_source control_id \ + <<< "$mutation_case" + mutated_repo="$temporary_root/$case_id/repo" + results="$temporary_root/$case_id/results" + mutation="$repo_root/formal/contracts/mutations/$patch_name" + mkdir -p "$(dirname "$mutated_repo")" + + git clone --quiet --no-local "$repo_root" "$mutated_repo" + git -C "$mutated_repo" checkout --quiet --detach "$base_sha" + if ! git -C "$mutated_repo" apply --check "$mutation"; then + echo "$case_id: mutation patch no longer applies to exact HEAD" >&2 + exit 1 + fi + git -C "$mutated_repo" apply "$mutation" + git -C "$mutated_repo" config user.email "formal-mutation@example.invalid" + git -C "$mutated_repo" config user.name "Formal Mutation Test" + git -C "$mutated_repo" add "$mutable_path" + git -C "$mutated_repo" commit --quiet \ + -m "test: inject $case_id mutation" + + # First prove that the immutable native regression is behavior-sensitive, + # independently of whether ESBMC finds the same mutation first. + native_binary="$temporary_root/$case_id/native-test" + c++ -std=c++17 -O0 -Wall -Wextra -Werror \ + -I "$mutated_repo/server/src" \ + "$mutated_repo/$native_source" \ + -o "$native_binary" + set +e + "$native_binary" + native_status=$? + set -e + if [[ "$native_status" -eq 0 ]]; then + echo "$case_id: native regression survived mutation" >&2 + exit 1 + fi + + set +e + LUCEBOX_FORMAL_RESULTS="$results" \ + "$mutated_repo/scripts/formal.sh" --base-sha "$base_sha" + verification_status=$? + set -e + + if [[ "$verification_status" -ne 10 ]]; then + if [[ -f "$results/summary.md" ]]; then + cat "$results/summary.md" >&2 + fi + echo "$case_id: expected counterexample exit 10, got $verification_status" >&2 + exit 1 + fi + + python3 - "$results/report.json" "$target_id" "$control_id" <<'PY' +import json +import sys + +report = json.load(open(sys.argv[1], encoding="utf-8")) +target_id = sys.argv[2] +control_id = sys.argv[3] +results = {item["id"]: item for item in report["results"]} +if report.get("conclusion") != "counterexample": + raise SystemExit("mutation did not produce a counterexample conclusion") +if results[target_id]["status"] != "counterexample": + raise SystemExit(f"{target_id} did not reject its mutation") +if control_id and results[control_id]["status"] != "verified": + raise SystemExit(f"unrelated control {control_id} did not remain verified") +native = results[target_id].get("assumptions", {}).get("native_test") +if native is not None and native.get("status") != "counterexample": + raise SystemExit(f"{target_id} native result was not a counterexample") +PY + + cat "$results/summary.md" + echo "$case_id mutation sensitivity: PASS" +done + +echo "all formal mutation cases: PASS" diff --git a/scripts/formal_plan.py b/scripts/formal_plan.py new file mode 100644 index 000000000..e6ff8beda --- /dev/null +++ b/scripts/formal_plan.py @@ -0,0 +1,381 @@ +#!/usr/bin/env python3 +"""Plan approved minimal-core formal contracts for a Lucebox change. + +This intentionally small, dependency-free tool is a Luce-side fixture +validator for the per-PR formal planner. It does not invent contracts: it +selects only targets declared in a supplied registry, renders their approved +templates deterministically, and reports edits to critical paths that have no +approved target as advisory gaps. + +CI integration and its base-revision blob loading are owned by the companion +planner. This script is intentionally not the authoritative CI implementation. +""" + +from __future__ import annotations + +import argparse +import fnmatch +import hashlib +import json +import subprocess +import sys +import tomllib +from pathlib import Path, PurePosixPath +from typing import Any + +SCHEMA_VERSION = 1 +POLICIES = {"required", "advisory"} +TARGET_REQUIRED_FIELDS = { + "id", + "policy", + "description", + "source_paths", + "trigger_paths", + "symbol", + "signature", + "template", + "entry_function", + "include_dirs", + "timeout_seconds", + "pr_defines", + "nightly_defines", + "pr_esbmc_args", + "nightly_esbmc_args", + "mutable_paths", + "contract_paths", +} + + +class RegistryError(ValueError): + """A registry is not safe or complete enough for deterministic planning.""" + + +def _repo_path(value: object, field: str) -> str: + if not isinstance(value, str) or not value: + raise RegistryError(f"{field} must be a non-empty repository path") + path = PurePosixPath(value) + if path.is_absolute() or ".." in path.parts or str(path) == ".": + raise RegistryError(f"{field} must remain inside the repository: {value}") + return value + + +def _string_list(value: object, field: str) -> list[str]: + if not isinstance(value, list) or not all(isinstance(item, str) for item in value): + raise RegistryError(f"{field} must be a list of strings") + return list(value) + + +def _repo_paths(value: object, field: str) -> list[str]: + return [_repo_path(item, field) for item in _string_list(value, field)] + + +def _template_sha256(root: Path, template: str) -> str: + source = root / template + if not source.is_file(): + raise RegistryError(f"template does not exist: {template}") + return hashlib.sha256(source.read_bytes()).hexdigest() + + +def load_registry(registry_path: Path, root: Path) -> dict[str, Any]: + data = tomllib.loads(registry_path.read_text(encoding="utf-8")) + if data.get("schema_version") != SCHEMA_VERSION: + raise RegistryError("unsupported registry schema_version") + if not isinstance(data.get("registry"), dict): + raise RegistryError("registry table is required") + compatibility_manifest = data["registry"].get("compatibility_manifest") + if compatibility_manifest is not None: + data["registry"]["compatibility_manifest"] = _repo_path( + compatibility_manifest, + "registry.compatibility_manifest", + ) + + critical_paths = data.get("critical_paths") + if not isinstance(critical_paths, list) or not critical_paths: + raise RegistryError("at least one critical_paths table is required") + critical_ids: set[str] = set() + for area in critical_paths: + if not isinstance(area, dict): + raise RegistryError("critical_paths entries must be tables") + area_id = area.get("id") + if not isinstance(area_id, str) or not area_id: + raise RegistryError("critical_paths.id must be a string") + if area_id in critical_ids: + raise RegistryError(f"duplicate critical path area: {area_id}") + critical_ids.add(area_id) + if not isinstance(area.get("description"), str): + raise RegistryError(f"{area_id}: critical-path description is required") + area["paths"] = _repo_paths(area.get("paths"), f"{area_id}.paths") + area["watch_paths"] = _repo_paths( + area.get("watch_paths", []), + f"{area_id}.watch_paths", + ) + area["include_roots"] = _repo_paths( + area.get("include_roots", []), + f"{area_id}.include_roots", + ) + area_policy = area.get("policy", "advisory") + if area_policy not in POLICIES: + raise RegistryError( + f"{area_id}: unsupported critical-path policy {area_policy!r}" + ) + area["policy"] = area_policy + if not isinstance(data.get("toolchain"), dict): + raise RegistryError("toolchain table is required") + if not isinstance(data["toolchain"].get("esbmc_version"), str): + raise RegistryError("toolchain.esbmc_version must be a string") + + targets = data.get("targets") + if not isinstance(targets, list) or not targets: + raise RegistryError("at least one targets table is required") + target_ids: set[str] = set() + for target in targets: + if not isinstance(target, dict): + raise RegistryError("targets entries must be tables") + missing = TARGET_REQUIRED_FIELDS - target.keys() + if missing: + raise RegistryError( + f"target missing required fields: {', '.join(sorted(missing))}" + ) + target_id = target["id"] + if not isinstance(target_id, str) or not target_id: + raise RegistryError("target.id must be a non-empty string") + if target_id in target_ids: + raise RegistryError(f"duplicate target id: {target_id}") + target_ids.add(target_id) + if target["policy"] not in POLICIES: + raise RegistryError(f"{target_id}: unsupported policy {target['policy']!r}") + for field in ("description", "symbol", "signature", "entry_function"): + if not isinstance(target[field], str) or not target[field]: + raise RegistryError(f"{target_id}: {field} must be a non-empty string") + if not isinstance(target["timeout_seconds"], int) or not 0 < target["timeout_seconds"] <= 3600: + raise RegistryError(f"{target_id}: timeout_seconds must be between 1 and 3600") + nightly_timeout = target.setdefault( + "nightly_timeout_seconds", target["timeout_seconds"] + ) + if ( + not isinstance(nightly_timeout, int) + or nightly_timeout < target["timeout_seconds"] + or nightly_timeout > 3600 + ): + raise RegistryError( + f"{target_id}: nightly_timeout_seconds must be between timeout_seconds and 3600" + ) + for field in ( + "source_paths", + "trigger_paths", + "include_dirs", + "mutable_paths", + "contract_paths", + ): + target[field] = _repo_paths(target[field], f"{target_id}.{field}") + native_test = target.get("native_test") + native_source = target.get("native_test_source") + if (native_test is None) != (native_source is None): + raise RegistryError( + f"{target_id}: native_test and native_test_source must be declared together" + ) + if native_test is not None: + if not isinstance(native_test, str) or not native_test: + raise RegistryError(f"{target_id}: native_test must be a non-empty string") + native_source = _repo_path( + native_source, + f"{target_id}.native_test_source", + ) + if native_source not in target["contract_paths"]: + raise RegistryError( + f"{target_id}: contract_paths must include native_test_source" + ) + target["native_test"] = native_test + target["native_test_source"] = native_source + for field in ( + "pr_defines", + "nightly_defines", + "pr_esbmc_args", + "nightly_esbmc_args", + ): + target[field] = _string_list(target[field], f"{target_id}.{field}") + target["template"] = _repo_path(target["template"], f"{target_id}.template") + variables = target.get("template_variables", {}) + if not isinstance(variables, dict) or not all( + isinstance(key, str) and isinstance(value, str) + for key, value in variables.items() + ): + raise RegistryError(f"{target_id}: template_variables must be a string map") + target["template_variables"] = variables + target["template_sha256"] = _template_sha256(root, target["template"]) + if target["template"] not in target["contract_paths"]: + raise RegistryError(f"{target_id}: contract_paths must include template") + + return data + + +def _matches(path: str, patterns: list[str]) -> bool: + return any(fnmatch.fnmatchcase(path, pattern) for pattern in patterns) + + +def selected_targets(registry: dict[str, Any], changed_paths: list[str]) -> list[dict[str, Any]]: + return [ + target + for target in registry["targets"] + if any(_matches(path, target["trigger_paths"]) for path in changed_paths) + ] + + +def coverage_gaps(registry: dict[str, Any], changed_paths: list[str]) -> list[dict[str, Any]]: + gaps: list[dict[str, Any]] = [] + target_patterns = [ + pattern for target in registry["targets"] for pattern in target["trigger_paths"] + ] + for area in registry["critical_paths"]: + uncovered = [ + path + for path in changed_paths + if _matches(path, area["paths"]) and not _matches(path, target_patterns) + ] + if uncovered: + gaps.append( + { + "id": area["id"], + "description": area["description"], + "policy": area["policy"], + "changed_paths": uncovered, + } + ) + return gaps + + +def make_plan(registry_path: Path, root: Path, changed_paths: list[str]) -> dict[str, Any]: + registry = load_registry(registry_path, root) + targets = selected_targets(registry, changed_paths) + gaps = coverage_gaps(registry, changed_paths) + return { + "schema_version": SCHEMA_VERSION, + "registry": registry_path.relative_to(root).as_posix(), + "changed_paths": changed_paths, + "targets": [ + { + key: target[key] + for key in ( + "id", + "policy", + "description", + "source_paths", + "symbol", + "signature", + "template", + "template_sha256", + "template_variables", + "entry_function", + "include_dirs", + "timeout_seconds", + "nightly_timeout_seconds", + "pr_defines", + "nightly_defines", + "pr_esbmc_args", + "nightly_esbmc_args", + "mutable_paths", + "contract_paths", + "native_test", + "native_test_source", + ) + } + for target in targets + ], + "coverage_gaps": gaps, + } + + +def _changed_paths_from_git(root: Path, base_sha: str) -> list[str]: + process = subprocess.run( + ["git", "diff", "--name-only", f"{base_sha}...HEAD"], + cwd=root, + check=False, + text=True, + capture_output=True, + ) + if process.returncode: + raise RegistryError( + f"could not compute changed paths from {base_sha}: {process.stderr.strip()}" + ) + return [line for line in process.stdout.splitlines() if line] + + +def _render_template(target: dict[str, Any], source: str) -> str: + variables = { + "ID": target["id"], + "SYMBOL": target["symbol"], + "SIGNATURE": target["signature"], + **target["template_variables"], + } + for name, value in variables.items(): + source = source.replace("{{" + name + "}}", value) + if "{{" in source or "}}" in source: + raise RegistryError(f"{target['id']}: unresolved template token") + return source + + +def _emit_templates(plan: dict[str, Any], root: Path, output: Path) -> None: + output.mkdir(parents=True, exist_ok=True) + generated: list[dict[str, str]] = [] + for target in plan["targets"]: + template = root / target["template"] + destination = output / f"{target['id']}.cpp" + destination.write_text( + _render_template(target, template.read_text(encoding="utf-8")), + encoding="utf-8", + ) + generated.append( + { + "id": target["id"], + "path": destination.name, + "sha256": hashlib.sha256(destination.read_bytes()).hexdigest(), + } + ) + plan["generated_harnesses"] = generated + + +def _parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=Path.cwd()) + parser.add_argument( + "--registry", type=Path, default=Path("formal/contracts/registry.toml") + ) + subparsers = parser.add_subparsers(dest="command", required=True) + subparsers.add_parser("validate") + for command in ("plan", "emit"): + subparser = subparsers.add_parser(command) + changed = subparser.add_mutually_exclusive_group(required=True) + changed.add_argument("--changed-path", action="append", default=[]) + changed.add_argument("--base-sha") + subparser.add_argument("--out", type=Path, required=command == "emit") + return parser + + +def main() -> int: + args = _parser().parse_args() + root = args.root.resolve() + registry = args.registry if args.registry.is_absolute() else root / args.registry + registry = registry.resolve() + try: + if args.command == "validate": + load_registry(registry, root) + print(f"valid registry: {registry.relative_to(root)}") + return 0 + changed_paths = ( + _changed_paths_from_git(root, args.base_sha) + if args.base_sha + else args.changed_path + ) + plan = make_plan(registry, root, changed_paths) + if args.command == "emit": + output = args.out if args.out.is_absolute() else root / args.out + _emit_templates(plan, root, output.resolve()) + print(json.dumps(plan, indent=2, sort_keys=True)) + return 0 + except (OSError, RegistryError, tomllib.TOMLDecodeError) as exc: + print(f"formal-plan error: {exc}", file=sys.stderr) + return 2 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/server/CMakeLists.txt b/server/CMakeLists.txt index ddef3cf44..98c59fece 100644 --- a/server/CMakeLists.txt +++ b/server/CMakeLists.txt @@ -1148,6 +1148,49 @@ if(DFLASH27B_TESTS) list(APPEND _raw_unit_test_targets test_server_unit) endif() + # Dependency-free production state core used by native tests and ESBMC. + # Keep this target free of tokenizer, ggml, and GPU libraries so formal + # transition checks remain fast and reproducible on hosted CPU runners. + if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/test/test_prefix_cache_state.cpp") + add_executable( + test_prefix_cache_state + test/test_prefix_cache_state.cpp) + target_include_directories(test_prefix_cache_state PRIVATE + ${CMAKE_CURRENT_SOURCE_DIR}/src) + add_test(NAME prefix_cache_state COMMAND test_prefix_cache_state) + endif() + + if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/test/test_full_prefix_cache_state.cpp") + add_executable( + test_full_prefix_cache_state + test/test_full_prefix_cache_state.cpp) + target_include_directories(test_full_prefix_cache_state PRIVATE + ${CMAKE_CURRENT_SOURCE_DIR}/src) + add_test( + NAME full_prefix_cache_state + COMMAND test_full_prefix_cache_state) + endif() + + if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/test/test_spec_commit.cpp") + add_executable( + test_spec_commit + test/test_spec_commit.cpp) + target_include_directories(test_spec_commit PRIVATE + ${CMAKE_CURRENT_SOURCE_DIR}/src) + add_test(NAME spec_commit COMMAND test_spec_commit) + endif() + + if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/test/test_kvflash_residency_map.cpp") + add_executable( + test_kvflash_residency_map + test/test_kvflash_residency_map.cpp) + target_include_directories(test_kvflash_residency_map PRIVATE + ${CMAKE_CURRENT_SOURCE_DIR}/src) + add_test( + NAME kvflash_residency_map + COMMAND test_kvflash_residency_map) + endif() + # Feature/architecture gate tests. check_feature_compatibility(), # collect_feature_warnings() and the capability table are pure functions, # so this target deliberately compiles only feature_gate.cpp and @@ -1221,6 +1264,18 @@ if(DFLASH27B_TESTS) if(TARGET test_feature_gate) list(APPEND _check_deps test_feature_gate) endif() + if(TARGET test_prefix_cache_state) + list(APPEND _check_deps test_prefix_cache_state) + endif() + if(TARGET test_full_prefix_cache_state) + list(APPEND _check_deps test_full_prefix_cache_state) + endif() + if(TARGET test_spec_commit) + list(APPEND _check_deps test_spec_commit) + endif() + if(TARGET test_kvflash_residency_map) + list(APPEND _check_deps test_kvflash_residency_map) + endif() if(_check_deps) add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND} --output-on-failure diff --git a/server/src/common/dflash_spec_decode.cpp b/server/src/common/dflash_spec_decode.cpp index 60e28c733..355d12d91 100644 --- a/server/src/common/dflash_spec_decode.cpp +++ b/server/src/common/dflash_spec_decode.cpp @@ -1,6 +1,7 @@ // dflash_spec_decode.cpp — Generic DFlash speculative-decode loop. #include "dflash_spec_decode.h" +#include "spec_commit.h" #include "internal.h" // DraftWeights #include "io_utils.h" @@ -198,22 +199,20 @@ bool run_dflash_spec_decode( } // Acceptance: longest matching prefix between draft and target argmax. - int accept_n = 1; - for (int i = 0; i < q_len - 1; i++) { - if (draft_tok[i + 1] == target_tok[i]) accept_n++; - else break; + const auto commit_decision = dflash::common::SpecCommitDecision::greedy( + draft_tok, target_tok, q_len, need_commit_budget); + if (!commit_decision.valid()) { + std::fprintf(stderr, "dflash-spec invalid commit decision\n"); + target.restore_kv(); + return false; } + const int accept_n = commit_decision.accepted_count(); // Track hint acceptance telemetry. if (hint_filled > 0) { n_hint_proposed += hint_filled; n_hint_accepted += std::min(hint_filled, accept_n - 1); } - int bonus_tok = (accept_n < q_len) ? target_tok[accept_n - 1] : -1; - int commit_n = accept_n + (bonus_tok >= 0 ? 1 : 0); - if (commit_n > need_commit_budget) { - commit_n = need_commit_budget; - if (commit_n <= accept_n) bonus_tok = -1; - } + int commit_n = commit_decision.commit_count(); // ── Commit accepted tokens to KV state ────────────────────────── // Adaptive: use fast-rollback when acceptance is high enough to benefit. @@ -222,9 +221,11 @@ bool run_dflash_spec_decode( target.supports_fast_rollback() && (accept_n >= rollback_policy.fast_rollback_threshold); - std::vector replay_tok((size_t)commit_n); - for (int i = 0; i < commit_n; i++) { - replay_tok[i] = (i < accept_n) ? draft_tok[i] : bonus_tok; + std::vector replay_tok; + if (!commit_decision.materialize(draft_tok, replay_tok)) { + std::fprintf(stderr, "dflash-spec commit materialization failed\n"); + target.restore_kv(); + return false; } bool fast_rolled_back = false; @@ -235,7 +236,6 @@ bool run_dflash_spec_decode( // budget (need_commit_budget). Committing accept_n would both // overrun the budget and grow replay_tok with zero-initialised // tokens (it was sized to the clamped commit_n above). - bonus_tok = -1; commit_n = std::min(accept_n, need_commit_budget); replay_tok.resize(commit_n); if (target.rollback_to(committed, commit_n)) { @@ -254,8 +254,8 @@ bool run_dflash_spec_decode( if (!fast_rolled_back) { rollback_diag.record_legacy_replay(); // Legacy path: restore SSM snapshot and replay accepted + bonus tokens. - // (When falling back from fast-rollback, bonus_tok is already -1 and - // replay_tok/commit_n reflect the budget-clamped accepted set.) + // When falling back from fast rollback, replay_tok/commit_n already + // reflect the budget-clamped accepted set, with the bonus deferred. if (!target.restore_kv()) { std::fprintf(stderr, "dflash-spec restore_kv failed\n"); return false; diff --git a/server/src/common/kvflash_pager.h b/server/src/common/kvflash_pager.h index d61707d96..77579c41c 100644 --- a/server/src/common/kvflash_pager.h +++ b/server/src/common/kvflash_pager.h @@ -46,6 +46,8 @@ #pragma once +#include "kvflash_residency_map.h" + #include "ggml.h" #include "ggml-backend.h" @@ -56,6 +58,7 @@ #include #include #include +#include #include #include @@ -69,13 +72,6 @@ namespace dflash::common { -struct KvFlashConfig { - int chunk_tokens = 64; // logical tokens per page - int pool_tokens = 0; // resident pool capacity (multiple of chunk_tokens) - int sink_chunks = 1; // leading chunks never evicted (attention sinks) - int tail_window_chunks = 4; // trailing chunks never evicted (local window) -}; - struct KvFlashStats { int64_t page_outs = 0; int64_t page_ins = 0; @@ -93,7 +89,7 @@ class KvFlashPager { // victim + the partially filled append head) or eviction deadlocks and // slot_for() starts failing once the pool fills. static int min_pool_tokens(const KvFlashConfig & cfg) { - return (cfg.sink_chunks + cfg.tail_window_chunks + 2) * cfg.chunk_tokens; + return KvFlashResidencyMap::min_pool_tokens(cfg); } ~KvFlashPager() { cleanup_(); } @@ -101,26 +97,45 @@ class KvFlashPager { bool attach(const KvFlashConfig & cfg, const std::vector & attn_k, const std::vector & attn_v) { - if (cfg.pool_tokens <= 0 || cfg.pool_tokens % cfg.chunk_tokens != 0) return false; - if (cfg.pool_tokens < min_pool_tokens(cfg)) { + const int minimum = min_pool_tokens(cfg); + if (!KvFlashResidencyMap::valid_config(cfg)) { std::fprintf(stderr, - "kvflash: pool %d < minimum %d (%d sink + %d tail chunks must " - "leave an evictable block)\n", - cfg.pool_tokens, min_pool_tokens(cfg), - cfg.sink_chunks, cfg.tail_window_chunks); + "kvflash: invalid config (pool=%d chunk=%d sink=%d tail=%d, " + "minimum=%d)\n", + cfg.pool_tokens, cfg.chunk_tokens, cfg.sink_chunks, + cfg.tail_window_chunks, minimum); return false; } if (attn_k.size() != attn_v.size()) return false; + if (!attn_k.empty()) { + const ggml_tensor * K0 = attn_k[0]; + const ggml_tensor * V0 = attn_v[0]; + if (!K0 || !V0 || K0->ne[1] < cfg.pool_tokens || + V0->ne[1] < cfg.pool_tokens || K0->ne[2] <= 0 || + V0->ne[2] != K0->ne[2]) { + return false; + } + for (size_t i = 0; i < attn_k.size(); ++i) { + const ggml_tensor * K = attn_k[i]; + const ggml_tensor * V = attn_v[i]; + if (!K || !V || K->ne[1] < cfg.pool_tokens || + V->ne[1] < cfg.pool_tokens || K->ne[2] != K0->ne[2] || + V->ne[2] != K0->ne[2] || K->nb[1] != K0->nb[1] || + V->nb[1] != V0->nb[1]) { + return false; + } + } + } + cleanup_(); // release pinned buffers + stream from any prior attach cfg_ = cfg; attn_k_ = attn_k; attn_v_ = attn_v; - n_blocks_ = cfg.pool_tokens / cfg.chunk_tokens; + if (!residency_.configure(cfg)) return false; // validated above if (!attn_k.empty()) { const ggml_tensor * K0 = attn_k[0]; - if ((int)K0->ne[1] < cfg.pool_tokens) return false; n_head_kv_ = (int)K0->ne[2]; // Per-(tensor, head) contiguous segment of chunk_tokens rows. @@ -136,11 +151,8 @@ class KvFlashPager { zero_buf_.clear(); } - free_blocks_.clear(); - for (int b = n_blocks_ - 1; b >= 0; b--) free_blocks_.push_back(b); - chunks_.clear(); + backing_.clear(); stats_ = {}; - clock_ = 0; has_pending_page_in_ = false; #ifdef KVFLASH_HAS_ASYNC_DMA @@ -156,7 +168,9 @@ class KvFlashPager { // Optional: custom block hand-out order (e.g. shuffled placement in // relocation tests). `order[i]` = i-th block to hand out. void set_block_order(const std::vector & order) { - free_blocks_.assign(order.rbegin(), order.rend()); + if (!residency_.set_block_order(order)) { + std::fprintf(stderr, "[kvflash] invalid block order ignored\n"); + } } // Drop all mappings and host backing (new request / cache reset). @@ -166,23 +180,20 @@ class KvFlashPager { if (page_stream_) { cudaStreamSynchronize(page_stream_); } - for (auto & st : chunks_) { - if (st.host_data) { - cudaError_t err = cudaFreeHost(st.host_data); + for (auto & backing : backing_) { + if (backing.host_data) { + cudaError_t err = cudaFreeHost(backing.host_data); if (err != cudaSuccess) { std::fprintf(stderr, "[kvflash] cudaFreeHost failed: %s\n", cudaGetErrorString(err)); } - st.host_data = nullptr; + backing.host_data = nullptr; } } #endif - chunks_.clear(); - free_blocks_.clear(); - for (int b = n_blocks_ - 1; b >= 0; b--) free_blocks_.push_back(b); + backing_.clear(); + residency_.reset(); stats_.host_bytes = 0; - cur_chunk_ = 0; - epoch_++; has_pending_page_in_ = false; } @@ -192,7 +203,7 @@ class KvFlashPager { // need stale rows to dequantise to ~zero contribution. Masked consumers // don't need this but it is cheap (pool-sized memset, sub-ms). void zero_free_blocks() { - for (int b : free_blocks_) zero_block(b); + for (int b : residency_.free_blocks()) zero_block(b); #ifdef KVFLASH_HAS_ASYNC_DMA if (page_stream_) { cudaStreamSynchronize(page_stream_); @@ -200,9 +211,9 @@ class KvFlashPager { #endif } - bool attached() const { return n_blocks_ > 0; } - int pool_tokens() const { return cfg_.pool_tokens; } - int chunk_tokens() const { return cfg_.chunk_tokens; } + bool attached() const { return residency_.attached(); } + int pool_tokens() const { return residency_.pool_tokens(); } + int chunk_tokens() const { return residency_.chunk_tokens(); } // Optional external relevance score; higher = keep. Falls back to LRU. std::function score_hook; @@ -216,11 +227,19 @@ class KvFlashPager { // issued, page_stream_ is synchronised here so that recalled KV data is // resident before the next attention forward. bool alloc_span(int kv_start, int n_tok) { + if (kv_start < 0 || n_tok < 0 || + (int64_t)kv_start + n_tok > std::numeric_limits::max()) { + std::fprintf(stderr, + "[kvflash] invalid allocation span start=%d count=%d\n", + kv_start, n_tok); + return false; + } for (int i = 0; i < n_tok; ++i) { - if (slot_for(kv_start + i) < 0) { + const int64_t pos = (int64_t)kv_start + i; + if (slot_for(pos) < 0) { std::fprintf(stderr, "[kvflash] no pool slot at pos %d " "(pool %d exhausted)\n", - kv_start + i, cfg_.pool_tokens); + (int)pos, cfg_.pool_tokens); return false; } } @@ -232,68 +251,37 @@ class KvFlashPager { // the pool is full, evicts) at chunk granularity. Call once per // appended token, in logical order. int slot_for(int64_t pos) { - const int c = (int)(pos / cfg_.chunk_tokens); - // cur_chunk_ tracks the append head only; a page_in of an older - // chunk must not shrink the protected tail window. It must advance - // BEFORE eviction (so the victim search protects the new tail), but - // a failed allocation must roll it back or the next eviction's tail - // window is computed from a chunk that never materialized. - const int prev_cur_chunk = cur_chunk_; - if (c > cur_chunk_) cur_chunk_ = c; - if ((int)chunks_.size() <= c) chunks_.resize(c + 1); - ChunkState & st = chunks_[c]; - if (st.block < 0) { - if (!ensure_free_block()) { - cur_chunk_ = prev_cur_chunk; - return -1; - } - st.block = free_blocks_.back(); - free_blocks_.pop_back(); - epoch_++; - if (st.on_host) { // recall: restore paged-out bytes - copy_chunk(c, st.block, /*to_host=*/false); - stats_.page_ins++; - stats_.moved_bytes += chunk_bytes_; + const KvFlashResidencyMap::Score score = score_hook + ? KvFlashResidencyMap::Score{&score_hook, &evaluate_score_} + : KvFlashResidencyMap::Score{}; + const KvFlashResidencyMap::PreparePageOut page_out{ + this, &prepare_page_out_thunk_}; + const KvFlashResidencyMap::AcquireResult acquired = + residency_.acquire(pos, score, page_out); + if (!acquired) return -1; + if (acquired.recalled) { + copy_chunk(acquired.chunk, acquired.block, /*to_host=*/false); + stats_.page_ins++; + stats_.moved_bytes += chunk_bytes_; #ifdef KVFLASH_HAS_ASYNC_DMA - has_pending_page_in_ = true; + has_pending_page_in_ = true; #endif - } } - st.last_use = ++clock_; - return st.block * cfg_.chunk_tokens + (int)(pos % cfg_.chunk_tokens); + return acquired.slot; } // Force a chunk out of the pool (host backing + zeroed slots). bool page_out(int c) { - if (c >= (int)chunks_.size() || chunks_[c].block < 0) return false; - ChunkState & st = chunks_[c]; - if (has_tensor_storage() && !st.on_host) { -#ifdef KVFLASH_HAS_ASYNC_DMA - cudaError_t err = cudaMallocHost(&st.host_data, chunk_bytes_); - if (err != cudaSuccess) { - std::fprintf(stderr, "[kvflash] cudaMallocHost failed: %s\n", - cudaGetErrorString(err)); - return false; - } -#else - st.host_data.resize(chunk_bytes_); -#endif - stats_.host_bytes += (int64_t)chunk_bytes_; - } - copy_chunk(c, st.block, /*to_host=*/true); - zero_block(st.block); - st.on_host = true; - free_blocks_.push_back(st.block); - st.block = -1; - epoch_++; - stats_.page_outs++; - stats_.moved_bytes += chunk_bytes_; - return true; + const KvFlashResidencyMap::PreparePageOut page_out{ + this, &prepare_page_out_thunk_}; + return residency_.page_out(c, page_out); } // Recall a chunk into the pool (used by reselect / tests). bool page_in(int c) { - if (c >= (int)chunks_.size() || !chunks_[c].on_host || chunks_[c].block >= 0) return false; + if (c < 0 || !residency_.is_host_backed(c) || residency_.is_resident(c)) { + return false; + } return slot_for((int64_t)c * cfg_.chunk_tokens) >= 0; } @@ -309,7 +297,7 @@ class KvFlashPager { } bool is_resident(int c) const { - return c < (int)chunks_.size() && chunks_[c].block >= 0; + return residency_.is_resident(c); } // True while every materialized chunk still sits in its identity block @@ -317,11 +305,7 @@ class KvFlashPager { // identity-copy snapshots rely on; it holds from reset() until the // first eviction of the CURRENT request (cumulative stats do not). bool is_identity() const { - for (int c = 0; c < (int)chunks_.size(); c++) { - if (chunks_[c].block >= 0 && chunks_[c].block != c) return false; - if (chunks_[c].block < 0 && chunks_[c].on_host) return false; - } - return true; + return residency_.is_identity(); } // True iff every chunk intersecting [0, n_tok) is resident in its identity @@ -330,24 +314,17 @@ class KvFlashPager { // the non-paged tree-verify graph relies on. Stronger than is_identity(), // which is also true for an empty / not-yet-materialized pager. bool identity_prefix_covers(int n_tok) const { - if (n_tok <= 0) return true; - const int nc = (n_tok + cfg_.chunk_tokens - 1) / cfg_.chunk_tokens; - if (nc > (int)chunks_.size()) return false; - for (int c = 0; c < nc; c++) - if (chunks_[c].block != c) return false; - return true; + return residency_.identity_prefix_covers(n_tok); } int block_of(int c) const { - return c < (int)chunks_.size() ? chunks_[c].block : -1; + return residency_.block_of(c); } // Const lookup (no alloc / LRU touch): physical slot currently holding // logical `pos`, or -1 if its chunk is not resident. Callers that may // need an allocation must use slot_for() beforehand. int slot_of(int64_t pos) const { - const int c = (int)(pos / cfg_.chunk_tokens); - if (c >= (int)chunks_.size() || chunks_[c].block < 0) return -1; - return chunks_[c].block * cfg_.chunk_tokens + (int)(pos % cfg_.chunk_tokens); + return residency_.slot_of(pos); } // Logical position held by each pool slot, -1 for free blocks. `dst` @@ -355,34 +332,22 @@ class KvFlashPager { // POSITION semantics in slot space (causal / sliding-window): the // mask condition is evaluated on dst[slot] instead of the column index. void fill_slot_pos(int32_t * dst) const { - for (int i = 0; i < cfg_.pool_tokens; i++) dst[i] = -1; - for (int c = 0; c < (int)chunks_.size(); c++) { - if (chunks_[c].block < 0) continue; - int32_t * p = dst + (size_t)chunks_[c].block * cfg_.chunk_tokens; - for (int i = 0; i < cfg_.chunk_tokens; i++) - p[i] = (int32_t)c * cfg_.chunk_tokens + i; - } + residency_.fill_slot_pos(dst); } const KvFlashStats & stats() const { return stats_; } - int resident_blocks() const { return n_blocks_ - (int)free_blocks_.size(); } - int n_chunks() const { return (int)chunks_.size(); } + int resident_blocks() const { return residency_.resident_blocks(); } + int n_chunks() const { return residency_.n_chunks(); } // Bumped on every residency change (alloc / page_out / page_in). // Callers cache the slot mask and refill only when the epoch moves. - uint64_t epoch() const { return epoch_; } + uint64_t epoch() const { return residency_.epoch(); } // F16 slot-validity mask for one query row: 0 for slots belonging to a // resident chunk, -inf for free / paged-out blocks. `dst` must hold // pool_tokens entries. Used as the FA mask so non-resident slots are // excluded exactly instead of via the zero-row ~exp(-max) approximation. void fill_slot_mask(uint16_t * dst) const { - constexpr uint16_t F16_ZERO = 0x0000, F16_NEG_INF = 0xFC00; - for (int i = 0; i < cfg_.pool_tokens; i++) dst[i] = F16_NEG_INF; - for (int c = 0; c < (int)chunks_.size(); c++) { - if (chunks_[c].block < 0) continue; - uint16_t * p = dst + (size_t)chunks_[c].block * cfg_.chunk_tokens; - for (int i = 0; i < cfg_.chunk_tokens; i++) p[i] = F16_ZERO; - } + residency_.fill_slot_mask(dst); } // Lookahead reselect (FlashMemory τ-step): rebuild the resident set as @@ -391,26 +356,19 @@ class KvFlashPager { // the number of page events. Call between decode steps. int reselect() { if (!score_hook) return 0; - struct Cand { int c; float s; }; - std::vector cands; - for (int c = 0; c < (int)chunks_.size(); c++) { - const ChunkState & st = chunks_[c]; - if (st.block < 0 && !st.on_host) continue; // never materialized - const bool prot = c < cfg_.sink_chunks || - c > cur_chunk_ - 1 - cfg_.tail_window_chunks; - cands.push_back({c, prot ? 3.4e38f : score_hook(c)}); - } - std::sort(cands.begin(), cands.end(), - [](const Cand & a, const Cand & b) { return a.s > b.s; }); - std::vector want(chunks_.size(), 0); - for (int i = 0; i < (int)cands.size() && i < n_blocks_; i++) want[cands[i].c] = 1; + const KvFlashResidencyMap::Score score{&score_hook, &evaluate_score_}; + const std::vector want = + residency_.desired_residency(score); int events = 0; - for (int c = 0; c < (int)chunks_.size(); c++) { // out first: frees blocks - if (!want[c] && chunks_[c].block >= 0) { page_out(c); events++; } + for (int c = 0; c < residency_.n_chunks(); c++) { // out first: frees blocks + if (!want[(size_t)c] && residency_.is_resident(c) && page_out(c)) { + events++; + } } - for (int c = 0; c < (int)chunks_.size(); c++) { - if (want[c] && chunks_[c].block < 0 && chunks_[c].on_host) { + for (int c = 0; c < residency_.n_chunks(); c++) { + if (want[(size_t)c] && !residency_.is_resident(c) && + residency_.is_host_backed(c)) { if (page_in(c)) events++; } } @@ -419,10 +377,7 @@ class KvFlashPager { } private: - struct ChunkState { - int block = -1; // pool block index, -1 = not resident - bool on_host = false; // backing store holds valid bytes - uint64_t last_use = 0; + struct ChunkBacking { #ifdef KVFLASH_HAS_ASYNC_DMA void * host_data = nullptr; // cudaMallocHost-pinned; allocated on first page_out #else @@ -430,25 +385,50 @@ class KvFlashPager { #endif }; - bool ensure_free_block() { - if (!free_blocks_.empty()) return true; - // Victim: unprotected resident chunk with the lowest score - // (score_hook) or the oldest use (LRU fallback). - int victim = -1; - float v_score = 0.f; - uint64_t v_use = 0; - for (int c = 0; c < (int)chunks_.size(); c++) { - if (chunks_[c].block < 0) continue; - if (c < cfg_.sink_chunks) continue; - if (c > cur_chunk_ - 1 - cfg_.tail_window_chunks) continue; - if (score_hook) { - const float s = score_hook(c); - if (victim < 0 || s < v_score) { victim = c; v_score = s; } - } else { - if (victim < 0 || chunks_[c].last_use < v_use) { victim = c; v_use = chunks_[c].last_use; } + static float evaluate_score_(const void * context, int chunk) { + const auto * score = + static_cast *>(context); + return (*score)(chunk); + } + + static bool prepare_page_out_thunk_( + void * context, int chunk, int block) { + return static_cast(context) + ->prepare_page_out_(chunk, block); + } + + bool prepare_page_out_(int chunk, int block) { + if (chunk < 0 || block < 0) return false; + if ((size_t)chunk >= backing_.size()) { + try { + backing_.resize((size_t)chunk + 1); + } catch (...) { + return false; } } - return victim >= 0 && page_out(victim); + ChunkBacking & backing = backing_[(size_t)chunk]; + if (has_tensor_storage() && !residency_.is_host_backed(chunk)) { +#ifdef KVFLASH_HAS_ASYNC_DMA + cudaError_t err = cudaMallocHost(&backing.host_data, chunk_bytes_); + if (err != cudaSuccess) { + std::fprintf(stderr, "[kvflash] cudaMallocHost failed: %s\n", + cudaGetErrorString(err)); + return false; + } +#else + try { + backing.host_data.resize(chunk_bytes_); + } catch (...) { + return false; + } +#endif + stats_.host_bytes += (int64_t)chunk_bytes_; + } + copy_chunk(chunk, block, /*to_host=*/true); + zero_block(block); + stats_.page_outs++; + stats_.moved_bytes += chunk_bytes_; + return true; } // Move one chunk between pool slots and host backing. @@ -459,7 +439,7 @@ class KvFlashPager { // alloc_span(), so host_data is coherent before any H2D read starts. void copy_chunk(int c, int block, bool to_host) { if (!has_tensor_storage()) return; - ChunkState & st = chunks_[c]; + ChunkBacking & backing = backing_[(size_t)c]; #ifdef KVFLASH_HAS_ASYNC_DMA size_t host_off = 0; for (size_t l = 0; l < attn_k_.size(); l++) { @@ -470,7 +450,7 @@ class KvFlashPager { const size_t dev_off = (size_t)block * cfg_.chunk_tokens * t->nb[1] + (size_t)h * t->nb[2]; - void * host_ptr = (uint8_t *)st.host_data + host_off; + void * host_ptr = (uint8_t *)backing.host_data + host_off; void * dev_ptr = (uint8_t *)t->data + dev_off; cudaError_t err; if (to_host) @@ -488,7 +468,7 @@ class KvFlashPager { } } #else - uint8_t * p = (uint8_t *)st.host_data.data(); + uint8_t * p = (uint8_t *)backing.host_data.data(); for (size_t l = 0; l < attn_k_.size(); l++) { for (int kv = 0; kv < 2; kv++) { ggml_tensor * t = kv == 0 ? attn_k_[l] : attn_v_[l]; @@ -532,8 +512,7 @@ class KvFlashPager { // Release page_stream_ and all pinned host_data buffers. // Safe to call on a never-attached or already-cleaned-up instance. - // Does NOT touch pool state (chunks_, free_blocks_) — that is the - // caller's responsibility (reset() or destructor via caller). + // Does NOT touch residency state; reset()/attach() own that transition. void cleanup_() { #ifdef KVFLASH_HAS_ASYNC_DMA cudaStreamSynchronize(page_stream_); // real stream, or default stream if create failed @@ -543,17 +522,18 @@ class KvFlashPager { } // Free pinned host buffers unconditionally: page_out() may have // allocated them even when stream creation failed (default-stream path). - for (auto & st : chunks_) { - if (st.host_data) { - cudaError_t err = cudaFreeHost(st.host_data); + for (auto & backing : backing_) { + if (backing.host_data) { + cudaError_t err = cudaFreeHost(backing.host_data); if (err != cudaSuccess) { std::fprintf(stderr, "[kvflash] cudaFreeHost failed: %s\n", cudaGetErrorString(err)); } - st.host_data = nullptr; + backing.host_data = nullptr; } } #endif + backing_.clear(); has_pending_page_in_ = false; } @@ -562,15 +542,13 @@ class KvFlashPager { } KvFlashConfig cfg_; + KvFlashResidencyMap residency_; std::vector attn_k_, attn_v_; - std::vector chunks_; - std::vector free_blocks_; + std::vector backing_; std::vector zero_buf_; // used by zero_block() in non-CUDA builds KvFlashStats stats_; size_t k_seg_bytes_ = 0, v_seg_bytes_ = 0, chunk_bytes_ = 0; - int n_blocks_ = 0, n_head_kv_ = 0, cur_chunk_ = 0; - uint64_t clock_ = 0; - uint64_t epoch_ = 0; + int n_head_kv_ = 0; #ifdef KVFLASH_HAS_ASYNC_DMA cudaStream_t page_stream_ = nullptr; diff --git a/server/src/common/kvflash_residency_map.h b/server/src/common/kvflash_residency_map.h new file mode 100644 index 000000000..c080ff855 --- /dev/null +++ b/server/src/common/kvflash_residency_map.h @@ -0,0 +1,435 @@ +// CPU-only ownership state for KVFlash's bounded logical-to-physical mapping. +// +// This class deliberately knows nothing about ggml, GPUs, DMA, or host +// backing buffers. A caller supplies a prepare_page_out callback before a +// resident mapping is released; the state transition is committed only when +// that callback succeeds. KvFlashPager owns the corresponding data movement. + +#pragma once + +#include +#include +#include +#include +#include + +namespace dflash::common { + +struct KvFlashConfig { + int chunk_tokens = 64; // logical tokens per page + int pool_tokens = 0; // physical capacity; whole pages only + int sink_chunks = 1; // leading pages protected from victim choice + int tail_window_chunks = 4; // recent pages protected from victim choice + // Bounds sparse logical-state growth independently of the resident pool. + // Backends may lower this to their configured context. The conservative + // default is far above supported production contexts while still + // rejecting pathological positions before a multi-gigabyte resize. + int max_logical_tokens = 16 * 1024 * 1024; +}; + +class KvFlashResidencyMap { +public: + // Non-owning callback views keep the formal core free of std::function's + // allocation and type-erasure machinery. Context lifetime is owned by + // the caller and need only cover the synchronous method invocation. + struct Score { + using Function = float (*)(const void *, int /* logical chunk */); + const void * context; + Function evaluate; + + constexpr Score(const void * ctx = nullptr, Function fn = nullptr) + : context(ctx), evaluate(fn) {} + + explicit operator bool() const { return evaluate != nullptr; } + float operator()(int chunk) const { return evaluate(context, chunk); } + }; + + struct PreparePageOut { + using Function = + bool (*)(void *, int /* logical chunk */, int /* physical block */); + void * context; + Function run; + + constexpr PreparePageOut(void * ctx = nullptr, Function fn = nullptr) + : context(ctx), run(fn) {} + + explicit operator bool() const { return run != nullptr; } + bool operator()(int chunk, int block) const { + return run(context, chunk, block); + } + }; + + struct AcquireResult { + int slot = -1; + int chunk = -1; + int block = -1; + int evicted_chunk = -1; + bool recalled = false; + bool changed = false; + + explicit operator bool() const { return slot >= 0; } + }; + + static bool valid_config(const KvFlashConfig & cfg) { + if (cfg.chunk_tokens <= 0 || cfg.pool_tokens <= 0 || + cfg.sink_chunks < 0 || cfg.tail_window_chunks < 0 || + cfg.max_logical_tokens < cfg.pool_tokens || + cfg.pool_tokens % cfg.chunk_tokens != 0) { + return false; + } + const int64_t min_chunks = + (int64_t)cfg.sink_chunks + cfg.tail_window_chunks + 2; + const int64_t min_tokens = min_chunks * cfg.chunk_tokens; + return min_tokens <= std::numeric_limits::max() && + cfg.pool_tokens >= min_tokens; + } + + static int min_pool_tokens(const KvFlashConfig & cfg) { + if (cfg.chunk_tokens <= 0 || cfg.sink_chunks < 0 || + cfg.tail_window_chunks < 0) { + return -1; + } + const int64_t tokens = + ((int64_t)cfg.sink_chunks + cfg.tail_window_chunks + 2) * + cfg.chunk_tokens; + return tokens <= std::numeric_limits::max() ? (int)tokens : -1; + } + + bool configure(const KvFlashConfig & cfg) { + if (!valid_config(cfg)) return false; + cfg_ = cfg; + n_blocks_ = cfg.pool_tokens / cfg.chunk_tokens; + configured_ = true; + initialize_empty_(false); + return true; + } + + bool attached() const { return configured_; } + int pool_tokens() const { return configured_ ? cfg_.pool_tokens : 0; } + int chunk_tokens() const { return configured_ ? cfg_.chunk_tokens : 0; } + int n_chunks() const { return (int)chunks_.size(); } + int resident_blocks() const { + return configured_ ? n_blocks_ - (int)free_blocks_.size() : 0; + } + uint64_t epoch() const { return epoch_; } + + // Drop request-local mappings while retaining the validated config. + void reset() { + if (!configured_) return; + initialize_empty_(true); + } + + // Optional deterministic placement order. A malformed or partial order is + // rejected without changing the current free-block stack. + bool set_block_order(const std::vector & order) { + if (!configured_ || resident_blocks() != 0 || + (int)order.size() != n_blocks_) { + return false; + } + std::vector seen((int)n_blocks_); + for (int block : order) { + if (block < 0 || block >= n_blocks_ || seen[(size_t)block]) { + return false; + } + seen[(size_t)block] = 1; + } + free_blocks_.clear(); + for (int index = n_blocks_ - 1; index >= 0; --index) { + free_blocks_.push_back(order[(size_t)index]); + } + return true; + } + + // Acquire the slot for a non-negative logical position. If eviction is + // necessary, prepare_page_out runs before ownership changes. Failure + // leaves the append head, mappings, free complement, clock, and epoch + // unchanged. + AcquireResult acquire( + int64_t pos, + Score score = Score{}, + PreparePageOut prepare_page_out = PreparePageOut{}) { + AcquireResult result; + if (!configured_ || pos < 0 || pos >= cfg_.max_logical_tokens) { + return result; + } + + const int64_t chunk64 = pos / cfg_.chunk_tokens; + if (chunk64 > std::numeric_limits::max()) return result; + const int chunk = (int)chunk64; + const int offset = (int)(pos % cfg_.chunk_tokens); + result.chunk = chunk; + + if (chunk < (int)chunks_.size() && chunks_[(size_t)chunk].block >= 0) { + ChunkState & state = chunks_[(size_t)chunk]; + state.last_use = ++clock_; + result.block = state.block; + result.slot = state.block * cfg_.chunk_tokens + offset; + return result; + } + + const int prospective_head = std::max(cur_chunk_, chunk); + int block = -1; + int victim = -1; + if (!free_blocks_.empty()) { + block = free_blocks_.back(); + } else { + victim = choose_victim_(prospective_head, score); + if (victim < 0 || !prepare_page_out) return result; + block = chunks_[(size_t)victim].block; + } + + const size_t old_size = chunks_.size(); + if ((size_t)chunk >= chunks_.size()) { + chunks_.resize((size_t)chunk + 1); + } + + // All potentially-throwing state growth is complete. A rejected + // external page-out preparation restores the exact prior map shape. + // Prepare callbacks must report failure before producing externally + // visible DMA/zero/stat side effects; KvFlashPager follows that rule. + if (victim >= 0 && !prepare_page_out(victim, block)) { + chunks_.resize(old_size); + return result; + } + + if (victim >= 0) { + chunks_[(size_t)victim].block = -1; + chunks_[(size_t)victim].on_host = true; + result.evicted_chunk = victim; + ++epoch_; + } else { + free_blocks_.pop_back(); + } + + ChunkState & state = chunks_[(size_t)chunk]; + result.recalled = state.on_host; + state.block = block; + state.last_use = ++clock_; + cur_chunk_ = prospective_head; + ++epoch_; + + result.block = block; + result.slot = block * cfg_.chunk_tokens + offset; + result.changed = true; + return result; + } + + // Explicitly release a resident chunk. This is intentionally permitted + // for protected chunks: policy protection constrains victim selection, + // while administrative reset/reselect code may explicitly page any chunk. + bool page_out(int chunk, PreparePageOut prepare_page_out) { + if (!configured_ || chunk < 0 || chunk >= (int)chunks_.size()) return false; + ChunkState & state = chunks_[(size_t)chunk]; + if (state.block < 0 || !prepare_page_out || + !prepare_page_out(chunk, state.block)) { + return false; + } + free_blocks_.push_back(state.block); + state.block = -1; + state.on_host = true; + ++epoch_; + return true; + } + + bool is_resident(int chunk) const { + return chunk >= 0 && chunk < (int)chunks_.size() && + chunks_[(size_t)chunk].block >= 0; + } + + bool is_host_backed(int chunk) const { + return chunk >= 0 && chunk < (int)chunks_.size() && + chunks_[(size_t)chunk].on_host; + } + + int block_of(int chunk) const { + return chunk >= 0 && chunk < (int)chunks_.size() + ? chunks_[(size_t)chunk].block : -1; + } + + int slot_of(int64_t pos) const { + if (!configured_ || pos < 0 || pos >= cfg_.max_logical_tokens) return -1; + const int64_t chunk64 = pos / cfg_.chunk_tokens; + if (chunk64 > std::numeric_limits::max()) return -1; + const int chunk = (int)chunk64; + if (!is_resident(chunk)) return -1; + return chunks_[(size_t)chunk].block * cfg_.chunk_tokens + + (int)(pos % cfg_.chunk_tokens); + } + + bool is_identity() const { + for (int chunk = 0; chunk < (int)chunks_.size(); ++chunk) { + const ChunkState & state = chunks_[(size_t)chunk]; + if (state.block >= 0 && state.block != chunk) return false; + if (state.block < 0 && state.on_host) return false; + } + return true; + } + + bool identity_prefix_covers(int n_tok) const { + if (!configured_ || n_tok < 0) return false; + if (n_tok == 0) return true; + if (n_tok > cfg_.max_logical_tokens) return false; + const int64_t n_chunks = + ((int64_t)n_tok + cfg_.chunk_tokens - 1) / cfg_.chunk_tokens; + if (n_chunks > (int64_t)chunks_.size()) return false; + for (int chunk = 0; chunk < n_chunks; ++chunk) { + if (chunks_[(size_t)chunk].block != chunk) return false; + } + return true; + } + + void fill_slot_pos(int32_t * dst) const { + if (!configured_ || !dst) return; + std::fill(dst, dst + cfg_.pool_tokens, (int32_t)-1); + for (int chunk = 0; chunk < (int)chunks_.size(); ++chunk) { + const int block = chunks_[(size_t)chunk].block; + if (block < 0) continue; + int32_t * out = dst + (size_t)block * cfg_.chunk_tokens; + for (int i = 0; i < cfg_.chunk_tokens; ++i) { + const int64_t pos = (int64_t)chunk * cfg_.chunk_tokens + i; + out[i] = pos <= std::numeric_limits::max() + ? (int32_t)pos : -1; + } + } + } + + void fill_slot_mask(uint16_t * dst) const { + if (!configured_ || !dst) return; + constexpr uint16_t F16_ZERO = 0x0000; + constexpr uint16_t F16_NEG_INF = 0xFC00; + std::fill(dst, dst + cfg_.pool_tokens, F16_NEG_INF); + for (const ChunkState & state : chunks_) { + if (state.block < 0) continue; + uint16_t * out = dst + (size_t)state.block * cfg_.chunk_tokens; + std::fill(out, out + cfg_.chunk_tokens, F16_ZERO); + } + } + + const std::vector & free_blocks() const { return free_blocks_; } + + // Desired resident set for score-driven reselect. Sinks and the current + // tail window sort ahead of scored candidates and therefore stay pinned. + std::vector desired_residency(Score score) const { + std::vector wanted((int)chunks_.size()); + if (!configured_ || !score) return wanted; + struct Candidate { + int chunk; + float score; + bool protected_chunk; + }; + std::vector candidates; + candidates.reserve(chunks_.size()); + for (int chunk = 0; chunk < (int)chunks_.size(); ++chunk) { + const ChunkState & state = chunks_[(size_t)chunk]; + if (state.block < 0 && !state.on_host) continue; + const bool keep = protected_(chunk, cur_chunk_); + const float value = keep ? 0.0f : normalized_score_(score(chunk)); + candidates.push_back({chunk, value, keep}); + } + std::stable_sort( + candidates.begin(), candidates.end(), + [](const Candidate & lhs, const Candidate & rhs) { + if (lhs.protected_chunk != rhs.protected_chunk) { + return lhs.protected_chunk; + } + return lhs.score > rhs.score; + }); + for (int i = 0; i < (int)candidates.size() && i < n_blocks_; ++i) { + wanted[(size_t)candidates[(size_t)i].chunk] = 1; + } + return wanted; + } + + // Runtime-checkable representation invariant, also useful to formal and + // dependency-free native harnesses. + bool invariant_holds() const { + if (!configured_) { + return n_blocks_ == 0 && chunks_.empty() && free_blocks_.empty(); + } + if (!valid_config(cfg_) || n_blocks_ != cfg_.pool_tokens / cfg_.chunk_tokens) { + return false; + } + std::vector owner((int)n_blocks_); + for (int block = 0; block < n_blocks_; ++block) { + owner[(size_t)block] = -1; + } + for (int chunk = 0; chunk < (int)chunks_.size(); ++chunk) { + const int block = chunks_[(size_t)chunk].block; + if (block < 0) continue; + if (block >= n_blocks_ || owner[(size_t)block] >= 0) return false; + owner[(size_t)block] = chunk; + } + std::vector free((int)n_blocks_); + for (int block : free_blocks_) { + if (block < 0 || block >= n_blocks_ || free[(size_t)block]) return false; + if (owner[(size_t)block] >= 0) return false; + free[(size_t)block] = 1; + } + for (int block = 0; block < n_blocks_; ++block) { + if ((owner[(size_t)block] >= 0) == (free[(size_t)block] != 0)) { + return false; + } + } + return resident_blocks() >= 0 && resident_blocks() <= n_blocks_; + } + +private: + struct ChunkState { + int block = -1; + bool on_host = false; + uint64_t last_use = 0; + }; + + static float normalized_score_(float score) { + return std::isnan(score) ? -std::numeric_limits::infinity() : score; + } + + bool protected_(int chunk, int append_head) const { + return chunk < cfg_.sink_chunks || + chunk > append_head - 1 - cfg_.tail_window_chunks; + } + + int choose_victim_(int append_head, Score score) const { + int victim = -1; + float victim_score = 0.0f; + uint64_t victim_use = 0; + for (int chunk = 0; chunk < (int)chunks_.size(); ++chunk) { + const ChunkState & state = chunks_[(size_t)chunk]; + if (state.block < 0 || protected_(chunk, append_head)) continue; + if (score) { + const float value = normalized_score_(score(chunk)); + if (victim < 0 || value < victim_score) { + victim = chunk; + victim_score = value; + } + } else if (victim < 0 || state.last_use < victim_use) { + victim = chunk; + victim_use = state.last_use; + } + } + return victim; + } + + void initialize_empty_(bool advance_epoch) { + chunks_.clear(); + free_blocks_.clear(); + free_blocks_.reserve((size_t)n_blocks_); + for (int block = n_blocks_ - 1; block >= 0; --block) { + free_blocks_.push_back(block); + } + cur_chunk_ = 0; + clock_ = 0; + if (advance_epoch) ++epoch_; + } + + KvFlashConfig cfg_; + std::vector chunks_; + std::vector free_blocks_; + int n_blocks_ = 0; + int cur_chunk_ = 0; + uint64_t clock_ = 0; + uint64_t epoch_ = 0; + bool configured_ = false; +}; + +} // namespace dflash::common diff --git a/server/src/common/spec_commit.h b/server/src/common/spec_commit.h new file mode 100644 index 000000000..a97bc8fc5 --- /dev/null +++ b/server/src/common/spec_commit.h @@ -0,0 +1,162 @@ +#pragma once + +#include +#include +#include + +namespace dflash::common { + +// Pure decision object for a single linear speculative-decode commit. +// +// Slot 0 is the already-selected seed. Slots 1..N are accepted only while +// they equal the target decision for the preceding slot. The first target +// decision that does not match is an optional bonus token. This class owns no +// model, KV, sampler, or rollback state; callers retain those responsibilities. +class SpecCommitDecision { +public: + // Greedy verification from target argmax tokens. target_tokens[i] is the + // target's decision after draft_tokens[i], and therefore approves (or + // rejects) draft_tokens[i + 1]. The last target row is deliberately not + // inspected: there is no subsequent draft token to match against it. + static SpecCommitDecision greedy( + const int32_t * draft_tokens, + int draft_count, + const int32_t * target_tokens, + int target_count, + int verify_count, + int commit_budget) noexcept { + if (draft_tokens == nullptr || target_tokens == nullptr || + verify_count <= 0 || draft_count < verify_count || + target_count < verify_count) { + return {}; + } + + int accepted = 1; // seed + while (accepted < verify_count && + draft_tokens[accepted] == target_tokens[accepted - 1]) { + ++accepted; + } + + const int32_t mismatch_token = + accepted < verify_count ? target_tokens[accepted - 1] : 0; + const bool has_bonus = + accepted < verify_count && mismatch_token >= 0; + const int32_t bonus = has_bonus ? mismatch_token : 0; + return precomputed(accepted, verify_count, has_bonus, bonus, commit_budget); + } + + static SpecCommitDecision greedy( + const std::vector & draft_tokens, + const std::vector & target_tokens, + int verify_count, + int commit_budget) noexcept { + return greedy( + draft_tokens.empty() ? nullptr : &draft_tokens[0], + static_cast(draft_tokens.size()), + target_tokens.empty() ? nullptr : &target_tokens[0], + static_cast(target_tokens.size()), + verify_count, commit_budget); + } + + // Finalize a match walk performed by a model-specific verifier (for + // example, sampled verification). The caller supplies the accepted prefix + // and, when a mismatch occurred, the already-selected target bonus token. + static SpecCommitDecision precomputed( + int accepted_count, + int verify_count, + bool bonus_available, + int32_t bonus_token, + int commit_budget) noexcept { + SpecCommitDecision result; + // A full prefix cannot have a bonus. A strict prefix may omit one when + // the target/sample reports the negative no-token sentinel. + if (verify_count <= 0 || accepted_count <= 0 || + accepted_count > verify_count || + (bonus_available && accepted_count >= verify_count) || + (bonus_available && bonus_token < 0)) { + return result; + } + result.valid_ = true; + result.accepted_count_ = accepted_count; + const int budget = std::max(0, commit_budget); + result.commit_count_ = std::min( + budget, result.accepted_count_ + (bonus_available ? 1 : 0)); + result.bonus_available_ = bonus_available; + result.commits_bonus_ = + bonus_available && result.commit_count_ > result.accepted_count_; + result.bonus_token_ = bonus_available ? bonus_token : 0; + return result; + } + + int accepted_count() const noexcept { return accepted_count_; } + int commit_count() const noexcept { return commit_count_; } + bool valid() const noexcept { return valid_; } + bool has_bonus() const noexcept { return bonus_available_; } + bool commits_bonus() const noexcept { return commits_bonus_; } + int32_t bonus_token() const noexcept { return bonus_token_; } + + // Select a committed token without reading beyond the draft prefix or + // returning an unavailable/clipped bonus. + bool token_at( + int index, + const int32_t * draft_tokens, + int draft_count, + int32_t & token) const noexcept { + if (index < 0 || index >= commit_count_ || draft_tokens == nullptr) { + return false; + } + if (!valid_) { + return false; + } + if (index < accepted_count_) { + if (index >= draft_count) { + return false; + } + token = draft_tokens[index]; + if (token < 0) { + return false; + } + return true; + } + if (index == accepted_count_ && commits_bonus_) { + token = bonus_token_; + return true; + } + return false; + } + + bool token_at( + int index, + const std::vector & draft_tokens, + int32_t & token) const noexcept { + return token_at(index, draft_tokens.empty() ? nullptr : &draft_tokens[0], + static_cast(draft_tokens.size()), token); + } + + bool materialize( + const std::vector & draft_tokens, + std::vector & committed_tokens) const { + if (!valid_) { + committed_tokens.clear(); + return false; + } + committed_tokens.resize(static_cast(commit_count_)); + for (int i = 0; i < commit_count_; ++i) { + if (!token_at(i, draft_tokens, committed_tokens[static_cast(i)])) { + committed_tokens.clear(); + return false; + } + } + return true; + } + +private: + int accepted_count_ = 0; + int commit_count_ = 0; + bool bonus_available_ = false; + bool commits_bonus_ = false; + int32_t bonus_token_ = 0; + bool valid_ = false; +}; + +} // namespace dflash::common diff --git a/server/src/gemma4/gemma4_backend.cpp b/server/src/gemma4/gemma4_backend.cpp index 774c4d08f..7400b0686 100644 --- a/server/src/gemma4/gemma4_backend.cpp +++ b/server/src/gemma4/gemma4_backend.cpp @@ -5,6 +5,7 @@ // KV cache with layer sharing, snapshot/restore. #include "gemma4_backend.h" +#include "common/spec_commit.h" #include "dflash27b.h" #include "../qwen3/qwen3_kvflash_scorer.h" #include "common/sampler.h" @@ -637,16 +638,24 @@ bool Gemma4Backend::do_spec_decode(int committed, int n_gen, } // 5. Acceptance: longest matching prefix - int accept_n = 1; - for (int i = 0; i < q_len - 1; i++) { - if (draft_tok[i + 1] == target_tok[i]) accept_n++; - else break; + const auto commit_decision = dflash::common::SpecCommitDecision::greedy( + draft_tok, target_tok, q_len, need_commit_budget); + if (!commit_decision.valid()) { + std::fprintf(stderr, "[gemma4-spec] invalid commit decision\n"); + cache_.cur_pos = committed; + step_graph_destroy(draft_sg); + return false; } - int bonus_tok = (accept_n < q_len) ? target_tok[accept_n - 1] : -1; - int commit_n = accept_n + (bonus_tok >= 0 ? 1 : 0); - if (commit_n > need_commit_budget) { - commit_n = need_commit_budget; - if (commit_n <= accept_n) bonus_tok = -1; + const int accept_n = commit_decision.accepted_count(); + const int bonus_tok = commit_decision.commits_bonus() + ? commit_decision.bonus_token() : -1; + const int commit_n = commit_decision.commit_count(); + std::vector commit_tokens; + if (!commit_decision.materialize(draft_tok, commit_tokens)) { + std::fprintf(stderr, "[gemma4-spec] commit materialization failed\n"); + cache_.cur_pos = committed; + step_graph_destroy(draft_sg); + return false; } // 6. KV truncation: discard rejected positions, keep accepted. @@ -678,7 +687,7 @@ bool Gemma4Backend::do_spec_decode(int committed, int n_gen, bool hit_eos = false; int emitted = 0; for (int i = 0; i < commit_n; i++) { - int tok = (i < accept_n) ? draft_tok[i] : bonus_tok; + const int tok = commit_tokens[(size_t)i]; out_tokens.push_back(tok); io.emit(tok); emitted++; diff --git a/server/src/laguna/laguna_backend.cpp b/server/src/laguna/laguna_backend.cpp index db2d366e0..756ff449f 100644 --- a/server/src/laguna/laguna_backend.cpp +++ b/server/src/laguna/laguna_backend.cpp @@ -7,6 +7,7 @@ // snapshots, and pflash compress lifecycle. #include "laguna_backend.h" +#include "common/spec_commit.h" #include "laguna_internal.h" #include "qwen3/qwen3_kvflash_scorer.h" #include "dflash27b.h" @@ -1106,6 +1107,7 @@ bool LagunaBackend::do_spec_decode(int committed, int n_gen, int accept_n = 1; int bonus_tok = -1; int verify_vocab = 0; + dflash::common::SpecCommitDecision commit_decision; if (sampled_verify) { if (!target->read_verify_logits(q_len, verify_logits)) { std::fprintf(stderr, "[laguna-spec] verify logits read failed\n"); @@ -1127,22 +1129,29 @@ bool LagunaBackend::do_spec_decode(int committed, int n_gen, break; } } + commit_decision = dflash::common::SpecCommitDecision::precomputed( + accept_n, q_len, bonus_tok >= 0, bonus_tok, need_commit_budget); } else { - for (int i = 0; i < q_len - 1; i++) { - if (draft_tok[(size_t)i + 1] == target_tok[(size_t)i]) accept_n++; - else break; - } - bonus_tok = (accept_n < q_len) ? target_tok[(size_t)accept_n - 1] : -1; + commit_decision = dflash::common::SpecCommitDecision::greedy( + draft_tok, target_tok, q_len, need_commit_budget); } - int commit_n = accept_n + (bonus_tok >= 0 ? 1 : 0); - if (commit_n > need_commit_budget) { - commit_n = need_commit_budget; - if (commit_n <= accept_n) bonus_tok = -1; + if (!commit_decision.valid()) { + std::fprintf(stderr, "[laguna-spec] invalid commit decision\n"); + cache_.cur_pos = committed; + step_graph_destroy(draft_sg); + return false; } + accept_n = commit_decision.accepted_count(); + bonus_tok = commit_decision.commits_bonus() + ? commit_decision.bonus_token() : -1; + int commit_n = commit_decision.commit_count(); - std::vector replay_tok((size_t)commit_n); - for (int i = 0; i < commit_n; ++i) { - replay_tok[(size_t)i] = (i < accept_n) ? draft_tok[(size_t)i] : bonus_tok; + std::vector replay_tok; + if (!commit_decision.materialize(draft_tok, replay_tok)) { + std::fprintf(stderr, "[laguna-spec] commit materialization failed\n"); + cache_.cur_pos = committed; + step_graph_destroy(draft_sg); + return false; } std::vector history_after_commit = sample_history; for (int32_t tok : replay_tok) { diff --git a/server/src/qwen35/qwen35_backend.cpp b/server/src/qwen35/qwen35_backend.cpp index 357fef97c..83e4c05b2 100644 --- a/server/src/qwen35/qwen35_backend.cpp +++ b/server/src/qwen35/qwen35_backend.cpp @@ -1,5 +1,6 @@ #include "qwen35_backend.h" #include "common/chain_rollback_policy.h" +#include "common/spec_commit.h" #include "placement/skip_park_guard.h" #include "qwen35_dflash_target.h" #include "graph_builders.h" @@ -2410,6 +2411,7 @@ bool Qwen35Backend::do_spec_decode(int committed, int n_gen, // token (it is already a valid target sample at that position). int accept_n = 1; int bonus_tok = -1; + dflash::common::SpecCommitDecision commit_decision; if (sampled_verify) { if (!target->read_verify_logits(q_len, verify_logits)) { std::fprintf(stderr, "spec-decode: verify logits read failed\n"); @@ -2471,23 +2473,27 @@ bool Qwen35Backend::do_spec_decode(int committed, int n_gen, } } (void)mismatched; + commit_decision = dflash::common::SpecCommitDecision::precomputed( + accept_n, q_len, bonus_tok >= 0, bonus_tok, need_commit_budget); } else { - for (int i = 0; i < q_len - 1; i++) { - if (draft_tok[i + 1] == target_tok[i]) accept_n++; - else break; - } - bonus_tok = (accept_n < q_len) ? target_tok[accept_n - 1] : -1; + commit_decision = dflash::common::SpecCommitDecision::greedy( + draft_tok, target_tok, q_len, need_commit_budget); + } + if (!commit_decision.valid()) { + std::fprintf(stderr, "spec-decode: invalid commit decision\n"); + target->restore_kv(); + step_graph_destroy(draft_sg); + return false; } + accept_n = commit_decision.accepted_count(); + bonus_tok = commit_decision.commits_bonus() + ? commit_decision.bonus_token() : -1; // Track hint acceptance telemetry. if (hint_fill > 0) { n_hint_proposed += hint_fill; n_hint_accepted += std::min(hint_fill, accept_n - 1); } - int commit_n = accept_n + (bonus_tok >= 0 ? 1 : 0); - if (commit_n > need_commit_budget) { - commit_n = need_commit_budget; - if (commit_n <= accept_n) bonus_tok = -1; - } + int commit_n = commit_decision.commit_count(); // 6. Fix state: adaptive fast-rollback vs legacy replay. // Fast-rollback (implicit bonus, skip replay) is profitable when @@ -2532,10 +2538,13 @@ bool Qwen35Backend::do_spec_decode(int committed, int n_gen, step_graph_destroy(draft_sg); return false; } - std::vector replay_batch((size_t)commit_n); - for (int i = 0; i < commit_n; i++) { - replay_batch[i] = (i < accept_n) ? draft_tok[i] : bonus_tok; + std::vector replay_batch; + if (!commit_decision.materialize(draft_tok, replay_batch)) { + std::fprintf(stderr, "spec-decode: commit materialization failed\n"); + step_graph_destroy(draft_sg); + return false; } + replay_batch.resize((size_t)commit_n); if (!target->verify_batch(replay_batch, committed, replay_last_tok, nullptr)) { std::fprintf(stderr, "spec-decode: replay failed\n"); step_graph_destroy(draft_sg); @@ -2545,10 +2554,13 @@ bool Qwen35Backend::do_spec_decode(int committed, int n_gen, } // Build replay_tok for emitting committed tokens. - std::vector replay_tok((size_t)commit_n); - for (int i = 0; i < commit_n; i++) { - replay_tok[i] = (i < accept_n) ? draft_tok[i] : bonus_tok; + std::vector replay_tok; + if (!commit_decision.materialize(draft_tok, replay_tok)) { + std::fprintf(stderr, "spec-decode: commit materialization failed\n"); + step_graph_destroy(draft_sg); + return false; } + replay_tok.resize((size_t)commit_n); // 7. Sync features for replayed range to mirror (needed for next draft step) if (use_remote_draft && cache_.target_feat) { diff --git a/server/src/qwen35moe/qwen35moe_backend.cpp b/server/src/qwen35moe/qwen35moe_backend.cpp index 78052a757..1fc24dbaa 100644 --- a/server/src/qwen35moe/qwen35moe_backend.cpp +++ b/server/src/qwen35moe/qwen35moe_backend.cpp @@ -1,4 +1,5 @@ #include "qwen35moe_backend.h" +#include "common/spec_commit.h" #include "../common/moe_hybrid_placement.h" #include "../common/moe_hybrid_stream.h" @@ -2098,18 +2099,20 @@ bool Qwen35MoeBackend::do_hybrid_spec_decode(int committed, int n_gen, } // 5. Acceptance: longest matching prefix - int accept_n = 1; - for (int i = 0; i < verify_width - 1; i++) { - if (draft_tok[i + 1] == target_tok[i]) accept_n++; - else break; + const auto commit_decision = dflash::common::SpecCommitDecision::greedy( + draft_tok, target_tok, verify_width, need_commit_budget); + if (!commit_decision.valid()) { + std::fprintf(stderr, "[hybrid-spec] invalid commit decision\n"); + if (!restore_ssm_state(target_cache(), target_backend())) { + std::fprintf(stderr, + "[hybrid-spec] recurrent-state restore failed\n"); + } + step_graph_destroy(draft_sg); + return false; } - int bonus_tok = (accept_n < verify_width) ? target_tok[accept_n - 1] : -1; + const int accept_n = commit_decision.accepted_count(); observed_max_accept = std::max(observed_max_accept, accept_n); - int commit_n = accept_n + (bonus_tok >= 0 ? 1 : 0); - if (commit_n > need_commit_budget) { - commit_n = need_commit_budget; - if (commit_n <= accept_n) bonus_tok = -1; - } + const int commit_n = commit_decision.commit_count(); // 6. Restore and replay accepted tokens if (!restore_ssm_state(target_cache(), target_backend())) { @@ -2118,9 +2121,11 @@ bool Qwen35MoeBackend::do_hybrid_spec_decode(int committed, int n_gen, return false; } - std::vector replay_tok((size_t)commit_n); - for (int i = 0; i < commit_n; i++) { - replay_tok[i] = (i < accept_n) ? draft_tok[i] : bonus_tok; + std::vector replay_tok; + if (!commit_decision.materialize(draft_tok, replay_tok)) { + std::fprintf(stderr, "[hybrid-spec] commit materialization failed\n"); + step_graph_destroy(draft_sg); + return false; } // Replay tokens through batched hybrid forward (captures features for next draft step) diff --git a/server/src/server/http_server.cpp b/server/src/server/http_server.cpp index 46081fa23..a67ab3f2a 100644 --- a/server/src/server/http_server.cpp +++ b/server/src/server/http_server.cpp @@ -2916,10 +2916,11 @@ HttpServer::GenerationCacheState HttpServer::prepare_generation_cache( cache.snap_cut = prepared_snapshot.second; }; auto prepare_full = [&]() { + cache.full_snap_pos = (int) effective_prompt.size(); cache.full_snap_slot = - prefix_cache_.prepare_full_snap(req.prompt_tokens); + prefix_cache_.prepare_full_snap( + req.prompt_tokens, cache.full_snap_pos); if (cache.full_snap_slot >= 0) { - cache.full_snap_pos = (int) effective_prompt.size(); generate_request.snap_slot = cache.full_snap_slot; generate_request.snap_pos = cache.full_snap_pos; cache.full_snap_prepared = true; @@ -2994,8 +2995,13 @@ void HttpServer::finalize_generation_cache( backend_.snapshot_cur_pos(cache.full_snap_slot); if (saved_position > 0 && saved_position <= cache.full_snap_pos) { - prefix_cache_.confirm_full_snap( - cache.full_snap_slot, req.prompt_tokens, saved_position); + if (!prefix_cache_.confirm_full_snap( + cache.full_snap_slot, + req.prompt_tokens, + saved_position)) { + backend_.snapshot_free(cache.full_snap_slot); + prefix_cache_.abort_full_snap(cache.full_snap_slot); + } } else { backend_.snapshot_free(cache.full_snap_slot); prefix_cache_.abort_full_snap(cache.full_snap_slot); diff --git a/server/src/server/prefix_cache.cpp b/server/src/server/prefix_cache.cpp index 4ab20c590..1555e618b 100644 --- a/server/src/server/prefix_cache.cpp +++ b/server/src/server/prefix_cache.cpp @@ -140,38 +140,6 @@ PrefixHash hash_prefix(const int32_t * ids, int count) { return h; } -// ─── Prefix-aware eviction ────────────────────────────────────────────── - -static bool is_strict_prefix(const std::vector & a, - const std::vector & b) { - // True iff `a` is a strict (shorter) prefix of `b`. - if (a.size() >= b.size()) return false; - return std::equal(a.begin(), a.end(), b.begin()); -} - -int select_inline_evict_victim(const std::vector *> & ids_lru) { - const int n = (int)ids_lru.size(); - if (n <= 0) return 0; - // Oldest-first scan: evict the first entry that is not a strict prefix of any - // other entry (a leaf). Shared ancestor prefixes are thereby kept resident. - for (int i = 0; i < n; i++) { - bool is_ancestor = false; - for (int j = 0; j < n; j++) { - if (j == i) continue; - if (is_strict_prefix(*ids_lru[i], *ids_lru[j])) { is_ancestor = true; break; } - } - if (!is_ancestor) return i; // oldest leaf - } - return 0; // unreachable (the longest entry is always a leaf); pure-LRU fallback -} - -int select_inline_evict_victim(const std::vector> & ids_lru) { - std::vector *> ptrs; - ptrs.reserve(ids_lru.size()); - for (const auto & v : ids_lru) ptrs.push_back(&v); - return select_inline_evict_victim(ptrs); -} - int select_inline_snapshot_boundary(const std::vector & boundaries, int restored_prefix_len) { if (boundaries.empty()) return 0; @@ -184,7 +152,8 @@ int select_inline_snapshot_boundary(const std::vector & boundaries, // ─── PrefixCache ──────────────────────────────────────────────────────── PrefixCache::PrefixCache(int cap, const Tokenizer & tokenizer) - : cap_(std::min(cap, MAX_SLOTS)) + : cap_(std::min(cap, MAX_SLOTS)), + inline_state_(std::max(0, std::min(cap, MAX_SLOTS))) { if (cap_ <= 0) { disabled_ = true; @@ -203,32 +172,14 @@ PrefixCache::PrefixCache(int cap, const Tokenizer & tokenizer) // ── LRU helpers ───────────────────────────────────────────────────────── -int PrefixCache::find_entry(const PrefixHash & h) const { - for (int i = 0; i < (int)entries_.size(); i++) { - if (entries_[i].hash == h) return i; - } - return -1; +void PrefixCache::sync_inline_size() { + entries_size_count_.store( + inline_state_.size(), std::memory_order_relaxed); } -void PrefixCache::move_to_end(int idx) { - if (idx < 0 || idx >= (int)entries_.size()) return; - auto e = std::move(entries_[idx]); - entries_.erase(entries_.begin() + idx); - entries_.push_back(std::move(e)); -} - -int PrefixCache::find_full_entry(const PrefixHash & h) const { - for (int i = 0; i < (int)full_entries_.size(); i++) { - if (full_entries_[i].hash == h) return i; - } - return -1; -} - -void PrefixCache::move_full_to_end(int idx) { - if (idx < 0 || idx >= (int)full_entries_.size()) return; - auto e = std::move(full_entries_[idx]); - full_entries_.erase(full_entries_.begin() + idx); - full_entries_.push_back(std::move(e)); +void PrefixCache::sync_full_size() { + full_entries_size_count_.store( + full_state_.size(), std::memory_order_relaxed); } // ── Inline prefix cache ───────────────────────────────────────────────── @@ -241,26 +192,21 @@ std::pair PrefixCache::lookup(const std::vector & prompt_ids) for (int cut : boundaries) { auto key = hash_prefix(prompt_ids.data(), cut); - int idx = find_entry(key); - if (idx >= 0) { - const int committed = (int)entries_[idx].ids.size(); - if (committed != cut) { - // Slot was refreshed in-place at a deeper boundary; a shallow - // hash→slot entry would restore the wrong cur_pos. - std::fprintf(stderr, - "[pc] lookup stale slot=%d key_cut=%d committed=%d — evicting\n", - entries_[idx].slot, cut, committed); - entries_.erase(entries_.begin() + idx); - entries_size_count_.fetch_sub(1, std::memory_order_relaxed); - continue; - } - if (cut > best_len) { - best_slot = entries_[idx].slot; - best_len = cut; - } - move_to_end(idx); + const auto result = inline_state_.lookup_candidate(key, cut); + if (result.stale_removed) { + // Slot was refreshed in-place at a deeper boundary; a shallow + // hash→slot entry would restore the wrong cur_pos. + std::fprintf(stderr, + "[pc] lookup stale slot=%d key_cut=%d committed=%d — evicting\n", + result.stale_slot, cut, result.stale_committed_len); + continue; + } + if (result.slot >= 0 && cut > best_len) { + best_slot = result.slot; + best_len = result.prefix_len; } } + sync_inline_size(); if (best_slot >= 0) { lifetime_hits_.fetch_add(1, std::memory_order_relaxed); @@ -281,68 +227,44 @@ std::pair PrefixCache::prepare_inline_snap( if (target_cut <= 0) return {-1, 0}; auto key = hash_prefix(prompt_ids.data(), target_cut); - if (find_entry(key) >= 0) return {-1, 0}; // already cached - - int slot; - if ((int)entries_.size() >= cap_) { - // At capacity — reserve a slot without evicting yet. Prefix-aware: prefer - // the oldest leaf so shared ancestor prefixes (reused by later branches) - // stay resident. entries_ is already in LRU order (front = oldest). - std::vector *> ids_lru; - ids_lru.reserve(entries_.size()); - for (const auto & e : entries_) ids_lru.push_back(&e.ids); - int victim = select_inline_evict_victim(ids_lru); - pending_evict_key_ = entries_[victim].hash; - has_pending_evict_ = true; - slot = entries_[victim].slot; - if (victim != 0) { - std::fprintf(stderr, - "[pc] prefix-aware evict: victim idx=%d (len=%zu) kept oldest " - "ancestor (len=%zu)\n", - victim, entries_[victim].ids.size(), entries_.front().ids.size()); - } - } else { - slot = next_slot_; - next_slot_ = (next_slot_ + 1) % cap_; - has_pending_evict_ = false; + const auto reservation = inline_state_.prepare(key, target_cut); + if (reservation.slot < 0) return {-1, 0}; + if (reservation.victim_index > 0) { + std::fprintf(stderr, + "[pc] prefix-aware evict: victim idx=%d (len=%d) kept oldest " + "ancestor (len=%d)\n", + reservation.victim_index, reservation.victim_len, + reservation.oldest_len); } - return {slot, target_cut}; + return {reservation.slot, reservation.target_cut}; } void PrefixCache::confirm_inline_snap(int slot, int target_cut, const std::vector & prompt_ids) { if (disabled_) return; - - // Evict the reserved entry (if any). - if (has_pending_evict_) { - int idx = find_entry(pending_evict_key_); - if (idx >= 0) { - entries_.erase(entries_.begin() + idx); - entries_size_count_.fetch_sub(1, std::memory_order_relaxed); - } - has_pending_evict_ = false; + if (slot < 0 || slot >= cap_ || target_cut <= 0 || + target_cut > (int)prompt_ids.size()) { + std::fprintf(stderr, + "[pc] rejected inline-snap slot=%d prefix_len=%d prompt_len=%zu\n", + slot, target_cut, prompt_ids.size()); + return; } - // The new snapshot replaces whatever this slot previously held. Drop any - // other entries still pointing at the slot: their hashes describe a - // different (or shorter) token stream than the new snapshot, and a later - // restore through them would attach mismatched KV. Stale entries arise - // when an aborted snap burns a round-robin next_slot_ step and a later - // confirm wraps onto a slot with a live entry (PR #370 repro). - for (int i = (int)entries_.size() - 1; i >= 0; --i) { - if (entries_[(size_t)i].slot == slot) { - std::fprintf(stderr, - "[pc] dropping stale entry for reused slot=%d\n", slot); - entries_.erase(entries_.begin() + i); - entries_size_count_.fetch_sub(1, std::memory_order_relaxed); - } + const auto key = hash_prefix(prompt_ids.data(), target_cut); + const auto result = + inline_state_.confirm(slot, key, target_cut, prompt_ids); + if (!result.accepted) { + std::fprintf(stderr, + "[pc] rejected inline-snap slot=%d prefix_len=%d prompt_len=%zu\n", + slot, target_cut, prompt_ids.size()); + return; } - - auto key = hash_prefix(prompt_ids.data(), target_cut); - std::vector ids(prompt_ids.begin(), prompt_ids.begin() + target_cut); - entries_.push_back({key, slot, std::move(ids)}); - entries_size_count_.fetch_add(1, std::memory_order_relaxed); + for (int i = 0; i < result.stale_slot_entries_removed; ++i) { + std::fprintf(stderr, + "[pc] dropping stale entry for reused slot=%d\n", slot); + } + sync_inline_size(); std::fprintf(stderr, "[pc] inline-snap committed slot=%d prefix_len=%d\n", slot, target_cut); } @@ -353,40 +275,32 @@ void PrefixCache::abort_inline_snap(int slot) { // metadata still pointing at it is therefore invalid, whether the slot was // selected through the explicit eviction path or through a round-robin // hole left by an earlier aborted reservation. - for (int i = (int)entries_.size() - 1; i >= 0; --i) { - if (entries_[(size_t)i].slot == slot) { - entries_.erase(entries_.begin() + i); - entries_size_count_.fetch_sub(1, std::memory_order_relaxed); - } - } - has_pending_evict_ = false; + inline_state_.abort(slot); + sync_inline_size(); } void PrefixCache::cancel_inline_snap(int slot) { if (disabled_) return; - if (has_pending_evict_) { - const int idx = find_entry(pending_evict_key_); - if (idx >= 0 && entries_[idx].slot != slot) return; - } - has_pending_evict_ = false; + inline_state_.cancel(slot); } void PrefixCache::mark_all_cleared() { if (disabled_) return; - int n = (int)entries_.size(); - entries_.clear(); - entries_size_count_.store(0, std::memory_order_relaxed); - next_slot_ = 0; - has_pending_evict_ = false; + const int n = inline_state_.size(); + inline_state_.clear(); + sync_inline_size(); std::fprintf(stderr, "[pc] all-cleared — dropped %d LRU entries\n", n); } // ── Full-compress cache ───────────────────────────────────────────────── void PrefixCache::init_full_cache(int full_cap) { + constexpr int DISK_STAGING_SLOT = MAX_SLOTS - 1; if (full_cap <= 0) { full_disabled_ = true; full_cap_ = 0; + full_state_.configure(0, 0, DISK_STAGING_SLOT); + sync_full_size(); return; } // Reserve the last slot (MAX_SLOTS-1) for the disk-prefix-cache staging @@ -397,108 +311,98 @@ void PrefixCache::init_full_cache(int full_cap) { if (full_cap > remaining) full_cap = remaining; if (full_cap <= 0) { full_disabled_ = true; + full_cap_ = 0; + full_state_.configure(0, 0, DISK_STAGING_SLOT); + sync_full_size(); return; } full_cap_ = full_cap; - full_slot_base_ = cap_; - full_next_slot_ = 0; - full_disabled_ = false; + full_disabled_ = + !full_state_.configure(cap_, full_cap_, DISK_STAGING_SLOT); + sync_full_size(); + if (full_disabled_) { + full_cap_ = 0; + std::fprintf(stderr, + "[pc] full-cache disabled: invalid slot range base=%d cap=%d " + "staging=%d\n", + cap_, full_cap, DISK_STAGING_SLOT); + return; + } std::fprintf(stderr, "[pc] full-cache enabled: cap=%d slots=[%d,%d)\n", - full_cap_, full_slot_base_, full_slot_base_ + full_cap_); + full_cap_, full_state_.slot_base(), + full_state_.slot_base() + full_cap_); } std::pair PrefixCache::lookup_full(const std::vector & prompt_ids) { if (full_disabled_) return {-1, 0}; auto key = hash_prefix(prompt_ids.data(), (int)prompt_ids.size()); - int idx = find_full_entry(key); - if (idx < 0) return {-1, 0}; - - auto & e = full_entries_[idx].entry; - e.hits++; - e.last_used_ns = std::chrono::duration_cast( - std::chrono::steady_clock::now().time_since_epoch()).count(); - int slot = e.slot; - int cur_ids_len = e.cur_ids_len; - move_full_to_end(idx); + const int64_t now_ns = + std::chrono::duration_cast( + std::chrono::steady_clock::now().time_since_epoch()).count(); + const auto result = full_state_.lookup(key, now_ns); + if (result.slot < 0) return {-1, 0}; + full_lifetime_hits_.fetch_add(1, std::memory_order_relaxed); std::fprintf(stderr, "[pc] full-cache hit slot=%d cur_ids_len=%d\n", - slot, cur_ids_len); - return {slot, cur_ids_len}; + result.slot, result.cur_ids_len); + return {result.slot, result.cur_ids_len}; } -int PrefixCache::prepare_full_snap(const std::vector & prompt_ids) { +int PrefixCache::prepare_full_snap(const std::vector & prompt_ids, + int expected_snapshot_len) { if (full_disabled_) return -1; auto key = hash_prefix(prompt_ids.data(), (int)prompt_ids.size()); - if (find_full_entry(key) >= 0) return -1; // already cached - - int abs_slot; - if ((int)full_entries_.size() >= full_cap_) { - // Evict LRU - full_pending_evict_key_ = full_entries_.front().hash; - full_has_pending_evict_ = true; - abs_slot = full_entries_.front().entry.slot; - } else { - abs_slot = full_slot_base_ + full_next_slot_; - full_next_slot_ = (full_next_slot_ + 1) % full_cap_; - full_has_pending_evict_ = false; - } - - return abs_slot; + const auto reservation = + full_state_.prepare(key, expected_snapshot_len); + return reservation.accepted ? reservation.slot : -1; } -void PrefixCache::confirm_full_snap(int slot, +bool PrefixCache::confirm_full_snap(int slot, const std::vector & prompt_ids, - int cur_ids_len) { - if (full_disabled_) return; - - if (full_has_pending_evict_) { - int idx = find_full_entry(full_pending_evict_key_); - if (idx >= 0) { - full_entries_.erase(full_entries_.begin() + idx); - full_entries_size_count_.fetch_sub(1, std::memory_order_relaxed); - } - full_has_pending_evict_ = false; - } - - for (int i = (int)full_entries_.size() - 1; i >= 0; --i) { - if (full_entries_[(size_t)i].entry.slot == slot) { - std::fprintf(stderr, - "[pc] dropping stale full-cache entry for reused slot=%d\n", slot); - full_entries_.erase(full_entries_.begin() + i); - full_entries_size_count_.fetch_sub(1, std::memory_order_relaxed); - } - } + int saved_snapshot_len) { + if (full_disabled_) return false; auto key = hash_prefix(prompt_ids.data(), (int)prompt_ids.size()); - FullCacheEntry entry; - entry.slot = slot; - entry.cur_ids_len = cur_ids_len; - entry.raw_prompt_len = (int)prompt_ids.size(); - entry.last_used_ns = std::chrono::duration_cast( - std::chrono::steady_clock::now().time_since_epoch()).count(); - entry.hits = 0; - full_entries_.push_back({key, std::move(entry)}); - full_entries_size_count_.fetch_add(1, std::memory_order_relaxed); + const int64_t now_ns = + std::chrono::duration_cast( + std::chrono::steady_clock::now().time_since_epoch()).count(); + const auto result = full_state_.confirm( + slot, key, (int)prompt_ids.size(), saved_snapshot_len, now_ns); + if (!result.accepted) { + std::fprintf(stderr, + "[pc] rejected full-cache confirm slot=%d raw_len=%zu " + "saved_pos=%d expected_pos=%d\n", + slot, prompt_ids.size(), saved_snapshot_len, + full_state_.pending_expected_snapshot_len()); + return false; + } + sync_full_size(); std::fprintf(stderr, "[pc] full-cache committed slot=%d cur_ids_len=%d\n", - slot, cur_ids_len); + slot, saved_snapshot_len); + return true; } void PrefixCache::abort_full_snap(int slot) { if (full_disabled_) return; - // The reserved backend slot was cleared before generation. Purge every - // stale key that still names it, including round-robin reuse through a - // sparse pool where no LRU eviction key was recorded. - for (int i = (int)full_entries_.size() - 1; i >= 0; --i) { - if (full_entries_[(size_t)i].entry.slot == slot) { - full_entries_.erase(full_entries_.begin() + i); - full_entries_size_count_.fetch_sub(1, std::memory_order_relaxed); + + if (full_state_.has_pending_reservation()) { + const auto result = full_state_.abort(slot); + if (!result.accepted) { + std::fprintf(stderr, + "[pc] rejected full-cache abort slot=%d pending_slot=%d\n", + slot, full_state_.pending_slot()); + return; } + } else { + // This is invalidation of a committed backend snapshot, not an + // in-flight reservation abort (e.g. snapshot loss after recovery). + full_state_.invalidate_slot(slot); } - full_has_pending_evict_ = false; + sync_full_size(); } PrefixCache::InlineStats PrefixCache::stats() const { diff --git a/server/src/server/prefix_cache.h b/server/src/server/prefix_cache.h index 2a0515749..22bca7e0c 100644 --- a/server/src/server/prefix_cache.h +++ b/server/src/server/prefix_cache.h @@ -12,9 +12,9 @@ #pragma once +#include "prefix_cache_state.h" #include "tokenizer.h" -#include #include #include #include @@ -42,7 +42,6 @@ std::vector find_all_boundaries(const std::vector & ids, const ChatMarkers & markers); // SHA-1 hash of a prefix (truncated to 16 bytes). -using PrefixHash = std::array; PrefixHash hash_prefix(const int32_t * ids, int count); // Prefix-aware inline eviction policy. Given the cached prefixes in LRU order @@ -50,12 +49,8 @@ PrefixHash hash_prefix(const int32_t * ids, int count); // whose ids are NOT a strict prefix of any other entry's ids (a "leaf"). Keeping // shared ancestor prefixes resident avoids re-prefilling them for later branches. // Returns 0 (pure-LRU fallback) when ids_lru is empty or, impossibly, no leaf -// is found. Pure and model-free so it can be unit-tested without a PrefixCache. -// The pointer overload is the core (the caller passes pointers into its own -// entries so no token vectors are copied); the value overload is a convenience -// wrapper for tests. -int select_inline_evict_victim(const std::vector *> & ids_lru); -int select_inline_evict_victim(const std::vector> & ids_lru); +// is found. The implementation lives in prefix_cache_state.h so the exact +// production policy can also be model-checked without server dependencies. // Pick the inline snapshot boundary for a request. We cache the boundary before // the current user turn (second-to-last marker) and only when it advances past @@ -63,16 +58,9 @@ int select_inline_evict_victim(const std::vector> & ids_lru int select_inline_snapshot_boundary(const std::vector & boundaries, int restored_prefix_len = 0); -// ─── Prefix cache entry ───────────────────────────────────────────────── - -struct FullCacheEntry { - int slot = -1; - std::string cur_bin_path; - int cur_ids_len = 0; - int raw_prompt_len = 0; - int64_t last_used_ns = 0; - int hits = 0; -}; +// Preserve the existing public entry name while keeping one authoritative +// representation in the state core. +using FullCacheEntry = FullPrefixCacheState::Entry; // ─── PrefixCache ──────────────────────────────────────────────────────── @@ -123,12 +111,15 @@ class PrefixCache { // Exact-match lookup. Returns (slot, cur_ids_len) or (-1, 0). std::pair lookup_full(const std::vector & prompt_ids); - // Reserve a slot. Returns slot or -1. - int prepare_full_snap(const std::vector & prompt_ids); + // Reserve a slot and bind the effective-prompt boundary beyond which the + // backend must not report a saved snapshot. Returns slot or -1. + int prepare_full_snap(const std::vector & prompt_ids, + int expected_snapshot_len); - // Confirm after successful snapshot save. - void confirm_full_snap(int slot, const std::vector & prompt_ids, - int cur_ids_len); + // Confirm after successful snapshot save. Returns false without committing + // unless slot, raw-prompt key, and saved position match the reservation. + bool confirm_full_snap(int slot, const std::vector & prompt_ids, + int saved_snapshot_len); // Abort reservation. void abort_full_snap(int slot); @@ -163,52 +154,33 @@ class PrefixCache { int cap_ = 0; ChatMarkers markers_; - // LRU for inline prefix cache: ordered map of hash → slot. - // We use a vector to maintain insertion order (front = oldest). - struct LruEntry { - PrefixHash hash; - int slot; - std::vector ids; // prefix tokens [0, target_cut) for prefix-aware eviction - }; - std::vector entries_; - int next_slot_ = 0; - PrefixHash pending_evict_key_{}; - bool has_pending_evict_ = false; + // Boundary detection and hashing live in PrefixCache; all inline-cache + // transitions live in this dependency-free core shared with ESBMC. + InlinePrefixCacheState inline_state_; - // Full-cache state + // Full-cache transitions and LRU ownership live in the same + // dependency-light state core used by native and formal tests. bool full_disabled_ = true; int full_cap_ = 0; - int full_slot_base_ = 0; - int full_next_slot_ = 0; - - struct FullLruEntry { - PrefixHash hash; - FullCacheEntry entry; - }; - std::vector full_entries_; - PrefixHash full_pending_evict_key_{}; - bool full_has_pending_evict_ = false; + FullPrefixCacheState full_state_; // Atomic so /props can read them from a client thread without // tearing across the daemon thread's increments. Relaxed ordering // is sufficient — no synchronization with other state required. std::atomic lifetime_hits_{0}; // inline cache hits std::atomic full_lifetime_hits_{0}; // full-compress cache hits std::atomic full_disk_bytes_{0}; // best-effort snapshot of disk usage - // Atomic mirrors of `entries_.size()` and `full_entries_.size()`. - // The vectors themselves are mutated only on the daemon thread + // Atomic mirrors of `inline_state_.size()` and `full_state_.size()`. + // The backing states are mutated only on the daemon thread // under the daemon's serialised request loop, but `/props` reads // happen from the client thread — calling `.size()` there is a - // data race per the C++ memory model. Bump these alongside every - // push_back / erase / clear so the public introspection counters - // stay well-defined. (Codex r1 P2 follow-up.) - std::atomic entries_size_count_{0}; // mirrors entries_.size() - std::atomic full_entries_size_count_{0}; // mirrors full_entries_.size() + // data race per the C++ memory model. Store these after mutations so the + // public counters stay well-defined. (Codex r1 P2 follow-up.) + std::atomic entries_size_count_{0}; // mirrors inline_state_.size() + std::atomic full_entries_size_count_{0}; // mirrors full_state_.size() // Helpers - int find_entry(const PrefixHash & h) const; - void move_to_end(int idx); - int find_full_entry(const PrefixHash & h) const; - void move_full_to_end(int idx); + void sync_inline_size(); + void sync_full_size(); }; } // namespace dflash::common diff --git a/server/src/server/prefix_cache_state.h b/server/src/server/prefix_cache_state.h new file mode 100644 index 000000000..c28125536 --- /dev/null +++ b/server/src/server/prefix_cache_state.h @@ -0,0 +1,606 @@ +// Verification-friendly state core for the inline prefix cache. +// +// This header deliberately contains no tokenizer, hashing, ggml, CUDA, or +// server dependencies. PrefixCache performs boundary detection and key +// derivation, then delegates its state transitions here. The same production +// transition code is therefore usable by native unit tests and ESBMC harnesses. + +#pragma once + +#include +#include +#include +#include +#include +#include + +namespace dflash::common { + +using PrefixHash = std::array; + +// Keep equality explicit instead of delegating to std::array's loop. Besides +// being cheap for a fixed 128-bit key, this gives model checkers a finite, +// fully unrolled comparison while remaining the production implementation. +inline bool prefix_hash_equal( + const PrefixHash & lhs, const PrefixHash & rhs) { + return lhs[0] == rhs[0] && lhs[1] == rhs[1] && + lhs[2] == rhs[2] && lhs[3] == rhs[3] && + lhs[4] == rhs[4] && lhs[5] == rhs[5] && + lhs[6] == rhs[6] && lhs[7] == rhs[7] && + lhs[8] == rhs[8] && lhs[9] == rhs[9] && + lhs[10] == rhs[10] && lhs[11] == rhs[11] && + lhs[12] == rhs[12] && lhs[13] == rhs[13] && + lhs[14] == rhs[14] && lhs[15] == rhs[15]; +} + +inline void prefix_hash_copy(PrefixHash & dst, const PrefixHash & src) { + dst[0] = src[0]; + dst[1] = src[1]; + dst[2] = src[2]; + dst[3] = src[3]; + dst[4] = src[4]; + dst[5] = src[5]; + dst[6] = src[6]; + dst[7] = src[7]; + dst[8] = src[8]; + dst[9] = src[9]; + dst[10] = src[10]; + dst[11] = src[11]; + dst[12] = src[12]; + dst[13] = src[13]; + dst[14] = src[14]; + dst[15] = src[15]; +} + +namespace prefix_cache_detail { + +inline bool is_strict_prefix(const std::vector & a, + const std::vector & b) { + if (a.size() >= b.size()) return false; + return std::equal(a.begin(), a.end(), b.begin()); +} + +} // namespace prefix_cache_detail + +// Prefix-aware inline eviction policy. Inputs are in LRU order +// (index 0 = oldest). Prefer the oldest leaf so shared ancestors remain hot. +inline int select_inline_evict_victim( + const std::vector *> & ids_lru) { + const int n = (int)ids_lru.size(); + if (n <= 0) return 0; + for (int i = 0; i < n; ++i) { + bool is_ancestor = false; + for (int j = 0; j < n; ++j) { + if (j == i) continue; + if (prefix_cache_detail::is_strict_prefix( + *ids_lru[(size_t)i], *ids_lru[(size_t)j])) { + is_ancestor = true; + break; + } + } + if (!is_ancestor) return i; + } + return 0; +} + +inline int select_inline_evict_victim( + const std::vector> & ids_lru) { + std::vector *> ptrs; + ptrs.reserve(ids_lru.size()); + for (const auto & ids : ids_lru) ptrs.push_back(&ids); + return select_inline_evict_victim(ptrs); +} + +// Select a slot below the production PrefixCache limit of 64 slots. Keeping +// this allocation decision scalar makes the behavior independently +// model-checkable; InlinePrefixCacheState remains responsible for deriving the +// occupancy mask from its committed entries. +inline int select_inline_free_slot( + int next_slot, int capacity, uint64_t occupied_slots) { + if (capacity <= 0 || next_slot < 0 || next_slot >= capacity) { + return -1; + } + // InlinePrefixCacheState is independently usable, while the production + // PrefixCache clamps capacity to 64. Preserve the legacy round-robin + // behavior for out-of-contract standalone capacities that do not fit the + // occupancy mask. + if (capacity > 64) return next_slot; + + for (int offset = 0; offset < capacity; ++offset) { + const int candidate = (next_slot + offset) % capacity; + const uint64_t candidate_bit = uint64_t{1} << candidate; + if ((occupied_slots & candidate_bit) == 0) { + return candidate; + } + } + return -1; +} + +class InlinePrefixCacheState { +public: + struct Entry { + PrefixHash hash{}; + int slot = -1; + std::vector ids; + }; + + struct LookupResult { + int slot = -1; + int prefix_len = 0; + bool stale_removed = false; + int stale_slot = -1; + int stale_committed_len = 0; + }; + + struct PrepareResult { + int slot = -1; + int target_cut = 0; + int victim_index = -1; + int victim_len = 0; + int oldest_len = 0; + }; + + struct ConfirmResult { + bool accepted = false; + int pending_removed = 0; + int stale_slot_entries_removed = 0; + }; + + explicit InlinePrefixCacheState(int capacity = 0) + : capacity_(std::max(0, capacity)) {} + + int capacity() const { return capacity_; } + int size() const { return (int)entries_.size(); } + int next_slot() const { return next_slot_; } + bool has_pending_eviction() const { return has_pending_evict_; } + const PrefixHash & pending_eviction_key() const { + return pending_evict_key_; + } + const std::vector & entries() const { return entries_; } + + int find(const PrefixHash & hash) const { + for (int i = 0; i < (int)entries_.size(); ++i) { + if (prefix_hash_equal(entries_[(size_t)i].hash, hash)) return i; + } + return -1; + } + + bool contains(const PrefixHash & hash) const { return find(hash) >= 0; } + + LookupResult lookup_candidate(const PrefixHash & hash, int cut) { + LookupResult result; + const int idx = find(hash); + if (idx < 0) return result; + + const int committed = (int)entries_[(size_t)idx].ids.size(); + if (committed != cut) { + result.stale_removed = true; + result.stale_slot = entries_[(size_t)idx].slot; + result.stale_committed_len = committed; + entries_.erase(entries_.begin() + idx); + return result; + } + + result.slot = entries_[(size_t)idx].slot; + result.prefix_len = cut; + move_to_end(idx); + return result; + } + + PrepareResult prepare(const PrefixHash & hash, int target_cut) { + PrepareResult result; + if (capacity_ <= 0 || target_cut <= 0 || contains(hash)) return result; + + result.target_cut = target_cut; + if ((int)entries_.size() >= capacity_) { + std::vector *> ids_lru; + ids_lru.reserve(entries_.size()); + for (const auto & entry : entries_) ids_lru.push_back(&entry.ids); + + const int victim = select_inline_evict_victim(ids_lru); + pending_evict_key_ = entries_[(size_t)victim].hash; + has_pending_evict_ = true; + result.slot = entries_[(size_t)victim].slot; + result.victim_index = victim; + result.victim_len = + (int)entries_[(size_t)victim].ids.size(); + result.oldest_len = (int)entries_.front().ids.size(); + } else { + uint64_t occupied_slots = 0; + if (capacity_ <= 64) { + for (const auto & entry : entries_) { + if (entry.slot >= 0 && entry.slot < 64) { + occupied_slots |= uint64_t{1} << entry.slot; + } + } + } + result.slot = select_inline_free_slot( + next_slot_, capacity_, occupied_slots); + next_slot_ = (result.slot + 1) % capacity_; + has_pending_evict_ = false; + } + return result; + } + + ConfirmResult confirm(int slot, const PrefixHash & hash, int target_cut, + const std::vector & prompt_ids) { + ConfirmResult result; + if (slot < 0 || slot >= capacity_ || target_cut <= 0 || + target_cut > (int)prompt_ids.size()) { + return result; + } + + if (has_pending_evict_) { + const int idx = find(pending_evict_key_); + if (idx >= 0) { + entries_.erase(entries_.begin() + idx); + result.pending_removed = 1; + } + has_pending_evict_ = false; + } + + for (int i = (int)entries_.size() - 1; i >= 0; --i) { + if (entries_[(size_t)i].slot == slot) { + entries_.erase(entries_.begin() + i); + ++result.stale_slot_entries_removed; + } + } + + std::vector ids( + prompt_ids.begin(), prompt_ids.begin() + target_cut); + entries_.push_back({hash, slot, std::move(ids)}); + result.accepted = true; + return result; + } + + int abort(int slot) { + int removed = 0; + for (int i = (int)entries_.size() - 1; i >= 0; --i) { + if (entries_[(size_t)i].slot == slot) { + entries_.erase(entries_.begin() + i); + ++removed; + } + } + has_pending_evict_ = false; + return removed; + } + + // Returns false only when the supplied slot does not own the pending + // reservation. In that case state is left untouched. + bool cancel(int slot) { + if (has_pending_evict_) { + const int idx = find(pending_evict_key_); + if (idx >= 0 && entries_[(size_t)idx].slot != slot) return false; + } + has_pending_evict_ = false; + return true; + } + + void clear() { + entries_.clear(); + next_slot_ = 0; + has_pending_evict_ = false; + pending_evict_key_ = {}; + } + +private: + void move_to_end(int idx) { + if (idx < 0 || idx >= (int)entries_.size()) return; + auto entry = std::move(entries_[(size_t)idx]); + entries_.erase(entries_.begin() + idx); + entries_.push_back(std::move(entry)); + } + + int capacity_ = 0; + std::vector entries_; + int next_slot_ = 0; + PrefixHash pending_evict_key_{}; + bool has_pending_evict_ = false; +}; + +// Exact-match full-prompt cache state. Slots are absolute backend snapshot +// slots, while allocation is relative to [slot_base, slot_base + capacity). +// The staging slot is supplied separately and configuration is rejected when +// the two ranges overlap. +// +// A reservation binds the requested key, destination slot, effective snapshot +// boundary, and (when the pool is full) the LRU victim. Confirm and +// abort must match that reservation before committed metadata can change. +// This prevents a late or partial snapshot from being published as an +// exact-prompt hit. +class FullPrefixCacheState { +public: + struct Entry { + PrefixHash hash{}; + int slot = -1; + int cur_ids_len = 0; + int raw_prompt_len = 0; + int64_t last_used_ns = 0; + int hits = 0; + + Entry() = default; + Entry(const Entry & other) { copy_from(other); } + Entry(Entry && other) noexcept { copy_from(other); } + Entry & operator=(const Entry & other) { + if (this != &other) copy_from(other); + return *this; + } + Entry & operator=(Entry && other) noexcept { + if (this != &other) copy_from(other); + return *this; + } + + private: + void copy_from(const Entry & other) { + prefix_hash_copy(hash, other.hash); + slot = other.slot; + cur_ids_len = other.cur_ids_len; + raw_prompt_len = other.raw_prompt_len; + last_used_ns = other.last_used_ns; + hits = other.hits; + } + }; + + struct LookupResult { + int slot = -1; + int cur_ids_len = 0; + }; + + struct PrepareResult { + bool accepted = false; + int slot = -1; + int expected_snapshot_len = 0; + bool reuses_victim = false; + PrefixHash victim_key{}; + int victim_slot = -1; + }; + + struct MutationResult { + bool accepted = false; + int entries_removed = 0; + }; + + FullPrefixCacheState() = default; + + FullPrefixCacheState(int slot_base, int capacity, int staging_slot) { + configure(slot_base, capacity, staging_slot); + } + + bool configure(int slot_base, int capacity, int staging_slot) { + clear(); + slot_base_ = slot_base; + capacity_ = capacity; + staging_slot_ = staging_slot; + enabled_ = slot_base >= 0 && capacity > 0 && capacity <= 64 && + slot_base <= std::numeric_limits::max() - capacity && + (staging_slot < slot_base || + staging_slot >= slot_base + capacity); + if (!enabled_) { + capacity_ = 0; + } + return enabled_; + } + + bool enabled() const { return enabled_; } + int slot_base() const { return slot_base_; } + int capacity() const { return capacity_; } + int staging_slot() const { return staging_slot_; } + int size() const { return (int)entries_.size(); } + int next_relative_slot() const { return next_relative_slot_; } + const std::vector & entries() const { return entries_; } + + bool has_pending_reservation() const { return pending_.active; } + int pending_slot() const { return pending_.active ? pending_.slot : -1; } + const PrefixHash & pending_key() const { return pending_.key; } + int pending_expected_snapshot_len() const { + return pending_.active ? pending_.expected_snapshot_len : 0; + } + bool pending_reuses_victim() const { + return pending_.active && pending_.has_victim; + } + const PrefixHash & pending_victim_key() const { + return pending_.victim_key; + } + int pending_victim_slot() const { + return pending_.has_victim ? pending_.victim_slot : -1; + } + + int find(const PrefixHash & hash) const { + for (int i = 0; i < (int)entries_.size(); ++i) { + if (prefix_hash_equal(entries_[(size_t)i].hash, hash)) return i; + } + return -1; + } + + bool contains(const PrefixHash & hash) const { return find(hash) >= 0; } + + LookupResult lookup(const PrefixHash & hash, int64_t now_ns) { + LookupResult result; + const int idx = find(hash); + if (idx < 0) return result; + + // prepare() means the backend destination is about to be cleared. + // Never advertise that victim as a usable hit while it is reserved. + if (pending_.active && entries_[(size_t)idx].slot == pending_.slot) { + return result; + } + + Entry entry = std::move(entries_[(size_t)idx]); + entries_.erase(entries_.begin() + idx); + entry.hits += 1; + entry.last_used_ns = now_ns; + result.slot = entry.slot; + result.cur_ids_len = entry.cur_ids_len; + entries_.push_back(std::move(entry)); + return result; + } + + PrepareResult prepare(const PrefixHash & hash, + int expected_snapshot_len) { + PrepareResult result; + if (!enabled_ || pending_.active || contains(hash) || + expected_snapshot_len <= 0) { + return result; + } + + int abs_slot = -1; + if ((int)entries_.size() < capacity_) { + uint64_t occupied = 0; + if (capacity_ <= 64) { + for (const auto & entry : entries_) { + const int relative = entry.slot - slot_base_; + if (relative >= 0 && relative < 64) { + occupied |= uint64_t{1} << relative; + } + } + } + const int relative = select_inline_free_slot( + next_relative_slot_, capacity_, occupied); + if (relative < 0) return result; + abs_slot = slot_base_ + relative; + next_relative_slot_ = (relative + 1) % capacity_; + } else { + if (entries_.empty()) return result; + pending_.has_victim = true; + prefix_hash_copy( + pending_.victim_key, entries_.front().hash); + pending_.victim_slot = entries_.front().slot; + abs_slot = pending_.victim_slot; + } + + if (abs_slot == staging_slot_) return result; + pending_.active = true; + prefix_hash_copy(pending_.key, hash); + pending_.slot = abs_slot; + pending_.expected_snapshot_len = expected_snapshot_len; + + result.accepted = true; + result.slot = abs_slot; + result.expected_snapshot_len = expected_snapshot_len; + result.reuses_victim = pending_.has_victim; + if (pending_.has_victim) { + prefix_hash_copy( + result.victim_key, pending_.victim_key); + } + result.victim_slot = pending_.victim_slot; + return result; + } + + MutationResult confirm(int slot, const PrefixHash & hash, + int raw_prompt_len, int cur_ids_len, + int64_t now_ns) { + MutationResult result; + // raw_prompt_len describes the lookup key, but it is not necessarily + // the effective model-input length after compression/translation. + // Only the boundary explicitly bound by prepare() is authoritative. + if (!reservation_matches(slot, hash) || raw_prompt_len <= 0 || + cur_ids_len <= 0 || + cur_ids_len > pending_.expected_snapshot_len) { + return result; + } + if (!victim_still_matches()) return result; + + result.entries_removed = erase_slot(slot); + Entry entry; + prefix_hash_copy(entry.hash, hash); + entry.slot = slot; + entry.cur_ids_len = cur_ids_len; + entry.raw_prompt_len = raw_prompt_len; + entry.last_used_ns = now_ns; + entries_.push_back(std::move(entry)); + reset_pending(); + result.accepted = true; + return result; + } + + MutationResult abort(int slot) { + MutationResult result; + if (!pending_.active || pending_.slot != slot || + !victim_still_matches()) { + return result; + } + + // The backend clears the reserved slot before attempting generation, + // so a victim at that slot is no longer restorable after an abort. + result.entries_removed = erase_slot(slot); + reset_pending(); + result.accepted = true; + return result; + } + + // A backend snapshot may disappear independently of a reservation (for + // example after OOM recovery). Keep that operation distinct from abort so + // the reservation transition itself remains strictly validated. + int invalidate_slot(int slot) { + if (!slot_in_pool(slot)) return 0; + if (pending_.active && pending_.slot == slot) reset_pending(); + return erase_slot(slot); + } + + void clear() { + entries_.clear(); + next_relative_slot_ = 0; + reset_pending(); + } + +private: + struct PendingReservation { + bool active = false; + PrefixHash key{}; + int slot = -1; + int expected_snapshot_len = 0; + bool has_victim = false; + PrefixHash victim_key{}; + int victim_slot = -1; + }; + + bool slot_in_pool(int slot) const { + return enabled_ && slot >= slot_base_ && + slot < slot_base_ + capacity_ && slot != staging_slot_; + } + + bool reservation_matches(int slot, const PrefixHash & hash) const { + return pending_.active && slot_in_pool(slot) && + pending_.slot == slot && + prefix_hash_equal(pending_.key, hash); + } + + bool victim_still_matches() const { + if (!pending_.has_victim) return true; + const int idx = find(pending_.victim_key); + return idx >= 0 && entries_[(size_t)idx].slot == pending_.victim_slot && + pending_.victim_slot == pending_.slot; + } + + int erase_slot(int slot) { + int removed = 0; + for (int i = (int)entries_.size() - 1; i >= 0; --i) { + if (entries_[(size_t)i].slot == slot) { + entries_.erase(entries_.begin() + i); + ++removed; + } + } + return removed; + } + + void reset_pending() { + // Keys are irrelevant while inactive. Reset only scalar ownership + // fields; avoiding a whole-struct std::array memcpy also keeps this + // transition tractable in bounded-verifier C++ frontends. + pending_.active = false; + pending_.slot = -1; + pending_.expected_snapshot_len = 0; + pending_.has_victim = false; + pending_.victim_slot = -1; + } + + bool enabled_ = false; + int slot_base_ = 0; + int capacity_ = 0; + int staging_slot_ = -1; + int next_relative_slot_ = 0; + std::vector entries_; + PendingReservation pending_; +}; + +} // namespace dflash::common diff --git a/server/test/test_full_prefix_cache_state.cpp b/server/test/test_full_prefix_cache_state.cpp new file mode 100644 index 000000000..ab32f4d93 --- /dev/null +++ b/server/test/test_full_prefix_cache_state.cpp @@ -0,0 +1,209 @@ +#include "server/prefix_cache_state.h" + +#include +#include +#include + +using dflash::common::FullPrefixCacheState; +using dflash::common::PrefixHash; +using dflash::common::prefix_hash_equal; + +namespace { + +PrefixHash key(uint8_t value) { + PrefixHash result{}; + result[0] = value; + return result; +} + +void assert_invariants(const FullPrefixCacheState & state) { + assert(state.size() >= 0); + assert(state.size() <= state.capacity()); + for (size_t i = 0; i < state.entries().size(); ++i) { + const auto & lhs = state.entries()[i]; + assert(lhs.slot >= state.slot_base()); + assert(lhs.slot < state.slot_base() + state.capacity()); + assert(lhs.slot != state.staging_slot()); + assert(lhs.cur_ids_len > 0); + assert(lhs.raw_prompt_len > 0); + for (size_t j = i + 1; j < state.entries().size(); ++j) { + const auto & rhs = state.entries()[j]; + assert(lhs.slot != rhs.slot); + assert(!prefix_hash_equal(lhs.hash, rhs.hash)); + } + } + if (state.has_pending_reservation()) { + assert(state.pending_slot() >= state.slot_base()); + assert(state.pending_slot() < + state.slot_base() + state.capacity()); + assert(state.pending_slot() != state.staging_slot()); + } +} + +void commit(FullPrefixCacheState & state, PrefixHash hash, + int expected_slot, int64_t now_ns) { + const auto reservation = state.prepare(hash, 12); + assert(reservation.accepted); + assert(reservation.slot == expected_slot); + assert(reservation.expected_snapshot_len == 12); + const auto confirmed = + state.confirm(reservation.slot, hash, 16, 12, now_ns); + assert(confirmed.accepted); +} + +void test_capacity_two_abort_hole_reuses_free_slot() { + FullPrefixCacheState state(8, 2, 63); + commit(state, key(1), 8, 10); + + // Allocation advances past slot 9. Aborting this free-slot reservation + // must leave slot 9 as a hole rather than returning occupied slot 8. + const auto failed = state.prepare(key(2), 12); + assert(failed.accepted); + assert(failed.slot == 9); + assert(!failed.reuses_victim); + assert(state.abort(failed.slot).accepted); + assert(state.contains(key(1))); + + const auto replacement = state.prepare(key(3), 14); + assert(replacement.accepted); + assert(replacement.slot == 9); + assert(!replacement.reuses_victim); + assert(state.confirm(replacement.slot, key(3), 20, 14, 20).accepted); + assert(state.contains(key(1))); + assert(state.contains(key(3))); + assert_invariants(state); +} + +void test_lru_lookup_selects_oldest_victim() { + FullPrefixCacheState state(12, 2, 63); + commit(state, key(1), 12, 10); + commit(state, key(2), 13, 20); + + const auto hit = state.lookup(key(1), 30); + assert(hit.slot == 12); + assert(hit.cur_ids_len == 12); + assert(state.entries().back().hits == 1); + assert(state.entries().back().last_used_ns == 30); + + const auto reservation = state.prepare(key(3), 18); + assert(reservation.accepted); + assert(reservation.reuses_victim); + assert(prefix_hash_equal(reservation.victim_key, key(2))); + assert(reservation.victim_slot == 13); + assert(reservation.slot == 13); + assert(prefix_hash_equal(state.pending_key(), key(3))); + assert(state.pending_expected_snapshot_len() == 18); + assert(prefix_hash_equal(state.pending_victim_key(), key(2))); + assert(state.pending_victim_slot() == 13); + + // A backend slot selected for replacement is not a usable cache hit. + assert(state.lookup(key(2), 40).slot == -1); + assert(state.confirm(reservation.slot, key(3), 22, 18, 40).accepted); + assert(!state.contains(key(2))); + assert(state.contains(key(1))); + assert(state.contains(key(3))); + assert_invariants(state); +} + +void test_aborted_victim_is_no_longer_committed() { + FullPrefixCacheState state(20, 1, 63); + commit(state, key(1), 20, 10); + const auto reservation = state.prepare(key(2), 12); + assert(reservation.accepted); + assert(reservation.reuses_victim); + const auto aborted = state.abort(reservation.slot); + assert(aborted.accepted); + assert(aborted.entries_removed == 1); + assert(state.size() == 0); + assert(!state.contains(key(1))); + assert_invariants(state); +} + +void test_invalid_reservations_do_not_mutate_state() { + FullPrefixCacheState state(30, 2, 63); + commit(state, key(1), 30, 10); + + assert(!state.confirm(31, key(2), 8, 8, 20).accepted); + assert(!state.prepare(key(2), 0).accepted); + const auto reservation = state.prepare(key(2), 8); + assert(reservation.accepted); + assert(reservation.slot == 31); + + assert(!state.prepare(key(3), 8).accepted); + assert(!state.confirm(30, key(2), 8, 8, 20).accepted); + assert(!state.confirm(31, key(3), 8, 8, 20).accepted); + assert(!state.confirm(31, key(2), 0, 8, 20).accepted); + assert(!state.confirm(31, key(2), 8, 0, 20).accepted); + assert(!state.confirm(31, key(2), 8, 9, 20).accepted); + assert(!state.abort(30).accepted); + assert(state.has_pending_reservation()); + assert(prefix_hash_equal(state.pending_key(), key(2))); + assert(state.pending_slot() == 31); + assert(state.contains(key(1))); + assert(state.size() == 1); + + assert(state.abort(31).accepted); + assert(!state.has_pending_reservation()); + assert(state.contains(key(1))); + assert(state.size() == 1); + assert_invariants(state); +} + +void test_slot_range_excludes_staging() { + FullPrefixCacheState overlap(62, 2, 63); + assert(!overlap.enabled()); + assert(!overlap.prepare(key(1), 8).accepted); + + FullPrefixCacheState adjacent(61, 2, 63); + assert(adjacent.enabled()); + commit(adjacent, key(1), 61, 10); + commit(adjacent, key(2), 62, 20); + assert_invariants(adjacent); + + // External invalidation is deliberately separate from reservation abort. + assert(adjacent.invalidate_slot(62) == 1); + assert(!adjacent.contains(key(2))); + assert(adjacent.invalidate_slot(63) == 0); + assert_invariants(adjacent); +} + +void test_effective_boundary_not_raw_length_is_authoritative() { + FullPrefixCacheState state(40, 1, 63); + const auto reservation = state.prepare(key(1), 10); + assert(reservation.accepted); + + // The core does not infer the effective snapshot boundary from raw input + // length. Compression/translation owns that mapping and binds it at + // prepare time. A chunk-aligned backend snapshot may validly stop before + // the bound even when its position is greater than the raw key length. + assert(state.confirm(reservation.slot, key(1), 8, 9, 10).accepted); + const auto hit = state.lookup(key(1), 20); + assert(hit.slot == 40); + assert(hit.cur_ids_len == 9); + assert_invariants(state); +} + +void test_snapshot_past_effective_boundary_is_rejected() { + FullPrefixCacheState state(42, 1, 63); + const auto reservation = state.prepare(key(1), 9); + assert(reservation.accepted); + assert(!state.confirm(reservation.slot, key(1), 20, 10, 10).accepted); + assert(state.has_pending_reservation()); + assert(state.abort(reservation.slot).accepted); + assert(!state.has_pending_reservation()); + assert(state.size() == 0); +} + +} // namespace + +int main() { + test_capacity_two_abort_hole_reuses_free_slot(); + test_lru_lookup_selects_oldest_victim(); + test_aborted_victim_is_no_longer_committed(); + test_invalid_reservations_do_not_mutate_state(); + test_slot_range_excludes_staging(); + test_effective_boundary_not_raw_length_is_authoritative(); + test_snapshot_past_effective_boundary_is_rejected(); + ::puts("full_prefix_cache_state: PASS"); + return 0; +} diff --git a/server/test/test_kvflash_residency_map.cpp b/server/test/test_kvflash_residency_map.cpp new file mode 100644 index 000000000..4c8be1fbb --- /dev/null +++ b/server/test/test_kvflash_residency_map.cpp @@ -0,0 +1,236 @@ +// Dependency-free native contract test for KVFlash ownership bookkeeping. + +#include "../src/common/kvflash_residency_map.h" + +#include +#include +#include +#include +#include + +using dflash::common::KvFlashConfig; +using dflash::common::KvFlashResidencyMap; + +static void expect(bool condition, const char * message) { + if (!condition) { + std::fprintf(stderr, "FAIL: %s\n", message); + std::exit(1); + } +} + +static KvFlashConfig small_config() { + KvFlashConfig cfg; + cfg.chunk_tokens = 4; + cfg.pool_tokens = 16; + cfg.sink_chunks = 1; + cfg.tail_window_chunks = 1; + cfg.max_logical_tokens = 32; + return cfg; +} + +static bool accept_page_out(void *, int, int) { + return true; +} + +static bool reject_page_out(void *, int, int) { + return false; +} + +static KvFlashResidencyMap::PreparePageOut accepting_page_out() { + return {nullptr, &accept_page_out}; +} + +static void test_config_validation() { + KvFlashConfig cfg = small_config(); + expect(KvFlashResidencyMap::valid_config(cfg), "valid config accepted"); + expect(KvFlashResidencyMap::min_pool_tokens(cfg) == 16, + "minimum includes sink, tail, victim, and append head"); + + cfg.chunk_tokens = 0; + expect(!KvFlashResidencyMap::valid_config(cfg), "zero chunk rejected"); + cfg = small_config(); + cfg.pool_tokens = 15; + expect(!KvFlashResidencyMap::valid_config(cfg), "partial block rejected"); + cfg = small_config(); + cfg.pool_tokens = 12; + expect(!KvFlashResidencyMap::valid_config(cfg), "deadlocking pool rejected"); + cfg = small_config(); + cfg.sink_chunks = -1; + expect(!KvFlashResidencyMap::valid_config(cfg), "negative sink rejected"); + cfg = small_config(); + cfg.tail_window_chunks = -1; + expect(!KvFlashResidencyMap::valid_config(cfg), "negative tail rejected"); + cfg = small_config(); + cfg.max_logical_tokens = 15; + expect(!KvFlashResidencyMap::valid_config(cfg), + "logical bound below resident pool rejected"); +} + +static void test_identity_bijection_and_masks() { + KvFlashResidencyMap map; + expect(map.configure(small_config()), "configure"); + expect(map.invariant_holds(), "initial free complement"); + const uint64_t initial_epoch = map.epoch(); + + for (int pos = 0; pos < 16; ++pos) { + const auto acquired = map.acquire(pos); + expect(acquired.slot == pos, "identity handout"); + expect(map.invariant_holds(), "bijection after acquire"); + } + expect(map.epoch() == initial_epoch + 4, "epoch changes once per new chunk"); + expect(map.resident_blocks() == 4, "pool full"); + expect(map.is_identity(), "full identity map"); + expect(map.identity_prefix_covers(16), "identity prefix covered"); + expect(!map.identity_prefix_covers(17), "unmaterialized prefix rejected"); + + std::vector positions(16, -2); + std::vector mask(16, 0xFFFF); + map.fill_slot_pos(positions.data()); + map.fill_slot_mask(mask.data()); + for (int i = 0; i < 16; ++i) { + expect(positions[(size_t)i] == i, "slot position reflects owner"); + expect(mask[(size_t)i] == 0, "resident slot unmasked"); + } + + const uint64_t epoch = map.epoch(); + expect(!map.acquire(-1), "negative logical position rejected"); + expect(map.slot_of(-1) == -1, "negative lookup rejected"); + expect(!map.acquire(32), "logical-context boundary rejected"); + expect(map.slot_of(32) == -1, "bounded lookup rejected"); + expect(!map.acquire( + (int64_t)(std::numeric_limits::max()) * 4 + 4), + "unrepresentable logical chunk rejected"); + expect(map.epoch() == epoch, "invalid input does not change epoch"); + expect(map.invariant_holds(), "invalid input preserves invariant"); +} + +static void test_protection_eviction_and_recall() { + KvFlashResidencyMap map; + expect(map.configure(small_config()), "configure eviction map"); + for (int chunk = 0; chunk < 4; ++chunk) { + expect(map.acquire((int64_t)chunk * 4).slot >= 0, "fill block"); + } + + struct Capture { + int chunk = -1; + int block = -1; + } capture; + const auto capture_page_out = KvFlashResidencyMap::PreparePageOut{ + &capture, + [](void * context, int chunk, int block) { + auto * captured = static_cast(context); + captured->chunk = chunk; + captured->block = block; + return true; + }}; + const auto acquired = map.acquire( + 16, {}, capture_page_out); + expect(acquired.slot >= 0, "append acquires through eviction"); + expect(capture.chunk == 1, "LRU skips sink and protected tail"); + expect(capture.block == 1, "victim block reported"); + expect(acquired.evicted_chunk == 1 && acquired.block == 1, + "ownership transfers atomically"); + expect(map.is_host_backed(1) && !map.is_resident(1), + "victim becomes host-backed"); + expect(map.block_of(0) == 0 && map.block_of(3) == 3 && + map.block_of(4) == 1, "protected mappings retained"); + expect(!map.is_identity(), "eviction ends identity layout"); + expect(map.invariant_holds(), "post-eviction bijection"); + + struct Scores { + std::vector values; + } scores{{0.0f, std::numeric_limits::infinity(), 2.0f, 0.0f, 0.0f}}; + const KvFlashResidencyMap::Score score{ + &scores, + [](const void * context, int chunk) { + const auto & values = static_cast(context)->values; + return values[(size_t)chunk]; + }}; + const std::vector wanted = map.desired_residency(score); + expect(wanted[0] && wanted[3] && wanted[4], + "reselect always includes sink and protected tail"); + expect(wanted[1] && !wanted[2], + "remaining capacity follows score after protection"); + + const auto recalled = map.acquire( + 4, {}, accepting_page_out()); + expect(recalled.slot >= 0 && recalled.recalled, "host-backed chunk recalled"); + expect(map.is_resident(1), "recalled chunk resident"); + expect(map.invariant_holds(), "recall preserves bijection"); +} + +static void test_failed_allocation_rolls_back() { + KvFlashResidencyMap map; + expect(map.configure(small_config()), "configure rollback map"); + for (int chunk = 0; chunk < 4; ++chunk) { + expect(map.acquire((int64_t)chunk * 4).slot >= 0, "fill rollback map"); + } + + const uint64_t epoch = map.epoch(); + const int chunks = map.n_chunks(); + std::vector owners; + for (int chunk = 0; chunk < chunks; ++chunk) { + owners.push_back(map.block_of(chunk)); + } + struct Count { + int calls = 0; + } count; + const auto reject_counting = KvFlashResidencyMap::PreparePageOut{ + &count, + [](void * context, int, int) { + ++static_cast(context)->calls; + return false; + }}; + const auto failed = map.acquire( + 16, {}, reject_counting); + expect(!failed, "rejected page-out fails acquire"); + expect(count.calls == 1, "victim preparation attempted once"); + expect(map.epoch() == epoch, "failed acquire preserves epoch"); + expect(map.n_chunks() == chunks, "failed acquire restores logical extent"); + for (int chunk = 0; chunk < chunks; ++chunk) { + expect(map.block_of(chunk) == owners[(size_t)chunk], + "failed acquire preserves ownership"); + } + expect(map.invariant_holds(), "failed acquire preserves free complement"); +} + +static void test_order_page_out_and_reset() { + KvFlashResidencyMap map; + expect(map.configure(small_config()), "configure ordered map"); + expect(!map.set_block_order({3, 2, 1}), "partial order rejected"); + expect(!map.set_block_order({3, 2, 2, 0}), "duplicate order rejected"); + expect(map.set_block_order({3, 1, 0, 2}), "permutation accepted"); + expect(map.acquire(0).block == 3, "custom first block"); + expect(!map.set_block_order({0, 1, 2, 3}), + "order cannot replace live ownership"); + + const uint64_t before_page_out = map.epoch(); + expect(!map.page_out(0, {nullptr, &reject_page_out}), + "failed explicit page-out rejected"); + expect(map.block_of(0) == 3 && map.epoch() == before_page_out, + "failed page-out rolls back"); + expect(map.page_out(0, accepting_page_out()), + "explicit page-out succeeds"); + expect(map.block_of(0) == -1 && map.is_host_backed(0), + "explicit page-out updates state"); + expect(map.invariant_holds(), "explicit page-out preserves complement"); + + const uint64_t before_reset = map.epoch(); + map.reset(); + expect(map.epoch() == before_reset + 1, "reset advances epoch"); + expect(map.n_chunks() == 0 && map.resident_blocks() == 0, + "reset drops request state"); + expect(map.is_identity() && map.invariant_holds(), + "reset restores empty identity invariant"); + expect(map.acquire(0).slot == 0, "reset restores identity handout order"); +} + +int main() { + test_config_validation(); + test_identity_bijection_and_masks(); + test_protection_eviction_and_recall(); + test_failed_allocation_rolls_back(); + test_order_page_out_and_reset(); + std::puts("PASS: kvflash residency map"); + return 0; +} diff --git a/server/test/test_prefix_cache_state.cpp b/server/test/test_prefix_cache_state.cpp new file mode 100644 index 000000000..8bc0c6244 --- /dev/null +++ b/server/test/test_prefix_cache_state.cpp @@ -0,0 +1,201 @@ +#include "server/prefix_cache_state.h" + +#include +#include +#include +#include + +using dflash::common::InlinePrefixCacheState; +using dflash::common::PrefixHash; +using dflash::common::prefix_hash_equal; +using dflash::common::select_inline_evict_victim; + +namespace { + +PrefixHash key(uint8_t family, uint8_t depth) { + PrefixHash result{}; + result[0] = family; + result[1] = depth; + return result; +} + +void assert_invariants(const InlinePrefixCacheState & state) { + assert(state.capacity() >= 0); + assert(state.size() >= 0); + assert(state.size() <= state.capacity()); + if (state.capacity() > 0) { + assert(state.next_slot() >= 0); + assert(state.next_slot() < state.capacity()); + } + + const auto & entries = state.entries(); + for (size_t i = 0; i < entries.size(); ++i) { + assert(entries[i].slot >= 0); + assert(entries[i].slot < state.capacity()); + assert(!entries[i].ids.empty()); + for (size_t j = i + 1; j < entries.size(); ++j) { + assert(entries[i].slot != entries[j].slot); + assert(!prefix_hash_equal(entries[i].hash, entries[j].hash)); + } + } + + if (state.has_pending_eviction()) { + assert(state.contains(state.pending_eviction_key())); + } +} + +void test_round_robin_and_reuse() { + InlinePrefixCacheState state(2); + const std::vector a = {7, 10}; + const std::vector b = {8, 20}; + const std::vector c = {9, 30}; + + auto ra = state.prepare(key(1, 2), 2); + assert(ra.slot == 0); + assert(state.confirm(ra.slot, key(1, 2), 2, a).accepted); + + auto rb = state.prepare(key(2, 2), 2); + assert(rb.slot == 1); + assert(state.confirm(rb.slot, key(2, 2), 2, b).accepted); + assert_invariants(state); + + auto rc = state.prepare(key(3, 2), 2); + assert(rc.slot == 0); + assert(rc.victim_index == 0); + auto confirmed = state.confirm(rc.slot, key(3, 2), 2, c); + assert(confirmed.accepted); + assert(confirmed.pending_removed == 1); + assert(!state.contains(key(1, 2))); + assert(state.contains(key(2, 2))); + assert(state.contains(key(3, 2))); + assert_invariants(state); +} + +void test_abort_purges_reused_slot() { + InlinePrefixCacheState state(2); + const std::vector a = {7}; + const std::vector b = {8}; + + auto ra = state.prepare(key(1, 1), 1); + assert(state.confirm(ra.slot, key(1, 1), 1, a).accepted); + auto rb = state.prepare(key(2, 1), 1); + assert(state.confirm(rb.slot, key(2, 1), 1, b).accepted); + + auto pending = state.prepare(key(3, 1), 1); + assert(pending.slot >= 0); + state.abort(pending.slot); + for (const auto & entry : state.entries()) { + assert(entry.slot != pending.slot); + } + assert(!state.has_pending_eviction()); + assert_invariants(state); +} + +void test_abort_reuses_hole_before_occupied_slot() { + InlinePrefixCacheState state(2); + const std::vector a = {7}; + + auto committed = state.prepare(key(1, 1), 1); + assert(committed.slot == 0); + assert(state.confirm( + committed.slot, key(1, 1), 1, a).accepted); + + // Reserving the second slot advances the round-robin cursor back to slot + // zero. If that reservation aborts, slot one is a hole and slot zero still + // owns a valid snapshot. + auto failed = state.prepare(key(2, 1), 1); + assert(failed.slot == 1); + assert(state.abort(failed.slot) == 0); + assert(state.contains(key(1, 1))); + + // The HTTP layer immediately frees the slot returned by prepare(). It must + // therefore receive the free slot, not the occupied slot zero. + auto replacement = state.prepare(key(3, 1), 1); + assert(replacement.slot == failed.slot); + for (const auto & entry : state.entries()) { + assert(entry.slot != replacement.slot); + } + assert(state.contains(key(1, 1))); + assert_invariants(state); +} + +void test_cancel_preserves_entry() { + InlinePrefixCacheState state(1); + const std::vector ids = {7, 10}; + auto initial = state.prepare(key(1, 2), 2); + assert(state.confirm(initial.slot, key(1, 2), 2, ids).accepted); + + auto pending = state.prepare(key(2, 2), 2); + assert(pending.slot == initial.slot); + assert(state.has_pending_eviction()); + assert(state.cancel(pending.slot)); + assert(state.contains(key(1, 2))); + assert(!state.contains(key(2, 2))); + assert(!state.has_pending_eviction()); + assert_invariants(state); +} + +void test_stale_lookup_is_removed() { + InlinePrefixCacheState state(2); + const std::vector ids = {7, 10}; + auto reservation = state.prepare(key(1, 2), 2); + assert(state.confirm( + reservation.slot, key(1, 2), 2, ids).accepted); + + const auto stale = state.lookup_candidate(key(1, 2), 1); + assert(stale.stale_removed); + assert(stale.stale_slot == reservation.slot); + assert(stale.stale_committed_len == 2); + assert(state.size() == 0); + assert_invariants(state); +} + +void test_invalid_confirm_is_non_mutating() { + InlinePrefixCacheState state(2); + const std::vector ids = {7}; + assert(!state.confirm(-1, key(1, 1), 1, ids).accepted); + assert(!state.confirm(2, key(1, 1), 1, ids).accepted); + assert(!state.confirm(0, key(1, 2), 2, ids).accepted); + assert(state.size() == 0); + assert_invariants(state); +} + +void test_prefix_aware_eviction() { + const std::vector> chain = { + {7}, {7, 10}, {7, 10, 20}, + }; + assert(select_inline_evict_victim(chain) == 2); + + const std::vector> branch = { + {7}, {7, 10}, {7, 20}, + }; + assert(select_inline_evict_victim(branch) == 1); +} + +void test_clear_resets_allocator() { + InlinePrefixCacheState state(2); + const std::vector ids = {7}; + auto reservation = state.prepare(key(1, 1), 1); + assert(state.confirm( + reservation.slot, key(1, 1), 1, ids).accepted); + state.clear(); + assert(state.size() == 0); + assert(state.next_slot() == 0); + assert(!state.has_pending_eviction()); + assert_invariants(state); +} + +} // namespace + +int main() { + test_round_robin_and_reuse(); + test_abort_purges_reused_slot(); + test_abort_reuses_hole_before_occupied_slot(); + test_cancel_preserves_entry(); + test_stale_lookup_is_removed(); + test_invalid_confirm_is_non_mutating(); + test_prefix_aware_eviction(); + test_clear_resets_allocator(); + ::puts("prefix_cache_state: PASS"); + return 0; +} diff --git a/server/test/test_spec_commit.cpp b/server/test/test_spec_commit.cpp new file mode 100644 index 000000000..d441c0833 --- /dev/null +++ b/server/test/test_spec_commit.cpp @@ -0,0 +1,124 @@ +#include "common/spec_commit.h" + +#include +#include +#include + +using dflash::common::SpecCommitDecision; + +static void test_greedy_mismatch_commits_bonus() { + const std::vector draft = {10, 11, 12, 13}; + const std::vector target = {11, 99, 13, 14}; + const auto decision = + SpecCommitDecision::greedy(draft, target, 4, 4); + + assert(decision.accepted_count() == 2); + assert(decision.valid()); + assert(decision.commit_count() == 3); + assert(decision.has_bonus()); + assert(decision.commits_bonus()); + assert(decision.bonus_token() == 99); + + int32_t token = -1; + assert(decision.token_at(0, draft, token) && token == 10); + assert(decision.token_at(1, draft, token) && token == 11); + assert(decision.token_at(2, draft, token) && token == 99); + assert(!decision.token_at(3, draft, token)); + + std::vector committed; + assert(decision.materialize(draft, committed)); + assert((committed == std::vector{10, 11, 99})); +} + +static void test_all_matches_have_no_bonus() { + const std::vector draft = {20, 21, 22}; + const std::vector target = {21, 22, 23}; + const auto decision = + SpecCommitDecision::greedy(draft, target, 3, 8); + + assert(decision.accepted_count() == 3); + assert(decision.valid()); + assert(decision.commit_count() == 3); + assert(!decision.has_bonus()); + assert(!decision.commits_bonus()); +} + +static void test_budget_clips_bonus_and_prefix() { + const auto no_bonus = + SpecCommitDecision::precomputed(3, 4, true, 77, 3); + assert(no_bonus.accepted_count() == 3); + assert(no_bonus.commit_count() == 3); + assert(no_bonus.has_bonus()); + assert(!no_bonus.commits_bonus()); + + const auto clipped_prefix = + SpecCommitDecision::precomputed(3, 4, true, 77, 2); + assert(clipped_prefix.accepted_count() == 3); + assert(clipped_prefix.commit_count() == 2); + assert(clipped_prefix.has_bonus()); + assert(!clipped_prefix.commits_bonus()); +} + +static void test_invalid_inputs_are_safe() { + const auto empty = + SpecCommitDecision::greedy(nullptr, 0, nullptr, 0, 0, 4); + assert(!empty.valid()); + assert(empty.accepted_count() == 0); + assert(empty.commit_count() == 0); + + const std::vector short_draft = {1}; + int32_t token = -1; + const auto malformed = + SpecCommitDecision::precomputed(2, 2, false, 0, 2); + assert(malformed.valid()); + assert(!malformed.token_at(1, short_draft, token)); + std::vector committed; + assert(!malformed.materialize(short_draft, committed)); + assert(committed.empty()); + + const auto no_budget = + SpecCommitDecision::precomputed(1, 2, true, 2, -1); + assert(no_budget.valid()); + assert(no_budget.commit_count() == 0); + assert(no_budget.has_bonus()); + assert(!no_budget.commits_bonus()); + + assert(!SpecCommitDecision::precomputed(0, 2, true, 2, 2).valid()); + assert(!SpecCommitDecision::precomputed(3, 2, false, 0, 2).valid()); + assert(!SpecCommitDecision::precomputed(2, 2, true, 2, 2).valid()); + const auto strict_without_bonus = + SpecCommitDecision::precomputed(1, 2, false, -1, 2); + assert(strict_without_bonus.valid()); + assert(strict_without_bonus.accepted_count() == 1); + assert(strict_without_bonus.commit_count() == 1); + assert(!strict_without_bonus.has_bonus()); + std::vector sentinel_prefix; + assert(strict_without_bonus.materialize( + std::vector{42, 43}, sentinel_prefix)); + assert((sentinel_prefix == std::vector{42})); + assert(!SpecCommitDecision::precomputed(1, 2, true, -1, 2).valid()); + + const std::vector invalid_draft = {1, -1}; + const auto invalid_token = + SpecCommitDecision::precomputed(2, 2, false, 0, 2); + assert(!invalid_token.materialize(invalid_draft, committed)); + + const std::vector mismatched_draft = {1, 2}; + const std::vector invalid_target = {-1, 0}; + const auto greedy_sentinel = + SpecCommitDecision::greedy(mismatched_draft, invalid_target, 2, 2); + assert(greedy_sentinel.valid()); + assert(greedy_sentinel.accepted_count() == 1); + assert(greedy_sentinel.commit_count() == 1); + assert(!greedy_sentinel.has_bonus()); + assert(greedy_sentinel.materialize(mismatched_draft, committed)); + assert((committed == std::vector{1})); +} + +int main() { + test_greedy_mismatch_commits_bonus(); + test_all_matches_have_no_bonus(); + test_budget_clips_bonus_and_prefix(); + test_invalid_inputs_are_safe(); + return 0; +}