feat(formal): compose the policy profile from the kernel library

[lan17]

Summary

Step 5 of #165, slice 9B: the policy conformance profile is composed from the kernel library over the layered shape. Stacked on #184 (the seam); the base moves to main when #184 merges. The corpus differential replays the hand-written model's corpus through the composed one and back: 541 of 541 histories agree in both directions.

What changes in the library

• policy_overlay (new): the drivers' 26 overlay codes resolved against a fixture's baseline Ttls: the TTLs the reply carries and whether it coalesces (codes 10 to 19 repeat 0 to 9 with coalescing disabled); the reply's layer set is the shape's (remote only when Redis is available) and the traversal's gated turns a layer off when the reply's TTL for it is 0, the same rule runtime_policy states for runtime TTLs; a failed reply (provider fault or invalid read budget) resolves to the bypass.
• config_errors (new): the policyErrors channel as an opt-in record; a wrapper records one config_resolution error against no layer for the release whose reply failed.
• receipts (new): one record of the latest release, which caller it served, for which key, from which layer (local hit, remote hit, a started source, or none), and the local slot the release saw (value and insertion expiry), judged from the same layeredRelease judgment the traversal consumed; Receipts::release is the receipted variant of the layered release, as diagnostics wraps the request-only one. It exists because the two read invariants (a local hit respects the entry's insertion expiry, a remote hit respects the acquired freshness) cannot be restated from the post-state alone: a remote hit warms the very slot the local property would read.
• serving.layeredRelease: the layered release decision (caller, call, effective resolution, decision) stated once, as requestRelease is for the request-only shape; release consumes it and receipts reads it.

The policy profile

formal/dialcache-policy-conformance.qnt (670 -> 612 lines) assigns state only through Serving::admit, Serving::release wrapped in Receipts::record and ConfigErrors::recordConfigError, Serving::settle, Clock::advance, Clock::shiftWall, Remote::seedFrame and record updates of the overlay and the four fault switches. Its 29 regressions are verbatim in inputs and expectations, with the private expectations translated to the composed fields, and a thirtieth pins that a remote hit warms local for the reply's local TTL rather than its freshness. Eleven invariants: the two read invariants are one-step in both directions over the receipt (a local hit happened only with the local layer on, with no pending shared flight to join, over a live entry holding the caller's value, and left its insertion expiry unchanged; any other outcome with the local layer on found no live entry; a remote hit happened only with no flight to join, over a retained fresh frame, and a miss found none), a third pins that a remote hit warms local for the reply's local TTL, a fourth that a join happens only when a registered shared flight was joinable; seven are restated over library records (the gate, the process registry, the source list); eachFailedPolicyReplyHasOneDiagnostic is dropped with named carriers (the regression providerFailureReportsStablePolicyCategoryTest and the drivers' compared policyErrors channel). Deleted: the hand-written traversal and settlement, the two receipt lists, the reply list, and the private slot and frame fields.

Evidence

• node formal/differential.mjs --composed --reference=<the #184 head>: policy forward 541 of 541 and reverse 542 of 542 (512 sampled, 29 regressions, the new one candidate-only), bytes per state 3405 -> 2533 (x0.74); layers, runtime-boundaries, scope and source-budgets agree both ways at x1.00.
• Challenges: policy-inclusive-local-expiry re-anchored on local_storage.localValue and policy-inclusive-remote-freshness on remote_frames.fresh, both with reproducers that partition every profile (the freshness one gains an exported-regression reproducer and leaves the backlog); two new challenges on serving.decide: policy-hit-before-join (C13, the join-first order; observable in policy, runtime-boundaries and layers, each carried by an exported regression, two of them new: a coalescing caller joins the pending flight before reading a seeded frame in layers, and a default-sharing reply joins the registered leader over a warmed local entry in runtime-boundaries) and policy-join-ignores-coalesce (C13, the coalesce conjunct of the process join, reproducer independentCompletionKeepsRegisteredLeaderTest); all detected, as is stale-recovery-future-candidate. Regressions 415 scheduled, 248 exported.
• Composition lint: policy 47 violations -> 0 with 13 library transitions. quint test 30 of 30; the nine invariants clean at 2000 x 40 under the manifest seed; kernel fixtures 47 of 47; make audit, typecheck and the vitest pins green.
• Witnesses: the public-only policy classifier (test(formal): read the policy witnesses from inputs and public observations only #183) is untouched; its fidelity check is re-encoded to the composed layout (clocks as now and skew, the held caller, per-key local slots and frames, the process registry, and each source's captured TTLs) and ran on every one of the 541 candidate histories without a mismatch; every label count is identical to the recorded baseline, whose corpus fingerprint is the only baseline change.
• Ledgers: quint-case-audit rows re-cite the kernel definitions; go-parity mirrors them; the fixture projection for the policy smoke follows the composed fields (the smoke artifact regenerates); formal/README.md names the fifth composed profile (ledger refreshed).

Review

A report-mode review-loop round (seven lanes plus holistic) on the first version found the local read invariant weaker than the one it replaced: it could not see a remote hit served over a live local entry, so a traversal reading remote before local passed every invariant where the old model caught it in under a second. The fix commit gives the receipt the local slot the release saw and states the property in both directions; the reviewers' traversal-order and renew-on-hit mutants now fail. Also from that round: the receipted release is one library variant instead of the profile spelling the same five arguments twice; the receipt's caller is read instead of derived from the newest admission, and a started source has its own code; the invalid-read-budget diagnostic is pinned by a regression after its invariant was dropped; the asymmetric-TTL regression above; the fidelity check compares the receipt; the overlay decoder no longer restates the TTL gate the traversal owns. A second round found two more directions the old biconditional receipts had covered: a local hit was not required to happen with the local layer on, and neither hit clause forbade serving a layer past a pending shared flight for the same key (a traversal joining after reading layers passed every invariant). Both are stated now, and the hit-before-join fault is ledgered as a challenge. Also from that round: the overlay decoder reads the fixture's configured layers and remote availability instead of a literal; the release judgment carries only what the traversal consumes and the receipt reads the pre-release slot from the same state; the alias block and the string-dispatch fault setter are gone; the fidelity check compares the receipt and the owners; a third invariant pins the remote-hit warming TTL. A third round returned only low items, landed as the last commit: the join direction of the old receipts stated as an invariant with its own challenge; the hit-before-join partition corrected and carried by exported regressions instead of a scratch probe; the overlay decoder returning the shape's layer set so the traversal's TTL gate is the one statement of layer participation (as for runtime TTLs); doc residue and a stale exclusion reason fixed; fidelity probes for the receipt and the owners.