---
title: "fak proof: cachemeta binding-key determinism"
description: "Proof that fak's payload-free cachemeta key is a deterministic, injective fold over its binding axes, so distinct bindings never alias one entry."
---

# A3 · cachemeta

`internal/cachemeta` is the **payload-free metadata layer** for fak's reuse planes.
It lowers a reuse event — a KV prefix, an importable/signed KV manifest, a GLM-5.2 DSA
attention index, a live-engine KV-residency transfer (offload/restore/route/migrate), a
vDSO tool-result key, a recall context page, a memory view, or a provider prompt-cache
record — into a single `Entry` carrying a stable `EntryID` (digest · media-type · length ·
unit) plus the derivation, validity, security, residency, and coherence axes a hit must
match. It never holds the payload. For this module **"correct" is algebraic (regime A)**:
the identity key is a *deterministic, injective* fold over the binding axes; lowering an
event and reading it back *preserves the binding* (a matching lookup recovers a serveable
HIT / the recorded typed verdict); and *collision and eviction are well-defined* — distinct
bindings never alias to one key, a partial-match never serves the wrong entry (it yields a
typed MISS/FAULT, failing closed), and the external-invalidation cascade is a deterministic,
deduplicated set. All witnesses below ran **green natively** on this macOS node
(go1.26 darwin/arm64; the Windows/WSL machinery in the root `CLAUDE.md` does not apply here).

---

## Theorem A3.1 — the binding key is deterministic and axis-sensitive

**THEOREM.** For a fixed set of binding axes, the cache key is a deterministic function:
`ManifestBindingDigest` / `AttentionIndexBindingDigest` return the *same* hex digest on
repeat, and changing *any* covered axis changes the digest (so the key is injective on the
binding tuple).

**REGIME.** A — structural / determinism + injectivity.

**PROOF.** `ManifestBindingDigest` (`manifest.go:49`) and `AttentionIndexBindingDigest`
(`attention_index.go:58`) construct a `sha256.New()`, `writeField` each binding axis
followed by a `0x00` separator in a **fixed declared order**, and hex-encode the sum. The
only inputs are the struct fields; there is no map iteration over the digested set (layers
are ranged over an ordered slice, `attention_index.go:73`), no wall-clock, no RNG. A pure
fold over an ordered field list is by construction same-input → same-output. The `0x00`
field separator makes the fold injective on the *tuple* of fields (it rules out the
`"ab"+"c"` vs `"a"+"bc"` aliasing a naive concatenation would admit). The token digest
`DigestTokenIDs` (`cachemeta.go:645`) is the same shape over big-endian-encoded ids.

**WITNESS.**
```
go test ./internal/cachemeta/ -count=1 -timeout 120s -run \
  'TestManifestBindingDigestIsDeterministicOverBindingAxes|TestAttentionIndexDigestIncludesIndexShareLayerSet' -v
```
`TestManifestBindingDigestIsDeterministicOverBindingAxes` (`manifest_test.go:22`) asserts
`d1 == d2` on repeat **and** that `ModelID`/`Precision`/`PositionConvention` changes each
flip the digest. `TestAttentionIndexDigestIncludesIndexShareLayerSet`
(`attention_index_test.go:153`) asserts a different layer set yields a different digest.

**VERDICT.** **PROVEN** — 2026-06-20, both PASS. *Residual (honest):* the manifest key has
a direct same→same equality-on-repeat assertion; the attention-index key has only a
*sensitivity* witness (different layers → different digest). Its idempotence-on-repeat is
structurally true (pure ordered fold) and corroborated indirectly by
`TestFromAttentionIndexRecordsDSAPlaneAndIndexShareConsumers`, which recomputes
`DigestTokenIDs(tokens)` and compares it to the lowered `prefix_digest` label — but it is
not pinned by a dedicated `d1==d2` test. A one-line `AttentionIndexBindingDigest(idx) ==
AttentionIndexBindingDigest(idx)` assertion would close that last gap.

**DOS.** bound at ship.

---

## Theorem A3.2 — the kv-transfer / attention-index round-trip preserves the entry

**THEOREM.** Lowering an event into an `Entry` and reading it back preserves the binding:
`FromKVTransfer → KVTransferVerdict` recovers the recorded outcome as the correct typed
verdict (ok→HIT, fault→FAULT(`residency_fault`), missed→MISS(`restore_miss`)); and
`FromAttentionIndex`/`FromKVManifest` followed by a *matching-axis*
`AttentionIndexLookup`/`CheckResidentClaim` recovers a serveable HIT preserving plane,
handle, parents, and reason.

**REGIME.** A — round-trip / involution of the binding (not the payload; cachemeta is
payload-free by design).

