test(formal): add shared lifecycle kernel pilot

[lan17]

The layers and effects profiles currently implement the same flight lifecycle separately. This PR adds a bounded shared-kernel slice so we can test the settlement design before migrating either complete profile. It advances #165; it does not close the issue.

Design

formal/kernel/cache-kernel.qnt owns calls, registered executions, raw sources, traversal and publication using sum-typed records. Thin layers/effects views supply fixtures, input choices, settlement availability and the existing observation encoding. Layers completes adapter effects within a public action; effects holds read, decode, serialization and write completions. Both use the same ownership and source-acceptance transitions.

A timeout releases the registered execution while its raw source may continue. A timely accepted source retains its execution through publication even after its original deadline. Caller completion uses captured ownership, and acquired fences remain distinct from later invalidations.

Evidence

make kernel-pilot executes twelve input-only histories in the original profiles and their kernel views, compares public observations at every step, and replays the kernel-generated histories through the unchanged TypeScript and Go drivers. Histories cover coalesced success/reuse, failure/retry, overlapping instances with different results, abandoned-source replacement, post-deadline publication, exact-deadline resolve/reject, and future-frame rejection followed by refill after a wall-clock rollback.

The tracked layers histories distinguish invalidation before acquisition (suppress serialization and writing) from invalidation after acquisition (allow the source publication, then fence a later read on another instance). A third history requires a tracked source to fill Redis, a later Redis hit to warm local storage, and a subsequent local hit. Each requires a consequential witness with negative monitor controls.

The same target requires:

• Parsed-IR thin-profile and witness-isolation checks.
• Five properties over 2,000 sampled histories of up to 40 steps per view, with per-view applicability in the report. The publication property checks retained serialization-acceptance records and effect counts after completion, so it applies to immediate layers actions. Active publication phases must also have an acceptance record. Source deadline checking is consequential only in effects; closed-scope memo checking is consequential only in layers.
• Thirteen positive/negative Quint monitor tests, based only on public inputs and observations.
• Five compiling single-site faults across seven exact-checkpoint property checks, each with a passing clean baseline. These include ignoring the recorded source fence at a completed layers checkpoint and entering publication before acceptance.
• Native assertion reports for every fixed history in both languages; missing results, skips, infrastructure failures and source drift cannot produce a complete report.

Reports retain source fingerprints, trace identities, checkpoints, native evidence and counterexamples. They separate short-history generation timings from baseline/kernel exploration measurements using the same evaluator, seed, thread count and 2,000-by-40 bounds, without unequal invariant costs. Equal sampling settings do not imply identical random inputs across different choice trees. Challenge catalog and mutation-anchor validation runs before expensive checks.

The target is included in local make formal and required by the hosted full aggregate. Documentation and reviewed guide fingerprints are updated.

Scope

This is supplemental migration evidence. All 15 existing profiles and their complete replay, witness and mutation gates remain authoritative and required. Pilot reports explicitly carry acceptance: false. Sampled pilot histories check invariants only; the twelve fixed histories are compared and replayed against implementations. No exhaustive equivalence or increased semantic coverage percentage is claimed.

The source-acceptance property checks eligibility against the recorded fence; it does not independently validate fence acquisition or the second check before write dispatch. Differential/native fence histories add separate evidence. Effects classification overrides, live read-budget changes, observer faults and other feature profiles remain outside this slice. Preserved-corpus comparison, incremental witness evaluation, independent capture checks, additional original properties, and diversity/runtime acceptance thresholds remain migration work. Timing includes CLI startup and is diagnostic. Production APIs and implementations are unchanged.

Validation

• Local Node 24.21 / Go 1.27.1: make check passed, including typecheck, 3,094 TypeScript tests with coverage, Go vet/formatting/race tests, build, packed-package smoke, docs and audits.
• make kernel-pilot passed: both bounded/lint checks, all thirteen witness controls, all twelve original/kernel comparisons and both native replays, and all seven fault checkpoints, with unchanged source fingerprints.
• Hosted sampled exploration: layers 4.60s original / 32.24s kernel (7.01x); effects 4.30s original / 39.83s kernel (9.27x). Same Rust evaluator, seed, one thread, 2,000 samples and 40 steps, with no invariant selection. These diagnostic measurements include CLI startup and confirm that full-history witness accumulation needs incremental evaluation before broader migration. The hosted kernel-pilot-evidence artifact contains the raw results and source fingerprints.
• Hosted full formal validation passed on codex/formal-kernel-pilot, including all scheduled model checks, complete TypeScript/Go replay, symbolic checks, both complete mutation reports, the supplemental pilot and the final aggregate. Optional fresh-seed exploration was not requested for this run.
• Normal CI, formal smoke and fixture regeneration, and documentation passed for the updated branch. Normal CI includes both languages' real Redis/Valkey/Cluster integrations and the Node 22.15 package floor; title and security checks also passed.

