## Koda-Ruskey's algorithm

Topics: Trees

Tools: Why3

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

Koda-Ruskey's algorithm

Authors: Mário Pereira (Université Paris Sud) Jean-Christophe Filliâtre (CNRS)

```module KodaRuskey_Spec

use import map.Map
use import list.List
use import list.Append
use import int.Int

type color = White | Black

type forest =
| E
| N int forest forest

type coloring = map int color

function size_forest (f: forest) : int = match f with
| E -> 0
| N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
end

lemma size_forest_nonneg : forall f.
size_forest f >= 0

predicate mem_forest (n: int) (f: forest) = match f with
| E -> false
| N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
end

predicate between_range_forest (i j: int) (f: forest) =
forall n. mem_forest n f -> i <= n < j

predicate disjoint (f1 f2: forest) =
forall x. mem_forest x f1 -> mem_forest x f2 -> false

predicate no_repeated_forest (f: forest) = match f with
| E -> true
| N i f1 f2 ->
no_repeated_forest f1 && no_repeated_forest f2 &&
not (mem_forest i f1) && not (mem_forest i f2) &&
disjoint f1 f2
end

predicate valid_nums_forest (f: forest) (n: int) =
between_range_forest 0 n f &&
no_repeated_forest f

predicate white_forest (f: forest) (c: coloring) = match f with
| E -> true
| N i f1 f2 ->
c[i] = White && white_forest f1 c && white_forest f2 c
end

predicate valid_coloring (f: forest) (c: coloring) =
match f with
| E -> true
| N i f1 f2 ->
valid_coloring f2 c &&
match c[i] with
| White -> white_forest f1 c
| Black -> valid_coloring f1 c
end
end

function count_forest (f: forest) : int = match f with
| E         -> 1
| N _ f1 f2 -> (1 + count_forest f1) * count_forest f2
end

lemma count_forest_nonneg:
forall f. count_forest f >= 1

predicate eq_coloring (n: int) (c1 c2: coloring) =
forall i. 0 <= i < n -> c1[i] = c2[i]

end

module Lemmas

use import map.Map
use import list.List
use import list.Append
use import int.Int
use import KodaRuskey_Spec

type stack = list forest

predicate mem_stack (n: int) (st: stack) = match st with
| Nil       -> false
| Cons f tl -> mem_forest n f || mem_stack n tl
end

lemma mem_app: forall n st1 "induction" st2.
mem_stack n (st1 ++ st2) -> mem_stack n st1 || mem_stack n st2

function size_stack (st: stack) : int = match st with
| Nil -> 0
| Cons f st -> size_forest f + size_stack st
end

lemma size_stack_nonneg : forall st.
size_stack st >= 0

lemma white_forest_equiv:
forall f c.
white_forest f c <-> (forall i. mem_forest i f -> c[i] = White)

predicate even_forest (f: forest) = match f with
| E -> false
| N _ f1 f2 -> not (even_forest f1) || even_forest f2
end

predicate final_forest (f: forest) (c: coloring) = match f with
| E -> true
| N i f1 f2 ->
c[i] = Black && final_forest f1 c &&
if not (even_forest f1) then white_forest f2 c
else final_forest f2 c
end

predicate any_forest (f: forest) (c: coloring) =
white_forest f c || final_forest f c

lemma any_forest_frame:
forall f c1 c2.
(forall i. mem_forest i f -> c1[i] = c2[i]) ->
(final_forest f c1 -> final_forest f c2) &&
(white_forest f c1 -> white_forest f c2)

predicate unchanged (st: stack) (c1 c2: coloring) =
forall i. mem_stack i st -> c1[i] = c2[i]

predicate inverse (st: stack) (c1 c2: coloring) =
match st with
| Nil -> true
| Cons f st' ->
(white_forest f c1 && final_forest f c2 ||
final_forest f c1 && white_forest f c2) &&
if even_forest f then
unchanged st' c1 c2
else
inverse st' c1 c2
end

predicate any_stack (st: stack) (c: coloring) = match st with
| Nil -> true
| Cons f st -> (white_forest f c || final_forest f c) && any_stack st c
end

lemma any_stack_frame:
forall st c1 c2.
unchanged st c1 c2 ->
any_stack st c1 -> any_stack st c2

lemma inverse_frame:
forall st c1 c2 c3.
inverse   st c1 c2 ->
unchanged st c2 c3 ->
inverse   st c1 c3

lemma inverse_frame2:
forall st c1 c2 c3.
unchanged st c1 c2 ->
inverse   st c2 c3 ->
inverse   st c1 c3

let lemma inverse_any (st: stack) (c1 c2: coloring)
requires { any_stack st c1 }
requires { inverse st c1 c2 }
ensures  { any_stack st c2 }
= ()

lemma inverse_final:
forall f st c1 c2.
final_forest f c1 ->
inverse (Cons f st) c1 c2 ->
white_forest f c2

lemma inverse_white:
forall f st c1 c2.
white_forest f c1 ->
inverse (Cons f st) c1 c2 ->
final_forest f c2

let lemma white_final_exclusive (f: forest) (c: coloring)
requires { f <> E }
ensures  { white_forest f c -> final_forest f c -> false }
= match f with E -> () | N _ _ _ -> () end

lemma final_unique:
forall f c1 c2.
final_forest f c1 ->
final_forest f c2 ->
forall i. mem_forest i f -> c1[i] = c2[i]

let rec lemma inverse_inverse
(st: stack) (c1 c2 c3: coloring)
requires { inverse st c1 c2 }
requires { inverse st c2 c3 }
ensures  { unchanged st c1 c3 }
variant  { st }
= match st with
| Nil -> ()
| Cons E st' -> inverse_inverse st' c1 c2 c3
| Cons f st' -> if even_forest f then () else inverse_inverse st' c1 c2 c3
end

inductive sub stack forest coloring =
| Sub_reflex:
forall f, c. sub (Cons f Nil) f c
| Sub_brother:
forall st i f1 f2 c.
sub st f2 c -> sub st (N i f1 f2) c
| Sub_append:
forall st i f1 f2 c.
sub st f1 c -> c[i] = Black ->
sub (st ++ Cons f2 Nil) (N i f1 f2) c

lemma sub_not_nil:
forall st f c. sub st f c -> st <> Nil

lemma sub_empty:
forall st f0 c. st <> Nil -> sub (Cons E st) f0 c ->
sub st f0 c

lemma sub_mem:
forall n st f c.
mem_stack n st -> sub st f c -> mem_forest n f

lemma sub_weaken1:
forall st i f1 f2 f0 c.
sub (Cons (N i f1 f2) st) f0 c ->
sub (Cons         f2  st) f0 c

lemma sub_weaken2:
forall st i f1 f2 f0 c.
sub (Cons (N i f1 f2) st) f0 c ->
c[i] = Black ->
sub (Cons f1 (Cons f2 st)) f0 c

lemma not_mem_st: forall i f st c.
not (mem_forest i f) -> sub st f c -> not (mem_stack i st)

lemma sub_frame:
forall st f0 c c'.
no_repeated_forest f0 ->
(forall i. not (mem_stack i st) -> mem_forest i f0 -> c'[i] = c[i]) ->
sub st f0 c ->
sub st f0 c'

predicate disjoint_stack (f: forest) (st: stack) =
forall i. mem_forest i f -> mem_stack i st -> false

lemma sub_no_rep: forall f st' f0 c.
sub (Cons f st') f0 c ->
no_repeated_forest f0 ->
no_repeated_forest f

lemma sub_no_rep2: forall f st' f0 c.
sub (Cons f st') f0 c ->
no_repeated_forest f0 ->
disjoint_stack f st'

lemma white_valid: forall f c.
white_forest f c -> valid_coloring f c

lemma final_valid: forall f c.
final_forest f c -> valid_coloring f c

lemma valid_coloring_frame:
forall f c1 c2.
valid_coloring f c1 ->
(forall i. mem_forest i f -> c2[i] = c1[i]) ->
valid_coloring f c2

lemma valid_coloring_set:
forall f i c.
valid_coloring f c ->
not (mem_forest i f) ->
valid_coloring f c[i <- Black]

forall f1 f2: 'a, st1 st2: list 'a.
Cons f1 st1 = st2 ++ Cons f2 Nil ->
st2 <> Nil ->
exists st. st1 = st ++ Cons f2 Nil /\ st2 = Cons f1 st

lemma sub_valid_coloring_f1:
forall i f1 f2 c i1.
no_repeated_forest (N i f1 f2) ->
valid_coloring (N i f1 f2) c ->
c[i] = Black ->
mem_forest i1 f1 ->
valid_coloring f1 c[i1 <- Black] ->
valid_coloring (N i f1 f2) c[i1 <- Black]

lemma sub_valid_coloring:
forall f0 i f1 f2 st c1.
no_repeated_forest f0 ->
valid_coloring f0 c1 ->
sub (Cons (N i f1 f2) st) f0 c1 ->
valid_coloring f0 c1[i <- Black]

lemma sub_Cons_N:
forall f st i f1 f2 c.
sub (Cons f st) (N i f1 f2) c ->
f = N i f1 f2 || (exists st'. sub (Cons f st') f1 c) || sub (Cons f st) f2 c

lemma white_white:
forall f c i.
white_forest f c ->
white_forest f c[i <- White]

let rec lemma sub_valid_coloring_white
(f0: forest) (i: int) (f1 f2: forest) (c1: coloring)
requires { no_repeated_forest f0 }
requires { valid_coloring f0 c1 }
requires { white_forest f1 c1 }
ensures  { forall st. sub (Cons (N i f1 f2) st) f0 c1 ->
valid_coloring f0 c1[i <- White] }
variant  { f0 }
= match f0 with
| E -> ()
| N _ f10 f20 ->
sub_valid_coloring_white f10 i f1 f2 c1;
sub_valid_coloring_white f20 i f1 f2 c1
end

function count_stack (st: stack) : int = match st with
| Nil        -> 1
| Cons f st' -> count_forest f * count_stack st'
end

lemma count_stack_nonneg:
forall st. count_stack st >= 1

use seq.Seq as S

type visited = S.seq coloring

predicate stored_solutions
(f0: forest) (bits: coloring) (st: stack) (v1 v2: visited) =
let n = size_forest f0 in
let start = S.length v1 in
let stop  = S.length v2 in
stop - start = count_stack st &&
(forall j. 0 <= j < start ->
eq_coloring n (S.get v2 j) (S.get v1 j)) &&
forall j. start <= j < stop ->
valid_coloring f0 (S.get v2 j) &&
(forall i. 0 <= i < n -> not (mem_stack i st) ->
(S.get v2 j)[i] = bits[i]) &&
forall k. start <= k < stop -> j <> k ->
not (eq_coloring n (S.get v2 j) (S.get v2 k))

let lemma stored_trans1
(f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
(v1 v2 v3: visited)
requires { valid_nums_forest f0 (size_forest f0) }
requires { 0 <= i < size_forest f0 }
requires { forall j. 0 <= j < size_forest f0 ->
not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
requires { forall j. S.length v1 <= j < S.length v2 ->
(S.get v2 j)[i] = White }
requires { forall j. S.length v2 <= j < S.length v3 ->
(S.get v3 j)[i] = Black }
requires { stored_solutions f0 bits1 (Cons f2 st) v1 v2 }
requires { stored_solutions f0 bits2 (Cons f1 (Cons f2 st)) v2 v3 }
ensures  { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
= ()

let lemma stored_trans2
(f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
(v1 v2 v3: visited)
requires { valid_nums_forest f0 (size_forest f0) }
requires { 0 <= i < size_forest f0 }
requires { forall j. 0 <= j < size_forest f0 ->
not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
requires { forall j. S.length v1 <= j < S.length v2 ->
(S.get v2 j)[i] = Black }
requires { forall j. S.length v2 <= j < S.length v3 ->
(S.get v3 j)[i] = White }
requires { stored_solutions f0 bits1 (Cons f1 (Cons f2 st)) v1 v2 }
requires { stored_solutions f0 bits2 (Cons f2 st) v2 v3 }
ensures  { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
= ()

end

module KodaRuskey

use import seq.Seq as S
use import list.List
use import KodaRuskey_Spec
use import Lemmas
use map.Map as M
use import array.Array
use import int.Int
use import ref.Ref

val map_of_array (a: array 'a) : M.map int 'a
ensures { result = a.elts }

val ghost visited: ref visited

let rec enum (bits: array color) (ghost f0: forest) (st: list forest) : unit
requires { size_forest f0 = length bits }
requires { valid_nums_forest f0 (length bits) }
requires { sub st f0 bits.elts }
requires { st <> Nil }
requires { any_stack st bits.elts }
requires { valid_coloring f0 bits.elts }
variant  { size_stack st, st }
ensures  { forall i.
not (mem_stack i st) -> bits[i] = (old bits)[i] }
ensures  { inverse st (old bits).elts bits.elts }
ensures  { valid_coloring f0 bits.elts }
ensures  { stored_solutions f0 bits.elts st (old !visited) !visited }
= match st with
| Nil ->
absurd
| Cons E st' ->
match st' with
| Nil ->
(* that's where we visit the next coloring *)
assert { valid_coloring f0 bits.elts };
ghost visited := S.snoc !visited (map_of_array bits);
()
| _ ->
enum bits f0 st'
end
| Cons (N i f1 f2 as f) st' ->
assert { disjoint_stack f1 st' };
assert { not (mem_stack i st') };
let ghost visited1 = !visited in
if bits[i] = White then begin
'A:   enum bits f0 (Cons f2 st');
assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in
'B:   bits[i] <- Black;
assert { sub st f0 bits.elts };
assert { white_forest f1 bits.elts };
assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts};
assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts };
'C:   enum bits f0 (Cons f1 (Cons f2 st'));
assert { bits[i] = Black };
assert { final_forest f1 bits.elts };
assert { if not (even_forest f1)
then inverse (Cons f2 st') (at bits 'C).elts bits.elts &&
white_forest f2 bits.elts
else unchanged (Cons f2 st') (at bits 'C).elts bits.elts &&
final_forest f2 bits.elts };
ghost stored_trans1 f0 bits1 (map_of_array bits)
i f1 f2 st' visited1 visited2 !visited
end else begin
assert { if not (even_forest f1) then white_forest f2 bits.elts
else final_forest f2 bits.elts };
'A:   enum bits f0 (Cons f1 (Cons f2 st'));
assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in
'B:   bits[i] <- White;
assert { unchanged (Cons f1 (Cons f2 st'))
(at bits 'B).elts bits.elts };
assert { inverse (Cons f1 (Cons f2 st'))
(at bits 'A).elts bits.elts };
assert { sub st f0 bits.elts };
assert { if even_forest f1 || even_forest f2
then unchanged st' (at bits 'A).elts bits.elts
else inverse st' (at bits 'A).elts bits.elts };
'C:   enum bits f0 (Cons f2 st');
assert { bits[i] = White };
assert { white_forest f  bits.elts };
ghost stored_trans2 f0 bits1 (map_of_array bits)
i f1 f2 st' visited1 visited2 !visited
end
end

let main (bits: array color) (f0: forest)
requires { white_forest f0 bits.elts }
requires { size_forest f0 = length bits }
requires { valid_nums_forest f0 (length bits) }
ensures  { S.length !visited = count_forest f0 }
ensures  { let n = S.length !visited  in
forall j. 0 <= j < n ->
valid_coloring f0 (S.get !visited j) &&
forall k. 0 <= k < n -> j <> k ->
not (eq_coloring (length bits)
(S.get !visited j) (S.get !visited k)) }
= visited := S.empty;
enum bits f0 (Cons f0 Nil)

end

```

Independently, let's prove that count_forest is indeed the number of colorings.

```(* wip
module CountCorrect

use import seq.Seq as S
use map.Map as M
use import map.Const
use import list.List
use import int.Int
use import KodaRuskey_Spec
use import Lemmas
use import ref.Ref

predicate id_forest (f: forest) (c1 c2: coloring) =
forall j. mem_forest j f -> M.get c1 j = M.get c2 j

(* valid coloring, all white outside of f *)
predicate solution (f: forest) (c: coloring) =
valid_coloring f c &&
forall j. not (mem_forest j f) -> M.get c j = White

lemma solution_eq:
forall n f c1 c2.
valid_nums_forest f n ->
solution f c1 -> eq_coloring n c1 c2 -> solution f c2

predicate is_product (i: int) (f1 f2: forest) (c1 c2 r: coloring) =
solution (N i f1 f2) r &&
M.get r i = Black &&
id_forest f1 r c1 &&
id_forest f2 r c2

let product (n: int) (i: int) (f1 f2: forest) (c1 c2: coloring) : coloring
requires { valid_nums_forest (N i f1 f2) n }
requires { solution f1 c1 }
requires { solution f2 c2 }
ensures  { is_product i f1 f2 c1 c2 result }
= let rec copy (acc: coloring) (f: forest)
variant { f }
ensures { forall i. M.get result i =
if mem_forest i f then M.get c2 i else M.get acc i }
= match f with
| E -> acc
| N i2 left2 right2 ->
M.set (copy (copy acc left2) right2) i2 (M.get c2 i2)
end
in
let c = copy c1 f2 in
M.set c i Black

lemma solution_product:
forall n i f1 f2 c1 c2 c.
valid_nums_forest (N i f1 f2) n ->
solution f1 c1 -> solution f2 c2 ->
is_product i f1 f2 c1 c2 c -> solution (N i f1 f2) c

predicate solutions (n: int) (f: forest) (s: seq coloring) =
(forall j. 0 <= j < length s -> solution f s[j]) &&
(* colorings are disjoint *)
(forall j. 0 <= j < length s ->
forall k. 0 <= k < length s -> j <> k ->
not (eq_coloring n s[j] s[k]))

let product_all (n: int) (i: int) (f1 f2: forest) (s1 s2: seq coloring)
: seq coloring
requires { valid_nums_forest (N i f1 f2) n }
requires { solutions n f1 s1 }
requires { solutions n f2 s2 }
ensures  { solutions n (N i f1 f2) result }
ensures  { forall j. 0 <= j < length s1 ->
forall k. 0 <= k < length s2 ->
is_product i f1 f2 s1[j] s2[k] result[j * length s2 + k] }
ensures  { length result = length s1 * length s2 }
= let s = ref empty in
for j = 0 to length s1 - 1 do
invariant { length !s = j * length s2 }
invariant { solutions n (N i f1 f2) !s }
invariant { forall j' k'. 0 <= j' < j -> 0 <= k' < length s2 ->
let c = !s[j' * length s2 + k'] in
is_product i f1 f2 s1[j'] s2[k'] c }
for k = 0 to length s2 - 1 do
invariant { length !s = j * length s2 + k }
invariant { solutions n (N i f1 f2) !s }
invariant { forall j' k'. 0 <= j' < j && 0 <= k' < length s2
|| j' = j && 0 <= k' < k ->
let c = !s[j' * length s2 + k'] in
is_product i f1 f2 s1[j'] s2[k'] c }
let p = product n i f1 f2 s1[j] s2[k] in
assert { forall l. 0 <= l < length !s ->
not (eq_coloring n p !s[l]) };
s := snoc !s p
done
done;
!s

lemma solution_white_or_black:
forall n i f1 f2 c.
valid_nums_forest (N i f1 f2) n ->
solution (N i f1 f2) c ->
match M.get c i with
| White -> solution f2 c
| Black -> exists c1 c2. is_product i f1 f2 c1 c2 c &&
solution f1 c1 && solution f2 c2
end

let rec enum (n: int) (f: forest) : seq coloring
requires { valid_nums_forest f n }
ensures  { length result = count_forest f }
ensures  { solutions n f result }
ensures  { forall c. solution f c <->
exists j. 0 <= j < length result && eq_coloring n c result[j] }
variant  { f }
= match f with
| E ->
cons (const White) empty
| N i f1 f2 ->
let s1 = enum n f1 in
let s2 = enum n f2 in
s2 ++ product_all n i f1 f2 s1 s2
end

end
*)
```

