# Deductively Verifying Functional Scalable Parallel Programs with Why3

Frédéric Loulergue, Olivia Proust

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

## To cite this version:

Frédéric Loulergue, Olivia Proust. Deductively Verifying Functional Scalable Parallel Programs with Why3. Software and Systems Modeling, inPress, pp.1-37. hal-05342070

HAL Id: hal-05342070

https://hal.science/hal-05342070v1

Submitted on 20 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
PREPRINT

Deductively Verifying
Functional Scalable Parallel Programs
with WHY3

Frédéric Loulergue

Olivia Proust

Université d'Orléans, INSA CVL, LIFO UR 4022, Orléans, France

Abstract

Bulk Synchronous Parallelism (BSP) is a simple, yet realistic, model of scalable parallel computing. BSML is a pure functional library for the multi-paradigm language OCaml that embodies the principles of BSP. We propose a formalization of BSML primitives with WhyML, the specification language of WHY3 and specify and prove the correctness of set of parallel functions forming a standard library. We develop and verify the correctness of small BSML applications based on transformation theorems and the correspondence of a set of sequential functions on lists with algorithmic skeletons, i.e. functions implemented in parallel and manipulating distributed lists. Leveraging the WHY3 feature generating OCaml code from WhyML code, we experiment these applications on parallel machines.

**Keywords:** software engineering, formal methods, scalable parallel computing, functional programming, deductive verification, Why3

# 1 Introduction

Big data analytics requires scalable parallel processing in order to deliver analyses in a reasonable amount of time. Rather than writing programs in languages and libraries commonly used in high-performance computing — in particular MPI [52] a de facto standard for distributed memory parallel programming — more high-level frameworks have been developed such as Google MapReduce [14], Hadoop MapReduce [55] and Apache Spark [1]. All these frameworks offer patterns of parallel algorithms which are especially suited to the analysis of large volumes of data. This ease of use comes at the price of a lesser applicability: MPI can express a larger variety of parallel algorithms than these more recent approaches.

High-level big data analytics approaches are often inspired by bulk synchronous parallelism (BSP) [54], a model of scalable parallel computing, or by algorithmic skeletons [11, 27] and functional programming. In this context, scalable means that the number of processors of the parallel machines running BSP programs could range from a few to several dozens of thousand cores or more. BSP is more expressive than algorithmic skeletons, MapReduce and Spark, but more restrictive and simpler than MPI. Its cost model allows programmer to reason about the performances of their programs.

Bulk Synchronous Parallel ML (BSML) [39] is a pure functional library for the multi-paradigm language OCaml<fnref n="1" />. BSML is pure in the sense that mixing a pure functional sequential language with BSML primitives gives a pure functional language: this is not always the case

<footnote n="1">¹https://ocaml.org</footnote>
for parallel extensions of functional languages, for e.g. CamlFlight [20]. BSML embodies the principles of the BSP model, at a higher level than libraries such as the BSPlib library [30] and can easily express algorithmic skeletons [24, 35] which provide parallel algorithmic patterns similar to those provided by frameworks such as MapReduce or Spark. One important property of BSML is that it offers deterministic parallelism [26] and there exists a formalization of BSML as a confluent λ-calculus [38].

WHY3 [5, 6] is a framework for the deductive verification of programs. It provides a specification and programming language named WhyML which can be used directly or as an intermediate language for other tools to verify C [32], Java[18], Ada [43] or Rust [15] programs. WHY3 generates verification conditions to be verified by external provers. One of the strength of WHY3 is that it targets a large variety of provers including Alt-Ergo [12], Z3 [44], CVC4 [3] and CVC5 [2]. OCaml code can be extracted from WhyML. Assuming verification conditions have been proved and trusting WHY3 logic and transformations, the external provers and WHY3 extraction mechanism, the obtained OCaml code is correct with respect to the associated contracts in the source WhyML code. When a verification condition is proved by different provers, the trust one can have that it is indeed true increases. While to our knowledge there is no work on the verification of the code extraction mechanism of WHY3, there is a formalization of a subset of WHY3 [10] in the Rocq prover (formerly known as the Coq proof assistant).

BSML is composed of a small set of primitives which are implemented in parallel on top of MPI and of a standard library of useful parallel functions implemented using only these primitives and the sequential subset of the host language OCaml. The core primitives of BSML cannot be implemented using the sequential language WhyML but as their semantics is deterministic they can be *axiomatized*. The standard library can be implemented using WhyML and the axiomatized BSML primitives, and verified with respect to contracts written in WhyML. Using both the primitives and the standard library, it is then possible to implement high-level MapReduce-like algorithmic skeletons libraries and apply them to example applications. BSML primitives in WhyML cannot be extracted as they are axiomatized. To be able to run extracted BSML code from WhyML, we need to link the extracted code with an unverified parallel implementation of BSML primitives. This implementation is therefore an additional element to the trusted computing base. Note that it is possible to write a *sequential* realization in WhyML of the BSML primitive axiomatization. Extracting this realization provides a verified sequential implementation of BSML primitives than could be used to test the unverified parallel implementation of these primitives.

Our contributions are the formalization of BSML and its standard library in WhyML and its use in the specification and verification of several scalable parallel functions: for computing the average of a list of numbers, the number of values in a list of values satisfying a predicate, and the maximum prefix sum problem. All these parallel programs are proved correct with respect to a sequential specification and implemented using map and reduce algorithmic skeletons.

This work extends and revises a conference article published in the proceedings of SEFM 2023 [49]. Additional material that did not appear in the conference version include: (1) a realization of BSML axiomatization; (2) additional applications; (3) code extraction and experiments on parallel machines; (4) additional explanations.

The remaining of the paper is organized as follows. In Section 2, we give an overview of WHY3 and WhyML, including its limitations when dealing with higher-order functions. We introduce functional bulk synchronous parallel programming with BSML in Section 3. Section 4 is devoted to the formalization of the primitives of BSML and Section 5 shows to the specification and verification of (a sub-set of) the BSML standard library. We consider the specification, development and verification of several small applications (Section 7) based on the first homomorphism theorem and related algorithmic skeletons (Section 6). We use the code extraction feature of WHY3 to obtain OCaml code that is compiled using the BSML implementation on top of MPI, and we report results of experiments on parallel machines in Section 8. Section 9 discusses related work, and we conclude in Section 10.

The set of WHY3 modules is called WhyBSML [37]. The version corresponding to this paper
<figure><img src="image_3.png" /><figcaption>Figure 1: A WhyML Example</figcaption></figure>

is version 0.2.

## 2 An Overview of Why3

We begin with a short introduction to Why3 (Section 2.1) and discuss one limitation we faced and a workaround (Section 2.2).

### 2.1 Specifying and verifying functional programs with Why3

Why3 is often used in the verification of imperative programs. As BSML is purely functional and BSML applications mostly rely on the functional features of OCaml, we focus here on the verification of functional programs. This focus is also a necessity as we will explain in the next subsection.

In addition to its core features, Why3 provides a standard library with data structures such as lists and arrays, as well as basic arithmetic logic with integers and reals. We illustrate this
short introduction with the example of Figure 1. The function `max` is actually already defined in the standard library, in a way that uses more WhyML concepts than the version given here. Note that this figure presents a pretty-printed version of the actual code, `\` is rendered as `∧`, `\/` as `∨`, `->` as `→`, `forall` as `∀`, `exists` as `∃`, `<=` as `≤`, `>=` as `≥` and type variables as greek letters for example, `'a` as `α`.

WhyML developments are organized in *modules*. The example defines two modules: `Max` (lines 1–8) and `MaxList` (lines 10-32). Defined modules can be used in other modules with the `use` keyword. We use some modules of WHY3 standard library: `int.Int` about integer arithmetic (lines 2 and 11) and `list.List`, `list.Length`, `list.NthNoOpt` for basic definitions and facts about lists (lines 12–14).

The module `Max` is devoted to the specification and definition of a function `max` which returns the largest of two integers. This function does not have any pre-condition but its post-conditions are introduced by the keyword `ensures`.

Assuming the file `maximum.mlw` contains only the module `Max`, verifying that `max` satisfies its preconditions using the prover Alt-Ergo can be done with the following command:

```
why3 prove --prover Alt-Ergo,2.6.0 maximum.mlw
```

and the tool answers `max` indeed satisfies its contract:

```
File maximum.mlw:
```

```
Goal max'vc.
```

```
Prover result is: Valid (0.00s, 9 steps).
```

The number of steps is an information returned by the external solver. Alt-Ergo is an SMT solver mixing SAT solving and decision procedures for specific theories. Each step is a call to a decision procedure. In the remaining of the section, we use only this external prover.

In our study, most of the functions to verify are recursive and often manipulate lists. Lines 19–31 are an example of a recursive function that takes a list of integers and returns the highest value the list contains.

To write the contract of function `maximum`, we use the notation `xs[i]` to access the `i`th element of list `xs`. This notation is defined as a binary function in line 17 and is actually an alias for the `nth` function of the standard library. Note that this definition is introduced by the keyword `function` instead of the keyword `let` (as in line 4). The purpose of (`[]`) is to be used only in specifications while `max` is code that is meant to be executed.

In this example, `max` cannot be used in assertions while the bracket notation cannot be used in programs. Pure functions may be used in both roles if they are defined using both keywords. In Figure 10, lines 6-9 define two pure functions `op` and `f` that are both used in lemmas to prove some of their properties but also as arguments of higher-order program functions. Note that in the code presented in the remaining of the paper, functions used in both roles are without contracts.

The function `nth` is axiomatized: it is only defined when the position is valid. If the position is not valid there is no axiom at all. This avoids having a `nth` function returning an optional value as discussed in the next section. As we use `nth` in specifications only and only with valid positions, there is no need for a function retuning an optional value.

For `maximum`, we have a larger contract with new clause types. We add a pre-condition (following the keyword `requires`) to this contract, due to the fact that our function is not defined on empty lists. To ensure termination, we define a `variant`, which must be decreasing with each recursive call. The recursive call in line 30 is indeed called on the tail of the input list, thus this call is made on strictly smaller argument than `xs`.

We need quantifiers to express our post-conditions. The maximum value must be contained in the list (line 22 using `∃`), and must be greater than or equal to all the values in the list (line 21 using `∀`).

The definition of the function follows in lines 24–31. It proceeds by pattern matching on the input list. The case of the empty list (constructor `Nil`) is `absurd` as the pre-condition specifies
the input list should not be empty (expressed as a fact on its length in line 20). For this specific branch, the verification condition is equivalent to `forall xs:list int. length xs > 0 -> not (xs = Nil)`. If the list is a singleton (case `(Cons x Nil)`), the result is of course the only element of the list. Otherwise, — and let us ignore lines 28–29 for the moment — the result is the maximum of the head and the recursive call on the tail (line 30). Without lines 28–29, the execution of the tool now answers:

```
File maximum.mlw:
Goal max'vc.
Prover result is: Valid (0.00s, 9 steps).
File maximum.mlw:
Goal maximum'vc.
Prover result is: Timeout (5.00s).
```

Using Z3 or CVC5, or increasing the timeout, or changing the proof strategy does not change the outcome. It is possible to apply transformations to the goals. Using the WHY3 IDE, just splitting the verification condition for `maximum` gives five verification conditions: one for verifying the empty case is indeed absurd, one to check that the recursive call is indeed decreasing, one to check the pre-condition of the recursive call and one for each post-condition. All these sub-goals are valid but the one corresponding to the post-condition in line 22 which remains unknown.

To help the provers, we added lines 28–29 which relate elements of `xs` with elements of its tail via `nth`. The WHY3 IDE has a panel called “Task” [8] that shows the selected verification condition, a goal, together with the local context in which the proof is tried. Often, asking oneself how one would prove the goal using the local context and possibly lemmas in the global context is enough to find an assertion to guide the provers. Indeed, in this case, the assertion is easily verified and then eases the verification of the post-condition. The answer of the tool changes to:

```
Prover result is: Valid (0.09s, 478 steps).
```

Note that instead of an assertion, we could state the following lemma:

```
lemma cons_ext:
    ∀ xs xs': list α, x': α.
        xs = Cons x' xs' →
        ∀ i: int. 0 ≤ i < length xs' → xs[i+1] = xs'[i]
```

This lemma is proved in 10 steps and the proof of the verification condition for `maximum` takes about 800 steps. There is also an important difference. If the assertion needs to be modified, WHY3 only has to reprove the function that contains it: the assertion is in the local context of the verification condition of the function. If we change the lemma, all the modules that import the lemma will be rechecked.

## 2.2 Limitations with higher-order functions

To show the limitations of WHY3 in handling higher-order functions, let us consider the example of Figure 2. Intuitively, `option α` extends the type `α` with a value `None` and all the other values are encapsulated in the constructor `Some`.

In lines 1–10, we define a module `Concrete` containing the definition of a function `remove_option` that extracts the value encapsulated in an optional value assuming this value is not `None`. In the module `Failure`, we apply this function but through a higher-order function `apply` that just applies a function to a value. The tool fails to verify the function `test_KO` which intuitively does exactly the same as `remove_option`. Note that if `remove_option` was performing side effects or was partial because it may raise exceptions, WHY3 would reject the program with an error. Here the problem is less visible. Indeed, the arguments of a higher-order function
<figure><img src="image_4.png" /><figcaption>Figure 2: Limitations with Higher-Order Functions</figcaption></figure>

must be purely functional and *total* functions. In our case `remove_option` is not total as its pre-condition excludes `None`. The manifestation of the problem can be seen in a sub-verification condition generated by `WHY3: ∀ opt:option α. opt ≠ None`, which is impossible to prove.

Still, as most BSML primitives are higher-order functions, and we need to use functions such as `remove_option`, a work-around was needed. Our solution is shown in module `Abstract` (lines 19–24). Instead of writing a concrete implementation of `remove_option`, we declare a function `remove_option` without defining it, and we only give its semantics (with an `axiom`) when the pre-condition is met. It looks like a total function but if its application does not satisfy
the precondition then it is impossible to reason about the result of the application. In module `Success`, the same client code as module `Failure` uses module `Abstract` instead of module `Concrete` and the verification succeeds.

The overall verification of a client code may work despite an application of `remove_option` to `None`. Function `g` in module `BizarreUse` is correct with respect to its specification. But `remove_option` is applied to `None`. This application is not axiomatized thus `WHY3` cannot reason about this expression. But as the expression is not used, it does not matter.

Now imagine we extract this code. To run the extracted code, we have to provide an implementation for `remove_option`. We can basically write an OCaml version which is almost like the version of the `Concrete` module but raises an exception instead of using `absurd`. Such an implementation satisfies the semantics of the abstract version. As OCaml has an eager evaluation strategy, the expression `(remove_option None)` would be executed and the program would stop with an uncaught exception. The only way to avoid this kind of problem is to statically analyze the OCaml code extracted from `WHY3` to check for uncaught exceptions [33, 34].

Currently, `remove_option` is only used a few times in our development, and we were careful to check the value of the application is not discarded but used thus guaranteeing that `remove_option` is not applied to `None`.

## 3 Functional Bulk Synchronous Parallelism

The OCaml language is a versatile programming language that combines functional, imperative and object-oriented paradigms. BSML [39] (Bulk Synchronous Parallel ML) is an OCaml-based library that embodies the principles of the BSP [54, 42, 4] (Bulk Synchronous Parallel) model. It provides a range of constants and functions to facilitate BSP programming.

The BSP machine, viewed as a homogeneous distributed memory system with a point-to-point communication network and a global synchronization unit, serves as the underlying architecture for BSML. Note that this architecture is abstract in the sense that any general purpose parallel architecture can be seen as a BSP machine. For example, in a cluster of PCs there is rarely a global synchronization unit provided by hardware but rather provided by software. A shared memory machine can also be seen as a BSP computer if each core uses a dedicated part of the shared memory and communications and synchronizations are done in shared parts.

BSP programs, composed of consecutive super-steps, run on this kind of machine. The execution of each super-step follows a distinct pattern, starting with the computation phase where each processor-memory pair performs local computations using data available locally. This phase is followed by the communication phase, during which processors can request and exchange data with other processors. Finally, the synchronization phase concludes the super-step, synchronizing all processors globally. The BSP model also comes with a simple, yet realistic, computational cost model. For the sake of conciseness, we refer to [51] for a presentation.

With its collection of four expressive functions and constants like `bsp_p` representing the number of processors in the BSP machine, BSML empowers developers to implement BSP algorithms. While OCaml supports imperative programming and BSML can exploit it [36], in this paper we only consider the pure functional aspects of OCaml and BSML. This deliberate focus differentiates it from the imperative counterparts provided by libraries such `BSPlib` for C [30]. The types and informal semantics of BSML *primitives* are listed in Figure 3. In this Figure, `p` is the number of processes of the BSP machine, which is a constant during a run. The current implementation of BSML relies on MPI [52]: `p` is not set at compile time but can be set at runtime. The BSML primitives can be associated to BSP cost formulas to reason about the computational cost of BSML programs [35].

Let us consider a function `f` that maps integers to values of type `α` (denoted as `f: int→α` in OCaml). The BSML primitive `mkpar f` produces a *parallel vector* of type `α par` when applied to function `f`. Parallel vectors always have size `bsp_p`. In this parallel vector, each processor,
bsp-p : int
bsp-p = p
mkpar : (int → α) → α par
mkpar f = ⟨f 0, ..., f (p − 1)⟩
proj : α par → (int → α)
proj ⟨v₀, ..., vₚ₋₁⟩ = function 0 → v₀ | ... | p − 1 → vₚ₋₁
apply : (α → β)par → α par → β par
apply ⟨f₀, ..., fₚ₋₁⟩ ⟨v₀, ..., vₚ₋₁⟩ = ⟨f₀ v₀, ..., fₚ₋₁ vₚ₋₁⟩
put : (int → α)par → (int → α)par
put ⟨tosend₀, ..., tosendₚ₋₁⟩ = ⟨received₀, ..., receivedₚ₋₁⟩
where for all src, dst
0 ≤ src, dst < p ⇒ receivedₐₛₙ src = tosendₐₛₙ dst

<caption>Figure 3: BSML primitives</caption>

identified by the index value *i* within the range 0 ≤ *i* < bsp_p, stores the computed value of expression (*f* *i*). For instance, evaluating the expression mkpar(*fun* *i*→*i*) yields a parallel vector denoted as ⟨0, ..., bsp_p - 1⟩ of type *int* par. Throughout subsequent discussions, we shall refer to this parallel vector as *this*.

To apply a parallel vector of functions (which is not a function) to a parallel vector of values, one has to use the primitive `apply`. Both `mkpar` and `apply` are executed within the pure computation phase of a super-step. For communications and an implicit synchronization barrier, the last two primitives `proj` and `put` should be applied. `proj` is essentially an inverse of `mkpar` but the resulting function is partial and only defined on the interval `[0, p - 1]`. In the input vector of `put`, each function encodes the messages to be sent to other processors by the processor holding it. In the result vector, each function represents the messages received from other processors by the processor holding the function. It may look as if the `put` primitive implements a communication pattern where each processor exchanges messages with all the processors. It is however not the case. For example, the type `option` described in Section 2.2 is defined in the `WHY3` standard library as `type option α = None | Some α`. The constructor `None` does not take any argument: it is a so-called "constant" constructor. As it is the first constant constructor of this type, it is considered by BSML to represent the empty message which is never actually exchanged. Therefore, the `put` primitive allows one to program any communication pattern of a BSP super-step. This is not specific to the `option` type: for any type, the first constant constructor is considered to represent the empty message. For example, this is also the case of the empty list. If a type does not have a constant constructor then if messages are of the type `put` can only perform an all-to-all communication pattern.

Figure 4 presents a small BSML example using its primitives and `parfun` which is part of its standard library. `List.map` and `List.fold_left` are part of the OCaml standard library and are sequential map and reduce functions.

Lines 4–5, we define a function `list_of_par` which converts a parallel vector into a list. This function requires a full super-step for its execution because it needs data exchanges. Also, part of the BSML standard library, `procs` has type `int list` and is the list `[0;...;bsp_p-1]`.

Lines 7–8, we define an algorithmic skeleton: a parallel map that operates on a distributed list (represented here as a value of type `α list par`). This function requires the computation phase of a super-step and does not need any data exchange or synchronization.

Lines 10–13, we define the `reduce` algorithmic skeleton, using a binary associative operation `op` and a neutral element `e`, it “sums” a distributed list into a single value. It proceeds in two steps. First, each processor compute a partial “sum” of the list it holds locally. Second, this vector of partial sums is transformed into a list which is finally summed up. As we call
`list_of_par`, a full super-step is required.

Finally, in lines 15–18, we implement a parallel function to solve the maximum prefix sum problem. Computing at the same time the maximum prefix sum and the sum of a list (in a pair) can be implemented using `map` and `reduce`. For example, on a machine with at least 4 processors, the value of `mps` (`mkpar(function|0→[1;2]|1→[-1;2]|2→[-1;3]|3→[-4]|_→[])`) is 6. Indeed, the argument of `mps` is a distributed version (on 4 processors) of the list `[1;2;-1;2;-1;3;-4]` and its prefix with the largest sum is the list without its last element. We specify and prove the correctness of `mps` in Section 7.2.

1. `open Bsml`
2. `open Stdlib.Base`
3. `let list_of_par (v: α par) : α list =`
   List.map (proj v) procs
4. `let map : (α→β) → α list par → β list par =`
   fun f v → parfun (List.map f) v
5. `let reduce : (α→α→α) → α → α list par → α =`
   fun op e v →
   let locally_reduced = parfun (List.fold_left op e) v in
   List.fold_left op e (list_of_par locally_reduced)
6. `let mps : int list par → int =`
   let op (xm, xs) (ym, ys) = (max 0 (max xm (xs+ym)), xs+ys) in
   let f x = (max 0 x, x) in
   fun v → fst (reduce op (0, 0) (map f v))

<caption>Figure 4: A BSML Example</caption>

# 4 Formalization of BSML Core

To be able to specify and write BSML programs, we need BSML primitives in WhyML. BSML primitives are implemented in parallel on top of MPI [52] called through OCaml's Foreign Function Interface (FFI). Therefore, we cannot provide BSML in WhyML as an *implementation*. We need to give a BSML *theory*: a set of constant, *axioms* and function *declarations*. The axiomatization of BSML primitives can be found in Figure 5.

The semantics of functions `mkpar`, `apply`, `proj` and `put` are expressed in their contract (lines 12–25) while the strict positivity condition on `bsp_p` is given as an axiom on line 4. The type of parallel vector is abstract. Still we need to be able to observe parallel vectors. That is the role of logic function `get`: it can only be used in specifications.

The axiomatization is very close to the informal semantics of Figure 3. Instead of considering the parallel vectors globally with the notation $\langle v_0, \dots, v_{p-1} \rangle$, we consider each value $v_i$ denoted by `get v i`, and a bounded universal quantification of the form $\forall i:int. 0 \le i < bsp_p \rightarrow get v i = \dots$.

This way of presenting the semantics (wrt. to the way it is presented in Figure 3) makes very clear that `proj` and `get` have the same semantics, thus making `get` a function for specifications only may look redundant. However, the intent is very different: `get` is written only in specifications, can be thought as an indexed array access, and is used for *local* reasoning, while `proj` is used only in programs and requires a full super-step to execute. `proj` should rather be thought as a *global* (i.e. concerning and involving all the processors) conversion of a parallel
module BSML
use int.Int

val constant bsp_p : int

axiom at_least_one�processor : bsp_p > 0
type par α

function get (_: par α) (_: int): α

val mkpar (f: int→α): par α
ensures { ∀ i:int. 0 ≤ i < bsp_p → get result i = f i }

val apply (vf: par(α→β))(vv: par α): par β
ensures { ∀ i:int. 0 ≤ i < bsp_p →
           get result i = (get vf i) (get vv i) }

val proj (v: par α)(pid: int): α
ensures { result = get v pid }

val put (v: par(int→α)): par(int→α)
ensures { ∀ src dst: int.
           0 ≤ src < bsp_p → 0 ≤ dst < bsp_p →
           (get result dst) src = (get v src) dst }
end

<caption>Figure 5: BSML Theory in WhyML</caption>

vector into a function. From this point of view, and as we wrote in Section 3, **proj** is essentially
the inverse of **mkpar**. Of course, if we forget the cost of communication and synchronization,
this primitive allows one to obtain the value of a vector **v** at a given processor **i**. However,
it should not be used for such individual vector access, otherwise the performances would be
extremely poor. In practice, **get** is fully applied, while **proj** is first partially applied to its first
argument only.

It is possible to realize this theory by a sequential implementation, to ensure the consistency
of this theory. Figure 6 presents such a realization where parallel vectors are represented by
functions from processor identifiers to values. On line 1, the module **Realization** is declared
to respect the interface **bsml.BSML** (meaning the theory **BSML** in file **bsml.mlw**). Verification
conditions are generated to check this is the case. Constant and functions declarations are
replaced by constant and function definitions and the only axiom is replaced by a **lemma** (line 6).
**WHY3** proves this lemma automatically.

5 Formalization of BSML Standard Library

The BSML theory allows us to write BSML programs and their specifications. It is expressive enough for the WHY3 framework to verify that they indeed satisfy their specifications.

To illustrate the use of this theory, we now specify, implement and verify several of the
functions provided in the BSML standard library. The first one is `replicate`:
module Realization : bsml.BSML
use int.Int

let constant bsp_p = 16

lemma at_least_one�processor : bsp_p > 0
type par α = int → α

function get (v: par α)(pid: int) : α
= v pid

let mkpar (f: int→α): par α
ensures { ∀ i:int. 0 ≤ i < bsp_p → get result i = f i }
= f

let apply (vf: par(α→β))(vv: par α): par β
ensures { ∀ i:int. 0 ≤ i < bsp_p →
           get result i = (get vf i) (get vv i) }
= fun pid → (vf pid)(vv pid)

let proj (v: par α)(pid: int) : α
ensures { result = get v pid }
= v pid

let put (v: par(int→α)): par(int→α)
ensures { ∀ src dst:int.
           0 ≤ src < bsp_p → 0 ≤ dst < bsp_p →
           (get result dst) src = (get v src) dst }
= fun dst src → (v src) dst
end

<caption>Figure 6: A Realization of the BSML Theory</caption>

let replicate (x: α): par α
ensures { ∀ i:int. 0 ≤ i < bsp_p → get result i = x }
= mkparfun _ → x)

This verified function has only one post-condition: the result of replication is a parallel vector
which contains the same value everywhere.

In Section 3, we mentioned the function **parfun** without defining it. Its implementation and
specification follows, as well as the definition of function **parfun2**:

let parfun (f: α→β)(v: par α): par β
ensures { ∀ i:int. 0 ≤ i < bsp_p →
           get result i = f (get v i) }
= apply (replicate f) v

let parfun2 (f: α→β→γ)(u: par α)(v: par β): par γ
ensures { ∀ i:int. 0 ≤ i < bsp_p →
           get result i = f (get u i) (get v i) }
= apply (parfun f u) v

It shows how to use the `apply` primitive. There is also a `parfun`3 function omitted here.

To illustrate `proj`, we define `list_of_par`. As we mentioned before this function requires a complete super-step to run. Again it should be seen as a *global* conversion from parallel vectors to lists:

```hkl
let function list_of_par (v: par α): list α
ensures { ∀ i:int. 0 ≤ i < bsp_p → result[i] = get v i }
ensures { length result = bsp_p }
= map (proj v) procs
```

As in the BSML/OCaml version we call `procs`, the list of all processor identifiers. The definition of `procs` relies on a function `from_to` itself implemented using an `init` function. Our contribution also contains a library of sequential functions, mostly on lists, as well as verified lemmas stating their properties. These functions can in most cases be used both in programs and in specifications.

Finally, the `put` primitive is illustrated to implement a broadcast function. This data exchange (and implicit global synchronization) function is more precise than `proj`. We remind that after a `put`, for all processors `d` and `s`, the result function at destination processor `d`, applied to the identifier of source processor `s` returns the value of the input function at source processor `s` applied to destination processor `d`.

The definition of the `bcast_direct` function of the standard library follows. This function is used to broadcast a value from a `root` processor to all other processors. To do so, first, we prepare a function vector for the processors to make the messages to send to each other (local definitions `makeMsg` and `to_send`). It is clear that only the `root` processor will send data. The other processors' messages are `None` which is interpreted by the BSML/OCaml implementation as an empty message. Second, the local definition `received` proceeds with the data exchange and ends the super-step. `received` is a parallel vector of functions. What we are interested in is the value sent by processor `root`. That is why the local definition `optional_result` then applies this parallel vector of functions to the replicated value `root`. Of course, the obtained message is encapsulated in a `Some` constructor. Therefore, all the processors finally apply `remove_option` to yield the final result. The broadcast is meaningless if `root` is not a valid processor identifier. In this case, the exception `Bcast` is raised:

```hkl
let bcast_direct (root: int)(v: par α): par α
ensures { 0 ≤ root < bsp_p →
           ∀ i:int. 0 ≤ i < bsp_p →
               get result i = get v root }
raises { Bcast → not(0 ≤ root < bsp_p) }
= if (0 ≤ root) && (root < bsp_p)
then
  let makeMsg src load = fun _ →
                        if src = root then Some load else None in
  let to_send = apply (mkpar makeMsg) v in
  let received = put to_send in
  let optional_result = apply received (replicate root) in
  parfun remove_option optional_result
else raise Bcast
```

We only presented a sub-set of the functions of the BSML standard library we implemented, and we refer to the companion artifact for the complete set of functions. We provide:

* several variants of `apply`,

* the `shift`, `shift_right` and `shift_left` communication functions, which offer a different communication pattern than `bcast`: Each data item is shifted by a certain number of processors,
* the `scatter` function that cuts the value at a given processor into pieces and scatters the pieces on all the processors,

* the `gather` and `gather_list` functions that gather all the values of a vector in a given processor, the result being a function (of processor identifiers) or a list.

Compared to the BSML standard library implemented in parallel, functions working on mutable data structures are omitted because they cannot be verified due to the limitations related to higher-order functions. A few communication functions are also omitted because they are basically implementations with the current primitives of previous versions of BSML primitives which are not often used.

# 6 First Homomorphism Theorem and Algorithmic Skeletons

```hml
module ListFirstHomomorphismTheorem

use ListBasic

use ListAppend

use ListMap

use ListFold

```

```hml
predicate homomorphic (h: list α→β)(op: β→β→β) =
    ∀ xs ys: list α. h(xs++ys) = op(h xs)(h ys)
```