[lan17]

Verdict

Reviewed commit 07dfd4a2b32d832fa444cbde8c6f51eea21ee17f.

Mergeable as the explicitly bounded, supplemental pilot described here. I found no blocking lifecycle-correctness defect. The two findings below are assurance gaps to address before replacing either original profile, not reasons to block this additive PR. Keeping all existing profiles authoritative and marking the pilot reports acceptance: false is important.

1. Non-blocking: the publication invariant is vacuous in the layers view

Location: formal/kernel/cache-kernel.qnt, publicationHasTimelySource (lines 439–446), and the immediate-settlement chain through sourceResult, dumpResult, and writeResult.

The property examines an execution only when its phase is Serializing or Writing. In the layers view, serialization and writing complete within the same public transition. By the next committed state, the execution is already Finished, so the antecedent is false and the property does not inspect that publication, including its fence condition.

This is not evidence of an incorrect layers transition. It is a structural blind spot in the evidence: running the property over more layers histories cannot make those uncommitted intermediate phases observable. A passing result should not suggest equivalent publication assurance across the two views.

Suggested change: retain publication/dispatch receipts in committed state, containing the source identity, source-acceptance time, acquired fence, and dispatch timestamp. Check those receipts after completion, using independently reconstructed input/settlement context where appropriate. Alternatively, explicitly check the intermediate transition before collapsing it. Make per-view property applicability visible in the report until this is strengthened.

A distinguishing challenge should also demonstrate that a layers publication fault is detected after the action has settled, rather than only while an effects gate holds the execution in an intermediate phase.

2. Non-blocking: the fixed corpus does not distinguish loss of a nonzero acquired fence

Location: formal/kernel/pilot.json, fence capture in cache-kernel.qnt, and formal/kernel/challenges.json.

In the nine fixed histories, every acquired execution fence is zero. The future-frame history introduces a watermark but follows the future, unfenced-frame path; it does not establish preservation of a nonzero acquired fence.

A review-only evaluation of the saved parsed Quint IR could discard the acquired fence and retain identical public observations for all nine fixed histories. This was supplemental diagnostic evaluation, not an official Quint CLI mutation run.

There is a related independence limitation: checking publication against execution.fence does not establish that this is the fence the execution should have acquired. A capture bug can change both the transition's decision and the value against which its property checks. Kernel-facing connection monitors are explicitly deferred, so this fits the stated unfinished assurance scope.

Two small layers regressions would exercise the distinction:

A. Invalidation before acquisition

[
  ["init", 1],
  ["invalidate", 0],
  ["beginCall", 0],
  ["resolveLoader", 1]
]

With no clock advancement, the clean model returns calls: [1] with zero dumps and zero writes. Discarding the acquired fence incorrectly produces one dump and one write. This gives the mutation a public consequence rather than merely a changed private field.

B. Invalidation after acquisition

[
  ["init", 1],
  ["beginCall", 0],
  ["invalidate", 0],
  ["resolveLoader", 1],
  ["beginCall", 16]
]

Here the first execution acquired the earlier zero fence. Its write is allowed, but the subsequent other-instance read must miss against the newer watermark and start a second loader. The clean end checkpoint is calls: [1, 0], loaders: 2, dumps: 1, writes: 1.

This opposite ordering guards against an incorrect repair that substitutes the latest watermark for the captured fence. It preserves the distinction between authority acquired by an execution and invalidation observed by a later read.

Suggested change: add both input-only histories to the official old/kernel comparison and both native replays, add consequential positive/negative witness controls, and add a single-site “discard acquired fence” challenge with a clean baseline and an exact public failure checkpoint. The outcomes above come from the supplemental IR evaluation and should be confirmed through the official runner when adding the regressions.

What the extraction preserves correctly

• Registered execution versus raw source: timeout releases the registration while abandoned work can remain outstanding. Its later settlement does not complete replacement callers or publish the abandoned result.
• Acceptance versus publication: a timely accepted source retains its execution through serialization and writing after the original source deadline. The timeout is not incorrectly reapplied as a publication deadline.
• DialCache-specific local publication policy: a tracked remote-path source result does not directly warm process-local storage, while a validated remote hit can. Remote invalidation is not modeled as synchronous eviction of existing local hits.
• Comparison and challenge boundaries: exact external input histories are compared through public observations, rather than private state equality or assumed same-seed schedule equivalence. The challenge runner requires compilation, a passing clean baseline, the intended input sequence, and an invariant violation at the declared checkpoint; evaluator failures do not earn detection credit.

Validation and limits

