DEV Community: Georgii

Commit to marriage with TLA+ pt.2

Georgii — Mon, 24 Feb 2025 01:28:43 +0000

Introduction

This is the second blog post (here is the first one [1]) in the series of the conspectus of the "Introduction to TLA+" course by Leslie Lamport. As usual, all credits are to Leslie Lamport and his course that can be found on his website. In this part, we will consider the Transaction Commit and Two-Phase Commit algorithms.

Transaction Commit

In the first part we consider the Transaction Commit algorithm [3], pp.2-4. In a distributed system, a transaction commit involves multiple resource managers (RMs) across different nodes that must unanimously decide to either commit or abort a transaction. The protocol ensures that all RMs either reach a committed state or an aborted state, supported by the conditions of stability and consistency, which mandate that once an RM reaches one of these states, it cannot revert, and no RM can be in the opposite state.

A database transaction is performed by a collection of processes called resource managers. A transaction can either commit or abort. It can commit only iif all resource managers are prepared to commit and must abort if any resource manager wants to abort.

All resource managers must agree on whether a transaction is committed or aborted.

Unfortunately, this platform does not fully support the formatting we have on our website, so if you are interested, please read the original blog post.

Do not die hard with TLA+ pt.1

Georgii — Sun, 16 Feb 2025 04:12:19 +0000

Introduction

This is the first blog post in the series of the conspectus of the “Introduction to TLA+” course by Leslie Lamport. It would directly follow the course structure and would be a good reference for those who are taking the course because it adds some additional information and explanations to the course material. So all credits are to Leslie Lamport and his course, which can be found on his website.

TLA + is based on temporal logic so you may read about it in our LTL and CTL Applications for Smart Contracts Security blog post.

Inroduction to TLA+

TLA+ is a language for high-level (design level, above the code) systems (modules, algorithms, etc.) modelling and consists of the following components:

TLC — the model checker;
TLAPS — the TLA+ proof system;
TLA+ Toolbox — the IDE.

TLA+ system is used to model critical parts of digital systems, abstracting away less-critical parts and lower-level implementation details. TLA+ was designed for designing concurrent and distributed systems in order to help find and correct design errors that are hard to find by testing and before writing any single line of code.

OpenComRTOS is a commercial network-centric, real-time operating system [3] that heavily used TLA+ during the design and development process and shared their experience in the freely available book [4]. And showed that using design gratefully reduces the code base size and number of errors and boosts the engineering view overall.

Consequently, TLA+ provides programmers and engineers a new way of thinking that makes them better programmers and engineers even when TLA+ are not useful. TLA+ forces engineers to think more abstractly.

Abstraction — the process of removing irrelevant details and the most important part of engineering. Without them, we cannot design and understand small systems.

An example of using TLA+ in a huge company for verifying a system that many of us use daily is Amazon Web Services. They use TLA+ to verify the correctness of their distributed algorithms and AWS system design [5]. The problem of algorithms and communication in distributed systems is well described in Leslie Lamport's paper "Time, Clocks, and the Ordering of Events in a Distributed System" [6].

A system design is expressed in a formal way called specification.

Specification — the precise high-level model.

TLA+ defines the specification, but it cannot produce the code. But it helps come with much clearer architecture and write more precise, accurate, in some cases compact code. It is able to check properties that express conditions on an individual execution (a system satisfies a property if and only if every single execution satisfies it).

The underlying abstraction of TLA+ is as follows: an execution of a system is represented as a sequence of discrete steps, where a step is the change from one state to the next one:

discrete — continuous evolution is a sequence of discrete events (computer is a discrete events-based system);
sequence — a concurrent system can be simulated with a sequential program;
step — a state change;
state — an assignment of values to variables.

Behavior — a sequence of states.

A state machine in the context of TLA+ system is described by:

all possible initial states – [what the variables are] and [their possible initial values];
what next states can follow any given state – a relation between their values in the current state and their possible values in the next state;
halts if there is no possible next state.

Control state — the next to be executed statement.

State machines eliminate low-level implementation details, and TLA+ is a language to describe state machines.

State Machines in TLA+

TLA+ uses ordinary, simple math. Consider a defined state machine example for the following C code

int i;
void main()
{
    i = someNumber();
    i = i + 1;
}

In order to turn this code into the TLA+ state machine definition we need to pack the execution flow of this code into states (sets of variables). For the given example, it is obvious how to define i variable. But we also need to instantiate the control state. We call it a pc such as:

pc = "start" = i = someNumber();
pc = "middle" = i = i + 1;
pc = "done" = execution is finished.

Assume for this example someNumber() returns an integer from the [0:1000] interval.

