formal: add local prefix-cache contract registry

.github/workflows/ci.yml

@@ -79,12 +79,15 @@ 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_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|deepseek4_unit" \
+            --no-tests=error
 
       - name: Populate venv with cu128 torch + setuptools
         # First pass: install the workspace's default deps. dflash declares

.gitignore

@@ -78,6 +78,7 @@ fix-plan.md
 
 # Harness test artifacts
 .harness-work/
+.formal-results/
 health
 
 # lucebox host-side generated config + benchmark output

formal/README.md

@@ -0,0 +1,100 @@
+# Local formal-contract pilot
+
+This directory defines two deterministic proof capsules and the local planning
+tools that select them. This change is deliberately inert at repository level:
+it adds no GitHub Actions workflow, required status check, branch-protection
+rule, credentials, or AI integration. CI integration is a separate, later
+change for maintainers to review.
+
+The capsules run against the production prefix-cache transition boundary
+introduced by the preceding prefix-cache correctness change. On a standalone
+checkout of this component branch, registry and planner checks are meaningful,
+but compiling or verifying the capsules requires that production change.
+
+## Current capsules
+
+`prefix-cache-inline` checks the production
+`InlinePrefixCacheState` prepare, confirm, and exact-lookup path for symbolic
+cache capacity, branch, and prefix depth. Its checked properties and exclusions
+are documented in
+[`prefix_cache/PROPERTIES.md`](prefix_cache/PROPERTIES.md).
+
+`prefix-cache-abort-hole` checks the scalar free-slot selector. The complete
+local plan also compiles and runs the paired native regression against the
+selected source revision, covering the production
+prepare/confirm/prepare/abort/prepare sequence. The formal and native
+guarantees are separated in
+[`prefix_cache/ABORT_HOLE_PROPERTIES.md`](prefix_cache/ABORT_HOLE_PROPERTIES.md).
+
+Only behavior named in those property documents is claimed as checked.
+
+## Policy files
+
+[`manifest.toml`](manifest.toml) is the compatibility description consumed by
+the verifier's legacy local mode.
+
+[`contracts/registry.toml`](contracts/registry.toml) records the same two
+capsules as deterministic templates, along with their source triggers, bounds,
+mutable implementation paths, immutable contract paths, and critical-path
+routing metadata. [`contracts/README.md`](contracts/README.md) describes the
+registry and planner in detail.
+
+The targets retain `policy = "required"` as their intended planner
+classification. In this PR that value is data used only by local tools: nothing
+invokes the planner automatically and it has no effect on merges. Any future
+CI change must define and review the trust boundary separately before relying
+on this metadata.
+
+## Local validation
+
+Registry and planner validation do not require Docker:
+
+```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
+```
+
+The full local verifier uses the immutable verifier image declared in the
+registry. It requires Docker and a committed checkout containing the preceding
+prefix-cache production change:
+
+```bash
+./scripts/formal.sh --all
+./scripts/formal.sh --nightly
+./scripts/formal.sh --all --legacy
+./scripts/formal_mutation_test.sh
+```
+
+`--base-sha REVISION` is available for local comparison only after that
+revision contains the registry; it is not a bootstrap command for this first
+registry change.
+
+Results are written to `.formal-results/`. Set
+`LUCEBOX_FORMAL_IMAGE` only when deliberately testing a different companion
+image.
+
+Local verifier containers run without network access or Linux capabilities,
+with a read-only repository mount and writable temporary plan/result
+directories. Immutable image digests make local runs reproducible; accepting
+the companion image's source, ownership, and release process remains an
+explicit maintainer decision before CI integration.
+
+## Adding a contract
+
+1. Extract a dependency-light production boundary; do not verify a duplicate
+   implementation.
+2. Write a deterministic template and a property document that separates
+   checked properties from exclusions.
+3. Add a deterministic native regression for integration behavior that is not
+   captured by the scalar contract.
+4. Declare exact symbols, triggers, PR/nightly bounds, mutable paths, and
+   contract paths in the registry.
+5. Keep the compatibility manifest and registry execution settings aligned.
+6. Run both bounds and demonstrate mutation sensitivity.
+
+A later CI proposal may build on these files, but it must independently review
+base-locked policy loading, exact-head verification, failure behavior,
+artifact handling, and branch-enforcement rollout. No such integration is part
+of this PR.

formal/contracts/README.md

@@ -0,0 +1,57 @@
+# Local formal-contract registry
+
+`registry.toml` is the source of truth for deterministic local selection of
+the approved minimal formal boundaries. It coexists with `../manifest.toml`,
+which preserves compatibility with the verifier's legacy local mode.
+
+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 does not generate contracts.
+
+This PR does not install a workflow or alter branch protection. The targets'
+`policy = "required"` values are planner metadata for a possible future
+integration, not repository enforcement.
+
+## Registered boundaries
+
+The registry contains two complementary prefix-cache capsules:
+
+- `prefix-cache-inline` maps to the prepare, confirm, and exact-lookup
+  harness.
+- `prefix-cache-abort-hole` checks the bounded scalar free-slot selector and
+  pairs it with the native regression for the production
+  prepare/abort/prepare integration point.
+
+Both templates call production code rather than duplicate it. The component
+depends on the production state extraction and regression from the preceding
+prefix-cache correctness PR.
+
+`[[critical_paths]]` also describes narrow state-machine areas that deserve
+review when changed without a matching target. An unmatched critical path is
+reported as an advisory coverage gap, never as verified. `watch_paths` and
+`include_roots` are routing hints only; they do not expand formal coverage.
+
+## 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
+```
+
+The `emit` command renders selected templates into an output directory and
+records their hashes. It does not invoke ESBMC or modify the manifest lane.
+
+## Boundary for a later CI change
+
+If maintainers later approve CI integration, that change must load the
+registry and selected template blobs from the accepted merge base (or an
+equivalent protected artifact), verify the exact proposed source revision, and
+record the immutable inputs in its plan. A contract-changing PR must not be
+allowed to redefine the policy used to judge itself.
+
+Those trust and enforcement mechanics are intentionally absent here. They
+belong in a separate CI/security review and rollout.

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"
+  ]
+}

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": []
+}

formal/contracts/registry.toml

@@ -0,0 +1,173 @@
+# Approved minimal-core formal contracts for local planning.
+#
+# This registry is deliberately separate from formal/manifest.toml.  The
+# latter remains the compatibility manifest for the verifier's legacy local
+# mode while the planner uses this file to select approved templates.  This PR
+# adds no CI integration or repository enforcement.
+schema_version = 1
+
+# An edit below changes the definition of formal coverage, not merely a new
+# test.  A later CI integration must load accepted policy from its merge base
+# rather than allowing a change to judge itself.
+[registry]
+description = "Approved Lucebox minimal-core contracts for deterministic local 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",
+]
+
+# Target policies are inert planner metadata in this PR.  They express the
+# intended result classification if a separately reviewed integration later
+# invokes this registry; they do not install or require a repository check.
+[[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/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/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"