1 Introduction↩︎

Functional programs often interact with stateful libraries that hide internal state behind their APIs. Such libraries are a vital component of a programming language’s ecosystem, providing well-tested implementations of databases, key-value stores, logging and system services, and other stateful abstractions. A common use case for how these libraries are used is for programmers to build higher-level data structures on top of the abstractions they provide [1]. A set abstract data type (ADT) equipped with intersection and cardinality operations, for example, might use the aforementioned key-value library to maintain a persistent collection of its elements by associating those elements (represented as values) with unique ids (their associated keys). Since the internal state of the underlying stateful library is opaque to its clients, the implementations of these higher-level modules will necessarily be expressed in terms of the operations provided by the library: the methods of the set ADT might use methods like and to interact with the backing key-value store, for example. To maximize reusability, these low-level libraries are typically quite permissive in how client may use them, resulting in weak specifications that only describe simple algebraic or equational constraints. For example, the specification of the key-value store might state that two operations over distinct keys commute or that a operation on a key always returns the last value in that key.

In contrast, the higher-level abstractions provided by clients built on top of these libraries are equipped with stronger guarantees: for example, the operations of our set ADT need to respect the semantics of mathematical sets, for example, so that \(\forall A\; B : \Code{Set.t}.\; |A \cup B| + |A \cap B| = |A| + |B|\). Verifying such semantically rich properties typically requires a strong guarantee that the internal state of the set library is consistent with the abstract states of the datatype, i.e., the ADT implementation should be equipped with a representation invariant [2], [3]. Ensuring that distinct keys are always associated with distinct values allows us to prove the above relationship between the intersection and cardinality operations of the set ADT, for example. Establishing such an invariant is complicated by the fact that our set ADT is built on top of another library with an opaque internal state, and whose weak specifications do not directly address the notion of uniqueness central to the set ADT. This paper presents an automated type-based verification procedure that addresses these complications.

Our proposed solution augments a refinement type system for a call-by-value functional core language that supports calls to stateful libraries, with Hoare Automata Types (HATs). HATs are a new type abstraction that qualifies basic types with pre- and post-conditions expressed as symbolic finite-state automata [4], [5], a generalization of finite-state automata equipped with an unbounded alphabet, and whose transitions are augmented with predicates over the elements of this alphabet. HATs serve as a compact representation of the trace of stateful API calls and returns made prior to a function invocation and those performed during its execution. As a result, HATs serve as an expressive basis for a fine-grained effect system within a general refinement type framework, enabling compositional reasoning about invocations of stateful APIs in a form amenable to automated verification of a client module’s representation invariant. For example, he representation invariant from our set ADT is captured by the following symbolic automaton, written using a variant of linear temporal logic on finite sequences [6]. The base predicates of this formula describe events, or invocations of the methods of a key-value store whose values are drawn from a \(\Code{setElem}\) type: \[\begin{align} &\riA{Set}(\Code{el}) \doteq \globalA (\evop{put}{key\,val}{\I{val} = \Code{el}} \impl \nextA \neg \finalA \evop{put}{key\,val}{\I{val} = \Code{el}}) \end{align}\] This representation invariant (\(\riA{Set}\)) is expressed using standard temporal logic modalities (e.g., \(\globalA\) (always), \(\nextA\) (next), and \(\finalA\) (eventually)) to express the history of valid interactions between the set implementation and the underlying key-value store that ensure the expected element uniqueness property holds. Informally, the invariant establishes that, at every step of the execution (\(\globalA(...)\)), once a value \(\Code{el}\) has been inserted into the set (\(\evop{put}{key\,val}{\I{val} = \Code{el}}\)), it will never be reinserted (\(\nextA \neg \finalA \evop{put}{key\,val}{\I{val} = \Code{el}}\)). An implementation that preserves this invariant guarantees that every value is always associated with at most one key.

To verify it, we can check the \(\Code{insert}\) method of the set ADT against the following type \[\begin{align} &\tau_{\Code{insert}} \doteq \gvn{el}{setElem} \Code{x}{:}\nuot{setElem}{\top} \sarr \htriple{\riA{Set}(\Code{el})}{\nuot{unit}{\top}}{\riA{Set}(\Code{el})} \end{align}\] The output type of \(\tau_{\Code{insert}}\) (\(\htriple{\riA{Set}(\Code{el})}{\nuot{unit}{\top}}{\riA{Set}(\Code{el})}\)) is a Hoare Automata Type (HAT) over the representation invariant \(\riA{Set}\). This type captures the behavior required of any correct implementation of \(\Code{insert}\): assuming the invariant holds for any value \(\Code{el}\) (encoded here as a ghost variable scoped using \(\garr\)) prior to the insertion of a new element \(\Code{x}\), it must also hold after the insertion as well. The precondition of the HAT captures the set of interactions that lead to a valid underlying representation state (namely, one in which every value in the store is unique), and the postcondition of the HAT specifies that this condition remains valid even after executing \(\Code{insert}\).

Our use of HATs differs in important ways from other type-based verification approaches for functional programs that allow computations to perform fine-grained effects, such as F* [7] or Ynot [8]. These systems use the power of rich dependent types to specify fine-grained changes to the heap induced by an stateful operation. The Dijkstra monad [9], [10] used by F*, for example, extends ideas first proposed by Nanevski et. al [11] in their development of Hoare Type Theory to embed a weakest precondition predicate transformer semantics into a type system that can be used to generate verification conditions consistent with a provided post-condition on the program heap.

Our approach also bears some similarity to recent (refinement) type and effect systems for verifying temporal properties of event traces produced during a computation [12], [13]. While the idea of using symbolic traces of previous observations as a handle to reason about the hidden state of a library is similar to these other efforts, incorporating return values of operations as part of such traces is a significant point of difference. This capability, critical for the validation of useful representation invariants, allows the precondition encoded in a HAT to describe a fine-grained context of events in which a program can run, expressed in terms of both library method arguments and return values. These important differences with prior work position HATs as a novel middle-ground in the design space between explicit state-based verification techniques and trace-based effect systems. Our formulation also leads to a number of significant technical differences with other refinement type systems [14] and their associated typing algorithms, since we must now contend with type-level reasoning over symbolic automata qualifiers.

In summary, this paper makes the following contributions:

1. We formalize a new trace-based specification framework for expressing representation invariants of functional clients of stateful libraries that manage hidden state.

2. We show how this framework can be embedded within a compositional and fine-grained effect-tracking refinement type system, by encoding specifications as symbolic automata and instantiated as HATs in the type system.

