TLA+ verification redesign: proof obligations, exact reductions, honest scheduled gates - #5
Open
zsumz wants to merge 19 commits into
Open
TLA+ verification redesign: proof obligations, exact reductions, honest scheduled gates#5zsumz wants to merge 19 commits into
zsumz wants to merge 19 commits into
Conversation
Two scheduled lanes run multi-gigabyte TLC continuations against checkpoints cached under one repository cache allowance, and nothing kept them apart. Nightly ran daily at 09:00 UTC; weekly runs Saturday at 07:00 UTC and its TLA+ leg is still going at 09:00. They sit in separate concurrency groups, so on Saturday both restored, saved, and pruned multi-gigabyte checkpoint generations concurrently against the same allowance, each evicting the generation the other had just seeded. Nightly now runs Sunday through Friday. The second failure is local disk. TLC writes its successor checkpoint beside the recovered one before retiring it, so peak disk is the restored bytes plus a full successor plus that successor's growth. Standard runners have roughly 14 GB free; the nightly checkpoint is already 8.14 GB. A continuation started under that shortfall does not merely fail, it breaks the lineage: no new generation is saved and the successor the pruning step expects never exists. scripts/tla-checkpoint-disk-gate measures the restored bytes and free bytes after restore and fails in seconds unless free >= restored * 1.5 + 4 GiB. Against today's numbers the gate refuses the run, which is the correct answer: 8.14 GB restored needs 15.37 GiB free and the runner has about 13. Gate semantics are untouched. An incomplete nightly continuation stays red. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A scheduled continuation that ends incomplete says nothing about whether continuing it converges. The lane reports pass or fail; it does not say whether the frontier was draining or still growing, and that is the only number that decides whether this lineage is worth another six hours. scripts/tla-continuation-telemetry samples the run every five minutes into a JSONL artifact: TLC's progress counters read from the live stdout capture the runner already keeps under target/rafter-invariants/telemetry, the queue slope between samples, frontier fanout (new distinct states per retired state), checkpoint bytes, free disk, and the TLC process RSS and CPU. On finish it classifies the trajectory as exhausted, violated, incomplete-expanding, incomplete-shrinking, or incomplete-flat, and writes that to the step summary. Fanout is the diagnostic that matters. The nightly lineage currently sits near 2.85 new states per retired state, which names it incomplete-expanding: the checkpoint is growing because exploration is diverging, not because it is close to finishing. This is a side channel by construction. It runs outside the producer, writes under RUNNER_TEMP so it cannot reach the source-bound evidence tree, and adds no receipt field, schema, or producer version -- a producer bump would cascade into contract migrations and the verifier. The terminology is additive and `summarize` always exits 0: pass/fail stays with the invariant producer, and an incomplete nightly continuation stays red. GC statistics are deliberately omitted; jstat would need a JDK attach against a process this script does not own. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…nfigs Split the monolithic proof surface into named obligations. CoreNext, MembershipNext, SnapshotNext, and ReadNext are strict disjunct-subsets of ProtocolNext composed from the existing action operators under unmodified guards, so every behavior of a focused spec is a behavior of Spec. SnapshotNext is the one subset of Next rather than ProtocolNext, because CompactSnapshot is reachable only through Next's compaction-first branch, which it reproduces. JointQuorumInit is a focused initial state for the joint-quorum obligation: the exact post-state of Timeout(L), three vote round trips, and BecomeLeader(L) from Init. Every witness and monitor variable is derived from the action that last writes it along that prefix rather than guessed, so the state is reachable under Spec and TLC reports no invariant violation on it. Naming a leader makes ModelPermutations unsound, so JointQuorumPermutations supplies the reduced set that fixes the leader. Two manual-run configs carry RaftJointQuorum.cfg's constants and all nine invariants, changing only the transition relation and initial state, plus the script flags that run them. Neither is wired to a profile; the profile contract in crates/rafter-invariants is untouched. Raft.tla is additive only. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Restricting Next did not make the four-voter joint-quorum model exhaust. The focused relations are cheaper per state -- MembershipSpec passed the full model's 45-minute counts in about 14 minutes -- but the frontier grew monotonically for the whole of both runs, and the extra throughput bought depth 24 against the full model's 20 rather than closure. The focused initial state did not change that and costs a symmetry quotient to have, since ModelPermutations was already collapsing the elections it skips. Records both trajectories, states plainly that the answer is negative, and notes that the focused-init run was truncated by a full host filesystem rather than by a budget. Also records what the relations are good for: CoreSpec and ReadSpec both exhaust at two voters in seconds, so the obligations are usable wherever the bounds are already tractable. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
One config per focused relation, each carrying the theorem it states, what it deliberately excludes, and why each constant narrowing is sound for that theorem. All four check the nine invariants with CHECK_DEADLOCK FALSE and SYMMETRY ModelPermutations. Two are calibrated and exhaust, measured with the pinned tla2tools 2026.08.11.125311 at -workers 4: RaftCoreObligation.cfg 20,282 distinct, depth 27, 6s RaftReadObligation.cfg 98,948 distinct, depth 31, 26s Those counts are the ratchet floors for a CI gate that passes only on states_left = 0. Both sit at two voters because three does not work. CoreSpec at the nightly bounds reached 4,210,497 distinct with 2,699,386 queued and depth stalled at 19, and at MaxTerm 2 / MaxLogLen 2 it reached 5,443,386 distinct with 2,557,643 queued at depth 21; both queues grew monotonically throughout. The node count binds, not the term or log bound, so no reduced-bound three-voter variant recovers it. ReadNext contains every CoreNext disjunct, so it cannot exhaust anywhere CoreSpec does not. The membership and snapshot configs were never run -- the host filesystem fell below its safety floor first -- and say so in their headers. Their bounds are reasoned, not measured, and both carry a DO NOT WIRE note until a run reports states_left = 0. Membership is the harder question: two voters is tractable but nearly vacuous for quorum intersection, and four voters is already known to diverge. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The TLA+ layer could only ever state one theorem per profile: one config, checked until it drained or ran out of budget. Anything a profile's bounds could not reach had no way to be stated at all, so the narrower transition relations the specification now defines stayed manual-run artifacts with nothing in the contract holding them. The runner contract becomes one primary configuration plus a list of focused proof obligations. Each obligation pins its own config, seed, whole-minute budget, and calibrated state floors, and passes only by draining its queue with no invariant violated and both floors cleared. Three rules make that mean something. Obligations run before the primary configuration, after harness qualification. A broken theorem is red in minutes instead of after a five-hour continuation, and the primary run inherits what is left of the shared execution window -- which is the budget it was always supposed to have. The contract refuses an obligation set whose budgets plus the primary soft_timeout exceed total_timeout less finalization_reserve, so the ordering cannot silently truncate the monolith at runtime. Obligations never checkpoint. Each runs from scratch into an ephemeral state directory, recovers nothing, and participates in no cache key. An obligation that cannot exhaust in one bounded run is not an obligation but a second monolith, and belongs in the primary continuation instead. Keeping the list outside the serialized configuration map is what enforces this: the checkpoint contract digests only that map, so adding, retuning, or removing an obligation cannot invalidate accumulated primary TLC state. Every obligation binds the same nine invariants as the primary config and is held to the same safety-only boundary, so a config that checks nothing cannot discharge by exiting cleanly. The negative detector stays bound once per layer, to the primary config; obligations strengthen the layer and add no registry evidence rows, so a refutation inside one is reported red as a harness-level failure for a human to read rather than attached to a predicate the primary run never falsified. The verifier reconstructs each obligation independently: its exact TLC argv from the pinned contract rather than the observed argv, and its terminal frames from its own authenticated log. Producer and verifier share only serialized vocabulary. Receipts gain a per-obligation observation frame and exactly two artifacts per obligation, and the log prefix that fail-fast ordering produces is checked rather than assumed -- a gap, an out-of-order log, or a main log after an undischarged obligation is rejected. The same migration re-pins TLC, because it must. Upstream v1.8.0 is a rolling nightly channel, not a release: the pinned asset 481553986 was deleted and now 404s, and three distinct jar digests appeared in five weeks. The new pin is asset 510140106, sha256 ab323b79..., reporting TLC 2026.08.11.125311. The asset ID is only a liveness pin; the sha256 is the identity, and a new guard asserts the checked-in manifest and all three profile pins agree. Because the tool pin lives in the configuration map the checkpoint contract digests, this resets the TLC checkpoint lineage once for every profile (pr 84f4980f->15e3d0ca, nightly 4ca7833d->d1528483, weekly 8d09c275->a14088ec). Obligations sit outside that map, so future obligation edits do not repeat it. TLC -coverage was evaluated for this same migration and rejected on measured evidence: on this repository's own trace-sample model one coverage report costs about 790 KB of framed stdout (3,849 bytes without, 793,379 with), so -coverage 5 over the PR tier's 325-minute budget would add roughly 50 MB against the producer's 64 MiB per-process stdout cap, all of it inside the hashed, uploaded, and re-parsed tla-log artifact. No profile declares an obligation yet. All three arrays are empty, and empty is exactly the identity: receipts, artifact sets, and observation frames stay byte-identical to the v15 contract apart from the version and tool fields, so the deterministic PR gate still emits 44 green verdicts. Adding a measured obligation is a profiles-manifest edit. Profile schema 9 -> 10 and producer rafter-invariants-tla-v15 -> v16 land together with negative fixtures rejecting every retired identity. They cannot be split: the schema version, producer id, tool pin, and obligation vocabulary validate against each other, so any intermediate commit fails its own contract tests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Snapshot creation set a `compactionPending[n]` flag, `Next` carried a compaction-first branch that disabled every protocol action while any flag was set, and `CompactSnapshot(n)` cleared the flag and wrote nothing else. The intermediate state that sequence produced was unobservable. No protocol action was enabled in it, the only action that was agreed with its own successor on every variable except the flag, and no predicate outside the flag's own type constraint read the flag. It was one extra distinct state per snapshot creation, plus the branching over which pending node compacts, and no property could tell it apart from the state that followed it. The two actions become one, and `compactionPending` goes away entirely -- declarations, `vars`, `snapshotVars`, `TypeOK`, `Init`, every UNCHANGED clause, and `SnapshotIdentitySoundFor`'s fourth parameter. The folded spec is stuttering-equivalent to the old one for every property over the remaining variables: drop the flag from any old behavior and the intermediate state becomes a stuttering step, which `[][Next]_vars` already admits. Two names collapse with it. `Next` had a compaction-first branch and `ProtocolNext` was the disjunction without it; with the branch gone they were the same relation, so `ProtocolNext` is retired and `Next` is the disjunction. `SnapshotNext` needed an IF wrapper because `CompactSnapshot` was reachable only through the branch -- it is now a plain disjunct-subset of `Next` like its three siblings. Measured on exhaustive runs, old vs new distinct states: two-voter full `Spec` at MaxTerm=1/MaxLogLen=1, 35,363 -> 24,995; `SnapshotSpec` at MaxLogLen=2, 305,787 -> 210,043; at MaxLogLen=1, 3,963 -> 2,811. `CoreSpec`, `ReadSpec` and `MembershipSpec` exclude the snapshot lifecycle and are unchanged to the state: 387/124, 1,405/336 and 7,215/1,708 generated/distinct before and after. That identity is the evidence the fold touched only what it claims. The detector's own snapshot lifecycle fixture goes 7 distinct states and depth 7 to 6 and 6 -- exactly the one intermediate state, which is the claim stated as a number. The mutation suite keeps all 34 tests, but one had to be rewritten rather than retuned. `snapshot_compaction_pending_tracks_create_and_compact_transitions` patched `compactionPending' = [... EXCEPT ![n] = TRUE]` to FALSE and the converse in `CompactSnapshot`; neither string exists now, and the second has no folded equivalent at all, because atomicity leaves no obligation for a completing action to discharge. It is renamed `snapshot_creation_atomically_advances_and_retains_the_snapshot_floor` and asserts the folded action's two effects instead: a mutation that stops the snapshot floor advancing stalls the lifecycle and is caught by the same liveness property as before, and a mutation that compacts the ghost log physically instead of retaining it breaks `snapshotIndex[n] <= Len(log[n])` and is caught as an invariant violation. The suite count is unchanged and the inventory arrays stay sorted. The membership trace sample executed `CompactSnapshot` as step 38, so that step is removed and 39..44 renumbered down; the trace is one step shorter and still executes every transition in REQUIRED_MODEL_TRANSITIONS, which drops from 19 to 18. The trace floors move 46 -> 45 with it, and the reviewed-source digests for the trace module and the detector replay inventory are re-pinned because the specs they authenticate changed on purpose. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`snapshotPrefix[n]` was a variable holding a copy of the log up to the snapshot floor, maintained in parallel with `log` and `snapshotIndex`, and `SnapshotIdentitySoundFor` asserted it equal to `Prefix(log[n], snapshotIndex[n])` on every state `LogMatching` was checked on. It becomes `SnapshotPrefix(n) == Prefix(log[n], snapshotIndex[n])`, and the variable goes away: declarations, `vars`, `snapshotVars`, `TypeOK`, `Init`, `JointQuorumInit`, every UNCHANGED clause, and the `snapshotPrefixes` parameter of the eight operators that took a snapshot view alongside a log. Soundness needs one step beyond "the invariant held". Two recorders are called with a primed log against an unprimed snapshot floor -- `RecordLogicalPrefixes(log', snapshotIndex, ...)` in `ClientAppend` and `DeliverAppend` -- where the derived form reads the successor log while the stored form still held the predecessor's prefix. They agree because no action rewrites a log at or below its own snapshot floor. `ClientAppend`, `EnterJoint` and `LeaveJoint` only append. `DeliverAppend` replaces the receiver's log wholesale, but only under `CanAdoptLog`, which pins every index up to `commitIndex[n]`, and `snapshotIndex[n] <= commitIndex[n]` holds throughout because `CreateSnapshot` snapshots at `AppliedThrough(n)` and `InstallSnapshot` raises `commitIndex` to the transfer index in the same step. That bound is now a `TypeOK` conjunct, so the argument is machine-checked rather than asserted in a comment. One read site is a frozen payload and stays stored. `snapshotTransfer.prefix` is captured at send time and the sender's log may move before the receiver installs, so it is a value and not a view; only the expression that computes it in `TransferSnapshot` changes, from a variable read to `SnapshotPrefix(from)`. Every other read site was a live view and now goes through the derived operator. This does not reduce the state count and is not claimed to. The removed variable was a function of two others, so no two reachable states differed in it alone: `CoreSpec`, `ReadSpec` and `MembershipSpec` are unchanged to the state at two and three voters, up to 1,213,423 generated, and so are the snapshot models -- `SnapshotSpec` at `MaxLogLen=2` reports the same 1,312,094/210,043 before and after. Peak RSS is unchanged within noise (2.90-2.97 GiB over four runs at `-Xmx8g`, with the two variants' wall times interleaving, so the apparent wall-time difference was host contention). What it buys is an obligation retired rather than a cost avoided. Three of `SnapshotIdentitySoundFor`'s four conjuncts said the stored copy really was the log's prefix at the floor; they are definitional now, and the one that remains is the bound that makes the definition well formed. The way to violate them -- writing the wrong prefix -- no longer exists. The header's correspondence notes gain the two differences this makes explicit: the model stores no snapshot and models no physical compaction, and creation and compaction are one atomic action where the implementation has two moments. All 34 mutation tests still pass. Six of them name the changed operator signatures as textual patch targets or delimiters and were updated to the new arities; none changed what it mutates or what it asserts. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The reductions changed measured state counts that this document reports as fact, and left two paragraphs describing machinery that no longer exists. Adds an "Exact state-space reductions" section stating each reduction, its soundness argument, and an old/new comparison over eight exhaustive models. The arguments are the load-bearing part: the fold is sound because the intermediate state was unobservable and the folded spec is stuttering-equivalent over the remaining variables; the derivation is sound because the equality it replaces was already checked on every reachable state, plus the one step that needs more than that -- a recorder called with a primed log against an unprimed snapshot floor, which agrees because `CanAdoptLog` pins the committed prefix and `snapshotIndex[n] <= commitIndex[n]`. The comparison table reports the derivation as changing no state count, because it does not. Four snapshot-free relations are identical to the state across both reductions, up to 1.2 million generated states, and that identity is the evidence the reductions touched only snapshot machinery. Peak RSS was flat within noise too, so the section says what the derivation actually buys -- an obligation retired -- rather than a cost saved. Existing measurement rows are annotated rather than rewritten: they were true of the spec they were taken on. The two-voter row is marked as no longer reproducing, with the current figure alongside it. The unexhausted three- and four-voter rows are left alone, since a reduction does not turn a reading of a still-growing frontier into a different fact. Also drops `CompactSnapshot` from the `SnapshotNext` action-family row and replaces the paragraph explaining why `SnapshotNext` needed a compaction-first wrapper, since it no longer does. The `raft_trace_vars_name_every_raft_tla_state_variable` guard asserted the parsed `vars` tuple had more than 20 members, which was a sanity check on the parse that happened to sit one below the old count of 22. At 20 it started failing for the wrong reason. It now guards the parse and says so; the exact equality against `Raft.tla`'s own tuple, which is the real check, is unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The obligations vocabulary landed empty; this fills it with the two theorem families measurement says can pass a states_left = 0 gate, at floors set to their exact measured counts. The pr profile gates on core-replication (RaftCoreObligation.cfg, 113,201 generated / 20,282 distinct, 15s) and read-fencing (RaftReadObligation.cfg, 592,279 / 98,948, 30s), fitting the 11-minute obligation headroom its 325-minute primary leaves. Nightly and weekly gate on read-fencing plus core-replication-deep (RaftCoreObligationDeep.cfg, new: the same core theorem at the full three-term, three-slot, two-value nightly bounds -- 14,734,799 / 2,004,053, 8.5 minutes measured), inside their 45-minute headroom. Floors are exact because TLC's breadth-first counts are deterministic for a fixed spec, config, and symmetry: a deviation is a spec change and should be recalibrated deliberately, not absorbed by slack. The two-voter core and read counts were re-measured on this tree, after the snapshot reductions, and match the pre-reduction calibration to the state; the deep floor was measured pre-reduction, and CoreSpec contains no snapshot action -- the reductions' identity was verified exactly at four other core/read bound-sets. Membership and snapshot stay unwired, now with measured reasons instead of missing ones: MembershipSpec at three voters diverges (9,935,434 distinct, 3,959,098 queued and growing at a 30-minute kill), and SnapshotSpec explodes a two-voter model at MaxLogLen 3 (13,356,326 distinct, 4,992,419 queued, growing). Their headers carry the numbers, the DO NOT WIRE markers, and the one unmeasured bound reduction each has left. The pattern across every divergent run is a single wall: the set-valued messages variable at three voters, or the snapshot lifecycle at two. Exhausting those obligations is a message-dimension redesign, not a bounds hunt, and docs/model-checking.md now says so next to the wired manifest. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Wiring real proof obligations left thirteen tests behind, because the synthetic evidence builders described the TLA+ receipt shape as a frozen list instead of reading it off the contract. Every one of those failures was the verifier correctly refusing evidence that no longer matched the profile it claimed to come from. The shared builders in tests.rs now derive the TLA+ shape from whatever obligations the manifest declares: two artifacts per obligation, and the four observations the receipt defines, taken from the same production helper the producer and verifier use rather than restated. The synthetic terminal frame is an obligation that drains its queue and clears its own calibrated ratchets exactly -- the weakest run the contract accepts, so a floor regression cannot hide behind a generous fixture. The TLA+ bundle fixture follows: it copies each obligation's configuration into the fixture checkout so the bound-source comparison has real bytes to compare, writes a discharged log per obligation, reconstructs the obligation argv from the pinned contract (its own config, its own seed, the profile's inherited worker and memory profile), and rebases obligation logs along with every other TLC process log when the producer root moves. No verifier acceptance was weakened and no production path learned about test mode. The round-trip test that asserted the live manifest declares no obligations now builds a synthetic obligation-free document instead. What it tests is what the *absence* of the key means, and that property stopped being observable on the live manifest the moment obligations were wired; asserting it against real data would only have re-broken on the next edit. Teaching the fixtures to model the contract then caught a real defect the empty-array contract could never expose: intake's reviewed artifact-kind policy admits the detector log and config prefixes but was never taught the obligation ones, so it classified every obligation artifact as an unreviewed kind. A receipt carrying a real obligation would have been rejected at preflight, before verification ever ran. Both prefixes are now reviewed with semantic bytes retained -- they are text the verifier reads back and re-parses -- and the policy test pins them so the gap cannot reopen. The detector-replay inventory failure was unrelated to obligations and is worth naming separately. Commit dc2ee99 edited crates/rafter-sim/src/model_check/tests/tla.rs, which is inside the replay source graph, without re-pinning the reviewed inventory digest. Restoring that file to its pinned-era content reproduces the old digest exactly, which identifies the drift precisely; the pin is therefore refreshed to the inventory the tree actually computes, in both the constant and all three verifier contracts. The fixture set is unchanged at 77 fixtures, 79 evidence bindings, and 2 targets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The pre-fold spec diverged at two voters and MaxLogLen 3: 13,356,326 distinct states with 4,992,419 still queued and growing at a 30-minute kill. On the folded spec at MaxLogLen 2 the same relation drains -- 14,119,884 generated, 2,002,205 distinct, 0 left on queue, under seven minutes -- so the snapshot lifecycle joins the wired manifest for nightly and weekly at exactly those floors, inside the 45-minute obligation headroom (25m + 6m + 12m). Atomic create-and-compact, transfer, install, restart, and application-state loss are now an exhaustive gating theorem, which is the fold's payoff stated as a verdict rather than a percentage. Membership closes the other way. The last candidate bound, three voters at MaxTerm 2 / MaxLogLen 2 on the folded spec, diverges like every bound before it: 46,023,230 generated, 7,526,805 distinct, 2,416,633 queued and growing. Its header now records the complete measurement history and the conclusion: no exhaustible non-vacuous bound exists under the current message model, and the honest fix is a message-dimension redesign, not a smaller config. Fixtures needed no change for the third obligation -- they synthesize evidence from whatever the manifest declares, which was the point. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Upstream tlaplus/tlaplus publishes v1.8.0 as a rolling nightly channel: the tag stays fixed while its assets are rebuilt under fresh IDs and the predecessors deleted. Two successively pinned upstream asset IDs went stale in five weeks, which makes an upstream asset ID a liveness pin that keeps breaking, not an identity pin. The exact reviewed bytes (sha256 ab323b79..., TLC 2026.08.11.125311) now live at zsumz/tla-tools release tla2tools-2026.08.11.125311, asset 510788686, whose contract is that published assets are never replaced or deleted. The fetch URL, ASSET_ID, VERSION, the profile tool_asset_id pins, and the pinned contract constant all move to the mirror; the sha256 is unchanged because the bytes are unchanged, and it remains the only trust anchor -- the mirror solves liveness, the digest solves identity. Fetch verified end-to-end from a cleared cache. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Nightly and weekly TLA+ could not go green as gated. The primary monolith passes only on states_left = 0, and the measured frontier grows at a fanout near 2.85 with no inflection: it will not drain. Gating on an event that cannot occur produced a permanently red lane that said nothing about the protocol, while the evidence those lanes do produce -- proof obligations that exhaust sound sub-relations, plus accumulated monolith coverage -- went unreported. The primary continuation's meaning becomes contract state. A new `primary_completion` key in the tla configuration map pins `gating-frontier-exhausted` for pr and `reporting-continuation` for nightly and weekly, value-checked per profile alongside every other pinned key. It lives in the map rather than beside it so the checkpoint contract and the verifier's argv reconstruction read one source of truth. PR is unchanged in every respect. RaftCi.cfg genuinely drains, so its continuation still gates on exhaustion at its calibrated floors, and the verifier refuses outright any PR receipt claiming a reporting continuation -- the one lane that blocks a merge cannot relax itself from inside a receipt. Reporting relaxes the budget and nothing else. The continuation still runs its full budget, still checkpoints, still recovers, still emits every artifact, and is still verified end to end as source-bound evidence. A counterexample it finds still fails the layer red. So does a malformed, missing, or unreadable artifact set, an incompatible checkpoint, a failed qualification probe, and an undischarged obligation. Exactly one outcome stops being red: budget elapsed with a readable progress frame and an open frontier. The pinned 120M/16M minimums stay in the contract for the scheduled profiles as the accumulation bar the lineage reports progress against, published beside the observed counters instead of enforced as a terminal condition. They are now pinned per profile rather than shared, so the PR floors are two adjacent named constants and a RaftCi recalibration is that edit and nothing else. Receipts state both halves of the truth. Every TLA+ check carries a `tla_continuation` binding naming its pinned policy and the continuation's actual ending -- frontier-exhausted, counterexample, or budget-elapsed-frontier-open -- so a green scheduled receipt cannot be read as a completed monolith. The verifier rederives the outcome from the same log it already parsed and rejects a binding that disagrees, and rejects a declared policy the profile does not pin. Under a reporting policy the `checked:` observations are sourced from the obligations rather than the monolith: they bind the same nine invariants and they did drain. That claim always has a source because the contract now refuses a reporting profile that declares no obligations -- a profile may only demote its primary when something else still exhausts. This folds into v16, which has never run anywhere, rather than minting a v17. The recorded runner_contract_sha256 table moves with the configuration maps: pr 84f4980f->a9c75c28, nightly 4ca7833d->931838e2, weekly 8d09c275->724e90e9. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…udit Two measurement campaigns close the calibration ledger this branch opened. The post-reduction RaftCi.cfg exhaustion completed: 255,177,640 states generated, 36,058,645 distinct, queue drained, 93 minutes at -workers 4 on a 14-core host. Those exact counts replace the round 120M/16M floors in the pinned contract, matching the obligation-floor philosophy -- counts are deterministic for a fixed spec, config, and symmetry, so the floor is the measurement, and a deviation is a spec change asking for deliberate recalibration. The synthetic fixtures now read the floors from the pinned contract instead of hardcoding cleared values, so the weakest accepted run is what they model and a future recalibration is a contract edit alone. Weekly gains its unsymmetrized obligation family: core, read, snapshot, and an all-feature integration model, each measured to exhaustion without a symmetry quotient and wired at exact floors. The budget comes from the reporting continuation -- weekly's primary drops from 265 to 200 minutes, and the recovered hour funds the symmetry audit applied to every theorem that gates. The audit is a pair of numbers per config, not a round ratio: each unsymmetrized count falls short of group-order-times-quotient by exactly the symmetric states' missing orbit mass (151, 219, 5, and 715 states), which the config headers and docs now state precisely. The joint-quorum section's tier-registration objection is retired: the obligations vocabulary is exactly the mechanism that section said could not exist. What survives is the measured objection -- it does not exhaust -- and that one is sufficient. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
First CI contact for the branch failed in five places. Four were one defect wearing four faces, and the fifth was drift between two gates that are deliberately duplicated. Artifact kinds are receipt vocabulary and several are structured with a colon. The detector pair has always kept that colon out of the filesystem: detector configs and logs are written to explicitly named paths, so the kind stays a receipt identity and never becomes a filename. Obligation configs went through the content-addressed capture path instead, which derives the filename from the kind, and `actions/upload-artifact` rejects a colon outright for Windows portability -- discarding a completed layer's entire evidence tree after the work was already paid for. The kind is unchanged; the mapping from kind to filename now normalizes `:` to `-`, which is the normalization the source-identity policy already applied when recognizing those same files. A guard walks every artifact kind the producers can emit, drawn from the live registries rather than a copied list, and asserts each maps to an uploadable, non-colliding filename. The same omission had three more faces that only the serialized end-to-end fixture could reach, each in a policy that is intentionally owned twice so producer and verifier cannot weaken each other in one edit. The producer's source-identity policy and the verifier's generated-output allowlist both had to learn obligation evidence names, and each derives the rule itself. The verifier's resource-metric classifier had to learn that obligation logs are TLC processes: the producer folds their duration and peak RSS into the check totals, so every receipt that ran an obligation would have disagreed with its own hashed process logs. That one would have failed the PR gate the moment the upload was fixed. The weekly producer refused its own profile at runtime -- "checkpointed weekly TLA runner requires soft_timeout=265m" -- because the weekly budget moved to 200m in the contract layer while the producer's independent allow-list kept the old literal. That duplication is the design and stays; what was missing was a test that runs the reviewed manifest through the producer's gate, so the two copies can only drift where a test says so. Every earlier test here fed the allow-list a hand-built map, which is exactly why this reached CI. Nightly's `snapshot-lifecycle` obligation did not exhaust in its 12m budget on a hosted runner. It was close: 12,544,244 of 14,119,884 generated states with a queue that was draining (139,953 -> 91,724 states left) and roughly eighty seconds of work remaining. The other two obligations landed on their calibrated counts exactly -- core-replication-deep in 16m26s of 25m, read-fencing in 33s of 6m -- so the calibration is sound and only this budget was set too close to its own cost. It moves to 25m on both scheduled profiles, paid for by nightly's primary continuation dropping 265m to 250m. That is the trade the reporting policy exists to make: the continuation accumulates, the obligations gate, so budget belongs to whichever one decides the verdict. Weekly already had the room. A second guard asserts every profile's obligations plus its primary fit inside its execution window. Three public enums are documented as deliberately exhaustive. They are deny-unknown wire vocabularies where an unreviewed value must fail decoding, so `#[non_exhaustive]` would state the opposite of what they mean. Also pays the deferred rustfmt drift across the crate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…l time The first nightly dispatch measured CI runners at almost exactly twice the local calibration wall on the multi-minute models: the deep core obligation ran 16m26s against 8.5 local minutes and the snapshot obligation 13m24s against 6.7 -- killed eighty seconds short of a drained queue by a 12-minute budget set from the local number. Weekly's unsymmetrized snapshot obligation carried the same mistake at larger scale: 17 local minutes projected to ~34 on CI against a 25-minute budget. Every multi-minute obligation budget now carries roughly twice its CI projection: unsymmetrized snapshot moves to 40 minutes, funded by the weekly reporting primary dropping from 200 to 190 -- budget belongs to what decides the verdict. Weekly now runs 110 obligation minutes inside its 120-minute window; the guards that pin the reviewed manifest against the producer allow-list and the weekly workflow assertions move in the same commit, which is exactly the lockstep they were built to force. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
The TLA+ tier ladder gated everything on one monolithic model per profile, and the scheduled tiers gated on an event that measurement shows cannot occur: the nightly frontier grows at ~2.85 new states per retired state with no inflection, so the continuation can never drain its queue. This branch turns the layer into one primary configuration plus a manifest of focused proof obligations — each a strict disjunct-subset of the protocol relation, each passing only on
states_left = 0at exact measured floors — and makes the scheduled monolith continuation honest reporting instead of an unpassable gate.Every architectural claim in here is backed by a measurement recorded in
docs/model-checking.md; the short version:Next/Init. One wall seen five ways: the set-valuedmessagesvariable. Their configs carryDO NOT WIREmarkers with the numbers; the unlock is a message-dimension redesign, documented as future work.snapshotPrefixderived instead of stored, 34/34 mutation detectors preserved, identity proven on snapshot-free relations to the state.zsumz/tla-tools(upstream v1.8.0 is a rolling channel that deleted two pinned assets in five weeks; the sha256 remains the trust anchor).Contract
Producer
rafter-invariants-tla-v15 → v16, manifest schema9 → 10, with negative fixtures for every retired identity.primary_completionpinsgating-frontier-exhaustedfor PR (RaftCi still exhausts — 255,177,640 generated / 36,058,645 distinct measured post-reduction, floors tightened to those exact counts) andreporting-continuationfor nightly/weekly (a violation or malformed artifact still fails red; only "budget elapsed, frontier healthy" stops being a failure — the verifier rejects any PR receipt claiming reporting mode). Obligations live outside the checkpoint digest, so tuning them never resets primary lineage.Landing notes
cargo test -p rafter-invariants857 passed, the three CI contract guard targets 84 passed, action pins verified, and every wired floor re-measured on this exact tree.🤖 Generated with Claude Code