examples/verifythis_2018_le_rouge_et_le_noir_2.mlw

   1 (**
   2
   3 {1 VerifyThis @ ETAPS 2018 competition
   4    Challenge 2: Le rouge et le noir}
   5
   6 Author: Martin Clochard (LRI, Université Paris Sud)
   7 *)
   8
   9 use int.Int
  10 use import set.Fset as F
  11
  12 (* The part about bijections, preservation of finiteness and cardinality,
  13    should be moved somewhere in stdlib. *)
  14 predicate bijection (p:fset 'a) (q:'b -> bool) (f:'a -> 'b) (g:'b -> 'a) =
  15   (forall x. mem x p -> q (f x) /\ g (f x) = x)
  16   /\ (forall x. q x -> mem (g x) p /\ f (g x) = x)
  17
  18 let rec ghost bij_preserve (p:fset 'a) (q:'b -> bool)
  19                            (f:'a -> 'b) (g:'b -> 'a) : fset 'b
  20   requires { bijection p q f g }
  21   ensures  { forall x. q x <-> mem x result }
  22   ensures  { cardinal p = cardinal result }
  23   variant  { cardinal p }
  24 = if cardinal p = 0 then empty else
  25   let x = pick p in
  26   add (f x) (bij_preserve (remove x p) (fun y -> pure { q y /\ y <> f x}) f g)
  27
  28 let rec ghost disjoint_union (p q:fset 'a) : unit
  29   requires { forall x. not (mem x p /\ mem x q) }
  30   ensures  { cardinal (union p q) = cardinal p + cardinal q }
  31   variant  { cardinal p }
  32 = if cardinal p = 0 then assert { union p q == q } else
  33   let x = pick p in
  34   assert { union (remove x p) q == remove x (union p q) };
  35   disjoint_union (remove x p) q
  36
  37 (* Abstraction layer over the integers. Reduce to standard integers
  38    after ghost code erasure (=ghost wrapping of integers operation for
  39    proof purposes). *)
  40 type cardinal 'a = {
  41   card : int;
  42   ghost cset : fset 'a;
  43 } invariant { card = cardinal cset }
  44 by { card = 0; cset = empty }
  45
  46 let czero () : cardinal 'a
  47   ensures { result.cset = empty }
  48   ensures { result.card = 0 }
  49 = { card = 0; cset = empty }
  50 let cone (ghost x:'a) : cardinal 'a
  51   ensures { result.cset = singleton x }
  52   ensures { result.card = 1 }
  53 = { card = 1; cset = singleton x }
  54
  55 (* reduce to identity after ghost code erasure. *)
  56 let cmap (ghost q:'b -> bool)
  57          (ghost f:'a -> 'b)
  58          (ghost g:'b -> 'a) (i:cardinal 'a) : cardinal 'b
  59   requires { bijection i.cset q f g }
  60   ensures { forall x. mem x result.cset <-> q x }
  61   ensures { result.card = i.card }
  62 = { card = i.card; cset = bij_preserve i.cset q f g }
  63
  64 (* reduce to integer addition after ghost code erasure. *)
  65 let cadd (i1 i2:cardinal 'a) : cardinal 'a
  66   requires { forall x. not (mem x i1.cset /\ mem x i2.cset) }
  67   ensures  { result.cset = union i1.cset i2.cset }
  68   ensures  { result.card = i1.card + i2.card }
  69 = ghost disjoint_union i1.cset i2.cset;
  70   { card = i1.card + i2.card; cset = union i1.cset i2.cset }
  71
  72 (* Specification of colorings:
  73    sequence of tiles that can be obtained by catenating unit black tiles
  74    or large (>=3 units) red tiles, with red tiles being non-consecutive. *)
  75 type color = Red | Black
  76 use import seq.Seq as S
  77 constant black : seq color = singleton Black
  78 function red (n:int) : seq color = create n (fun _ -> Red)
  79 (* color is color of first square. Default to black for empty sequence,
  80    as a black tile does not give any constraints. *)
  81 inductive valid_coloring_f color (seq color) =
  82   | ValidEmpty : valid_coloring_f Black empty
  83   | ValidBlack : forall c s.
  84     valid_coloring_f c s -> valid_coloring_f Black (black++s)
  85   | ValidRed : forall n s. n >= 3 /\ valid_coloring_f Black s ->
  86     valid_coloring_f Red (red n ++ s)
  87
  88 predicate valid_coloring (s:seq color) =
  89   valid_coloring_f Red s \/ valid_coloring_f Black s
  90
  91 predicate valid_coloring_l (n:int) (s:seq color) =
  92   valid_coloring s /\ s.length = n
  93
  94 predicate valid_coloring_inter (n:int) (m:int) (s:seq color) =
  95   valid_coloring_l n s /\ exists i. 0 <= i < m /\ s[i] = Black
  96
  97 predicate valid_coloring_at (n:int) (m:int) (s:seq color) =
  98   valid_coloring_l n s /\ s[m] = Black /\ forall i. 0 <= i < m -> s[i] = Red
  99
 100 use array.Array
 101
 102
 103 let main () : unit
 104 = let count = Array.make 51 (czero ()) in
 105   count[0] <- cone S.empty;
 106   assert { forall s. mem s count[0].cset <-> valid_coloring_l 0 s };
 107   count[1] <- cone (black ++ S.empty);
 108   assert { forall s. mem s count[1].cset <-> valid_coloring_l 1 s };
 109   count[2] <- cone (black ++ (black ++ S.empty));
 110   assert { forall s. mem s count[2].cset <-> valid_coloring_l 2 s };
 111   count[3] <- { card = 2;
 112                 cset = F.add (red 3 ++ S.empty)
 113                              (F.singleton (black ++ (black ++
 114                                                     (black ++ S.empty)))); };
 115   assert { forall s. mem s count[3].cset <-> valid_coloring_l 3 s };
 116   for n = 4 to 50 do
 117     invariant { forall i s. 0 <= i < n ->
 118       valid_coloring_l i s <-> mem s count[i].cset }
 119     label L in
 120     let ghost q = pure { valid_coloring_inter n 3 } in
 121     let ghost f = pure { fun (s:seq color) -> black ++ s } in
 122     let ghost g = pure { fun (s:seq color) -> s[1 ..] } in
 123     assert { bijection count[n-1].cset q f g
 124       by (forall s. valid_coloring_l (n-1) s ->
 125         (valid_coloring_inter n 3 (black ++ s)
 126          by 0 <= 0 < (black ++ s).S.length /\ S.get (black++s) 0 = Black)
 127         /\ g (f s) == s)
 128       /\ (forall s. valid_coloring_inter n 3 s ->
 129         (valid_coloring_l (n-1) s[1 ..]
 130          /\ f (g s) == s)
 131         by (exists c s'. s = black ++ s' /\ valid_coloring_f c s'
 132           so s' == s[1 ..])
 133         \/ (false by exists i s'. 3 <= i /\ s = red i ++ s')
 134       ) };
 135     count[n] <- cmap q f g count[n-1];
 136     for k = 3 to n - 1 do
 137       invariant { forall i. 0 <= i < n -> count[i] = (count[i] at L) }
 138       invariant { forall s.
 139         valid_coloring_inter n k s <-> mem s count[n].cset
 140       }
 141       let ghost q = pure { valid_coloring_at n k } in
 142       let ghost f = pure { fun (s:seq color) -> red k ++ (black ++ s) } in
 143       let ghost g = pure { fun (s:seq color) -> s[k+1 ..] } in
 144       assert { bijection count[n-k-1].cset q f g
 145         by (forall s. g (f s) == s
 146           by forall i. 0 <= i < s.S.length ->
 147             S.get (g (f s)) i = S.get (f s) (i+k+1) = S.get s i)
 148         so (forall s. valid_coloring_l (n-k-1) s ->
 149           valid_coloring_at n k (f s) /\ g (f s) = s
 150         ) /\ (forall s. valid_coloring_at n k s ->
 151           valid_coloring_l (n-k-1) (g s) /\ f (g s) = s
 152           by (false by exists s'. s = black ++ s'
 153             so 0 <= 0 < k /\ S.get s 0 = Black)
 154           \/ (exists i s'.
 155             3 <= i /\ s = red i ++ s' /\ valid_coloring_f Black s'
 156             so s' <> empty so exists c s''.
 157               s' = black ++ s'' /\ valid_coloring_f c s''
 158             so (i = k by not (i < k so S.get s i = Black)
 159                       /\ not (i > k so S.get s k = Red))
 160             so s'' = g s by s = f s'')
 161         ) };
 162       count[n] <- cadd count[n] (cmap q f g count[n-k-1])
 163     done;
 164     count[n] <- cadd count[n] (cone (red n));
 165     assert { forall s. valid_coloring_l n s ->
 166       s = red n \/ valid_coloring_inter n n s
 167       by (exists s'. s = black ++ s'
 168         so 0 <= 0 < n /\ S.get s 0 = Black so valid_coloring_inter n n s)
 169       \/ (exists i s'. 3 <= i /\ s = red i ++ s' /\ valid_coloring_f Black s'
 170         so if i = n then s == red n else
 171         (s' <> empty by s'.S.length > 0)
 172         so exists s''. s' = black ++ s'' so 0 <= i < n /\ S.get s i = Black
 173         so valid_coloring_inter n n s
 174       )
 175     };
 176     assert { valid_coloring_l n (red n) by red n == red n ++ empty }
 177   done;
 178   (* Property asked by the problem. *)
 179   assert { forall s. valid_coloring_l 50 s <-> mem s count[50].cset };
 180   assert { count[50].card = cardinal count[50].cset }