| 1 | package hostlife |
| 2 | |
| 3 | import ( |
| 4 | "os" |
| 5 | "strings" |
| 6 | ) |
| 7 | |
| 8 | // Every protocol rule the model enforces has a name here. The mutation |
| 9 | // harness (spec §14.2) runs one prebuilt test binary with HOSTLIFE_MUTATE |
| 10 | // set to one rule name (or a comma-separated combination), and requires at |
| 11 | // least one seed to fail. A rule whose mutation no seed catches is either |
| 12 | // redundant or untested, and the run says which. |
| 13 | // |
| 14 | // Never edit `mutated` in place; the harness sets HOSTLIFE_MUTATE. |
| 15 | var mutated = "" |
| 16 | |
| 17 | // HOSTLIFE_MUTATE sets `mutated` for one run of a prebuilt test binary, so |
| 18 | // the mutation harness never edits or copies the source (mutate.sh). |
| 19 | func init() { |
| 20 | if v := os.Getenv("HOSTLIFE_MUTATE"); v != "" { |
| 21 | mutated = v |
| 22 | } |
| 23 | } |
| 24 | |
| 25 | func on(rule string) bool { |
| 26 | for _, m := range strings.Split(mutated, ",") { |
| 27 | if m == rule { |
| 28 | return false |
| 29 | } |
| 30 | } |
| 31 | return true |
| 32 | } |
| 33 | |
| 34 | // allRules is the mutation list, in spec order. The comment names the |
| 35 | // finding or spec section each rule answers. |
| 36 | var allRules = []string{ |
| 37 | // claim spec |
| 38 | "claim-op-exclusive", // C2/§4: one operation at a time |
| 39 | "claim-cas-opid", // C2: every CAS conditional on op.id |
| 40 | "revalidate-before-effect", // C3: a worker re-reads under its lease before acting |
| 41 | "sign-before-safeuntil", // C3/§3.1: a paused round signs only before its lease's SafeUntil |
| 42 | "sign-at-check", // model 18: signed at the check, so S3's age limit bounds any later pause |
| 43 | "sdk-no-resign", // claim rev 5 C3 (CC19): the SDK\'s retry resends the original signature |
| 44 | "location-per-incarnation", // claim rev 4 C3a (J2-R2-1): no location shared between incarnations |
| 45 | "fresh-admission", // C4: admission reads the claim fresh |
| 46 | "exec-admission", // C4/K1: op.exec names this box (and the role column, which is op.exec here) |
| 47 | "recovery-pass", // C2/§8: console claim-recovery pass |
| 48 | "fresh-incarnation", // §5.1/R3-12 |
| 49 | "touched-incomplete", // §9/J-N5: adopted legacy parks every region |
| 50 | "legacy-discovery", // this model's finding: park legacy residue at adoption |
| 51 | "obligations-block-ops", // this model's finding: no op over a pending chore |
| 52 | "park-by-version", // C3/J-N1: destructive calls name versions |
| 53 | "park-all-versions", // §6.2 step 5: noncurrent versions too |
| 54 | "park-skip-lock", // §6.2 step 2/J-N6 |
| 55 | "retirement-ids", // §6.2/J-D5/J-N7 |
| 56 | "hostguard", // §6.4/J-N8 |
| 57 | "fence-by-installation", // claim rev 6.5 §6.4 (R3-3): a new installation of a retired incarnation sets its own active stamp; the mutation is rev 5.2's marker, retired for good |
| 58 | "fence-stamp", // claim rev 6.5 §6.4 (R4-2): a writer is admitted only if its stamp equals the active stamp; the mutation admits any writer for the incarnation while one is active |
| 59 | "purge-reserve-first", // §5.3/J-N9 |
| 60 | "purge-adopts", // this model's finding: purge claims unclaimed legacy records first |
| 61 | "purge-journal", // this model's finding: the reservation is the purge's journal |
| 62 | "admission-registration", // claim rev 4 §5.1 step 0, §5.3 step 1b (J2-R2-2) |
| 63 | "registration-recovery", // CC16: a registration is a lease, so a dead create cannot block purge |
| 64 | "registration-check", // claim rev 5.1 §5.3: the creator re-reads its registration before its claim CAS (cheap, not sufficient) |
| 65 | "purge-claim-fence", // claim rev 5.1 §5.3 (CC21): purge fences a free host claim before removing a registration |
| 66 | "fence-etag", // claim rev 5.2 §5.1 (CC22): the creator's claim CAS is If-Match the ETag read at registration (If-None-Match: * if absent); a 412 restarts the create |
| 67 | "claim-never-deleted", // claim rev 5.2 C5a (CC22): a claim object is never deleted; a fence on an absent claim is released by writing free |
| 68 | "cancelled-creates", // claim rev 4 §5.1 (J2-R2-7): a late record PUT is removed |
| 69 | "orphan-no-deadline", // CC17: ... whenever it lands, not only before `until` |
| 70 | "orphan-order", // claim rev 6 §5.1 step 5 (R3-2): read the record, then the claim fresh, then DeleteIfMatch; the mutation reads the claim first |
| 71 | "door-by-version", // §6.5/J-N10 |
| 72 | "door-reread", // claim rev 4 §6.5 (J2-R2-4): O2 refuses if the holder or op changed |
| 73 | "strict-spawn", // §6.1/J-D3 |
| 74 | "evidence-whole-tree", // §6.1: stray and non-strict processes |
| 75 | "evidence-from-state", // §6.1/R2-2 |
| 76 | "watchdog-independent", // §7.1 self-fencing outside the agent |
| 77 | "declare-lost-compute", // §7.2 compute fencing (this model's finding) |
| 78 | "lost-quarantine", // §7.2 |
| 79 | "floor-boot-recovery", // §10/J-N12 |
| 80 | "participant-rows", // claim §2/R2-4 |
| 81 | "stale-hold-release", // this model's finding: release a hold whose op ended |
| 82 | "restore-by-generation", // C3a + moves rev 6 §5.1: restore replays the claim's generation only |
| 83 | "restore-overlap", // rev 7.5 §5.1 (R4-1): the planner takes a file whose range overlaps the one restored so far (litestream's rule); the mutation requires min == current+1 and discards a compacted continuation |
| 84 | "restore-gap-closed", // rev 7.5 §5.1 (R4-1): a current file that starts beyond current+1 once nothing extends the range is a gap, and the restore refuses; the mutation returns what it has |
| 85 | "restore-anchor", // rev 7.6 §5.1 (R5-1): a cold restore with no level-0 file at its position writes the anchor [cur,cur] before replication starts; the mutation leaves the position to litestream's open |
| 86 | "root-advance", // rev 7.6 §5.1 (R5-3): the restore roots at the newest current successor snapshot at or past the pinned one; the mutation roots at the pinned snapshot only |
| 87 | "anchor-acked", // rev 7.7 §5.1 step 7 (R6-1): replication opens only once the anchor PUT is acknowledged, and the position is read from the listing; the mutation opens at once with whatever the listing shows |
| 88 | "return-stamp", // claim rev 6.5 (R6-4): the CAS that returns execution to the source writes holder.stamp = the source installation's stamp from the journal; the mutation leaves the target's |
| 89 | "recovery-generation", // claim rev 6.6 §6.4a (R7-1): a wake with lost replication state is a cold recovery, an installing CAS into a fresh generation; the mutation restarts in the same generation (rev 7.7) |
| 90 | "closed-marker", // claim rev 6.6 §6.4a (R7-1): a generation is continued only if closed.json exists with max_txid at the remote maximum and the box's active stamp, and the marker is consumed; the mutation takes any marker as intact |
| 91 | "close-waits", // claim rev 6.6 §6.4a (R7-1): a clean close writes closed.json only after every upload returned; the mutation writes it at once |
| 92 | "newest-l0", // rev 7.8 §5.1 step 8 (R7-3): every retention path keeps the newest level-0 file; the mutation is rev 7.6's deletion of inputs and of every file below the previous snapshot |
| 93 | "build-completion", // rev 7.8 §7.6 (R7-4): generation.json is published only from a completed build, snapshot and anchor acknowledged; the mutation publishes from the intent |
| 94 | "writer-session", // claim rev 6.8 §6.4a (R8-1): a warm admission needs the certificate of the observed holder.session and moves the session forward, so a certificate is one-use; the mutation takes the newest certificate of any session and moves nothing |
| 95 | "admit-everywhere", // claim rev 6.8 §6.4a (R8-2): every path that opens replication is an AdmitWriter, a committed landing's serving, a probe restart, a reverted source, an opened rollback included; the mutation gates ordinary wakes only |
| 96 | "exec-writer", // claim rev 6.8.1 (D1): the AdmitWriter CAS requires op.exec to be this box, in every operation; the mutation admits any box the phase table reaches |
| 97 | "remote-baseline", // claim rev 6.9 §6.4a (R9-1): a box never reuses its local database; every admitted writer purges it and restores from the certified remote baseline; the mutation keeps a local database of the generation it opens, as today's activator does |
| 98 | "writes-lost", // claim rev 6.9 §6.4a (R9-2): a cold admission whose observed session had no certificate records writes_lost {box: holder.writer_box, generation, session, remote_max_txid} and alerts; the mutation loses the writes silently |
| 99 | "admit-before-start", // claim rev 6.10 §6.4a (R10-1): the admitting CAS comes before the app starts, so nothing the app acknowledges is outside a session; the mutation admits after readiness, as rev 7.10 did, and a background acknowledgement before the CAS is lost silently |
| 100 | "baseline-live", // claim rev 6.10 (R10-2): an unfinished admission's predecessor is live until generation.json names the new generation; the retire chore is queued then; the mutation queues it at the CAS and sweeps the predecessor as dead |
| 101 | "admit-bind-op", // claim rev 6.9 §6.4a (R9-4): the AdmitWriter CAS is bound to the observed op.id and phase, serving's "" compared literally; the mutation compares session and generation alone |
| 102 | "valid-ltx", // rev 7.9 §5.1 step 9 (R8-3): an empty generation gets no LTX file, never a zero-TXID snapshot or anchor; the mutation writes [1,0] and [0,0] |
| 103 | "close-evidence", // claim rev 6.8 §6.4a (R8-5): a certificate needs every request of the writer's lifetime returned with success and no retry after a timeout; the mutation looks at the level-0 queue alone |
| 104 | "quiet-before-ack", // this model's finding (late writes after a park) |
| 105 | "straggler-sweep", // claim rev 5 §6.2a (CC15): the at-rest sweep |
| 106 | "sweep-staging", // CC20: the sweep also covers moves/<host>/ |
| 107 | "sweep-namespace", // claim rev 6 §6.2a (R3-4): the sweep discovers locations from the namespace; the mutation reads the capped retired_incarnations |
| 108 | "live-set-region", // claim rev 6.5 §6.2a (R4-3): the live set is {authoritative region, location, generation}; the mutation exempts matching keys in every region |
| 109 | // moves spec |
| 110 | "record-first-close", // rev 7.23 §7.5, §19 K8 (ruling M4): a move's close CASes the record (move into last_move) before the claim's release, and the recovery pass releases from last_move; the mutation is rev 7.22's claim-first close, whose record half the recovery pass wrote after the release |
| 111 | "seal-by-version", // J-N2: landing copies sealed versions |
| 112 | "staging-quiet", // J-N2: staging retired after its writers' horizon |
| 113 | "commit-before-open", // INV-5 |
| 114 | "hold-op-open", // §5.2 conditional open |
| 115 | "start-check", // INV-4: markers agree |
| 116 | "start-check-claim-gen", // rev 6 §5.1 (R2-8): and name the generation the claim expects |
| 117 | "generation-conditional", // rev 7.1 §5.1 (model 29): generation.json is written If-Match the marker it supersedes |
| 118 | "markers-last", // R2-6 |
| 119 | "revert-journal", // J-N11 |
| 120 | "fence-converts-moving", // moves rev 7.20 §7.10, claim rev 6.28 §4: a terminated source of a pre-flip move converts the op to relocating at pinning (exec none, stamp and generation kept, obligations untouched, the lane's park queued); a replacement box of the region takes it; without the rule the move never converges |
| 121 | "rollback-journal", // R2-3 |
| 122 | "dirty-return", // INV-2 |
| 123 | "seal-return", // rev 7.11 §7.8: a rollback whose source replica stops short of the stopped database returns the seal |
| 124 | "clean-return-identity", // claim rev 6.12, R11-4: the predecessor is the last admitted writer, and a clean return with src_covered declares nothing |
| 125 | "foreign-region-uncovered", // claim rev 6.14 item 5: a predecessor in another region stays uncovered, never queued into its region from here (R12-3) |
| 126 | "cover-at-park", // claim rev 6.14 item 6: CoverRegionPredecessors inside the CAS that queues a region's whole-location park (R12-3) |
| 127 | "session-scoped-loss", // rev 7.13 §14.2.3: a writes_lost record exempts the writes of the session it names, no other (R12-1) |
| 128 | "probe-window", // rev 7.13 §7.7: a probe attempt's deadline is checked before the start and before readiness is accepted (R12-2) |
| 129 | "absent-marker-origin", // rev 7.12 §6.4: the sweep reads an absent generation.json as the origin (R11-1), isolated from baseline-live |
| 130 | "persisted-park-scope", // claim rev 6.15 §2: a remote chore's park scope is persisted, so a retry after an agent restart keeps the original evidence time (R13-4) |
| 131 | "holderless-park", // claim rev 6.15 §6.2a: a free host's sweep is a holderless parking op that blocks the successor create until FreeAfterPark (R13-4) |
| 132 | "covered-baseline-refused", // claim rev 6.22 §6.2a: walking an unfinished run, a covered foreign link is passed over and a covered local generation reached as a needed baseline refuses the start (R13-1) |
| 133 | "restore-selected-baseline", // rev 7.15 §5.1: the start restores the generation the run walk selected, rooted at [1, 1], as the oracle does; not the marker's alone (R14-1) |
| 134 | "unique-declarations", // claim rev 6.22 item 2: writes_lost plus additional_writes_lost, unique by (box, session); the source's cut session joins the list and is never declared twice (R14-2) |
| 135 | "scope-membership", // claim rev 6.24 §2: a park executes strictly within its scope's namespace; the legacy instances/<host> scope excludes child incarnations and an instances scope never touches moves/ (R16-1, R16-2) |
| 136 | "lost-return-park", // rev 7 §7.10 (model 27): declare-lost parks a return lane the lost target had begun (rev 7.2: a biased schedule stops the target mid-return) |
| 137 | "target-park", // R2-5/INV-10 |
| 138 | "abort-target-owner", // J-N13 |
| 139 | "timer-freeze", // J-N14 runner bookkeeping |
| 140 | "timer-canonical", // J-N14 prune path |
| 141 | "cut-deadline", // J-N15 |
| 142 | "readiness-key", // T2 |
| 143 | "source-readiness", // S1: the source can run the instance before the cut |
| 144 | "readiness-quiet", // T12: the target region's quiet_after has passed |
| 145 | "files-carried", // §8 (the kpmg outage) |
| 146 | "config-before-probe", // L3 (the kpmg outage) |
| 147 | "recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs |
| 148 | // region HA (two boxes per region, L18) |
| 149 | "create-choice-once", // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone |
| 150 | "reloc-start-guard", // region HA §5.8, claim §4 CC11 as L11 amends it (plan 1b-next RelocationStartGuard): a park-generation in the region never blocks a relocation start; a park-replica in the region and a park-local on the target or a live source do |
| 151 | "reloc-exec-ack-barrier", // claim D6, region HA §5.8 (requireAcks): every participant's execution lease is current before the operation leaves starting or hands op.exec to the target |
| 152 | "reloc-release-first", // region HA §5.8 releasing, A3-2 (PinAfterRelease): pinning cites the source's journaled release; the mutation pins while the source still runs |
| 153 | "reloc-pin-reaches-release", // region HA §5.8 (JournalPin): a pin after a release reaches its final_txid; the mutation pins the listing as it stands |
| 154 | "reloc-failover-pin-delay", // region HA §5.8 (JournalPin, FailoverPinDelay): a failover pins no earlier than the fence's observed_at plus 30 s; a loss bound, not a safety bound (expected miss) |
| 155 | "reloc-exec-only-installs", // region HA §5.8 Exclusion, HA2: only op.exec builds P and makes the local install; the mutation lets every box of the region materialize |
| 156 | "reloc-install-receipt", // region HA §5.8 B1-2 (RecordLocalInstall, ToProbing): probing needs a receipt for exactly op.exec and install_stamp; the mutation lets a replacement inherit its predecessor's and skip its install |
| 157 | "reloc-no-reinstall", // region HA §5.8 B2-5 (RecordLocalInstall after preparedOpened): after P's first admission the local install is never remade; the mutation reapplies the pinned wake state on every agent restart |
| 158 | "reloc-released-coverage", // claim §6.4a item 2, L9 (AdmitWriter): released only on the admission opening P whose predecessor is exactly the flushed release's box and session and whose pin reached final_txid; the mutation grants it to every first opening of P, a failover's included |
| 159 | "reloc-row-cases", // region HA §5.3, L12 (hostbox.RelocationRow): the former executor's row is held once its admission fence closed; the mutation reopens it as a stale hold (an admission fence: caught with exec-admission and its partners) |
| 160 | "reloc-replacement-cap", // region HA §5.8 (replaceTargetSlot, MaxTargetReplacements): a third replacement of the target marks the operation stuck; an operator bound (expected miss) |
| 161 | "reloc-enrolled-only", // region HA §2, HA7 (eligibleBoxes): an unenrolled reference is never chosen as a target; Task 3 gives it its witness |
| 162 | // plan 1b-next rev 16's additions to the phase table (rev 2 of this plan) |
| 163 | "reloc-drain-needs-writer", // 1b-next ruling 11 (Worker.Start): a host that never admitted a writer is never drained, only failed over; liveness (expected miss) |
| 164 | "reloc-ack-before-pinning", // 1b-next rev 4 N6 (PinAfterRelease requires requireAcks from releasing): a target replaced in releasing acknowledges before the operation leaves the phase; defence in depth (expected miss) |
| 165 | "reloc-pin-claim-gen", // 1b-next ruling 16 (JournalPin, RecoveryPinKey pin-<gen>.json): a pin is journaled only against the claim version it was selected against; the mutation journals a pin selected before a nested reset |
| 166 | "reloc-pin-evidenced-empty", // 1b-next ruling 15 (JournalPin, StorePinner's Empty evidence): an empty pin needs a release flushed at 0 or a holder that never had a writer; otherwise stuck for an operator; the mutation pins the empty listing and the install loses the durable writes (caught by its witness, INV-2) |
| 167 | "reloc-release-deadline", // 1b-next ruling 14 (Worker.releaseOverdue, ReleaseDeadline): a release not journaled 10 minutes after releasing or probe-failed began marks the operation stuck; the mutation waits forever (INV-3) |
| 168 | "reloc-probe-attempts", // 1b-next ruling 19 (BeginProbeAttempt, MaxProbeAttempts): each probe attempt is counted in the claim before it is made, the fourth is probe-failed; liveness (expected miss) |
| 169 | "reloc-ensure-local", // 1b-next rev 15 finding 2 (Effects.EnsureLocal): before P's first admission the local install is verified, and restored under the same install_stamp if a lost lease's scoped cleanup retired it; the mutation admits over a missing install |
| 170 | "reloc-verify-receipt", // 1b-next rev 16 finding 1 (Effects.VerifyReceipt, MarkStuck in probing): after P opens, a missing or different receipt marks the operation stuck before any further admission; the mutation makes the attempt anyway |
| 171 | "reloc-prepared-opened-journal", // 1b-next rev 12 S1 (prepared_opened, PreparedOpened): P's opening is journaled with its admission and outlives holder.admissions' trim; the mutation reads the trimmed list and remakes the install after P opened |
| 172 | // termination, the fence and the replacement table (Task 3) |
| 173 | "fence-terminated-only", // region HA §5.9 "What never counts", H10, H19 (termfence.Verify, VerifyFence): only a terminated, enrolled box is fenced; the mutation fences a stopped box, which may start again with its disk |
| 174 | "fence-discharge-qualified", // region HA §5.9, L3, H19 (fenceBox with LocalDischarge): a fenced box's park-local chores are discharged automatically only when every volume record qualifies; the mutation discharges regardless (INV-26) |
| 175 | "fence-declares-timers", // moves §7.10, region HA §5.9 (the D4 loss record, timer knowledge partial): the timers acknowledged on a fenced box are declared lost and alerted; the mutation drops them silently |
| 176 | "fence-reassigns-regional", // 1b-next rev 6 finding 2 (fenceBox, as DeclareLost's reassign_regional): the fence passes the dead box's park-generation and park-replica chores to its region; the mutation leaves them with the dead box, where nothing runs them |
| 177 | "reloc-source-loss", // region HA §5.8 B1-6 (FenceSource): a source terminated before its release is journaled makes the operation a failover, which declares its writes; the mutation takes it as released at what the remote holds |
| 178 | "reloc-replacement-table", // region HA §5.8 (ReplaceTarget): a target lost after P's first admission is a nested failover from holder.generation; the mutation resumes at installed with the same P (the admission rules refuse the reopening: expected miss, see expected-outcomes.txt) |
| 179 | "reloc-replace-not-owing", // 1b-next rev 6 finding 1 (replaceTargetSlot's ErrPendingChore, Worker.next's LocalChoreBoxes): a replacement target never owes a park-local for the host, in the chooser and inside the CAS; the mutation lifts both for a relocation's target |
| 180 | "reloc-exhausted-fence", // 1b-next ruling 23 as rev 9 amended it (FenceExhaustedTarget): an exhausted target's fence while the live source is op.exec records stuck and changes nothing else; the mutation is rev 8's, op.exec none at pinning, revoking the source without its stop evidence |
| 181 | // the files publisher, the files pin and the files live set (Task 4) |
| 182 | "files-pin-exact", // region HA §5.8 the pinned recovery set, B2-4 (RecoveryPin.FilesManifest, StorePinner, ruling 21's retained copy): the local install applies the manifest version the pin names; the mutation reads the newest at install time. A determinism rule: a later PUT adds a version nothing reads (expected miss) |
| 183 | "files-live-set", // region HA §5.6, L13, claim §6.2a (the classifier's files live set, 1b-next rev 12 finding 1's referenced origins): a park-generation never archives the live manifest of the chain, holder.generation's, P's or the pinned one; the mutation archives them with their dead generation |
| 184 | "files-prepared-seq-zero", // claim rev 6.30 R18-1, moves rev 7.22 §7.6, 1b-next rev 15 finding 1 (CopyPinnedManifest, PreparedAuthority.FilesSeq 0): P's prepared manifest is at sequence 0 and the session publisher starts at 1; the mutation keeps the source's sequence, so a later pin takes the stale prepared manifest over the session's (INV-28) |
| 185 | // plan 1b-next rev 17 to 19's fixes for the model's findings F1 to F3 (rev 3 of this plan) |
| 186 | "reloc-no-spare-bound", // 1b-next ruling 26 (rev 17, F1): probe-failed with no eligible spare is stuck ReleaseDeadline after probe_failed_since, never sent to the source; the mutation waits for ever (INV-3) |
| 187 | "reloc-dead-target-bound", // 1b-next rev 18 finding 2 (FenceTargetWithoutSpare): a dead target with no spare is fenced into stuck ReleaseDeadline after its observed_at; the mutation waits for ever (INV-3) |
| 188 | "reloc-abandoned-prepared", // 1b-next ruling 27, rev 18 finding 3 (abandonPrepared, abandoned_prepared): every unopened P that is replaced or dropped, on every path, is parked at completion; the mutation records none (INV-10) |
| 189 | "files-pin-needs-key", // 1b-next ruling 25 as rev 18 amended it (F2, L21): a nonempty database with an admitted writer pins only a manifest carrying instance.key, else stuck; the mutation pins it keyless and the install mints a fresh key (INV-4) |
| 190 | // Astra's round 1 on this plan (rev 4) |
| 191 | "reloc-stuck-refuses-admission", // 1b-next relocationAdmission's stuck check (ruling 9, R1-16): a stuck operation admits no writer, the live source's ordinary wake included; the mutation admits it |
| 192 | "ha-sole-box-eligibility", // region HA §2 with region HA on: the last remaining box of a region is checked for enrollment, key, executable, lost and park-local like any other; the mutation keeps the one-box shortcut |
| 193 | "reloc-pin-delay-every-fence", // JournalPin checks every retained fence observation, after a release too (a target replaced after the source's release); the mutation skips the delay once a release exists |
| 194 | "reloc-deadline-from-observed-at", // FenceTargetWithoutSpare's deadline runs from the fence record's observed_at; the mutation runs it from the termination, which no worker saw |
| 195 | "tie-hash-host", // claim P5-D2, 1b-next R18-2 (ExecutorChooser hashes the record's host): the tie-break is SHA-256(host + "\x00" + box); the mutation hashes a constant name |
| 196 | "files-origins-referenced", // 1b-next rev 12 finding 1 (filesPin's referencedOrigins, R11-1): the pin authorizes the generations the pinned manifest's objects lie in, never only those the trimmed admission list names; the mutation refuses an unchanged file's old origin and the failover waits for ever (INV-3) |
| 197 | "files-objects-region-bound", // §5.6 region binding (filesPin: the object in this region's data bucket): a host that came from another region uploads its unchanged files again before naming them; the mutation keeps naming the source region's objects and the failover can never pin (INV-3) |
| 198 | "files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3) |
| 199 | "reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29) |
| 200 | "fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3) |
| 201 | "reloc-release-needs-receipt", // rev 11 (Astra round 8; 1b-next rev 19 Task 7 Release, RecoveryReleaseDrain): recorded positions finish a release only for the controller that recorded them, or with root's durable receipt after a restart; the mutation replays the positions alone (TestReleaseRefusedAfterACrashBeforeTheReceipt, TestOperatorStopsATargetWithNoReceipt) |
| 202 | "operator-stop-unrecoverable-only", // rev 10 (Astra round 7; plan ruling 13, no 1b-next code): the operator stops a live target that has not released only when its release is unrecoverable (no recorded flush, and the session's replicator or its files gone); otherwise the resolve resumes the release; the mutation stops every such target (TestOperatorResumesASlowRelease, TestOperatorResumesARecordedFlush) |
| 203 | "reloc-release-needs-flush", // rev 9 (Astra round 6; 1b-next rev 19 Task 7 Release, relocationFlushDB, ReleaseFlushFiles, ReleasePositions): a release needs the session's own replicator and the box's own files directory, or the positions it recorded for this stop; otherwise none, and the deadline makes the operation stuck; the mutation journals the remote position with Flushed false (TestReleaseRefusedAfterACrashBeforeTheFlush, TestReleaseReplaysTheRecordedFlush) |
| 204 | "reloc-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase) |
| 205 | "reloc-name-before-pin", // rev 7 (Astra round 4 finding 1; 1b-next rev 19 Worker.pinning): a relocation at pinning with no target names one before it selects a pin, on every path; the mutation pins first, and a manifest that lands while no box is eligible is left out (a loss bound: TestConvertedMoveWaitsForATargetBeforeItsPin) |
| 206 | "reloc-failover-start-guard", // rev 7 (Astra round 4 finding 3; 1b-next rev 19 Worker.Start, StartRelocation): a serving executor's failover starts only with an eligible target, the app admitting the registration (and its recheck) and RelocationStartGuard with the source fenced; the mutation starts at once (TestFailoverStartWaitsForAdmission, TestFailoverStartWaitsForParkReplica) |
| 207 | "reloc-failover-ack-before-pin", // rev 5 and 6 (Astra rounds 2 and 3; 1b-next rev 19 PinFailover): an initial failover (op.PinFailover, the model's starting) selects its pin only after the target is named and every participant acknowledged; converted moves, nested failovers and replays pin first, as Worker.pinning does; the mutation pins first, and a manifest that lands while the target's controller is unavailable is left out (a loss bound: TestFailoverPinWaitsForTheAcknowledgement) |
| 208 | "reloc-name-drops-move-target", // final review Important 1 (1b-next 151261fe, NameTarget; moves §7.10, region HA §5.8): naming a converted move's same-region target takes the move's own target (move_target_box, in the other region) off the participants in the same CAS; the mutation keeps it on the barrier, and a stopped move target holds the relocation at pinning for ever (liveness, expected miss; TestConvertedMoveDropsTheMoveTargetFromTheBarrier) |
| 209 | "park-evidence-every-box", // final review Important 2 (cf566b41; hostops RetirementEvidence.VerifyObligation, collectEvidence over the inventory; claim §6.2a): in a two-box region a park-replica or park-superseded run by a box that is not the executor waits for every live box of the region not on lost to publish its stop evidence for the operation; the mutation parks on the owner's evidence alone, and the sibling writer's replicator ships into the parked region (INV-10, seed 819; witness) |
| 210 | // Astra's joint round 1 on the two-box model |
| 211 | "files-live-region", // joint round 1 finding 1, claim §6.2a (the live set is {authoritative region, location, generation}; region HA §5.6, L13): the files live set is region-qualified: holder.generation's manifests, the pin's, P's, the chain's newest and the objects they or a box's files directory name are live only in the files home (filesHome: the authoritative region, and while a relocation runs its source region holds the whole files live set), and the newest manifest is read only in the key's own region; the mutation reads every region, so a manifest PUT landing in the former region after a move's cleanup protects itself and the object it names, and the sweep never retires them (INV-10; witness) |
| 212 | "files-home-move-phases", // joint round 1 review I1, claim §6.2a and moves §5.1's authoritative-region table: the files home also holds the source region while moving (op.exec none from stopped on), while landing until the move commits (op.Committed: admission does not rule out a clean rollback, joint round 2), and while restoring until the source's return CAS (releasing and released; after a dirty return the newest admission decides until the source's probe is admitted, so the return's install park retires the pre-move generations, moves' D6, a5e8c13f: TestDirtyReturnParksPreMoveFiles); the mutation keeps op.exec's region and a relocation's source only, so a park-generation queued during the move archives the live manifest in stopped, or after the target's admission before a clean rollback, and the source-region failover pins no keyed manifest (INV-30, INV-3 with INV-30 off; wMoveStoppedKeepsLiveFiles, wRollbackKeepsSourceFiles) |
| 213 | // L18 joint round findings 2 to 4 (regionha_completion_test.go; 1b-next 596fa8b1 and a092ddc2) |
| 214 | "reloc-probe-stop", // finding 2, ruling 49 (Participant's EndProbe, RecordProbeStop, CompleteRelocation's probeStopped): the passed probe's session is stopped with root's receipt and the stop journaled before the serving CAS, bounded by ruling 67; the mutation completes over the running probe, which strands its session across the kind change (INV-31; wProbeStopBeforeServing) |
| 215 | "reloc-probe-fence-owner", // finding 2, ruling 75 (relocationStopProbe's FenceAndStopAs, relocationReleaseHold's LiftFenceAs): the probe stop installs its owned activator fence only on an unfenced host or meets its own, and refuses any other owner's with nothing stopped; the lift lifts only its own; the mutation installs over, and lifts, any fence (INV-32; wProbeStopMeetsAnotherFence, wLiftAfterRestartMeetsAnotherFence) |
| 216 | "reloc-completion-discharge-first", // finding 2, ruling 66 (relocationReleaseHold, DischargeCompleted): C10's discharge succeeds, while the row is still held for the op and the holder is still the stopped probe session, before the hold is released or the fence lifted, and reconcile never releases that hold as stale; the mutation releases and lifts first, and a serving wake moves the holder off the undischarged session (INV-31; wDischargeFailsHoldsTheRow) |
| 217 | "reloc-completion-mark-last", // finding 2, ruling 80 (relocationReleaseHold, MarkCompletedDischarged): the mark is written last, after the discharge, the hold's release and the lift; the mutation marks first, so a discharge that then fails is never retried and the barrier lets a successor name the undischarged box (INV-31; wMarkLastAfterAFailedDischarge) |
| 218 | "reloc-completion-from-claim", // finding 2, ruling 80 (RelocationRuntime.once, finishCompletion): the pass finds every unmarked completion on this box from the claim record, never from the row, so a mark that failed after the hold's release is retried; the mutation finds it from the row's hold, and the completion is never marked, so nothing ever starts from the host again (INV-3; wFailedMarkRetriedFromTheClaim) |
| 219 | "reloc-completion-barrier", // finding 2, ruling 77 (completionBarrier in StartGuard and RelocationStartGuard): no move, delete, purge, push or relocation starts from serving while the completion is unmarked, unless the completion box is on lost or is a failover's cited fenced source; the mutation starts a drain and a move over the undischarged box (INV-31; wSuccessorWaitsForTheDischarge) |
| 220 | "reloc-completion-claim-mode", // finding 2, ruling 82 (newCompletionRuntime): the completion pass runs whenever claim mode is on, region HA on or off; the mutation runs it with region HA on only, and a completion pending when region HA is turned off never finishes (INV-3; wCompletionWithRegionHAOff) |
| 221 | "reloc-completed-handover", // finding 2, N6 (wireCompletedHandover, relocationCompletedHandover): the first serving wake after a completion hands over from the probe's receipt and stops nothing; the mutation routes it to main's stop, whose serving-shaped fence replaces the probe's, and the handover refuses for good (INV-3; wServingWakeHandsOver) |
| 222 | "reloc-completed-catchup-hold", // finding 3, ruling 85 (hostbox completedHold, 1b-next a092ddc2): a source whose reconcile runs only after the target completed holds its row for the completed op until its park-local retires it; the mutation leaves the row its release left ready (INV-33; wDelayedSourceHoldsItsRow) |
| 223 | "reloc-completion-fenced-exempt", // ruling 86 (1b-next ca282378: StartGuard's fencedCompletion, ProductionAuthority.completionFence): a delete or purge whose caller verified the completion box's termination fence passes the barrier, as a failover with its fenced source does; the mutation verifies nothing, and a completion box terminated before its discharge while a purge holds admission closed blocks both the purge and the failover for ever (INV-3; wPurgeOverAFencedCompletionBox) |
| 224 | "reloc-probe-stop-flush", // ruling 87 (1b-next 6a4eadde, EndProbe through flushStopped): the probe stop stops the writers, flushes the database and files and records the positions before the activator's fence and root's stop, and with another owner's fence it refuses after the flush; a restart before the record has no replicator, so it refuses until ruling 67's deadline; the mutation stops with nothing flushed, and the first serving wake declares writes the probe session acknowledged (INV-34; wProbeStopFlushes) |
| 225 | "dirty-return-needs-admission", // Astra joint round 4 item 2 (moves movesinstall.go's targetAdmitted, movessources.go's restoring case): a dirty return ends the source region's files protection, and its install parks the pre-move generations, only when the claim records an admission of this move's generation by the target; src_covered false makes a return dirty without one, and then the pre-move generation stays the source's live state and nothing is parked; the mutation drops the admission check, and the install park retires the manifest the source's next install would pin (INV-30; wDirtyReturnWithoutAdmission) |
| 226 | "reloc-admits-probe-only", // L18 joint round 2 finding 3 (hostclaim relocatingAdmission): a relocating claim admits only op.exec's cold probe in probing, so between StopWriters' launch-journal closure and Collect's admission fence no wake of the source admits a writer; the mutation admits the source's wake in starting and releasing, as the model did before (TestNoAdmissionBetweenStopAndFence) |
| 227 | "reloc-c1-failed-release-refused", // finding 4, claim ask C1 open (QueueRelocationRelease requires the source in releasing): a live failed target cannot release in probe-failed and reaches stuck at the release deadline, and the operator's resolve stops it; the mutation releases as if C1 had landed (a fidelity guard: TestFailedTargetCannotReleaseWithoutC1) |
| 228 | "reloc-c11-later-attempt-refused", // finding 4, claim ask C11 open (Preflight's ErrLaterAttemptUnlaunchable, ruling 58): after P's opening a later cold probe attempt is refused before it is counted, which is probe-failed; the mutation counts and makes it as if C11 had landed (a fidelity guard: TestLaterAttemptRefusedWithoutC11) |
| 229 | } |
| 230 | |
amadan