# Why3 Proof Results for Project "koda_ruskey"

## Theory "koda_ruskey.KodaRuskey_Spec": fully verified in 0.00 s

 Obligations Alt-Ergo (1.30) size_forest_nonneg --- induction_ty_lex size_forest_nonneg.1 0.00 count_forest_nonneg --- induction_ty_lex count_forest_nonneg.1 0.00

## Theory "koda_ruskey.Lemmas": fully verified in 0.05 s

 Obligations Alt-Ergo (1.30) CVC3 (2.4.1) CVC4 (1.4) Coq (8.6.1) Eprover (1.8-001) Z3 (4.4.1) Z3 (4.4.1 noBV) mem_app --- --- --- --- --- --- --- induction_ty_lex mem_app.1 --- --- --- --- --- --- --- split_goal_wp mem_app.1.1 0.00 --- --- --- --- --- --- mem_app.1.2 0.05 --- --- --- --- --- --- size_stack_nonneg --- --- --- --- --- --- --- induction_ty_lex size_stack_nonneg.1 --- --- --- --- --- --- --- split_goal_wp size_stack_nonneg.1.1 0.00 --- --- --- --- --- --- size_stack_nonneg.1.2 0.01 --- --- --- --- --- --- white_forest_equiv --- --- --- --- --- --- --- induction_ty_lex white_forest_equiv.1 0.02 --- --- --- --- --- --- any_forest_frame --- --- --- --- --- --- --- induction_ty_lex any_forest_frame.1 --- --- --- --- --- --- --- split_goal_wp any_forest_frame.1.1 0.01 --- --- --- --- --- --- any_forest_frame.1.2 0.01 --- --- --- --- --- --- any_forest_frame.1.3 0.04 --- --- --- --- --- --- any_forest_frame.1.4 0.08 --- --- --- --- --- --- any_stack_frame --- --- --- --- --- --- --- induction_ty_lex any_stack_frame.1 --- --- --- --- --- --- --- split_goal_wp any_stack_frame.1.1 0.01 --- --- --- --- --- --- any_stack_frame.1.2 --- --- --- --- --- --- --- introduce_premises any_stack_frame.1.2.1 --- --- --- --- --- --- --- compute_in_goal any_stack_frame.1.2.1.1 --- --- --- --- --- --- --- split_goal_wp any_stack_frame.1.2.1.1.1 0.02 --- --- --- --- --- --- any_stack_frame.1.2.1.1.2 --- 0.06 --- --- --- --- --- inverse_frame --- --- --- --- --- --- --- induction_ty_lex inverse_frame.1 0.07 --- --- --- --- --- --- inverse_frame2 --- --- --- --- --- --- --- induction_ty_lex inverse_frame2.1 0.11 --- --- --- --- --- --- 8. VC for inverse_any --- --- --- --- --- --- --- induction_ty_lex 1. VC for inverse_any 0.02 --- --- --- --- --- --- inverse_final --- --- --- --- --- --- --- compute_in_goal inverse_final.1 0.44 --- --- --- --- --- --- inverse_white --- --- --- --- --- --- --- compute_in_goal inverse_white.1 1.10 --- --- --- --- --- --- 11. VC for white_final_exclusive 0.01 --- --- --- --- --- --- final_unique --- --- --- --- --- --- --- induction_ty_lex final_unique.1 --- --- --- --- --- --- --- split_goal_wp final_unique.1.1 0.00 --- --- --- --- --- --- final_unique.1.2 0.30 --- --- --- --- --- --- 13. VC for inverse_inverse --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.01 --- --- --- --- --- --- 2. variant decrease 0.01 --- --- --- --- --- --- 3. precondition 0.01 --- --- --- --- --- --- 4. precondition 0.01 --- --- --- --- --- --- 5. postcondition 0.01 --- --- --- --- --- --- 6. postcondition 0.18 --- --- --- --- --- --- 7. variant decrease 0.01 --- --- --- --- --- --- 8. precondition 0.01 --- --- --- --- --- --- 9. precondition 0.01 --- --- --- --- --- --- 10. postcondition 0.18 --- --- --- --- --- --- sub_not_nil --- --- --- --- --- --- --- induction_pr sub_not_nil.1 0.00 --- --- --- --- --- --- sub_not_nil.2 --- --- --- --- --- 0.76 --- sub_not_nil.3 --- --- 0.01 --- --- --- --- sub_empty --- --- --- --- --- --- --- induction_pr sub_empty.1 0.00 --- --- --- --- --- --- sub_empty.2 --- --- 0.04 --- --- --- --- sub_empty.3 --- --- --- --- --- 2.54 --- sub_mem --- --- --- --- --- --- --- induction_pr sub_mem.1 0.00 --- --- --- --- --- --- sub_mem.2 --- --- --- --- --- --- --- simplify_trivial_quantification sub_mem.2.1 --- --- 0.04 --- --- --- --- sub_mem.3 --- --- 0.02 --- --- --- --- sub_weaken1 --- --- --- --- --- --- --- induction_pr sub_weaken1.1 --- --- 0.04 --- --- --- --- sub_weaken1.2 --- --- --- --- --- --- --- induction_ty_lex sub_weaken1.2.1 0.02 --- --- --- --- --- --- sub_weaken1.3 --- --- 1.33 --- --- --- --- sub_weaken2 --- --- --- --- --- --- --- induction_pr sub_weaken2.1 --- --- 0.05 --- --- --- --- sub_weaken2.2 --- --- --- --- --- --- --- induction_ty_lex sub_weaken2.2.1 --- --- --- --- --- --- --- split_goal_wp sub_weaken2.2.1.1 --- --- --- --- --- --- 0.02 sub_weaken2.3 --- --- --- --- --- --- --- simplify_trivial_quantification_in_goal sub_weaken2.3.1 --- --- --- --- --- --- --- introduce_premises sub_weaken2.3.1.1 --- --- --- --- --- 0.88 --- not_mem_st --- --- --- --- --- --- --- induction_pr not_mem_st.1 0.01 --- --- --- --- --- --- not_mem_st.2 0.01 --- --- --- --- --- --- not_mem_st.3 0.01 --- --- --- --- --- --- sub_frame --- --- --- --- --- --- --- induction_pr sub_frame.1 0.01 --- --- --- --- --- --- sub_frame.2 --- --- 0.03 --- --- --- --- sub_frame.3 --- --- 0.04 --- --- --- --- sub_no_rep --- --- --- --- --- --- --- induction_pr sub_no_rep.1 0.01 --- --- --- --- --- --- sub_no_rep.2 --- --- 0.13 --- --- --- --- sub_no_rep.3 --- --- 0.16 --- --- --- --- sub_no_rep2 --- --- --- --- --- --- --- induction_pr sub_no_rep2.1 --- --- --- --- --- --- --- split_goal_wp sub_no_rep2.1.1 --- --- 0.02 --- --- --- --- sub_no_rep2.2 --- --- --- --- --- --- --- split_goal_wp sub_no_rep2.2.1 --- --- 0.04 --- --- --- --- sub_no_rep2.3 --- --- --- --- --- --- --- split_goal_wp sub_no_rep2.3.1 --- --- 1.09 --- --- --- --- white_valid --- --- --- --- --- --- --- induction_ty_lex white_valid.1 --- --- --- --- --- --- --- split_goal_wp white_valid.1.1 0.00 --- --- --- --- --- --- white_valid.1.2 0.01 --- --- --- --- --- --- final_valid --- --- --- --- --- --- --- induction_ty_lex final_valid.1 --- --- --- --- --- --- --- split_goal_wp final_valid.1.1 0.01 --- --- --- --- --- --- final_valid.1.2 0.01 --- --- --- --- --- --- valid_coloring_frame --- --- --- --- --- --- --- induction_ty_lex valid_coloring_frame.1 0.18 --- --- --- --- --- --- valid_coloring_set --- --- --- --- --- --- --- induction_ty_lex valid_coloring_set.1 0.02 --- --- --- --- --- --- head_and_tail --- --- --- --- --- --- --- induction_ty_lex head_and_tail.1 0.01 --- --- --- --- --- --- sub_valid_coloring_f1 0.02 --- --- --- --- --- --- sub_valid_coloring --- --- --- --- --- --- --- induction_pr sub_valid_coloring.1 --- --- --- --- --- --- --- introduce_premises sub_valid_coloring.1.1 --- --- --- --- --- --- --- compute_in_goal sub_valid_coloring.1.1.1 --- --- --- --- --- --- --- split_goal_wp sub_valid_coloring.1.1.1.1 0.03 --- --- --- --- --- --- sub_valid_coloring.1.1.1.2 0.01 --- --- --- --- --- --- sub_valid_coloring.1.1.1.3 0.03 --- --- --- --- --- --- sub_valid_coloring.2 --- --- --- --- --- --- --- introduce_premises sub_valid_coloring.2.1 --- --- --- --- --- --- --- simplify_trivial_quantification sub_valid_coloring.2.1.1 --- --- --- --- --- --- --- compute_in_goal sub_valid_coloring.2.1.1.1 --- --- --- --- --- --- --- split_goal_wp sub_valid_coloring.2.1.1.1.1 0.04 --- --- --- --- --- --- sub_valid_coloring.2.1.1.1.2 --- --- 0.18 --- --- --- --- sub_valid_coloring.2.1.1.1.3 --- --- 0.20 --- 0.04 --- --- sub_valid_coloring.3 --- --- --- --- --- --- --- introduce_premises sub_valid_coloring.3.1 --- --- --- --- --- --- --- compute_in_goal sub_valid_coloring.3.1.1 --- --- --- --- --- --- --- split_goal_wp sub_valid_coloring.3.1.1.1 --- --- --- --- --- --- --- introduce_premises sub_valid_coloring.3.1.1.1.1 --- --- --- --- 12.19 --- --- sub_valid_coloring.3.1.1.2 --- --- --- --- --- 0.03 --- sub_valid_coloring.3.1.1.3 0.18 --- --- --- --- --- --- sub_Cons_N --- --- --- --- --- --- --- induction_pr sub_Cons_N.1 0.01 --- --- --- --- --- --- sub_Cons_N.2 --- --- 0.02 --- --- --- --- sub_Cons_N.3 --- --- 0.08 --- --- --- --- white_white 0.02 --- --- --- --- --- --- 32. VC for sub_valid_coloring_white --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.01 --- --- --- --- --- --- 2. variant decrease 0.01 --- --- --- --- --- --- 3. precondition 0.01 --- --- --- --- --- --- 4. precondition 0.02 --- --- --- --- --- --- 5. precondition 0.01 --- --- --- --- --- --- 6. variant decrease 0.02 --- --- --- --- --- --- 7. precondition 0.01 --- --- --- --- --- --- 8. precondition 0.02 --- --- --- --- --- --- 9. precondition 0.01 --- --- --- --- --- --- 10. postcondition --- --- --- 2.37 --- --- --- count_stack_nonneg --- --- --- --- --- --- --- induction_ty_lex count_stack_nonneg.1 0.01 --- --- --- --- --- --- 34. VC for stored_trans1 --- --- --- --- --- --- --- introduce_premises 1. VC for stored_trans1 --- --- --- --- --- --- --- inline_goal 1. VC for stored_trans1 --- --- --- --- --- --- --- split_goal_wp 1. postcondition --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.02 --- --- --- --- --- --- 2. postcondition 0.24 --- --- --- --- --- --- 3. postcondition 0.29 --- --- --- --- --- --- 4. postcondition 0.16 --- --- --- --- --- --- 5. postcondition 0.34 --- --- --- --- --- --- 35. VC for stored_trans2 --- --- --- --- --- --- --- introduce_premises 1. VC for stored_trans2 --- --- --- --- --- --- --- inline_goal 1. VC for stored_trans2 --- --- --- --- --- --- --- split_goal_wp 1. postcondition --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.02 --- --- --- --- --- --- 2. postcondition 0.22 --- --- --- --- --- --- 3. postcondition 0.29 --- --- --- --- --- --- 4. postcondition 0.24 --- --- --- --- --- --- 5. postcondition 0.28 --- --- --- --- --- ---

