Wiki Agenda Contact Version française

VerifyThis 2018: le rouge et le noir

solution to VerifyThis 2018 challenge 2


Authors: Raphaël Rieu-Helft

Topics: Array Data Structure / Algorithms / Mathematics

Tools: Why3

References: VerifyThis @ ETAPS 2018 / Project Euler

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


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

Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)

module ColoredTiles

use int.Int
use set.Fset
use seq.Seq

type color = Red | Black

type coloring = seq color

predicate tworedneighbors (c: coloring) (i:int)
  = ((c[i-2] = Red /\ c[i-1] = Red /\ 2 <= i)
     \/ (c[i-1] = Red /\ c[i+1] = Red /\ 1 <= i <= length c - 2)
     \/ (c[i+1] = Red /\ c[i+2] = Red /\ i <= length c - 3))

predicate valid (c:coloring) =
  forall i. 0 <= i < length c -> c[i] = Red -> tworedneighbors c i

function black (_n:int) : color = Black
function red (_n:int) : color = Red

function colorings0 : fset coloring = add (create 0 black) Fset.empty
function colorings1 : fset coloring = add (create 1 black) Fset.empty
function colorings2 : fset coloring = add (create 2 black) Fset.empty
function colorings3: fset coloring =
         add (create 3 red) (add (create 3 black) Fset.empty)

lemma valid_contr:
  forall c i. valid c -> 0 <= i < length c -> not (tworedneighbors c i) -> c[i] = Black

lemma colo_0 : forall c: coloring. length c = 0 ->
      (valid c <-> mem c colorings0 by Seq.(==) c (create 0 black))

lemma colo_1 : forall c: coloring. length c = 1 ->
      (valid c <-> mem c colorings1
                   by c[0] = Black
                   so Seq.(==) c (create 1 black))

lemma colo_2 : forall c: coloring. length c = 2 ->
      (valid c <-> mem c colorings2
                   by c[0] = Black = c[1]
                   so Seq.(==) c (create 2 black)
                   so c = create 2 black)

lemma colo_3 : forall c: coloring. length c = 3 ->
      (valid c <-> mem c colorings3
                   by if c[0] = Black
                      then (c[0]=c[1]=c[2]=Black
                            so c == create 3 black
                            so c = create 3 black)
                      else (c[0]=c[1]=c[2]=Red
                            so c == create 3 red
                            so c = create 3 red))

let lemma valid_split_fb (c:coloring) (k: int)
  requires { 3 <= k < length c }
  requires { forall i. 0 <= i < k -> c[i] = Red }
  requires { valid c[k+1 ..] }
  ensures  { valid c }
