Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Data stream processing frameworks like Flink [12], Kafka [21], Spark Streaming [34], and Timely Dataflow [26] are widely used in industry to compute with and analyze streams of data at a large scale. With a long-term objective of formally verifying the correctness of programs expressed in such frameworks in mind, we focus on their common algebraic dataflow foundation in this paper. The dataflow programming paradigm represents a streaming computation as a graph of operators, which are themselves data stream transformers.

We focus on asynchronous dataflow in which operators work autonomously without blocking the overall computation following the mantra “if I cannot make progress maybe someone else can.” Asynchronous computation is naturally nondeterministic: the order in which operators are invoked is not predetermined and might affect the overall computation’s behavior.

Bergstra et al. [3] provide an algebra of asynchronous dataflow operators and building blocks (including sequential and parallel composition and a feedback loop construct), axiomatize the properties of these operators, and give two instances satisfying the axioms. We develop a new instance in Isabelle/HOL using a shallow embedding as a coinductive datatype (short: codatatype). Our operators are essentially nondeterministic input-output machines with silent actions (Section 2). The coinductive representation allows us to keep the state implicit when composing operators. We use corecursion to define composition, feedback, and the various basic asynchronous operators of Bergstra et al. (Section 3). We use countable sets to represent nondeterminism, which simplifies our definition of composition and feedback operators.

We validate that our operators work as intended by proving all but one of Bergstra et al.’s axioms by coinduction (Section 4). Thereby, we use weak bisimilarity as the notion of operator equality. Some of our originally proved properties deviate mildly from Bergstra et al.’s axioms due to a simplification we made in some operators’ definitions and the fact that Isabelle does not have empty types. (Types are used by both us and Bergstra et al. to index the inputs and outputs of an operator. Bergstra et al.’s empty types signify that an operator has no inputs or no outputs). We show how to close this gap and obtain precisely Bergstra et al.’s axioms by working with the subtype of well-behaved operators (Section 5).

With the help of Isabelle’s code generator, we extract executable Haskell code from our formalization (Section 6). To this end, we represent countable sets as a quotient of lazy lists. This allows us to run operators, which is useful for testing. A particular challenge is the executability of the union of a countable set of countable sets as the corresponding merge function on lazy lists. We conclude with discussions of related work (Section 7) and particular formalization aspects (Section 8). Our formalization is publicly available [31].

Isabelle/HOL’s codatatypes [6] formalize potentially infinite objects such as infinite streams ($\mathrm{𝑠𝑡𝑟𝑒𝑎𝑚}$ type) and lazy lists ($\mathrm{𝑙𝑙𝑖𝑠𝑡}$ type). We introduce operators as:

This $\mathrm{𝐜𝐨𝐝𝐚𝐭𝐚𝐭𝐲𝐩𝐞}$ command introduces a new type constructor, $\mathrm{𝑜𝑝}$ (written postfix), with type parameters $\text{'}i$ indexing the input ports, $\text{'}o$ indexing the output ports, and $\text{'}d$ representing the type of data items (or events) an operator processes. An operator will perform one of four actions corresponding to the four codatatype constructors: (1) read an event from a given input port and continue based on the read event, (2) write an event to a given output port and continue as specified, (3) execute an internal (silent) action and continue as specified, and (4) nondeterministically choose a continuation from a countable set (type $\mathrm{𝑐𝑠𝑒𝑡}$) of options. Operators are possibly infinite trees with nodes labeled by one of these four actions with $\mathrm{𝖱𝖾𝖺𝖽}$ branching over the read event $\text{'}d$ and $\mathrm{𝖢𝗁𝗈𝗂𝖼𝖾}$ branching over the countable set of choices. For an operator to be finite, the operator must eventually reach the only leaf $\oslash \equiv \mathrm{𝖢𝗁𝗈𝗂𝖼𝖾}{\{\}}_c$ along all branches. Note that we use the subscript _c to distinguish sets and operations on them from their countable set counterparts: $\mathrm{𝑠𝑒𝑡}$ and $\mathrm{𝑐𝑠𝑒𝑡}$ are separate types in Isabelle.

