The Blag

Logic, Computer Graphics, OCaml, Rust, etc.

10 Mar 15

Simple Refinement Types for OCaml

For more than one year, vulnerabilies in software (especially pervasive C software) have been disclosed at an alarmingly high rate. I love OCaml, which is definitely safer, but still has gaps left open. I believe formal verification, albeit a very powerful tool, is not mature enough for most programmers (too difficult to use, requires too much efforts), so I'm thinking about alternative solutions that would be more lightweight to define and use, but would still increase the confidence in source code.

So here is a draft of a relatively simple extension to OCaml, that allows to specify more invariants in types without requiring a full-fledged proof system. It's purely hypothetical and I did not implement it (nor don't I plan to do it, not before the end of my PhD). The purpose is to propose a conservative extension of OCaml with a type system that can represent more complex invariants, without putting too much of a burden on the user, in a way so adding annotations to existing programs incrementally is feasible and even easy.

The idea relies on refinement types, noted { ty | F } where ty is a regular OCaml type and F is a boolean formula (read "type ty such that F holds). A regular type ty in a signature is short for { ty | true }.

Now, the boolean formula F is inductively built from conjunction and, disjunction or, negation not, and atoms. The atoms, for a type ty, are OCaml values of type ty -> bool (actually, of a type that can be specialized into ty -> bool, to handle polymorphism. e.g. if ty = int list, and p : 'a list -> bool, then { ty | p } is valid). The predicates of type ty -> bool should be referentially transparent and terminating (although we don't try to enforce this).

Type Checking

Whenever f : { ty | p } -> foo is called on an expression e : { ty | q }, a boolean proof obligation q => p is issued to a SAT-solver. If the proof obligation fails, either an error is emitted, or a warning is issued and some runtime check of the form assert (p e); f e replaces f e.

Applying f to some "static" value c (e.g. the constant 2) that has a bare type should, ideally, check p c at compile-time. A runtime check can also be used if the compile-time check proves too complicated.

It would also be interesting to expose to the type checker some logic properties about predicates, in the form of rules: given two predicates p : ty -> bool and q : ty -> bool, a rule would say p => q (for any x : ty, p x implies q x). The type checker can use such affirmations to help solving the proof obligations generated by functions calls. The rules could be checked either by adding runtime checks, or using random testing, or by formal proving.

Type Inference

Given a function let f x = <body>, the type inference infers the type tau of x normally, but it also collects every points where a function of type {tau | p} is called on x so the final type of x is { tau | p1 and p2 and ... and pn} (in the absence of any annotation, we find the empty conjunction, that is, true, that is, x : tau. Hence the conservative extension). The return value collects the annotations in a similar way, but joins them using a disjunction.

In the .mli, the user can express more tight constraints on the signature of functions and values, same as phantom types or private aliases.

Runtime Checking

The assertions that refine a type can be checked at runtime, if some compiler flag is enabled or disabled (similar to -no-assert). Runtime checks for a function f : { ty1 | p1 } -> { ty2 | p2 } look like this:

let f x =
  assert (p1 x);
  (* body of f *)
  let res = ..... in
  assert (p2 res);
  res

Usage

The refinement types as defined here are very simple, yet they can serve to encode interesting invariants in the large (proving programs in the small is left to more ambitious tools: extraction from Coq, why3, CFML etc.)

Examples:

  • a balanced predicate for AVL trees
module type AVL_SET = sig
    type elt

    type t = E | N of t * int * elt * t

    val balanced : t -> bool

    val empty : {t | balanced }
    (* empty tree *)

    val add : {t | balanced} -> elt -> {t | balanced}

    val as_balanced : t -> {t | balanced} option
    (* check the tree is balanced *)

    val random : (Random.State.t -> elt) -> Random.State.t -> t
    (* combine with as_balanced to generate balanced trees *)
end
  • sorting arrays
val sorted : 'a array -> bool

val as_sorted : 'a array -> {'a array | sorted} option
(* check the array is sorted, and cast it *)

val sort : 'a array -> {'a array | sorted}

val binary_search : {'a array | sorted} -> 'a -> int option
(* Expects the array to be sorted *)
  • encoding basic state machines (à la phantom types, but without redefining the type)
type t

val at_start : t -> bool
val at_middle : t -> bool
val at_stop : t -> bool

val start : unit -> {t | at_start}

val loop : {t | at_start or at_middle} -> {t | at_middle}

val stop : {t | at_start or at_middle} -> {t | at_stop}

Combining Properties

It can work on third-party types without changing them: a function accepting int also accepts any {int | F}. Some row polymorphism is probably needed to combine properties. For instance, the predicate as_sorted: 'a array -> {'a array | sorted} option should really have the type as_sorted : {'a array | 'p} -> {'a array | 'p and sorted} option not to lose any other properties the array already has.

Maybe assert (p x); e on a value x: {ty | q} should modify the type of x to {ty | p and q} in e, or require that x has type {ty | p} if x is an argument. This would make the idiom val as_foo : ty -> {ty | foo} option redundant.

Limitations

How to parametrize predicates with values, even known statically? Would be extremely useful for invariants parametrized by comparison function, for instance. Maybe the values can be existentially quantified in argument positions, and made opaque in return value position…

Conclusion

This is clearly just a rough idea, in dire need of refinement (no pun intended). However, I think it is both really simple on the type-checking/type inference side (compared to true formal verification) and easy to use, as a more powerful version of private aliases or phantom types to express simple invariants in type signatures. I would love to hear the opinion of people who have a good knowledge of OCaml's type-{checker, system}.

Edit: instead of a SAT-solver, a BDD library (binary decision diagrams) might be simpler to use in the context of a type-checker.

I got many interesting pointers from people: