Proofs Debugging 2

[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

```dafny datatype List = Nil | Cons(head: T, tail: List) function append(xs: List, ys: List): List { match xs { case Nil => ys case Cons(x, xs') => Cons(x, append(xs', ys)) } } lemma {:induction false} AppendAssociativeLemma(xs: List, ys: List, zs: List) 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

```dafny // Adapted from Program Proofs Chapter 8 datatype List = Nil | Cons(head: T, tail: List) // Insertion Sort function insertionSort(xs: List): List { match xs { case Nil => Nil case Cons(x, xs') => insertInSortedList(x, insertionSort(xs')) } } function insertInSortedList(v: int, xs: List): List { 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) { 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) 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) 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. https://github.com/EmilyOng/AlgebraicEffect/issues/2#issuecomment-1859026406 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 cb12a488e6f77962937126cce236b076b05d9943

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

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

[EmilyOng]

Ok ✅	Failed ❌
```ocaml let rec integers n = if n <= 0 then [] else n :: integers (n - 1) let foo n (*@ req n>=2 @*) = integers n ```	```ocaml 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