coq-io

KO | EN

gitlite — search

#javascript #react #typescript #go #android #rust #deep-learning #macos #kubernetes #awesome-list #vue #pytorch #security #ios

(★ 10)

Modeling I/O in Coq using free monads

coq-io Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Free monads for modeling IO in Coq

A small example of how to model various kinds of IO using a _free monad_ over primitive operations in Coq, including how to extract and run code written in this style.

In [FSCQ](https://github.com/mit-pdos/fscq), we need to model programs that have access to a disk. We write our code in a shallow embedding of programs with primitives for reading and writing to and from the disk. This shallow embedding is a free monad over the desired, primitive disk operations. We give the monadic programs a semantics as a transition system from one state to another. Programs are values in a monad, and the type argument gives the type of a return value for finished programs. The state is manipulated by the primitives, whose behavior is also specified in the semantics.

The code here has a similar model, but is written in a more general way and attempts to expose only the details needed to understand the concepts and get a simple example running. It works almost the same way as FSCQ disk programs, but is phrased in terms of accessing a single input file with a simple single-byte API.

# Overview

The Coq model has a very generic definition `prog`, which takes an argument `Op : Type -> Type` giving the type constructor for the primitives (the type argument indicates the return type). Primitives are chained using `Ret` and `Bind`. Then there's an execution semantics, which is expresses the behavior of a program in terms of how it transforms some state type and what return values are allowed (the semantics are relational, so non-determinism is allowed). These semantics specify how `Ret` and `Bind` work and take a parameter `step` for the behavior of the primitives.

As an example, we define `FileOp`, a set of primitives for access to a single input file. These operations have a semantics, in terms of a state which is simply a list of bytes (which we call a `File`). Then there are two example programs of type `prog FileOp T`: one copies a byte, the other is a fixpoint `countNewlines` that counts newlines in the file.

On the Haskell side, any given `prog` extracts to a Haskell data type, a sort of abstract syntax tree of operations, but with Haskell functions extracted from Gallina implementing important functionality. Due to a limitation with Coq extraction, we extract `prog` specialized to `FileOp`.

Then we have some non-Coq components that won't be under verification. These are fairly simple: there's an "interpreter" that runs extracted `prog FileOp`'s, and then a driver program that calls the interpreter on the `countNewlines` program, with some command line parsing and file setup that falls outside of the Coq model.

# Compiling

Run `make` to compile the Coq code and generate the Haskell library. This compiles `Prog.v` with Coq and extracts to `word-count/src/Prog.hs`.

From there, we have a hand-written interpreter (`word-count/src/Interpreter.hs`), and a driver program (`word-count/app/Main.hs`) around the `countNewlines` example in `Prog.v`.

To compile the driver program and produce the `word-count` binary, use Haskell Stack. Stack requires a one-time setup to download the compiler:

```
cd word-count
stack setup
```

Then you can compile and run the binary:

```
stack build
stack exec word-count -- <file>
```

This should give the same output as `wc -l <file>`.

coq-io

coq-io Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

coq-io

coq-io Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README