3. We develop a bidirectional type-checking algorithm that translates the declarative type system into efficient subtype inclusion checks amenable to SMT-based automated verification.

4. Using a tool () that implements these ideas, we present a detailed evaluation study over a diverse set of non-trivial OCaml datatype implementations that interact with stateful libraries. To the best of our knowledge, is the first system capable of automated verification of sophisticated representation invariants for realistic OCaml programs.

The remainder of this paper is organized as follows. In the next section, we provide further motivation for the problem by developing a running example, which is used in the rest of the paper. 3 introduces a core functional language equipped with operators that model stateful library methods. 4 presents a refinement type system that augments basic type qualifiers to also include HATs; a brief background on symbolic automata is also given. An efficient bidirectional typing algorithm is then presented in  5. Implementation details, as well as experimental results on its effectiveness in automatically verifying the representation invariants of a number of realistic data structure client programs that interact with stateful libraries is provided in 6. The paper ends with a discussion of related work and conclusions.

2 Motivation↩︎

To further motive our approach, consider the (highly-simplified) Unix-like file-system directory abstraction () shown in 1. This module is built on top of other libraries that maintain byte arrays () which hold a file or a directory’s contents and metadata, and which manipulate paths (), strings that represent fully-elaborated file and directory names. ’s implementation also uses an underlying key-value store library () to provide a persistent and scalable storage abstraction, where keys represent file paths and values are byte arrays. The interface to this store is defined by three stateful library methods: persistently stores a key-value pair \(\Pair{k}{v}\), adding the pair to the store if \(k\) does not already exist, and overwriting its old value with \(v\) if it does; returns true if the given key has been previously and false otherwise; and, returns the value associated with its key argument, and fails (i.e., raises an exception) if the key does not exist in the store.

1 shows three of the methods provided by : initializes the file system by storing a root path (““); allows users to add regular files or directories to the filesystem; and, logically removes files or directories from the filesystem. The latter two operations return a Boolean value to indicate whether they were successful. The \(\Code{add}\) operation succeeds (line \(15\)) only if (a) the given path does not already exist in the file system (line \(6\)) and (b) a path representing the parent directory for the file does exist (line \(9\)). Besides adding the file (line \(13\)), \(\Code{add}\) also updates the contents of the parent directory to make it aware that a new child has been added (line \(14\)). Similar to , requires that the supplied path exists and is not the root (line \(19\)). If the path corresponds to a directory, its children are marked deleted (line \(22\)) using procedure \(\Code{deleteChildren}\) (not shown). Additionally, the directory’s metadata, and that of its parent, are updated to record the deletion (lines \(25\) and \(26\)). Implicit in ’s implementation is the assumption that the parent path of the file to be deleted exists in the store: observe that there is no check to validate the existence of this path before the of the parent’s contents is performed on line \(24\). This assumption can be framed as a representation invariant that must hold prior to and after every call and return of and . Intuitively, this invariant captures the following property:
: Any path that is stored as a key in the key-value store (other than the root path) must also have its parent stored as a non-deleted directory in the store.

2.0.0.1 Representation Invariants

In a language that guarantees proper data abstraction, library developers can safely assume that any guarantees about an API established using a representation invariant are independent of a particular client’s usage. However, as we noted earlier, numerous challenges arise when validating a representation invariant in our setting because we can only characterize the state of the underlying library in terms of its admissible sequence of interactions with the client. In our example, this characterization must be able to capture the structure of a valid filesystem, in terms of sequences of , , and calls and returns that are sufficient to ensure that the invariant is preserved. Verifying that holds requires us to prove that, except for the root, the path associated with a file or directory can only be recorded in the store when its parent path exists, i.e., its parent has previously been and has not yet been deleted. Establishing that this property holds involves reasoning over both data dependencies among filesystem calls and temporal dependencies among store operations.

2.0.0.2 Events, Traces, and Symbolic Finite Automata

We address these challenges by encoding desired sets of stateful interactions between the client and library as symbolic finite automata (SFA). Besides constants and program variables, the alphabet of an automaton that captures these interactions includes a set of stateful operators \(\effop\) (e.g., and ). The language recognized by an automaton specifies the sequences of permitted library method invocations. Each such invocation (called an event) \(\pevapp{\effop}{\overline{v_i}}{v}\) records the operator invoked (\(\effop\)), a list of its arguments ( \(\overline{v_i}\)), and a single result value \(v\). It is critical that we record both inputs and outputs of an operation, in order to enable our type system to distinguish among different hidden library states. Consider, for example, a stateful library initialization operator \(\S{initialize}\) \(\Code{: unit\sarr bool}\). The hidden state after observing “\(\evapp{initialize}{()}{true}\)”, representing a successful initialization action, is likely to be different from the hidden state that exists after observing the event “\(\evapp{initialize}{()}{false}\)”, which indicates an initialization error. The language accepted by an SFA is a potentially infinite set of finite sequences of events, or traces.

    let add!$_\Code{bad}$! (path: Path.t) (bytes: Bytes.t) = !$\S{put}$! path bytes

2.0.0.3 Hoare Automata Types

While SFAs provide a convenient language in which to encode representation invariants, it is not immediately apparent how they can help with verification since, by themselves, they do not impose any safety constraints on expressions. To connect SFAs to computations, we embed them as refinements in a refinement type (and effect) system. In a standard refinement type system, the refinement type \(\rawnuot{b}{\phi}\) of an expression \(e\) uses a qualifier \(\phi\) to refine the value of \(e\). Similarly, a Hoare Automata Type (HAT), \(\htriple{A}{\rawnuot{b}{\phi}}{B}\), additionally refines a pure refinement type \(\rawnuot{b}{\phi}\) with two symbolic automata: a precondition automaton \(A\) defining an effect context under which \(e\) is allowed to evaluate, and a postcondition automata \(B\) that augments this context with the effects induced by \(e\) as it executes. A HAT thus allows us to track the sequence of stateful interactions between higher-level datatypes and the underlying stateful library, as well as to record the consequences of this interaction in terms of the return values of stateful calls.

