| 1 | # rule outcome reason. Read by mutate.sh: a rule listed `missed` is not |
| 2 | # expected to be caught alone, by the random sweep or by its witness |
| 3 | # (witness_test.go), and is reported EXPECTED-MISS; the sweep fails if it |
| 4 | # is caught (the expectation is stale). Spec §14.2.5 gives the |
| 5 | # combination that catches each, or why none does. A rule listed `rare N` |
| 6 | # has no witness and the random sweep reaches it only at N seeds or more |
| 7 | # (rev 7.11); below N its miss is expected. |
| 8 | claim-cas-opid missed caught with revalidate-before-effect |
| 9 | config-before-probe missed liveness only: a target that cannot render config fails its probe and rolls back |
| 10 | readiness-key missed liveness only: T2 avoids a pointless cut |
| 11 | readiness-quiet missed unreachable under claim rev 4: acknowledgements wait out their own horizon and CC11 holds |
| 12 | watchdog-independent missed caught with declare-lost-compute (witness; sweep 3 / 100,000 on rev 7.2); alone, compute fencing makes it redundant |
| 13 | exec-admission missed one of four admission fences (claim rev 6.8.1 adds exec-writer); caught with hold-op-open, start-check-claim-gen and exec-writer |
| 14 | hold-op-open missed one of four admission fences; caught with exec-admission, start-check-claim-gen and exec-writer |
| 15 | touched-incomplete missed caught with legacy-discovery |
| 16 | door-reread missed subsumed by C3a and, since rev 7.8, by writer epochs (claim rev 6.6): a recreated incarnation writes into a fresh generation the listing never selects; its witness is retired |
| 17 | door-by-version missed subsumed by C3a and, since rev 7.8, by writer epochs (claim rev 6.6): a recreated incarnation writes into a fresh generation the listing never selects; its witness is retired |
| 18 | registration-check missed a cheap extra: subsumed by purge-claim-fence and fence-etag together |
| 19 | exec-writer missed one of four admission fences (claim rev 6.8.1): the AdmitWriter CAS refuses a box that is not op.exec; caught with exec-admission, hold-op-open and start-check-claim-gen (witness) |
| 20 | admit-bind-op missed caught with claim-cas-opid: the model's general CAS condition on op.id (C2) already refuses a closure whose operation changed; the binding adds the phase and the kinds in which no writer opens, and its witness needs both gone |
| 21 | hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start) |
| 22 | stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10) |
| 23 | strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10) |
| 24 | create-choice-once missed no box-side effect precedes the serving CAS in this model, so a substituted executor leaves nothing behind; the rule's effect is the cancellation of a create whose box is gone (TestCreateNamesItsExecutorOnce fails under the mutation) |
| 25 | reloc-start-guard missed the chooser's §2 eligibility already excludes a target owing a park-local, a live source never owes one for the host it serves, and a whole-location chore cannot be pending in the region the host serves in (a move into it waits, CC11); TestRelocationStartGuardRefuses shows the refusal |
| 26 | reloc-exec-ack-barrier missed liveness in the sweep: without the barrier a target that never acknowledged is handed op.exec and the operation waits there instead; TestReplacementWithoutAcknowledgementHoldsEachTransition fails under the mutation (rev 4) |
| 27 | reloc-pin-reaches-release missed the release's step 2 already waits for the listing to show N, so in the sweep the pin's own check is never the first to see a short listing; TestPinNeverShortOfTheRelease hides the newest file after the release and fails under the mutation (rev 4) |
| 28 | reloc-failover-pin-delay missed a loss bound, not a safety bound (§5.8): the pin names exact versions and a later PUT adds a version nothing reads; TestFailoverPinWaitsOutTheDelay fails under the mutation (rev 4) |
| 29 | reloc-exec-only-installs missed every installing CAS is conditional on op.exec, so in the sweep a non-executor's writes are the same create-only objects and its install is retired by its park-local; TestOnlyTheExecutorWritesP lets only the source act at installing and fails under the mutation (rev 4) |
| 30 | reloc-install-receipt missed caught with reloc-ensure-local (witness): EnsureLocal restores a replacement's missing install whatever the receipt says, as 1b-next rev 14 found ("each covers the other") |
| 31 | reloc-row-cases missed caught with exec-admission and exec-writer (witness): a reopened stale row routes a request to a box the exec check and AdmitWriter refuse |
| 32 | reloc-replacement-cap missed an operator bound: without the cap the operation replaces its target a third time instead of waiting for carlos ops host resolve; TestStuckAfterTwoReplacements fails under the mutation |
| 33 | reloc-drain-needs-writer missed liveness only (1b-next ruling 11): a never-woken host's drain would wait for a release root refuses, until the release deadline; TestDrainRefusedForANeverWokenHost fails under the mutation |
| 34 | reloc-ack-before-pinning missed defence in depth (1b-next rev 4 N6): installing still waits for the barrier, so a replaced target that never acknowledged holds the operation at pinning instead of releasing; TestReplacedTargetAcknowledgesBeforePinning fails under the mutation |
| 35 | reloc-probe-attempts missed liveness only (ruling 19): uncounted attempts still end at the probe deadline; TestProbeAttemptsCountedBeforeTheyAreMade fails under the mutation |
| 36 | fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; TestStoppedBoxNeverFenced fails under the mutation |
| 37 | reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does; TestL18NestedFailover fails under the mutation (no nested failover) |
| 38 | files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads; TestInstallAppliesThePinnedManifest lands the newer manifest between the pin and the install and fails under the mutation (rev 4) |
| 39 | reloc-abandoned-prepared missed the at-rest sweep, which 1b-next ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it; the operation's own park is the rule's effect, and TestAbandonedPreparedGenerationParked (both paths) fails under the mutation |
| 40 | reloc-stuck-refuses-admission missed the stuck operation's live source is still op.exec, so admitting its wake makes no second writer; the refusal keeps a stuck operation from running anything until the operator resolves it (ruling 9); TestStuckSourceRefusesAdmission fails under the mutation |
| 41 | ha-sole-box-eligibility missed the sweep's HA regions keep two boxes until a termination, and a depleted region's last box is normally eligible; TestHASoleBoxIsCheckedLikeAnyOther checks each refusal and fails under the mutation |
| 42 | reloc-pin-delay-every-fence missed a loss bound like reloc-failover-pin-delay; TestPinWaitsForEveryFenceObservation replaces the target after the source's release and fails under the mutation |
| 43 | reloc-deadline-from-observed-at missed liveness: a deadline from the termination marks stuck earlier than 1b-next would, which the operator then resolves; TestDeadTargetDeadlineFromObservation delays the observation past the deadline and fails under the mutation |
| 44 | tie-hash-host missed a preference: either winner is a correct choice; TestTieHashFollowsTheHost computes both hosts' winners independently and fails under the mutation |
| 45 | reloc-failover-ack-before-pin missed a loss bound like reloc-failover-pin-delay: an initial failover's pin selected before its target acknowledged misses only files that land later, and the sweep's controllers acknowledge within a step of being named; TestFailoverPinWaitsForTheAcknowledgement holds the target's controller while the newer manifest lands and fails under the mutation |
| 46 | reloc-name-before-pin missed a loss bound like reloc-failover-pin-delay: a converted move's or a replay's pin selected before a target is named misses only files that land while no box is eligible; TestConvertedMoveWaitsForATargetBeforeItsPin holds every box ineligible while the newer manifest lands and fails under the mutation |
| 47 | reloc-failover-start-guard missed a fidelity guard: the mutation starts the failover earlier (no target yet, admission closed, a park-replica outstanding), and no model invariant distinguishes the earlier start, whose target is then named at pinning; TestFailoverStartWaitsForAdmission and TestFailoverStartWaitsForParkReplica fail under the mutation |
| 48 | reloc-fence-pending-blocks missed a fidelity guard: under the mutation the phase moves on while a dead target's fence waits for a spare, and the fence is consumed later by the replacement table at whatever phase the operation reached, which no model invariant distinguishes; TestPendingTargetFenceHoldsThePhase fails under the mutation |
| 49 | reloc-release-needs-flush missed a fidelity guard: the mutation's unflushed release is legal in the model (the next admission declares what the remote does not hold, as writes_lost), so no invariant fails, but 1b-next refuses it and waits for the deadline; TestReleaseRefusedAfterACrashBeforeTheFlush and TestReleaseReplaysTheRecordedFlush fail under the mutation |
| 50 | operator-stop-unrecoverable-only missed a fidelity guard on the operator's resolve: the mutation stops a target that could still release, and the declared loss and replay that follow are legal in the model, so no invariant fails; TestOperatorResumesASlowRelease and TestOperatorResumesARecordedFlush fail under the mutation |
| 51 | reloc-release-needs-receipt missed a fidelity guard: under the mutation recorded positions replay without root's receipt, and the release they journal is the flushed one, so no model invariant fails, but 1b-next refuses it after a restart; TestReleaseRefusedAfterACrashBeforeTheReceipt and TestOperatorStopsATargetWithNoReceipt fail under the mutation |
| 52 | reloc-name-drops-move-target missed liveness: under the mutation a converted move's own target stays on the barrier and stalls the relocation only if that box never acknowledges, which the sweep does not produce (0 of 3,000 at two boxes, 0 of 300 at one box, on this revision); TestConvertedMoveDropsTheMoveTargetFromTheBarrier stops the move's target and fails under the mutation |
| 53 | reloc-c1-failed-release-refused missed a fidelity guard for today's fallback (claim ask C1 open): under the mutation a failed target releases and the nested relocation follows, which is the post-C1 behaviour and legal in the model, so no invariant fails; TestFailedTargetCannotReleaseWithoutC1 fails under the mutation (L18 joint round finding 4) |
| 54 | reloc-c11-later-attempt-refused missed a fidelity guard for today's fallback (claim ask C11 open): under the mutation a later cold attempt after P's opening is counted and made, which is the post-C11 behaviour and legal in the model, so no invariant fails; TestLaterAttemptRefusedWithoutC11 fails under the mutation (L18 joint round finding 4) |
| 55 | reloc-admits-probe-only missed a fidelity guard (L18 joint round 2 finding 3, relocatingAdmission): under the mutation the source's wake in starting or releasing admits a new session, as the model did before, and the release then stops that session and flushes it, so no invariant fails; TestNoAdmissionBetweenStopAndFence fails under the mutation |
| 56 | |
amadan