**Proposition 4.2.6.** Suppose $\Gamma \vdash e : s$ and $\sigma$ is a substitution adequate for $\Gamma$ compatible with $e$. Then $\Gamma \vdash e\sigma : s$. The property holds analogously for well-formed arguments.

*Proof.* This is proved by induction on the derivation of $\Gamma \vdash e : s$. We treat the variable, application and universal quantification case. All the other cases are trivial or analogous.

If the last rule is VAR then $e = x$, $s = \Gamma(x)$ and $e\sigma = \sigma(x)$. We have $\Gamma \vdash \sigma(x) : \Gamma(x)$ by assumption, which is exactly the same as $\Gamma \vdash e\sigma : s$.

If the last rule is APP then we have $e = K(f_1, \dots, f_n)$ with $\Gamma \vdash f_i : \tau_i$ for all $i$ and $\Sigma(K) = \tau_1 \times \dots \times \tau_n \to s$. According to the induction hypothesis, $\Gamma \vdash f_i\sigma : \tau_i$ for all $i$. Therefore

$$ \frac{\Sigma(K) = \tau_1 \times \dots \times \tau_n \to s \qquad \Gamma \vdash f_i\sigma : \tau_i}{\Gamma \vdash K(f_1\sigma, \dots, f_n\sigma) : s} \text{APP} $$

But $e\sigma = K(f_1\sigma, \dots, f_n\sigma)$ so the result is proved.

If the last rule is FORALL then $e = \forall x^s : e' \text{ with } \Gamma, x : s \vdash e' : o$. Clearly, $\sigma^x$ is an adequate substitution for $\Gamma, x : s$. Therefore, according to the induction hypothesis, $\Gamma, x : s \vdash e'\sigma^x : o$. Then

$$ \frac{\Gamma, x : s \vdash e'\sigma^x : o}{\Gamma \vdash \forall x^s : e'\sigma^x : o} \text{FORALL} $$

