## Tree reconstruction from a list of leave depths

Problem 4 of the second verified software competition.

The ZIP file below contains both the source code, the Why3 proof session file and the Coq scripts of the proofs made in Coq. The Why3 source code is then displayed, followed by a summary of the proofs.

**Authors:** Jean-Christophe Filliâtre / Andrei Paskevich

**Topics:** Trees

**Tools:** Why3

**References:** The 2nd Verified Software Competition

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

download ZIP archive

(* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 4: Tree Reconstruction Build a binary tree from a list of leaf depths, if any This is a purely applicative implementation, using immutable lists from Why3's standard library. *) module Tree use export int.Int use export list.List use export list.Append type tree = Leaf | Node tree tree (* the list of leaf depths for tree t, if root is at depth d *) function depths (d: int) (t: tree) : list int = match t with | Leaf -> Cons d Nil | Node l r -> depths (d+1) l ++ depths (d+1) r end (* lemmas on depths *) lemma depths_head: forall t: tree, d: int. match depths d t with Cons x _ -> x >= d | Nil -> false end let rec lemma depths_unique (t1 t2: tree) (d: int) (s1 s2: list int) requires { depths d t1 ++ s1 = depths d t2 ++ s2 } variant { t1 } ensures { t1 = t2 && s1 = s2 } = let d' = d+1 in match t1,t2 with | Leaf,Leaf -> () | Node t11 t12, Node t21 t22 -> depths_unique t11 t21 d' (depths d' t12 ++ s1) (depths d' t22 ++ s2); depths_unique t12 t22 d' s1 s2 | Leaf, (Node t _) | (Node t _), Leaf -> match depths d' t with | Nil -> absurd | Cons x _ -> assert { x >= d' } end end lemma depths_prefix: forall t: tree, d1 d2: int, s1 s2: list int. depths d1 t ++ s1 = depths d2 t ++ s2 -> d1 = d2 lemma depths_prefix_simple: forall t: tree, d1 d2: int. depths d1 t = depths d2 t -> d1 = d2 let rec lemma depths_subtree (t1 t2: tree) (d1 d2:int) (s1:list int) requires { depths d1 t1 ++ s1 = depths d2 t2 } variant { t1 } ensures { d1 >= d2 } = assert { depths d2 t2 = depths d2 t2 ++ Nil }; match t1 with | Leaf -> () | Node t3 t4 -> depths_subtree t3 t2 (d1+1) d2 (depths (d1+1) t4 ++ s1) end lemma depths_unique2: forall t1 t2: tree, d1 d2: int. depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2 end module TreeReconstruction use export Tree use import list.Length (* termination of build_rec (below) requires a lexicographic order *) predicate lex (x1 x2: (list int, int)) = let s1, d1 = x1 in let s2, d2 = x2 in length s1 < length s2 || length s1 = length s2 && match s1, s2 with | Cons h1 _, Cons h2 _ -> d2 < d1 <= h1 = h2 | _ -> false end exception Failure (* used to signal the algorithm's failure i.e. there is no tree *) let rec build_rec (d: int) (s: list int) : (tree, list int) variant { (s, d) with lex } ensures { let t, s' = result in s = depths d t ++ s' } raises { Failure -> forall t: tree, s' : list int. depths d t ++ s' <> s } = match s with | Nil -> raise Failure | Cons h t -> if h < d then raise Failure; if h = d then (Leaf, t) else let l, s = build_rec (d+1) s in let r, s = build_rec (d+1) s in (Node l r, s) end let build (s: list int) : tree ensures { depths 0 result = s } raises { Failure -> forall t: tree. depths 0 t <> s } = let t, s = build_rec 0 s in match s with | Nil -> t | _ -> raise Failure end end module Harness use import TreeReconstruction let harness () ensures { result = Node Leaf (Node (Node Leaf Leaf) Leaf) } raises { Failure -> false } = build (Cons 1 (Cons 3 (Cons 3 (Cons 2 Nil)))) let harness2 () ensures { false } raises { Failure -> true } = build (Cons 1 (Cons 3 (Cons 2 (Cons 2 Nil)))) end (* A variant implementation proposed by Jayadev Misra Given the input list [x1; x2; ...; xn], we first turn it into the list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)]. Then, repeatedly, we scan this list from left to right, looking for two consecutive pairs (v1, t1) and (v2, t2) with v1 = v2. Then we replace them with the pair (v1-1, Node t1 t2) and we start again. We stop when there is only one pair left (v,t). Then we must have v=0. The implementation below achieves linear complexity using a zipper data structure to traverse the list of pairs. The left list contains the elements already traversed (thus on the left), in reverse order, and the right list contains the elements yet to be traversed. *) (* Proving termination is quite easy and we do it first (though we could, obviously, do it together with proving correctness) *) module ZipperBasedTermination use import Tree use import list.Length use import list.Reverse exception Failure let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree variant { length left + length right, length right } raises { Failure } = match left, right with | _, Nil -> raise Failure | Nil, Cons (v, t) Nil -> if v = 0 then t else raise Failure | Nil, Cons (v, t) right' -> tc (Cons (v, t) Nil) right' | Cons (v1, t1) left', Cons (v2, t2) right' -> if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right') else tc (Cons (v2, t2) left) right' end end (* Now soundness and completeness *) module ZipperBased use import Tree use import list.Length use import list.Reverse (* the following function generalizes function [depths] to a forest, that is a list of pairs (depth, tree) *) function forest_depths (f: list (int, tree)) : list int = match f with | Nil -> Nil | Cons (d, t) r -> depths d t ++ forest_depths r end (* an obvious lemma on [forest_depths] *) lemma forest_depths_append: forall f1 f2: list (int, tree). forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2 (* to prove completeness, one needs an invariant over the list [left]. The main ingredient is predicate [greedy] below, which states that [d] is distinct from all depths along the left branch of [d1, t1]. *) predicate greedy (d: int) (d1: int) (t1: tree) = d <> d1 /\ match t1 with Leaf -> true | Node l1 _ -> greedy d (d1+1) l1 end (* then we extend it to a list of pairs [(dn,tn); ...; (d2,t2); (d1,t1)] as follows: [greedy d2 d1 t1], [greedy d3 d2 t2], etc. this is inductive predicate [g] *) inductive g (l: list (int, tree)) = | Gnil: g Nil | Gone: forall d: int, t: tree. g (Cons (d, t) Nil) | Gtwo: forall d1 d2: int, t1 t2: tree, l: list (int, tree). greedy d1 d2 t2 -> g (Cons (d1, t1) l) -> g (Cons (d2, t2) (Cons (d1, t1) l)) (* an easy lemma on [g] *) lemma g_append: forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l1 (* key lemma for completeness: whenever we fail because [right] is empty, we have to prove that there is no solution Note: the proof first generalizes the statement as follows: forest_depths ((d1,t1) :: l) <> depths d t + s whenever d < d1 (see the corresponding Coq file) *) lemma right_nil: forall l: list (int, tree). length l >= 2 -> g l -> forall t: tree, d: int. forest_depths (reverse l) <> depths d t (* key lemma for soundness: preservation of the invariant when we move a tree from [right] to [left] *) lemma main_lemma: forall l: list (int, tree), d1 d2: int, t1 t2: tree. d1 <> d2 -> g (Cons (d1, t1) l) -> match t2 with Node l2 _ -> greedy d1 (d2+1) l2 | Leaf -> true end -> g (Cons (d2, t2) (Cons (d1, t1) l)) (* finally, we need a predicate to state that a forest [l] contains only leaves *) predicate only_leaf (l: list (int, tree)) = match l with | Nil -> true | Cons (_, t) r -> t = Leaf /\ only_leaf r end exception Failure let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree requires { (* list [left] satisfies the invariant *) g left /\ (* when [left] has one element, it can't be a solution *) match left with Cons (d1, _) Nil -> d1 <> 0 \/ right <> Nil | _ -> true end /\ (* apart (possibly) from its head, all elements in [right] are leaves; moreover the left branch of [right]'s head already satisfies invariant [g] when consed to [left] *) match right with | Cons (d2, t2) right' -> only_leaf right' /\ match t2 with Node l2 _ -> g (Cons (d2+1, l2) left) | Leaf -> true end | Nil -> true end } variant { length left + 2 * length right } ensures { depths 0 result = forest_depths (reverse left ++ right) } raises { Failure -> forall t: tree. depths 0 t <> forest_depths (reverse left ++ right) } = match left, right with | _, Nil -> raise Failure | Nil, Cons (v, t) Nil -> if v = 0 then t else raise Failure | Nil, Cons (v, t) right' -> tc (Cons (v, t) Nil) right' | Cons (v1, t1) left', Cons (v2, t2) right' -> if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right') else tc (Cons (v2, t2) left) right' end (* Getting function [build] from [tc] is easy: from the list [x1; x2; ...; xn] we simply build the list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)]. Function [map_leaf] below does this. *) function map_leaf (l: list int) : list (int, tree) = match l with | Nil -> Nil | Cons d r -> Cons (d, Leaf) (map_leaf r) end (* two lemmas on [map_leaf] *) lemma map_leaf_depths: forall l: list int. forest_depths (map_leaf l) = l lemma map_leaf_only_leaf: forall l: list int. only_leaf (map_leaf l) let build (s: list int) ensures { depths 0 result = s } raises { Failure -> forall t: tree. depths 0 t <> s } = tc Nil (map_leaf s) end

