Commit dd2a8ea8 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

verifythis 2018 : Martin's solution to challenge 2

parent 2c36c66d
(**
{1 VerifyThis @ ETAPS 2018 competition
Challenge 2: Le rouge et le noir}
Author: Martin Clochard (LRI, Université Paris Sud)
*)
use import 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 import 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 }
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../challenge2.mlw" proved="true">
<theory name="Top" proved="true">
<goal name="VC bij_preserve" expl="VC for bij_preserve" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC bij_preserve.0" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC bij_preserve.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="158"/></proof>
</goal>
<goal name="VC bij_preserve.2" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC bij_preserve.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="64"/></proof>
</goal>
</transf>
</goal>
<goal name="VC disjoint_union" expl="VC for disjoint_union" proved="true">
<proof prover="0"><result status="valid" time="0.27" steps="1122"/></proof>
</goal>
<goal name="VC cardinal" expl="VC for cardinal" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC czero" expl="VC for czero" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC cone" expl="VC for cone" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC cmap" expl="VC for cmap" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC cadd" expl="VC for cadd" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="VC main" expl="VC for main" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.0" expl="array creation size" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC main.1" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC main.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="309"/></proof>
</goal>
<goal name="VC main.3" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC main.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.27" steps="861"/></proof>
</goal>
<goal name="VC main.5" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="VC main.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.72" steps="1951"/></proof>
</goal>
<goal name="VC main.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.51" steps="544"/></proof>
</goal>
<goal name="VC main.8" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC main.9" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="2.01" steps="4248"/></proof>
</goal>
<goal name="VC main.10" expl="loop invariant init" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.10.0" expl="loop invariant init" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="3.53" steps="5327"/></proof>
</goal>
<goal name="VC main.10.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.11" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.11.0" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC main.11.1" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="43"/></proof>
</goal>
<goal name="VC main.11.2" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="103"/></proof>
</goal>
<goal name="VC main.11.3" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.80" steps="623"/></proof>
</goal>
<goal name="VC main.11.4" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.20" steps="459"/></proof>
</goal>
<goal name="VC main.11.5" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="281"/></proof>
</goal>
<goal name="VC main.11.6" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="386"/></proof>
</goal>
<goal name="VC main.11.7" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="353"/></proof>
</goal>
<goal name="VC main.11.8" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="254"/></proof>
</goal>
<goal name="VC main.11.9" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="248"/></proof>
</goal>
<goal name="VC main.11.10" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="808"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.12" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC main.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC main.14" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="VC main.15" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
<goal name="VC main.16" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="240"/></proof>
</goal>
<goal name="VC main.17" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.17.0" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.42" steps="406"/></proof>
</goal>
<goal name="VC main.17.1" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.21" steps="288"/></proof>
</goal>
<goal name="VC main.17.2" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="355"/></proof>
</goal>
<goal name="VC main.17.3" expl="VC for main" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC main.17.3.0" expl="VC for main" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC main.17.3.0.0" expl="VC for main" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.17.3.0.0.0" expl="VC for main" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="1.32" steps="1358"/></proof>
</goal>
<goal name="VC main.17.3.0.0.1" expl="VC for main" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="7.14" steps="4075"/></proof>
</goal>
<goal name="VC main.17.3.0.0.2" expl="VC for main" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="5.84" steps="2460"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC main.17.4" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="120"/></proof>
</goal>
<goal name="VC main.17.5" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.54" steps="701"/></proof>
</goal>
<goal name="VC main.17.6" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC main.17.7" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC main.17.8" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="131"/></proof>
</goal>
<goal name="VC main.17.9" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="VC main.17.10" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.49" steps="405"/></proof>
</goal>
<goal name="VC main.17.11" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="184"/></proof>
</goal>
<goal name="VC main.17.12" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="55"/></proof>
</goal>
<goal name="VC main.17.13" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
</goal>
<goal name="VC main.17.14" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.19" steps="396"/></proof>
</goal>
<goal name="VC main.17.15" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.92" steps="736"/></proof>
</goal>
<goal name="VC main.17.16" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="51"/></proof>
</goal>
<goal name="VC main.17.17" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="55"/></proof>
</goal>
<goal name="VC main.17.18" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="131"/></proof>
</goal>
<goal name="VC main.17.19" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="220"/></proof>
</goal>
<goal name="VC main.17.20" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
<goal name="VC main.17.21" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.33" steps="565"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.18" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="43"/></proof>
</goal>
<goal name="VC main.19" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="43"/></proof>
</goal>
<goal name="VC main.20" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
<goal name="VC main.21" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="72"/></proof>
</goal>
<goal name="VC main.22" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
<goal name="VC main.23" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="128"/></proof>
</goal>
<goal name="VC main.24" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.56" steps="1131"/></proof>
</goal>
<goal name="VC main.25" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC main.26" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="1066"/></proof>
</goal>
<goal name="VC main.27" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC main.28" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.28.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.25" steps="538"/></proof>
</goal>
<goal name="VC main.28.1" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="49"/></proof>
</goal>
<goal name="VC main.28.2" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="VC main.28.3" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="137"/></proof>
</goal>
<goal name="VC main.28.4" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="61"/></proof>
</goal>
<goal name="VC main.28.5" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="340"/></proof>
</goal>
<goal name="VC main.28.6" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="176"/></proof>
</goal>
<goal name="VC main.28.7" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="58"/></proof>
</goal>
<goal name="VC main.28.8" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="196"/></proof>
</goal>
<goal name="VC main.28.9" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="VC main.28.10" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="184"/></proof>
</goal>
<goal name="VC main.28.11" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.35" steps="574"/></proof>
</goal>
<goal name="VC main.28.12" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="66"/></proof>
</goal>
<goal name="VC main.28.13" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="218"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.29" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC main.29.0" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="134"/></proof>
</goal>
<goal name="VC main.29.1" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="315"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.30" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.33" steps="1031"/></proof>
</goal>
<goal name="VC main.31" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="38"/></proof>
</goal>
<goal name="VC main.32" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC main.33" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC main.34" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
(**
{1 VerifyThis @ ETAPS 2018 competition
Challenge 2: Le rouge et le noir}
Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)
*)
module ColoredTiles
use import int.Int
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment