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/

vstte12_combinators.mlw 5.82 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11

(* The 2nd Verified Software Competition (VSTTE 2012)
   https://sites.google.com/site/vstte2012/compet

   Problem 2:
   Combinators S and K *)

module Combinators

  type term = S | K | App term term

12 13 14 15 16 17 18 19 20
  let rec predicate eq (x y : term)
    ensures { result <-> x = y }
  = match x, y with
    | S, S -> True
    | K, K -> True
    | App x1 x2, App y1 y2 -> eq x1 y1 && eq x2 y2
    | _, _ -> False
    end

21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
  (* specification of the CBV reduction *)

  predicate is_value (t: term) = match t with
    | K | S -> true
    | App K v | App S v -> is_value v
    | App (App S v1) v2 -> is_value v1 /\ is_value v2
    | _ -> false
  end

  (* contexts *)

  type context = Hole | Left context term | Right term context

  predicate is_context (c: context) = match c with
    | Hole -> true
    | Left c _ -> is_context c
    | Right v c -> is_value v && is_context c
  end

  function subst (c: context) (t: term) : term = match c with
    | Hole -> t
    | Left c1 t2 -> App (subst c1 t) t2
    | Right v1 c2 -> App v1 (subst c2 t)
  end

  (* one step reduction
     (the notion of context is inlined in the following definition) *)

  inductive (-->) (t1 t2: term) =
    | red_K:
       forall c: context. is_context c ->
       forall v1 v2: term. is_value v1 -> is_value v2 ->
       subst c (App (App K v1) v2) --> subst c v1
    | red_S:
       forall c: context. is_context c ->
       forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 ->
       subst c (App (App (App S v1) v2) v3) -->
       subst c (App (App v1 v3) (App v2 v3))

  clone import relations.ReflTransClosure
    with type t = term, predicate rel = (-->)
  predicate (-->*) (t1 t2: term) = relTR t1 t2

64 65 66 67 68 69 70 71 72
  type zipper = ZHole | ZLeft context term | ZRight term context

  let rec function subst_c (c ct:context) : context
    ensures { is_context c /\ is_context ct -> is_context result }
  = match c with
    | Hole -> ct
    | Left c1 t2 -> Left (subst_c c1 ct) t2
    | Right v1 c2 -> Right v1 (subst_c c2 ct)
    end
73

74 75
  lemma subst_c_commute : forall c [@induction] ct t.
    subst c (subst ct t) = subst (subst_c c ct) t
76 77 78

  (* task 1: implement CBV reduction *)

79
  let rec reduction (ghost c:context) (t: term) : term
80
    diverges (* there are non-normalizable terms... *)
81 82 83
    requires { is_context c }
    ensures { subst c t -->* subst c result }
    ensures { is_value result }
84
  = match t with
85 86
    | S -> S
    | K -> K
87 88 89 90 91 92 93
    | App t1 t2 ->
      let v1 = reduction (subst_c c (Left Hole t2)) t1 in
      let v2 = reduction (subst_c c (Right v1 Hole)) t2 in
      match v1 with
      | K | S | App S _ -> App v1 v2
      | App K v3 -> v3
      | App (App S v3) v4 -> reduction c (App (App v3 v2) (App v4 v2))
94 95 96 97
      | _ -> absurd
      end
    end

MARCHE Claude's avatar
MARCHE Claude committed
98 99
  exception BenchFailure

100
  let constant i = App (App S K) K
MARCHE Claude's avatar
MARCHE Claude committed
101

102
  let test_SKK ()
103
    diverges (* would be hard to prove terminating *)
104
    raises { BenchFailure -> true }
105
  = let t1 = reduction Hole (App i i) in
106
    if not (eq t1 i) then raise BenchFailure;
107
    let t2 = reduction Hole (App (App (App (App K K) K) K) K) in
108
    if not (eq t2 K) then raise BenchFailure;
109
    t1, t2
MARCHE Claude's avatar
MARCHE Claude committed
110

111
  (* an irreducible term is a value *)
112
  predicate irreducible (t: term) = forall t': term. not (t-->t')
113

114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
  exception Fail
  let rec ghost reduce_step (c:context) (t:term) : term
    requires { is_context c }
    ensures  { subst c t --> subst c result }
    raises   { Fail -> is_value t }
    variant  { t }
  = match t with
    | App t1 t2 ->
      try App (reduce_step (subst_c c (Left Hole t2)) t1) t2 with Fail ->
      try App t1 (reduce_step (subst_c c (Right t1 Hole)) t2) with Fail ->
      match t1 with
      | App K v -> v
      | App (App S v1) v2 -> App (App v1 t2) (App v2 t2)
      | _ -> raise Fail
      end end end
    | _ -> raise Fail
    end
131

132 133 134 135 136 137 138 139 140
  let rec lemma value_in_context (c:context) (t:term) : unit
    requires { is_value (subst c t) }
    ensures  { is_value t }
    variant  { c }
  = match c with
    | Hole -> ()
    | Left cl _ -> value_in_context cl t
    | Right _ cr -> value_in_context cr t
    end
141

142 143 144
  let lemma irreducible_is_value (t:term) : unit
    ensures { irreducible t <-> is_value t }
  = try let _ = reduce_step Hole t in () with Fail -> () end
145 146 147 148 149 150 151 152 153 154 155

  (* task 2 *)

  use import int.Int

  inductive only_K (t: term) =
    | only_K_K:
        only_K K
    | only_K_App:
        forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2)

156 157
  let rec reduction2 (ghost c:context) (t: term) : term
    requires { only_K t /\ is_context c }
158
    ensures { only_K result /\ is_value result }
159 160
    ensures { subst c t -->* subst c result }
    variant { t }
161
  = match t with
162
    | K -> K
163 164 165 166 167 168
    | App t1 t2 ->
      let v1 = reduction2 (subst_c c (Left Hole t2)) t1 in
      let v2 = reduction2 (subst_c c (Right v1 Hole)) t2 in
      match v1 with
      | K -> App v1 v2
      | App K v3 -> v3
169 170
      | _ -> absurd
      end
171
    | _ -> absurd
172 173 174 175
    end

  (* task 3 *)

176 177
  let rec function ks (n: int) : term
    requires { n >= 0 }
178
    ensures  { only_K result }
179 180
    variant { n }
  = if n = 0 then K else App (ks (n-1)) K
181

182
  use import number.Parity
183

184 185
  let rec reduction3 (ghost c:context) (ghost n:int) (t: term) : term
    requires { n >= 0 /\ t = ks n /\ is_context c }
186
    variant { n }
187
    ensures { subst c t -->* subst c result }
188 189 190
    ensures { is_value result }
    ensures { even n -> result = K }
    ensures { odd n -> result = App K K }
191
  = match t with
192
    | K -> K
193 194 195 196 197 198
    | App t1 t2 ->
      let v1 = reduction3 (subst_c c (Left Hole t2)) (n-1) t1 in
      let v2 = reduction3 (subst_c c (Right v1 Hole)) 0 t2 in
      match v1 with
      | K -> App v1 v2
      | App K v3 -> v3
199 200
      | _ -> absurd
      end
201
    | _ -> absurd
202 203
    end

204 205 206 207 208 209 210
  let lemma ks_even_odd (n:int) : unit
    requires { n >= 0 }
    ensures  { ks (2*n) -->* K }
    ensures  { ks (2*n+1) -->* App K K }
  = let _ = reduction3 Hole (2*n) (ks (2*n)) in
    let _ = reduction3 Hole (2*n+1) (ks (2*n+1)) in
    ()
211 212

end