## VerifyThis 2017: Tree Buffer

solution to VerifyThis 2017 challenge 4

Authors: Jean-Christophe Filliâtre

Tools: Why3

References: VerifyThis @ ETAPS 2017

see also the index (by topic, by tool, by reference, by year)

# VerifyThis @ ETAPS 2017 competition Challenge 4: Tree Buffer

See https://formal.iti.kit.edu/ulbrich/verifythis2017/

Author: Jean-Christophe FilliĆ¢tre (CNRS)

```(* default implementation *)
module Spec

use export int.Int
use export list.List

type buf 'a = { h: int; xs: list 'a }

let rec function take (n: int) (l: list 'a) : list 'a =
match l with
| Nil -> Nil
| Cons x xs -> if n = 0 then Nil
else Cons x (take (n-1) xs) end

let function empty (h: int) : buf 'a =
{ h = h; xs = Nil }

let function add (x: 'a) (b: buf 'a) : buf 'a =
{ b with xs = Cons x b.xs }

let function get (b: buf 'a) : list 'a =
take b.h b.xs

(* the following lemma is useful to verify both Caterpillar and
RealTime implementations below *)

use list.Append
use list.Length

let rec lemma take_lemma (l1 l2 l3: list 'a) (n: int)
requires { 0 <= n <= length l1 }
ensures  { take n (l1 ++ l2) = take n (l1 ++ l3) }
variant  { l1 }
= match l1 with Nil -> ()
| Cons _ ll1 -> if n > 0 then take_lemma ll1 l2 l3 (n-1) end

end

(* task 1 *)
module Caterpillar

use Spec
use list.Append
use list.Length

type cat 'a = {
ch: int;
xs: list 'a;
xs_len: int;
ys: list 'a;
ghost b: buf 'a; (* the model is the default implementation *)
} invariant {
b.h = ch /\
xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
} by {
ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
}

(* for the three operations, the postcondition uses the default
implementation *)

let cat_empty (h: int) : cat 'a
requires { 0 < h }
ensures  { result.b = empty h }
= { ch = h; xs = Nil; xs_len = 0; ys = Nil;
b = empty h }

let cat_add (x: 'a) (c: cat 'a) : cat 'a
ensures { result.b = add x c.b }
= if c.xs_len = c.ch - 1 then
{ c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
b = add x c.b }
else
{ c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
b = add x c.b }

let cat_get (c: cat 'a) : list 'a
ensures { result = get c.b }
= take c.ch (c.xs ++ c.ys)

end

(* task 2 *)

(* important note: Why3 assumes a garbage collector and so it makes
little sense to implement the real time solution in Why3.

Yet I stayed close to the C++ code, with a queue to_delete where
lists are added when discarded and then destroyed progressively
(at most two conses at a time) in process_queue.

The C++ code seems to be missing the insertion into to_delete,
which I added to rt_add; see my comment below.
*)

module RealTime

use Spec
use list.Append
use list.Length

(* For technical reasons, the global queue cannot contain
polymorphic values, to we assume values to be of some
abstract type "elt". Anyway, the C++ code assumes integer
elements. *)
type elt

(* not different from the Caterpillar implementation
replacing 'a with elt everywhere *)
type rt = {
ch: int;
xs: list elt;
xs_len: int;
ys: list elt;
ghost b: buf elt; (* the model is the default implementation *)
} invariant {
b.h = ch /\
xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
} by {
ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
}

(* garbage collection *)
use queue.Queue as Q
(* note: when translating Why3 to OCaml, this module is mapped
to OCaml's Queue module, where push and pop are O(1) *)

val to_delete: Q.t (list elt)

let de_allocate (l: list elt)
= match l with Nil -> () | Cons _ xs -> Q.push xs to_delete end

let process_queue ()
= try
if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete);
if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete)
with Q.Empty -> absurd end

(* no difference wrt Caterpillar *)
let rt_empty (h: int) : rt
requires { 0 < h }
ensures  { result.b = empty h }
= { ch = h; xs = Nil; xs_len = 0; ys = Nil;
b = empty h }

(* no difference wrt Caterpillar *)
let rt_get (c: rt) : list elt
ensures { result = get c.b }
= take c.ch (c.xs ++ c.ys)

(* this is where we introduce explicit garbage collection
1. process_queue is called first (as in the C++ code)
2. when ys is discarded, it is added to the queue (which
seems to be missing in the C++ code) *)
let rt_add (x: elt) (c: rt) : rt
ensures { result.b = add x c.b }
= process_queue ();
if c.xs_len = c.ch - 1 then begin
Q.push c.ys to_delete;
{ c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
b = add x c.b }
end else
{ c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
b = add x c.b }

end
```

# Why3 Proof Results for Project "verifythis_2017_tree_buffer"

## Theory "verifythis_2017_tree_buffer.Spec": fully verified

 Obligations Alt-Ergo 2.0.0 Eprover 1.8-001 Z3 4.4.0 Z3 4.5.0 VC take_lemma --- --- --- --- split_goal_right VC take_lemma.0 0.01 --- 0.02 --- VC take_lemma.1 0.01 --- 0.02 --- VC take_lemma.2 --- --- --- --- split_goal_right VC take_lemma.2.0 --- 0.01 --- --- VC take_lemma.2.1 --- --- --- 0.74 VC take_lemma.2.2 0.01 --- --- ---