To define the system we need to define the initial state of the system the the next possible system state, expressed as a formula, that can be reached from the current state.

Here is the formula of the C code above, not the sequence of execution.

Initial-state formula: (i = 0) /\ (pc = "start")
Next-state formula:

\/    /\ pc = "start"
      /\ i' \in 0..1000
      /\ pc' = "middle"
\/    /\ pc = "middle"
      /\ i' = i + 1
      /\ pc' = "done"

Since this is the formula, it respects such formulas properties as commutativity, associativity, etc.

Sub-formulas can also be extracted into their own definitions to make a spec more compact.

A == /\ pc = "start"
     /\ i' \in 0..1000
     /\ pc' = "middle"

B == /\ pc = "middle"
     /\ i' = i + 1
     /\ pc' = "done"

Next == A \/ B

From this spec, we see that there are two possible next states that can be reached beginning from the initial state. A states the beginning of the execution, assigning a number to i and moving to the next pc state equals p', B states the increment of i and moving to the final state.

Resources and tools

There are not many learning resources of TLA+; however, there are some that we need to mention:

Learning TLA+ — a portal with useful links;
TLA+ toolbox binaries — a Java based TLA+ IDE;
pdflatex — a required component to render pdf;

Model Checking

Now, let us talk about TLC and model-checking-related topics.

TLC computes all possible behaviors allowed by the spec. More precisely, TLC checks a model of the specification.

TLC reports deadlock if execution stopped when it was not supposed to;
TLC reports termination if execution stopped when it was supposed to.

TLA+ allows writing theorems and formal proofs of those theorems.
TLAPS (TLA proof system) is a tool for checking those proofs, it can check proofs of correctness of algorithms.

Practically, the term spec (a specification) means:

the set of modules, including imported modules consists of .tla files;
the TLA formula specifies the set of allowed behaviors of the system or algorithm being specified.

A specification may contain multiple models. The model tells TLC what it should do. Here are the parts of the model that must be explicitly chosen:

what the behavior spec is (The behavior spec is the formula or pair of formulas that describe the possible behaviors of the system or algorithm you want to check);
what TLC should check;
what values to substitute for constant parameters.

Behavior spec

There are two ways to write the behavior spec:

Init and Next
- A pair of formulas that specify the initial state and the next-state relation, respectively.
Single formula
- A single temporal formula of the form Init and [][Next]_{vars} and F, where
  - Init is the initial predicate;
  - Next is the next-state relation;
  - vars is the tuple of variables;
  - and F is an optional fairness formula.

The only way to write a behavior spec that includes fairness is with a temporal formula, otherwise, a spec would not have variables and in this case, TLC will check assumptions and evaluate a constant expression.

There are three kinds of properties of the behavior spec that TLC can check:

Deadlock — A deadlock is said to occur in a state for which the next-state relation allows no successor states;
Invariants — a state predicate that is true of all reachable states--that is, states that can occur in a behavior allowed by the behavior spec;
Properties — TLC can check if the behavior spec satisfies (implies) a temporal property, which is expressed as a temporal-logic formula.

Model

The most basic part of a model is a set of assignments of values to declared constants.

Ordinary assignment

It is possible to set the value of the constant to any constant TLA+ expression that contains only symbols defined in the spec. The expression can even include declared constants, as long as the value assigned to a constant does not depend on that constant (escape circular dependencies). A model must specify the values of all declared constants.

Model value

A model value is an unspecified value that TLC considers to be unequal to any value that you can express in TLA+. You can substitute the set {p1, p2, p3\} of three model values for Proc. If by mistake you write an expression like p+1 where the value of p is a process, TLC will report an error when it tries to evaluate that expression because it knows that a process is a model value and thus not a number. An important reason for substituting a set of model values for Proc is to let TLC take advantage of symmetry.

Example: NotANat == CHOOSE n : n \notin Nat

It defines NotANat to be an arbitrary value that is not a natural number. TLC cannot evaluate this definition because it cannot evaluate the unbounded CHOOSE expression. To allow TLC to handle the spec, you need to substitute a model value for NotANat. The best model value to substitute for it is one named NotANat. This is done by the Definition Override. The TLA+ Toolbox creates the appropriate entry in that section when it creates a model if it finds a definition having the precise syntax above or the syntax:
NotANat == CHOOSE n: ~(n \in Nat), where Nat can be any expression, and NotANat and n can be any identifiers.

Model values can be typed as follows: a model value has type T if and only if its name begins with the two characters T_ .

A model value declared in the model can be used as an ordinary value in any expression that is part of the model's specification.