Our type system leverages this information to verify the preservation of stated representation invariants in terms of these interactions. For example, and can be ascribed the following HAT-enriched types: \[\begin{align} \Code{add} :&\ \gvn{p}{Path.t} \normalv{path}{\nuot{Path.t}{\top}} \normalv{bytes}{\nuot{Bytes.t}{\top}}\htriple{\riA{FS}(\Code{p})}{\nuot{bool}{\top}}{\riA{FS}(\Code{p})} \\ \Code{delete} :&\ \gvn{p}{Path.t} \normalv{path}{\nuot{Path.t}{\top}} \htriple{\riA{FS}(\Code{p})}{\nuot{bool}{\top}}{\riA{FS}(\Code{p})} \end{align}\] Here, the notation “\(\gvn{p}{Path.t}\)” indicates that \(\Code{p}\) is a ghost variable representing an arbitrary path; thus, the representation invariant must hold over any instantiation of \(\Code{p}\). While their input arguments (\(\nuot{Path.t}{\top}\) and (\(\nuot{Bytes.t}{\top}\))) are unconstrained, the return types of these functions are expressed as HATs in which both the precondition and postcondition automata refer to the representation invariant for the file system, \(\riA{FS}(\Code{p})\). Informally, this type reads “if we invoke the function in a context that is consistent with \(\riA{FS}\), then the state after the function returns should also be consistent with \(\riA{FS}\)”. The traces admitted by an SFA are used to represent these contexts and states.

More concretely, observe that the trace \(\alpha_2\) from Example 1 is derived by concatenating \(\alpha_0\) with the library calls generated during the (symbolic) execution of : \[\begin{align} {\alpha_{\Code{new}} \doteq [\evapp{exists}{``/a/b.txt"}{false};\, \evapp{exists}{``/a"}{false}]} \end{align}\] (i.e., \(\alpha_2 = \alpha_0 \listconcat \alpha_{\Code{new}}\)). Note that both \(\alpha_0\) and \(\alpha_2\) satisfy the representation invariant \(\riA{FS}\). To admit this trace, our type system automatically infers a new automata \(A\) that accepts the sequence of events in \(\alpha_{\Code{new}}\) by type-checking . Verifying that the representation invariant holds now reduces to an inclusion check between two symbolic automata, requiring that the trace expected by the concatenated automata \(\riA{FS};A\) is also accepted by the representation invariant \(\riA{FS}\).

3 Language↩︎

To formalize our approach, we first introduce , a core calculus for effectful programs.²

3.0.0.1 Syntax

