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

Activity

1. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
2. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
3. lan17

   added a commit that references this issue on Sep 12, 2026

   test: close the formalization review gaps, pin fragile witnesses, and…

   ...

   59bd443
4. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
5. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
6. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
7. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
8. lan17 commented on Sep 12, 2026

   

   lan17

   on Sep 12, 2026

   OwnerAuthor

   More actions

   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.
9. lan17

   added 4 commits that reference this issue on Sep 13, 2026

   test: add witness provenance, challenge reproducers, and a profile li…

   ...

   9a976ff

   test(formal): add shared lifecycle kernel pilot (#171)

   ...

   e8375ac

   test(formal): restore the scheduled model where it is rewritten and r…

   ...

   ac03fd1

   test(formal): advance the kernel witness monitor per step and bound t…

   ...

   957afa5
10. lan17 commented on Sep 16, 2026

    

    lan17

    on Sep 16, 2026

    OwnerAuthor

    More actions

    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.
11. lan17

    added a commit that references this issue on Sep 16, 2026

    feat(formal): extract the kernel library and compose the layers profi…

    ...

    a459f89
12. lan17 commented on Sep 16, 2026

    

    lan17

    on Sep 16, 2026

    OwnerAuthor

    More actions

    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).
13. 7 remaining items

    Load more
14. lan17

    added a commit that references this issue on Sep 16, 2026

    feat(formal): compose the source-budgets profile over a budgeted loca…

    ...

    575ca18
15. lan17 commented on Sep 16, 2026

    

    lan17

    on Sep 16, 2026

    OwnerAuthor

    More actions

    Progress since the slices 6 to 8 note.

    Landed

    • feat(formal): compose the runtime-boundaries profile from the kernel library #180 (slice 6b, runtime-boundaries composed) and feat(formal): compose the scope profile over a request-only projection of the traversal #181 (slice 7, scope composed over the request-only projection with diagnostics) are on main. Both went through two report-mode review rounds; the material findings were two scope invariants that had lost strength in the restatement (an empty memo row was accepted unconditionally; a registered source was no longer required to have coalesced), fixed by a bi-directional memo clause over the sources owned into a row, a one-step registration invariant, three regressions and a challenge on the scope-closure fold; and the release decision stated twice (diagnostics recomputed what the traversal computed), fixed by one requestRelease judgment both consume. The layered, request-only and diagnosed shapes are now aliases over one Traversed record.
    • The hosted witness gate had been running in its tolerance mode for the three profiles re-baselined since slice 5: the local Rust evaluator emits the ITF vars list differently from the pinned Linux build, and their corpus fingerprints had been recorded from raw local traces. The fingerprints are now taken from normalized corpora and the gate reports a matching corpus for all fourteen profiles.

    In flight

    • feat(formal): compose the source-budgets profile over a budgeted local lifecycle #182 (slice 8, source-budgets composed over a budgeted local lifecycle; deadlines module, local insertion expiry, the accepted-value gate) is on main. Two review rounds; the material finding was the deadline exemption keyed on the wrong call flag (the implementation bounds a source exactly when the invocation was initially enabled, so a disabled-context or closed-scope caller is unbounded while a failed key inside a request is bounded): Call.keyFailed replaces outside, pinned for every call shape by a kernel fixture; the local projection's source record now carries the identity it serves; local insertion expiry is pinned by an exported regression.
    • test(formal): read the policy witnesses from inputs and public observations only #183 (slice 9 witness pull request) is on main: the policy classifier reads inputs and public observations only. Three review rounds; the one material gap was that the shadow it keeps of the model's storage had nothing committed binding it to the model, closed by public cross-checks that throw on a contradicting observation and a fidelity check against the model's private predictions wherever a history carries them (re-encoded when the profile is recomposed, which is when it must speak). Old and new classifiers credit the same histories at the same checkpoints over 541 policy and 542 recovery histories. The public-only classifier rule is recorded once in the kernel README with the migration work list; the guides point at it.
    • feat(formal): stamp remote frames on the wall clock and carry TTLs and faults through the layered traversal #184 (slice 9A, the kernel seam for the policy profile) is open against main: the wall clock as now + skew, remote frames stamped on the wall clock and retained on the monotonic one with retained/fresh/readableFrame(freshMs), Ttls passed beside the resolution to every shape with a layer turned off by a zero TTL (stated once in the traversal), each source capturing the TTLs of the reply that started it so settle publishes with the source's own, Served fault switches read at the remote read, the dump and the write, a monotone watermark, and 47 kernel fixture runs pinning boundaries and faults with the two clocks apart. Three review rounds so far (watermark could lower after a rollback; write-side clock choices unpinned; the wall clock as independent state; TTLs in the layout; the settlement-TTL design record measured against the wrong variant); a fourth runs on the rebased head with the full run.
    • Slice 9B (the policy composition) is committed on a branch off feat(formal): stamp remote frames on the wall clock and carry TTLs and faults through the layered traversal #184 and under its first review round: policy_overlay (26 codes to a resolution and TTLs), config_errors, a one-record receipts variant for the two read invariants (the receipt-free restatement cannot tell a local hit from a remote hit that warmed local), the profile at 612 lines with its 29 regressions verbatim, nine invariants (one dropped with named carriers), both policy challenges re-anchored on kernel text, the witness fidelity check re-encoded to the composed layout. The policy corpus replays 541 of 541 histories both ways at x0.74 bytes per state; composition lint 47 to 0.

    Decisions taken (revisable)

    • Ttls travel as an argument beside Resolution rather than inside it (the scope and source-budgets profiles build and store Resolution literals; Quint records have no width subtyping). Layout carries no TTLs; every shape takes the reply's TTLs the same way at release, and each source record captures the two it publishes with (measured x1.13 bytes per state on layers, inside the bound), which deletes the parallel-list variant the design pass had planned.
    • The wall clock is now + skew so a profile cannot advance one clock without the other; shiftWall adjusts the skew.
    • A tracked flight whose remote read failed publishes to no layer, as the implementation does (finishRedisChain warms local on a read error only for untracked keys); pinned by a fixture.
    • Deferred: an environment-field allowance in the composition lint (so openScope need not live in request_memo); an absolute bytes-per-state budget per profile; hashing witness corpus fingerprints over states only so local reports stop saying "corpus differs".

    Next: land #184 after its round and run, then the 9B pull request; then local-failure folded into layers per the synthesis, with the open owner questions above still open.