```hml
let rec lemma first_homomorphism_theorem
    (h: list α → β)(op: β→β→β)(xs: list α)
    requires { homomorphic h op }
    ensures { h xs = fold_left op (h Nil)
                (map (fun x→h(Cons x Nil)) xs) }
    = match xs with
        | Nil → ()
        | Cons x' xs' →
            fold_left_homomorphic h op x' xs' Nil;
            first_homomorphism_theorem h op xs'
    end

end
```

<caption>Figure 7: The First Homomorphism Theorem</caption>

Proving the correctness of parallel programs with respect to sequential specifications will proceed as follows. First, we will establish that the specification is a homomorphism. Second, we will write the parallel program as a composition of the skeleton *map* and the skeleton *reduce*. Why3 will then be able to prove that the parallel program is indeed correct with respect to the specification by using:

1. the first homomorphism theorem [25] that states that a homomorphic function can be written as a composition of (sequential) *map* and *reduce*,

2. the contracts of our definitions of the skeletons that relate the results returned by the skeletons to the result returned by the corresponding sequential functions.
```hkl
let function map_par (f: α→β)(dl: par (list α)): par (list β)
ensures { ∀ i:int. 0 ≤ i < bsp_p →
         get result i = map f (get dl i) }
ensures { to_list result = map f (to_list dl) }
= let ghost _ = flatten_map f (list_of_par dl) in
  parfun (map' f) dl
```

```hkl
let function reduce_par (ghost inv: α→bool)
  (op: α→α→α)(e: α)(dl: par(list α)): α
requires { associative inv op }
requires { neutral inv op e }
requires { preserves inv op }
requires { inv e }
requires { ∀ i:int. 0 ≤ i < bsp_p →
           satisfies inv (get dl i) }
ensures { result = fold_left op e (to_list dl) }
= assert { fold_left op e (flatten (list_of_par dl)) =
           fold_left op e (map (fun xs→fold_left op e xs)
                                 (list_of_par dl)) };
let reduce_seq l = fold_left op e l in
let partial_reductions = parfun reduce_seq dl in
reduce_seq (list_of_par partial_reductions)
```

<caption>Figure 8: Verified Map and Reduce Algorithmic Skeletons in WhyML</caption>

## 6.1 First Homomorphism Theorem

Figure 7 shows an excerpt of the module containing the theorem. Lines 7-8 define what is a homomorphic function on lists. A function `f` is homomorphic when there exists a binary operation `⊙` such that: $\forall 11 \ 12: \text{list } \alpha$. $f(11++12) = (f \ 11) \odot (f \ 12)$ where `++` denotes list concatenation.

The statement of the first homomorphism theorem is given Line 10-14 and is quite straightforward. The function that reduces the list to a single value using the binary operator is called `fold_left` and takes as an additional argument an accumulator which is also the value returned if the input list is empty. The function used as argument to `map` is the function $x \mapsto [x]$ where $[x]$ denotes a singleton list.

Line 10 starts with `let rec` instead of just `lemma`. As `assert` in the example of Figure 1, this is another way to help the system proving verification conditions. `first_homomorphism_theorem` is a `lemma function`. As a function it returns a value of type `unit` (a type with only one value `()`) therefore nothing interesting, but its body helps structure the proof. The `match` constructor together with `let rec` indicates this is a proof by induction on the list `xs`. In the empty list case, we let the provers work by themselves. In the inductive case, in addition to an explicit recursive call to the lemma function, we also call `fold_left_homomorphic` which is another lemma function of the same module and proved by induction, but omitted here: it is a rather technical lemma used to transform a composition of `fold_left` and `map` using the fact that the binary operation associated to a homomorphic function is associative on the image of this function.
```
predicate associative (inv: α→bool)(op: α→α→α) =
    ∀ x y z:α. inv x → inv y → inv z →
    op x (op y z) = op (op x y) z
```

```
predicate neutral (inv: α→bool)(op: α→α→α)(e: α) =
    (∀ x:α. inv x → op x e = x) ∧
    (�forall x:α. inv x → op e x = x)
```

```
predicate preserves (inv: α→bool)(op: α→α→α) =
    ∀ x y: α. inv x → inv y → inv (op x y)
```

```
predicate satisfies (inv: α→bool)(xs: list α) =
    ∀ i:int. 0 ≤ i < length xs → inv (nth i xs)
```

<caption>Figure 9: Algebra Concepts</caption>

## 6.2 Algorithmic Skeletons: Map and Reduce

The skeleton `par_map` is defined in lines 1–6 of Figure 8. The only difference with its BSM-L/OCaml counterpart is the post-conditions including one expressed as a correspondence with the sequential `map`. Given a distributed list `dl` (of type `par(list α)`), one obtains the same result by either applying `par_map` then transforming the obtained distributed list into a list with `to_list`, or applying the sequential `map` to the sequentialization of the distributed list. Line 5 is just a hint for the provers: an application of lemma function `flatten_map` that basically commutes `map` and `flatten`. Note that `par_map` uses the function `map'` as the sequential map rather than `map`. `map'` is a tail recursive version which allows working on huge lists.

The implementation (lines 8-22) of the parallel reduction `reduce_par` is also very close to its BSML/OCaml counterpart of Figure 4. As expected, the post-condition on line 16 is expressed with respect to the sequential reduction here implemented with the usual `fold_left` function. As the result is already a sequential value there is no need to sequentialize it. However, this correspondence is true only if `op` is associative and `e` is its neutral element which are two pre-conditions stated lines 10–11. There are two additional pre-conditions and a `ghost` [19] argument, i.e. an argument only used in the contract (and possible annotations) of the function. The reason is again to deal with a form of partial functions. `op` is a total function, but it may not have the desired properties (associativity, neutral element) on all the values of its input type. Indeed, the OCaml version of `op` for `mps` that we will also use in the WhyML version of `mps`, is not associative if we consider all pairs of integers. In the maximum prefix sum problem, the first component of such a pair represents the maximum prefix sum, it is therefore positive, and the second component the sum of the list, thus it is lower or equal to the first component. The ghost argument `inv` expresses such properties on the values manipulated during the reduction. This is an invariant: `op` should preserve the property (line 12) and the input values `e` and `dl` should satisfy this property (line 13). The predicates `associative`, `neutral`, `preserves` and `satisfies` are defined in Figure 9. Such definitions work also well when there is no need for an invariant: in this case we simply use the constant Boolean function always returning `true`.

## 7 Applications

We built a set of modules of increasing abstraction, from BSML primitives to a small library of algorithmic skeletons and how a composition of skeletons relate to sequential homomorphic functions. We illustrate the use of these skeletons with three applications. The two first examples are simple applications (Section 7.1): the first compute in parallel the average of a distributed
module Average

function avg_spec (l: list int) : (int, int)
= (sum l, length l)

let function op (x: (int,int)) (y: (int,int)) : (int,int)
= (fst x + fst y, snd x + snd y)

let function f (x: int) = (x, 1)

lemma avg_spec_f: ∀ x: int. avg_spec (Cons x Nil) = f x

lemma avg_spec_Nil: avg_spec Nil = (0,0)

lemma avg_spec_homomorphic: ∀ 11 12: list int.
    avg_spec (11 ++ 12) = op (avg_spec 11) (avg_spec 12)

let avg_par (dl: par (list int)) : (int, int)
ensures { result = avg_spec (to_list dl) }
= let ghost _ =
    first_homomorphism_theorem avg_spec op (to_list dl) in
reduce_par (fun _→true) op (0,0) (map_par f dl)

end

<caption>Figure 10: Verified Parallel Average in WhyML</caption>

list of integers and the second counts the number of elements of a distributed list that satisfy a given predicate. This second parallel function is polymorphic. The third example (Section 7.2) is a verified parallel implementation to compute the maximum prefix sum of a distributed list of integers. In Section ??, we discuss statistics on the development and verification as well as a strategy, a feature of WHY3, that describes how to alternate the application of external provers to verification conditions and transformation steps on the verification conditions to perform the verification.

## 7.1 Average and Count

To compute the average of a list of integers, we compute the sum of the elements of the list and the length of the list. That is the specification for the program (Figure 10, lines 3-4). We then define the binary operation used by the reduction and the function `f` used by the map (lines 6-9). We then state a lemma relating the specification `avg_spec` to `f`, a lemma giving the value when the list is empty, and a lemma observing that `avg_spec` is homomorphic. Finally, in lines 18-21 we define a parallel implementation of the computation of the average using the skeletons defined in Section 6.2. The only annotation needed to help the provers check that this parallel implementation is equivalent to the specification `avg_spec` is a call to the lemma function `first_homomorphism_theorem` (lines 20-21).

To count the number of elements that satisfy a property (Figure 11), the process is the same: first we define the specification, in this case defined using the classic functions `length` and `filter` on lists (and defined in our sequential library), define a unary function (the binary operation is simply `+`) and state three lemmas. Second we define the parallel program using `reduce_par` and `map_par` and help the automatic provers with an annotation calling the first
homomorphism theorem.

<figure><img src="image_5.png" /><figcaption>Figure 11: Verified Parallel Count in WhyML</figcaption></figure>

## 7.2 Maximum Prefix Sum

As a last application, we specify and verify an implementation of the maximum prefix sum informally presented in Section 3. Similarly to the BSML implementation, the implementation with WhyML relies on algorithmic skeletons.

With these skeletons, it is possible to implement a parallel function to compute the maximum prefix sum of a distributed list as we did in Section 3. First, we define a *specification* which is an inefficient but direct translation of the informal specification: the `mps_spec` function on lines 3-4 of Figure 12. We also define `op` (lines 9-10) and `f` (line 12) which are the arguments to `map` and `reduce` as in the BSML/OCaml example of Figure 4. This time, they are not local definitions because we need to state and verify some lemmas about them and because we have three versions of `mps`: `mps_seq`, `mps_par`, and `mps_par'`.

The invariant explained in Section 6.1 is defined lines 14–15. We need an auxiliary function to verify the correctness of our functions with respect to the specification: `ms` (line 6–7) is the tupling of `mps_spec` and `sum`. The rest of the code in Figure 12 is the definitions of the sequential and parallel versions of the auxiliary function `ms` and maximum prefix sum computation. They are expressed as compositions of `map` and `reduce` (respectively sequential and parallel).

The proof that `ms_seq` indeed implements the specification `ms_spec` proceeds by using again the first homomorphism theorem. `mps_spec` is not homomorphic but `ms` is. Two lines of annotations are necessary to guide the provers in the sequential case (lines 19–20). The parallel cases need similar annotations.

While Figures 10 and 11 present almost the complete modules (the `used` modules are omitted as well as the sequential versions), Figure 12 presents only excerpts: additional lemmas and lemma functions are necessary.
module MPS

let function mps_spec (l: list int) : int
    = maximum (map sum (prefix l))

function ms (l: list int) : (int,int)
= (mps_spec l, sum l)

let function op (x: (int,int)) (y: (int,int)) : (int, int)
= (max (max 0 (fst x)) ((snd x)+(fst y)), (snd x)+(snd y))

let function f (x : int) = (max 0 x, x)

predicate mps_sum_inv (x: (int,int))
= 0 ≤ fst x ∧ fst x ≥ snd x

let function ms_seq (l: list int) : (int, int)
ensures { result = ms l }
= let ghost _ = first_homomorphism_theorem ms op 1 in
assert { fold_left op (0, 0) (map f 1)
    = fold_left op (0, 0) (map' f 1) };
fold_left op (0, 0) (map' f 1)

let function mps_seq (l: list int) : int
ensures { result = mps_spec l }
= fst (ms_seq l)

let ms_par (dl: par(list int)) : (int, int)
ensures { result = ms (to_list dl) }
= let mapped = map_par f dl in
assert { ms (to_list dl) = ms_seq (to_list dl) };
reduce_par mps_sum_inv op (0, 0) mapped

let mps_par (dl: par(list int)) : int
ensures { result = mps_spec (to_list dl) }
= fst (ms_par dl)

end

<caption>Figure 12: Verified Maximum Prefix Sum in WhyML</caption>

## 7.3 Statistics on the Development and Verification

The full development is about 950 lines of WhyML (excluding comments) with about 45% of specifications and 55% of code. The application are rather small: average and count are less than 20 lines long and mps is about 100 lines. A root goal is a verification condition. When the provers fail to prove such a goal, transformations may be applied that may generate several sub-goals. For example, the split_vc transformation creates sub-goals from a goal that is a conjunction and the verification condition of mps_seq is split in 3 sub-goals. The verification generates 134 root goals, 100% of which are verified. Their verification produces 105 sub-goals,
<table><caption>Table 1: WHY3 Session Information for WhyBSML</caption><thead><tr><td>Prover</td><td>Attempted</td><td>Proved</td><td>Min</td><td>Max</td><td>Avg</td></tr></thead><tbody><tr><td>Alt-Ergo 2.5.2</td><td>215</td><td>183</td><td>0.02s</td><td>11.42s</td><td>0.17s</td></tr><tr><td>CVC4 1.8</td><td>56</td><td>24</td><td>0.12s</td><td>39.48s</td><td>1.86s</td></tr></tbody></table>

also all automatically verified.

It is possible with WHY3 to apply interactively transformations to verification conditions. In some cases, the transformation to apply is very easy to find (for example applying a lemma) but provers take a long time to find the correct application. However, such proof scripts are not easily portable, thus we avoided using them. All the verification conditions are verified automatically.

Moreover, we designed a strategy [7, Chapter 12.6] to increase portability: it relies only on Alt-Ergo which is as easily available as WHY3 itself using the opam package manager of the OCaml ecosystem (and opam selects the correct version to install) and CVC4 version 1.8 which is also easily installed. WHY3 pre-defined strategies use a large subset of the installed provers on the machine running WHY3 and are therefore less portable. In the WHY3 IDE, our strategy is named Auto WhyBSML. It sets a 2s timeout and tries Alt-Ergo then CVC4, and if unsuccessful tries to apply various transformations to the goal: splitting the goal and unfolding definitions, with increasing timeouts up to 64s and running the two provers in parallel.

While this strategy improves portability, there are still reproducibility problems: indeed the timeouts need to be precise in the strategy, but the running time of the provers depends on the execution environment, in particular the hardware.

Table 1 presents information given by the why3 session command for a session run on a MacBook Pro 2 GHz Intel Core i5 (4 cores), MacOS Sonoma 14.1.1. The second column gives the number of attempted proofs and the third the number of successful proofs. In these numbers, the goals verified because their sub-goals are proved are not counted, that is why the total of proved goals is not 239 (134 root goals and 105 sub-goals). Appendix A gives detailed session information. Replaying this session takes about 2m30s running 3 tasks in parallel. There are not too many failed attempts, the average runtime of external prover is reasonable and the appendix shows that failed attempts timeout quickly most of the time. There are however 20 proofs that require more than a second, including one that is over 30s.

# 8 Code Extraction and Experiments

WHY3 allows one to extract [7, Sections 5.9, 9.2][46] OCaml code from WhyML code, which can then be compiled using the OCaml compiler. It is possible to extract all the modules of a file, a specific module or even a specific symbol in a module. The extracted code could be in one file (flat) or each WHY3 module could be extracted to a corresponding OCaml module (modular). Finally, if a specific module or symbol is selected, its dependencies are not extracted unless the recursive option is chosen. We extract in a modular way and recursively a set of modules.

There are however two pieces of code we cannot extract: the theory BSML and the axiomatized function remove_option. In the case of BSML, we wrote a realization of this theory, but we do not want to use this realization. We prefer instead to use an efficient parallel implementation of BSML on top of MPI.

In both cases, we need to use a WHY3 driver that automatically replaces declared constants or functions by OCaml code. The driver for BSML simply replaces each item with its corresponding item in the BSML implementation, for example bsp_p with Bsml.bsp_p. An expression remove_option e is replaced with (match e with Some x → x | None → failwith "None").

As an example, the first driver follows:

module bsml.BSML
    syntax type par "Bsml.par"
```
syntax val bsp_p "Bsml.bsp_p"
syntax val mkpar "Bsml.mkpar %1"
syntax val apply "Bsml.apply %1 %2"
syntax val proj "Bsml.proj %1 %2"
syntax val put "Bsml.put %1"
```

end

We experimented on two different parallel machines:

* SPEED2, a machine with a 32-core processor (Intel Xeon Gold 5218), with 192 GB of memory, running Ubuntu 22.04, Why3 1.7.1, OCaml 4.13.1, GCC 11.4 and OpenMPI 4.1.2,

* a node of the machine LETO: a 128-threads processor (AMD Epyc 7702), with 512 GB of memory, running openSUSE Leap 15.2, Why3 1.7.1, OCaml 4.12.1, GCC 10.2 and OpenMPI 4.1.0.

For each experiment, we measured the time required for the computation 30 times. The Figures 13 and 14 present the median of these measurements together with the standard deviation, as well as the relative speed-up.

Figure 13 presents the results for `count_par` where the elements are square floating-point number matrices of size 50 × 50 and the predicate checks if the square of the matrix is diagonal. The experiment was conducted on a list of length $10^5$. There is an important decrease in speedup from 64 to 128: it is expected as there are only 64 physical cores in an AMD Epyc 7702 processor, 128 is obtained through hyper-threading which is less efficient than having physical cores.

Figure 14 presents the results for `mps_par` with a list of length $10^8$. The decrease in speedup is less than in the case of LETO because only physical cores are used, but SPEED2 is a desktop machine with more OS tasks running in the background than a node of LETO. Moreover, the computation task is lower in the case of MPS, hence the impact of communication and synchronization costs is more visible.

# 9 Related Work

BSP-WHY [21, 22] also uses (a previous version of) WHY to verify bulk synchronous parallel programs. However, the two approaches are very different. BSP-WHY considers BSP programs written in an imperative style close to BSPLib [30]. The verification proceeds by transforming well-formed programs — a sub-class of what has been formally defined later by Dabrowski as textually aligned programs [13] — into sequential simulating programs that are then verified using WHY. The BSP-WHY code cannot be run on parallel machines.

The work closest to our is the specification, verification and extraction of BSML programs using the Coq proof assistant. Early contributions started with the work of Gava [23]. A formalization of BSML primitives in a style very close to the WHY3 formalization presented in this paper was proposed by Tesson and Loulergue [53] and used in a framework, named SYDPACC, for the verification of BSP functional programs [17, 40]. The two main differences with our work is that: proofs are much less automated in Coq than in WHY3 but the framework leverages the type-class resolution mechanism of Coq to automatically parallelize programs. For example in this framework, the user does not need to write the code for `mps_seq` and `mps_par`, but only needs to write `mps_spec` and to prove that its tupling with `sum` is leftwards and rightwards (i.e. can be written as calls to `fold_left` and `fold_right`) and exhibits a weak right inverse. The framework would then use transformation theorems to automatically obtain `mps_seq` and then verified correspondences as expressed in the post-conditions of `map_par` and `reduce_par` to automatically produce `mps_par` [41].

Ono et al. [45] employed Coq to verify Hadoop MapReduce programs and extract Haskell code for Hadoop Streaming or directly write Java programs annotated with JML, utilizing
<figure><img src="image_6.png" /><figcaption>Figure 13: Count on LETO</figcaption></figure>
<figure><img src="image_7.png" /><figcaption>Figure 14: Maximum Prefix Sum on SPEED2</figcaption></figure>

Krakatoa [18] to generate Coq lemmas. The first part of their work is functional and therefore closest to our work. However, it is limited to MapReduce which is more general than the `map_par` and `reduce_par` skeletons but is less expressive than BSML. The second part of their work is more imperative.

On the verification of OCaml programs, GOSPEL is a specification language [9] and Cameleer [48] is a deductive verification tool using GOSPEL as a specification language. Considering the main limitations described in Section 2.2, GOSPEL and Cameleer are not improvement with respect
to WHY3 for the verification of BSML programs. Indeed, a function argument of a higher-order function should be pure [48, page 678].

# 10 Conclusion and Future Work

We were able to formalize the primitives of the parallel programming library BSML with WhyML and leverage WHY3 for verifying a large part of the BSML standard library as well as small applications written in BSML. Extracted code run on parallel machines confirmed the scalability of the obtained parallel code.

The future research directions include work on (1) the expressivity of the BSML library, (2) the ability to reason about BSP cost formally and finally (3) the verification of the BSML parallel implementation to decrease the trusted code base.

(1) The expressivity of the WhyBSML library could be improved in the following ways. First, to explore as much as possible the pattern of imperative programming that can be considered even with the higher-order function argument limitations. WhyML offers exceptions and references thus allows a user to write imperative programs. However, such programs cannot be passed as arguments to higher-order functions. It therefore limits the usage of imperative features with BSML as all primitives are higher-order functions. The code outside BSML primitives can be imperative thus the sequencing of BSP super-steps could be imperative. It is also possible to use imperative features to implement pure functions passed as arguments to BSML primitives. Also, it is possible to deal with partial functions as we did with *remove_some*. We plan to explore all these possibilities in the future. From the parallel programming perspective, the set of algorithmic skeletons provided by WhyBSML is quite small, even though broadcasting, gathering and scattering functions could be considered as algorithmic skeletons in addition to *map*, *reduce* and their combination. As the first homomorphism theorem shows, new skeletons should come with theorems that ease reasoning about them. In this respect, considering the diffusion theorem [31] and the GTA approach [16] and their associated algorithmic skeletons, would extend the family of functions for which a strong support exists to verify their correctness with respect to sequential functional contracts.

(2) Work exist with Rocq [28] and WHY3 [47] to reason about the algorithmic complexity of sequential programs. These are candidates to consider extension to be able to handle reasoning about the BSP cost of BSML programs.

(3) The OCaml+MPI implementation of BSML is unverified. Its formal verification faces several challenges. First, one need to be able to deductively verify MPI programs. Some work exists that leverage WHY3 to reason about MPI programs [50]. Second, one needs to reason both about OCaml programs, OCaml's FFI and C programs. An approach such as Melocoton [29] would be necessary.

# References

[1] Michael Armbrust, Tathagata Das, Aaron Davidson, Ali Ghodsi, Andrew Or, Josh Rosen, Ion Stoica, Patrick Wendell, Reynold Xin, and Matei Zaharia. Scaling Spark in the Real World: Performance and Usability. *PVLDB*, 8(12):1840–1851, 2015. URL http://www.vldb.org/pvldb/vol8/p1840-armbrust.pdf.

[2] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In *Tools and Algorithms for the Construction and Analysis of Systems (TACAS)*, volume 13243 of LNCS, pages 415–442, Cham, 2022. Springer. doi:10.1007/978-3-030-99524-9_24.
[3] Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In *Computer Aided Verification (CAV)*, volume 6806 of LNCS, pages 171–177, Berlin, Heidelberg, 2011. Springer. doi:10.1007/978-3-642-22110-1_14.

[4] Rob Bisseling. *Parallel Scientific Computation*. Oxford University Press, Oxford, second edition, 2020. doi:10.1093/oso/9780198788348.001.0001.

[5] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. *International Journal on Software Tools for Technology Transfer (STTT)*, 2014. doi:10.1007/s10009-014-0314-5.

[6] François Bobot, Jean-Christophe Filliâtre, Marché Claude, Guillaume Melquiond, and Andrei Paskevich. The Why3 Platform. https://why3.org, 2023.

[7] François Bobot, Jean-Christophe Filliâtre, Marché Claude, Guillaume Melquiond, and Andrei Paskevich. The Why3 Platform. https://why3.org, 2024.

[8] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd Your Herd of Provers. In *Boogie 2011: First International Workshop on Intermediate Verification Languages*, pages 53–64, Wroclaw, Poland, 2011. URL https://inria.hal.science/hal-00790310.

[9] Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, and Mário Pereira. GOSPEL - providing ocaml with a formal specification language. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, *Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings*, volume 11800 of Lecture Notes in Computer Science, pages 484–501. Springer, 2019. doi:10.1007/978-3-030-30942-8_29. URL https://doi.org/10.1007/978-3-030-30942-8_29.

[10] Joshua M. Cohen and Philip Johnson-Freyd. A formalization of core Why3 in Coq. *Proc. ACM Program. Lang.*, 8(POPL), January 2024. doi:10.1145/3632902.

[11] Murray Cole. *Algorithmic Skeletons: Structured Management of Parallel Computation*. MIT Press, Cambridge, 1989.

[12] Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. Alt-Ergo 2.2. In *SMT Workshop: International Workshop on Satisfiability Modulo Theories*, Oxford, United Kingdom, July 2018. URL https://inria.hal.science/hal-01960203.

[13] Frédéric Dabrowski. A denotational semantics of textually aligned SPMD programs. *J. Log. Algebraic Methods Program.*, 108:90–104, 2019. doi:10.1016/j.jlamp.2019.02.010.

[14] Jeffrey Dean and Sanjay Ghemawat. MapReduce: Simplified Data Processing on Large Clusters. In *OSDI*, pages 137–150, San Francisco, California, USA, 2004. USENIX Association.

[15] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: A foundry for the deductive verification of Rust programs. In *Formal Methods and Software Engineering (ICFEM)*, volume 13478 of LNCS, pages 90–105, Cham, 2022. Springer. doi:10.1007/978-3-031-17244-1_6.

[16] Kento Emoto, Sebastian Fischer, and Zhenjiang Hu. Filter-embedding semiring fusion for programming with MapReduce. *Formal Aspects of Computing*, 24(4-6):623–645, 2012. doi:10.1007/s00165-012-0241-8.
[17] Kento Emoto, Frédéric Loulergue, and Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. In *Interactive Theorem Proving (ITP)*, number 8558 in LNCS, pages 258–274, Cham, 2014. Springer. doi:10.1007/978-3-319-08970-6_17.

[18] Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In W. Damm and H. Hermanns, editors, *19th International Conference on Computer Aided Verification*, LNCS, Berlin, Heidelberg, 2007. Springer. doi:10.1007/978-3-540-73368-3_21.

[19] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. *Form. Methods Syst. Des.*, 48(3):152–174, June 2016. ISSN 0925-9856. doi:10.1007/s10703-016-0243-x.

[20] C. Foisy and E. Chailloux. Caml Flight: a portable SPMD extension of ML for distributed memory multiprocessors. In A. W. Böhm and J. T. Feo, editors, *Workshop on High Performance Functional Computing*, Denver, Colorado, April 1995. Lawrence Livermore National Laboratory, USA.

[21] Jean Fortin and Frédéric Gava. BSP-WHY: an intermediate language for deductive verification of BSP programs. In *4th workshop on High-Level Parallel Programming and applications (HLPP)*, pages 35–44, New York, 2010. ACM. doi:10.1145/1863482.1863491.

[22] Jean Fortin and Frédéric Gava. BSP-Why: A tool for deductive verification of BSP algorithms with subgroup synchronisation. *Int J Parallel Prog*, pages 1–24, 2015. doi:10.1007/s10766-015-0360-y.

[23] Frédéric Gava. Formal Proofs of Functional BSP Programs. *Parallel Processing Letters*, 13(3):365–376, 2003.

[24] Frédéric Gava and Ilias Garnier. New implementation of a BSP composition primitive with application to the implementation of algorithmic skeletons. In *23rd IEEE International Symposium on Parallel and Distributed Processing (IPDPS 2009)*, APDCM workshop, pages 1–8, New York, 2009. IEEE. doi:10.1109/IPDPS.2009.5160876.

[25] J. Gibbons. The third homomorphism theorem. *J Funct Program*, 6(4):657–665, 1996. doi:10.1017/S0956796800001908.

[26] Laure Gonnord, Ludovic Henrio, Lionel Morel, and Gabriel Radanne. A survey on parallelism and determinism. *ACM Comput. Surv.*, 55(10):210:1–210:28, 2023. doi:10.1145/3564529.

[27] Horacio González-Vélez and Mario Leyton. A survey of algorithmic skeleton frameworks: high-level structured parallel programming enablers. *Software, Practice & Experience*, 40 (12):1135–1160, 2010. doi:10.1002/spe.1026.

[28] Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In Amal Ahmed, editor, *Programming Languages and Systems (ESOP)*, volume 10801 of *Lecture Notes in Computer Science*, pages 533–560. Springer, 2018. doi:10.1007/978-3-319-89884-1_19.

[29] Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, and Derek Dreyer. Melocoton: A program logic for verified interoperability between OCaml and C. *Proc. ACM Program. Lang.*, 7(OOPSLA2):716–744, 2023. doi:10.1145/3622823.

[30] Jonathan M. D. Hill, Bill McColl, Dan C. Stefanescu, Mark W. Goudreau, Kevin Lang, Satish B. Rao, Torsten Suel, Thanasis Tsantilas, and Rob Bisseling. BSPlib: The BSP Programming Library. *Parallel Computing*, 24:1947–1980, 1998.
[31] Z. Hu, M. Takeichi, and H. Iwasaki. Diffusion: Calculating Efficient Parallel Programs. In *ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'99)*, pages 85–94, San Antonio, Texas, USA, January 22-23 1999. ACM.

[32] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. *Formal Asp. Comput.*, 27(3): 573–609, 2015. doi:10.1007/s00165-014-0326-7.

[33] Pierre Lermusiaux and Benoît Montagu. Detection of uncaught exceptions in functional programs by abstract interpretation. In *Programming Languages and Systems (ESOP)*, volume 14577 of LNCS, pages 391–420, Cham, 2024. Springer. doi:10.1007/978-3-031-57267-8_15.

[34] Xavier Leroy and François Pessaux. Type-based analysis of uncaught exceptions. *ACM Trans Program Lang Syst*, 22(2):340–377, 2000. doi:10.1145/349214.349230.

[35] Frédéric Loulergue. Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML. In *Parallel and Distributed Computing, Applications and Technologies (PDCAT)*, pages 461–468, New York, 2017. IEEE. doi:10.1109/PDCAT.2017.00079.

[36] Frédéric Loulergue. A BSPlib-style API for Bulk Synchronous Parallel ML. *Scalable Computing: Practice and Experience*, 18:261–274, 2017. doi:10.12694/scpe.v18i3.1306.

[37] Frédéric Loulergue and Olivia Proust. Whybsml (0.3). Zenodo, 2025.

[38] Frédéric Loulergue, Gaétan Hains, and Christian Foisy. A Calculus of Functional BSP Programs. *Sci Comput Program*, 37(1-3):253–277, 2000. doi:10.1016/S0167-6423(99)00029-5.

[39] Frédéric Loulergue, Frédéric Gava, and David Billiet. Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. In *International Conference on Computational Science (ICCS)*, volume 3515 of LNCS, pages 1046–1054, Berlin, Heidelberg, 2005. Springer. doi:10.1007/11428848_132.

[40] Frédéric Loulergue, Simon Robillard, Julien Tesson, Jeffrey Légaux, and Zhenjiang Hu. Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem. In *ACM Symposium on Applied Computing (SAC)*, pages 1577–1584, New York, 2014. ACM. doi:10.1145/2554850.2554912.

[41] Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calculating Parallel Programs in Coq using List Homomorphisms. *Int J Parallel Prog*, 45:300–319, 2017. doi:10.1007/s10766-016-0415-8.

[42] W. F. McColl. Scalability, portability and predictability: The BSP approach to parallel programming. *Future Gener Comp Sy*, 12:265–272, 1996. doi:10.1016/S0167-739X(96)00030-1.

[43] John W. McCormick and Peter C. Chapin. *Building High Integrity Applications with SPARK*. Cambridge University Press, Cambridge, 2015. doi:10.1017/CBO9781139629294.

[44] Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In *Tools and Algorithms for the Construction and Analysis of Systems (TACAS)*, volume 4963 of LNCS, pages 337–340, Berlin, Heidelberg, 2008. Springer. doi:10.1007/978-3-540-78800-3_24.

[45] Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, and Masami Hagiya. Using Coq in specification and program extraction of Hadoop MapReduce applications. In *SEFM, LNCS*, pages 350–365, Berlin, Heidelberg, 2011. Springer. doi:10.1007/978-3-642-24690-6_24.
[46] Mário José Parreira Pereira. *Tools and Techniques for the Verification of Modular Stateful Code*. PhD thesis, Université Paris Saclay (COmUE), December 2018. URL https://theses.hal.science/tel-01980343.

[47] Mário Pereira and Simão Melo de Sousa. Complexity checking of ARM programs, by deduction. In *Proceedings of the 29th Annual ACM Symposium on Applied Computing*, SAC '14, page 1309–1314, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/2554850.2555012.

[48] Mário Pereira and António Ravara. Cameleer: A deductive verification tool for ocaml. In Alexandra Silva and K. Rustan M. Leino, editors, *Computer Aided Verification (CAV)*, volume 12760 of *Lecture Notes in Computer Science*, pages 677–689, Virtual Event, 2021. Springer. doi:10.1007/978-3-030-81688-9_31.

[49] Olivia Proust and Frédéric Louergue. Verified scalable parallel computing with Why3. In *21st International Conference on Software Engineering and Formal Methods (SEFM)*, volume 14323 of *LNCS*, page 246–262, Cham, 2023. Springer. doi:10.1007/978-3-031-47115-5_14.

[50] César Santos, Francisco Martins, and Vasco Thudichum Vasconcelos. Deductive verification of parallel programs using why3. In Sophia Knight, Ivan Lanese, Alberto Lluch-Lafuente, and Hugo Torres Vieira, editors, *8th Interaction and Concurrency Experience (ICE)*, volume 189 of *EPTCS*, pages 128–142, Grenoble, France, 2015. doi:10.4204/EPTCS.189.11.

[51] D. B. Skillicorn, J. M. D. Hill, and W. F. McColl. Questions and Answers about BSP. *Scientific Programming*, 6(3):249–274, 1997. doi:10.1155/1997/532130.

[52] M. Snir and W. Gropp. *MPI the Complete Reference*. MIT Press, Cambridge, 1998.

[53] Julien Tesson and Frédéric Louergue. A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In *International Conference on Computational Science (ICCS)*, pages 36–45, Singapore, 2011. Elsevier. doi:10.1016/j.procs.2011.04.005.

[54] Leslie G. Valiant. A bridging model for parallel computation. *Commun. ACM*, 33(8):103, 1990. doi:10.1145/79173.79181.

[55] Tom White. *Hadoop – The Definitive Guide*. O’Reilly, Sebastopol, CA, USA, fourth edition, 2015.
# A Why3 Session Information

The following pages have been produced using the command `why3 session html` which outputs session information in HTML format. It details the time required for each verification condition. Each time a root verification condition is not verified in time, a transformation is applied such as `split_vc` or `inline_goal` then the verification proceeds with the generated sub-goals.
# Why3 Proof Results for Project "session"

## Theory "average.Average": fully verified

<table><tbody><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>avg_spec_f</td><td>0.09</td><td>---</td></tr><tr><td>avg_spec_Nil</td><td>0.09</td><td>---</td></tr><tr><td>avg_spec_homophic</td><td>0.07</td><td>---</td></tr><tr><td>VC for avg_seq</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>precondition</td><td>0.09</td><td>---</td></tr><tr><td>postcondition</td><td>Timeout (8.00s)</td><td>Timeout (8.00s)</td></tr><tr><td>inline_goal</td><td></td><td></td></tr><tr><td>postcondition</td><td>---</td><td>5.29</td></tr><tr><td>VC for avg_par</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>precondition</td><td>0.09</td><td>---</td></tr><tr><td>precondition</td><td>0.33</td><td>---</td></tr><tr><td>precondition</td><td>Timeout (8.00s)</td><td>Timeout (8.00s)</td></tr><tr><td>inline_goal</td><td></td><td></td></tr><tr><td>precondition</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>precondition</td><td>0.27</td><td>---</td></tr><tr><td>precondition</td><td>0.27</td><td>---</td></tr><tr><td>precondition</td><td>0.07</td><td>---</td></tr><tr><td>precondition</td><td>0.06</td><td>---</td></tr><tr><td>precondition</td><td>0.07</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>0.96</td></tr></tbody></table>

## Theory "bsml_realization.Realization'impl": fully verified

<table><tbody><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>at.least_one�processor</td><td>0.02</td></tr><tr><td>VC for mkpar</td><td>0.02</td></tr><tr><td>VC for apply</td><td>0.02</td></tr><tr><td>VC for proj</td><td>0.02</td></tr><tr><td>VC for put</td><td>0.02</td></tr><tr><td>VC for at.least_oneimbprocessor'lemma'refn</td><td>0.02</td></tr><tr><td>BSML'impl_of.at.least_oneimbprocessor</td><td>0.02</td></tr><tr><td>VC for mkpar'refn</td><td>0.02</td></tr><tr><td>VC for apply'refn</td><td>0.02</td></tr><tr><td>VC for proj'refn</td><td>0.02</td></tr><tr><td>VC for put'refn</td><td>0.02</td></tr></tbody></table>
## Theory "count.Count": fully verified

<table><thead><tr><th>Obligations</th><th>Alt-Ergo 2.5.2</th><th>CVC4 1.8</th></tr></thead><tbody><tr><td>count_spec_f</td><td>0.13</td><td>---</td></tr><tr><td>avg_spec_Nil</td><td>0.06</td><td>---</td></tr><tr><td>count_spec_homomophic</td><td>0.11</td><td>---</td></tr><tr><td>VC for count_seq</td><td>1.61</td><td>---</td></tr><tr><td>VC for count_par</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>precondition</td><td>0.07</td><td>---</td></tr><tr><td>precondition</td><td>0.06</td><td>---</td></tr><tr><td>precondition</td><td>0.16</td><td>---</td></tr><tr><td>precondition</td><td>0.06</td><td>---</td></tr><tr><td>precondition</td><td>0.05</td><td>---</td></tr><tr><td>precondition</td><td>0.06</td><td>---</td></tr><tr><td>postcondition</td><td>1.48</td><td>---</td></tr></tbody></table>

## Theory "mps.MPS": fully verified

<table><thead><tr><th>Obligations</th><th>Alt-Ergo 2.5.2</th><th>CVC4 1.8</th></tr></thead><tbody><tr><td>VC for mps_spec</td><td>0.05</td><td>---</td></tr><tr><td>VC for op</td><td>0.04</td><td>---</td></tr><tr><td>VC for f</td><td>0.04</td><td>---</td></tr><tr><td>op<br>opNeutral</td><td>0.33</td><td>---</td></tr><tr><td>op_neutral</td><td>Timeout (8.00s)</td><td>Timeout (8.00s)</td></tr><tr><td>inline__goal</td><td></td><td></td></tr><tr><td>op_neutral.0</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>op_neutral.0.0</td><td>0.22</td><td>---</td></tr><tr><td>op_neutral.0.1</td><td>0.22</td><td>---</td></tr><tr><td>op_preserves_mps_sum_inv</td><td>0.36</td><td>---</td></tr><tr><td>mps_sum_inv_neutral</td><td>0.05</td><td>---</td></tr><tr><td>f__establishes_mps_sum_inv</td><td>0.06</td><td>---</td></tr><tr><td>VC for<br>maximum__map__plus</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>unreachable point</td><td>0.05</td><td>---</td></tr><tr><td>variant decrease</td><td>0.10</td><td>---</td></tr><tr><td>precondition</td><td>0.08</td><td>---</td></tr><tr><td>postcondition</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>postcondition</td><td>0.13</td><td>---</td></tr><tr><td>postcondition</td><td>0.20</td><td>---</td></tr><tr><td>VC for mps_spec_cons</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>assertion</td><td>0.09</td><td>---</td></tr></tbody></table>
<table><tbody><tr><td>precondition</td><td>0.06</td><td>---</td></tr><tr><td>precondition</td><td>0.13</td><td>---</td></tr><tr><td>postcondition</td><td>Timeout (8.00s)</td><td>Timeout (8.00s)</td></tr><tr><td>inline_goal</td><td></td><td></td></tr><tr><td>postcondition</td><td>Timeout (32.00s)</td><td>Timeout (32.00s)</td></tr><tr><td>split_all_full</td><td></td><td></td></tr><tr><td>postcondition</td><td>---</td><td>39.48</td></tr><tr><td>VC for mps_spec_pos</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>postcondition</td><td>---</td><td>0.66</td></tr><tr><td>postcondition</td><td>0.08</td><td>---</td></tr><tr><td>VC for ms_cons</td><td>0.44</td><td>---</td></tr><tr><td>ms_f</td><td>---</td><td>1.31</td></tr><tr><td>VC for ms_homomorphic</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>assertion</td><td>0.06</td><td>---</td></tr><tr><td>assertion</td><td>1.58</td><td>---</td></tr><tr><td>assertion</td><td>0.10</td><td>---</td></tr><tr><td>assertion</td><td>0.59</td><td>---</td></tr><tr><td>assertion</td><td>0.07</td><td>---</td></tr><tr><td>assertion</td><td>0.05</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>0.58</td></tr><tr><td>VC for mps_seq</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>precondition</td><td>0.13</td><td>---</td></tr><tr><td>assertion</td><td>---</td><td>3.27</td></tr><tr><td>postcondition</td><td>0.06</td><td>---</td></tr><tr><td>VC for mps_par</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>precondition</td><td>0.09</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.05</td><td>---</td></tr><tr><td>precondition</td><td>0.36</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>1.47</td></tr><tr><td>VC for mps_par'</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>precondition</td><td>0.10</td><td>---</td></tr><tr><td>precondition</td><td>0.05</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.05</td><td>---</td></tr><tr><td>precondition</td><td>0.41</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>3.36</td></tr></tbody></table>
## Theory "sequential.Int": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for max</td><td>0.02</td></tr><tr><td>VC for min</td><td>0.02</td></tr></table>

## Theory "sequential.Algebra": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>tail_satisfies_aux</td><td>0.02</td><td>---</td></tr><tr><td>tail_satisfies</td><td>---</td><td>0.12</td></tr><tr><td>tail_satisfies_head</td><td>0.03</td><td>---</td></tr><tr><td>max<br>add</td><td>0.04</td><td>---</td></tr><tr><td>add_neutral</td><td>0.03</td><td>---</td></tr><tr><td>max_add_distr</td><td>0.04</td><td>---</td></tr></table>

## Theory "sequential.ListExtensionality": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for extensionality</td><td>0.07</td></tr></table>

## Theory "sequential.ListAppend": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>app_cons</td><td>0.03</td></tr><tr><td>VC for app_satisfies</td><td>0.05</td></tr><tr><td>appROI</td><td>0.03</td></tr><tr><td>app_neutral</td><td>0.03</td></tr><tr><td>VC for nth_append_left</td><td>0.05</td></tr><tr><td>VC for nth_append_right</td><td>0.06</td></tr></table>

## Theory "sequential.ListInit": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for init_aux</td><td>0.05</td><td>---</td></tr><tr><td>VC for init</td><td>0.03</td><td>---</td></tr><tr><td>VC for from_to</td><td>0.06</td><td>---</td></tr><tr><td>VC for from_toeman</td><td>---</td><td>0.21</td></tr></table>

## Theory "sequential.ListRev": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for rev_aux</td><td>0.05</td></tr></table>
<table><tr><td>VC for rev</td><td>0.03</td></tr></table>

## Theory "sequential.ListMap": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for map</td><td>0.05</td></tr><tr><td>VC for map_ext</td><td>0.04</td></tr><tr><td>VC for map_map</td><td>0.05</td></tr><tr><td>VC for map_app</td><td>0.04</td></tr><tr><td>map_cons</td><td>0.03</td></tr></table>

## Theory "sequential.ListMapAlg": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for map_ext_inv</td><td>0.05</td></tr></table>

## Theory "sequential.ListTailRecMap": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for map_aux</td><td>0.47</td></tr><tr><td>VC for map'</td><td>0.05</td></tr><tr><td>map'_map</td><td>0.04</td></tr></table>

## Theory "sequential.ListMap2": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for map2</td><td>0.10</td></tr></table>

## Theory "sequential.ListMap3": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for map3</td><td>0.28</td></tr></table>

## Theory "sequential.ListFold": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for fold_left</td><td>0.03</td><td>---</td></tr><tr><td>VC for fold_left_app</td><td>0.04</td><td>---</td></tr><tr><td>VC for fold_left_map_r</td><td></td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td>Timeout (2.00s)</td></tr><tr><td>postcondition</td><td>0.04</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>0.68</td></tr></table>
## Theory "sequential.ListFoldMonoid": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for fold_left_inv</td><td>0.05</td></tr><tr><td>VC for fold_left_preserves</td><td>0.03</td></tr><tr><td>VC for fold_leftProp</td><td>0.06</td></tr><tr><td>VC for fold_left_appProp</td><td>0.04</td></tr></table>

## Theory "sequential.ListFlatten": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for flatten_cons</td><td>0.09</td></tr><tr><td>VC for flatten_map</td><td>0.04</td></tr><tr><td>VC for flatten_app</td><td>0.05</td></tr><tr><td>flatten.fequal</td><td>0.03</td></tr></table>

## Theory "sequential.ListFlattenAlg": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for flatten_satisfies</td><td>0.06</td><td>---</td></tr><tr><td>VC for fold_left_flatten</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.06</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>precondition</td><td>0.38</td><td>---</td></tr><tr><td>precondition</td><td>0.04</td><td>---</td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>postcondition</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>postcondition</td><td>0.03</td><td>---</td></tr><tr><td>postcondition</td><td>0.15</td><td>---</td></tr></table>

## Theory "sequential.ListSum": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for sum_cons</td><td>0.05</td></tr></table>
## Theory "sequential.ListMaximum": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for maximum</td><td>0.04</td><td>---</td></tr><tr><td>maximum_cons</td><td>---</td><td>0.40</td></tr></table>

## Theory "sequential.ListFirstHomomorphismTheorem": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for fold_left_homomorphic</td><td>1.59</td><td>---</td></tr><tr><td>VC for first_homomorphism_theorem</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>precondition</td><td>0.03</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>1.71</td></tr></table>

## Theory "sequential.ListFirstnSkipn": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for cut</td><td>0.17</td></tr><tr><td>VC for firstn</td><td>0.05</td></tr><tr><td>VC for skipn</td><td>0.05</td></tr><tr><td>VC for firstn_skipn</td><td>0.04</td></tr><tr><td>VC for skipn_skipn</td><td>0.08</td></tr><tr><td>VC for take</td><td>0.12</td></tr></table>

## Theory "sequential.ListPrefix": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for prefix</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>variant decrease</td><td>0.03</td><td>---</td></tr><tr><td>postcondition</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>postcondition</td><td>0.03</td><td>---</td></tr><tr><td>postcondition</td><td>0.14</td><td>---</td></tr><tr><td>postcondition</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vc</td><td></td><td></td></tr><tr><td>postcondition</td><td>0.03</td><td>---</td></tr><tr><td>postcondition</td><td>0.03</td><td>---</td></tr><tr><td>prefix_cons</td><td>0.76</td><td>---</td></tr></table>
<table><tr><td>VC for prefix_map</td><td>0.25</td><td>---</td></tr><tr><td>VC for prefix_satisfies</td><td>0.04</td><td>---</td></tr></table>

## Theory "sequential.ListFilter": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for filter_append</td><td>0.05</td></tr></table>

## Theory "sequential.ListZip": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for zip_length</td><td>0.43</td><td>---</td></tr><tr><td>VC for zip_map2</td><td>---</td><td>0.68</td></tr><tr><td>zip_nth</td><td>0.03</td><td>---</td></tr></table>

## Theory "skeletons.Skeletons": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>VC for map_par</td><td style="background-color: #f9c63d;">Timeout (2.00s)</td><td style="background-color: #f9c63d;">Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>postcondition</td><td>0.06</td><td>---</td></tr><tr><td>postcondition</td><td>1.57</td><td>---</td></tr><tr><td>VC for reduce_par</td><td style="background-color: #f9c63d;">Timeout (2.00s)</td><td style="background-color: #f9c63d;">Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>assertion</td><td>0.26</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>2.82</td></tr><tr><td>VC for mapreduce_par</td><td style="background-color: #f9c63d;">Timeout (2.00s)</td><td style="background-color: #f9c63d;">Timeout (2.00s)</td></tr><tr><td>split_vm</td><td></td><td></td></tr><tr><td>assertion</td><td>11.42</td><td>---</td></tr><tr><td>assertion</td><td>---</td><td>6.15</td></tr><tr><td>assertion</td><td>---</td><td>2.11</td></tr><tr><td>postcondition</td><td>---</td><td>6.48</td></tr></table>

## Theory "stdlib.Base": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td></tr><tr><td>VC for procs</td><td>0.04</td></tr><tr><td>procs_spec_nth</td><td>0.05</td></tr><tr><td>procs_spec_length</td><td>0.05</td></tr><tr><td>VC for this</td><td>0.04</td></tr><tr><td>this_spec</td><td>0.05</td></tr><tr><td>VC for replicate</td><td>0.06</td></tr><tr><td>VC for parfun</td><td>0.05</td></tr></table>
<table><tr><td>VC for parfun2</td><td>0.05</td></tr><tr><td>VC for parfun3</td><td>0.05</td></tr><tr><td>VC for list_of_par</td><td>0.10</td></tr><tr><td>VC for apply2</td><td>0.05</td></tr><tr><td>VC for applyif</td><td>0.12</td></tr><tr><td>VC for applyat</td><td>0.04</td></tr><tr><td>VC for mask</td><td>0.12</td></tr></table>

Theory "stdlib.Comm": fully verified

<table><tr><td>Obligations</td><td>Alt-Ergo 2.5.2</td><td>CVC4 1.8</td></tr><tr><td>shift_pid_lt</td><td>0.05</td><td>---</td></tr><tr><td>shift_pid_ge</td><td>0.05</td><td>---</td></tr><tr><td>shift_id</td><td>0.05</td><td>---</td></tr><tr><td>VC for shift</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>postcondition</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>postcondition</td><td>0.04</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>5.38</td></tr><tr><td>postcondition</td><td>0.04</td><td>---</td></tr><tr><td>VC for shift_right</td><td>0.11</td><td>---</td></tr><tr><td>VC for shift_left</td><td>0.11</td><td>---</td></tr><tr><td>VC for totex</td><td>0.10</td><td>---</td></tr><tr><td>VC for totalExchange</td><td>1.51</td><td>---</td></tr><tr><td>VC for bcast proj</td><td>0.05</td><td>---</td></tr><tr><td>VC for bcast direct</td><td>---</td><td>0.94</td></tr><tr><td>VC for gather</td><td>1.30</td><td>---</td></tr><tr><td>VC for gather_list</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>precondition</td><td>0.05</td><td>---</td></tr><tr><td>postcondition</td><td>---</td><td>3.72</td></tr><tr><td>postcondition</td><td>---</td><td>2.20</td></tr><tr><td>VC for scatter</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>split_vm</td><td>Timeout (2.00s)</td><td>Timeout (2.00s)</td></tr><tr><td>postcondition</td><td>---</td><td>14.45</td></tr><tr><td>postcondition</td><td>0.04</td><td>---</td></tr></table>