is a call-by-value lambda calculus with built-in inductive datatypes, pattern matching, a set of pure and effectful operators, and recursive functions. Its syntax is given in 2. For simplicity, programs are expressed in monadic normal-form (MNF) [15], a variant of A-Normal Form (ANF) [16] that permits nested let-bindings. The terms in are syntactically divided into two classes: values \(v\) and expressions \(e\), where the latter include both pure terms and those that have computational effects. Similar to the simply-typed lambda calculus, function parameters have explicit type annotations. is parameterized over two sets of primitive operators: pure operators (\(\primop\)) include basic arithmetic and logical operators, while examples of effectful operators (\(\effop{}\)) include state manipulating operators (e.g., // for interacting with a key-value store, or / for manipulating a stateful set library). We express sequencing of effectful computations \(e_1; e_2\) in terms of \(\Code{let}\)-bindings: \(e_1;e_2 \doteq \zlet{x}{e_1}{e_2}\), where \(x\) does not occur free in \(e_2\). The application \(e_1\,e_2\) is syntactic sugar for \(\zlet{x}{e_1}{\zlet{y}{e_2}{\zlet{z}{x\,y}{z}}}\).

3.0.0.2 Operational Semantics

Our programming model does not have access to the underlying implementation of effectful operators, so the semantics of constrains the behavior of impure operations in terms of the outputs they may produce. To do so, we structure its semantics in terms of traces that record the history of previous effectful operations and their results. The syntax of traces adopts standard list operations (i.e., cons \({::}\) and concatenation \(\listconcat{}\)), as shown in 3. Traces are lists of effect events \(\pevapp{\effop}{\overline{v}}{v}\) that record the application of an effectful operator \(\effop\) to its arguments \(\overline{v}\) as well as the resulting value \(v\). The traces \(\alpha_2\) and \(\alpha_1\) from Example 1 record the events generated by correct and incorrect implementations of the function of the ADT, for example.

The operational semantics of is defined via a small-step reduction relation, \(\steptr{\alpha}{e}{~\alpha'}{e'}\). This relation is read as “under an effect context (i.e., trace) \(\alpha\), the term \(e\) reduces to \(e'\) in one step and performs the effect \(\alpha'\)”, where \(\alpha'\) is either empty \(\emptr{}\) or holds a single event. The semantics is parameterized over two auxiliary relations, \(e \Downarrow v\) and \(\alpha \vDash e \Downarrow v\), used to evaluate pure and impure operations, respectively. 3 shows how the corresponding reduction rules use these relations.³ The reduction rule for pure operators (STPureOp) holds in an arbitrary effect context (including the empty one), and produces no additional events. The rule for effectful operators (STEffOp), in contrast, can depend on the current context \(\alpha\), and records the result value of the effectful operator in the event it emits. The multi-step reduction relation \(\msteptr{\alpha}{e}{\alpha'}{e'}\) defines the reflexive, transitive closure of the single-step relation; its trace \(\alpha\) records all events generated during evaluation.

4 Type System↩︎

The syntax of ’s types is shown in 4. Our type system uses pure refinement types to describe pure computations and Hoare Automata Types (HATs) to describe effectful computations. Our pure refinement types are similar to those of other refinement type systems [14], and allow base types (e.g., ) to be further constrained by a logical formula or qualifier. Qualifiers in are universally quantified formulae over linear arithmetic operations (\(\primop\)) as well as uninterpreted functions, or method predicates (\(\mpred\)), e.g., \(\Code{isRoot}\). Verification conditions generated by our type-checking algorithm can nonetheless be encoded as effectively propositional (EPR) sentences [17], which can be efficiently handled by an off-the-shelf theorem prover such as Z3 [18]. We also allow function types to be prefixed with a set of ghost variables with base types (\(\overline{x{:}b}\garr \tau\)). Ghost variables are purely logical – they can only appear in other qualifiers and are implicitly instantiated when the function is applied.

Unique to are the HATs ascribed to a stateful computation, which constrain the traces it may produce. HATs use Symbolic Finite Automata (SFAs) [5], [19], [20] to qualify traces, similar to how standard refinement types use formulae to qualify the types of pure terms. We adopt the symbolic version of linear temporal logic on finite traces [6] as the syntax of SFAs.⁴

As shown in 4, HATs support two kinds of atomic propositions, or symbolic effect events: \(\evop{\effop}{\overline{x}}{\phi}\) and \(\evparenth{\phi}\). A symbolic effect event \(\evop{\effop}{\overline{x}}{\phi}\) describes an application of an effectful operator \(\effop\) to a set of argument variables \(\overline{x}\) that produces a result variable \(\vnu\). The formula \(\phi\) constrains the possible instantiation of \(\overline{x}\) and \(\vnu\) in a concrete event. The other symbolic effect event, \(\evparenth{\phi}\), is used to constrain the relationship between pure values (e.g., ghost variables and function arguments). In addition to the temporal next (\(\nextA A\)) and until operators (\(A \untilA A\)), the syntax of HATs includes negation (\(\neg A\)), intersection (\(A \landA A\)), union (\(A \lorA A\)), and concatenation (\(A;A\)). 4 defines notations for other useful logical and temporal operators: implication (\(A \impl B \doteq \neg A \lor B\)), the eventually operator \(\finalA\), the globally operator \(\globalA\), and importantly, the last modality \(\lastA\), which describes a singleton trace, thus prohibiting a trace from including any other effects [6]. 4 also provides notations for specifying the value of an argument \(\evop{\effop}{{\overline{x}~\sim}{\text{v_x}}~\overline{x}}{\phi}\). As is standard, we abbreviate the qualified type \(\rawnuot{b}{\top}\) as \(b\).

::: {#ex:SFA+put+get .example} Example 4. This syntax can capture rich properties over effect contexts. For example, the following formulae concisely specify traces under which a key holds a certain value (\(\predA{stored}{}\)) and when a particular key exists in the current store (\(\predA{exists}{}\)):

:::

4.1 HATs, By Example↩︎

Formally, a Hoare Automata Type \(\htriple{A}{t}{B}\) qualifies a refinement type \(t\) with two SFAs: a precondition SFA \(A\) that captures the context traces in which a term can be executed and a postcondition SFA \(B\) that describes the effect trace after the execution of the term. Our type system also includes intersection types on HATs ( \(\tau \interty \tau\)), in order to precisely specify the behaviors of a program under different effect contexts.

::: {#ex:Typing+Delta .example} Example 5 (Built-in Effectful Operators). Our type system is parameterized over a (global) typing context \(\Delta\) containing the types of built-in operators. Intuitively, the signatures of effectful operators in \(\Delta\) captures the semantics the library developer ascribes to their API. Using the SFAs from Example 4, for example, the signatures of , , and are:

The postcondition SFAs of all three operators use \(\lastA\), to indicate that they append a single effect event to the end of the effect context (\(\evop{\effop}{\overline{v}}{\phi} \land \lastA\)). The type of permits it to be used under any context ( \(\globalA\topA\)). More interestingly, the built-in type of uses a ghost variable (\(\Code{a}\)) to represent the current value of the key \(\Code{k}\); its precondition stipulates that it should only be applied to keys that have been previously stored. Finally, the intersection type of describes two possible behaviors, depending on whether the key \(\Code{k}\) has been previously added to the store. :::

4.2 Typing Rules↩︎

4.2.0.1 Type contexts

A type context (shown in 4) is a sequence of bindings from variables to pure refinement types (i.e., \(t\)). Type contexts are not allowed to contain HATs, as doing so breaks several structural properties (e.g., weakening) that are used to prove type safety.⁵

4.2.0.2 Auxiliary typing relations

5 shows selected rules from three sets of auxiliary relations used by our type system. The first set describes the type erasure functions \(\eraserf{t}\), \(\eraserf{\tau}\), and \(\eraserf{\Gamma}\). The former two functions return basic types by erasing all qualifiers and automata from types, while the latter \(\eraserf{\Gamma}\) is the type context derived by applying \(\eraserf{...}\) to all of \({\Gamma}\)’s bindings. The second set describes well-formedness conditions on SFAs (\(\Gamma \wellfoundedvdash A\)) and types (\(\Gamma \wellfoundedvdash t\) and \(\Gamma \wellfoundedvdash \tau\)). These rules largely ensure that all the qualifiers appearing in a type are closed under the current typing context \(\Gamma\). The exceptions are \(\mathrm{\small WFInter}\), which stipulates that only HATs with the same basic type can be intersected, and \(\mathrm{\small WFHoare}\), which requires the language accepted by the precondition SFA to be a prefix of the postcondition automata (i.e., \(\langA{B} \subseteq \langA{A;\globalA\topA}\), where \(\globalA\topA\) denotes the SFA that accepts an arbitrary trace) after performing a substitution consistent with the current typing context (\(\sigma \in \denotation{\Gamma}\)); the functions \(\langA{...}\) and \(\denotation{...}\) are defined in the next subsection.

Our type system also uses a mostly-standard subtyping relation that aligns with the denotation of the types being related. 5 highlights key subtyping rules that do not have analogues in a standard refinement type system. The subtyping rule for symbolic automata (\(\mathrm{\small SubAutomata}\)) checks inclusion between the languages of the automata, after performing substitutions consistent with the current typing context. The subtyping rule for (non-intersected) HATs (\(\mathrm{\small SubHoare}\)) checks that the inclusion is contravariant over the precondition automata and covariant over the postcondition automata under the same context (i.e., the conjunction of \(B_1\) and \(B_2\) with \(A_2; \globalA\topA\)). The subtyping rules for the intersection of HATs - \(\mathrm{\small SubIntLL}\), \(\mathrm{\small SubIntLR}\), and \(\mathrm{\small SubIntR}\) - are standard. The \(\mathrm{\small SubIntMerge}\) rule additionally allows the precondition automata of intersected types to be merged. Finally, the subtyping rules for ghost variables either bind a ghost variable in the type context (\(\mathrm{\small SubGhostR}\)), or instantiate it to some concrete value (\(\mathrm{\small SubGhostL}\)).

A subset of our typing rules⁶ is shown in 6. Note that an stateful computations can only be ascribed a HAT. As mentioned in Example 5, our type system is parameterized over \(\Delta\), a typing context for built-in operators that provides HATs for both pure (TPOp) and effectful operators (TEOp). This system features the standard subsumption and intersection rules (TSub and TInter), which enables our type system to use fine-grained information about the effect context when typing different control flow paths. The rule TEPur allows a pure term to be treated as a computation that does not perform any effects.

4.2.0.3 Effectful operator application

TPOpApp is the standard rule for operator application in a typical refinement type system [14]. On the other hand, rule TEOpApp, the rule for effect operator application, with the help of the subsumption rule (TSub), allows operators to have function types whose ghost variables are instantiated properly; moreover, the return type of effect operators is a non-intersected HAT. After ensuring each argument \(v_i\) types against the corresponding argument type \(t_i\) and substituting all parameters (\(\overline{z_i}\)) with the supplied arguments (\(\overline{v_i}\)), the return type of an effectful operator must be in the form \(\htriple{A}{t_x}{A'}\) and have exactly the same precondition SFA (\(A\)) as the type of the surrounding term. Typing the -body \(e\) is similar to TPOpApp, where a new binding \(x{:}t_x\) is added to the type context. Moreover, the rule replaces the precondition SFA used to type the body of the with the postcondition SFA from the return type of the effect operator \(A'\), so that the body is typed in a context reflecting the use of the effectful operator.

4.3 Type Soundness↩︎

The denotation of a SFA \(\langA{A}\), shown in 7, is the set of traces accepted or recognized by the automata; the denotation of refinement types \(\denotation{t}\) and HATs \(\denotation{\tau}\) are sets of terms; these functions are defined mutually recursively.

The language of traces ranges over the set of all well-formed traces \(\mathit{Tr}^\boldsymbol{WF}\), i.e., those only containing events (\(\pevapp{\effop}{\overline{v_i}}{v}\)) that are well-typed according to the basic type system. As is standard [6], our denotation uses an auxiliary judgement \(\alpha,i \models A\) that defines when the suffix of a trace \(\alpha\) starting at the \(i^{th}\) position is accepted by an automaton. The denotation of an SFA \(A\) is the set of (well-formed) traces recognized by \(A\), starting at index \(0\).

4.3.0.1 Type denotations

Out type denotations use a basic typing judgement \(\emptyset \basicvdash e : s\) that types an expression \(e\) according to the standard typing rules of the simply-typed lambda-calculus (STLC), erasing all qualifiers in function argument types. The denotation of pure refinement types is standard [14]. The denotation of ghost variables is similar to function types whose parameters are restricted to base types. The denotation of an intersection type \(\tau_1 \interty \tau_2\) is the intersection of the denotations \(\tau_1\) and \(\tau_2\). An expression \(e\) belongs to the denotation of a HAT \(\htriple{A}{t}{B}\) iff every trace and value produced by \(e\) is consistent with the SFA \(B\) and refinement type \(t\), under any effect context accepted by the SFA \(A\). Intuitively, the denotation of a HAT is naturally derived from the language’s operational semantics, as depicted by the following correspondence: \[\begin{align} {3} \text{Pure Language:}&& \ \ \mstep{e}{v} &\impl e \in \denotation{\rawnuot{b}{\phi}} \ &&\text{ where } \phi[\vnu \mapsto v] \text{ is valid} \\ \text{\langname:}&& \ \ \msteptr{\alpha}{e}{\alpha'}{v} &\impl e \in \denotation{\htriple{A}{\rawnuot{b}{\phi}}{B}} \ &&\text{ where } \alpha \in \langA{A}, \alpha \listconcat \alpha' \in \langA{B}, \text{and }\phi[\vnu \mapsto v] \text{ is valid} \end{align}\] In a pure language with the simple multi-step reduction relation \(\mstep{e}{v}\), refinement types qualify the value \(v\) that \(e\) produces. In contrast, the multi-step reduction relation of , \(\msteptr{\alpha}{e}{\alpha'}{v}\) depends on the effect context \(\alpha\) and emits a trace \(\alpha'\) that records the sequence of effects performed by \(e\) during evaluation. Thus, HATs use precondition and postcondition automata (i.e., \(A\) and \(B\)) to qualify the trace before and after a term is evaluated (i.e., \(\alpha\) and \(\alpha \listconcat \alpha'\)).

4.3.0.2 Type context denotation

The denotation of a type context is a set of closing substitutions \(\sigma\), i.e., a sequence of bindings \(\overline{[x_i \mapsto v_i]}\) consistent with the type denotations of the corresponding variables in the type context. The denotation of the empty context is a singleton set containing only the identity substitution \(\emptyset\).

5 Typing Algorithm↩︎

Converting our declarative type system into an efficient algorithm requires resolving two key issues. First, we cannot directly use existing SFA inclusion algorithms [19], [20] to implement the check in SubAutomata, because our SFAs may involve non-local variables corresponding to function parameters and ghost variables; these variables can have refinement types. We deal with this wrinkle by integrating the subtyping algorithm for pure refinement types into the existing SFA algorithm. Second, typing the use of an effectful operator, e.g., or , depends on the set of effects in the precondition of the current HAT. The declarative type system can ensure that this automaton has the right shape by applying the TInter and TSub rules at any point in a derivation, but an efficient implementation must perform this conversion more intelligently. Our solution to this problem is to employ a bidirectional type system [21] that closely tracks a context of effects that have preceded the term being typed, and selectively applies the subsumption rule to simplify the context when switching between checking and synthesis modes.

5.1 SFA Inclusion↩︎

Symbolic alphabets allow the character domains of SFAs to be infinite, making them strictly more expressive than standard FAs. This enhanced expressivity comes at a cost, however, as the standard FA inclusion algorithm cannot be directly applied to SFAs. Thankfully, prior work has shown how to reduce an inclusion check over SFAs to an inclusion check over FAs [19], [20]. The high-level approach is to first construct a finite set of equivalence classes over an SFA’s infinite character domain, defined in terms of a set of maximal satisfiable Boolean combinations of logic literals (called minterms) in the automaton’s symbolic alphabet. An alphabet transformation procedure then replaces characters in the original SFA with their corresponding equivalence classes, and replaces the SFA’s symbolic alphabet with minterms, thus allowing SFAs to be translated into FAs. As long as the satisfiability of minterms is decidable, so is checking inclusion between two SFAs.

The pre- and post-conditions used in HATs have two features that distinguish them from standard SFAs, however: 1) characters are drawn from a set of distinct events and their qualifiers may range over multiple variables, instead of a single local variable; and, 2) event qualifiers may refer to variables in the typing context, i.e., function parameters and ghost variables.

5.1.0.1 Candidate Minterms

The first step in checking SFA inclusion is to construct the equivalence classes used to finitize its character set. With HATs, these characters range over events triggered by the use of library operations \(\pevapp{\effop}{\overline{v}}{v}\), and return events \(\pevappret{v}\). As each class of events is already disjoint (e.g., and events will never overlap), we only need to build minterms that partition individual classes. The minterms of each class of events have the form \(\evop{\effop}{\overline{x_i}}{(\bigwedge \overline{l_j}) \land (\bigwedge \overline{\neg l_k})}\). To build the literals used in these minterms for an event \(\effop\), we collect all the literals \(\overline{l}\) used to qualify \(\effop\), as well as any literals appearing in atomic predicates \(\evparenth{\phi}\), and then construct a maximal set of satisfiable Boolean combinations of those literals. Notably, these literals may contain variables bound in the current typing context.

5.1.0.2 Satisfiability Check

The soundness of the alphabet transfer procedure requires that only satisfiable minterms are used, so that every transition in the output FA corresponds to an actual transition in the original SFA. To understand how this is done, observe that the typing context plays a similar role in checking both the satisfiability of minterms and the subtyping relation. Thus, the algorithm reduces checking the satisfiability of \(\evop{\effop}{\overline{x_i}}{(\bigwedge \overline{l_j}) \land (\bigwedge \overline{\neg l_k})}\) to checking whether the refinement type \(\rawnuot{b}{(\bigwedge \overline{l_j}) \land (\bigwedge \overline{\neg l_k})}\) is not a subtype of \(\rawnuot{b}{\bot}\) (line \(8\)), that is \(\Gamma, \overline{x_i{:}b_i} \not\vdash \rawnuot{b}{(\bigwedge \overline{l_j}) \land (\bigwedge \overline{\neg l_k})} <: \rawnuot{b}{\bot}\). Since \(\rawnuot{b}{\bot}\) is uninhabited, this subtype check fails precisely when \((\bigwedge \overline{l_j}) \land (\bigwedge \overline{\neg l_k})\) is satisfiable under \(\Gamma\).

5.1.0.3 Inclusion Check

Equipped with the set of satisfiable minterms, the final inclusion check (line \(10\)) is a straightforward application of the textbook inclusion check between the FA produced by the standard alphabet transformation algorithm (line \(10\)).⁹

5.2 Bidirectional Type System↩︎

As is standard, our bidirectional type system consists of both type synthesis (\(\typeinfer\)) and type checking (\(\typecheck\)) judgments. The bidirectional system features a minor divergence from the declarative rules. While the declarative system was able to use the subsumption rule (TSub) to freely instantiate ghost variables, a typing algorithm requires a more deterministic strategy. Our solution is to treat ghost variables \(x{:}b \garr\) as instead being qualified by an unknown formula which is specialized as needed, based on the information in the current typing context.

With this minor tweak in hand, the top-level typing algorithm is mostly a matter of bidirectionalizing the typing rules of by choosing appropriate modes for the assumptions of each rule. This is largely straightforward: the type checking rule for ghost variables (ChkGhost) adapts the corresponding declarative rule (TGhost) in the standard way, for example. The rule for checking effectful operations (ChkEOpApp) is similar, although it adopts a fixed strategy for applying the subsumption rule: 1) instead of using TSub to instantiate ghost variables directly, it now relies on an auxiliary function, \(\effinfer\), to strengthen their qualifiers based on the current context; 2) when the result of the library operation \(\effop\) is an intersection type (\(\biginterty \overline{\htriple{A_i}{t_i}{A_i'}}\)), ChkEOpApp considers each case of the intersection, instead of using TSub to focus on a single case; and 3) instead of relying on TSub to align the postcondition automata (\(A_i'\)) of \(\effop\) with the precondition of the HAT being checked against (\(A\)), the rule uses the conjunction of the automata (\((A;\globalA\topA) \land A_i'\)) as the precondition automata used to check the term that uses the result of \(\effop\).

6 Implementation and Evaluation↩︎

We have implemented a tool based on the above approach, called , that targets ADTs implemented in terms of other stateful libraries. consists of approximately 12K lines of OCaml and uses Z3 [18] as its backend solver for both SMT and FA inclusion queries.¹¹

takes as an input the implementation of an ADT in OCaml, enhanced signatures of ADT operations that include representation invariants expressed as HATs, and specifications of the supporting libraries as HATs (e.g., the signatures in Example 5). The typing context used by includes signatures for a number of (pure) OCaml primitives, including the pure operators listed in 2. also includes a set of predefined method predicates (i.e., \(mp\) in 4) that allow qualifiers to capture non-trivial datatype properties. For example, the method predicates \(\Code{isDir}(\Code{x})\) and \(\Code{isDel}(\Code{y})\) from the motivating example in 2 encode that \(\Code{x}\) holds the contents of a directory, and that \(\Code{y}\) is marked as deleted, respectively. The semantics of method predicates are defined via a set of lemmas in FOL, in order to enable automated verification; e.g., the axiom \(\forall \Code{x}.\Code{isDir}(\Code{x}) \impl \neg\Code{isDel}(\Code{x})\) encodes that a set of bytes cannot simultaneously be an active directory and marked as deleted.

We have evaluated on a corpus of complex and realistic ADTs drawn from a variety of sources (shown in the title of [tab:evaluation]), including general datatypes such as stacks, queues, sets, heaps, graphs, as well as custom data structures including the Unix-style file system from 1 and the deterministic finite automata described in 4 (Q1). [tab:evaluation] presents the results of this evaluation. Each datatype includes multiple implementations using different underlying libraries (Library column), each of which provides a distinct set of operations. Our backing APIs include linked lists, a persistent key-value store, sets, trees, and graphs, each of which induces a different encoding of the target ADT’s representation invariant.

[tab:evaluation] divides the results of our experiments into two categories, separated by the double bars; the first gives comprehensive results about analyzing the entire datatype, while the second reports information about the most complex method of each ADT implementation.¹² The first group of columns describes broad characteristics of each ADT, including its number of methods (#Method), the number of ghost variables in its representation invariant (#Ghost), and the size of the formula encoding the representation invariant (s\(_I\)), after it is desugared into a symbolic regular expression. The next column reports the total time needed to verify all the method of each ADT (t\(_{\text{total}}\)). performs quite reasonably on all of our benchmarks, taking between 1.42 to 176.89 seconds for each ADT. As expected, more complicated ADT implementations (i.e., those with larger values in the #Method, #Ghost, and s\(_I\) columns), take longer to verify (Q3).

The first group of columns in the second half of [tab:evaluation] list features relevant to the complexity of the most demanding method in the ADT. These methods feature between \(3\) and \(5\) branches (#Branch) and \(3\) to \(12\) uses of built-in operators (#App). The last two groups of columns present type checking results for these methods. The #SAT and #FA\(_\subseteq\) columns list the number of SMT queries and finite automata (FA) inclusion checks needed to type check the method. The next column (avg. s\(_{\text{FA}}\)) gives the average number of transitions in the finite state automata (FA) after the alphabet transformation described in 5. These numbers are roughly proportional to code complexity (column #Branch and #App) and invariant complexity (column #Ghost and s\(_I\)) — intuitively, programs that have more uses of operators and larger specifications, require more queries and produce more complicated FAs. The last two columns report verification time for the method (Q3). These times are typically dominated by the SFA inclusion checks (ranging from .63 to 73.09 seconds) that result from minterm satisfiability checks during the alphabet transformation phase (t\(_{\text{SAT}}\)) and FA inclusion checks (t\(_{\text{FA}_\subseteq}\)). Unsurprisingly, generating more queries (both #SMT and #FA\(_\subseteq\)) result in more time spent checking minterm satisfiability and FA inclusion. Our results also indicate that FA inclusion checks are not particularly sensitive to the size of the FA involved; rather, the cost of these checks corresponds more closely to the deep semantics of the representation invariant, in which the choice of the underlying library is an important factor. Taking the FileSystem benchmark as an example, both Tree and KVStore implementations lead to similar sizes for the invariant, in term of #Ghost. s\(_I\), and FA (avg.s\(_{\text{FA}}\)). However, the use of the former library results in a significantly shorter verification time since the relevant property captured by the invariant “every child has its parent in the file system” is naturally supported by the Tree library; the only remaining verification task in this case for the client to handle involves ensuring these parents are indeed directories in the file system. In contrast, the KVStore provides no such guarantees on how its elements are related, requiring substantially more verification effort to ensure the invariant is preserved.

7 Related Work↩︎

Representation Invariant Inference. [3] develop a data-driven CEGIS-based inference approach, while  [2] develop a solution derived from examining testcases. Solvers used to infer predicates that satisfy a set of Constrained Horn Clauses (CHCs) [23]–[25] can also be thought of as broadly addressing similar goals. Our focus in this paper is orthogonal to these efforts, however, as it is centered on the automated verification of user-specified representation invariants expressed in terms of SFAs.

Effect Verification. There has been significant prior work that considers the type-based verification of functional programs extended with support for (structured) effectful computation. Ynot [8] and F* [7] are two well-known examples whose type specifications allow fine-grained effect tracking of stateful functional programs. These systems allow writing specifications that leverage type abstractions like the Hoare monad [11] or the Dijkstra monad [9], [10], [26]–[28]. For example, specifications using the Hoare monad involve writing type-level assertions in the form of pre- and post-conditions over the heaps that exist before and after a stateful computation executes. The Dijkstra monad generalizes this idea by allowing specifications to be written in the style of a (weakest precondition) predicate transformer semantics, thus making it more amenable for improved automation and VC generation. While our goals are broadly similar to these other efforts, our setup (and consequently, our approach) is fundamentally different. Because we assume that the implementation of effectful operations are hidden behind an opaque interface, and that the specifications of these operations are not tailored for any specific client application, our verification methodology must necessarily reason about stateful library actions, indirectly in terms of the history of calls (and returns) to library methods made by the client, rather than in terms of predicates over the concrete representation of the state. One important way that our significantly different representation choice impacts our verification methodology is that unlike e.g., the Dijkstra monad that uses a predicate transformer semantics to establish a relation between pre- and post-states of an effectful action, our typing of interaction history in terms of HATs allows us to simply reuse a standard subtying relation (suitably adapted), instead. Consequently, the implementation of our typing algorithm is amenable to a significant degree of automation, on par with other refinement type systems like Liquid Haskell [29].

Type and Effect Systems. Type and effect systems comprise a broad range of techniques that provide state guarantees about both what values a program computes and how it computes them. These systems have been developed for a number of different applications: static exception checking in Java [30], ensuring effects are safely handled in the languages with algebraic effects [31], and reasoning about memory accesses [32], in order to ensure, e.g., programs can be safely parallelized [33]. Notably, a majority of these systems are agnostic to the order in which these effects are produced: the effect system in Java, for example, only tracks whether or not a computation may raise an exception at run-time.

In contrast, sequential effect systems [34] provide finer grained information about the order in which a computation’s effects may occur. More closely related to this work are type and effect systems that target temporal properties on the sequences of effects a program may produce. For example, [35] present a type and effect system for reasoning about the shape of histories (i.e., finite traces) of events embedded in a program, with a focus on security-related properties expressed as regular expressions augmented with fixed points. Their specification language is not rich enough to capture data-dependent properties: the histories of a conditional expression must include the histories of both branches, even when its condition is a variable that is provably false. [36] present a type and effect system that additionally supports verification properties of infinite traces, specified as Büchi automata. Their system features refinement types and targets a language similar to . Their effect specifications also include a second component describing the sets of infinite traces a (non-terminating) program may produce, enabling it to reason about liveness properties. Unlike , however, events in their system are not allowed to refer to program variables. This restriction was later lifted by [12], whose results support value-dependent predicates in effect specifications written in a first-order fixpoint logic. To solve the resulting verification conditions, they introduce a novel proof system for this logic. More recently, [13] consider how to support richer control flow structures, e.g., delimited continuations, in such an effect system. To the best of our knowledge, all of these effect systems lack an analogue to the precondition automaton of HATs, and instead have to rely on the arguments of a dependently typed function to constrain its set of output traces, as opposed to constructing and managing the context of previously seen events and their results.

While our focus has been on the development of a practical type system for the purposes of verification, there have also been several works that provide foundational characterizations of sequential effect systems. Most of these works adopt a semantics-oriented approach and seek to develop categorical semantics for effectful languages [34], [37], [38]. More closely related is the recent work of Gordon [39], which defines a generic model of sequential effects systems in terms of a parameterized system. The key idea is to represent effects as a quantale, a join semi-lattice equipped with a top element and whose underlying set is also a monoid. The proposed type system is parameterized over an arbitrary effect quantale; this system is proven to be safe for any appropriate instantiation of this parameter.

Type-Based Protocol Enforcement. Because HATs express a history of the interaction between a client and an stateful library, they naturally serve as a form of protocol specification on client behavior , although the kinds of protocols we consider in this work are limited to those that are relevant to defining a representation invariant, i.e., those that capture constraints on library methods sufficient to ensure a desired client invariant. In this sense, HATs play a similar role as typestate in object-oriented languages [40]–[42], which augments the interface of objects with coarse-grained information about the state of an object, in order to constrain its set of available methods. Typestate specifications differ in obvious ways from HATs, most notably with respect to the level of granularity that is expressible; in particular, HATs are designed to capture fine-grained interactions between libraries and clients that are necessary to specify useful representation invariants.

8 Conclusion↩︎

This paper explores the integration of SFAs within a refinement type system as a means to specify and verify client-specific representation invariants of functional programs that interact with stateful libraries. Our key innovation is the manifestation of SFAs as HATs in the type system, which allows the specification of context traces (preconditions) as well as computation traces (postconditions) that allow us to characterize the space of allowed client/library interactions and thus enable us to prove that these interactions do not violate provided representation invariants. HATs integrate cleanly within a refinement type system, enjoy pleasant decidability properties, and are amenable to a high-degree of automation.

Another potential direction is extending our current formalization to support richer automata classes (e.g., symbolic visibly pushdown [43] or Büchi automata), in order to support a larger class of safety properties, .

9 Operational Semantics↩︎

The auxiliary big-step reduction rules for effect operators and the small-step operational semantics of our core language are shown in 10.

10 Basic Typing Rules↩︎

The basic typing rules of our core language and qualifiers are shown in 11 and 12. We use an auxiliary function \(\S{Ty}\) to provide a basic type for the primitives of our language, e.g., constants, built-in operators, and data constructors.

11 Declarative Typing Rules↩︎

The full set of rules for our auxiliary typing relations are shown in 13, and the full set of declarative typing rules are shown in 14. We elide the basic typing relation (\(\emptyset \basicvdash e : s\)) in the premises of the rules in 14; which assume all terms have a basic type.

12 Typing Algorithm↩︎

In this section, we provide the details of our typing algorithm. The full set of bi-directional typing rules for this algorithm are shown in 15; again, we again omit the basic typing relation (\(\emptyset \basicvdash e : s\)) in the precondition of these rules. The detail of alphabet transformation (\(\mintermReplace\)) and SFA instantiation (\(\instantiate\)) procedures are provided in [algo:alphabet] and [algo:instantiate], respectively.

12.0.0.1 Alphabet Transformation

The alphabet transformation function \(\mintermReplace\) translates a SFA into a FA that shares the same regular operators. Notably, the alphabet transformation for effect events gathers all minterms that can imply the qualifier of the effect event (line \(17\)); moreover, the effect event \(\evop{\effop}{\overline{x_i}}{\phi}\) requires the gathered minterms have the same operator (\(\effop\)).

12.0.0.2 Ghost Variable Instantiatation

As we show in [algo:instantiate], the abductive synthesizer adapts an existing algorithm [44] that synthesizes a maximal assignment of unknown qualifier \(\phi_i\) for the given ghost variables \(x_i{:}b_i\). These inferred qualifiers are strong enough to prove the given inclusion relation between two input automata under the given type context (i.e., \(\Gamma \vdash A \subseteq A'\)). Note that the ghost variables only make sense when the inclusion relation holds with all unknown formulae \(\phi_i\) are maximally weak (i.e., true) (line \(2\)). Similar to the minterm algorithm in [algo:alphabet], the abductive algorithm gathers all literals that appear in the pre- and post-condition automata and type context (line \(3\)) that will be used to generate candidate minterms (feature vectors, in the literature of abductive synthesis [44]), to build the hypothesis space for synthesis. The function uses a counterexample-guided refinement loop (line \(6\) - \(12\)) adapted from the existing algorithm [44] manipulating three sets of minterms: unknown minterms \(M^?\), positive minterms \(M^+\), and negative minterms \(M^-\). Thanks to the multi-abduction approach from the existing algorithm [44], inferring a formula \(\phi\) from the union of all minterms induces all the assignment of unknown qualifiers \(\overline{\phi_i}\) at one shot. The auxiliary synthesizer (line \(8\)) returns a formula that can be implied by given positive minterm and unknown minterms but cannot be implied by any given negative minterms. Following the existing algorithm [44], function is implemented as a Decision Tree (DT) that classifies these two sets of minterms. On the other hand, the inclusion query on line \(9\) decides if unknown minterms should be positive or negative; it also guarantees the soundness of the algorithm, that is, a synthesized type is always consistent with the given automaton \(A\) and \(A'\). Finally, the function returns refinement type \(\rawnuot{b_i}{\phi_i}\) for each ghost variable \(x_i\), where \(\phi_i\) is the union of all local minterms that can imply \(\phi\) (line \(14\) - \(15\)).

13 Proofs↩︎

13.0.0.1 Type Soundness

The Coq formalization of our core language, typing rules, and the proof of [theorem:fundamental] and Corollary 1 are available on Zenodo

https://doi.org/10.5281/zenodo.10806686

13.0.0.2 Soundness of Algorithmic Typing

We present the proof for [theorem:algo-sound] from 5. The proof requires the following lemmas about the \(\subqueryA\) subroutine and the instantiation function \(\instantiate\).

The soundness of establishes that it is safe to treat the subtyping relation in our typing algorithm as in declarative type system. On the other hand, the soundness of instantiation function induces the following lemma.

We need three auxiliary lemmas about declarative typing, which establish that we can drop unused binding from the type context, well-typed substitution preserves typing judgement, and well-formedness implies subtyping.

Now we can prove the soundness theorem of our typing algorithm with respect to our declarative type system. As the type synthesis rules are defined mutually recursively, we simultaneously prove both are correct. The following theorem states a stronger inductive invariant that is sufficient to prove the soundness of the typing algorithm.

13.0.0.3 Decidability of Algorithmic Typing

We present the proof for [theorem:algo-decidable] from 5. The proof requires the following lemmas about the \(\subqueryA\) subroutine and the instantiation function \(\instantiate\).

Now we can prove the decidability theorem of our typing algorithm. As the type synthesis rules are defined mutually recursively, we simultaneously prove both are decidable. The following theorem states a stronger inductive invariant that is sufficient to prove the decidability of the typing algorithm.

14 Evaluation Details↩︎

[tab:evaluation-long-1] and [tab:evaluation-long-2] list the information for individual ADT methods from [tab:evaluation]. All our benchmarks suite, and corresponding Coq proofs are available on Zenodo https://doi.org/10.5281/zenodo.10806686

References↩︎