**PROOF.** The round-trip is *lower* then *read-back*. For KV-transfer the carried datum is
the outcome string written to `Labels["outcome"]` (`kvtransfer.go:100`); `KVTransferVerdict`
switches on `KVTransferOutcome(e.Labels["outcome"])` (`kvtransfer.go:122`), so
`verdict(lower(t))` equals the typed form of `t.Outcome` exactly, with the default arm
mapping any unrecognized outcome to `MISS(absent)` — fail-closed. For attention-index and
manifest the binding is recovered by equality match: `AttentionIndexLookup`
(`attention_index.go:143`) and `CheckResidentClaim` (`manifest.go:92`) compare every
request/claim axis against the candidate/manifest axis and return `Hit(e)` only when all
agree; a request built from the entry's own axes therefore yields HIT, and `Hit()` sets
`Handle = e.ID` (`cachemeta.go:262`), so the recovered handle equals the lowered identity.
`ParentKV` round-trips into `Coherence.Parents` and is recovered by
`AttentionIndexReferences` (`attention_index.go:194`).

**WITNESS.**
```
go test ./internal/cachemeta/ -count=1 -timeout 120s -run \
  'TestFromKVTransferRecordsResidencyTransition|TestKVTransferRestoreFaultIsTypedNotSilent|TestKVRouteAndMigrateDirectionsSupported|TestAttentionIndexLookupRequiresPrefixDecisionAndCausality|TestAttentionIndexLookupBindsParentAndQualityBudget|TestCheckResidentClaimHitsOnVerifiedExactBinding|TestFromAttentionIndexRecordsDSAPlaneAndIndexShareConsumers' -v
```

**VERDICT.** **PROVEN** — 2026-06-20, all PASS. KV-transfer round-trips outcome + residency
tier/owner/from-tier/to-tier; the attention-index/manifest lower→lookup recovers HIT with
the correct plane (`attention_index` / `kv_artifact`), serveable handle, parents, and the
non-semantic-proof reason.

**DOS.** bound at ship.

---

## Theorem A3.3 — collision / eviction behavior is well-defined

**THEOREM.** Distinct bindings produce distinct digests (no false hit); a lookup whose axes
disagree returns a typed MISS/FAULT rather than serving the candidate (fail-closed); and the
external-invalidation cascade for a poisoned KV span is deterministic and deduplicated —
each engine object emitted at most once, referencing attention indexes invalidated with the
KV, provider telemetry excluded, empty poisoned id → no directives.

**REGIME.** A — structural (injectivity + fail-closed match + idempotent fold).

**PROOF.** Two parts. **(a) Key injectivity:** the digest folds are injective on the field
tuple (null-separated, Theorem A3.1), so two distinct bindings get distinct keys and the
package never indexes by a truncated/partial key. **(b) Match safety:** serving requires
*every* axis to match — `AttentionIndexLookup` (`attention_index.go:147`–`188`) and
`CheckResidentClaim` (`manifest.go:92`–`108`) return `Hit` only after all guards pass and
otherwise return a typed `Miss`/`Fault`, so a near-collision (some axes equal) never serves
the wrong entry; unknown/zero branches fail closed (`KVTransferVerdict` default → `Miss(absent)`,
`kvtransfer.go:129`; an unsigned manifest → `Fault(unsigned_artifact)`, `manifest.go:94`).
**Eviction determinism:** `PlanExternalInvalidations` (`external_invalidation.go:32`) gates
on `poisonedKV.Valid()`, iterates entries in slice order, and a `seen` set keyed on
`(kind,digest,mediatype,length,unit)` (`external_invalidation.go:37`) makes the output a
*set* — idempotent under duplicate inputs — while provider-plane telemetry is explicitly
skipped (`external_invalidation.go:57`) so cost-only metadata is never mistaken for an
evictable engine handle.

**WITNESS.**
```
go test ./internal/cachemeta/ -count=1 -timeout 120s -run \
  'TestAttentionIndexLookupRequiresPrefixDecisionAndCausality|TestCheckResidentClaimRefusesBindingMismatch|TestCheckResidentClaimRefusesUnsignedArtifact|TestKVTransferVerdictRefusesUnknownOutcome|TestPlanExternalInvalidationsDropsRemoteKVAndReferencingAttentionIndex|TestPlanExternalInvalidationsRejectsEmptyPoisonedKV|TestManifestBindingDigestIsDeterministicOverBindingAxes' -v
```
The lookup tests assert mismatched decision/prefix/model/parent → typed MISS, non-causal →
FAULT, incomplete candidate → FAULT, binding/length mismatch → FAULT(`manifest_mismatch`),
unsigned → FAULT(`unsigned_artifact`), unknown outcome → MISS(`absent`). The invalidation
tests assert exactly the remote KV + its referencing attention index are emitted, telemetry
dropped, and an invalid poisoned id → no directives.

**VERDICT.** **PROVEN** — 2026-06-20, all PASS.

**DOS.** bound at ship.

---

### Reproduce the whole module

```
go test ./internal/cachemeta/ -count=1 -timeout 120s
```
Ran green here (`ok github.com/anthony-chaudhary/fak/internal/cachemeta`). The dedicated
per-theorem `-run` filters above are the exact witnesses; the DOS column for each is bound
to the shipping commit at release via `dos commit-audit` / `dos verify` against the fleet
repo root.
