Getting started

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-system
This will install the main library coq-io and some basic effects coq-io-system to interact with your operating system.

Write a Hello World

Open your favorite Coq editor and type: 
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.

More examples

The full documentation of the coq-io-system library is available on v2.3.0.

Your name

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.

Cat

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.

Uname

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.

Use concurrency

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.

The effects system

What is the definition of a computation with IO and how does this work?

Effects

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.

Computations

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.

Compilation

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.

Verification by use cases

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.

Use cases

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:

  • the program displays "What is your name?" on the terminal;
  • the program asks to read a new line;
  • the user answers by the string name;
  • the program displays a message containing the string name.

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.

Runs

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:

  • the run of C.Ret e is the computation e with an empty environment;
  • the run of C.Call c is this call together with an environment given by an answer to this call;
  • the run of C.Let e1 e2 is a sequence of a run of e1 and of a run of e2;
  • the run of C.Choose e1 e2 is either a run of e1 or a run of e2;
  • the run of 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.

A symbolic debugger

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.

Validate a use case

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".

Follow the project on GitHub.