The review included source inspection and inspection of the hosted kernel-pilot evidence, not just the PR's validation summary. The downloaded report records the nine fixed-history comparisons, both native replays, witness controls, and fault checks as passed, with acceptance: false.

Supplemental exploration used a review-only subset evaluator of the saved parsed Quint IR, calibrated against 158 hosted model checkpoints. Its acquired-fence diagnostic covered the nine fixed histories and 79 public checkpoints. This is useful review evidence, but it is not an official Quint run or independent native conformance evidence.

I did not independently rerun make kernel-pilot, full CI, or the Redis integrations; Quint was unavailable in the review environment. The pilot's sampled invariant checks are bounded simulation, not exhaustive equivalence or a refinement proof. The PR's scope language correctly maintains that distinction.

Recommendation: merge this bounded additive slice, retain the original profiles and gates, and strengthen committed-state publication checks plus acquired-fence regression/mutation coverage before using the pilot as evidence to delete an original transition.

[lan17]

Reviewed commit 07dfd4a with four independent lanes, each running Quint 0.32.0 and the official runner rather than reading alone: conformance to #165, the kernel and views, the runner and CI wiring, and an independent check of the earlier review's two findings.

Verdict

Mergeable as the bounded, supplemental pilot it claims to be, after the three small changes listed at the end. This is a genuine step-3 slice of #165 in the agreed shape: one kernel entry module with a types submodule, sum-typed records with explicit ownership, cache-rules imported, two views as qualified kernel instances with fixture, projection and settlement policy as constants, every wrapper owning the single nondet choice and calling a parameterized kernel action, no nondeterminism in the kernel. One Settlement constant expresses both the layers boundary (all effects immediate) and the effects boundary (read, load, dump and write held), which was the plan's hardest risk. The full check passed locally in 110 seconds: nine of nine histories match the original profiles at every step and replay through both unchanged drivers, ten witness controls, two bounded checks, five challenge checkpoints, acceptance: false.

The runner and gates hold

