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 map.Map use list.List use list.Append use int.Int type color = White | Black let eq_color (c1 c2:color) : bool ensures { result <-> c1 = c2 } = match c1,c2 with | White,White | Black,Black -> True | _ -> False end 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 map.Map use list.List use list.Append use int.Int use 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 seq.Seq as S use list.List use KodaRuskey_Spec use Lemmas use map.Map as M use array.Array use int.Int use ref.Ref val ghost 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 eq_color bits[i] White then begin label A in 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 label B in bits[i] <- Black; assert { sub st f0 bits.elts }; assert { white_forest f1 bits.elts }; assert { unchanged (Cons f2 st') (bits at B).elts bits.elts}; assert { inverse (Cons f2 st') (bits at A).elts bits.elts }; label C in 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') (bits at C).elts bits.elts && white_forest f2 bits.elts else unchanged (Cons f2 st') (bits at 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 }; label A in 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 label B in bits[i] <- White; assert { unchanged (Cons f1 (Cons f2 st')) (bits at B).elts bits.elts }; assert { inverse (Cons f1 (Cons f2 st')) (bits at A).elts bits.elts }; assert { sub st f0 bits.elts }; assert { if even_forest f1 || even_forest f2 then unchanged st' (bits at A).elts bits.elts else inverse st' (bits at A).elts bits.elts }; 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 seq.Seq as S
use map.Map as M
use map.Const
use list.List
use int.Int
use KodaRuskey_Spec
use Lemmas
use 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
Obligations | Alt-Ergo 2.3.3 | CVC4 1.8 | |
VC for eq_color | 0.00 | 0.03 | |
size_forest_nonneg | --- | --- | |
induction_ty_lex | |||
size_forest_nonneg.0 | 0.00 | 0.03 | |
count_forest_nonneg | --- | --- | |
induction_ty_lex | |||
count_forest_nonneg.0 | 0.01 | 0.05 |
Theory "koda_ruskey.Lemmas": fully verified
Obligations | Alt-Ergo 2.3.3 | CVC3 2.4.1 | CVC4 1.8 | CVC5 1.0.5 | ||||
mem_app | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
mem_app.0 | 0.01 | --- | 0.06 | --- | ||||
size_stack_nonneg | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
size_stack_nonneg.0 | 0.01 | --- | 0.06 | --- | ||||
white_forest_equiv | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
white_forest_equiv.0 | 0.02 | --- | 0.06 | --- | ||||
any_forest_frame | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
any_forest_frame.0 | 0.04 | --- | 0.11 | --- | ||||
any_stack_frame | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
any_stack_frame.0 | --- | --- | --- | --- | ||||
split_vc | ||||||||
any_stack_frame.0.0 | 0.00 | --- | 0.05 | --- | ||||
any_stack_frame.0.1 | --- | --- | --- | --- | ||||
compute_in_goal | ||||||||
any_stack_frame.0.1.0 | --- | --- | --- | --- | ||||
split_vc | ||||||||
any_stack_frame.0.1.0.0 | 0.02 | --- | 0.07 | --- | ||||
any_stack_frame.0.1.0.1 | --- | 0.08 | --- | --- | ||||
inverse_frame | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
inverse_frame.0 | 0.05 | --- | --- | --- | ||||
inverse_frame2 | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
inverse_frame2.0 | 0.05 | --- | --- | --- | ||||
VC for inverse_any | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
VC for inverse_any | 0.02 | --- | 0.05 | --- | ||||
inverse_final | 0.15 | --- | --- | --- | ||||
inverse_white | 0.01 | --- | 0.06 | --- | ||||
VC for white_final_exclusive | 0.02 | --- | --- | --- | ||||
final_unique | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
final_unique.0 | 0.04 | --- | 0.07 | --- | ||||
VC for inverse_inverse | 0.32 | --- | 0.45 | --- | ||||
sub_not_nil | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_not_nil.0 | 0.02 | --- | 0.06 | --- | ||||
sub_not_nil.1 | 0.01 | --- | 0.04 | --- | ||||
sub_not_nil.2 | 0.02 | --- | 0.08 | --- | ||||
sub_empty | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_empty.0 | 0.01 | --- | 0.07 | --- | ||||
sub_empty.1 | 0.02 | --- | 0.07 | --- | ||||
sub_empty.2 | --- | --- | 0.15 | --- | ||||
sub_mem | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_mem.0 | 0.02 | --- | 0.06 | --- | ||||
sub_mem.1 | 0.01 | --- | 0.05 | --- | ||||
sub_mem.2 | 0.03 | --- | 0.07 | --- | ||||
sub_weaken1 | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_weaken1.0 | 0.04 | --- | 0.08 | --- | ||||
sub_weaken1.1 | 0.02 | --- | 0.06 | --- | ||||
sub_weaken1.2 | --- | --- | 0.16 | --- | ||||
sub_weaken2 | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_weaken2.0 | --- | --- | 0.10 | --- | ||||
sub_weaken2.1 | 0.02 | --- | 0.06 | --- | ||||
sub_weaken2.2 | --- | --- | 0.27 | --- | ||||
not_mem_st | --- | --- | --- | --- | ||||
induction_pr | ||||||||
not_mem_st.0 | 0.02 | --- | 0.07 | --- | ||||
not_mem_st.1 | 0.02 | --- | 0.05 | --- | ||||
not_mem_st.2 | 0.03 | --- | 0.08 | --- | ||||
sub_frame | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_frame.0 | 0.01 | --- | 0.06 | --- | ||||
sub_frame.1 | 0.05 | --- | 0.07 | --- | ||||
sub_frame.2 | --- | --- | 0.13 | --- | ||||
sub_no_rep | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_no_rep.0 | 0.02 | --- | 0.06 | --- | ||||
sub_no_rep.1 | 0.02 | --- | 0.06 | --- | ||||
sub_no_rep.2 | --- | --- | 0.11 | --- | ||||
sub_no_rep2 | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_no_rep2.0 | 0.01 | --- | 0.06 | --- | ||||
sub_no_rep2.1 | 0.01 | --- | 0.06 | --- | ||||
sub_no_rep2.2 | --- | --- | --- | 0.32 | ||||
white_valid | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
white_valid.0 | 0.02 | --- | 0.06 | --- | ||||
final_valid | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
final_valid.0 | 0.02 | --- | 0.07 | --- | ||||
valid_coloring_frame | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
valid_coloring_frame.0 | 0.08 | --- | 0.10 | --- | ||||
valid_coloring_set | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
valid_coloring_set.0 | 0.02 | --- | 0.07 | --- | ||||
head_and_tail | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
head_and_tail.0 | 0.02 | --- | 0.08 | --- | ||||
sub_valid_coloring_f1 | 0.04 | --- | 0.07 | --- | ||||
sub_valid_coloring | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_valid_coloring.0 | 0.04 | --- | 0.08 | --- | ||||
sub_valid_coloring.1 | --- | --- | --- | --- | ||||
split_vc | ||||||||
sub_valid_coloring.1.0 | --- | --- | --- | --- | ||||
compute_in_goal | ||||||||
sub_valid_coloring.1.0.0 | --- | --- | --- | --- | ||||
split_vc | ||||||||
sub_valid_coloring.1.0.0.0 | 0.16 | --- | 0.16 | --- | ||||
sub_valid_coloring.1.0.0.1 | --- | 2.29 | --- | --- | ||||
sub_valid_coloring.1.0.0.2 | --- | 1.76 | --- | --- | ||||
sub_valid_coloring.2 | 0.32 | --- | --- | --- | ||||
sub_Cons_N | --- | --- | --- | --- | ||||
induction_pr | ||||||||
sub_Cons_N.0 | 0.02 | --- | 0.08 | --- | ||||
sub_Cons_N.1 | 0.02 | --- | 0.07 | --- | ||||
sub_Cons_N.2 | 0.08 | --- | 0.08 | --- | ||||
white_white | 0.02 | --- | 0.07 | --- | ||||
VC for sub_valid_coloring_white | --- | --- | --- | --- | ||||
split_vc | ||||||||
variant decrease | 0.03 | --- | 0.07 | --- | ||||
precondition | 0.01 | --- | 0.05 | --- | ||||
precondition | 0.02 | --- | 0.07 | --- | ||||
precondition | 0.01 | --- | 0.04 | --- | ||||
variant decrease | 0.03 | --- | 0.08 | --- | ||||
precondition | 0.02 | --- | 0.06 | --- | ||||
precondition | 0.01 | --- | 0.06 | --- | ||||
precondition | 0.01 | --- | 0.04 | --- | ||||
postcondition | --- | --- | --- | --- | ||||
compute_in_goal | ||||||||
postcondition | --- | --- | --- | --- | ||||
split_vc | ||||||||
postcondition | --- | 3.50 | --- | --- | ||||
postcondition | 0.76 | --- | --- | --- | ||||
postcondition | --- | 2.99 | --- | --- | ||||
count_stack_nonneg | --- | --- | --- | --- | ||||
induction_ty_lex | ||||||||
count_stack_nonneg.0 | 0.02 | --- | 0.09 | --- | ||||
VC for stored_trans1 | 0.42 | --- | --- | --- | ||||
VC for stored_trans2 | 0.40 | --- | --- | --- |
Theory "koda_ruskey.KodaRuskey": fully verified
Obligations | Alt-Ergo 2.3.3 | CVC4 1.8 | Eprover 2.0 | |
VC for enum | --- | --- | --- | |
split_goal_right | ||||
unreachable point | 0.02 | 0.08 | --- | |
assertion | 0.02 | 0.07 | --- | |
postcondition | 0.01 | 0.06 | --- | |
postcondition | 0.04 | 0.14 | --- | |
postcondition | 0.02 | 0.08 | --- | |
postcondition | 0.06 | --- | --- | |
variant decrease | 0.05 | 0.11 | --- | |
precondition | 0.02 | 0.08 | --- | |
precondition | 0.02 | 0.08 | --- | |
precondition | 0.03 | 0.10 | --- | |
precondition | 0.03 | 0.10 | --- | |
precondition | 0.02 | 0.11 | --- | |
precondition | 0.01 | 0.08 | --- | |
postcondition | 0.03 | 0.12 | --- | |
postcondition | 0.04 | 0.12 | --- | |
postcondition | 0.02 | 0.08 | --- | |
postcondition | 0.80 | --- | --- | |
assertion | 0.42 | 0.20 | --- | |
assertion | 0.40 | 0.22 | --- | |
index in array bounds | --- | --- | 0.48 | |
variant decrease | 0.06 | 0.15 | --- | |
precondition | 0.02 | 0.07 | --- | |
precondition | 0.02 | 0.08 | --- | |
precondition | 0.03 | 0.11 | --- | |
precondition | 0.02 | 0.08 | --- | |
precondition | 0.08 | 0.13 | --- | |
precondition | 0.02 | 0.08 | --- | |
assertion | 0.46 | 0.26 | --- | |
index in array bounds | --- | --- | 0.50 | |
assertion | 0.45 | 0.36 | --- | |
assertion | --- | 0.58 | 0.18 | |
assertion | 0.41 | 0.14 | --- | |
assertion | 0.04 | 0.11 | --- | |
variant decrease | 0.05 | 0.13 | --- | |
precondition | 0.02 | 0.10 | --- | |
precondition | 0.02 | 0.09 | --- | |
precondition | 0.04 | 0.10 | --- | |
precondition | 0.02 | 0.07 | --- | |
precondition | 0.16 | 0.14 | --- | |
precondition | 0.04 | 0.12 | --- | |
assertion | 0.29 | 0.15 | --- | |
assertion | 0.04 | 0.10 | --- | |
assertion | 1.09 | 0.16 | --- | |
precondition | 0.02 | 0.10 | --- | |
precondition | --- | --- | 0.62 | |
precondition | 1.97 | 0.28 | --- | |
precondition | 1.08 | 0.22 | --- | |
precondition | 1.13 | 0.22 | --- | |
precondition | 0.02 | 0.09 | --- | |
precondition | 0.02 | 0.09 | --- | |
postcondition | 1.42 | 0.92 | --- | |
postcondition | --- | 0.74 | --- | |
postcondition | 0.02 | 0.07 | --- | |
postcondition | 0.02 | 0.08 | --- | |
assertion | 0.10 | 0.12 | --- | |
variant decrease | 0.05 | 0.12 | --- | |
precondition | 0.02 | 0.08 | --- | |
precondition | 0.02 | 0.07 | --- | |
precondition | 0.04 | 0.11 | --- | |
precondition | 0.02 | 0.07 | --- | |
precondition | 0.17 | 0.13 | --- | |
precondition | 0.02 | 0.08 | --- | |
assertion | --- | 0.30 | --- | |
index in array bounds | --- | 3.96 | 0.40 | |
assertion | 4.70 | 0.17 | --- | |
assertion | 0.04 | 0.10 | --- | |
assertion | 4.13 | 0.28 | --- | |
assertion | 3.78 | 0.73 | --- | |
variant decrease | 0.22 | 0.18 | --- | |
precondition | 0.02 | 0.11 | --- | |
precondition | 0.02 | 0.10 | --- | |
precondition | 0.04 | 0.10 | --- | |
precondition | 0.02 | 0.07 | --- | |
precondition | 1.74 | 0.22 | --- | |
precondition | 0.48 | 0.15 | --- | |
assertion | 0.29 | 0.15 | --- | |
assertion | --- | 2.54 | --- | |
precondition | 0.02 | 0.11 | --- | |
precondition | --- | --- | 0.68 | |
precondition | 2.26 | 0.22 | --- | |
precondition | --- | 0.21 | --- | |
precondition | 1.80 | 0.23 | --- | |
precondition | 0.02 | 0.09 | --- | |
precondition | 0.03 | 0.09 | --- | |
postcondition | --- | 0.22 | --- | |
postcondition | --- | 0.67 | --- | |
postcondition | 0.02 | 0.08 | --- | |
postcondition | 0.02 | 0.08 | --- | |
VC for main | 0.06 | --- | --- |