## VerifyThis 2017: Tree Buffer

solution to VerifyThis 2017 challenge 4

**Authors:** Jean-Christophe Filliâtre

**Topics:** Data Structures / List Data Structure

**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

download ZIP archive

# Why3 Proof Results for Project "verifythis_2017_tree_buffer"

## Theory "verifythis_2017_tree_buffer.Spec": fully verified

Obligations | Alt-Ergo 2.1.0 | Eprover 1.8-001 | Z3 4.12.2 | ||

VC for take_lemma | --- | --- | --- | ||

split_goal_right | |||||

variant decrease | 0.01 | --- | 0.01 | ||

precondition | 0.01 | --- | 0.01 | ||

postcondition | --- | --- | --- | ||

split_goal_right | |||||

postcondition | --- | 0.01 | --- | ||

postcondition | 0.01 | --- | --- | ||

postcondition | --- | --- | 0.01 |

## Theory "verifythis_2017_tree_buffer.Caterpillar": fully verified

Obligations | Alt-Ergo 2.1.0 | CVC4 1.4 | ||||

VC for cat | 0.00 | --- | ||||

VC for cat_empty | 0.01 | --- | ||||

VC for cat_add | --- | --- | ||||

split_goal_right | ||||||

precondition | --- | --- | ||||

split_goal_right | ||||||

VC for cat_add | 0.01 | --- | ||||

VC for cat_add | 0.01 | --- | ||||

VC for cat_add | 0.01 | --- | ||||

VC for cat_add | --- | 1.28 | ||||

precondition | --- | --- | ||||

split_goal_right | ||||||

VC for cat_add | 0.01 | --- | ||||

VC for cat_add | 0.00 | --- | ||||

VC for cat_add | 0.01 | --- | ||||

VC for cat_add | --- | --- | ||||

introduce_premises | ||||||

VC for cat_add | --- | --- | ||||

inline_goal | ||||||

VC for cat_add | 0.01 | --- | ||||

postcondition | 0.01 | --- | ||||

VC for cat_get | 0.00 | --- |

## Theory "verifythis_2017_tree_buffer.RealTime": fully verified

Obligations | Alt-Ergo 2.1.0 | CVC4 1.4 | CVC4 1.6 | ||

VC for rt | 0.00 | --- | --- | ||

VC for process_queue | 0.01 | --- | --- | ||

VC for rt_empty | 0.01 | --- | --- | ||

VC for rt_get | 0.01 | --- | --- | ||

VC for rt_add | --- | --- | --- | ||

split_goal_right | |||||

precondition | --- | --- | --- | ||

split_goal_right | |||||

VC for rt_add | 0.00 | --- | --- | ||

VC for rt_add | 0.01 | --- | --- | ||

VC for rt_add | 0.01 | --- | --- | ||

VC for rt_add | --- | Timeout (5.00s) | 0.13 | ||

postcondition | 0.01 | --- | --- | ||

precondition | 0.03 | --- | --- | ||

postcondition | 0.01 | --- | --- |