Certi ed programming is one of the desirable approaches to developing dependable software, where expected properties of programs are formally proved by proof assistants such as Coq. One way for certi ed programming with Coq is to de ne a function, give proofs for its properties in Coq, and then extract a program in OCaml. Another way for certi ed programming with Coq is to import the de nition from OCaml and give proofs for its properties in Coq. Since translations in both methods are unidirectional, we can modify only either of Coq and OCaml. That makes it hard to develop large certi ed programs. To solve this problem, we propose a new framework for certi ed programming through bidirectional transformation between Coq functions and OCaml programs. In our system, one can develop certi ed programs by modifying both Coq functions and OCaml programs alternatingly. All updates of the OCaml program are re ected to the Coq function, and vice versa, while reusing as many parts of the original one as possible.
Copyright c by the paper's authors. Copying permitted for private and academic purposes. in OCaml. The major di erence is that we must care for totality of functions and termination of recursion in Coq. In addition, all functions have to be de ned without either side e ects or exception handling. These requirements make certi ed programing in Coq more di cult.
In actual development with certi ed programming, we make a compromise by specifying functions in Coq only for a part of the large programs. One may develop a software using both Coq and OCaml, where the whole program is written in OCaml and a part of functions in it are veri ed in Coq. There are two approaches to this mixed style of programing, prove-and-extract and import-and-prove.
In the prove-and-extract method, we de ne important functions in Coq and give proofs for their properties in Coq. Then we translate them into equivalent OCaml programs by the extraction mechanism of Coq so that they can be referred from the other user-written OCaml programs. In this style, we have to carefully specify functions in Coq because the program extraction of Coq may generate a program that behaves equivalently but has an unexpected type. For example, consider the following function of type nat * nat -> nat speci ed in Coq:
Definition add_pair (p: nat * nat) := let (x, y) := p in x + y. which takes a pair of natural numbers and returns their sum. The program extraction produces an OCaml program
let add_pair = function Pair (x, y) -> add x y that is semantically equivalent to the original one but has type (nat, nat) prod -> nat even if the OCaml function of type nat * nat -> nat might be expected. Although some cases may be solved by the representation mapping mechanism of Coq (e.g., Extraction Inductive), it is not easy in general to predict extracted OCaml programs from Coq scripts.
In the import-and-prove method, we write the whole program in OCaml language and only important functions in it are translated into functions to be accepted in Coq. Then we prove their expected properties in Coq independently from the original program. In this style, we never su er from the unexpected program extraction of Coq. CFML [Cha11] and CoqOfOCaml [Cla14] are possible approaches to the import-and-prove method, in which one can verify existing OCaml programs by translating them into Coq. However, the proof of the properties cannot be reused if the speci cation of the OCaml programs is updated. We need to retranslate the program and prove the properties from scratch. In addition, the existing approaches generate di erent structures of functions in Coq. This also makes it hard to reuse the original proof for updates.
In this paper, we propose a new framework which combines both advantages of the prove-and-extract and import-and-prove methods. Our key idea is a bidirectional transformation between Coq functions and OCaml programs. In our system, one can develop certi ed programs by modifying both Coq functions and OCaml programs alternatingly. All updates of the OCaml program are re ected to the Coq function, and vice versa, while reusing as many parts of the original one as possible.
Our system is designed so as to meet the following requirements:
The speci cation of functions are given in OCaml so that we can obtain the advantage of the importand-proof style for certi ed programming. Since we need to combine with the other user-written OCaml programs in the nal product, the speci cation should be provided by OCaml instead of Coq. OCaml programs are translated into Coq with preserving as much information as possible. Initial translation just generates an equivalent Coq script from the OCaml program. If the translation has been done before, Coq-speci c portions, in particular statements and their proofs, should be left as they are. The user may have to revise the proof of properties of a function in Coq if its de nition is updated in OCaml. Updates in Coq are re ected to OCaml as far as needed so that we can modify the de nition of types and functions in Coq (without changing their behaviors) to make it easy to verify their properties. The translated Coq functions may be too complicated to treat for certi cation because OCaml has a less powerful type system than Coq (e.g., partial type application). Hence the Coq script should be modi able and the modi cation should be re ected to OCaml whenever needed.
Whatever is common between Coq and OCaml should be synchronized so that we can modify as exibly as possible in the both side of Coq and OCaml. One may prefer to use the syntax only allowed in one side, e.g., inlined pattern in OCaml and binding variables sharing the same type in Coq. The system should translate them correctly and be preserved as much as possible against updating. All of these requirements are achieved by combining with four bidirectional transformations between ve data, Coq script text, Coq AST, common data, OCaml AST, and OCaml program text. Two bidirectional transformations between text and AST are implemented with BiYacc [KZH16] which preserving comments and indentations appropriately. The other two between ASTs are implemented with BiGUL [ZZK+16] which is a formally-veri ed bidirectional language. 2
This section explains how users develop a program through bidirectional transformation between Coq and OCaml, giving a possible scenario using our system and a concrete example of practical situations. 2.1
1. We rst write an OCaml program P0 to be veri ed. Our system translates it into a function D0 in Coq. 2. When the function de nition in Coq is required to change for making it easier for the users to prove its property, we may modify the de nition and give the proof. Our system translates the modi ed function D1 into a new OCaml program P1 which is obtained by updating with a possibly small modi cation. 3. When the speci cation of the OCaml program is required to be changed due to updates of the other userwritten program, we may modify the translated program P1 to one that satis es the requirement. Our system translates the updated program P2 into a new function de nition D2 in Coq as a possibly small modi cation for D1. 4. The proof should be modi ed in general because the function de nition is changed. Most of the original proof may be reused for the modi cation. Our system does not try to translate the updated script in Coq unless the function de nition is changed.
This is a typical scenario for certi ed programming using our system, where can modify both OCaml programs and their corresponding functions in Coq. The `possibly small modi cation' requirement in steps 2 and 3 is ful lled by a put-based implementation written in BiGUL as mentioned later. Our solution in the current implementation may not be optimal, though. What should be emphasized here is that both Coq script and OCaml program can be a `source' of bidirectional transformation in terms of bidirectional lenses [FGM+07]. The `view' is an internal data which contains common information of the both languages. 2.2
We shall show a concrete example of the usage of our system. Consider the case where the user initially writes an OCaml program: type 'a binary_tree = | Leaf of 'a | Node of 'a binary_tree * 'a binary_tree let rec size (bt : int binary_tree) : int = match bt with | Leaf i -> i + 1 | Node (bt1, bt2) -> size bt1 + size bt2 where the type declaration speci es a polymorphic type binary_tree with a type variable 'a and the let rec declaration de nes a recursive function that computes a size of binary trees by summing up all integer values at leaves after incrementing by one. Our system translates the OCaml program into a script in Coq: Inductive binary_tree ( A : Type ) : Type := | Leaf : A -> binary_tree A | Node : binary_tree A * binary_tree A -> binary_tree A.
Fixpoint size ( bt : binary_tree nat ) : nat := match bt with | Leaf _ i => i + 1 | Node _ (bt1, bt2) => size bt1 + size bt2 end. where type int is translated into nat (type of natural numbers) in Coq by default. The user may modify nat into Z (type of integers) without changing the type int in OCaml after re ecting the update. Although the de nition of recursive functions in Coq requires the evidence of termination in general, this kind of structural recursion is automatically guaranteed to terminate. Because of the di erence of the type systems between Coq and OCaml, the constructors Leaf and Node have to take an additional argument for instantiating a type variable in the polymorphic type.
The user may certify the property of the size function that it returns a positive integer for any inputs. The Coq script is updated as:
Inductive binary_tree ( A : Type ) : Type := | Leaf : A -> binary_tree A | Node : binary_tree A * binary_tree A -> binary_tree A. Fixpoint size ( bt : binary_tree nat ) : nat := match bt with | Leaf _ i => i + 1 | Node _ (bt1, bt2) => size bt1 + size bt2 end.
Functional Scheme size_ind := Induction for size Sort Prop.
where the statement size_gt_zero represents the property to be certi ed. The user adds a few commands for proving the statement. We do not give details of the proof here because it is not essential. In our system, this modi cation does not update the original OCaml program because the de nitions of types and functions are left as they are.
Now consider the case where the speci cation of the size function is changed so that it counts the number of leaves as follows: let rec size (bt : int binary_tree) : int = match bt with | Leaf i -> 1 | Node (bt1, bt2) -> size bt1 + size bt2 where we just modify the branch Leaf in the pattern matching of bt to be 1 instead of i + 1. For this modi cation, our system updates only the de nition of the size function as:
Fixpoint size ( bt : binary_tree nat ) : nat := match bt with | Leaf _ i => 1 | Node _ (bt1, bt2) => size bt1 + size bt2 end. and the other descriptions are left as it was. Since our system leaves all proofs of statements as they were, the user might have to modify the proof of the size_gt_zero statement because the de nition of the involved function size is changed. However, in this case, fortunately, any modi cation is not required due to the genericity of the omega tactic that solves Presburger arithmetic formulas. The original proof can be used without changing for this modi cation.
The user may change the type of natural numbers nat into the type of integers Z and replace * in the de nition of inductive data type with -> to make it curried. This modi cation does not a ect updates of the OCaml program but makes it easy to prove its properties in many cases as explained in Section 3.2. In addition, if the termination of recursive de nition is not automatically detected, the user should add the proof by rede ning the function. 3
We design our system so as to meet our requirements through combining four bidirectional transformations as mentioned in Section 1. This section gives a summary of architecture of our system and how we achieve a bidirectional transformation between a Coq script and an OCaml program. 3.1
Our system is based on combination of four bidirectional transformations as shown in Fig. 2 where common data contains shared information between Coq and OCaml ASTs. Two outer bidirectional transformations, between Coq script and Coq AST and between OCaml program and OCaml AST, are described in BiYacc [ZZK+16] where the text side is a source and the AST side is a view. BiYacc makes it possible to modify an AST with preserving comments and indentations in the text. Two inner bidirectional transformations, between Coq AST and common data and between OCaml AST and common data, are described in BiGUL [KZH16] where the AST side is a source and the common data side is a view. BiGUL makes it easy to write a translation between Coq and OCaml because of its put-based semantics. 3.2
Even though Coq and OCaml have similar syntax because of their close relationship, the gap between them is not so small for translating one into another. For example, OCaml allows inlined patterns like let f (x,y) = ... in a function de nition but Coq does not, and Coq allows curried data constructors like Cons: A -> List -> List but OCaml does not. Although such di erences could be ignored just as unsupported notations, our system tries to allow them for exible programming in both Coq and OCaml sides. We give a brief summary for their di erences and how to deal with them in our system. For simplicity, we will explain here the bidirectional translation between Coq and OCaml as it were directly de ned without intermediate common data. The actual translation of our system is done through an intermediate data structure which stores shared information between Coq and OCaml. This is implemented by combining with two bidirectional transformations in BiGUL. Type conversion Since Coq has a more powerful type system than OCaml, the translation from Coq to OCaml either drops some information or merges informative types into a single type. For example, a user-de ned data type in Coq is usually declared as a subtype of Type or Set depending on the usage. This information is dropped in the translation to OCaml but preserved in the update re ection from OCaml. Another example is two types for the numbers in Coq, nat (natural numbers) and Z (integers). Our system translates these types into the same type int in OCaml. The update re ection of this type from OCaml to Coq preserves the original type. Binding variables of the same type Coq has abbreviated syntax for multiple parameters sharing the same type, while OCaml requires to declare a type for each parameter separately. One can write (x y z: ) for (x: )(y: )(z: ) in Coq. In our system, the translation from the separated style to the abbreviated one checks if the consecutive parameters have the same type. For example, consider the case where (x y z:nat) in Coq is translated into (x:int)(y:int)(z:int) in OCaml. When the speci cation in OCaml is changed to (x:int)(y:int)(z:string), our system updates the Coq script as (x y:nat)(z:string).
Inlined parameter patterns OCaml allows to describe a pattern as a parameter in the function de nition like let f (x, y) = x + y, which is not supported in Coq. Our system solves the problem only for a pair pattern. Introducing a new variable x_y, this OCaml program is translated into
Definition f x_y := let (x, y) := x_y in x + y. where two parameters x and y are extracted from x_y by the let binding. Patterns other than pairs in OCaml can be supported in a similar way.
Locally-de ned recursive functions Coq and OCaml have di erent syntax to represent a recursive function in a local context. An expression fix f x := e in Coq is evaluated to a recursive function itself, while an expression let rec f x = e in e0 in OCaml is evaluated by e where f is bound to the recursive function. For Coq-to-OCaml translation, the expression fix f x := e maps into (let rec f x = e in f ) as default. When the expression occurs at the beginning of the let-binding (of the same function name) like let f := (fix f x := e) in e0, the whole expression is translated into let rec f x = e in e0. For OCaml-to-Coq translation, the expression let rec f x = e in e0 is translated into let f := (fix f x := e) in e0.
Curried data constructors Coq allows a curried data constructor like Node in the following de nition.
Inductive binary_tree1 (A: Type): Type := | Leaf : A -> binary_tree1 A | Node : binary_tree1 A -> binary_tree1 A -> binary_tree1 A.
For example, Node (Leaf 1) (Leaf 2) is a binary tree of type binary_tree1 nat. OCaml requires uncurried style for data constructors like type 'a binary_tree2 = | Leaf of 'a | Node of 'a binary_tree2 * 'a binary_tree2 where Node must take a pair of binary trees to construct a binary tree. The type variables are translated into those in the OCaml style. As we have seen in Section 2.2, our system translates into
Inductive binary_tree2 (A: Type): Type := | Leaf : A -> binary_tree2 A | Node : binary_tree2 A * binary_tree2 A -> binary_tree2 A. where the Node constructor is not uncurried. This uncurried de nition for inductive data types is known to be quite harmful for proving the statement in Coq because its induction principle is futile unlike that of the curried type binary_tree1.
To solve this problem, our system allows the users to change the de nition in Coq into the curried one like binary_tree1 without a ecting the re ection to the OCaml programs. Accordingly, every occurrence of Node e1 e2 in Coq is translated into Node(e01,e02) in OCaml where e01 and e02 are appropriate translations of e1 and e2, respectively.
Curried type constructors Coq allows also a curried type constructor like either in the following de nition:
Inductive either (A B: Type): Type := | Left : A -> either A B.
| Right : B -> either A B. corresponding to type ('a, 'b) either = | Left of 'a | Right of 'b in OCaml where polymorphic type variables should be passed as a tuple. Our system assumes that all type constructors of Coq are curried and those of OCaml are uncurried, hence it converts the curried/uncurried style for Coq/OCaml translation.
Function expressions OCaml has special syntax for function expressions function : : : that is equivalent to fun x => match x with : : : end in Coq. This is a convenient syntax sugar for pattern matching functions in OCaml. The translation of this expression into Coq is not so straightforward. Consider the recursive de nition of the fact function:
let rec fact = function 0 -> 1 | n -> n * fact (n - 1) This should not be simply translated into
Fixpoint fact := fun X => match X with 0 => 1 | n => n * fact (n - 1) end. with a fresh variable X because the recursive function must have parameters. Our system solves the problem by translating it into
Fixpoint fact X := match X with 0 => 1 | n => n * fact (n - 1) end. by detecting that the location is the beginning of the body of the recursive function de nition. 3.3
Our system imposes several restrictions to both Coq and OCaml. First, it is for data constructors in Coq. We must use capital names for data constructors and partial application of data constructors are not allowed. Second, user-de ned pre x and in x operators are prohibited in OCaml. This is because of the current limitation of the BiYacc parsers. Additionally, we only support the basic feature of Coq and OCaml. Record, type class, and extending notation are not supported. 4
There are several approaches to certi ed programming by a `unidirectional' translation but in both Coq-toOCaml and OCaml-to-Coq directions. However, we cannot combine these translations for bidirectional certi ed programming we aim for.
For Coq-to-OCaml, we could use the program extraction mechanism [Let08] provided by Coq. Many existing certi ed softwares such as CompCert C compiler [Ler09] were developed in this approach. For OCaml-to-Coq, we could use CFML [Cha11] or CoqOfOCaml [Cla14]. In CFML, all function de nitions in OCaml are translated into Coq axioms, which are never translated into OCaml by the program extraction. In CoqOfOCaml, the type of functions may be changed through translating OCaml to Coq. For example, the translation of a recursive function adds a `fuel' as an additional argument to de ne a corresponding terminating function because Coq does not accept de nitions of non-terminating functions. As the result of the program extraction from the translated function, a function of a di erent type is obtained. Our system does not change the type of functions. The proof of its termination can be added after the translation if Coq fails to detect the evidence of the termination. Adding the proof will not a ect the function de nition in OCaml when re ecting the modi cation. We proposed bidirectional certi ed programming which have advantages of both proof-and-extract and importand-proof approaches, where a Coq script and an OCaml program are modi ed alternatingly. Every modi cation in one side is re ected into another side with preserving the original description as much as possible by combining four bidirectional transformations. This makes it easy to prove properties in Coq and to write programs in OCaml. Our system succeeded to translate more than half (27 out of 48) of function de nitions in the List module provided in OCaml. Most of the failures are caused by lack of exception handling in Coq.
The current implementation still imposes restriction on the style of programming, e.g., data constructors in Coq should be capitalized, user-de ned in x operators are prohibited. Although some of these restrictions come from the limitation of BiYacc, it will be soon resolved in near future.
Additionally, our system itself is not developed by certi ed programming, that is, the translation is not guaranteed to preserve the semantics. This problem is common with the program extraction of Coq [Let08] in the proof-and-extract approach and existing work [Cha11, Cla14] in the import-and-proof approach. We wish for BiGUL to have a facility for formally-speci ed semantic preserving translation because our bidirectional translation strongly relies on BiGUL. Or otherwise we should take an approach in a way similar to the success of CakeML [MO14] which achieves certi ed extraction from HOL.
The authors would like to thank anonymous reviewers for their many insightful suggestions and corrections. They are also indebted to Hsiang-Shang Ko, Zhenjiang Hu, and Mirai Ikebuchi for their helpful comments. [BC10] [Cla14] [KZH16] [Let08] [MO14]
Arthur Chargueraud. Characteristic Formulae for the Veri cation of Imperative Programs. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 418{430, New York, NY, USA, 2011. ACM.
Guillaume Claret. Coq of OCaml. In Proceedings of the 2014 OCaml Workshop, OCaml '14, 2014. Coq Development Team. The Coq Reference Manual, version 8.6 edition, 2016. URL: http://coq. inria.fr/.
Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. BiGUL: A Formally Veri ed Core Language for Putback-based Bidirectional Programming. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM '16, pages 61{72, New York, NY, USA, 2016. ACM.
Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program., 24(2-3):284{315, 2014.