# Why3 Proof Results for Project "vstte12_tree_reconstruction"

## Theory "vstte12_tree_reconstruction.Tree": fully verified in 0.14 s

Obligations | Alt-Ergo (1.30) | CVC4 (1.4) | Z3 (4.4.1) | |

depths_head | --- | --- | --- | |

induction_ty_lex | ||||

depths_head.1 | 0.02 | --- | --- | |

2. VC for depths_unique | 0.08 | --- | --- | |

depths_prefix | --- | --- | --- | |

induction_ty_lex | ||||

depths_prefix.1 | 0.02 | --- | --- | |

depths_prefix_simple | --- | --- | 0.05 | |

5. VC for depths_subtree | --- | --- | --- | |

split_goal_wp | ||||

1. assertion | 0.01 | --- | --- | |

2. postcondition | 0.04 | --- | --- | |

3. variant decrease | 0.01 | --- | --- | |

4. precondition | 0.01 | --- | --- | |

5. postcondition | 0.02 | --- | --- | |

depths_unique2 | --- | 0.01 | --- |

## Theory "vstte12_tree_reconstruction.TreeReconstruction": fully verified in 0.00 s

Obligations | Alt-Ergo (1.30) | CVC4 (1.4) | Coq (8.6.1) | Z3 (4.4.1) | |

1. VC for build_rec | --- | --- | --- | --- | |

split_goal_wp | |||||

1. exceptional postcondition | 0.00 | --- | --- | --- | |

2. exceptional postcondition | --- | 0.03 | --- | --- | |

3. postcondition | 0.00 | --- | --- | --- | |

4. variant decrease | 0.01 | --- | --- | --- | |

5. variant decrease | 0.02 | --- | --- | --- | |

6. postcondition | 0.01 | --- | --- | --- | |

7. exceptional postcondition | --- | --- | 0.50 | --- | |

8. exceptional postcondition | --- | --- | 0.37 | --- | |

2. VC for build | --- | --- | --- | --- | |

split_goal_wp | |||||

1. postcondition | 0.00 | --- | --- | --- | |

2. exceptional postcondition | --- | 0.13 | --- | --- | |

3. exceptional postcondition | --- | --- | --- | 0.04 |

## Theory "vstte12_tree_reconstruction.Harness": fully verified in 0.38 s

Obligations | Coq (8.6.1) | |

1. VC for harness | --- | |

split_goal_wp | ||

1. postcondition | 0.31 | |

2. VC for harness | 0.29 | |

2. VC for harness2 | 0.38 |

## Theory "vstte12_tree_reconstruction.ZipperBasedTermination": fully verified in 0.00 s

