The labours of Sisyphus

Real-world programs change. Consider two versions of Seq.to_array (taken from the Containers library):

Old version

let to_array s =
  match s () with
  | Nil -> [| |]
  | Cons (x, _) ->
    let n = length s in
    let a = Array.make n x in
    let _ = iteri
        (fun i x -> a.(i) <- x)
        s in
    a

New version

let to_array s =
  let len, ls =
    fold (fun (i,acc) x -> 
      (i + 1, x :: acc)) (0, []) s in
  match ls with
  | [] -> [| |]
  | init::rest ->
    let a = Array.make len init in
    let idx = len - 2 in
    List.fold_left (fun i x -> 
      a.(i) <- x;
      i - 1) idx rest
    a

Radically different implementations...

...how can we know it's correct?

We manually verified the
old version in Coq (using CFML).

Lemma to_array_old_spec :
  forall A (l : list A) (s : func),
  SPEC (to_array s)
  PRE [Seq l s]
  POST (fun a => a ~> Array l).
Proof using (All).
(* .. *)
(* .. *)
(* .. *)
Qed.

Sisyphus was able to automatically repair the proof to work for the new program.

Why Sisyphus?

1

Scalable

We evaluated Sisyphus on 14 OCaml programs, 10 of which were taken from real-world OCaml libraries (Jane Street's Core, Inria's Menhir, Containers e.t.c.).

2

Elegant

Sisyphus's repair procedure builds some of the most elegant truths of Computer Science, the Curry-Howard correspondence, to automatically and efficiently infer invariants for programs.

3

Free

Sisyphus is built from the ground up using Free (as in freedom) technologies, and is licensed under the ultimate AGPLv3+ libre license to ensure the Freedoms of its users are preserved!

Get rolling with Sisyphus!

You can learn more about Sisyphus by reading our paper, or try it out using our artefact, or built and extend it from the source code:

Read the Paper

Run the Artefact

Get the Code