Skip to content

Towards a TLAPS stdlib #127

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
muenchnerkindl merged 5 commits into from
Jul 14, 2026
Merged

Towards a TLAPS stdlib #127

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
da7dcc1
Theorems about Contains and majority supersets
lemmy Jul 8, 2026
2a921b4
IsSorted operator and sortedness theorems
lemmy Jul 9, 2026
15d49d4
theorems about sequences, finite sets, and quorum systems
muenchnerkindl Jul 10, 2026
c5b1627
fixing two apparently brittle proofs
muenchnerkindl Jul 10, 2026
c27bdc9
align theorem statements in SequencesExtTheorems with those in the _p…
muenchnerkindl Jul 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions modules/FiniteSetsExtTheorems.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,5 +357,23 @@ THEOREM MinNat ==
PROVE /\ Min(S) \in S
/\ \A y \in S : Min(S) <= y

---------------------------------------------------------------------------

(*************************************************************************)
(* Theorems about majorities. A "majority" of a finite set U is any *)
(* subset whose cardinality is more than half that of U. This *)
(* generalizes the notion of a quorum used in distributed-consensus *)
(* specifications, where U is the set of servers. *)
(*************************************************************************)

(*************************************************************************)
(* Any superset (within U) of a majority of U is itself a majority. *)
(*************************************************************************)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not, but in my experience a more abstract definition of a quorum system as sets (of processes) such that any two quorums intersect and closed under superset is easier to use. Something like

QuorumSystem(S) ==
    { QS \in SUBSET (SUBSET S) : 
          /\ QS # {}
          /\ \A Q1, Q2 \in QS : Q1 \cap Q2 # {}
          /\ \A Q1, Q2 \in SUBSET S : Q1 \in QS /\ Q1 \subseteq Q2 => Q2 \in QS
    }

One could then show that majorities constitute a quorum system, i.e.

THEOREM MajorityIsQS ==
    ASSUME NEW S, S # {}, IsFiniteSet(S)
    PROVE  { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) } \in QuorumSystem(S)

@lemmy lemmy Jul 9, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your def is similar to what appears e.g. in https://github.com/microsoft/CCF/blob/main/tla/consensus/ccfraft.tla#L427-L429

THEOREM SupersetOfMajorityIsMajority ==
ASSUME NEW U, IsFiniteSet(U),
NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2,
2 * Cardinality(Q1) > Cardinality(U)
PROVE 2 * Cardinality(Q2) > Cardinality(U)


===========================================================================
16 changes: 16 additions & 0 deletions modules/FiniteSetsExtTheorems_proofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -621,4 +621,20 @@ THEOREM MinNat ==
/\ \A y \in S : Min(S) <= y
BY MinIntBounded, \A y \in S : 0 <= y

---------------------------------------------------------------------------

(*************************************************************************)
(* Any superset (within U) of a majority of U is itself a majority. *)
(*************************************************************************)
THEOREM SupersetOfMajorityIsMajority ==
ASSUME NEW U, IsFiniteSet(U),
NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2,
2 * Cardinality(Q1) > Cardinality(U)
PROVE 2 * Cardinality(Q2) > Cardinality(U)
<1>1. IsFiniteSet(Q2) /\ Cardinality(Q2) <= Cardinality(U) BY FS_Subset
<1>2. IsFiniteSet(Q1) /\ Cardinality(Q1) <= Cardinality(Q2) BY <1>1, FS_Subset
<1>3. Cardinality(Q1) \in Nat /\ Cardinality(Q2) \in Nat /\ Cardinality(U) \in Nat
BY FS_CardinalityType, <1>1, <1>2
<1>. QED BY <1>2, <1>3
Comment thread
lemmy marked this conversation as resolved.

================================================================================
19 changes: 19 additions & 0 deletions modules/Quorum.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
--------------------------------- MODULE Quorum -----------------------------

(***************************************************************************)
(* A quorum system for a set S is a non-empty collection of quorums, i.e. *)
(* subsets of S such that any two quorums intersect. It is typically also *)
(* assumed that a superset of a quorum is itself a quorum. *)
(* *)
(* For example, given a finite and non-empty set S of servers, the sets of *)
(* strict majorities among servers form a quorum system. *)
(***************************************************************************)

