**Step 1: Internal representation.** First, H¨ayh¨a reads the configuration of the current and target infrastructure and translates them to the internal representation. This representation is a dataflow graph identifying which component of the infrastructure has access to which other components, and under which security assumptions. Figure 2 shows two such simplified dataflow graphs that our tool built from arch in Fig. 1. From this graph, H¨ayh¨a learns the desired security level of each component. In this section we describe how to compute security levels of resources in a given CloudFormation file: in Section 2.1 we describe the concrete syntax of a general CloudFormation file and how it applies

Fig. 2: Dataflow graphs derived from an infrastructure

to other IaC tools; in Section 2.2 we describe how we model an infrastructure in terms of network communication and security; finally, in Section 2.3 we show the execution semantics and computation of the security level of resources in an infrastructure.

**Step 2: Capturing all potential upgrade states.** After the initial and target configurations are converted to our model, H¨ayh¨a builds an upgrade state, designed to represent every possible intermediate infrastructure that could exist during the upgrade. In Section 2.4 we formally define the upgrade semantics from an initial state to a target state in terms of our model, while in Section 3.1 we show how the upgrade state is built in practice. Figure 3 shows such a state, in form of a graph, which contains a path (Web to PublicGet to PrivateLambda) allowing any user on the web to access a sensitive resource in a non-secure manner. Finally, in Section 3.2 we discuss how dependency relations refine the upgrade state.

Fig. 3: Upgrade State with a Path Exposing a Security Vulnerability

**Step 3: Analysis.** (Section 3.3) H¨ayh¨a computes an over-approximation of the intermediate states and the security level of their nodes in order to answer two questions: 1) is every node in every possible intermediate state at least as secure as the corresponding node in the initial or target configuration? and 2) does every node in every possible intermediate state communicate only with existing nodes? Any possible violation is reported to the user so they can take action and modify their target configuration accordingly. For example, using the

DependsOn keyword, one can enforce build orders in a CloudFormation file. For Figure 3, H¨ayh¨a reports the possible insecure access to PrivateLambda:

Resource PrivateLambda is not sufficiently protected, it needs at least Authorizer and is protected by None during upgrade. Add DependsOn properties to ensure correct security.

#### **2.1 CloudFormation Infrastructures**

CloudFormation uses a declarative language in which users can specify the desired state of their system. An example of a CloudFormation file is given on the left side of Figure 4. It shows a simplified example of an infrastructure in which an API can be called to access the result of running a Lambda (a simple function). There are no formal semantics for CloudFormation files [4,9] – they are simply YAML or JSON files created from the given AWS CloudFormation templates. Other tools, such as Terraform by HashiCorp, follow a similar template-based design.

To formalize the behavior of IaC languages, we would also need to formalize the precise behavior of components. However, these components are very diverse, ranging from firewalls and HTTP servers to general purpose machines or even entire network configurations. Fortunately, the intra-update sniping vulnerability is independent from the precise behavior of individual components, and we only need to analyze the network and security behavior of the infrastructure. We only track the security level of requests, and abstract away from their content. To describe our model, we need to introduce three concepts used in IaC:

A component of the infrastructure is called a resource. Every configuration file declares a set of resources and their configurations (e.g. Figure 4). Some resources, like the LambdaExecutionRole and the LambdaPermission are security resources, and they prevent an unauthorized use of other resources. Other resources, like the GreetingLambda and the GreetingRequestGET are actual running processes, the later also being publicly accessible. Finally, some resources do not correspond to a running process, but to a group of resources such as GreetingApi that gives some configuration value to every resource in the group.

A resource's configuration may reference other resources, and we record that information in our model. Based on the CloudFormation documentation, we distinguish different types of references that we list below:

```
CloudFormation File Corresponding Model
{ "Resources": {
"LambdaPermission": { LambdaPermission [security]
 "Type": "AWS::Lambda::Permission", intrinsic security: LambdaPermission,
 "Properties": {
   "FunctionName": "GreetingLambda", connection security(GreetingApi, Greet-
   "SourceArn": "GreetingApi" ingLambda, this)
 }
},
"GreetingLambda": { GreetingLambda
 "Type": "AWS::Lambda::Function", intrinsic security:
 "Properties": {
   "Role": "LambdaExecutionRole"
 }
},
"GreetingRequestGET": { GreetingRequestGET [public]
 "Type": "AWS::ApiGateway::Method", intrinsic security: ,
 "Properties": {
   "Integration": "GreetingLambda", network(this, GreetingLambda),
   "RestApiId": "GreetingApi" collects(GreetingApi, this)
 }
},
"GreetingApi": { GreetingApi [collection]
 "Type": "AWS::ApiGateway::Api" intrinsic security:
},
"LambdaExecutionRole": {
 "Type": "AWS::IAM::Role"
 "Properties": {
   ...
 }}}}
```
Fig. 4: Mapping Between a CloudFormation File and our Model

Each of these reference types can be present in any resource, any number of time. The resource it is declared in can take any role in the relation that it defines, and we represent the resource as this in the model, as shown on the right side of Figure 4.

In CloudFormation, a dependency is declared by using e.g. the DependsOn keyword. A dependency restricts the order in which updates can occur: before a resource can be updated, all the resources it depends on must have been updated.

#### **2.2 Model of a CloudFormation Infrastructure**

We now describe a model for a CloudFormation infrastructure. We define a state S = (R, D) as a set of resources and a partial order that represents the dependency relation between resources. A resource is a tuple composed of a name (string), a type, an intrinsic security context, an origin flag, the different types of references discussed above, and the original configuration of the resource.

With (id, id ) ∈ D we denote that id depends on id , and that id cannot be upgraded until id is upgraded.

The origin flag denotes whether the resource comes from the initial state or the target state during an upgrade, but it is not used at all when dealing with a single state. Similarly, the original configuration's type is not further defined, and depends on the vendor. It is not used for a single deployment, and we only use it to check for equality of resources when updating an existing deployment.

Inspired by Abstract Interpretation [10], we define a security context as an abstract domain with a partial order and some abstract operations: a top, a bottom, a meet, and a join. When two security contexts are comparable (x % y), we say that x is less permissive than y, or that x is more secure than y.

We define predicates that can help us to express some properties of resources in a specific state S: collection(r), resp. security(r), means that r is a resource whose type is that of a collection resource, resp. a security resource. We use public(r) to denote when r is a resource whose type is that of a resource that can be accessed from anywhere on the internet (although this might be restricted with security references), or if it is contained in a collection that is itself publicly accessible.

**Definition 1 (connection).** A connection is possible between two resources when there is a network reference between them or resources that collects them.

ref(r, r ) ⇐⇒ ∃c, c . ∧ ⎧ ⎨ ⎩ network reference(c, c ) r = c ∨ collects(c, r) r = c ∨ collects(c , r )

The security of a connection is the minimum security level a request from r must have to be able to reach r directly. This definition reflects the fact that, when a connection is secured by multiple security resources, it must have sufficient authority to be accepted by all of them.

#### **Definition 2 (connection security).**

$$security(r, r') \iff \sqcap \left\{ \begin{array}{l} \\ \exists c, c'. \lor \begin{cases} \textit{incoming} \,\, protein(c, s) \\ \textit{outgoing} \,\, protection(c', s) \\ \textit{comtion} \,\, protection(c, c', s) \end{cases} \right\} \\ \text{with } \land \left\{ \begin{array}{l} (r = c \lor collects(c, r)) \\ (r' = c' \lor collects(c', r')) \end{array} \right\} \end{array} \right\}$$

#### **2.3 Execution Semantics**

The execution semantics for our intermediate representation is given below. The semantics explains which resources are allowed to talk to which resources, and under which security level. When we write L & r → r , it means that r is allowed to send a request to r , under the security level L.

A request can come from the internet (represented with the constant W) and reach a public resource r if it has a sufficient security level L. Similarly, a request can come from a resource r and reach r if it has a sufficient security level, r is not a collection, and both resources have an adequate configuration that allows them to communicate.

OutsideRequest r ∈ R ¬collection(r ) L % security(W, r ) public(r ) L & W → r

$$\text{InternalRequire} \xrightarrow{\begin{array}{c} (r, r') \in R^2 \ \ \ \negcollection(r') \quad L \sqsubseteq security(r, r') \ \ \mathit{ref}(r, r') \ \hline \mathit{ref}(r, r') \ \hline \mathit{L} \vdash r \rightarrow r' \end{array}} $$

A path P is a finite sequence of resources whose first resource is public, and subsequent resources can be reached from the previous, using the above semantics under some security level. The security of a path is then defined as the minimal security level under which every node can be reached in the above semantics:

$$security((r\_1, \ldots, r\_n)) = \bigwedge\_{i=1}^n secarray(r\_{i-1}, r\_i).$$

with r0 = W. We note W →∗ r the set of paths whose last element is r. Similarly, the security of a node is defined as the minimal security level under which the node can be reached by at least one path:

$$Sec(r) = \vee \{ succity(P) | P \in W \to^\* r\}$$

When the infrastructure, under which we consider the security of resources, is not clear from the context, we clarify that with a subscript SecS(r).

**Definition 3 (Substate).** When comparing two states, S1 and S2, we say that S1 ⊆ S2 when

Our first lemma states that, when a state is a substate of another, its nodes are at least as secure as the other.

#### **Lemma 1 (Substate Security).** ∀S1, S2. ∀id ∈ S1. S1 ⊆ S2 =⇒ SecS1 (id) % SecS2 (id)

Proof. We note that by definition, id is in both states. Additionally, any path in S1 is also a path in S2, and since the security of connections in S1 is more secure than the same connections in S2, the security of paths in S1 is greater than the security of the same paths in S2.

The security of a node is the meet of the security of paths that lead to it in the state. Paths that lead to id is S2 are the paths that lead to it in S1, and potentially additional paths. Therefore, the security of id in S1 is greater than in S2.

#### **2.4 Upgrade Semantics and Security Policy**

In IaC tools, an upgrade changes a given infrastructure state to a new state. This is done by upgrading each node that needs to be changed as specified by the new configuration. Generally, nodes are upgraded in an unspecified order, even in parallel, to improve deployment speed. Node updates are sent asynchronously to every service that needs to be updated, and there are dozens if not hundreds of steps each service must take to complete its update. When these upgrades are sent in parallel, it is difficult to reason about the state of the system as the running time for a node upgrade depends on the latency of the service. To model this behavior, we define an interleaving semantics for upgrades.

An upgrade starts in an initial state Si and ends in a target state St. Additional dependency ordering information is provided by the relation D of the target state.

The configuration of an identifier can be updated if all its dependencies are already updated (∀id ,(id, id ) ∈ R =⇒ S(id ) = St(id )), and it has not been updated yet:

$$\text{UppgradeConf} \xrightarrow{S(id) \neq S\_t(id)} \frac{\forall id', (id, id') \in R \implies S(id') = S\_t(id')}{S \to S[id \gets S\_t(id)]}$$

A new resource can be created under the same conditions, if it was not present in the initial state:

$$\text{UppgradeAdd} \xrightarrow{id \notin S \quad \forall id', R(id, id') \implies S(id') = S\_t(id')}$$

An identifier can be removed, if it is not in the target state:

$$\text{UpgradeDel} \xrightarrow{id \notin S\_t \quad id \in S} S \quad \begin{array}{l} id \in S \\ \hline S \to S \lor id \end{array}$$

We collect every accessible intermediate state in a set denoted by Acc:

$$\text{AccInit} \xrightarrow[S\_i \in Acc]{} \quad \text{AccNext} \\ \frac{S \in Acc \quad S \to S'}{}$$

Note that, in the absence of any dependency, Acc contains every combination where each resource is either at its initial or target configuration, leading to 2n possible intermediate states when n is the number of changed resources.

We next show that, when two identifiers are in a dependency relation, some intermediate states are not possible. For ease of expressing this lemma, we extend equality to also check whether id is in the domain of S. If id is neither in S nor S , we have S(id) = S (id). Otherwise, id must be in both and associated to the same configuration for the equality to hold.

#### **Lemma 2 (Dependency Restriction).**

∀(id, id ) ∈ R, S ∈ Acc =⇒ S(id) = St(id) ∨ S(id ) = Si(id ) ∨ St(id) = Si(id) ∨ St(id ) = Si(id )

Proof. By induction of S ∈ Acc and by case analysis on the inequality that holds in the inductive case.

We now define the security policy as:

**Definition 4 (Security Policy).** A deployment from Si to St is secure iff:

$$\forall S \in Acc, \forall id, \begin{cases} Sec(S, id) \sqsubseteq Sec(S\_i, id) & \text{if } S\_i(id) = S(id) \\ Sec(S, id) \sqsubseteq Sec(S\_t, id) & \text{if } S\_t(id) = S(id) \\ Sec(S, id) = \bot & \text{otherwise (id is not in } S) \end{cases}$$

Our work focuses on security issues that happen during upgrades, assuming that the initial and target states are both secure. We require that in any intermediate state any resource is at least as secure as their counterpart in the initial or target state, depending on where their configuration comes from.

#### **3 Architectural Design of the H¨ayh¨a Tool**

#### **3.1 Upgrade States**

To verify the security of intermediate states, we could compute all the possible intermediate states and pass them to existing tools that could check the security of such states. However, this approach has two main drawbacks. First, we would need to construct 2n intermediate states, which does not scale for large infrastructure changes. Second, the result of such tools would not be easy to understand for end users, as they would report issues with states that are not defined or even considered by the user. Our goal is a tool that is both scalable and able to provide suggestions on how to change the target configuration, not some hidden intermediate configuration.

Fig. 5: Example Upgrade State

To address scalability we introduce upgrade states which represent multiple states on which we can apply the same execution semantics. Recall that a state is composed of a list of resources with their origin, type and references, and of a dependency relation. An upgrade state is composed in the same way. The set of resources is the union of the resources from the initial and target states, excluding initial resources that only differ from their target counterpart by their

provenance flag. When resources are added or removed from an infrastructure, we introduce an empty resource for each of them. They represent the absence of these resources. The dependency relation of the upgrade state is the dependency relation of the target state.

The execution semantics of an upgrade state is the same as the execution semantics of a normal state. Since the upgrade state represents multiple versions of the same resources at the same time, we need to change the definition of the security level of a connection between resources. An example of an upgrade state is given in Figure 5. The initial state has an API, a GET method and a lambda, and everything is public. The target state modifies the lambda and adds an authorizer. The upgrade state is comprised of the unchanged API, the target authorizer (with an empty resource as its initial counterpart), the GET method (which did not change), and the two variants of the lambda. The connection to the GET method is protected either by the empty node (!) or the target authorizer. The minimal security level for this connection is therefore !.

In summary, when a security resource is relevant for a connection, we need to consider its counterpart that has a different provenance flag. If it is also relevant, the connection is protected by the disjunction of the security level of these resources (they cannot both exist at the same time, but one of them exists at any given time). If it is not relevant, the upgrade state represents at least one case where the security resource is not relevant, meaning that the connection is protected by the disjunction of the first security level and !, which is ! (no security at all). If the counterpart is an empty resource, the upgrade state represents at least one case where the security resource was deleted (or not yet added), so the connection is also unprotected. If there is no counterpart, the connection is simply protected by the resource, because it does not change in any way during the upgrade.

We denote by U(Si, St) the upgrade state created from the initial state Si and the target state St. We now show that this state indeed collects all possible intermediate states.

#### **Lemma 3 (Upgrade Graph is an Overapproximation).**

∀S ∈ Acc.S ⊆ U(Si, St)

Proof. To apply the definition, we first show resources of S are resources of U. Then, we show that any connection in S is a connection in U, because resources come with the same references in both states.

#### **3.2 Splitting Dependencies**

We have seen that the upgrade state created from the initial and target configurations is an over-approximation of all the intermediate states, when we do not consider dependencies. Because dependencies reduce the number of intermediate states, the upgrade state might not be precise enough and might produce a warning when no actual intermediate states violate the security policy.

**Variants**. When the state has two nodes A and A with the same identifier, but a different label, we call them a variant of one another. When A belongs to the initial configuration and A to the target configuration, (A, A ) is called an upgrade pair.

We refine the upgrade state by splitting it along a dependency. Considering a state S, its dependency relation D, and two target resources (A , B ) ∈ D, the split of S, split(S, A , B ) is a set of upgrade states. Suppose A and B are, respectively, part of an upgrade pair (A, A ) and (B,B ). Then, split(S, A , B ) is the set of three upgrade states, where only one of A or A remains, and only one of B or B . We exclude the case where A and B remain. When any of these nodes does not exist, the number of possible combination is reduced. When only A and B exist in S, we have found an impossible situation, and the result of splitting is the empty set.

Although this process creates an exponential number of states, the number of dependencies tends to be limited in practice, because they slow upgrades down. At the same time, a big number of dependencies actually reduces the number of possible intermediate states, until every node is in a dependency, in which case there are exactly n intermediate states.

We now prove that splitting the upgrade state is correct, in the sense that the set of states split(S) still contains all the possible intermediate states (Acc):

#### **Theorem 1 (Correct Split).**

∀S ∈ Acc. ∃u ∈ split(U(Si, St)). S ⊆ u

Proof. Let us take a state S ∈ Acc from the set of all possible intermediate states. Since splitting a state according to a dependency preserves the states from Acc (Lemma 4 below), we can consider every dependency and split them in any order. Initially, it holds that S ⊆ U(Si, St), using Lemma 3.

Consider an upgrade state u such that S ⊆ u and D(id, id ). By Lemma 4, we can find a state u ∈ split(u, id, id ) such that S ⊆ u .

After applying this for each dependency, u is one of the states resulting from split(U(Si, St)), and the claim of the theorem holds.

The following intermediate lemma is needed to prove the correction of the split. It states that if a state contains one of the accessible states, splitting a dependency in it results in a set of states, where one of them still contains this intermediate state.

**Lemma 4 (Split Graphs).** ∀S ∈ Acc. ∀(id, id ) ∈ D. S ⊆ u =⇒ ∃u ∈ split(u, id, id ), S ⊆ u

Proof. Take (A, A ) the upgrade pair whose identifier is id. Similarly, take (B,B ) the upgrade pair whose identifier is id . Since S ∈ Acc, A and B cannot both exist at the same time in S (Lemma 2). Since S ⊆ u, we also know that u has at least one variant of id and one variant of id , the ones that are present in S.

The states from split(u, id, id ) are composed of the same nodes as u, except for id and id , where they all have one of the four possible combinations of initial and target states, except for the pair A , B. Since S doesn't have them both either, one states has the same variants of id and id as S, and we call it u . We now show that S ⊆ u .

First, we note that u has the same nodes as u, except for those with identifier id and id . For any resource in S, the resource was present in u, so it is also in u , unless it has identifier id or id . For this last cases, we note that u is defined to contain the same variants as S, so the resources of S are also resources of u .

Second, if we take L & r → r in S, we can use the same reasoning as in Lemma 3 to conclude that is also holds in u . Thus we conclude that S ⊆ u .

#### **3.3 Finding Vulnerabilities**

After H¨ayh¨a constructs the upgrade state, the next step is to check for security issues. Although we could split the upgrade state recursively until no dependency remains, a more interesting strategy is to immediately check the upgrade state for issues. If none is found, it is not necessary to refine the upgrade state. Otherwise, we try to find a relevant dependency and split the upgrade state on it, running the analysis on the resulting states, splitting on other dependencies as needed.

Our analysis detects two types of issues: first, if an empty node is accessible, it might be used by the infrastructure at a point it is not registered by the owner of the infrastructure. This is the case for a new node that is accessible before it is created. When that node is a resource that can be claimed by a third party (such as an S3 bucket), the attacker might be able to register it before the user. Similarly, for a deleted resource, an attacker could register it for themselves before the user stops using it.

Second, the security context of every node in the upgrade state is compared to the security of the same node in the initial or target state (depending on its provenance flag). When its security is strictly lower than the security of the node in the state it comes from, or incomparable, we raise an alarm because there is an intermediate step where the resource might not be sufficiently protected.

Using Lemma 1 and Theorem 1, when the security of a node in a possible intermediate state (collected in Acc) is insufficient, the security of that node in at least one split upgrade state is even lower. Therefore, if there is a violation of the security property, our tool will detect it.

#### **4 Experiments**

H¨ayh¨a is designed to be used before the deployment of a CloudFormation update, and it is crucial that H¨ayh¨a does not interrupt developer workflow. Our goal was, therefore, to evaluate the scalability of H¨ayh¨a on a variety of real-world CloudFormation updates. To do this, we collected 36 CloudFormation files from GitHub, where each file had a history of updates (commits). We ran H¨ayh¨a against every update recorded in GitHub to that file, and measured the running time. We found that our analysis completed within one seconds for all files – we believe that these results indicate that H¨ayh¨a could be integrated in developer workflow with minimal disruption to the user. The details of the evaluation dataset are given in Fig. 6.

Fig. 6: Analysis time of various CloudFormation files from GitHub. Point size is proportional to the number of updated resources, which are between 0 and 31.

To collect the set of GitHub CloudFormation files used in our scalability benchmark, we searched GitHub using the web search tool for code with the keyword AWSTemplateFormatVersion - which is a required keyword for any Cloud-Formation file. We then filtered by the .yaml extension, and further manually filtered for valid CloudFormation files (as opposed to other languages with overlap). Since we wanted to track updates to these files, we also filtered manually to find only files that had a revision history (≥ 2 commits for the file).

While we showed that H¨ayh¨a scales well on real world data, we did not identify any instances of intra-update sniping vulnerability in these files. This is an expected result, as the CloudFormation files we found on GitHub were generally designed as templates that developers would customize to their own needs. We believe application-focused CloudFormation files are not often uploaded, since CloudFormation files can contain sensitive and proprietary information (e.g. infrastrucuture design). In order to run a large-scale analysis to check for past instances of intra-update sniping vulnerability, we would need access to a repository of the private user data for many CloudFormation users.

#### **5 Related Work**

Following the development and use of Infrastructure as Code (IaC) practices, many threats and security challenges were recognized [26,27]. The security risks that have been identified in IaC have thus far remained similar to existing vulnerabilities arising from poor security practices, such as infrequent key rotation and hard-coded secret values [25]. Additionally, despite existing recommendations and good practices when dealing with cloud infrastructure, many existing deployments are still left insecure by user misconfigurations. For example, storage "buckets" which host files, should generally be configured by user to disallow world readable/writable permissions. However, in practice, users struggle with this [8]. Existing work has used SMT solver to automatically detect such vulnerabilities and help users secure their resources [4,9]. In contrast, we focus on the dynamic behavior of deployment updates that occur when using IaC tools, and their effect on security configuration.

Much work has focused on the security of virtualization technologies based on attack models such as malicious cloud users to compromised cloud providers, as summarized in [13]. In our work however, we do not make any assumption on the specific technology, as intra-update sniping vulnerabilities rely mostly on timing and insecure configuration on the user's side.

Our work is based on a graph model of the dataflow network of resources created in an infrastructure configuration. Similarly, Al-Shaer et al [2] propose to model and check network security using a graph-based model of the network. As with other work on the network and infrastructure security [5,18], the focus of the analysis is on the security of static network topologies, instead of the security of a moving topology, as we have in this paper. The analysis of security in static networks and static information flow models [21] is complementary to our work, as we assume the initial and target infrastructure are secure.

Beyond network configurations, there has been work in the analysis of configuration files. In particular, static analysis has been used to check that IaC configurations are idempotent [14,30], an important property for maintaining reproducibility of infrastructure. The reproducibility of infrastructure is known to be a challenge [7], despite IaC being declarative and version controlled. Further efforts have used probabilistic modelling to learn constraints on configurations [22,28,29].

#### **6 Conclusion**

We have identified a new class of vulnerability that applies to Infrastructure as Code services, intra-update sniping vulnerabilities, that arise from a lack of ordering in upgrading resources. We presented a tool, H¨ayh¨a, that detects such vulnerabilities in CloudFormation, and gives feedback to users on how securely update their infrastructure deployment. Our evaluation shows the scalability of H¨ayh¨a by running it on existing configurations from GitHub and found that it runs quickly enough to be usable in practice.

#### **Acknowledgement**

This work was completed while working on the grant supported by the National Science Foundation under Grant No. CCF-1715387, and partially supported by the Office of Naval Research under Grant N00014-17-1-2787.

#### **References**

Interest Group on Data Communication. SIGCOMM '18, Association for Computing Machinery, New York, NY, USA (2018)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### **Proof Generation/Validation**

#### **Certifying Proofs in the First-Order Theory of Rewriting***-*

Fabian Mitterwallner1 (-), Alexander Lochmann1 , Aart Middeldorp1 , and Bertram Felgenhauer2

**Consistent \* Complete \* Well Documen et d t ysaE \* o Reuse \*** \* **Eva ul det a** \* TACAS \* **Artifact** \* AEC

1 Department of Computer Science, University of Innsbruck, Innsbruck, Austria<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>2 Innsbruck, Austria

<EMAIL_ADDRESS>
**Abstract.** The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present FORT-h, a reincarnation of the decision tool FORT with certifiable output, and the formally verified certifier FORTify.

#### **1 Introduction**

Many properties of rewrite systems can be expressed as logical formulas in the first-order theory of rewriting. This theory is decidable for the class of linear variable-separated rewrite systems, which includes all ground rewrite systems. The decision procedure is based on tree automata techniques and goes back to Dauchet and Tison [7]. It is implemented in FORT [17,18]. FORT takes as input one or more rewrite systems R0, R1,... and a formula ϕ, and determines whether or not the rewrite systems satisfy the property expressed by ϕ, in which case it reports yes or no. FORT may not reach a conclusion due to limited resources.

For properties related to confluence and termination, designated competitions (CoCo [15], termCOMP [9]) of software tools take place regularly. Occasionally, yes/no conflicts appear. Since the participating tools typically couple a plethora of techniques with sophisticated search strategies, human inspection of the output of tools to determine the correct answer is often not feasible. Hence certified categories were created in which tools must output a formal certificate. This certificate is verified by CeTA [21], an automatically generated Haskell program using the code generation feature of Isabelle. This requires not only that the underlying techniques are formalized in Isabelle, but the formalization must be executable for code generation to apply. During the time-consuming formalization process, mistakes in papers are sometimes brought to light.

-This research is supported by FWF (Austrian Science Fund) project P30301.

c The Author(s) 2021

J. F. Groote and K. G. Larsen (Eds.): TACAS 2021, LNCS 12652, pp. 127–144, 2021. https://doi.org/10.1007/978-3-030-72013-1 7

Since 2017 we are concerned with the question of how to ensure the correctness of the answers produced by FORT. The certifier CeTA supports a great many techniques for establishing concrete properties like termination and confluence, but the formalizations in the underlying Isabelle Formalization of Rewriting (IsaFoR)3 are orthogonal to the ones required for supporting the decision procedure underlying FORT. We recently completed the formalization of the automata constructions involved in the decision procedure [14]. Earlier fragments were described in [8, 13]. In this paper we put these efforts to the test. More precisely, we

The remainder of the paper is organized as follows. The next section briefly recapitulates the first-order theory of rewriting and the variant of the decision procedure described in [14]. Sections 3 and 4 describe the representation of formulas in certificates and the certificate language. In Section 5 we describe how certificates are validated by FORTify, the verified Haskell program obtained from the Isabelle formalization. Section 6 describes FORT-h. Experimental results are presented in Section 7, before we conclude in Section 8.

#### **2 Preliminaries**

Familiarity with term rewriting [2] and tree automata [6] is useful, but we briefly recall important definitions and notation that we use in the remainder.

Terms T (F, V) are constructed from a signature F, consisting of function symbols with fixed arities, and a set of variables V. A term rewrite system (TRS for short) R consists of rewrite rules → r between terms and r. Instead of the usual restrictions /∈ V and Var(r) ⊆ Var(), we require Var()∩Var(r) = ∅. Here Var(t) denotes the set of variables in a term t. Moreover, and r are assumed to be linear terms (i.e., variables occur at most once). The conditions on the rewrite rules are necessary to ensure decidability of the first-order theory of rewriting for these linear variable-separated TRSs. The (one-step) rewrite relation of a TRS R is denoted by →R. A term t is ground if Var(t) = ∅. The set of ground terms is denoted by T (F).

The first-order theory of rewriting is defined over a language L containing the predicate symbols →, →∗, =, and many more. As models, we consider finite linear variable-separated TRSs R over signatures F such that T (F) is nonempty. The set T (F) serves as domain for the variables in formulas over L. The

3 http://cl-informatik.uibk.ac.at/software/ceta/

interpretation of the predicate symbol → in R is the one-step rewrite relation →R over T (F), →∗ denotes the restriction of →∗ R to terms in T (F), and = is interpreted as the identity relation on T (F). Since we use ground terms as carrier, formulas in the first-order theory of rewriting express properties on ground terms. For instance, the following formula ϕ expresses the property of having unique normal forms (UNR):

$$\forall s \forall t \forall u \left( s \to^\* t \land \neg \exists \ v \left( t \to v \right) \land s \to^\* u \land \neg \exists \ v \left( u \to v \right) \implies t = u \right)$$

To use ϕ for establishing UNR for arbitrary terms (i.e., terms in T (F, V)) two additional constant symbols need to be added to the signature [18]. (More on this in Section 8.) Additional predicates in L increase the expressive power and also allow expressing properties more compactly. For instance, we can write NF(t) for ¬∃ v (t → v) and s →! t for s →∗ t ∧ ¬∃ v (t → v). In Section 3 we present a grammar that describes the available constructions for predicates. All predicates that can be represented using these constructions are supported in our decision procedure.

The decision procedure is based on tree automata that recognize relations on ground terms. Here we give a brief summary. More information can be found in [6] and [14]. A tree automaton A = (F, Q, Qf , Δ) consists of a finite signature F, a finite set Q of states, disjoint from F, a subset Qf ⊆ Q of final states, and a set of transition rules Δ. Transition rules have one of the following two shapes: f(p1,...,pn) → q with f ∈ F and p1,...,pn, q ∈ Q, or p → q with p, q ∈ Q. The latter are called epsilon transitions. Transition rules can be viewed as rewrite rules between ground terms in T (F ∪Q). The induced rewrite relation is denoted by →Δ or →A. A ground term t ∈ T (F) is accepted by A if t →∗ Δ q for some q ∈ Qf . The set of all accepted terms is denoted by L(A) and a set L of ground terms is regular if L = L(A) for some tree automaton A.

We encode n-tuples with n 1 of ground terms as terms over an enriched signature, as follows. We write F(n) for the signature (F ∪ {⊥})n where ⊥ ∈ F/ is a fresh constant. The arity of a symbol f1 ··· fn ∈ F(n) is the maximum of the arities of f1,...,fn. The encoding of terms t1,...,tn ∈ T (F) is the unique term t1,...,tn∈T (F(n)) such that Pos(t1,...,tn) = Pos(t1)∪···∪Pos(tn) and t1,...,tn(p) = f1 ··· fn where fi = ti(p) if p ∈ Pos(ti) and fi = ⊥ otherwise, for all p ∈ Pos(t1,...,tn) and 1 i n. As an example, for the terms s = f(g(a), f(b, b)), t = g(g(a)), and u = f(b, g(a)) we obtain s, t, u = fgf(ggb(aa⊥), f⊥g(b⊥a, b⊥⊥)). An n-ary relation on ground terms is regular if its encoding is accepted by a tree automaton operating on terms in T (F(n)). Such an automaton is called an RRn automaton and regular n-ary relations are called RRn relations. The i-th cylindrification of an RRn relation R over T (F) is the RRn+1 relation {(t1,...,ti−1, u, ti,...,tn) | (t1,...,tn) ∈ R and u ∈ T (F)}.

Besides RRn automata, the decision procedure makes use of ground tree transducers (GTTs for short). A GTT is a pair G = (A, B) of tree automata over the same signature F. A pair (s, t) of ground terms in T (F) is accepted by G if s →∗ A u B ∗ →t for some term u ∈ T (F ∪ Q). Here Q is the combined set of states of A and B. The set of all such pairs is denoted by L(G). We denote by La(G) the set of all pairs (s, t) such that s →∗ A q B ∗ →t for some state q ∈ Q. A binary relation R on ground terms is a(n anchored) GTT relation if there exists a GTT G such that R = L(G) (R = La(G)). The decision procedure for the firstorder theory of rewriting described in [7] and implemented in FORT uses GTTs, the formalized variant described in [14] uses anchored GTTs (aGTTs), which have better closure properties. Both are supported in our certificate language, but FORT-h and FORTify use anchored GTTs since they permit us to model more predicates while reducing the need for ad-hoc constructions that need to be turned into executable (verified) code.

The decision procedure for the first-order theory of rewriting constructs RRn automata for the subformulas in a bottom-up fashion. GTTs (aGTTs) come into play for some of the atomic subformulas consisting of predicate symbols and variables. Closure properties take care of the logical structure of formulas. A final emptiness check determines whether the formula is satisfied for the TRS given as input to the decision procedure. Rather than formally stating the properties involved, we illustrate the decision procedure on an example.

Example 1. Consider the formula ϕ = ∀ s ∃ t(s →∗ t ∧ NF(t)), which expresses the normalization property of TRSs. To determine whether a TRS R over a signature F satisfies ϕ, we first construct an RR1 automaton A1 that accepts the ground normal forms in T (F), using an algorithm first described in [5] and recently formalized in [13]. For the subformula s →∗ t we construct a GTT G1 for the parallel rewrite relation −→ R. Since GTT relations are effectively closed under transitive closure (while RR2 relations are not), we obtain a GTT G2 for →∗ R. This GTT is transformed into an RR2 automaton A2. (In the formalized decision procedure described in [14], an RR2 automaton for →∗ is constructed from an anchored GTT for the root step relation → R, using suitable closure properties of anchored GTT and RR2 relations.) We cylindrify the RR1 automaton A1 into an RR2 automaton A3 that accepts T (F) × NFR. A product construction involving A2 and A3 produces an RR2 automaton A4 for the subformula s →∗ t ∧ NF(t). Projection yields an RR1 automaton A5 corresponding to ∃ t(s →∗ t∧NF(t)). So ϕ holds if and only if L(A5) = T (F). In FORT the ∀ quantifier is transformed into the equivalent ¬∃¬. Hence complementation is used to obtain an RR1 automaton A6 and the existential quantifier is implemented using projection. This gives an RR0 automaton A7 which either accepts the empty relation ∅ or the singleton set {()} consisting of the nullary tuple (). The outermost negation gives rise to another complementation step. The final RR0 automaton A8 is tested for emptiness: L(A8) = ∅ if and only the TRS R does not satisfy ϕ.

#### **3 Formulas**

The first step in the certification process is to translate formulas in the first-order theory of rewriting into a format suitable for further processing. We adopt de Bruijn indices [4] to avoid alpha renaming.

Example 2.  It expresses the commutation of two TRSs, indicated by the indices 0 and 1. Using de Bruijn indices for the term variables s, t, u, v produces

$$\forall \forall \forall \left(2 \to\_0^\* 1 \land 2 \to\_1^\* 0\right) \implies \exists \left(2 \to\_1^\* 0 \land 1 \to\_0^\* 0\right).$$

We refer to Example 4 for further explanation.

The formal syntax of formulas in certificates is given below. Angle brackets are used for non-terminal symbols. Here rr2 denotes the supported binary regular relations, which are formally defined after Example 3. Likewise, rr1 stands for regular sets (which are identified with unary regular relations).

$$\begin{aligned} \langle \langle \langle \mathtt{formula} \rangle ::= & \{ \mathtt{r} \mathtt{r} \langle \langle \mathtt{r} \rangle \langle \mathtt{term} \rangle \} \mid \{ \mathtt{r} \mathtt{r} \mathtt{2} \langle \langle \mathtt{term} \rangle \rangle \} \\ & \qquad \mid \langle \mathtt{and} \langle \langle \mathtt{formula} \rangle \* \rangle \mid \{ \mathtt{or} \langle \mathtt{formula} \rangle \* \} \mid \{ \mathtt{st} \mathtt{is} \mathtt{st} \mathtt{if} \mathtt{m} \} \rangle \\ & \qquad \mid \langle \mathtt{for} \mathtt{il} \mathtt{1} \langle \langle \mathtt{formula} \rangle \rangle \mid \{ \mathtt{true} \} \rangle \mid \{ \mathtt{true} \} \mid \{ \mathtt{false} \} \\ & \qquad \mid \{ \mathtt{restr} \mathtt{it} \mathtt{st} \langle \mathtt{formula} \rangle \mid \{ \mathtt{trs} \} + \} \rangle \\ \end{aligned} $$

De Bruijn indices are used for term variables and nat - denotes a TRS with index nat in which the left- and right-hand sides of the rules have been swapped. The class of linear variable-separated TRSs is closed under this operation. We use it to represent the conversion relation ↔∗ of a TRS R as the reachability relation →∗ induced by the TRS R∪R−.

Example 3. The commutation property in Example 2 is rendered as follows:

(forall (forall (forall (or (not (and (rr2 (step\* (0)) 2 1) (rr2 (step\* (1)) 2 0))) (exists (and (rr2 (step\* (1)) 2 0) (rr2 (step\* (0)) 1 0)))))))

Here (step\* (0)) denotes the RR2 relation →∗ induced by the first TRS (which is indexed by 0) and (rr2 (step\* (1)) 2 0) represents the subformula [1] t ->\* v of the FORT formula in Example 2.

We continue with the certificate syntax of RR1 and RR2 relations:

$$\begin{array}{lcl} \langle \begin{array}{lcl} \langle \begin{array}{lcl} \langle \mathsf{r}r\_{1} \rangle & ::= & \mathsf{l} \end{array} & \langle \mathsf{inf} \left\langle \begin{array}{lcl} \langle \mathsf{r}r\_{2} \rangle & \mathsf{l} \end{array} & \langle \mathsf{r}r\_{2} \rangle \end{array} \\ & & \mid \begin{array}{lcl} \langle \mathsf{union} \langle \mathsf{r}r\_{1} \rangle \langle \mathsf{r}r\_{1} \rangle \rangle & \langle \mathsf{initer} \,\langle \mathsf{r}r\_{1} \rangle \rangle \, & \langle \mathsf{diff} \,\langle \mathsf{r}r\_{1} \rangle \rangle \\ \end{array} \\ \end{array} \\ \langle \begin{array}{lcl} \langle \mathsf{r}r\_{2} \rangle & ::= & \mathsf{l} \,\mathsf{gtt} \,\langle \mathsf{gtt} \rangle \langle \mathsf{pos} \,\langle \mathsf{num} \rangle \rangle \, & \langle \mathsf{preduct} \,\langle \mathsf{r}r\_{1} \rangle \rangle \, & \langle \mathsf{id} \,\langle \mathsf{r}r\_{1} \rangle \rangle \\ & & \mid \begin{array}{lcl} \langle \mathsf{union} \langle \mathsf{r}r\_{2} \rangle \langle \mathsf{r}r\_{2} \rangle \rangle & \langle \mathsf{iflect} \,\langle \mathsf{r}r\_{2} \rangle \rangle \\ \end{array} \\ & & \mid \begin{array}{lcl} \langle \mathsf{comp} \langle \mathsf{r}r\_{2} \rangle \langle \mathsf{r}r\_{2} \rangle \rangle & \langle \mathsf{inverse} \,\langle \mathsf{r}r\_{2} \rangle \rangle \end{array} \\ \end{array} \end{array} \end{array}$$

$$\begin{array}{rcl} \langle \langle \mathsf{pos} \rangle ::= & \mathsf{=} \mid \mathsf{e} \mid \rangle & \langle \mathsf{num} \rangle ::= & \langle \mathsf{1} \mid \rangle \\\\ \langle \langle gt \rangle ::= & \langle \mathsf{root} \cdot \mathsf{step} \{ \langle trs \rangle + \} \rangle & \langle \mathsf{inverse} \, \langle gtt \rangle \rangle \\\\ & & & \langle \mathsf{acomp} \, \langle gtt \rangle \langle \langle gtt \rangle \rangle \rangle & \langle \mathsf{gcom} \, \langle gtt \rangle \rangle \, \mid \, \langle \mathsf{inter} \, \langle gtt \rangle \rangle \, \\\\ & & & \langle \mathsf{acomp1ement} \, \langle gtt \rangle \rangle \, \mid \, \langle \mathsf{etc} \, \langle gtt \rangle \rangle \, \mid \, \langle \mathsf{gtc} \, \langle gtt \rangle \rangle \, \end{array}$$

Here (terms) refers to T (F), (nf ( trs + )) to the normal forms (NF) induced by the union of the underlying TRSs, and (inf rr2) to the infinity predicate (INFR) which is satisfied by all terms having infinitely many successors with respect to the relation R. Furthermore, (proj (1 | 2)rr2) denotes projection (π) to the first (second) argument, (gtt gtt pos num) the transformation of a GTT relation into an RR2 relation with corresponding context closure (cf. [14, Section 3]), (id rr1) the identity relation on the underlying set, and (gtc gtt) ((atc gtt)) the (anchored) transitive closure of the underlying (anchored) GTT relation.

The constructs defined above closely correspond to the formalized closure operations for the predicates in the first-order theory of rewriting, reported in [14] and summarized below:

$$\begin{array}{lcl} \text{marized below:} & \\ \\ A & ::= & \to\_{\epsilon} \mid A^{-} \mid A \cup A \mid A^{+} \mid A^{\widehat{+}} \mid A \circ A \mid A \bigcirc A \mid A^{c} \mid A \cap A \\\ R & ::= & A \mid R\_{p}^{n} \mid R \cup R \mid R \cap R \mid R^{-} \mid T \times T \mid = & \\ \end{array}$$

$$\begin{array}{lcl} T & ::= & \mathcal{T}(\mathcal{F}) \mid \mathbb{N}\mathbb{F} \mid \mathbb{N}\mathbb{F}\_{R} \mid T \cup T \mid T \cap T \mid T^{c} \mid \pi\_{1}(R) \mid \pi\_{2}(R) \\\ n & ::= & \geqslant \mid 1 \mid > & p \ \coloneqq & \geqslant \mid \epsilon \mid > \end{array}$$

Here A are anchored GTT relations (gtt), R are RR2 relations (rr2), and T are regular sets of ground terms (rr1).

For convenience of tool authors, we add a few other constructs to rr2. The certifier expands these to a sequence of basic constructs given above.

$$\begin{aligned} \{\tau\_2\} &::= \dots \mid \{\mathsf{step} \{\langle trs \rangle + \}\} \mid \{\mathsf{step} \{\langle trs \rangle + \}\} \\ &\mid \{\mathsf{step} + \langle \langle trs \rangle + \}\} \mid \{\mathsf{step} + \}\nmid \{\mathsf{squareity}\} \\ &\mid \{\mathsf{paral1el-step} \{\langle trs \rangle + \}\} \mid \{\mathsf{root-step} + \langle \langle trs \rangle + \}\} \\ &\mid \{\mathsf{non-root-step} \{\langle trs \rangle + \}\} \mid \{\mathsf{join1}\{\langle trs \rangle + \}\} \end{aligned}$$

The complete list can be obtained from the accompanying website.

#### **4 Certificates**

A certificate for a first-order formula ϕ explains how the corresponding RRn automaton is constructed. We adopt a line-oriented natural deduction style. The automata are implicit. This is a deliberate design decision to keep certificates small. More importantly, it avoids having to check equivalence of finite tree automata, which is EXPTIME-complete [6, Section 1.7].

```
certificate ::= ( item inference formula info ∗ ) certificate
```

$$\begin{aligned} \mid \{\mathtt{empty}\langle\acute{e}item\rangle\} \mid \{\mathtt{non\mathtt{empty}}\langle\acute{e}item\rangle\} \\ \mid \langle\acute{e}item\rangle ::= \langle\acute{o}art\rangle \quad \langle\inf o\rangle ::= \{\mathtt{size}\langle\acute{o}nat\rangle\langle\acute{o}nat\rangle\} \mid \cdots \\ \mid \langle\acute{o}rm\rangle ::= \{\mathtt{r}1\langle\acute{r}r\_{1}\rangle\langle\acute{e}rm\rangle\rangle \mid \{\mathtt{r}r2\langle\acute{r}r\_{2}\rangle\langle\acute{e}rm\rangle\} \} \\ \mid \langle\acute{a}\mathtt{and}\langle\acute{e}item\rangle\*\rangle \mid \langle\acute{o}rm\rangle\*\rangle \mid \langle\acute{o}rm\rangle\rangle \\ \mid \langle\mathtt{existss}\langle\acute{e}item\rangle\rangle \mid \langle\mathtt{n}rm\rangle\rangle \mid \cdots \end{aligned}$$

Currently the info field only serves as an interface between the tool (which provides the certificate) and the certifier to compare the sizes of the constructed automata. In the future we plan to extend this field with concrete automata. This allows to test language equivalence of a tree automaton computed by a tool that supports our certificate language and the one reconstructed by FORTify, thereby providing tool authors with a mechanism to trace buggy constructions in case a certificate is rejected.

We revisit Example 1 to illustrate the construction of certificates.

Example 4. The formula ϕ = ∀ s ∃ t(s →∗ t ∧ NF(t)) expressing normalization is rendered as ϕ = ∀∃(1 →∗ 0 0 ∧ 0 ∈ NF[0]) in de Bruijn notation. Here 1 refers to the variable s, the second and third occurrences of 0 refer to t, and the last occurrence of 0 refer to the first (and only) TRS, which has index 0. We construct the certificate bottom-up, to mimic the decision procedure. The first line is for NF[0]:

(0 (rr1 (nf (0)) 0) (rr1 (nf (0)) 0))

The components can be read as follows:

The apparent redundancy will disappear when we continue. We proceed by expressing the relation →∗ 0 and subsequently make sure that the second component of →∗ 0 is in normal form:

```
(1 (rr2 (step* (0)) 1 0) (rr2 (step* (0)) 1 0))
(2 (and (1 0)) (and ((rr2 (step* (0)) 1 0) (rr1 (nf (0)) 0))))
```
Line 1 is similar to line 0. The inference step and 1 0 in line 2 constructs an RR2 automaton that accepts the intersection of the relations modeled in lines 1 and 0. This automaton corresponds to A4 in Example 1. The cylindrification step from A1 to A3 in Example 1 is left implicit. We continue with the projection of variable 0 and afterwards complement the resulting automaton. This is done by an exists followed by a not inference step:

The inference steps until this point describe the construction of A6 in Example 1. We complete the certificate by introducing the remaining operators:

(nonempty 7)

The nnf inference step does not modify the tree automaton computed in step 6 (which corresponds to A8 in Example 1) but checks the equivalence of the formula in line 6 with the one of line 7, which corresponds to the input formula ϕ . The equivalence check incorporates ∀ elimination, negation normal form, and associativity, commutativity and idempotency of ∧ and ∨. In the future we might add support for additional equivalences in first-order logic. The final step (nonempty 7) checks that L(A8) = ∅. So this certificate claims that the input TRS is normalizing. For TRSs that do not satisfy ϕ, the final line in the certificate would be (empty 7).

In the previous example we intentionally skipped over some details to convey the underlying intuition. First of all, the rr2 construct (step\* (0)) is derived and internally unfolded via (anchored) GTTs into

(gtt (gtc (root-step 0)) >= >)

Starting from an anchored GTT that accepts the root step relation induced by the first (and only) TRS in the list, an application of the GTT transitive closure operation followed by a multi-hole context closure operation with at least one hole that may appear in any position, an RR2 automaton that accepts the relation →∗ 0 is constructed. We also mentioned that cylindrification is implicit. The same holds for the projection operation that is used in the exists inference steps. A projection takes place in the first component if the variable 0 is present in the list of variables, otherwise the inference step preserves the automaton. This approach is sound as variables indicate the relevant components of the RRn automaton. Thanks to the de Bruijn representation, the innermost quantifier refers to variable 0, the first component in the given RRn automaton. However we must keep track of all variables occurring in the surrounding formula and update that list accordingly.

#### **5 FORTify**

The example in the preceding section makes clear that a certificate can be viewed as a recipe for the certifier to perform certain operations on automata and formulas to confirm the final (non-)emptiness claim. In particular, checking a certificate is expensive because the decision procedure for the first-order theory is replayed using code-generated operations from a verified version of the decision procedure. In this section we describe the steps we performed to turn the Isabelle formalization of the decision procedure described in [14] into our certifier FORTify.

We use the FOL-Fitting library [3], which is part of the Archive of Formal Proofs,4 to connect the first-order theory of rewriting and first-order logic. The translation is more or less straightforward. We interpret RR1 constructions as predicates and RR2 construction as relations in first-order logic and prove both interpretations to be semantically equivalent:

**lemma** eval formula F Rs α f = eval α undefined (for eval rel F Rs) (form of formula f )

With this equivalence we are able to define the semantics of formulas:

**definition** formula satisfiable **where** formula satisfiable F Rs f ←→ (∃ α. range α ⊆ T G F ∧ eval formula F Rs α f )

**definition** formula unsatisfiable **where** formula unsatisfiable F Rs fm ←→ (formula satisfiable F Rs fm = False)

**definition** correct certificate **where** correct certificate F Rs claim infs n ≡ (claim = Empty ←→ (formula unsatisfiable (fset F) (map fset Rs) (fst (snd (snd (infs ! n))))) ∧ claim = Nonempty ←→ formula satisfiable (fset F) (map fset Rs) (fst (snd (snd (infs ! n)))))

Last but not least we define the important function check certificate which takes as input a signature, a list of TRSs, a boolean, a formula, and a certificate. This function first verifies that the given formula and the claim corresponds to the ones referenced in the certificate and afterwards checks the integrity of the certificate. The following lemmata, which are formally proved in Isabelle, state the correctness of the check certificate function:

**lemma** check certificate F Rs A fm (Certificate infs claim n) = Some B =⇒ fm = fst (snd (snd (infs ! n))) ∧ A = (claim = Nonempty) **lemma** check certificate F Rs A fm (Certificate infs claim n) = Some B =⇒ (B = True −→ correct certificate F Rs claim infs n) ∧ (B = False −→ correct certificate F Rs (case claim of Empty ⇒ Nonempty | Nonempty ⇒ Empty) infs n)

4 https://www.isa-afp.org

The first lemma ensures that our check function verifies that the provided parameters fm (formula) and A (answer satisfiable/unsatisfiable) match the formula and the claim stated in the certificate. The second lemma is the key result. It states that the check function returns Some True if and only if the certificate is correct. The only-if case is hidden in the last two lines. More precisely, if the claim of the certificate is wrong then negating the claim (the first-order theory of rewriting is complete) leads to a correct certificate. Therefore, if our check function returns Some None then the certificate is correct after negating the claim.

Our check function returns None if the global assumptions (the input TRS is not linear variable-separated, the signature is not empty, etc.) are not fulfilled. We plan to extend the check certificate function in the near future such that it reports these kind of errors.

A central part of the formalization is to obtain a trustworthy decision procedure to verify certificates. Hence we use the code generation facility of Isabelle/HOL to produce an executable version of our check certificate function. Isabelle's code generation facility is able to derive executable code for our constructions with the exception of inductively defined sets. In [8, Section 7] an abstract Horn inference system for finite sets is introduced to overcome this limitation. We use this framework to obtain executable code for the following constructions defined as inductive sets:

At this point we can use Isabelle's code generation to obtain an executable check function. However, more effort is needed to obtain an efficient check function. Checking the certificate in Example 6 below did not terminate after more than 24 hours computation time. We used the profiling capabilities of the Glasgow Haskell Compiler (GHC) to analyze the generated code. This revealed that most of the time was spent on checking membership. Since the computed tree automata can grow very large, the use of lists as underlying data structure for sets in the generated code is a bottleneck.

To overcome this problem we decided to use the container framework of Lochbihler [12]. In our case, the setup involved a non-trivial overhead as the container framework requires multiple class instances for data types used inside sets. Some of these instances could be derived automatically by the deriving framework of Sternagel and Thiemann [20]. Afterwards Isabelle's code generation was able to generate a check certificate function that uses red-black trees as underlying data structure for sets.

Sadly, the function was still infeasible for the certificate in Example 6. This time the power set construction, which is exponential in worst case, turned out to be the culprit. In this construction we compute the transitive closure of the present epsilon transitions multiple times. Adding an explicit construction to

**Fig. 1.** Certificate validation with FORTify.

remove epsilon transitions from tree automata solved this issue. To make a long story short, after further modifications we were able to verify the certificate for Example 6 in a little less than 3 minutes, which we consider fast enough for a first prototype. The resulting code-generated certifier is called FORTify.

The overall design of FORTify is shown in Figure 1. It can be viewed as two separate modules A and B. Module B is the verified Haskell code base that is generated by Isabelle's code generation facility, containing the check certificate function and the data type declarations for formulas and certificates. To use this functionality, we wrote a parser which translates strings representing formulas (signatures, TRSs, certificates) to semantically equivalent formulas (signatures, TRSs, certificates) represented in the data types obtained from the generated code. This was done in Haskell and refers to module A in Figure 1. Module A accepts formulas in FORT syntax. Hence it also applies the conversion to the de Bruijn representation. After the translation in module A, the check certificate function in module B is executed and its output is reported.

Importantly, the code in module A is not verified in Isabelle. Correctness of FORTify must therefore assume correctness of module A as well as the correctness of the Glasgow Haskell Compiler, which we use to generate a standalone executable from the generated code.

#### **6 FORT-h**

FORT-h is a new decision tool for the first order theory of rewriting. It is a reimplementation of the decision mode of the previous FORT tool [18] based on a modified decision procedure. The decision procedure, like the formalization, is based on anchored GTTs. The new tool is implemented in Haskell whereas FORT is written in Java.

FORT-h supports all features of FORT while extending the domain of supported TRSs from left-linear right-ground TRSs to linear variable-separated ones. While FORT could technically take such TRSs as input, it is unsound when checking non-ground properties on them.

**Fig. 2.** Interface of FORT-h.

Example 5. To check confluence of the linear variable-separated TRS

$$\mathbf{g(g(x)) \to g(y)}\qquad\qquad\qquad\qquad\qquad\qquad\mathbf{a \to g(a)}$$

FORT-h can be called with

> ./fort-h "CR" input.trs NO

where input.trs is a text file containing the rewrite system. The tool correctly states that NO the system is not confluent. However, FORT incorrectly identifies this as confluent due to the lack of support for variables appearing in right-hand sides of rules.

FORT-h took part in the 2020 edition of the Confluence Competition, competing in five categories: COM, GCR, NFP, UNC and UNR. Even though it does not support many problems tested in the competition, due to the restriction to linear variable-separated TRSs, it was able to win the category for most YES results in UNR. The tool expects as input a formula ϕ and one or more TRSs, as seen in Figure 2. It then outputs the answer YES or NO depending on whether ϕ is satisfied or not by the given TRSs. FORT-h may be passed some additional options:

As an example of the latter, consider Example 5 and the call

```
> fort-h -w "CR" input.trs
NO
formula body / witness:
    (0 (<- o ->*) 1 & ~ 0 (->* o *<-) 1)
    0 = g(_00())
    1 = g(_01())
```
So in addition to the answer NO, it also outputs a counter example for the given formula consisting of the two terms g( 00()) and g( 01()). Here 00 and 01 are additional constants required to reduce confluence to ground-confluence, and represent variables. The terms should therefore be read as g(x) and g(y).

Internally FORT-h represents formulas using de Bruijn indices as described in Section 4. Additionally, universal quantifiers and implications are eliminated, and negations are pushed as far as possible to the atomic subformulas. The tool then traverses the formula in a bottom-up fashion, constructing the corresponding anchored GTTs and RRn automata. During this traversal we also keep track of the steps taken, to construct the certificate if necessary. To improve performance the automata are cached and reused for equal subformulas. The tree automaton representing the whole formula is then checked for emptiness. If the accepted language is empty, FORT-h reports NO, otherwise it outputs YES.

#### **7 Experiments**

The experiments described in this section were run on a computer with a Intel(R) Core(TM) i7-5930K CPU with 6 cores at 3.50GHz.

In the 2019 edition of the Confluence Competition [15] three tools contested the commutation (COM) category:5 ACP [1], CoLL [19], and FORT. On input problem COPS #1118 the tools gave conflicting answers.

Example 6. COPS #1118 is about the commutation of the TRSs COPS #669

a → c f(a) → b b → b b → h(b, h(c, a))

and COPS #695

h(a, a) → c b → h(b, a) b → a f(c) → c c → a

To determine the correct answer we use FORT-h to produce a certificate for ground-confluence by calling

```
> fort-h -c cert -i "GCom([0],[1])" 1118.trs
YES
```
This produces the following certificate:

```
(0 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
   (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
   (size 13 53 0))
(1 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)
   (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)
   (size 11 47 0))
(2 (not 1) (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))
(3 (and (0 2))
   (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
      (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))
(4 (exists 3)
```

```
5 https://cops.uibk.ac.at/results/?y=2019&c=COM
```

**Table 1.** FORT(-h) run on GCR formulas with a 60 s timeout (FORTify with 600 s).

```
(exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
      (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
(5 (exists 4)
   (exists (exists (and ((rr2 (comp (inverse (step* (1)))
      (step* (0))) 0 1) (not (rr2 (comp (step* (0))
      (inverse (step* (1)))) 0 1)))))))
(6 (not 5)
   (not (exists (exists (and (
      (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
      (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))))
(7 (nnf 6)
   (forall (forall (or (
      (not (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
      (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
(nonempty 7)
```
When passing this certificate to FORTify, after 2 minutes and 57 seconds the output Certified is produced, so we can be assured that the TRSs do commute. Note that the inference steps 0 and 1 contain the optional size information. Here (size k m n) means the underlying RRn automaton constructed by FORT-h contains k final states, m transitions, and n epsilon transitions.

We also ran some experiments comparing FORT-h to FORT. The problems for these experiments are taken from the Confluence Problems database (COPS), and consists of 122 left-linear right-ground TRSs. Note that FORT-h implements no parallelism, while FORT does. For the first two experiments we chose a timeout of 60 seconds for the decision tools and 600 seconds for FORTify. The formulas were taken from the experiments reported in [17].

The results are shown in Table 1, where the YES (NO) column shows the number of systems determined to be (non-)ground-confluent together with average time (∅-time) the tool took. The ∞ column is the number of timeouts. To compare overall performance the total time column contains the sum of all runtimes, including timeouts but excluding the time taken by FORTify. The ✔ columns show the numbers of certifiable results as well as the overall time taken by FORTify (✔-time). These results show that, even though they have the same meaning, the choice of formula has an impact on performance. Interestingly FORT-h is generally faster and can solve more problems than FORT even though it can not take advantage of any parallelism. This performance advantage is more prominent in systems which are non-confluent. For problems with the answer YES, FORT can still prove more. The table also shows that FORTify can only certify a small portion the results. This is due to the performance of the certifier, since all other problems time out.  No wrong results by the decision tools where identified.

The second set of formulas represents the normal form property, restricted to ground terms (GNFP):

$$\forall t \forall u \left( t \leftrightarrow^\* u \land \mathsf{NF}(u) \implies t \to^\* u \right) \tag{4}$$

$$\forall s \forall t \forall u \left(s \to t \land s \to^! u \implies t \to^\* u\right) \tag{5}$$

$$\forall t \left( \mathsf{WN}(t) \implies \mathsf{CR}(t) \right) \tag{6}$$

The results for these are shown in Table 2. The same pattern is observed, where even though both can (dis)prove satisfaction for the same formulas, FORT-h is faster overall.

For the last experiment we test performance on properties over two TRSs. This is done by checking ground-commutation (GCOM) for all pairs of systems form the dataset, resulting in 7503 problems. A timeout of 60 seconds was used. The results, presented in Table 3, show that FORT-h is ahead here as well, (dis)proving more problems and doing so in significantly less time.

Full details of the experiments are available from the website6 accompanying this paper. Precompiled binaries of FORT-h and FORTify are available from the same site. We also present a few additional experiments with FORTify.

6 https://fortissimo.uibk.ac.at/tacas2021

#### **8 Conclusion**

In this paper we presented FORTify, a certifier for the first-order theory of rewriting for linear variable-separated TRSs, together with an expressive certificate language for formulas and proofs. Moreover, a new implementation of the decision procedure for the theory of rewriting, FORT-h, is capable of producing certificates in this language.

We mention three topics which require further research. First of all, many certificates produced by FORT-h cannot be validated by the current version of FORTify within reasonable time. We will further improve the algorithms and data structures used in the check-certificate function. A natural candidate for optimization is the transitive closure algorithm generated by Isabelle, which always takes cubic time. Currently, sharing only takes place in the inference rules. Expanding this to the individual constructions will be the next step. Also trimming of anchored GTTs could improve the run time. In the current state of the formalization only trimming of GTTs is proved to be sound. Profiling will be used to determine other candidates that are likely to have a large impact on the validation time.

A second topic for future research is the certification of properties on open (i.e., non-ground) terms. In [8,16,18] conditions are presented to reduce properties related to confluence to the corresponding properties on ground terms, by adding additional constants to the signature. These results need to be formalized in Isabelle and the certificate language needs to be extended, before FORTify can be used to certify the corresponding categories in the Confluence Competition. We plan to define signature extensions directly in formulas, to offer the most flexibility. A related issue is the support for many-sorted signatures in the Isabelle formalization. FORT-h already supports many-sorted TRSs, which is the format in the GCR category of CoCo.

A third topic is improving the efficiency of FORT-h. We anticipate that supporting parallelism will further speed up FORT-h, especially for large formulas. Preprocessing techniques that go beyond the mere transformation to negation normal form will be helpful to obtain equivalent formulas that reduce the size of the ensuing tree automata in the decision procedure. In [10] similar ideas are applied to WSkS, in connection with MONA [11].

Acknowledgments. We thank Ren´e Thiemann for giving valuable advice on how to improve the efficiency of the generated code. The comments by the anonymous reviewers improved the presentation.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

#### **Syntax-Guided Quantifier Instantiation***-*

Aina Niemetz1 , Mathias Preiner1(-) , Andrew Reynolds2 , Clark Barrett1 , and Cesare Tinelli2

1 Stanford University, Stanford, USA<EMAIL_ADDRESS>2 The University of Iowa, Iowa City, USA

**Abstract.** This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntaxguided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of stateof-the-art solvers on a range of background theories.

#### **1 Introduction**

Modern Satisfiability Modulo Theories (SMT) solvers are highly efficient tools, capable of reasoning about constraints over a wide range of logical theories, including (non-linear) real and integer arithmetic, fixed-size bit-vectors, and floating-point arithmetic. Their core algorithms are designed primarily for quantifier-free constraints, but various extensions have been shown to work well also for quantified constraints in many cases. Quantified reasoning in SMT has many practical applications, including software verification, automated theorem proving, and synthesis.

Current SMT solvers handle quantified constraints in a variety of ways, with a degree of effectiveness that usually depends on the background theory. For instance heuristic instantiation techniques such as E-matching [15] are used for quantified formulas with heavy use of uninterpreted functions. These heuristic instantiation techniques are refutationally incomplete but they can be highly effective, in particular in the context of verification applications. For quantified constraints over a particular background theory, such as linear arithmetic or fixed-size bit-vectors, on the other hand, SMT solvers resort to an entirely different set of techniques. While also based on quantifier instantiation, these other

- This work was supported in part by DARPA (award no. FA8650-18-2-7861), NSF (award no. 1656926) and ONR (award no. N68335-17-C-0558).

c The Author(s) 2021

J. F. Groote and K. G. Larsen (Eds.): TACAS 2021, LNCS 12652, pp. 145–163, 2021. https://doi.org/10.1007/978-3-030-72013-1 8

techniques tend to be counterexample-guided and can be complete for theories and fragments of first-order logic that admit quantifier elimination.

Specific previous work in the latter direction includes counterexample-guided quantifier instantiation techniques for linear arithmetic [25] and fixed-size bitvectors [18,20]. The key to developing each of them is to devise an appropriate, theory-specific selection function, which determines a term selection strategy for instantiating universal quantifiers. For some logics, e.g., linear arithmetic, selection functions can be based on the notion of elimination set found in classic algorithms for quantifier elimination [9, 14]. However, since many theories used in practice do not admit quantifier elimination, the design of a good selection function is usually non-trivial. These challenges are further magnified when reasoning in combinations of multiple theories.

We propose a novel, syntax-guided quantifier instantiation (SyQI) approach, which is both general-purpose and highly effective for quantified formulas in background theories such as (non)linear integer, reals and floating-point arithmetic, and their combinations. The new approach leverages an embedding of a solver for the syntax-guided synthesis (SyGuS) problem [1] within an SMT solver in order to choose terms for quantifier instantiation in a counterexample-guided manner. It is theory-agnostic and only requires the specification, via a grammar, of the set of terms to consider for each sort in the theory when instantiating quantifiers.3 Since it can be applied to quantified formulas in any background theory, it is more general in scope than previous work [20]. Our approach is intended for logics such as quantified floating-point arithmetic, which would benefit from counterexample-guided quantifier instantiation, but for which appropriate selection function are not obvious. We show that the use of syntax-guided synthesis gives us the flexibility to develop variants of our approach that are highly competitive with the state of the art in SMT solving. More specifically, this paper makes the following contributions:

Related Work. Handling quantified formulas in SMT solvers is a long-standing challenge. Early approaches for quantified formulas were largely based on Ematching [8, 10, 15]. They have been later supplemented with techniques that rely on models for establishing satisfiability [11, 26], and on conflict finding to accelerate the search for unsatisfiability [27]. Pragmatic enumerative approaches

3 Our implementation provides a default grammar for all supported sorts. In general, grammars can also be provided by the user. We do not explore this option here.

for quantifier instantiation have also been explored and shown to increase the precision of SMT solvers on inputs involving uninterpreted functions where Ematching is incomplete [21]. The approach we describe here is also enumerative in nature; however, it leverages syntax-guided synthesis for choosing instantiations and does not target inputs with uninterpreted functions.

For quantified formulas over a single background theory, counterexampleguided approaches have been considered by Bjørner and Janota [6] and by Reynolds et al. [25], targeting primarily quantified linear integer/real arithmetic. For theories of other data types (e.g., bit-vectors), most approaches use valuebased instantiation, where concrete variable assignments for a set of quantifierfree formulas derived from the negation of the input formula (the counterexamples) provide instantiations for the universal variables. In the SMT solver Z3 [16], model-based quantifier instantiation (MBQI) [11] is combined with a templatebased model finding procedure [29]. A recent line of work by Niemetz et al. [18] leverages invertibility conditions in a counterexample-guided loop for quantifier instantiation of formulas in the theory of fixed-size bit-vectors. Brain et al. [7] lift the concept of invertibility conditions to the theory of floating-point arithmetic and presented a preliminary quantifier elimination procedure for a fragment of the theory based on these conditions. Another approach for lazy quantifier elimination for bit-vector formulas is explored by Vediramana Krishnan et al. [12], based on iterative approximate quantifier elimination.

Reynolds et al. [24] leverage counterexample-guided quantifier instantiation (CEGQI) to efficiently solve a restricted but practically useful form of syntaxguided synthesis problems. In contrast, the work in this paper has the dual goal of leveraging enumerative syntax-guided synthesis to establish a strategy for quantifier instantiation of (first-order) quantified formulas.

SyGuS techniques to solve quantified problems were previously explored by Preiner et al. in [20]. However, instead of focusing on quantifier instantiation they combined enumerative syntax-guided synthesis with value-based quantifier instantiation to synthesize Skolem functions for existential variables.

#### **2 Background**

We assume the usual notions and terminology of many-sorted first-order logic with equality (denoted by ≈). Let S be a set of sort symbols. For every σ ∈ S, let Xσ be an infinite set of variables of sort σ. Let X = % σ∈S Xσ. Let Σ be a signature consisting of a set Σs ⊆ S of sort symbols and a set Σf of interpreted (and sorted) function symbols fσ1···σnσ with arity n ≥ 0 and σ1, ..., σn, σ ∈ Σs. We assume that Σ includes a Boolean sort Bool and the Boolean values ! (true) and ⊥ (false). Let I be a Σ-interpretation that maps: each sort σ ∈ Σs to a nonempty set σI (the domain of I), with BoolI = {!, ⊥}; each variable x ∈ Xσ to an element xI ∈ σI; and each function fσ1···σnσ ∈ Σf to a total function fI: σI 1 × ... × σI n → σI if n > 0, and to an element in σI if n = 0.

We assume the usual definition of well-sorted terms, literals, and formulas as Bool terms with variables in X and symbols in Σ, and refer to them as Σ- terms, Σ-atoms, and so on. A ground term/formula is a Σ-term/formula without variables. We define *x* = (x1, ..., xn) as a tuple of variables and write Q*x*.ϕ with Q ∈ {∀, ∃} for a quantified formula Qx1. ··· Qxn.ϕ. A formula is universal if it has the form ∀*x*. P where P is a quantifier-free formula. For simplicity, we consider only universal quantifiers since existential quantifiers can be rewritten in terms of universal ones. We use Lit(ϕ) to denote the set of Σ-literals of Σformula ϕ. For a Σ-term or Σ-formula e, we use e[*x*] to indicate that the free variables of e are in *x*. For a tuple of Σ-terms *t* = (t1, ..., tn), we write e[*t*] for the term or formula obtained from e by simultaneously replacing each occurrence of xi in e by ti. If t is a Σ-term/formula and I a Σ-interpretation, we write t I to denote the meaning of t in I. We use the usual inductive definition of a satisfiability relation |= between Σ-interpretations and Σ-formulas.

A theory T is a pair (Σ,I), where Σ is a signature and I is a non-empty class of Σ-interpretations (the models of T) that is closed under variable reassignment, i.e., every Σ-interpretation that only differs from an I ∈ I in how it interprets variables is also in I. A Σ-formula ϕ is T-satisfiable (resp. T-unsatisfiable) if it is satisfied by some (resp. no) interpretation in I; it is T-valid if it is satisfied by all interpretations in I.

Enumerative SyGuS using an Embedding into Datatypes. A syntax-guided synthesis problem for an n-ary function f in a background theory T consists of a set of semantic restrictions (a specification) for f, given as a (second-order) T-formula of the form ∃f.ϕ[f], and a set of syntactic restrictions on the solutions for f, typically expressed as a context-free grammar. A solution to such a problem is a term t[x1,...,xn] that satisfies the syntactic restrictions and is such that the formula ϕ[λx1,...,xn.t] is T-valid.

As shown in previous work [24], syntactic restrictions for the bodies of functions to synthesize can be conveniently represented as a set of (algebraic) datatypes. The setting in this paper is simpler. Instead of synthesizing terms corresponding to function bodies, we use context-free-grammars for defining a set of (first-order) terms in a given theory, possibly containing free function symbols. For instance, let a and b be free constants of sort Int. The context-free grammar R below specifies a set of integer (Z) and Boolean (B) terms:

$$Z ::= 0 \quad | \quad 1 \quad | \quad a \quad | \quad b \quad | \quad Z + Z \quad | \quad Z - Z \quad | \quad \text{ite}(B, Z, Z) \tag{1}$$

$$B \implies B \ge B \quad | \quad Z \approx Z \quad | \quad \neg B \quad | \quad B \land B \tag{2}$$

Given such a grammar, our SyGuS solver generates the following mutually recursive datatypes:

$$\mathcal{Z} = \mathbf{zero} \mid \text{one} \mid \text{a} \mid \text{b} \mid \text{plus}(\mathcal{Z}, \mathcal{Z}) \mid \text{minus}(\mathcal{Z}, \mathcal{Z}) \mid \text{ite}(\mathcal{B}, \mathcal{Z}, \mathcal{Z}) \quad (3)$$

$$\mathcal{B} = \text{geq}(\mathcal{Z}, \mathcal{Z}) \mid \text{eq}(\mathcal{Z}, \mathcal{Z}) \mid \text{not}(\mathcal{B}) \mid \text{ and}(\mathcal{B}, \mathcal{B}) \tag{4}$$

Each datatype constructor, listed on the right-hand side of each equation, corresponds to a production rule of R, e.g., plus corresponds to the rule Z ::= Z + Z.

In previous work [22, 24], a smart enumerative approach for syntax-guided synthesis was presented and implemented in CVC4. In that work, the generation of terms is based on finding solutions for an evolving set of constraints in an extension of the quantifier-free fragment of algebraic datatypes, for which some SMT solvers have dedicated decision procedures [3, 23]. In the remainder of this paper, we write TD to denote the theory of datatypes over a signature ΣD of constructor and selector symbols. The signature ΣD includes (parametric) datatype sorts that are interpreted as the universe of a term algebra over the constructors. Selectors are interpreted as functions that extract the immediate subterms of a constructor term.

In our setting, datatype constraints are used to express syntactic restrictions on the terms in the original theory. For instance, in case of the example theory and corresponding datatypes Z and B defined above, we can write a datatype constraint that is falsified by all terms of the form plus(zero, t) where t is a constructor term of sort Z. This corresponds to ruling out terms of the form (0 + ...) in the original theory where s is a term of sort Int. In more detail, for a datatype term d, we write isC(d) to denote the discriminator predicate, which is satisfied exactly when d is interpreted as a datatype value whose top constructor is C. We write selσ,n(d) to denote a shared selector [28] applied to d, interpreted as the nth child of d with sort σ if one exists, and as an arbitrary element of σ otherwise. These symbols are used for constructing blocking constraints. For example, we can write ¬isplus(d) ∨ ¬iszero(selZ,1(d)) to state the constraint above that d cannot be interpreted as any datatype value corresponding to an Int term of the form (0 + ...). In the context of syntax-guided synthesis, a constraint like this is added, for instance, to filter out redundant terms (like 0 + ...) or terms already known to falsify the synthesis conjecture.

Our approach for syntax-guided instantiation relies on a notion of evaluation variables. A related, more general, notion of evaluation functions was used in the context of syntax-guided synthesis (see Section 2 of [22] for details). Let d be a term of a datatype sort encoding a grammar over terms of sort σ. We write ed to denote a free constant of sort σ, which we call the evaluation variable for d. We use evaluation variables to determine which terms to use in instantiations of quantified formulas. The algorithm given in the following section will add constraints that force the interpretation of ed to be equal to **to term**(dI) in interpretations I. A simple example of such a constraint is isa(d) ⇒ ed ≈ a, stating that the evaluation variable ed for d is equal to the free constant a of integer type when d is interpreted as the datatype value a.

#### **3 SyGuS Quantifier Instantiation (SyQI)**

Our new SyGuS-based instantiation approach combines counterexample-guided quantifier instantiation (CEGQI) with smart enumerative SyGuS techniques to synthesize terms for quantifier instantiation. In essence, it is an algorithm that tries to synthesize a term t for a variable x in a given formula ∀x. P[x] such that ¬P[t] holds. For synthesis purposes, each quantified variable is associated with

a SyGuS grammar based on the sort of the variable. For example, our algorithm uses a bit-vector-specific grammar to synthesize bit-vector terms as possible instantiations of quantified variables of bit-vector sort. Our SyGuS solver suggests instantiations based on such grammars and an evolving set of constraints on the instance term. The main advantage of this instantiation approach is that it does not require theory-specific quantifier instantiation algorithms. Its only theory-specific aspects are the construction of the grammar for each theory sort and the satisfiability checks performed on the generated instances.

Algorithm 1 shows the two main procedures **syqi** and **select lemmas**L of our SyGuS instantiation approach. To simplify the exposition, we describe the restricted case where the quantified input formula are all universal. Our implementation in CVC4, however, applies to the general case through a lazy conversion to DNF and resolution of quantifier alternations.

Procedure **syqi** takes as argument a set {Q1,...,Qn} of universal (quantified) T-formulas and a set G of ground T-formulas. As an initial step, and prior to solving the problem, we generate a lemma for each quantified formula Qi as part of our counterexample-guided quantifier instantiation approach (lines 2-5). We first create a fresh datatype constant dx of sort **grammar**S (x) for each variable x ∈ *x* in each input formula ∀*x*. P[*x*]. The datatype sort **grammar**S (x) is constructed from a SyGuS grammar determined by the sort of variable x. The language generated by the grammar includes ground terms from Qi and G of the same sort. These terms are chosen following a selection strategy S, which we describe in Section 3.1. Apart from running **check**, used as a black box, **grammar**S implements the only theory-specific handling of our procedure. Finally, we add to G a lemma of the form li ⇒ ¬P[**e***dx* ] for each quantified formula, where li is a fresh Boolean constant (the counterexample literal for Qi). Thanks to li being fresh, this preserves the satisfiability of G. The notation **e***dx* is a shorthand for (edx1 ,..., edxm ), the tuple of evaluation variables for each dx of x ∈ *x*. The purpose of a counterexample lemma is twofold. First, it indicates whether a quantified formula Qi is active (li assigned to true) or inactive (li assigned to false). Second, it focuses on finding counterexamples that falsify the body of Qi.

The main loop of procedure **syqi** is provided in lines 6-11. Each iteration starts with a quantifier-free satisfiability check (performed by procedure **check** on line 7) on the current set of ground formulas G in the combined theory T ∪ TD. If G is unsatisfiable, procedure **syqi** returns unsat. If G is satisfiable, the procedure further checks whether it can find a counterexample for any of the quantified formulas Q1,...,Qn, which is done by checking the satisfiability of G∧(l1∨...∨ln). If the check returns unsat then no more counterexamples can be found; the algorithm concludes that input set is satisfiable and returns sat. The reason is that, in this case, the set G is satisfiable and entails each input formula, as proven later in this section. If the second call to **check** (line 8) returns sat, it additionally returns (a finite representation of) a model I for the current set of ground formulas G. Since I satisfies l1 ∨ ... ∨ ln, it does not satisfy at least one quantified formula in Q1,...,Qn. 4 For each active quantified formula in I, we generate new lemmas via procedure **select lemmas**L (lines 10-11), and repeat the main loop of the algorithm. Note that the second satisfiability check can be avoided by employing a special decision heuristic for counterexample literals li in the SAT solver. The decision heuristic will always assign a counterexample literal li to true on a decision. Consequently, li can only be assigned to false in a candidate interpretation I if ¬li is entailed by the set of ground formulas G.

Procedure **select lemmas**L takes a formula ∀*x*. P[*x*] and a model I as arguments and generates a set of lemmas based on I and selection strategy L. The procedure maintains the invariant of always returning a set of lemmas L where L \ G is non-empty. This set L includes a single instantiation lemma (of the form P[*t*]) and an evaluation unfolding lemmas (see below) for each variable x ∈ *x*. The returned lemmas are generated based on one of three lemma selection strategies: priority-inst, priority-eval, and interleave. Strategy interleave selects both the instantiation lemma and a set of evaluation unfolding lemmas at the same time. Strategies priority-inst and priority-eval give priority to instantiation lemmas and evaluation unfolding lemmas, respectively; i.e., strategy priority-inst selects the instantiation lemma and only selects evaluation unfolding lemmas if the instantiation lemma was already in G. Analogously, priority-eval gives priority to evaluation unfolding lemmas.

The various lemmas are constructed as follows. For each variable x ∈ *x* we use the model value dI x of datatype constant dx to construct the corresponding term **to term**(dI x) in the theory of variable x (line 15). The constructed term corresponds to a term synthesized by the SyGuS extension of our datatypes

4 Note that this does not mean the quantified formula is unsatisfiable, only that it is not satisfied in I.

solver based on the grammar specified for x. To ensure that dx evaluates to the same values as term **to term**(dI x) under model value dI x, we generate the evaluation unfolding lemma **explain**(dx ≈ dI x) ⇒ edx ≈ **to term**(dI x). The explanation for the model value dI x is expressed in terms of discriminator predicates. For example, if value dI x represents term a + b, the procedure generates lemma isplus(dx) ∧ isa(selZ,1(dx)) ∧ isb(selZ,2(dx)) ⇒ edx = a + b. As a last step, **select lemmas**L selects a non-empty subset of the generated instantiation lemma P[t1,...,tp] (where each ti is **to term**(dI xi )) and the evaluation unfolding lemmas L according to the lemma selection strategy L.

We now discuss the correctness properties of our approach. In the following, we say a grammar R for sort σ is complete, if for all interpretations I and values v of sort σ, it generates at least one term t such that t I = v. Note that we only consider complete grammars in this paper. We say a lemma selection strategy L is fair wrt a set of formulas G if it returns a set of lemmas that contain at least one lemma inequivalent to each formula in G whenever such lemma exists.

**Theorem 1.** Let T be a theory with signature Σ, let F be a set of universal formulas {Q1,...,Qn} and G0 is a set of quantifier-free formulas. If all grammars constructed by the calls to *grammar*S in *syqi* are complete and the selection strategy L used for *select lemmas*L is fair, then the following statements hold:

Conceptually, the proof of refutational soundness relies on the fact that all lemmas added to G are entailed by the input or maintain equisatisfiability with respect to the input. The proof of model soundness relies on the fact that when G collectively entails the negation of (all) quantified formulas, then the current model I for G must be a model for all quantified formulas. Procedure **syqi** is not terminating in general. However, the progress property guarantees that the algorithm does not get stuck in a single state and keeps making progress towards refining the set of possible models by ruling out at least one candidate model at each iteration of the procedure's main loop.

Proof. For brevity, we show these statements for the case of n = 1 and where Q1 is ∀*x*. P[*x*]; the proof can be easily lifted to n > 1. When **syqi**(F, G0) terminates, the internal set G is the union of:

To show (1), assume that ϕ is satisfied by some Σ-interpretation J , where without loss of generality assume that l J is false. Let I be a Σ∪ΣD-interpretation that extends J such that for each evaluation variable ed, the interpretation of d in I is such that **to term**(dI)I = eI d . Such a value exists since our grammars are complete by assumption. We show that I satisfies each formula ψ in G. If ψ ∈ G0, then this holds since J satisfies ϕ, and hence, by extension I does as well. If ψ ∈ Gcex, then ψ is satisfied by I since it interprets li as false. If ψ ∈ Ginst is an instantiation lemma of some Qi, then it is satisfied by I since J also satisfies Qi. If ψ ∈ Gev is an evaluation lemma, this is satisfied by our construction of dI. Thus ϕ is T-satisfiable, then G must be (T ∪ TD)-satisfiable. Thus, since **syqi**(F, G0) returns unsat when G is (T ∪ TD)-unsatisfiable, this means that F ∪ G0 must be T-unsatisfiable as well.

To show (2), if **syqi**(F, G0) returns sat, then the set G is satisfied by some Σ∪ΣD-interpretation and G∪{l1} is unsatisfiable. Let J be the Σ-interpretation that interprets all symbols in Σ the same as in I. Since G∪ {l1} is unsatisfiable, we have that G0 ∪ Ginst ∪ Gev ∪ {¬P[**e***dx* ]} is T ∪ TD-unsatisfiable. Since all Σinterpretations can be lifted to a Σ ∪ ΣD-interpretation satisfying Gev, it must also be the case that G0∪Ginst∪ {¬P[**e***dx* ]} is T-unsatisfiable. Hence, all models of G0 ∪ Ginst must make P[**e***dx* ] true. Since **e***dx* does not occur in G0 ∪ Ginst, this implies that all models of G0 ∪ Ginst satisfy ∀*x*. P[*x*]. Since G0 ∪ Ginst ⊆ G and I satisfies G, we have that J satisfies {∀*x*.P[*x*]} ∪ G.

To show (3), assume ad absurdum that G is satisfied by a T ∪ TD-interpretation I where **to term**(*dx* I) = *t* and Q1 is active in I. Also assume that G contains the evaluation unfolding lemmas for *dx* I and the instantiation lemma P[*t*]. Due to the former, we have that **e***dx* I = *t*I. Since Q1 is active in I, I satisfies ¬P[**e***dx* ]. However, P[*t*] is also satisfied by I, a contradiction. Thus, at least one of the lemmas returned by **select lemmas**L for Q1 must be inequivalent to the lemmas in G, due to our assumption that L is a fair selection strategy.

#### **3.1 Grammar Construction**

For quantifier instantiation, we focus on the theories of fixed-size bit-vectors, floating-point numbers, integers, and reals as defined by the SMT-LIB 2 standard [4]. The signature of the theory of fixed-size bit-vectors includes a unique sort for each positive bit-vector width n, denoted here as BV[n]. The signature of the theory of floating-point numbers includes a rounding-mode sort RM and a unique floating-point sort for each combination of positive exponent width e and significand width s, denoted here as FP[e,s]. The theories of Integers and Reals include the integer sort Int and the real sort Real, respectively. For each of these sorts we define a SyGuS grammar that includes the following operators and constants.

RBV : {∼ , −, &, |, ⊕, +, ·, ÷, ÷s, mod, mods <<, >>, >>a, 0, 1, ones, smin, smax} RFP : {−, abs, rem, √, rti, +, ·, ÷, fma, NaN, ±∞, ±0, ±mins , ±maxs , ±minn, ±maxn} RRM : {RNA, RNE, RTE, RTP, RTZ} RInt : {+, −, 0, 1} RReal : {+, −, ÷, 0, 1}

**Table 1.** Set of operators considered in SyGuS grammars.

The (non-constant) operators and their SMT-LIB names and types are listed in Table 1. Note that we further restrict the division operator ÷ of sort Real to division by value, i.e., we do not allow division by an arbitrary term of sort Real. We also add a set of special values of the corresponding sort to each default grammar. We represent bit-vector values of sort BV[n] as bit-strings of length n, where the left-most bit is the most significant bit. For floating-point values of sort FP[e,s], we use bit strings where the left-most bit indicates the sign, the following e bits represent the exponent, and the remaining bits the significand. For the theory of fixed-size bit-vectors, we use smax[n] or smin[n] for the maximum or minimum signed value of width n, e.g., smax[4] = 0111 and smin[4] = 1000, and ones[n] for the maximum unsigned value, e.g., ones[4] = 1111. For the theory of floating-point numbers, we use ±0 for positive and negative zero, ±∞ for positive and negative infinity, and NaN for not a number, e.g., −0[3,5] = 10000000 and +∞[3,5] = 01110000. We further use ±mins for the positive and negative smallest subnormal, ±maxs for the positive and negative largest subnormal, ±minn for the positive and negative smallest normal, and ±maxn for the positive and negative largest normal, e.g., −maxs [3,5] = 10001111 and +minn [3,5] = 00010000. In the definition of grammar RFP above, we use symbol ± to indicate that both the positive and negative variant of a special value is included in the grammar.

We extend the above set of default grammars (**grammar**S in Algorithm 1) with ground terms that occur in an input set {Q1,...,Qn}∪G0 based on the sort of variable x ∈ *x* in Qi = ∀*x*. P[*x*] and a term selection strategy. This strategy is based on the following two factors. We consider three modes for the scope of ground terms: (1) ground terms that occur in quantified formula Qi (strategy in) (2) ground terms that occur in the set of ground formulas G (strategy out), and (3) the union of (1) and (2) (strategy both). We consider three modes for the size of ground terms, defined as the number of subterms a term consists of: (a) terms of minimal size, i.e., constants that occur in a term (strategy min) (b) terms of maximal size (strategy max), and (c) the union of (a) and (b) (strategy both). For example, for a ground term a + b · c, strategy min will select a, b, c, max will select a+b · c, and both will select a, b, c, a+b · c. Each of the scope and size modes may be combined, giving 3 ∗ 3 = 9 possible term selection strategies.

Example 1. Let Q = ∀x. x·x ≈ a·a+b · b+ 2 ·a· b where x, a, b have integer type and suppose we run **syqi**({Q}, ∅). The algorithm first constructs the grammar **grammar**S (x) for x, where we assume term selection strategy S with scope in and size min, which considers ground terms that occur in Q and are of minimal size (2, a, and b). This grammar is encoded as the following datatype Z:

$$\mathcal{Z} = \mathsf{zero} \mid \mathsf{one} \mid \mathsf{plus}(\mathcal{Z}, \mathcal{Z}) \mid \mathsf{minus}(\mathcal{Z}, \mathcal{Z}) \mid \mathsf{two} \mid \mathsf{a} \mid \mathsf{b}$$

The algorithm introduces a fresh datatype variable dx of type Z, a fresh integer variable edx of integer type, and adds l ⇒ edx · edx ≈ a · a + b · b + 2 · a · b to the internal set G of ground formulas, where l is a fresh Boolean variable. In the first iteration of the loop, we have that G (and G ∪ {l}) are satisfiable. Hence, the algorithm calls **select lemmas**L on Q and a model I for G; assume that dI x = zero and eI dx = aI = bI = 0. Based on the lemma selection strategy, we may choose to add the instantiation lemma 0 · 0 ≈ a · a + b · b + 2 · a · b, or the evaluation lemma iszero(dx) ⇒ edx ≈ 0, or both lemmas to G. Assuming both lemmas are added to G, the next iteration of the loop will consider a new model I where dI x = zero and eI dx = 0. The algorithm will continue finding models with new values for dx, until it finds a model I where dI x = plus(a, b). At this point the instantiation lemma (a+b)·(a+b) ≈ a · a+b · b+ 2 · a · b will be added to G, which is equivalent to false, and **syqi** will terminate with unsat.

#### **3.2 Implementation Details**

We implemented syntax-guided quantifier instantiation in the CVC4 [5] solver, which has support for a wide range of background theories, covering all those in the SMT-LIB standard library [2]. CVC4 is based on the CDCL(T) (formerly DPLL(T)) framework [19]. This framework integrates a propositional SAT solver, which attempts to find a Boolean assignment that propositionally satisfies the input formula, with one or more specialize theory solvers, which monitor the assignments made by the SAT solver to theory literal and flag a conflict if the assignments are ever inconsistent in their theory.

Our SyQI technique is implemented as a module of the subsolver of CVC4 that handles quantified formulas. We leverage CVC4's support for smart enumerative SyGuS as described in Reynolds et al. [22]. Specifically, the **check** method in line 7 in Algorithm 1 involves calling the (combination) of quantifier-free theory solvers, which includes an extension of the theory of datatypes described in the following.

Symmetry Breaking for Smart Enumerative Synthesis. As described in previous work [22, 24], CVC4 uses advanced techniques for symmetry breaking for the datatypes over which context-free grammars are embedded. The quantifier-free

datatype theory solver in CVC4 is extended to issue symmetry blocking clauses based on reasoning about such datatypes, so that the models we generate for a datatype variable d are such that **to term**(d) is unique with respect to rewriting. For example, the terms a + b and b + a are equivalent, and in CVC4, one will be rewritten to the other. Thus, we know that we only have to consider one variant, e.g., a + b. Hence, the extended datatypes solver may issue the blocking clause ¬isplus(d) ∨ ¬isb(selZ,1(d)) ∨ ¬isa(selZ,2(d)), effectively stating that the term associated with d should not be b + a. This technique is highly valuable for syntax-guided synthesis, since it reduces the set of terms considered in the search for candidate solutions. In the context of this work, these techniques are of great importance, since they guarantee that our algorithm does not consider multiple instantiations over tuples of pairwise equivalent terms.

