Wiki Agenda Contact Version française

Koda-Ruskey's algorithm


Authors: Jean-Christophe Filliâtre / Mário Pereira

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]

  lemma head_and_tail:
    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
*)

download ZIP archive

Why3 Proof Results for Project "koda_ruskey"

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

ObligationsAlt-Ergo (1.30)
size_forest_nonneg---
induction_ty_lex
  size_forest_nonneg.10.00
count_forest_nonneg---
induction_ty_lex
  count_forest_nonneg.10.00

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

ObligationsAlt-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.10.00------------------
mem_app.1.20.05------------------
size_stack_nonneg---------------------
induction_ty_lex
  size_stack_nonneg.1---------------------
split_goal_wp
  size_stack_nonneg.1.10.00------------------
size_stack_nonneg.1.20.01------------------
white_forest_equiv---------------------
induction_ty_lex
  white_forest_equiv.10.02------------------
any_forest_frame---------------------
induction_ty_lex
  any_forest_frame.1---------------------
split_goal_wp
  any_forest_frame.1.10.01------------------
any_forest_frame.1.20.01------------------
any_forest_frame.1.30.04------------------
any_forest_frame.1.40.08------------------
any_stack_frame---------------------
induction_ty_lex
  any_stack_frame.1---------------------
split_goal_wp
  any_stack_frame.1.10.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.10.02------------------
any_stack_frame.1.2.1.1.2---0.06---------------
inverse_frame---------------------
induction_ty_lex
  inverse_frame.10.07------------------
inverse_frame2---------------------
induction_ty_lex
  inverse_frame2.10.11------------------
8. VC for inverse_any---------------------
induction_ty_lex
  1. VC for inverse_any0.02------------------
inverse_final---------------------
compute_in_goal
  inverse_final.10.44------------------
inverse_white---------------------
compute_in_goal
  inverse_white.11.10------------------
11. VC for white_final_exclusive0.01------------------
final_unique---------------------
induction_ty_lex
  final_unique.1---------------------
split_goal_wp
  final_unique.1.10.00------------------
final_unique.1.20.30------------------
13. VC for inverse_inverse---------------------
split_goal_wp
  1. postcondition0.01------------------
2. variant decrease0.01------------------
3. precondition0.01------------------
4. precondition0.01------------------
5. postcondition0.01------------------
6. postcondition0.18------------------
7. variant decrease0.01------------------
8. precondition0.01------------------
9. precondition0.01------------------
10. postcondition0.18------------------
sub_not_nil---------------------
induction_pr
  sub_not_nil.10.00------------------
sub_not_nil.2---------------0.76---
sub_not_nil.3------0.01------------
sub_empty---------------------
induction_pr
  sub_empty.10.00------------------
sub_empty.2------0.04------------
sub_empty.3---------------2.54---
sub_mem---------------------
induction_pr
  sub_mem.10.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.10.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.10.01------------------
not_mem_st.20.01------------------
not_mem_st.30.01------------------
sub_frame---------------------
induction_pr
  sub_frame.10.01------------------
sub_frame.2------0.03------------
sub_frame.3------0.04------------
sub_no_rep---------------------
induction_pr
  sub_no_rep.10.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.10.00------------------
white_valid.1.20.01------------------
final_valid---------------------
induction_ty_lex
  final_valid.1---------------------
split_goal_wp
  final_valid.1.10.01------------------
final_valid.1.20.01------------------
valid_coloring_frame---------------------
induction_ty_lex
  valid_coloring_frame.10.18------------------
valid_coloring_set---------------------
induction_ty_lex
  valid_coloring_set.10.02------------------
head_and_tail---------------------
induction_ty_lex
  head_and_tail.10.01------------------
sub_valid_coloring_f10.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.10.03------------------
sub_valid_coloring.1.1.1.20.01------------------
sub_valid_coloring.1.1.1.30.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.10.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.30.18------------------
sub_Cons_N---------------------
induction_pr
  sub_Cons_N.10.01------------------
sub_Cons_N.2------0.02------------
sub_Cons_N.3------0.08------------
white_white0.02------------------
32. VC for sub_valid_coloring_white---------------------
split_goal_wp
  1. postcondition0.01------------------
2. variant decrease0.01------------------
3. precondition0.01------------------
4. precondition0.02------------------
5. precondition0.01------------------
6. variant decrease0.02------------------
7. precondition0.01------------------
8. precondition0.02------------------
9. precondition0.01------------------
10. postcondition---------2.37---------
count_stack_nonneg---------------------
induction_ty_lex
  count_stack_nonneg.10.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. postcondition0.02------------------
2. postcondition0.24------------------
3. postcondition0.29------------------
4. postcondition0.16------------------
5. postcondition0.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. postcondition0.02------------------
2. postcondition0.22------------------
3. postcondition0.29------------------
4. postcondition0.24------------------
5. postcondition0.28------------------

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

ObligationsAlt-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 point0.01------------
2. assertion0.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. postcondition0.02------------
5. postcondition0.02------------
6. variant decrease0.02------------
7. precondition0.01------------
8. precondition0.01------------
9. precondition0.02------------
10. precondition0.01------------
11. precondition------0.08------
12. precondition0.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. postcondition0.01------------
16. postcondition0.10------------
17. assertion------0.73------
18. assertion0.04------------
19. index in array bounds---------0.06---
20. variant decrease0.01------------
21. precondition0.01------------
22. precondition0.01------------
23. precondition0.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. assertion0.57------------
29. assertion------3.45------
30. assertion------3.53------
31. assertion------0.04------
32. variant decrease------0.14------
33. precondition0.00------------
34. precondition0.02------------
35. precondition0.14------------
36. precondition0.25------------
37. precondition0.14------------
38. assertion------0.19------
39. assertion------0.06------
40. assertion------0.30------
41. precondition0.01------------
42. precondition0.02------------
43. precondition------0.24------
44. precondition------0.30------
45. precondition------0.21------
46. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. precondition0.03------------
2. precondition0.03------------
3. precondition0.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. postcondition0.01------------
51. postcondition---------------
split_goal_wp
  1. postcondition---------------
inline_goal
  1. postcondition---------------
split_goal_wp
  1. postcondition0.01------------
2. postcondition------------0.02
3. postcondition0.01------------
4. postcondition------0.10------
5. postcondition------------0.02
52. assertion0.18------------
53. variant decrease0.13------------
54. precondition0.01------------
55. precondition0.01------------
56. precondition0.01------------
57. precondition------0.08------
58. precondition------0.15------
59. assertion---0.23---------
60. index in array bounds------0.02------
61. assertion0.33------------
62. assertion0.02------------
63. assertion1.27------------
64. assertion3.63------------
65. variant decrease0.20------------
66. precondition0.01------------
67. precondition0.01------------
68. precondition0.08------------
69. precondition------0.14------
70. precondition------0.15------
71. assertion------0.19------
72. assertion------5.30------
73. precondition0.01------------
74. precondition0.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. postcondition0.02------------
83. postcondition0.03------------
2. VC for main---------------
split_goal_wp
  1. precondition0.01------------
2. precondition0.01------------
3. precondition0.01------------
4. precondition0.00------------
5. precondition0.01------------
6. postcondition0.01------------
7. postcondition0.02------------