QuorumSystem(S) ==
{ QS \in SUBSET (SUBSET S) :
/\ QS # {}
/\ \A Q1, Q2 \in QS : Q1 \cap Q2 # {}
/\ \A Q1, Q2 \in SUBSET S : Q1 \in QS /\ Q1 \subseteq Q2 => Q2 \in QS
}

=============================================================================
26 changes: 26 additions & 0 deletions modules/QuorumTheorems.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE QuorumTheorems -------------------------
EXTENDS Quorum, Integers, FiniteSets

(***************************************************************************)
(* Direct consequences of the definition of a quorum system. *)
(***************************************************************************)

THEOREM QuorumsIntersect ==
ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS
PROVE \E s \in S : s \in Q1 \cap Q2

THEOREM QuorumSuperset ==
ASSUME NEW S, NEW QS \in QuorumSystem(S),
NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2
PROVE Q2 \in QS

(***************************************************************************)
(* Strict majorities of a non-empty set S form a quorum system. *)
(***************************************************************************)

THEOREM MajoritiesQuorumSystem ==
ASSUME NEW S, IsFiniteSet(S), S # {}
PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) }
\in QuorumSystem(S)

=============================================================================
29 changes: 29 additions & 0 deletions modules/QuorumTheorems_proofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
------------------------- MODULE QuorumTheorems_proofs ----------------------
EXTENDS Quorum, Integers, FiniteSetTheorems, FiniteSetsExtTheorems

(***************************************************************************)
(* Direct consequences of the definition of a quorum system. *)
(***************************************************************************)

THEOREM QuorumsIntersect ==
ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS
PROVE \E s \in S : s \in Q1 \cap Q2
BY DEF QuorumSystem

THEOREM QuorumSuperset ==
ASSUME NEW S, NEW QS \in QuorumSystem(S),
NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2
PROVE Q2 \in QS
BY DEF QuorumSystem

(***************************************************************************)
(* Strict majorities of a non-empty set S form a quorum system. *)
(***************************************************************************)

THEOREM MajoritiesQuorumSystem ==
ASSUME NEW S, IsFiniteSet(S), S # {}
PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) }
\in QuorumSystem(S)
BY FS_CardinalityType, FS_EmptySet, FS_Subset, FS_Union DEF QuorumSystem

=============================================================================
25 changes: 25 additions & 0 deletions modules/SequencesExt.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,31 @@ BoundedSeq(S, n) ==
Contains(s, e) ==
\E i \in 1..Len(s) : s[i] = e

(**************************************************************************)
(* TRUE iff the sequence s is sorted with respect to the binary *)
(* relation op, i.e. op(s[i], s[j]) holds for every pair of positions *)
(* i, j in the domain of s with i < j. *)
(* *)
(* No assumptions are made about op; its meaning is fixed by the *)
(* caller. When op is a strict order (irreflexive and transitive), *)
(* s is strictly increasing and therefore duplicate-free; when op is *)
(* a reflexive relation such as <=, equal elements may be adjacent. *)
(* Instantiating op with the converse relation sorts s in the *)
(* opposite direction. The empty sequence and every singleton are *)
(* vacuously sorted under any op. *)
(* *)
(* Examples: *)
(* IsSorted(<<>>, <) = TRUE *)
(* IsSorted(<<5>>, <) = TRUE *)
(* IsSorted(<<1, 2, 3>>, <) = TRUE *)
(* IsSorted(<<1, 2, 2>>, <) = FALSE (not strictly increasing) *)
(* IsSorted(<<1, 2, 2>>, <=) = TRUE *)
(* IsSorted(<<3, 2, 1>>, <) = FALSE *)
(* IsSorted(<<3, 2, 1>>, >) = TRUE *)
(**************************************************************************)
IsSorted(s, op(_, _)) ==
\A i, j \in 1..Len(s) : i < j => op(s[i], s[j])

(**************************************************************************)
(* Reverse the given sequence s: Let l be Len(s) (length of s). *)
(* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>> *)
Expand Down
91 changes: 91 additions & 0 deletions modules/SequencesExtTheorems.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,97 @@ THEOREM SequencesInductionCons ==
\A s \in Seq(S), e \in S : P(s) => P(Cons(e,s))
PROVE \A seq \in Seq(S) : P(seq)

(***************************************************************************)
(* Theorems about Contains. *)
(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *)
(***************************************************************************)