The result is obtained by $e\sigma = (\forall x^s : e'\sigma^x)$.

□

## Semantics

Compared to $\mathcal{L}$ and its unsorted semantics, $\mathcal{L}^s$ assigns a domain of evaluation for every sort and type. Formulas are always evaluated in the Boolean domain; sort annotations restrict the domain of evaluation of bound variables.

**Definition 4.2.7 (Evaluation).** Let $S$ be a collection of sorts. We define $D_o$ as the two-valued collection whose elements are the Boolean values $\top$ and $\bot$. Given a family of collections $(D_s)_{s \in S}$, we associate a domain to every type in the natural way:

$$ D_{\tau_1 \times \dots \times \tau_n \to s} \triangleq D_{\tau_1} \times \dots \times D_{\tau_n} \to D_s $$

Let $\Sigma$ be some signature. An interpretation $I$ consists of two families $(D_s)_{s \in S}$ and $(K^I)_{K \in \text{Dom}(\Sigma)}$ such that $K^I \in D_{\Sigma(K)}$ for all $K$. Let $\Gamma$ be a typing context. A valuation $\theta$ is a function from $\text{Dom}(\Gamma)$ such that $\theta(x) \in D_{\Gamma(x)}$ for all $x$. The evaluation of expressions and
arguments is defined by

$$ \llbracket x \rrbracket_{\theta}^{I} \triangleq \theta(x) \\ \llbracket K(f_1, \dots, f_n) \rrbracket_{\theta}^{I} \triangleq K^{I}(\llbracket f_1 \rrbracket_{\theta}^{I}, \dots, \llbracket f_n \rrbracket_{\theta}^{I}) $$

$$ \llbracket e_1 = e_2 \rrbracket_{\theta}^{I} \triangleq \left\{ \begin{array}{ll} \top & \text{if } \llbracket e_1 \rrbracket_{\theta}^{I} = \llbracket e_2 \rrbracket_{\theta}^{I} \\ \bot & \text{otherwise} \end{array} \right. $$

$$ \llbracket \text{FALSE} \rrbracket_{\theta}^{I} \triangleq \bot $$

$$ \llbracket e_1 \Rightarrow e_2 \rrbracket_{\theta}^{I} \triangleq \left\{ \begin{array}{ll} \top & \text{if } \llbracket e_1 \rrbracket_{\theta}^{I} = \bot \text{ or } \llbracket e_2 \rrbracket_{\theta}^{I} = \top \\ \bot & \text{otherwise} \end{array} \right. $$

$$ \llbracket \forall x^s : e \rrbracket_{\theta}^{I} \triangleq \left\{ \begin{array}{ll} \top & \text{if } \llbracket e \rrbracket_{\theta^x}^{I} = \top \text{ for all } v \text{ in } D_s \\ \bot & \text{otherwise} \end{array} \right. $$

For all $v_1 \in D_{s_1}, \dots, v_n \in D_{s_n}$:

$$ \llbracket K \rrbracket_{\theta}^{I}(v_1, \dots, v_n) \triangleq K^{I}(v_1, \dots, v_n) \quad \text{where } \Sigma(k) = s_1 \times \dots \times s_n \to s $$

$$ \llbracket \lambda x_1^{s_1}, \dots, x_n^{s_n} : e \rrbracket_{\theta}^{I} (v_1, \dots, v_n) \triangleq \llbracket e \rrbracket_{\theta^{x_1, \dots, x_n}}^{I} $$

We admit the following result, which can be proved by induction on the structure of typing derivations:

**Proposition 4.2.8.** Let $\Gamma$ be a typing context, $I$ an interpretation and $\theta$ a valuation. We have the following properties:

* For all $e$ and $s$, if $\Gamma \vdash e : s$ then $\llbracket e \rrbracket_{\theta}^{I} \in D_s$

* For all $f$ and $\tau$, if $\Gamma \vdash f : \tau$ then $\llbracket f \rrbracket_{\theta}^{I} \in D_{\tau}$

We proved (Proposition 4.2.6) that substitutions preserve typing. It follows that if $\Gamma \vdash e : s$ and $\sigma$ is a substitution then $\llbracket e\sigma \rrbracket_{\theta}^{I} \in D_s$. However, we admit the following stronger property on the evaluation of $e\sigma$:

**Proposition 4.2.9.** Let $\Gamma$, $I$ and $\theta$ as in the previous proposition. Let $\sigma$ be a substitution adequate for $\Gamma$. We define $\sigma\theta$ as a valuation for $\Gamma$ by

$$ (\sigma\theta)(x) \triangleq \llbracket \sigma(x) \rrbracket_{\theta}^{I} $$

It follows from the definition of a substitution for $\Gamma$ and Proposition 4.2.8 that $\sigma\theta$ is well-defined. The following equations hold for all $e$ and $f$ well-typed in $\Gamma$:

$$ \llbracket e\sigma \rrbracket_{\theta}^{I} = \llbracket e \rrbracket_{\sigma\theta}^{I} $$

$$ \llbracket f\sigma \rrbracket_{\theta}^{I} = \llbracket f \rrbracket_{\sigma\theta}^{I} $$

Typing contexts carry the necessary typing information for the free variables of all expressions. It is clear then that annotations $x : s$ for variables $x$ that do not occur free may be omitted. In particular, well-typed closed expressions can be typed in the empty context.
The letter $\phi$ denotes well-typed formulas. The satisfaction relation $|=$ for $\mathcal{L}^s$ is defined for closed formulas by

$$I \models \phi \text{ iff } [[\phi]]^I = \top$$

We define the notations $T \models \phi$ and $| = \phi$ as before, where $T$ is a collection of closed formulas.

The language and semantics of TLAPS sequents $\Gamma \vdash e$ are extended too. Let us briefly indicate how the definitions may be adapted. In $\Gamma$, the shape specifications that annotate declarations are replaced by type specifications; we write NEW $K : \tau$ for the declaration of $K$ with type $\tau$, where ord($\tau$) ≤ 1. It follows that the signature induced by a sequent context is a signature of $\mathcal{L}^s$, as it maps operator symbols to types. The hypotheses in $\Gamma$ must be formulas or well-formed nested sequents. The goal must be a formula as well.

## 4.3 Recovering Formulas

Let $\mathcal{L}^t$ be the version of $\mathcal{L}^s$ for which $S$ is reduced to one sort symbol, noted $\iota$. A term is an expression $e : \iota$. We describe a sound and complete encoding of $\mathcal{L}$ into $\mathcal{L}^t$. We start with an elementary version of the encoding that systematically assigns types over the sort $\iota$ to all operators. For many TLA⁺ primitive operators, it is desirable to use types with $o$; for example, $\epsilon$ should be assigned a predicate type. We consider this feature as an extension and introduce it in the last section.

Before we start, let us give the basic intuition behind the encoding. All operators are assigned types corresponding to their original shapes, for instance the shape (1, 0) is mapped to the type ($\iota \to \iota$) $\times \iota \to \iota$. All variables are annotated with $\iota$. If we attempt to translate expressions from $\mathcal{L}$ to $\mathcal{L}^t$ directly in the most natural way, we will encounter two kinds of type errors:

TRUE $\in$ BOOLEAN

FALSE $\Rightarrow$ 42

TRUE is a formula, but $\epsilon$ expects a term

42 is a term, but $\Rightarrow$ expects a formula

It suffices to rewrite the subexpressions causing those errors. The first kind is simpler to address. We add a new primitive operator $\mathbf{cast}_o : o \to \iota$ and rewrite:

$$\mathbf{cast}_o(\mathbf{TRUE}) \in \mathbf{BOOLEAN}$$

The second kind is trickier, as it seems counter-intuitive that any term could be translated as a formula in a sound way. However, we only need to convert terms when a formula is expected. This translation is sound:

$$\mathbf{FALSE} \Rightarrow (42 = \mathbf{cast}_o(\mathbf{TRUE}))$$

That conversion formalizes the intuition that the original TLA⁺ formula is equivalent to $\mathbf{FALSE} \Rightarrow (42 = \mathbf{TRUE})$ under the liberal interpretation of Boolean connectives. It suffices to use $\mathbf{cast}_o$ on $\mathbf{TRUE}$ to make the expression well-typed.

**Example 4.3.1.** Here is a simple valid example that illustrates both conversions:

$$\forall x : x = \mathbf{FALSE} \Rightarrow \neg x \quad \text{is encoded as}$$

$$\forall x^t : x = \mathbf{cast}_o(\mathbf{FALSE}) \Rightarrow \neg(x = \mathbf{cast}_o(\mathbf{TRUE}))$$

Note that restricting quantification to $o$ would not be sound in general: consider the non valid TLA⁺ expression $\forall x : x = \mathbf{TRUE} \lor x = \mathbf{FALSE}$, which becomes a valid formula of $\mathcal{L}^t$ if we translate it as $\forall x^o : x = \mathbf{TRUE} \lor x = \mathbf{FALSE}$. The encoding we consider here will always annotate quantifiers with $\iota$.
**4.3.1 Definition**

We define three mappings $\mathcal{B}^i$, $\mathcal{B}^o$ and $\mathcal{B}^{op}$. The first two are applied to expressions, the last one is applied to arguments. Before we define the mappings themselves, we define a mapping $\Sigma \mapsto \Sigma^B$ that maps signatures of $\mathcal{L}$ to signatures of $\mathcal{L}^i$.

**Definition 4.3.2.** For all $n > 0$, let $i^n \to i$ denote the $n$-ary type $i \times \cdots \times i \to i$. The 0-ary type $i^0 \to i$ is just the sort $i$. For all TLA$^+$ shape $\kappa = (n_1, \dots, n_k)$, the type $\text{type}(\kappa)$ is defined as $\tau_1 \times \cdots \times \tau_k \to i$ where $\tau_i$ is the $n_i$-ary type.

Let $\Sigma$ be a TLA$^+$ signature. We define $\Sigma^B$ as the signature of $\mathcal{L}^i$ whose domain is $\text{Dom}(\Sigma)$ plus the fresh symbol $\text{cast}_o$. If $K \in \text{Dom}(\Sigma)$, then $\Sigma^B(K) \triangleq \text{type}(\Sigma(K))$. $\Sigma^B(\text{cast}_o) \triangleq o \to i$.

For example, the TLA$^+$ operator `setst` (set comprehension) has the shape `(0,1)`. Its corresponding type in $\Sigma^B$ is $i \times (i \to i) \to i$. Note that for a $\Sigma$-interpretation and a $\Sigma^B$-interpretation on the same domain $D$, if $K \in \text{Dom}(\Sigma)$ then $K$ is interpreted as a function of the collection $D \times (D \to D) \to D$ in both logics.

**Definition 4.3.3 (Mappings).** The three mappings $\mathcal{B}^i$, $\mathcal{B}^o$ and $\mathcal{B}^{op}$ are defined recursively by the following rules:

$$
\begin{align*}
\mathcal{B}^o(e_1 = e_2) &\triangleq \mathcal{B}^t(e_1) = \mathcal{B}^t(e_2) & \mathcal{B}^t(x) &\triangleq x \\
\mathcal{B}^o(\text{FALSE}) &\triangleq \text{FALSE} & \mathcal{B}^t(K(f_1, \dots, f_n)) &\triangleq K(\mathcal{B}^{op}(f_1), \dots, \mathcal{B}^{op}(f_n)) \\
\mathcal{B}^o(e_1 \Rightarrow e_2) &\triangleq \mathcal{B}^o(e_1) \Rightarrow \mathcal{B}^o(e_2) & \mathcal{B}^t(e) &\triangleq \text{cast}_o(\mathcal{B}^o(e)) \tag{\star} \\
\mathcal{B}^o(\forall x : e) &\triangleq \forall x^t : \mathcal{B}^o(e) & & \\
\mathcal{B}^o(e) &\triangleq \mathcal{B}^t(e) = \text{cast}_o(\text{TRUE}) \tag{\star} & \mathcal{B}^{op}(e) &\triangleq \mathcal{B}^t(e) \\
& & \mathcal{B}^{op}(K) &\triangleq K \tag{\star\star} \\
& & \mathcal{B}^{op}(\lambda x_1, \dots, x_n : e) &\triangleq \lambda x_1, \dots, x_n : \mathcal{B}^t(e)
\end{align*}
$$

The recursive definition above is not inductive, because the two conversion rules are not applied on a subexpression of the original expression. However, consider the last case of $\mathcal{B}^o(e)$, in which $\mathcal{B}^o(e)$ is defined as $\mathcal{B}^t(e) = \text{cast}_o(\text{TRUE})$. Then $e$ is necessarily a variable or an application (otherwise, some non-conversion rule would apply to construct $\mathcal{B}^o(e)$). In that case, there is a non-conversion rule that applies to construct $\mathcal{B}^t(e)$. A similar argument can be made for the case where $\mathcal{B}^t(e)$ is constructed by converting $\mathcal{B}^o(e)$ into a term. This proves that a conversion can never immediately follow another in the recursive construction of $\mathcal{B}^t(e)$ and $\mathcal{B}^o(e)$, and so the recursive definition above is well-founded.

This also justifies proofs by induction on the construction of $\mathcal{B}^t(e)$, $\mathcal{B}^o(e)$ and $\mathcal{B}^{op}(f)$. To illustrate, we detail the proof of the next theorem.

**Theorem 4.3.4.** If $e$ is an expression of $\mathcal{L}$, we note $\Gamma_e$ the typing context whose domain is $\text{FV}(e)$ and such that $\Gamma_e(x) = i$ for all $x$ free in $e$. The context $\Gamma_f$ is defined analogously for all arguments $f$.

For all $\Sigma$-expression $e$ and $\Sigma$-argument $f$ with arity $n$, the following properties hold:

<footnote>(\star) We call these rules *conversions*. They are applied with lowest priority.</footnote>

<footnote>(\star\star) Only applies when $K$ is first-order. For constants, the rule just above applies.</footnote>
(i) $\Gamma_e \vdash \mathcal{B}^t(e) : \iota$

(ii) $\Gamma_e \vdash \mathcal{B}^o(e) : o$

(iii) $\Gamma_f \vdash \mathcal{B}^{op}(f) : \iota^n \to \iota$

*Proof.* The proof is by induction on the construction of $\mathcal{B}^t(e)$, $\mathcal{B}^o(e)$ and $\mathcal{B}^{op}(f)$. There is one case for each equation in Definition 4.3.3. Depending on the term being constructed, we prove only i, ii or iii.

**Variable** Let $e = x$ and $\mathcal{B}^t(e) = x$. $\Gamma_e(x) = \iota$ by definition of $\Gamma_e$, thus $\Gamma_e \vdash x : \iota$ by application of the typing rule VAR.

**Application** Let $e = K(f_1, \dots, f_p)$ and $\mathcal{B}^t(e) = K(\mathcal{B}^{op}(f_1), \dots, \mathcal{B}^{op}(f_p))$. The induction hypothesis (property iii) states that $\Gamma_{f_i} \vdash \mathcal{B}^{op}(f_i) : \iota^n \to \iota$ where $n$ is the arity of $f_i$.

Let $f'_i = \mathcal{B}^{op}(f_i)$. Then we must prove $\Gamma_e \vdash K(f'_1, \dots, f'_p) : \iota$. Let $\Sigma(K) = (n_1, \dots, n_p)$. By assumption, $e$ is a well-formed application, so each $f_i$ is $n_i$-ary. Moreover, it is clear that $\Gamma_{f_i} \subseteq \Gamma_e$. Therefore, according to the induction hypothesis, for all $i$ we have $\Gamma_e \vdash f'_i : \iota^{n_i} \to \iota$. By definition, $\Sigma^\mathcal{B}(K) = \tau_1 \times \dots \times \tau_n \to \iota$ where $\tau_i = \iota^{n_i} \to \iota$. Then the following derivation is valid:

$$ \frac{\Sigma^{\mathcal{B}}(K) = \tau_1 \times \dots \times \tau_n \to \iota \qquad \Gamma_e \vdash f'_i : \tau_i}{\Gamma_e \vdash K(f'_1, \dots, f'_p) : \iota} \qquad \text{APP} $$

**Formula-to-term conversion** Let $\mathcal{B}^t(e) = \text{cast}_o(\mathcal{B}^o(e))$. The induction hypothesis (property ii) states that $\Gamma_e \vdash \mathcal{B}^o(e) : o$. The result is obtained by the derivation

$$ \frac{\Sigma^{\mathcal{B}}(\text{cast}_o) = o \to \iota \qquad \Gamma_e \vdash \mathcal{B}^o(e) : o}{\Gamma_e \vdash \text{cast}_o(\mathcal{B}^o(e)) : \iota} \qquad \text{APP} $$

**Equality** Let $e$ be $e_1 = e_2$. The induction hypothesis (property i) states $\Gamma_{e_1} \vdash \mathcal{B}^t(e_1) : \iota$ and $\Gamma_{e_2} \vdash \mathcal{B}^t(e_2) : \iota$. The result $\Gamma_e \vdash \mathcal{B}^t(e_1) = \mathcal{B}^t(e_2) : o$ is immediate by $\Gamma_{e_i} \subseteq \Gamma_e$ ($i \in \{1, 2\}$) and using the typing rule EQ.

**False** Let $e = \text{FALSE}$. The result $\vdash \mathcal{B}^o(e) : o$ is immediate by $\mathcal{B}^o(e) = \text{FALSE}$.

**Implication** Let $e$ be $e_1 \Rightarrow e_2$. The induction hypothesis (property ii) states that $\Gamma_{e_1} \vdash \mathcal{B}^o(e_1) : o$ and $\Gamma_{e_2} \vdash \mathcal{B}^o(e_2) : o$. The result $\Gamma_e \vdash \mathcal{B}^o(e_1) \Rightarrow \mathcal{B}^o(e_2) : o$ is immediate by $\Gamma_{e_i} \subseteq \Gamma_e$ ($i \in \{1, 2\}$) and using the typing rule IMP.

**Universal quantification** Let $e$ be $\forall x : e'$. The induction hypothesis (property ii) states that $\Gamma_{e'} \vdash \mathcal{B}^o(e') : o$. Clearly, $\Gamma_{e'} \subseteq \Gamma_e, x : \iota$ (the free variables of $e'$ are among $x$ and the free variables of $e$). Then $\Gamma_e \vdash (\forall x' : \mathcal{B}^o(e')) : o$ by application of the rule FORALL.

**Term-to-formula conversion** Let $\mathcal{B}^o(e)$ be $\mathcal{B}^t(e) = \text{cast}_o(\text{TRUE})$. The induction hypothesis (property i) states that $\Gamma_e \vdash \mathcal{B}^t(e) : \iota$. The result is obtained by the derivation

$$ \frac{\Gamma_e \vdash \mathcal{B}^t(e) : \iota \qquad \frac{\Sigma^{\mathcal{B}}(\text{cast}_o) = o \to \iota \qquad \Gamma_e \vdash \text{TRUE} : o}{\Gamma_e \vdash \text{cast}_o(\text{TRUE}) : \iota} \qquad \text{APP}}{\Gamma_e \vdash \mathcal{B}^t(e) = \text{cast}_o(\text{TRUE}) : o} \qquad \text{EQ} $$
**Argument (expression)** We have $\Gamma_e \vdash \mathcal{B}^i(e) : \iota$ by the induction hypothesis (property i). Then $\Gamma_e \vdash \mathcal{B}^{op}(e) : i^0 \to i$ by $\mathcal{B}^{op}(e) = \mathcal{B}^i(e)$ and $i^0 \to i = i$.

**Argument (operator symbol)** Let $K$ be a first-order operator with arity $n > 0$. By definition, $\Sigma^\mathcal{B}(K) = i^n \to \iota$ and then $\mathrm{ord}(\Sigma^\mathcal{B}(K)) = 1$. The result $\vdash K : i^n \to \iota$ is obtained by the rule OPARG.

**Argument (lambda-expression)** Let $f = \lambda x_1, \dots, x_n : e$ and $\mathcal{B}^{op}(f) = \lambda x_1^i, \dots, x_n^i : \mathcal{B}^i(e)$. The induction hypothesis (property i) states that $\Gamma_e \vdash \mathcal{B}^i(e) : \iota$. It is clear that $\Gamma_e \subseteq \Gamma_f, x_1 : \iota, \dots, x_n : \iota$. Then $\Gamma_f \vdash \lambda x_1^i, \dots, x_n^i : \mathcal{B}^i(e) : i^n \to \iota$ by application of LAMARG.

□

### 4.3.2 Correctness

The encoding is defined by $\mathcal{B}^o$, which maps $\Sigma$-expressions of $\mathcal{L}$ to $\Sigma^\mathcal{B}$-expressions of $\mathcal{L}^i$. The soundness property states that the validity of $\mathcal{B}^o(e)$ entails the validity of $e$. The dual implication is completeness. Both properties are derived as corollaries of a result about the preservation of all values by $\mathcal{B}^i$, $\mathcal{B}^o$ and $\mathcal{B}^{op}$. For completeness, we also need to specify the operator cast$_o$ in the target logic.

#### Soundness

We map $\Sigma$-interpretations to $\Sigma^\mathcal{B}$-interpretations in the natural way.

**Definition 4.3.5.** Let $I$ be a $\Sigma$-interpretation with domain $D$. The $\Sigma^\mathcal{B}$-interpretation $I^\mathcal{B}$ is defined as follows:

* $D_i \triangleq D$;

* For all $K \in \mathrm{Dom}(\Sigma)$, $K^{I^\mathcal{B}} \triangleq K^I$. This is correct because $D_{\Sigma^\mathcal{B}(K)}$ equals $D_{\Sigma(K)}$;

* $\mathrm{cast}_o^{I^\mathcal{B}}$ is the function $\{\top \mapsto \top^D, \bot \mapsto \bot^D\}$.

$I^\mathcal{B}$ essentially provides the interpretation for the new operator cast$_o$, which maps the truth values of $D_o$ to their counterparts in $D_i = D$.

By Theorem 4.3.4, for all expressions $e$, $\mathcal{B}^i(e)$ and $\mathcal{B}^o(e)$ are well-formed in the context $\Gamma_e$, and their respective sorts are $i$ and $o$. Consider a TLA$^+$ valuation $\theta$ for the logic $\mathcal{L}$. $\theta$ interprets variables as elements of $D$. Since $\Gamma_e(x) = i$ for all $x$ and $D_i = D$, $\theta$ is an adequate valuation for the context $\Gamma_e$, and the values $[\mathcal{B}^i(e)]_{\theta}^{I^\mathcal{B}}$ and $[\mathcal{B}^o(e)]_{\theta}^{I^\mathcal{B}}$ are well-defined respectively as elements of $D$ and $D_o$. Likewise, for all $n$-ary $f$ then $[\mathcal{B}^{op}(f)]_{\theta}^{I^\mathcal{B}}$ is well-defined as an element of $D^n \to D$ (or simply $D$ if $n = 0$).

**Theorem 4.3.6.** Let $\Sigma$ be a TLA$^+$ signature and $I$ a $\Sigma$-interpretation. For all valuations $\theta$, expression $e$ and argument $f$, we have the properties:

$$ (i) \quad [\mathcal{B}^i(e)]_{\theta}^{I^\mathcal{B}} = [e]_{\theta}^{I} $$

$$ (ii.a) \quad [\mathcal{B}^o(e)]_{\theta}^{I^\mathcal{B}} = \top \iff [e]_{\theta}^{I} = \top^D $$
(ii.b) $[[\mathcal{B}^o(e)]]_\theta^{IB} = \perp$ implies $[[e]]_\theta^I = \perp^D$ when $\mathcal{B}^o(e)$ is not obtained by conversion

$$ (iii) \quad [[\mathcal{B}^{op}(f)]]_{\theta}^{IB} = [[f]]_{\theta}^{I} $$

*Proof.* The result is proved by induction on the construction of $\mathcal{B}^t(e)$, $\mathcal{B}^o(e)$ or $\mathcal{B}^{op}(f)$. For cases constructing $\mathcal{B}^t(e)$, we prove $i$. For cases constructing $\mathcal{B}^o(e)$, we prove ii.a and ii.b. For cases constructing $\mathcal{B}^{op}(f)$, we prove iii.

For all cases constructing $\mathcal{B}^o(e)$ except the case of term-to-formula conversion, ii.a entails ii.b immediately. That is because, in all those cases, $e$ has a Boolean top connective, and the semantics of $\mathcal{L}$ is made in such a way that $[[e]]_\theta^I \neq \top^D$ implies $[[e]]_\theta^I = \perp^D$ for such $e$.

**Variable** The result is immediate since $\mathcal{B}^t(x)$ is $x$. Both values equal $\theta(x)$.

**Application** The result is also immediate since $K^{IB} = K^I$ and using the induction hypothesis to derive $[[\mathcal{B}^{op}(f_i)]]_\theta^{IB} = [[f_i]]_\theta^I$ for all arguments.

**Formula-to-term conversion** We have $\mathcal{B}^t(e) = \mathrm{cast}_o(\mathcal{B}^o(e))$. By construction, $\mathcal{B}^o(e)$ is not a term-to-formula conversion, because a conversion cannot be applied immediately after another. Therefore, according to the induction hypothesis, both ii.a and ii.b hold for $\mathcal{B}^o(e)$.

$$
\begin{align*}
[[\mathcal{B}^t(e)]]_{\theta}^{IB} &= [[\mathrm{cast}_o(\mathcal{B}^o(e))]_{\theta}^{IB} \\
&= \mathrm{cast}_o^{IB}([\mathcal{B}^o(e)]_{\theta}^{IB}) \\
&= \left\{ \begin{array}{ll} \top^D & \text{if } [[\mathcal{B}^o(e)]_{\theta}^{IB} = \top \\ \perp^D & \text{if } [[\mathcal{B}^o(e)]_{\theta}^{IB} = \perp \end{array} \right. \tag*{(by definition)} \\
&= \left\{ \begin{array}{ll} \top^D & \text{if } [[e]]_{\theta}^I = \top^D \\ \perp^D & \text{if } [[e]]_{\theta}^I = \perp^D \end{array} \right. \tag*{(induction hypothesis)} \\
&= [[e]]_{\theta}^I
\end{align*}
$$

### Equality

$$
\begin{align*}
[[\mathcal{B}^o(e_1 = e_2)]]_{\theta}^{IB} &= \top \quad \text{iff} \quad [[\mathcal{B}^t(e_1) = \mathcal{B}^t(e_2)]]_{\theta}^{IB} = \top \\
&\quad \text{iff} \quad [[\mathcal{B}^t(e_1)]]_{\theta}^{IB} = [[\mathcal{B}^t(e_2)]]^{IB} \\
&\quad \text{iff} \quad [[e_1]]_{\theta}^{I} = [[e_2]]_{\theta}^{I} \tag*{(induction hypothesis)} \\
&\quad \text{iff} \quad [[e_1 = e_2]]_{\theta}^{I} = \top^D
\end{align*}
$$

**False** The result is immediate: $[[\mathcal{B}^o(\mathrm{FALSE})]]_\theta^{IB} = \perp$ and $[[\mathrm{FALSE}]_\theta^I = \perp^D$

### Implication

$$
\begin{align*}
[[\mathcal{B}^o(e_1 \Rightarrow e_2)]]_{\theta}^{IB} &= \top \quad \text{iff} \quad [[\mathcal{B}^o(e_1) \Rightarrow \mathcal{B}^o(e_2)]]_{\theta}^{IB} = \top \\
&\quad \text{iff} \quad [[\mathcal{B}^o(e_1)]]_{\theta}^{IB} \neq \top \quad \text{or} \quad [[\mathcal{B}^o(e_2)]]_{\theta}^{IB} = \top \\
&\quad \text{iff} \quad [[e_1]]_{\theta}^{I} \neq \top^D \quad \text{or} \quad [[e_2]]_{\theta}^{I} = \top^D \tag*{(induction hypothesis)} \\
&\quad \text{iff} \quad [[e_1 \Rightarrow e_2]]_{\theta}^{I} = \top^D
\end{align*}
$$

Remark that only property ii.a of the induction hypothesis is needed.
**Universal quantification**

$$ 
\begin{align*}
\llbracket \mathcal{B}^o (\forall x : e) \rrbracket_{\theta}^{I^B} &= \top \quad \text{iff} \quad \llbracket \forall x : \mathcal{B}^o (e) \rrbracket_{\theta}^{I^B} = \top \\
&\quad \text{iff} \quad \llbracket \mathcal{B}^o (e) \rrbracket_{\theta_x}^{I^B} = \top \quad \text{for all } v \text{ in } D \\
&\quad \text{iff} \quad \llbracket e \rrbracket_{\theta_x}^{I} = \top^D \quad \text{for all } v \text{ in } D \quad \text{(induction hypothesis)} \\
&\quad \text{iff} \quad \llbracket \forall x : e \rrbracket_{\theta}^{I} = \top^D
\end{align*}
$$

**Term-to-formula conversion**

$$ 
\begin{align*}
\llbracket \mathcal{B}^t (e) = \text{cast}_o (\text{TRUE}) \rrbracket_{\theta}^{I^B} &= \top \quad \text{iff} \quad \llbracket \mathcal{B}^t (e) \rrbracket_{\theta}^{I^B} = \top^D \\
&\quad \text{iff} \quad \llbracket e \rrbracket_{\theta}^{I} = \top^D \quad \text{(induction hypothesis)}
\end{align*}
$$

**Argument (expression)** If $f$ is just an expression $e$ then the result is immediate by $i$.

**Argument (operator symbol)** If $f$ is some $K$ then the result is immediate from $K^{I^B} = K^I$

**Argument (lambda-expression)** If $f$ is $\lambda x_1, \dots, x_n : e$ then we have, for all $v_1, \dots, v_n$:

$$ 
\begin{align*}
\llbracket \mathcal{B}^{op} (f) \rrbracket_{\theta}^{I^B} (v_1, \dots, v_n) &= \llbracket \lambda x_1, \dots, x_n : \mathcal{B}^t (e) \rrbracket_{\theta}^{I^B} (v_1, \dots, v_n) \\
&= \llbracket \mathcal{B}^t (e) \rrbracket_{\theta_{v_1, \dots, v_n}}^{I^B} \\
&= \llbracket e \rrbracket_{\theta_{v_1, \dots, v_n}}^{I} \tag*{(induction hypothesis)} \\
&= \llbracket \lambda x_1, \dots, x_n : e \rrbracket_{\theta}^{I} (v_1, \dots, v_n) \\
&= \llbracket f \rrbracket_{\theta}^{I} (v_1, \dots, v_n)
\end{align*}
$$

$$ \text{Thus } \llbracket \mathcal{B}^{op} (f) \rrbracket_{\theta}^{I^B} = \llbracket f \rrbracket_{\theta}^{I}. $$

□

**Corollary 4.3.7 (Soundness).** Let $e$ be a closed expression of $\mathcal{L}$. If $\mathcal{B}^o (e)$ is valid then $e$ is also valid.

*Proof.* Let $I$ be a $\Sigma$-interpretation. By assumption, $I^B \models \mathcal{B}^o (e)$, i.e. $\llbracket \mathcal{B}^o (e) \rrbracket^{I^B} = \top$. By Theorem 4.3.6, $\llbracket e \rrbracket^{I} = \top^D$, i.e. $I \models e$. Therefore $e$ is valid. □

**Completeness**

Completeness is the fact that $\mathcal{B}^o$ preserves validity from $\mathcal{L}$ to $\mathcal{L}^t$. It is dual to soundness, which states that $\mathcal{B}^o (e)$'s validity implies $e$'s validity. We proved soundness as a corollary of Theorem 4.3.6 by using only the implication $\Rightarrow$ from case (ii.a). We may derive completeness by using the other direction $\Leftarrow$.

However, it may be the case that $I^B \models \mathcal{B}^o (e)$ for all $I$, but $J \not\models \mathcal{B}^o (e)$ for some $J$. The TLA$^+$ valid formula $\text{TRUE} \neq \text{FALSE}$ is encoded as $\text{cast}_o (\text{TRUE}) \neq \text{cast}_o (\text{FALSE})$, but the latter formula is not valid in $\mathcal{L}^t$, because there are interpretations $J$ such that $\text{cast}_o^I$ is not injective (any interpretation where $D$ is reduced to one element suffices). To ensure completeness, we must put a constraint on the interpretation of $\text{cast}_o$ in the target logic.
**Lemma 4.3.8.** Consider the axiom

$$ \mathit{cast}_o(\mathit{TRUE}) \neq \mathit{cast}_o(\mathit{FALSE}) \qquad (B) $$

The mapping $I \mapsto I^B$ is surjective as a mapping of $\Sigma$-interpretations to $\Sigma^B$-interpretations satisfying the axiom (B).

*Proof.* Every $I^B$ satisfies (B) by definition of $\mathit{cast}_o^I$, so the mapping is well-defined.

Let $J$ be a $\Sigma^B$-interpretation satisfying (B). The axiom implies that $\llbracket \mathit{cast}_o(\mathit{TRUE}) \rrbracket^J$ and $\llbracket \mathit{cast}_o(\mathit{FALSE}) \rrbracket^J$ are two distinct values in $D$. Thus $D$ is an adequate domain for TLA⁺. We let $\top^D \triangleq \llbracket \mathit{cast}_o(\mathit{TRUE}) \rrbracket^J$ and $\bot^D \triangleq \llbracket \mathit{cast}_o(\mathit{FALSE}) \rrbracket^J$. We then define the $\Sigma$-interpretation $I$ as the restriction of $J$ to $\Sigma$. It is then easily verified that $I^B = J$. Therefore $I \mapsto I^B$ is surjective. $\square$

**Corollary 4.3.9 (Completeness).** Let $e$ be a closed expression of $\mathcal{L}$. If $e$ is valid then $\mathcal{B}^o(e)$ is valid for the class of interpretations that satisfy (B).

*Proof.* Suppose $e$ is valid. Let $J$ be a $\Sigma^B$-interpretation. By Lemma 4.3.8, there is an $I$ such that $J = I^B$. By assumption, $I \models e$, i.e. $\llbracket e \rrbracket^I = \top^D$. By Theorem 4.3.6, $\llbracket \mathcal{B}^o(e) \rrbracket^J = \top$. Therefore, $\mathcal{B}^o(e)$ is valid. $\square$

### 4.3.3 Predicate Types

$\mathcal{B}^o$ can be applied to TLA⁺'s theory $T$, resulting in a new theory $T'$ in the target logic $\mathcal{L}^t$. However, because the mapping $\mathcal{B}^o$ described so far preserves all operator types with $t$, the resulting theory would not feature any predicate or other operator involving Booleans. For instance, applying $\mathcal{B}^o$ to the schema of set comprehension results in

$$ \begin{array}{l} \mathit{in} : t \times t \rightarrow t \\ \mathit{setst} : t \times (t \rightarrow t) \rightarrow t \\ \forall a^t, x^t : \mathit{in}(x, \mathit{setst}(a, P)) = \mathit{cast}_o(\mathit{TRUE}) \Leftrightarrow \mathit{in}(x, a) = \mathit{cast}_o(\mathit{TRUE}) \wedge P(x) = \mathit{cast}_o(\mathit{TRUE}) \\ \qquad \text{for all } P : t \rightarrow t \end{array} $$

Our implementation actually assigns types with $o$ to some TLA⁺ primitives and defines axioms in $T'$ closer to what one would expect:

$$ \begin{array}{l} \mathit{in} : t \times t \rightarrow o \\ \mathit{setst} : t \times (t \rightarrow o) \rightarrow t \\ \forall a^t, x^t : \mathit{in}(x, \mathit{setst}(a, P)) \Leftrightarrow \mathit{in}(x, a) \wedge P(x) \quad \text{for all } P : t \rightarrow o \end{array} $$

This optimization is justified by the semantics of in and setst. We present the arguments for assigning those types to in and setst below. The arguments for in also apply to the subset relation and the comparison operators, which are encoded as predicates. The arguments for set comprehension apply to the choose operator, which expects a predicate argument in the target logic.

The signature $\Sigma^B$ is modified so that $\Sigma^B(\mathit{in}) = t \times t \rightarrow o$, and the definitions of $\mathcal{B}^o$ and $\mathcal{B}^t$ are adapted:

$$ \mathcal{B}^t(\mathit{in}(e_1, e_2)) \triangleq \mathit{cast}_o(\mathit{in}(\mathcal{B}^t(e_1), \mathcal{B}^t(e_2))) $$

$$ \mathcal{B}^o(\mathit{in}(e_1, e_2)) \triangleq \mathit{in}(\mathcal{B}^t(e_1), \mathcal{B}^t(e_2)) $$
Next, we define an interpretation for in by

$$ \text{in}^{I^B}(v_1, v_2) \text{ iff } \text{in}^I(v_1, v_2) = \top^D $$

The proof of Theorem 4.3.6 is easily adapted. The key argument is that set membership is specified to be a relation in TLA$^+$, meaning in always returns a Boolean value. From this fact and the definition of $I^B$, it follows that

$$ \llbracket \text{in}(e_1, e_2) \rrbracket^{I^B} = \top \text{ iff } \llbracket \text{in}(e_1, e_2) \rrbracket^I = \top^D $$

$$ \llbracket \text{in}(e_1, e_2) \rrbracket^{I^B} = \bot \text{ iff } \llbracket \text{in}(e_1, e_2) \rrbracket^I = \bot^D $$

The proof is trivial from here. For completeness, remark that the mapping $I \mapsto I^B$ is still surjective, because the original interpretation of in : $\iota \times \iota \to \iota$ can be defined from the interpretation of in : $\iota \times \iota \to o$ (simply convert $\top$ to $\top^D$ and $\bot$ to $\bot^D$).

We now turn to set comprehension. The argument is trickier, as we need to prove that these sets are preserved if their first-order parameters are projected as predicates. To provide the intuition, remark that the equation

$$ \{x \in e_1 : e_2\} = \{x \in e_1 : e_2 = \text{TRUE}\} $$

is provable in TLA$^+$ using set extensionality, because the predicates that characterize both sets are equivalent.

Let $\Sigma^B(\text{setst}) \triangleq \iota \times (\iota \to o) \to \iota$. Only one rule for $\mathcal{B}^t$ is adapted:

$$ \mathcal{B}^t(\text{setst}(e_1, \lambda x : e_2)) \triangleq \text{setst}(\mathcal{B}^t(e_1), \lambda x^t : \mathcal{B}^o(e_2)) $$

Note that the second argument to setst will always be a lambda-term, because users only have access to the notation $\{x \in e_1 : e_2\}$. Let the new interpretation for setst be defined by

$$ \text{setst}^{I^B}(v, p) \triangleq \text{setst}^I(v, p') \quad \text{where } p'(u) \triangleq \top^D \text{ if } p(u) = \top, \text{ otherwise } \bot^D \quad (*) $$

We now indicate how the proof of Theorem 4.3.6 is adapted. It suffices to prove that

$$ \llbracket \mathcal{B}^t(\text{setst}(e_1, \lambda x : e_2)) \rrbracket_{\theta}^{I^B} = \llbracket \text{setst}(e_1, \lambda x : e_2) \rrbracket_{\theta}^{I} $$

We define the following values and functions on D:

$$ v \triangleq \llbracket \mathcal{B}^t(e_1) \rrbracket_{\theta}^{I^B} $$

$$ p(u) \triangleq \llbracket \mathcal{B}^o(e_2) \rrbracket_{\theta_u}^{I^B} $$

$$ w \triangleq \llbracket e_1 \rrbracket_{\theta}^{I} $$

$$ q(u) \triangleq \llbracket e_2 \rrbracket_{\theta_u}^{I} $$

The desired equation is verified by

$$ \text{setst}^{I^B}(v, p) = \text{setst}^I(v, p') = \text{setst}^I(w, q) $$

where the first equality is the definition of setst$^{I^B}$ and the second equality is proved by set extensionality. Indeed, the induction hypothesis gives $v = w$ and $p(u) = \top$ iff $q(u) = \top^D$ for all $u$ in D. But $p(u) = \top$ iff $p'(u) = \top^D$, so the elements of both sets are the same.

Let us now prove that the mapping $I \mapsto I^B$ remains surjective when setst expects a predicate argument. Given a $\Sigma^B$-interpretation J, we define a $\Sigma$-interpretation I such that $K^{I^B} = K^J$ for all $K \neq \text{setst}$, and

$$ \text{setst}^I(v, f) \triangleq \text{setst}^J(v, f') \quad \text{where } f'(u) \triangleq \top \text{ if } f(u) = \top^D, \text{ otherwise } \bot $$
We prove that $\mathbf{setst}^{\mathcal{I}^B} = \mathbf{setst}^J$. Let $v$ in $D$ and $p$ a predicate on $D$. Let $f = p'$ defined as in $(*)$. Clearly, $f' = p$, thus

$$ \mathbf{setst}^{\mathcal{I}^B}(v, p) = \mathbf{setst}^I(v, f) = \mathbf{setst}^J(v, p) $$

For choose expressions, the justifications are analogous, but instead of set extensionality, the axiom of choice determinacy is used:

$$ (\forall x : P(x) \Leftrightarrow Q(x)) \Rightarrow \mathbf{choose}(P) = \mathbf{choose}(Q) $$

Here is a summary of the TLA⁺ primitives that are assigned a type with $o$:

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>choose</td><td>(ι → o) → ι</td></tr><tr><td>in</td><td>ι × ι → o</td></tr><tr><td>subseteq</td><td>ι × ι → o</td></tr><tr><td>setst</td><td>ι × (ι → o) → ι</td></tr><tr><td>isafcn</td><td>ι → o</td></tr><tr><td>lteq</td><td>ι × ι → o</td></tr><tr><td>IsFiniteSet</td><td>ι → o</td></tr></tbody></table>

To finish, let us go back to our running example from this chapter.

**Example 4.3.10.** The result of applying our transformation on the proof obligation is:

$$
\begin{array}{l}
\text{NEW } A : \iota, \text{ NEW } B : \iota, \text{ NEW } f : \iota, \\
\quad \text{in}(f, \text{arrow}(\text{domain}(f), B)), \\
\quad \text{subseteq}(\text{domain}(f), A)) \\
\vdash \quad \text{in}(f, \text{union}(\text{setof}_1(\text{subset}(A), \lambda X^ι : \text{arrow}(X, B)))))
\end{array}
$$

There are no differences with the original form of the obligation, except that declared constants have sort annotations. The logical context has changed; the primitive symbols in $\Sigma^B$ are assigned types, some of them featuring the sort $o$. One could verify that the proof obligation is well-sorted in the target logic; in particular, the two hypotheses and the goal are formulas.

## 4.4 Rewriting

Rewriting is a natural way to eliminate primitive constructs with no counterpart in the target logic. Sets are essentially defined by their characteristic predicates, so we may attempt to replace expressions of the form $x \in S$ by simpler expressions. For example:

$$ x \in (S \cup T) \quad \longrightarrow \quad x \in S \lor x \in T $$

This idea is naturally extended to TLA⁺ functions, since a function is characterized by its domain and its body:

$$ [z \in D \mapsto F(z)][x] \quad \longrightarrow \quad F(x) \quad \text{when } x \in D $$
This approach leads to some difficulties. As illustrated by the line above, some rewritings are valid only under certain semantics conditions. Since $D$ can be any set, the problem of checking the validity of that rewriting is undecidable in general.

Another difficulty is to guarantee that rewriting always terminates. Assuming the natural rule $x \in \{y \in S : P(y)\} \rightarrow x \in S \wedge P(x)$, if we define $R \triangleq \{x \in S : \neg(x \in x)\}$ then we have the non-terminating sequence

$$R \in R \rightarrow R \in S \wedge \neg(R \in R) \rightarrow R \in S \wedge \neg(R \in S \wedge \neg(R \in R)) \rightarrow \dots$$

Expressions like $R$ are rarely found in the practice of TLA$^+$. A larger obstacle to a suitable implementation of rewriting is the opposite problem: rewriting often terminates too soon, leaving primitive constructs in the obligation. The instance of $\cup$ cannot be simplified by direct application of a rewriting rule in

$$z = (S \cup T) \Rightarrow x \in z$$

The original SMT encoding, currently implemented in TLAPS, features a rewriting system that is neither terminating nor confluent. We present here an alternative rewriting system that satisfies both of these properties. Rewriting alone was already recognized as insufficient for eliminating enough TLA$^+$ primitives, which is why, in the original implementation, rewriting is supported by a set of auxiliary techniques such as elimination of equalities, or abstraction of complex subexpressions. Our objective here is not to revisit that fragment of the original implementation; we will focus on the rewriting system, even if the resulting implementation is weaker.

### 4.4.1 Definition and Correctness

Let $\square$ be some variable symbol called a *hole*. An expression with a hole is any expression with exactly one occurrence of $\square$. We denote $E$ such expressions. If $e$ is any other expression, the expression $E[e]$ is defined as $E\{\square \mapsto e\}$. We leave implicit the sort of $\square$, which may be $l$ or $o$ depending on the context. We always assume the sorts of $e$ and $\square$ are identical when writing $E[e]$, so the substitution is well-defined, and the sorts of $E$ and $E[e]$ coincide.

**Definition 4.4.1 (Rewriting).** A rewriting rule is a pair of open expressions $(l, r)$ such that every free variable of $r$ is in $l$. We introduce a rewriting rule with the notation

$$l \triangleright r$$

Let $\Gamma_l$ be the typing context such that $\Gamma_l(x) = l$ for all $x$ free in $l$. Both $l$ and $r$ have a sort in the context $\Gamma_l$; we impose that their sorts coincide.

Let $R$ be a set of rewriting rules, also called rewriting system. The relation $\rightarrow_R$ is defined on expressions by

$$E[l\sigma] \rightarrow_R E[r\sigma]$$

where $l \triangleright r$ is a rule in $R$, $E$ is a term with a hole, and $\sigma$ is a substitution. We simply note $\rightarrow$ if the set $R$ is obvious in context.

Clearly, if $e_1 \rightarrow e_2$ and $\Gamma \vdash e_1 : s$ then $\Gamma \vdash e_2 : s$. The fact that $\square$ only occurs once in expressions implies that subexpressions can only be rewritten one at a time by $\rightarrow$. This is relevant to the question of confluence, which is a property we will discuss in the next section.
**Example 4.4.2.** Consider the rule

$$a \cup \emptyset \triangleright a$$

and the expression $\{S \cup \emptyset, T\} \cup \emptyset$, where $S$ and $T$ are two constants.

Here are two different ways to rewrite the expression, with the respective definitions for $E$ and $\sigma$:

$$\{S \cup \emptyset, T\} \cup \emptyset \rightarrow \{S, T\} \cup \emptyset \qquad \sigma(a) \triangleq S \qquad E \triangleq \{\square, T\} \cup \emptyset$$

$$\{S \cup \emptyset, T\} \cup \emptyset \rightarrow \{S \cup \emptyset, T\} \qquad \sigma(a) \triangleq \{S \cup \emptyset, T\} \qquad E \triangleq \square$$

We usually represent this situation with a diagram:

<figure><img src="image_13.png" /></figure>

**Proposition 4.4.3.** Let $E$ be an expression with a hole, $e$ an expression, $I$ an interpretation and $\theta$ a valuation. Then $[[E[e]]]_{\theta}^{I} = [[E]]_{\theta^{\square}}^{I}$ where $v = [[e]]_{\theta}^{I}$.

*Proof.* This is proved by

$$\begin{align*}
[[E[e]]]_{\theta}^{I} &= [[E\{\square \mapsto e\}]_{\theta}^{I} && \text{by definition of } E[e] \\
&= [[E]]_{\{\square \to e\}\theta}^{I} && \text{by Proposition 4.2.9} \\
&= [[E]]_{\theta^{\square}}^{I}
\end{align*}$$

□

**Theorem 4.4.4 (Correctness).** A rewriting system is defined as correct iff for all rules $l \triangleright r$, interpretations $I$ and valuations $\theta$, $[[l]]_{\theta}^{I} = [[r]]_{\theta}^{I}$.

If $R$ is correct, then $e_1 \rightarrow_R e_2$ implies $[[e_1]]_{\theta}^{I} = [[e_2]]_{\theta}^{I}$ for all $I$ and $\theta$.

*Proof.* Let $v = [[l\sigma]]_{\theta}^{I}$ and $w = [[r\sigma]]_{\theta}^{I}$. Then by Proposition 4.2.9 and the correctness assumption,

$$v = [[l]]_{\sigma\theta}^{I} = [[r]]_{\sigma\theta}^{I} = w$$

By Proposition 4.4.3, it follows that

$$[[E[l\sigma]]]_{\theta}^{I} = [[E]]_{\theta^{\square}}^{I} = [[E]]_{\theta^{\square}}^{I} = [[E[r\sigma]]]_{\theta}^{I}$$

□

An immediate corollary of Theorem 4.4.4 is that $e_1 \rightarrow e_2$ implies that $I \models e_1$ iff $I \models e_2$ for all $I$ when $e_1$ and $e_2$ are formulas. Thus we only have to guarantee $l$ and $r$ always have the same value (if they are formulas, the same truth value) to guarantee both the soundness and the completeness of rewriting.

Our rewriting system for TLA$^+$ is presented in Figure 4.4. The TLA$^+$ notations are used for better readability. Note that the characters $x$, $a$, $b$, $f$, $t$ and $r$ all denote variables. The characters $T$ and $\phi$ are not variables but placeholders for terms or formulas, respectively. The
rules that feature a T or a φ are schemas of rewriting rules; these rules must be presented as schemas because they involve a higher-order parameter. There are also schemas of rules for the operators that accept an arbitrary number of arguments. For instance, the actual schema for set refinement is

$$x \in \{T : y_1 \in a_1, \dots, y_p \in a_p\} \triangleright \exists y_1, \dots, y_p : y_1 \in a_1 \wedge \dots \wedge y_p \in a_p \wedge x = T$$

Only the representative case for $p = 1$ is shown for the sake of readability. All the rules that involve tuples or records are understood to be generalized to any $p$ as well.

It is easy to check that all rules preserve types from $l$ to $r$, and values as well. Thus rewriting is correct by Theorem 4.4.4. An alternative way to state correctness is to assert that

$$\forall x_1, \dots, x_n : l = r$$

is a theorem of TLA$^+$ for all $l \triangleright r$, where $x_1, \dots, x_n$ are the free variables of $l$. Many of these statements are among the axioms we pass to the provers, which we discuss in the next section.

Any implementation that is based on this rewriting system is therefore correct, but so far we have described rewriting as a non-deterministic procedure represented by the relation $\to$. Any rewriting is of the form $E[l\sigma] \to E[r\sigma]$, but there can be several ways to put a given expression under the form on the left. The property of *confluence* ensures that diverging rewriting sequences can always be joined. Combined with *termination*, this will guarantee that any implementation of $\to$ converges to a unique solution.

### 4.4.2 Termination and Confluence

The previous version of rewriting did not terminate because of this rule:

$$x \in \{y \in a : e\} \triangleright x \in a \wedge e\sigma \quad \text{where } \sigma(y) \triangleq x$$

The problem is that the substitution $e\sigma$ may introduce a match for some rewriting rule that was not present before. We illustrated this with the formula $R \in R$ where $R \triangleq \{x \in S : \neg(R \in R)\}$. Termination is recovered by using this rule instead:

$$x \in \{y \in a : e\} \triangleright x \in a \wedge \exists y : y = x \wedge e$$

Applying this to the example:

$$R \in R \to R \in V \wedge \exists x : x = R \wedge \neg(x \in x)$$

The subformula $x \in x$ cannot be rewritten because $x$ is a variable.

**Theorem 4.4.5 (Termination).** *The rewriting system of Figure 4.4 terminates, i.e. there is no infinite sequence $e_1, e_2, \dots$ such that $e_1 \to e_{i+1}$.*

*Proof.* The idea of the proof is to exhibit a measure on expressions that is strictly decreasing with $\to$, with respect to some well-founded order.

With each expression $e$, we will associate a triple of natural numbers $w(e)$. We consider the lexicographic order on $\mathbb{N}^3$, noted $<$, which is defined by

$$\begin{align*}
(m, n, p) < & (m', n', p') && \text{iff either } m < m' \\
& & \text{or } m = m' \text{ and } n < n' \\
& & \text{or } m = m' \text{ and } n = n' \text{ and } p < p'
\end{align*}$$
```
a ⊆ b ▷ ∀x : x ∈ a ⇒ x ∈ b
x ∈ {a₁, ..., aₚ} ▷ x = a₁ ∨ ... ∨ x = aₚ
x ∈ ∅ ▷ FALSE
x ∈ UNION a ▷ ∃y : y ∈ a ∧ x ∈ y
x ∈ SUBSET a ▷ ∀y : y ∈ x ⇒ y ∈ a
x ∈ {y ∈ a : φ} ▷ x ∈ a ∧ ∃y : y = x ∧ φ
x ∈ {T : y ∈ a} ▷ ∃y : x = T ∧ y ∈ a

x ∈ a ∪ b ▷ x ∈ a ∨ x ∈ b
x ∈ a ∩ b ▷ x ∈ a ∧ x ∈ b
x ∈ a \ b ▷ x ∈ a ∧ ¬(x ∈ b)
x ∈ BOOLEAN ▷ ∨ x = cast₀(TRUE)
          ∨ x = cast₀(FALSE)
"foo" ∈ STRING ▷ TRUE
```

```
f ∈ [a → b] ▷ ∧ isafcn(f)
      ∧ DOMAIN f = a
      ∧ ∀x : x ∈ a ⇒ f[x] ∈ b

isafcn([x ∈ a ↦ T]) ▷ TRUE
DOMAIN [x ∈ a ↦ T] ▷ a
isafcn([f EXCEPT ! [x] = y]) ▷ TRUE
DOMAIN [f EXCEPT ! [x] = y] ▷ DOMAIN f
```

```
t ∈ a × b ▷ ∧ t[1] ∈ a
      ∧ t[2] ∈ b
      ∧ t = ⟨t[1], t[2]⟩

isafcn(⟨x, y⟩) ▷ TRUE
DOMAIN ⟨x, y⟩ ▷ {1, 2}
⟨x, y⟩[1] ▷ x
⟨x, y⟩[2] ▷ y
```

```
r ∈ [foo : a, bar : b] ▷ ∧ r["foo"] ∈ a
      ∧ r["bar"] ∈ b
      ∧ r = [foo ↦ r["foo"],
             bar ↦ r["bar"]]

isafcn([foo ↦ x, bar ↦ y]) ▷ TRUE
DOMAIN [foo ↦ x, bar ↦ y] ▷ {"foo", "bar"}
[foo ↦ x, bar ↦ y]["foo"] ▷ x
[foo ↦ x, bar ↦ y]["bar"] ▷ y
```

<caption>Figure 4.4: Rewriting Rules</caption>
It remains to define $w(e) = (n_1, n_2, n_3)$. The idea is to count occurrences of certain primitive operators in $e$. The measure will decrease because all rewriting rules simplify $e$ by removing at least one primitive operator. But some rules also introduce new operators which count for $w(e)$, for example:

$$ \text{DOMAIN} \langle x, y \rangle \triangleright \{1, 2\} $$

The key is to define $w(e)$ in such a way that the operator $\langle \_, \_ \rangle$ weighs more than $\{ \_, \_ \}$. This is why we have chosen a lexicographic order rather than the simpler order $<$ on $\mathbb{N}$.

$n_1$ is defined as the number of occurrences of the operators $\times$ and $[foo : \_, bar : \_]$. $n_2$ is the number of occurrences of $\langle \_, \_ \rangle$ and $[foo \mapsto \_, bar \mapsto \_]$. $n_3$ is the number of occurrences of $\subseteq$, $\{ \_, \dots, \_, \}_$, $\emptyset$, UNION, SUBSET, $\{ \_ \in \_ : \_ \}$, $\{ \_ : \_ \in \_ \}$, $\cup$, $\cap$, $\setminus$, BOOLEAN, STRING, $[ \_ \to \_]$, $[ \_ \in \_ \mapsto \_]$, $[ \_ \text{EXCEPT } ![ \_] = \_]$. We can verify that $w(l) \succ w(r)$ for all rules $l \triangleright r$. For instance:

$$ w(\text{DOMAIN} \langle x, y \rangle) = (0, 1, 0) \succ (0, 0, 1) = w(\{1, 2\}) $$

Then, clearly, $w(E[l\sigma]) \succ w(E[r\sigma])$ for all $l \triangleright r$. Therefore $e \to e'$ implies $w(e) \succ w(e')$. But $\mathbb{N}^3$ is known to be well-ordered by $<$, so $\to$ terminates. $\square$

<figure><img src="image_14.png" /></figure>

We now turn to the confluence property, starting with some basic definitions.

**Definition 4.4.6.** We denote by $\to^*$ the reflexive transitive closure of $\to$. Two expressions $e_1$ and $e_2$ are joinable iff there exists $e'$ such that $e_1 \to^* e'$ and $e_2 \to^* e'$. A rewriting system is confluent if for every $e$, $e_1$ and $e_2$ such that $e \to^* e_1$ and $e \to^* e_2$, $e_1$ and $e_2$ are joinable. A rewriting system is locally confluent if for every $e$, $e_1$ and $e_2$ such that $e \to e_1$ and $e \to e_2$, $e_1$ and $e_2$ are joinable.

Any confluent rewriting system is locally confluent. The converse is not true in general, but a classic result by Newman states that local confluence suffices for terminating systems.

**Lemma 4.4.7 (Newman).** *Any terminating, locally confluent rewriting system is confluent.*

*Proof.* A proof of this result is given by Huet [42]. The proof consists of a double induction on the lengths of the two sequences $e \to^* e_1$ and $e \to^* e_2$. $\square$

<figure><img src="image_15.png" /></figure>

It suffices to prove that our rewriting system is locally confluent. Let us look again at the rule $a \cup \emptyset \triangleright a$ (which is not part of our system). We saw that the expression $\{S \cup \emptyset, T\} \cup \emptyset$ could be reduced in two different ways. The two resulting formulas are joinable:

<figure><img src="image_16.png" /></figure>

However, the introduction of this rule to our system would break (local) confluence, as this case illustrates:
<figure><img src="image_17.png" /></figure>

Since $x \in \emptyset$ can be rewritten as FALSE, we could join the pair by adding the schema of rules $\phi \lor \text{FALSE} \triangleright \phi$. We purposefully avoided rules that act on propositional connectives to make confluence easy to prove. In the original version of the encoding, confluence was only proved for rewriting systems that exclude applications of set extensionality. $a \cup \emptyset \triangleright a$ is an instance of set extensionality.

It can be difficult to prove local confluence directly. We may reduce the problem to a small number of easy verifications with the notion of critical pair.

**Definition 4.4.8.** A common instance of two expressions $e_1$ and $e_2$ is an expression $e'$ such that $e' = e_1\rho = e_2\sigma$ for some substitutions $\rho$ and $\sigma$. The expression $e'$ is a most general common instance if for all common instance $e''$ of the same expressions, there is a substitution $\sigma'$ such that $e'' = e'\sigma'$.

**Definition 4.4.9.** Let $l_1 \triangleright r_1$ and $l_2 \triangleright r_2$ be two rewriting rules. Suppose there exists an open expression $e$ such that $l_1 = E[e]$ and a most general common instance $e\rho = l_2\sigma$. Then the pair of expressions $\langle E\rho[r_2\sigma], r_1\rho \rangle$ is called a critical pair. A critical pair is joinable if the two expressions are joinable.

The definition of critical pairs is based on the following template for diverging rewritings:

<figure><img src="image_18.png" /></figure>

**Example 4.4.10.** A critical pair can be derived from the rules

$l_1 \triangleright r_1:$

$l_2 \triangleright r_2:$

$x \in (a \cup b) \triangleright x \in a \lor x \in b$

$a \cup \emptyset \triangleright a$

The relevant subterm of $l_1$ is $(a \cup b)$. It admits a most general common instance with $l_2$ through the substitution $\rho(b) \triangleq \emptyset$ (all other variables are ignored). This leads to the critical pair $\langle x \in a, x \in a \lor x \in \emptyset \rangle$.

Critical pairs are useful because we can enumerate them. It suffices to go through all rules $l \triangleright r$ and check if some subterm of $l$ can be matched with the left pattern $l'$ of another (or the same) rule. When that is the case it suffices to consider the most general match possible.

**Lemma 4.4.11.** A rewriting system is locally confluent if all of its critical pairs are joinable.

*Proof.* This is proven by Huet [42]. □

**Theorem 4.4.12 (Confluence).** *The rewriting system of Figure 4.4 is confluent.*
*Proof.* Since it is terminating (Theorem 4.4.5), it suffices to check that all critical pairs are joinable (Lemmas 4.4.7 and 4.4.11).

There are actually almost no critical pair in our rewriting system. All critical pairs result from the rules that are parameterized by a term *T* or a formula *φ*. For instance, there is a class of critical pairs that consists of pairs of the form

<figure><img src="image_19.png" /></figure>

For some rule $l \triangleright r$. But the pair is easily joinable, as the diagram also shows.

Note that $y \in a$ is not a subexpression of $\{y \in a : \phi\}$. Although we are using the readable TLA$^+$ notations here, such an expression must be read as `setst(a, \lambda y : \phi)`. $\square$

To summarize the results of this section, we state the following:

**Theorem 4.4.13.** For all *e*, there is a unique *e'* such that *e* →\* *e'* and *e'* cannot be rewritten.

*Proof.* Termination ensures the existence of *e'*. Suppose *e''* also satisfies the conditions of the theorem. Then *e'* and *e''* must be joinable, by confluence. But neither can be rewritten, therefore *e'* = *e''*. $\square$

**Example 4.4.14.** Let us see how rewriting affects our running example. The last section ended with the obligation

**ASSUME** NEW $A : \iota$, NEW $B : \iota$, NEW $f : \iota$,
$\quad \ln(f, arrow(domain(f), B))$,
$\quadsubseteq(domain(f), A))$

**PROVE** $\ln(f, union(setof_1(subset(A), \lambda X^\iota : arrow(X, B))))$

We apply as many rewriting rules as possible (we let the reader translate the expressions of Figure 4.4 into our alternative notations). With some minor modifications to improve the presentation, we obtain the following result:

**ASSUME** NEW $A : \iota$, NEW $B : \iota$, NEW $f : \iota$,
$\quad isafcn(f)$,
$\quad domain(f) = domain(f)$,
$\quad \forall x : \ln(x, domain(f)) \Rightarrow \ln(fcnapp(f, x), B)$,
$\quad \forall x : \ln(x, domain(f)) \Rightarrow \ln(x, A)$

**PROVE** $\exists y : \wedge \exists X : \wedge \forall x : \ln(x, X) \Rightarrow \ln(x, A)$
$\quad \wedge y = arrow(X, B)$
$\quad \wedge \ln(f, y)$
Note that it is possible to rearrange quantifiers and substitute arrow($X, B$) for $y$ in the goal, and then eliminate the redundant quantifier $∃y$. That would result in the goal

$$ \exists X : \bigwedge \forall x : \mathbf{in}(x, X) \Rightarrow \mathbf{in}(x, A) \\ \wedge \mathbf{in}(f, \mathbf{arrow}(X, B)) $$

This can be rewritten further, eliminating the last occurrence of the operator arrow. However, implementing this kind of simplifications might result in a non-terminating encoding.

## 4.5 Axiomatization

All TLA⁺ primitive operators are specified by axioms. During the axiomatization phase of the encoding, explicit declarations and axioms are inserted in the proof obligation's context for all relevant operators.

### 4.5.1 Definition and Correctness

The input of this step is a sequent $Γ ⊢ φ$, where $Γ$ contains operator declarations with types, hypotheses which are just Boolean expressions, and the goal $φ$ is a Boolean expression. We consider that the primitive operators of TLA⁺ are bound to a standard signature $Σ$, and the class of possible interpretations is defined by a theory $T$. Axiomatization can be formally understood as the selection of operators from $Σ$ and axioms from $T$ to be inserted at the top of the sequent's context, resulting in a new sequent $Δ, Γ ⊢ φ$. The signature $Σ$ and the theory $T$ are omitted; when the obligation is discharged to an automated prover, that prover will only have access to the information about TLA⁺'s theory that is encoded in $Δ$.

The implementation of this step is straightforward. Let $Γ ⊢ φ$ be the current sequent and $K ∈ Dom(Σ)$ some operator that has not been explicitly declared yet. We select a finite set of axioms $T'$ for $K$ and produce the new sequent

$$ \text{NEW } K : Σ(K), T', Γ ⊢ φ $$

While the original sequent $Γ ⊢ φ$ is preserved, all occurrences of $K$ in it refer to the new declaration.<fnref n="1" /> This process must be repeated as long as the sequent contains operator symbols bound in $Σ$. Note that the addition of $T'$ may introduce operators that did not occur in the sequent before; we must be mindful of dependencies between primitive operators, or axiomatization may not terminate.

**Theorem 4.5.1.** *Axiomatization is sound and terminating.*

We can only lay out the arguments in an abstract manner. To actually prove it, one would need to verify all axioms individually, either by hand or by automated means.

*Proof.* The full list of axioms for the TPTP encoding can be found in appendix B. It is clear that there is no cycle between operator dependencies, so the process terminates.

<footnote n="1">¹Some transformation of $Γ ⊢ φ$ is actually required in practice. TLAPS implements bound variables as De Bruijn indices—natural numbers identifying the unique binder a variable is linked to. Any modification of the proof obligation's context must be accompanied by an update of all variable indices. This technical point about the implementation is hidden by our formalism.</footnote>
For soundness, consider a Σ-interpretation I such that $I \models T$. Let $\Delta \triangleq \text{NEW } k : \Sigma(k), T'$ as described above. Appending $\Delta$ to the current context is sound if $I \models \Delta$, which is obvious as long as $T \models T'$. In general, the axioms of $T'$ are elementary consequences of $T$ (see the discussion below for examples). □

We do not claim that axiomatization is complete. Typical cases of incompleteness arise when the operator(s) required for expressing an existential witness do not occur in the obligation. Consider Cantor's theorem expressed as the proof obligation

ASSUME NEW S, NEW $f \in [S \rightarrow \text{SUBSET } S]$

PROVE $\exists P \in \text{SUBSET } S : \forall x \in S : f[x] \neq P$

The expected witness for $P$ is the set $\{x \in S : x \notin f[x]\}$, but the original obligation does not include that instance of set comprehension. To prove Cantor's theorem, users must insert an intermediary definition or proof step to introduce this set into the proof's context.

## 4.5.2 Second-order Axiomatization of TLA⁺

We refer the reader to appendix B for the full list of axioms. All axioms are elementary reformulations or consequences of the axioms of TLA⁺. Since our target language is HOL, we accept higher-order quantifiers for axioms; typically, the axiom schemas of TLA⁺ are encoded as single axioms $\forall F^\tau : \phi$ where $ord(\tau) = 1$.

In the original theory, primitive constructs are defined from “more primitive” ones when possible, for example $a \cup b \triangleq \text{UNION } \{a, b\}$. This makes TLA⁺'s relative consistency with ZFC more evident. But using those axioms would result in very long chains of dependencies between operators. Moreover, they reflect poorly how a user would reason about those operators. In general, we replaced a complex definition from primitive operators by a more direct characterization, with less dependencies:

$$ \forall a^t, b^t, x^t : \text{in}(x, \text{cup}(a, b)) \Leftrightarrow \text{in}(x, a) \lor \text{in}(x, b) \quad (\text{CupDef}) $$

Which axioms are assigned to a given operator is always evident. In each case, the operator depends on all the other operators that appear in its associated axioms. For instance cup is specified by (CupDef) and depends on in.

The axioms of set theory are standard; we omit the axiom of infinity and the axiom of foundation, since they rarely play any role in TLA⁺ proofs (users can explicitly invoke them if needed). Here are the basic axioms for TLA⁺ functions:
$$ \forall f^t, g^t : \begin{array}{l} \text{isafcn}(f) \land \text{isafcn}(g) \end{array} \qquad (\text{FcnExt}) \\ \land \text{domain}(f) =_\iota \text{domain}(g) \\ \land (\forall x^t : \text{in}(x, \text{domain}(f)) \Rightarrow \text{fnapp}(f, x) =_\iota \text{fnapp}(g, x)) \\ \Rightarrow f =_\iota g $$

$$ \forall F^{t \to t}, a^t : \text{isafcn}(\text{fnc}(a, F)) \qquad (\text{FcnIsafcn}) $$

$$ \forall F^{t \to t}, a^t : \text{domain}(\text{fnc}(a, F)) =_\iota a \qquad (\text{FcnDom}) $$

$$ \forall F^{t \to t}, a^t, x^t : \text{in}(x, a) \Rightarrow \text{fnapp}(\text{fnc}(a, F), x) =_\iota F(x) \qquad (\text{FcnApp}) $$

$$ \forall a^t, b^t, f^t : \text{in}(f, \text{arrow}(a, b)) \Leftrightarrow \qquad (\text{ArrowDef}) $$

$$ \land \text{isafcn}(f) $$

$$ \land \text{domain}(f) =_\iota a $$

$$ \land (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(\text{fnapp}(f, x), b)) $$

The operator `isafcn` is specified by `(FcnExt)`. The operator `fn` is specified by `(FcnIsafcn)`, `(FcnDom)`, `(FcnApp)`. The operator `arrow` is specified by `(ArrowDef)`. The operators `domain` and `fnapp` are not assigned any axioms, but all other functional operators depend on them.

Tuples and records inherit from the theory of functions, but specify additional operators that essentially replace `fn` and `arrow`. For instance, tuples are usually constructed from `tup`, and product sets from `prod`.

$$ \text{For all } n \ge 0, \\ \forall x_1^t, \dots, x_n^t : \begin{array}{l} \text{isafcn}(\text{tup}_n(x_1, \dots, x_n)) \end{array} \qquad (\text{TupIsafcn}) \\ \forall x_1^t, \dots, x_n^t : \begin{array}{l} \text{domain}(\text{tup}_n(x_1, \dots, x_n)) = \text{enum}_n(1, \dots, n) \end{array} \qquad (\text{TupDomain}) \\ \forall x_1^t, \dots, x_n^t : \begin{array}{l} \land \text{fnapp}(\text{tup}_n(x_1, \dots, x_n), 1) = x_1 \\ \land \dots \\ \land \text{fnapp}(\text{tup}_n(x_1, \dots, x_n), n) = x_n \end{array} \qquad (\text{TupApp}) $$

$$ \text{For all } n \ge 2, \\ \forall a_1^t, \dots, a_n^t, t^t : \begin{array}{l} \text{in}(t, \text{prod}_n(a_1, \dots, a_n)) \Leftrightarrow \\ \quad \begin{array}{l} \land t = \text{tup}_n(\text{fnapp}(t, 1), \dots, \text{fnapp}(t, n)) \\ \land \text{in}(\text{fnapp}(t, 1), a_1) \\ \land \dots \\ \land \text{in}(\text{fnapp}(t, n), a_n) \end{array} \end{array} \qquad (\text{ProdDef}) $$

The axiom `(ProdDef)` is justified by the TLA⁺ theorem

$$ \forall a_1, \dots, a_n : a_1 \times \dots \times a_n = \{ \langle x_1, \dots, x_n \rangle : x_1 \in a_1, \dots, x_n \in a_n \} $$
We chose this formulation because it permits a more efficient treatment of functional exten-
sionality for tuples. If *t* and *u* are two tuples of the same length, and all of their components
are equal, then *t* = *u* can be derived from (ProdDef) alone.

Our theory does not include proper axiomatizations of natural, integer or real arithmetic.
We would prefer arithmetic to be handled by a prover's internal engine, but this has only been
implemented for our SMT encoding (Chapter 5). Still, there are a few facts about TLA⁺'s
arithmetical operators that are required so often that we decided to include them for this
simple encoding. For instance, we specify *Int* to be closed under the operations +, -, (both
the unary and binary versions), *. Likewise, ÷ and % are defined as binary functions on *Int*,
but the second argument must be positive. For every numerical constant *n*: *ι* that we declare,
we specify *n* ∈ *Int* and *n* ≥ 0. Note that we treat -1 as -(1), so we only declare constants
for positive numbers. The set *Nat* is specified as the set of integers *z* such that *z* ≥ 0.

**Example 4.5.2.** We go back to our running example, assuming rewriting has not been applied. The result with a top context $\Delta$ is

ASSUME
NEW in : ι × ι → o
NEW subseteq : ι × ι → o
NEW union : ι → ι
NEW subset : ι → ι
NEW setof₁ : ι × (ι → ι) → ι
NEW isafcn : ι → o
NEW fcn : ι × (ι → ι) → ι
NEW domain : ι → ι
NEW fcnapp : ι × ι → ι
NEW arrow : ι × ι → ι

∀a<sup>t</sup>, b<sup>t</sup> : subseteq(a, b) ⇔ (∀x<sup>t</sup> : in(x, a) ⇒ in(x, b)), (SubseteqDef)
∀a<sup>t</sup>, x<sup>t</sup> : in(x, union(a)) ⇔ (∃y<sup>t</sup> : in(x, y) ∧ in(y, a)), (UnionDef)
∀a<sup>t</sup>, x<sup>t</sup> : in(x, subset(a)) ⇔ (∀y<sup>t</sup> : in(y, x) ⇒ in(y, a)), (SubsetDef)
∀F<sup>t→ι</sup>, a<sup>t</sup>, x<sup>t</sup> : in(x, setof<sub>1</sub>(a, F)) ⇔ ∃y<sup>t</sup> : in(y, a) ∧ x =<sub>ι</sub> F(y), (SetofDef<sub>1</sub>)
∀F<sup>t→ι</sup>, a<sup>t</sup> : isafcn(fcn(a, F)), (FcnIsafcn)
∀F<sup>t→ι</sup>, a<sup>t</sup> : domain(fcn(a, F)) =<sub>ι</sub> a, (FcnDom)
∀F<sup>t→ι</sup>, a<sup>t</sup>, x<sup>t</sup> : in(x, a) ⇒ fcnapp(fcn(a, F), x) =<sub>ι</sub> F(x), (FcnApp)
∀a<sup>t</sup>, b<sup>t</sup>, f<sup>t</sup> : in(f, arrow(a, b)) ⇔
  ∧ isafcn(f)
  ∧ domain(f) =<sub>ι</sub> a
  ∧ (∀x<sup>t</sup> : in(x, a) ⇒ in(fcnapp(f, x), b)),

NEW A : ι, NEW B : ι, NEW f : ι,
in(f, arrow(domain(f), B)), (Hyp<sub>1</sub>)
subseteq(domain(f), A)) (Hyp<sub>2</sub>)
PROVE in(f, union(setof<sub>1</sub>(subset(A), λX<sup>t</sup> : arrow(X, B)))) (Goal)
thf(fresh_mem, type, ( mem: $i > $i > $o ) ).
thf(fresh_subsetEq, type, ( subsetEq: $i > $i > $o ) ).
thf(fresh_union, type, ( union: $i > $i ) ).
thf(fresh_subset, type, ( subset: $i > $i ) ).
thf(fresh_setof_1, type, ( setof_1: $i > ( $i > $i ) > $i ) ).
thf(fresh_fcnlsafcn, type, ( fcnlsafcn: $i > $o ) ).
thf(fresh_fcn, type, ( fcn: $i > ( $i > $i ) > $i ) ).
thf(fresh_fcnDom, type, ( fcnDom: $i > $i ) ).
thf(fresh_fcpApp, type, ( fcpApp: $i > $i > $i ) ).
thf(freshArrowSet, type, ( arrowSet: $i > $i > $i ) ).

% axioms omitted...

thf(fresh_a, type, ( a: $i ) ).

thf(fresh_b, type, ( b: $i ) ).

thf(fresh_f, type, ( f: $i ) ).

thf(fact35, axiom,
( mem @ f @
( arrowSet @ ( fcnDom @ f ) @ b ) ) ).

thf(fact36, axiom,
( subsetEq @ ( fcnDom @ f ) @ a ) ).

thfgoal, conjecture,
( mem @ f @
( union @
( setof_1 @ ( subset @ a ) @
( ~ [ X: $i ] :
( arrowSet @ X @ b ) ) ) ) ) ).

<caption>Figure 4.5: Running Example Encoded in TPTP</caption>

Axioms that play no part in the proof have been omitted (set and functional extensionality).
All the functional axioms are added, plus some axioms of set theory.

4.6 Translation to TPTP

The proof obligation is now a sequent $\Delta, \Gamma \vdash \phi$ in the logic $\mathcal{L}',$ which we view as a subset of HOL. All the relevant information about TLA⁺'s semantics has been encoded into the $\Delta$ part of the context. The last step is the translation to TPTP/THF itself. The translation is direct and without any difficult point to address, so we will simply demonstrate it by showing the result of encoding our running example. The output is displayed below; we have omitted the axioms so that it can fit on the page.

The sorts `i` and `o` are represented by the builtin sorts `$i` and `$o`, respectively. A functional
type $s_1 \rightarrow s_2$ is represented $s_1 > s_2$. There is no builtin type for functions of several arguments, but a type $s_1 \times s_2 \rightarrow s_3$ may be encoded as $s_1 \rightarrow (s_2 \rightarrow s_3)$ in HOL, which is written $s_1 > (s_2 > s_3)$ in TPTP. An application $f(x, y)$ is then translated as $(f @ x) @ y$. The connective > has right associativity and @ has left associativity, therefore parentheses can be removed for both expressions: $s_1 > s_2 > s_3$ and $f @ x @ y$.

## 4.7 Evaluation

We implemented the TPTP encoding in order to integrate Zipperposition as a backend solver for TLAPS. Zipperposition is a superposition theorem prover for first-order logic with equality and theories [20]. It features an extension to support higher-order logic [7, 82, 83].

In this section, we evaluate the new Zipperposition backend on a large set of TLA⁺ specifications. We focus our evaluation on the effects of enabling rewriting in the TPTP encoding, and the performances of Zipperposition compared to the Isabelle backend.

### 4.7.1 Methodology

Our data is a set of TLA⁺ specifications coming from three different sources:

* The library of TLA⁺ Examples;<fnref n="2" />

* The TLAPS Examples as found in the distribution of the tool;

* A recent specification of Lamport's *Deconstructed Bakery* algorithm [49].

The full dataset contains 35 specifications with proofs, from which TLAPS generates a total number of 4612 proof obligations. Specifications vary wildly in size: the largest file, which contains the proof of refinement for the Deconstructed Bakery, contains 892 obligations; in contrast, many files contains only elementary results of fewer than 10 obligations.

We proceeded in two steps for our experiment: first, we generated benchmarks for each solver by calling TLAPS on the TLA⁺ files; then, we ran the solvers on their respective benchmarks. Each benchmarks corresponds to a different encoding of TLA⁺ (Isabelle, TPTP without rewriting, TPTP with rewriting). For the Isabelle benchmark, we tested Isabelle for the three tactics *auto*, *blast* and *force*, which are the tactics available from TLAPS. We considered a given obligation to be solved by Isabelle if at least one tactic could solve it.

For all solvers, we set a timeout of 5 seconds, which is the default timeout in TLAPS. The experiment was carried out on a Dell Latitude laptop with a 1.90 GHz Intel Core i7 processor.

### 4.7.2 Results and Discussion

The results are presented in Table 4.1 and Table 4.2. The first table compares the results of Zipperposition with and without rewriting. The second table compares Isabelle with Zipperposition—for the latter, we combined the results obtained by disabling or enabling rewriting. For all tables, we indicate the number of obligations solved by each backend (top numbers) and the number of obligations solved *uniquely* by each backend (bottom numbers).

As Table 4.1 demonstrates, rewriting's impact on performances is only marginal. The overlap between the two versions of the TPTP encoding (2400 obligations) is substantial.

<footnote n="2">²https://github.com/tlaplus/Examples</footnote>
<table><caption>Table 4.1: Number of Obligations Solved by Zipperposition</caption><thead><tr><th rowspan="2">Specification</th><th rowspan="2">Size (# POs)</th><th colspan="2">Backend</th></tr><tr><th>Zipper.</th><th>Zipper.+RW</th></tr></thead><tbody><tr><td>TLA<sup>+</sup> Distribution</td><td>1996</td><td>1124<br>10</td><td>1124<br>10</td></tr><tr><td>TLAPS Distribution</td><td>1402</td><td>810<br>13</td><td>800<br>3</td></tr><tr><td>Deconstructed Bakery</td><td>1214</td><td>510<br>21</td><td>498<br>9</td></tr><tr><td><strong>Total</strong></td><td>4612</td><td>2444<br>44</td><td>2422<br>22</td></tr></tbody></table>

<table><caption>Table 4.2: Comparison of the Isabelle and Zipperposition Backends</caption><thead><tr><th rowspan="2">Specification</th><th rowspan="2">Size (# POs)</th><th colspan="2">Backend</th></tr><tr><th>Isabelle</th><th>Zipperposition</th></tr></thead><tbody><tr><td>TLA<sup>+</sup> Distribution</td><td>1996</td><td>1106<br>181</td><td>1134<br>209</td></tr><tr><td>TLAPS Distribution</td><td>1402</td><td>898<br>204</td><td>813<br>119</td></tr><tr><td>Deconstructed Bakery</td><td>1214</td><td>609<br>196</td><td>519<br>106</td></tr><tr><td><strong>Total</strong></td><td>4612</td><td>2613<br>581</td><td>2466<br>434</td></tr></tbody></table>
This is not especially surprising as the rewriting system we implement is very elementary, compared to the rewriting system of the SMT encoding it is based on. Enabling rewriting actually results in *less* obligations being solved. One possible explanation is that rewriting may remove important terms by eliminating TLA⁺ primitives, making certain existential statements harder to prove; however, we could not find a particular obligation that clearly fails for that specific reason.

Table 4.2 shows that Isabelle and Zipperposition perform rather similarly, with Isabelle solving 147 additional obligations in total. Isabelle uniquely solves 581 obligations, Zipperposition uniquely solves 434, which indicates the backends have complementary strengths. Combined in a portfolio, they solve 3047 obligations.
# Chapter 5

# An Optimized Encoding into First-order SMT

## 5.1 Overview

In Chapter 4, we described a direct encoding of TLA⁺ into HOL, more precisely the THF dialect of TPTP. We proved that encoding sound with respect to the semantics defined in Chapter 3. In this chapter, we describe our encoding to SMT-LIB.

The encoding is presented in Figure 5.1. The general structure is identical to the encoding presented in the previous chapter (Figure 4.1), with two steps completely preserved (recovering formulas, optional rewriting). The axiomatization is adapted for SMT and completed with user patterns (triggers) to guide the instantiation module of SMT. Expressions are also transformed during this step to encode second-order expressions, arithmetical expressions, and equalities relevant to the axiom of set extensionality. The final translation step is of course modified to target SMT-LIB. The final problem sets the SMT logic to UFNIA by default, and UFLIA when the target solver is veriT.

The target logic $\mathcal{L}_1^{\text{t,int}}$ is a restriction of the logic $\mathcal{L}^s$ with an uninterpreted sort $\iota$ and the interpreted sort int of SMT. We assume the arithmetical operators of SMT are present with their intended semantics.<fnref n="1" /> Moreover, second-order applications are not permitted in $\mathcal{L}_1^{\text{t,int}}$. Operator symbols cannot occur as arguments to other operators, and lambda-expressions cannot appear at all. Nested sequents cannot be parameterized by operators, as this is a form of second-order quantification. When an obligation $\Gamma \vdash e$ is such that $\Gamma$ contains a sequent $S$, and $S$ contains an operator declaration, like NEW $F(\_)$, then $S$ is simply omitted to finish the translation. If $S$ is essential to the proof then SMT will likely fail, so users should opt for a higher-order backend like Isabelle or Zipperposition in that case.

The rest of this chapter is organized as follows. We first provide some background on SMT solvers and E-matching (Section 5.2). This will also serve as a general introduction to our method supported by some examples. We then present our strategy for writing an axiomatization of TLA⁺ with triggers (Section 5.3). We then present some fragments of the axiomatizations that are handled in a special ways: axiom schemas, integer arithmetic, and set extensionality (Section 5.4). Finally, we evaluate our SMT encoding and compare its performances with the original SMT encoding (Section 5.5).

<footnote n="1">¹For a presentation, see the SMT documentation [6] or the page https://smtlib.cs.uiowa.edu/theories-Ints.shtml</footnote>
<figure><img src="image_20.png" /><figcaption>Figure 5.1: SMT Encoding Overview</figcaption></figure>

## 5.2 E-matching Patterns

SMT solvers extend SAT solvers with procedures for first-order theories. Theories of interest for SMT users include integer and real arithmetic (linear, non-linear), bit vectors, and extensional arrays. First-order logic is undecidable in general, but quantifiers over uninterpreted domains are still supported by an *instantiation module*. The purpose of this module is to produce instances of the quantified formulas of the problem to insert into the quantifier-free problem.

Propositional logic is decidable, so we will focus on the much harder problem of generating the right instances of our first-order axioms. In this context, it is helpful to restrict our study to universally quantified formulas in prenex form:

$$ \forall x_1^{s_1}, \dots, x_n^{s_n} : \phi \quad \text{where } \phi \text{ is quantifier-free} $$

All problems of first-order logic can be reduced to problems with formulas of the form above through the application of elementary logical equivalences and Skolemization [3].

**Example 5.2.1.** Take the axiom specifying the subset relation in TLA⁺:

$$ \forall a^t, b^t : \text{subseteq}(a, b) \Leftrightarrow (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(x, b)) \quad (\text{Subseq}) $$

To put (Subseq) in prenex form, we apply logical rules to move the nested quantifier $\forall x^t$ up the structure of the formula. Before this, we split the equivalence in two implications:

$$ \begin{aligned} \forall a^t, b^t : \wedge \text{subseteq}(a, b) &\Rightarrow (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(x, b)) \\ &\wedge (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(x, b)) \Rightarrow \text{subseteq}(a, b) \end{aligned} $$

We can now apply the following rules for moving quantifiers above implications:

$$ \begin{aligned} \phi &\Rightarrow (\forall x : \psi) &\Leftrightarrow &\forall x : \phi \Rightarrow \psi \\ (\forall x : \phi) &\Rightarrow \psi &\Leftrightarrow &\exists x : \phi \Rightarrow \psi \end{aligned} $$
As the second rule shows, the $\forall x^t$ that originally occurs on the left of a $\Rightarrow$ must become existential. Quantifiers that become existential when moved to the top are called *strong*, and the others *weak*. To finish putting the axiom in prenex form, we put the conjuncts in two separate axioms:

$$ \forall a^t, b^t, x^t : \text{subseteqq}(a, b) \Rightarrow (\text{in}(x, a) \Rightarrow \text{in}(x, b)) \quad (\text{SubseteqElim}) $$

$$ \forall a^t, b^t : \exists x^t : (\text{in}(x, a) \Rightarrow \text{in}(x, b)) \Rightarrow \text{subseteqq}(a, b) \quad (\text{SubseteqIntro}) $$

Skolemization is a technique for eliminating strong quantifiers. The intuition is that existentially quantified variables can be safely replaced by terms playing the role of witnesses in inner formulas. Since $\exists x^t$ occurs below two universal quantifiers, we introduce a new binary symbol $w$ and rewrite (SubseteqIntro) as

$$ \forall a^t, b^t : (\text{in}(w(a, b), a) \Rightarrow \text{in}(w(a, b), b)) \Rightarrow \text{subseteqq}(a, b) $$

SMT solvers vary in how they preprocess formulas and apply Skolemization, which itself admits several definitions. We will not systematically transform expressions to put them in universal prenex form as we did in Example 5.2.1, because we assume SMT solvers can handle this part more efficiently. However we will consider moving weak quantifiers at the top of our axioms, as this makes it easier to focus on quantifier instantiation. Finding relevant instances is a difficult problem, and we need to assist the SMT solvers for this task.

E-matching is one of several approaches to the problem of quantifier instantiation [24, 36, 63, 64]. The basic principle of E-matching is to look in the current ground problem for terms matching syntactical patterns. Patterns can be user-defined or heuristically generated. Formally, we represent the ground problem with a set $E$ of propositional formulas with uninterpreted symbols and equalities, and a pattern by a term $p$ with free variables. A match is a ground term $t$ and a substitution $\sigma$ such that $E \models t = p\sigma$. Typically, solvers will look for terms $t$ that occur in the current problem, possibly resulting from Skolemization; those terms are said to be *known*.

**Example 5.2.2.** Consider the following elementary theorem of TLA⁺:

MODULE Subseteq

EXTENDS TLAPS

THEOREM ASSUME NEW $S$, NEW $T$, NEW $U$,

$$ U = S \cap T $$

PROVE $U \subseteq S$

OBVIOUS

This is proved intuitively by taking an $x \in U$ and proving $x \in S$. Because $U = S \cap T$, we have $x \in S \cap T$ and therefore $x \in S$. We will now look at a possible formalization in SMT to see how the automated proof might proceed.

The obligation is first-order and does not feature arithmetic, so the direct encoding of Chapter 4 results in a problem that SMT can handle. We insert two axioms into the problem for specifying the subset relation and the intersection operator (one unnecessary axiom is omitted). Axioms are annotated with patterns indicated between curly braces. The obligation is proved if the set of formulas below is found unsatisfiable. Note that we use different
notations to highlight the structures of first-order expressions: **subseteq** is the relation $\subseteq$, **cap** is the binary operator $\cap$, **in** is the relation $\in$.

$$ \forall a^t, b^t : \{\text{subseteq}(a, b)\} \quad (\text{in}(w(a, b), a) \Rightarrow \text{in}(w(a, b), b)) \Rightarrow \text{subseteq}(a, b) \quad (\text{Subseteq}) $$

$$ \forall a^t, b^t, x^t : \{\text{in}(x, \text{cap}(a, b))\} \quad \text{in}(x, \text{cap}(a, b)) \Leftrightarrow \text{in}(x, a) \wedge \text{in}(x, b) \quad (\text{Cap}) $$

$$ U = \text{cap}(S, T) \qquad (\text{H}) $$

$$ \neg \text{subseteq}(U, S) \qquad (\text{G}) $$

The term **subseteq**(*U*, *S*) in the goal matches the pattern of (Subseteq). We say that the axiom is triggered by this match. The match is represented by the substitution {$a \mapsto U, b \mapsto S$}. That substitution is used to generate an instance of the axiom, which is introduced into the ground problem:

$$ (\text{in}(w(U, S), U) \Rightarrow \text{in}(w(U, S), S)) \Rightarrow \text{subseteq}(U, S) \qquad (\text{F1}) $$

Note that $w(U, S)$ plays the role of $x$ in our intuitive proof, because it now suffices to assume $w(U, S)$ is an element of $U$ and prove it is an element of $S$ to derive a contradiction.

The subterm $\text{in}(w(U, S), U)$ in (F1) matches the pattern $\{\text{in}(x, \text{cap}(a, b))\}$ for the substitution $\{a \mapsto S, b \mapsto T, x \mapsto w(U, S)\}$. E-matching finds matches *modulo equality*, so the equality in (H) is accounted for to match $U$ with $\text{cap}(a, b)$. The new fact is

$$ \text{in}(w(U, S), \text{cap}(S, T)) \Leftrightarrow \text{in}(w(U, S), S) \wedge \text{in}(w(U, S), T) \qquad (\text{F2}) $$

Now a contradiction can be derived from the ground problem, which means the problem has been solved. That last step was essentially the expansion of $x \in S \cap T$ into $x \in S \wedge x \in T$.

Example 5.2.2 considered axioms with single patterns, but typically we want to match several patterns at the same time. A *trigger* for the variables $x_1, \dots, x_n$ is a set of patterns $\{p_1, \dots, p_k\}$ such that the free variables of all $p_j$ are exactly the variables $x_i$. We may annotate axioms with several triggers, so the general form is

$$ \begin{array}{l} \forall x_1^{s_1}, \dots, x_n^{s_n} : \{p_{1,1}, \dots, p_{1,n_1}\} \\ \qquad \dots \\ \qquad \{p_{m,1}, \dots, p_{1,n_m}\} \\ \phi \end{array} $$

where $\phi$ is quantifier-free. A term $t$ is a match if there exists a substitution $\sigma$ such that $E \models t = p_{i,j}\sigma$ for some $i$ and all $j \le n_i$. So any individual trigger can produce an instance, but all patterns of that trigger must match simultaneously.

Modern SMT solvers implement efficient procedures for detecting terms matching triggers [24]. As a result, triggers have become a popular solution among SMT users for writing custom axiomatizations [50, 55]. Triggers offer some control over the instantiation engine to the user, which is why they are sometimes presented as a way to program SMT solvers. In fact, it is possible to define notions of termination and completeness for triggers in a satisfactory way [30]. Intuitively, we will say an axiomatization terminates if only a finite number of instances can be produced from any finite ground problem. We will say it is complete if any provable problem is still provable when only instances produced by triggers are allowed.
SMT solvers can generate triggers automatically, but we found that we could achieve better results by selecting our own triggers. The next section will detail our strategy for trigger selection through motivating examples. On the subject of soundness, there is nothing to add from our previous discussion on axiomatization (Section 4.5): triggers do not change the semantics of formulas, so they are perfectly safe to use. However, termination and completeness are not guaranteed. Our axiomatization enjoys neither of these properties, but many of our choices are still guided by considerations of termination and completeness: we select as many adequate triggers as possible to anticipate different proof scenarios, but we reject triggers that obviously result in irrelevant instances or matching loops.

# 5.3 Selecting Axioms and Triggers for TLA⁺

## 5.3.1 Case Study

In this section, we will focus on a simple theorem of TLA⁺, displayed below.

```
MODULE Intersection

EXTENDS TLAPS, Integers

THEOREM ASSUME NEW S,
        S ∩ Int ⊆ {}

PROVE 1 ∉ S

OBVIOUS
```

Here is an intuitive proof: we assume $1 \in S$ and derive a contradiction; since $1 \in S$ and $1 \in Int$, we have $1 \in S \cap Int$; since $S \cap Int \subseteq {}$, we have $1 \in {}$, which is contradictory.

The proof involves three set-theoretic primitive operators of TLA⁺, namely the subset relation, the intersection and the empty set. No arithmetic is needed beyond the fact that $1 \in Int$. We will look at a few different ways to formulate the axioms with triggers, starting from a rather naive theory and finishing with the actual theory we implement. For every attempt, it is important that we consider exclusively instances resulting from triggers, so that the solution scales to larger problems. The problem above is simple enough so that SMT solvers can find all instances by enumerative approaches; in very large problems, the search space of ground terms may be too large, and there may be too many quantifiers for this approach to work.

**Example 5.3.1** (First Attempt). The encoded problem is displayed below. We treat 1 as a constant of the sort $\iota$ and assume the fact $1 \in Int$ has been derived. Details about how arithmetic is handled can be found in Section 5.4.2.

```
∀a^t, b^t : {subseteq(a, b)}      subseteq(a, b) ⇔ (∀x^t : in(x, a) ⇒ in(x, b))      (Subseteq)
∀a^t, b^t, x^t : {in(x, cap(a, b))}   in(x, cap(a, b)) ⇔ in(x, a) ∧ in(x, b)          (Cap)
∀x^t : {in(x, enum0)}               ¬in(x, enum0)                             (Empty)

subseteq(cap(S, Int), enum0)          (H1)
in(1, Int)                               (H2)
in(1, S)                                 (G)
```
Here, the only match possible is the term `subseteq(cap(S, Int), enum0)` for the axiom (Subseteq) and the substitution `{a ↦ cap(S, Int), b ↦ enum0}`. This results in the new fact

$$ \text{subseteq}(\text{cap}(S, \text{Int}), \text{enum}_0) \Leftrightarrow (\forall x^t : \text{in}(x, \text{cap}(S, \text{Int})) \Rightarrow \text{in}(x, \text{enum}_0)) \quad (\text{F1}) $$

Let us put (F1) in prenex form to continue the proof. This is the exact process we described earlier, it results in the two facts

$$ \forall x^t : \text{subseteq}(\text{cap}(S, \text{Int}), \text{enum}_0) \wedge \text{in}(x, \text{cap}(S, \text{Int})) \Rightarrow \text{in}(x, \text{enum}_0) \quad (\text{F1a}) $$

$$ (\text{in}(w(\dots), \text{cap}(S, \text{Int})) \Rightarrow \text{in}(w(\dots), \text{enum}_0)) \Rightarrow \text{subseteq}(\text{cap}(S, \text{Int}), \text{enum}_0) \quad (\text{F1b}) $$

where $w$ is a new symbol and $w(\dots)$ is the term $w(\text{cap}(S, \text{Int}), \text{enum}_0)$.

(F1a) is a quantified formula. Since it has no trigger and we do not consider other methods of instantiation, we cannot use it. However, the path to a contradiction requires instantiating the formula with 1. Therefore, we are stuck. The fact (F1b) is ground, but it will not make the proof progress.

The problem from Example 5.3.1 is not provable using triggers only. Before we present a solution, let us stress the obvious analogy between those triggers and the rewriting rules

$$ \begin{align*} & a \subseteq b \triangleright \forall x : x \in a \Rightarrow x \in b \\ & x \in a \cap b \triangleright x \in a \wedge x \in b \\ & x \in \{\} \triangleright \text{FALSE} \end{align*} $$

Triggers were directly taken from the left patterns of the rewriting rules. We might say the axioms essentially implement those rewritings into the SMT problem. In both cases, a universal quantifier with no trigger is introduced into the problem, getting us stuck.

The solution is to reformulate (Subseteq) as we did in the previous section. The axiom is split in two; in one case, the nested quantifier $\forall x^t$ is moved at the top. This opens up the possibility to assign a trigger that includes the three variables $a$, $b$ and $x$.

**Example 5.3.2 (Second Attempt).** Compared to the previous example, only (Subseteq) has changed. We do not Skolemize (SubseteqIntro) below—the axiom plays no role in the proof. The axiom (SubseteqElim) is slightly reformulated to save some parentheses.

$$ \forall a^t, b^t : \{\text{subseteq}(a, b)\} \qquad (\text{SubseteqIntro}) $$

$$ (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(x, b)) \Rightarrow \text{subseteq}(a, b) $$

$$ \forall a^t, b^t, x^t : \{\text{subseteq}(a, b), \text{in}(x, a)\} \qquad (\text{SubseteqElim}) $$

$$ \text{subseteq}(a, b) \wedge \text{in}(x, a) \Rightarrow \text{in}(x, b) $$

$$ \forall a^t, b^t, x^t : \{\text{in}(x, \text{cap}(a, b))\} \qquad \text{in}(x, \text{cap}(a, b)) \Leftrightarrow \text{in}(x, a) \wedge \text{in}(x, b) \qquad (\text{Cap}) $$

$$ \forall x^t : \{\text{in}(x, \text{enum}_0)\} \qquad \neg\text{in}(x, \text{enum}_0) \qquad (\text{Empty}) $$

$$ \text{subseteq}(\text{cap}(S, \text{Int}), \text{enum}_0) \qquad (\text{H1}) $$

$$ \text{in}(1, \text{Int}) \qquad (\text{H2}) $$

$$ \text{in}(1, S) \qquad (\text{G}) $$

Despite the modification, the situation has not changed. The axiom (SubseteqIntro) is triggered by `subseteq(cap(S, Int), enum0)`, but this does not make the proof progress.
Formulating the axiom (Subseteq) differently has not solved the issue, but it brought us closer to the solution. We know that (SubseteqElim) is the relevant axiom and we know how it must be instantiated. The expected match is `{a ↦ cap(S, Int), b ↦ enum0, x ↦ 1}`. The terms SMT must know about in order to find this match are `subseteq(cap(S, Int), enum0)` and `in(1, cap(S, Int))`. Only the latter is missing.

The current trigger for (Cap) can be used to generate the definition of `in(x, cap(a, b))` when the term is already known. However, in situations when that term is not known but must be inferred, the axiom is useless. It is then natural to provide a new trigger matching the other side of the equivalence, so that whenever `in(x, a)` and `in(x, b)` are known, `in(x, cap(a, b))` is inferred.

**Example 5.3.3 (Third Attempt).** We add a second trigger to (Cap) and consider the problem

$$ \forall a^t, b^t : \{\text{subseteq}(a, b)\} \qquad (\text{SubseteqIntro}) $$

$$ \forall a^t, b^t, x^t : \{\text{subseteq}(a, b), \text{in}(x, a)\} \qquad (\text{SubseteqElim}) $$

$$ \forall a^t, b^t, x^t : \{\text{in}(x, \text{cap}(a, b))\} \qquad (\text{Cap}) $$

$$ \begin{array}{l} \text{in}(x, \text{cap}(a, b)) \Leftrightarrow \text{in}(x, a) \wedge \text{in}(x, b) \\ \neg \text{in}(x, \text{enum}_0) \end{array} $$

$$ \forall x^t : \{\text{in}(x, \text{enum}_0)\} \qquad (\text{Empty}) $$

$$ \text{in}(1, \text{Int}) \qquad (\text{H2}) $$

$$ \text{in}(1, S) \qquad (\text{G}) $$

The terms `in(1, Int)` and `in(1, S)` form an appropriate match, but so does the term `in(1, S)` by itself (both `a` and `b` are matched to `S`). If the instantiation engine decides to use that match, SMT will generate the fact

$$ \text{in}(1, \text{cap}(S, S)) \Leftrightarrow \text{in}(1, S) \wedge \text{in}(1, S) \qquad (\text{F1}) $$

Then the new term `in(1, cap(S, S))` matches (Cap) again; using this match will result in yet another matching term. Clearly, the new trigger leads to a matching loop.

The trigger `{in(x, a), in(x, b)}` does make the problem solvable, but it may also result in SMT generating too many irrelevant instances. This could make large proof obligations significantly harder to prove in a short amount of time, so we need to avoid this kind of problem. Hopefully, the problem can be fixed by using triggers as *guards*. To ensure no new term of the form `cap(a, b)` is ever introduced in the ground problem, it suffices to only select triggers that include that term.

**Example 5.3.4 (Final Attempt).** This version of the SMT problem is the one we do implement. Only (Cap) has changed compared with the previous version. The solution presented here is not the only possible one; in particular, we could have selected the trigger `{in(x, a), in(x, b), cap(a, b)}`. Our solution does not require both `in(x, a)` and `in(x, b)` to
be known.

$$ \forall a^t, b^t : \{\text{subseteq}(a, b)\} \qquad (\text{SubseteqIntro}) $$

$$ (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(x, b)) \Rightarrow \text{subseteq}(a, b) $$

$$ \forall a^t, b^t, x^t : \{\text{subseteq}(a, b), \text{in}(x, a)\} \qquad (\text{SubseteqElim}) $$

$$ \text{subseteq}(a, b) \wedge \text{in}(x, a) \Rightarrow \text{in}(x, b) $$

$$ \forall a^t, b^t, x^t : \{\text{in}(x, \text{cap}(a, b))\} \qquad (\text{Cap}) $$

$$ \{\text{in}(x, a), \text{cap}(a, b)\} $$

$$ \{\text{in}(x, b), \text{cap}(a, b)\} $$

$$ \text{in}(x, \text{cap}(a, b)) \Leftrightarrow \text{in}(x, a) \wedge \text{in}(x, b) $$

$$ \forall x^t : \{\text{in}(x, \text{enum}_0)\} \qquad \neg\text{in}(x, \text{enum}_0) \qquad (\text{Empty}) $$

$$ \text{subseteq}(\text{cap}(S, \text{Int}), \text{enum}_0) \qquad (\text{H1}) $$

$$ \text{in}(1, \text{Int}) \qquad (\text{H2}) $$

$$ \text{in}(1, S) \qquad (\text{G}) $$

The axiom (Cap) is triggered by the terms in(1, S) and cap(S, Int), resulting in the fact (F1) below. Then the facts (F2) and (F3) are successively introduced as instances of (SubseteqElim) and (Empty). We do not detail the matching terms for those.

$$ \text{in}(1, \text{cap}(S, \text{Int})) \Leftrightarrow \text{in}(1, S) \wedge \text{in}(1, \text{Int}) \qquad (\text{F1}) $$

$$ \text{subseteq}(\text{cap}(S, \text{Int}), \text{enum}_0) \wedge \text{in}(1, \text{cap}(S, \text{Int})) \Rightarrow \text{in}(1, \text{enum}_0) \qquad (\text{F2}) $$

$$ \neg\text{in}(1, \text{enum}_0) \qquad (\text{F3}) $$

The ground problem is now contradictory, therefore the proof is done.

### 5.3.2 General Strategy

We refined our axioms and triggers progressively by inspecting some difficult TLA⁺ obligations and looking for trigger-based solutions. Thus or method for trigger selection is essentially heuristic and does not follow a strict set of rules. Nevertheless, we were able to extract some recurring ideas. In this section, we formulate some key principles behind our strategy for trigger selection. First, we define a few general notions.

We denote by $\vec{x}$ a sequence of variables $x_1, \dots, x_n$. The length $n$ of the sequence is left ambiguous. A sequence of variables annotated by the sort $s$ is written $\vec{x}^s$. Our axioms are all of the form

$$ \forall \vec{x}^t : \{p_1, \dots, p_n\} \phi $$

where $\phi$ is without weak quantifiers. For all terms $t$, let Terms($t$) be the collection of all first-order subterms of $t$ (including $t$ itself). For a given axiom with a trigger as noted above, the terms generated by the trigger are the elements of the collection

$$ \text{Terms}(\phi) \setminus \bigcup_{1 \le i \le n} \text{Terms}(p_i) $$

By inspecting the terms in that collection, we can predict what kinds of terms an instance may introduce into the ground problem.
**Example 5.3.5.** Consider again the axiom for the intersection of two sets:

$$ \forall a^t, b^t, x^t : \mathbf{in}(x, \mathbf{cap}(a, b)) \Leftrightarrow \mathbf{in}(x, a) \wedge \mathbf{in}(x, b) $$

Here are the four triggers we considered and the set of terms each generates:

<table><tr><td>{in(x, cap(a, b))}</td><td>generates</td><td>in(x, a), in(x, b)</td></tr><tr><td>{in(x, a), in(x, b)}</td><td>generates</td><td>in(x, cap(a, b)), cap(a, b)</td></tr><tr><td>{in(x, a), cap(a, b)}</td><td>generates</td><td>in(x, cap(a, b)), in(x, b)</td></tr><tr><td>{in(x, b), cap(a, b)}</td><td>generates</td><td>in(x, cap(a, b)), in(x, a)</td></tr></table>

Borrowing the terminology of Leino [50], we call *adequate* a trigger that mentions all quantified variables, and *parsimonious* a trigger {$p_1, \dots, p_n$} that becomes inadequate when any $p_i$ is removed. Adequacy is a strict requirement of SMT. Parsimony captures the notion of a most general trigger: a nonparsimonious trigger can be simplified into another trigger that matches more often.

Example 5.3.5 above presents the four triggers for cap that are both adequate and parsimonious. Of these four triggers, only the one generating the term cap(a, b) has been rejected, because it results in an obvious matching loop. The remaining triggers only generate terms that have in as a top connective. Besides the matching loop, we make the following observation: it is generally useful to generate new facts of the form in(t₁, t₂) where t₁ and t₂ are known, because it may lead to discover some implicit connexions between the different sets involved in a proof; on the contrary, we can hypothesize that many TLA⁺ obligations do not require inventing sets that are not already mentioned in the obligation's statement, so generating terms of the form cap(t₁, t₂) is not as useful.

We found helpful to classify the operators of TLA⁺ as either *constructors* or *accessors*. Intuitively, constructors (like cap) build complex objects from simpler ones, and accessors (like in) give information about the objects they are applied to. We assume typical valid TLA⁺ obligations can be proved without mentioning objects (sets, functions, etc.) that are not already mentioned in the obligation; thus we avoid generating terms C(t₁, ..., tₙ) where C is a constructor. We also encourage the generation of specific terms A(t₁, ..., tₙ) where A is an accessor.

We may now formulate our general strategy for selecting triggers:

I Only axioms of the form $\forall \vec{x}^t : \phi$ where $\phi$ is without weak quantifiers are considered. Axioms are reformulated and sometimes split to obtain that form.

II To select triggers, we start from the set of adequate and parsimonious triggers that can be formulated using only subterms of $\phi$.

III We reject a trigger if it generates a term $C(t_1, \dots, t_n)$ where C is a constructor, or if it contains two terms with no variable in common.

IV For all terms $A(t_1, \dots, t_n)$ in $\phi$ where A is an accessor, we look if the term is generated by at least one trigger. If not, and if generating $A(t_1, \dots, t_n)$ is important for some proofs, we consider adding a nonparsimonious trigger.

The third principle reduces the risk of generating irrelevant terms and prevents matching loops. The fourth principle increases the chances of generating the terms necessary to a proof.
$$ \forall a^t, x^t : \{\text{in}(x, \text{union}(a))\} \qquad (\text{UnionElim}) \\ \qquad \text{in}(x, \text{union}(a)) \Rightarrow \exists y^t : \text{in}(x, y) \land \text{in}(y, a) $$

$$ \begin{array}{l} \forall a^t, x^t, y^t : \{\text{in}(y, a), \text{in}(x, \text{union}(a))\} \\ \qquad \{\text{in}(x, y), \text{in}(x, \text{union}(a))\} \\ \qquad \{\text{in}(x, y), \text{in}(y, a), \text{union}(a)\} \\ \qquad \text{in}(x, y) \land \text{in}(y, a) \Rightarrow \text{in}(x, \text{union}(a)) \end{array} \qquad (\text{UnionIntro}) $$

<caption>Figure 5.2: Axioms for UNION</caption>

For the rest of this section, we illustrate how these principles are applied to the axioms of set theory and functions for TLA$^+$. Integer arithmetic will be dealt with elsewhere (Section 5.4.2) as it involves using SMT's native arithmetic. Other fragments of TLA$^+$'s theory (tuples, records, sequences...) are based on the axioms of functions. For the full list of axioms used in the SMT encoding, we refer the reader to Appendix C.

## Set Theory

The following operators of ZF set theory are considered to be constructors: `enum_n`, `union`, `subset`, `setst_P`, `setof_F`, `cup`, `cap`, `diff`. The only accessor is the membership relation `in`. The following pattern is shared by many axioms of set theory:

$$ \forall \vec{a}^t, x^t : \text{in}(x, C(\vec{a})) \Leftrightarrow \phi(x, \vec{a}) \qquad (\text{C-Define}) $$

where $C$ is a constructor. When the defining formula $\phi$ contains quantifiers, we split the axiom in two, resulting in a *introduction* and an *elimination* axioms:

$$ \forall \vec{a}^t, x^t, \vec{y}^t : \text{in}(x, C(\vec{a})) \Rightarrow \phi_1(x, \vec{a}, \vec{y}) \qquad (\text{C-Elim}) $$

$$ \forall \vec{a}^t, x^t, \vec{y}^t : \phi_2(x, \vec{a}, \vec{y}) \Rightarrow \text{in}(x, C(\vec{a})) \qquad (\text{C-Intro}) $$

The formula $\phi_1$ may contain strong quantifiers. The formula $\phi_2$ may contain weak quantifiers (which are strong for the axiom as a whole, since $\phi_2$ occurs on the left of an implication).

To illustrate, we take the example of the TLA$^+$ operator `UNION`, which we denote `union`. Our axioms are displayed in Figure 5.2. The basic form of the axiom is

$$ \forall a^t, x^t : \text{in}(x, \text{union}(a)) \Leftrightarrow \exists y^t : \text{in}(x, y) \land \text{in}(y, a) $$

The defining formula is an existential statement, so the axiom is split in two. The existential quantifier is still present in the elimination part; in the introduction part, it is moved at the front as a universal quantifier.

Axiom (UnionElim) receives only one trigger, $\{\text{in}(x, \text{union}(a))\}$. This is the only adequate trigger possible. We could apply Skolemization to the formula to have more candidate triggers. However, Skolem terms do not occur in the starting ground problem, so it is unclear if triggers
$$ \forall c_1^t, \dots, c_n^t, a^t : \{\mathit{fcn}_F(a, c_1, \dots, c_n)\} \qquad (\mathit{FcnIsafcn}) \\ \phantom{\forall c_1^t, \dots, c_n^t, a^t : \{\mathit{fcn}_F(a, c_1, \dots, c_n)\}} \mathit{isafcn}(\mathit{fcn}_F(a, c_1, \dots, c_n)) $$

$$ \forall c_1^t, \dots, c_n^t, a^t : \{\mathit{fcn}_F(a, c_1, \dots, c_n)\} \qquad (\mathit{FcnDom}) \\ \mathit{domain}(\mathit{fcn}_F(a, c_1, \dots, c_n)) = a $$

$$ \forall c_1^t, \dots, c_n^t, a^t, x^t : \{\mathit{fcnapp}(\mathit{fcn}_F(a, c_1, \dots, c_n), x)\} \qquad (\mathit{FcnApp}) \\ \{\mathit{in}(x, a), \mathit{fcn}_F(a, c_1, \dots, c_n)\} $$

$$ \mathit{in}(x, a) \Rightarrow \mathit{fcnapp}(\mathit{fcn}_F(a, c_1, \dots, c_n), x) = F(x, c_1, \dots, c_n) $$

<caption>Figure 5.3: Axioms for Functions</caption>

that mention such terms will generate relevant instances. In general, we do not Skolemize our axioms.

Axiom (UnionIntro) is an interesting case. The first two triggers are parsimonious. Other parsimonious triggers are

$$ \{\mathit{in}(x, y), \mathit{in}(y, a)\} \\ \{\mathit{in}(x, y), \mathit{union}(a)\} $$

We reject the first one because it generates union(a), and the second one because the terms in(x, y) and union(a) have no variable in common (there are too many ways to match it).

The triggers we kept both mention the term in(x, union(a)), so they can never generate this term. For the introduction axioms of set theory, we found that many obligations relied on the implicit inference of such facts. Consider for instance

$$ x \in y \land y \in S \land \mathit{UNION} S \subseteq T \Rightarrow x \in T $$

The fact $x \in \mathit{UNION} S$ follows from the assumptions, but it is not mentioned explicitly. The third trigger is added to handle this kind of obligations:

$$ \{\mathit{in}(x, y), \mathit{in}(y, a), \mathit{union}(a)\} $$

Note that it is not parsimonious.

In general, for all axioms of the form (C-Define), (C-Elim) or (C-Intro), all selected triggers contain either in(x, C(ā)) or C(ā). This ensures no term C(ā) is ever generated. Furthermore, for axioms of the form (C-Define) and (C-Intro), we ensure at least one trigger generates the term in(x, C(ā)). In most cases, this is already done by a parsimonious trigger. (UnionIntro) is the only exception among the axioms of ZF set theory.

## Functions

TLA⁺'s theory of functions involves the following primitive constructs:

$$ [x \in S \mapsto F(x)], \quad \mathit{DOMAIN} f, \quad f[x], \quad [S \to T] $$
These constructs are respectively noted using the operators $fcn_F$, domain, fcnapp and arrow. The operator $fcn_F$ is rather a family of operators parameterized by the higher-order argument $F$. We treat it as a constructor. The operators domain and fcnapp are accessors. Internally, the class of all functions is specified by a predicate `isafcn`, which is not accessible in the user language. We treat it as an accessor. The operator arrow is a constructor specified by an axiom of the form (C-Define).

Let us focus first on the specification of explicit functions with their domains and values. They are specified by three axiom schemas, presented in Figure 5.3. The subject of axiom schemas will be treated in more details in the next section. Each of the three schemas specifies the return value of some accessor for an explicit function as input. To clarify using TLA⁺'s notations:

* (FcnIsafcn) specifies `isafcn([y ∈ a ↦→ F(y)])` to be true in all cases;

* (FcnDom) specifies `DOMAIN [y ∈ a ↦→ F(y)]` to be $a$ in all cases;

* (FcnApp) specifies `[y ∈ a ↦→ F(y)][x]` to be $F(x)$ under the condition $x ∈ a$.

In general, each axiom gives the definition of some term $A(C(\vec{a}), \vec{x})$ under an optional condition $\phi$. Thus all the axioms of Figure 5.3 fall under the pattern

$$ \forall \vec{a}^t, \vec{x}^t : \phi(\vec{a}, \vec{x}) \Rightarrow A(C(\vec{a}), \vec{x}) = t(\vec{a}, \vec{x}) \quad (\text{C-A-Define}) $$

where $C$ is a constructor, $A$ an accessor, $\phi$ a formula and $t$ a term. The constructor $C$ is $fcn_F$ for the three schemas. $\phi$ is just `TRUE` for (FcnIsafcn) and (FcnDom)

It is helpful to consider the general form (C-A-Define), because this form is also applicable to the axioms of tuples, records and sequences. These theories introduce new constructors, but also reuse the accessors `isafcn`, `domain` and `fcnapp`.

We describe our strategy for the general axiom. Triggers that do not generate a term $C(\vec{a})$ can be of two sorts; some mention the term $C(\vec{a})$, some mention the term $A(C(\vec{a}), \vec{x})$. When the list of variables $\vec{x}$ is empty, the simple trigger $\{C(\vec{a})\}$ is already adequate and parsimonious, so we just select this one; the axioms (FcnIsafcn) and (FcnDom) fall under this case. If $\vec{x}$ is not empty, then $\{A(C(\vec{a}), \vec{x})\}$ is adequate and parsimonious, so we select it. In the case of (FcnApp), this corresponds to the trigger

$$ \{fcnapp(fcn_F(a, c_1, \dots, c_n), x)\} $$

It is also desirable to select triggers that generate the term $A(C(\vec{a}), \vec{x})$. We also look for parsimonious triggers that contain $C(\vec{a})$. This must be done on a case by case basis for every axiom. Typically, adequate triggers are obtained by selecting subterms from the condition formula $\phi$. In the case of (FcnApp), we select

$$ \{\text{in}(x, a), fcn_F(a, c_1, \dots, c_n)\} $$

We do not look for subterms in $F(x, c_1, \dots, c_n)$, even though there might be more parsimonious triggers to select from those subterms. This is a limitation of our implementation, as we have not gone as far as implementing a procedure for selecting triggers automatically.

Lastly, the operator arrow is treated as a set constructor, and its axiom falls under the general form (C-Define). The axiom is split into an introduction and elimination axioms, and
triggers are selected for it as we described before. Consider the introduction part:

$$ 
\begin{array}{l}
\forall a^t, b^t, f^t : \{\text{in}(f, \text{arrow}(a, b))\} \qquad (\text{ArrowIntro}) \\
\quad \wedge \text{isafcn}(f) \\
\quad \wedge \text{domain}(f) = a \\
\quad \wedge (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(\text{fnapp}(f, x), b)) \\
\quad \Rightarrow \text{in}(f, \text{arrow}(a, b))
\end{array}
$$

This axiom is lacking a trigger to generate in(f, arrow(a, b)). The two parsimonious triggers below do generate this term:

$$ 
\begin{array}{l}
\{\text{isafcn}(f), \text{arrow}(a, b)\} \\
\{\text{domain}(f), \text{arrow}(a, b)\}
\end{array}
$$

But we reject them because they both feature two terms with no variable in common; any of these triggers would lead SMT to match all functions with all sets of functions mentioned in the problem.

Our solution for generating in(f, arrow(a, b)) comes in the form of a new axiom:

$$ 
\begin{array}{l}
\forall c_1^t, \dots, c_n^t, a^t, b^t : \{\text{fnf}_F(a, c_1, \dots, c_n), \text{arrow}(a, b)\} \qquad (\text{FnTyping}) \\
(\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(F(x, c_1, \dots, c_n), b)) \Rightarrow \text{in}(\text{fnf}_F(a, c_1, \dots, c_n), \text{arrow}(a, b))
\end{array}
$$

To clarify using TLA⁺'s notations, this axiom allows us to prove $[x \in a \mapsto F(x)] \in [a \to b]$ when the condition $\forall x : x \in a \Rightarrow F(x) \in b$ is verified. It complements the introduction axiom for arrow by taking advantage of the fact that explicit functions with domain $a$ are good candidates for the elements of a set $[a \to b]$.

The axiom (FnTyping) exemplifies another recurrent pattern in our axiomatization, which is

$$ \forall \vec{a}^t, \vec{b}^t, \vec{c}^t : \phi(\vec{a}, \vec{b}, \vec{c}) \Rightarrow \text{in}(C(\vec{a}, \vec{b}), D(\vec{a}, \vec{c})) \qquad (\text{C-Typing}) $$

where $C$ is a constructor, $D$ a set constructor, and $\phi$ a formula. Typing axioms are pervasive in the theories of tuples, records and sequences. When $\vec{a}$ is nonempty, the trigger

$$ \{C(\vec{a}, \vec{b}), D(\vec{a}, \vec{c})\} $$

is a good option: the fact that one variable of the list $\vec{a}$ must be present in the two terms matching the pattern ensures less irrelevant instances are considered. When $\vec{a}$ is empty, this is not the case anymore, so we select triggers differently. Typically, the triggers selected mention $C(\vec{b})$ and some subterm of $\phi$ containing $D(\vec{c})$ and a variable of $\vec{b}$. Some good examples of this are found in the theory of sequences. A set of sequences is noted Seq($a$) and the concatenation of two sequences $s$ and $t$ is noted Cat($s, t$). The typing axiom for Cat is

$$ 
\begin{array}{l}
\forall a^t, s^t, t^t : \{\text{in}(s, \text{Seq}(a)), \text{Cat}(s, t)\} \qquad (\text{CatTyping}) \\
\quad \{\text{in}(t, \text{Seq}(a)), \text{Cat}(s, t)\} \\
\quad \text{in}(s, \text{Seq}(a)) \wedge \text{in}(t, \text{Seq}(a)) \Rightarrow \text{in}(\text{Cat}(s, t), \text{Seq}(a))
\end{array}
$$
$$
\begin{array}{l}
\text{For all } P : \iota^{n+1} \to o, \\
\quad \forall c_1^\iota, \dots, c_n^\iota, a^\iota, x^\iota : \left\{
\begin{array}{@{}l@{}}
  \mathbf{in}(x, \mathbf{setst}_P(a, c_1, \dots, c_n)) \\
  \phantom{\mathbf{in}(x, \mathbf{setst}_P(a, c_1, \dots, c_n))} \\
  \mathbf{in}(x, a), \mathbf{setst}_P(a, c_1, \dots, c_n)
\end{array}
\right\} \\
\quad \mathbf{in}(x, \mathbf{setst}_P(a, c_1, \dots, c_n)) \Leftrightarrow \mathbf{in}(x, a) \wedge P(x, c_1, \dots, c_n)
\end{array}
\qquad (\mathbf{SetstDef})
$$

<caption>Figure 5.4: Axiom Schema for Set Comprehension</caption>

5.4 Other Topics in the SMT Axiomatization

Some fragments of the axiomatization are handled in a particular way. This section provides
more details on the topics of axiom schemas, integer arithmetic and set extensionality. Most
of these extensions involve simple transformations on proof obligations, so we will indicate
how they are implemented.

5.4.1 Axiom Schemas

The following primitive operators of TLA⁺ are specified by one or several axiom schemas:
choose, setst, setof and fcn. For the encoding into HOL, we could simply declare the second-
order operator and the full schema as a second-order axiom, for instance:

$$
\forall P^{\iota \to o}, a^{\iota}, x^{\iota} : \mathbf{in}(x, \mathbf{setst}(a, P)) \Leftrightarrow \mathbf{in}(x, a) \Rightarrow P(x)
$$

The principle is the same for each operator, so we will focus on **setst** for our examples.

A reduction to FOL is achieved by replacing every occurrence **setst**(a, P) by a first-order term **setst**<sub>P</sub>(a, c<sub>1</sub>, . . . , c<sub>n</sub>), where **setst**<sub>P</sub> is a new symbol and c<sub>1</sub>, . . . , c<sub>n</sub> are parameters that encode the context in which the original term occurs. The operator **setst**<sub>P</sub> is specified by the particular instance of the set comprehension schema for P. See Figure 5.4 for the first-order axiom schema used by the SMT encoding, triggers included.

**Example 5.4.1.** Consider the TLA⁺ formula

$$
\exists n : \{p \in \mathit{Int} : p \neq n\} \neq \mathit{Int}
$$

In HOL, the instance of set comprehension above is written **setst**(Int, λp : p ≠ n). The higher-
order argument is λp : p ≠ n. It includes the variable n, which is bound by a quantifier in
the formula. When writing the relevant instance of the comprehension schema, we cannot
reference n, because it is bound locally. Therefore, we will use a parameter to pass n as an
argument in the encoded term.

We declare **setst**<sub>P</sub> : ι × ι → ι and specify it with the axiom

$$
\forall n^\iota, a^\iota, x^\iota : \mathbf{in}(x, \mathbf{setst}_P(a, n)) \Leftrightarrow \mathbf{in}(x, a) \wedge x \neq n
$$

The original formula is encoded as

$$
\exists n^t : \mathbf{setst}_P(\mathbf{Int}, n) \neq \mathbf{Int}
$$
In general, we must at least make parameters $c_1, \dots, c_n$ for the free variables of $P$ that are bound by a quantifier. However, implementing this naively, we will find that many easy proof obligations have become much harder to solve. Consider the formula

$$ \exists n : \{p \in \mathit{Int} : p \neq n\} = \{p \in \mathit{Int} : p \neq 1 + 1\} $$

The set on the left is the same as in example 5.4.1. The set on the right has a different higher-order argument $Q$, which does not include the variable $n$. Applying the procedure we just described results in the formula

$$ \exists n^t : \mathit{setst}_P(\mathit{Int}, n) = \mathit{setst}_Q(\mathit{Int}) $$

which is still provable, but only by invoking set extensionality, whereas the original obligation seems trivial by instantiating $\exists n$ with $1+1$.

To fix this particular example, we can reuse the symbol $\mathit{setst}_P$ to encode the other set as $\mathit{setst}_P(\mathit{Int}, 1+1)$. In general, when treating an occurrence $\mathit{setst}(a, \lambda x : e)$, we can anticipate reuses by selecting the most general lambda-expression $P$ such that $\lambda x : e$ is an instance of $P$. For $\lambda p : p \neq 1+1$, we can choose $\lambda p : p \neq x$ where $x$ is any variable other than $p$. The same lambda-expression works for $\lambda p : p \neq n$, which shows the two lambda-expressions have the same “shape”. Let us now make this idea more formal.

**Definition 5.4.2.** An instance of a lambda-expression $f$ is any lambda-expression $f\sigma$ for a substitution $\sigma$. The *matrix* of a lambda-expression $f$ is an $m$ such that $f$ is an instance of $m$, and if $f$ is an instance of another $m'$ then $m'$ is an instance of $m$.

Notice that it would not be very useful to generalize the definition above to expressions. The matrix of any $e$ would just be $x$ for the substitution $\{x \mapsto e\}$. For a lambda-expression $\lambda x_1, \dots, x_n : e$, the matrix has to be a lambda-expression $\lambda x_1, \dots, x_n : e'$ such that $e = e'\sigma$ and no $x_i$ is in the domain or the range of $\sigma$. This follows from the definition and the fact that we assume $\sigma$ to be compatible with the lambda-expression.

**Proposition 5.4.3.** *The matrix $m$ of a lambda-expression $f$ is unique up to renaming of free variables. Furthermore, every free variable of $m$ has exactly one occurrence.*

*Proof.* Suppose $m_1$ and $m_2$ are two matrices of $f$. By definition, $m_1$ and $m_2$ must be instances of each other. Let $\sigma_1$ and $\sigma_2$ such that $m_1 = m_2\sigma_2$ and $m_2 = m_1\sigma_1$. We have $m_1 = m_1\sigma_1\sigma_2$. The composite substitution $\sigma_1\sigma_2$ is the identity, so clearly $\sigma_1$ and $\sigma_2$ are just renamings of free variables.

If $m$ has a free variable $x$ that occurs more than once, then $m$ cannot be a matrix, because it is easy to construct a $m'$ such that $m$ is an instance of $m'$ but not the converse. Simply define $m'$ by replacing every occurrence of $x$ in $m$ by a distinct variable $y_i$. Then $m$ is an instance of $m'$ for $\{y_1 \mapsto x, y_2 \mapsto x, \dots\}$. $\square$

It remains to prove the existence of matrices for all lambda-expressions. Consider the algorithm presented in Figure 5.5. If $\sigma$ and $\rho$ are substitutions with disjoint domains then $\sigma \uplus \rho$ is their union. $\emptyset$ also denotes the unique substitution whose domain is empty. To simplify the presentation, we omit all sort annotations. The input expression $e$ is assumed to be without second-order applications, because during preprocessing all second-order applications are rewritten from the bottom up.
$$
\begin{align*}
& \text{abstract}(e, X, \sigma) := \begin{cases} (v, \sigma \uplus \{v \mapsto e\}) & \text{if } \text{FV}(e) \cap X = \emptyset \text{ with } v \notin X \cup \text{Dom}(\sigma) \\ \text{visit}(e, X, \sigma) & \text{otherwise} \end{cases} \\
& \text{visit}(x, X, \sigma) := (x, \sigma) \\
& \text{visit}(K(e_1, \dots, e_n), X, \sigma) := \begin{cases} \sigma_0 := \sigma & \text{and } (e'_i, \sigma_i) := \text{abstract}(e_i, X, \sigma_{i-1}) \text{ for } 1 \le i \le n \text{ in } \\ & (K(e'_1, \dots, e'_n), \sigma_n) \end{cases} \\
& \text{visit}(e_1 = e_2, X, \sigma) := \begin{cases} \text{let } (e'_1, \sigma_1) := \text{abstract}(e_1, X, \sigma) & \text{in} \\ \text{let } (e'_2, \sigma_2) := \text{abstract}(e_2, X, \sigma_1) & \text{in} \\ (e'_1 = e'_2, \sigma_2) \end{cases} \\
& \text{visit}(e_1 \Rightarrow e_2, X, \sigma) := \begin{cases} \text{let } (e'_1, \sigma_1) := \text{abstract}(e_1, X, \sigma) & \text{in} \\ \text{let } (e'_2, \sigma_2) := \text{abstract}(e_2, X, \sigma_1) & \text{in} \\ (e'_1 \Rightarrow e'_2, \sigma_2) \end{cases} \\
& \text{visit}(\forall x : e, X, \sigma) := \begin{cases} \text{let } (e', \sigma_1) := \text{abstract}(e, X \cup \{x\}, \sigma) & \text{in} \\ (\forall x : e', \sigma_1) \end{cases} \\
& \text{matrix}(e, X) ::= \text{abstract}(e, X, \emptyset)
\end{align*}
$$

<caption>Figure 5.5: Matrix Algorithm</caption>

We admit the algorithm is correct in the following sense: if $(e', \sigma) = \text{matrix}(e, \{x_1, \dots, x_n\})$ then $\lambda x_1, \dots, x_n : e'$ is the matrix of $\lambda x_1, \dots, x_n : e$ for the substitution $\sigma$. The idea of the algorithm is to build $\sigma$ incrementally while parsing the input expression from the top down. When a subterm does not contain any variable from $X$, it is replaced by a fresh variable and $\sigma$ is updated.

We now describe how the implementation of the axiomatization phase must be modified. During this phase, the proof obligation $\Gamma \vdash e$ is parsed; for all primitive operators encountered, a declaration and axioms are inserted in the sequent. The final sequent has the form $\Delta, \Gamma \vdash e$ where $\Delta$ contains the additional declarations and axioms. We focus now on the case where a second-order application is encountered:

$$
K(e_1, \dots, \lambda x_1, \dots, x_n : e, \dots, e_n)
$$

If the higher-order argument is a symbol *F* instead, we treat it as $\lambda x_1, \dots, x_n : F(x_1, \dots, x_n)$, where *n* is the arity of *F*. Let $(e', \sigma)$ be the result of the call *matrix*(e, {*x*₁, ..., *x*ₙ}). Then the original application is replaced by

$$
K_{e'}(e_1, \dots, \sigma(v_1), \dots, \sigma(v_m), \dots, e_n)
$$

where {$v_1, \dots, v_m$} is the domain of $\sigma$. The operator $K_{e'}$ may have been declared already, in which case we resume parsing the sequent. Otherwise, we need to make a declaration for $K_{e'}$ and insert its axioms, if there are any.

An axiom schema for *K* is a formula *φ* parameterized by an operator *F* such that *φ*
contains at least one occurrence of *K*, and all applications of *K* are of the form

$$
K(e_1, \dots, F, \dots, e_n)
$$
$$ \forall z^{\text{int}} : \{\text{cast}_{\text{int}}(z)\} \qquad z = \text{proj}_{\text{int}}(\text{cast}_{\text{int}}(z)) \qquad (\text{CastIntInjective}) $$

$$ \forall z^{\text{int}} : \{\text{cast}_{\text{int}}(z)\} \qquad \text{in}(\text{cast}_{\text{int}}(z), \text{Int}) \qquad (\text{IntIntro}) $$

$$ \forall x^{\iota} : \{\text{in}(x, \text{Int})\} \qquad \text{in}(x, \text{Int}) \Rightarrow x = \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x)) \qquad (\text{IntElim}) $$

$$ \forall z_1^{\text{int}}, z_2^{\text{int}} : \{\text{plus}(\text{cast}_{\text{int}}(z_1), \text{cast}_{\text{int}}(z_2))\} \qquad \text{plus}(\text{cast}_{\text{int}}(z_1), \text{cast}_{\text{int}}(z_2)) = \text{cast}_{\text{int}}(z_1 +_{\text{int}} z_2) \qquad (\text{PlusTyping}) $$

<caption>Figure 5.6: Axioms for Integer Arithmetic (Addition Only)</caption>

The first-order instance of $\phi$ for $K_{e'}$ is the formula $\forall v_1, \dots, v_m : \phi'$ where $\phi'$ is obtained from $\phi$ by replacing all applications of $K$ like the one above by

$$ K_{e'}(e_1, \dots, v_1, \dots, v_m, \dots, e_n) $$

The top context $\Delta$ is updated with the declaration of $K_{e'}$ (its type is easy to infer from the type of $K$ and the sorts of the variables in $\text{Dom}(\sigma)$) and the appropriate instances for all axiom schemas associated with $K$.

## 5.4.2 Integer Arithmetic

Reasoning modulo theory is a strength of SMT. We want to leverage SMT's native support for integer arithmetic to handle the TLA$^+$ obligations that involve this theory. Our encoding so far has only dealt with one sort $\iota$ besides the Boolean sort, so no term is encoded into `int`. We present now an extension of the axiomatic theory that effectively links SMT's and TLA$^+$'s arithmetics.

SMT's integer arithmetic is characterized by a sort `int`, several primitive operators like addition `+` `int`: `int` `x` `int` `->` `int`, and a specific interpretation of `int` and the primitive operators on it. TLA$^+$, in comparison, defines integers as the elements of the set `Int` and specifies operators like `+` axiomatically. Despite the differences between the two languages, the idea is still to define a homomorphism between their respective arithmetical structures. Concretely, we declare a new operator `cast` `int`: `int` `->` $\iota$ that is injective and ranges over the elements of `Int`. We then introduce axioms to link the operators of TLA$^+$ with their counterparts in SMT if they have one.

The axioms are displayed in Figure 5.6. Besides `cast` `int`, we provide the new operator `proj` `int`: $\iota$ `->` `int`. `cast` `int` is specified as a surjective operator from $\iota$ to the subdomain of $\iota$ characterized by the predicate $x \in \text{Int}$ (axioms (`IntIntro`) and (`IntElim`). It is specified as injective by (`CastIntInjective`). Indeed, if `cast` `int`(m) = `cast` `int`(n) for some m, n: `int`, then m = `proj` `int`(`cast` `int`(m)) = `proj` `int`(`cast` `int`(n)) = n. Compare (`CastIntInjective`) with the more natural expression of injectivity with its obvious trigger:

$$ \forall z_1^{\text{int}}, z_2^{\text{int}} : \{\text{cast}_{\text{int}}(z_1), \text{cast}_{\text{int}}(z_2)\} \quad \text{cast}_{\text{int}}(z_1) = \text{cast}_{\text{int}}(z_2) \Rightarrow z_1 = z_2 $$

Suppose there are $N$ known terms `cast` `int`(n) at a given time while SMT solves an obligation. The axiom above will generate $N^2$ different instances—one per couple of terms. The axiom (`CastIntInjective`) will only generate $N$.
The axiom (PlusTyping) establishes the homomorphic relation between TLA⁺'s addition (which is noted plus) and SMT's +<sub>int</sub>. It is easily generalized to the other operators of TLA⁺ for integer arithmetic: unary and binary subtraction, multiplication, quotient and remainder, and the comparison relation. We could apply the same principle to numerical constants, which would lead to trivial axioms such as

$$1 = \mathit{cast}_{\mathit{int}}(1_{\mathit{int}})$$

where 1 is the TLA⁺ constant and 1<sub>int</sub> the interpreted SMT constant. It is much simpler to just rewrite 1 as cast<sub>int</sub>(1<sub>int</sub>) in proof obligations, so that is what we implement during the axiomatization phase. For quotient and remainder, we must restrict the axiom to positive integers for the second argument, as the operators are unspecified in TLA⁺ otherwise:

$$\forall z_1^{\text{int}}, z_2^{\text{int}} : \{\text{div}(\text{cast}_{\text{int}}(z_1), \text{cast}_{\text{int}}(z_2))\} \\ z_2 >_{\text{int}} 0_{\text{int}} \Rightarrow \text{div}(\text{cast}_{\text{int}}(z_1), \text{cast}_{\text{int}}(z_2)) = \text{cast}_{\text{int}}(z_1 \div_{\text{int}} z_2)$$

Without the condition z₂ ><sub>int</sub> 0<sub>int</sub>, we would be able to prove 1 ÷ 0 ∈ Int and 1 ÷ (-1) ∈ Int, which are both unprovable in TLA⁺.

**Theorem 5.4.4.** The extension of the axiomatic theory for including SMT's arithmetic is sound.

*Proof.* The axioms (CastIntInjective), (IntIntro) and (IntElim) essentially declare cast<sub>int</sub> as a bijection between the domain of int and the elements of TLA⁺'s domain that are members of Int. The two collections have the same cardinality so there must be such a bijection. The axiom (PlusTyping) essentially states that TLA⁺'s interpretation of plus on the elements of Int coincides with SMT's interpretation of +<sub>int</sub>, which we assume to be true. □

**Example 5.4.5.** To see how the axioms work in practice, we demonstrate with the theorem

$$\forall x : x \in \mathit{Int} \Rightarrow x + 0 = x$$

We assume a constant x : ι is declared and derive a contradiction from the assumptions

$$\text{in}(x, \mathit{Int}) \qquad (\text{H})$$

$$\text{plus}(x, \text{cast}_{\text{int}}(0_{\text{int}})) \neq x \qquad (\text{G})$$

Here is the sequence of relevant instances that are generated from this starting set:

$$\text{in}(x, \mathit{Int}) \Rightarrow x = \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x)) \qquad \text{by (IntElim)} \qquad (\text{F1})$$

$$\text{plus}(\text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x)), \text{cast}_{\text{int}}(0_{\text{int}})) = \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x) +_{\text{int}} 0_{\text{int}}) \qquad \text{by (PlusTyping)} \qquad (\text{F2})$$

The fact (F1) is the instance of (IntElim) triggered by the term in(x, Int). After the insertion of (F1), the equality x = cast<sub>int</sub>(proj<sub>int</sub>(x)) can be derived by ground reasoning, so the subterm plus(x, cast<sub>int</sub>(0<sub>int</sub>)) from (G) becomes a match for the axiom (PlusTyping), resulting in the new fact (F2). The final problem is contradictory, as shown by the following equalities:

$$\begin{align*}
\text{plus}(x, \text{cast}_{\text{int}}(0_{\text{int}})) &= \text{plus}(\text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x)), \text{cast}_{\text{int}}(0_{\text{int}})) \\
&= \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x) +_{\text{int}} 0_{\text{int}}) \qquad \text{by (F2)} \\
&= \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(x)) \qquad \text{by SMT's arithmetic} \\
&= x
\end{align*}$$

But plus(x, cast<sub>int</sub>(0<sub>int</sub>)) ≠ x by (G).
$$ \forall x^t, y^t : \{\text{invokeSetExt}(x, y)\} $$

$$ \forall x^t, y^t : \{\text{setEquals}(x, y)\} $$

$$ \forall x^t, y^t : \{\text{setEquals}(x, y)\} $$

$$ (\forall z^t : \text{in}(z, x) \Leftrightarrow \text{in}(z, y)) \Rightarrow x = y $$

$$ \text{setEquals}(x, y) \Leftrightarrow x = y $$

$$ \text{invokeSetExt}(x, y) $$

(SetExt)

(SetEqualsDef)

(InvokeSetExt)

<caption>Figure 5.7: Set Extensionality Axioms for SMT</caption>

### 5.4.3 Set Extensionality

Some obligations cannot be solved without the axiom of set extensionality:

$$ \forall x, y : (\forall z : z \in x \Leftrightarrow z \in y) \Rightarrow x = y $$

The axiom applies to every object in the universe of set theory. We know from experience that SMT solvers are unable to infer the relevant instances of set extensionality without triggers; but there is no obvious trigger to choose for the axiom. However, in many cases, the relevant equality to prove by extensionality occurs explicitly in the obligation. For example:

$$ \text{ASSUME NEW } S, \text{ NEW } T $$

$$ \text{PROVE } S \cup T = T \cup S $$

A less trivial example may be found at the end of the Paxos proof in the distribution of TLAPS (we modified the names and removed irrelevant facts):

$$ \text{ASSUME NEW } S, \text{ NEW } T, $$

$$ S \subseteq T \land S \neq T, $$

$$ \forall x, y \in T : x = y $$

$$ \text{PROVE } S = \emptyset $$

Here is the intuitive proof: $T$ is either empty or a singleton set; $S$ is a proper subset of $T$, so it can only be empty. Set extensionality must be invoked twice to prove the goal: one time to use $S \neq T$, the other to prove $S = \emptyset$.

The idea then is to let equalities found in the obligation trigger the axiom of set extensionality. This cannot be implemented in the form of a trigger $\{x = y\}$, because the symbol $=$ is interpreted by SMT. The solution is the set of axioms of Figure 5.7. Two new binary predicates `invokeSetExt` and `setEquals` are introduced. The axiom (`SetEqualsDef`) specifies `setEquals` as an alias for `=`. The operator `invokeSetExt` is not specified by anything; it is just used to control the instantiation of (`SetExt`). The axiom (`InvokeSetExt`) is a rule: it is triggered when an equality `setEquals(x, y)` is found; its only effect is to introduce `invokeSetExt(x, y)` into the ground problem, triggering (`SetExt`) right after.

To make this solution work, relevant equalities in the PO must be rewritten:

$$ x = y \triangleright \text{setEquals}(x, y) \quad \text{in positive contexts when } x \text{ or } y \text{ is a set} $$

The two conditions are heuristics to aim for more relevant instances of set extensionality. A *polarity* is assigned to every subexpression in the standard way: the top expression is positive;
the polarity is reversed when going down a negation, or left of an implication, and for the hypotheses of a sequent. A subexpression is in a positive context if its polarity is positive. Here is an example of an expression with an equality in a negative context:

$$ \forall x, y : x = \emptyset \Rightarrow y \notin x $$

The subexpression $x = \emptyset$ will not be rewritten; there is no need to in order to prove that the expression is valid. The second condition is related to typing: it would be ill-advised to try solving, for example, the goal $1 + 1 = 2$ by set extensionality. In the absence of a type inference mechanism, we simply consider a set to be a term whose top connective is set-theoretic, like $\cup$ or UNION for instance.

## 5.5 Evaluation

We implemented the new SMT encoding in TLAPS. It can be used in place of the original encoding. The original encoding can still be used by passing the argument `--debug oldsmt` to TLAPS. We present now an evaluation designed to compare the performances of the two versions of the SMT encoding.

### 5.5.1 Methodology

We adapt the methodology of Section 4.7 to evaluate the different encodings for the SMT backend. Our set of TLA⁺ specifications is the same as before. TLAPS is invoked to encode each obligation three times: one version is for our encoding, the other two correspond to the $T_0$ and $T_1$ type systems of the original encoding. There is a third option $T_2$ for the original encoding, but during our evaluation we found that the implementation of this type system is unsound in a way that is too difficult to fix. The error would cause type-checking conditions such as $x \in \text{DOMAIN } f$ to be ignored, making it very easy to prove invalid statements.

The three encodings lead to three different SMT benchmarks. Several SMT solvers are tested on the benchmarks: CVC4, cvc5, veriT and Z3. The timeout for solving is set to 5 seconds for all solvers (this is the default timeout in TLAPS). For veriT, the mention of SMT's logic UFNIA is replaced with UFLIA, because veriT does not support non-linear integer arithmetic. To obtain the results of the original encoding, we merged the results obtained from $T_0$ and $T_1$. An obligation is considered solved using the original encoding if it is solved using either $T_0$ and $T_1$.

By default, SMT solvers use our custom patterns, but this default behavior can be overriden by an option for each solver. To confirm the impact of our triggers, we tested every solver with the default behavior and with an option to ignore user patterns, for every obligation.

### 5.5.2 Results and Discussion

The results are presented in Tables 5.1, 5.2 and 5.3. Table 5.1 compares performances when using the original SMT encoding or our new version. We report the number of obligations solved using each version (top numbers) and the number of obligations *uniquely* solved using each version (bottom numbers). Table 5.2 is read similarly. It focuses on our new encoding and compares the results of three solvers—the results of CVC4 and cvc5 have been merged because of the substantial overlap between them. Table 5.3 looks at solvers individually to measure the impact of our custom patterns on performances. The top left numbers indicate
<table><caption>Table 5.1: Comparison with the Original SMT Encoding</caption><thead><tr><th rowspan="2">Specification</th><th rowspan="2">Size (# POs)</th><th colspan="2">Encoding</th></tr><tr><th>Original</th><th>New</th></tr></thead><tbody><tr><td>TLA<sup>+</sup> Distribution</td><td>1996</td><td>1688<br>56</td><td>1821<br>189</td></tr><tr><td>TLAPS Distribution</td><td>1402</td><td>1281<br>44</td><td>1333<br>96</td></tr><tr><td>Deconstructed Bakery</td><td>1214</td><td>1030<br>26</td><td>1188<br>184</td></tr><tr><td><strong>Total</strong></td><td>4612</td><td>3999<br>126</td><td>4342<br>469</td></tr></tbody></table>

<table><caption>Table 5.2: Solvers' Performances with the New Encoding</caption><thead><tr><th rowspan="2">Specification</th><th rowspan="2">Size (# POs)</th><th colspan="3">Solver</th></tr><tr><th>Z3</th><th>CVC4-5</th><th>veriT</th></tr></thead><tbody><tr><td>TLA<sup>+</sup> Distribution</td><td>1996</td><td>1754<br>53</td><td>1762<br>67</td><td>995<br>0</td></tr><tr><td>TLAPS Distribution</td><td>1402</td><td>1278<br>52</td><td>1273<br>53</td><td>854<br>0</td></tr><tr><td>Deconstructed Bakery</td><td>1214</td><td>1104<br>67</td><td>1121<br>84</td><td>236<br>0</td></tr><tr><td><strong>Total</strong></td><td>4612</td><td>4136<br>172</td><td>4156<br>204</td><td>2085<br>0</td></tr></tbody></table>

<table><caption>Table 5.3: Impact of User Patterns (Triggers)</caption><thead><tr><th rowspan="2">Specification</th><th rowspan="2">Size (# POs)</th><th colspan="6">Solver</th></tr><tr><th>Z3</th><th>CVC4</th><th>cvc5</th><th>veriT</th><th>portfolio</th></tr></thead><tbody><tr><td>TLA<sup>+</sup> Dist.</td><td>1996</td><td>1516<br>21</td><td>1754<br>259</td><td>1695<br>14</td><td>1750<br>69</td><td>1686<br>22</td><td>1722<br>58</td><td>748<br>18</td><td>995<br>265</td><td>1745<br>4</td><td>1821<br>80</td></tr><tr><td>TLAPS Dist.</td><td>1402</td><td>1120<br>12</td><td>1278<br>170</td><td>1155<br>4</td><td>1256<br>105</td><td>1156<br>5</td><td>1240<br>89</td><td>510<br>3</td><td>854<br>347</td><td>1232<br>0</td><td>1333<br>101</td></tr><tr><td>D. Bakery</td><td>1214</td><td>927<br>17</td><td>1104<br>194</td><td>1027<br>48</td><td>1109<br>130</td><td>1036<br>42</td><td>1116<br>122</td><td>199<br>5</td><td>236<br>42</td><td>1093<br>2</td><td>1188<br>97</td></tr><tr><td><strong>Total</strong></td><td>4612</td><td>3563<br>50</td><td>4136<br>623</td><td>3877<br>66</td><td>4115<br>304</td><td>3878<br>69</td><td>4078<br>269</td><td>1457<br>26</td><td>2085<br>654</td><td>4070<br>6</td><td>4342<br>278</td></tr></tbody></table>
how many obligations where solved without our triggers, the top right numbers indicate how many obligations where solved with our triggers. The bottom numbers are the numbers of obligations *uniquely* solved, for that solver. We also report the performances of a *virtual best solver* in the last column “portfolio”, whose results are obtained by merging the results of all solvers: an obligation is solved in portfolio mode if it solved by one solver at least.

As Table 5.1 shows the original encoding solves 3999 obligations in total while ours solves 4342—an increase of 8,5%. There are 126 obligations that we do not solve anymore, and 469 that only our version solves. Among these 469 obligations, many are not solved with the original encoding because of a bug in the preprocessing phase: 195 obligations were not successfully encoded with $T_0$, 432 with $T_1$.

Table 5.2 details how solvers performed with the new encoding. Among the 4342 obligations solved, 4136 (95%) were solved by Z3, 4156 (95%) were solved by either CVC4 or cvc5, and 2085 (48%) were solved by veriT. The poorer performances of veriT may be due to the limitation of the solver to linear integer arithmetic. There are 172 obligations solved uniquely by Z3, and 204 solved by CVC4 or cvc5 but no other solver. Thus, the majority of TLA⁺ obligations that can be solved by the SMT backend may be solved by combining Z3 with either CVC4 or cvc5.

If we ask solvers to ignore our triggers (user patterns), the total number of obligations solved is 4070, as reported by Table 5.3. Thus, our triggers represent an increase of 6,6% in terms of obligations solved, compared to the triggers automatically generated by the solvers. Moreover, disabling user patterns results in only 6 additional obligations to be solved. All solvers are positively impacted by enabling our triggers, but some more than others. Z3 and veriT profit the most from our triggers, with 623 and 654 obligations uniquely solved respectively. The impact is not as significant for CVC4 and cvc5, with 304 and 269 obligations solved uniquely respectively.

In summary, there is good evidence that our SMT encoding, which is an almost direct translation of TLA⁺ completed by custom triggers, improves the SMT backend of TLAPS. This conclusion must be nuanced by the fact that 126 obligations are not solved anymore by our version. We believe our axiomatization could be improved, for example by selecting better triggers for the instances of axiom schemas.
# Chapter 6

## Conclusion

TLAPS is used to ensure the soundness of computer systems through theorem proving. While efficient automation is important, it is critical that TLAPS can be ensured sound as well. To this end, we defined and implemented a *direct encoding* of TLA$^+$ for automated theorem provers. The direct encoding preserves most of the source obligations' structures and is easy to prove sound. We extended the direct encoding in a minimal way to implement a new *SMT encoding*. We optimized this encoding with custom E-matching patterns, resulting in a new SMT backend that is not only safer, but also as efficient as the one previously implemented.

### New Encodings of TLA$^+$

Our translations are based on a formalization of TLA$^+$ as a particular theory (collection of symbols and axioms) on top of a first-order logic. We adopted this formalism to capture the unique semantics of TLA$^+$, which is underspecified. TLA$^+$ features all the usual *logical connectives* from propositional and first-order logic, but it extends their traditional semantics to account for the new combinations the language permits. For instance, the expression $2 \wedge 5$ is legitimate, and this particular example is a refutable formula (if 2 and 5 are both true then they must be equal). The *primitive operators* of TLA$^+$, which include symbols from set theory, arithmetic, and symbols for functions, may also be combined in unconventional ways. For instance, $2 \cup 5$ is a legitimate expression, and while it seems nonsensical, we may derive some facts about it, like the fact that it equals $5 \cup 2$. Our formalization does not assign interpretations to the primitive operators of TLA$^+$; it only provides axioms.

This formalization of TLA$^+$ naturally leads to an encoding in two steps: first, “type errors” resulting from unconventional uses of logical connectives must be corrected, so that the usual semantics of first-order logic is recovered; second, the relevant operators must be declared as uninterpreted symbols and their axioms must be included in the problem. Regarding the first step, a similar transformation was defined for the original version of the SMT encoding, only it was not total. For instance, with the original backend, the formula $42 \Rightarrow 42$ is not supported, even though it is both legitimate and valid according to TLA$^+$'s semantics. We defined this step and proved that it results in equisatisfiable expressions of regular first-order logic. As for the second step, it is straightforward to implement. Only the operators occurring in the obligation are declared, along with the axioms we have attached to them.

Encoded problems can be directly translated to higher-order logic. We implemented a translation to the THF dialect of the TPTP standard, and added the superposition prover
Zipperposition as a backend for TLAPS. This new backend is especially useful for TLA⁺ obligations that require higher-order reasoning. These obligations are not very common, but they are inevitable in certain situations: proofs by induction on *Nat* or other structures, or proofs involving user-defined recursive operators. Support for these obligations was lacking before the addition of Zipperposition, as only the Isabelle backend could attempt to solve them using basic automation tactics. Our evaluation shows Zipperposition and Isabelle have complementary strengths. Zipperposition is limited by the fact that it does not support interpreted arithmetic (for the version supporting HOL), but for problems involving higher-order unification, it can cope with harder problems than Isabelle.

The SMT encoding is based on the architecture of the direct encoding. Second-order constructs such as set comprehension or explicit functions are reduced to first-order applications, and the appropriate instances of their axiom schemas are generated in the process. Integer arithmetic is supported by a few special axioms that specify a correspondence between TLA⁺'s arithmetical operators and SMT's interpreted symbols. Set extensionality is difficult to support, but the instances of set extensionality needed for most TLA⁺ obligations fall into a few predictable patterns; we use some special axioms to generate these instances. The most important feature of our SMT encoding is the axiomatization, which is fully optimized with E-matching patterns (triggers). We carefully selected those patterns by inspecting difficult proof obligations and refining our axioms through an empirical process. Our method relies on heuristics, but the strategy can be summarized in a few principles. One important principle is to watch for the kind of terms that specific patterns may produce when they are triggered: for instance, we avoid producing terms that introduce new sets, but we encourage the production of new facts $x \in S$ for known $x$ and $S$.

The resulting encoding is still very efficient despite the simple translation it is based on. Our evaluation shows that most obligations that were previously solved with the previous SMT backend are still solved with our version using a combination of CVC4 and Z3. There are also obligations that our version solves uniquely. Typically, the new version is more likely to solve *typing theorems* with less assistance from the user than before. These theorems usually consist of elementary verifications about TLA⁺'s set theory, but for large specifications there are many verifications to perform, and several cases for the different possible transitions of the system. With the previous backend, it is often the case that at least one case of the lemma is too difficult to prove, so this particular case must be detailed or proved with Zenon. With our backend, it is more frequent that the whole lemma can be solved in a single step.

## Perspectives

Our work on translating TLA⁺ for ATPs can be continued in many different ways. We outline some ideas below. The first two are simple ways to improve the SMT encoding that we described in this work. The remaining ideas are more ambitious, and involve revisiting the type synthesis mechanism of Vanzetto’s original work.

**Verification of the Axioms.** The direct encoding is based on a modular architecture with only two nontrivial components. We presented the arguments for why our translation is sound, so the next step would be to verify it formally. In particular, one should verify the axioms used by the SMT encoding and documented in Appendix C. All axioms are either simple consequences of TLA⁺'s theory, or special axioms that extend the theory conservatively, like our axioms for leveraging SMT's arithmetic. This verification supposes a formalization
of the logic $\mathcal{L}^s$ (which is essentially MS-FOL with second-order applications). Ideally, the implementation of TLAPS should be linked to the verified axiomatization, to eliminate the risk of introducing errors when copying axioms into the code.

**Extension of the Axiomatization.** There are some fragments of TLA⁺'s theory that our implementation does not cover. We could extend the axiomatization to support (for example) the theory of finite sets, or real arithmetic, or bags. The reals can be supported in the same way as the integers in our framework, by specifying a few special axioms to link TLA⁺'s operators to SMT's interpreted symbols. The theory of finite sets in TLA⁺ revolves around two operators *IsFiniteSet* and *Card*. It does not seem difficult to apply our strategy for assigning triggers to the axioms that specify finite sets. A more ambitious goal would be to implement our strategy as a general procedure for generating patterns automatically. This could lead to a better treatment of the axiom schemas of TLA⁺ for which there is no obvious pattern (in particular the axiom schema specifying *CHOOSE*) and the user lemmas involved in proof obligations.

**Typed Encodings.** One important shortcoming of the original SMT encoding is that most type information is actually discarded during the translation. Type synthesis assigns various types to expressions, including the sorts $\iota$, int, but also types for sets, functions, tuples, records, etc. However, these types are merely used to optimize the preprocessing phase. All expressions are encoded as terms of the sort $\iota$ in the final problem, with the exception of the sort int which is preserved. Thus the use of various typed encodings preserving constructed types in their outputs have not been explored yet. Two applications in particular seem more promising. First, SMT solvers may benefit from refined sort annotations to quantifiers and symbols, if enumerative instantiation techniques must be used. Second, the type annotations of the system $T_1$ may be exploited to implement the so-called *sets-as-predicates encoding*, which encodes set membership through the functional application of HOL. Types are necessary for this encoding, because the legitimate TLA⁺ expression $x \in x$ cannot be encoded as the application of $x$ to itself in HOL.

**Soft Typing for TLA⁺.** The lack of a traditional type system allows for more creativity in formalizations and great ease of use. However, it bears some negative consequences on the experience of interactive proof with TLAPS. Users of TLA⁺ are accustomed to the notion of proving typing lemmas of the form *Spec* $\Rightarrow \Box$ *TypingOK*. In our experience with the prover, one should also prove typing lemmas for each user-defined operator, otherwise it becomes difficult to manage definitions as the proofs get larger. For instance, suppose a specification defines the composition of two functions:

$$ g \circ f \triangleq [x \in \text{DOMAIN } f : g[f[x]]] $$

For each step of a proof, the user can choose to either expand every occurrence of $\circ$ into its definition, or leave the operator completely opaque. However, there are many kinds of situations in which the full definition of $\circ$ is not relevant, but some basic information about the symbol is necessary. That basic information is precisely the kind of information that is normally captured by typing. Thus it is often in the interest of the user that they prove the following lemma and make sure it is always visible in proofs:

$$
\begin{array}{l@{\qquad}l}
\textbf{THEOREM} & \textsc{Assume} \quad \begin{array}{@{}l@{}} \textsc{new } A, \textsc{ new } B, \textsc{ new } C, \\ \textsc{new } f \in [A \to B], \textsc{ new } g \in [B \to C] \end{array} \\
\textbf{PROVE} & (g \circ f) \in [A \to C]
\end{array}
$$
We want to suggest that the derivation and management of such lemmas could be further supported by automation. This could take the form of a subsystem of TLAPS that automatically infers *typing lemmas* from definitions, searches for *typing hypotheses* to infer the types of quantified variables in the manner of the $T_1$ type system, and performs *type inference* over whole TLA$^+$ specifications. Besides the interest for definition management, the system could be used to provide immediate feedback in the form of warnings to report type errors.
Bibliography

[1] Jean-Raymond Abrial. *The B-book - assigning programs to meanings*. Cambridge University Press, 1996.

[2] Jean-Raymond Abrial. *Modeling in Event-B - System and Software Engineering*. Cambridge University Press, 2010.

[3] Matthias Baaz, Uwe Egly, and Alexander Leitsch. Normal form transformations. In John Alan Robinson and Andrei Voronkov, editors, *Handbook of Automated Reasoning* (in 2 volumes), pages 273–333. Elsevier and MIT Press, 2001.

[4] Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors, *Handbook of Automated Reasoning* (in 2 volumes), pages 19–99. Elsevier and MIT Press, 2001.

[5] Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, *Proceedings of the 23rd International Conference on Computer Aided Verification (CAV '11)*, volume 6806 of *Lecture Notes in Computer Science*, pages 171–177. Springer, July 2011. Snowbird, Utah.

[6] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org.

[7] Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, and Uwe Waldmann. Superposition with lambdas. In Pascal Fontaine, editor, *Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings*, volume 11716 of *Lecture Notes in Computer Science*, pages 55–73. Springer, 2019.

[8] Nikolaj S. Bjørner and Mark C. Pichora. Deciding fixed and non-fixed size bit-vectors. In Bernhard Steffen, editor, *Tools and Algorithms for the Construction and Analysis of Systems*, pages 376–392, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.

[9] Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. *J. Autom. Reason.*, 51(1):109–128, 2013.

[10] Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. *J. Formalized Reasoning*, 9(1):101–148, 2016.
[11] Richard Bonichon, David Delahaye, and Damien Doligez. Zenon : An extensible automated theorem prover producing checkable proofs. In Nachum Dershowitz and Andrei Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings*, volume 4790 of *Lecture Notes in Computer Science*, pages 151-165. Springer, 2007.

[12] Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, and Pascal Fontaine. verit: An open, trustable and efficient smt-solver. In Renate A. Schmidt, editor, *Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings*, volume 5663 of *Lecture Notes in Computer Science*, pages 151-156. Springer, 2009.

[13] Samuel R. Buss. On Herbrand's theorem. In Daniel Leivant, editor, *Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, Indiana, USA, 13-16 October 1994*, volume 960 of *Lecture Notes in Computer Science*, pages 195-209. Springer, 1994.

[14] Alonzo Church. A formulation of the simple theory of types. *J. Symb. Log.*, 5(2):56-68, 1940.

[15] George E. Collins. Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In H. Barkhage, editor, *Automata Theory and Formal Languages, 2nd GI Conference, Kaiserslautern, May 20-23, 1975*, volume 33 of *Lecture Notes in Computer Science*, pages 134-183. Springer, 1975.

[16] Alessio Coltellacci. Reconstruction of TLAPS proofs solved by VeriT in Lambdapi. In *Rigorous State-Based Methods: 9th International Conference, ABZ 2023, Nancy, France, May 30-June 2, 2023, Proceedings*, page 375-377, Berlin, Heidelberg, 2023. Springer-Verlag.

[17] The Coq Development Team. The Coq Proof Assistant, version 8.7.1, December 2017. Official Release.

[18] T. Coquand. Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA, September 1989.

[19] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ Proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, *18th International Symposium On Formal Methods - FM 2012*, volume 7436 of *Lecture Notes in Computer Science*, pages 147-154, Paris, France, August 2012. Springer. The original publication is available at www.springerlink.com.

[20] Simon Cruanes. Superposition with structural induction. In Clare Dixon and Marcelo Finger, editors, *Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings*, volume 10483 of *Lecture Notes in Computer Science*, pages 172-188. Springer, 2017.

[21] Nigel Cutland. *Computability: An Introduction to Recursive Function Theory*. Cambridge University Press, 1980.
[22] Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. *J. Autom. Reason.*, 61(1-4):423-453, 2018.

[23] Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. *Commun. ACM*, 5(7):394-397, 1962.

[24] Leonardo Mendonça de Moura and Nikolaj Bjørner. Efficient E-matching for SMT solvers. In Frank Pfenning, editor, *Automated Deduction - CADE-21, 21st International Conference on Automated Deduction*, Bremen, Germany, July 17-20, 2007, *Proceedings*, volume 4603 of *Lecture Notes in Computer Science*, pages 183-198. Springer, 2007.

[25] Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, *Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings*, volume 4963 of *Lecture Notes in Computer Science*, pages 337-340. Springer, 2008.

[26] Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, *Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings*, volume 5195 of *Lecture Notes in Computer Science*, pages 410-425. Springer, 2008.

[27] [Rosalie] Defourné. Improving automation for higher-order proof steps. In Boris Konev and Giles Reger, editors, *Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings*, volume 12941 of *Lecture Notes in Computer Science*, pages 139-153. Springer, 2021.

[28] Rosalie Defourné. Encoding TLA⁺ proof obligations safely for SMT. In Uwe Glässer, José Creissac Campos, Dominique Méry, and Philippe A. Palanque, editors, *Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings*, volume 14010 of *Lecture Notes in Computer Science*, pages 88-106. Springer, 2023.

[29] David Déharbe, Pascal Fontaine, Yoann Guyot, and Laurent Voisin. Integrating SMT solvers in Rodin. *Sci. Comput. Program.*, 94:130-143, 2014.

[30] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, *10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012, volume 20 of EPiC Series in Computing*, pages 22-31. EasyChair, 2012.

[31] Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, *Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers*, volume 2919 of *Lecture Notes in Computer Science*, pages 502-518. Springer, 2003.
[32] Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. SMTCoq: A plug-in for integrating SMT solvers into Coq. In Rupak Majumdar and Viktor Kuncak, editors, *Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II*, volume 10427 of *Lecture Notes in Computer Science*, pages 126-133. Springer, 2017.

[33] Limor Fix. Fifteen years of formal property verification in Intel. In Orna Grumberg and Helmut Veith, editors, *25 Years of Model Checking - History, Achievements, Perspectives*, volume 5000 of *Lecture Notes in Computer Science*, pages 139-144. Springer, 2008.

[34] Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, and Alwen Ferranto Tiu. Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In Holger Hermanns and Jens Palsberg, editors, *Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings*, volume 3920 of *Lecture Notes in Computer Science*, pages 167-181. Springer, 2006.

[35] Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): fast decision procedures. In Rajeev Alur and Doron A. Peled, editors, *Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings*, volume 3114 of *Lecture Notes in Computer Science*, pages 175-188. Springer, 2004.

[36] Yeting Ge and Leonardo Mendonça de Moura. Complete instantiation for quantified formulas in satisfiability modulo theories. In Ahmed Bouajjani and Oded Maler, editors, *Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings*, volume 5643 of *Lecture Notes in Computer Science*, pages 306-320. Springer, 2009.

[37] Paul C. Gilmore. A proof method for quantification theory: Its justification and realization. *IBM J. Res. Dev.*, 4(1):28-35, 1960.

[38] Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. *J. Formalized Reasoning*, 3(2):153-245, 2010.

[39] David Gries and Fred B. Schneider. Avoiding the undefined by underspecification. In Jan van Leeuwen, editor, *Computer Science Today: Recent Trends and Developments*, volume 1000 of *Lecture Notes in Computer Science*, pages 366-373. Springer, 1995.

[40] Joseph Y. Halpern. Presburger arithmetic with unary predicates is $Π_1^1$ complete. *J. Symb. Log.*, 56(2):637-642, 1991.

[41] Jacques Herbrand. *Recherches sur la théorie de la démonstration*. PhD thesis, Faculté des Sciences de Paris, 1930.

[42] Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. *J. ACM*, 27(4):797-821, 1980.
[43] Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Benjamin Kuipers and Bonnie L. Webber, editors, *Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island, USA*, pages 203–208. AAAI Press / The MIT Press, 1997.

[44] Cezary Kaliszyk and Karol Pąk. Semantics of mizar as an isabelle object logic. *Journal of Automated Reasoning*, 63(3):557–595, Oct 2019.

[45] S.C. Kleene. *Mathematical Logic*. Dover books on mathematics. Dover Publications, 2002.

[46] Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ model checking made symbolic. *Proc. ACM Program. Lang.*, 3(OOPSLA):123:1–123:30, 2019.

[47] Leslie Lamport. The temporal logic of actions. *ACM Trans. Program. Lang. Syst.*, 16(3):872–923, 1994.

[48] Leslie Lamport. *Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers*. Addison-Wesley, 2002.

[49] Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed. *ACM Trans. Program. Lang. Syst.*, 21(3):502–526, 1999.

[50] K. Rustan M. Leino and Clément Pit-Claudel. Trigger selection strategies to stabilize program verifiers. In Swarat Chaudhuri and Azadeh Farzan, editors, *Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I*, volume 9779 of *Lecture Notes in Computer Science*, pages 361–381. Springer, 2016.

[51] Stephan Merz. On the logic of TLA+. *Comput. Artif. Intell.*, 22(3-4):351–379, 2003.

[52] Stephan Merz. Formal specification and verification. In Dahlia Malkhi, editor, *Concurrency: the Works of Leslie Lamport*, pages 103–129. ACM, 2019.

[53] Stephan Merz and Hernán Vanzetto. Encoding TLA$^+$ into unsorted and many-sorted first-order logic. *Sci. Comput. Program.*, 158:3–20, 2018.

[54] Jean-François Monin. *Understanding formal methods*. Springer, 2003.

[55] Michal Moskal. Programming with triggers. *ACM International Conference Proceeding Series*, 01 2009.

[56] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In *Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001*, pages 530–535. ACM, 2001.

[57] Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. *J. ACM*, 27(2):356–364, 1980.
[58] Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon web services use formal methods. *Commun. ACM*, 58(4):66–73, 2015.

[59] Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). *J. ACM*, 53(6):937–977, 2006.

[60] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. *Isabelle/HOL - A Proof Assistant for Higher-Order Logic*, volume 2283 of *Lecture Notes in Computer Science*. Springer, 2002.

[61] Lawrence C. Paulson. The foundation of a generic theorem prover. *J. Autom. Reason.*, 5(3):363–397, 1989.

[62] Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, *The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011*, volume 2 of *EPiC Series in Computing*, pages 1–11. EasyChair, 2010.

[63] Andrew Reynolds. Conflicts, models and heuristics for quantifier instantiation in SMT. In Laura Kovács and Andrei Voronkov, editors, *Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016*, volume 44 of *EPiC Series in Computing*, pages 1–15. EasyChair, 2016.

[64] Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting enumerative instan-
tiation. In Dirk Beyer and Marieke Huisman, editors, *Tools and Algorithms for the Con-
struction and Analysis of Systems - 24th International Conference, TACAS 2018, Held
as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS
2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II*, volume 10806 of
*Lecture Notes in Computer Science*, pages 112–131. Springer, 2018.

[65] Andrew Reynolds, Cesare Tinelli, and Leonardo Mendonça de Moura. Finding conflicting instances of quantified formulas in SMT. In *Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014*, pages 195–202. IEEE, 2014.

[66] John Alan Robinson. A machine-oriented logic based on the resolution principle. *J. ACM*, 12(1):23–41, 1965.

[67] John M. Rushby, Sam Owre, and Natarajan Shankar. Subtypes for specifications: Predicate subtyping in PVS. *IEEE Trans. Software Eng.*, 24(9):709–720, 1998.

[68] Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine. Alethe: Towards a generic SMT proof format (extended abstract). In Chantal Keller and Mathias Fleury, editors, *Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021*, volume 336 of *EPTCS*, pages 49–54, 2021.

[69] Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais. Reliable reconstruction of fine-grained proofs in a proof assistant. In André Platzer and Geoff Sutcliffe, editors,
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 450-467. Springer, 2021.

[70] Robert E. Shostak. An algorithm for reasoning about equality. Commun. ACM, 21(7):583-585, jul 1978.

[71] Robert E. Shostak. Deciding combinations of theories. J. ACM, 31(1):1-12, 1984.

[72] João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999.

[73] Jean Souyris, Virginie Wiels, David Delmas, and Hervé Delseny. Formal verification of avionics software products. In Ana Cavalcanti and Dennis Dams, editors, *FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings*, volume 5850 of *Lecture Notes in Computer Science*, pages 532-546. Springer, 2009.

[74] John Michael Spivey. *The Z notation - a reference manual*. Prentice Hall International Series in Computer Science. Prentice Hall, 1989.

[75] Ryan Stansifer. Presburger's article on integer arithmetic: Remarks and translation. Technical Report TR84-639, Cornell University, Computer Science Department, September 1984.

[76] Martin Suda and Christoph Weidenbach. A PLTL-Prover based on labelled superposition with partial model guidance. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, *Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings*, volume 7364 of *Lecture Notes in Computer Science*, pages 537-543. Springer, 2012.

[77] Geoff Sutcliffe. The TPTP problem library and associated infrastructure - from CNF to th0, TPTP v6.4.0. J. Autom. Reason., 59(4):483-502, 2017.

[78] Geoff Sutcliffe. The 10th IJCAR automated theorem proving system competition - CASC-J10. AI Commun., 34(2):163-177, 2021.

[79] G. S. Tseitin. *On the Complexity of Derivation in Propositional Calculus*, pages 466-483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983.

[80] Alan M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proc. London Math. Soc., s2-42(1):230-265, 1937.

[81] Hernán Vanzetto. *Proof automation and type synthesis for set theory in the context of TLA<sup>+</sup>. (Automatisation de preuves et synthèse de types pour la théorie des ensembles dans le contexte de TLA<sup>+</sup>)*. PhD thesis, University of Lorraine, Nancy, France, 2014.

[82] Petar Vukmirovic, Alexander Bentkamp, and Visa Nummelin. Efficient full higher-order unification. In Zena M. Ariola, editor, *5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)*, volume 167 of LIPICS, pages 5:1-5:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
[83] Petar Vukmirovic and Visa Nummelin. Boolean reasoning in a higher-order superposition prover. In Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, and Sophie Tourret, editors, *Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020)*, Paris, France, June-July, 2020 (*Virtual*), volume 2752 of *CEUR Workshop Proceedings*, pages 148–166. CEUR-WS.org, 2020.

[84] Freek Wiedijk. Mizar's soft type system. In *Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings*, pages 383–399, 2007.

[85] Yuan Yu, Panagiotis Manolios, and Leslie Lamport. Model checking TLA⁺ specifications. In Laurence Pierre and Thomas Kropf, editors, *Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenlb, Germany, September 27-29, 1999, Proceedings*, volume 1703 of *Lecture Notes in Computer Science*, pages 54–66. Springer, 1999.
# Appendix A

## The Standard Theory of TLA⁺

This appendix contains an axiomatization for TLA⁺. This theory is based on the logic $\mathcal{L}$ that is defined in chapter 3. To sum up briefly: $\mathcal{L}$ is a variant of unsorted FOL in which formulas do not form a distinct syntactic class, and second-order operators are permitted in signatures and can occur in applications.

We have organized the theory in thematic layers: epsilon-calculus, set theory, function theory, arithmetic, special functions (tuples, records and sequences) and finite sets. For each layer, we provide the list of primitive operators and their assigned shapes, followed by a list of axioms. There are several ways to formulate the theory, we have chosen one that highlights the proximity of TLA⁺ with traditional ZFC. Many axioms are just definitions of primitive constructs from already defined constructs; this choice of presentation makes the question of TLA⁺'s consistency relative to ZFC easier to apprehend.

The original reference for the standard theory of TLA⁺ is [48]. While we have adapted the presentation, we believe that our axiomatization is compatible with the reference book as it only differs in superficial ways. The most notable difference is our treatment of functions, as we leave the primitive operator isafcn unspecified. We refer the reader to section 3.3 for a discussion on this topic.

Some axioms are schemas, in which case the parameters will be put in parentheses next to the axiom's name:

$$ \mathit{ENUMDEF} (p > 0) \qquad \forall a_1, \dots, a_p, x : x \in \{a_1, \dots, a_p\} \Leftrightarrow x = a_1 \lor \dots \lor x = a_p $$

We use the following convention for denoting parameters: the character $n$ will always denote a natural number, $p$ a positive natural number, $s$ a string of characters, and $F, P, Q$ first-order operator symbols whose arity will be obvious in context.

Note that we will use readable notations for primitive constructs when possible. These notations will be indicated when new primitive operators are introduced. Another kind of notation we use is the multiline conjunction (or disjunction):

$$ \begin{array}{l} \wedge \phi_1 \\ \wedge \phi_2 \\ \dots \\ \wedge \phi_n \end{array} \qquad \text{means} \qquad \phi_1 \wedge \phi_2 \wedge \dots \wedge \phi_n $$
## Epsilon-calculus

The epsilon-calculus consists of only one second-order operator and two axioms.

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>choose</td><td>(1)</td><td>CHOOSE x : e &triangleq; choose(λx : e)</td></tr></tbody></table>

CHOOSEDEF (P)

∀x : P(x) ⇒ P(choose(P))

CHOOSEEXT (P, Q)

(∀x : P(x) ⇔ Q(x)) ⇒ choose(P) = choose(Q)

The notation `CHOOSE` is not used in the axioms above because it is not general enough: `CHOOSE x : P(x)` represents `choose(λx : P(x))` but not `choose(P)`. Using the extentionality axiom, we have the equality `choose(λx : P(x)) = choose(P)`, so may use `CHOOSE` in the remaining axioms.

The TLA⁺ constructs for if-then-else- and case-expressions are treated as notations:

CASE p₁ → e₁, ..., pₙ → eₙ

□ CHOOSE x : ∨ p₁ ∧ x = e₁

∨ p₂ ∧ x = e₂

∨ ...

∨ pₙ ∧ x = eₙ

CASE p₁ → e₁, ..., pₙ → eₙ, OTHER → e

□ CASE p₁ → e₁, ..., pₙ → eₙ, (¬p₁ ∧ ... ∧ ¬pₙ) → e

IF p THEN e₁ ELSE e₂

□ CASE p → e₁, OTHER → e₂

## Set Theory
<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>in</td><td>(0, 0)</td><td>e<sub>1</sub> &isin; e<sub>2</sub> &triangleq; in(e<sub>1</sub>, e<sub>2</sub>)<br/>e<sub>1</sub> &notin; e<sub>2</sub> &triangleq; notin(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>subseteq</td><td>(0, 0)</td><td>e<sub>1</sub> &sube; e<sub>2</sub> &triangleq; subseteq(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>enum<sub>n</sub></td><td>(0, ..., 0)*</td><td>{e<sub>1</sub>, ..., e<sub>n</sub>} &triangleq; enum<sub>n</sub>(e<sub>1</sub>, ..., e<sub>n</sub>)</td></tr><tr><td>union</td><td>(0)</td><td>UNION e &triangleq; union(e)</td></tr><tr><td>subset</td><td>(0)</td><td>SUBSET e &triangleq; subset(e)</td></tr><tr><td>setst</td><td>(0, 1)</td><td>{x &isin; e<sub>1</sub> : e<sub>2</sub>} &triangleq; setst(e<sub>1</sub>, &lambda;x : e<sub>2</sub>)</td></tr><tr><td>setof<sub>p</sub></td><td>(0, ..., 0, p)**</td><td>{e<sub>p+1</sub> : x<sub>1</sub> &isin; e<sub>1</sub>, ..., x<sub>p</sub> &isin; e<sub>p</sub>} &triangleq; setof<sub>p</sub>(e<sub>1</sub>, ..., e<sub>p</sub>, &lambda;x<sub>1</sub>, ..., x<sub>p</sub> : e<sub>p+1</sub>)</td></tr><tr><td>cup</td><td>(0, 0)</td><td>e<sub>1</sub> &cup; e<sub>2</sub> &triangleq; cup(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>cap</td><td>(0, 0)</td><td>e<sub>1</sub> &cap; e<sub>2</sub> &triangleq; cap(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>diff</td><td>(0, 0)</td><td>e<sub>1</sub> &setminus; e<sub>2</sub> &triangleq; diff(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>boolean</td><td>()</td><td>BOOLEAN &triangleq; boolean</td></tr></tbody></table>

(*) The operator `enum_n` expects `n` arguments; (**) the operator `setof_p` expects `p` constant arguments followed by one `p`-ary operator argument.

TLA⁺'s set theory follows closely the axiomatic theory of ZFC. Set replacement is treated differently through the operator `setof_p`, but the traditional schema of replacement can be derived from the axioms. The axiom of choice is not included, but it is trivially derived from the epsilon-calculus. The axiom of foundation and the axiom of infinity are included.

<table><tr><td>SETEXT</td><td>∀x, y : (∀z : z ∈ x &leftrightarrow; z ∈ y) ⇒ x = y</td></tr><tr><td>SUBSETEQDEF</td><td>∀x, y : x &sube; y &leftrightarrow; ∀z : z ∈ x ⇒ z ∈ y</td></tr><tr><td>ENUMDEF (p)</td><td>∀a<sub>1</sub>, ..., a<sub>p</sub>, x : x ∈ {a<sub>1</sub>, ..., a<sub>p</sub>} &leftrightarrow; x = a<sub>1</sub> &or; ... &or; x = a<sub>p</sub></td></tr><tr><td>EMPTYDEF</td><td>∀x : x &notin; {}</td></tr><tr><td>UNIONDEF</td><td>∀a, x : x ∈ UNION a &leftrightarrow; ∃y : y ∈ a &and; x ∈ y</td></tr><tr><td>SUBSETDEF</td><td>∀a, x : x ∈ SUBSET a &leftrightarrow; x &sube; a</td></tr><tr><td>SETSTDEF (P)</td><td>∀a, x : x ∈ {y ∈ a : P(y)} &leftrightarrow; x ∈ a &and; P(x)</td></tr><tr><td>SETOFDEF (p, F)</td><td>∀a<sub>1</sub>, ..., a<sub>p</sub>, x : x ∈ {F(y<sub>1</sub>, ..., y<sub>p</sub>) : y<sub>1</sub> ∈ a<sub>1</sub>, ..., y<sub>p</sub> ∈ a<sub>p</sub>} &leftrightarrow;<br/>∃z<sub>1</sub>, ..., z<sub>p</sub> :<br/>&and; ...<br/>&and; z<sub>p</sub> ∈ a<sub>p</sub><br/>&and; x = F(z<sub>1</sub>, ..., z<sub>p</sub>)</td></tr><tr><td>CUPDEF</td><td>∀a, b : a &cup; b = UNION {a, b}</td></tr><tr><td>CAPDEF</td><td>∀a, b : a &cap; b = {x ∈ a : x ∈ b}</td></tr><tr><td>SETMINUSDEF</td><td>∀a, b : a &setminus; b = {x ∈ a : x &notin; b}</td></tr><tr><td>BOOLEANDEF</td><td>BOOLEAN = {TRUE, FALSE}</td></tr><tr><td>FOUNDATION</td><td>∀x : x &ne; {} ⇒ ∃y : y ∈ x &and; x &cap; y = {}</td></tr><tr><td>INFINITY</td><td>∃x : {} ∈ x &and; ∀y : y ∈ x ⇒ y &cup; {y} ∈ x</td></tr></table>
In the axiom CAPDEF, the notation {$x \in a : x \in b$} is ambiguous, because it can be resolved as setst(a, $\lambda x : x \in b$) or as setof($\lambda x : x \in a, b$). The former resolution holds. In SETSTDEF, the notation {$x \in a : P(x)$} is resolved as setst(a, $\lambda x : P(x)$), but this is equal to setst(a, P) by extensionality, so there is no loss of generality. A similar argument can be made about SETOFDEF.

## Function Theory

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>isafcn</td><td>(0)</td><td></td></tr><tr><td>fn</td><td>(0, 1)</td><td>[x ∈ e₁ ↦→ e₂] ≜ fn(c₁, λx : e₂)</td></tr><tr><td>except</td><td>(0, 0, 0)</td><td>[f EXCEPT ! [x] = y] ≜ except(f, x, y)</td></tr><tr><td>domain</td><td>(0)</td><td>DOMAIN e ≜ domain(e)</td></tr><tr><td>fnapp</td><td>(0, 0)</td><td>e₁[e₂] ≜ fnapp(e₁, e₂)</td></tr><tr><td>arrow</td><td>(0, 0)</td><td>[e₁ → e₂] ≜ arrow(e₁, e₂)</td></tr></tbody></table>

In ZFC, functions are typically defined as binary relations with specific properties. TLA⁺ defines functions axiomatically. Functions are sets like any other element of the theory, but their underlying representation as sets is not specified. The fact that functions could be defined from binary relations proves that the following extension is conservative.

FCNEXTENSIONALITY

∀f, g : ∧ isafcn(f) ∧ isafcn(g)

∧ DOMAIN f = DOMAIN g

∧ ∀x : x ∈ DOMAIN f ⇒ f[x] = g[x]

⇒ f = g

FCNISAFCN (F)

∀a : isafcn([x ∈ a ↦→ F(x)])

FCNDOMAIN (F)

∀a : DOMAIN [x ∈ a ↦→ F(x)] = a

FCNAPP (F)

∀a, y : y ∈ a ⇒ [x ∈ a ↦→ F(x)][y] = F(y)

FCNSET

∀a, b, f : f ∈ [a → b] ⇔

∧ isafcn(f)

∧ DOMAIN f = a

∧ ∀x : x ∈ a ⇒ f[x] ∈ b

FCNEXCEPT

∀f, x, y : [f EXCEPT ! [x] = y] =

[z ∈ DOMAIN f ↦→ IF z = x THEN y ELSE f[z]]
## Arithmetic

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>Int</td><td>()</td><td></td></tr><tr><td>Nat</td><td>()</td><td></td></tr><tr><td>Real</td><td>()</td><td></td></tr><tr><td>0, 1, 2, ...</td><td>()</td><td></td></tr><tr><td>0.1, 0.2, 1.5, 5.647, ...</td><td>()</td><td></td></tr><tr><td>Infinity</td><td>()</td><td></td></tr><tr><td>plus</td><td>(0, 0)</td><td>e<sub>1</sub> + e<sub>2</sub> &triangleq; plus(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>minus</td><td>(0)</td><td>-e &triangleq; minus(e)</td></tr><tr><td>minus</td><td>(0, 0)</td><td>e<sub>1</sub> - e<sub>2</sub> &triangleq; minus(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>mult</td><td>(0, 0)</td><td>e<sub>1</sub> * e<sub>2</sub> &triangleq; mult(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>div</td><td>(0, 0)</td><td>e<sub>1</sub>/e<sub>2</sub> &triangleq; div(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>quotient</td><td>(0, 0)</td><td>e<sub>1</sub> &divide; e<sub>2</sub> &triangleq; quotient(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>remainder</td><td>(0, 0)</td><td>e<sub>1</sub> % e<sub>2</sub> &triangleq; remainder(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>exp</td><td>(0, 0)</td><td>e<sub>1</sub><sup>e<sub>2</sub></sup> &triangleq; exp(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>lteq</td><td>(0, 0)</td><td>e<sub>1</sub> &le; e<sub>2</sub> &triangleq; lteq(e<sub>1</sub>, e<sub>2</sub>)<br>e<sub>1</sub> &ge; e<sub>2</sub> &triangleq; lteq(e<sub>2</sub>, e<sub>1</sub>)<br>e<sub>1</sub> &lt; e<sub>2</sub> &triangleq; lteq(e<sub>1</sub>, e<sub>2</sub>) &and; e<sub>1</sub> &ne; e<sub>2</sub><br>e<sub>1</sub> &gt; e<sub>2</sub> &triangleq; lteq(e<sub>2</sub>, e<sub>1</sub>) &and; e<sub>1</sub> &ne; e<sub>2</sub></td></tr><tr><td>range</td><td>(0, 0)</td><td>e<sub>1</sub> .. e<sub>2</sub> &triangleq; range(e<sub>1</sub>, e<sub>2</sub>)</td></tr></tbody></table>

We use the different font for the constants *Int*, *Nat* and *Real* because it is how they are written in TLA⁺, and there is no point in introducing them as notations. The natural and decimal numbers are also introduced directly with their literal representation. Each number is a constant in TLA⁺. The operator * should not be confused with ×, which is used for product sets.

As for functions, TLA⁺ does not specify an underlying representation for *Int*, *Nat* and *Real*. It merely assumes those sets exist and satisfy the theories of integer, natural and real arithmetic, respectively. This is indeed the case in the context of set theory with the axiom of infinity. TLA⁺ furthermore specifies that *Nat* ⊂ *Int* ⊂ *Real*. Operators are defined for real numbers, but they are overloaded for integers and naturals. For instance, 1 + 1 = 2 and 0.8 + 6.3 = 7.1 are both valid TLA⁺ statements; both feature the same operator +, but the former can be derived from the theory of naturals whereas the latter must be derived from the theory of reals.

We do not provide an explicit axiomatization for the theories of arithmetic of TLA⁺. Details about TLA⁺'s arithmetic can be found in [48, sec. 18.4]. We will generally want to have TLA⁺ arithmetic handled by a solver's builtin arithmetic engine. We may assume TLA⁺'s interpretation of arithmetic is the same as that solver's interpretation—only the domain of interpretation will generally be a type in the solver's logic.

It might be useful to clarify how TLA⁺ defines division. *a/b* is division on reals, defined for all *a* ∈ *Real* and *b* ∈ *Real* \ {0}. *a* ÷ *b* and *a* % *b* are the euclidian quotient and its corresponding remainder, defined for all *a* ∈ *Int* and *b* ∈ *Nat* \ {0}. Unless those expressions are unspecified, the following relation is always satisfied:

$$a = b * (a \div b) + (a \% b)$$
Moreover, $a \div b \in \mathit{Int}$ and $a \% b \in 0..(b-1)$. Therefore, when $a < 0$, TLA⁺ truncates the euclidian quotient towards $-\infty$ and keeps the remainder positive. For instance, $-10 \div 3 = -4$ and $-10 \% 3 = 2$. When $b < 0$ then both results are unspecified.

The only operator that is not purely arithmetic is `range`, for which we provide an axiom.

RANGEDEF

$$ \forall m, n : m .. n = \{i \in \mathit{Int} : m \le i \land i \le n\} $$

## Tuples

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>tup<sub>n</sub></td><td>(0, ..., 0)*</td><td>⟨e<sub>1</sub>, ..., e<sub>n</sub>⟩ ≜ tup<sub>n</sub>(e<sub>1</sub>, ..., e<sub>n</sub>)</td></tr><tr><td>prod<sub>p+1</sub></td><td>(0, 0, ..., 0)*</td><td>e<sub>1</sub> × e<sub>2</sub> × ... × e<sub>p</sub> ≜ prod<sub>p</sub>(e<sub>1</sub>, e<sub>2</sub>, ..., e<sub>p</sub>)</td></tr></tbody></table>

The tuples of TLA⁺ are just functions from an interval set $1..n$. They are defined in terms of functions, which has the benefit of allowing a form of overloading over the operators for functions. (⋆) The operators `tup<sub>n</sub>` and `prod<sub>n</sub>` both expect $n$ arguments, but `prod<sub>n</sub>` is only defined for $n \ge 2$. It is indeed impossible to write $a_1 \times \dots \times a_n$ for $n = 0, 1$ in TLA⁺'s user language.

TUPLEDEF (n)

$$ \forall x_1, \dots, x_n : \langle x_1, \dots, x_n \rangle = [i \in 1..n \mapsto \begin{cases} \text{CASE } i = 1 \to x_1 \\ \dots \\ \text{CASE } i = n \to x_n \end{cases}] $$

PRODUCTDEF (p)

$$ \forall a_1, \dots, a_{p+1} : a_1 \times \dots \times a_{p+1} = \{\langle x_1, \dots, x_{p+1} \rangle : x_1 \in a_1, \dots, x_{p+1} \in a_{p+1} \} $$

## Strings

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>string</td><td>()</td><td>STRING ≜ string</td></tr><tr><td>"foo", "bar", ...</td><td>()</td><td></td></tr></tbody></table>

STRINGINTRO ("foo")

"foo" ∈ STRING

STRINGDISTINCT ("foo", "bar" distinct)

"foo" ≠ "bar"
Records

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>record<sub>s<sub>1</sub>,...,s<sub>p</sub></sub></td><td>(0, ..., 0)*</td><td>[s<sub>1</sub> ↦ e<sub>1</sub>, ..., s<sub>p</sub> ↦ e<sub>p</sub>] &triangleq; record<sub>s<sub>1</sub>,...,s<sub>p</sub></sub>(e<sub>1</sub>, ..., e<sub>p</sub>)</td></tr><tr><td>recset<sub>s<sub>1</sub>,...,s<sub>p</sub></sub></td><td>(0, ..., 0)*</td><td>[s<sub>1</sub> : e<sub>1</sub>, ..., s<sub>p</sub> : e<sub>p</sub>] &triangleq; recset<sub>s<sub>1</sub>,...,s<sub>p</sub></sub>(e<sub>1</sub>, ..., e<sub>p</sub>)<br>r.s &triangleq; r["s"]</td></tr></tbody></table>

(⋆) The operators `record`$_{s_1,...,s_p}$ and `recset`$_{s_1,...,s_p}$ both expect $p$ arguments; string parameters $s_1, ..., s_p$ are assumed distinct from each other. Records are similar to tuples in that they are defined as special functions. The domain of a record is a non-empty, finite set of strings.

$$ \begin{array}{l} \texttt{RECORDDEF} (s_1, \dots, s_p) \quad \forall x_1, \dots, x_p : [s_1 \mapsto x_1, \dots, s_p \mapsto x_p] = \\ \qquad [x \in \{\texttt{"s}_1\}, \dots, \texttt{"s}_p\} \mapsto \begin{array}{l} \texttt{CASE } x = \texttt{"s}_1 \to x_1 \\ \dots \\ \texttt{CASE } x = \texttt{"s}_p \to x_p \end{array} \\ \\ \texttt{RECORDSETDEF} (s_1, \dots, s_p) \quad \forall a_1, \dots, a_p : [s_1 : a_1, \dots, s_p : a_p] = \\ \qquad \{[s_1 \mapsto x_1, \dots, x_p \mapsto x_p] : x_1 \in a_1, \dots, x_p \in a_p\} \end{array} $$

Sequences

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>Seq</td><td>(0)</td><td></td></tr><tr><td>Len</td><td>(0)</td><td></td></tr><tr><td>Cat</td><td>(0, 0)</td><td>f &circ; g &triangleq; Cat(f, g)</td></tr><tr><td>Append</td><td>(0, 0)</td><td></td></tr><tr><td>Head</td><td>(0)</td><td></td></tr><tr><td>Tail</td><td>(0)</td><td></td></tr><tr><td>Subseq</td><td>(0, 0, 0)</td><td></td></tr><tr><td>Selectseq</td><td>(0, 1)</td><td></td></tr></tbody></table>

Sequences are another special case of TLA⁺ functions. A sequence over the set $S$ is a tuple of arbitrary length whose elements are in $S$. There are many new operators introduced with sequences, all are defined from previous operators. The definition of `Selectseq` stands out as the only recursive definition of this axiomatization; this particular definition is not particularly useful in practise, but it is the true definition of the operator.
# Appendix B

## Axioms for TPTP

This section documents the axioms used in the encoding to TPTP, which is detailed in chapter 4. The organization of the theory follows the one for TLA⁺ that we presented in appendix A (epsilon-calculus, set theory, functions, arithmetic, tuples and records). The theories of sequences and finite sets are not included here; those theories require non trivial integer arithmetic to be handled properly, so they are only supported by our SMT backend.

The underlying logic of the axioms is higher-order logic, although only the second-order fragment is used. Compared to TLA⁺'s logic, the Boolean sort `o` is available, and we note the individuals sort `ι`. We use standard notations for types, for instance the type of a binary relation on `ι` is written `ι × ι → o`.

### Epsilon-calculus

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>choose</td><td>(ι → o) → ι</td></tr></tbody></table>

CHOOSEDEF

$$ \forall P^{ι→o}, x^{ι} : P(x) \Rightarrow P(choose(P)) $$

CHOOSEEXT

$$ \forall P^{ι→o}, Q^{ι→o} : (\forall x^{ι} : P(x) \Leftrightarrow Q(x)) \Rightarrow choose(P) =_ι choose(Q) $$

### Set Theory

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>in</td><td>ι × ι → o</td></tr><tr><td>subseteq</td><td>ι × ι → o</td></tr><tr><td>enum<sub>n</sub></td><td>ι<sup>n</sup> → ι</td></tr><tr><td>union</td><td>ι → ι</td></tr><tr><td>subset</td><td>ι → ι</td></tr><tr><td>setst</td><td>ι × (ι → o) → ι</td></tr><tr><td>setof<sub>p</sub></td><td>ι<sup>p</sup> × (ι<sup>p</sup> → ι) → ι</td></tr></tbody></table>

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>cup</td><td>ι × ι → ι</td></tr><tr><td>cap</td><td>ι × ι → ι</td></tr><tr><td>diff</td><td>ι × ι → ι</td></tr><tr><td>boolean</td><td>ι</td></tr><tr><td>cast<sub>o</sub></td><td>o → ι</td></tr></tbody></table>
$$ \mathbf{SETEXT} \quad \forall x^t, y^t : (\forall z^t : \mathbf{in}(z, x) \Leftrightarrow \mathbf{in}(z, y)) \Rightarrow x =_t y $$

$$ \mathbf{SUBSETEQDEF} \quad \forall x^t, y^t : \mathbf{subseteqq}(x, y) \Leftrightarrow (\forall z^t : \mathbf{in}(z, x) \Leftrightarrow \mathbf{in}(z, y)) $$

$$ \mathbf{ENUMDEF}(p) \quad \forall a_1^t, \dots, a_p^t, x^t : \mathbf{in}(x, \mathbf{enum}_p(a_1, \dots, a_p)) \Leftrightarrow x =_t a_1 \lor \dots \lor x =_t a_p $$

$$ \mathbf{EMPTYDEF} \quad \forall x^t : \neg \mathbf{in}(x, \mathbf{enum}_0) $$

$$ \mathbf{SUBSETDEF} \quad \forall a^t, x^t : \mathbf{in}(x, \mathbf{subset}(a)) \Leftrightarrow (\forall y^t : \mathbf{in}(y, x) \Rightarrow \mathbf{in}(y, a)) $$

$$ \mathbf{UNIONDEF} \quad \forall a^t, x^t : \mathbf{in}(x, \mathbf{union}(a)) \Leftrightarrow (\exists y^t : \mathbf{in}(x, y) \land \mathbf{in}(y, a)) $$

$$ \mathbf{SETSTDEF} \quad \forall P^{t \to o}, a^t, x^t : \mathbf{in}(x, \mathbf{setst}(a, P)) \Leftrightarrow \mathbf{in}(x, a) \land P(x) $$

$$ \mathbf{SETOFDEF}(p) \quad \forall F^{t \to t}, a_1^t, \dots, a_p^t, x^t : \mathbf{in}(x, \mathbf{setof}(a_1, \dots, a_p, F)) \Leftrightarrow \\ \phantom{\mathbf{SETOFDEF}(p) \quad \forall F^{t \to t}, a_1^t, \dots, a_p^t, x^t : \mathbf{in}(x, \mathbf{setof}(a_1, \dots, a_p, F)) \Leftrightarrow} \exists y_1^t, \dots, y_p^t : \mathbf{in}(y_1, a_1) \land \dots \land \mathbf{in}(y_p, a_p) \land x =_t F(y_1, \dots, y_p) $$

$$ \mathbf{CUPDEF} \quad \forall a^t, b^t, x^t : \mathbf{in}(x, \mathbf{cup}(a, b)) \Leftrightarrow \mathbf{in}(x, a) \lor \mathbf{in}(x, b) $$

$$ \mathbf{CAPDEF} \quad \forall a^t, b^t, x^t : \mathbf{in}(x, \mathbf{cap}(a, b)) \Leftrightarrow \mathbf{in}(x, a) \land \mathbf{in}(x, b) $$

$$ \mathbf{SETMINUSDEF} \quad \forall a^t, b^t, x^t : \mathbf{in}(x, \mathbf{diff}(a, b)) \Leftrightarrow \mathbf{in}(x, a) \land \neg \mathbf{in}(x, b) $$

$$ \mathbf{BOOLCASTINJ} \quad \mathbf{cast}_o(\top) \neq \mathbf{cast}_o(\bot) $$

$$ \mathbf{BOOLEANDEF} \quad \forall x^t : \mathbf{in}(x, \mathbf{boolean}) \Leftrightarrow x =_t \mathbf{cast}_o(\top) \lor x =_t \mathbf{cast}_o(\bot) $$

## Function Theory

<table><thead><tr><td>Operator</td><td>Type</td></tr></thead><tbody><tr><td>isafcn</td><td>ι → o</td></tr><tr><td>fn</td><td>ι × (ι → ι) → ι</td></tr><tr><td>except</td><td>ι × ι × ι → ι</td></tr><tr><td>domain</td><td>ι → ι</td></tr><tr><td>fnapp</td><td>ι × ι → ι</td></tr><tr><td>arrow</td><td>ι × ι → ι</td></tr></tbody></table>
$$ \begin{array}{l} \text{FCNEXTENSIONALITY} \quad \forall f^t, g^t : \land \text{isafcn}(f) \land \text{isafcn}(g) \\ \qquad \qquad \qquad \land \text{domain}(f) =_t \text{domain}(g) \\ \qquad \qquad \qquad \land (\forall x^t : \text{in}(x, \text{domain}(f)) \Rightarrow \text{fnapp}(f, x) =_t \text{fnapp}(g, x)) \\ \qquad \qquad \qquad \Rightarrow f =_t g \end{array} $$

$$ \text{FCNISAFCN} \quad \forall F^{t \to t}, a^t : \text{isafcn}(\text{fn}(a, F)) $$

$$ \text{FCNDOM} \quad \forall F^{t \to t}, a^t : \text{domain}(\text{fn}(a, F)) =_t a $$

$$ \text{FCNAPP} \quad \forall F^{t \to t}, a^t, x^t : \text{in}(x, a) \Rightarrow \text{fnapp}(\text{fn}(a, F), x) = F(x) $$

$$ \text{ARROWDEF} \quad \forall a^t, b^t, f^t : \text{in}(f, \text{arrow}(a, b)) \Leftrightarrow \\ \qquad \qquad \qquad \land \text{isafcn}(f) $$

$$ \qquad \qquad \qquad \land \text{domain}(f) =_t a $$

$$ \qquad \qquad \qquad \land (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(\text{fnapp}(f, x), b)) $$

$$ \text{EXCEPTISAFCN} \quad \forall f^t, x^t, y^t : \text{isafcn}(\text{except}(f, x, y)) $$

$$ \text{EXCEPTDOM} \quad \forall f^t, x^t, y^t : \text{domain}(\text{except}(f, x, y)) =_t \text{domain}(f) $$

$$ \text{EXCEPTAPP} \quad \forall f^t, x^t, y^t, z^t : \text{in}(z, \text{domain}(f)) \Rightarrow \\ \qquad \qquad \qquad \land z =_t x \Rightarrow \text{fnapp}(\text{except}(f, x, y), z) =_t y \\ \qquad \qquad \qquad \land z \neq_t x \Rightarrow \text{fnapp}(\text{except}(f, x, y), z) =_t \text{fnapp}(f, z) $$

## Arithmetic and Strings

Contrary to the previous appendix, we note numerical constants with symbols `num_n`. This will make clearer in expressions when a natural number is an actual constant or some parameter (for instance the `n` in `enum_n`).

Our axiomatization does not cover real arithmetic, nor the characterizations of strings as sequences of characters.

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>Int</td><td>ι</td></tr><tr><td>Nat</td><td>ι</td></tr><tr><td>num<sub>n</sub></td><td>ι</td></tr><tr><td>plus</td><td>ι × ι → ι</td></tr><tr><td>uminus</td><td>ι → ι</td></tr><tr><td>minus</td><td>ι × ι → ι</td></tr><tr><td>mult</td><td>ι × ι → ι</td></tr></tbody></table>

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>quotient</td><td>ι × ι → ι</td></tr><tr><td>remainder</td><td>ι × ι → ι</td></tr><tr><td>exp</td><td>ι × ι → ι</td></tr><tr><td>lteq</td><td>ι × ι → o</td></tr><tr><td>range</td><td>ι × ι → ι</td></tr><tr><td>str<sub>s</sub></td><td>ι</td></tr><tr><td>string</td><td>ι</td></tr></tbody></table>
<table>
  <tr>
    <td>NATDEF</td>
    <td>∀n<sup>t</sup> : in(n, Nat) ⇔ in(n, Int) ∧ lteq(0, n)</td>
  </tr>
  <tr>
    <td>NUMTYPING (n)</td>
    <td>in(num<sub>n</sub>, Nat)</td>
  </tr>
  <tr>
    <td>NUMDISTINCT (n<sub>1</sub>, n<sub>2</sub> distincts)</td>
    <td>num<sub>n<sub>1</sub></sub> ≠<sub>ι</sub> num<sub>n<sub>2</sub></sub></td>
  </tr>
  <tr>
    <td>PLUSTYPING</td>
    <td>∀m<sup>t</sup>, n<sup>t</sup> : in(m, Int) ∧ in(n, Int) ⇒ in(plus(m, n), Int)</td>
  </tr>
  <tr>
    <td>UMINUSTYPING</td>
    <td>∀n<sup>t</sup> : in(n, Int) ⇒ in(uminus(n), Int)</td>
  </tr>
  <tr>
    <td>MINUSTYPING</td>
    <td>∀m<sup>t</sup>, n<sup>t</sup> : in(m, Int) ∧ in(n, Int) ⇒ in(minus(m, n), Int)</td>
  </tr>
  <tr>
    <td>MULTTYPING</td>
    <td>∀m<sup>t</sup>, n<sup>t</sup> : in(m, Int) ∧ in(n, Int) ⇒ in(mult(m, n), Int)</td>
  </tr>
  <tr>
    <td>QUOTIENTTYPING</td>
    <td>∀m<sup>t</sup>, n<sup>t</sup> : in(m, Int) ∧ in(n, Nat) ∧ n ≠ num<sub>0</sub> ⇒ in(quotient(m, n), Int)</td>
  </tr>
  <tr>
    <td>REMAINDERTYPING</td>
    <td>∀m<sup>t</sup>, n<sup>t</sup> : in(m, Int) ∧ in(n, Nat) ∧ n ≠ num<sub>0</sub> ⇒ in(remainder(m, n), range(num<sub>0</sub>, n))</td>
  </tr>
  <tr>
    <td>RANGEDEF</td>
    <td>∀m<sup>t</sup>, n<sup>t</sup>, p<sup>t</sup> : in(p, range(m, n)) ⇔ in(p, Int) ∧ lteq(m, p) ∧ lteq(p, n)</td>
  </tr>
  <tr>
    <td>STRTYPING (s)</td>
    <td>in(str<sub>s</sub>, string)</td>
  </tr>
  <tr>
    <td>STRDISTINCT (s<sub>1</sub>, s<sub>2</sub> distincts)</td>
    <td>str<sub>s<sub>1</sub></sub> ≠<sub>ι</sub> str<sub>s<sub>2</sub></sub></td>
  </tr>
</table>

Tuples and Records

<table>
  <thead>
    <tr>
      <th>Operator</th>
      <th>Type</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>tup<sub>n</sub></td>
      <td>ι<sup>n</sup> → ι</td>
    </tr>
    <tr>
      <td>prod<sub>p</sub></td>
      <td>ι<sup>p+1</sup> → ι</td>
    </tr>
    <tr>
      <td>record<sub>s<sub>1</sub>,...,s<sub>p</sub></sub></td>
      <td>ι<sup>p</sup> → ι</td>
    </tr>
    <tr>
      <td>recset<sub>s<sub>1</sub>,...,s<sub>p</sub></sub></td>
      <td>ι<sup>p</sup> → ι</td>
    </tr>
  </tbody>
</table>
TUPISAFCN (n) $\forall x_1^t, ..., x_n^t : \text{isafcn}(\text{tup}_n(x_1, ..., x_n))$
TUPDOM (n) $\forall x_1^t, ..., x_n^t : \text{domain}(\text{tup}_n(x_1, ..., x_n)) = \text{enum}_n, ..., n$
TUPAPP (n) $\forall x_1^t, ..., x_n^t : \begin{array}{l} \wedge \text{fnapp}(\text{tup}_n(x_1, ..., x_n), \text{num}_1) = x_1 \\ \qquad \wedge \dots \\ \qquad \wedge \text{fnapp}(\text{tup}_n(x_1, ..., x_n), \text{num}_n) = x_n \end{array}$
PRODDEF (p) $\forall a_1^t, ..., a_p^t, a_{p+1}^t, t^t : \begin{array}{l} \text{in}(t, \text{prod}_p(a_1, ..., a_p, a_{p+1})) \Leftrightarrow \\ \qquad \wedge t = \text{tup}_{p+1}(\text{fnapp}(t, \text{num}_1), ..., \text{fnapp}(t, \text{num}_{p+1})) \\ \qquad \wedge \text{in}(\text{fn}(t, \text{num}_1), a_1) \\ \qquad \wedge \dots \\ \qquad \wedge \text{in}(\text{fn}(t, \text{num}_{p+1}), a_{p+1}) \end{array}$
RECISAFCN (s<sub>1</sub>, ..., s<sub>p</sub>) $\forall x_1^t, ..., x_p^t : \text{isafcn}(\text{record}_{s_1, ..., s_p}(x_1, ..., x_p))$
RECDOM (s<sub>1</sub>, ..., s<sub>p</sub>) $\forall x_1^t, ..., x_p^t : \text{domain}(\text{record}_{s_1, ..., s_p}(x_1, ..., x_p)) = \text{enum}_p(\text{str}_{s_1}, ..., \text{str}_{s_p})$
RECAPP (s<sub>1</sub>, ..., s<sub>p</sub>) $\forall x_1^t, ..., x_p^t : \begin{array}{l} \wedge \text{fnapp}(\text{record}_{s_1, ..., s_p}(x_1, ..., x_p), \text{strs}_1) = x_1 \\ \qquad \wedge \dots \\ \qquad \wedge \text{fnapp}(\text{record}_{s_1, ..., s_p}(x_1, ..., x_p), \text{strs}_p) = x_p \end{array}$
RECSETDEF (s<sub>1</sub>, ..., s<sub>p</sub>) $\forall a_1^t, ..., a_p^t, r^t : \begin{array}{l} \text{in}(r, \text{recset}_{s_1, ..., s_p}(a_1, ..., a_p)) \Leftrightarrow \\ \qquad \wedge r = \text{record}_{s_1, ..., s_p}(\text{fnapp}(r, \text{str}_{s_1}), ..., \text{fnapp}(r, \text{str}_{s_p})) \\ \qquad \wedge \text{in}(\text{fnapp}(r, \text{str}_{s_1}), a_1) \\ \qquad \wedge \dots \\ \qquad \wedge \text{in}(\text{fnapp}(r, \text{str}_{s_p}), a_p) \end{array}$
# Appendix C

## Axioms for SMT

This section documents the axioms used in the encoding to SMT-LIB, which is detailed in chapter 5.

Axioms are expressed in multi-sorted first-order logic. Operators are assigned first-order types at declaration instead of shapes. There are axiom schemas, for which parameters are indicated after the schema's name. As before, we use the letter $n$ for natural numbers, $p$ for positive natural numbers, $s$ for strings of characters, and the letters $F, P, Q$ for operators symbols, which will be assigned types this time.

A major addition compared to previous axiomatizations is the presence of E-matching patterns. All patterns are indicated between curly-braces just below the relevant chain of quantifiers. The general syntax is:

$$ \forall x_1^{s_1}, \dots, x_n^{s_n} : \left\{ \begin{array}{l} t_1^1, \dots, t_{n_1}^1 \\ \vdots \\ t_1^m, \dots, t_{n_m}^m \end{array} \right\} \\ \phi $$

Where, for all $1 \le i \le m$, the pattern $\{t_1^i, \dots, t_{n_i}^i\}$ is a set of well-sorted terms, the free variables of which are exactly $x_1, \dots, x_n$.

For abbreviating types, we will sometimes use the syntax $s^n \to s$. For instance the expression $\text{int} \times \iota^2 \to o$ is short for the type $\text{int} \times \iota \times \iota \to o$. If $n = 0$ then $s^n \to s$ is just $s$.

### Epsilon-calculus

$$ \frac{\text{Operator} \qquad \text{Type}}{\text{choose}_P^* \qquad \iota^n \to \iota} \qquad (\star) \quad P : \iota^{n+1} \to o. $$