The $\mathrm{𝐜𝐨𝐝𝐚𝐭𝐚𝐭𝐲𝐩𝐞}$ command also introduces the functions $\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}\mathit{::}(\text{'}i,\text{'}o,\text{'}d)\mathrm{𝑜𝑝}\Rightarrow \text{'}i\mathrm{𝑠𝑒𝑡}$ and $\mathrm{𝗈𝗎𝗍𝗉𝗎𝗍𝗌}\mathit{::}(\text{'}i,\text{'}o,\text{'}d)\mathrm{𝑜𝑝}\Rightarrow \text{'}o\mathrm{𝑠𝑒𝑡}$ that collect the sets of used ports as well as a map function on the ports $\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}\mathit{::}({\text{'}i}_{\mathit{1}}\Rightarrow {\text{'}i}_{\mathit{2}})\Rightarrow ({\text{'}o}_{\mathit{1}}\Rightarrow {\text{'}o}_{\mathit{2}})\Rightarrow ({\text{'}i}_{\mathit{1}},{\text{'}o}_{\mathit{1}},\text{'}d)\mathrm{𝑜𝑝}\Rightarrow ({\text{'}i}_{\mathit{2}},{\text{'}o}_{\mathit{2}},\text{'}d)\mathrm{𝑜𝑝}$. Note that an operator does not necessarily have to use all available ports. For example, an operator of type $(\mathrm{𝑛𝑎𝑡},\mathrm{𝑛𝑎𝑡},\mathrm{𝑛𝑎𝑡})\mathrm{𝑜𝑝}$ does not necessarily have an infinite number of input and output ports; rather, it uses some subset of naturally-numbered ports, given by $\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}$ and $\mathrm{𝗈𝗎𝗍𝗉𝗎𝗍𝗌}$.

Isabelle requires all functions to be total. For recursive functions on datatypes, totality means termination. In contrast, corecursive functions, which produce elements of a codatatype, are guaranteed to be total if they are productive – that is, they must always eventually produce a codatatype constructor. The $\mathrm{𝐜𝐨𝐫𝐞𝐜}$ command facilitates the definition of corecursive functions, in which a codatatype constructor guards all corecursive calls and all call contexts are comprised of friendly functions [5], thereby maintaining productivity and totality.