Every weakening probe was refused at the right step: a skipped TypeScript test ("Incomplete TypeScript run"), a skipped Go leaf, a byte changed in cache-kernel.qnt after generation ("Kernel pilot inputs changed during validation", status failed although all histories had passed), a changed projection (differential failure at step 10 with expected and actual observations), a semantically no-op mutant ("Compiling model fault survived"), and a view that assigns kernel state (thin-profile lint failure in four seconds; K::s' = K::s and a witness read in a guard are caught too). In CI the job has no dependency on generate, a 20-minute budget, an if: always() artifact, and the aggregate requires it. The kernel models are not scheduled in execution.json, so the 32-model check is unchanged. Source-audit and go-parity ledgers verify.

The earlier review's two findings, confirmed with the official runner

Finding 1 holds. An instrumented invariant "no execution is ever in Serializing or Writing" is never violated over 2,000 layers samples of 40 steps and is violated within 31 states in effects. A kernel mutant that drops the fence check from source acceptance passes all five layers invariants and is caught only by the effects view.

Finding 2 holds. Every acquired fence in the nine histories is zero. With fence: fence changed to fence: 0 at the source start, all nine differentials still pass. History A (invalidate, then begin, then resolve) ends clean at calls [1], zero dumps and writes, and under the mutant shows one dump and one write at step 3. History B (begin, invalidate, resolve, then a begin on the other instance) ends clean at calls [1, 0], two loaders, one dump, one write, and catches the opposite "use the latest watermark" repair at step 3. They are complementary exactly as stated.

One coupling the earlier review did not draw out. The suggested "discard acquired fence" challenge cannot be written today. checkChallenges is invariant-only, and the one relevant invariant compares against execution.fence, the very field the fault zeroes, so it passes in both views; only the differential detects the fault. The challenge therefore has to wait for committed-state publication receipts, or for a differential-based challenge mode. And A and B cannot be added as-is: validatePilot requires every history to declare and reach a witness label, and the lifecycle monitor earns nothing on either, because the mixed rule stops label accrual once a second identity appears. Adding them needs one new consequential label with positive and negative controls.

What the earlier review did not cover

A generation-scale performance regression hidden by the recorded metric. The report's per-history ratio (PR says 1.21x) comes from single-sample runs dominated by Quint CLI startup. At the pilot's own bounds, same machine, --max-samples=2000 --max-steps=40, seed 0xd1a1ca, Rust backend: dialcache-layers-conformance 3.5 s against layers-pilot 16.8 s (4.8x); dialcache-effects-conformance 2.8 s against effects-pilot 20.7 s (7.4x). A scratch kernel with history' = List() and witnesses' = Set() runs at parity (3.6 s and 2.9 s), so the whole cost is var history: List[Step] growing every step and commit refolding the entire history through Witness::reached on every step. Traces are 2.4x to 3.8x the baseline size; history is 28% of a final layers state. #165's exit criterion is a same-job old-versus-new ratio at generation scale, and the report records the kernel's 2000x40 duration but never the originals', so the number the criterion needs does not exist yet. The fix is the one #165 already permits: an incremental monitor that reads its own prior state, with the history kept out of the trace.

Preserved corpus replay is not done. The nine histories are hand-written schedules. The description's "54 additional legacy input histories matched their kernel views" has no script, catalog or artifact in the PR, so it is unverifiable and not a gate. generateHistory already replays any input list through constrainAction, so corpus replay is a data change, not new machinery.

cache-rules is partly restated. Zero means "unbounded" in the kernel (cache-kernel.qnt:138, :309) while cache-rules.qnt:29-34 says negative is the canonical unbounded budget and finite zero is already expired; sourceAcceptsAt is never called; the deadline judgment is written as raw now >= deadline at :165, :347 and :355 where the original effects profile uses deadlinePendingAt throughout.

The kernel is not yet profile-agnostic. Layers policy encodings (:87-89), grid dimensions (:42-47), slot arithmetic, a 60,000 TTL (:291) and a -1,000 rollback (:412) are constants in the kernel rather than the fixture. begin emits the effects-only disabled/local/policy_disabled event unconditionally at :243 and then drops it on the memo-hit, local-hit and no-remote paths (:245, :248, :249) while keeping it on join and remote read (:244, :254); unobservable now only because layers has diagnostics off and effects has no local layer. settleLoad, settleDump and settleWrite take no owner and require exactly one execution in that phase. Seventeen public action names are string literals inside the kernel, where #165 says the wrapper is the vocabulary.

The layers view drops eight of the original's nine invariants (capacityIsPerInstance, localMembershipMatchesLru, zeroCapacityHasNoLocalValues, absentRemoteHasNoAdapterEffects, sourceEffectsMatch, registeredSourcesArePending, callsKeepSourceOutcome, sourceOwnershipNeverCrossesKeyOrInstance), so the kernel's LRU and eviction code runs unconstrained in the sampled checks. Both fixed layers histories use fixture 0 and keys 0 and 1 only. A five-step tracked-fixture history (init 1, begin 12, resolve 1, begin 12, begin 12) passes the runner today and would pin tracked local warming.

Witness labels are mostly, not entirely, functions of public inputs and observations. The monitor's View is the kernel's publicView, not the profile's PROJECT, and includes now, which the layers driver never asserts; identityOf re-encodes the layers profile's choice-to-identity decoding inside the witness module; future-frame-refills-after-source is an exact ten-input prefix recognizer, so sampled exploration can earn it only through that one schedule. The negative controls are real for all eight labels.

Smaller items. challenges.json is validated after about 80 seconds of Quint work rather than up front; no test pins the catalog sizes (a history no challenge references can be deleted and the check still completes); fixture-scope.mjs treats formal/kernel/*.qnt as fixture inputs, so every kernel-only change forces a full fixture recompute in the PR lane although kernel files feed no committed artifact; the PR smoke lane does not run the pilot, so a break is detected only by the weekly run; the aggregate gate step name does not mention the pilot; README line 66 and the description say "five independent properties per view" without the layers qualification, and "exact-history equivalence" in SEMANTIC-COVERAGE.md should read "exact-history observation agreement".

Against the #165 exit criteria

Met: explicit public-action and settlement boundaries for both profiles; native replay through both drivers. Not met: preserved input histories from the existing corpus; diversity and sampled witness-hit distributions for the kernel views; a same-job relative runtime budget; an independent readability judgment. Guarantees 3, 4, 5 and 7 and architecture point 5 are untouched, mostly as the scope section says.

Before merge

1. State in formal/kernel/README.md, the description and the report that publicationHasTimelySource never inspects a committed layers state, and reword "equivalence" to "observation agreement".
2. Add histories A and B and a tracked-fixture layers history to pilot.json, with a consequential witness label they can earn and its positive and negative controls.
3. Record the originals' same-job 2000x40 generation time next to the kernel's in the report, so the ratio exists even before it is gated. Rerun the full check.

Next slice, in priority order

Incremental witness accumulation with the history out of the trace, then gate the runtime ratio; preserved-corpus replay for both profiles; committed-state publication receipts, which also makes a fence challenge possible; route deadline and budget judgments through cache-rules; carry the original layers invariants into the view or the kernel; sampled-hit and diversity reporting for the kernel views; the remaining effects vocabulary and fixtures.

Nothing here is a DialCache behavior defect. Everything is about what the pilot proves and how fast it can be generated, which is what a pilot is for.