16. lan17

    added 2 commits that reference this issue on Sep 17, 2026

    feat(formal): stamp remote frames on the wall clock and carry TTLs an…

    ...

    605c58b

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

    ...

    2302018
17. lan17 commented on Sep 17, 2026

    

    lan17

    on Sep 17, 2026

    OwnerAuthor

    More actions

    Slice 9 is on main.

    Landed since the last note

    • feat(formal): stamp remote frames on the wall clock and carry TTLs and faults through the layered traversal #184 (slice 9A, the kernel seam for the policy profile): the wall clock as now + skew so a profile cannot advance one clock without the other; remote frames stamped on the wall clock and retained on the monotonic one, served only while retained, fresh for the reply's TTL and fence-cleared; a watermark that never lowers (the implementation's invalidation takes the maximum); Ttls passed beside the resolution to every shape with a zero TTL turning a layer off, stated once in the traversal; each source capturing the TTLs of the reply that started it, so settlement publishes with the source's own; fault switches read at the remote read, the dump and the write; 47 kernel fixture runs pinning the boundaries and faults with the two clocks apart. Four review rounds.
    • feat(formal): compose the policy profile from the kernel library #185 (slice 9B, the policy profile composed): policy_overlay (the 26 codes to TTLs and coalescing), config_errors, a one-record receipts variant judged from the same release judgment the traversal consumes (the receipt-free restatement cannot tell a local hit from a remote hit that warmed local), eleven invariants including the join direction and the remote-hit warming TTL, two new challenges on the traversal order in decide each carried by exported regressions in every profile that observes the fault, the witness fidelity check re-encoded to the composed layout (receipt and owners bound). The policy corpus replays 541 of 541 and 542 of 542 histories both ways at x0.74 bytes per state; composition lint 47 to 0. Three review rounds.
    • fix(formal): restate the latest local publication in the composed source-budgets profile #186: a follow-up the independent coverage audit prompted. The composed source-budgets profile had restated its local publication invariant in an existence form that could not see a later accepted value failing to replace an earlier equal one, or a failed settlement clearing the slot; it is now bi-directional with a one-step clause at the settlement step, two challenges anchored on the kernel's local settlement and two exported regressions.

    Coverage. An independent three-lens audit over the whole range (before slice 6 to the current main) found no loss of coverage against the TypeScript and Go implementations: driver descriptors, src/ and go/ byte-identical; regressions 406 to 417 scheduled and 239 to 250 exported with none removed or renamed and every public expectation verbatim; 262 semantic cases and 435 required witness labels unchanged; challenges 67 to 72. The model-check lane traded two hand-written invariants for regression carriers (a traversal-order property in runtime-boundaries, the failed-reply diagnostic count in policy) and had three restated invariants strengthened back after review.

    Housekeeping. The composed profiles' witness corpus fingerprints are now recorded from normalized traces (the local Rust evaluator emits the ITF vars list differently from the pinned Linux build; the hosted gate had been running in tolerance mode for three profiles and now reports a matching corpus for all fourteen). Two ledgered guides still quote the old challenge count; a docs pass follows.

    Next per the synthesis above: local-failure folded into layers as a fault fixture (deletes that profile; needs the "deleted profile" outcome ratified), then local-clock (descriptor plumbing first), then the held-I/O design pass before independent. The open owner questions (bytes exceptions for recovery, admission and shadow; the deleted-profile outcome) still stand.
18. lan17 commented on Sep 18, 2026

    

    lan17

    on Sep 18, 2026

    OwnerAuthor

    More actions

    Fault mapping by meaning (evidence guarantee 3) is implemented in #188, ready for review and not merged.

    What it adds

    • Every model challenge in execution.json carries a nativeMutants entry: mapped to a native mutant that injects the same wrong behavior into both ports, or an explanation (unobservable: a port line exists but the port re-checks the condition later, so no public history distinguishes the fault; model-only: the fault rewrites model bookkeeping no port line carries). The result over 72 challenges: 62 mapped, 2 unobservable, 6 model-only, 2 in a frozen backlog (the Lua watermark cutoff, which no in-process cohort executes; the buffer limit, whose client-side lines exist in both ports but which no generated history reaches). Before this, 9 of the 34 challenged contracts had any native mutant.
    • One mutant catalog, formal/mutations.json, replaces the two paired files: 54 faults (13 before), each described once with a rationale naming the port lines it changes and a TypeScript and a Go section of exact-anchor edits. node formal/execution.mjs, make audit, the test suite and both mutation runners check that every anchor still matches the port text exactly once, so a src/ or go/ refactor that moves an anchored line fails the pull request rather than the weekly lane; the Quint generation lanes never read port text.
    • Two exported regressions pin faults only sampled histories reached (policy independentFailureKeepsSettledLocalValueTest, local-failure rejectedSourceDoesNotSeedLocalTest); both replay in both ports.
    • Measurement rules that the new mutants forced: an unhandled rejection beside failed assertions is recorded as a consequence of the fault rather than an infrastructure failure; each port's own unit suite is informational for a mutant, so a synctest panic or an unhandled rejection with no failed assertion is recorded as a crashed cohort and the shard continues, as is a mutant that does not compile; the Go runner credits the core replay's two pair assertions; MUTATION_ONLY=Mnn make mutations-ts|go measures named mutants while authoring.
    • Ground truth: both lanes ran locally over the CI corpus and the hosted full run on the final head (35348844512) is green across all sixteen shards; the generated cohort detects all 54 mutants in both ports. The lanes now run six TypeScript and ten Go shards, and a test pins how many mutants a shard may hold within its timeout on the slow runner class so catalog growth fails the pull request until the matrix grows.
    • Extensibility: adding a behavior now needs a challenge with a native mutant in both ports or an enumerated explanation, and the backlog cannot grow; AUTHORING.md carries the rules, VALIDATION.md and SEMANTIC-COVERAGE.md describe the table and no longer quote counts that go stale.

    Review. Three report rounds of seven lanes plus a holistic pass. Round one moved the anchor check onto the pull-request path, corrected a backlog rationale, and simplified the schema; round two folded the two catalogs into one file with the port-side account beside the anchors and cut the challenge texts to the model-side identity under a length ceiling, split anchor checking out of manifest validation, and added per-mutant crash records; round three was low-only. The hosted run on the round-two head exposed one nondeterministic mutant (a shared Go flight map without a common lock), fixed in the final commit.

    Decisions taken (revisable)

    • New mutants require generated and portable detection only; the thirteen original mutants keep their ordinary requirement. Requiring the unit suite's incidental detections would turn every unit-test refactor into a weekly-lane failure.
    • The two unobservable challenges keep no catalog entry: measured once, the edit survived every history in both ports, and an ungated survivor in every weekly report was noise.
    • portable stays in every required list (it is implied by generated); dropping it catalog-wide is a separate cleanup.

    Follow-ups this opened

    • An integration cohort against real Redis for the Lua cutoff challenge, and a profile input for the future buffer so the buffer-limit challenge can be mapped.
    • Formatting the core replay's pair assertions as expected/actual so the Go runner needs no message-specific branch (a go/ test-file change).
    • Witness labels for the two new regressions; a shadow-cohort fixture at the exact ramp sample; an exported cross-instance flight regression in the layers model so M20 no longer relies on sampled histories.

    Next in the strengthening order: required witnesses for the fifteen semantic cases that have exported regressions but no sampled witness, then a machine-checkable settlement contract. The owner questions above (deleted-profile outcome, bytes exceptions) still stand.
19. lan17 commented on Sep 19, 2026

    

    lan17

    on Sep 19, 2026

    OwnerAuthor

    More actions

    The two remaining coverage holes are closed on #188 (same branch as the fault map; two more commits, 2ec10a4 and 4952b77), ready for review and not merged.

    A required generated witness for every semantic case

    • Fifteen cases in semantic-cases.json had exported regressions but no required sampled witness, so nothing checked that generated histories reach them; check-go-parity listed them under withoutRequiredGeneratedWitnesses. Each now names at least one generated witness: the runtime-boundaries exact-serving and bypass clauses are narrowed to what the public observation proves, a layers tracked-local-only rule and an independent source-budget rule are new classifiers that read inputs and public observations only, and two policy labels the classifier already credited are registered. The registry grows to 440 labels; the inventory reports 240 cases with required generated witnesses and none without.
    • Two fixture recipes give the new labels committed histories with tests; the witness baseline is re-recorded for the recorded seed so the strict gate covers them.

    The settlement contract, checked

    • causally-ready-v1 was prose with one no-settle control per port. Every behavior observe now carries a settlement receipt (elapsedMs, runnable, held), and the coordinator keeps a ledger of the commands it issued per session and checks the receipt before comparing the observation: nothing runnable after one zero-time verification drain (R2); the monotonic clock at the sum of the advances plus the fixture's callback work (R3); the wall clock at the epoch plus the clock commands plus the same work (R4); exactly the loader, adapter and scope gates the schedule leaves open (R5). Core sessions carry no receipt and are held to R4 alone; the local-clock driver's process clock is unconstrained.
    • The rules read only issued commands and the driver's public counters, so a library fault that starts an extra source moves the counters, the ledger and the clock together, passes the receipt, and fails the observation comparison where the mutation lanes credit it. A missing, malformed or violated receipt fails by name without comparison markers, and both mutation runners fail a lane on one instead of counting it.
    • Both drivers compute the receipt from their own bookkeeping (Node: fake-timer drain and timer-count delta; Go: synctest.Wait and the deferred queue), both transports send it exactly when prepare names it after validating it locally, and both no-settle controls must fail every behavior-driver profile with a settlement violation, never an observation mismatch. Receipts held at every observe of every history in both ports over the CI corpus.
    • PORTING.md states rules R1 to R5, the receipt table with each port's computation, and what the coordinator still cannot check: runnable is the driver's attestation from one drain, timer delivery is checked by the next observation, core is held to the wall-clock rule alone. A third port must carry a no-settle control of its own.

    Review and ground truth. Four review rounds of seven lanes plus a holistic pass on the new commits. Round four found the snapshot-encoding defect the hosted run had already exposed and had a settlement violation under a mutant recorded against that mutant instead of stopping the lane, the ledger's per-interval attribution of held gates stated and enforced, the TypeScript transport's duplicate checks removed and a Go test shim deleted; round five had portable evidence left unmeasured with its component, the two binding fields folded into one, the independent classifier reading its budget from the profile, a driver-side diagnostic of what the verification drain found, and new controls for the independence clauses, the fixture work terms and the timer term; round six moved the violation matcher both runners use next to the texts it matches and gave the Go driver the same diagnostic; round seven was clean apart from two low items, one applied. The first hosted full run on the receipt commit failed one TypeScript mutation shard and thereby found a driver defect: under M37, which publishes a rejected source's error object into local storage, the driver's quiescence check compared a structured clone of the observation with the live one and read an unchanged Error object as runnable work. The snapshot is now the JSON text that crosses the wire; the hosted runs on that fix and on each review-round head (35402562963, 35404844418, 35407448531, 35409976443) are green on all sixteen mutation shards, both merges and both parity jobs; run 35411849865 covers the final head.

    Decisions taken (revisable)

    • The receipt is a self-attestation verified by one zero-time drain rather than executor inspection; the ports' executors expose no portable "nothing runnable" query, and the drain is what the controls already relied on.
    • A settlement violation under a mutant fails the lane instead of being recorded as a cohort state: it is a finding about that mutant's scheduling, and letting it pass as infrastructure would hide it in the weekly report.
    • Prepare-time validation of a history's own schedule (R8) is left out; the runtime check covers every replayed observe and the history validators already reject malformed schedules.

    Where the #165 guarantees stand. Fault mapping by meaning (3) and witness coverage for every case are in place; the settlement contract is machine-checked. Still open from the plan: finishing composition (10 of 15 profiles remain hand-written; held-I/O design first), single-authority kernel citations for semantic cases (7), witness-to-failure linkage (4), fault coupling (5), and connection monitors.
