test: add witness provenance, challenge reproducers, and a profile lint baseline (#165 step 2) - #170
Merged
Merged
Conversation
…klog Implements evidence guarantee 2 of #165: "A deterministic reproducer for each new challenge. Random exploration discovers distinguishing histories; preserving them keeps a known fault detected regardless of seed. Every new model challenge carries a checked mapping: the contract and fault family, the applicable profiles, a distinguishing public-input history, the expected property or observation failure, and explicit exclusions saying why other profiles cannot exercise the fault. For a portable behavior fault the reproducer is an exported public regression that both ports replay; for a fault in model-only instrumentation it is a deterministic model-level run with its scope and the reason it has no native counterpart documented. Each reproducer passes on the clean baseline and fails under the challenge for the intended semantic reason. Existing challenges are backfilled as their models are touched; the remaining backlog is reported and is not a prerequisite for the pilot." A challenge may carry `reproducer: { kind, run, family, profiles, exclusions, scope? }`. `execution.mjs` requires an exported-regression to cite an exported public-only run of the challenged model and a model-run to cite a scheduled non-exported run with a scope; family and profiles are non-empty, exclusion keys are known profiles, and every challenge either has a reproducer or is listed in the new top-level `reproducerBacklog`, whose size the validation summary reports. `check-model-properties.mjs` replays the cited run with `quint test --max-samples=1 --seed=<manifest seed> --match=^<run>$` on the same source copy as the invariant measurement: the baseline must report the run passed and the mutant must exit 1 and report that run failed; a history the fault does not distinguish is a measurement failure. The report (schema 4) records the outcome and Quint error code per challenge. Seven challenges are backfilled with existing runs verified to distinguish their faults (baseline passed, mutant failed with QNT508 "Expect condition does not hold true"): stale-recovery-future-candidate and envelope-strips-unknown-zero-prefix as model-runs, and source-budgets-accepts-at-deadline-equality, shadow-inclusive-c0-freshness, policy-inclusive-local-expiry, local-clock-precise-ttl and admission-capacity-off-by-one as exported regressions. The other 60 challenges are listed in reproducerBacklog. No model or exported run changed; the fixture lock only refreshes the execution.json/execution.mjs input hashes. AUTHORING.md states the reproducer rules and backlog policy; SEMANTIC-COVERAGE.md and VALIDATION.md point at the reported backlog and carry the current 67/64 challenge counts.
Implement evidence guarantee 6 of issue #165: "Structural enforcement of the thin-profile rule and witness isolation. A lint over Quint's parsed module IR follows resolved references through helpers and operator arguments. Thin-profile rule: from each profile action, the transitive closure of referenced definitions contains no state assignment outside the kernel. Witness isolation: no definition reachable from a cache guard, a cache assignment, a profile init or step, an input-choice domain, an observation projection, or the body of an operator constant bound at instantiation may reference witness state. [...] The lint runs on today's profiles before the pilot; its output on each profile is the list of private transition logic that profile carries, which is that profile's migration work list and the baseline for measuring the kernel's effect." formal/lint-profiles.mjs parses a model with `quint parse --out`, builds the reference graph from the lookup table (definitions, variables, constants and instance overrides as nodes), and reports both rules with the definition chain that reaches each violation. `baseline --write` records, for the 15 conformance profiles with no kernel module, the action count, the definitions reachable from public actions, the state-assigning ones by name and the parse table size; `baseline --check` fails on drift with the changed paths. It is not wired into make audit, which runs without Quint. Synthetic fixtures under test/fixtures/profile-lint prove the lint on a const-configured kernel instance: a clean instance passes both rules, a profile whose wrapper calls a local `decide` helper reports the chain bumpWrapper -> decide for every assigned variable, and three variants name the choice domain, the projection and the guard through which witness state feeds back. Quint 0.32 rejects an operator constant that reads any variable (QNT201) or the state of the instance it configures (QNT099), so the projection variant leaks through the kernel's observation assignment instead.
…aseline Every classifier now credits labels through a recorder that keeps the history and the checkpoint step of each credit, without changing which labels any history earns: over the same pinned-seed corpus the old and new evaluators agree on seen and required for all 14 profiles, and every required label's sampled and regression counts equal the ad-hoc counts recorded for #168. Witness evidence moves to schema 2 with per-label { sampled, regression, traces: [{ name, kind, checkpoints }] } and per-profile diversity counts; the Go replay accepts schema 2 and checks the provenance minimally. formal/witnesses.mjs prints a fragility report, writes witness-report.json next to the corpus, records formal/witness-baseline.json with `baseline --write`, and fails `evaluate` when a gated label's sampled hits drop below half its recorded count. The exploration lane keeps that report in its report.json while still tolerating a witness failure. Implements evidence guarantees 1 and 8 of #165: 1. "Per-label witness provenance. The witness evidence records, for every credited label, the trace identity, whether that trace is a sampled history or a named regression, and the public checkpoint steps that establish its consequence, alongside the aggregate labels and corpus hashes it records today. Sampled and regression counts are reported separately per label, because a regression pins a label regardless of seed while only the sampled count says whether random exploration still finds it." 8. "Corpus diversity signal. From the provenance in guarantee 1, every profile reports distinct action sequences, distinct observation sequences, and per-label hit counts split into sampled and named-regression hits. Once a baseline is recorded in the manifest, a drop in the sampled counts beyond a stated tolerance fails generation, so regression protection and exploration quality stay separately visible." formal/profiles.json replaySources gains recorder.mjs and recorder.d.mts and the generated-fixtures lock is regenerated for that input; the source-audit and go-parity ledgers need their central refresh.
…ogic Review of the lint for evidence guarantee 6 of issue #165: "A lint over Quint's parsed module IR follows resolved references through helpers and operator arguments. [...] Textual checks are not sufficient because private logic can hide behind a helper." A `match` whose arms are actions selects a transition on its scrutinee, so the scrutinee is a guard; the kernel will be sum-typed, making this the common guard shape. The lint reported a witness read there under the bare step root; `matchVariant` now joins the structural combinators and the read is reported as a guard. Eight fixtures pin the routes a profile could use to hide logic from the lint, each with the chain the report must show: an assignment made by a let-bound action two calls deep (settle), an assignment inside a lambda handed to an operator (bumpWrapper), a guard two pure calls deep through an operator argument (screen -> blocked), a choice domain computed by a helper (domain), witness state added to a kernel action's input (the step root itself), a match scrutinee (mode), a profile that shadows the kernel's `room` and `bump` by name (only the local pair is reported, so resolution is by declaration, not name), and an operator constant whose body reads a profile witness variable. Quint rejects the last one at typecheck (QNT201), so it is a parse-only fixture with that reason pinned. Every profile fixture also runs under `quint run`, not only `quint typecheck`.
Review follow-up for the witness provenance slice (#165 guarantees 1 and 8). Guarantee 1 asks for "the public checkpoint steps that establish its consequence": the local-clock shared-instance-grid label credited the last step of the history; it now credits the two calls that observed the paired expirations, and the recorder and PORTING.md no longer describe a whole-history fallback. Guarantee 8 asks that "once a baseline is recorded in the manifest, a drop in the sampled counts beyond a stated tolerance fails generation". The baseline's corpus fingerprint hashed the ITF files byte for byte; Quint stamps #meta with the creation time, so regenerating the pinned seed always reported a different sampled corpus. The fingerprint now covers vars and states only, and the recorded baseline is rewritten with the same counts and the new fingerprints. The Go checker takes each cited history's kind from the corpus directory it replays and requires the sampled and regression counts to match the citations, so relabelled provenance is rejected like a missing label.
…profile Review of the reproducer slice against evidence guarantee 2 of #165 found three places where the manifest carried less than the guarantee asks for. The guarantee says every challenge "carries a checked mapping: the contract and fault family, the applicable profiles, a distinguishing public-input history, the expected property or observation failure, and explicit exclusions saying why other profiles cannot exercise the fault. For a portable behavior fault the reproducer is an exported public regression that both ports replay ... Each reproducer passes on the clean baseline and fails under the challenge for the intended semantic reason." The expected failure was not declared: any failure of the cited run counted, including a step the fault disables. A reproducer now carries `failure`, the condition of one top-level `expect` in the cited run, which `execution.mjs` resolves token by token against the run body. The measurement appends two probes to the cited model, the chain cut before that expect and the chain cut through it, and runs them with the run: all three pass on the baseline; on the mutant the run and the through-probe must fail with "Expect condition does not hold true" while the before-probe still passes. The report records `code` for that checkpoint failure. A shared-library fault could list one profile and no exclusions, so the mapping was unchecked exactly where a fault reaches many profiles. When the mutation source is a library, every known profile must now appear in `profiles` or in `exclusions`. The portable cache-rules fault challenged through the stale-recovery model was cited as a model-run because that model has no exported runs. An exported-regression may now name another profile `model` for a shared-library fault; stale-recovery-future-candidate cites the policy profile's exported wallRollbackRejectsFutureRemoteFrameTest, lists recovery, policy and shadow as observing profiles, and excludes the other twelve with the reason each cannot observe a future stamp. All seven reproducers declare their checkpoint and pass the probe measurement; the full catalog still detects 67 of 67. The scanner keeps string literals as opaque tokens and records token spans so a run can be sliced; tests and AUTHORING.md, SEMANTIC-COVERAGE.md and VALIDATION.md follow. The fixture lock refreshes only the execution.json and execution.mjs input hashes.
…for the evidence slices A label derived from a cumulative public list is credited at every later step of a history; only the first step of each run of consecutive credits establishes the consequence, so the recorder now records that step and skips the continuation. Label sets are unchanged. The source-audit and go-parity ledgers, the fixture lock and the generated artifacts are refreshed for the merged provenance, reproducer and lint slices.
Collapsing consecutive implicit credits dropped the second of two expiring calls in the local-clock expiry label, which are distinct establishing checkpoints. The recorder records every credited step again; compaction for labels derived from cumulative public lists belongs in those classifiers, crediting only when the list grows.
lan17
commented
Sep 12, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
This is a material improvement to the reliability and auditability of the formal evidence, and a useful step toward the layers + effects pilot in #165.
The strongest additions are per-label trace/checkpoint provenance, separate sampled versus regression counts, and reproducers that must fail at a declared expectation rather than earning credit for any failure. The dependency-following lint also provides a concrete baseline for the kernel migration. I compared the main and PR classifiers against the downloaded CI corpus: all 14 witness profiles credit identical label sets. The behavioral coverage is preserved while the supporting evidence becomes more inspectable.
Two enforcement gaps should be tightened before relying on this as the pilot's acceptance gate; details are in the inline comments:
- Fresh-seed sampled-count failures are retained in the report but do not affect exploration's final status. This occurred in the current full CI run, which reports four such failures while passing.
- The requirement that new challenges carry reproducers is documented but not enforced: an arbitrary new challenge can enter the reported backlog and pass validation.
Scope qualifications: seven of 67 challenges now have checked reproducers; retaining the existing 60 as a visible backfill backlog matches the agreed sequence. The sampled-count gate covers 264 of 435 required labels. Five profiles have no gated labels because their required witnesses are supported only by named regressions. Those limits should remain explicit when interpreting green results. The kernel consolidation and the complete linkage between witnesses, faults, and native detecting assertions remain subsequent work.
Validation: local typecheck, 83 focused TypeScript tests, and Go witness tests passed. I inspected the full CI artifacts: all 67 model challenges were detected, all seven reproducers passed on baseline and failed at the declared checkpoint under mutation, and both ports completed their replay. The full run is https://github.com/lan17/DialCache/actions/runs/34685979197; its green exploration status has the qualification above.
I recommend retaining this scope, tightening the two enforcement boundaries, and then proceeding with the agreed two-profile pilot.
…cklog Review of #170 found two enforcement gaps. The exploration lane decided its status from the native replays alone, so a fresh seed whose sampled hits fell below the baseline tolerance was recorded under witnesses.failed and the run still passed; run 34685979197 passed with four such drops. The witness step stays tolerated so both ports replay, and the gate now decides afterwards with the status coverage-gate-failure. The reproducer rule accepted any challenge listed in reproducerBacklog, so a new challenge could opt out by listing itself; the ids allowed in the backlog are now frozen in grandfatheredReproducerBacklog, which only shrinks, and a new listed challenge is rejected. Docs state both, and the fixture lock follows the validator change.
The first two exploration seeds under an effective gate dropped four and five gated labels below half their recorded counts while every label stayed reachable: baselines of ten to thirty vary by a third or more between seeds, so the fixed tolerance fails most fresh seeds on noise. On the recorded corpus the tolerance rule stays exact evidence of a model or classifier change. On any other corpus a gated label now fails only when it also falls more than freshSeedSigma (4) Poisson standard deviations below the recorded count, and always at zero hits. The baseline file records the new constant; PORTING.md and VALIDATION.md state the rule and the data behind it.
The previous commit added the fresh-seed collapse bound but left the type declarations and the committed baseline file behind it, which failed tsc and the gate test. The declarations carry the rule fields and the optional freshCorpus option, the baseline file records freshSeedSigma, and the gate test states the bound as the formula rather than a rounded number.
lan17
commented
Sep 12, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
Re-reviewed the update on claude/formal-evidence-step2 against the previously reviewed revision.
The original backlog finding is resolved: the same in-memory attempt to add a new challenge without a reproducer now fails validation. Recorded sampled-count failures also now propagate after both native replays finish, with the intended coverage-gate-failure status.
The looser fresh-seed threshold is a reasonable heuristic response to the observed variation, provided it remains explicitly scoped to fresh-seed exploration. Two remaining enforcement problems need attention:
- The new rule identifies a fresh seed from a changed corpus fingerprint. A model change generated with the same pinned seed also changes that fingerprint, so it silently receives the weaker threshold precisely when the pilot needs a strict regression check.
- A missing or structurally invalid witness report still defaults to an empty failure list. The evaluator's tolerated failure can therefore disappear from the aggregate if both native reports pass.
Both are reproduced below. These are evidence-gate issues, not observed failures in either native DialCache implementation.
Validation: all 45 tests in the three changed test suites passed, typecheck passed, and the diff is clean. I inspected the full CI artifacts for https://github.com/lan17/DialCache/actions/runs/34714237904: every job passed, all 67 model challenges were detected, and the fresh-seed report completed both ports with no recorded gate failures. The green run does not exercise the two negative cases in the inline findings.
…n without a completed witness report Second review of #170 found two gaps. The fresh-seed collapse rule was selected by corpus-fingerprint inequality, so a model change regenerated under the pinned seed, which also changes the fingerprint, would have been judged by the lenient rule exactly when the strict one is needed. The evaluator now reads the generation seed (QUINT_SEED or the manifest seed, the same variable run-models.mjs uses), the exploration plan passes the seed to the witness step, and the rule follows the seed: tolerance under the recorded seed regardless of fingerprint, collapse under another seed. The fingerprint stays a change signal and the report says when the corpus differs under the recorded seed. Exploration also treated a missing or malformed witness report as a clean gate; it now requires a completed report (schema, command, failed and incomplete arrays, profiles object) after both ports finish and otherwise ends with infrastructure-failure. Tests cover the same-seed model change, the exploration seed, the plan's seeding of the witness step, and missing, empty, wrongly shaped and unreadable reports; the saved-run fixture writes a completed report.
… recorded corpus A local adversarial review of the seed-selected gate found the comparison trusted a raw environment string. The same seed written as 0xD1A1CA or 13738442 selected the exploration rule for the pinned corpus, a stray QUINT_SEED in a shell did the same, and nothing tied the baseline's recorded seed to the manifest. Seeds now compare in one canonical form wherever they enter; a sampled corpus byte-identical to the recorded one is judged strictly whatever the seed claims, and the report records the contradiction; evaluate refuses a baseline recorded under any seed but the manifest's and baseline --write refuses to run under another seed; the mutation lane strips QUINT_SEED before its baseline witness evaluation. Exploration additionally requires the witness report to carry its own seed and cover every scheduled witness profile, keeps a tolerated evaluator failure in its report, and the docs qualify that the infrastructure status applies when both ports passed.
lan17
commented
Sep 12, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
Re-reviewed the latest two updates on claude/formal-evidence-step2. Both findings from my previous review are resolved: pinned-seed corpus changes retain the strict baseline gate, and absent/malformed/wrong-seed/incomplete-profile witness reports no longer produce a successful exploration when both native ports pass.
Two follow-up findings remain inline:
- P2: saved-run replay validates profile completeness against the current checkout instead of the saved snapshot.
- P3: the stale-seed baseline guard also blocks the full rewrite command offered as its recovery path.
Validation: 88 focused tests across witness provenance, exploration, execution, mutation sharding and validation passed locally; TypeScript typecheck passed. I also reproduced the two findings with a saved-run test fixture and the baseline CLI, respectively. Current PR checks are green. The full formal run passed on this head, including 7,254 completion records per native port, mutation jobs, model checks, bounded symbolic checking and a separate fresh-seed exploration.
The fixes strengthen the evidence infrastructure. These remaining issues concern reproducibility and baseline maintenance; this review does not identify a new DialCache runtime behavior defect.
…a full rewrite replace a stale-seed baseline Third review of #170. A saved exploration replayed with --replay was checked for a witness report covering every profile the current checkout schedules, so a profile added after the run was saved made a complete report fail; the expected profiles now come from the snapshot's own manifest and registry, and a snapshot without that inventory is an infrastructure failure rather than a silent fallback. The stale-seed baseline guard also rejected the full rewrite it named as the recovery; evaluation, reporting and partial rewrites still refuse a baseline recorded under another seed, and only baseline --write --profile all, which replaces the file, is exempt. The saved-run fixture now schedules one profile while the checkout schedules fourteen, and the replay test asserts the report was judged against the saved inventory.
lan17
commented
Sep 13, 2026
lan17
left a comment
lan17
left a comment
Owner
Author
There was a problem hiding this comment.
Re-reviewed the latest update: no outstanding findings. All six findings raised across the previous review rounds are resolved. The saved-snapshot replay reproducer now passes, and the full baseline rewrite succeeds while stale partial rewrites and foreign generation seeds remain rejected.
Validation: 89 focused tests and TypeScript typecheck passed locally. All current CI checks are green, including the full formal verification run with both native replays, mutation checks, model checks, symbolic checking and fresh-seed exploration: https://github.com/lan17/DialCache/actions/runs/34719436896.
Ready to merge from a code-review standpoint.
GitHub does not permit an APPROVE review from the PR author's account, so this result is recorded as a comment.
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.
Step 2 of the sequence agreed in #165. None of it depends on the kernel; all of it makes the pilot measurable against tightened evidence. Production code is unchanged in both languages.
1. Per-label witness provenance and the diversity baseline (guarantees 1 and 8)
Every classifier now credits labels through one recorder that keeps, per label, the history that earned it and the checkpoint steps that establish it. The evidence schema moves to version 2:
labels[<label>] = { sampled, regression, traces: [{ name, kind, checkpoints }] }for every credited label, wherekindsays whether the history is a sampled trace or an exported regression, plus per-profilediversitywith distinct action sequences and distinct observation sequences over what the drivers assert. The Go checker requires schema 2, derives each cited history's kind from the corpus layout rather than trusting it, and rejects evidence that omits a required label.formal/witness-baseline.jsonrecords, from the pinned seed, every required label's sampled hit count and a content fingerprint of the sampled corpus.evaluatefails when a label with a baseline of at least 10 sampled hits drops below half of it; labels below that minimum are reported, not gated.evaluateand the newreportcommand print, per profile, the fragile-and-unpinned labels (empty for all 14 profiles), the pinned-but-rare labels, the diversity counts and the baseline findings, and writewitness-report.json; the exploration report carries that seed's copy.Equivalence: on the same regenerated pinned-seed corpus the evaluator from main and this one credit identical label sets for all 14 profiles, and every required label's sampled and regression counts equal the per-history counts computed by hand in #168.
2. Deterministic reproducers for challenges (guarantee 2)
A challenge may carry
reproducer: { kind, run, family, profiles, exclusions, scope? }.exported-regressionrequires a profile model, a run inreplayRegressionsclassified public-only, and noscope;model-runrequires ascopeexplaining why the fault has no native counterpart.profilesmust partition the profiles that import the mutated source: a shared-library fault must list or exclude, with a reason, every profile that imports the library. Every challenge either has a reproducer or is listed inreproducerBacklog, and the validator rejects a challenge in both or in neither.check-model-propertiesruns the cited run on the clean source and on the mutant: it must pass on the baseline and fail on the mutant at its declared checkpoint, proven by appended probe runs, and a run that still passes under the fault is a measurement failure ("this history does not distinguish it").Seven challenges are backfilled with existing runs verified to distinguish their faults, across both kinds and five models; 60 remain in the backlog, reported by
execution.mjs, to be backfilled as their models are touched. One challenge was found to have no distinguishing run today (independent-deadline-settles-at-start) and will need a new public run when backfilled.3. Dependency-following profile lint and its baseline (guarantee 6)
formal/lint-profiles.mjsparses a model withquint parse --out, builds the resolved reference graph from Quint's lookup table, and reports two things. Thin-profile violations: every state assignment reachable from a profile action whose variable or containing definition is outside the named kernel modules, with the chain from the public wrapper. Witness-isolation violations: every reference to a witness variable reachable frominitandstep, guards, cache assignments, choice domains, the observation projection and the bodies of operator constants bound at instantiation, followed through helpers and operator arguments and immune to shadowing. Fifteen synthetic fixtures pin both rules, including private logic hidden two calls deep, inside a lambda passed to an operator, in amatchscrutinee, and behind a shadowed name.formal/profile-lint-baseline.jsonrecords today's 15 profiles with no kernel, so every reachable assignment is private; this is each profile's migration work list.baseline --checkfails on drift.Two Quint 0.32 facts the pilot needs, found while building the lint: an operator constant bound at instantiation must be pure (QNT201), so a projection cannot read state directly and the kernel must apply it; and Quint lets a profile assign an instance's variable from outside (
K::x' = ...typechecks), which is exactly why the thin-profile rule is needed.Review fixes (94b9c46)
The first review found two enforcement gaps, both now closed. Exploration decided its status from the native replays alone, so a fresh seed whose sampled hits fell below the baseline tolerance was recorded under
witnesses.failedwhile the run passed; the first full run of this PR did exactly that with four drops. The witness step stays tolerated so both ports replay, and the gate now decides afterwards with the statuscoverage-gate-failure. The reproducer rule accepted any challenge listed inreproducerBacklog, so a new challenge could opt out by listing itself; the ids allowed in the backlog are now frozen ingrandfatheredReproducerBacklog, which only shrinks, and a new listed challenge is rejected. The first run under the effective gate then failed exploration as designed, and the data showed a calibration problem in the design's fixed tolerance rather than in the fix: fresh seed 0x3dadfe79 dropped five gated labels below half their baseline (for examplereply:45 of a baseline 12,late-shadow-decode-cannot-start-c111 of 30) while every label stayed reachable, on top of four such drops on the previous seed. Baselines of ten to thirty vary by a third or more between seeds, so the tolerance alone fails most fresh seeds on noise. Commits 08e7599 and 5af1dae make the fresh-seed gate a collapse detector: on the recorded corpus the tolerance rule stays exact evidence of a model or classifier change; on any other corpus a gated label fails only when it also falls more thanfreshSeedSigma(4) Poisson standard deviations below the recorded count, and always at zero hits. Under that rule neither fresh seed would have failed, both reports still list every drop, and a collapsed label still fails the lane. The constants are recorded in the baseline file and are the obvious thing to revisit once more seeds have accumulated.Second-round fixes (5b3755f)
The second review found that the fresh-seed collapse rule was selected by corpus-fingerprint inequality, so a model change regenerated under the pinned seed, which also changes the fingerprint, would have been judged leniently exactly when strictness matters. The rule now follows the generation seed, read from the same variable
run-models.mjsgenerates with and passed to the witness step by the exploration plan; a fingerprint mismatch under the recorded seed is reported as a model or classifier change and judged by the strict rule. The review also found that a missing or malformed witness report read as a clean gate; exploration now requires a completed report after both ports finish and otherwise ends withinfrastructure-failure. A local adversarial pass on those fixes (1c2b479) then hardened them: seeds compare in one canonical form, a byte-identical corpus is always judged strictly and a contradicting seed claim is recorded, a baseline recorded under any seed but the manifest's is refused, the mutation lane strips a strayQUINT_SEED, and exploration requires the witness report to carry its own seed and every scheduled profile, keeping a tolerated evaluator failure in its report.Third-round fixes (97cd95c)
A saved exploration replayed with
--replaywas checked against the current checkout's profile inventory, so a profile added after the run was saved made a complete report fail; replays are now judged against the snapshot's own manifest and registry. The stale-seed baseline guard also blocked the full rewrite it named as the recovery; onlybaseline --write --profile all, which replaces the file, is exempt from it.Review
Each slice had an adversarial reviewer. The provenance reviewer found the baseline's corpus fingerprint was unusable because Quint stamps a timestamp into every trace, found that the Go checker trusted the
kindfield, and found the shared-grid label credited at the end of the history rather than at its two establishing calls; all three were fixed. The reproducer reviewer found that any failure of the cited run earned credit rather than a failure at the declared checkpoint, that exclusions were unchecked for shared-library faults, and that a portable fault was cited as model-only; all fixed. The lint reviewer added eight hiding routes as fixtures and fixed the classification of a witness read in amatchscrutinee.Validation on this head
baseline --checkcleantsc --noEmitclean; 50 formal suites, 2,407 testsgo vet,gofmt,go test -racewith the schema-2 evidenceNoted
Evidence files grew from a few kilobytes to about 26 MB in total because provenance lists every history per label and a label derived from a cumulative public list (an event kind, a read budget) is credited at every later step of a history, so its checkpoints run to the end of the trace. The recorder is deliberately faithful: an attempt to collapse consecutive credits inside it dropped a legitimate second checkpoint for the local-clock expiry label, so any compaction belongs in those classifiers, crediting only when the list grows. The Go checker and the mutation lane read the files without trouble; a per-trace layout is the fallback if artifact size matters. Diversity counts saturate on the pinned corpus (every sampled history is distinct), so the signal only bites when exploration collapses, as designed. Labels whose baseline is below 10 sampled hits are never gated, which leaves the profiles whose required labels are all regression-only with zero gated labels.