= let c' = c[k+1 ..] in
  assert { forall i. k+1 <= i < length c -> c[i] = Red ->
             (tworedneighbors c i
              by c'[i - (k+1)] = Red
              so [@case_split] tworedneighbors c' (i - (k+1))) }

let lemma valid_restrict (c: coloring) (k: int)
  requires { valid c }
  requires { 0 <= k < length c }
  requires { c[k] = Black }
  ensures  { valid c[k+1 ..] }
= ()

(*1st black tile starting at i *)
let rec function first_black_tile (c:coloring) : int
  ensures { 0 <= result <= length c }
  ensures { forall j. 0 <= j < result <= length c
            -> c[j] = Red }
  ensures { result < length c -> c[result] = Black }
  ensures { valid c -> result = 0 \/ 3 <= result }
  variant { length c }
= if Seq.length c = 0 then 0
  else match c[0] with
       | Black -> 0
       | Red ->
           assert { valid c -> c[1]=Red /\ c[2] = Red };
           let r = first_black_tile c[1 ..] in
           assert { forall j. 1 <= j < 1+r
                    -> c[j] = Red
                       by c[1 ..][j-1] = Red };
           1+r end

let rec function addleft (nr:int) (c:coloring) : coloring
  variant { nr }
  ensures { nr >= 0 -> Seq.length result = Seq.length c + nr + 1 }
= if nr <= 0 then cons Black c
  else cons Red (addleft (nr-1) c)

(* add nr red tiles and a black tile to the left of each coloring *)
function mapaddleft (s:fset coloring) (nr:int) : fset coloring
=  map (addleft nr) s

lemma addleft_fb:
  forall c nr. 0 <= nr -> first_black_tile (addleft nr c) = nr

lemma mapaddleft_fb:
  forall s c nr. 0 <= nr -> mem c (mapaddleft s nr) -> first_black_tile c = nr

predicate reciprocal (f: 'a -> 'b) (g: 'b -> 'a)
  = forall y. g (f y) = y

let lemma bij_image (u: fset 'a) (f: 'a -> 'b) (g: 'b -> 'a)
  requires { reciprocal f g }
  ensures  { subset u (map g (map f u)) }
= assert { forall x. mem x u -> mem (f x) (map f u)
                     -> mem (g (f x)) (map g (map f u))
                     -> mem x (map g (map f u)) }

let lemma bij_cardinal (u: fset 'a) (f: 'a -> 'b) (g: 'b -> 'a)
  requires { reciprocal f g }
  ensures  { cardinal (map f u) = cardinal u }
= assert { cardinal (map f u) <= cardinal u };
  assert { cardinal (map g (map f u)) <= cardinal (map f u) };
  assert { cardinal u <= cardinal (map g (map f u)) }

function rmleft (nr:int) (c:coloring) : coloring = c[nr+1 ..]

use seq.FreeMonoid

lemma ext: forall c1 c2: coloring. Seq.(==) c1 c2 -> c1 = c2
lemma app_eq: forall c1 c2 c3 c4: coloring. c1 = c2 -> c3 = c4 -> c1 ++ c3 = c2 ++ c4

let rec lemma addleft_result (c:coloring) (nr:int)
  requires { 0 <= nr }
  ensures  { addleft nr c = (Seq.create nr red) ++ (cons Black c) }
  variant  { nr }
= if nr = 0 then assert { addleft nr c = (Seq.create nr red) ++ (cons Black c) }
  else begin
    let cnr = create nr red in
    let cnrm = create (nr - 1) red in
    addleft_result c (nr-1);
    assert { addleft (nr-1) c = cnrm ++ cons Black c };
    assert { cons Red cnrm = cnr
               by Seq.(==) (cons Red cnrm) cnr };
    assert { addleft nr c = cnr ++ cons Black c
             by addleft nr c
                = cons Red (addleft (nr-1) c)
                = cons Red (cnrm ++ cons Black c)
                = (cons Red cnrm) ++ cons Black c
                = cnr ++ cons Black c }
  end

let lemma addleft_bijective (nr:int)
  requires { 0 <= nr }
  ensures  { reciprocal (addleft nr) (rmleft nr) }
= assert { forall c i. 0 <= i < length c -> (rmleft nr (addleft nr c))[i] = c[i] };
  assert { forall c. Seq.(==) (rmleft nr (addleft nr c)) c }

let lemma mapaddleft_card (s: fset coloring) (nr: int)
  requires { 0 <= nr }
  ensures  { cardinal (mapaddleft s nr) = cardinal s }
= addleft_bijective nr;
  bij_cardinal s (addleft nr) (rmleft nr)

let lemma addleft_valid (c:coloring) (nr:int)
  requires { nr = 0 \/ 3 <= nr }
  requires { valid c }
  ensures  { valid (addleft nr c) }
= addleft_result c nr;
  if nr = 0 then assert { valid (addleft 0 c) }
  else valid_split_fb (addleft nr c) nr

let lemma mapaddleft_valid (s: fset coloring) (nr: int)
  requires { forall c. mem c s -> valid c }
  requires { nr = 0 \/ 3 <= nr }
  ensures  { forall c. mem c (mapaddleft s nr) -> valid c }
= assert { forall c. mem c (mapaddleft s nr) ->
                     valid c
                     by mem c (map (addleft nr) s)
                     so (exists y. mem y s /\ c = addleft nr y) }

let lemma mapaddleft_length (s: fset coloring) (nr: int) (l1 l2: int)
  requires { forall c. mem c s -> Seq.length c = l1 }
  requires { 0 <= nr }
  requires { l2 = l1 + nr + 1 }
  ensures  { forall c. mem c (mapaddleft s nr) -> Seq.length c = l2 }
= ()

let rec ghost disjoint_union (s1 s2: fset coloring) : fset coloring
  requires { forall x. mem x s1 -> not mem x s2 }
  ensures  { result = union s1 s2 }
  ensures  { cardinal result = cardinal s1 + cardinal s2 }
  variant  { cardinal s1 }
= if is_empty s1
  then begin
    assert { union s1 s2 = s2
             by (forall x. mem x (union s1 s2)
                -> mem x s1 \/ mem x s2 -> mem x s2)
             so subset (union s1 s2) s2 };
    s2
  end
  else
    let x = pick s1 in
    let s1' = remove x s1 in
    let s2' = add x s2 in
    let u = disjoint_union s1' s2' in
    assert { u = union s1 s2
             by u = union s1' s2'
             so (forall y. (mem y s2' <-> (mem y s2 \/ y = x)))
             so (forall y. ((mem y s1' \/ y = x) <-> mem y s1))
             so (forall y. mem y u <-> mem y s1' \/ mem y s2'
                       <-> mem y s1' \/ mem y s2 \/ y = x
                       <-> mem y s1 \/ mem y s2
                       <-> mem y (union s1 s2))
             so (forall y. mem y u <-> mem y (union s1 s2))
             so Fset.(==) u (union s1 s2)};
    u

use array.Array

let enum () : (count: array int, ghost sets: array (fset coloring))
  ensures { Array.length count = 51 = Array.length sets
            /\ (forall i. 0 <= i <= 50 ->
               (forall c: coloring. Seq.length c = i ->
                          (valid c <-> mem c (sets[i]))))
            /\ (forall i. 0 <= i < 50 ->
                          count[i] = cardinal (sets[i])) }
= let count = Array.make 51 0 in
  let ghost sets : array (fset coloring) = Array.make 51 Fset.empty in
  count[0] <- 1;
  sets[0] <- colorings0;
  assert { forall c. ((Seq.length c = 0 /\ valid c) <-> mem c (sets[0])) };
  count[1] <- 1;
  sets[1] <- colorings1;
  assert { forall i c. (i=0 \/ i=1)
           -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
  count[2] <- 1;
  sets[2] <- colorings2;
  assert { forall i c. (i=0 \/ i=1 \/ i=2)
           -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
  count[3] <- 2;
  sets[3] <- colorings3;
  assert { sets[3] = colorings3 };
  assert { forall i c. (i=0 \/ i=1 \/ i=2 \/ i = 3)
           -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
  assert { cardinal colorings3 = 2 };
  for n = 4 to 50 do
    invariant { forall c i. 0 <= i < n -> Seq.length c = i ->
                         valid c -> mem c (sets[i]) }
    invariant { forall c i. 0 <= i < n -> mem c (sets[i]) ->
                         (Seq.length c = i /\ valid c) }
    invariant { forall i. 0 <= i < n ->
                         count[i] = cardinal (sets[i]) }
    label StartLoop in
    (* colorings with first_black_tile = 0 *)
    count[n] <- count[n-1];
    mapaddleft_valid (sets[n-1]) 0;
    sets[n] <- mapaddleft (sets[n-1]) 0;
    assert { forall i. 0 <= i < n -> sets[i] = sets[i] at StartLoop };
    assert { forall i. 0 <= i < n -> count[i] = count[i] at StartLoop };
    assert { forall c. Seq.length c = n -> valid c -> first_black_tile c < 3 ->
                       mem c sets[n]
                       by first_black_tile c = 0
                       so valid c[1 ..]
                       so mem c[1 ..] (sets[n-1])
                       so addleft 0 c[1 ..] = c
                       so mem c (mapaddleft sets[n-1] 0) };
    for k = 3 to n-1 do
      invariant { forall c i. 0 <= i < n -> Seq.length c = i ->
                           valid c -> mem c (sets[i]) }
      invariant { forall c i. 0 <= i < n -> mem c (sets[i]) ->
                             (Seq.length c = i /\ valid c) }
      invariant { forall i. 0 <= i < n ->
                            count[i] = cardinal (sets[i]) }
      invariant { forall c. (mem c (sets[n]) <->
                            (Seq.length c = n /\ valid c
                            /\ first_black_tile c < k)) }
      invariant { count[n] = cardinal (sets[n]) }
      label InnerLoop in
      (* colorings with first_black_tile = k *)
      count[n] <- count [n] + count [n-k-1];
      mapaddleft_length (sets[n-k-1]) k (n-k-1) n;
      mapaddleft_valid  (sets[n-k-1]) k;
      mapaddleft_card   (sets[n-k-1]) k;
      let ghost ns = mapaddleft sets[n-k-1] k in
      assert { forall c. mem c ns -> first_black_tile c = k };
      assert { forall c. Seq.length c = n -> valid c -> first_black_tile c = k
                         -> mem c ns
                         by valid c[k+1 ..]
                         so mem c[k+1 ..] (sets[n-k-1])
                         so let c' = addleft k c[k+1 ..] in
                            ((forall i. 0 <= i < n -> Seq.get c i = Seq.get c' i)
                             by c[k+1 ..] = c'[k+1 ..])
                         so Seq.(==) c' c
                         so c' = c
                         so mem c (mapaddleft sets[n-k-1] k) };
      sets[n] <- disjoint_union (sets[n]) ns;
      assert { forall i. 0 <= i < n -> sets[i] = sets[i] at InnerLoop };
      assert { forall i. 0 <= i < n -> count[i] = count[i] at InnerLoop };
    done;
    (* coloring with first_black_tile = n *)
    label LastAdd in
    let ghost r = Seq.create n red in
    let ghost sr = Fset.singleton r in
    assert { forall c. mem c sets[n] -> first_black_tile c < n };
    assert { first_black_tile r = n };
    assert { valid r /\ Seq.length r = n };
    count[n] <- count[n]+1;
    sets[n] <- disjoint_union (sets[n]) sr;
    assert { forall c. mem c sets[n] -> valid c /\ Seq.length c = n
                       by [@case_split] mem c (sets[n] at LastAdd) \/ mem c sr };
    assert { forall c. Seq.length c = n -> first_black_tile c = n ->
                       mem c sets[n]
                       by (forall k. 0 <= k < n -> Seq.get c k = Red)
                       so c == r so c = r };
    assert { forall i. 0 <= i < n -> sets[i] = sets[i] at LastAdd };
    assert { forall i. 0 <= i < n -> count[i] = count[i] at LastAdd };
  done;
  count, sets

end

download ZIP archive

Why3 Proof Results for Project "verifythis_2018_le_rouge_et_le_noir_1"

Theory "verifythis_2018_le_rouge_et_le_noir_1.ColoredTiles": fully verified

ObligationsAlt-Ergo 2.3.3CVC4 1.8Z3 4.8.10
valid_contr0.01------
colo_0---------
split_vc
colo_0.00.01------
colo_0.10.01------
colo_0.2---0.08---
colo_1---------
split_vc
colo_1.00.01------
colo_1.10.01------
colo_1.20.02------
colo_1.3---0.08---
colo_2---------
split_vc
colo_2.00.01------
colo_2.10.01------
colo_2.20.02------
colo_2.30.01------
colo_2.40.11------
colo_2.5---0.09---
colo_3---------
split_vc
colo_3.00.01------
colo_3.10.01------
colo_3.20.01------
colo_3.30.01------
colo_3.40.01------
colo_3.50.01------
colo_3.60.12------
colo_3.70.01------
colo_3.80.17------
colo_3.90.02------
colo_3.100.30------
colo_3.11---0.21---
VC for valid_split_fb---------
split_vc
precondition0.01------
assertion---------
split_vc
assertion0.02------
VC for valid_split_fb0.02------
VC for valid_split_fb0.08------
postcondition0.12------
VC for valid_restrict---------
split_vc
postcondition---------
split_all_full
postcondition0.48------
VC for first_black_tile---------
split_vc
assertion0.02------
precondition0.01------
variant decrease0.01------
assertion---------
split_vc
assertion0.02------
VC for first_black_tile0.04------
postcondition0.02------
postcondition0.02------
postcondition0.04------
postcondition0.03------
VC for addleft---------
split_vc
variant decrease0.01------
postcondition0.01------
addleft_fb---------
introduce_premises
addleft_fb.0---------
induction nr
base case0.02------
recursive case---------
split_all_full
recursive case------0.08
mapaddleft_fb0.02------
VC for bij_image---------
split_vc
assertion0.01------
postcondition0.02------
VC for bij_cardinal---------
split_vc
assertion0.01------
assertion0.01------
assertion0.02------
postcondition0.01------
ext0.01------
app_eq0.01------
VC for addleft_result---------
split_vc
assertion0.06------
precondition0.01------
precondition0.01------
variant decrease0.01------
precondition0.01------
assertion---0.10---
assertion---------
split_vc
assertion2.00------
VC for addleft_result0.02------
assertion0.04------
postcondition---2.86---
VC for addleft_bijective---------
split_vc
assertion0.25------
assertion0.07------
postcondition0.02------
VC for mapaddleft_card---------
split_vc
precondition0.01------
precondition0.01------
postcondition0.01------
VC for addleft_valid---------
split_vc
precondition0.01------
assertion---1.79---
precondition0.02------
precondition0.02------
precondition0.12------
postcondition0.01------
VC for mapaddleft_valid0.06------
VC for mapaddleft_length0.03------
VC for disjoint_union---------
split_vc
assertion0.02------
variant decrease0.01------
precondition0.02------
assertion---------
split_vc
assertion0.01------
VC for disjoint_union0.02------
VC for disjoint_union0.02------
VC for disjoint_union0.02------
VC for disjoint_union0.01------
VC for disjoint_union0.01------
VC for disjoint_union0.01------
VC for disjoint_union0.01------
VC for disjoint_union0.02------
VC for disjoint_union0.01------
VC for disjoint_union0.01------
VC for disjoint_union0.01------
VC for disjoint_union0.01------
VC for disjoint_union0.03------
VC for disjoint_union0.02------
VC for disjoint_union0.02------
VC for disjoint_union0.02------
postcondition0.01------
postcondition0.05------
VC for enum---------
split_vc
array creation size0.01------
array creation size0.01------
index in array bounds0.01------
index in array bounds0.01------
assertion0.03------
index in array bounds0.01------
index in array bounds0.01------
assertion0.22------
index in array bounds0.01------
index in array bounds0.01------
assertion---0.42---
index in array bounds0.02------
index in array bounds0.02------
assertion---0.19---
assertion---------
case i=3
true case (assertion)---------
rewrite h
true case (assertion)---------
rewrite Assert
true case (assertion)---------
split_all_full
VC for enum---------
introduce_premises
VC for enum---------
apply colo_31
apply premises0.02------
apply premises0.02------
VC for enum0.10------
VC for enum---------
introduce_premises
VC for enum---------
apply colo_3
apply premises0.10------
apply premises---------
apply H
false case (assertion)0.21------
assertion0.70------
loop invariant init0.04------
loop invariant init0.06------
loop invariant init---------
assert (i=0\/i=1\/i=2\/i=3)
asserted formula0.02------
loop invariant init---------
revert h
loop invariant init---------
split_all_full
loop invariant init0.48------
loop invariant init0.46------
loop invariant init0.45------
loop invariant init---------
introduce_premises
loop invariant init---------
replace i 3
loop invariant init---------
replace sets[3] colorings3
loop invariant init---------
rewrite Assert
loop invariant init0.04------
equality hypothesis---0.20---
equality hypothesis0.03------
index in array bounds0.02------
index in array bounds0.02------
index in array bounds0.02------
precondition0.03------
precondition0.02------
index in array bounds0.02------
index in array bounds0.03------
assertion0.07------
assertion0.07------
assertion---------
split_vc
assertion0.05------
VC for enum0.05------
VC for enum0.31------
VC for enum0.05------
VC for enum0.14------
VC for enum0.05------
loop invariant init0.12------
loop invariant init0.12------
loop invariant init0.12------
loop invariant init1.23------
loop invariant init0.05------
index in array bounds0.03------
index in array bounds0.03------
index in array bounds0.03------
index in array bounds0.03------
precondition0.05------
precondition0.03------
precondition0.03------
index in array bounds0.03------
precondition0.05------
precondition0.03------
index in array bounds0.03------
precondition0.03------
index in array bounds0.04------
assertion0.05------
assertion---------
split_vc
assertion0.06------
VC for enum0.36------
VC for enum2.72------
VC for enum---------
case i<k
true case0.11------
false case---------
case i=k
false case (true case)0.19------
false case---------
assert (get1 c i = get1 c[k+1 ..] (i-k-1))
asserted formula0.70------
false case0.74------
VC for enum0.62------
VC for enum0.05------
VC for enum0.18------
VC for enum0.04------
index in array bounds0.03------
precondition0.05------
index in array bounds0.04------
assertion0.08------
assertion0.09------
loop invariant preservation0.18------
loop invariant preservation0.16------
loop invariant preservation0.14------
loop invariant preservation0.34------
loop invariant preservation0.06------
precondition0.03------
assertion0.04------
assertion0.32------
assertion---------
introduce_premises
assertion---------
inline_goal
assertion0.34------
index in array bounds0.03------
index in array bounds0.03------
index in array bounds0.03------
precondition0.06------
index in array bounds0.04------
assertion---------
split_vc
assertion0.14------
VC for enum0.09------
VC for enum0.09------
assertion---------
split_all_full
VC for enum0.06------
VC for enum0.18------
VC for enum0.06------
VC for enum0.56------
assertion0.09------
assertion0.09------
loop invariant preservation0.43------
loop invariant preservation0.28------
loop invariant preservation0.29------
out of loop bounds0.03------
postcondition0.19------
VC for enum0.02------