Symmetry

Consider a specification of a memory system containing a declared constant Val that represents the set of possible values of a memory register. The set Val of values is probably a symmetry set for the memory system's behavior specification, meaning that permuting the elements in the set of values does not change whether or not a behavior satisfies that behavior spec. TLC can take advantage of this to speed up its checking. Suppose we substitute a set {v1, v2, v3} of model values for Val. We can use the Symmetry set option to declare this set of model values to be a symmetry set of the behavior spec. This will reduce the number of reachable states that TLC has to examine by up to 3!, or 6.

You can declare more than one set of model values to be a symmetry set. However, the union of all the symmetry sets cannot contain two typed model values with different types.

TLC does not check if a set you declare to be a symmetry set really is one. If you declare a set to be a symmetry set and it isn't, then TLC can fail to find an error that it otherwise would find. An expression is symmetric for a set S if and only if interchanging any two values of S does not change the value of the expression. The expression {{v1, v2}, {v1, v3}, {v2, v3}} is symmetric for the set {v1, v2, v3} — for example, interchanging v1 and v3 in this expression produces {{v3, v2}, {v3, v1}, {v2, v1}}, which is equal to the original expression. You should declare a set S of model values to be a symmetry set only if the specification and all properties you are checking are symmetric for S after the substitutions for constants and defined operators specified by the model are made. For example, you should not declare {v1, v2, v3} to be a symmetry set if the model substitutes v1 for some constant. The only TLA+ operator that can produce a non-symmetric expression when applied to a symmetric expression is CHOOSE. For example, the expression CHOOSE x \in {v1, v2, v3} : TRUE is not symmetric for {v1, v2, v3}.

Symmetry sets should not be used when checking liveness properties. Doing so can make TLC fail to find errors, or to report nonexistent errors.

Die Hard

Die Hard is an action movie from 1988. In this movie, there is a scene where our heroes need to solve a problem with two jugs in order to disable a bomb. The problem is to measure 4 gallons of water using 3 and 5-gallon jugs.

For the plot, search: "Die Hard Jugs problem" on YouTube or simply click here 🙂. We will solve this problem using TLA+.

First, we need to write the behavior. Let values of small and big represent a number of gallons in each jug.

$\begin{bmatrix} small & 0 \ big & 0 \ \end{bmatrix} \rightarrow \begin{bmatrix} small & 3 \ big & 0 \ \end{bmatrix} \rightarrow \begin{bmatrix} small & 0 \ big & 3 \ \end{bmatrix} \rightarrow \begin{bmatrix} small & 3 \ big & 3 \ \end{bmatrix} \rightarrow ...$

Filling a jug is a single step; there are no intermediate steps.

Real specifications are written to eliminate some kinds of errors.

TLA+ has no type declarations; however, it is important to define a formula that asserts type correctness. It helps to understand the spec and TLC can check types by checking if such a formula is always true.

TypeOK == /\ small \in 0..3
          /\ big   \in 0..5

Here, we define that small is an integer in the range [0:3] and big is an integer in the range [0:5]. But this definition is not a part of the spec.

The Initial-State Formula Init == small = 0 /\ big = 0 defines the initial state of the system.
The Next-State Formula defines possible transfers from state to state and is usually written as F_1 or F_2 or ... or F_n, where each formula F_i allows a different kind of step.

Our problem has 3 kinds of steps:

fill a jug;
empty a jug;
pour from one jug into the other.

We define the spec as follows:

Next == \/ FillSmall  \* fill the small jug
        \/ FillBig    \* fill the big jug
        \/ EmptySmall \* empty the small jug
        \/ EmptyBig   \* empty the big jug
        \/ SmallToBig \* pour water from small jug in the big jug
        \/ BigToSmall \* pour water from the big jug in the small jug

The names of definitions (like FillSmall, etc.) must be defined before the usage (precede the definition of Next).

FillSmall == /\ small' = 3
             /\ big' = big

When defining formulas we need to keep in mind thinking of the system as a whole and about steps as a transition from one state to another. In our case, it means that we cannot define FillSmall as FillSmall == small' = 3 because this formula doesn't have a part defining the second part of the program state (big). In other words, this formula turns true if small' equals 3 and big' equals whatever. But this is not correct. In fact, if we fill the small jug, we keep the big jug in the state it is without changes.

Now, we define SmallToBig. There are two possible cases we need to consider:

SmallToBig == /\ IF big + small <= 5
                  THEN /* There is room -> empty small.
                  ELSE /* There is no room -> fill big.

SmallToBig == /\ IF big + small <= 5
                  THEN /\ big' = big + small
                       /\ small' = 0
                  ELSE /\ big' = 5
                       /\ small' = small - (5 - big)

------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers

VARIABLES small, big

TypeOK == /\ small \in 0..3
          /\ big \in 0..5

Init == /\ big = 0
        /\ small = 0

FillSmall == /\ small' = 3
             /\ big' = big

FillBig == /\ big' = 5
           /\ small' = small

EmptySmall == /\ small' = 0
              /\ big' = big

EmptyBig == /\ big' = 0
            /\ small' = small

SmallToBig == IF big + small =< 5
                THEN /\ big' = big + small
                     /\ small' = 0
                ELSE /\ big' = 5
                     /\ small' = small - (5 - big)

BigToSmall == IF big + small =< 3
               THEN /\ big' = 0
                    /\ small' = big + small
               ELSE /\ big' = big - (3 - small)
                    /\ small' = 3

Next == \/ FillSmall
        \/ FillBig
        \/ EmptySmall
        \/ EmptyBig
        \/ SmallToBig
        \/ BigToSmall

=============================================================================

If we create and run a model for this spec we will see no errors and this is fine; however, it doesn't check any particular invariant of our spec.

Invariant is a formula that is true in every reachable state.

We have defined a TypeOK as a type definition for small and big, so we can add this formula as an invariant to check that this invariant is not broken.

If we run it now, we still see no errors meaning small and big respecting their types in every reachable state.

Now we can solve the die-hard problem of pouring big with exactly 4 gallons of water. To do it, we add a new invariant big /= 4 into the invariants section.

Here, this invariant works as a counterexample. An invariant is a formula that turns to true in every reachable state. We need to find a state (actually a state sequence) where big = 4, so we negate this by the /= symbol that equals neq. With this new formula, if we run the model, it finds an error (a state where an invariant is broken) and shows a sequence of states that led to this state.

Now, we can see the exact steps that are required to be done to solve the problem and our heroes can move on.

Original publication

References

Small and Big Step Semantics

Georgii — Sat, 08 Feb 2025 04:18:02 +0000

Small-step semantics and big-step semantics are two approaches used in the field of formal semantics within computer science, particularly in the study of programming languages and formal verification. These semantic models provide formal ways to describe how programs execute and are used to reason about the behavior of programs in a deductive way.

Small-Step Semantics (Operational Semantics)

Small-step semantics, also known as structural operational semantics, describes the execution of programs as a sequence of individual computation steps. Each step represents a single, atomic action, such as the evaluation of an expression, the execution of a statement, or a change in the program’s state.

Granularity: It focuses on the fine-grained, step-by-step execution process.
Transition System: The execution is modelled as a transition system where each transition corresponds to a small step. The system is described by a set of rules that define how one program state transitions to another.
Expressions and Commands: Both expressions and commands are evaluated using rules that specify how a single computational step proceeds.

Small-step semantics is particularly useful for understanding the dynamics of program execution, analyzing properties like termination, and reasoning about concurrent or interactive systems where the interleaving of actions matters.

Big-Step Semantics (Natural Semantics)

Big-step semantics, also known as natural semantics, describes the execution of programs as a relation between an initial program state and its final state after the program has completed execution. Instead of focusing on the individual steps of execution, it captures the overall effect of executing a piece of code.

Completeness: It emphasizes the result of executing an expression or a command, usually ignoring the intermediate steps.
Evaluation Relations: The semantics are given in terms of evaluation relations that directly relate an initial state and an expression or command to their final state and result.
Suitability: Big-step semantics is well-suited for reasoning about the final outcomes of program execution, making it useful for proving properties like correctness and equivalence of programs.

Small-step semantics offer a detailed view of execution, allowing for the analysis of intermediate states, which is essential for understanding how specific computations unfold over time. Big-step semantics provides a more abstract, high-level view, focusing on the initial and final states without detailing how those states are reached.

Small-step semantics is often preferred in scenarios where the process of computation is as important as the result, such as in interactive systems, concurrent programming, and step-wise debugging tools. Big-step semantics is typically used when the interest lies in the outcome of computation, such as verifying the correctness of algorithms or functional equivalences between programs.

Original publication

LTL and CTL Applications for Smart Contracts Security

Georgii — Sat, 01 Feb 2025 02:54:51 +0000

Both LTL and CTL are fragments of propositional logic and parts of CTL*.

Linear Temporal Logic (LTL)

LTL is a modal temporal logic with modalities referring to time [1]. In the context of smart contracts, LTL can be used to specify and verify properties that must hold over the sequences of states that a contract might pass through.

For example, it allows developers to make assertions like, "If condition $X$ is $t r u e$ , then condition $Y$ will eventually be $t r u e$ " (expressed as $\implies \lozenge Y$ in LTL). This is particularly useful for smart contracts, which may need to guarantee certain outcomes after a sequence of events.

Imagine a smart contract that has a critical function to ensure that once a user deposits a certain amount of assets, they will eventually receive interest payments. With LTL, we could formally verify this property by expressing it as:

$G(\text{deposit} \implies F\text{ interest payment})$

This LTL formula states that it is globally $t r u e$ ( $G$ ) that if a deposit action occurs, it will be followed eventually ( $F$ ) by an interest payment. This kind of temporal logic allows developers and security analysts to prove that the smart contract will behave as intended over time.

LTL uses temporal operators to express logical statements about the future, such as:

$G$ (Globally): A condition must hold in all future states.
$F$ (Finally): A condition will eventually hold in some future state.
$X$ (neXt): A condition will hold in the next state.
$U$ (Until): A condition will hold until another condition holds.

Computation Tree Logic (CTL)

While LTL is linear and considers the flow of time as a single path, CTL allows for branching time, where multiple future possibilities can be considered from any given point [2]. CTL introduces path quantifiers to specify properties of computation trees — structures representing all possible executions of a system from any given state.

The two path quantifiers are:

$A$ (for All paths): Specifies that a property must hold on all possible future paths.
$E$ (there Exists a path): Specifies that there is at least one possible future path where a property holds.

CTL uses the same temporal operators as LTL, but prefixed with path quantifiers. So, you might see formulas like $A G$ (on all paths, globally) or $EF$ (there exists a path where finally).

For instance, a smart contract might have a function that only allows funds to be withdrawn by a specific party after a certain date. CTL can be used to validate this by expressing properties like "For all paths, if the withdrawal function is called, then for every possible continuation of that path, either the caller is the authorized party, and the date is correct, or the withdrawal fails."

In CTL, this could be expressed as:

$A[\text{withdraw} \implies (E[\text{caller} = \text{authorized} \land \text{date} \geq \text{specified}] \lor E[\text{transaction reverted}])]$

This states that along all paths ( $A$ ), if a withdrawal attempt occurs, there exists a path ( $E$ ) where either the caller is authorized and the date is on or after the specified date, or there exists a path where the transaction is reverted, ensuring funds can't be incorrectly withdrawn.

Keeping in mind: LTL synthesis and the problem of verification of games against an LTL winning condition is 2EXPTIME-complete [3].

We think these logics can be used to verify; hence, cover high-level logical scenarios for smart-contract as within a single transaction as in a sequence of blocks.

Of course, for such digital systems as smart contracts, design and modelling based on temporal logic should be done before the actual implementation. [The same is true of any other considered digital system]. This is a part of the Verification-Driven Development process [4] and to reduce the number of possible errors, it must be a predecessor of code.

References

Why use formal specification

Georgii — Sat, 25 Jan 2025 04:25:31 +0000

Why use formal specification

Imagine a programmer tasked with a challenge: to bring a Dutch auction to life through code. With an arsenal of skill and determination, they approach this journey, piecing together logic and functionality, guided by what feels right and what their experience dictates.

Once they reach a point where the digital auction seems ready to face the world, they step back, inviting testers into this creation to scrutinize his work, to ensure it behaves as intended. In this dance between creation and evaluation, both programmers and testers lean on a set of guidelines that are more akin to unwritten rules than formal commandments. This ambiguity can also open a door to endless interpretations, a breeding ground for misunderstandings.

Testers navigate through scenarios they believe will prove the auction’s readiness. Each discovery of a flaw sends the project into a loop of corrections, where solving one problem might unwittingly birth another, trapping them in a potentially endless cycle of tweaking.

Contrast this with a world where every stroke of the programmer’s keyboard is directed by a formal specification, a map that outlines the operational semantics of the program with precision. In this realm, the programmer’s role transforms into one of diligent adherence, ensuring each line of code aligns with the predefined semantics, sculpting the auction into its ideal form.

The tester’s role, too, shifts focus — now, they must verify that the real-world behaviour of the code, shaped by the interplay between compiler, operating system, and beyond, truly matches those expectations laid out in the specification. This narrative isn’t just about building and testing software; it’s about navigating the accurate balance between creativity and conformity, between the freedom of interpretation and the clarity of specification.

It’s a journey through the complexities of bringing a concept to life, where each decision can lead to success or endless revision, and the path chosen can make all the difference.

You can read about the software development based on the specification/verification, or as we call it Verification Driven Development presented as a mathematical formalism in our post.