Proofs Debugging 2

[EmilyOng]

No description provided.

[EmilyOng]

✘ Associativity of append

let rec append xs ys =
  match xs with
  | [] -> ys
  | x :: xs' -> x :: append xs' ys

let append_append1 xs ys zs = append (append xs ys) zs
let append_append2 xs ys zs = append xs (append ys zs)

(*@
  lemma append_associativity_lemma xs ys zs res =
    append_append1(xs, ys, zs, res) <: ex r; append_append2(xs, ys, zs, r); ens res=r
@*)

This generates the following induction hypothesis:

IH: forall [xs; ys; zs; res; res],
      append_append1(xs,ys,zs,res) <: ex r;
      append_append2(xs, ys, zs, r); Norm(res=r)

Successful Dafny verification using structural induction directly

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

function append<T>(xs: List<T>, ys: List<T>): List<T>
{
    match xs {
        case Nil => ys
        case Cons(x, xs') => Cons(x, append(xs', ys))
    }
}

lemma {:induction false} AppendAssociativeLemma<T>(xs: List<T>, ys: List<T>, zs: List<T>)
ensures append(append(xs, ys), zs) == append(xs, append(ys, zs))
{
    var LHS := append(append(xs, ys), zs);
    var RHS := append(xs, append(ys, zs));
    match xs {
        case Nil =>
            // LHS
            // == append(append(Nil, ys), zs)
            // == append(ys, zs) (by definition of append)
            // == append(Nil, append(ys, zs)) (by definition of append)
            // == RHS
            assert LHS == RHS;
        case Cons(x, xs') =>
            // LHS
            // == append(append(xs, ys), zs)
            // == append(append(Cons(x, xs'), ys), zs) (by substitution)
            // == append(Cons(x, append(xs', ys)), zs) (by rewriting)
            // == Cons(x, append(append(xs', ys), zs)) (by rewriting)
            // == Cons(x, append(xs', append(ys, zs))) (by induction hypothesis)
            // == append(Cons(x, xs'), append(ys, zs)) (by rewriting)
            // == append(xs, append(ys, zs))
            // == RHS

            AppendAssociativeLemma(xs', ys, zs);
            assert LHS == RHS;
    }
}

[EmilyOng]

✘ Foldr exists

let rec foldr f li acc =
  match li with 
  | [] -> acc 
  | x :: xs -> 
    let acc' = f x acc in 
    foldr f xs acc'

let rec exists xs f =
  match xs with
  | [] -> false
  | x :: xs' -> f x || exists xs' f

let foldr_exists xs pred
(*@ ex r; exists(xs, pred, r); ens res=r @*)
= let f x acc = acc || pred x in
  foldr f xs false

(Dafny: todo. Find out the required lemmas)

[EmilyOng]

✔ Simple closure with effect

let closure_with_effects ()
(*@
  ex i j; ens i->2*j->4/\res=5
@*)
= let i = ref 1 in
  let j = ref 2 in
  let f () =
    i := !i + 1;
    j := !j + 2;
    5 in
  f ()

[EmilyOng]

✘ Partial specification of insertion sort

let rec is_sorted xs =
  match xs with
  | [] -> true
  | x :: xs' -> (
    match xs' with
    | [] -> true
    | x' :: xs'' -> x <= x' && is_sorted xs'
  )

let rec insert_in_sorted_list v xs
= match xs with
  | [] -> [v]
  | x :: xs' -> if v <= x then v :: xs else x :: insert_in_sorted_list v xs'

let insert_in_sorted_list_ v xs
(*@
  ex t1 t2 r;
  is_sorted(xs, t1); req t1=true;
  insert_in_sorted_list(v, xs, r);
  is_sorted(r, t2); ens t2=true/\res=r
@*)
= insert_in_sorted_list v xs

Dafny verification

// Adapted from Program Proofs Chapter 8

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

// Insertion Sort

function insertionSort(xs: List<int>): List<int>
{
    match xs {
        case Nil => Nil
        case Cons(x, xs') => insertInSortedList(x, insertionSort(xs'))
    }
}

function insertInSortedList(v: int, xs: List<int>): List<int>
{
    match xs {
        case Nil => Cons(v, Nil)
        case Cons(x, xs') => if v <= x then Cons(v, xs) else Cons(x, insertInSortedList(v, xs'))
    }

}

ghost predicate IsSorted(xs: List<int>) {
    match xs {
        case Nil => true
        case Cons(x, Nil) => true
        case Cons(x, Cons(x', xs')) => x <= x' && IsSorted(Cons(x', xs'))
    }
}

lemma {:induction false} InsertInSortedListLemma(v: int, xs: List<int>)
requires IsSorted(xs)
ensures IsSorted(insertInSortedList(v, xs))
{
    match xs {
        case Nil =>
        // Only need to consider the case where v > x
        case Cons(x, xs') => InsertInSortedListLemma(v, xs');
    }
}

