feat(formal): map challenges to native mutants, require witnesses for every semantic case, and check settlement by receipt - #188
Merged
Merged
Conversation
Every challenge in execution.json carries a nativeMutants entry naming the TypeScript and Go mutants that inject its fault, or an enumerated explanation of why no native line exists; node formal/execution.mjs validates the table against both catalogs and freezes the two-challenge backlog. The catalogs grow from 13 to 55 paired mutants under one edits shape, with a declared ordinary cohort skip for the three Go mutants whose fault panics a synctest bubble. Two exported regressions pin faults only sampled histories reached. The semantic reporter records unhandled rejections beside failed assertions as consequences of the fault, the Go runner credits the core replay's pair assertion, MUTATION_ONLY measures named mutants into a partial report, and the workflow shards the lanes six and ten ways. Guides describe the table and stop quoting counts that go stale.
…d simplify the mapping table Review round one. readMutantCatalogs now owns the whole catalog shape for both ports, including that every edit anchor still matches the port text exactly once when applied in order, so a src/ or go/ refactor fails the pull request instead of the weekly lane; both runners and the coverage checker reuse it. The table names one mutant per challenge and a crossContract sentence; the unused environment kind, the Go catalog's copied twin fields, the unobservable catalog entry M16 and the declared ordinary-cohort skip are gone, the runner recording a crashed Go unit cohort instead. M28's Go edit defaults coalescing off only when the static leaf is omitted, matching TypeScript; the M33 texts state each driver's clock anchor; M24 names all three port asymmetries; explanations name the port files they examined; the buffer-limit backlog entry states its real reason. The Go runner credits the core replay's request-pair assertion too. A test pins how many mutants a shard may hold within its timeout and the guides stop quoting shard counts.
…checked by the audit, per-mutant crash records Review round two. formal/mutations.json replaces the two catalogs kept in lockstep: each fault is described once, carries a rationale with the port-side account, and holds a TypeScript and a Go section of edits and required detections, so pairing is structural. The challenge texts shrink to why the mutant is the same fault as the model's, under a length ceiling, so the code they used to quote cannot go stale. checkMutantAnchors runs in the audit, the test suite and both runners while manifest validation only checks the catalog schema, so the Quint lanes never read port text. Both runners record a crashed unit cohort and a noncompiling mutant per mutant and keep measuring the shard; the gate names the mutant. The M17, M34 and M33 texts describe the shipped mechanisms; new mutants require generated and portable detection only; the Go slow-class budget constant is 3.5 minutes.
…d only this port's sources Review round three, low items. M20's Go edit shared the process flight map across instances without a common lock and crashed a hosted shard with a concurrent map write; process flights now share one package-level lock. The TypeScript report fingerprints only src/ files; the shard merge gates through the shared catalog reader; the detection scorers take their cohorts from the port registry; a partial run exits nonzero when a selected mutant loses a required detection; a compile step that could not run is infrastructure, not a noncompiling mutant; a Go cohort that hits the go test timeout ends the shard as the budget assumes.
lan17
force-pushed
the
claude/fault-map
branch
from
September 18, 2026 13:46
4181ae0 to
76ba3ef
Compare
Fifteen semantic cases had exported regressions but no required sampled witness, so nothing checked that generated histories reach them. Each now names at least one generated witness: the runtime-boundaries exact-serving and bypass clauses are narrowed to what the public observation proves, the layers tracked-local-only rule and a new independent source-budget rule read inputs and public observations only, and the two policy labels the classifier already credited are registered. The registry grows to 440 labels in place, the baseline is re-recorded for seed 0xd1a1ca, two fixture recipes give the new labels committed histories with tests, and the parity ledger reports no case without a required generated witness.
Every behavior observe now carries a settlement receipt: the driver's controlled monotonic clock, what one zero-time verification drain found after the snapshot, and the gates it still holds. The coordinator keeps a ledger of the commands it issued per session and checks the receipt before comparing the observation: nothing runnable, the monotonic and wall clocks where the schedule puts them, and exactly the held gates the schedule leaves open. Core sessions carry no receipt and are held to the wall-clock rule alone; the local-clock driver's process clock is unconstrained. 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. The TypeScript and Go drivers compute the receipt from their own bookkeeping, both transports send it exactly when prepare names it, and both no-settle controls must fail every behavior profile with a settlement violation. PORTING.md states the rules R1 to R5 and what remains unchecked. The Go changes are test drivers and transport only.
lan17
changed the title
The hosted run on the receipt commit failed one TypeScript mutation shard: under M37, which publishes a rejected source's error object into local storage, six shadow-layers histories reported a settlement violation of one runnable task. No task had run. The driver recorded the error object by reference, took its snapshot with structuredClone, which keeps fewer members of an Error than JSON does, and then compared the JSON of the live observation against the JSON of the clone, so the two encodings of one unchanged object read as a change. The snapshot is now the JSON text that crosses the wire and the quiescence check compares that same encoding after the verification drain. Under M37 the six histories fail as observation mismatches, which is the detection the catalog requires; the unmutated corpus is unchanged.
… the ledger's hold-order rule Round-four review of the receipt commit. A settlement violation under a mutant is now recorded as a crashed cohort naming the first violating history and rule, in both runners, so the required-detection gate fails by mutant id while the rest of the shard is measured instead of the lane stopping at that mutant. The ledger attributes held gates per observation interval while both drivers decide holding at effect start; it now refuses, as its own limit and never as a violation, a schedule whose hold change follows an effect-starting command in one interval, and PORTING.md states the rule. The coordinator checks that a binding carrying a receipt controls its wall clock. The TypeScript transport sends the driver's receipt as is and leaves the presence and shape checks to the coordinator, which performed them again one call later; the Go mutation-evidence test drops the PATH-level node shim that injected a violation the evaluator's unit test already covers. A driver control pins the snapshot-encoding fix: an Error instance handed back as a call value reports nothing runnable. The layers witness test gains one negative per clause of the tracked local-only rule, the replay suites take one snapshot per step, and AUTHORING.md says what a new profile or held effect kind must touch.
…d bind the settlement check as one field Round-five review of the receipt commits. Portable evidence is composed once, in mutation-reports.mjs for both runners, and is recorded as crashed whenever its generated or fixed component is, naming the component; before, a settlement violation in the generated cohort left portable reading as detected or survived from the fixed cohort alone. A baseline violation names its rule in the failure message. Both runners match the settlement rule texts rather than the bare phrase, which a failed expectation can print. Each binding now carries one field for how the coordinator checks the contract (receipt, wall clock alone, or not at all) in place of two that had to agree and a guard for their impossible combination. The independent source-deadline classifier reads its budget from the profile's declared fallback deadline instead of a copy and is named for its profile. The driver keeps, for the harness message only, what its verification drain changed, and the replay suites and the transport append it to a violation. New controls: the independent clauses of the two source-deadline witnesses, the fixture work terms of the monotonic and wall clocks through the real driver, the timer term of the quiescence attestation, and the live-object control now checks the driver's encoding rather than the error type's member set. PORTING.md states the fake-timer parking limit, the schema-as-compatibility-unit rule and the ledger's per-interval attribution.
…and report the Go drain's findings Round-six review of the receipt commits. The rule texts the ledger produces were copied into both mutation runners as a literal; a new or reworded rule would have passed every runner test and, in the TypeScript lane, let a violation under a mutant count as a detection. The pattern is now exported beside the texts it matches in replay/settlement.mjs and imported by both runners; the coordinator test checks every rule text against it, and both runner tests check that the bare phrase, or a printed expectation regex, is not a violation. The Go driver keeps, for the failure message only, what its verification drain found (the first changed observation member and the deferred functions pending) and the transport appends it to a settlement violation, as the TypeScript transport does; the Go control requires it. AUTHORING.md notes that a new rule text belongs in the exported pattern.
The capture that lifts the violating output line for a mutant's crashed cohort began with an unanchored wildcard, quadratic in the length of a multi-kilobyte expected/actual line and rebuilt for every failed leaf. One anchored multiline regex at module scope extracts the same line linearly.
…bservations only The independent classifier read eleven of its sixteen labels from private model predictions (active reads and sources, load ownership and recovery flags, captured ages, the watermark). It now shadows the profile's schedule from the inputs, the asserted observation and the io channel alone: the clock from advances, read budgets and recovery ages from the policy inputs, source and decode ownership from which step grew the counters, deadlines by the same due-instant walk the model takes. Every public delta is bound to that schedule and a disagreement throws; a fidelity check compares the shadow with private predictions where a history still carries them and never credits. All thirty labels credit the same histories at the same checkpoints over the recorded corpus and the named regressions, so the baseline is untouched. Eight fixture recipes give the redefined labels committed histories, with one negative per discriminating clause.
…ines to the kernel library The remaining remote profiles hold their reads, decodes, dumps and writes as external gates the drivers release by index. The kernel now states that once: remote_io is a variant family over the layered shape whose held records are pending-only (a read carries its effect index, its flight and the effective TTLs of the reply; a decode carries its index, flight, TTLs, value and whether it recovers), every held read registers its flight at dispatch so followers join a pending read, loader ordinals map to flights, and 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. deadlines becomes one pending-only list of due instants delivered by an instant-ordered fold instantiated inside the kernel, with late arrival as one judgment and no drain at expiry; the local variants keep their history and source-budgets gains the field with no wiring change. serving exposes the release judged with the remote layer unobserved, the shared prologue, the 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 that a visible but declined frame yields no fence. The composition lint reports a profile-supplied lambda passed to a kernel definition. Sixteen kernel fixture runs pin the new seams; the five composed profiles replay their corpora step-identically in both directions at unchanged bytes per state.
The independent profile becomes wiring over the kernel library: seven library transitions (the deadline-wrapped held begin, read and decode settlement, loader settlement and advance, an aged remote seed and invalidation), the profile's own bounded state, input decoding and guards, and nothing else; the composition lint reports zero violations. Three invariants carry verbatim, four are restated one step over library records, and the settled-at-deadline invariant is replaced by an equivalence carried by the connection monitor's origins clause, two regressions and a kernel fixture run. The ten regressions pass verbatim once their three private-state patches become input schedules, and two new exported regressions pin a failed fresh decode that cannot recover and a visible stale miss that carries no fence and refills. The connection model is retargeted to the library records with an owned-flight conjunct, six challenges are re-anchored on kernel text and every mutant is caught by its named invariant or regression, and nine reproducer exclusions are rewritten to say why each other profile cannot reach the fault. All 512 sampled histories and the regressions replay step-identically in both directions at 0.76 of the old bytes per state and 0.64 of its generation time; the witness labels credit the same histories.
…rator a profile passes to the kernel, and pin the seams the corpora cannot reach Round-eight review of the held-I/O seam. A held release whose reply left the remote layer off started a source without a loader ordinal, so its deadline was registered at index -1 or on another flight's loader; the mapping is now one remote_io helper used by admission, release and the loader start, pinned by fixture runs and a per-step fixture invariant. The composition lint reports every operator a profile passes to a kernel definition, whether a lambda literal, a named profile operator, a let-bound lambda or a parameter forwarded through a helper, with fixtures for each spelling. The C23 challenge is re-anchored on the deadline rule itself and the source-connection monitor checks a pending deadline against its origin, so the fault fires under both consumers. The C58 rule on the atomic path, which no composed corpus can observe, is pinned by two frame-clock fixture runs and by the TypeScript reading. Dead or duplicate definitions go: the superseded flight settlement, the ERROR classifier that decodes to DENY, an unread parameter, a duplicated error carrier and a duplicated remote observation, now one judgment both release paths call. Seven more fixture runs pin recovering-flight joins, delivered-deadline recovery, failed recovery decodes, held-path local warming and zero-budget delivery; the fixture checker matches declared runs in batches so a large fixture cannot exceed a host's argument limit. A new exported regression pins the loader started by a read expiry at the read's due instant, and the behavior guide stops quoting a regression count.
A kernel change replays every composed profile in both directions. Six composed profiles took about 35 minutes on the hosted runner and the lane was cancelled at its 30 minute budget on the last two heads; five took 26. The budget is now an hour, with the measurements beside it and a note to shard the lane before the profiles approach it. A change outside the kernel still skips unchanged closures in under ten minutes.
… run fixtures under Quint's own selection, and pin the timeout classifier Round-nine review of the composition. The composition lint now reads the operator-typed parameter positions of kernel definitions from the parsed declarations and reports whatever fills one unless it names a kernel definition through aliases and let bindings, which deletes the list of spellings and covers the two it missed; the kernel fixture checker runs each fixture once under Quint's default selection, requires every declared run name to end in Test, and keeps the completeness guard, which deletes the batching and its argument-length reasoning. Fixture runs pin that a delivered or late deadline is a timeout for the recovery classifier, that a restarted loader carries no fence while a watermark stands, and that a reply leaving the local layer off warms nothing on the held path. The unread held begin goes; the frames row states the true reason the composed differentials cannot observe the atomic fence rule; the deadlines comment records the zero-budget delivery instant as the open point for a budgeted recovery composition.
…l callees in the lint, and replay the unfenced refill after a failed decode Round-ten review of the composition. The composition lint resolves a kernel parameter typed through a type alias to the operator type it names, following alias chains and failing loudly on one it cannot resolve, and resolves a kernel definition applied through a parameterless profile alias before judging its arguments and recording the transition, so neither spelling can carry rule logic into a kernel fold unseen; fixtures pin both. The recovery module retains a snapshot by appending, since a flight retains at most once. A new exported independent regression replays, in both ports, the refill a loader makes without a fence after a failed fresh decode under a raised watermark, and the decode-failure regression returns to pinning the rejection path alone.
…on cap, RemoteIO::begin and the latest-effect judgments A new kernel module, payloads, holds the payload validity classes (the drivers' value codes below 100 decode to themselves; 101 compressed, 102 corrupt, 103 unsupported encoding from 100 up) with valueOf, readFails, decodeFails and decodeOutcome. remote_frames::observe judges a frame's code once for the atomic release and the held read settlement, reporting failed and payload beside visible and value, remote_io holds the code in the decode and decodes it at settleLoad on the fresh and the recovery branch, remote_frames gains the tracked one-hour cap (TRACKED_RETENTION_CAP_MS, physicalRetention) that serving::authority applies to the retention a refill is written with while the recovery snapshot keeps the reply's maximum, and remote_io gains begin and the latestRead, latestLoad and latestOrdinal judgments. Every serve site judges the decoded value, never the code: serving::decide and remote_io::settleRead serve a positive valueOf only, and recovery::retain admits a candidate only when its code decodes to a value, so a code in the band that names no class (readable, no decode fault, valueOf NO_VALUE) is no recovery candidate and its flight misses with the loader's own error instead of completing a caller with NO_VALUE, the integer CALL_PENDING shares; the payloads header states the invariant that way. serving::judgeRelease now carries readOk = not(remote.failed) and startSource takes it instead of computing not(state.readFailed); at the two sites that start a source without observing the remote layer (remote_io::release under a reply without the remote layer, and the admission bypass in serving::admit, which passes false) layers.remote is false, so authority.refills is false whatever readOk says, and at the atomic release readOk equals not(state.readFailed) for every code below 100, so no existing composed profile moves; the candidate rule is the identity for every code below 100 and for the two compressed classes. The new fixture test/fixtures/kernel/payload-classes.qnt (15 runs) pins the three classes on both paths, including the documented limit that the atomic release serves a fresh corrupt frame's decoded value with no decode step, the no-class code that is no recovery candidate, the cap on tracked and atomic refills against the uncapped snapshot maximum and the untracked refill, and the decodeOutcome labels. The composed differential against 0135f49 agrees both ways at bytes x1.000 on every profile: independent 526/526, layers 528/528, policy 543/543, runtime-boundaries 283/283, scope 270/270, source-budgets 266/266. The manifest lists the module, the independent-wrong-recovered-value challenge is re-anchored on Payloads::valueOf(snapshot.candidate) and still caught, and the lint baseline, the generated-fixtures lock and the libraries count pin are refreshed.
…he kernel Serving::invalidate now owns all three outcome codes of the drivers' write-fault switch: missing_remote when the remote layer is absent, mutation_error under a write fault with the invalidation counted and the watermark unmoved, and ok with the watermark raised; Serving::maintains states whether an invalidation takes effect, the one judgment a marker lifetime will read. No composed corpus reaches the new branch: policy has 11,351 writeFailed states and no invalidate step, layers and independent invalidate 4,767 and 5,071 times with writeFailed never true, and runtime-boundaries, scope and source-budgets never invalidate under a write fault (measured on the feature corpora at 68eafb3). The composed differential against 68eafb3 agrees both ways on all six profiles at x1.000 (independent 526/526, layers 528/528, policy 543/543, runtime-boundaries 283/283, scope 270/270, source-budgets 266/266 histories). The frames-and-faults fixture pins the branch: under a write fault an invalidation is counted, reports mutation_error and leaves a watermark the wall clock has passed unchanged, and the next invalidation after the fault clears reports ok and raises it. The remote_frames header now says an invalidation never lowers a watermark, leaving a marker's expiry to the profile that composes one.
…utant anchors Merges origin/main c02bf6e (PR 190, the Go API reshape) into the fault-map branch at its K2 commit so PR 188 stops conflicting. Two files conflicted: formal/go-mutations.json, deleted on this branch in favour of the single catalog formal/mutations.json, stays deleted (main's M01 and M09 retargets are carried into the single catalog); formal/go-parity.json takes main's Go-side content and this branch's formal ledger pins, with the source-audit and feature-coverage pins refreshed for the merged files. The reshape invalidated the Go anchors of 16 mutants whose before text no longer occurs (M01, M09, M15, M18, M19, M20, M23, M24, M27, M30, M31, M32, M34, M45, M48, M49) and left 7 whose after text no longer compiles (M11, M14, M17, M21, M28, M29, M44; M17 moves from go/cache.go to go/engine.go), so all 23 go.edits arrays are retargeted to main's go/ text, each anchor matching exactly once. No Quint model, src/ or go/*.go library code changes; the branch's go/*_test.go drivers compile unchanged against the reshaped API.
The recovery-read profile now assigns every state transition to the kernel library: RemoteIO::begin, the compression variants of settleRead and settleLoader, RemoteIO::settleLoad, Remote::seedAged and storeFrame (the drivers' literal unsafe stamp, selected by a guarded wrapper under any), Markers::advance, invalidate and observe, and Serving::closeScope, with the seed tables, policy decoding and guards kept in the profile; the composition lint reports 13 library transitions and no violations, down from 80. The three receipt invariants and recoveredAgeUsesLogicalMaximum move into the connection model as one-step clauses over the library records (five invariants), and the profile keeps eight over the public channels and the held records, completedCallsHaveNoActiveWork admitting the NO_OWNER a caller served from the request memo or local storage carries. The four recovery-read challenges re-anchor on recovery.qnt and remote-io.qnt with exported-regression reproducers, a new challenge on serving.qnt's authority pins the tracked retention cap through trackedWritesRespectPhysicalCap and maps to the new catalog mutant M56, and recovery-read joins the partitions of five shared-library faults. The parked markers and compression modules land with their fixtures (9 kernel fixtures, 105 runs), and the profile exports 31 regressions, five of them new and passing identically on the former text. The differential against 0a47889 agrees on 282 of 282 reference and 287 of 287 candidate histories at 2034 to 2304 bytes per state (x1.133, bound x1.2) with generation wall 3.1 s to 4.5 s (x1.45, advisory), and the six other composed profiles are unchanged at x1.000. M56 is detected in the generated cohort of both ports (TypeScript in every cohort; Go in generated, fixed and portable).
…lease, separate payload class from value, and state the recovery monitor over storage fields The layered release and the read settlement carry remote_frames::Observed instead of flattened booleans, and a source started without the remote layer passes UNOBSERVED. A payload code in the band is a class hundred plus the value, so a profile spells a seed as Payloads::COMPRESSED + VALUE_ONE and the class rules read the class alone. The recovery connection restates presence, retention and fence from the raw fields, compares a retained candidate to the acquired raw code, requires local expiry and recency unchanged after a recovery decode, and hoists its shared clauses. Serving::invalidate branches on maintains, and a new regression pins the unsupported-version miss under a raised watermark as fenced. The composed differential against 20b9159 agrees both ways for all seven profiles at x1.000. Not taken: the far-future-age encoding of the unsafe stamp, which would drop the drivers' literal vector; computing the recovery decode's failure once, which would move a challenge anchor; a decodes fact for the atomic corrupt frame and a Go unit test for the tracked clamp, both later slices.
…get, pin the encoding-failed read and the bare corrupt code, and state the read-settlement clause both ways The pull_request CI typescript job failed on 20b9159 and cd28a96 because the reproducer-validation test in test/formal-execution.test.ts took 5.7 s on the hosted runner under coverage against vitest's 5 s default. One validation pass now reads and scans each model source once, the test's validate helper shares scans across its passes keyed by source text, and both manifest-validation tests carry an explicit 60 s budget. Locally under coverage the two tests fell from 1.4 s to 0.35 s and from 1.75 s to 0.39 s. The recovery connection states the read-settlement clause both ways, so a decode is held exactly when the raw fields say the frame is observable and its age lies in [0, freshness). A new regression pins that an encoding-failed read leaves no candidate, so the loader failure that follows is unclassified and reports no recovery label; the payload-classes fixture pins the same over public channels and pins a bare corrupt code as a declined frame. The payloads header states that a compressed or corrupt code needs a positive value to reach a decode step, its unused import is gone, remote_frames owns the watermark baseline through clearWatermark, and the kernel comments this slice wrote cite symbols instead of line numbers. The composed differential against cd28a96 agrees both ways for all seven profiles at x1.000, and the sampled recovery-read corpus fingerprint is unchanged.
…re class code's miss label exactly The recovery-connection monitor's header now lists the unsupported-encoding seed (code 10) as a third seed shape that fails the read, instead of claiming every seed is a value below 100 or a class code plus a positive value. The payloads header now says a bare COMPRESSED or CORRUPT code reports the miss recovery label when its loader fails, as any declined frame with no candidate does, instead of claiming it reports no recovery label; the fixtures lock input hash for payloads.qnt is refreshed.
…re the portable cohort for M56, and drop a duplicated fixture pin A new recovery-read regression, lapsedMarkerUnfencesTheFrameStampedAtItsCutoffTest, pins on the public channels that once a watermark's marker lapses a frame stamped at the old cutoff is read as a stale recovery candidate and served without a write; it passes on the old profile text and fails when markers::advance drops expire. M56 now requires detection in the portable cohort of both ports, as every other catalogued mutant does. The markers fixture no longer restates the Serving::invalidate write-fault outcome that frames-and-faults pins. The profile header points at the BEHAVIOR.md composition-profile row and the replay driver module where the input mapping lives. The differential against 1937249 agrees both ways at x1.000 and the sampled corpus fingerprint is unchanged.
… the scheduled deadline shape and the failure judgment serving splits the atomic release into the judgment and its application (releaseJudged) and adds startDetachedSource over the new flights::registerDetached, a source no caller owns. deadlines splits the Scheduled shape, the clock beside the pending deadlines, out of Budgeted and retypes registration, forgetting and delivery over it. recovery adds the failure judgment and missed, which remote_io::failed now applies in place of its inline classification. Every change is a split or an addition over the same state, so no composed profile moves: the composed differential against 9d64a88 agrees both ways for all seven profiles at bytes x1.000. The frames-and-faults fixture pins the detached source and the generated-fixtures lock records the five edited kernel files.
The previous commit took the differential test file from before the recovery composition and lost the pin that lists recovery among the composed profiles. The file is the composition's version again, with the prepare test it already carried.
…profile pin The rebase of the recovery slice onto the differential hotfix dropped the unit test that prepares the head against itself; it is back, and the composed-profile pin still names recovery.
… TTL withdrawal, and delete the recipe-side action binding local_faults::begin withdrew the reply's local TTL before the layer gating, so a faulted call lost the local layer and, with the remote layer off, two faulted callers each started an unshared source where the implementations coalesce from the resolved configuration before the read. serving gains judgeReleaseUnder, the layered judgment with the local read's fault as an argument: the local value is hidden, the layers stay as the reply resolved them, and releaseJudged publishes for the TTLs the judgment allows (publishable), so a faulted remote hit warms nothing and a faulted miss's source captures no local TTL; no state field is added and settle still withdraws the captured TTL. The local-faults fixture pins that two faulted callers share one source exactly as two healthy callers do. generated-fixtures.mjs loses the dead recipe-side actionBindings, the differential's descriptor binding is recorded as transitional until the merge base with main carries the renamed local-clock text, local-clock schedules noProviderMakesNoPolicyCall, and policy_gate::hold and serving's admission state that held replies need a layout with a policy provider. The composed differential against 43c8dc9 agrees on every history both ways for all ten profiles at x1.000 (local-failure 133 of 133 at 1477 bytes per state); kernel fixtures 12 with 137 runs, lock and ledger pins refreshed.
…e prepare test's budget, and cite the landed kernel commit remote_io::settleDispatched and remote_io::beginRead had no caller: the recovery profile reaches Diagnostics::beginRead, which calls the Deadlines pair, so the rule is stated in deadlines alone and the C42.allow-override ledger citation names the executed definition. Diagnostics::attributed guarded a condition its only call site made always true; the bypass branch records NO_LAYER directly, as admitRequest does. The differential prepare test spawns about 65 git processes and now carries an explicit 30 s budget. The recovery record row cites 2add082, the landed kernel commit, instead of a pre-rebase hash on no branch, and says the 1.85 bytes bound is transitional. The composed differential against e88d137 agrees on every compared profile in both directions at x1.000, and the fixtures lock moves only its two kernel input hashes.
…ult-map Lane B brings the fractional clock, the inline local call, flights::latest, instances::construct, Layout.policyProvider and the local-failure and local-clock compositions onto the recovery slice. Conflicts were ledgers and shared tooling: one validate-as-written hunk in differential.mjs with lane B's descriptor binding, one 30 s prepare test carrying both lanes' assertions, reproducer lists derived from the merged catalog, and one record table in the kernel README. execution.json is additive; its eight cross-lane exclusion cells were restated and re-measured, and the recovery profile and held-diagnostics fixture declare policyProvider: true. Regenerated: profile-lint-baseline.json, generated-fixtures.lock.json, the source-audit.json and go-parity.json pins (scheduledInvariants 231), and the local-failure witness-baseline entry, whose recorded corpus predated lane B's fix commit.
…time check-go-parity.mjs now reads a case's rule, contracts, cited checks, witnesses, replays and vectors from semantic-cases.json, scans each production file's declarations from src/, takes each reviewed file's hash, entries and contracts from source-audit.json and the profile schedule from execution.json and profiles.json, and checks them against the schedule and the repository instead of comparing them with stored copies. The ledger keeps only what a reviewer writes: per case its group, gaps and evidence paths; per source its hash, Go bindings and rationale; per reviewed file its Go applicability; the adaptations and boundaries. The file shrinks from 19,933 to 5,149 lines with every kept row byte-identical (schemaVersion 2). The test injects broken inputs to show each derived fact still fails the check.
Each case's Quint citations are now `models: [{ref, scope}]` and `definitions: [{ref, scope}]`, one citation per line, so a check and the scope a reviewer gave it are stated once on the case instead of joined across two files. check-semantic-coverage.mjs derives a citation's kind from the schedule or the declaration and requires a scope structurally; check-go-parity.mjs reads the refs and drops the audit pin. The shared disclaimer sentence and the general limitations move into SEMANTIC-COVERAGE.md once; the two case-specific limitations become evidenceNotes on C16.sparse-leaves and C54.read-ownership. quint-case-audit.json (5,229 lines) and its test go; semantic-cases.json grows from 268 to 1,137 lines and its test carries the ported mutation cases.
formal/replay/witnesses/fidelity.mjs now holds what independent.mjs, policy.mjs and recovery.mjs each restated: the test for a history that still carries private state, the layout guard that names a history in another layout at its first missing field, and the step-by-step comparison of the shadow with the model's predictions. Each classifier hands fidelityBinding its public channels, layout fields and a view that puts its shadow beside the model's state, keeping only its shadow and modelView. Behavior is unchanged: the witness fixture tests pass and the evidence from witnesses.mjs agrees label for label over the hosted policy and independent corpora and over regenerated independent and recovery corpora. profiles.json lists the module in replaySources and in the three profiles' witnessSources.
… in the profile lint The composition rule no longer resolves type aliases to their typedefs or follows def and let-bound aliases on both sides of a kernel call to decide whether an operator position holds a kernel definition. It computes the kernel definitions that declare an operator-typed parameter (deadlines::deliver today; a parametrized kernel definition without a declared type is an error) and reports any reference to one from a profile's assigned value, as the callee or by name, whatever the argument is. The five alias fixtures and library-alias go with their expectations; the lambda, named-operator and helper fixtures keep theirs under the new detail, and composition-wiring-passes keeps the record-literal and chosen-input wiring. profile-lint-baseline.json is unchanged and every composed profile lints clean.
…ees in the profile lint The denylist commit judged a kernel definition higher-order only when a parameter type was spelled as an operator inline, so a parameter typed through an alias such as `type Step[r] = (Counter[r], int) => Counter[r]` made the fold instantiable from a profile with no report, and a kernel definition applied through a profile alias (`pure def bumpAlias = L::bump`) recorded no transition, which empties the list the composed-violations gate keys on. The rule now resolves a `const` parameter type through the lookup table to its typedef, following alias chains and failing on one the parse does not resolve, and follows `def x = <name>` and let-bound aliases for the callee only, judging and recording the application as the kernel's. The library-alias, alias-typed-operator-position and aliased-transition fixtures return with the denylist's expectations, and the kernel README states the rule as checked. profile-lint-baseline.json is unchanged.
The admission profile now assigns every state transition to the kernel library: Shadow::beginHeld, settleRead, settleLoad, settleLoader and advance over a new held section of the shadow module, and Remote::seedFrame; the composition lint reports six library transitions and no violations, down from 65. The held section captures the cohort selection when the caller's read is dispatched and consults it when the decode completes the hit, holds a served job's decode and confirmation read in remote_io's lists, and factors admitServed, busy and confirmation once for both shapes; remote_io::holdRead is factored out of dispatchRead. Six invariants are carried and two added; effectsMatchRecords restates the read count over the append-only io.budgets, one row per held read, so a read counted without a budget violates it. The six regressions replay verbatim and two new ones pin the captured selection and an uncoalesced caller's own read; admission joins three shared-library partitions and its two faults re-anchor on shadow.qnt over all fifteen profiles. The differential against 56bb2bb agrees on 134 of 134 reference and 136 of 136 candidate histories at 3024 to 4910 bytes per state (x1.624 under a declared transitional bound of 1.65), and the other compared composed profiles are unchanged at x1.000. The admission witness classifier binds its shadow to the composed layout through the shared fidelity scaffold, the held-shadow fixture lands with 13 runs, and the ledgers, lint and witness baselines, fixture lock and count pins follow.
The admission slice (21d57bf) composes the admission profile from the kernel library: a held section in shadow.qnt (capture, beginHeld and releaseHeld, settleRead, settleLoad and settleLoader, admitServed, busy, confirmation over Limits and Shadowing), remote_io::holdRead, the held-shadow fixture, the admission public classifier over fidelity.mjs, and the ledgers. The merge onto b1b5c83 (the profile lint alias fix) resolved without textual conflicts; the lint baseline, execution manifest, and ledger pins already matched the merged tree, so nothing was regenerated.
lan17
commented
Sep 20, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
This PR materially advances the goal of a robust DialCache formalization that can validate behavior against TypeScript as the reference implementation. Its strongest contribution is a more trustworthy, measurable connection between the formal models and the real implementation, together with greater reuse of behavioral definitions. The improvement is larger in validation quality than in the breadth of feature combinations covered.
Review scope: the detailed review and local checks below were performed on 3733b6b62ee3ebcd6b9181a577d6a4748405b417. Before posting, I checked the relevant fix and CI status at d9e6d5a91867a9a740bcafe9de9eec16b9baf64c. The subsequent 18 commits have not received the same full review, so the earlier counts and measurements below are explicitly tied to the reviewed revision.
The concrete blocker found in the original review is now fixed. Previously, readManifests() added derived regression lists and prepare() passed that expanded manifest to a validator that rejects those fields, aborting every differential run. The current prepare implementation validates the raw manifest first, and a regression test exercises preparation. The current differential job passes. I am not reporting that issue as an outstanding blocker.
The strongest evidence of practical value is the TypeScript mutation report at 3733b6b: generated replay detects 55/55 selected faults, while the ordinary TypeScript unit suite detects 45/55. The additional detections include joining a flight despite coalescing being disabled, refusing to replace a local entry, clearing a valid local entry after source failure, and caching a rejected source result. Some of this establishes stronger evidence for coverage that already existed; it should not all be counted as newly added behavior coverage.
The substantive advances at the reviewed revision are:
- Implementation assertion strength: the native catalog grows from 13 to 55 faults, with 63 of 73 model challenges mapped to native mutations. Generated replay must detect the selected faults in both ports; noncompilation and settlement failures do not earn detection credit.
- Consequential coverage: all 240 behavioral semantic cases have required generated witnesses. The new classifiers derive coverage from inputs and public observations, strengthening the connection between a coverage label and the behavior it claims.
- Replay integrity: settlement receipts are checked before expected results. Incorrect driver timing can fail as a harness error instead of misleadingly counting as behavior-mutation detection.
- Model reuse and independent checks: eight of fifteen profiles were composed at that revision, up from five. The three newly migrated profiles add 15 named regressions and make three private-state regressions replayable through native APIs. The recovery connection reconstructs freshness from raw storage facts and checks local expiry/LRU alongside values, which can expose unintended TTL refreshes.
The remaining priorities for the formalization are:
- Validate interactions across features. Kernel reuse does not establish correctness for arbitrary combinations. The reviewed profiles exclude important combinations of concurrency, request/local storage, shadow work, held I/O, decoding faults, and source deadlines. The kernel explicitly documents out-of-profile differences from native behavior, including corrupt payload handling on its atomic path and a zero-budget recovery timing case. Add interaction histories and executable restrictions on unsupported combinations before treating the kernel as a general behavioral model.
- Require boundary-specific mutation evidence. The current gate requires detection somewhere in a cohort, rather than by the named boundary's consequential assertion. For example, M29 can be detected by an extra policy-provider call before incorrect retention is observed. A named detecting history and relevant observation would strengthen each mapping. There were also 51 model challenges without deterministic reproducers at the reviewed revision.
- Keep settlement claims precise. TypeScript infers remaining runnable work from observable changes and net timer-count changes during another drain. This strengthens harness validation, but does not independently prove executor quiescence. The PR documents that limitation.
- Clarify TypeScript's authority. The existing specification calls Quint the behavioral source of truth. Given the intended role of TypeScript as reference implementation, document the relationship explicitly: TypeScript is the executable reference being formalized; Quint is an independently reviewed contract; discrepancies require a distinguishing regression and an explicit decision about intended behavior.
Validation: on 3733b6b, local focused checks produced 375 passing TypeScript tests, four skipped tests, and a passing Go settlement-control test. Inventory, semantic-coverage, and fixture verification also passed. I inspected that revision's successful full formal workflow and its TypeScript mutation report; I did not rerun the full Quint campaign locally.
At the current d9e6d5a head, the full formal workflow succeeds, as does the differential job. The ordinary TypeScript PR job is still failing: its recorded failure is a 5,000 ms timeout at test/formal-semantic-coverage.test.ts:80 (3,263 tests passed, 37 skipped). That needs resolution before treating current PR validation as green.
The definition-citation case re-checks the whole inventory five times against the Quint sources. It runs in about half a second locally and took 5.2 s on the hosted runner at d9e6d5a, past the 5 s default, so the TypeScript PR job went red while every formal lane stayed green. The suite now declares a 30 s budget, as the execution and differential suites already do for their inventory-wide cases.
…reviewed contract The guides called Quint the behavioral source of truth for both ports, which misstates the relationship: TypeScript is the executable reference the models formalize, and Quint is the independently reviewed contract that TypeScript, Go and later ports are held to. The landing page, AUTHORING.md, SPEC.md and GO-PARITY.md now say so, and state how a disagreement is settled: a regression that distinguishes the two behaviors plus a recorded decision about the intended one, never a quiet edit to whichever side is easier to change. Ledger pins refreshed.
Owner
Author
|
Review disposition at eacef47:
|
…oad forms once, buffer the invalidation watermark, and keep the job registry pending-only The shadow module gains the held lifecycle the shadow profile composes next: a job's C0 read, decode and confirmation read are held in remote_io's lists over the job's source, so served and dark jobs share settleJobHeld, settleJobLoad and settleJobRead. The registry is pending-only and keyed by the job's source; Job carries the reply's TTLs, the C0 stamp and the captured logging, and Shadowing gains the hook and the logging flag. payloads spells the PADDED and UNICODE classes and the BINARY form line once; raiseWatermark, serving::invalidate and markers::invalidate take the invalidator's future buffer, every call site passing 0. A source the caller's deadline fails ends its job timeout on every path (sourceOutcome; expireHeld continues the job waiting on the expired flight), pinned by the held-dark-shadow fixture under a job budget above the source budget, and admission's effectsMatchRecords keeps the direction that every pending loader flight has its job. The differential against d9e6d5a agrees both ways for all twelve composed profiles, at x1.000 for ten, x0.903 for shadow-layers and x0.964 for admission, both down because finished jobs leave the registry.
…retire the shadow validation model The shadow profile now assigns every state transition to the kernel library: Shadow::beginDark, settleHeld, releaseRead, releaseLoad, releaseDump, releaseWrite and advanceHeld over the dark arm of the held shadow lifecycle, Remote::seedFrame, Serving::invalidate with the drivers' future buffer and Clock::shiftWall; the composition lint reports fifteen library transitions and no violations, down from 96. Seven invariants carry verbatim, two restate one step over the library records, four are new over the held records and their deadlines, and warningsRequireValidCapturedPolicy becomes the rule shadow::recordVerdict states, pinned by five regressions; the 31 state-patching runs become public schedules, so all 39 regressions export (one duplicate deleted, two added as reproducers), each settling its source explicitly so no export depends on the seed. The standalone shadow validation model is retired with its two challenges re-anchored on remote_writes::dispatch and shadow::settleJobRead, shadow-inclusive-c0-freshness re-anchors on shadow::acquired beside its shadow-layers twin, and shadow joins four shared-library partitions while its other twenty cells restate their reasons for the composed text. The shadow witness classifier is one public-only replay of the profile's rules that refuses an observation the inputs do not produce and binds to the composed layout through the fidelity scaffold, replacing the two private readers, and its excerpt fixtures become full public histories under the o/d projection. The differential against 943f139 agrees on 1031 of 1031 reference and 1063 of 1063 candidate histories at 1816 to 3251 bytes per state (x1.791 under a declared transitional bound of 1.8) with generation wall 8.1 s to 17.0 s (x2.10, advisory); every other composed profile has an identical closure, and the ledgers, lint and witness baselines, fixture lock and count pins follow.
…e refill over the held read path remote_io::settleObserved applies the held read settlement from a judgment already made (the observation and the fence a refill it starts carries, startLoaderFenced), settleRead is its composition with the judgment of the frames, and deadlines::settleObserved is the budgeted variant over expiredIfReached. remote_writes gains the held refill over the held read path (HeldWriting, settleLoader: an accepted result that refills records its outcome, drops its snapshot and holds its dump; every other arrival is deadlines::settleLoader) and a held dump records the wall clock its first fence check sampled (HeldDump.sampled, C34). diagnostics::begin is the labelled admission and held release for a profile whose drivers hold the read; beginRead settles it in the same step through Deadlines::settleDispatched. The future-buffer invalidation the effects design proposed as raiseWatermarkAhead and invalidateAhead is the bufferMs signature 943f139 landed, reused unchanged. Behavior is preserved: the fence is judged on the pre-settlement state startLoader read it from, the begin/beginRead split is the deadlines pattern, and sampled lives only in the held dump. The composed differential against 943f139 agrees both ways for admission 136/136, independent 526/526, recovery 542/542, recovery-read 290/290, scope 270/270, shadow-layers 281/281 and source-budgets 266/266 at x1.000 (shadow-layers x1.001, the sampled field of its held dumps), five composed profiles keep identical import closures, and the fixture lock moves on the four module hashes with no artifact change.
The shadow slice lands as two commits: the kernel commit 943f139 (the shadow job's reads and decodes held as remote I/O records, the payload forms spelled once, a buffered invalidation watermark, a pending-only job registry) and the composition 99da12d (the shadow profile as wiring over the kernel; the shadow validation model retired with its two challenges re-anchored on kernel text). The merge onto eacef47 (the authority wording) conflicted only in the two pin ledgers; both were taken from lane B and recomputed with refresh-pins over the merged guides. Lint baseline, manifest and audit matched without regeneration.
Brings the shadow composition (99da12d, merged as f6ced95) under the effects kernel commit 6164e43, whose parent 943f139 is the common ancestor. The one textual conflict was the kernel README's module table: the remote_writes and diagnostics rows keep K's held-refill and begin sentences, the shadow row takes the fault-map side naming shadow as its third consumer. The merged tree typechecks, the 15 kernel fixtures pass (170 runs), the lint baseline matches, the fixture lock regenerated from a scratch copy is byte-identical to the auto-merged one with no artifact change, and make audit passes. The composed differential against 943f139 agrees both ways on every compared profile at x1.000 (admission 136/136, independent 526/526, recovery 542/542, recovery-read 290/290, scope 270/270, shadow 1031/1031 and 1063/1063 at x1.791 under its declared 1.8, shadow-layers 281/281 at x1.001 from the held dump's sampled field, source-budgets 266/266), with layers, local-clock, local-failure, policy and runtime-boundaries not compared under identical closures.
… retire the flight-deadlines and effects connection models The effects profile now assigns every state transition to the kernel library: Metrics::begin, settleRead, settleLoad, settleLoader, releaseDump, releaseWrite, advance and invalidate over two new modules, adapter_replies (the queued adapter reply normalized once at the trust boundary) and metrics (the ordered event trail the drivers compare, stated as metered variants over the diagnosed held lifecycle), plus Replies::queue, Remote::seedFrame, Clock::advance and shiftWall; the composition lint reports fifteen library transitions and no violations, down from 64. Three invariants carry verbatim, six restate one step over the library records and acceptedSourcesSettledBeforeTheirDeadline is new; the five state-patching runs become public through replyWith and overrideReadBudgetWith, lateSourceResultIsADeadlineErrorTest is added, and all 48 regressions export. The flight-deadlines and effects connection models are deleted with their two challenges; the three effects challenges re-anchor on serving::refills, deadlines::arrival and metrics::stamped with exported-regression reproducers partitioned over all fifteen profiles, effects joins six shared-library partitions, and the 26 retired citations move to runtime-boundaries, effects and kernel definitions. The differential against cf03e05 agrees on 554 of 554 reference and 560 of 560 candidate histories at 3586 to 5108 bytes per state (x1.425 under a declared transitional bound of 1.45) with generation wall 11.2 s to 17.7 s (x1.58, advisory); every other composed profile keeps an identical closure. The driver parses both layouts into the version-2 asserted record (Go untouched), the witness classifiers read inputs and the asserted record only and bind through the fidelity scaffold with all 93 labels reached, the held-writes fixture lands with 19 runs, and the ledgers, lint and witness baselines, fixture lock, guides and count pins follow.
`metrics::missReason` reported a queued frame reply's miss through `adapter_replies::reason`, which normalizes the miss classes, so a frame reply declined as stale was `unclassified` where the ports report `expired` for any frame whose age reaches the freshness (`redis-cache.ts` `getWithResolvedConfig`, `engine.go` `readServing`). Both arms now judge the declined frame's stamp through one `declinedFrameReason`: `unclassified` ahead of the wall clock, `expired` otherwise. The held-writes fixture pins the inclusive boundary: a hit at the last fresh millisecond, `expired` at the freshness, `unclassified` one millisecond ahead. The effects corpus never reaches a stale reply (560 of 560 histories agree both ways); the kernel README records why the composition re-recorded 74 effects label counts, and BEHAVIOR.md's witness count now matches the 93 listed.
lan17
commented
Sep 20, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
Re-reviewed the updates through 8136c1b35bfeb52c87a3ad4162c8bf9b4bf2f750, including the changes since the last detailed review at 3733b6b. No new blocking correctness finding from this review. The updates improve the fit with the stated goal: define behavioral tests once and use them to validate TypeScript, Go and future implementations.
The earlier actionable concerns are addressed:
- The differential validates the raw manifest before deriving schedules, with a regression test exercising preparation.
- The semantic-coverage suite has an explicit timeout budget, and the current ordinary TypeScript PR job passes.
- README, AUTHORING, SPEC and GO-PARITY now identify TypeScript as the executable reference and Quint as the reviewed contract, with a distinguishing regression and recorded decision required when they disagree.
The additional progress is concrete:
| Capability | Earlier detailed review | Current head |
|---|---|---|
| Profiles using shared kernel transitions | 8 of 15 | 14 of 15 |
| Named public histories scheduled for implementation replay | 270 | 310 |
| Model challenges with deterministic reproducers | 22 | 33 |
The extra replay histories are useful coverage, not just inventory growth. Shadow now exports 39 public regressions instead of 7; effects exports 48 instead of 42; admission exports 8 instead of 6. Former private-state fixtures become commands that the real implementations execute. Recovery, shadow, admission and effects classifiers also reconstruct their relevant state from commands and public observations, with a separate comparison against private model state to detect drift.
I checked the removal or replacement of the older recovery, shadow-validation, flight-deadlines and effects-connection checks. I found no demonstrated behavior now escaping the combined test gates. However, the rewrite does not preserve every old independent invariant unchanged: some checks move to another profile sharing the same transition, and some become named regression histories. For example, shadow warning authorization is now covered by specific public regressions, as documented beside the invariants. The improvement should be described as consolidation plus more native replay coverage, rather than a uniform strengthening of every model property.
The author's proposed follow-up scope is appropriate:
- Add histories combining features that the current separate profiles exclude.
- Require each mapped mutation to fail a named history at the relevant behavioral assertion, in addition to failing somewhere in the generated cohort.
- Keep settlement receipts described as an external harness check, with their documented limits on proving executor quiescence.
Those remain outstanding. Sharing a transition between profiles makes combined tests easier to write; it does not establish that the combinations have been exercised.
Validation in this re-review: focused TypeScript tests passed across the manifest/differential tools, semantic and Go-parity accounting, effects replay, recovery/shadow/admission/local-clock smoke histories, and witness boundary/attribution controls. Execution-manifest validation, semantic coverage, Go-parity accounting and committed-fixture verification passed. The current generated witness report has no failed or incomplete entries. Quint-specific local tests were skipped because Quint is unavailable locally; hosted results remain the evidence for those checks.
At posting time, the ordinary TypeScript and Go PR jobs, PR Quint check, full-run generation, symbolic check and full TypeScript replay pass. The current full formal workflow and differential job are still running. My recommendation is to merge once the required current-head validation completes successfully, then prioritize the promised interaction histories and boundary-specific mutation evidence.
Replaying all fourteen composed profiles in one job overran the smoke workflow's 60-minute budget (57 minutes at d9e6d5a; cancelled at f6ced95). The differential job is now a four-shard matrix: formal/differential.mjs takes --shard=<index>/<count> with --composed and deals the profiles sorted by name round-robin, so each lands in exactly one shard, and make differential threads DIFFERENTIAL_SHARD to it through the parser the mutation lanes use. Every shard still checks the lint baseline and the kernel fixtures and preserves its reports as formal-differential-<index>. The workflow shape test pins the matrix against the count in DIFFERENTIAL_SHARD.
lan17
commented
Sep 21, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
Re-reviewed 84fccb1f7222c8566f48bca5c03bb7525e76cf97, specifically the two commits since the previous detailed review. No new blocking findings. I recommend merging this head; the validation that was pending at the previous review is now green.
The latest changes are sound:
- Stale adapter-frame replies now match TypeScript. The model reports
expiredwhen the frame's age reaches the freshness limit, andunclassifiedwith a clock offset when the frame is future-dated. Miss-shaped replies retain their existing normalization. The new kernel regressions pin the last fresh millisecond, the expiry boundary, and a frame one millisecond ahead. - Splitting the differential check preserves its coverage. Selection still includes every profile composed in either revision, with each assigned to one shard. Every shard retains the composition lint and kernel fixture checks, and failures still fail the job. I downloaded all four CI artifacts and verified 14 unique profiles, with 5,493 forward and 5,553 reverse history comparisons and zero disagreements. All four jobs completed in about 12–21 minutes, resolving the previous single-job timeout.
This PR materially advances the stated goal of authoring behavior once and validating multiple implementations. The broader improvements from the previous review remain: 14 of 15 profiles use shared model transitions, and 310 named public regression histories are scheduled for implementation replay. TypeScript remains the executable reference for deciding whether the contract matches intended behavior. The latest two commits improve model accuracy and make the existing checks practical to run in CI.
There is one concrete coverage limit in this update: the new stale-reply boundary histories are kernel-only tests. The current effects corpus cannot reach that stale-reply case, so its passing replay does not establish this particular boundary in both implementations. Exporting a portable history for that case is a useful follow-up. The previously identified priorities also remain: histories combining features, and requiring each mapped mutation to fail the relevant behavioral assertion in a named history.
Validation: the full formal workflow passes at this exact head, including model checks, generation, symbolic checks, full TypeScript/Go replay, and both languages' mutation runs and merges. The four differential shards and PR Quint checks also pass, as do the ordinary TypeScript and Go PR jobs. Locally, execution-manifest validation and committed-fixture verification passed; focused differential/validation tests passed 34 tests, and Redis/metrics tests passed 68. Five Quint-dependent local tests were skipped because Quint is unavailable locally; hosted checks provide that evidence.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR closes three coverage holes of #165 and starts the composition of the held-I/O profiles, one commit series each: fault mapping by meaning (evidence guarantee 3), a required generated witness for every semantic case, a machine-checked
causally-ready-v1settlement contract, and the kernel seam for held remote I/O with theindependentprofile composed over it. The first series is described under "Fault mapping"; the others follow it.Fault mapping
Every model challenge in
formal/execution.jsonnow maps to the native mutants that inject the same wrong behavior into both ports, or explains why no native line exists. This is evidence guarantee 3 of #165 (fault mapping by meaning): a mapped challenge proves the corpus would catch that mistake in a port, not only that the model rejects it.What changes
nativeMutants: { kind, mutant, text, crossContract }with kindsmapped,unobservable,model-only. The text says why the mutant is the same fault as the model's (under 500 characters, naming the mutant and the model definition); the port-side account lives once on the catalog entry as itsrationale.node formal/execution.mjsvalidates the table on every manifest validation: the mutant exists and both its port sections requiregenerateddetection; an explanation names the port file it examined;crossContractis a sentence present exactly when the mutant's semantic case does not list the challenge's contract; two challenges repeating one fault map it the same way; every challenge has an entry or is listed in the frozennativeMutantBacklog, never both. Result: 62 mapped, 2 unobservable, 6 model-only, 2 backlog, over 72 challenges. Before this change 9 of the 34 challenge contracts had any native mutant and no anchor was checked before the weekly run.formal/mutations.json, replacessemantic-mutations.jsonandgo-mutations.json: 54 faults (M01 to M55 without M16, whose fault turned out to be unobservable and is now an explanation), each described once with arationaleand atypescriptand agosection ofedits: [{ path, before, after }]plusrequiredDetections, so pairing is structural rather than validated. Every anchor is checked against the port text bynode formal/execution.mjs,make audit, the test suite and both runners (checkMutantAnchors), so asrc/orgo/refactor that moves an anchored line fails the pull request rather than the weekly lane, while the Quint generation lanes never read port text. Each port's own unit suite is informational for a mutant: a synctest panic, or a TypeScript unhandled rejection with no failed assertion, is recorded as acrashedordinary cohort (M17 and M34 in Go today), a mutant that does not compile is recorded with every cohort crashed, and the gate names the mutant while the rest of the shard is measured. New mutants requiregeneratedandportable; the thirteen original mutants keep theirordinaryrequirement.formal-traces), and the hosted full runs on the first two heads (35335831285, 35340267557) are green across all sixteen shards; the run on the round-two head (35344793734) failed only on M20's then-unsynchronized shared map, fixed in the final commit. All 54 mutants compile in both ports and the generated cohort detects every one in both ports. TypeScript's own unit suite additionally detects 44; Go's detects 15 and crashes on 2. Every required detection held in every shard and partial run.policy/independentFailureKeepsSettledLocalValueTest(a source settling with the source error is not a local writer) andlocal-failure/rejectedSourceDoesNotSeedLocalTest(a rejected source seeds nothing). Both replay in both ports.pair returned different values,request pair differs), which carry no expected/actual pair.test/formal-validation.test.tspins 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.MUTATION_ONLY=Mnn make mutations-ts|gomeasures named mutants into a partial report while authoring; both runners and the coverage checker reuse the one catalog check inexecution.mjsinstead of their own loops; the mutation reports gain a Challenges column; the shard-merge tests no longer assume thirteen mutants.node formal/execution.mjs). Ledger pins refreshed textually.What it establishes
62 challenges now have a native twin in each port that the generated corpus detects. The two unobservable challenges (late memoization into a closed scope) name the port line and the read-side closure check that hides the fault; measured once while authoring, the edit survived every history in both ports. The six model-only explanations name the model construct and the port code that makes the fault inexpressible (owner tables the ports do not have, settlement stamps the ports do not record, failed-read and failed-write seams that yield no value). Of the two backlog challenges, the watermark cutoff lives only in the Lua invalidation script, which no in-process cohort executes; the buffer limit has client-side lines in both ports but no generated history reaches the maximum buffer, so a mapped mutant would lack its required detection until a profile exposes the buffer.
Extensibility
Adding a behavior now requires a challenge with native mutants in both ports or an enumerated explanation;
node formal/execution.mjsfails otherwise and the backlog cannot grow. The steps are in AUTHORING.md under "Codifying the next behavior" and "Mapping every challenge to native mutants".Review
Round two (seven lanes plus holistic) accepted: one catalog file with per-port sections instead of two files kept in lockstep; the port-side account moved once onto each entry's
rationaleand every challenge text cut to the model-side identity under a length ceiling (the texts had grown to 53 KB of code quotes that no check could keep current); anchor checking split out of manifest validation so the Quint lanes never read port text; per-mutantcrashedrecords in both ports, including noncompiling mutants, so one mutant cannot take a shard down; M17 and M34 texts that still described the deleted skip declaration corrected; the M33 texts corrected once more (the effects profile replays through the same behavior driver as the features and mocks the perf_hooks clock, so the anchor is the history clock; only the core driver pins it to 0); TypeScriptordinaryno longer required for the new mutants (it was set from one observation of the unit suite); the Go slow-class cost constant raised to 3.5 minutes; the unmapped-mutant count no longer pinned as an id list. Rejected or deferred: droppingportablefrom every required list (pre-existing convention), report-size changes, a setup-time term in the shard budget.Round three (seven lanes plus holistic) found only low items, applied as a final commit: the TypeScript report fingerprints only
src/files; the shard merge gates through the shared catalog reader; the detection scorers take their cohort lists from the port registry; a partial run exits nonzero when a selected mutant loses a required detection; a compile step that could not run is infrastructure rather than a noncompiling mutant; a Go cohort that hits thego testtimeout ends the shard as the budget assumes. The hosted run on the round-two head exposed one nondeterministic mutant: M20's Go edit shared the process flight map across instances without a common lock and crashed a shard with a concurrent map write; it now shares one package-level lock for process flights and was re-measured.Review rounds and the hosted full run are recorded below as they complete.
Witnesses for every semantic case
Before this series, 15 semantic cases in
formal/semantic-cases.jsonhad exported regressions but no required sampled witness, so nothing checked that generated histories reach them andcheck-go-parityreported them aswithoutRequiredGeneratedWitnesses. Each now names at least one generated witness that the sampled corpus must produce:trackedLocalOnlyWitnesses(path, steps, recorder)and the branch that read private predictions is deleted.later-source-survives-earlier-deadlineandlater-source-expires-at-own-deadline, from a newsourceBudgetWitnessesclassifier.Every classifier reads inputs and public observations (
s.o) only. The registryformal/coverage-witnesses.jsongrows by five labels to 440, appended in place because its order is a GoDeepEqualcontract.check-go-paritynow reports 240 cases with required generated witnesses and none without; 306 labels are cited by a case. Two new fixture recipes (test/fixtures/layers-witnesses.json,test/fixtures/independent-witnesses.json; the lock now pins 30 artifacts and 148 histories) give each new label a committed history with a test, and the witness baseline (seed 0xd1a1ca) is re-recorded so the strict gate sees the new labels.Settlement contract, checked
The
causally-ready-v1contract, which every driver must satisfy before it reports an observation, existed only as prose; the only executable control was a no-settle test per port. It is now checked by the coordinator on every behaviorobserve:{ elapsedMs, runnable, held }to each observation: its controlled monotonic clock, what one zero-time verification drain found after the snapshot, and the loader, adapter and scope gates it still holds.preparenames the receipt definition (settlementReceipt, ornullfor core and local-clock), so a port knows what to send and validates it locally, as both transports do.formal/replay/settlement.mjskeeps, per session, the commands the coordinator issued and derives what the schedule requires: R2runnable === 0; R3elapsedMs = Σ advance + loaders × sourceWorkMs + comparisons × comparisonMs; R4environment.wallMs = 1788868800000 + Σ advance + Σ shiftWall + the same work; R5 held gates by kind. 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. Core sessions carry no receipt and are held to R4 alone (advanceWall); the local-clock driver's process clock is unconstrained.Missing settlement receipt,Unexpected settlement receipt,Malformed settlement receipt at receipt.<path>orSettlement violation: <rule>, before the observation compare and without comparison markers. Both mutation runners record a settlement violation under a mutant as a crashed cohort naming the history and rule, so the required-detection gate fails by mutant id while the rest of the shard is measured, and an unsettled driver can never earn mutation credit. The ledger attributes held gates per observation interval and refuses, as its own limit, a schedule whose hold change follows an effect-starting command in one interval.BehaviorDrivercomputes the receipt at the end ofapply(settle drain, snapshot, one more zero-time drain;runnableis 1 if the observation changed plus the pending fake-timer delta). The GobehaviorDriverdoes the same undersynctest(deferred functions found aftersynctest.Wait, plus 1 if the observation changed). Both no-settle controls are rewritten: skipping the drain must fail the smoke history of every behavior-driver profile (all thirteen) with a settlement violation, never an observation mismatch, and each control logs its first-detection step per profile.-raceover the CI corpus all pass with the receipt required. The first hosted run on the receipt commit (35400216841) failed one TypeScript mutation shard and thereby found a driver defect: under M37, which publishes a rejected source's error object into local storage, six shadow-layers histories reported one runnable task although nothing had run, because the driver snapshotted withstructuredClone(which keeps fewer members of anErrorthan JSON does) and compared it against the JSON of the live observation. The snapshot is now the JSON text that crosses the wire (16559e1); under M37 those histories fail as observation mismatches, the detection the catalog requires. The hosted runs on 16559e1 (35402562963), e3bb674 (35404844418), dd3d2ce (35407448531) and c16990a (35409976443) are green on all sixteen mutation shards, both merges and both parity jobs; run 35411849865 on the final head (cad8afa, a one-line regex change in the Go runner) is green as well.runnableis an attestation, timer delivery is checked by the next observation, core is held to R4 alone) and the acceptance requirement for a third port's control.protocol.schema.jsongains$defs/settlementReceipt, the preparereceiptmember and the observereceiptmember with one sentence per rule.Files under
go/changed are test drivers and transport (*_test.go) only; no library code undergo/orsrc/changes.Review of the witness and settlement commits
Round four (seven lanes plus holistic; correctness and contracts clean) found the snapshot-encoding defect the hosted run had already exposed, and the following, all applied: a settlement violation under a mutant is recorded against that mutant instead of stopping the lane; the ledger's per-interval attribution of held gates is stated in PORTING.md and enforced by refusing a hold change that follows an effect-starting command; the coordinator checks that a binding with a receipt controls its wall clock; the TypeScript transport no longer duplicates the coordinator's presence and shape checks, and PORTING.md again names the Go transport as the one that validates locally; the Go mutation-evidence test drops a PATH-level node shim whose one assertion a unit test already made; a driver control pins that an Error instance handed back as a call value reports nothing runnable; the layers witness test gains one negative per clause; the replay suites take one snapshot per step (the receipt adds one verification drain and one encoding per step, about a third more replay time per mutant, which no timeout approaches); AUTHORING.md says what a new profile or held effect kind must touch. Left as is: the observe request's
receiptstays optional in the JSON schema (the coordinator enforces presence per binding so the error names the member); the Go transport accepts a null receipt on a behavior prepare, which the coordinator never sends; the independent source-budget classifier throws on a contradiction rather than dropping credit.Round five (confirmation; correctness, reliability and performance clean) found low items, all applied: portable evidence is composed once for both runners and left unmeasured when either component is, so a settlement violation in the generated cohort no longer leaves portable reading from the fixed cohort alone; the two binding fields for the settlement check became one; the independent source-deadline classifier reads its budget from the profile instead of a copy and is named for its profile; the driver records what its verification drain changed and the harness and transport append it to a violation; new controls pin the independence clauses of the two source-deadline witnesses, the fixture work terms of both clocks through the real driver, and the timer term of the quiescence attestation; PORTING.md states the fake-timer parking limit (a zero-delay timer scheduled during a tick is due one millisecond later, so
runnabletruthfully reads 0 for work parked there) and that the schema file, not the version constant, is the compatibility unit.Round six (confirmation; correctness, performance and holistic clean) converged on one item, applied: the settlement-violation matcher both mutation runners use is exported from the ledger module beside the texts it matches, the coordinator test checks every rule text against it, and both runner tests check that the bare phrase or a printed expectation regex is not a violation; the Go driver now carries the same drain diagnostic as the TypeScript one and its control requires it.
Round seven (confirmation; six lanes clean) left two low items: the Go runner's violation-line capture is now one anchored per-line regex at module scope (applied), and the two direct TypeScript replay loops still each own the ledger lifecycle and marker discipline (deferred, see below).
Composition: held remote I/O and the independent profile
The remaining remote profiles hold their reads, decodes, dumps and writes as external gates the drivers release by index. This series states those rules once in the kernel library and composes the first consumer:
scratchpaddesign record on request).remote_iois a variant family over the layered shape with pending-only held records (a read carries its effect index, its flight and the reply's effective TTLs; a decode its index, flight, TTLs, value and whether it recovers); every held read registers its flight at dispatch so followers join a pending read; loader ordinals map to flights; the drivers' io channel is written by the transitions that hold each fact.recoveryis a consulted record: a snapshot retained at read settlement from the classifier passed there.deadlinesbecomes one pending-only list of due instants delivered by an instant-ordered fold instantiated inside the kernel, with late arrival as one judgment and no drain at expiry.servingexposes the release judged with the remote layer unobserved, the shared prologue, completion split from the result record, warming, publication and source authority with an explicit fence;remote_framesstates the C58 rule (a visible but declined frame yields no fence). The composition lint reports an operator a profile passes to a kernel definition. Sixteen kernel fixture runs pin the seams. The five already composed profiles replay their corpora step-identically in both directions at unchanged bytes per state (source-budgets x1.010 for its new field).Review of the seam (round eight, seven lanes plus holistic) found one high item, a held reply that leaves the remote layer off started a source without a loader ordinal; two medium, the lint's operator rule only caught a literal lambda, and one challenge anchor had drifted onto property history; and low items (dead definitions after the split, a duplicate classifier code, single-statement clean-ups, more fixture runs, and fixture pins for the C58 rule that no composed corpus can observe). The fixes landed as a19e1c5: one loader-mapping helper on every held start with a per-step fixture invariant; the lint reports any operator a profile passes to the kernel (literal, named, let-bound or forwarded); the C23 challenge anchored on the deadline rule with the source-connection monitor checking a pending deadline against its origin; two frame-clock runs pinning the atomic C58 rule; the dead and duplicate definitions removed; seven more fixture runs; a new exported regression for the loader a read expiry starts; and the kernel fixture checker matching declared runs in batches. Round nine (composition plus fixes) was clean on correctness and reliability; its items landed as ff5c1dd: the lint judges operator arguments from the kernel's declared parameter types, the fixture checker runs under Quint's own selection with the Test-suffix rule, the timeout classifier is pinned, the unread held begin is gone. Round ten was clean on correctness, architecture and performance; its low items landed as 0135f49: alias-typed operator positions and aliased kernel callees resolved in the lint, a redundant recovery helper removed, and an exported regression that replays the unfenced refill after a failed decode in both ports. Hosted full runs are green on a19e1c5 (35442599999), ff5c1dd (35446071419) and 0135f49 (35448859364). The differential lane's budget is an hour as of 2de6dc1: six composed profiles replaying both ways after a kernel change took about 35 minutes on the hosted runner, and the lane needs sharding before many more profiles compose.
Composition: the recovery-read profile
The seventh composed profile, landed as two kernel commits, a merge of main, and the composition:
payloadsholds the drivers' enveloped payload codes (100 and up: compressed, corrupt, unsupported encoding) withvalueOf,readFails,decodeFailsanddecodeOutcome;remote_frames::observejudges a frame's code once for the atomic release and the held read, so "an unsupported encoding fails the read" is stated once for both paths andserving::judgeReleasecarriesreadOkfrom that judgment.remote_framesowns the tracked one-hour cap (TRACKED_RETENTION_CAP_MS,physicalRetention) thatserving::authorityapplies to the retention a refill is written with while the recovery snapshot keeps the reply's logical maximum.remote_iogainsbegin(admission and held release in one step) and the latest-effect judgments. Review found one hole before landing: a code in the band naming no class was admitted as a recovery candidate and completed its caller withNO_VALUE, the integerCALL_PENDINGshares;recovery::retainnow admits a candidate only when its code decodes to a value. Fixturepayload-classes(17 runs) pins the three classes on both paths, the documented atomic-path limit for a corrupt frame, and the cap against the uncapped snapshot maximum.Serving::invalidateowns all three outcome codes of the drivers' write-fault switch (missing_remote,mutation_errorwith the invalidation counted and the watermark unmoved,ok);Serving::maintainsis the one judgment a marker lifetime reads. No composed corpus reaches the new branch (policy has 11,351 write-failed states and no invalidation; layers and independent invalidate 4,767 and 5,071 times with the fault never on).go/cache.gotogo/engine.go), each anchor matching exactly once, every Go mutant compile-checked and its detection replayed against main's tree.formal/go-mutations.jsonstays deleted; main's own copy carried a non-compiling M11 after the reshape, which the single catalog fixes. The M20 mutant has a pre-existing read of the shared flight map under the instance lock while the mutant mutates it under the shared one; the lane runs without-raceand no hosted shard has hit it.remote_io::begin, the held settlements through thecompressionvariants,markers::advance/invalidate/observe,remote_frames::seedAged/storeFrame,serving::closeScope, the latest-effect judgments); lint 0 violations, was 80. Two new kernel modules land with their composer:markers(a marker's lifetime ismax(2 x cap, cutoff - wall + cap + margin); its expiry is a time transition that zeroes the watermark, sofenceClearedandmissFencekeep reading the raw watermark and no layered profile carries a lifetime field) andcompression(two variants of the held settlements that append the decode outcome the drivers report). The unsafe fixture stamp is stored literally throughstoreFrame(the age rules reject it natively: visible, never fresh, no candidate, unfenced refill), and the unsupported frame version is seeded as absence, so neither needs a kernel class. Eight profile invariants (three verbatim, three restated over library records,oneExecutionandexpiredMarkersFenceNothingnew) and five connection invariants replace the old nine; the receipt invariants became one-step connection clauses. 34 regressions: 26 ported (20 verbatim) and 8 new (five from the design, three from review: the unsupported-version fenced miss, the encoding-failed read leaving no candidate, the lapsed marker un-fencing the frame stamped at its cutoff), each passing on the old text too. Four challenges re-anchored on kernel text with reproducers, a new challenge for the tracked cap mapped to new mutant M56 (detected in the generated cohort of both ports), five reproducer partitions joined, four exclusions rewritten to true statements. Differential against the old text: every sampled history and every regression agrees both ways (forward 282/282, reverse 287/287 at the composition; 289/289 and 290/290 at the final head), bytes per state x1.133 (bound x1.2); the six other composed profiles unmoved at x1.000 both ways after every kernel commit.Counts after this series: 7 of 15 profiles composed; 21 kernel modules; 9 kernel fixtures (107 runs); 431 scheduled regressions, 221 invariants, 267 exported regressions, 73 challenges (67 distinct faults), 20 reproducers, backlog 53, 63 mapped native mutants over 55 (M56 new, required in the generated and portable cohorts of both ports).
Review of the recovery-read slice. Each kernel commit and the composition were verified by a three-lens pass (design conformance, adversarial semantics, ledger integrity) before landing; the K1 pass found a real hole, a payload code naming no class admitted as a recovery candidate and completing its caller with
NO_VALUE(the integerCALL_PENDINGshares), fixed inrecovery::retainbefore the commit landed. Round one of the slice review (six lanes plus holistic at 20b9159; correctness and reliability clean) converged on improvements landed as cd28a96: the remote observation record carried through the layered release andstartSourceinstead of three flattened booleans (deletingReadSettlementand an always-false argument); the payload band re-encoded as class hundreds plus value so the shadow slice's representations add no constants; the recovery connection monitor stated over raw storage fields, its no-publication clause comparing local expiry and LRU beside the value (a same-value re-warm was invisible), two duplicated clauses hoisted, the new invariants cited in the ledgers, and a regression pinning the unsupported-version fenced miss in both ports. Round two (fresh reviewers at cd28a96; correctness clean) found the one defect of the slice: the pull-request CI's TypeScript job had gone red because one manifest-validation test re-scanned every model source about thirty times and crossed vitest's five-second default on the hosted runner once the slice added five reproducers with fifteen-profile partitions; e961635 memoizes the scans per validation pass (the test runs in 0.4 s under coverage, was 1.7 s locally and 5.7 s hosted) and gives the two manifest tests an explicit budget, and also states the read-settlement clause both ways (it now catches a kernel that serves an expired or fenced frame at equality), pins the encoding-failed read as an exported regression, pins the bare class code's routing, deletes an unused import, cites Go and TypeScript symbols instead of line numbers in the kernel comments this slice wrote, and gives the watermark's zero baseline one owner (Remote::clearWatermark). Rejected on purpose: encoding the unsafe fixture stamp as a far-future age (the literal stamp is the drivers' vector), computing the recovery decode's failure once above the branch (moves a challenge anchor), deleting the atomic-path limit for a fresh corrupt frame through adecodesfact (a design change for the shadow and admission slices), and a Go unit test for the tracked clamp (go/*_test.go is outside this slice). Round three (fresh reviewers at 1937249; correctness, architecture and reliability clean) left four low items landed as 9d64a88: an exported regression pinning the lapsed marker's un-fencing in both ports, a duplicated fixture pin deleted, M56 required in the portable cohort like every peer, and a header pointer corrected. Round four (fresh reviewers at 9d64a88): six lanes clean; the holistic pass raised one low improvement, a connection clause monitoring recovery candidacy against the raw observability the monitor already restates, which is recorded under "Not in this PR" for the recovery slice (it reworks the same monitor) rather than landed here. The review is clean at 9d64a88; the pull-request CI and the hosted full runs are green on every head of the series.Composition: the shadow-layers profile
The eighth composed profile, two commits plus one review fix:
serving::releaseJudgedapplies a release judgment made bylayeredRelease, so a variant that records beside the release (receipts,remote_writes,shadow) judges once and applies the same judgment;serving::startDetachedSourceoverflights::registerDetachedregisters a source no caller owns (a served hit's diagnostic source);deadlinesis retyped overScheduled(the clock and the pending deadlines) so a module that bounds work of its own kind composes it without a source budget;recovery::failureis the failure judgmentremote_ioandremote_writesboth consult.remote_writes(the atomic layered release with held dump and write refills and stale-on-error on the atomic path) andshadow(the job registry: per-instance capacity, dark and served jobs, the 60 s budget throughdeadlines, cohort boundaries, captured fill authority throughserving::authorityso the tracked cap applies). Six library transitions and nothing else; lint 0, was 98. Twelve profile invariants (two verbatim, seven restated over library records, three new) and a five-clause connection model replace the fourteen; 22 regressions ported plus one pinning the exclusive local expiry; two challenges re-anchored on kernel text with reproducers. Differential against the old text: forward 278/278, reverse 279/279, bytes per state x0.929 (bound x1.2); the seven other composed profiles unmoved.redis_error, with the confirmation read ignoring the fault switch. Both corrected and pinned in the shadow-jobs fixture (21 runs), together with the low items:remote_writes::begin/releasedeleted (no consumer), the deadline kind table owned bydeadlinesalone,recovery::failurerecording the miss itself, a BYPASS reply admitting no shadow work, deterministic regressions for thematchandsupersededoutcomes (25 regressions), and a false rationale removed from the local-expiry regression. Deferred as follow-ups: thejobsOfset as an optional index; served jobs' captured but unused fill retention.Counts after this series: 8 of 15 profiles composed; 23 kernel modules; 10 kernel fixtures (129 runs); 434 scheduled regressions, 224 invariants, 270 exported regressions, 73 challenges, 22 reproducers, backlog 51.
Slimming the apparatus
A three-auditor pass over this PR and the formal tree (artifacts, ledgers, code) found the bloat where the line count suggested it was not: of the PR's 28k added lines, 60% were two pretty-printed witness fixtures and 14% were ledger rows a checker recomputes; the kernel is 2,455 lines with no dead text. The first slimming wave landed as seven commits (the seventh compares the exported regression list as a set when the differential judges an identical closure, so the hosted lane skips unchanged profiles against a pre-wave reference):
formal/compact-json.mjs), pinned in the fixture lock: 186,747 lines become 5,138, JSON values identical, every TypeScript and Go reader unchanged except one Go negative-control test that edited the pretty-printed text and now compacts it first (go/core_replay_test.go).regressions,replayRegressionsandlibrariesare derived from the Quint text (every run ending inTest; public-only runs for replay; every source no model claims, each reached by a scheduled model, any other Quint file refused); the manifest lost 839 lines and a regression is scheduled by writing it. Readers in both ports follow (go/feature_replay_test.go globs the exported regressions; go/witness_evidence_test.go derives the library list).differential.maxBytesPerStateRatio; the differential applies and names it. The recovery and local-failure compositions declare one: their old texts are the thinnest profiles in the tree and the shared kernel shapes have a structural floor above x1.2.The second slimming wave landed as four commits. go-parity.json (fa27569) keeps only its hand-written content, about 5,100 lines instead of 19,900: the per-case Quint citations, the source declaration inventory, the reviewed-file audit rows and the whole per-profile section are derived at check time from semantic-cases, the manifest, the profiles registry, source-audit and the sources themselves, and the checker fails by name when any derived fact drifts (each derivation was mutation-tested). quint-case-audit.json is folded into semantic-cases.json (2dc8099): a case cites its Quint checks as
{ ref, scope }rows, the scope is mandatory and validated structurally, and the shared disclaimer is stated once in the guide; 4,400 hand-edited lines gone. The witness fidelity scaffold the independent, policy and recovery classifiers each carried is one module,formal/replay/witnesses/fidelity.mjs(ca4354a), label-for-label identical over the recorded corpora. The composition lint judges higher-order kernel definitions by a computed denylist (56bb2bb, b1b5c83): the alias walk was cut to the two load-bearing cases the verification found it still needed (an operator parameter typed through an alias, and a kernel transition applied through a profile alias, both pinned by fixtures again), the baseline is unchanged, and every construct the earlier fixtures pinned is still reported. The fifth item, kernelinitial(...)constructors for the composed shapes, is not expressible in Quint 0.32.0: a record spread cannot add fields, a row-polymorphic return type is refused as too general, andinitcannot read a carrier state; the profiles keep their init literals.Net for the two waves: about 210,000 lines removed from the tree against the pre-slimming head. Verified: audit, fixtures-check, the 54 formal test files,
make check-ts,make check-go; the hosted lanes run on the pushed head. Remaining follow-ups from the audit: aformal/pins.jsonmanifest replacing the hand-typed sha pins (then the last mirrored rows of go-parity.json); the settlement ledger and the two connection models whose anchored faults are all caught elsewhere (effects-connection goes with the effects slice); the two remaining witness-fixture pairs merged per profile.Composition: the recovery profile
The ninth composed profile (lane A), two commits:
remote_io::settleDispatchedsettles a read in the step that dispatched it, taking the shape's read-fault switch;releaseJudgedsplits the held release from its judgment;beginReadopens a call whose reply dispatches at once;deadlinesmirrors the three under a budget (a dispatched read registers no read deadline under an unbounded budget);diagnosticsgains the held lifecycle's channel (layer and scope attribution, age records, the settlement and expiry variants); fixtureheld-diagnostics(16 runs).formal/dialcache-recovery-connection.qnt(it takes the name; recovery-read's monitor is renameddialcache-recovery-read-connection.qnt; the legacy monitor is deleted). The monitor carries the candidate-window clause recorded as a follow-up from the recovery-read review. The old text is the thinnest profile in the tree (1,544 bytes per state) and any composition over the shared held-path shape has a floor near x1.7, so the profile declares a bytes bound of 1.85 (measured x1.79; the corpus is about 85 MB). Differential against the old text: forward 542/542, reverse 542/542. Challenges:recovery-strands-followersre-anchored on kernel text,recovery-connection-inclusive-maximumon the monitor with a reproducer, the legacy challenge deleted with recovery joiningprofile-recovery-wrong-snapshot; six partitions joined. The witness classifier reads inputs and public observations only (63 labels, counts identical on the recorded corpus) and refuses a history in the retired layout by name.Review: one round (six lanes plus holistic) with correctness and contracts clean and low items only; landed as a hygiene commit (the uncalled
remote_io::settleDispatched/beginReadpair deleted,Diagnostics::attributedfolded away, the prepare test given an explicit budget, the record row citing the landed kernel commit). Recorded follow-ups: two exclusions justified by corpus absence deserve regressions; the finite and zero read-budget paths ofsettleDispatchedare unpinned; a classifier fidelity-divergence unit test;beginRead's budget parameter has one truthful value; two witness test files share plumbing that belongs in one helper; the held diagnosed variants widen the scope profile's import closure; aretainedSnapshotsPersistmonitor clause; delete the 1.85 declaration in the first PR after this one merges.Composition: local-failure and local-clock
The tenth and eleventh composed profiles (lane B, merged from
claude/fault-map-lane-b), two commits:clock::advanceTicksprojecting native ticks onto the whole-millisecond grid, overcache_rules.wholeMs), an inline local call (serving::beginLocal/callLocal), the newest source (flights::latest), instance construction (instances::construct), and a layout fact: a policy call is counted only when the scope is open and the layout has a provider. The local-clock old text's public action is renamed so the profile can be replayed; the differential learns a per-profile action binding for a renamed public action and validates the working tree's manifest as written.local_faultswithdraws the reply's local TTL under a local read fault and the source's captured TTL at settlement; lint 24 to 0 and 11 to 0; five and four regressions verbatim; four challenges re-anchored on kernel text with measured fifteen-profile partitions; thirty exclusion reasons restated after a review found them stale (the composed profiles now reach faults the old texts could not). local-failure declares a bytes bound of 1.45 (measured x1.40: the profile owns 43 bytes per state; the layered shape's remote fields and registries on a 1,056-byte base account for the rest); local-clock measures x0.63. Differentials: 133/133 and 132/132 both ways. core stays uncomposed: both ports' core replay drivers read the model's private state by name and its loader values collide with kernel outcome codes; a later slice may rewrite the two drivers to the public observation record.Review: one round (six lanes plus holistic), correctness and reliability clean; two medium items fixed before the merge: the local read fault was stated as a TTL withdrawal through the gate, which also switched off layer participation and sharing (the implementation decides coalescing from configuration and a failed read only skips the local value), now a judgment argument (
serving::judgeReleaseUnder) with no new state field and the nine other composed profiles exactly unchanged; and the recipe-side action binding in the fixture generator, dead since the rename, deleted. Recorded follow-ups: a per-fill grid instant so the local-clock invariant, not only its regression, rejects a renewed insertion; delete the differential's transitional action binding once the merge base with main carries the renamed text; a lint environment allowance replacinginstances::constructandrequest_memo::openScope; receipted faults so local-failure states storage identity under a fault as an invariant.Composition: the admission profile
The twelfth composed profile (lane B, merged from
claude/fault-map-lane-b), one commit:shadowmodule gains the held shape it lacked: a job registry over the held read (capture,beginHeld,releaseHeld, thesettleRead/settleLoad/settleLoadersettlements,admitServed,busy,confirmation) underLimits(capacity and budget) andShadowing;remote_io::holdReadis factored out of the dispatched read. Fixtureheld-shadow(13 runs). The profile keeps six library transitions and nothing else; lint 0, was 65. Eight regressions and eight invariants; the duplicate-key and capacity challenges re-anchor onshadow::busy(the duplicate-key reproducer leaves the grandfathered backlog). Differential against the old text: forward 134/134, reverse 136/136; bytes x1.62 under a declared 1.65 (the held registry rows sit on the shared layered shape). The witness classifier reads inputs and public observations through the shared fidelity scaffold (18 labels, counts identical on the recorded corpus).Review: one round (semantics and conformance; ledgers and integrity), one low item fixed before the merge (the effects invariant had dropped the read and decode count identities the old text stated; restored) and re-verified clean. The merge onto the lint fix resolved without conflicts; no baseline, pin or lock needed regeneration.
Counts after this series: 12 of 15 profiles composed; 14 kernel fixtures (166 runs); 436 scheduled regressions, 233 invariants, 272 exported histories.
Composition: the shadow profile
The thirteenth composed profile (lane B, merged from
claude/fault-map-lane-b), two commits:remote_iorules as a caller's; the payload forms (PADDED,UNICODE,BINARY) are spelled once inpayloadsand classified over the bytes; the invalidation watermark takes a buffer argument (raiseWatermark/invalidate(state, entity, bufferMs), existing call sites pass 0); the job registry is pending-only, so finished jobs leave it and shadow-layers' bytes fall 10 percent, admission's 4 percent. The verify pass found a gap the old texts never reached: a caller's source deadline did not end a waiting dark job, so the job's label depended on whether its read had settled first. The kernel now ends the job at the source deadline, pinned by a fixture run. Kernel fixtures: 15 files, 170 runs.formal/dialcache-shadow-validation.qntis retired: its two challenges re-anchor on kernel text (shadow-fenced-fill-writesonremote_writes::dispatch,shadow-fill-before-sourceon the dark read's wait) with new invariants and reproducers, andshadow-inclusive-c0-freshnessre-anchors onshadow::acquired; shadow joins three partitions; the backlog loses two ids. Differential against the old text: forward 1031/1031, reverse 1063/1063; bytes x1.79 under a declared 1.8 (each job's held read and decode carry their own records; the tightest transitional margin so far, deterministic under the manifest seed). The public classifier replaces the private-state one and the recovery-shadow variant (77 labels, counts identical on the recorded corpus); the six excerpt fixtures become full public histories.Review: one round, both lenses clean (semantics and conformance; ledgers and integrity). Open questions recorded as follow-ups: a pre-existing classifier rule credits a superseded frame that carries the C0's bytes but is fenced; three exclusion texts describe the profile's recovery mode loosely.
Counts after this series: 13 of 15 profiles composed; 32 models; 15 kernel fixtures (170 runs); 425 scheduled regressions, 227 invariants, 304 exported histories.
Composition: the effects profile
The fourteenth and last composed profile (lane C, merged from
claude/fault-map-effects; core stays uncomposed by decision because both ports' core drivers read the model's private state), two commits:remote_io::settleObservedapplies a held read settlement from a judgment already made andstartLoaderFencedtakes the fence as an argument, so the read settlement and its judgment are separable;deadlines::settleObservedis the budgeted variant;remote_writesgains the held refill over the held read path (HeldWriting,settleLoader) and the wall clock a pre-serialization fence check sampled (HeldDump.sampled, 4 bytes per state in shadow-layers);diagnostics::beginlabels an admission and its held release from the judgment. The future-buffer invalidation is reused from the shadow slice, not re-added.adapter_replies(the queued adapter reply normalized once) andmetrics(the ordered metric events as metered variants over the diagnosed held shape); fixtureheld-writes(19 runs). Fifteen library transitions and nothing else; lint 0. Forty-eight public regressions (the forty-two old exports plus six ported to public inputs) and ten invariants.formal/dialcache-flight-deadlines.qntandformal/dialcache-effects-connection.qntare retired: their challenges re-anchor on kernel text with reproducers, and the backlog loses five ids. Differential against the old text: forward 554/554, reverse 560/560; bytes x1.43 under a declared 1.45. The effects driver becomes public-only (it reads the observation record, the I/O record and the event list; the shared codes are mapped once) and its classifier binds through the fidelity scaffold (93 required labels, none missing); the retired-layout parser branch stays, marked transitional, until the hosted corpus is regenerated.Review: one round, both lenses clean of material findings; two low items were taken before landing.
metrics::missReasonreported a stale frame-class adapter reply's miss asunclassifiedwhere both ports reportexpired, unreachable at the profile's 600 ms horizon; 070e42f mirrors the stored-frame arm (the rule now lives in one helper) and adds two fixture runs pinning the inclusive fresh-age boundary from both sides and the future-dated case. The composed effects text samples a different corpus at the pinned seed (74 of 93 label counts moved; the both-way differential is the equivalence evidence); the kernel README records it, and BEHAVIOR.md's stale witness count is corrected in the same commit.The smoke lane's differential job runs as four shards (84fccb1:
--shard=<index>/<count>on the differential,DIFFERENTIAL_SHARDin the validation plan, a workflow matrix): with fourteen composed corpora one runner no longer finished inside its hour.Counts after this series: 14 of 15 profiles composed (core excluded by decision); 30 models; 29 kernel modules; 16 kernel fixtures (189 runs); 413 scheduled regressions, 213 invariants, 310 exported histories; 70 challenges, 33 with deterministic reproducers, backlog 37 (was 51 at the start of the composition series).
Not in this PR
different-bytes-same-value-supersededcredits a supersession whose frame carries the C0's bytes but is fenced; three exclusion texts describe the shadow profile's recovery mode loosely; recovery-read's public-observation witness rules match exact command prefixes of the named regressions, so every label records zero sampled hits; the tracked one-hour clamp has no Go unit test (the Goordinarycohort survives M56; the generated and portable cohorts detect it).integrationcohort (real Redis) for the Lua cutoff challenge, and a profile input for the future buffer so the buffer-limit challenge can be mapped.accepted()guard where a decoded payload value is warmed or served (valueOf(COMPRESSED + 3)would equalSOURCE_ERROR); unreachable for every scheduled profile today.