## Theory "koda_ruskey.KodaRuskey": fully verified in 0.00 s

 Obligations Alt-Ergo (1.30) CVC3 (2.4.1) CVC4 (1.4) Eprover (1.8-001) Z3 (4.4.1 noBV) 1. VC for enum --- --- --- --- --- split_goal_wp 1. unreachable point 0.01 --- --- --- --- 2. assertion 0.01 --- --- --- --- 3. postcondition --- --- --- --- --- introduce_premises 1. postcondition --- --- --- --- --- compute_in_goal 1. postcondition --- --- --- --- --- split_goal_wp 1. VC for enum --- --- 0.15 --- --- 2. VC for enum --- --- 0.07 --- --- 3. VC for enum --- --- 0.17 --- --- 4. postcondition 0.02 --- --- --- --- 5. postcondition 0.02 --- --- --- --- 6. variant decrease 0.02 --- --- --- --- 7. precondition 0.01 --- --- --- --- 8. precondition 0.01 --- --- --- --- 9. precondition 0.02 --- --- --- --- 10. precondition 0.01 --- --- --- --- 11. precondition --- --- 0.08 --- --- 12. precondition 0.01 --- --- --- --- 13. postcondition --- --- 0.04 --- --- 14. postcondition --- --- --- --- --- introduce_premises 1. postcondition --- --- --- --- --- compute_in_goal 1. postcondition --- --- --- --- --- split_goal_wp 1. VC for enum --- --- 0.12 --- --- 2. VC for enum --- --- 0.08 --- --- 3. VC for enum --- --- 0.06 --- --- 15. postcondition 0.01 --- --- --- --- 16. postcondition 0.10 --- --- --- --- 17. assertion --- --- 0.73 --- --- 18. assertion 0.04 --- --- --- --- 19. index in array bounds --- --- --- 0.06 --- 20. variant decrease 0.01 --- --- --- --- 21. precondition 0.01 --- --- --- --- 22. precondition 0.01 --- --- --- --- 23. precondition 0.12 --- --- --- --- 24. precondition --- --- 0.07 --- --- 25. precondition --- --- 0.06 --- --- 26. assertion --- --- 2.14 --- --- 27. index in array bounds --- --- --- --- --- introduce_premises 1. index in array bounds --- --- --- --- --- inline_goal 1. index in array bounds --- --- 0.03 --- --- 28. assertion 0.57 --- --- --- --- 29. assertion --- --- 3.45 --- --- 30. assertion --- --- 3.53 --- --- 31. assertion --- --- 0.04 --- --- 32. variant decrease --- --- 0.14 --- --- 33. precondition 0.00 --- --- --- --- 34. precondition 0.02 --- --- --- --- 35. precondition 0.14 --- --- --- --- 36. precondition 0.25 --- --- --- --- 37. precondition 0.14 --- --- --- --- 38. assertion --- --- 0.19 --- --- 39. assertion --- --- 0.06 --- --- 40. assertion --- --- 0.30 --- --- 41. precondition 0.01 --- --- --- --- 42. precondition 0.02 --- --- --- --- 43. precondition --- --- 0.24 --- --- 44. precondition --- --- 0.30 --- --- 45. precondition --- --- 0.21 --- --- 46. precondition --- --- --- --- --- inline_goal 1. precondition --- --- --- --- --- split_goal_wp 1. precondition 0.03 --- --- --- --- 2. precondition 0.03 --- --- --- --- 3. precondition 0.02 --- --- --- --- 4. precondition --- --- 0.10 --- --- 5. precondition --- --- 0.24 --- --- 47. precondition --- --- 0.05 --- --- 48. postcondition --- --- 0.20 --- --- 49. postcondition --- --- --- --- --- introduce_premises 1. postcondition --- --- --- --- --- compute_in_goal 1. postcondition --- --- --- --- --- split_goal_wp 1. VC for enum --- --- 0.22 --- --- 2. VC for enum --- --- 4.92 --- --- 3. VC for enum --- --- 0.20 --- --- 50. postcondition 0.01 --- --- --- --- 51. postcondition --- --- --- --- --- split_goal_wp 1. postcondition --- --- --- --- --- inline_goal 1. postcondition --- --- --- --- --- split_goal_wp 1. postcondition 0.01 --- --- --- --- 2. postcondition --- --- --- --- 0.02 3. postcondition 0.01 --- --- --- --- 4. postcondition --- --- 0.10 --- --- 5. postcondition --- --- --- --- 0.02 52. assertion 0.18 --- --- --- --- 53. variant decrease 0.13 --- --- --- --- 54. precondition 0.01 --- --- --- --- 55. precondition 0.01 --- --- --- --- 56. precondition 0.01 --- --- --- --- 57. precondition --- --- 0.08 --- --- 58. precondition --- --- 0.15 --- --- 59. assertion --- 0.23 --- --- --- 60. index in array bounds --- --- 0.02 --- --- 61. assertion 0.33 --- --- --- --- 62. assertion 0.02 --- --- --- --- 63. assertion 1.27 --- --- --- --- 64. assertion 3.63 --- --- --- --- 65. variant decrease 0.20 --- --- --- --- 66. precondition 0.01 --- --- --- --- 67. precondition 0.01 --- --- --- --- 68. precondition 0.08 --- --- --- --- 69. precondition --- --- 0.14 --- --- 70. precondition --- --- 0.15 --- --- 71. assertion --- --- 0.19 --- --- 72. assertion --- --- 5.30 --- --- 73. precondition 0.01 --- --- --- --- 74. precondition 0.02 --- --- --- --- 75. precondition --- --- 0.21 --- --- 76. precondition --- --- 0.31 --- --- 77. precondition --- --- 0.20 --- --- 78. precondition --- --- 0.04 --- --- 79. precondition --- --- 0.04 --- --- 80. postcondition --- --- 0.22 --- --- 81. postcondition --- --- 5.98 --- --- 82. postcondition 0.02 --- --- --- --- 83. postcondition 0.03 --- --- --- --- 2. VC for main --- --- --- --- --- split_goal_wp 1. precondition 0.01 --- --- --- --- 2. precondition 0.01 --- --- --- --- 3. precondition 0.01 --- --- --- --- 4. precondition 0.00 --- --- --- --- 5. precondition 0.01 --- --- --- --- 6. postcondition 0.01 --- --- --- --- 7. postcondition 0.02 --- --- --- ---