Formal: converge the Quint specification on one kernel model with profile instances

[lan17]

Summary

The Quint specification should converge on one kernel library that states every portable DialCache rule exactly once, with every conformance profile written as a composition of that library over the profile's own bounded state. The goal is a formal base that covers all behavior and features of the TypeScript implementation, is easy to update when behavior changes, and keeps validating ports through the same replay corpus, drivers and mutation evidence as today. This is the third version of this issue. The first two described the kernel as a single state machine that every profile instantiates and that generates the corpus; the two-profile pilot (#171, #172) showed that shape is achievable for behavior but not for generation cost, and the review recorded in the comments below produced this version. The evidence guarantees are unchanged.

Where the specification is today

The boundary between the specification and the implementations works. Quint generates histories; the shared coordinator hands drivers fixtures and external commands and never its predictions; drivers report observations; the coordinator asserts them. Witness classification, observation validation and the mutation catalog are shared and language neutral. A port supplies a native implementation, a controlled test environment, a driver and a transport.

The boundary inside the specification does not. Behavior is defined more than once:

Model kind	Files	Lines	Role
Conformance profiles	15	6,492	Generate histories; each is a bounded re-implementation of the cache with integer encodings
Verification models	7	2,760	Readable sum-typed slices with the semantic invariants
Rule checks	1	61	Finite symbolic checks over cache-rules; the only Apalache target
Connection monitors	5	294	Check that a profile's captured records agree with cache-contract
Wire vector models	4	1,033	Deterministic transforms (keys, frames, envelopes, invalidation)
Shared libraries	5	256	cache-rules, cache-contract, observation encodings, wire text, cohort boundaries
Kernel pilot	5	1,374	One kernel of pure transitions with layers and effects views (#171, #172)

cache-rules.qnt fixed the worst duplication: 18 files import the age, expiry, deadline and fence judgments instead of restating them. But a profile still restates ownership, publication authority, request memo lifetime, flight registration and diagnostics in its own transitions; a verification model states the same rule a third time; the connection monitors reconstruct ownership and timing facts independently and check the profile against them; and witness classification lives in 25 JavaScript modules (2,276 lines) that read private trace fields to decide whether a history reached a boundary. A behavior change touches a verification model, one or more profiles, their receipt invariants, a connection monitor and a witness classifier.

What the pilot established

The pilot wrote one kernel of pure transitions and expressed the layers and effects profiles as instances of it. It settled the design risk the previous version named as the one that should stop the migration: one kernel with one settlement constant reproduces both the layers boundary (adapter completions inside the call) and the effects boundary (held gates) step for step on twelve fixed histories, both ports replay the result unchanged, and a dependency-following lint proves the views assign no kernel state and that witness state feeds no transition.

It also measured what instantiation costs, and the cost is structural. Quint records every state variable in every ITF state and has no projection flag, so a view exports the whole kernel record: 2.7 to 2.8 times the original's bytes per state, 61 to 83 percent of them the kernel state the view mostly never touches. Under the generation lane's own command (512 traces per profile) both views exhaust Node's default heap before writing a trace; with a 12 GB heap the effects view completes at 2.3 times the original's wall time, 2.75 times its bytes and 7 GB of memory. Sampling cost after the witness monitor was made incremental is 1.0 to 1.2 times the original for layers and 1.6 to 1.8 for effects with each model's own invariants, but that pairing compares nine original invariants against five kernel ones; without invariants the views cost 1.9 and 3.5 times, and the effects view's transitions alone cost about double a 200-line profile because they carry request, local and diagnostic state that profile never had. Every further feature the kernel absorbs (recovery, shadow, admission, policy) would grow the record every view exports. The pilot's own report records generation parity as unmet.

Two other results shape this version. The witness monitor written in Quint computed eleven labels at 13 to 15 microseconds per step and about 23 lines of Quint plus controls per label, against about 5 lines per label in today's JavaScript classifiers, and none of its labels were among the 410 required ones; moving 410 labels into a per-step monitor would tax every sampled step of every profile. And a review of the goal found that what a porter consumes is the coordinator protocol, the contract table, SPEC.md and the corpus, not Quint module structure: the kernel's value is single authority for maintainers and for resolving ambiguity, not a porter reading path.

What the contract is

Kernel initialization and transitions, together with explicit environment assumptions, define allowed behavior. Independent properties, exported regressions and witnesses check that behavior; they do not by themselves define every permitted execution. Progress is stated as bounded-progress obligations checked on every explored state, never as eventual completion: a completion witness establishes one successful execution, and a bounded-progress invariant establishes completion within a declared budget for every eligible call the simulation reached. Each such obligation says what makes a call eligible, when its step budget starts, which scheduling steps count, and which environment assumptions hold. A disabled caller deadline alone does not exclude a call whose source work has settled. Fixtures with intentionally unbounded source work are excluded by name. A call that becomes eligible near the end of a sampled trace may have too few remaining steps to test its budget; a passing invariant then establishes only that no eligible call exceeded its budget while incomplete. Such an obligation is reported as inconclusive because the trace ended, the inconclusive count is part of the diversity report, and it is distinct from a discharged obligation.

Target architecture: one library, composed profiles

1. A kernel library states every portable rule once. The library is a set of concern modules, each with its types and pure transitions: flights and ownership (registration, coalescing, joining, completion of owned callers), request memo and scope lifetime, local storage (insert, LRU order, capacity eviction, expiry), remote frames and watermarks (fences, tracked invalidation), deadlines and budgets (read and source), publication and refill authority, stale recovery, shadow jobs, runtime policy capture, admission, and diagnostics. cache-rules stays the judgment layer under them. Each module owns a record type for its part of the state and transitions of the form pure def f(state: T, inputs...): T or a record of results. Success is measured by whether a behavior change has one authoritative implementation, not by a line count; the exact module boundaries are fixed by the first migration slice from a concern map of the fifteen profiles.

2. Profiles compose the library over their own bounded state. A profile declares only the state its fixtures exercise (a profile without a local layer has no local storage variable), owns the nondet choice of inputs, restricts the environment, and projects its observations. Every assignment in a profile is the result of a library transition; a profile contains no rule logic of its own. The public action vocabulary the drivers are keyed on (mbt::actionTaken, mbt::nondetPicks with { choice }) is unchanged: the profile's actions remain the wrappers. Traces keep their current shape and size because the profile exports only its own state.

3. The settlement boundary is an explicit environment restriction, as before. The pilot's design stands: fine-grained effect steps in the library, and each profile states which external responses are immediately available and which remain held. Ownership, publication authority, timeout decisions and accepted values are governed by the library's transitions. Draining ready work must not silently advance deadline time, release unresolved gates, or discard observable effects. Effect ordering and clock capture happen at the internal step where the event occurs. The projection collapses auto-settled internal steps into one observation per public input and never manufactures an outcome.

4. Witnesses are labels computed from public inputs and projected observations, in the shared JavaScript evaluator. The rule is unchanged: a label may depend only on the input history and the observations the drivers assert, so credit can never depend on state no driver checks. The mechanism changes: the evaluator already classifies once per corpus, carries per-label provenance and is consumed by the Go port by hash, and it costs no sampled step and no trace bytes. Classifiers that read private trace fields today are rewritten to read inputs and public observations only, and a test enforces that they read nothing else; labels that depended on private storage state (LRU order, memo contents) are redefined around a later public probe read as their checkpoint. Each label keeps a positive regression and a distinguishing negative. The Quint witness monitor from the pilot is deleted.

5. Independent checks survive; duplicate transition logic does not. The connection monitors reconstruct source starts, settlement receipts, fence acquisition and clock capture from external inputs independently of the library's records and check the composed profiles against them, one monitor per concern. Verification models fold into module lemmas where they restate a rule the library now owns, are kept where they state a property nothing else states, and are deleted when they do neither. The rule-checks model stays as the symbolic boundary check over cache-rules.

6. Wire vector models stay separate. Key encoding, frames, envelopes and invalidation transitions are deterministic transforms and are correctly specified as vectors.

7. The implementation is the only second implementation. Drivers, the transport, the driver-facing coordinator contract, the completion gates and the trace shape are unchanged. A port is validated exactly as today: it replays the corpus, passes the witness gates, and its mutation lane shows the corpus would catch its mistakes.

8. Coverage is complete and stated. Every behavioral feature and option of the TypeScript implementation that a port must reproduce maps to contract IDs and to the profiles that exercise it, or is recorded as a wire vector or as intentionally out of scope (non-portable, such as metrics adapters). The map is produced by the first slice and maintained as a validated table; a feature without a profile is a coverage gap to close, not a footnote.

Why composition rather than instantiation

Instantiation removes every duplicated line, including the profile's state declaration and action wiring, at the price the pilot measured: every profile exports and updates every feature's state. Composition leaves that wiring in each profile (a few dozen lines of declarations and wrapper actions that call library transitions) and removes only the rules, which is where the duplication that costs maintainers lives. It keeps trace sizes, generation cost, replay cost and the trace readers unchanged, and it lets each profile migrate in place: the rewritten profile replays its own preserved corpus against the old text before the old text is deleted in the same change. That is the "not fully DRY" the owner accepted in exchange for a base that fits the lane and can be updated one module at a time.

What this is not

It is not one model whose step enables every action over every domain. The bounded profiles exist for a good reason and remain. It is not a porter reading path: porters consume the contracts, the specification prose, the coordinator and the corpus; the library is the maintainers' single authority and the place ambiguity in the prose is resolved. It is not a change to how ports are validated.

Evidence guarantees

These are unchanged from the previous version and none depends on the library.

1. Per-label witness provenance. Done (#170): every credited label records its trace identity, whether the trace is sampled or a named regression, and the public checkpoint steps; sampled and regression counts are reported separately.

2. A deterministic reproducer for each new challenge. Done for new challenges (#170); 60 existing challenges remain in a reported backlog and are backfilled as their models are touched.

3. Fault mapping by meaning. Not started. Every model challenge maps to relevant native mutation evidence in both ports, or carries a precise model-only or not-applicable explanation, in a validated many-to-many table; today 67 model challenges stand against 13 native mutants per port, a mapping backlog rather than a measure of strength.

4. Witness-to-failure linkage at the distinguishing checkpoint. Not started. The chain is contract, relevant fault, distinguishing history, failure at the observable checkpoint that establishes the consequence, joined over the provenance from guarantee 1.

5. Fault coupling as a report. Not started. Each catalog fault is injected once in the library module that owns the rule and the detecting profiles are listed; a profile that reaches the rule but does not detect the fault is a gap to investigate, not a gate.

6. Structural enforcement of the thin-profile rule and witness isolation. Done for today's shape (#170); the thin-profile rule changes with this version: a profile may assign its own state, but the assigned values must come from library transitions, and no profile definition may contain rule logic (see tooling). Witness isolation moves to the evaluator: a test that classifiers read only inputs and public observations.

7. Single-authority citations. Not started. Every contract ID cites exactly one authoritative definition in semantic-cases.json: a library module definition for behavioral contracts, or a definition in an explicitly scoped wire module for the wire contracts. Monitors and lemmas are cited as independent checks and tagged as such.

8. Corpus diversity signal. Done (#170): distinct action and observation sequences and per-label hit counts, gated against a recorded baseline.

9. Fresh-seed exploration stays in the aggregate. Done (#164).

Tooling changes

• Corpus differential. The pilot runner's history comparison becomes the migration tool: a generated scheduler replays a profile's preserved sampled histories and exported regressions through the rewritten profile in a few Quint processes and compares the driver-asserted observation at every step with the original's trace. It runs in the pull request that rewrites the profile and on later pull requests that touch the library, path filtered.
• Lint. The dependency-following lint keeps its resolved-reference walk and gains the composition rule: within a profile module, every state assignment's value must resolve to a library transition or a field of one, and no profile definition may branch on cache semantics (the walk reports any comparison or arithmetic over library record fields outside a wrapper's input choice). Its baseline over today's profiles is the migration work list.
• Deletions from the pilot. The layers and effects views, the Quint witness monitor and its controls, the frozen-monitor and generation-parity measurements, and the kernel-pilot workflow job are deleted as the first slice lands; the pilot kernel's pure transitions seed the library modules and the pilot README's measurements move into this issue's record.
• Trace readers and fixtures are unchanged. Profiles keep plain s and input variables and today's integer encodings until a profile's own change replaces them; variant encodings ({ tag, value }) are introduced only where a profile's observation schema changes with them.
• Docs. SPEC.md and PORTING.md cite library definitions as the authority behind each contract; the reading path for porters stays the contracts, the specification prose and the coordinator. Docs: language-neutral behavior pages, generated per-language references, and executed examples #166 generates behavior pages from the semantic cases and library definitions.

Sequence

1. Update this issue (this version).
2. Concern map and coverage audit: map every profile's state fields, public actions, rule logic and witness private reads onto concerns; audit the TypeScript feature surface against contracts and profiles; record the module boundaries, the profile migration order grouped by the modules they compose, and the coverage gaps. No code changes.
3. Library extraction and the first in-place rewrite: turn the pilot kernel's transitions into concern modules; rewrite the layers profile in place as a composition; replay its preserved corpus and regressions through the rewrite against the old text; delete the pilot views, the Quint monitor and the parity measurement; land the corpus differential and the composition lint. This slice fixes the module boundaries.
4. Evidence guarantees 3 and 4 in parallel with step 3, and the reproducer backlog for the profiles being rewritten.
5. Rewrite the remaining profiles in place, grouped by the modules they compose (lifecycle: effects, core, scope, independent, source-budgets, local-clock; then recovery and recovery-read; then policy, runtime-boundaries, admission, local-failure; then shadow and shadow-layers), each with the corpus differential, the composition lint clean, its verification model folded or kept by the rule above, its connection monitor retargeted, and its witness classifiers made public-only. Close coverage gaps found in step 2 as the module that owns the feature lands.
6. Guarantees 5 and 7 as the modules stabilize; SPEC.md, PORTING.md and README.md updated to cite the library; Docs: language-neutral behavior pages, generated per-language references, and executed examples #166.

Per-profile migration criteria

A profile rewrite lands only when:

• Every sampled history and every exported regression of the profile's current corpus replays through the rewritten profile with step-by-step agreement on the driver-asserted observation, in the same job. Any disagreement is resolved in the library, never by adjusting a projection or patching the rewrite to match the old text.
• The composition lint reports no rule logic in the profile.
• The profile carries every invariant it had, or a written equivalence argument per dropped one, and its fault challenges still fail at their declared steps.
• Both ports replay the regenerated corpus and the witness gates pass with the profile's baseline within tolerance.
• The profile's generation time in the same job is within 1.5 times the old text's, and its trace bytes per state within 1.2 times.
• The old text is deleted in the same change.

Risks and how to see them early

• Wiring drifts into rule logic. The composition lint is the guard; its report is reviewed on every profile pull request.
• Module boundaries are wrong. The first slice is the test: if the layers rewrite needs a transition that crosses two modules' records repeatedly, the boundary moves before a second profile is written.
• Public-only witnesses lose sampled hits. Labels redefined around a probe read may be reached less often by random sampling; the diversity baseline shows it, and a named regression pins the label until the profile's schedule is adjusted.
• A library change breaks a profile it does not exercise. The corpus differential runs on library-touching pull requests for every migrated profile.
• Stop rule. If two consecutive profile rewrites exceed 1.5 times the old text's generation time or need library changes that grow other profiles' state, the approach is re-examined here before a third.

Acceptance criteria

• A kernel library under formal/ of concern modules with sum-typed state and every portable rule stated once; cache-rules imported, not restated. Every behavioral contract ID cites one authoritative library definition in semantic-cases.json; wire contracts cite an explicitly scoped wire module.
• Every conformance profile declares only its own bounded state, owns its input choice and environment restriction, and assigns state only through library transitions; the composition lint reports no rule logic and no witness feedback in any profile.
• Every required witness label is computed by the shared evaluator from inputs and projected observations only, with a positive regression and a distinguishing negative; a test proves the classifiers read nothing else.
• Witness evidence carries per-label provenance, diversity counts and a baseline gate (done).
• Every model challenge carries a checked mapping and a deterministic reproducer or is in the reported backlog; every challenge maps to native evidence in both ports or carries a precise explanation.
• The connection monitors are library-facing, one per concern, with their challenges intact. Rule checks and the wire vector models remain.
• A validated coverage table maps every TypeScript behavioral feature and option to contract IDs and profiles, or records it as a wire vector or out of scope; no feature is unmapped.
• Bounded-progress obligations are stated with eligibility, budget start, counted steps and assumptions, hold on every explored state, and report inconclusive obligations separately.
• Full validation passes: models and regressions, both ports' replay of the complete corpus, all witness gates, both mutation catalogs, exploration on a fresh seed, at today's generation and replay budgets.

Reference points

• feat: add Quint-driven Go port with shared behavior contracts #161 introduced the profiles and the shared behavior contracts.
• test: unify Quint contracts and cross-language conformance replay #163 introduced cache-rules, cache-contract, the connection monitors and the shared replay coordinator.
• test: close the formalization review gaps, pin fragile witnesses, and parallelize the formal lanes #164 moved witness classification into the shared evaluator, typed the observation contract, made the mutation catalog per model, split model checking from generation, ran Quint concurrently, pinned ten seed-fragile witnesses and sharded the mutation lanes.
• test: add witness provenance, challenge reproducers, and a profile lint baseline (#165 step 2) #170 delivered guarantees 1, 2, 6 and 8: provenance, reproducers, the dependency-following lint with its baseline, the diversity baseline.
• test(formal): add shared lifecycle kernel pilot #171 and test(formal): advance the kernel witness monitor per step and bound the pilot's generation ratio #172 are the pilot: one kernel of pure transitions with layers and effects views, the settlement design, the incremental witness monitor, and the generation-cost measurements recorded in formal/kernel/README.md at the time.
• Docs: language-neutral behavior pages, generated per-language references, and executed examples #166 records the documentation target.
• The comments on this issue record the reviews that produced each version.

[lan17]

Thanks. Four of the five points are right and expose real gaps in the issue as written; the fifth is right but needs a measurable form. The most important correction is point 2, where the issue conflated two different failure modes. Point by point, with the amendments we intend to make.

Where the feedback is right and the issue is wrong

Point 2, independent properties. The issue says "delete the five connection monitors once no profile can drift, because instances cannot." That confuses profile drift, which instantiation removes, with kernel error, which it does not. The effects monitor reconstructs source start times and settlement receipts from the external inputs and the clock, independently of the profile's deadline and acceptedAt fields, and checks publication against that reconstruction. An instance trusts the kernel's fields, so if the kernel stamps the wrong owner or clock, no instance can notice. The monitors' obligations and their mutation challenges have to survive as independent reconstructions aimed at the kernel, one monitor per concern rather than per profile. That is a deliberate second implementation of a few timing and ownership rules and should be named as the only sanctioned duplication, kept small and input-driven.

The second half of the point is also right: bounded simulation cannot check progress. Today progress is carried by witnesses (something completed) and by the settlement contract. The issue should say the contract is invariants plus exported regressions plus reachability labels, and should state the progress obligations explicitly, for example that every begun call completes once its held gates are released.

Point 3, witness attribution. The issue says each label needs "a mutation-catalog entry or a named run that must fail to reach it." An arbitrary non-reaching run proves nothing. The current publication-authority classifier credits the label only when the history contains the subsequent public read that shows reuse, and it reads only observations every driver asserts, never model phase or private timestamps. If kernel-recorded labels are computed from private kernel state, attribution rigor goes backwards even as maintenance gets easier. Proposed rule, one step further than the feedback: labels are pure functions of the input history and the projected observation, defined in a module with no access to kernel state variables. The kernel recording is then a convenience, the label could be recomputed outside Quint, and credit can never depend on state no driver sees. Each label gets a positive regression and a distinguishing negative: a history that does everything except the consequence must not earn it. "Labels cannot influence enabled actions" becomes a structural rule: the label variable appears only on the left of assignments and in invariants.

Point 4, equivalence by preserved histories. Right, and migration step 2 was wrong as written. After the model structure changes, the same seed produces different random choices, so seed equality proves nothing. The inputs are explicit {name, choice} records, so the existing corpus can be turned into deterministic Quint runs against the new instance and observations compared per step. The boundaries named are the real design problem: the layers profile completes read and decode inside one call, the effects profile exposes reads as held gates. The kernel therefore needs fine-grained effect steps plus a per-profile settlement policy, a constant that says which effects auto-settle inside a public action and which are held for external release, with the projection collapsing auto-settled internal steps into one observation per public input. The issue mentions none of this and it is the hardest part of the kernel.

Point 5, exploration strength. Agreed. Reaching every label says nothing about combinations or depth. Keep the current trace and step budgets, measure throughput and per-label hit distributions (the diversity signal in the evidence section), and keep the cross-feature profiles. The rule that projections encode and never decide is in the issue but should be stated as a rule.

Where we would sharpen rather than accept

Point 1, success metric. Dropping the line-count target is correct; it was a proxy and it invites the wrong optimization. But "one authoritative implementation" needs something checkable or it becomes a matter of opinion in review. Two proposals: every contract ID in semantic-cases.json cites exactly one kernel definition as its authority, with monitors and lemmas tagged as independent checks rather than authorities; and a fault-coupling measurement, where each catalog fault is injected once in the kernel and every instance whose schedule reaches the behavior must detect it. If an instance does not, either its schedule never reaches the rule or it carries a private copy. Both are mechanical. Readable modules are fine and Quint supports them; "this is the file a porter reads" becomes "one entry module with focused submodules".

The pilot. Two profiles, layers plus effects, is the right first step and better than "generalize the layers profile, then re-express one profile". Layers exercises multi-instance ownership, effects exercises held asynchronous effects, and together they force the settlement-policy design early. We would add runtime to the exit criteria: generation time per profile within a stated multiple of today's, and per-label hit counts not collapsing.

Amendments we intend to make

• Replace the line-count acceptance criterion with single-authority citations and the fault-coupling check.
• Rewrite the monitor bullet: obligations and challenges survive as kernel-facing independent reconstructions.
• Rewrite the witness section: labels are pure over inputs and projected observations, with positive and distinguishing negative regressions, and never read by guards.
• Replace seed equality with preserved-history replay, and add the settlement-policy requirement to the kernel design.
• Add the two-profile pilot as step 1 with its exit criteria, and keep exploration budgets fixed during migration.
• Extend "its invariants are the contract" to invariants, regressions and labels, with progress obligations named.

Holding the edits until you have had a chance to respond.

[lan17]

Following up on the reply above: these amendments address my main architectural concerns. I support proceeding with the layers + effects pilot. I would tighten the evidence criteria below before adopting them as gates.

The strongest improvement is the proposed witness boundary: labels derived from explicit inputs and projected observations, in a module that cannot inspect private kernel state. Preserving independent ownership/timing reconstructions, replaying preserved histories, retaining exploration budgets, and using focused modules behind one entry point also make sense.

1. Make fault coupling depend on a distinguishing history.

Injecting a shared fault once and checking its effect across applicable profiles is a useful measurement. However, reaching a rule does not imply that every mutation of that rule must be detected.

For example, changing age < ttl to age <= ttl does not change a read at age zero with a positive TTL. A profile can execute the canonical freshness rule repeatedly without exercising its exclusive boundary. A fault can also change intermediate state without affecting the observed result, or be equivalent under a particular fixture. None of those outcomes establishes that the profile contains a private implementation.

I suggest a checked mapping with these elements:

Element	What it establishes
Contract and fault family	The behavioral obligation being challenged
Applicable profiles	The fixtures and bounds that can expose that fault
Distinguishing public-input history	A concrete execution on which correct and faulty behavior differ
Expected property or observation failure	The independent assertion that must detect the difference
Explicit exclusions	Why another profile cannot meaningfully exercise that fault

Missing a required distinguishing history is a coverage gap. Surviving one is an assurance gap to investigate. Detecting it is evidence for that specific obligation. This makes the coupling check useful without interpreting every survivor as proof of duplicated behavior.

Single-authority citations are also valuable: each contract should identify its authoritative definition, with independent checks classified separately. They need structural enforcement of the thin-profile rule; citations and mutation scores alone cannot establish that no private transition logic exists.

2. Map model and implementation faults by meaning, rather than matching their counts.

I agree with expanding implementation mutation coverage. The revised issue's challenge-parity requirement should support an explicit many-to-many mapping between contract/fault families, Quint challenges, and native mutations.

Several model challenges may exercise the same shared defect through different profiles. A fault in model-only receipt instrumentation may have no direct production counterpart. Conversely, a language binding may need several native mutations to challenge one portable obligation.

Each model challenge should therefore map to relevant native evidence in both ports, or carry a precise explanation of its model-only scope or non-applicability. Preserve the clean baselines and the requirement that detection comes from a relevant property/assertion failure. Compilation failures, malformed transport, and runner failures still receive no detection credit. Comparing the raw number of model challenges with native mutants is useful for finding mapping work, but is not itself a comparison of assurance strength.

3. Link witnesses to relevant failures at their distinguishing checkpoints.

The updated issue's witness-to-mutant linkage is a good direction, but a label and an arbitrary mutant failure occurring in the same trace is too weak.

A trace could demonstrate recovery at step 30 while an unrelated invalidation mutant fails at step 3. That does not establish that the recovery consequence is tested. The desired chain is:

Contract → relevant fault → distinguishing history → failure at the relevant observable checkpoint.

For each credited witness, retain the trace identity, the public checkpoints establishing its consequence, the relevant fault/contract mapping, and the assertion that detects the altered consequence. A later public read may be the checkpoint that establishes an earlier publication; attribution should preserve that causal chain rather than insist on failure at the instant a label is first emitted.

There is some new evidence plumbing here. At the currently examined #164 revision, the witness writer stores aggregate labels and corpus hashes. Per-label trace/checkpoint provenance needs to be added before this can become a join over saved artifacts.

Keep the positive and distinguishing negative controls when moving classification into Quint. A history that preserves the setup but removes the required consequence must lose the label. Generic malformed-trace, provenance, and completion-gate controls remain useful outside Quint.

One implementation clarification: an accumulating witness monitor must be allowed to read its own prior state. The structural restriction should be that witness state cannot influence cache transitions, enabled actions, scheduling, or results; requiring it to appear only on assignment left-hand sides would prohibit accumulation itself.

4. Define the contract through allowed executions, and state progress assumptions explicitly.

I would replace the proposed formulation with:

Kernel initialization and transitions, together with explicit environment assumptions, define allowed behavior. Independent properties, exported regressions, and witnesses check that behavior.

Invariants, regressions, and labels do not by themselves define all permitted executions.

Also, bounded simulation can check bounded progress on the executions it explores, such as completion within a declared number of steps or elapsed-time bound under specified inputs. It cannot prove eventual completion across all possible fair executions. Reaching a completion witness establishes one successful execution, not completion of every eligible call.

A completion obligation should say which source/adapter work must settle, which clocks must advance, and what scheduling assumptions apply. This matters for fixtures with intentionally unbounded source work or disabled caller deadlines.

5. Make the settlement policy an explicit environment restriction.

The proposed fine-grained kernel and per-profile settlement policy address the right problem. The policy may determine which external responses are immediately available and which remain held. Ownership, publication authority, timeout decisions, and accepted values remain governed by the shared kernel.

Draining ready work must not silently advance deadline time, release unresolved gates, or discard observable effects. Preserve effect ordering and clock capture at the internal step where the event actually occurs. The projection should expose the agreed public boundary and encode its observations; it must not manufacture an outcome to reproduce an old profile.

For the layers + effects pilot, I would require:

• Explicit public-action/settlement boundaries for both profiles.
• Preserved input histories replayed against old and new models, comparing observations at corresponding boundaries; any disagreement reviewed rather than hidden in a projection.
• Preserved independent properties, compiling-fault challenges, and witness attribution controls.
• Successful replay through the existing TypeScript and Go drivers.
• Unchanged initial trace/depth budgets, reported diversity and witness-hit distributions, and an agreed generation-runtime budget measured against the same baseline conditions.

That is enough to begin. The pilot should establish whether the settlement design preserves behavior and whether the modular kernel improves readability at an acceptable cost. The remaining profiles can then migrate against demonstrated criteria rather than a speculative line-count target.

[lan17]

Agreed on the direction and on most of the tightening. Point by point, with what we would adopt and where we would add to it. Nothing is applied to the issue body yet; this is to check agreement first.

1. Fault coupling needs a distinguishing history. Accepted. "Inject once, every reaching profile must detect" was too blunt: reaching a rule is not exercising its boundary, and a survivor can be an equivalent mutant under that fixture rather than a private copy. We would adopt the checked mapping as written (contract and fault family, applicable profiles, distinguishing public-input history, expected failure, explicit exclusions).

One corollary worth drawing out: challenge detection today relies on bounded random simulation reaching the boundary, which is the same seed fragility #168 just fixed for witnesses (ten required labels reached by three or fewer of about 550 sampled histories, one by a single history). A distinguishing history per challenge is a named public regression that must fail on the mutant, so detection becomes deterministic and seed-independent, using an artifact type that is already exported and replayed. We would phase it: required for new challenges, added to existing ones when they are touched, with the count of challenges lacking one reported.

On structural enforcement of the thin-profile rule: agreed that citations and mutation scores cannot establish it. quint parse exposes the module IR, so a lint can require that a profile module declares no state variable of its own and that every action is a wrapper that chooses an input and calls one kernel action. That lint is the gate; the coupling measurement becomes a report of things to investigate, not proof of duplication.

2. Map faults by meaning. Accepted. "67 model challenges against 13 native mutants" is a mapping backlog, not a comparison of assurance strength, and the issue should say so. The criterion becomes a validated many-to-many mapping: every model challenge maps to native evidence in both ports, or carries a precise model-only or not-applicable explanation. Clean baselines and the rule that only a relevant property or assertion failure earns credit are unchanged.

3. Linkage at distinguishing checkpoints. Accepted, including the gap you located: the evidence writer stores aggregate labels and corpus hashes, with no per-label trace or checkpoint provenance, so the join is not possible today and a naive one would link unrelated failures. The chain is contract, relevant fault, distinguishing history, failure at the observable checkpoint that establishes the consequence, which may be a later public read. Per-label provenance (trace identity and the public checkpoint steps) is cheap plumbing that needs no kernel, and it also yields the per-label hit counts #168 computed by hand. We would make it the first deliverable of the evidence section.

Correction accepted on witness state: an accumulating monitor must read its own prior state. The restriction is that witness state is never read by a cache transition, guard, schedule or result, and that is lintable the same way as the thin-profile rule. Positive and distinguishing-negative controls stay when classification moves into Quint; malformed-trace, provenance and completion-gate controls stay outside it.

4. Contract through allowed executions. We would adopt your formulation verbatim: kernel initialization and transitions, together with explicit environment assumptions, define allowed behavior; independent properties, exported regressions and witnesses check it. On progress, agreed that a completion witness establishes one execution. One addition: bounded simulation can still check a universally quantified bounded-progress invariant on every explored state, such as "every begun call whose gates are all released completes within K internal steps", which is stronger than a witness while remaining honest about being bounded. Fixtures with unbounded source work or disabled caller deadlines are excluded by name.

5. Settlement as an explicit environment restriction. Accepted in full, including the three prohibitions for draining (no silent deadline advance, no releasing unresolved gates, no discarding observable effects), clock capture at the internal step where the event occurs, and a projection that encodes rather than manufactures. The pilot criteria are right. One addition from this week's runs: the generation-runtime budget should be relative, measured by generating the old profile and the kernel instance in the same job and bounding the ratio, because hosted runners varied 1.8x day to day on identical work.

Sequencing. We would put per-label provenance and the distinguishing-history requirement for new challenges ahead of the pilot, so the pilot is measured against the tightened evidence rather than the current one. Neither depends on the kernel.

If this matches your reading, the issue body gets these amendments plus the earlier six (monitors survive as kernel-facing reconstructions, preserved-history replay, settlement policy as a constant, pilot as step 1, budgets fixed during migration, contract restated as above), and the pilot can start.

[lan17]

Following up on your latest reply: I think we have converged on the architecture and evidence criteria. I support updating the issue and proceeding with the agreed sequence. The remaining details fit within that design and can be resolved during implementation.

The most valuable addition is a deterministic reproducer for each new challenge. Random exploration discovers distinguishing histories; preserving those histories ensures that a known fault continues to be detected. PR #168 demonstrates why this matters: some required witnesses depended on very rare sampled histories. Requiring reproducers for new challenges, backfilling existing challenges as their models are touched, and reporting the remaining backlog is a practical approach. Each reproducer should pass against the clean baseline and fail for the intended semantic or property reason under the challenge.

I also agree with making witness provenance the first deliverable. Per-label trace and checkpoint references will let us inspect which histories establish which consequences, identify labels supported by very few cases, and assess what the pilot preserves. The same-job comparison of old and new generation is also the right way to evaluate runtime without confusing runner variation with architectural cost.

Three clarifications should carry into implementation:

1. Keep portable and model-only fault obligations explicit. A portable behavior fault should have an exported regression expressed through public inputs. A fault in model-only instrumentation can have a deterministic model-level test with its scope and the reason it has no native counterpart documented. The new reproducer requirement should preserve those agreed exceptions. Likewise, model/native fault mappings should remain many-to-many where appropriate; raw challenge counts are not a parity measure.

2. Make the structural lint follow dependencies. Inspect resolved helper calls and operator arguments so that private transitions or feedback from witness state cannot hide behind another function. Direct textual checks would not enforce the intended boundary. Witness state may maintain its own history, but it must not influence cache transitions, guards, scheduling, or results.

3. Define bounded progress precisely. Specify when a call becomes eligible, when its step budget starts, and which scheduling steps count, together with the required environment assumptions. A disabled caller deadline alone should not exclude a call whose source work has settled. The property can quantify over every eligible call in every explored state, while the evidence claim remains explicitly limited to the executions explored.

My recommended sequence is:

1. Update the issue with the agreed amendments and these clarifications.
2. Add per-label trace/checkpoint provenance and the deterministic-reproducer requirement for new challenges.
3. Run the layers + effects pilot, backfilling relevant existing challenges as those models are touched.
4. Expand the migration once the pilot meets its behavior, coverage, readability, and runtime criteria.

I would not make completion of the entire historical challenge backlog a prerequisite for the pilot. Keep that backlog visible, preserve the agreed exceptions, and let the pilot provide concrete evidence for the remaining implementation choices.

[lan17]

The body is updated to the agreed version: the contract stated through allowed executions with bounded-progress obligations defined precisely; the settlement policy as an explicit environment restriction with the three draining prohibitions; witnesses computed from inputs and projected observations with positive and distinguishing-negative controls, and monitor state that may accumulate but never feeds transitions; independent monitors retargeted at the kernel as the only sanctioned duplication; the nine evidence guarantees including per-label provenance, deterministic reproducers with the portable versus model-only distinction, mapping by meaning, checkpoint-anchored linkage, fault coupling as a report, and the dependency-following lint run on today's profiles as a baseline; preserved-history replay instead of seed equality; the two-profile pilot with its exit criteria and a relative runtime budget; and the four-step sequence with the reproducer backlog kept visible rather than gating the pilot. The previous body is preserved in the edit history.

[lan17]

I re-reviewed the updated body against our discussion. It is ready to guide the layers + effects pilot. It incorporates the substantive agreements: independent monitors survive, witnesses use public observations, challenges get deterministic reproducers, settlement assumptions are explicit, and migration starts with two profiles.

Four small clarifications remain. None requires reopening the architecture discussion.

1. Allow wire models to be authoritative. The target architecture and acceptance criteria retain wire models separately, but evidence guarantee 7 and the first acceptance criterion require every contract to cite a kernel definition. Those requirements conflict for wire contracts. Use “one authoritative Quint definition, in the kernel or an explicitly scoped wire module.” Shared rules should still be imported rather than duplicated; monitors and lemmas remain separately identified independent checks.

2. Make the lint cover the full witness-isolation boundary. The design prohibits witness state from influencing scheduling and results, but guarantee 6 specifically describes dependency roots at cache guards and assignments. Explicitly include profile init/step, input-choice domains, observation projections, and operator-constant bindings, following resolved dependencies through helpers and operator arguments. Otherwise, witness feedback could affect the explored inputs or reported results without appearing in a cache assignment.

3. Separate sampled coverage from regression coverage. Deterministic regressions now preserve rare witnesses. An aggregate witness gate can therefore remain green even when random exploration stops finding those cases. The risk section's claim that witness gates immediately expose lost corners is too strong. Record sampled versus named-regression provenance and counts in the planned evidence, and distinguish them in the diversity report. This makes reliable regression protection and exploration quality separately visible; it fits the existing provenance work rather than requiring another workstream.

4. Account for unfinished progress obligations at trace boundaries. A call can become eligible near the end of a sampled trace, leaving insufficient steps to test its completion budget. A passing invariant establishes that no observed eligible call exceeded its budget while incomplete; it does not establish completion for every eligible call reached. Either extend the execution until the obligation is discharged or its budget is exhausted, under the declared environment assumptions, or report that obligation as inconclusive because the trace ended. The extension must still respect the settlement restrictions, including no silent clock advance or release of unresolved gates.

I recommend incorporating these clarifications and proceeding with the provenance/reproducer work, followed by the pilot. The architecture now has enough concrete constraints and exit criteria for implementation to answer the remaining questions.

[lan17]

Applied all four clarifications to the body. (1) Guarantee 7 and the first acceptance criterion now read one authoritative Quint definition, in the kernel or an explicitly scoped wire module, with shared rules imported and monitors and lemmas tagged as independent checks. (2) Guarantee 6 roots the witness-isolation lint at cache guards and assignments, profile init and step, input-choice domains, observation projections and the bodies of operator constants bound at instantiation, following resolved references through helpers and operator arguments. (3) Guarantee 1 records whether each credited trace is a sampled history or a named regression and reports the two counts separately; guarantee 8 gates the sampled counts; the risk section no longer claims the aggregate gate exposes a lost corner. (4) The contract section reports an obligation left unfinished at a trace boundary as inconclusive, counts it in the diversity report, requires a minimum number of discharged obligations per profile through the same baseline, and keeps extension under the settlement restrictions as the alternative if discharged counts are too low. Next is step 2 of the sequence: per-label provenance with sampled versus regression counts, the reproducer requirement for new challenges, and the lint baseline over today's profiles.

[lan17]

The body is now the third version. What changed and why, in short:

• Target: one kernel library, composed profiles, instead of one kernel state machine that every profile instantiates and that generates the corpus. The pilot (test(formal): add shared lifecycle kernel pilot #171, test(formal): advance the kernel witness monitor per step and bound the pilot's generation ratio #172) proved the settlement design and the thin-profile lint, and measured that instantiation makes every profile export the whole kernel record: 2.7 to 2.8 times the bytes per state, heap exhaustion under the generation lane's own 512-trace command, and a sampling cost that only looked near parity because the pairing compared nine original invariants against five. Composition keeps each rule stated once in a concern module while each profile exports only its own state, so trace sizes, generation cost and the trace readers stay as they are, and each profile can be rewritten in place and checked against its own preserved corpus before the old text is deleted.
• Witnesses stay in the shared JavaScript evaluator, made public-only with a test that classifiers read nothing private. The Quint monitor from the pilot is deleted: it cost 13 to 15 microseconds per sampled step for eleven labels that were not among the 410 required ones, and the evaluator already gives the same attribution rule at no per-step cost.
• Coverage becomes an acceptance criterion: a validated table from every TypeScript behavioral feature and option to contract IDs and profiles, or to a wire vector or an explicit out-of-scope reason.
• Porting rationale narrowed: porters consume the contracts, the specification prose, the coordinator and the corpus; the library is the maintainers' single authority and where ambiguity is resolved, not a reading path.
• Sequence: concern map and coverage audit; library extraction with the layers profile rewritten in place under a corpus differential; guarantees 3 and 4 in parallel; the remaining profiles grouped by the modules they compose, each with the same per-profile criteria and a stop rule.

The evidence guarantees are unchanged; 1, 2, 6, 8 and 9 are done, 3, 4, 5 and 7 are not. The previous body is preserved in this issue's edit history.

[lan17]

Step 3 landed: the kernel library and the first composed profile (#178)

What exists now

• formal/kernel/: eight concern modules (encodings, layer_policy, request_memo, local_storage, remote_frames, flights, clock, serving), each a set of pure transitions over a row-polymorphic record type (type Scoped[r] = { memo: List[int], closed: List[bool] | r }), so a profile composes them over its own flat state with no change to its trace shape. Quint 0.32 supports row variables in aliases and across modules on the Rust backend; that settled the composition mechanism.
• formal/dialcache-layers-conformance.qnt is composed from the library (549 to 386 lines): same constants, flat state, input contract, nondet choices, guards, nine invariants and fifteen regressions; every s' is a library transition, a record literal or input decoding. The two layers fault challenges anchor on flights and request_memo and still fail at their steps.
• formal/differential.mjs (make differential, a pull-request job): both revisions' texts and manifests are read as recorded, the reference corpus replays through the candidate and the candidate corpus through the reference, every driver-asserted channel is compared per step, bytes per state may not grow beyond 1.2x, an intended change is declared by bumping differential.behaviorVersion (or the profile's schema version), an unchanged import closure is skipped, and refused inputs are named with the evaluator's diagnostic. Result for layers: 527 of 527 histories agree in both directions, wall x1.00, bytes per state x1.000.
• The composition lint replaces the thin-profile rule: assigned values may only be library transitions, wiring and input decoding; wrapper arguments and nested helpers carry taint. Its baseline is a ratchet (library transitions and counts as recorded, zero for any composing profile) checked in the PR lane and the weekly run. Migration work list (violations per profile): core 11, local-clock 11, local-failure 24, source-budgets 35, scope 39, policy 47, runtime-boundaries 58, effects 64, admission 65, independent 66, recovery 80, recovery-read 80, shadow 89, shadow-layers 98.
• The kernel modules are ordinary manifest libraries (purity check, witness inputs, fixture lock, challenge sources, case citations follow), and the validator refuses a kernel module no scheduled model imports. The pilot (instantiated kernel, views, Quint witness monitor, parity measurement, CI job) is deleted; its measurements stand in the earlier comments.

Decisions made in review (four rounds, 50 files)

• Per-caller identity (instance, key) is recorded by the flights registry next to owner and memo slot, so the ownership invariant is a registry property available to every composed profile; the request registry has one owner (flights) and scope closure goes through serving.closeScope(state, layout, context).
• The differential is two-way and declared-change aware rather than a permanent freeze; a profile the working tree no longer generates is reported, not compared (the manifest validators own whether a profile may disappear).
• The lint is a shape check: a record literal overriding a library result passes it; the differential is the behavioral evidence. This is stated in formal/kernel/README.md.

Preconditions for the next profiles

• The differential replays only profiles with an explicit-input driver descriptor in formal/replay/features.mjs. core, effects and local-clock have none today and need one before they compose; local-failure, source-budgets, scope, runtime-boundaries and the rest are ready.
• Composing serving adopts the layers encoding of every field it names. A profile with a different private layout re-encodes when it composes, and the witness classifiers that read its private fields (step 4 of this issue) move with it; the next slice measures bytes per state for that profile against the 1.2 bound before committing to the monolithic serving.begin or splitting it per concern.
• Known gaps carried forward: the layers classifiers still read private fields; a profile skipped by a declared change is not replayed informationally in that PR; --composed runs profiles sequentially (fine for one profile, to revisit as more compose); the committed witness-baseline.json layers fingerprint differs from what main's own text generates locally (pre-existing; refresh separately).