(* Membership in a sequence coincides with membership in its image set. *)
THEOREM ContainsRange ==
ASSUME NEW S, NEW s \in Seq(S), NEW e
PROVE Contains(s, e) <=> e \in Range(s)

THEOREM ContainsEmpty ==
ASSUME NEW e
PROVE ~ Contains(<< >>, e)

THEOREM ContainsAppend ==
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x)

THEOREM ContainsSingleton ==
ASSUME NEW S, NEW x
PROVE \A e : Contains(<< x >>, e) <=> e = x

THEOREM ContainsConcat ==
ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e
PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e))

THEOREM ContainsCons ==
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e))

THEOREM ContainsTail ==
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e
PROVE Contains(Tail(s), e) => Contains(s, e)

(* An element other than the head of a non-empty sequence that occurs in *)
(* the sequence also occurs in its tail. *)
THEOREM ContainsTailExceptHead ==
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e,
Contains(s, e), e # Head(s)
PROVE Contains(Tail(s), e)

(***************************************************************************)
(* Theorems about IsSorted (see SequencesExt). *)
(* *)
(* The relevant order properties of op (transitivity, irreflexivity) *)
(* are stated locally as hypotheses of each theorem, so that the *)
(* theorems apply to an arbitrary binary relation op rather than only *)
(* to relations globally known to be orders. *)
(***************************************************************************)

THEOREM SortedEmpty ==
ASSUME NEW op(_,_)
PROVE IsSorted(<< >>, op)

THEOREM SortedSingleton ==
ASSUME NEW S, NEW x \in S, NEW op(_,_)
PROVE IsSorted(<< x >>, op)

(* Appending an element that dominates the last one keeps the sequence *)
(* sorted, provided the ordering relation is transitive. *)
THEOREM SortedAppend ==
ASSUME NEW S, NEW op(_,_),
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We might consider using the predicate IsTransitiveUnder from Relation.tla instead of this explicit hypothesis, although it may introduce unnecessarily heavy notation.

NEW s \in Seq(S), IsSorted(s, op),
NEW e \in S, s # << >> => op(s[Len(s)], e)
PROVE IsSorted(Append(s, e), op)

(* Concatenating two sorted sequences whose boundary elements are ordered *)
(* yields a sorted sequence (for a transitive ordering relation). *)
THEOREM SortedConcat ==
ASSUME NEW S, NEW op(_,_),
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
NEW s \in Seq(S), NEW t \in Seq(S),
IsSorted(s, op), IsSorted(t, op),
(Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1])
PROVE IsSorted(s \o t, op)

(* A sequence sorted by an irreflexive relation has no repeated elements. *)
THEOREM SortedInjective ==
ASSUME NEW S, NEW op(_,_),
\A x \in S : ~ op(x, x),

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly, there is a predicate IsIrreflexiveUnder in Relation.tla.

NEW s \in Seq(S), IsSorted(s, op)
PROVE IsInjective(s)

(* Any contiguous subsequence of a sorted sequence is sorted. *)
THEOREM SortedSubSeq ==
ASSUME NEW S, NEW op(_,_),
NEW s \in Seq(S), IsSorted(s, op),
NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s)
PROVE IsSorted(SubSeq(s, m, n), op)

(***************************************************************************)
(* Theorems about InsertAt and RemoveAt. *)
(* InsertAt(seq,i,elt) == *)
Expand Down
102 changes: 102 additions & 0 deletions modules/SequencesExtTheorems_proofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,108 @@ THEOREM SequencesInductionCons ==
<2>. QED BY <2>1
<1>. QED BY <1>2, <1>3, NatInduction, Isa

(***************************************************************************)
(* Theorems about Contains. *)
(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *)
(***************************************************************************)

THEOREM ContainsRange ==
ASSUME NEW S, NEW s \in Seq(S), NEW e
PROVE Contains(s, e) <=> e \in Range(s)
BY DEF Contains, Range

THEOREM ContainsEmpty ==
ASSUME NEW e
PROVE ~ Contains(<< >>, e)
BY DEF Contains

THEOREM ContainsAppend ==
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For me, the simple proof BY DEF Contains works.

BY DEF Contains

THEOREM ContainsSingleton ==
ASSUME NEW x
PROVE \A e : Contains(<< x >>, e) <=> e = x
BY Isa DEF Contains

