Mostly Automated Proof Repair of Verified Libraries View Paper
Programs evolve, so why shouldn't proofs?

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


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

Radically different implementations... 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).
(* .. *)
(* .. *)
(* .. *)

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

Mostly Automated Proof Repair

Why Sisyphus?



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



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.



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: