Ralph Matthes

Celia Picard

Verification of redecoration for infinite triangular matrices using coinduction

Keywords: nested datatype, coinduction, theorem proving, Coq

Finite triangular matrices with a dedicated type for the diagonal elements can be profitably represented by a nested data type, i. e., a heterogeneous family of inductive data types, while infinite triangular matrices form an example of a nested coinductive type, which is a heterogeneous family of coinductive data types.

Redecoration for infinite triangular matrices is taken up from previous work involving the first author, and it is shown that redecoration forms a comonad with respect to bisimilarity.

The main result, however, is a validation of the original algorithm against a model based on infinite streams of infinite streams. The two formulations are even provably equivalent, and the second is identified as a special instance of the generic cobind operation resulting from the well-known comultiplication operation on streams that creates the stream of successive tails of a given stream. Thus, perhaps surprisingly, the verification of redecoration is easier for infinite triangular matrices than for their finite counterpart.

All the results have been obtained and are fully formalized in the current version of the Coq theorem proving environment where these coinductive datatypes are fully supported since the version 8.1, released in 2007. Nonetheless, instead of displaying the Coq development, we have chosen to write the paper in standard mathematical and type-theoretic language. Thus, it should be accessible without any specific knowledge about Coq.

Introduction

Redecoration for the finite triangles has been verified against a list-based model in previous work [START_REF] Matthes | Verification of the redecoration algorithm for triangular matrices[END_REF]. This is the point of departure for our present paper.

