diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3cfe3e446..d2df963ab 100644 --- a/.github/workflows/ci.yml +++ b/.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 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/README.md b/formal/README.md new file mode 100644 index 000000000..3a1425145 --- /dev/null +++ b/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. diff --git a/formal/contracts/README.md b/formal/contracts/README.md new file mode 100644 index 000000000..8424d881d --- /dev/null +++ b/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. 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/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/registry.toml b/formal/contracts/registry.toml new file mode 100644 index 000000000..bac99d951 --- /dev/null +++ b/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" 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..ee41dd85b --- /dev/null +++ b/formal/contracts/templates/prefix-cache-abort-hole.cpp.in @@ -0,0 +1,38 @@ +// Generated from the approved 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-inline.cpp.in b/formal/contracts/templates/prefix-cache-inline.cpp.in new file mode 100644 index 000000000..12fe6f82d --- /dev/null +++ b/formal/contracts/templates/prefix-cache-inline.cpp.in @@ -0,0 +1,102 @@ +// Generated from the approved 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/tests/test_formal_plan.py b/formal/contracts/tests/test_formal_plan.py new file mode 100644 index 000000000..aef0f059f --- /dev/null +++ b/formal/contracts/tests/test_formal_plan.py @@ -0,0 +1,104 @@ +from __future__ import annotations + +import importlib.util +import json +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"], + ) + self.assertEqual( + [target["policy"] for target in registry["targets"]], + ["required", "required"], + ) + 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"], + ) + + 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_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"], + ) + 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["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_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), 2) + 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/manifest.toml b/formal/manifest.toml new file mode 100644 index 000000000..0af2afb6a --- /dev/null +++ b/formal/manifest.toml @@ -0,0 +1,83 @@ +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/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" diff --git a/formal/prefix_cache/ABORT_HOLE_PROPERTIES.md b/formal/prefix_cache/ABORT_HOLE_PROPERTIES.md new file mode 100644 index 000000000..555ddec91 --- /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 +baseline regression against the selected local checkout. 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 default local runs and 1–16 in +extended local 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 local verifier writes ESBMC's native, +self-contained HTML counterexample report and textual trace to the configured +results directory. diff --git a/formal/prefix_cache/PROPERTIES.md b/formal/prefix_cache/PROPERTIES.md new file mode 100644 index 000000000..b35e20abd --- /dev/null +++ b/formal/prefix_cache/PROPERTIES.md @@ -0,0 +1,33 @@ +# 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 + +Default local runs cover a symbolic fresh-cache prepare/confirm/lookup path +for capacities 1–4. Extended local 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/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/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..43088718c --- /dev/null +++ b/scripts/formal_mutation_test.sh @@ -0,0 +1,86 @@ +#!/usr/bin/env bash +set -euo pipefail + +script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +repo_root="$(cd "$script_dir/.." && pwd)" + +cd "$repo_root" +if [[ -n "$(git status --short --untracked-files=no)" ]]; then + echo "mutation sensitivity requires a committed production checkout" >&2 + exit 2 +fi + +base_sha="$(git rev-parse HEAD)" +temporary_root="$(mktemp -d)" +trap 'rm -rf -- "$temporary_root"' EXIT +mutated_repo="$temporary_root/repo" +results="$temporary_root/results" + +git clone --quiet --no-local "$repo_root" "$mutated_repo" +git -C "$mutated_repo" checkout --quiet --detach "$base_sha" +git -C "$mutated_repo" apply - <<'PATCH' +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; +PATCH +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 server/src/server/prefix_cache_state.h +git -C "$mutated_repo" commit --quiet \ + -m "test: bypass production free-slot selector" + +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 "expected counterexample exit 10, got $verification_status" >&2 + exit 1 +fi + +python3 -c ' +import json +import sys + +report = json.load(open(sys.argv[1], encoding="utf-8")) +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["prefix-cache-inline"]["status"] != "verified": + raise SystemExit("unrelated inline contract did not remain verified") +abort = results["prefix-cache-abort-hole"] +if abort["status"] != "counterexample": + raise SystemExit("abort-hole target did not reject the call-site mutation") +native = abort.get("assumptions", {}).get("native_test", {}) +if native.get("status") != "counterexample": + raise SystemExit("baseline native regression did not catch the mutation") +' "$results/report.json" + +cat "$results/summary.md" +echo "abort-hole call-site mutation sensitivity: PASS" diff --git a/scripts/formal_plan.py b/scripts/formal_plan.py new file mode 100644 index 000000000..b013336c7 --- /dev/null +++ b/scripts/formal_plan.py @@ -0,0 +1,369 @@ +#!/usr/bin/env python3 +"""Plan approved minimal-core formal contracts for a local 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. + +This script installs no CI integration. A later integration must separately +define trusted base-revision loading and exact-head verification. +""" + +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: + 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") + 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", + "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 0da29ea33..5bb2de90e 100644 --- a/server/CMakeLists.txt +++ b/server/CMakeLists.txt @@ -1163,6 +1163,18 @@ 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() + # 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 @@ -1236,6 +1248,9 @@ 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(_check_deps) add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND} --output-on-failure diff --git a/server/src/server/prefix_cache.cpp b/server/src/server/prefix_cache.cpp index 4ab20c590..0768363ab 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,18 +172,9 @@ 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::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)); +void PrefixCache::sync_inline_size() { + entries_size_count_.store( + inline_state_.size(), std::memory_order_relaxed); } int PrefixCache::find_full_entry(const PrefixHash & h) const { @@ -241,26 +201,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 +236,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,31 +284,20 @@ 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); } diff --git a/server/src/server/prefix_cache.h b/server/src/server/prefix_cache.h index 2a0515749..dd0d7b1de 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 @@ -163,17 +158,9 @@ 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 bool full_disabled_ = true; @@ -194,19 +181,18 @@ class PrefixCache { 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()`. + // Atomic mirrors of `inline_state_.size()` and `full_entries_.size()`. // The vectors themselves 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 entries_size_count_{0}; // mirrors inline_state_.size() std::atomic full_entries_size_count_{0}; // mirrors full_entries_.size() // Helpers - int find_entry(const PrefixHash & h) const; - void move_to_end(int idx); + void sync_inline_size(); int find_full_entry(const PrefixHash & h) const; void move_full_to_end(int idx); }; diff --git a/server/src/server/prefix_cache_state.h b/server/src/server/prefix_cache_state.h new file mode 100644 index 000000000..e14127565 --- /dev/null +++ b/server/src/server/prefix_cache_state.h @@ -0,0 +1,281 @@ +// 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 + +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]; +} + +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; +}; + +} // namespace dflash::common 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; +}