20. lan17 commented on Sep 19, 2026

    

    lan17

    on Sep 19, 2026

    OwnerAuthor

    More actions

    Composition resumes on #188 (same branch): the kernel seam for held remote I/O and the independent profile composed over it, ready for review and not merged.

    The seam (036c6d9, fixed up in a19e1c5). Designed once for every remaining remote profile by a four-reader, three-design, three-judge pass with a completeness critic:

    • remote_io is a variant family over the layered shape. Held reads and decodes are pending-only records; every held read registers its flight at dispatch so followers join a pending read; loader ordinals map to flights through one helper on every held start; the drivers' io channel is written by the transitions that hold each fact.
    • recovery is a consulted record: a snapshot retained at read settlement from the classifier passed there, consulted at loader failure and at the recovery decode. No profile composes a recovery transition, so recovery-read and recovery need no wrapper order.
    • deadlines is one pending-only list of due instants delivered by an instant-ordered fold instantiated inside the kernel, late arrival as one judgment, no drain at expiry; the local variants keep their history and source-budgets gains a field with no wiring change.
    • serving exposes the release judged with the remote layer unobserved, the shared prologue, completion split from the result record, warming and publication as named steps, and source authority with an explicit fence; remote_frames states the C58 rule (a visible but declined frame yields no fence), pinned by fixture runs and the TypeScript reading because no composed corpus can observe it.
    • The composition lint reports any operator a profile passes to a kernel definition, literal, named, let-bound or forwarded, so the higher-order fold cannot become a hook for rule logic.
    • Kernel fixtures: seven files, 75 runs; the held-remote fixture pins every seam, including a per-step invariant that loader ordinals track started sources.

    independent composed (37d166e). Seven library transitions and nothing else; lint zero. Three invariants verbatim, four restated one step over library records, one replaced by an equivalence carried by the connection monitor, two regressions and a fixture run. Ten regressions verbatim (three private-state patches became input schedules) plus three new exported ones. Six challenges re-anchored on kernel text with every mutant caught by its named invariant or regression; nine reproducer exclusions rewritten to state why each other profile cannot reach the fault; two challenges left the reproducer backlog. All 512 sampled histories and the regressions replay step-identically in both directions at 0.76 of the old bytes per state and 0.65 of its generation time; the witness labels credit the same histories (the classifier had been made public-only first, in 7d0cada).

    Review. Three rounds of seven lanes plus a holistic pass. The seam's round found one high item before any profile used it: a held reply that left the remote layer off started a source without a loader ordinal, so its deadline landed on index -1; fixed with one mapping helper on every held start and a fixture invariant, alongside the lint's operator rule, a challenge anchor that had drifted onto property history, dead definitions after the split and fixture pins for the C58 rule. The second round, on the composition and those fixes, was clean on correctness and reliability and had the lint judge operator arguments from the kernel's declared parameter types, the fixture checker run under Quint's own selection, and the timeout classifier pinned. The third round was clean on correctness, architecture and performance; its low items (an alias-typed or alias-applied kernel operator the lint did not see, one redundant recovery helper, and an exported regression for the unfenced refill after a failed decode) are applied as the final commit of the slice.

    Ground truth. Hosted full runs are green on the fix heads a19e1c5 (35442599999) and ff5c1dd (35446071419), the composed independent corpus included; run 35448859364 covers the final commit 0135f49. Locally at the head: every kernel module and composed profile typechecks, all six composed profiles replay their reference corpora step-identically in both directions (independent at 0.76 of the old bytes per state and 0.6 of its generation time), 7 fixture files with 78 runs, lint baseline, manifest, ledgers and locks consistent, full test suites of both ports green.

    Lane budget. With six composed profiles a kernel change replays every one in both directions, about 35 minutes on the hosted runner; the differential lane's budget is now an hour, and it needs sharding before many more profiles compose.

    Decisions taken (revisable), and questions

    • The C58 fence rule lands in the kernel's atomic path. It restates what six uncomposed profile texts already say and matches the TypeScript refill fencing, but no composed corpus can observe it; the owner should confirm it explicitly.
    • sourceSettlementsRespectOwnDeadline is dropped as a scheduled invariant in favor of the written equivalence; a new exported regression pins the loader a read expiry starts at the read's due instant.
    • Still open from the design: whether a profile may be deleted as an acceptance outcome (local-failure folded into layers as a fault fixture), and whether recovery, shadow and admission may carry a reviewed per-profile bytes bound above 1.2x; independent, recovery-read and shadow-layers need neither.

    Next. recovery-read (markers, payload classes, the retention cap in authority) over the same seam; then shadow-layers (held dumps and writes, detached sources, shadow jobs).