For example, we define two uncommunicative operators using $\mathrm{𝐜𝐨𝐫𝐞𝐜}$ in Figure 1. The operator $\odot$ corecurses forever with the $\mathrm{𝖲𝗂𝗅𝖾𝗇𝗍}$ constructor. The operator $\otimes$ corecurses forever with the (singleton) $\mathrm{𝖢𝗁𝗈𝗂𝖼𝖾}$ constructor as shown in the lemma $\text{spin\_op\_code}$. The actual $\mathrm{𝐜𝐨𝐫𝐞𝐜}$ definition is slightly more convoluted. The codatatype nests the corecursive occurrence of $\mathrm{𝑜𝑝}$, in the countable set type $\mathrm{𝑐𝑠𝑒𝑡}$, which means that any corecursive call guarded by the $\mathrm{𝖢𝗁𝗈𝗂𝖼𝖾}$ constructor must be applied using the map function on $\mathrm{𝑐𝑠𝑒𝑡}$, i.e., the image function ${\stackrel{`}{}}_c$ (written infix). To this end, we pull the corecursive call out of the singleton set. We also use similar transformations in some subsequent operators. To improve readability, we only present the user-friendly derived equations, such as $\mathrm{𝗌𝗉𝗂𝗇}\mathrm{\_}\mathrm{𝗈𝗉}\mathrm{\_}\mathrm{𝖼𝗈𝖽𝖾}$, rather than the original $\mathrm{𝐜𝐨𝐫𝐞𝐜}$ command.

This section explains the set of operators of the network algebra for asynchronous dataflow. Following Bergstra et al. [3], they are divided into two categories. First, basic network algebra consists of three operators for structuring the network – sequential composition, parallel composition, and feedback – along with the identity and transposition constants. The second category includes additional asynchronous dataflow constants such as split, sink, merge, dummy source, asynchronous copy, and asynchronous equality test. Except for the sink, all operators are stateful, maintaining internal buffers to store communication data. These buffers function as intermediate first-in-first-out communication channels where data can reside indefinitely.

We show that the axioms from Tables 1, 2, and 3 presented in Bergstra et al. [3] with the exception of axiom $\text{A1}$ in their Table 3 are valid in our shallow embedding. We discuss insights from proving the axioms and explain formulation differences. To make referencing transparent, we will use the axiom numbering of Bergstra et al.’s, but we merge their Tables 2 and 3 (which use the same axiom numbers) into a single table.

First, we establish a notation for sequentially composing an operator with identity: $\mathrm{𝑜𝑝}⊢$ denotes $\mathrm{𝑜𝑝}\bullet ℐ$ and $⊣\mathrm{𝑜𝑝}$ is $ℐ\bullet \mathrm{𝑜𝑝}$. This pre-/post-composition is added in our formalization to certain lemmas to ensure that the operator exhibits the required asynchronous behavior. This allows for a more precise account on where these additions are needed. For instance, the process algebra model from Bergstra et al. [3] surrounds most operators by identities on both sides. Changes to axiom statements of this nature are highlighted in gray. In Section 5, we demonstrate how these differences can be eliminated through the introduction of a new type.

The first set of axioms is shown in Table 1. First, we identify some notable axioms. Axiom $\text{B1}$ is the associativity of parallel composition and axiom $\text{B3}$ is the associativity of sequential composition. Notice that for $\text{B1}$ we need to map ports with the $\curvearrowright \mathit{::}(\text{'}a+\text{'}b)+\text{'}c\Rightarrow \text{'}a+\text{'}b+\text{'}c$ function so the sum types are properly reassociated. We also define its inverse function $\curvearrowleft$. Bergstra et al. mostly ignore such port mismatches; in a proof assistant more rigor is needed. Both parts of $\text{B4}$ show that an operator sequentially composed with identity can absorb another identity. This follows directly from the $ℐ\bullet ℐ\approx ℐ$ auxiliary lemma. We call such lemmas that remove identities identity absorption.

The feedback operator axioms require additional assumptions to guarantee that arbitrary operators do not use default ports when looping-back (on the right). These assumptions use the inverse image function $f\text{-}\stackrel{`}{}B\equiv \{x.fx\in B\}$ to capture the right inputs and outputs. Recall that the wiring of $\uparrow$ forces $\mathrm{𝑑𝑒𝑓𝑎𝑢𝑙𝑡𝑠}$ ports on the right to not loop back. Without these assumptions, the invariant that the ports on the right are the looping-back ones would be violated. Again, these modifications are highlighted and will be abstracted away in Section 5.

Table 2 is about the asynchronous equality test, merge, copy, split, the dummy source, and sink operators. Axioms $\text{A14}$, $\text{A15}$, $\text{A18}$, and $\text{A19}$ can be seen as a recursive characterization of equality test, merge, copy, and split. The merge and split operators satisfy fewer axioms than equality test and copy. For example, $\text{A11}$ first duplicates inputs and then performs an equality test on them on the subsequent operator, which is bisimilar to the identity operator. For the $𝒱$ and $\mathrm{\Lambda }$, the axiom $\text{A11}$ is not valid because nondeterministic split choices do not necessarily align with the nondeterministic merge order. A related reason prevented us from proving $\text{A1}$ for $𝒱$. In fact, we proved that $(𝒱\parallel ℐ)\bullet 𝒱⊢$ and $\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}\curvearrowleft \mathrm{𝗂𝖽}((ℐ\parallel 𝒱)\bullet 𝒱⊢)$ are not weakly bisimilar as they make partial nondeterministic choices in different orders. We explain this in more detail at the end of the section. We do believe that these operators are trace equivalent, but do not have a formal proof of this statement.

To prove the axioms, we follow the approach outlined in Section 2.1. This involves deriving introduction and elimination rules, such as the ones in Figure 3, for each operator and using these rules to construct the required simulations generated by the coinduction. The coinduction proofs require generalizing the operator’s buffers, as using empty buffers from the notations would eventually cause us to be outside of the bisimulation during the coinduction. Consequently, we must consider arbitrary buffers and establish an invariant between them. In most cases, this is straightforward. For example, in the generalization of axiom $\text{B7}$ in Figure 10, the buffers from both sides are related using the $\gg$ function. In this figure, the left-side ports are of the numeral type $\mathit{3}$, and the right-side ports are of type $\mathit{1}$. Also, we re-use the same symbols as the introduced operator notations to unambiguously identify them.

A common pattern in the proofs involves forward reasoning to move data through the buffers. For instance, consider one of the cases in the $\text{B7}$ proof, where $ℐ$ on the right-hand side of the weak bisimilarity produces an output from the $l$ buffer. Then the left-hand side must also produce the same output. However, it may be the case that the buffers $l_2$ and $l_3$ are empty, and the head of $l_1$ must traverse the diagram to generate the output. This results in a sequence of $\mathrm{𝖳𝖺𝗎}$ steps that move $l_1$’s head to $l_2$ and then to $l_3$. The Isar proof language [32] offers fact chaining using $\mathrm{𝐚𝐥𝐬𝐨}$, which is well-suited for this kind of transitive reasoning.

The axiom $\text{A10}$ was a challenging one to prove as it required a non-trivial buffer invariant. We consider the diagram in Figure 11, and we assume that $a=a_{\mathit{1}}\gg a_{\mathit{2}}\gg a_{\mathit{3}}\gg a_{\mathit{4}}\gg a_{\mathit{5}}$, and similarly for $b$, $c$, and $d$. Furthermore, we assume $\mathrm{𝑎𝑐}={\mathrm{𝑎𝑐}}_{\mathit{1}}\gg a{c}_2$ and $\mathrm{𝑏𝑑}={\mathrm{𝑏𝑑}}_{\mathit{1}}\gg b{d}_2$. To find the invariant, we analyze the left-to-right simulation first. Assume that the left-hand side does an equality test step with ${𝒬}_0$. This step can only be weakly simulated on the right-hand side if either or both ${𝒬}_1$ and ${𝒬}_2$ can make some sequences of tests to catch up with ${𝒬}_0$. However, there is no way to have a simulation if either ${𝒬}_1$ or ${𝒬}_2$ has tested more than ${𝒬}_0$. The sequence of channels $ap$ and $cp$ must have the same length as they are consumed together by ${𝒬}_1$, and symmetrically $bp$ and $dp$. Thus, for every port $p$, there exist natural numbers $n,m$, such that $\mathrm{𝖽𝗋𝗈𝗉}n(ap)=xp\wedge \mathrm{𝖽𝗋𝗈𝗉}n(cp)=yp\wedge \mathrm{𝖽𝗋𝗈𝗉}m(bp)=xp\wedge \mathrm{𝖽𝗋𝗈𝗉}m(dp)=yp$. As ${𝒬}_1$ and ${𝒬}_2$ advance independently, we maintain $n=0\vee m=0$ as invariant. The already tested elements in $z\gg v$ and in $z\gg w$ can be ahead of the tested elements on the right-hand side of the equivalence ($\mathrm{𝑎𝑐}$ and $\mathrm{𝑏𝑑}$). This means that $(z\gg v)p$ is precisely the same as $\mathrm{𝑎𝑐}p$ followed by the sequence of $n$ elements still to be pairwise tested in $ap$ and $cp$.

The established invariant must also hold for the right-to-left simulation. We assume an equality test on the right-hand side in ${𝒬}_2$ testing if $\mathrm{𝖡𝖧𝖣}p{b}_{\mathit{5}}$ equals $\mathrm{𝖡𝖧𝖣}p{d}_{\mathit{5}}$. We must avoid testing too little on the left-hand side of the equivalence to keep the invariant. For example, if $b=x$ and $d=y$, this new equality test with $b_{\mathit{5}}$ and $d_{\mathit{5}}$ will reduce the size of $b$ and $d$ by one; therefore, one equality test on the left-hand side must happen as well.

The axiom $\text{A1}$ for the merge operator is $(𝒱\parallel ℐ)\bullet 𝒱⊢\approx \mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}\curvearrowleft \mathrm{𝗂𝖽}((ℐ\parallel 𝒱)\bullet 𝒱⊢)$. Intuitively, equating the two sides means that it does not matter in which order the data from the three input ports are merged: all interleavings should be allowed by either operator. However, using weak bisimilarity, this axiom turns out to be invalid. Note we include here the post-composition with identities after the last merge operator, so we can later lift the result to the type defined in Section 5. Assuming that the operators are weakly bisimilar, then for every weak step that one operator makes, there must exist a weak step that the other operator makes such that they remain equivalent. We now sketch how we derive a contradiction from this. Consider that $({𝒱}_0\parallel {ℐ}_0)\bullet {𝒱}_1⊢$ (where we annotate operators with indices to distinguish different instances of the same operator) reads a value $x$ on port 1, the top input port in Figure 12, and $x$ is moved beyond ${𝒱}_0$ but before ${𝒱}_1$ (into the buffer of sequential composition). Then we consider all possible weak steps $\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}\curvearrowleft \mathrm{𝗂𝖽}(({ℐ}_2\parallel {𝒱}_2)\bullet {𝒱}_3⊢)$ can make by reading value $x$ on port 1. On a high level, there are two separate cases. First, assume $x$ is read and then may be moved along the buffers but only before ${𝒱}_3$ actually performs the merge. Then this operator can read any value $y\ne x$ on port 2 (the middle input port in Figure 12) and output it before $x$. However, this cannot be replicated by the left-hand side because $x$ has already moved beyond ${𝒱}_0$, so $y$ would be enqueued after $x$ and cannot be output before $x$. The second case is that $x$ is read and then moved along the buffers beyond ${𝒱}_3$. Then the left-hand side can read any value $z\ne x$ on port 3 (the bottom input port in Figure 12) and output it before $x$. However, this cannot be replicated by the right-hand side because $x$ has already moved beyond ${𝒱}_3$, so $z$ cannot be output before $x$.

The main challenge we experienced in disproving weak bisimilarity is dealing with weak steps in the assumptions. Weak steps are significantly more difficult to reason about than single steps, because we do not have simple elimination rules for them, as any number of silent steps may occur before and after the visible action. We can use induction on these sequences of silent steps, but it is generally difficult to use the induction hypotheses because they typically require making buffers arbitrary, which was not practical for disproving $\text{A1}$. Our workaround was to explicitly obtain all possible states of the operators after a weak step, which was manageable here because we know exactly what the operators are and we start from empty buffers.

We outline the process for eliminating the differences in our lemmas compared to Bergstra et al. [3]: the gray highlights in Table 1 and Table 2. To achieve this, we define a subtype of well-behaved operators using Isabelle’s $\mathrm{𝐭𝐲𝐩𝐞𝐝𝐞𝐟}$ command. The new type requires its elements to be weakly bisimilar to some operator surrounded by $⊣$ and $⊢$.

Next, we lift every definition to this new type. This includes all operators, weak bisimilarity, and $\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}$. The lifting is done by the $\mathrm{𝐥𝐢𝐟𝐭}\mathrm{\_}\mathrm{𝐝𝐞𝐟𝐢𝐧𝐢𝐭𝐢𝐨𝐧}$ command [18], which requires a proof that the lifted term respects the subtype’s property. When an operator has identity absorption lemmas, it can be lifted without changes; for example, $ℐ$ can be lifted directly as it satisfies $ℐ\bullet ℐ\approx ℐ$. Similarly, $\bullet$, $\parallel$, and$\uparrow$ are lifted directly too; they satisfy $⊣(o{p}_1\bullet o{p}_2)⊢\approx (⊣o{p}_1)\bullet (o{p}_2⊢)$, $⊣(o{p}_1\parallel o{p}_2)⊢\approx (⊣o{p}_1⊢)\parallel (⊣o{p}_2⊢)$, and $⊣(op\uparrow )⊢\approx (⊣op⊢)\uparrow$.

Other operators such as $𝒞$ are lifted with no changes as well because they also have identity absorption lemmas for both sides: $⊣𝒞⊢\approx 𝒞$. We lift the definitions of ! and $!$ using the $\mathrm{𝖺𝗅𝗅}\mathrm{\_}\mathrm{𝖽𝖾𝖿𝖺𝗎𝗅𝗍𝗌}$ type class constraint to ensure that they have no usable ports for their inputs and output, respectively. This guarantees their identity absorption lemmas. In contrast, the operators $𝒬$ and $𝒱$ satisfy only weaker one-sided absorption lemmas: $⊣𝒬⊢\approx 𝒬⊢$, $⊣𝒱⊢\approx 𝒱⊢$. Hence, to make the subtype constraint hold, we lift $⊣𝒬$ and $⊣𝒱$ instead of $𝒬$ and $𝒱$.

The lifting of $\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}$ requires $⊣(\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}fg\mathrm{𝑜𝑝})⊢\approx \mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}fg(⊣\mathrm{𝑜𝑝}⊢)$ to hold. This is not true in general, but we can impose sufficient constraints on $f$ and $g$. They must maintain the exclusive use of ports in the set ${𝔘}_c$ (i.e., $\forall x.fx\in \mathrm{𝖽𝖾𝖿𝖺𝗎𝗅𝗍𝗌}⟶x\in \mathrm{𝖽𝖾𝖿𝖺𝗎𝗅𝗍𝗌}$). The same property must also hold for the inverse of $f$ and $g$ because in the bisimilarity proof their inverses are necessary to construct the respective simulation. In addition, this lemma further requires that $f$ and $g$ and their inverses are injective on ${𝔘}_c$. Fortunately, all usages of $\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗈𝗉}$ in all tables meet these conditions. Lastly, the highlighted assumptions from Table 1 are also eliminated for the lifted operators because they are weakly bisimilar to $⊣{\mathrm{𝑜𝑝}}^{\prime }⊢$ for some ${\mathrm{𝑜𝑝}}^{\prime }$, the ports of $⊣{\mathrm{𝑜𝑝}}^{\prime }⊢=ℐ\bullet {\mathrm{𝑜𝑝}}^{\prime }\bullet ℐ$ are in ${𝔘}_c$, and weakly bisimilar operators have the same ports.

Our operators are infinitary in two respects: they may branch over a countably infinite set of choices and as codatatypes, they may be trees of infinite depth. We use code generation to Haskell [17] to execute operators lazily and produce prefixes of their traces up to a given depth.

A particular challenge for code generation is our usage of the abstract type of countable sets, which are originally defined as a subtype of arbitrary sets. The default code generation setup for sets supports finite and cofinite sets, but not the countable sets we are interested in. Instead, we provide a new setup for countable sets that recasts them as quotients [20] of the lazy list type modulo reordering of elements. For this purpose, we define the abstraction function $\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗈𝖿}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathit{::}\text{'}a\mathrm{𝑙𝑙𝑖𝑠𝑡}\Rightarrow \text{'}a\mathrm{𝑐𝑠𝑒𝑡}$ which is used by the code generator as the only pseudo-constructor of countable sets: a standard way to provide code generation for quotients [16]. Then, operations on countable sets can be made executable by providing a code equation that pattern-matches on this pseudo-constructor and performs the according operation on the underlying lazy lists. For example, countable set union becomes lazy list interleaving:

Things become more challenging for functions on countable sets of more complex types, e.g., countable sets themselves. Specifically, the above recipe fails for the function ${\mathrm{\bigcup }}_c\mathit{::}(\text{'}a\mathrm{𝑐𝑠𝑒𝑡})\mathrm{𝑐𝑠𝑒𝑡}\Rightarrow \text{'}a\mathrm{𝑐𝑠𝑒𝑡}$. It is not a problem to define a corresponding function on lazy lists:

This definition crucially relies on Isabelle’s corecursion up-to friends [5], in particular that $\mathrm{𝗅𝗂𝗇𝗍𝖾𝗋𝗅𝖾𝖺𝗏𝖾}$ is a friendly function (which is proved automatically for its definition). However, the following equation uses the map function on lazy lists on the left and is thus invalid code:

A dual problem occurs for functions on subtypes with compound return types. Kunčar [22, §6.4] presents and automates a solution for subtypes, which inspires our solution for quotients. We introduce a type $\text{'}a\mathrm{𝑐𝑠𝑒𝑡}\mathrm{\_}\mathrm{𝑙𝑙𝑖𝑠𝑡}$ that is isomorphic to $(\text{'}a\mathrm{𝑐𝑠𝑒𝑡})\mathrm{𝑙𝑙𝑖𝑠𝑡}$ as a quotient of $(\text{'}a\mathrm{𝑙𝑙𝑖𝑠𝑡})\mathrm{𝑙𝑙𝑖𝑠𝑡}$ (with the abstraction function $\mathrm{𝖺𝖻𝗌}\mathrm{\_}\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathit{::}(\text{'}a\mathrm{𝑙𝑙𝑖𝑠𝑡})\mathrm{𝑙𝑙𝑖𝑠𝑡}\Rightarrow \text{'}a\mathrm{𝑐𝑠𝑒𝑡}\mathrm{\_}\mathrm{𝑙𝑙𝑖𝑠𝑡}$ serving as the pseudo-constructor for code generation). Since this new type does not have a compound domain, the standard lifting of $\mathrm{𝗅𝗆𝖾𝗋𝗀𝖾}$ to the function $\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathrm{\_}\mathrm{𝗆𝖾𝗋𝗀𝖾}\mathit{::}\text{'}a\mathrm{𝑐𝑠𝑒𝑡}\mathrm{\_}\mathrm{𝑙𝑙𝑖𝑠𝑡}\Rightarrow \text{'}a\mathrm{𝑐𝑠𝑒𝑡}$ yields a valid code equation. Thus we have reduced the problem to finding an executable function $\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathrm{\_}\mathrm{𝗈𝖿}\mathit{::}(\text{'}a\mathrm{𝑐𝑠𝑒𝑡})\mathrm{𝑙𝑙𝑖𝑠𝑡}\Rightarrow \text{'}a\mathrm{𝑐𝑠𝑒𝑡}\mathrm{\_}\mathrm{𝑙𝑙𝑖𝑠𝑡}$. This function can be defined by lifting the identity on lazy lists. And it can be made executable by lifting the lazy list constructors to $\text{'}a\mathrm{𝑐𝑠𝑒𝑡}\mathrm{\_}\mathrm{𝑙𝑙𝑖𝑠𝑡}$ and using the following code equations:

Overall, we obtain ${\bigcup }_c(\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗈𝖿}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathrm{𝑥𝑠𝑠})=\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathrm{\_}\mathrm{𝗆𝖾𝗋𝗀𝖾}(\mathrm{𝖼𝗌𝖾𝗍}\mathrm{\_}\mathrm{𝗅𝗅𝗂𝗌𝗍}\mathrm{\_}\mathrm{𝗈𝖿}\mathrm{𝑥𝑠𝑠})$, which is executable. We remark that we cannot use Lochbihler and Stoop’s framework [24] for executing generated Isabelle code lazily in strict programming languages, because quotient types are not supported by that framework. Thus, we resort to Haskell as the code generation target.

This work provides mechanized proofs of most asynchronous dataflow algebra axioms by Bergstra et al [3]. They present the two original algebra instances: the relation-based stream transformer model and the process algebra model using the Algebra of Communicating Processes (ACP) [2]. Our operator definitions closely follow their ACP counterparts. One difference is that most of their operators are defined by explicitly pre- and post-composing with identity operators ($⊣\mathrm{𝑜𝑝}⊢$ instead of $\mathrm{𝑜𝑝}$), whereas we work with the core operators and only use the additional identities where they are necessary. For the stream transformer model, Broy and Ştefănescu [9] provide pen-and-paper proofs for a slightly different algebra.

The recent Isabelle/HOL formalization of time-aware stream processing [30] bears some similarities to our work. It defines stream processing operators using a codatatype with a single constructor that combines both reading and writing: a finite list of outputs is produced as a reaction to reading an input. In contrast, we separate both operations (so that the operator can decide what it wants to do next) and additionally support nondeterministic choices and silent steps. Their approach covers time metadata associated with processed events (which is necessary for aggregating computations) but does not support loops. We plan to extend our network algebra operators with capabilities to observe time metadata.

Chappe et al. [14] formalize choice trees – a semantic domain for modeling nondeterministic, recursive, and impure programs, based on interaction trees developed by Xia et al [33] in Rocq. (Later, interaction trees have also been formalized in Isabelle [15].) Our operators can be seen as a domain specific variant of choice trees tailored to asynchronous dataflow. In particular, our types make inputs and output ports explicit, which is used in composition and feedback operators. In contrast, choice trees are monadically composed along their only output. Due to Isabelle’s simple types, our operators are restricted to use a fixed type parameter for the data items. In a dependently-typed system, the type of data could be indexed by the corresponding port, much like the interaction type depends on the action type in choice/interaction trees.