Finite triangles can be represented by "triangular matrices", i. e., finite square matrices, where the part below the diagonal has been cut off. Equivalently, one may see them as symmetric matrices where the redundant information below the diagonal has been omitted. The elements on the diagonal play a different role than the other elements in many mathematical applications, e. g., one might require that the diagonal elements are invertible (non-zero). This is modeled as follows: a type E of elements outside the diagonal is fixed throughout (we won't mention it as parameter of any of our definitions), and there is a type of diagonal elements that enters all definitions as an explicit parameter. More technically, if A is the type of diagonal elements, then Tri fin A shall denote the type of finite triangular matrices with A's on the diagonal and E's outside (see Figure 1). Then, Tri fin becomes a family of types, indexed over all types, hence a type transformation. Moreover, the different Tri fin A are inductive datatypes that are all defined simultaneously, hence they are an "inductive family of types" or "nested datatype" [START_REF] Bird | Nested datatypes[END_REF]. If we cut the triangle into the first column and the rest, we get one element of A and a "trapezium", with an uppermost row solely consisting of E's. In order not to have to ensure explicitly by a dependent type that the number of columns is coherent, the solution is to transform the trapezium into a triangle, integrating the side diagonal (just above the diagonal) into the diagonal itself, as shown in Figure 2. From the left to the right, the lowermost element of E in each column is paired with the element of A on the diagonal, and the other elements of E remain untouched.

E E E E E E A A A A . . .

E E E E E E

A A A A E E E E . . . E E E E E E E × A E × A E × A E × A . .

. triangle trapezium

Following this remark, the triangles can be defined theoretically [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF], and in Coq and Isabelle by the following constructors [START_REF] Matthes | Verification of the redecoration algorithm for triangular matrices[END_REF]: a : A sg fin a : Tri fin A a : A t : Tri fin (E × A) constr fin a t : Tri fin A ◮ Remark. In this paper, single-lined inference rules denote inductive definitions, double-lined inference rules are for coinductive definitions.

In more theoretical terms, Tri fin is modeled as the least solution to the fixed-point equation

Tri fin A = A + A × Tri fin (E × A)
The left summand corresponds to a triangle that only consists of a single element of A (a singleton), thus ensuring the base case. The algorithm of redecoration (see work by Uustalu and Vene for the general categorical notion [START_REF] Uustalu | The dual of substitution is redecoration[END_REF]) is the following: for a given redecoration rule f : Tri fin A → B, it is a function redec f that redecorates A-triangles t (elements of Tri fin A) into B-triangles by applying f to the whole triangle t to obtain the new top element, and then by successively applying the same operation to the triangle cut out from the remaining trapezium. This ends in the singleton case where f is applied to it and the result is turned into a triangle by applying sg fin . This algorithm only changes the diagonal elements in A into elements of B, as shown in Figure 3. We do not give the formal definition of redecoration for finite triangles here.

E E E E E E

A A A A . . . E E E E E E B B B B . . . f Figure 3 Redecoration
The redecoration for infinite triangles [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF] has not yet been verified. This is what we intend to do in this paper.

Reasoning about nested coinductive types naturally rests on observational equality, just as for ordinary coinductive types, and since version 8.2, Coq greatly helps in using the rewrite mechanism for Leibniz equality also for the notion of bisimilarity of infinite triangular matrices. With respect to that notion of equality, redecoration is shown to form a (sligthly weakened form of) comonad, and its implementation is compared with an alternative one based on streams of streams.

These new results come with a full formalization in Coq [START_REF] Matthes | Formalization in Coq for this article[END_REF], and limitations of what Coq recognizes as a guarded definition make the theoretical development more challenging, but we still obtained smooth results without an excessive overhead that would be imposed by a naive dualization of the formalization for the finite triangles [START_REF] Matthes | Verification of the redecoration algorithm for triangular matrices[END_REF].

In Section 2, inspired by the previous theoretical development [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF], we introduce the dual to the definition of finite triangles [START_REF] Matthes | Verification of the redecoration algorithm for triangular matrices[END_REF]. We present it with all the tools necessary to define redecoration. We then propose a definition for the redecoration algorithm on these infinite triangles and add further tools and properties. In Section 3, we change the point of view in the observation of the triangles. We give an alternative definition for the infinite triangles, considering this new approach, and provide various tools. We also show that this new representation is equivalent to the previous one. Finally, we propose two ways of defining redecoration, trying always to simplify and generalize our definitions and show their adequation with previous definitions.

Since the results are fully formalized in the current version of Coq, hence ensuring complete and sound proofs, we took the liberty to write the paper in standard mathematical and type-theoretic language and also to omit most proofs. Therefore, it should be accessible without any specific knowledge about Coq. For the study of the development [START_REF] Matthes | Formalization in Coq for this article[END_REF], the Coq'Art book [START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF] should mostly suffice, but the (type) class mechanism [START_REF] Sozeau | First-class type classes[END_REF] and the revised setoid rewriting mechanism based on it have to be consulted elsewhere -by default in the Coq Reference Manual [START_REF] Tahar | The Coq Proof Assistant Reference Manual[END_REF].

Reference Representation with a Coinductive Family

Dually to the representation of finite triangles discussed in the introduction, "triangular matrices" are now introduced as infinite square matrices, where the part below the diagonal has been cut off. Recall that a type E of elements outside the diagonal is fixed throughout.

If A is the type of diagonal elements, then Tri A shall denote the type of infinite triangular matrices with A's on the diagonal and E's outside. The different Tri A are coinductive datatypes that are all defined simultaneously, as was the case for Tri fin , hence they are a "coinductive family of types" or "nested codatatype", as will be developed below.

Infinite triangles as nested coinductive type

Infinite triangles can also be visualized as in Figure 1, this time with the dots representing an infinite extension.

If we now cut the triangle into the first column and the rest, we get one element of A (as before for Tri fin ) and a trapezium, with an uppermost row consisting of infinitely many E's.

The n-th column consists of an element of A on the diagonal and n elements of E above the diagonal, as in the case of Tri fin . As before, we do not want to parameterize the type of the columns by their index and instead integrate the side diagonal into the diagonal -and this has to be done corecursively [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF]. This integration is possible since trapeziums are again in one-to-one correspondence to triangles, as shown in Figure 2, now interpreted infinitely. In this figure, the trapezium to the left is considered as the "trapezium view" of the triangle to the right. Vice versa, the triangle to the right is the "triangle view" of the trapezium to the left.

We now formalize triangles through the following constructor that has to be interpreted coinductively.

◮ Definition 1 (Tri, defined coinductively).

a : A t : Tri(E × A) constr a t : Tri A with A a type variable.
This means that the types Tri A for all types A are simultaneously conceived as greatest solution to the fixed-point equation

T ri A = A × Tri(E × A),
and constr has two arguments instead of a pair of type A × Tri(E × A) just for technical convenience.

The second argument to constr corresponds to the triangle view of the trapezium in our visualization in Figure 1, but there is no passage between a trapezium and a triangle -this is only the motivation. In the formalization, there are only infinite triangles, but we set Trap A := Tri(E × A) to hint to the trapezium view of these triangles.

◮ Definition 2 (Projections).

top : ∀A. Tri A → A rest : ∀A. Tri A → Trap A top (constr a r) := a rest (constr a r) := r
This definition by pattern matching implicitly uses the direction from right to left in the above fixed-point equation. Thus, the top element and the trapezium part of a triangle are calculated by unfolding the fixed point.

In order to obtain the triangle that arises by cutting off the top row of a trapezium, we have to go through all the columns. ◮ Definition 3 (cut : ∀A.Trap A → Tri A, defined corecursively).

cut (constr e, a r) := constr a (cut r)

The definition does pattern matching on elements of Trap A and constructs an element of the coinductive type Tri A. The subterm cut r represents a corecursive call to cut, which is accepted also by the Coq system as admissible corecursion since it is placed directly as an argument to the constructor constr.

Redecoration for infinite triangles

We are heading for a corecursive definition of the generic redecoration operation redec on triangles. It has type ∀A∀B.

(Tri A → B) → Tri A → Tri B,
which is the type of a coextension operation for Tri viewed as support of a comonad. Coextension -also called cobind -is the dual of the extension / bind operation of a monad, which is so successfully used in the functional programming language Haskell. The counit for the comonad we are about to construct is our top operation. Redecoration for Tri follows the same pattern as for Tri fin , but the successive applications of the same operation will never reach a base case, as there is none in Tri.

Formally, this is done by a corecursive definition, where redec f t for t of type Tri A has to call itself with second argument of type Trap A, hence f is not even type-correct as a first argument in that corecursive call. Instead of f :

Tri A → B, a "lifted" version of f is needed that has type Tri(E × A) → E × B. ◮ Definition 4 (lift : ∀A∀B. (Tri A → B) → Tri(E × A) → E × B). lift f r := fst(top r), f (cut r) ,
where fst is the first projection (from a pair to its first component).

The definition is illustrated in Figure 4.

E E E E E E A A A . . . E × B id f Figure 4 Definition of lifting
The formal definition of redecoration is as follows:

◮ Definition 5 (redec : ∀A∀B. (Tri A → B) → Tri A → Tri B, defined corecursively). redec f t := constr (f t) redec (lift f ) (rest t) ,
see Figure 5. This definition is accepted since it is guarded: the corecursive call to redec is as second argument to constr, and it does not matter that the argument f becomes lift f there. A function argument that becomes more complicated in the recursive call is typical of recursion on nested datatypes, see, e. g., [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF]. This completes the definition, but leaves open the question if this is really (in what sense) the cobind of a comonad and if it corresponds to operations that are easier to understand than corecursion on nested codatatypes. We note that recursion schemes for nested datatypes have been subject of a long line of research, starting from work by Bird and colleagues [START_REF] Bird | Nested datatypes[END_REF][START_REF] Bird | Generalised folds for nested datatypes[END_REF].

Properties of redecoration

It is well-known that propositional equality = (called Leibniz equality in Coq since t 1 = t 2 allows the replacement of t 1 by t 2 in any mathematical context) cannot suffice as criterion for the correctness of elements that are calculated in coinductive types. Propositional equality cannot be established by coinductive reasoning because this is confined to coinductively defined conclusions, and propositional equality is not coinductive (in Coq, it is defined inductively). We write Rel C for the type of the binary relations on C, and we use these relations in infix notation. In Coq, their type is C → C → Prop, where Prop is the universe of propositions.

E E E E E E A A A A . . . E E E E E E B B B B . . . f redec (lift f )
◮ Definition 6 (≃ : ∀A. Rel(Tri A), defined coinductively).

t 1 , t 2 : Tri A top t 1 = top t 2 rest t 1 ≃ rest t 2 t 1 ≃ t 2
It is easy to show that ≃ is an equivalence relation for any argument type A. It is an equivalence relation but not a congruence: for every operation of interest we have to establish compatibility with bisimilarity. This is in particular easily done for the projection functions top and rest and for the cut operation.

Using this notion of bisimilarity, we can show that redec is extensional in its function argument (modulo ≃), using full extensionality of lift:

◮ Lemma 7. ∀A∀B∀(f f ′ : Tri A → B). (∀t, f t = f ′ t) ⇒ ∀t, lift f t = lift f ′ t ◮ Lemma 8. ∀A∀B∀(f f ′ : Tri A → B). (∀t, f t = f ′ t) ⇒ ∀t, redec f t ≃ redec f ′ t
The main properties of redec we are interested in express that top and redec together constitute a comonad for "functor" Tri. The precise categorical definition in coextension form (with a cobind operation instead of the traditional comultiplication) is, e. g., given in [START_REF] Uustalu | The dual of substitution is redecoration[END_REF]. Here, we give the constructive notion we use in this paper, and it is parameterized by an equivalence relation while classically, only mathematical equality = is employed.

◮ Definition 9 (Constructive comonad). A constructive comonad consists of a type transforma- tion T , a function counit : ∀A. T A → A, a function cobind : ∀A∀B.(T A → B) → T A → T B
and an equivalence relation ≅ : ∀A. Rel(T A) such that the following comonad laws hold:

∀A∀B∀f T A→B ∀t T A . counit(cobind f t) = f t (1) ∀A∀t T A . cobind counit A t ≅ t (2) ∀A∀B∀f T A→B ∀g T B→C ∀t T A . cobind (g • cobind f ) t ≅ cobind g (cobind f t) (3)
Here, in order to save space, we gave the type information for the term variables as superscripts.

The index A to counit is meant to say that the type parameter to counit is set to A -in all other cases, we leave type instantiation implicit.

◮ Definition 10 (Constructive weak comonad). A constructive weak comonad is defined as a constructive comonad, but where the equation in ( 3) is restricted to functions g that are compatible with ≅ in the following sense: ∀t t ′ , t ≅ t ′ ⇒ g t = g t ′ .

◮ Lemma 11. The type transformation Tri, the projection function top and redec form a constructive weak comonad with respect to ≃.

The first comonad law is satisfied in an especially strong form: top(redec f t) actually is f t by definition. The other comonad laws go through with suitable generalizations of the lemmas -in order to ensure guardedess of the proofs. The current solution is unspectacular, but it was not obvious how to do it (much more complicated solutions were found on the way and are now obsolete). We only show the strengthening of the second comonad law, but it is the same style for the third one.

◮ Lemma 12 (strengthened form of second comonad law for redec).

∀A∀(f : Tri

A → A). (∀(t : Tri A), f t = top t) ⇒ ∀(t : Tri A). redec f t ≃ t
The proof is by coinduction and uses Lemma 7. Obviously, this implies the second comonad law. For all the details, see our formalization in Coq [START_REF] Matthes | Formalization in Coq for this article[END_REF]. We only get a weak comonad because proving pointwise equality of lift(g • (redec f )) and (lift g) • (redec(lift f )) requires compatibility of g with ≃, and this is a crucial step for proving the third comonad law.

When defining the cut operation, one might naturally want to get also the part that has been cut out (the elements of E). These elements are given by the following function: Using es_cut, we can define the first row of E elements in a triangle as

◮ Definition 13 (es_cut : ∀A. Trap A → Str E, defined corecursively).
frow : ∀A. Tri A → Str E frow t := es_cut (rest t)
Once we have these definitions, we might want to be able to "glue" the two cut parts in order to recreate the original trapezium. This is done by the function addes

◮ Definition 14 (addes : ∀A. Str E → Tri A → Trap A, defined corecursively).
addes (e :: es) (constr a r) := constr e, a (addes es r)

And it is then easy to show that addes indeed performs the gluing:

∀A∀(r : Trap A). addes (es_cut r) (cut r) ≃ r

Another Conception of Triangles

In this section, we show another way to perceive and represent infinite triangles. And we propose two ways of defining redecoration on this new representation.

A new definition using streams

In the previous section, we always visualized the infinite triangles by their columns. Indeed, we said that a triangle was a first column with only one element of type A (the element of the diagonal) and a trapezium, itself actually a triangle, as suggested in Figure 1.

While elements of the finite triangles in Tri fin A (see Section 1) are (globally) finite, also all the columns of our infinite triangles in Tri A are finite. In the work that we started from for this article [START_REF] Matthes | Verification of the redecoration algorithm for triangular matrices[END_REF], redecoration on Tri fin is verified against a model where triangles are represented by finite lists of columns, where each column consists of the diagonal element in A and a finite list of elements in E. A naive dualization of that approach would consist in taking as representation of infinite triangles streams of columns that would be formed as for the finite ones. This mixture of inductive and coinductive datatypes is notoriously difficult to handle. We have been confronted with this problem many times in the last few years, as can be seen in the second author's thesis [START_REF] Picard | Représentation coinductive des graphes[END_REF] which deals with this kind of problems particularly in Coq. But in other proof assistants, the same kind of issues has appeared; there is also an experimental solution in Agda [START_REF] Anders | Beating the productivity checker using embedded languages[END_REF][START_REF] Anders | Subtyping, declaratively[END_REF]. Still, the representation of infinite triangles mixing inductive and coinductive datatypes can be carried out, but we refrain from presenting this column-based approach here.

However, we can also visualize triangles the other way around. We now consider the triangle by its rows, as suggested in Figure 6. Then, on any row, we have one element of Here, nothing is finite (only the single element of A at the head of each row, but this is not a problem), therefore, we do not have any embedded inductive type in our descriptionunlike in the columnwise decomposition mentioned above. This new visualization can be represented as a stream of pairs made of one element of type A and a stream of elements of type E.

E E E E E E A A A A . . .

◮ Definition 15. Tri

′ A := Str(A × Str E)
Actually, following the definition of Str, we can read this new definition of the triangles as consisting of three parts: the top element, the stream of elements of E of the first row and the triangle corresponding to the rest, as shown in Figure 7. We define functions that allow us to access to each of these elements: Notice that rest and rest ′ are conceptually different -the former yields the trapeziums after cutting off the first column, the latter triangles after cutting off the first row.

E E E E E E

A A A A . . . top ′ frow ′ rest ′
◮ Definition 16 (Projections). top ′ : ∀A. Tri ′ A → A frow ′ : ∀A. Tri ′ A → Str E rest ′ : ∀A. Tri ′ A → Tri ′ A top ′ (
To compare two elements of Tri ′ , we need a notion of bisimilarity, which on Str is pre-defined in Coq as follows:

◮ Definition 17 (≡ : ∀C. Rel(Str C), defined coinductively).

s 1 , s 2 : Str C hd s 1 = hd s 2 tl s 1 ≡ tl s 2 s 1 ≡ s 2
However, we cannot use it directly. Indeed, we would need to prove, for two triangles t 1 and t 2 that their first rows are Leibniz-equal, i. e., frow ′ t 1 = frow ′ t 2 . This is too strict, since the rows are defined partially coinductively (because of the stream of E's). Therefore, we need to define a new relation on Tri ′ that will compare the three elements of the triangles. The tops can be compared through Leibniz equality, the first rows can be compared using ≡ and the rests with the relation on Tri ′ , corecursively.

◮ Definition 18 ( ∼ = : ∀A. Rel(Tri ′ A), defined coinductively).

t 1 , t 2 : Tri ′ A top ′ t 1 = top ′ t 2 frow ′ t 1 ≡ frow ′ t 2 rest ′ t 1 ∼ = rest ′ t 2 t 1 ∼ = t 2
It is immediate to show that ∼ = is an equivalence relation.

In order to validate this view of the triangles, we want to show that it is indeed equivalent to the original one. Therefore, we are going to show that there is a bijection between the two definitions (modulo pointwise bisimilarity). To do so we define two conversion functions (toStreamRep, from Tri to Tri ′ and fromStreamRep for the other way around) and show that their compositions are pointwise bisimilar to the identity.

The two conversion functions are quite natural. To transform an element of Tri A into an element of Tri ′ A, we need to reconstruct from the original triangle the three elements of Tri ′ A. The top remains the original top, this is trivial. The first row of elements of E is given by frow. Finally, the triangle has to be transformed again by toStreamRep from the rest of the triangle with the first row cut out by the function cut. The calculation for the different parts is represented in Figure 8. The definition of fromStreamRep is also quite intuitive. We have to construct the two elements that compose elements of type Tri. The top remains the top as before, this is again trivial. For the rest, we have to "glue" the first row to the rest of the triangle (basically the inverse of the cut and es_cut functions on Tri ′ ) before transforming it again. We call addes ′ the function that performs this operation, as shown in Figure 9.

E E E E E E

E E E E E E A A A A E E E E . . . E E E E E E E × A E × A E × A E × A . . . addes ′ Figure 9 Definition of addes ′ ◮ Definition 20 (addes ′ : ∀A. Str E → Tri ′ A → Tri ′ (E × A), defined corecursively).
addes ′ (e :: es) t := e, top ′ t , es ::

addes ′ (frow ′ t) (rest ′ t) ◮ Definition 21 (fromStreamRep : ∀A. Tri ′ A → Tri A, defined corecursively). fromStreamRep t := constr (top ′ t) fromStreamRep (addes ′ (frow ′ t) (rest ′ t))
◮ Remark. Our first idea was to do the gluing after the transformation. Indeed, as the transformation does not affect the elements of E, it seemed more natural to us not to submit this part to the corecursive call of the transformation. Thus, we wanted to define fromStreamRep coinductively as follows:

fromStreamRep t := constr (top ′ t) (addes (frow ′ t) (fromStreamRep (rest ′ t)))
However, even if this seems harmless, this definition cannot be accepted by Coq since the corecursive call to fromStreamRep is not guarded (it is an argument of addes and not of a constructor). Nevertheless, we have shown that the solution to the previous equation is unique with respect to pointwise bisimilarity and that fromStreamRep of Definition 21 satisfies it.

◮ Lemma 22. ∀A∀(t : Tri

′ A). toStreamRep (fromStreamRep t) ∼ = t
Proof. To prove this result, we actually prove the following stronger result that we then only instantiate to finish the proof:

∀A∀(t : Tri ′ A)(u : Tri A), toStreamRep (fromStreamRep t) ∼ = u ⇒ t ∼ = u
The proof of this statement is a simple coinduction, that uses some straightforward results on cut and addes ′ . ◭ ◮ Lemma 23. ∀A∀(t : Tri A). fromStreamRep (toStreamRep t) ≃ t Proof. We use the same technique as before. We prove a stronger result that we instiantiate to prove our lemma:

∀A∀(t : Tri A)(u : Tri ′ A). fromStreamRep (toStreamRep t) ≃ u ⇒ t ≃ u
Here again, the proof is a straightforward coinduction using compatibility of top and rest with ≃ and a simple result on addes ′ . ◭

Redecoration on Tri ′

Thus, we have a completely different view of the triangles, but still, it is fully equivalent to the original one. The interest of this view is that now the redecoration is very easy to perform. Indeed, before, the tricky part was that we had to lift the function f to trapeziums, and therefore to cut out the elements of E remaining (implicitly) from the first row. The problem was that we roughly had to cut out a row, while we were reasoning on columns.

Here, as we directly reason on rows, it is much easier. As shown in Figure 10, the three elements of the transformed triangle will be: the top is the application of f to the whole triangle (as before) the first row of elements of E is the same row as in the original triangle (and as we said we have direct access to it) the rest of the triangle is the application of the redecoration function to the rest ◮ Definition 24 (redec ′ : ∀A∀B.

E E E E E E A A A A . . . E E E E E E B B B B . . . f redec ′ f id
(Tri ′ A → B) → Tri ′ A → Tri ′ B, defined corecursively). redec ′ f t := f t, frow ′ t :: redec ′ f (rest ′ t)
We can finally show that this new version of the redecoration is equivalent to the previous one, modulo compatibility, using the conversion functions. We show that:

◮ Lemma 25. ∀f, (∀t t ′ , t ∼ = t ′ ⇒ f t = f t ′ ) ⇒ ∀t, redec ′ f t ∼ = toStreamRep (redec (f • toStreamRep) (fromStreamRep t)) ◮ Lemma 26. ∀f, (∀t t ′ , t ≃ t ′ ⇒ f t = f t ′ ) ⇒ ∀t, redec f t ≃ fromStreamRep (redec ′ (f • fromStreamRep) (toStreamRep t))
◮ Remark. The compatibility hypotheses here are needed to work with Tri. Up to these extra requirements, the two conversion functions yield an isomorphism of comonads (the associated properties for top and top ′ are immediate by definition).

Simplifying redecoration again

As the representation of infinite triangles Tri ′ is only as a stream of streams, we can use standard functions on streams to define redecoration. Indeed, redecoration can be interpreted as consisting of applying a function to each element of the diagonal of an infinite triangle, where each element of the diagonal is itself a triangle (iterated tails of the given triangle).

We can thus decompose the redecoration operation into two steps: first transform the infinite triangle into a triangle of triangles and then apply the transformation function on the elements of the diagonal, as shown in Figure 11. These two steps are then trivial to define on streams. Indeed, the first step consists of replacing all the elements of A by the corresponding iterated tail of the triangle itself. In fact, the information about the elements of E is redundant. Indeed, it is contained in the terms of the diagonal themselves (the row of elements of E "to the right" of an element of the diagonal is the first row of this element, minus the element of A). Therefore, we can omit them and only concentrate on the triangles. Thus, we need to obtain the stream of all the iterated tails of the initial triangle (see the first part of Figure 12). This is given by the classical tails operation defined below:

E E E E E E A A A A . . . E E E E E E E A A A A . . . E E E A A A . . . E E E E E E A A . . . A . . . . . . E E E E E E B B B B . . . 1 st step 2 nd step
◮ Definition 27 (tails : ∀C. Str C → Str(Str C), viewed coinductively). tails s := s :: tails(tl s)

◮ Remark. The function tails has the signature of the comultiplication operation in a comonad based on Str according to the classical definition of comonads [START_REF] Mac | Categories for the Working Mathematician[END_REF] (the term "comultiplication" is not used there, but only the letter δ that is dual to the multiplication of a monad). See Lemma 32 below for the constructive comonad based on Str.

In Figure 11, the second step only consists of applying f to all the elements of the diagonal.

In fact, the first step corresponds to transforming t of type Tri ′ A into map λx. x, frow ′ x (tails t) , and the second one consists in transforming s of type Tri ′ (Tri ′ A) into map λ u, es . f u, es s .

We can alternatively see the transformation of t into tails t as the first step, and the two successive map operations as the second step, which is therefore (by applying the functor law for map saying that map's compose) performed by map (lift ′ f ), with lift ′ defined as follows:

◮ Definition 28 (lift ′ : ∀A∀B. (Tri ′ A → B) → Tri ′ A → B × Str E). lift ′ f := λx. f x, frow ′ x
As for rest and rest ′ , lift and lift ′ are unrelated and belong to the respective point of view. This new version of the redecoration operation is shown in Figure 12.

E E E E E E

A A A A . . . E A A A A . . . ; E E E A A A . . . ; E E E E E E A A . . .
◮ Definition 29 (redec ′ alt : ∀A∀B. (Tri ′ A → B) → Tri ′ A → Tri ′ B). redec ′ alt f t := map (lift ′ f ) (tails t)
One can then easily show that this operation is equivalent to the previous one:

◮ Lemma 30. ∀A∀B∀(f : Tri ′ A → B)∀(t : Tri ′ A). redec ′ f t ≡ redec ′ alt f t
The proof is a straightforward coinduction.

It is interesting to note that here, we do not need the bisimulation relation defined on Tri ′ . We can directly use the standard relation on Str, ≡. This should not be surprising. Indeed, here we only really manipulate streams. Those streams are made of pairs and we only manipulate the finite part of each pair (the first element). The second one is only a copy. Therefore the relation ∼ = would be artificial here.

Let's continue abstracting and define redec ′ gen as follows:

◮ Definition 31 (redec ′ gen : ∀A∀B.

(Str A → B) → Str A → Str B).
redec ′ gen f s := map f (tails s)

As we remarked previously, tails has the signature of a comultiplication for a comonad (in the triple format [START_REF] Mac | Categories for the Working Mathematician[END_REF]) based on Str, and it is well known that map is the functor (on morphisms) for Str. Therefore, redec ′ gen becomes the cobind operation of this comonad, generically. We do not develop this piece of constructive category theory here, but only state the result for this instance: ◮ Lemma 32. The type transformation Str, the projection function hd and redec ′ gen form a constructive comonad with respect to ≡. This section is inspired by Adriano [START_REF] Adriano | Answer to Markus Schnell's message slide: useful function? Haskell Mailing List[END_REF] who suggested a redecoration function for Haskell lists just in this form. More precisely, a function slide :: (

[a] -> b) -> [a] -> [b]
was defined by slide f = map f.tails. Note that Haskell lists can be finite and infinite, thus this definition captured streams as well.

The function redec ′ alt is an instance of redec ′ gen , i. e., the following lemma is trivial:

◮ Lemma 33. ∀A∀B∀(f : Tri ′ A → B)(t : Tri ′ A). redec ′ alt f t = redec ′ gen (lift ′ f ) t
Therefore, it is natural to show the three laws of comonads for redec ′ alt and the proofs are much simplified by the use of redec ′ gen . In particular, we can show a kind of commutativity of lift ′ with redec ′ alt .

◮ Lemma 34. The type transformation Tri ′ , the projection function top ′ and redec ′ alt form a constructive comonad with respect to ≡ (more precisely, the equivalence relation is ≡ A×Str E for every A).

◮ Remark. Through the functions toStreamRep and fromStreamRep, one can then transfer this comonad structure back to Tri. Since Lemma 25 and Lemma 26 require compatibility of f with bisimilarity, this will not even give a constructive weak comonad, but the first and third law have to be relativized to compatible f 's as well. Still, this does not seem a problematic constraint. Anyway, Lemma 11 has been proved independently of streams.

Conclusion

In this paper we have presented various verifications of the redecoration algorithm for infinite triangles. We have first dualized directly the representation for finite triangles by a nested inductive datatype to obtain a nested coinductive datatype. In both cases, the triangles are visualized by their columns. We have implemented the corresponding redecoration algorithm redec (already available [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF] in higher-order parametric polymorphism) and shown that we (only) obtained a constructive weak comonad (because of the compatibility hypothesis required). In this part, the redecoration algorithm, although deduced directly from the finite case, is quite tricky to manipulate because of the cutting and lifting it requires.

We then noticed that we could also consider the triangles by their rows, representing this time the triangles by purely coinductive datatypes, Tri ′ , where we only took advantage of the existing type of streams (Str). This new visualization allowed us to define -keeping the same algorithmic idea as before -a function of redecoration redec ′ already simpler than redec and equivalent to it, modulo compatibility. But taking advantage of this representation by streams, we can simplify again the redecoration algorithm, using only standard functions on streams. This new function redec ′ alt is fully equivalent to redec ′ . Generalizing again, we get nearly for free the cobind of the comonad Str, redec ′ gen . This finally allows us to prove the three comonad laws for redec ′ alt . In short, we have shown that the redecoration function, which is a quite subtle operation if we translate it directly from the finite triangles, reduces to something very basic in the completely infinite (i. e., in both directions) view of the infinite triangles. In this case, it is much easier to work with only infinite elements than with partially finite ones in the sense of consisting of infinitely many finitely presented columns. In fact, the stream representation is even easier to manipulate than the representation of finite triangles, and the comonad laws even hold with less restrictions due to constructivity.

Notice that the row-based view would not have given new insights for finite triangles. Indeed, as they are symmetric, we would have obtained exactly the same representation as for the column-based approach, only perceived with interchanged roles of rows and columns.

As a final remark on the Coq side, the improved support for setoid rewriting and the class mechanism [START_REF] Sozeau | First-class type classes[END_REF] has shown to be of great help for the formalization and verification decribed in this paper.

Figure 1

 1 Figure 1 Dividing a triangle into columns

Figure 5

 5 Figure 5 Definition of redecoration

  es_cut (constr e, a r) := e :: (es_cut r) ◮ Remark. In the standard library of Coq, the type of streams with elements in type C are predefined, and we can represent this definition as follows: c : C s : Str C c :: s : Str C The projection functions are called hd and tl. They are such that hd(c :: s) = c and tl(c :: s) = s. We will also use the map function defined by map f (c :: s) = f c :: (map f s).

Figure 6

 6 Figure 6 Dividing a triangle into rows

Figure 7

 7 Figure 7 Conceptualizing a triangle as a triple

Figure 8

 8 Figure 8 Definition of toStreamRep

  toStreamRep t := top t, frow t :: toStreamRep (cut (rest t))

Figure 10

 10 Figure 10 Definition of redecoration

Figure 11

 11 Figure 11 Idea of another definition of redecoration

Figure 12

 12 Figure 12 Another definition of redecoration


Van Chan Ngo

Jean-Pierre Talpin

Thierry Gautier

Paul Le Guernic

Translation Validation for Clock Transformations in a Synchronous Compiler

Keywords: Formal Verification, Translation Validation, Certified Compiler, Smt Solver, Synchronous Data-Flow Languages

Translation validation was introduced as a technique to formally verify the correctness of code generators that attempts to ensure that program transformations preserve the semantics of input program. In this work, we adopt this approach to construct a validator that formally verifies the preservation of clock semantics during the Signal compiler transformations. The clock semantics is represented as a first-order logic formula called clock model. We then introduce a refinement which expresses the preservation of clock semantics, as a relation on clock models. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.

Introduction

Motivation. Synchronous programming languages such as Signal, Lustre and Esterel propose a formal semantic framework to give a high-level specification of safety-critical software in automotive and avionics systems [START_REF] Gamatié | Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification[END_REF][START_REF] Halbwachs | A Synchronous Language at Work: the Story of Lustre[END_REF][START_REF] Berry | The Foundations of Esterel[END_REF]. As other programming languages, synchronous languages are associated with a compiler. The compiler takes a source program, analyses and transforms it, performs optimizations, and finally generates executable code for a particular hardware platform or in some general-purpose programming languages. However, a compiler is a large and very complex program which often consists of hundreds of thousands, if not millions, lines of code, divided into multiple sub-systems and modules. The compilation process involves many analyzes, program transformations and optimizations. Some transformations and optimizations may introduce additional information, or constrain the compiled program. They may refine its meaning and specialize its behavior to meet a specific safety or optimization goal. Consequently, it is not uncommon that compilers silently issue an incorrect result in some unexpected context or inappropriate optimization goal. To circumvent compiler bugs, one can entirely rewrite the compiler with a theorem proving tool such as Coq [START_REF]The Coq Proof Assitant[END_REF], or check that it is compliant to the DO-178C documents [22]. Nonetheless, these solutions yield a situation where any change of the compiler (e.g., further optimization and update) means redoing the proof.

Another approach, which provides ideal separation between the tool under verification and its checker, is trying to verify that the output and the input have the same semantics. In this aim, translation validation was introduced in the 90's by Pnueli et al. [START_REF] Pnueli | Translation Validation[END_REF][START_REF] Pnueli | Translation Validation: From Signal to C[END_REF], as a technique to formally verify correctness of code generators. Translation validators can be used to ensure that program transformations do not introduce semantic discrepancies, or to help debugging the compiler implementation. Contribution. We consider the Signal compiler, in the first two phases, The clock information and Boolean abstraction are computed. The next phase is static scheduling and the final phase is the executable code generation. Obviously, one can prove that the input program and its transformed program at the final phase have the same semantics. However, we believe that a better approach consists in separating the concerns and proving for each phase the preservation of different kinds of semantic properties. In the case of a synchronous compiler such as Signal, the preservation of the semantics can be decomposed into the preservation of clock semantics, data dependencies, and value-equivalence of variables [START_REF] Ngo | Formal Verification of a Synchronous Data-flow Compiler: from Signal to C[END_REF].

This paper focuses on constructing a validator that proves the preservation of clock semantics in the first two phases of the Signal compiler. The clock semantics of the source program and its transformed counterpart are formally represented as clock models. A clock model is a first-order logic formula with uninterpreted functions. This formula deterministically characterizes the presence/absence status of all discrete data-flows (input, output and local variables of a program) manipulated by the specification at a given logic instant. Given two clock models, a correct transformation relation between them is checked by the existence of their refinement relation, which expresses the semantic preservation of clock semantics. In the implementation, we apply our translation validation to the first two transformation steps of the compiler.

The remainder of this paper is organized as follows. Section 2 introduces the Signal language. Section 3 presents the abstraction that represents the clock semantics in terms of first-order logic formula. In Section 4, we consider the definition of correct transformation on clock models which formally proves the conformance between the original specification and its transformed counterpart. The application of the verification process to the Signal compiler, and its integration in the Polychrony toolset [START_REF]Polychrony Toolset[END_REF] is addressed in Section 5. Section 6 presents related works and concludes our work.

The SIGNAL Language

Signal [START_REF] Benveniste | Hybrid Dynamical Systems Theory and the Signal Language[END_REF][START_REF] Gautier | Signal, a Declarative Language for Synchronous Programming of Real-time Systems[END_REF] is a polychronous data-flow language that allows the specification of multi-clocked systems, called polychrony models. Signal handles unbounded sequences of typed values x(t) t∈N , called signals, denoted as x. Each signal is implicitly indexed by a logical clock indicating the set of instants at which the signal is present, noted C x . At a given instant, a signal may be present where it holds a value, or absent where it holds no value, denoted by ⊥. Given two signals, they are synchronous iff they have the same clock. A process, written P or Q, consists of the synchronous composition of equations over signals x, y, z, written x := y op z or x := op(y, z), where op is an operator. In particular, a process can be used as a basic pattern, by means of an interface that describes its parameters and its input and output signals. Moreover, a process can use other subprocesses, or even other processes as external parameters. A program is a process and the language is modular. Data Domains. Data types consist of usual scalar types (Boolean, integer, float, complex, and character), enumerated types, array types, tuple types, and the special type event. It is a subtype of the Boolean which has only one value, true.

Operators. The core language consists of two kinds of "statement" defined by the following primitive operators: four operators on signals and two operators on processes. The operators on signals define basic processes with implicit clock relations while the operators on processes are used to construct complex processes with the parallel composition operator. In the delay operator, inf and sup denote the greatest lower bound and the least upper bound.

• Stepwise Functions:

y := f (x 1 , ..., x n ),

Clock Model

In Signal, clocks play a much more important role than in other synchronous languages, they are used to express the underlying control (i.e., the synchronization between signals) for any conditional definition. This differs from Lustre, where all clocks are built by sampling the fastest clock. We consider the following equation with the primitive operator sampling, where x and y are numerical signals, and b is a Boolean signal: y := x when b. To express the control, we need to represent the status of the signals x, y and b. We use a Boolean variable x to capture the status of x: (x = true) means x is present, and (x = false) means x is absent. In the same way, the Boolean variable ŷ captures the status of y.

Abstraction

Let X = {x 1 , ..., x n } be the set of all signals in program P consisting of input, output, register (corresponding to delay operator), and local signals, denoted by I, O, R and L, respectively. With each signal x i , based on the encoding scheme proposed in [START_REF] Gamatié | Static Analysis of Synchronous Programs in Signal for Efficient Design of Multi-Clocked Embedded Systems[END_REF], we attach a Boolean variable x i to encode its clock and a variable x i of same type as x i to encode its value. The composition of processes corresponds to logical conjunctions. Thus the clock model of P will be a conjunction Φ(P) = n i=1 φ(eq i ), whose atoms are x i , x i , where φ(eq i ) is the abstraction of statement eq i , and n is the number of statements in the program. In the following, we present the abstraction corresponding to each Signal operator.

Stepwise Functions. The functions which apply on signal values in the stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, / =), and numerical operators (+, -, * , /). In our experience working with the Signal compiler, it performs very few arithmetical optimizations and leaves most of the arithmetical expressions intact. Every definition of a signal is determined explicitly by the input and register signals, otherwise program can not be compiled. This suggests that most of the implications will hold independently of the features of the numerical comparison functions and numerical operators and we can replace these operations by uninterpreted functions. By following the encoding procedure of [START_REF] Ackerman | Solvable Cases of the Decision Problem[END_REF], for every numerical comparison function and numerical operator (denoted by ) occurring in an equation, we perform the following rewriting: i) Replace each x y by a new variable v i of the same type as the return value by . Two stepwise functions x y and x y are replaced by the same variable v i iff x, y are identical to x and y , respectively; ii) For every pair of newly added variables v i and v j , i = j, corresponding to the non-identical occurrences x y and x y , add the

implication ( x = x ∧ y = y ) ⇒ v i = v j into the abstraction Φ(P). The abstrac- tion φ(y := f (x 1 , ..., x n ))
of stepwise functions is defined by induction as follows: φ(true) = true and φ(false) = false; φ(y

:= x) = (ŷ ⇔ x) ∧ (ŷ ⇒ ( y = x)); φ(y := x) = (ŷ ⇔ x) ∧ (ŷ ⇒ ( y = x)) ∧ (x ⇒ x) if x is an event signal; φ(y := not x) = (ŷ ⇔ x) ∧ (ŷ ⇒ ( y ⇔ ¬ x)); φ(y := x 1 and x 2 ) = (ŷ ⇔ x 1 ⇔ x 2 ) ∧ (ŷ ⇒ ( y ⇔ x 1 ∧ x 2 )); φ(y := x 1 or x 2 ) = (ŷ ⇔ x 1 ⇔ x 2 ) ∧ (ŷ ⇒ ( y ⇔ x 1 ∨ x 2 )); φ(y := x 1 x 2 ) = (ŷ ⇔ v i ⇔ x 1 ⇔ x 2 ) ∧ (ŷ ⇒ ( y = v i )).
Delay. Considering the delay operator, y := x$1 init a, its encoding φ(y := x$1 init a) contributes to Φ(P) with the following conjunct:

(ŷ ⇔ x) ∧ (ŷ ⇒ (( y = m.x) ∧ (m.x = x))) ∧ (m.x 0 = a)
. This encoding requires that at any instant, signals x and y have the same status (present or absent). To encode the value of the output signal as well, we introduce a memorization variable m.x that stores the last value of x. The next value of m.x is m.x and it is initialized to a in m.x 0 .

Merge. The encoding of the merge operator, y := x default z, contributes to Φ(P) with the following conjunct:

(ŷ ⇔ (x ∨ ẑ)) ∧ ŷ ⇒ ((x ∧ ( y = x)) ∨ (¬x ∧ ( y = z))))
Sampling. The encoding of the sampling operator, y := x when b, contributes to Φ(P) with the following conjunct:

(ŷ ⇔ (x ∧ b ∧ b)) ∧ (ŷ ⇒ ( y = x))
Composition. Consider the composition of two processes P 1 and P 2 . Its abstraction φ(P 1 |P 2 ) is defined as follows: φ(P 1 ) ∧ φ(P 2 ) Clock Relations. Given the above rules, we can obtain the following abstraction for derived operators on clocks. Here, z is a signal of type event:

φ(z :=ˆx) = (ẑ ⇔ x) ∧ (ẑ ⇒ z); φ(xˆ= y) = x ⇔ ŷ; φ(z := xˆ+ y) = (ẑ ⇔ (x ∨ ŷ)) ∧ (ẑ ⇒ z); φ(z := xˆ * y) = (ẑ ⇔ (x∧ŷ))∧(ẑ ⇒ z); φ(z := xˆ-y) = (ẑ ⇔ (x∧¬ŷ))∧(ẑ ⇒ z); φ(z := when b) = (ẑ ⇔ ( b ∧ b)) ∧ (ẑ ⇒ z).
Example. Applying the abstraction rules above, the clock semantics of the program DEC is represented by the following formula Φ(DEC), where ZN <= 1 and ZN -1 are replaced by two fresh variables ZN1 and ZN2, and encoded by two uninterpreted function symbols v 1 <= and v 1 -, respectively.

(

F B ⇔ ZN 1 ∧ ZN 1) ∧ ( ZN 1 ⇔ v 1 <= ⇔ ZN ) ∧ ( ZN 1 ⇒ ( ZN 1 = v 1 <= )) ∧ ( ZN ⇔ N ) ∧ ( ZN ⇒ ( ZN = m.N ∧ m.N = Ñ )) ∧ (m.N 0 = 1) ∧ ( N ⇔ F B ∨ ZN 2) ∧ ( N ⇒ (( F B ∧ Ñ = F B) ∨ (¬ F B ∧ Ñ = ZN 2))) ∧ ( ZN 2 ⇔ v 1 -⇔ ZN ) ∧ ( ZN 2 ⇒ ( ZN 2 = v 1 -))
In the following sections, we denote input, output, register, memorization and local variables used in a clock model by I clk , O clk , R clk , M clk and L clk , respectively. Note that the memorization variables are introduced only by the translation into clock models, they are not original in the Signal programs.

Definition 1 (Clock configuration). Consider a clock model Φ(P) over the set of variabels X. A clock configuration I is an interpretation over X such that it is a model of the first-order logic formula Φ(P).

For instance, ( FB → true, N → true, ZN → true, FB → 6, Ñ → 6, ZN → 1) is a clock configuration of Φ(DEC).

Concrete Clock Semantics

We rely on the basic elements of trace semantics [START_REF] Guernic | Advanced Topics in Data-flow Computing, Chapter Data-flow to von Neumann: the Signal Approach[END_REF] to define the clock semantics of a synchronous program. For each x i ∈ X, we use D xi to denote its domain of values, and D ⊥ xi = D xi ∪ {⊥} to denote its domain of values with absent value, where ⊥ ∈ D xi denotes the absent value. Then, the domain of values of X with absent value is defined as D ⊥ X = n i=1 D xi ∪ {⊥} Definition 2 (Clock events, clock traces). Given a non-empty set X, the set of clock events on X, denoted by Ec X , is the set of all possible interpretations I over X. The set of clock traces on X, denoted by T c X , is defined by the set of functions T c defined from the set N of natural numbers to Ec X , denoted by

T c : N -→ Ec X .
An interpretation I is an assignment of values from X to D ⊥ X . The assignment I(x) = ⊥ means x holds no value while I(x) = v means that x holds the value v. The natural numbers represent the instants, t = 0, 1, 2, ..., a trace T c is a chain of clock events. We denote the interpreted value of a variable x i at instant t by T c (t)(x i ).

Definition 3 (Restriction clock trace). Given a non-empty set X, a subset X 1 ⊆ X, and a clock trace T c being defined on X, the restriction of T c onto X 1 is denoted by X 1 .T c . It is defined as

X 1 .T c : N -→ Ec X1 such that ∀t ∈ N, ∀x ∈ X 1 , X 1 .T c (t)(x) = T c (t)(x).
Let X be the set of all signals in program P. We write [[P]] c to denote the clock semantics of P which is defined as the set of all possible clock traces on X. For any subset X 1 ⊆ X, the set of all restriction clock traces on X 1 defines the clock semantics of P on X 1 , denoted by ([[P]] c ) \X1 .

Let Φ(P) be the clock model of the program P. We now define the concrete clock semantics of a clock model based on the notion of clock configurations. Given a clock configuration Î, the set of clock events according to Î is the set of interpretations I such that for every signal x i , if x i holds a value then x i has the value true (x i is present), and x i holds the same value as x i . Otherwise, x i has the value false (meaning x i is absent). The set of clock events according to Î and the set of all clock events of Φ(P) are computed as follows:

S Ec X ( Î) = {I ∈ Ec X | ∀x i ∈ X, (I(x i ) = Î( x i ) ∧ Î( x i ) = true) ∨(I(x i ) = ⊥ ∧ Î( x i ) = false)} S Ec X (Φ(P)) = Î|=Φ(P) S Ec X ( Î)
With a set of clock events S Ec X (Φ(P)), the concrete clock semantics of Φ(P) is defined by the following set of clock traces

Γ (Φ(P)) = {T c ∈ T c X | ∀t, T c (t) ∈ S Ec X (Φ(P))}. For any subset X 1 ⊆ X, the concrete clock semantics of Φ(P) on X 1 is defined as Γ (Φ(P)) \X1 = {X 1 .T c | T c ∈ T c X and ∀t, T c (t) ∈ S Ec X (Φ(P))}.
Due to the lack of space, we do not present the proof of soundness of our abstraction.

Clock Model Translation Validation

We adopt the translation validation approach [START_REF] Pnueli | Translation Validation[END_REF][START_REF] Pnueli | Translation Validation: From Signal to C[END_REF] to formally verify that the clock semantics is preserved for every transformation of the compiler. In order to apply the translation validation to the transformations, we capture the clock semantics of the original program and its transformed counterpart by means of clock models. Then we introduce a refinement relation which expresses the preservation of clock semantics, as relation on clock models.

Clock Refinement

Let Φ(A) and Φ(C) be two clock models of programs A and C, to which we refer respectively as a source program and its transformed counterpart produced by the compiler. We denote the sets of all signals in A, C by X A and X C , respectively. The corresponding sets of variables which are used to construct the clock models are denoted by X A and X C . Consider the finite set of common signals X = X A ∩ X C and the set of common variables which are used to construct the clock models is X = X A ∩ X C , we say that A and C have the same clock semantics on X if Φ(A) and Φ(C) have the same set of concrete restriction clock traces on X:

∀X.T c .(X.T c ∈ Γ (Φ(C)) \X ⇔ X.T c ∈ Γ (Φ(A)) \X )
In fact, the compilation makes the transformed program more concrete. For instance, when the Signal compiler performs the "endochronization" which is used to generate the sequential executable code, the signal with the fastest clock is always present in the generated code. Moreover, compilers perform transformations and optimizations for removing or eliminating some redundant behaviors of the source program (e.g., eliminating subexpressions, trivial clock relations). Consequently, the above requirement is too strong to be practical. Hence, we have to relax it as follows:

∀X.T c .(X.T c ∈ Γ (Φ(C)) \X ⇒ X.T c ∈ Γ (Φ(A)) \X ) It expresses that every restriction clock trace of Φ(C) is also a clock trace of Φ(A) on X, or Γ (Φ(C)) \X ⊆ Γ (Φ(A)) \X . We say that Φ(C) is a correct clock transformation of Φ(A), or Φ(C) is a clock refinement of Φ(A) on X, denoted by Φ(C) clk Φ(A).
Proposition 1. The clock refinement is reflexive and transitive Proof. Proposition 1 is proved based on the clock refinement definition. Φ(P) clk Φ(P) since Γ (Φ(P)) \X ⊆ Γ (Φ(P)) \X . For every clock trace X.T c ∈ Γ (Φ(P 1 )) \X , Φ(P 1 ) clk Φ(P 2 ) on X implies X.T c ∈ Γ (Φ(P 2 )) \X . Since Φ(P 2 ) clk Φ(P 3 ) on X, we have X.T c ∈ Γ (Φ(P 3 )) \X , or Φ(P 1 ) clk Φ(P 3 ) on X.

Adaptation to SIGNAL Compiler

We will adapt the definition of the above general clock refinement to the case of the Signal compiler. We need to consider the following factors [START_REF] Besnard | Compilation of Polychronous Data Flow Equations[END_REF]. A first consideration is that the programs take the inputs from their environment and the register values. Then, they calculate the outputs to react with the environment. In general, the programs can use some local variables to make the output calculations. However, from the outside, the natural observation of the programs is the snapshot of the values of the input and output signals. In our context, it is the snapshot of the presence of the input and output signals. For example, for the program DEC, the observation is the tuple of the presence of the signals (FB, N) at a considered instant.

A second consideration is that in the compilation process of the Signal compiler, the local signals in the source program do not necessarily have counterparts in the transformed program. However, all input and output signals are preserved in the transformations and are represented by identical names in the transformed program. Moreover, all signals in the R set are also preserved in the transformations. Therefore, it is natural to choose the snapshot of the presence of the input and output signals to be the observation for the transformed program.

These considerations let us adapt the above definition of clock refinement as follows. Let X A and X C be the sets of all signals in the source program A and its counterpart transformed program C. We write X IO to denote the set of common input and output signals. We say that C is correct transformation of A if at any instant, the tuples of values representing the presence of the signals in X IO are the same in both programs. In other words, Φ(C) clk Φ(A) on X IO .

Proving Clock Refinement by SMT

