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/

Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

vacid_0_build_maze.mlw 4.3 KB
Newer Older
1 2

theory UnionFind
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
3

4 5
  use import int.Int

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
6 7
  type uf

Andrei Paskevich's avatar
Andrei Paskevich committed
8 9 10
  predicate repr uf int int
  function size uf : int
  function num uf : int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11

12
  axiom Repr_function_1:
13
    forall u:uf, x:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
14
    0 <= x < size u -> exists y:int. 0 <= y < size u /\ repr u x y
15
  axiom Repr_function_2:
16
    forall u:uf, x y z:int.
17 18
    0 <= x < size u -> repr u x y -> repr u x z -> y = z

Andrei Paskevich's avatar
Andrei Paskevich committed
19
  predicate same (u:uf) (x y:int) =
20
     forall r:int. repr u x r <-> repr u y r
21

Andrei Paskevich's avatar
Andrei Paskevich committed
22
  predicate same_reprs (u1 u2 : uf) =
23
     forall x r:int. repr u1 x r <-> repr u2 x r
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24 25

  axiom OneClass :
26
    forall u:uf. num u = 1 ->
27
    forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28

29 30 31 32 33
end

module UnionFind_sig

  use import int.Int
34
  use import ref.Ref
35 36 37

  use export UnionFind

38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  val create (n:int) : ref uf
    requires { 0 <= n }
    ensures { num !result = n /\ size !result = n /\
      forall x:int. 0 <= x < n -> repr !result x x }

  val find (u:ref uf) (x:int) : int writes {u}
    requires { 0 <= x < size !u }
    ensures { repr !u x result /\
      size !u = size (old !u) /\ num !u = num (old !u) /\
      same_reprs !u (old !u) }

  val union (u:ref uf) (a:int) (b:int) : unit writes {u}
    requires { 0 <= a < size !u /\ 0 <= b < size !u /\ not same !u a b }
    ensures { same !u a b /\
      size !u = size (old !u) /\ num !u = num (old !u) - 1 /\
      forall x y:int. 0 <= x < size !u -> 0 <= y < size !u ->
         same !u x y <->
         same (old !u) x y \/
         same (old !u) x a /\ same (old !u) b y \/
         same (old !u) x b /\ same (old !u) a y }

  val get_num_classes (u:ref uf) : int reads {u} ensures { result = num !u }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
60

61 62 63 64 65
end

theory Graph

  type vertex
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66 67 68

  type graph

69
  inductive path graph vertex vertex =
70 71
    | Path_refl : forall g:graph, x:vertex. path g x x
    | Path_sym  : forall g:graph, x y:vertex. path g x y -> path g y x
72 73
    | Path_trans:
        forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74

75
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76

77
theory Graph_int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78

79
  clone export Graph with type vertex = int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80

81 82 83 84 85
end

module Graph_sig

  use import int.Int
86
  use import ref.Ref
87

88 89
  (* clone export Graph with type vertex = int *)
  use export Graph_int
90

Andrei Paskevich's avatar
Andrei Paskevich committed
91
  val graph : ref graph
92

Andrei Paskevich's avatar
Andrei Paskevich committed
93
  val num_edges : ref int
94

95 96 97
  val add_edge (a:int) (b:int) : unit writes {num_edges,graph}
    requires { not path !graph a b }
    ensures { !num_edges = old !num_edges + 1 /\
98
      (forall x y:int.
99
          path !graph x y <->
Andrei Paskevich's avatar
Andrei Paskevich committed
100 101
          path (old !graph) x y \/
          path (old !graph) x a /\ path (old !graph) b y \/
102
          path (old !graph) x b /\ path (old !graph) a y) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103

104 105 106 107 108
end

module BuildMaze

  use import int.Int
109
  use import ref.Ref
110

111 112
  use import UnionFind_sig
  use import Graph_sig
113

114
  val rand (s:int) : int requires { 0 < s } ensures { 0 <= result < s }
115 116 117 118

  lemma Ineq1 :
    forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n

119 120
  let add_edge_and_union (u: ref uf) (a:int) (b:int)
    requires { 0 <= a < size !u /\ 0 <= b < size !u /\
Andrei Paskevich's avatar
Andrei Paskevich committed
121
      not same !u a b /\ not path !graph a b /\
122
      forall x y:int.
123
        0 <= x < size !u -> 0 <= y < size !u ->
124 125
        same !u x y <-> path !graph x y }
    ensures { !num_edges = old !num_edges + 1 /\
Andrei Paskevich's avatar
Andrei Paskevich committed
126 127
      same !u a b /\
      size !u = size (old !u) /\ num !u = num (old !u) - 1 /\
128
      (forall x y:int.
129
         0 <= x < size !u -> 0 <= y < size !u ->
130 131 132 133 134 135 136 137 138 139
         same !u x y <-> path !graph x y) }
  = add_edge a b;
    union u a b

let build_maze (n:int)
  requires { 1 <= n /\ !num_edges = 0 /\
    forall x y:int. x=y <-> path !graph x y }
  ensures { !num_edges = n*n-1 /\
    forall x y:int. 0 <= x < n*n -> 0 <= y < n*n -> path !graph x y }
  = let u = create (n*n) in
140
    assert { forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
141
             same !u x y -> (repr !u x y && repr !u x x && x = y) };
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142
    while get_num_classes u > 1 do
143 144
      invariant {
          1 <= num !u /\ num !u + !num_edges = size !u = n*n /\
145
          forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
146
                          (same !u x y <-> path !graph x y) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147 148
      let x = rand n in
      let y = rand n in
149 150 151 152
      let d = rand 2 in
      let w = if d = 0 then x+1 else x in
      let z = if d = 0 then y else y+1 in
      if w < n && z < n then begin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
153 154 155 156 157 158 159 160 161
        let a = y * n + x in
        assert { 0 <= a < n*n };
        let b = w * n + z in
        assert { 0 <= b < n*n };
        if find u a <> find u b then
          add_edge_and_union u a b
      end
    done

162
end