Beyond the world of mechanization, the streaming language Flo [23] has been recently proposed as a formal representation of streaming computations originating from systems like Flink [12] and DBSP [11]. Flo makes two assumptions on these systems: streaming progress and eager execution. The first assumption means that a program produces as much output as it can given the observed inputs; the second ensures that this output is deterministic. One practical challenge in Flo is the need to demonstrate that operators satisfy both assumptions.

Synchronous dataflow languages have received some attention in mechanization, with the Lustre [13] compiler Vélus [7] being a prominent example. Bergstra et al. [4] also develop algebraic foundations for synchronous dataflow, which subtly differ from the asynchronous ones.

Milner’s classic chapter on weak bisimilarity [25] provided us with valuable insights for our proofs. The network algebra axioms were well-behaved in a sense that we did not have to use advanced up-to techniques for weak bisimilarity, such as the ones developed by Pous [28, 29].

We have presented our Isabelle formalization of a semantic domain for asynchronous dataflow along with operators that satisfy all but one of Bergstra et al.’s axioms [3]. Our formalization comprises 28 000 lines of definitions and proofs. A major bulk of this work are the coinduction proofs of the 51 axioms, each spanning between 12 and almost 4 000 lines.

In terms of proof assistant technology, we make use of Isabelle’s support for codatatypes, in particular using nested corecursion through the type of countable sets. While we could define all our desired operators, some definitions needed adjustments from their most natural (presented) formulations to be accepted by $\mathrm{𝐜𝐨𝐫𝐞𝐜}$. Our formalization may give insight to developers on how to make this advanced command even more convenient to use.

Although not visible in the resulting formalization, we made great use of the Sketch and Explore tool when proving the axioms. Typically, we would invoke $\mathrm{𝑎𝑢𝑡𝑜}$ and obtain a number of subgoals to work on. (In case of $\text{A10}$ there are more than fifty subgoals.) The Sketch and Explore tool presents these subgoals as an Isar proof outline, so that once finished the $\mathrm{𝑎𝑢𝑡𝑜}$ invocation can become a terminal proof method, which is deemed better proof style.

Our formalization provides reusable artifacts beyond dataflow. In particular, we have outlined an approach for emulating empty types through the use of the $\mathrm{𝑑𝑒𝑓𝑎𝑢𝑙𝑡𝑠}$ type class. We have also sketched how to generate executable code for functions on quotient types with compound domain types. Although we were mostly interested in countable sets, we presented a general technique dualizing the existing solution for a similar problem with subtypes.

An anecdote from our formalization journey is illustrative. After having completed all axiom proofs, we have noticed that we actually proved the $\mathrm{\Lambda }$ version of A5, which according to Bergstra et al. is not expected to hold in all models. This made us suspicious and we were inspecting the axioms extra carefully. The proof assistant did not help here: Isabelle had happily accepted our proofs. It turned out that we made a mistake in statements: instead of reassociating sum types we were rotating them, which has trivialized several axioms. We rushed to fix the mistake and proved all axioms but $\text{A1}$ for $𝒬$ and $𝒱$. After some (useful) struggle with Isabelle, we realized that our definition of $𝒬$ deviated from Bergstra et al.’s: instead of replacing non-equal pairs by $\mathrm{𝖭𝗈𝗇𝖾}$ we were dropping such pairs entirely. Fixing $𝒬$ meant that we had to revisit all our proofs involving it, including $\text{A10}$. Here, Isabelle turned out to be tremendously helpful: the proof structure did not change and local fixes (in places Isabelle pointed to) were sufficient to bring us back on track. We finally also managed to prove $\text{A1}$ for $𝒬$ (but not for $𝒱$).

We are working on proving $\text{A1}$ for $𝒱$ using trace equivalence. As future work, we will formalize the history model (i.e., give operators a semantics in terms of input/output relations on lazy lists) and demonstrate that it suffers from the Brock–Ackermann anomaly [8, 19]. We have already formalized the trace semantics, which constitutes Jonsson’s workaround for this issue [19]. However, a characterization of traces for composition and feedback in terms of their arguments’ traces is missing. As a long term objective, we want to make time a first-class citizen in our dataflows, so that we can formalize programs expressed in data stream processing frameworks such as Timely Dataflow [26]. Our work provides a solid foundation for asynchronous dataflow into which we will incorporate promising initial progress in that direction [30, 10].