Our aim is proving that Φ(C) refines Φ(A) on X IO . Let X A , X C and X IO be the set of variables which are used to construct Φ(A), Φ(C) and the set of common variables between the two clock models. For every variable in the clock model Φ(C) except the common variables in X IO , we added "c" as superscript to distinguish them from the variables in the clock model of the input program. The standard way of proving the existence of the clock refinement is based on the following elements:

• The identification of a variable mapping that maps the non input/output variables from the clock model Φ(A) to the non input/output variables in the clock model Φ(C). We denote the mapping by: X A \ X IO = α( X C \ X IO ) • The premises of a rule such that if the premises hold, then the conclusion, Φ(C) refines Φ(A), is true. The premise is presented in Fig. 1.

For a variable mapping The rule CLKREF indicates that for any interpretation Î over X A ∪ X C such that the variable mapping is evaluated to true, Î is a clock configuration of Φ(C) then it is also a clock model of Φ(A). Then there exists a clock refinement for (Φ(C), Φ(A)). The rule CLKREF is sound based on the following theorem.

X A \ X IO = α( X C \ X IO ), Premise ∀ Î over X A ∪ X C .( Î |= Φ(C) ⇒ Î |= Φ(A)) Conclusion Φ(C) clk Φ(A) on X IO
Theorem 1. For a variable mapping

X A \ X IO = α( X C \ X IO ), if the formula Φ(C) ⇒ Φ(A) is valid, then Φ(C) clk Φ(A) on X IO .
Proof. To prove it, we have to show that for every interpretation Î over X =

X A ∪ X C such that it is evaluated to true. If Î |= (Φ(C) ⇒ Φ(A)), then Γ (Φ(C)) \X IO ⊆ Γ (Φ(A)) \X IO . Given X IO .T c ∈ Γ (Φ(C)) \X IO , it means that ∀t, T c (t) ∈ S Ec X (Φ(C)). Since for every interpretation Î, Î |= Φ(C) implies that Î |= Φ(A)), thus S Ec X (Φ(C)) ⊆ S Ec X (Φ(A)
) under the variable mapping. We get T c (t) ∈ S Ec X (Φ(A)) for every t. Therefore, we have T c ∈ Γ (Φ(A)).

Consider a variable x ∈ X A \ X IO , the mapping α x of the variable mapping defines the value of x in the clock model Φ(A) α-related to the value represented by the clock model Φ(C). We therefore need to describe the mappings

α x for x c ∈ X C \ X IO = M clk ∪ R clk ∪ L clk .
⇔ f ∧ ( l ⇒ l = f ) or l ⇔ f ∧ ( l ⇒ l = f ) ∧ f 0 ,
where f , f and f 0 are the formulas which define the clock relation, the value, and the initial value of the signal l in the clock model Φ(A). Therefore, we define the following instance of the α mapping in the clock model corresponding to each register or local signal l:

l ⇔ f ∧ ( l ⇒ l = f ) or l ⇔ f ∧ ( l ⇒ l = f ) ∧ f 0 .
For example, the mapping for the variables ZN and ZN in the clock model Φ(DEC) corresponding to the local variable ZN in the program DEC will be given by the formula:

( ZN ⇔ N ) ∧ ( ZN ⇒ ( ZN = m.N ∧ m.N = N )) ∧ (m.N 0 = 1).
Therefore, the variable mapping X A \ X IO = α( X C \ X IO ) is expressed as the following formula:

m.s∈M ( s = s c ⇒ m.s = m.s c ) ∧ l, l∈S∪L ( l ⇔ f ∧ ( l ⇒ l = f )) or m.s∈M ( s = s c ⇒ m.s = m.s c ) ∧ l, l∈S∪L ( l ⇔ f ∧ ( l ⇒ l = f ) ∧ f 0 )
To solve the validity of the formula (Φ(C) ⇒ Φ(A)) in Theorem 1 under the variable mapping, a Smt solver is needed since this formula involves non-Boolean variables and uninterpreted functions (using a Sat solver would not be sufficient). A Smt solver decides the satisfiability of arbitrary logic formulas of linear real and integer arithmetic, scalar types, other user-defined data structures, and uninterpreted functions. If the formula belongs to the decidable theory, the solver gives two types of answers: sat when the formula has a model (there exists an interpretation that satisfies it); or unsat, otherwise. In our case, we will ask the solver to check whether the formula

¬(Φ(C) ∧ X A \ X IO = α( X C \ X IO ) ⇒ Φ(A)) is unsatisfiable, since this formula is unsatisfiable iff |= (Φ(C) ∧ X A \ X IO = α( X C \ X IO ) ⇒ Φ(A)).
In our translation validation, the clock models which are constructed from Boolean or numerical variables and uninterpreted functions belong to a part of first-order logic which has a small model property according to [START_REF] Borger | The Classical Decision Problem[END_REF]. The numerical variables are involved only in some implications with uninterpreted functions such as ( x = x ∧ y = y ) ⇒ v i = v j .

In addition, the formula is quantifier-free. This means that the check of satisfiability can be established by examining a certain finite cardinality of models. Therefore, the formula can be solved efficiently and significantly improves the scalability of the solver.

Implementation

This section describes the implementation of our validator and some adaptation when the translation validation is applied to the real Signal compiler. We also show the previously unknown bugs have been detected so far by our validator.

Towards Certified Compiler

Given a program P, with an unverified compiler, the compilation process can be represented in the following pseudo-code, where Cp(P) is the compilation step from the source program P to either compiled code IR(P) or compilation errors: This will provide a formal guarantee as strong as that provided by a certified compiler in case the correctness of the validator is proved. We describe the main components of the implementation which is integrated in the existing Polychrony toolset [START_REF]Polychrony Toolset[END_REF] to prove the preservation of clock semantics of the Signal compiler. We are interested here in the first phase: clock calculation and Boolean abstraction where the intermediate forms of the source program of are expressed in the Signal language itself. At a high level, our validator, which is depicted in Figure 2, works as follows. First, it takes the input program P and its transformed counterpart P BASIC TRA, and constructs the corresponding clock models. These clock models are combined as the formula (Φ(P BASIC TRA) ⇒ Φ(P)). In the solving phase, it checks the validity of the formula Φ(P BASIC TRA) ⇒ Φ(P). The result of this check can be exploited for the preservation of clock semantics of the transformations. If the formula is not valid then it emits a compiler bug. Otherwise, the compiler continues its work. The same procedure is applied for the other steps of the compiler. Finally, our verification process asserts that Φ(P BOOL TRA) clk Φ(P BASIC TRA) clk Φ(P) along the transformations of the compiler. We delegate the checking of the clock refinement to a Smt solver. For our experiments, we consider the Yices [START_REF] Dutertre | Yices Sat-solver[END_REF] solver, which is one of the best solvers at the Smt-Comp competition [START_REF] Stump | SMT-Comp[END_REF].

Detected Bugs

So far, our validator has revealed three previously unknown bugs in the compilation of the Signal compiler. The first problem was introduced when multiple

Related Work and Conclusion

The notion of translation validation was introduced in [START_REF] Pnueli | Translation Validation[END_REF][START_REF] Pnueli | Translation Validation: From Signal to C[END_REF] by A. Pnueli et al. to verify the code generator of Signal. In that work, the authors define a language of symbolic models to represent both the source and target programs, called Synchronous Transition Systems (Sts). A Sts is a set of logic formulas which describes the functional and temporal constraints of the whole program and its generated C code. Then they use Bdd [START_REF] Bryant | Graph-based Algorithms for Boolean Function Manipulation[END_REF] representations to implement the symbolic Sts models, and their proof method uses a solver to reason on constraints over signals. The drawback of this approach is that it does not capture explicitly the clock semantics. Additionally, for a large program, the formula is very large, including numerical expressions that cause some inefficiency. Moreover, the whole calculation of a synchronous program or the corresponding generated code is considered as one atomic transition in Sts, thus it does not capture the data dependencies between signals and does not explicitly prove the preservation of abstract clocks in the compiler transformations.

