Wiki Agenda Contact Version française

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: 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:set '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:set 'a) (q:'b -> bool)
                           (f:'a -> 'b) (g:'b -> 'a) : set '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 = choose 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:set '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 = choose 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 : set '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 empty;
  assert { forall s. mem s count[0].cset <-> valid_coloring_l 0 s };
  count[1] <- cone (black ++ empty);
  assert { forall s. mem s count[1].cset <-> valid_coloring_l 1 s };
  count[2] <- cone (black ++ (black ++ empty));
  assert { forall s. mem s count[2].cset <-> valid_coloring_l 2 s };
  count[3] <- { card = 2;
                cset = F.add (red 3 ++ empty)
                             (F.singleton (black ++ (black ++
                                                    (black ++ 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

ObligationsAlt-Ergo 2.0.0CVC4 1.5
VC bij_preserve------
split_goal_right
VC bij_preserve.00.01---
VC bij_preserve.10.06---
VC bij_preserve.2---0.03
VC bij_preserve.30.02---
VC disjoint_union0.27---
VC cardinal0.00---
VC czero0.00---
VC cone0.00---
VC cmap0.01---
VC cadd0.00---
VC main------
split_goal_right
VC main.00.00---
VC main.10.01---
VC main.20.05---
VC main.30.01---
VC main.40.27---
VC main.50.02---
VC main.60.72---
VC main.70.51---
VC main.80.02---
VC main.92.01---
VC main.10------
split_goal_right
VC main.10.02.98---
VC main.10.1---0.15
VC main.11------
split_goal_right
VC main.11.00.02---
VC main.11.10.01---
VC main.11.20.03---
VC main.11.30.45---
VC main.11.40.20---
VC main.11.50.06---
VC main.11.60.16---
VC main.11.70.15---
VC main.11.80.06---
VC main.11.90.05---
VC main.11.100.26---
VC main.120.02---
VC main.130.02---
VC main.140.03---
VC main.150.03---
VC main.160.05---
VC main.17------
split_goal_right
VC main.17.00.22---
VC main.17.10.21---
VC main.17.20.17---
VC main.17.3------
introduce_premises
VC main.17.3.0------
inline_goal
VC main.17.3.0.0------
split_goal_right
VC main.17.3.0.0.00.70---
VC main.17.3.0.0.14.44---
VC main.17.3.0.0.24.48---
VC main.17.40.05---
VC main.17.50.30---
VC main.17.60.02---
VC main.17.70.02---
VC main.17.80.04---
VC main.17.90.02---
VC main.17.100.29---
VC main.17.110.10---
VC main.17.120.02---
VC main.17.130.02---
VC main.17.140.19---
VC main.17.150.49---
VC main.17.160.03---
VC main.17.170.08---
VC main.17.180.03---
VC main.17.190.11---
VC main.17.200.02---
VC main.17.210.11---
VC main.180.02---
VC main.190.02---
VC main.200.03---
VC main.210.04---
VC main.220.02---
VC main.230.05---
VC main.240.56---
VC main.250.02---
VC main.260.52---
VC main.270.02---
VC main.28------
split_goal_right
VC main.28.00.25---
VC main.28.10.03---
VC main.28.20.02---
VC main.28.30.08---
VC main.28.40.03---
VC main.28.50.14---
VC main.28.60.04---
VC main.28.70.05---
VC main.28.80.09---
VC main.28.90.02---
VC main.28.100.09---
VC main.28.110.18---
VC main.28.120.04---
VC main.28.130.04---
VC main.29------
split_goal_right
VC main.29.00.03---
VC main.29.10.08---
VC main.300.33---
VC main.310.02---
VC main.320.02---
VC main.330.01---
VC main.340.01---