21. lan17 commented on Sep 20, 2026

    

    lan17

    on Sep 20, 2026

    OwnerAuthor

    More actions

    Progress 7 (PR 188, head 9d64a88): the recovery-read profile is composed, the seventh of fifteen.

    • Kernel: payloads (enveloped payload classes judged once in remote_frames::observe for both remote paths), the tracked one-hour cap in remote_frames applied by serving::authority, remote_io::begin and the latest-effect judgments, Serving::maintains and the mutation_error invalidation outcome, and with the composer, markers (marker lifetime; expiry zeroes the watermark) and compression (settlement variants reporting the decode outcome). 21 modules, 9 fixtures, 105 runs.
    • Profile: 13 library transitions, lint 0 (was 80); 8 + 5 invariants; 34 regressions (8 new, all passing on the old text); differential agrees both ways (289/289, 290/290 at the final head), bytes x1.133 under the 1.2 bound; six other composed profiles at x1.000 both ways after each kernel commit.
    • Evidence: four challenges re-anchored on kernel text with reproducers; new cap challenge mapped to M56, detected in the generated and portable cohorts of both ports; five reproducer partitions joined; backlog 57 -> 53; mapped native mutants 62 -> 63. Four review rounds (six lanes plus holistic each; round four clean with one low follow-up recorded); the one defect found was the pull-request CI's TypeScript job crossing vitest's 5 s default on the hosted runner, fixed by memoizing the manifest validator's source scans (0.4 s under coverage now).
    • Found on the way: a payload code naming no class was admitted as a recovery candidate and completed its caller with NO_VALUE (= CALL_PENDING); fixed in recovery::retain before landing. Main's Go API reshape (PR 190) invalidated 23 catalog anchors; all retargeted and compile/detection-verified in the merge commit.
    • Design decisions recorded in the kernel README: literal unsafe stamp and absence seed instead of two kernel classes; marker expiry as a time transition rather than a judgment threaded through the fence; the guarded two-wrapper any for input decoding that selects between two library transitions (replay-safe because normalizeReplayInputs overwrites mbt::actionTaken).

    Next: shadow-layers (designed: one shadow module over Serving::releaseJudged; bytes x0.93; two commits), then recovery, shadow (needs a futureBufferMs dimension on Serving::invalidate or a profile-side raise), admission, effects; the local-failure fold and the per-profile bytes knob await the owner decisions listed in progress 6.