Quantified Formulas within Boolean Structure and Nested Quantification. As mentioned earlier, while not shown in Algorithm 1, our approach uses standard techniques for handling qeneral quantified formulas, in particular with quantifiers that occur below Boolean connectives. In the context of CDCL(T), for each quantified formula Qi of the form ∀*x*. P[*x*], the propositional model of our Boolean structure may either assign Qi to true or false, or leave it unassigned. Quantified formulas that are assigned to false are Skolemized, i.e., a lemma of the form ¬Qi ⇒ ¬P[*k*], where *k* are fresh constants, is returned to the SAT solver. Quantified formulas that are unassigned are ignored. Quantified formulas that are assigned to true are either active or inactive based on the value assigned to their counterexample literals. Those that are active are processed via **select lemmas**L. In practice, instantiation lemmas are guarded so that Qi ⇒ P[*t*] is returned to the SAT solver, meaning that the conclusion only holds when Qi is assigned to true. Furthermore, each Qi may have nested quantification, that is, the formula P the counterexample lemma li ⇒ ¬P[**e***dx* ] may contain quantified subformulas. Those quantified formulas are then processed by our full algorithm in the same way as quantified formulas from the input.

#### **4 Experiments**

We implemented our approach in the SMT solver CVC4 [5]. We provide here an extensive evaluation of the techniques and strategies described in Section 3. We first evaluate term and lemma selection strategies for grammar construction, and then compare the performance of our best configuration against Z3 [16], the only state-of-the-art SMT solver besides CVC4 that supports all the logics supported by our implementation.

We performed all experiments on a cluster with Intel Xeon CPU E5-2620 CPUs with 2.1GHz and 128GB memory. We used a time limit of 300 seconds, and an 8GB memory limit for each solver/benchmark pair and count memory out as time out. We evaluate here all configurations on all quantified logics in SMT-LIB [2] that do not contain uninterpreted functions (UF). As an exception, we include the logic UFBV, since the benchmarks in this logic rely

**Table 2.** Selection strategies on considered logics (15,746 benchmarks).

almost entirely on BV reasoning only. We generally exclude logics with UF since for such logics counterexample-guided techniques, as in our approach, are not expected to be more effective than heuristic instantiation techniques such as E-matching, which we confirmed in a preliminary evaluation. Overall, we include logics BV (bit-vectors), FP (floating-point arithmetic), LIA (linear integer arithmetic), LRA (linear real arithmetic), NIA (non-linear integer arithmetic), NRA (non-linear real arithmetic), and their combinations BVFP, BVFPLRA, FPLRA, and UFBV. In total, our benchmark set consists of 15,746 benchmarks.

**Term Selection for Grammar Construction.** As a first experiment, we determine the best combination of scope-based and size-based ground term selection strategies for grammar construction as introduced in Section 3.1. We combine strategies based on scope with strategies based on term size into nine selection strategies: in-min, in-max, in-both, out-min, out-max, out-both, both-min, both-max, both-both. The results for our SyGuS instantiation approach with these strategies enabled is shown in Table 2. Note that preliminary experiments identified lemma selection strategy interleave as the best. Hence, we use strategy interleave as the lemma selection strategy for this experiment.

Overall, using strategy both for the scope performs best. Furthermore, for this strategy all three size-based strategies perform equally well. For the remaining experiments, we use strategy both-both as the term selection strategy for grammar construction, where both minimal and maximal ground terms are selected from both the quantified formula Qi (containing the variable we construct a grammar for) and the set of ground formulas G. Note that we choose the more general strategy both-both over strategy both-max even though both-max performs slightly better.

**Lemma Selection.** In our second experiment, we determine the best lemma selection strategy out of the three strategies priority-inst, priority-eval and interleave described in Section 3. The results are shown in Table 2. Note that we use the previously determined best term selection strategy both-both in this experiment.

The best overall strategy is interleave, indicating that it is beneficial to consider instantiation lemmas and evaluation unfolding lemmas in parallel. On the other hand, prioritizing evaluation lemmas over instantiation lemmas (priorityeval) performed significantly worse than the other two configurations. Since this strategy prioritizes evaluation lemmas, it has the advantage over other configurations of delaying instantiations until we obtain an interpretation I where the interpretation of edx is consistent with respect to dx, i.e., eI dx = **to term**(dx)I. As a consequence, prioritizing evaluation lemmas puts more effort into finding terms in instantiation that are guaranteed to refine the current candidate model I. However, we conclude from these results that it is often effective to consider instantiations in an eager fashion, either in parallel or even before considering evaluation lemmas. This is likely because instantiation lemmas may often refine the set of possible models even when G does not yet force our evaluation variables to have an interpretation that is consistent with their corresponding datatype values. Nevertheless, we found that evaluation lemmas are often necessary in practice for ensuring our procedure does not get stuck on a single model. When only instantiation lemmas are used, our procedure often terminates the loop with no new lemmas. This is to be expected, as such a strategy violates the requirements for the progress property of Theorem 1.

In the remaining experiment, we use strategy interleave as the lemma selection strategy since it performs slightly better than priority-inst.

**Comparison Against Other Techniques.** Finally, we compare our SyGuS instantiation approach against other techniques implemented in CVC4, the stateof-the-art SMT solvers Z3 [16] (version 4.8.9) and Boolector [17] (version 3.2.1), and the superposition-based theorem prover Vampire [13] (version 4.5.1). Note that Boolector implements counterexample-guided model synthesis [20] but only supports the SMT-LIB logic BV, whereas Vampire supports LIA, LRA, NIA, and NRA. We consider the following four configurations of CVC4: **ematch**: with E-matching [15] enabled; **cegqi**: with CEGQI for linear arithmetic [25] and bit-vectors [18] enabled, falls back to value-based instantiation techniques for other theories; **enum**: with enumerative instantiation [21] enabled; **syqi**: with our SyGuS instantiation approach enabled. We use strategy both-both for term selection, and interleave for lemma selection.

The results are summarized in Table 3. First, note that Z3 disagrees on 10 benchmarks in logic FP with the other four CVC4 configurations. This is due to a known problem in Z3 related to operator rem, where it answers sat instead of unsat. We do not count these 10 benchmarks as solved and give the number of disagreements in parenthesis marked with a \* in Table 3.

Overall, note that E-matching (**ematch**) performs very poorly on these benchmark sets. This is not surprising since it is designed with a focus on problems with uninterpreted functions. To a lesser extent, enumerative instantiation (**enum**) also performs poorly, probably also due to the fact that it is not designed for inputs without uninterpreted functions. In detail, both this configuration and

**Table 3.** SyQI vs. other techniques, Z3, Boolector, and Vampire (15,746 benchmarks).

**syqi** are enumerative in nature. The former uses a selection strategy based on the evolving ground terms in the current context, whereas the latter uses a fixed grammar built from the initial set of terms. In a sense, **syqi** leverages the power of a grammar for discovering new terms, whereas **enum** adapts to what terms are generated by instantiations. Overall, **syqi** solves 556 more benchmarks than enumerative instantiation, justifying the need for a syntax-guided approach for instantiation for inputs that are rich in background theories.

Our results show that **syqi** is remarkably competitive when compared to **cegqi**, which uses the best known theory-specific instantiation strategies. The performance of syntax-guided instantiation matches or exceeds counterexampleguided instantiation on logics BVFP, BVFPLRA, FP, FPLRA, NIA, NRA, and UFBV. In particular, for quantified floating-point arithmetic (FP), the performance of **syqi** significantly outperforms **cegqi**, where it solves 224 more benchmarks. We attribute this to the fact that **cegqi** only performs value-based instantiation, whereas the use of grammars is effective in determining useful symbolic terms to use in instantiations for this theory. Interestingly, **syqi** solves the only satisfiable benchmark in the NIA category that is unsolved by **cegqi**, meaning that in a portfolio setting with all available configurations, CVC4 solves all benchmarks in this category. On the other hand, counterexample-guided instantiation outperforms **syqi** on logics such as LIA, LRA, and BV, where wellestablished instantiation strategies exist. Syntax-guided techniques are especially ineffective for linear real arithmetic, since it is often important to construct specific real constants based on solving sets of linear (in)equalities [25].

Comparing all configurations of CVC4 with Z3, Boolector, and Vampire, we see that in some logics like LIA and NIA, counterexample-guided instantiation in CVC4 outperforms Z3 and Vampire, whereas in other logics like NRA, UFBV, and many logics that combine BV, FP and LRA, Z3 performs best. For the logic BV, Boolector outperforms CVC4 and Z3; however, CVC4 solves the most unsatisfiable instances. The **syqi** configuration performs best on the floatingpoint benchmarks, where it solves 181 more than the closest competitor. When comparing the four CVC4 configurations in terms of uniquely solved instances, **cegqi** uniquely solves 660 instances, **syqi** 119 instances, **enum** 117 instances, and **ematch** not a single one. Between configurations **cegqi** and **syqi**, the former uniquely solves 1479 instances, and the latter 402 instances.

In summary, theory-specific approaches as implemented in CVC4, Z3, and Boolector outperform **syqi** in categories where instantiation strategies are highly mature, such as linear integer and real arithmetic, and fixed-width bit-vectors. Nevertheless, our evaluation demonstrates the versatility of the approach, especially for benchmarks using quantified floating-point arithmetic or combined theories where no good approach to quantifier instantiation was known.

#### **5 Conclusion**

We have presented a syntax-guided approach for quantifier instantiation and implemented it in the SMT solver CVC4. Our experiments show that our approach is a viable alternative to theory-specific quantifier instantiation techniques and can be applied to a wide range of logics. In particular, for the theory of floatingpoint arithmetic, syntax-guided instantiation in CVC4 significantly outperforms the state of the art. In future work, we plan to tune our grammar construction based on an analysis of which terms are more likely to appear in conflicts, which can potentially be done automatically. Another direction of future work is to provide an interface that would allow users to supply their own grammars for use in SyQI, similarly to the user-provided triggers for E-matching. We also plan to use our approach as a baseline for quantified logics in recent (and future) new theories. Currently, support in SMT solvers is highly limited, for instance, for quantified formulas involving the theory of strings and regular expressions. Syntax-guided instantiation can serve as a baseline for potential user applications that rely on quantified formulas in these theories.

#### **References**

1-7, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9195, pp. 197– 213. Springer (2015). https://doi.org/10.1007/978-3-319-21401-6 13, https://doi. org/10.1007/978-3-319-21401-6 13

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### **Making Theory Reasoning Simpler**

Giles Reger1, Johannes Schoisswohl1(-) , and Andrei Voronkov1,2

> 1 University of Manchester, Manchester, UK 2 EasyChair, Manchester, UK<EMAIL_ADDRESS>
**Abstract** Reasoning with quantifiers and theories is at the core of many applications in program analysis and verification. Whilst the problem is undecidable in general and hard in practice, we have been making large pragmatic steps forward. Our previous work proposed an instantiation rule for theory reasoning that produced pragmatically useful instances. Whilst this led to an increase in performance, it had its limitations as the rule produces ground instances which (i) can be overly specific, thus not useful in proof search, and (ii) contribute to the already problematic search space explosion as many new instances are introduced. This paper begins by introducing that specifically addresses these two concerns as it produces general solutions and it is a simplification rule, i.e. it replaces an existing clause by a 'simpler' one. Encouraged by initial success with this new rule, we performed an experiment to identify further common cases where the complex structure of theory terms blocked existing methods. This resulted in four further simplification rules for theory reasoning. The resulting extensions are implemented in the Vampire theorem prover and evaluated on SMT-LIB, showing that the new extensions result in a considerable increase in the number of problems solved, including 90 problems unsolved by state-of-the-art SMT solvers.

#### **1 Introduction**

Many applications of reasoning in program analysis and verification depend on reasoning with the first-order theory of arithmetic, often in combination with other theories and quantifiers. A common approach to this problem is via Satisfiability Modulo Theory (SMT) solving, which has strong support for decidable theories but may struggle to scale in the presence of quantifiers. Conversely, superposition-based first-order solvers handle quantifiers naturally and have, recently, been extended to reason with theories [2,3,5,6,9,13,16,21]. Such solvers are based on a saturation loop and tend to suffer from search space explosion. This is compounded by the effective but explosive use of theory axioms, leading to the derivation of numerous inconsequential consequences of the theory. So far we have attempted to control this explosive behaviour [10,17] but now we aim to eliminate some of it. This paper introduces a set of simplification rules for reasoning in the theory of (any combination of linear or non-linear real, rational, or integer) arithmetic, i.e. rules that make reasoning in arithmetic simpler.

c The Author(s) 2021

J. F. Groote and K. G. Larsen (Eds.): TACAS 2021, LNCS 12652, pp. 164–180, 2021. https://doi.org/10.1007/978-3-030-72013-1\_9

This work was motivated by our previous attempt [20] to find useful instances of first-order clauses that would be otherwise difficult to find via reasoning with theory axioms. For example, when considering the two clauses

$$r(7x) \qquad \neg r(6+y) \lor p(y)$$

our previous work would apply resolution on r(7x) and ¬r(6+y) using unification with abstraction to produce the clause 7x = 6+y ∨p(y) and then applied theory instantiation, utilising an SMT solver to find the substitution {x → 1, y → 1}, producing the instance p(1). This may or may not be useful to proof search and, crucially, we need to keep performing inferences with the original clauses in case it is not. In this case, we would prefer to instantiate with {y → 7x − 6} to produce 7x = 6 + (7x − 6) ∨ p(7x − 6), which can be reduced to p(7x − 6). This is a general solution (being logically equivalent) that is also simpler – in this case it has fewer variables than the original clause. Hence, we replace the clause by the more general result, aiding proof search and preventing the addition of unnecessary instances.