Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 34f552b2 authored by Mario Pereira's avatar Mario Pereira
Browse files

New example in progres : Koda Ruskey (functional correctness done; missing...

New example in progres : Koda Ruskey (functional correctness done; missing proof of correctness for the number of forest colorings)
parent 4022988c
module KodaRuskey_Spec
use import map.Map
use import list.List
use import list.Append
use import int.Int
type color = White | Black
type forest =
| E
| N int forest forest
type coloring = map int color
function size_forest (f: forest) : int = match f with
| E -> 0
| N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
end
lemma size_forest_nonneg : forall f.
size_forest f >= 0
predicate mem_forest (n: int) (f: forest) = match f with
| E -> false
| N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
end
predicate between_range_forest (i j: int) (f: forest) =
forall n. mem_forest n f -> i <= n < j
predicate disjoint (f1 f2: forest) =
forall x. mem_forest x f1 -> mem_forest x f2 -> false
predicate no_repeated_forest (f: forest) = match f with
| E -> true
| N i f1 f2 ->
no_repeated_forest f1 && no_repeated_forest f2 &&
not (mem_forest i f1) && not (mem_forest i f2) &&
disjoint f1 f2
end
predicate valid_nums_forest (f: forest) (n: int) =
between_range_forest 0 n f &&
no_repeated_forest f
predicate white_forest (f: forest) (c: coloring) = match f with
| E -> true
| N i f1 f2 ->
c[i] = White && white_forest f1 c && white_forest f2 c
end
predicate valid_coloring (f: forest) (c: coloring) =
match f with
| E -> true
| N i f1 f2 ->
valid_coloring f2 c &&
match c[i] with
| White -> white_forest f1 c
| Black -> valid_coloring f1 c
end
end
function count_forest (f: forest) : int = match f with
| E -> 1
| N _ f1 f2 -> (1 + count_forest f1) * count_forest f2
end
lemma count_forest_nonneg:
forall f. count_forest f >= 1
predicate eq_coloring (n: int) (c1 c2: coloring) =
forall i. 0 <= i < n -> c1[i] = c2[i]
end
module Lemmas
use import map.Map
use import list.List
use import list.Append
use import int.Int
use import KodaRuskey_Spec
type stack = list forest
predicate mem_stack (n: int) (st: stack) = match st with
| Nil -> false
| Cons f tl -> mem_forest n f || mem_stack n tl
end
lemma mem_app: forall n st1 "induction" st2.
mem_stack n (st1 ++ st2) -> mem_stack n st1 || mem_stack n st2
function size_stack (st: stack) : int = match st with
| Nil -> 0
| Cons f st -> size_forest f + size_stack st
end
lemma size_stack_nonneg : forall st.
size_stack st >= 0
lemma white_forest_equiv:
forall f c.
white_forest f c <-> (forall i. mem_forest i f -> c[i] = White)
predicate even_forest (f: forest) = match f with
| E -> false
| N _ f1 f2 -> not (even_forest f1) || even_forest f2
end
predicate final_forest (f: forest) (c: coloring) = match f with
| E -> true
| N i f1 f2 ->
c[i] = Black && final_forest f1 c &&
if not (even_forest f1) then white_forest f2 c
else final_forest f2 c
end
predicate any_forest (f: forest) (c: coloring) =
white_forest f c || final_forest f c
lemma any_forest_frame:
forall f c1 c2.
(forall i. mem_forest i f -> c1[i] = c2[i]) ->
(final_forest f c1 -> final_forest f c2) &&
(white_forest f c1 -> white_forest f c2)
predicate unchanged (st: stack) (c1 c2: coloring) =
forall i. mem_stack i st -> c1[i] = c2[i]
predicate inverse (st: stack) (c1 c2: coloring) =
match st with
| Nil -> true
| Cons f st' ->
(white_forest f c1 && final_forest f c2 ||
final_forest f c1 && white_forest f c2) &&
if even_forest f then
unchanged st' c1 c2
else
inverse st' c1 c2
end
predicate any_stack (st: stack) (c: coloring) = match st with
| Nil -> true
| Cons f st -> (white_forest f c || final_forest f c) && any_stack st c
end
lemma any_stack_frame:
forall st c1 c2.
unchanged st c1 c2 ->
any_stack st c1 -> any_stack st c2
lemma inverse_frame:
forall st c1 c2 c3.
inverse st c1 c2 ->
unchanged st c2 c3 ->
inverse st c1 c3
lemma inverse_frame2:
forall st c1 c2 c3.
unchanged st c1 c2 ->
inverse st c2 c3 ->
inverse st c1 c3
let lemma inverse_any (st: stack) (c1 c2: coloring)
requires { any_stack st c1 }
requires { inverse st c1 c2 }
ensures { any_stack st c2 }
= ()
lemma inverse_final:
forall f st c1 c2.
final_forest f c1 ->
inverse (Cons f st) c1 c2 ->
white_forest f c2
lemma inverse_white:
forall f st c1 c2.
white_forest f c1 ->
inverse (Cons f st) c1 c2 ->
final_forest f c2
let lemma white_final_exclusive (f: forest) (c: coloring)
requires { f <> E }
ensures { white_forest f c -> final_forest f c -> false }
= match f with E -> () | N _ _ _ -> () end
lemma final_unique:
forall f c1 c2.
final_forest f c1 ->
final_forest f c2 ->
forall i. mem_forest i f -> c1[i] = c2[i]
let rec lemma inverse_inverse
(st: stack) (c1 c2 c3: coloring)
requires { inverse st c1 c2 }
requires { inverse st c2 c3 }
ensures { unchanged st c1 c3 }
variant { st }
= match st with
| Nil -> ()
| Cons E st' -> inverse_inverse st' c1 c2 c3
| Cons f st' -> if even_forest f then () else inverse_inverse st' c1 c2 c3
end
inductive sub stack forest coloring =
| Sub_reflex:
forall f, c. sub (Cons f Nil) f c
| Sub_brother:
forall st i f1 f2 c.
sub st f2 c -> sub st (N i f1 f2) c
| Sub_append:
forall st i f1 f2 c.
sub st f1 c -> c[i] = Black ->
sub (st ++ Cons f2 Nil) (N i f1 f2) c
lemma sub_not_nil:
forall st f c. sub st f c -> st <> Nil
lemma sub_empty:
forall st f0 c. st <> Nil -> sub (Cons E st) f0 c ->
sub st f0 c
lemma sub_mem:
forall n st f c.
mem_stack n st -> sub st f c -> mem_forest n f
lemma sub_weaken1:
forall st i f1 f2 f0 c.
sub (Cons (N i f1 f2) st) f0 c ->
sub (Cons f2 st) f0 c
lemma sub_weaken2:
forall st i f1 f2 f0 c.
sub (Cons (N i f1 f2) st) f0 c ->
c[i] = Black ->
sub (Cons f1 (Cons f2 st)) f0 c
lemma not_mem_st: forall i f st c.
not (mem_forest i f) -> sub st f c -> not (mem_stack i st)
lemma sub_frame:
forall st f0 c c'.
no_repeated_forest f0 ->
(forall i. not (mem_stack i st) -> mem_forest i f0 -> c'[i] = c[i]) ->
sub st f0 c ->
sub st f0 c'
predicate disjoint_stack (f: forest) (st: stack) =
forall i. mem_forest i f -> mem_stack i st -> false
lemma sub_no_rep: forall f st' f0 c.
sub (Cons f st') f0 c ->
no_repeated_forest f0 ->
no_repeated_forest f
lemma sub_no_rep2: forall f st' f0 c.
sub (Cons f st') f0 c ->
no_repeated_forest f0 ->
disjoint_stack f st'
lemma white_valid: forall f c.
white_forest f c -> valid_coloring f c
lemma final_valid: forall f c.
final_forest f c -> valid_coloring f c
lemma valid_coloring_frame:
forall f c1 c2.
valid_coloring f c1 ->
(forall i. mem_forest i f -> c2[i] = c1[i]) ->
valid_coloring f c2
lemma valid_coloring_set:
forall f i c.
valid_coloring f c ->
not (mem_forest i f) ->
valid_coloring f c[i <- Black]
lemma head_and_tail:
forall f1 f2: 'a, st1 st2: list 'a.
Cons f1 st1 = st2 ++ Cons f2 Nil ->
st2 <> Nil ->
exists st. st1 = st ++ Cons f2 Nil /\ st2 = Cons f1 st
lemma sub_valid_coloring_f1:
forall i f1 f2 c i1.
no_repeated_forest (N i f1 f2) ->
valid_coloring (N i f1 f2) c ->
c[i] = Black ->
mem_forest i1 f1 ->
valid_coloring f1 c[i1 <- Black] ->
valid_coloring (N i f1 f2) c[i1 <- Black]
lemma sub_valid_coloring:
forall f0 i f1 f2 st c1.
no_repeated_forest f0 ->
valid_coloring f0 c1 ->
sub (Cons (N i f1 f2) st) f0 c1 ->
valid_coloring f0 c1[i <- Black]
lemma sub_Cons_N:
forall f st i f1 f2 c.
sub (Cons f st) (N i f1 f2) c ->
f = N i f1 f2 || (exists st'. sub (Cons f st') f1 c) || sub (Cons f st) f2 c
lemma white_white:
forall f c i.
white_forest f c ->
white_forest f c[i <- White]
let rec lemma sub_valid_coloring_white
(f0: forest) (i: int) (f1 f2: forest) (c1: coloring)
requires { no_repeated_forest f0 }
requires { valid_coloring f0 c1 }
requires { white_forest f1 c1 }
ensures { forall st. sub (Cons (N i f1 f2) st) f0 c1 ->
valid_coloring f0 c1[i <- White] }
variant { f0 }
= match f0 with
| E -> ()
| N _ f10 f20 ->
sub_valid_coloring_white f10 i f1 f2 c1;
sub_valid_coloring_white f20 i f1 f2 c1
end
function count_stack (st: stack) : int = match st with
| Nil -> 1
| Cons f st' -> count_forest f * count_stack st'
end
lemma count_stack_nonneg:
forall st. count_stack st >= 1
use seq.Seq as S
type visited = S.seq coloring
predicate stored_solutions
(f0: forest) (bits: coloring) (st: stack) (v1 v2: visited) =
let n = size_forest f0 in
let start = S.length v1 in
let stop = S.length v2 in
stop - start = count_stack st &&
(forall j. 0 <= j < start ->
eq_coloring n (S.get v2 j) (S.get v1 j)) &&
forall j. start <= j < stop ->
valid_coloring f0 (S.get v2 j) &&
(forall i. 0 <= i < n -> not (mem_stack i st) ->
(S.get v2 j)[i] = bits[i]) &&
forall k. start <= k < stop -> j <> k ->
not (eq_coloring n (S.get v2 j) (S.get v2 k))
let lemma stored_trans1
(f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
(v1 v2 v3: visited)
requires { valid_nums_forest f0 (size_forest f0) }
requires { 0 <= i < size_forest f0 }
requires { forall j. 0 <= j < size_forest f0 ->
not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
requires { forall j. S.length v1 <= j < S.length v2 ->
(S.get v2 j)[i] = White }
requires { forall j. S.length v2 <= j < S.length v3 ->
(S.get v3 j)[i] = Black }
requires { stored_solutions f0 bits1 (Cons f2 st) v1 v2 }
requires { stored_solutions f0 bits2 (Cons f1 (Cons f2 st)) v2 v3 }
ensures { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
= ()
let lemma stored_trans2
(f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
(v1 v2 v3: visited)
requires { valid_nums_forest f0 (size_forest f0) }
requires { 0 <= i < size_forest f0 }
requires { forall j. 0 <= j < size_forest f0 ->
not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
requires { forall j. S.length v1 <= j < S.length v2 ->
(S.get v2 j)[i] = Black }
requires { forall j. S.length v2 <= j < S.length v3 ->
(S.get v3 j)[i] = White }
requires { stored_solutions f0 bits1 (Cons f1 (Cons f2 st)) v1 v2 }
requires { stored_solutions f0 bits2 (Cons f2 st) v2 v3 }
ensures { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
= ()
end
module CountCorrect
use import seq.Seq as S
use map.Map as M
use import map.Const
use import list.List
use import list.Append
use import int.Int
use import KodaRuskey_Spec
use import Lemmas
use import ref.Ref
predicate id_forest (f: forest) (c1 c2: coloring) =
forall j. mem_forest j f -> M.get c1 j = M.get c2 j
let product (n: int) (i: int) (f1 f2: forest) (s1 s2: coloring) : coloring
requires { valid_nums_forest (N i f1 f2) n }
requires { valid_coloring f1 s1 }
requires { forall j. not (mem_forest j f1) -> M.get s1 j = White }
requires { valid_coloring f2 s2 }
requires { forall j. not (mem_forest j f2) -> M.get s2 j = White }
ensures { valid_coloring (N i f1 f2) result }
ensures { M.get result i = Black }
ensures { id_forest f1 result s1 }
ensures { id_forest f2 result s2 }
ensures { forall j.
not (mem_forest j (N i f1 f2)) -> M.get result j = White }
= let rec copy (acc: coloring) (f: forest)
variant { f }
ensures { forall i. M.get result i =
if mem_forest i f then M.get s2 i else M.get acc i }
= match f with
| E -> acc
| N i2 left2 right2 ->
M.set (copy (copy acc left2) right2) i2 (M.get s2 i2)
end
in
let c = copy s1 f2 in
M.set c i Black
predicate solutions (n: int) (f: forest) (s: seq coloring) =
(* these are colorings, white outside of f *)
(forall j. 0 <= j < length s -> valid_coloring f s[j]) &&
(forall j. 0 <= j < length s ->
(forall i. not (mem_forest i f) -> M.get s[j] i = White)) &&
(* colorings are disjoint *)
(forall j. 0 <= j < length s ->
forall k. 0 <= k < length s -> j <> k ->
not (eq_coloring n s[j] s[k]))
let rec enum (n: int) (f: forest) : seq coloring
requires { valid_nums_forest f n }
ensures { length result = count_forest f }
ensures { solutions n f result }
variant { f }
= match f with
| E ->
cons (const White) empty
| N i f1 f2 ->
let s1 = enum n f1 in
let s2 = enum n f2 in
let s = ref s2 in
(* c[i] = Black *)
for j = 0 to length s1 - 1 do
invariant { length !s = length s2 + j * length s2 }
invariant { solutions n f !s }
invariant { forall m. 0 <= m < length s2 ->
eq_coloring n s2[m] !s[m] }
invariant { forall j' k'. 0 <= j' < j -> 0 <= k' < length s2
->
let c = !s[length s2 + j' * (length s2) + k'] in
id_forest f1 c s1[j'] &&
id_forest f2 c s2[k'] &&
M.get c i = Black }
for k = 0 to length s2 - 1 do
invariant { length !s = length s2 + j * length s2 + k }
invariant { solutions n f !s }
invariant { forall m. 0 <= m < length s2 ->
eq_coloring n s2[m] !s[m] }
invariant { forall j' k'. 0 <= j' < j && 0 <= k' < length s2
|| j' = j && 0 <= k' < k ->
let c = !s[length s2 + j' * (length s2) + k'] in
id_forest f1 c s1[j'] &&
id_forest f2 c s2[k'] &&
M.get c i = Black }
let p = product n i f1 f2 s1[j] s2[k] in
assert { forall l. 0 <= l < length !s ->
not (eq_coloring n p !s[l]) };
s := snoc !s p
done
done;
!s
end
end
module KodaRuskey
use import seq.Seq as S
use import list.List
use import KodaRuskey_Spec
use import Lemmas
use map.Map as M
use import array.Array
use import int.Int
use import ref.Ref
val map_of_array (a: array 'a) : M.map int 'a
ensures { result = a.elts }
val bits : array color
constant f0: forest
val ghost visited: ref visited
let rec enum (ghost f0: forest) (st: list forest) : unit
requires { size_forest f0 = length bits }
requires { valid_nums_forest f0 (length bits) }
requires { sub st f0 bits.elts }
requires { st <> Nil }
requires { any_stack st bits.elts }
requires { valid_coloring f0 bits.elts }
variant { size_stack st, st }
ensures { forall i.
not (mem_stack i st) -> bits[i] = (old bits)[i] }
ensures { inverse st (old bits).elts bits.elts }
ensures { valid_coloring f0 bits.elts }
ensures { stored_solutions f0 bits.elts st (old !visited) !visited }
= match st with
| Nil ->
absurd
| Cons E st' ->
match st' with
| Nil -> (* display *)
assert { valid_coloring f0 bits.elts };
ghost visited := S.snoc !visited (map_of_array bits);
()
| _ ->
enum f0 st'
end
| Cons (N i f1 f2 as f) st' ->
(* assert { disjoint f1 f2 }; *)
assert { disjoint_stack f1 st' };
assert { not (mem_stack i st') };
let ghost visited1 = !visited in
if bits[i] = White then begin
'A: enum f0 (Cons f2 st');
(* assert { white_forest f1 bits.elts }; *)
(* assert { final_forest f2 bits.elts }; *)
assert { sub st f0 bits.elts };
(* assert { if not (even_forest f2) *)
(* then inverse st' (at bits 'A).elts bits.elts *)
(* else unchanged st' (at bits 'A).elts bits.elts }; *)
let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in
'B: bits[i] <- Black;
assert { sub st f0 bits.elts };
assert { white_forest f1 bits.elts };
(* assert { final_forest f2 bits.elts }; *)
assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts};
assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts };
'C: enum f0 (Cons f1 (Cons f2 st'));
assert { bits[i] = Black };
assert { final_forest f1 bits.elts };
assert { if not (even_forest f1)
then inverse (Cons f2 st') (at bits 'C).elts bits.elts &&
white_forest f2 bits.elts
else unchanged (Cons f2 st') (at bits 'C).elts bits.elts &&
final_forest f2 bits.elts };
(* assert { final_forest f bits.elts }; *)
(* assert { let start = S.length (at !visited 'A) in *)
(* let stop = S.length !visited in *)
(* forall j. start <= j < stop -> *)
(* start <= j < start + count_stack (Cons f2 st') \/ *)
(* start + count_stack (Cons f2 st') <= j < stop }; *)
ghost stored_trans1 f0 bits1 (map_of_array bits)
i f1 f2 st' visited1 visited2 !visited
end else begin
assert { if not (even_forest f1) then white_forest f2 bits.elts
else final_forest f2 bits.elts };
'A: enum f0 (Cons f1 (Cons f2 st'));
assert { sub st f0 bits.elts };
let ghost bits1 = map_of_array bits in
let ghost visited2 = !visited in
'B: bits[i] <- White;
(* assert { white_forest f1 bits.elts }; *)
assert { unchanged (Cons f1 (Cons f2 st')) (at bits 'B).elts bits.elts };
assert { inverse (Cons f1 (Cons f2 st')) (at bits 'A).elts bits.elts };
assert { sub st f0 bits.elts };
assert { if even_forest f1 || even_forest f2
then unchanged st' (at bits 'A).elts bits.elts
else inverse st' (at bits 'A).elts bits.elts };
'C: enum f0 (Cons f2 st');
(* assert { white_forest f1 bits.elts }; *)
(* assert { white_forest f2 bits.elts }; *)
assert { bits[i] = White };
assert { white_forest f bits.elts };
(* assert { inverse (Cons f2 st') (at bits 'C).elts bits.elts }; *)
(* assert { if not (even_forest f2) *)
(* then inverse st' (at bits 'C).elts bits.elts *)
(* else unchanged st' (at bits 'C).elts bits.elts }; *)
(* assert { even_forest f2 -> unchanged st' (at bits 'A).elts bits.elts }; *)
ghost stored_trans2 f0 bits1 (map_of_array bits)
i f1 f2 st' visited1 visited2 !visited
end
end
let main ()
requires { white_forest f0 bits.elts }
requires { size_forest f0 = length bits }
requires { valid_nums_forest f0 (length bits) }
ensures { S.length !visited = count_forest f0 }
ensures { let n = S.length !visited in
forall j. 0 <= j < n ->
valid_coloring f0 (S.get !visited j) &&
forall k. 0 <= k < n -> j <> k ->
not (eq_coloring (length bits) (S.get !visited j) (S.get !visited k)) }
= visited := S.empty;
enum f0 (Cons f0 Nil)
end
\ No newline at end of file
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require map.Map.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive color :=
| White : color
| Black : color.
Axiom color_WhyType : WhyType color.
Existing Instance color_WhyType.
(* Why3 assumption *)
Inductive forest :=
| E : forest
| N : Z -> forest -> forest -> forest.
Axiom forest_WhyType : WhyType forest.
Existing Instance forest_WhyType.
(* Why3 assumption *)