22. lan17 commented on Sep 20, 2026

    

    lan17

    on Sep 20, 2026

    OwnerAuthor

    More actions

    Progress 8 (PR 188, head 5b4da7b): the shadow-layers profile is composed, the eighth of fifteen.

    • Kernel: serving::releaseJudged (a variant that records beside the release judges once), startDetachedSource/flights::registerDetached, deadlines over Scheduled, recovery::failure; with the composer, remote_writes (atomic release with held dump/write refills) and shadow (job registry, capacity, budgets, cohorts, captured fill authority). 23 modules, 10 fixtures, 129 runs.
    • Profile: 6 library transitions, lint 0 (was 98); 12 + 5 invariants; 25 regressions (3 new); differential 278/278 and 279/279 both ways at composition, bytes x0.929; seven other composed profiles unmoved.
    • Review (one round plus a confirmation, the new cadence): two kernel rules on unreachable paths were stated opposite to the ports (fence judged after serializing; a failed C0 read filling with zero retention) and are now stated as the ports do, pinned by fixture runs. This is the kernel doing its job before the shadow and admission profiles inherit those rules. The confirmation round was clean on correctness, tests, contracts and reliability; four low improvements (two arm merges in shadow, one shared refill-authority judgment, two connection clauses to restate over the drivers' literal code tables) are recorded in the PR for the shadow slice, which reworks the same module.
    • Bloat audit (three auditors + synthesis, recorded in the PR): the 28k-line PR diff is 60% pretty-printed generated fixtures and 14% ledger mirrors; the kernel is 2,455 lines with no dead text. A slimming wave lands next: compact fixture encoding (-182k lines), a narrower fixture lock, manifest arrays derived from the Quint text, computed count pins; then the ledger mirrors.
    • Parallel lanes: recovery (lane A) and the three small profiles local-failure, local-clock, core (lane B) are in design.

    Next: slimming wave 1, then recovery and the small profiles.
23. lan17 commented on Sep 20, 2026

    

    lan17

    on Sep 20, 2026

    OwnerAuthor

    More actions

    Progress 9 (PR 188, head 7db25ec): recovery, local-failure and local-clock are composed, the ninth, tenth and eleventh of fifteen; core stays uncomposed by decision (its drivers read private state), so three remain: shadow, admission, effects.

    • Kernel: remote_io::settleDispatched/releaseJudged/beginRead and their deadlines mirrors; diagnostics gains the held lifecycle's channel; a fractional clock, an inline local call, flights::latest, instances::construct, the policy-provider layout fact, local_faults. Kernel fixtures 12 files.

    • recovery: 9 library transitions, lint 0 (was 80); 30 regressions verbatim; 10 + 5 invariants (the monitor carries the candidate-window clause from the recovery-read follow-ups); differential 542/542 both ways; bytes x1.79 under a declared 1.85. local-failure x1.40 under 1.45, local-clock x0.63; both 100% agreement both ways.

    • Apparatus: the slimming wave landed (compact fixture encoding, minus 186k lines; derived schedules; narrower lock; per-model bytes bound; computed pins). A slice now touches the profile, the manifest's invariants and bound, mutations/semantic-cases citations, and tool-written files.

    • Decisions taken by default: per-model bytes bounds for recovery and local-failure (the shared kernel shapes have a structural floor above x1.2 on thin profiles); core stays uncomposed (its drivers read private state).

    • Parallel lanes: lane A (this branch) and lane B (a sibling branch merged in with a ledger reconciliation) ran the two slices concurrently.

    • Reviews (one round each plus the merge): recovery clean on correctness and contracts with hygiene items landed (dead kernel definitions deleted, a test budget, a citation); the small profiles had two medium items fixed before the merge (the local read fault is now a judgment argument, so it no longer switches off layer participation or sharing; a dead recipe binding deleted). Eight cross-lane exclusion cells were re-measured at the merge.

    Next: shadow, admission, effects; the second slimming wave (derive go-parity.json, fold quint-case-audit into semantic-cases).
24. lan17 commented on Sep 20, 2026

    

    lan17

    on Sep 20, 2026

    OwnerAuthor

    More actions

    Progress 10 (PR 188, head d9e6d5a): admission is composed, the twelfth of fifteen; core stays uncomposed by decision, so two remain: shadow (in progress on a lane branch) and effects.

    • Kernel: shadow gains the held lifecycle (job registry, capacity and budget limits, held settlements, busy, confirmation); remote_io::holdRead. Kernel fixtures 14 files, 166 runs.
    • admission: 6 library transitions, lint 0 (was 65); 8 regressions, 8 invariants; two challenges re-anchored on kernel text; differential 134/134 forward and 136/136 reverse; bytes x1.62 under a declared 1.65.
    • Review: one round (two lenses), one low item fixed (an invariant had dropped two count identities), re-verified clean. The merge into the PR branch had no conflicts and regenerated nothing.
    • Inventory: 233 invariants, 436 regressions, 272 exported histories.

    Next: shadow (lane branch, kernel commit then composition), effects (reusing shadow's future-buffer invalidation signature), then the audit follow-ups (pins manifest, the last go-parity mirrors, connection-model merges).
25. lan17 commented on Sep 20, 2026

    

    lan17

    on Sep 20, 2026

    OwnerAuthor

    More actions

    Progress 11 (PR 188, head f6ced95): shadow is composed, the thirteenth of fifteen; effects is in flight (its kernel commit runs on a third lane), and core stays uncomposed by decision.

    • Kernel: the shadow job's reads and decodes are held remote I/O records; payload forms spelled once; invalidate(state, entity, bufferMs); pending-only job registry (shadow-layers bytes x0.90, admission x0.96). The kernel verify found and fixed a gap no old text reached: a caller's source deadline now ends a waiting dark job. Fixtures 15 files, 170 runs.
    • shadow: 15 library transitions, lint 0; 39 regressions (32 newly exported), 13 invariants; the shadow validation model retired, its two challenges re-anchored on kernel text with reproducers; differential 1031/1031 forward, 1063/1063 reverse; bytes x1.79 under a declared 1.8.
    • Review: one round, both lenses clean; low items and open questions go to the follow-up list.
    • Also on the branch since progress 10: the guides name TypeScript the executable reference and Quint the reviewed contract (eacef47), and the semantic coverage suite has an explicit budget (6fed122) after a hosted-runner timeout.
    • Inventory: 227 invariants, 425 regressions, 304 exported histories, 32 models.

    Next: effects (kernel commit in progress; its composition merges this head first), then the interactions PR whose design is being written.
26. lan17 commented on Sep 20, 2026

    

    lan17

    on Sep 20, 2026

    OwnerAuthor

    More actions

    Progress 12 (PR 188, head 070e42f): effects is composed, the fourteenth of fifteen and the last planned one; core stays uncomposed by decision (both ports' core drivers read private state; a later slice may rewrite them to the public record). The composition series is complete.

    • Kernel: remote_io::settleObserved/startLoaderFenced, deadlines::settleObserved, the held refill over the held read path (remote_writes::HeldWriting/settleLoader, HeldDump.sampled), diagnostics::begin; new modules adapter_replies and metrics. 29 modules; fixtures 16 files, 189 runs.
    • effects: 15 library transitions, lint 0; 48 public regressions, 10 invariants; flight-deadlines and effects-connection retired with their challenges re-anchored on kernel text; differential 554/554 forward, 560/560 reverse; bytes x1.43 under a declared 1.45. The effects driver and classifier are public-only.
    • Review: one round, both lenses clean of material findings; two low items fixed before landing (070e42f): a kernel miss-reason arm reported a stale frame-class adapter reply as unclassified where both ports report expired, at a boundary no current history reaches, now pinned by two fixture runs; and the re-sampled pinned-seed corpus of the composed effects text is recorded.
    • Inventory: 30 models, 213 invariants, 413 regressions, 310 exported histories, 70 challenges, reproducer backlog 37 (51 at the series' start).

    Next: the interactions PR (design written: a dark-shadow-over-layers profile first, executable refusals of unmodeled combinations, and a boundary-specific mutation gate), then the audit leftovers and the transitional bytes bounds.
27. lan17

    added a commit that references this issue on Sep 21, 2026

    feat(formal): map challenges to native mutants, require witnesses for…

    ...

    85077fb