Obligations | Alt-Ergo (1.30) | |

1. VC for tc | --- | |

split_goal_wp | ||

1. variant decrease | 0.00 | |

2. variant decrease | 0.01 | |

3. variant decrease | 0.01 | |

4. variant decrease | 0.01 | |

5. variant decrease | 0.02 |

## Theory "vstte12_tree_reconstruction.ZipperBased": fully verified in 4.17 s

Obligations | Alt-Ergo (1.30) | CVC3 (2.4.1) | CVC4 (1.4) | Coq (8.6.1) | Z3 (4.4.1) | ||

forest_depths_append | --- | --- | --- | 0.48 | --- | ||

g_append | --- | --- | --- | 0.97 | --- | ||

right_nil | --- | --- | --- | 2.67 | --- | ||

main_lemma | 0.02 | --- | --- | --- | --- | ||

5. VC for tc | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. exceptional postcondition | --- | 0.04 | 0.06 | --- | --- | ||

2. postcondition | --- | 0.02 | 0.04 | --- | --- | ||

3. exceptional postcondition | --- | 0.03 | 0.05 | --- | --- | ||

4. variant decrease | 0.01 | --- | --- | --- | --- | ||

5. precondition | 0.08 | --- | --- | --- | --- | ||

6. postcondition | --- | --- | 0.85 | --- | --- | ||

7. exceptional postcondition | --- | --- | 0.52 | --- | --- | ||

8. variant decrease | 0.01 | --- | --- | --- | --- | ||

9. precondition | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. VC for tc | 0.34 | --- | --- | --- | --- | ||

2. VC for tc | 0.01 | --- | --- | --- | --- | ||

3. VC for tc | 0.01 | --- | --- | --- | --- | ||

4. VC for tc | 0.03 | --- | --- | --- | --- | ||

10. postcondition | 0.01 | --- | --- | --- | --- | ||

11. exceptional postcondition | 0.01 | --- | --- | --- | --- | ||

12. variant decrease | 0.01 | --- | --- | --- | --- | ||

13. precondition | 0.21 | --- | --- | --- | --- | ||

14. postcondition | 0.01 | --- | --- | --- | --- | ||

15. exceptional postcondition | 0.01 | --- | --- | --- | --- | ||

16. variant decrease | 0.01 | --- | --- | --- | --- | ||

17. precondition | 0.31 | --- | --- | --- | --- | ||

18. postcondition | --- | --- | 0.84 | --- | --- | ||

19. exceptional postcondition | --- | 2.92 | 0.46 | --- | --- | ||

20. variant decrease | 0.02 | --- | --- | --- | --- | ||

21. precondition | 0.84 | --- | --- | --- | --- | ||

22. postcondition | 0.02 | --- | --- | --- | --- | ||

23. exceptional postcondition | 0.01 | --- | --- | --- | --- | ||

map_leaf_depths | --- | --- | --- | --- | --- | ||

induction_ty_lex | |||||||

map_leaf_depths.1 | --- | --- | --- | --- | 0.04 | ||

map_leaf_only_leaf | --- | --- | --- | --- | --- | ||

induction_ty_lex | |||||||

map_leaf_only_leaf.1 | 0.01 | --- | --- | --- | --- | ||

8. VC for build | 0.03 | --- | --- | --- | --- |