From a611a51fcff9ff2e32de5b7642ea9cda4e891195 Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Wed, 14 Oct 2026 19:03:37 -0700 Subject: [PATCH] docs(formal): index the challenges and mutants; read an entry with where.mjs The first shape of this change mirrored the challenge and mutant catalogs into 8,190 lines of Markdown. A mirror of 345 KB is no easier to read than the JSON it copies, costs a regeneration on every catalog edit and is worse for an agent, which parses JSON fine. What a reader needs is a skimmable list and one entry at a time. CHALLENGES.md and MUTANTS.md are now one-row-per-entry indexes (91 and 76 lines): challenge, contract, source, invariant, native mutant, reproducer run and detected/excluded counts; mutant, case, description, detections per port and the challenges mapped to it. The entry itself is read on demand: `node formal/tools/where.mjs recovery-inclusive-maximum` prints the edit, the invariant, the mapping with its cross-contract note and evidence checkpoint, the reproducer and every exclusion with its reason; `node formal/tools/where.mjs M01` prints the rationale, the edits per port including the Rust mirror, the required detections and the challenges mapped to it. The indexes are checked in the audit lane; the lookups are tested on the committed catalogs. --- formal/README.md | 4 +- formal/catalogs/source-audit.json | 6 +- formal/generated/CHALLENGES.md | 91 +++++++++++++++++++++ formal/generated/MUTANTS.md | 76 +++++++++++++++++ formal/generated/README.md | 1 + formal/guides/AUTHORING.md | 10 ++- formal/guides/README.md | 1 + formal/tools/README.md | 4 +- formal/tools/generate-catalog-docs.mjs | 52 +++++++++++- formal/tools/where.mjs | 70 +++++++++++++++- typescript/test/formal-catalog-docs.test.ts | 26 ++++-- typescript/test/formal-where.test.ts | 15 ++++ 12 files changed, 335 insertions(+), 21 deletions(-) create mode 100644 formal/generated/CHALLENGES.md create mode 100644 formal/generated/MUTANTS.md diff --git a/formal/README.md b/formal/README.md index 3022fb58..f445cb1a 100644 --- a/formal/README.md +++ b/formal/README.md @@ -16,7 +16,7 @@ the test [coordinator](./guides/GLOSSARY.md#coordinator). | Change a behavior or extend coverage | [AUTHORING.md](./guides/AUTHORING.md) | | Implement another language | [PORTING.md](./guides/PORTING.md) and [PROTOCOL.md](./guides/PROTOCOL.md) | | Locate or reproduce a failing check | [TEST-MAP.md](./guides/TEST-MAP.md) and the commands below | -| See where one contract is stated, tested, challenged and mapped | `node formal/tools/where.mjs C45` (or a case, `C45.recheck-after-decode` or `B01.registration-and-policy-snapshot`) | +| See where one contract is stated, tested, challenged and mapped, or read one challenge or mutant in full | `node formal/tools/where.mjs C45` (or `C45.recheck-after-decode`, `B01.registration-and-policy-snapshot`, `recovery-inclusive-maximum`, `M01`) | | Interpret validation results | [VALIDATION.md](./guides/VALIDATION.md) | | Look up a term | [GLOSSARY.md](./guides/GLOSSARY.md) | @@ -34,7 +34,7 @@ and generated artifacts; a reader should not need to open them to learn a rule. | [replay/](./replay/) | The shared replay coordinator, profile descriptors and witness classifiers every port executes | [replay/README.md](./replay/README.md) | | [tools/](./tools/) | The Node scripts behind the `make` targets: checks, generators, measurements and runners | [tools/README.md](./tools/README.md) | | [catalogs/](./catalogs/) | Hand-maintained manifests, evidence catalogs, ledgers, baselines and the fixed vector corpora | [catalogs/README.md](./catalogs/README.md) | -| [generated/](./generated/) | Smoke traces, the fixtures lock, generated vectors and the generated read views such as [PROFILES.md](./generated/PROFILES.md); regenerated, never edited | [generated/README.md](./generated/README.md) | +| [generated/](./generated/) | Smoke traces, the fixtures lock, generated vectors and the generated read views ([PROFILES.md](./generated/PROFILES.md), the [CHALLENGES.md](./generated/CHALLENGES.md) and [MUTANTS.md](./generated/MUTANTS.md) indexes); regenerated, never edited | [generated/README.md](./generated/README.md) | ## How the specification connects to code diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index ba9d3f7c..9ea9b436 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -1084,7 +1084,7 @@ "reviewedGuides": [ { "path": "formal/README.md", - "sha256": "8042f90203465f6836322afa565479e36dcfdc6628a9a1d4140eea38093cd6f8", + "sha256": "f03253dbdc8b87c8b272b16a0b0898413efddf9cb97a144b261810eff09633bc", "entries": [ {"title":"Executable DialCache specification"}, {"title":"Start with your task"}, @@ -1102,7 +1102,7 @@ }, { "path": "formal/guides/AUTHORING.md", - "sha256": "a8927a0580df5e67d795407d78040aa2a364e54cc20530c3d3db59507ce67d6f", + "sha256": "46ea31d30b5cfebfa6163dfad1ad33b770148bf147329bb5c0a93271d4806962", "entries": [ {"title":"Reading and extending the DialCache models"}, {"title":"Reading a model"}, @@ -1534,7 +1534,7 @@ }, { "path": "formal/guides/README.md", - "sha256": "14d3ff0c562d1d2679d1127c050d266fda452cd27ce93d891adde8967b327137", + "sha256": "4607559e473de61ff46e08b855ad262b6851c1a5e6b505dd31ed80c36e21445f", "entries": [ {"title":"Guides"}, {"title":"Contract guides: what a port must preserve"}, diff --git a/formal/generated/CHALLENGES.md b/formal/generated/CHALLENGES.md new file mode 100644 index 00000000..86e17634 --- /dev/null +++ b/formal/generated/CHALLENGES.md @@ -0,0 +1,91 @@ +# Model-fault challenges + +Generated by `node formal/tools/generate-catalog-docs.mjs --write` from the `challenges` of +[execution.json](../catalogs/execution.json); `make audit` fails when this index is stale. A challenge is +one compiling single-site edit of a Quint source that a named invariant must detect; its native mutant +is the matching edit of the ports in [MUTANTS.md](./MUTANTS.md), or the reason no port line +corresponds. `node formal/tools/where.mjs ` prints an entry in full (edit, mapping, reproducer, +profile partition with exclusion reasons); [AUTHORING.md](../guides/AUTHORING.md#challenging-every-model) +explains what a challenge measures. + +| Challenge | Contract | Source | Invariant | Native mutant | Reproducer run | Detected / excluded | +| --- | --- | --- | --- | --- | --- | --- | +| `recovery-inclusive-maximum` | C45 | cache-rules.qnt | `recoveryBoundaryIsExclusive` | mapped `M01` | `maximumAgeAfterDecodeFromStrictlyStaleFrameTest` | 8 / 8 | +| `recovery-future-candidate` | C45 | cache-rules.qnt | `recoveryBoundaryIsExclusive` | mapped `M40` (cross-contract) | `wallRollbackRejectsFutureRemoteFrameTest` | 6 / 10 | +| `recovery-connection-inclusive-maximum` | C45 | cache-rules.qnt | `recoveredValueWasWithinAcceptedAge` | mapped `M01` | `maximumAgeAfterDecodeFromStrictlyStaleFrameTest` | 8 / 8 | +| `policy-inclusive-local-expiry` | C09 | kernel/local-storage.qnt | `localHitsRespectInsertionExpiry` | mapped `M18` | `localHitDoesNotRenewInsertionTtlTest` | 4 / 12 | +| `local-precise-grid` | C09 | cache-rules.qnt | `localGridUsesWholeMilliseconds` | mapped `M19` | `fractionalInsertionExpiresAtWholeMillisecondTest` | 1 / 15 | +| `source-inclusive-deadline` | C25 | cache-rules.qnt | `sourceBoundaryIsExclusive` | mapped `M35` | `lateSourceResultIsADeadlineErrorTest` | 11 / 5 | +| `fence-inclusive-timestamp` | C33 | cache-rules.qnt | `fenceBoundaryIsExclusive` | mapped `M06` | `frameAtTheWatermarkIsFencedFromTheDarkReadTest` | 4 / 12 | +| `profile-source-wrong-clock` | C23 | kernel/deadlines.qnt | `sourceOriginsMatchContract` | mapped `M33` | `heldPolicyDoesNotSpendSourceBudgetTest` | 9 / 1 | +| `profile-source-wrong-owner` | C24 | kernel/flights.qnt | `sourceOwnersMatchContract` | model-only | `outsideSourcesKeepDistinctOwnersTest` | 16 / 0 | +| `profile-recovery-wrong-snapshot` | C44 | kernel/recovery.qnt | `retainedSnapshotMatchesAcquisition` | mapped `M43` | `compressedRecoveryRechecksMaximumAfterDecodeTest` | 3 / 8 | +| `recovery-read-wrong-admission-policy` | C45 | kernel/remote-io.qnt | `retainedSnapshotMatchesAcquisition` | mapped `M45` | `compressedRecoveryRechecksMaximumAfterDecodeTest` | 4 / 7 | +| `independent-wrong-admission-policy` | C45 | kernel/remote-io.qnt | `independentSnapshotsMatchAcquisition` | mapped `M46` | `recoveryPolicyIsCapturedPerCallerTest` | 4 / 7 | +| `independent-wrong-recovered-value` | C43 | kernel/remote-io.qnt | `independentRecoveryMatchesContract` | mapped `M41` | `independentRecoveriesServeDistinctAcquiredSnapshotsTest` | 3 / 8 | +| `effects-wrong-acceptance-receipt` | C25 | kernel/metrics.qnt | `measurementsAreNonnegative` | mapped `M36` | `sourceDurationExcludesPublicationTest` | 1 / 0 | +| `recovery-strands-followers` | C24 | kernel/serving.qnt | `pendingCallersOwnActiveFlights` | mapped `M34` | `crossRequestRecoveryMemoizesBothScopesTest` | 9 / 7 | +| `independent-source-wrong-clock` | C23 | kernel/deadlines.qnt | `independentSourceOriginsMatchContract` | mapped `M33` | `heldPolicyDoesNotSpendSourceBudgetTest` | 9 / 1 | +| `independent-source-wrong-owner` | C24 | kernel/flights.qnt | `independentSourceOriginsMatchContract` | model-only | `independentReadSourcesKeepDistinctOwnersTest` | 16 / 0 | +| `tracked-read-inclusive-fence` | C33 | cache-rules.qnt | `servedSnapshotClearedObservedFence` | mapped `M06` | `frameAtTheWatermarkIsFencedFromTheDarkReadTest` | 4 / 12 | +| `policy-inclusive-remote-freshness` | C22 | kernel/remote-frames.qnt | `remoteHitsRespectAcquiredFreshness` | mapped `M30` | `exactRemoteFreshBoundaryStartsSourceTest` | 7 / 9 | +| `shadow-inclusive-c0-freshness` | C22 | kernel/shadow.qnt | `c0AcquisitionsRespectFreshness` | mapped `M31` | `expiredC0BeginsFillBeforePublicationTest` | 3 / 2 | +| `core-unhealthy-local-read-hits` | C27 | dialcache-core.qnt | `failedLocalReadSkipsReuseAndPublication` | model-only | `failedLocalReadCannotServePreviouslyStoredValueTest` | 0 / 0 | +| `core-tracked-fallback-warms-local` | C31 | cache-rules.qnt | `trackedRemoteFallbackSuppressesLocalPublication` | mapped `M10` | `trackedRefillIsReadAgainBeforeLocalReuseTest` | 2 / 14 | +| `runtime-policy-coalesce-defaults-off` | C17 | cache-rules.qnt | `featureLibraryDefaults` | mapped `M28` | `omittedRampAndSharingUseLibraryDefaultsTest` | 1 / 15 | +| `runtime-policy-physical-ttl-ignores-recovery` | C22 | cache-rules.qnt | `existingRemoteEntryKeepsPhysicalTtl` | mapped `M32` | `eachSourceKeepsPublicationPolicyTest` | 1 / 15 | +| `stale-recovery-inclusive-served-maximum` | C45 | cache-rules.qnt | `servedStaleIsStrictlyWithinMaxAge` | mapped `M01` | `maximumAgeAfterDecodeFromStrictlyStaleFrameTest` | 3 / 13 | +| `stale-recovery-candidate-stamped-at-read` | C44 | cache-contract.qnt | `retainedCandidateWasEligible` | mapped `M44` | `compressedRecoveryRechecksMaximumAfterDecodeTest` | 3 / 8 | +| `shadow-fenced-fill-writes` | C53 | kernel/remote-writes.qnt | `fillsClearTheirFence` | mapped `M04` (cross-contract) | `fenceRejudgedAtDumpReleaseAfterRollbackTest` | 3 / 3 | +| `shadow-fill-before-source` | C49 | kernel/shadow.qnt | `fillsRequireMissAndAcceptedSource` | mapped `M47` | `darkReadBeforeSourceWaitsForItTest` | 3 / 2 | +| `redis-protocol-inclusive-fence` | C33 | cache-rules.qnt | `fenceCanPrecedeEncodingError` | mapped `M06` | `frameAtWatermarkIsDeclinedTest` | 4 / 12 | +| `redis-protocol-untracked-fence` | W04 | cache-rules.qnt | `untrackedDecodingIgnoresWatermarks` | mapped `M52` | `untrackedReadsIgnoreGroupedInvalidationTest` | 2 / 14 | +| `frame-vectors-inclusive-fence` | C33 | dialcache-frame-vectors.qnt | `trackedHitsStrictlyClearValidFence` | mapped `M06` | `frameAtWatermarkIsDeclinedTest` | 0 / 0 | +| `invalidation-transition-cutoff-moves-backwards` | C38 | dialcache-invalidation-transition.qnt | `successfulCutoffIsExactMaximum` | mapped `M63` | `futureCutoffDoesNotMoveBackwardsTest` | 0 / 0 | +| `invalidation-transition-inclusive-buffer-limit` | C39 | dialcache-invalidation-transition.qnt | `argumentValidationIsExact` | mapped `M64` | `maximumBufferAndTimestampSumAreAcceptedTest` | 0 / 0 | +| `key-protocol-untracked-brace-rejection` | W01 | dialcache-key-protocol.qnt | `keyAcceptanceRespectsTextAndHashTagDomain` | mapped `M50` | `untrackedTypeBraceRemainsValidTest` | 0 / 0 | +| `cohort-inclusive-threshold` | W03 | cohort-boundaries.qnt | `cohortNumeratorsAreUnsignedAndBoundariesStrict` | mapped `M51` | `localCohortEqualityLeavesNoValueForLaterAdmissionTest` | 2 / 0 | +| `envelope-vectors-tie-compresses` | W07 | dialcache-envelope-vectors.qnt | `compressionUsesByteThresholdAndStrictShrink` | mapped `M55` | `compressionTieKeepsRawRepresentationTest` | 0 / 0 | +| `envelope-vectors-escape-misses-binary-marker` | W06 | dialcache-envelope-vectors.qnt | `escapeConsumesExactlyOnePrefix` | mapped `M53` | `escapedBinaryMarkerRemainsLiteralTest` | 0 / 0 | +| `conformance-local-hit-returns-source` | C05 | dialcache-conformance.qnt | `servedLayerValueMatchesCache` | mapped `M17` | `localValueSurvivesSourceChangeTest` | 1 / 0 | +| `conformance-remote-miss-skips-publication` | C28 | dialcache-conformance.qnt | `servedLayerValueMatchesCache` | mapped `M38` | `invalidationRefillsFromCurrentSourceTest` | 1 / 0 | +| `effects-fenced-source-publishes` | C34 | kernel/serving.qnt | `writeRequiresAcceptedSource` | mapped `M39` | `fencedSourceSkipsSerializationTest` | 3 / 13 | +| `effects-late-source-accepted` | C25 | kernel/deadlines.qnt | `acceptedSourcesSettledBeforeTheirDeadline` | mapped `M03` | `lateSourceResultIsADeadlineErrorTest` | 2 / 8 | +| `scope-late-source-repopulates-closed-memo` | C03 | kernel/request-memo.qnt | `closedScopesHaveNoMemo` | unobservable | `lateSourceCannotPopulateReplacementTest` | 4 / 12 | +| `scope-source-error-memoized` | C15 | kernel/serving.qnt | `memoFollowsLatestSuccessfulSettlement` | mapped `M25` | `rejectedDarkSourceSeedsNoLayerTest` | 3 / 13 | +| `scope-nested-close-evicts-outer-memo` | C02 | kernel/request-memo.qnt | `memoFollowsLatestSuccessfulSettlement` | mapped `M15` | `nestedCloseAndDisabledBypassKeepOuterMemoTest` | 2 / 14 | +| `admission-duplicate-key-admitted` | C54 | kernel/shadow.qnt | `oneJobPerIdentity` | mapped `M48` | `duplicateDropsBeforeCapacityIsFullTest` | 2 / 3 | +| `admission-capacity-off-by-one` | C54 | kernel/shadow.qnt | `capacityIsPerInstance` | mapped `M49` | `fullInstanceDoesNotBlockOtherInstanceTest` | 4 / 1 | +| `layers-process-flight-crosses-instance` | C11 | kernel/serving.qnt | `sourceOwnershipNeverCrossesKeyOrInstance` | mapped `M20` | `sameKeyCallersOnTwoInstancesKeepSeparateFlightsTest` | 3 / 13 | +| `layers-late-memo-into-closed-scope` | C03 | kernel/request-memo.qnt | `closedScopesHaveNoMemo` | unobservable | `lateSourceCannotPopulateReplacementTest` | 4 / 12 | +| `independent-fresh-frame-retained` | C40 | kernel/recovery.qnt | `retainedSnapshotsWereEligible` | model-only | `initiallyExpiredFrameIsNotRetainedTest` | 1 / 10 | +| `independent-deadline-settles-at-start` | C24 | kernel/deadlines.qnt | `independentSourceOriginsMatchContract` | model-only | `readExpiryStartsItsLoaderAtTheReadsDueInstantTest` | 1 / 9 | +| `recovery-read-inclusive-maximum` | C45 | kernel/recovery.qnt | `recoveryReturnMatchesAcquiredContract` | mapped `M01` | `compressedRecoveryRechecksMaximumAfterDecodeTest` | 3 / 8 | +| `recovery-read-recovery-warms-local` | C43 | kernel/remote-io.qnt | `recoveredResultsNeverPublishShared` | mapped `M42` | `untrackedCompressedRecoveryDoesNotWarmLocalTest` | 1 / 10 | +| `recovery-read-tracked-retention-uncapped` | C37 | kernel/serving.qnt | `trackedWritesRespectPhysicalCap` | mapped `M56` | `trackedPhysicalRetentionExpiresAtCapTest` | 1 / 15 | +| `local-failure-write-fault-publishes` | C27 | kernel/local-faults.qnt | `faultedSettlementPublishesNothingLocally` | model-only | `localWriteFailureKeepsSourceAndRequestMemoTest` | 1 / 0 | +| `local-failure-source-error-published` | C27 | kernel/serving.qnt | `storageHoldsAcceptedValuesOnly` | mapped `M37` | `rejectedSourceDoesNotSeedLocalTest` | 3 / 13 | +| `runtime-boundaries-inclusive-cohort` | W03 | kernel/runtime-policy.qnt | `equalAndLowerCohortsNeverTraverse` | mapped `M51` | `localCohortEqualityLeavesNoValueForLaterAdmissionTest` | 1 / 0 | +| `runtime-boundaries-inherited-sharing-ignores-default` | C16 | kernel/runtime-policy.qnt | `inheritedDisabledSharingNeverJoins` | mapped `M27` | `inheritedFalseStartsBothSourcesBeforeSettlementTest` | 1 / 0 | +| `shadow-layers-inclusive-c0-freshness` | C22 | kernel/shadow.qnt | `retainedC0WasFreshWhenAcquired` | mapped `M31` | `expiredC0StartsFillWithoutDecodingTest` | 3 / 2 | +| `shadow-layers-fill-uses-current-retention` | C18 | kernel/shadow.qnt | `fillKeepsCapturedRetention` | mapped `M29` | `darkFillRetainsPolicyThroughSerializationTest` | 3 / 2 | +| `local-clock-precise-ttl` | C09 | cache-rules.qnt | `clockIsOnTheGrid` | mapped `M19` | `fractionalInsertionExpiresAtWholeMillisecondTest` | 1 / 15 | +| `local-clock-hit-renews-insertion` | C09 | kernel/local-storage.qnt | `localHitsRespectInsertionExpiry` | mapped `M11` | `fractionalInsertionExpiresAtWholeMillisecondTest` | 4 / 12 | +| `source-budgets-outside-call-has-deadline` | C01 | kernel/deadlines.qnt | `outsideSourcesHaveNoDeadline` | mapped `M14` | `outsideAndInvalidOutsideCallsIgnoreDeadlineAndSharingTest` | 2 / 8 | +| `source-budgets-settled-flight-stays-registered` | C15 | kernel/flights.qnt | `registeredWorkIsNotAbandoned` | mapped `M26` | `defaultSourceBudgetExpiresAtSixtySecondsTest` | 11 / 5 | +| `stale-recovery-future-candidate` | C40 | cache-rules.qnt | `futureFrameIsNeverFreshOrRetained` | mapped `M40` | `wallRollbackRejectsFutureRemoteFrameTest` | 6 / 10 | +| `envelope-strips-unknown-zero-prefix` | W06 | dialcache-envelope-vectors.qnt | `unknownZeroPrefixPassesThroughUnchanged` | mapped `M54` | `unknownLegacyZeroPrefixRemainsUntouchedTest` | 0 / 0 | +| `source-budgets-accepts-at-deadline-equality` | C25 | kernel/deadlines.qnt | `acceptedSourceRespectsItsOwnStart` | mapped `M35` | `lateSourceResultIsADeadlineErrorTest` | 9 / 1 | +| `policy-hit-before-join` | C13 | kernel/serving.qnt | `remoteHitsRespectAcquiredFreshness` | mapped `M21` | `independentCompletionKeepsRegisteredLeaderTest` | 4 / 12 | +| `policy-join-ignores-coalesce` | C13 | kernel/serving.qnt | `joinsOnlyJoinableFlights` | mapped `M22` | `nonCoalescingCallStartsSeparateSourceTest` | 4 / 12 | +| `source-budgets-settlement-never-replaces-local-entry` | C13 | kernel/local-storage.qnt | `localPublicationRequiresAcceptedSource` | mapped `M23` | `independentLocalPublicationUsesLastCompletionTest` | 4 / 12 | +| `source-budgets-failed-settlement-clears-local-entry` | C13 | kernel/serving.qnt | `localPublicationRequiresAcceptedSource` | mapped `M24` | `independentFailureKeepsLocalValueWhenRemoteFailsTest` | 3 / 13 | +| `dark-layers-process-flight-crosses-instance` | C11 | kernel/serving.qnt | `sourceOwnersShareTheSourcesIdentity` | mapped `M20` | `sameKeyCallersOnTwoInstancesKeepSeparateFlightsTest` | 3 / 13 | +| `dark-layers-budget-starts-at-clock-origin` | C23 | kernel/deadlines.qnt | `pendingDeadlinesAreFuture` | mapped `M33` | `laterDarkSourceKeepsItsWholeBudgetTest` | 9 / 1 | +| `admission-budget-starts-at-clock-origin` | C54 | kernel/deadlines.qnt | `pendingDeadlinesAreFuture` | mapped `M33` (cross-contract) | `laterServedShadowKeepsItsWholeBudgetTest` | 9 / 1 | +| `dark-layers-timeout-releases-held-capacity` | C54 | kernel/shadow.qnt | `heldEffectsKeepTheirJob` | mapped `M58` | `timedOutDarkDumpKeepsCapacityUntilRawReleaseTest` | 5 / 0 | +| `effects-stale-frame-reply-unclassified` | C58 | kernel/metrics.qnt | `staleFrameRepliesReportExpired` | mapped `M57` | `staleFrameReplyExpiresRefillsAndIsReadableTest` | 1 / 0 | +| `inspection-counts-leaders-as-followers` | C11 | kernel/flights.qnt | `inspectionsCountOnlyProcessFollowers` | mapped `M59` | `inspectionTracksKeysFollowersAndOldestLeaderTest` | 1 / 15 | +| `inspection-age-uses-wall-clock` | C11 | kernel/flights.qnt | `inspectionAgeUsesTheOldestLiveMonotonicStart` | mapped `M60` | `inspectionIsPerInstanceAndUsesMonotonicTimeTest` | 1 / 15 | +| `shadow-read-deadline-ignores-bounded-result` | C54 | kernel/shadow-reads.qnt | `abortedReadsHaveEndedTheirResult` | mapped `M61` | `c0ReadDeadlineKeepsRawCapacityTest` | 1 / 0 | +| `shadow-read-deadline-releases-raw-capacity` | C54 | kernel/shadow-reads.qnt | `rawReadsKeepTheirRegistration` | mapped `M62` | `c0ReadDeadlineKeepsRawCapacityTest` | 1 / 0 | diff --git a/formal/generated/MUTANTS.md b/formal/generated/MUTANTS.md new file mode 100644 index 00000000..3f36dddf --- /dev/null +++ b/formal/generated/MUTANTS.md @@ -0,0 +1,76 @@ +# Native mutants + +Generated by `node formal/tools/generate-catalog-docs.mjs --write` from +[mutations.json](../catalogs/mutations.json) (TypeScript and Go) and +[rust-mutations.json](../catalogs/rust-mutations.json); `make audit` fails when this index is stale. A native +mutant is one described fault injected into each port by anchored edits, with the detections each cohort +must record (`ordinary` tests, the `generated` corpus, the `fixed` scenarios and vectors, the `portable` +union of fixed and generated). `node formal/tools/where.mjs M01` prints an entry in full (rationale, edits +per port, detections, the challenges mapped to it); +[AUTHORING.md](../guides/AUTHORING.md#mapping-every-challenge-to-native-mutants) explains the lanes. + +| Mutant | Case | Description | TypeScript | Go | Rust | Challenges mapped | +| --- | --- | --- | --- | --- | --- | --- | +| `M01` | C45.maximum-age-exclusive | Accept a retained candidate at the exact maximum age after decoding | ordinary, generated, portable | generated, portable | generated, fixed, portable | `recovery-inclusive-maximum`, `recovery-connection-inclusive-maximum`, `stale-recovery-inclusive-served-maximum`, `recovery-read-inclusive-maximum` | +| `M02` | C45.recheck-after-decode | Reuse the pre-decode age instead of observing age after asynchronous decoding | ordinary, generated, portable | generated, portable | generated, fixed, portable | none | +| `M03` | C25.late-source-rejected | Accept an externally settled result after its elapsed deadline when the timer has not run | ordinary, generated, portable | generated, portable | generated, fixed, portable | `effects-late-source-accepted` | +| `M04` | C34.second-fence | Skip the tracked fence recheck after serialization | ordinary, generated, portable | generated, portable | generated, fixed, portable | `shadow-fenced-fill-writes` | +| `M05` | C03.detached-bypass | Treat a detached context whose outer scope closed as still enabled | ordinary, generated, portable | generated, portable | generated, fixed, portable | none | +| `M06` | W04.strict-fence | Accept a tracked frame timestamp equal to its watermark | ordinary, generated, portable | generated, portable | generated, fixed, portable | `fence-inclusive-timestamp`, `tracked-read-inclusive-fence`, `redis-protocol-inclusive-fence`, `frame-vectors-inclusive-fence` | +| `M07` | C51.changed-confirmation | Confirm an unequal shadow result even when C1 contains different payload bytes | ordinary, generated, portable | generated, portable | generated, fixed, portable | none | +| `M08` | C60.invalid-logging-policy | Enable mismatch logging after a malformed runtime logging flag | ordinary, generated, portable | generated, portable | generated, fixed, portable | none | +| `M09` | C60.logging-default-off | Enable mismatch logging when its flag is omitted | ordinary, generated, portable | generated, portable | generated, portable | none | +| `M10` | C31.tracked-no-local-fill | Publish an unvalidated tracked source value directly into local storage | ordinary, generated, portable | generated, portable | generated, fixed, portable | `core-tracked-fallback-warms-local` | +| `M11` | C09.fixed-local-ttl | Renew the local insertion TTL on every cache hit | ordinary, generated, portable | generated, portable | generated, fixed, portable | `local-clock-hit-renews-insertion` | +| `M12` | W02.sorted-arguments | Reverse the prescribed argument-name ordering | generated, portable | generated, portable | generated, fixed, portable | none | +| `M13` | C54.expired-before-start | Dispatch dark shadow reads after the job deadline already elapsed before deferred work starts | ordinary, generated, portable | generated, portable | generated, fixed, portable | none | +| `M14` | C01.no-deadline | Bound a disabled or outside call's source with the configured fallback deadline | generated, portable | generated, portable | - | `source-budgets-outside-call-has-deadline` | +| `M15` | C02.reenabled-memo | Evict the enclosing request's memo when a nested enable() completes | generated, portable | generated, portable | - | `scope-nested-close-evicts-outer-memo` | +| `M17` | C05.local-hit-stops-traversal | Serve a local hit with a value the layer never stored while still skipping the loader | generated, portable | generated, portable | - | `conformance-local-hit-returns-source` | +| `M18` | C09.fixed-local-ttl | Serve a local entry at its exact insertion expiry | generated, portable | generated, portable | - | `policy-inclusive-local-expiry` | +| `M19` | C09.fractional-clock-grid | Compute local insertion and expiry on the precise clock instead of the whole-millisecond grid | generated, portable | generated, portable | - | `local-precise-grid`, `local-clock-precise-ttl` | +| `M20` | C11.distinct-keys | Register process flights in one process-wide registry so a flight on one instance is joined from another (detection rests on sampled layers histories and the different-instances-own-distinct-flights witness, not on the case's exported replay) | generated, portable | generated, portable | - | `layers-process-flight-crosses-instance`, `dark-layers-process-flight-crosses-instance` | +| `M21` | C13.uncoalesced-caching | Serve a live local entry before joining the pending process flight | generated, portable | generated, portable | - | `policy-hit-before-join` | +| `M22` | C13.uncoalesced-caching | Join a pending process flight from a non-coalescing caller while registration still respects coalesce | generated, portable | generated, portable | - | `policy-join-ignores-coalesce` | +| `M23` | C13.local-last-writer | Never let a local publication replace an entry already occupying the slot, even an expired one | generated, portable | generated, portable | - | `source-budgets-settlement-never-replaces-local-entry` | +| `M24` | C13.local-last-writer | Clear the key's local entry when a source settlement fails | generated, portable | generated, portable | - | `source-budgets-failed-settlement-clears-local-entry` | +| `M25` | C15.shared-error-retry | Keep a rejected request-local flight registered so a later same-scope caller receives the rejection instead of retrying | generated, portable | generated, portable | - | `scope-source-error-memoized` | +| `M26` | C15.shared-error-retry | Never remove a settled process flight from the registry so later same-key callers join finished work | generated, portable | generated, portable | - | `source-budgets-settled-flight-stays-registered` | +| `M27` | C16.runtime-enables-coalescing | Capture the operation's coalesce default as true so an omitted runtime leaf or null provider inherits sharing over a configured false | generated, portable | generated, portable | - | `runtime-boundaries-inherited-sharing-ignores-default` | +| `M28` | C17.library-defaults | Default coalescing off when the static coalesce leaf is omitted while an explicit true still shares | generated, portable | generated, portable | - | `runtime-policy-coalesce-defaults-off` | +| `M29` | C18.captured-shadow-fill | Re-resolve the runtime policy at fill time and write the dark fill with the retention then in force | generated, portable | generated, portable | - | `shadow-layers-fill-uses-current-retention` | +| `M30` | C22.freshness-boundary | Serve a remote frame whose age equals the fresh TTL as a hit | generated, portable | generated, portable | - | `policy-inclusive-remote-freshness` | +| `M31` | C22.freshness-boundary | Acquire a dark C0 frame whose age equals the fresh TTL instead of treating it as expired | generated, portable | generated, portable | - | `shadow-inclusive-c0-freshness`, `shadow-layers-inclusive-c0-freshness` | +| `M32` | C22.physical-vs-logical | Write every remote frame with the fresh TTL, ignoring stale-on-error retention | generated, portable | generated, portable | - | `runtime-policy-physical-ttl-ignores-recovery` | +| `M33` | C23.policy-does-not-spend-source-budget | Judge a source settlement against a deadline anchored at the clock origin instead of the source start; the timer still fires at the source's own deadline | generated, portable | generated, portable | - | `profile-source-wrong-clock`, `independent-source-wrong-clock`, `dark-layers-budget-starts-at-clock-origin`, `admission-budget-starts-at-clock-origin` | +| `M34` | C24.follower-source | Complete followers of a joined flight with an undefined or zero value instead of the leader's accepted value while errors still propagate | generated, portable | generated, portable | - | `recovery-strands-followers` | +| `M35` | C25.late-source-rejected | Accept a settlement observed at exactly the elapsed deadline | generated, portable | generated, portable | - | `source-inclusive-deadline`, `source-budgets-accepts-at-deadline-equality` | +| `M36` | C25.late-source-rejected | Stamp the serialization-start receipt one millisecond late so the dump duration is measured short | generated, portable | generated, portable | - | `effects-wrong-acceptance-receipt` | +| `M37` | C27.source-error-no-publication | Publish a rejected source's result into process-local storage before rethrowing | generated, portable | generated, portable | - | `local-failure-source-error-published` | +| `M38` | C28.no-refill-after-read-failure | Skip the Redis publication after a semantic miss, including a decode failure, so only retained-candidate misses refill | generated, portable | generated, portable | - | `conformance-remote-miss-skips-publication` | +| `M39` | C34.first-fence | Drop the pre-serialization fence check so a source accepted behind an observed fence is serialized while the post-serialization recheck still blocks the write | generated, portable | generated, portable | - | `effects-fenced-source-publishes` | +| `M40` | C40.future-rejected | Classify a frame dated after the reader clock as a valid frame of age zero instead of rejecting it as future | generated, portable | generated, portable | - | `recovery-future-candidate`, `stale-recovery-future-candidate` | +| `M41` | C43.independent-values | Decode the retained candidate but serve an undefined or zero value instead of it from stale recovery | generated, portable | generated, portable | - | `independent-wrong-recovered-value` | +| `M42` | C43.request-memo | Publish a recovered stale value into process-local storage | generated, portable | generated, portable | - | `recovery-read-recovery-warms-local` | +| `M43` | C44.retained-invalidation | Retain the stale candidate with a creation timestamp one millisecond after the acquired frame | generated, portable | generated, portable | - | `profile-recovery-wrong-snapshot` | +| `M44` | C44.retained-invalidation | Stamp the retained candidate with the read time instead of its frame timestamp | generated, portable | generated, portable | - | `stale-recovery-candidate-stamped-at-read` | +| `M45` | C45.captured-policy | Admit calls with a recovery maximum one second larger than the configured policy | generated, portable | generated, portable | - | `recovery-read-wrong-admission-policy` | +| `M46` | C45.captured-policy | Capture the static default recovery maximum at admission, ignoring the runtime overlay (in the policy profile this also hides overlay configuration errors) | generated, portable | generated, portable | - | `independent-wrong-admission-policy` | +| `M47` | C49.dark-source-reuse | Continue dark shadow work without waiting for the caller source | generated, portable | generated, portable | - | `shadow-fill-before-source` | +| `M48` | C54.deduplication | Admit a shadow job for an identity that already has a live job | generated, portable | generated, portable | - | `admission-duplicate-key-admitted` | +| `M49` | C54.instance-isolation | Admit one shadow job beyond the per-instance capacity | generated, portable | generated, portable | - | `admission-capacity-off-by-one` | +| `M50` | W01.key-identity | Reject braces in keyType and id for untracked keys as well | generated, portable | generated, portable | - | `key-protocol-untracked-brace-rejection` | +| `M51` | W03.cohort-assignment | Admit a key whose cohort sample equals the configured ramp | generated, portable | generated, portable | - | `cohort-inclusive-threshold`, `runtime-boundaries-inclusive-cohort` | +| `M52` | W04.untracked-decoder | Read and apply the entity watermark fence on untracked keys | generated, portable | generated, portable | - | `redis-protocol-untracked-fence` | +| `M53` | W06.envelope-markers | Leave the escape prefix in place before an escaped binary-zstd marker | generated, portable | generated, portable | - | `envelope-vectors-escape-misses-binary-marker` | +| `M54` | W06.envelope-markers | Strip a leading zero byte even when the next byte is not an envelope marker | generated, portable | generated, portable | - | `envelope-strips-unknown-zero-prefix` | +| `M55` | W07.compression-selection | Store a compressed payload whose marked size ties the escaped raw size | generated, portable | generated, portable | - | `envelope-vectors-tie-compresses` | +| `M56` | C37.physical-cap | Write a tracked value for its full configured retention above the one-hour cap | generated, portable | generated, portable | - | `recovery-read-tracked-retention-uncapped` | +| `M58` | C54.dump-ownership | Release shadow capacity at the whole-job timeout before its raw work settles | generated, portable | generated, portable | - | `dark-layers-timeout-releases-held-capacity` | +| `M57` | C22.adapter-frame-expiry | Report a frame at its maximum age as an unclassified miss instead of expired | generated, portable | generated, portable | - | `effects-stale-frame-reply-unclassified` | +| `M59` | C11.process-inspection | Include process leaders in the reported follower count | generated, portable | generated, portable | - | `inspection-counts-leaders-as-followers` | +| `M60` | C11.process-inspection | Measure the oldest process leader age with the application wall clock | generated, portable | generated, portable | - | `inspection-age-uses-wall-clock` | +| `M61` | C54.read-ownership | Ignore the bounded shadow read result while the raw adapter operation remains pending | generated, portable | generated, portable | - | `shadow-read-deadline-ignores-bounded-result` | +| `M62` | C54.read-ownership | Release shadow capacity at bounded read failure before the raw adapter operation settles | generated, portable | generated, portable | - | `shadow-read-deadline-releases-raw-capacity` | +| `M63` | C38.marker-transition | Move an invalidation cutoff backwards when an older request arrives | generated, portable | generated, portable | - | `invalidation-transition-cutoff-moves-backwards` | +| `M64` | C39.numeric-limits | Reject the maximum supported invalidation buffer | generated, portable | generated, portable | - | `invalidation-transition-inclusive-buffer-limit` | diff --git a/formal/generated/README.md b/formal/generated/README.md index 5fe83730..e4b695a9 100644 --- a/formal/generated/README.md +++ b/formal/generated/README.md @@ -7,6 +7,7 @@ Never edit a file in this directory; regenerate it. - `generated-fixtures.lock.json`: the pinned input hashes (models, recipes, generators) and output hashes of every committed fixture, including the witness fixtures under `typescript/test/fixtures/`; written in the same pass. - `quint-key-vectors.json`, `quint-frame-vectors.json`, `quint-envelope-vectors.json`, `quint-invalidation-vectors.json`: the generated wire vectors, one per wire model, with the generator's own source hash in their provenance; written by the `generate-*-vectors.mjs` scripts. - `PROFILES.md`: the read view of every conformance profile (fixture, setup, each action's choice decodings into driver commands, observation channels), rendered from the replay descriptors, the catalogs and each model's public runs by `node formal/tools/generate-catalog-docs.mjs --write`; `make audit` fails when it is stale. +- `CHALLENGES.md`, `MUTANTS.md`: one-row-per-entry indexes of the model-fault challenges in `execution.json` and the native mutants in `mutations.json` and `rust-mutations.json`, written in the same pass; an entry is read in full with `node formal/tools/where.mjs `, not mirrored here. Regenerate the Quint artifacts (traces, lock, vectors) with Quint 0.32.0 on `PATH`, and the read views without Quint: diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index 8dc4fd00..d8b93cf7 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -403,10 +403,12 @@ Formatting and deduplication improve reviewability; they do not increase the number of behavioral cases or justify a broader conformance claim. Changes to behavior, bounds, or claims should be reviewed separately from cleanup. -The read views under `formal/generated/` ([PROFILES.md](../generated/PROFILES.md)) -are rendered from the replay descriptors and the catalogs; after a descriptor, -`profiles.json`, `execution.json`, `coverage-witnesses.json` or a model's public runs -(its replayed regressions) change, run +The read views under `formal/generated/` ([PROFILES.md](../generated/PROFILES.md) +and the [CHALLENGES.md](../generated/CHALLENGES.md) and +[MUTANTS.md](../generated/MUTANTS.md) indexes) are rendered from the replay +descriptors and the catalogs; after a descriptor, `profiles.json`, `execution.json`, +`coverage-witnesses.json`, `mutations.json`, `rust-mutations.json` or a model's +public runs (its replayed regressions) change, run `node formal/tools/generate-catalog-docs.mjs --write` and commit the result. `make audit` runs the `--check` form and fails on a stale view. Edit the descriptor or the catalog, never the view. diff --git a/formal/guides/README.md b/formal/guides/README.md index 0edce5e4..ca1483ff 100644 --- a/formal/guides/README.md +++ b/formal/guides/README.md @@ -33,6 +33,7 @@ by-task view; this index is the by-kind view it lacks. Read ## Generated views: read, never edit - [../generated/PROFILES.md](../generated/PROFILES.md): every conformance profile's fixture, setup, action decodings and observation channels, rendered from the replay descriptors; [BEHAVIOR.md](./BEHAVIOR.md) keeps the rules behind them. +- [../generated/CHALLENGES.md](../generated/CHALLENGES.md) and [../generated/MUTANTS.md](../generated/MUTANTS.md): one row per model-fault challenge and per native mutant, with `node formal/tools/where.mjs ` for the entry in full. ## Historical evidence: what was measured, and when diff --git a/formal/tools/README.md b/formal/tools/README.md index f14c73a7..45fab42a 100644 --- a/formal/tools/README.md +++ b/formal/tools/README.md @@ -13,7 +13,7 @@ which scripts a target runs. - [validation.mjs](./validation.mjs): the target dispatcher; composes every `make` target from the scripts below and checks prerequisites. - [execution.mjs](./execution.mjs): reads and validates the execution manifest; `node formal/tools/execution.mjs` prints the inventory. -- [where.mjs](./where.mjs): `node formal/tools/where.mjs C45` prints where one contract, semantic case or native case is stated, tested, challenged and mapped, from the catalogs and the model comments; `--json` for agents. +- [where.mjs](./where.mjs): `node formal/tools/where.mjs C45` prints where one contract, semantic case or native case is stated, tested, challenged and mapped, from the catalogs and the model comments; a challenge or mutant ID prints that entry in full; `--json` for agents. ## Checks @@ -38,7 +38,7 @@ generated-fixture verification; `validation.mjs` is the list of record. - [generate-artifacts.mjs](./generate-artifacts.mjs): regenerates every committed artifact (`--write`) or verifies it (`--check`). - [generated-fixtures.mjs](./generated-fixtures.mjs): the smoke traces, witness fixtures and the lock from `fixture-recipes.json`. - [generate-key-vectors.mjs](./generate-key-vectors.mjs), [generate-frame-vectors.mjs](./generate-frame-vectors.mjs), [generate-envelope-vectors.mjs](./generate-envelope-vectors.mjs), [generate-invalidation-vectors.mjs](./generate-invalidation-vectors.mjs): one generated vector file each. -- [generate-catalog-docs.mjs](./generate-catalog-docs.mjs): the generated read views under `formal/generated/` (`PROFILES.md`) from the replay descriptors and the catalogs; `--check` runs in the `audit` lane. +- [generate-catalog-docs.mjs](./generate-catalog-docs.mjs): the generated read views under `formal/generated/` (`PROFILES.md`, and the `CHALLENGES.md` and `MUTANTS.md` indexes) from the replay descriptors and the catalogs; `--check` runs in the `audit` lane. - [witnesses.mjs](./witnesses.mjs): language-neutral witness evaluation over the generated corpus and its baseline. - [replay-inputs.mjs](./replay-inputs.mjs): adds replay annotations to exported regressions from their explicit input record. - [explore.mjs](./explore.mjs): a fresh-seed exploration in an isolated source snapshot (`make explore`); `--replay` reproduces a saved run. diff --git a/formal/tools/generate-catalog-docs.mjs b/formal/tools/generate-catalog-docs.mjs index 1c04ed3c..1dbb6f5c 100644 --- a/formal/tools/generate-catalog-docs.mjs +++ b/formal/tools/generate-catalog-docs.mjs @@ -16,7 +16,7 @@ import { emptyObservation } from '../replay/observation.mjs'; import { scheduleExecution } from './execution.mjs'; export const root = fileURLToPath(new URL('../../', import.meta.url)); -export const views = { profiles: 'formal/generated/PROFILES.md' }; +export const views = { profiles: 'formal/generated/PROFILES.md', challenges: 'formal/generated/CHALLENGES.md', mutants: 'formal/generated/MUTANTS.md' }; const json = (path, directory = root) => JSON.parse(readFileSync(resolve(directory, path), 'utf8')); const code = value => `\`${JSON.stringify(value)}\``; const text = value => String(value).replaceAll('|', '\\|'); @@ -182,10 +182,56 @@ export function renderProfiles({ directory = root } = {}) { return lines.join('\n').trimEnd() + '\n'; } +// The two catalog indexes: one row per challenge and per mutant, enough to +// skim and to link from a review; the entry itself is read on demand with +// `node formal/tools/where.mjs `, not mirrored here. +export function renderChallenges({ directory = root } = {}) { + const challenges = json('formal/catalogs/execution.json', directory).challenges ?? []; + const lines = ['# Model-fault challenges', '', + 'Generated by `node formal/tools/generate-catalog-docs.mjs --write` from the `challenges` of', + '[execution.json](../catalogs/execution.json); `make audit` fails when this index is stale. A challenge is', + 'one compiling single-site edit of a Quint source that a named invariant must detect; its native mutant', + 'is the matching edit of the ports in [MUTANTS.md](./MUTANTS.md), or the reason no port line', + 'corresponds. `node formal/tools/where.mjs ` prints an entry in full (edit, mapping, reproducer,', + 'profile partition with exclusion reasons); [AUTHORING.md](../guides/AUTHORING.md#challenging-every-model)', + 'explains what a challenge measures.', '', + '| Challenge | Contract | Source | Invariant | Native mutant | Reproducer run | Detected / excluded |', + '| --- | --- | --- | --- | --- | --- | --- |']; + for (const c of challenges) { + const native = c.nativeMutants ?? {}, r = c.reproducer ?? {}; + const detected = (r.profiles ?? []).filter(p => !p.includes('/')).length, excluded = Object.keys(r.exclusions ?? {}).length; + lines.push(`| \`${text(c.id)}\` | ${text(c.contract ?? '-')} | ${text(c.source.replace(/^formal\/models\//, ''))} | \`${text(c.invariant)}\` | ${text(native.kind)}${native.mutant ? ` \`${text(native.mutant)}\`` : ''}${native.crossContract ? ' (cross-contract)' : ''} | ${r.run ? `\`${text(r.run)}\`` : '-'} | ${detected} / ${excluded} |`); + } + return lines.join('\n') + '\n'; +} + +export function renderMutants({ directory = root } = {}) { + const mutants = json('formal/catalogs/mutations.json', directory).mutations ?? []; + const rust = new Map((json('formal/catalogs/rust-mutations.json', directory).mutations ?? []).map(m => [m.typescriptMutation ?? m.id, m])); + const mappedBy = new Map(); + for (const c of json('formal/catalogs/execution.json', directory).challenges ?? []) if (c.nativeMutants?.mutant) mappedBy.set(c.nativeMutants.mutant, [...(mappedBy.get(c.nativeMutants.mutant) ?? []), c.id]); + const detections = spec => spec?.requiredDetections?.length ? text(spec.requiredDetections.join(', ')) : '-'; + const lines = ['# Native mutants', '', + 'Generated by `node formal/tools/generate-catalog-docs.mjs --write` from', + '[mutations.json](../catalogs/mutations.json) (TypeScript and Go) and', + '[rust-mutations.json](../catalogs/rust-mutations.json); `make audit` fails when this index is stale. A native', + 'mutant is one described fault injected into each port by anchored edits, with the detections each cohort', + 'must record (`ordinary` tests, the `generated` corpus, the `fixed` scenarios and vectors, the `portable`', + 'union of fixed and generated). `node formal/tools/where.mjs M01` prints an entry in full (rationale, edits', + 'per port, detections, the challenges mapped to it);', + '[AUTHORING.md](../guides/AUTHORING.md#mapping-every-challenge-to-native-mutants) explains the lanes.', '', + '| Mutant | Case | Description | TypeScript | Go | Rust | Challenges mapped |', + '| --- | --- | --- | --- | --- | --- | --- |']; + for (const m of mutants) lines.push(`| \`${text(m.id)}\` | ${text(m.case)} | ${text(m.description)} | ${detections(m.typescript)} | ${detections(m.go)} | ${detections(rust.get(m.id))} | ${(mappedBy.get(m.id) ?? []).map(id => `\`${text(id)}\``).join(', ') || 'none'} |`); + return lines.join('\n') + '\n'; +} + +const renderers = { profiles: renderProfiles, challenges: renderChallenges, mutants: renderMutants }; + export function checkCatalogDocs({ directory = root } = {}) { const stale = []; for (const [name, path] of Object.entries(views)) { - const rendered = name === 'profiles' ? renderProfiles({ directory }) : undefined; + const rendered = renderers[name]({ directory }); let committed; try { committed = readFileSync(resolve(directory, path), 'utf8'); } catch { committed = undefined; } if (committed !== rendered) stale.push(path); @@ -195,7 +241,7 @@ export function checkCatalogDocs({ directory = root } = {}) { } export function writeCatalogDocs({ directory = root } = {}) { - writeFileSync(resolve(directory, views.profiles), renderProfiles({ directory })); + for (const [name, path] of Object.entries(views)) writeFileSync(resolve(directory, path), renderers[name]({ directory })); return { views: Object.keys(views).length }; } diff --git a/formal/tools/where.mjs b/formal/tools/where.mjs index 4aa98d93..354468f9 100644 --- a/formal/tools/where.mjs +++ b/formal/tools/where.mjs @@ -11,7 +11,15 @@ // data and no gate: this is the navigation a reviewer or an agent otherwise // assembles by hand. // +// For one model-fault challenge (recovery-inclusive-maximum) or one native +// mutant (M01) it prints the entry in full: the edit, the invariant, the +// mapping, the reproducer and the profile partition, or the rationale, the +// edits per port and the required detections. The generated index tables under +// formal/generated/ list the IDs. +// // node formal/tools/where.mjs C45 [--json] +// node formal/tools/where.mjs recovery-inclusive-maximum +// node formal/tools/where.mjs M01 import { readFileSync, readdirSync } from 'node:fs'; import { resolve } from 'node:path'; import { fileURLToPath } from 'node:url'; @@ -51,8 +59,10 @@ function contractRow(id, directory) { } export function lookup(query, { directory = root } = {}) { + if (/^M\d{2}$/.test(query ?? '')) return lookupMutant(query, directory); + if (/^[a-z][a-z0-9]*(?:-[a-z0-9]+)+$/.test(query ?? '')) return lookupChallenge(query, directory); const match = /^([CWEBX]\d{2})(?:\.([\w-]+))?$/.exec(query ?? ''); - if (!match) throw new Error(`${query}: expected a contract ID such as C45, a semantic case such as C45.recheck-after-decode or a native case such as B01.registration-and-policy-snapshot`); + if (!match) throw new Error(`${query}: expected a contract ID such as C45, a semantic case such as C45.recheck-after-decode, a native case such as B01.registration-and-policy-snapshot, a challenge ID such as recovery-inclusive-maximum or a mutant ID such as M01`); const [, id, caseName] = match; const caseId = caseName ? `${id}.${caseName}` : undefined; const row = contractRow(id, directory); @@ -104,7 +114,63 @@ export function lookup(query, { directory = root } = {}) { const plural = (count, word) => `${count} ${word}${count === 1 ? '' : 's'}`; +function lookupChallenge(id, directory) { + const challenge = (json('formal/catalogs/execution.json', directory).challenges ?? []).find(entry => entry.id === id); + if (!challenge) throw new Error(`${id}: not a challenge in formal/catalogs/execution.json`); + const mutants = json('formal/catalogs/mutations.json', directory).mutations ?? []; + const mutant = challenge.nativeMutants?.mutant ? mutants.find(entry => entry.id === challenge.nativeMutants.mutant) : undefined; + return { kind: 'challenge', ...challenge, mutantCase: mutant?.case }; +} + +function lookupMutant(id, directory) { + const mutant = (json('formal/catalogs/mutations.json', directory).mutations ?? []).find(entry => entry.id === id); + if (!mutant) throw new Error(`${id}: not a mutant in formal/catalogs/mutations.json`); + const rust = (json('formal/catalogs/rust-mutations.json', directory).mutations ?? []).find(entry => (entry.typescriptMutation ?? entry.id) === id); + const challenges = (json('formal/catalogs/execution.json', directory).challenges ?? []).filter(entry => entry.nativeMutants?.mutant === id).map(entry => entry.id); + return { kind: 'mutant', ...mutant, rust, challenges }; +} + +const block = text => String(text).split('\n').map(line => ` ${line}`).join('\n'); + +function renderChallenge(c) { + const lines = [`${c.id}: challenge on ${c.contract}, ${c.source} under ${c.model}:${c.invariant}`, '']; + lines.push('Edit', ' before:', block(c.before), ' after:', block(c.after), ''); + const native = c.nativeMutants ?? {}; + lines.push(`Native mutant: ${native.kind}${native.mutant ? ` ${native.mutant}${c.mutantCase ? ` (${c.mutantCase})` : ''}` : ''}`); + if (native.text) lines.push(block(native.text)); + if (native.crossContract) lines.push(' cross-contract:', block(native.crossContract)); + if (native.evidence) lines.push(` evidence checkpoint: ${JSON.stringify(native.evidence)}`); + if (c.measures) lines.push('', 'Measures', block(c.measures)); + const r = c.reproducer ?? {}; + lines.push('', `Reproducer${r.kind ? ` (${r.kind})` : ''}`); + if (r.run) lines.push(` run ${r.run} in ${r.model ?? c.model}`); + if (r.family) lines.push(` family ${r.family}`); + if (r.scope) lines.push(' scope:', block(r.scope)); + if (r.failure) lines.push(' expected failure under the fault:', block(r.failure)); + const profiles = r.profiles ?? []; + lines.push('', `Detected by ${plural(profiles.filter(p => !p.includes('/')).length, 'profile')}${profiles.some(p => p.includes('/')) ? ` and ${plural(profiles.filter(p => p.includes('/')).length, 'model')}` : ''}: ${profiles.join(', ') || 'none'}`); + const exclusions = Object.entries(r.exclusions ?? {}); + lines.push('', `Excluded (${exclusions.length})`); + for (const [profile, reason] of exclusions) lines.push(` ${profile}: ${typeof reason === 'string' ? reason : JSON.stringify(reason)}`); + return lines.join('\n') + '\n'; +} + +function renderMutant(m) { + const lines = [`${m.id}: ${m.description} (case ${m.case})`, '']; + if (m.rationale) lines.push('Rationale', block(m.rationale), ''); + for (const [port, spec] of [['TypeScript', m.typescript], ['Go', m.go], ['Rust', m.rust]]) { + if (!spec?.edits?.length) continue; + lines.push(`${port}: required detections ${spec.requiredDetections?.join(', ') || 'none'}`); + for (const edit of spec.edits) lines.push(` ${edit.path}`, ' before:', block(edit.before).replace(/^/gm, ' '), ' after:', block(edit.after).replace(/^/gm, ' ')); + lines.push(''); + } + lines.push(`Challenges mapped to it: ${m.challenges.join(', ') || 'none'}`); + return lines.join('\n') + '\n'; +} + export function render(result) { + if (result.kind === 'challenge') return renderChallenge(result); + if (result.kind === 'mutant') return renderMutant(result); const lines = [result.case ? `${result.case}: ${result.caseRule}` : `${result.id}: ${result.obligation}`, '']; if (result.case) lines.push(`Contract ${result.id}: ${result.obligation}`, ''); lines.push('Stated', ` formal/guides/CONTRACTS.md:${result.contractsLine} (evidence column: ${result.evidence})`); @@ -144,7 +210,7 @@ export function render(result) { export function parseArguments(args) { const flags = args.filter(arg => arg.startsWith('--')), positional = args.filter(arg => !arg.startsWith('--')); const unknown = flags.filter(flag => flag !== '--json'); - if (positional.length !== 1 || unknown.length) throw new Error('Usage: node formal/tools/where.mjs [--json]'); + if (positional.length !== 1 || unknown.length) throw new Error('Usage: node formal/tools/where.mjs [--json]'); return { query: positional[0], json: flags.includes('--json') }; } diff --git a/typescript/test/formal-catalog-docs.test.ts b/typescript/test/formal-catalog-docs.test.ts index ec37884c..1c42276d 100644 --- a/typescript/test/formal-catalog-docs.test.ts +++ b/typescript/test/formal-catalog-docs.test.ts @@ -1,22 +1,38 @@ import { readFileSync } from "node:fs"; import { describe, expect, it } from "vitest"; -const { renderProfiles, describeProfile, decodeWithProbes, checkCatalogDocs, views } = await import( +const { renderProfiles, renderChallenges, renderMutants, describeProfile, decodeWithProbes, checkCatalogDocs, views } = await import( new URL("../../formal/tools/generate-catalog-docs.mjs", import.meta.url).href, ) as { renderProfiles(options?: { directory?: string }): string; + renderChallenges(options?: { directory?: string }): string; + renderMutants(options?: { directory?: string }): string; describeProfile(id: string): { actions: Record unknown }>; channels: Array<{ name: string }> }; decodeWithProbes(decode: (choice: number, observed: unknown, environment: unknown) => unknown, choice: number): { input: unknown; touched: string[] }; checkCatalogDocs(options?: { directory?: string }): { views: number }; views: Record; }; const registry = JSON.parse(readFileSync(new URL("../../formal/catalogs/profiles.json", import.meta.url), "utf8")) as { profiles: Array<{ id: string }> }; +const execution = JSON.parse(readFileSync(new URL("../../formal/catalogs/execution.json", import.meta.url), "utf8")) as { challenges: Array<{ id: string; nativeMutants?: { mutant?: string } }> }; +const mutations = JSON.parse(readFileSync(new URL("../../formal/catalogs/mutations.json", import.meta.url), "utf8")) as { mutations: Array<{ id: string }> }; describe("generated catalog views", () => { - it("renders the committed PROFILES.md exactly, so the audit lane can check freshness without Quint", () => { - const committed = readFileSync(new URL(`../../${views.profiles}`, import.meta.url), "utf8"); - expect(renderProfiles()).toBe(committed); - expect(checkCatalogDocs()).toEqual({ views: 1 }); + it("renders the committed views exactly, so the audit lane can check freshness without Quint", () => { + const committed = (name: keyof typeof views) => readFileSync(new URL(`../../${views[name]}`, import.meta.url), "utf8"); + expect(renderProfiles()).toBe(committed("profiles")); + expect(renderChallenges()).toBe(committed("challenges")); + expect(renderMutants()).toBe(committed("mutants")); + expect(checkCatalogDocs()).toEqual({ views: 3 }); + }); + + it("indexes every challenge and every mutant in one row each and stays small", () => { + const challenges = renderChallenges(), mutants = renderMutants(); + for (const challenge of execution.challenges) expect(challenges, challenge.id).toContain(`| \`${challenge.id}\` |`); + for (const mutant of mutations.mutations) expect(mutants, mutant.id).toContain(`| \`${mutant.id}\` |`); + expect(challenges.split("\n").length).toBeLessThan(execution.challenges.length + 20); + expect(mutants.split("\n").length).toBeLessThan(mutations.mutations.length + 20); + const mapped = execution.challenges.find(challenge => challenge.nativeMutants?.mutant === "M01")!; + expect(mutants).toMatch(new RegExp(`\\| \`M01\` \\|.*\`${mapped.id}\``)); }); it("is deterministic and covers every registered profile and every descriptor action", () => { diff --git a/typescript/test/formal-where.test.ts b/typescript/test/formal-where.test.ts index e83c3bbd..5b884a5d 100644 --- a/typescript/test/formal-where.test.ts +++ b/typescript/test/formal-where.test.ts @@ -82,6 +82,21 @@ describe("contract lookup", () => { expect(render(lookup("C45.maximum-age-exclusive"))).toMatch(/^C45\.maximum-age-exclusive: After asynchronous decoding/); }); + it("prints a challenge or a mutant in full on demand", () => { + const challenge = lookup("recovery-inclusive-maximum") as unknown as { kind: string; contract: string; mutantCase?: string; reproducer?: { run?: string } }; + expect(challenge).toMatchObject({ kind: "challenge", contract: "C45", mutantCase: "C45.maximum-age-exclusive" }); + const text = render(challenge); + for (const part of ["Edit", "before:", "after:", "Native mutant: mapped M01", "Reproducer", "Excluded ("]) expect(text).toContain(part); + const mutant = lookup("M01") as unknown as { kind: string; case: string; challenges: string[]; rust?: unknown }; + expect(mutant).toMatchObject({ kind: "mutant", case: "C45.maximum-age-exclusive" }); + expect(mutant.challenges).toContain("recovery-inclusive-maximum"); + expect(mutant.rust).toBeDefined(); + const rendered = render(mutant); + for (const part of ["Rationale", "TypeScript: required detections", "Go: required detections", "Rust: required detections", "Challenges mapped to it: "]) expect(rendered).toContain(part); + expect(() => lookup("not-a-thing")).toThrow(/not a challenge/); + expect(() => lookup("M99")).toThrow(/not a mutant/); + }); + it("rejects an unknown contract, a malformed query, an unknown case and bad arguments", () => { expect(() => lookup("C99")).toThrow(/not a contract in formal\/guides\/CONTRACTS.md/); expect(() => lookup("recovery")).toThrow(/expected a contract ID/);