## VerifyThis 2018: le rouge et le noir (alt)

solution to VerifyThis 2018 challenge 2

**Authors:** Martin Clochard

**Topics:** Array Data Structure / Algorithms / Mathematics

**Tools:** Why3

**References:** Project Euler / VerifyThis @ ETAPS 2018

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

# VerifyThis @ ETAPS 2018 competition Challenge 2: Le rouge et le noir

Author: Martin Clochard (LRI, Université Paris Sud)

use int.Int use import set.Fset as F (* The part about bijections, preservation of finiteness and cardinality, should be moved somewhere in stdlib. *) predicate bijection (p:fset 'a) (q:'b -> bool) (f:'a -> 'b) (g:'b -> 'a) = (forall x. mem x p -> q (f x) /\ g (f x) = x) /\ (forall x. q x -> mem (g x) p /\ f (g x) = x) let rec ghost bij_preserve (p:fset 'a) (q:'b -> bool) (f:'a -> 'b) (g:'b -> 'a) : fset 'b requires { bijection p q f g } ensures { forall x. q x <-> mem x result } ensures { cardinal p = cardinal result } variant { cardinal p } = if cardinal p = 0 then empty else let x = pick p in add (f x) (bij_preserve (remove x p) (fun y -> pure { q y /\ y <> f x}) f g) let rec ghost disjoint_union (p q:fset 'a) : unit requires { forall x. not (mem x p /\ mem x q) } ensures { cardinal (union p q) = cardinal p + cardinal q } variant { cardinal p } = if cardinal p = 0 then assert { union p q == q } else let x = pick p in assert { union (remove x p) q == remove x (union p q) }; disjoint_union (remove x p) q (* Abstraction layer over the integers. Reduce to standard integers after ghost code erasure (=ghost wrapping of integers operation for proof purposes). *) type cardinal 'a = { card : int; ghost cset : fset 'a; } invariant { card = cardinal cset } by { card = 0; cset = empty } let czero () : cardinal 'a ensures { result.cset = empty } ensures { result.card = 0 } = { card = 0; cset = empty } let cone (ghost x:'a) : cardinal 'a ensures { result.cset = singleton x } ensures { result.card = 1 } = { card = 1; cset = singleton x } (* reduce to identity after ghost code erasure. *) let cmap (ghost q:'b -> bool) (ghost f:'a -> 'b) (ghost g:'b -> 'a) (i:cardinal 'a) : cardinal 'b requires { bijection i.cset q f g } ensures { forall x. mem x result.cset <-> q x } ensures { result.card = i.card } = { card = i.card; cset = bij_preserve i.cset q f g } (* reduce to integer addition after ghost code erasure. *) let cadd (i1 i2:cardinal 'a) : cardinal 'a requires { forall x. not (mem x i1.cset /\ mem x i2.cset) } ensures { result.cset = union i1.cset i2.cset } ensures { result.card = i1.card + i2.card } = ghost disjoint_union i1.cset i2.cset; { card = i1.card + i2.card; cset = union i1.cset i2.cset } (* Specification of colorings: sequence of tiles that can be obtained by catenating unit black tiles or large (>=3 units) red tiles, with red tiles being non-consecutive. *) type color = Red | Black use import seq.Seq as S constant black : seq color = singleton Black function red (n:int) : seq color = create n (fun _ -> Red) (* color is color of first square. Default to black for empty sequence, as a black tile does not give any constraints. *) inductive valid_coloring_f color (seq color) = | ValidEmpty : valid_coloring_f Black empty | ValidBlack : forall c s. valid_coloring_f c s -> valid_coloring_f Black (black++s) | ValidRed : forall n s. n >= 3 /\ valid_coloring_f Black s -> valid_coloring_f Red (red n ++ s) predicate valid_coloring (s:seq color) = valid_coloring_f Red s \/ valid_coloring_f Black s predicate valid_coloring_l (n:int) (s:seq color) = valid_coloring s /\ s.length = n predicate valid_coloring_inter (n:int) (m:int) (s:seq color) = valid_coloring_l n s /\ exists i. 0 <= i < m /\ s[i] = Black predicate valid_coloring_at (n:int) (m:int) (s:seq color) = valid_coloring_l n s /\ s[m] = Black /\ forall i. 0 <= i < m -> s[i] = Red use array.Array let main () : unit = let count = Array.make 51 (czero ()) in count[0] <- cone S.empty; assert { forall s. mem s count[0].cset <-> valid_coloring_l 0 s }; count[1] <- cone (black ++ S.empty); assert { forall s. mem s count[1].cset <-> valid_coloring_l 1 s }; count[2] <- cone (black ++ (black ++ S.empty)); assert { forall s. mem s count[2].cset <-> valid_coloring_l 2 s }; count[3] <- { card = 2; cset = F.add (red 3 ++ S.empty) (F.singleton (black ++ (black ++ (black ++ S.empty)))); }; assert { forall s. mem s count[3].cset <-> valid_coloring_l 3 s }; for n = 4 to 50 do invariant { forall i s. 0 <= i < n -> valid_coloring_l i s <-> mem s count[i].cset } label L in let ghost q = pure { valid_coloring_inter n 3 } in let ghost f = pure { fun (s:seq color) -> black ++ s } in let ghost g = pure { fun (s:seq color) -> s[1 ..] } in assert { bijection count[n-1].cset q f g by (forall s. valid_coloring_l (n-1) s -> (valid_coloring_inter n 3 (black ++ s) by 0 <= 0 < (black ++ s).S.length /\ S.get (black++s) 0 = Black) /\ g (f s) == s) /\ (forall s. valid_coloring_inter n 3 s -> (valid_coloring_l (n-1) s[1 ..] /\ f (g s) == s) by (exists c s'. s = black ++ s' /\ valid_coloring_f c s' so s' == s[1 ..]) \/ (false by exists i s'. 3 <= i /\ s = red i ++ s') ) }; count[n] <- cmap q f g count[n-1]; for k = 3 to n - 1 do invariant { forall i. 0 <= i < n -> count[i] = (count[i] at L) } invariant { forall s. valid_coloring_inter n k s <-> mem s count[n].cset } let ghost q = pure { valid_coloring_at n k } in let ghost f = pure { fun (s:seq color) -> red k ++ (black ++ s) } in let ghost g = pure { fun (s:seq color) -> s[k+1 ..] } in assert { bijection count[n-k-1].cset q f g by (forall s. g (f s) == s by forall i. 0 <= i < s.S.length -> S.get (g (f s)) i = S.get (f s) (i+k+1) = S.get s i) so (forall s. valid_coloring_l (n-k-1) s -> valid_coloring_at n k (f s) /\ g (f s) = s ) /\ (forall s. valid_coloring_at n k s -> valid_coloring_l (n-k-1) (g s) /\ f (g s) = s by (false by exists s'. s = black ++ s' so 0 <= 0 < k /\ S.get s 0 = Black) \/ (exists i s'. 3 <= i /\ s = red i ++ s' /\ valid_coloring_f Black s' so s' <> empty so exists c s''. s' = black ++ s'' /\ valid_coloring_f c s'' so (i = k by not (i < k so S.get s i = Black) /\ not (i > k so S.get s k = Red)) so s'' = g s by s = f s'') ) }; count[n] <- cadd count[n] (cmap q f g count[n-k-1]) done; count[n] <- cadd count[n] (cone (red n)); assert { forall s. valid_coloring_l n s -> s = red n \/ valid_coloring_inter n n s by (exists s'. s = black ++ s' so 0 <= 0 < n /\ S.get s 0 = Black so valid_coloring_inter n n s) \/ (exists i s'. 3 <= i /\ s = red i ++ s' /\ valid_coloring_f Black s' so if i = n then s == red n else (s' <> empty by s'.S.length > 0) so exists s''. s' = black ++ s'' so 0 <= i < n /\ S.get s i = Black so valid_coloring_inter n n s ) }; assert { valid_coloring_l n (red n) by red n == red n ++ empty } done; (* Property asked by the problem. *) assert { forall s. valid_coloring_l 50 s <-> mem s count[50].cset }; assert { count[50].card = cardinal count[50].cset }

download ZIP archive

# Why3 Proof Results for Project "verifythis_2018_le_rouge_et_le_noir_2"

## Theory "verifythis_2018_le_rouge_et_le_noir_2.Top": fully verified

Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.2.0 | CVC4 1.5 | CVC4 1.6 | |||

VC for bij_preserve | --- | --- | --- | --- | |||

split_goal_right | |||||||

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

precondition | 0.06 | --- | --- | --- | |||

postcondition | --- | --- | 0.14 | --- | |||

postcondition | 0.02 | --- | --- | --- | |||

VC for disjoint_union | 0.78 | --- | --- | --- | |||

VC for cardinal | 0.00 | --- | --- | --- | |||

VC for czero | 0.00 | --- | --- | --- | |||

VC for cone | 0.00 | --- | --- | --- | |||

VC for cmap | 0.01 | --- | --- | --- | |||

VC for cadd | 0.00 | --- | --- | --- | |||

VC for main | --- | --- | --- | --- | |||

split_goal_right | |||||||

array creation size | 0.00 | --- | --- | --- | |||

index in array bounds | 0.01 | --- | --- | --- | |||

assertion | 0.05 | --- | --- | --- | |||

index in array bounds | 0.01 | --- | --- | --- | |||

assertion | 0.41 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

assertion | --- | --- | --- | --- | |||

split_all_full | |||||||

assertion | --- | --- | --- | 0.14 | |||

assertion | --- | --- | --- | --- | |||

introduce_premises | |||||||

assertion | --- | 10.60 | --- | --- | |||

precondition | 0.51 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

assertion | 3.41 | --- | --- | --- | |||

loop invariant init | --- | --- | --- | --- | |||

split_goal_right | |||||||

loop invariant init | --- | --- | --- | --- | |||

split_all_full | |||||||

loop invariant init | --- | --- | --- | 1.53 | |||

loop invariant init | --- | --- | 0.15 | --- | |||

assertion | --- | --- | --- | --- | |||

split_goal_right | |||||||

VC for main | 0.02 | --- | --- | --- | |||

VC for main | 0.02 | --- | --- | --- | |||

VC for main | 0.03 | --- | --- | --- | |||

VC for main | 0.62 | --- | --- | --- | |||

VC for main | 0.62 | --- | --- | --- | |||

VC for main | 0.06 | --- | --- | --- | |||

VC for main | 0.22 | --- | --- | --- | |||

VC for main | 0.09 | --- | --- | --- | |||

VC for main | 0.11 | --- | --- | --- | |||

VC for main | 0.03 | --- | --- | --- | |||

VC for main | 0.24 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

precondition | 0.02 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

loop invariant init | 0.03 | --- | --- | --- | |||

loop invariant init | 0.05 | --- | --- | --- | |||

assertion | --- | --- | --- | --- | |||

split_goal_right | |||||||

VC for main | --- | 0.14 | --- | --- | |||

VC for main | 0.14 | --- | --- | --- | |||

VC for main | 0.11 | --- | --- | --- | |||

VC for main | --- | 0.40 | --- | --- | |||

VC for main | --- | --- | --- | 0.17 | |||

VC for main | 0.50 | --- | --- | --- | |||

VC for main | 0.02 | --- | --- | --- | |||

VC for main | 0.01 | --- | --- | --- | |||

VC for main | --- | --- | --- | 0.18 | |||

VC for main | --- | --- | --- | 0.18 | |||

VC for main | 0.44 | --- | --- | --- | |||

VC for main | --- | --- | --- | 0.16 | |||

VC for main | --- | --- | --- | 0.20 | |||

VC for main | --- | --- | --- | 0.17 | |||

VC for main | --- | 0.07 | --- | --- | |||

VC for main | --- | --- | --- | 0.22 | |||

VC for main | 0.05 | --- | --- | --- | |||

VC for main | 0.02 | --- | --- | --- | |||

VC for main | 0.03 | --- | --- | --- | |||

VC for main | 0.06 | --- | --- | --- | |||

VC for main | --- | --- | --- | 0.15 | |||

VC for main | 0.11 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

precondition | 0.02 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

precondition | 0.02 | --- | --- | --- | |||

index in array bounds | 0.03 | --- | --- | --- | |||

loop invariant preservation | 0.05 | --- | --- | --- | |||

loop invariant preservation | 1.32 | --- | --- | --- | |||

index in array bounds | 0.03 | --- | --- | --- | |||

precondition | 0.66 | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | |||

assertion | --- | --- | --- | --- | |||

split_goal_right | |||||||

assertion | 0.25 | --- | --- | --- | |||

VC for main | 0.03 | --- | --- | --- | |||

VC for main | 0.02 | --- | --- | --- | |||

VC for main | 0.04 | --- | --- | --- | |||

VC for main | 0.03 | --- | --- | --- | |||

VC for main | 0.14 | --- | --- | --- | |||

VC for main | 0.04 | --- | --- | --- | |||

VC for main | 0.05 | --- | --- | --- | |||

VC for main | 0.09 | --- | --- | --- | |||

VC for main | 0.02 | --- | --- | --- | |||

VC for main | 0.09 | --- | --- | --- | |||

VC for main | 0.19 | --- | --- | --- | |||

VC for main | 0.04 | --- | --- | --- | |||

VC for main | 0.04 | --- | --- | --- | |||

assertion | --- | --- | --- | --- | |||

split_goal_right | |||||||

VC for main | 0.03 | --- | --- | --- | |||

VC for main | 0.08 | --- | --- | --- | |||

loop invariant preservation | 0.33 | --- | --- | --- | |||

out of loop bounds | 0.02 | --- | --- | --- | |||

assertion | 0.02 | --- | --- | --- | |||

assertion | 0.01 | --- | --- | --- | |||

out of loop bounds | 0.01 | --- | --- | --- |