THEOREM ContainsConcat ==
ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e
PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e))

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

simpler proof:

<1>1. ASSUME Contains(s \o t, e)  PROVE  Contains(s,e) \/ Contains(t,e)
  BY <1>1 DEF Contains 
<1>2. ASSUME Contains(s, e)  PROVE Contains(s \o t, e)
  <2>1. PICK i \in 1 .. Len(s) : s[i] = e 
    BY <1>2 DEF Contains
  <2>. QED  BY <2>1 DEF Contains 
<1>3. ASSUME Contains(t, e)  PROVE Contains(s \o t, e)
  <2>1. PICK i \in 1 .. Len(t) : t[i] = e 
    BY <1>3 DEF Contains
  <2>. QED  BY <2>1, Len(s)+i \in 1 .. Len(s \o t) DEF Contains 
<1>. QED  BY <1>1, <1>2, <1>3

<1>1. ASSUME Contains(s \o t, e), ~ Contains(t, e) PROVE Contains(s, e)
BY <1>1 DEF Contains
<1>2. ASSUME Contains(s, e) PROVE Contains(s \o t, e)
<2>. PICK i \in 1 .. Len(s) : s[i] = e
BY <1>2 DEF Contains
<2>. QED BY i \in 1 .. Len(s \o t) DEF Contains
<1>3. ASSUME Contains(t, e) PROVE Contains(s \o t, e)
<2>. PICK i \in 1 .. Len(t) : t[i] = e
BY <1>3 DEF Contains
<2>. QED BY Len(s)+i \in 1 .. Len(s \o t) DEF Contains
<1>. QED BY <1>1, <1>2, <1>3

THEOREM ContainsCons ==
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e))

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY ContainsConcat, ContainsSingleton, Zenon DEF Cons works.

BY ContainsConcat, ContainsSingleton, <<x>> \in Seq({x}) DEF Cons

THEOREM ContainsTail ==
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e
PROVE Contains(Tail(s), e) => Contains(s, e)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF Contains works.

BY DEF Contains

THEOREM ContainsTailExceptHead ==
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e,
Contains(s, e), e # Head(s)
PROVE Contains(Tail(s), e)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF Contains works.

BY DEF Contains

(***************************************************************************)
(* Theorems about IsSorted. *)
(* IsSorted(s, op) == \A i,j \in 1..Len(s) : i<j => op(s[i],s[j]) *)
(***************************************************************************)

THEOREM SortedEmpty ==
ASSUME NEW op(_,_)
PROVE IsSorted(<< >>, op)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF IsSorted is enough.

BY DEF IsSorted

THEOREM SortedSingleton ==
ASSUME NEW S, NEW x \in S, NEW op(_,_)
PROVE IsSorted(<< x >>, op)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF IsSorted works.

BY DEF IsSorted

THEOREM SortedAppend ==
ASSUME NEW S, NEW op(_,_),
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
NEW s \in Seq(S), IsSorted(s, op),
NEW e \in S, s # << >> => op(s[Len(s)], e)
PROVE IsSorted(Append(s, e), op)
Comment on lines +157 to +158

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF IsSorted works.

BY DEF IsSorted

THEOREM SortedConcat ==
ASSUME NEW S, NEW op(_,_),
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
NEW s \in Seq(S), NEW t \in Seq(S),
IsSorted(s, op), IsSorted(t, op),
(Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1])
PROVE IsSorted(s \o t, op)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF IsSorted works.

BY SMTT(20) DEF IsSorted

THEOREM SortedInjective ==
ASSUME NEW S, NEW op(_,_),
\A x \in S : ~ op(x, x),
NEW s \in Seq(S), IsSorted(s, op)
PROVE IsInjective(s)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF IsSorted, IsInjective works.

BY DEF IsSorted, IsInjective

THEOREM SortedSubSeq ==
ASSUME NEW S, NEW op(_,_),
NEW s \in Seq(S), IsSorted(s, op),
NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s)
PROVE IsSorted(SubSeq(s, m, n), op)

@muenchnerkindl muenchnerkindl Jul 9, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BY DEF IsSorted works.

BY DEF IsSorted

(***************************************************************************)
(* Theorems about InsertAt and RemoveAt. *)
(* InsertAt(seq,i,elt) == *)
Expand Down
Loading