Benchmark/vendor examples specs - #131
Draft
lemmy wants to merge 37 commits into
Draft
Conversation
`_set_extends` treated an EXTENDS clause as multi-line only when a line ends in a comma, so a clause written as `EXTENDS` followed by the module names on the next lines lost only its keyword. The names stayed behind as a dangling statement and the generated Defs module did not parse.
`compute_reachable` deletes definitions outside the target theorem's closure, but a RECURSIVE declaration is a separate statement and survived, so SANY reported `declared in RECURSIVE statement but not defined`. The same arises in the Defs layer when the definition belongs to the shared model. Pruning in `_sm_tidy` covers the model, Defs and task layers.
Igor Konnov, Thanh Hai Tran and Josef Widder's encoding of the BOSCO one-step Byzantine consensus algorithm, at tlaplus/Examples 1ef5f15. The module states no theorems, so the copy adds `Spec => []P` for each invariant bosco.cfg checks: TypeOK and the agreement lemmas Lemma3_0, Lemma3_1, Lemma4_0, Lemma4_1. The module's ASSUMEs (N > 3*T, T >= F) carry into the generated model, so the theorems hold over the constants rather than over the configuration's N = 4, T = 1, F = 1. OneStep0 and OneStep1 are not targets: upstream notes they need more than 7*T processes, which no ASSUME states.
…riants
Nicholas Schultz-Møller's models of the LMAX Disruptor, at tlaplus/Examples
47b0e2c: Disruptor_MPMC and Disruptor_SPMC, both instantiating RingBuffer. The
modules state no theorems, so each copy adds `Spec => []TypeOk` and
`Spec => []NoDataRaces`, the two invariants the upstream configurations check.
NoDataRaces is the reason the specification exists: no slot ever holds a reader
and a writer at once, and never more than one writer.
RingBuffer's ASSUMEs (Size \in Nat \ {0}, non-empty Readers and Writers,
NULL \notin Values) already constrain the constants, and MaxPublished appears
only in an ASSUME, the state constraint and Liveliness -- never in an action.
Liveliness is not a target: TLC checks it only under CONSTRAINT
StateConstraint, which truncates the graph the fairness conditions are
evaluated on.
Calvin Loncaric's specification of tlc2.util.BufferedRandomAccessFile, the caching layer TLC uses for filesystem access, at tlaplus/Examples 0e018bc. Copyright (c) 2024, Oracle and/or its affiliates.
Upstream holds BufferedRandomAccessFile, RandomAccessFile and Common in a
single file. tlapm resolves an EXTENDS by file name, so it reports
`Unknown module "Common"` and aborts with Failure("Module.Parser.load_module").
The split moves each module into its own file and changes no text.
The modules state no ASSUME, so a theorem about them quantifies over every value of MaxOffset, BuffSz, Symbols and ArbitrarySymbol -- including values for which the invariants are false. With MaxOffset outside Nat, Offset == 0..MaxOffset need not contain 0, so TypeOK fails in the initial state, where length = 0. The three assumptions restate the constants' own comments: MaxOffset is "the highest possible offset (in reality this is 2^63 - 1)", BuffSz is a buffer size, and ArbitrarySymbol is a "special token for an arbitrary symbol", i.e. not one of the Symbols. They hold for the values BufferedRandomAccessFile.cfg uses.
…rems Fourteen goals, one per invariant and property in BufferedRandomAccessFile.cfg: the invariants TypeOK and Inv1, Inv3, Inv4, Inv5; the per-action step simulations FlushBufferCorrect, SeekCorrect, Write1Correct, Read1Correct, WriteAtMostCorrect, ReadCorrect and SeekEstablishesInv2, each of the form [][A => RAF!A]_vars; the refinement Safety == RAF!Spec; and Inv2CanAlwaysBeRestored, which needs ENABLED reasoning. Inv2 is not a target: upstream excludes it from the invariants deliberately, treating it as an action precondition and stating Inv2CanAlwaysBeRestored instead. SetLengthCorrect is defined but absent from the configuration, so nothing has checked it.
Lorin Hochstein's B-tree specification and the kvstore module it refines, at tlaplus/Examples 0e018bc.
TLAPS does not support recursive operator definitions: one RECURSIVE
declaration anywhere in the module chain makes tlapm abort with
Failure("Expr.Anon: Recursive"), whatever the goal is. A recursive function is
supported, and the key argument is unchanged by the recursion, so a function
over Nodes expresses it.
Under btree.cfg, TLC explores 2,820,091 states (374,727 distinct) with no
invariant violation both before and after.
Nodes == 1..MaxNode and Keys == 1..MaxKey, so without an ASSUME a theorem also covers constants for which those sets are empty: root = CHOOSE n \in Nodes is then unconstrained and TypeOk fails in the initial state. MaxOccupancy bounds a node's key count and is compared with Cardinality, so it is a positive natural too. The assumptions hold for the values btree.cfg uses (MaxNode = 8, MaxKey = 4, MaxOccupancy = 2), and TLC re-checks them there. NIL and MISSING need no assumption: the module defines them by CHOOSE outside Nodes and Vals.
Five goals, one per invariant in btree.cfg except FreeNodesRemain: TypeOk, InnersMustHaveLast, LeavesCantHaveLast, KeyOrderPreserved and KeysInLeavesAreUnique. FreeNodesRemain (\E n \in Nodes : IsFree(n)) is not a target: it holds for the configuration's MaxNode = 8 with MaxKey = 4, not for every MaxNode. The Refinement property (Mapping!Spec) is commented out of the configuration, so nothing has checked it either.
Andrew Helwer's specification of the Nano cryptocurrency protocol, at tlaplus/Examples 0e018bc. It states THEOREM Safety == Spec => TypeInvariant /\ SafetyInvariant, which upstream discharges by model checking.
TLAPS does not support recursive operator definitions: one RECURSIVE
declaration anywhere in the module chain makes tlapm abort with
Failure("Expr.Anon: Recursive"), whatever the goal is. The recursion walks a
chain of block hashes and the ledger argument never changes, so a function over
Hash expresses it.
BalanceAt and ValueOfSendBlock were mutually recursive operators. Since ValueOfSendBlock(ledger, h) is BalanceAt(ledger, ledger[h].block.previous) minus that block's balance, inlining it leaves a single recursion over one hash chain, which one recursive function over Hash expresses. ValueOfSendBlock remains as a non-recursive definition in terms of BalanceAt.
…support The operator removed one copy of an element per step, so its recursion is over bags and not over a shrinking set. Summing e * B[e] over BagToSet(B) gives the same total and recurses over the subsets of a fixed set, which a recursive function expresses. Under MCNanoSmall, TLC explores 6,083 states (3,003 distinct) before and after the three rewrites; under MCNanoMedium, 1,120,079 (530,587 distinct). No invariant violation either way.
The upstream theorem, Spec => TypeInvariant /\ SafetyInvariant, is annotated PROOF OMITTED so the generator treats it as a target. Upstream checks both invariants with MCNano; the module comment notes that finite model checking scales poorly for a blockchain and that "formal proofs should be used instead".
Giuliano Losa's specification of the Sailfish and Sailfish++ DAG-based consensus algorithms, at tlaplus/Examples 47b0e2c, with the BlockDag, Digraph and Utils modules it builds on. The TLCSailfish1 and TLCSailfish2 harnesses, which supply the constants, are not vendored.
TLAPS does not support recursive operator definitions: one RECURSIVE
declaration anywhere in the module chain makes tlapm abort with
Failure("Expr.Anon: Recursive"), whatever the goal is. Each recursive call
passes a set of dag's vertices, so a function over SUBSET (Vertices(dag) \cup vs)
covers every argument the recursion reaches, including a vs that is not
contained in the dag.
The recursion removes one element per step, so a function over SUBSET S expresses it. CHOOSE is deterministic, so the resulting order is the same.
…-dags
Unlike OrderSet, this recursion is not over a shrinking set: each call passes
SubDag(dag, {prevL}) and a vertex of it. Both components of a sub-dag are
subsets of dag's, so the function's domain is
(SUBSET Vertices(dag)) \X (SUBSET Edges(dag)) and Vertices(dag). TLC never
enumerates that domain, only tests membership when the function is applied.
Under TLCSailfish1, TLC explores 314,144 states (109,604 distinct) with no
invariant violation before and after the three rewrites in BlockDag and
Digraph.
N, F, IsQuorum, IsBlocking and Leader are constants, and the module states nothing about them beyond R = 1..n, leaving that to whatever instantiates it. Agreement is then false as a theorem: nothing prevents two disjoint quorums, so two correct nodes can commit incompatible logs. The four assumptions are the ones TLCSailfish1 states in prose -- "quorums are chosen such that every two quorums have a correct node in common, and each blocking set intersects all quorums and contains a correct node" -- plus F \subseteq N and Leader(r) \in N, which TypeOK needs since a Byzantine node and a round's leader contribute vertices. They are the standard Byzantine quorum assumptions the Sailfish paper's proofs use. Quantifying over SUBSET N rather than unboundedly keeps them checkable: TLC verifies all four for the constants of TLCSailfish1 and TLCSailfish2.
Three goals, one per INVARIANT in TLCSailfish1 and TLCSailfish2: TypeOK, Agreement (any two correct nodes' logs are compatible) and Liveness (a correct node two rounds past a synchronous round with a correct leader has committed that round's leader vertex). All three are state predicates, so each goal is Spec => []P. Agreement and Liveness rest on the quorum assumptions added in the previous commit rather than on upstream text, so they are the goals to re-examine first if a result looks implausible.
lemmy
marked this pull request as ready for review
August 21, 2026 02:09
Qian-Cheng-nju
self-requested a review
August 21, 2026 02:55
tlapm admits a module-level assumption only when a proof cites it by name:
an unnamed one never enters the obligation context, whether it is declared
in the module or inherited through EXTENDS. Every assumption of the six
newly vendored specs was unnamed, so a task whose goal needs a constant
fact could not be discharged at all.
braf's Thm_TypeOK is the case that shows it. Opus 5 proved 479 of its 480
obligations and failed only on `MaxOffset \in Nat /\ BuffSz \in Nat \ {0}`,
which is not merely unprovable but the reason the goal is false for
arbitrary constants: Init sets length = 0 while TypeOK requires
length \in 0..MaxOffset. With the names in place and that one step citing
them, the same proof discharges all 482 obligations.
Only names are added; every statement, upstream's and ours alike, is
unchanged, as is the emitted task set.
Its ASSUME keyword stands alone on its line, so the previous commit's scan missed it and the constant typing facts stayed uncitable.
E741: the comprehension variable `l` is ambiguous. Renamed, and the file reformatted as `ruff format` wants it.
TLC checks the assumptions of a module it extends, but not of one it instantiates, and both harnesses instantiate Sailfish. Contrary to what the commit adding them says, running TLCSailfish1 does not exercise them; they were checked against each harness's constants separately.
Member
|
@lemmy I may be missing an intended constraint, but I can reproduce two counterexamples at
Are |
lemmy
marked this pull request as draft
August 21, 2026 17:43
An unnamed assumption is usable after all: a BY clause may cite it by
repeating its statement, in the module that declares it and in one that
extends it. Naming it is a matter of legibility, not of admissibility, and
the two commits that introduced the names overstate the case -- braf's
Thm_TypeOK was provable as shipped, as the Thm_Safety proof from the same
run shows, opening with
LEMMA AgCst == ... BY BuffSz \in Nat \ {0}, MaxOffset \in Nat, SMTT("r5")
against the very files whose assumptions were unnamed. Confirmed by
discharging all 482 obligations of that task's failed proof, unchanged
except for the one step that read OBVIOUS.
Collaborator
Author
Let's get confirmation from the spec's original author: tlaplus/Examples#232 |
Collaborator
Author
tlaplus/Examples f3e248a (PR 232) names the assumptions of Disruptor_MPMC and
Disruptor_SPMC, adds Writers \cap Readers = {}, and moves MaxPublished, the
state constraint and Liveliness into the new MCDisruptor_MPMC and
MCDisruptor_SPMC harnesses. The benchmark copies now differ from upstream in
the two theorems alone.
The disjointness assumption is what makes those theorems true. A thread id in
both sets shares one pc between its writer and its reader role, so BeginRead
enables EndWrite; with the assumption removed and Writers = {w1, r1} against
Readers = {r1, r2, r3}, TLC reports NoDataRaces violated. With it in place the
same constants are rejected as an assumption violation.
MaxPublished is gone from the models, where it only ever bounded TLC.
MCDisruptor is not vendored: it states no theorem and Liveliness holds only
under the state constraint.
TLC on both harnesses against these copies: MPMC 422781 states, 112929
distinct, depth 81; SPMC 28049 states, 8496 distinct, depth 82, Liveliness
included. Both match the upstream manifest.
tlaplus/Examples 45c1cfd names RingBuffer's assumptions and EXTENDs Naturals
and FiniteSets instead of instantiating them LOCALly, so the vendored copy is
now upstream's text unchanged and the whole group deviates in the theorems
alone.
The EXTENDS is what makes NoDataRaces provable. Under LOCAL INSTANCE the
Cardinality of the goal is a local definition of the instantiated module,
which tlapm copies under the unwritable name Buffer!Cardinality$126, leaving
FiniteSetTheorems inapplicable to it. Exported, the copy is nameable and
<1>2. \A S : Buffer!Cardinality(S) = Cardinality(S)
BY DEF Buffer!Cardinality, Cardinality
closes the gap: both sides expand to the same term. Adding it to the round-1
attempt at Disruptor_MPMC_NoDataRacesCorrect takes that proof from 394/396 to
397/398 obligations, the remainder being its unwritten inductive step.
TLC on both harnesses is unchanged: MPMC 422781 states, 112929 distinct,
depth 81; SPMC 28049 states, 8496 distinct, depth 82.
Contributor
|
I found three issues and verified all three with TLC by reproducing counterexamples.
|
Disruptor_SPMC is the single-producer variant and keeps no per-writer state:
`published' is one integer shared by all of Writers, and BeginWrite guards on
it alone. Two writers therefore claim the same slot. Under TLC with
Writers = {w1, w2}, MCDisruptor_SPMC reports NoDataRaces violated, and TypeOk
violated on its own -- a reader appends an unwritten slot, so consumed leaves
[Readers -> Seq(Nat)]. Both benchmark goals are false without the assumption.
Upstream states the restriction only in the configuration's Writers = {w},
which a theorem quantifying over the constants does not see. Reported for
tlaplus/Examples separately.
Opus 5 reduced both SPMC tasks to exactly this fact -- `\E wr : Writers =
{wr}` for NoDataRaces, `NULL \in Nat \/ TCOneWriter` for TypeOk -- in four
attempts each, one unproved obligation apiece.
TLC unchanged on the upstream configuration: 28049 states, 8496 distinct,
depth 82. With two writers the assumption is now what TLC reports.
Contributor
|
I found one more issue in btree. MaxOccupancyPositive allows MaxOccupancy = 1, and with Vals = {vx}, MaxKey = 3, and MaxNode = 8, TLC finds a KeyOrderPreserved violation in 24 steps. Node 3 points to node 1 through both key slots, while node 3 holds key 1 and node 1 holds key 2, breaking the ordering. Node 2 also remains reachable but is marked free. MaxOccupancy = 2 is clean at both MaxNode = 8 and 12, so this is a branching-factor issue, not a node-budget one. Upstream's 9126be8 already requires MaxOccupancy >= 2, the vendored copy predates that fix. Everything else looked good, I checked several valid bosco (N,T,F) combinations, including T > F and multi-million-state runs, Sailfish's GST, all 14 braf goals against the upstream config, and the generated tasks' assumption chain. Two smaller assumption gaps :
Neither breaks a goal, but both weaken the assumptions compared with upstream. Since I only ran TLC, not tlapm, I can't say whether the goals are actually provable under these weaker assumptions. |
Collaborator
Author
|
@munimthahmid and @sukanya1426, may I suggest reproducing the issue and reporting your findings upstream, i.e., in the The PRs for Braf and Sailfish are still open, so they can be amended. The others may require new PRs. Also, I just pushed the obvious strengthening of SPMC's assumption. |
…finite
Upstream now states the single producer itself, as
ExactlyOneWriter == Cardinality(Writers) = 1, replacing AtLeastOneWriter, so
Disruptor_SPMC is vendored verbatim again apart from the theorems.
Cardinality is unspecified on an infinite set, so that assumption alone yields
neither a singleton nor even a non-empty Writers: FS_Singleton concludes
Cardinality(S) = 1 <=> \E x : S = {x} only for a finite S, and FS_EmptySet
likewise. The benchmark copy therefore adds IsFiniteSet(Writers).
Both goals are provable again with it. The proofs that passed at 9204552
against the singleton form fail on exactly the step that derives
Writers = {wr}; adding the finiteness fact and citing FS_Singleton across the
library instance closes them, at 201 and 692 obligations.
TLC unchanged on the upstream configuration: 28049 states, 8496 distinct,
depth 82. With two writers the assumption is what TLC reports.
Upstream states ExactlyOneWriter as IsFiniteSet(Writers) /\ Cardinality(Writers) = 1, which is what a proof needs: Cardinality is unspecified on an infinite set, so the cardinality alone yields neither the writer nor a non-empty Writers. The finiteness assumption this branch had added is therefore dropped, and all three modules of the group are upstream's text plus the theorems. Disruptor_SPMC_TypeOkCorrect closes at 200 obligations, citing FS_Singleton across the library instance. TLC on the upstream configuration is unchanged at 28049 states, 8496 distinct, depth 82.
Upstream now states the assumptions the algorithm needs and moves the model bounds into MCbtree, so btree.tla deviates in the five theorems alone. Keys and Nodes are constants rather than 1..MaxKey and 1..MaxNode, and the module EXTENDs Relation for IsStrictlyTotallyOrderedUnder, which the grader supplies from the Community Modules. The four upstream assumptions replace the three this branch had added, and each answers a counterexample: StatesAreDistinct rules out aliasing the control states, which breaks InnersMustHaveLast and KeyOrderPreserved; MaxOccupancyPermitsSplitting rules out MaxOccupancy = 1, where PivotOf empties one side of every split and a node is handed out twice; KeysAreOrdered is all the tree needs of a key domain it does not bound; NodePoolIsNonEmpty is needed for Init to take a root. FindLeafNode is still RECURSIVE upstream, so the rewrite as a recursive function stays. TLC under MCbtree explores 2820091 states, 374727 distinct, depth 38, before and after it. kvstore is upstream's text with its two assumptions named.
main now lets a proof-from-scratch agent import the official libraries itself, so a task no longer carries LOCAL INSTANCE TLAPS and friends.
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
4 participants
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.
Vendors six
tlaplus/Examplesspecifications as proof-from-scratch tasks: 245 → 277.brafRAF!Specrefinement,ENABLEDboscoTypeOK, agreement lemmasbtreeDisruptorTypeOk,NoDataRaces(MPMC and SPMC)dag-consensusTypeOK,Agreement,LivenessNanoBlockchainSafetytheoremEvery goal is an invariant or property the upstream TLC configuration checks. Theorems and, where the constants were unconstrained, assumptions were added; each assumption commit states what breaks without it.
Refactorings
Committed separately from the verbatim vendoring, one commit each:
EXTENDSby file name.RECURSIVEdeclaration anywhere in the module chain makes tlapm abort withFailure("Expr.Anon: Recursive"), whatever the goal. Justified by TLC exploring the same state space before and after; counts are in the commit messages.Generator fixes (prerequisites)
EXTENDSwhose keyword stands alone lost only its keyword.RECURSIVEdeclaration survived the stripping of its definition.Regenerating the whole suite is byte-identical for all pre-existing tasks;
tests/datasetpasses.Review note
Sailfish's
AgreementandLivenessare the only goals whose truth at arbitrary constants rests on assumptions added here — the Byzantine quorum intersection propertiesTLCSailfish1states in prose. TLC verifies them for both harnesses' constants.