lemma {:induction false} InsertionSortLemma(xs: List<int>)
ensures IsSorted(insertionSort(xs))
{
    match xs {
        case Nil =>
        case Cons(x, xs') =>
            // Ensures that the tail is sorted
            InsertionSortLemma(xs');
            // Ensures that the resultant list is sorted
            InsertInSortedListLemma(x, insertionSort(xs'));
    }
}

It seems like the problem is whether a (pure) predicate can be used in the precondition? For example:

let is_one x = x = 1

let identity x = x

let one x
(*@
  ex t; is_one(x, t); req t=true; <~~ Cannot write this
  ens res=1
@*)
= identity x

[EmilyOng]

Unfolding bounds

W.r.t. #2 (comment) filter:

let rec filter xs pred =
  match xs with
  | [] -> []
  | y :: ys -> if pred y then y :: filter ys pred else filter ys pred

let is_positive x = x > 0

let positives ()
(*@ ens res=[1; 2] @*)
= filter [0; 1; 2; (-1)] is_positive

We can pass this specification using an unfolding bound of 5. But, increasing the unfolding bound fails existing tests:

   ALL OK!
 
   $ check test_lists.ml
-  ALL OK!
+  FAILED: map_inc_false
 
   $ check test_match.ml
   ALL OK!
@@ -77,7 +77,7 @@ ALL OK!
   ALL OK!
 
   $ check ../examples/map.ml
-  ALL OK!
+  FAILED: cl_map
 
   $ check ../examples/length.ml
   ALL OK!
@@ -86,10 +86,10 @@ ALL OK!
   ALL OK!
 
   $ check ../examples/fold.ml
-  ALL OK!

   $ check ../examples/iter.ml
-  ALL OK!
+  FAILED: build_fill
 
   $ check ../examples/exception.ml
   ALL OK!

Similarly, for_each:

let rec foreach xs f =
  match xs with
  | [] -> ()
  | y :: ys -> f y; foreach ys f

let incr v = v := !v + 1

let do_nothing v = ()

let foreach_example x (* FIXME *)
(*@ ex v1; req x->v1; ens x->v1 @*)
(*
  Can be temporarily fixed by increasing the unfolding bound for do_nothing.
  This workaround does not work for incr.
*)
= foreach [x] do_nothing;

[EmilyOng]

✘ Invoking lemmas

let rec length lst =
  match lst with
  | [] -> 0
  | x :: xs -> 1 + length xs

(*@
  lemma length_empty res =
    length([], res) <: ens res=0
@*)

let rec snoc lst x =
  match lst with
  | [] -> [x]
  | y :: ys -> y :: snoc ys x

let snoc_empty_length x
(*@ ens res=1 @*)
= length (snoc [] x)

Error trace

Fatal error: exception Invalid_argument("List.map2")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Hipprover__Entail.unify_lem_lhs_args in file "parsing/entail.ml", line 39, characters 9-45

In the following flow:

ex v103 v104 v72; req emp; ens is_nil([])=true/\v72=cons(x, [])/\tail(v72)=v104/\is_cons(v72)=true; length(v104, v103); ex v70; req emp; Norm(res=1+v103)
<:
req emp; Norm(res=1)

Unification between lemma args ([]) (missing res) and concrete args (v104, v103) fails due to an unhandled invalid argument exception, because of incompatible lengths for List.map2.

[EmilyOng]

We use the following filter function, tested at commit cb12a48

let rec filter xs pred =
  match xs with
  | [] -> []
  | y :: ys -> if pred y then y :: filter ys pred else filter ys pred

OK ✅	Failed ❌
let positives xs (*@ ex r; ens res=r @*) = let is_positive x = x > 0 in filter xs is_positive	let is_positive x = x > 0 let positives xs (*@ ex r; ens res=r @*) = filter xs is_positive

[EmilyOng]

Ok ✅	Failed ❌
let rec integers n = if n <= 0 then [] else n :: integers (n - 1) let foo n (*@ req n>=2 @*) = integers n	let rec integers n = if n <= 0 then [] else n :: integers (n - 1) let goo n = integers n let foo n (*@ req n>=2 @*) = goo n

[EmilyOng]

UPDATE (13 Jan): Fixed

✘ Scoping issue

let foo ()
(*@ ens res=5 @*) (* Fails. But, "ens res=3" passes *)
= let x = 3 in
  let f x = x in
  f 5

[EmilyOng]

✘ Specifying length directly

let rec length xs (* FIXME *)
(*@ ens res>=0 @*)
= match xs with
  | [] -> 0
  | x :: xs1 -> 1 + length xs1

let length_positive xs
(*@ ens res>=0 @*)
= length xs