To install the Coq.io library, enable the Coq OPAM repository:
opam repo add coq-released https://coq.inria.fr/opam/released
and run:
opam install -j4 -v coq-io-systemThis will install the main library
coq-io
and some basic effects coq-io-system
to interact with your operating system.
Require Import Coq.Lists.List. Require Import Io.All. Require Import Io.System.All. Require Import ListString.All. Import ListNotations. Import C.Notations. (** The classic Hello World program. *) Definition hello_world (argv : list LString.t) : C.t System.effect unit := System.log (LString.s "Hello world!").
We load some libraries and write the hello_world
program by calling the System.log
function to print a message on the terminal. The return type of the program is C.t System.effect unit
, which means this is an impure computation with the system effect and returning a value of type unit
. The impure computations are the computations which are not purely functional, in the sense they do some effects, like IO or modifying a state variable. The system effect is an effect we use to do IO with the system. The command-line arguments are given by the list of strings argv
, but are not used here.
To compile the hello_world
program to generate an OCaml file main.ml
, add the lines:
Definition main := Extraction.launch hello_world. Extraction "extraction/main" main.
We compile and run main.ml
with:
ocamlbuild main.native -use-ocamlfind -package io-system ./main.native
This should display Hello world!
on the terminal.
The full documentation of the coq-io-system
library is available on v2.3.0.
The following program reads a name on the command-line and answers "hello" to this name:
(** Ask for the user name and answer hello. *) Definition your_name (argv : list LString.t) : C.t System.effect unit := do! System.log (LString.s "What is your name?") in let! name := System.read_line in match name with | None => ret tt | Some name => System.log (LString.s "Hello " ++ name ++ LString.s "!") end.
We see here how to compose impure computations in sequence with the do!
and let!
keywords. The construct:
let! x := e1 in e2
executes e1
, assigns the result to x
and then executes e2
. The do!
is a syntactic sugar for a let!
without a variable x
, so for the case of e1
returning the unit
value. We use the System.read_line
function which reads a new line on the standard input. If the read_line
operation fails, we returns the pure value tt
of type unit
using the ret
operator, else we print the user name on the terminal. We run this program as before by compilation to OCaml.
This program opens a file and displays its content:
(** Display the content of a file. *) Definition cat (argv : list LString.t) : C.t System.effect unit := match argv with | [_; file_name] => let! content := System.read_file file_name in match content with | None => System.log (LString.s "Cannot read the file.") | Some content => System.log content end | _ => System.log (LString.s "Expected one parameter.") end.
It is analogous to the cat
Unix command. It uses the command-line argument to get the file name to display, and then read the file with System.read_file
.
This program wrap the uname
command to display the operating system kind and the type of machine:
Require Import Coq.ZArith.ZArith. (** A wrapper for the `uname` command. *) Definition uname (argv : list LString.t) : C.t System.effect unit := let! os := System.eval [LString.s "uname"; LString.s "-o"] in let! machine := System.eval [LString.s "uname"; LString.s "-m"] in match (os , machine) with | (Some (0%Z, os, _), Some (0%Z, machine, _)) => do! System.log (LString.s "OS: " ++ LString.trim os) in System.log (LString.s "Machine: " ++ LString.trim machine) | _ => ret tt end.
We use the function System.eval
to evaluate a command and get its status code and output. If the two uname
calls are successful, we retrieve the OS and machine names and display them. The 0%Z
stands for the zero in the type Z
of the relative integers. A null value means by convention that the commands were successful.
In order not to freeze, interactive programs usually need to run many IO operations in parallel. Consider for example an application which must keep a reactive user interface while doing slow network operations.
To run two operations in parallel, we use the join
operator:
join : C.t E A -> C.t E B -> C.t E (A * B)
with join x y
concurrently computing the couple of results for the computations x
and y
.
In the following program we concurrently run two sleep operations of 4 and 2 seconds:
(** Do two sleep operations. *) Definition double_sleep (argv : list LString.t) : C.t System.effect unit := let! _ : unit * unit := join (let! _ := System.eval [LString.s "sleep"; LString.s "4"] in System.log (LString.s "Task of 4 seconds ended.")) (let! _ := System.eval [LString.s "sleep"; LString.s "2"] in System.log (LString.s "Task of 2 seconds ended.")) in ret tt.
The output is:
Task of 2 seconds ended. Task of 4 seconds ended.
and the total execution time is 4 seconds. If the sleeps were done sequentially:
(** Do two sleep operations (sequential). *) Definition double_sleep_seq (argv : list LString.t) : C.t System.effect unit := let! _ := System.eval [LString.s "sleep"; LString.s "4"] in do! System.log (LString.s "Task of 4 seconds ended.") in let! _ := System.eval [LString.s "sleep"; LString.s "2"] in System.log (LString.s "Task of 2 seconds ended.").
the execution time would be of 6 seconds and the output:
Task of 4 seconds ended. Task of 2 seconds ended.
What is the definition of a computation with IO and how does this work?
An effect describes a set of IO or impure operations. An effect is declared by an element of type Effect.t
:
Module Effect. Record t := New { command : Type; answer : command -> Type }. End Effect.
This record contains a type of command
, a set of operations to communicate with the outer world, and a dependent type of answer
, the type of answers given by the system to a command.
For example, for an effect with print
and read_line
operations to communicate with the command-line, the declaration could be:
Inductive command : Type := | Print (message : LString.t) | ReadLine. Definition answer (c : command) : Type := match c with | Print _ => unit | ReadLine => LString.t end. Definition effect : Effect.t := Effect.New command answer.
A command is a Print message
or a ReadLine
. The answer for a Print
is of type unit
, the answer for a ReadLine
is of type LString.t
. Notice that we only declare the effect, the definition of how to actually execute it is given latter during compilation. Most effects are declared this way, with a sum type for the command type. A composition of two effects is made up by combining their command sum types.
The computations are used to write programs with IO by assembling pure Coq expressions with external calls to the system. A computation returning a value of type A
with the effect E
lives in the inductive type C.t E A
:
Module C. Inductive t (E : Effect.t) : Type -> Type := | Ret : forall (A : Type) (x : A), t E A | Call : forall (command : Effect.command E), t E (Effect.answer E command) | Let : forall (A B : Type), t E A -> (A -> t E B) -> t E B | Choose : forall (A : Type), t E A -> t E A -> t E A | Join : forall (A B : Type), t E A -> t E B -> t E (A * B). End C.
A computation can be:
Ret e
: the pure expression e
;Call c
: the call of the command c
, waiting for an answer of type answer c
from the system;Let e1 e2
: the sequential composition and binding of e1
and e2
. The term e2
is a function, applied to the result of the computation e1
. We used the notation let! x := e1 in e2
for Let e1 (fun x => e2)
;Choose e1 e2
: either e1
or e2
. The way the choice is made is not specified. In practice, it can be the first computation to terminate;Join e1 e2
: the couple of computations e1
and e2
, concurrently executed.As for the definition of Effect.t
, this definition is abstract: nothing is said about the implementation of these five primitives till compilation. The main advantage is that we do not need to introduce any axioms to reason about IO.
The Haskell user can recognize here the definition of a monad, with the return being the Ret
and the bind being the Let
:
Ret : A -> C.t E A Let : C.t E A -> (A -> C.t E B) -> C.t E B
As you can see, it is possible to lift a pure expression of type A
to a computation of type C.t E A
with the Ret
constructor, but it is impossible to do the reverse. The only way to access the result of a computation is by providing a function returning another computation, using the constructor Let
. This corresponds to the intuition that a program containing a program with IO is also a program with IO, so the property of being with IO is hereditary.
In order to be executed, the computations are compiled into OCaml programs with IO. This compilation is done by customizing the extraction mechanism used to compile pure Coq expressions to pure OCaml programs. The effects and computation primitives are extracted to explicit Lwt constructs. Lwt is a popular library for asynchronous IO in OCaml. This compilation phase is not formally verified.
How to exploit the Coq system to verify our programs?
A popular technique to specify interactive programs with a lot of IO is to define a set of use cases. Basically, a use case is a scenario of execution of the program, defined as a list of interaction steps between the program and its external world.
Let us take the previous example of your_name
:
(** Ask for the user name and answer hello. *) Definition your_name (argv : list LString.t) : C.t System.effect unit := do! System.log (LString.s "What is your name?") in let! name := System.read_line in match name with | None => ret tt | Some name => System.log (LString.s "Hello " ++ name ++ LString.s "!") end.
This program is very simple, but the techniques we will describe can apply to any program with IO, like a web application, a system script, ...
A use case for a valid execution is:
This use case is parametrized by a string name. To validate the use case, we could write a test program interacting with your_name
, answering the name string to the read_line
request and checking that the program outputs are as expected. The limitation of this method is that we can only test a finite number of name values, instead of all the possible strings.
To cover all the use case instances, Coq.io introduces the notion of run. A run describes one execution of a computation, by programming the behavior of the computation's environment in a particular execution. Said otherwise, a run contains two programs: the computation itself and its environment, with typing rules ensuring that the environment answers to each request of the computation.
A run is of type Run.t e v
, where e
is a computation and v
is the expected result of the computation. We formally define the type Run.t
by:
Module Run. Inductive t : forall {E : Effect.t} {A : Type}, C.t E A -> A -> Type := | Ret : forall {E A} (x : A), t (C.Ret (E := E) A x) x | Call : forall E (c : Effect.command E) (answer : Effect.answer E c), t (C.Call (E := E) c) answer | Let : forall {E A B} {c_x : C.t E A} {x : A} {c_f : A -> C.t E B} {y : B}, t c_x x -> t (c_f x) y -> t (C.Let A B c_x c_f) y | ChooseLeft : forall {E A} {c_x1 c_x2 : C.t E A} {x1 : A}, t c_x1 x1 -> t (C.Choose A c_x1 c_x2) x1 | ChooseRight : forall {E A} {c_x1 c_x2 : C.t E A} {x2 : A}, t c_x2 x2 -> t (C.Choose A c_x1 c_x2) x2 | Join : forall {E A B} {c_x : C.t E A} {x : A} {c_y : C.t E B} {y : B}, t c_x x -> t c_y y -> t (C.Join A B c_x c_y) (x, y). End Run.
Seemingly complex, this definition follows the one of the computations adding the definition of an environment. You do not need to read this definition carefully, you just need to get the intuition that:
C.Ret e
is the computation e
with an empty environment;C.Call c
is this call together with an environment given by an answer to this call;C.Let e1 e2
is a sequence of a run of e1
and of a run of e2
;C.Choose e1 e2
is either a run of e1
or a run of e2
;C.Join e1 e2
is the run of e1
and a run of e2
. Even if these two runs may actually interact, we are only interested in their projections on e1
and e2
.A use case can be formalized by a set of runs, with one run per instance of the use case. For our your_name
example, we will define a set of runs run_your_name_ok
parametrized by the variable name
to formalize our use case.
To give a run for a computation by directly writing its definition is quite cumbersome. Instead, we exploit the tactic mode of Coq to define a run by interacting with the computation like in a debugger. The breakpoints of this debugger are the constructors of the computation. By stepping through the beakpoints, you will provide a well-typed answer for each call of the computation.
Let's start by declaring run_your_name_ok
:
Definition run_your_name_ok (argv : list LString.t) (name : LString.t) : Run.t (your_name argv) tt.
This run is parametrized by the program arguments argv
and the user name name
. This is a run of type Run.t (your_name argv) tt
, running the program your_name
with the parameters argv
and expecting the unit value tt
as a final answer. The Coq system answers us:
1 subgoals argv : list LString.t name : LString.t ______________________________________(1/1) Run.t (your_name argv) tt
This means that we must define our run, and that we are at the beginning of the program your_name
. This program starts with a do! e1 in e2
, which corresponds to the constructor C.Let
applied to e1
and fun _ => e2
. We step into this C.Let
by applying the Run.Let
constructor:
apply Run.Let.
but get an error:
Error: Cannot infer the implicit parameter x of Let.
Coq needs to know the expected result of the left-hand side of the C.Let
. We know it must be tt
, but we let Coq infer this value with eapply
:
eapply Run.Let.
We get two subgoals, one for each side of the C.Let
:
2 subgoal argv : list LString.t name : LString.t ______________________________________(1/2) Run.t (log (LString.s "What is your name?")) ?29 ______________________________________(2/2) Run.t (let!name0 : option LString.t := read_line in match name0 with | Some name1 => log (LString.s "Hello " ++ name1 ++ LString.s "!") | None => ret tt end) tt
The library coq-io-system
provides a run Run.log_ok
for the logging of a string s
. This run executes the computation System.log s
checking that the printed string is s
. We apply this run:
apply (Run.log_ok (LString.s "What is your name?")).
and get one remaining goal:
1 subgoals argv : list LString.t name : LString.t ______________________________________(1/1) Run.t (let!name0 : option LString.t := read_line in match name0 with | Some name1 => log (LString.s "Hello " ++ name1 ++ LString.s "!") | None => ret tt end) tt
Like for the do!
, we step into the let!
with a:
eapply Run.Let.
to get:
2 subgoal argv : list LString.t name : LString.t ______________________________________(1/2) Run.t read_line ?38 ______________________________________(2/2) Run.t match ?38 with | Some name0 => log (LString.s "Hello " ++ name0 ++ LString.s "!") | None => ret tt end tt
The variable ?38
, the result of read_line
, is unknown at this point. We run the read_line
command by using the Run.read_line_ok
run with the parameter name
to answer the name of the user:
apply (Run.read_line_ok name).
We get:
1 subgoals argv : list LString.t name : LString.t ______________________________________(1/1) Run.t match Some name with | Some name0 => log (LString.s "Hello " ++ name0 ++ LString.s "!") | None => ret tt end tt
The variable ?38
has been replaced by Some name
. Once again, we use the run Run.log_ok
to run a System.log
:
apply (Run.log_ok (_ ++ name ++ _)).
The values of the underscores _
are automatically inferred by Coq:
No more subgoals.
We conclude:
Defined.
The full definition of the run is then:
Definition run_your_name_ok (argv : list LString.t) (name : LString.t) : Run.t (your_name argv) tt. eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")). eapply Run.Let. apply (Run.read_line_ok name). apply (Run.log_ok (_ ++ name ++ _)). Defined.
This run is the Coq formalization of our use case for the valid executions of the computation your_name
.
As another example, here is the formalization of the use case in which the System.read_line
command fails (because of a terminal error for instance):
Definition run_your_name_error (argv : list LString.t) : Run.t (your_name argv) tt. eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")). eapply Run.Let. apply Run.read_line_error. apply Run.Ret. Defined.
Once a use case has been formalized, we would like to formally verify it. There is actually... nothing to do, because we know that our runs must be valid since they are well-typed. If we have tried to define an invalid run like:
Definition run_your_name_ok (argv : list LString.t) (name : LString.t) : Run.t (your_name argv) tt. eapply Run.Let. apply (Run.log_ok (LString.s "What is your name? blabla#@!")) eapply Run.Let. apply (Run.read_line_ok name). apply (Run.log_ok (_ ++ name ++ _)). Defined.
we would have gotten an error at definition time:
Error: Impossible to unify "Run.t (log (LString.s "What is your name? blabla#@!")) tt" with "Run.t (log (LString.s "What is your name?")) ?29".