diff options
Diffstat (limited to 'site/posts/CoqffiIntro.org')
| -rw-r--r-- | site/posts/CoqffiIntro.org | 516 |
1 files changed, 0 insertions, 516 deletions
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org deleted file mode 100644 index e85f4b4..0000000 --- a/site/posts/CoqffiIntro.org +++ /dev/null @@ -1,516 +0,0 @@ -#+TITLE: ~coqffi~ in a Nutshell - -#+SERIES: ./Coqffi.html -#+SERIES_NEXT: ./CoqffiEcho.html - -For each entry of a ~cmi~ file (a /compiled/ ~mli~ file), ~coqffi~ -tries to generate an equivalent (from the extraction mechanism -perspective) Coq definition. In this article, we walk through how -~coqffi~ works. - -Note that we do not dive into the vernacular commands ~coqffi~ -generates. They are of no concern for users of ~coqffi~. - -#+BEGIN_EXPORT html -<nav id="generate-toc"></nav> -<div id="history">site/posts/CoqffiIntro.org</div> -#+END_EXPORT - -* Getting Started - -** Requirements - -The latest version of ~coqffi~ (~1.0.0~beta7~ at the time of writing) -is compatible with OCaml ~4.08~ up to ~4.12~, and Coq ~8.12~ up top -~8.13~. If you want to use ~coqffi~, but have incompatible -requirements of your own, feel free to -[[https://github.com/coq-community/coqffi/issues][submit an issue]]. - -** Installing ~coqffi~ - -The recommended way to install ~coqffi~ is through the -[[https://coq.inria.fr/opam/www][Opam Coq Archive]], in the ~released~ -repository. If you haven’t activated this repository yet, you can use -the following bash command. - -#+BEGIN_SRC sh -opam repo add coq-released https://coq.inria.fr/opam/released -#+END_SRC - -Then, installing ~coqffi~ is as simple as - -#+BEGIN_SRC sh -opam install coq-coqffi -#+END_SRC - -You can also get the source from -[[https://github.com/coq-community/coqffi][the upstream ~git~ -repository]]. The ~README~ provides the necessary pieces of -information to build it from source. - -** Additional Dependencies - -One major difference between Coq and OCaml is that the former is pure, -while the latter is not. Impurity can be modeled in pure languages, -and Coq does not lack of frameworks in this respect. ~coqffi~ -currently supports two of them: [[https://github.com/Lysxia/coq-simple-io][~coq-simple-io~]] and [[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]]. It is -also possible to use it with [[https://github.com/DeepSpec/InteractionTrees][Interaction Trees]], albeit in a less -direct manner. - -* Primitive Types - -~coqffi~ supports a set of primitive types, /i.e./, a set of OCaml -types for which it knows an equivalent type in Coq. The list is the -following (the Coq types are fully qualified in the table, but not in -the generated Coq module as the necessary ~Import~ statement are -generated too). - -| OCaml type | Coq type | -|-------------------+-------------------------------| -| =bool= | =Coq.Init.Datatypes.bool= | -| =char= | =Coq.Strings.Ascii.ascii= | -| =int= | =CoqFFI.Data.Int.i63= | -| ='a list= | =Coq.Init.Datatypes.list a= | -| ='a Seq.t= | =CoqFFI.Data.Seq.t= | -| ='a option= | =Coq.Init.Datatypes.option a= | -| =('a, 'e) result= | =Coq.Init.Datatypes.sum= | -| =string= | =Coq.Strings.String.string= | -| =unit= | =Coq.Init.Datatypes.unit= | -| =exn= | =CoqFFI.Exn= | - -The =i63= type is introduced by the =CoqFFI= theory to provide signed -primitive integers to Coq users. They are implemented on top of the -(sadly unsigned) Coq native integers introduced in Coq -~8.10~. Hopefully, the =i63= type will be deprecated once [[https://github.com/coq/coq/pull/13559][signed -primitive integers find their way to Coq upstream]]. - -When processing the entries of a given interface model, ~coqffi~ will -check that they only use these types, or types introduced by the -interface module itself. - -Sometimes, you may encounter a situation where you have two interface -modules ~b.mli~ and ~b.mli~, such that ~b.mli~ uses a type introduced -in ~a.mli~. To deal with this scenario, you can use the ~--witness~ -flag to generate ~A.v~. This will tell ~coqffi~ to also generate -~A.ffi~; this file can then be used when generating ~B.v~ thanks to -the ~-I~ option. Furthermore, for ~B.v~ to compile the ~--require~ -option needs to be used to ensure the ~A~ Coq library (~A.v~) is -required. - -To give a more concrete example, given ~a.mli~ - -#+BEGIN_SRC ocaml -type t -#+END_SRC - -and ~b.mli~ - -#+BEGIN_SRC ocaml -type a = A.t -#+END_SRC - -To generate ~A.v~, we can use the following commands: - -#+BEGIN_SRC bash -ocamlc a.mli -coqffi --witness -o A.v a.cmi -#+END_SRC - -Which would generate the following axiom for =t=. - -#+BEGIN_SRC coq -Axiom t : Type. -#+END_SRC - -Then, generating ~B.v~ can be achieved as follows: - -#+BEGIN_SRC bash -ocamlc b.mli -coqffi -I A.ffi -ftransparent-types -r A -o B.v b.cmi -#+END_SRC - -which results in the following output for =v=: - -#+BEGIN_SRC coq -Require A. - -Definition u : Type := A.t. -#+END_SRC - -* Code Generation - -~coqffi~ distinguishes five types of entries: types, pure values, -impure primitives, asynchronous primitives, exceptions, and -modules. We now discuss how each one of them is handled. - -** Types - -By default, ~coqffi~ generates axiomatized definitions for each type -defined in a ~.cmi~ file. This means that src_ocaml[:exports -code]{type t} becomes src_coq[:exports code]{Axiom t : Type}. -Polymorphism is supported, /i.e./, src_ocaml[:exports code]{type 'a t} -becomes src_coq[:exports code]{Axiom t : forall (a : Type), Type}. - -It is possible to provide a “model” for a type using the =coq_model= -annotation, for instance for reasoning purposes. For instance, -we can specify that a type is equivalent to a =list=. - -#+BEGIN_SRC ocaml -type 'a t [@@coq_model "list"] -#+END_SRC - -This generates the following Coq definition. - -#+BEGIN_SRC coq -Definition t : forall (a : Type), Type := list. -#+END_SRC - -It is important to be careful when using the =coq_model= annotation. -More precisely, the fact that =t= is a =list= in the “Coq universe” -shall not be used while the implementation phase, only the -verification phase. - -Unamed polymorphic type parameters are also supported. In presence of -such parameters, ~coqffi~ will find it a name that is not already -used. For instance, - -#+BEGIN_SRC ocaml -type (_, 'a) ast -#+END_SRC - -becomes - -#+BEGIN_SRC ocaml -Axiom ast : forall (b : Type) (a : Type), Type. -#+END_SRC - -Finally, ~coqffi~ has got an experimental feature called -~transparent-types~ (enabled by using the ~-ftransparent-types~ -command-line argument). If the type definition is given in the module -interface, then ~coqffi~ tries to generates an equivalent definition -in Coq. For instance, - -#+BEGIN_SRC ocaml -type 'a llist = - | LCons of 'a * (unit -> 'a llist) - | LNil -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Inductive llist (a : Type) : Type := -| LCons (x0 : a) (x1 : unit -> llist a) : llist a -| LNil : llist a. -#+END_SRC - -Mutually recursive types are supported, so - -#+BEGIN_SRC ocaml -type even = Zero | ESucc of odd -and odd = OSucc of even -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Inductive odd : Type := -| OSucc (x0 : even) : odd -with even : Type := -| Zero : even -| ESucc (x0 : odd) : even. -#+END_SRC - -Besides, ~coqffi~ supports alias types, as suggested in this write-up -when we discuss witness files. - -The ~transparent-types~ feature is *experimental*, and is currently -limited to variant types. It notably does not support -records. Besides, it may generate incorrect Coq types, because it does -not check whether or not the [[https://coq.inria.fr/refman/language/core/inductive.html#positivity-condition][positivity condition]] is -satisfied. - -** Pure values - -~coqffi~ decides whether or not a given OCaml values is pure or impure -with the following heuristics: - -- Constants are pure -- Functions are impure by default -- Functions with a =coq_model= annotation are pure -- Functions marked with the =pure= annotation are pure -- If the ~pure-module~ feature is enabled (~-fpure-module~), - then synchronous functions (which do not live inside the [[https://ocsigen.org/lwt/5.3.0/manual/manual][~Lwt~]] - monad) are pure - -Similarly to types, ~coqffi~ generates axioms (or definitions, if the -~coq_model~ annotation is used) for pure values. Then, - -#+BEGIN_SRC ocaml -val unpack : string -> (char * string) option [@@pure] -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Axiom unpack : string -> option (ascii * string). -#+END_SRC - -Polymorphic values are supported. - -#+BEGIN_SRC ocaml -val map : ('a -> 'b) -> 'a list -> 'b list [@@pure] -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b. -#+END_SRC - -Again, unamed polymorphic type are supported, so - -#+BEGIN_SRC ocaml -val ast_to_string : _ ast -> string [@@pure] -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Axiom ast_to_string : forall (a : Type), string. -#+END_SRC - -** Impure Primitives - -~coqffi~ reserves a special treatment for /impure/ OCaml functions. -Impurity is usually handled in pure programming languages by means of -monads, and ~coqffi~ is no exception to the rule. - -Given the set of impure primitives declared in an interface module, -~coqffi~ will (1) generate a typeclass which gathers these primitives, -and (2) generate instances of this typeclass for supported backends. - -We illustrate the rest of this section with the following impure -primitives. - -#+BEGIN_SRC ocaml -val echo : string -> unit -val scan : unit -> string -#+END_SRC - -where =echo= allows writing something the standard output, and =scan= -to read the standard input. - -Assuming the processed module interface is named ~console.mli~, the -following Coq typeclass is generated. - -#+BEGIN_SRC coq -Class MonadConsole (m : Type -> Type) := { echo : string -> m unit - ; scan : unit -> m string - }. -#+END_SRC - -Using this typeclass and with the additional support of an additional -=Monad= typeclass, we can specify impure computations which interacts -with the console. For instance, with the support of ~ExtLib~, one can -write. - -#+BEGIN_SRC coq -Definition pipe `{Monad m, MonadConsole m} : m unit := - let* msg := scan () in - echo msg. -#+END_SRC - -There is no canonical way to model impurity in Coq, but over the years -several frameworks have been released to tackle this challenge. - -~coqffi~ provides three features related to impure primitives. - -*** ~simple-io~ - -When this feature is enabled, ~coqffi~ generates an instance of the -typeclass for the =IO= monad introduced in the ~coq-simple-io~ package - -#+BEGIN_SRC coq -Axiom io_echo : string -> IO unit. -Axiom io_scan : unit -> IO string. - -Instance IO_MonadConsole : MonadConsole IO := { echo := io_echo - ; scan := io_scan - }. -#+END_SRC - -It is enabled by default, but can be disabled using the -~-fno-simple-io~ command-line argument. - -*** ~interface~ - -When this feature is enabled, ~coqffi~ generates an inductive type -which describes the set of primitives available, to be used with -frameworks like [[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]] or -[[https://github.com/DeepSpec/InteractionTrees][Interactions Trees]] - -#+BEGIN_SRC coq -Inductive CONSOLE : Type -> Type := -| Echo : string -> CONSOLE unit -| Scan : unit -> CONSOLE string. - -Definition inj_echo `{Inject CONSOLE m} (x0 : string) : m unit := - inject (Echo x0). - -Definition inj_scan `{Inject CONSOLE m} (x0 : unit) : m string := - inject (Scan x0). - -Instance Inject_MonadConsole `{Inject CONSOLE m} : MonadConsole m := - { echo := inj_echo - ; scan := inj_scan - }. -#+END_SRC - -Providing an instance of the form src_coq[:exports code]{forall i, -Inject i M} is enough for your monad =M= to be compatible with this -feature (see for instance -[[https://github.com/ANSSI-FR/FreeSpec/blob/master/theories/FFI/FFI.v][how -FreeSpec implements it]]). - -*** ~freespec~ - -When this feature in enabled, ~coqffi~ generates a semantics for the -inductive type generated by the ~interface~ feature. - -#+BEGIN_SRC coq -Axiom unsafe_echo : string -> unit. -Axiom unsafe_scan : uint -> string. - -Definition console_unsafe_semantics : semantics CONSOLE := - bootstrap (fun a e => - local match e in CONSOLE a return a with - | Echo x0 => unsafe_echo x0 - | Scan x0 => unsafe_scan x0 - end). -#+END_SRC - -** Asynchronous Primitives - -~coqffi~ also reserves a special treatment for /asynchronous/ -primitives —/i.e./, functions which live inside the ~Lwt~ monad— when -the ~lwt~ feature is enabled. - -The treatment is very analoguous to the one for impure primitives: (1) -a typeclass is generated (with the ~_Async~ suffix), and (2) an -instance for the ~Lwt~ monad is generated. Besides, an instance for -the “synchronous” primitives is also generated for ~Lwt~. If the -~interface~ feature is enabled, an interface datatype is generated, -which means you can potentially use Coq to reason about your -asynchronous programs (using FreeSpec and alike, although the -interleaving of asynchronous programs in not yet supported in -FreeSpec). - -By default, the type of the ~Lwt~ monad is ~Lwt.t~. You can override -this setting using the ~--lwt-alias~ option. This can be useful when -you are using an alias type in place of ~Lwt.t~. - -** Exceptions - -OCaml features an exception mechanism. Developers can define their -own exceptions using the ~exception~ keyword, whose syntax is similar -to constructors definition. For instance, - -#+BEGIN_SRC ocaml -exception Foo of int * bool -#+END_SRC - -introduces a new exception =Foo= which takes two parameters of type -=int= and =bool=. =Foo (x, y)= constructs of value of type =exn=. - -For each new exceptions introduced in an OCaml module, ~coqffi~ -generates (1) a so-called “proxy type,” and (2) conversion functions -to and from this type. - -Coming back to our example, the “proxy type” generates by ~coqffi~ is - -#+BEGIN_SRC coq -Inductive FooExn : Type := -| MakeFooExn (x0 : i63) (x1 : bool) : FooExn. -#+END_SRC - -Then, ~coqffi~ generates conversion functions. - -#+BEGIN_SRC coq -Axiom exn_of_foo : FooExn -> exn. -Axiom foo_of_exn : exn -> option FooExn. -#+END_SRC - -Besides, ~coqffi~ also generates an instance for the =Exn= typeclass -provided by the =CoqFFI= theory: - -#+BEGIN_SRC coq -Instance FooExn_Exn : Exn FooExn := - { to_exn := exn_of_foo - ; of_exn := foo_of_exn - }. -#+END_SRC - -Under the hood, =exn= is an [[https://caml.inria.fr/pub/docs/manual-ocaml/extensiblevariants.html][extensible datatype]], and how ~coqffi~ -supports it will probably be generalized in future releases. - -Finally, ~coqffi~ has a minimal support for functions which may raise -exceptions. Since OCaml type system does not allow to identify such -functions, they need to be annotated explicitely, using the -=may_raise= annotation. In such a case, ~coqffi~ will change the -return type of the function to use the =sum= Coq inductive type. - -For instance, - -#+BEGIN_SRC ocaml -val from_option : 'a option -> 'a [@@may_raise] [@@pure] -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Axiom from_option : forall (a : Type), option a -> sum a exn. -#+END_SRC - -** Modules - -Lastly, ~coqffi~ supports OCaml modules described within ~mli~ files, -when they are specify as ~module T : sig ... end~. For instance, - -#+BEGIN_SRC ocaml -module T : sig - type t - - val to_string : t -> string [@@pure] -end -#+END_SRC - -becomes - -#+BEGIN_SRC coq -Module T. - Axiom t : Type. - - Axiom to_string : t -> string. -End T. -#+END_SRC - -As of now, the following construction is unfortunately *not* -supported, and will be ignored by ~coqffi~: - -#+BEGIN_SRC coq -module S = sig - type t - - val to_string : t -> string [@@pure] -end - -module T : S -#+END_SRC - -* Moving Forward - -~coqffi~ comes with a comprehensive man page. In addition, the -interested reader can proceed to the next article of this series, -which explains how [[./CoqffiEcho.org][~coqffi~ can be used to easily implement an echo -server in Coq]]. |