Another related work is the static analysis of Signal programs for efficient code generation [START_REF] Gamatié | Static Analysis of Synchronous Programs in Signal for Efficient Design of Multi-Clocked Embedded Systems[END_REF]. In a similar way as we do, the authors formalize the abstract clocks and clock relations as first-order logic formulas with the help of interval abstraction technique. The objective is to make the generated code more efficient by detecting and removing the dead-code segments (e.g., segment of code to compute a data-flow which is always absent). They determine the existence of empty clocks, mutual exclusion of two or more clocks, or clock inclusions, by reasoning on the formal model using a Smt solver. Some other works have adopted the translation validation approach in verification of transformations, and optimizations. In [START_REF] Necula | Translation Validation for an Optimizing Compiler[END_REF], the translation validation is used to verify several common optimizations such as common subexpression elimination, register allocation, and loop inversion. The validator is simulationbased, that means it checks the existence of a simulation relation between two programs. Leroy et al. [START_REF] Leroy | Formal Certification of a Compiler Back-end, or Programming a Compiler with a Proof Assistant[END_REF][START_REF]The CompCert Project[END_REF] used this technique to develop the CompCert highassurance C compiler. The programs before and after the transformations and optimizations of the compiler are represented in a common intermediate form, then the preservation of semantics is checked by using symbolic execution and the proof assistant Coq. It also has shown that translation validation can be used to validate advanced loop optimizations such as software pipelining as in [START_REF] Tristan | A Simple, Verified Validator for Software Pipelining[END_REF]. Tristan et al. [START_REF] Tristan | Evaluating Value-graph Translation Validation for LLVM[END_REF] recently proposed a framework for translation validation of Llvm optimizer. For a function and its optimized counterpart, they compute a shared value-graph. The graph is normalized (roundly speaking, the graph is reduced). After the normalizing, if the outputs of two functions are represented by the same sub-graph, they can safely conclude that two functions are equivalent.

With the same purpose, in the work of [START_REF] Ngo | Formal Verification of Compiler Transformations on Polychronous Equations[END_REF], we encode the source Signal programs and their transformations with Polynomial Dynamical Systems (Pds), and we prove that the transformations preserve the abstract clocks and clock relations of the source programs. This approach uses simulation relation in model checking techniques, and it suffers from the increasing of the state-space when it deals with large programs. On the contrary, in our present work, the abstract clocks and clock relations are described as a logic formula over Boolean variables. Thanks to the efficiency of Smt solver implementation in processing formulas over Boolean variables and uninterpreted functions, our approach can deal with large programs whose number of variables is large. This situation generally makes the state-space explosion problem in model checking techniques.

The present paper provides a proof of correctness of a the synchronous dataflow compiler. We have presented a technique based on Smt solving to prove the preservation of clock semantics during the compilation. Namely, we have shown that implicit clock relations, describing the discrete timing model of a dataflow specification, are preserved in their implementation. The desired behavior of a given source program and the transformed one are represented as clock models. A refinement relation between source and transformed programs is used to express the preservation, which is checked by using a Smt solver. We have constructed and integrated our validator within the Polychrony toolset to prove the correctness of the Signal compiler.

We believe that our validator must have the following features to be effective and realistic. First, we do not modify or instrument the compiler, and we treat the compiler as a "black box". Hence the validator is not affected by some future update or modification of the compiler. We only need some additional information about the mapping between original names and potential new names of local variables. Our approach consists in applying formal methods to the compiler transformations themselves in order to automatically generate formal evidence that the clock semantics of the source program is preserved during program transformations, as per applicable qualification standard. Second, it is important that the validator can be scaled to large programs. For this purpose, we represent the desired program semantics using a scalable abstraction and we use efficient Smt libraries [START_REF] Dutertre | Yices Sat-solver[END_REF] to achieve the expected goals: traceability and formal evidence. Moreover, this approach provides an attractive alternative to develop a certified compiler for a synchronous language since in general the validator is much smaller and easier to verify than the compiler it validates.

  For b, two Boolean variables b and b are used to represent its status: ( b = true ∧ b = true) means b is present and holds a value true; ( b = true ∧ b = false) means b is present and holds a value false; and ( b = false) means b is absent. Hence, at a given instant, the clock relations of the equation above can be encoded by the formula: ŷ ⇔ (x ∧ b ∧ b)

Fig. 1 :

 1 Fig. 1: Rule CLKREF

  Recall that every register signal s, we introduce memorization variables m.s, m.s in the clock model Φ(A), and the corresponding memorization variables m.s c , m.s c in the clock model Φ(C). Therefore, we define the following instance of the α mapping for each register signal s: s = s c ⇒ m.s = m.s c ∧ m.s = m.s c .For example, the mapping for the variables m.N , m.N , m.N c , and m.N c will be given by the formula:N = N c ⇒ m.N = m.N c ∧ m.N = m.Nc . It remains to define the instance of the mapping α for variables l, l ∈ R clk ∪ L clk in the clock model Φ(A) which correspond to the local or register signal named l in the program. In a Signal program, one signal is defined by an equation l = eq, if we follow the definitions of all output and local signals in this equation and apply successively substitutions, then we get that the equation is constructed only by the input and register signals. This property is yielded since the Signal program is determinate, meaning that all definitions of signals are defined determinately by the input and register signals, and the compilers rejects all non-determinate program. Equivalently, in the corresponding clock model Φ(A), the output, register and local variables are determinately defined by the input I and memorization M variables. The definition is written in the clock model in the form l

If P 1 and P 2 are processes, then P 1 |P 2 , also denoted as (|P 1 |P 2

  where f is a n-ary function on values, defines a basic process whose output y is synchronous with x 1 , ..., x n (C y = C x1 = ... = C xn ) and ∀t ∈ C y , y(t) = f (x 1 (t), ..., x n (t)).• Delay: y := x$1 init a defines a basic process such that y and x are synchronous(C y = C x ), y(t 0 ) = a, and ∀t ∈ C y ∧ t > t 0 , y(t) = x(t -) with t 0 = inf{t |x(t ) = ⊥}, t -= sup{t |t < t ∧ x(t ) = ⊥}.Clock relations can be defined explicitly: y :=ˆx specifies that y with event type is the clock of x, C x . The synchronization xˆ= y means that x and y have the same clock. The clock extraction from a Boolean signal is denoted by a unary when: when b. The clock union x ˆ+ y defines a clock as the union C x ∪ C y . In the same way, the clock intersection xˆ * y and the clock difference xˆ-y define clocks C x ∩ C y and C x \ C y .

	input. The following diagram illustrates one possible execution of the program
	DEC.
	process DEC=
	(? integer FB; ! integer N) //FB is input signal and N is
	output signal
	(| FB ˆ= when (ZN<=1) //FB is present when ZN holds a value
	smaller than 1
	| N := FB default (ZN-1)
	| ZN := N$1 init 1 //ZN takes the previous value of N
	|)
	where integer ZN end; //ZN is defined as a local signal
	t . . . . . . . . . .
	FB 6 ⊥ ⊥ ⊥ ⊥ ⊥ 3 ⊥ ⊥ 2
	ZN 1 6 5 4 3 2 1 3 2 1
	N 6 5 4 3 2 1 3 2 1 2
	CFB t0	t6	t9
	CZN t0 t1 t2 t3 t4 t5 t6 t7 t8 t9
	CN t0 t1 t2 t3 t4 t5 t6 t7 t8 t9
	• Merge: y := x default z defines a basic process which specifies that y is
	present iff x or z is present (C y = C x ∪ C z ), and that y(t) = x(t) if t ∈ C x
	and y(t) = z(t) if t ∈ C z \ C x .
	• Sampling: y := x when b where b is a Boolean signal, defines a basic process
	such that ∀t ∈ C x ∩ C b ∧ b(t) = true, y(t) = x(t), and otherwise, y is absent
	(C y = C x ∩ [b], where [b] = {t ∈ C b |b(t) = true}).
	• Composition: |),
	is the process resulting of their parallel composition. This process consists
	of the composition of the systems of equations. The composition operator is
	commutative, associative, and idempotent.
	• Restriction: P where x, where P is a process and x is a signal, specifies a
	process by considering x as local variable to P (i.e., x is not accessible from
	outside P).
	Clock Relations. Example. The following Signal program emits a sequence of values FB, FB-1,...,
	2, 1, from each value of a positive integer signal FB coming from its environment.
	We can see that the clock of the output signal is more frequent than that of the

  Now, the compilation is followed by our refinement verification which checks that the transformed program IR(P) refines P w.r.t. the clock semantics:

	if (Cp(P) is Error) then
	output Error;
	else output IR(P);
	if (Cp(P) is Error) then
	output Error;
	else if (Φ(IR(P)) clk Φ(P)) then
	output IR(P);
	else output Error;

In the transformed counterpart P BASIC TRA, the introduction of signal XZX 24 and the synchronization between CLK and XZX 24 cause the incorrect specification of clocks, the signal x might be absent when XZX 24 is absent, which is not the case in P, nor in P BOOL TRA). This bug was caught by our validator when it found that Φ(P BOOL TRA) clk Φ(P BASIC TRA).

The second problem is the wrong implementation of xor operator as shown in the followng program. The validator detects this bug with the fact that Φ(P BASIC TRA) clk Φ(P). The last problem detected was not found by the translation validation but was indirectly discovered when trying to apply it. It occurred in a program in which a merge operator with a constant signal was used, such as y := 1 default x. In this case, the code generation phase of the compiler dealt wrongly with the clock context of a constant signal by introducing a syntax error in the generated C code. The bug and its fix are given by: // Version with bug // Version without bug if (C_y) { if (C_y) { y = 1; else y = x; if (C_y) y = 1; else y = x; w_ClockError_y(y); w_ClockError_y(y); } }