blocking_semantics3.mlw 26.3 KB
Newer Older
1
2
3
4
5
6
7
8

(** {1 A certified WP calculus} *)

(** {2 A simple imperative language with expressions, syntax and semantics} *)

theory ImpExpr

use import int.Int
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
9
use import int.MinMax
10
11
use import bool.Bool
use export list.List
Asma Tafat's avatar
Asma Tafat committed
12
use export list.Append
13
14
15
16
17
18
19
20
21
22
23
use map.Map as IdMap

(** types and values *)

type datatype = TYunit | TYint | TYbool
type value = Vvoid | Vint int | Vbool bool

(** terms and formulas *)

type operator = Oplus | Ominus | Omult | Ole

24
(** ident for mutable variables *)
25
26
type mident

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
27
lemma mident_decide :
28
29
  forall m1 m2: mident. m1 = m2 \/ m1 <> m2

30
(** ident for immutable variables *)
31
type ident = { ident_index : int }
Claude Marche's avatar
Claude Marche committed
32

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
33
lemma ident_decide :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
34
  forall m1 m2: ident. m1 = m2 \/ m1 <> m2
35
36

(** Terms *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
37
type term =
38
39
40
41
42
43
44
45
  | Tvalue value
  | Tvar ident
  | Tderef mident
  | Tbin term operator term


predicate var_occurs_in_term (x:ident) (t:term) =
  match t with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
46
47
48
49
  | Tvalue _  -> false
  |  Tvar i  -> x=i
  |  Tderef _  -> false
  |  Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
50
51
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
52
53
(* predicate term_inv (t:term) = *)
(*   forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar *)
54
55

function mk_tvalue (v:value) : term =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
56
   Tvalue v
57
58

function mk_tvar (i:ident) : term =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
59
   Tvar i
60
61

function mk_tderef (r:mident) : term =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
62
   Tderef r
63
64

function mk_tbin (t1:term) (o:operator) (t2:term) : term =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
65
    Tbin t1 o t2
66
67
68
69
70
71
72
73
74
75
76


(** Formulas *)
type fmla =
  | Fterm term
  | Fand fmla fmla
  | Fnot fmla
  | Fimplies fmla fmla
  | Flet ident term fmla         (* let id = term in fmla *)
  | Fforall ident datatype fmla  (* forall id : ty, fmla *)

77
78
79
80
81
82
83
84
(** Statements *)
type stmt =
  | Sskip
  | Sassign mident term
  | Sseq stmt stmt
  | Sif term stmt stmt
  | Sassert fmla
  | Swhile term fmla stmt  (* while cond invariant inv body *)
85

86
87
88
lemma decide_is_skip:
  forall s:stmt. s = Sskip \/ s <> Sskip

89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(** Typing *)

function type_value (v:value) : datatype =
    match v with
      | Vvoid  -> TYunit
      | Vint int ->  TYint
      | Vbool bool -> TYbool
end

inductive type_operator (op:operator) (ty1 ty2 ty: datatype) =
      | Type_plus : type_operator Oplus TYint TYint TYint
      | Type_minus : type_operator Ominus TYint TYint TYint
      | Type_mult : type_operator Omult TYint TYint TYint
      | Type_le : type_operator Ole TYint TYint TYbool

type type_stack = list (ident, datatype)  (* map local immutable variables to their type *)
function get_vartype (i:ident) (pi:type_stack) : datatype =
  match pi with
  | Nil -> TYunit
  | Cons (x,ty) r -> if x=i then ty else get_vartype i r
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
111

112
113
114
115
116
type type_env = IdMap.map mident datatype  (* map global mutable variables to their type *)
function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i

inductive type_term type_env type_stack term datatype =
  | Type_value :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
117
118
      forall sigma: type_env, pi:type_stack, v:value.
	type_term sigma pi  (Tvalue v) (type_value v)
119
  | Type_var :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
120
      forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
121
        (get_vartype v pi = ty) ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
122
        type_term sigma pi (Tvar v) ty
123
  | Type_deref :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
124
      forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
125
        (get_reftype v sigma = ty) ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
126
        type_term sigma pi (Tderef v) ty
127
128
  | Type_bin :
      forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator,
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
129
        ty1 ty2 ty:datatype.
130
131
132
        type_term sigma pi t1 ty1 ->
	type_term sigma pi t2 ty2 ->
	type_operator op ty1 ty2 ty ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
133
        type_term sigma pi (Tbin t1 op t2) ty
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171

inductive type_fmla type_env type_stack fmla =
  | Type_term :
      forall sigma: type_env, pi:type_stack, t:term.
	type_term sigma pi t TYbool ->
	type_fmla sigma pi (Fterm t)
  | Type_conj :
      forall sigma: type_env, pi:type_stack, f1 f2:fmla.
	type_fmla sigma pi f1 ->
        type_fmla sigma pi f2 ->
        type_fmla sigma pi (Fand f1 f2)
  | Type_neg :
      forall sigma: type_env, pi:type_stack, f:fmla.
	type_fmla sigma pi f ->
        type_fmla sigma pi (Fnot f)
  | Type_implies :
      forall sigma: type_env, pi:type_stack, f1 f2:fmla.
	type_fmla sigma pi f1 ->
        type_fmla sigma pi f2 ->
        type_fmla sigma pi (Fimplies f1 f2)
  | Type_let :
      forall sigma: type_env, pi:type_stack, x:ident, t:term, f:fmla, ty:datatype.
	type_term sigma pi t ty ->
        type_fmla sigma (Cons (x,ty) pi) f ->
        type_fmla sigma pi (Flet x t f)
  | Type_forall1 :
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
        type_fmla sigma (Cons (x,TYint) pi) f ->
  	type_fmla sigma pi (Fforall x TYint f)
  | Type_forall2 :
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
        type_fmla sigma (Cons (x,TYbool) pi) f ->
  	type_fmla sigma pi (Fforall x TYbool f)
  | Type_forall3:
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
        type_fmla sigma (Cons (x,TYunit) pi) f ->
  	type_fmla sigma pi (Fforall x TYunit f)

172
173
174
175
176
177
178
179
180
181
182
inductive type_stmt type_env type_stack stmt =
  | Type_skip :
      forall sigma: type_env, pi:type_stack.
	type_stmt sigma pi Sskip
  | Type_seq :
      forall sigma: type_env, pi:type_stack, s1 s2:stmt.
        type_stmt sigma pi s1 ->
	type_stmt sigma pi s2 ->
	type_stmt sigma pi (Sseq s1 s2)
  | Type_assigns :
      forall sigma: type_env, pi:type_stack, x:mident, t:term, ty:datatype.
183
	(get_reftype x sigma = ty) ->
184
185
186
187
188
189
190
191
192
193
        type_term sigma pi t ty ->
        type_stmt sigma pi (Sassign x t)
  | Type_if :
      forall sigma: type_env, pi:type_stack, t:term, s1 s2:stmt.
	type_term sigma pi t TYbool ->
	type_stmt sigma pi s1 ->
	type_stmt sigma pi s2 ->
    	type_stmt sigma pi (Sif t s1 s2)
  | Type_assert :
      forall sigma: type_env, pi:type_stack, p:fmla.
194
	type_fmla sigma pi p ->
195
196
197
    	type_stmt sigma pi (Sassert p)
  | Type_while :
      forall sigma: type_env, pi:type_stack, guard:term, body:stmt, inv:fmla.
198
	type_fmla sigma pi inv ->
199
200
        type_term sigma pi guard TYbool ->
        type_stmt sigma pi body ->
Claude Marche's avatar
Claude Marche committed
201
        type_stmt sigma pi (Swhile guard inv body)
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237

(** Operational semantic *)
type env = IdMap.map mident value  (* map global mutable variables to their value *)
function get_env (i:mident) (e:env) : value = IdMap.get e i

type stack = list (ident, value)  (* map local immutable variables to their value *)
function get_stack (i:ident) (pi:stack) : value =
  match pi with
  | Nil -> Vvoid
  | Cons (x,v) r -> if x=i then v else get_stack i r
  end

lemma get_stack_eq:
  forall x:ident, v:value, r:stack.
    get_stack x (Cons (x,v) r) = v

lemma get_stack_neq:
  forall x i:ident, v:value, r:stack.
    x <> i -> get_stack i (Cons (x,v) r) = get_stack i r

(** semantics of formulas *)

function eval_bin (x:value) (op:operator) (y:value) : value =
  match x,y with
  | Vint x,Vint y ->
     match op with
     | Oplus -> Vint (x+y)
     | Ominus -> Vint (x-y)
     | Omult -> Vint (x*y)
     | Ole -> Vbool (if x <= y then True else False)
     end
  | _,_ -> Vvoid
  end

function eval_term (sigma:env) (pi:stack) (t:term) : value =
  match t with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
238
239
240
241
  | Tvalue v -> v
  |  Tvar id  -> get_stack id pi
  |  Tderef id  -> get_env id sigma
  |  Tbin t1 op t2  ->
242
     eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
Asma Tafat's avatar
Asma Tafat committed
243
end
244

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
245
inductive compatible datatype value =
Claude Marche's avatar
Claude Marche committed
246
    | Compatible_bool :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
247
	forall b: bool. compatible TYbool (Vbool b)
Claude Marche's avatar
Claude Marche committed
248
    | Compatible_int :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
249
	forall n: int. compatible TYint (Vint n)
Claude Marche's avatar
Claude Marche committed
250
    | Compatible_void :
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
251
252
253
254
255
256
257
	compatible TYunit Vvoid

predicate existe_compatible (ty:datatype) (v:value) =
   match ty with
    | TYbool -> exists b: bool. v = Vbool b
    | TYint -> exists n: int. v = Vint n
    | TYunit -> v = Vvoid
Claude Marche's avatar
Claude Marche committed
258
end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
259

Claude Marche's avatar
Claude Marche committed
260
predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
261
262
263
 (forall id: mident. compatible (get_reftype id sigmat) (IdMap.get sigma id)) /\
   (forall id: ident. compatible (get_vartype id pit) (get_stack id pi))

Asma Tafat's avatar
Asma Tafat committed
264
lemma eval_type_term:
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
265
266
267
  forall t:term, sigma:env, pi:stack, sigmat:type_env, pit:type_stack, ty:datatype.
    compatible_env sigma sigmat pi pit ->
    type_term sigmat pit t ty -> existe_compatible ty (eval_term sigma pi t)
268

269
270


271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
  match f with
  | Fterm t -> eval_term sigma pi t = Vbool True
  | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
  | Fnot f -> not (eval_fmla sigma pi f)
  | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
  | Flet x t f ->
      eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
  | Fforall x TYint f ->
     forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f
  | Fforall x TYbool f ->
     forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f
  | Fforall x TYunit f ->  eval_fmla sigma (Cons (x,Vvoid) pi) f
  end

(** substitution of a reference [r] by a logic variable [v]
   warning: proper behavior only guaranted if [v] is "fresh",
   i.e index(v) > term_maxvar(t) *)

function msubst_term (t:term) (r:mident) (v:ident) : term =
  match t with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
292
293
294
  | Tvalue _ | Tvar _  -> t
  | Tderef x -> if r = x then mk_tvar v else t
  | Tbin t1 op t2  ->
Claude Marche's avatar
Claude Marche committed
295
      mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v)
296
297
298
299
  end

function subst_term (t:term) (r:ident) (v:ident) : term =
  match t with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
300
301
  | Tvalue _ | Tderef _  -> t
  | Tvar x  ->
302
      if r = x then mk_tvar v else t
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
303
  | Tbin t1 op t2  ->
304
305
306
307
308
     mk_tbin (subst_term t1 r v) op (subst_term t2 r v)
  end

(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (id:ident) (t:term) =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
309
    not (var_occurs_in_term id t)
310

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
311
312
313
314
lemma fresh_in_binop:
  forall t t':term, op:operator, v:ident.
    fresh_in_term v (mk_tbin t op t') ->
      fresh_in_term v t  /\ fresh_in_term v t'
Claude Marche's avatar
Claude Marche committed
315

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
316
317
318
319
320
(* lemma eval_subst_term: *)
(*   forall sigma:env, pi:stack, e:term, x:ident, v:ident. *)
(*     fresh_in_term v e -> *)
(*     eval_term sigma pi (subst_term e x v) = *)
(*     eval_term sigma (Cons (x, (get_stack v pi)) pi) e *)
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351

predicate fresh_in_fmla (id:ident) (f:fmla) =
  match f with
  | Fterm e -> fresh_in_term id e
  | Fand f1 f2   | Fimplies f1 f2 ->
      fresh_in_fmla id f1 /\ fresh_in_fmla id f2
  | Fnot f -> fresh_in_fmla id f
  | Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
  | Fforall y ty f -> id <> y /\ fresh_in_fmla id f
  end

function subst (f:fmla) (x:ident) (v:ident) : fmla =
  match f with
  | Fterm e -> Fterm (subst_term e x v)
  | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v)
  | Fnot f -> Fnot (subst f x v)
  | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v)
  | Flet y t f -> Flet y (subst_term t x v) (subst f x v)
  | Fforall y ty f -> Fforall y ty (subst f x v)
  end

function msubst (f:fmla) (x:mident) (v:ident) : fmla =
  match f with
  | Fterm e -> Fterm (msubst_term e x v)
  | Fand f1 f2 -> Fand (msubst f1 x v) (msubst f2 x v)
  | Fnot f -> Fnot (msubst f x v)
  | Fimplies f1 f2 -> Fimplies (msubst f1 x v) (msubst f2 x v)
  | Flet y t f -> Flet y (msubst_term t x v) (msubst f x v)
  | Fforall y ty f -> Fforall y ty (msubst f x v)
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
352
353
354
355
lemma subst_fresh_term :
  forall t:term, x:ident, v:ident.
   fresh_in_term x t -> subst_term t x v = t

356
357
358
359
lemma subst_fresh :
  forall f:fmla, x:ident, v:ident.
   fresh_in_fmla x f -> subst f x v = f

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
360
361
362
363
(* Not needed *)
(* lemma let_subst: *)
(*     forall t:term, f:fmla, x id':ident, id :mident. *)
(*     msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *)
364

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
365
lemma eval_msubst_term:
366
  forall e "induction":term, sigma:env, pi:stack, x:mident, v:ident.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
367
368
369
370
    fresh_in_term v e ->
    eval_term sigma pi (msubst_term e x v) =
    eval_term (IdMap.set sigma x (get_stack v pi)) pi e

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
371
(* Need it for monotonicity and wp_reduction *)
372
lemma eval_msubst:
373
  forall f "induction":fmla, sigma:env, pi:stack, x:mident, v:ident.
374
375
376
377
    fresh_in_fmla v f ->
    (eval_fmla sigma pi (msubst f x v) <->
     eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
378
379
380
381
382
(* lemma eval_subst: *)
(*   forall f:fmla, sigma:env, pi:stack, x:ident, v:ident. *)
(*     fresh_in_fmla v f -> *)
(*     (eval_fmla sigma pi (subst f x v) <-> *)
(*      eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)
383

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
384
lemma eval_swap_term:
385
forall t "induction":term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
Asma Tafat's avatar
Asma Tafat committed
386
387
388
id1 <> id2 ->
(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
Asma Tafat's avatar
Asma Tafat committed
389

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
390
391
392
393
394
lemma eval_swap_term_2:
  forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t =
    eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t)
Asma Tafat's avatar
Asma Tafat committed
395

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
396
lemma eval_swap:
397
  forall f "induction":fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
Asma Tafat's avatar
Asma Tafat committed
398
399
400
401
    id1 <> id2 ->
    (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
    eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)

Asma Tafat's avatar
Asma Tafat committed
402
lemma eval_swap_2:
403
  forall f:fmla, id1 id2:ident, v1 v2:value.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
404
    id1 <> id2 ->
405
      forall sigma:env, pi:stack.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
406
407
408
409
410
411
412
    (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
    eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)

lemma eval_term_change_free :
  forall t:term, sigma:env, pi:stack, id:ident, v:value.
    fresh_in_term id t ->
    eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
413

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
414
 (* Need it for monotonicity*)
415
lemma eval_change_free :
416
  forall f:fmla, id:ident, v:value.
417
    fresh_in_fmla id f ->
418
      forall sigma:env, pi:stack.
419
420
    (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)

atafat's avatar
atafat committed
421
(** [valid_fmla f] is true when [f] is valid in any environment *)
422
423
  predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p

424
(* Not needed *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
425
426
427
428
429
430
(* axiom msubst_implies : *)
(* forall p q:fmla. *)
(*   valid_fmla (Fimplies p q) -> *)
(*   forall sigma:env, pi:stack, x:mident, id:ident. *)
(*     fresh_in_fmla id (Fand p q) ->  *)
(*     eval_fmla sigma (Cons (id, (get_env x sigma)) pi) (Fimplies (msubst p x id) (msubst q x id))  *)
atafat's avatar
atafat committed
431

432
(** let id' = t in f[id <- id'] <=> let id = t in f*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
433
434
435
436
437
438
439
440
441
442
443
444
(* Not needed *)
(* lemma let_equiv : *)
(*   forall id:ident, id':ident, t:term, f:fmla. *)
(*     forall sigma:env, pi:stack. *)
(*       fresh_in_fmla id' f -> *)
(* 	eval_fmla sigma pi (Flet id' t (subst f id id')) *)
(* 	 -> eval_fmla sigma pi (Flet id t f) *)

(* lemma let_implies : *)
(*   forall id:ident, t:term, p q:fmla. *)
(*     valid_fmla (Fimplies p q) -> *)
(*     valid_fmla (Fimplies (Flet id t p) (Flet id t q)) *)
445

446
447
448
449
450
451
452
453
predicate fresh_in_stmt (id:ident) (s:stmt) =
  match s with
  | Sskip -> true
  | Sseq s1 s2 -> fresh_in_stmt id s1 /\ fresh_in_stmt id s2
  | Sassign _ t -> fresh_in_term id t
  | Sif t s1 s2 -> fresh_in_term id t /\ fresh_in_stmt id s1 /\ fresh_in_stmt id s2
  | Sassert f -> fresh_in_fmla id f
  | Swhile cond inv body -> fresh_in_term id cond /\ fresh_in_fmla id inv /\ fresh_in_stmt id body
454
455
456
457
458
  end


(** small-steps semantics for expressions *)

459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
inductive one_step env stack stmt env stack stmt =

  | one_step_assign :
      forall sigma sigma':env, pi:stack, x:mident, t:term.
        sigma' = IdMap.set sigma x (eval_term sigma pi t) ->
        one_step sigma pi (Sassign x t) sigma' pi Sskip

  | one_step_seq_noskip:
      forall sigma sigma':env, pi pi':stack, s1 s1' s2:stmt.
        one_step sigma pi s1 sigma' pi' s1' ->
          one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1' s2)

  | one_step_seq_skip:
      forall sigma:env, pi:stack, s:stmt.
        one_step sigma pi (Sseq Sskip s) sigma pi s
474
475

  | one_step_if_true:
476
477
478
      forall sigma:env, pi:stack, t:term, s1 s2:stmt.
        eval_term sigma pi t = Vbool True ->
        one_step sigma pi (Sif t s1 s2) sigma pi s1
479
480

  | one_step_if_false:
481
482
483
      forall sigma:env, pi:stack, t:term, s1 s2:stmt.
        eval_term sigma pi t = Vbool False ->
        one_step sigma pi (Sif t s1 s2) sigma pi s2
484
485
486
487
488

  | one_step_assert:
      forall sigma:env, pi:stack, f:fmla.
        (* blocking semantics *)
        eval_fmla sigma pi f ->
489
          one_step sigma pi (Sassert f) sigma pi Sskip
490

491
492
  | one_step_while_true:
      forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
493
494
        (* blocking semantics *)
        eval_fmla sigma pi inv ->
495
496
497
498
        eval_term sigma pi cond = Vbool True ->
        one_step sigma pi (Swhile cond inv body) sigma pi
        (Sseq body (Swhile cond inv body))

MARCHE Claude's avatar
MARCHE Claude committed
499
  | one_step_while_false:
500
501
502
503
504
      forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
        (* blocking semantics *)
        eval_fmla sigma pi inv ->
        eval_term sigma pi cond = Vbool False ->
        one_step sigma pi (Swhile cond inv body) sigma pi Sskip
505
506
507

 (** many steps of execution *)

508
 inductive many_steps env stack stmt env stack stmt int =
509
   | many_steps_refl:
510
     forall sigma:env, pi:stack, s:stmt. many_steps sigma pi s sigma pi s 0
511
   | many_steps_trans:
512
513
514
515
     forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:stmt, n:int.
       one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
       many_steps sigma2 pi2 s2 sigma3 pi3 s3 n ->
       many_steps sigma1 pi1 s1 sigma3 pi3 s3 (n+1)
516

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
517
518
519
lemma steps_non_neg:
  forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:stmt, n:int.
    many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0
520

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
521
(* Used by Hoare_logic/seq_rule*)
522
  lemma many_steps_seq:
523
524
    forall sigma1 sigma3:env, pi1 pi3:stack, s1 s2:stmt, n:int.
      many_steps sigma1 pi1 (Sseq s1 s2) sigma3 pi3 Sskip n ->
525
      exists sigma2:env, pi2:stack, n1 n2:int.
526
527
        many_steps sigma1 pi1 s1 sigma2 pi2 Sskip n1 /\
        many_steps sigma2 pi2 s2 sigma3 pi3 Sskip n2 /\
528
529
        n = 1 + n1 + n2

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
530
531
532
533
534
 (* lemma one_step_change_free : *)
 (*  forall s s':stmt, sigma sigma':env, pi pi':stack, id:ident, v:value. *)
 (*    fresh_in_stmt id s -> *)
 (*    one_step sigma (Cons (id,v) pi) s sigma' pi' s' -> *)
 (*    one_step sigma pi s sigma' pi' s' *)
535
536


537
538
539
540
541
542
543
544
545
546
547
548
549
550



lemma type_preservation :
  forall s1 s2:stmt, sigma1 sigma2:env, pi1 pi2:stack,
         sigmat:type_env, pit:type_stack.
     type_stmt sigmat pit s1 /\
     compatible_env sigma1 sigmat pi1 pit /\
     one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
     type_stmt sigmat pit s2 /\
     compatible_env sigma2 sigmat pi2 pit



551
552
553
(** {3 Hoare triples} *)

(** partial correctness *)
554
predicate valid_triple (p:fmla) (s:stmt) (q:fmla) =
555
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
556
557
558
      forall sigma':env, pi':stack, n:int.
        many_steps sigma pi s sigma' pi' Sskip n ->
          eval_fmla sigma' pi' q
559
560

(*** total correctness *)
561
predicate total_valid_triple (p:fmla) (s:stmt) (q:fmla) =
562
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
563
564
565
      exists sigma':env, pi':stack, n:int.
        many_steps sigma pi s sigma' pi' Sskip n /\
        eval_fmla sigma' pi' q
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593

end


theory TestSemantics

use import ImpExpr

function my_sigma : env = IdMap.const (Vint 0)
constant x : ident
constant y : mident

function my_pi : stack = Cons (x, Vint 42) Nil

goal Test13 :
  eval_term my_sigma my_pi (mk_tvalue (Vint 13)) = Vint 13

goal Test42 :
  eval_term my_sigma my_pi (mk_tvar x) = Vint 42

goal Test0 :
  eval_term my_sigma my_pi (mk_tderef y) = Vint 0

goal Test55 :
  eval_term my_sigma my_pi (mk_tbin (mk_tvar x) Oplus (mk_tvalue (Vint 13))) = Vint 55

goal Ass42 :
  forall sigma':env, pi':stack.
594
    one_step my_sigma my_pi (Sassign y (mk_tvalue (Vint 42))) sigma' pi' Sskip ->
595
596
597
      IdMap.get sigma' y = Vint 42

goal If42 :
598
    forall sigma1 sigma2:env, pi1 pi2:stack, s:stmt.
599
      one_step my_sigma my_pi
600
601
602
603
604
        (Sif (mk_tbin (mk_tderef y) Ole (mk_tvalue (Vint 10)))
             (Sassign y (mk_tvalue (Vint 13)))
             (Sassign y (mk_tvalue (Vint 42))))
        sigma1 pi1 s ->
      one_step sigma1 pi1 s sigma2 pi2 Sskip ->
605
606
607
608
609
610
611
612
613
614
615
616
617
618
        IdMap.get sigma2 y = Vint 13

end

(** {2 Hoare logic} *)

theory HoareLogic

use import ImpExpr


(** Hoare logic rules (partial correctness) *)

lemma consequence_rule:
619
  forall p p' q q':fmla, s:stmt.
620
  valid_fmla (Fimplies p' p) ->
621
  valid_triple p s q ->
622
  valid_fmla (Fimplies q q') ->
623
  valid_triple p' s q'
624

625
626
lemma skip_rule:
  forall q:fmla. valid_triple q Sskip q
627
628

lemma assign_rule:
629
630
631
  forall p:fmla, x:mident, id:ident, t:term.
  fresh_in_fmla id p ->
  valid_triple (Flet id t (msubst p x id)) (Sassign x t) p
632
633

lemma seq_rule:
634
635
636
  forall p q r:fmla, s1 s2:stmt.
  valid_triple p s1 r /\ valid_triple r s2 q ->
  valid_triple p (Sseq s1 s2) q
637
638

lemma if_rule:
639
640
641
642
  forall t:term, p q:fmla, s1 s2:stmt.
  valid_triple (Fand p (Fterm t)) s1 q /\
  valid_triple (Fand p (Fnot (Fterm t))) s2 q ->
  valid_triple p (Sif t s1 s2) q
643
644
645

lemma assert_rule:
  forall f p:fmla. valid_fmla (Fimplies p f) ->
646
  valid_triple p (Sassert f) p
647
648
649

lemma assert_rule_ext:
  forall f p:fmla.
650
  valid_triple (Fimplies f p) (Sassert f) p
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701

(*
lemma while_rule:
  forall e:term, inv:fmla, i:expr.
  valid_triple (Fand (Fterm e) inv) i inv ->
  valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)

lemma while_rule_ext:
  forall e:term, inv inv':fmla, i:expr.
  valid_fmla (Fimplies inv' inv) ->
  valid_triple (Fand (Fterm e) inv') i inv' ->
  valid_triple inv' (Swhile e inv i) (Fand (Fnot (Fterm e)) inv')
*)

(*** frame rule ? *)

end

(** {2 WP calculus} *)

theory WP

use import ImpExpr
use import bool.Bool

use set.Set

(** [assigns sigma W sigma'] is true when the only differences between
    [sigma] and [sigma'] are the value of references in [W] *)

predicate assigns (sigma:env) (a:Set.set mident) (sigma':env) =
  forall i:mident. not (Set.mem i a) ->
    IdMap.get sigma i = IdMap.get sigma' i

lemma assigns_refl:
  forall sigma:env, a:Set.set mident. assigns sigma a sigma

lemma assigns_trans:
  forall sigma1 sigma2 sigma3:env, a:Set.set mident.
    assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
    assigns sigma1 a sigma3

lemma assigns_union_left:
  forall sigma sigma':env, s1 s2:Set.set mident.
    assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'

lemma assigns_union_right:
  forall sigma sigma':env, s1 s2:Set.set mident.
    assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'

(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
702
703
704
705
706
707
708
predicate stmt_writes (s:stmt) (w:Set.set mident) =
  match s with
  | Sskip | Sassert _ -> true
  | Sassign id _ -> Set.mem id w
  | Sseq s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
  | Sif t s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
  | Swhile _ _ body -> stmt_writes body w
709
710
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
711
  function fresh_from (f:fmla) : ident
712

713
  (* Need it for monotonicity*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
714
715
  axiom fresh_from_fmla: forall f:fmla.
     fresh_in_fmla (fresh_from f) f
716

Claude Marche's avatar
Claude Marche committed
717
718
719
720
  (* intention:
       abstract_effects s f = "forall w. f"
     avec w = writes(s)
  *)
721
  function abstract_effects (s:stmt) (f:fmla) : fmla
722

Claude Marche's avatar
Claude Marche committed
723
724
725
726
727
  (* hypothese 1: si
       sigma, pi |= forall w. f
     alors
       sigma, pi |= f
  *)
MARCHE Claude's avatar
MARCHE Claude committed
728
729
730
731
732
  axiom abstract_effects_generalize :
     forall sigma:env, pi:stack, s:stmt, f:fmla.
        eval_fmla sigma pi (abstract_effects s f) ->
        eval_fmla sigma pi f

Claude Marche's avatar
Claude Marche committed
733
  (* hypothese 2: si
MARCHE Claude's avatar
MARCHE Claude committed
734
735
736
737
738
739
740
741
742
743
744
       sigma, pi |= (forall w, p) /\ (forall w, q)
     alors
       sigma, pi |= forall w, (f /\ q)
  *)
  axiom abstract_effects_distrib_conj :
     forall s:stmt, p q:fmla, sigma:env, pi:stack.
       eval_fmla sigma pi (abstract_effects s p) /\
       eval_fmla sigma pi (abstract_effects s q) ->
         eval_fmla sigma pi (abstract_effects s (Fand p q))

  (* hypothese 3: si
Claude Marche's avatar
Claude Marche committed
745
746
747
748
749
750
751
752
753
754
755
756
757
758
       |= p -> q
     alors
       |= (forall w, p) -> (forall w, q)

     remarque : il est essentiel de parler de validité dans tous les etats:
     on n'a pas
       sigma,pi |= p -> q
     implique
       sigma,pi |= (forall w, p) -> (forall w, q)

     contre-exemple: sigma(x) = 42 alors true -> x=42
        mais on n'a
             (forall x, true) -> (forall  x, x=42)
  *)
MARCHE Claude's avatar
MARCHE Claude committed
759
  axiom abstract_effects_monotonic :
MARCHE Claude's avatar
MARCHE Claude committed
760
761
762
763
     forall s:stmt, p q:fmla.
        valid_fmla (Fimplies p q) ->
        forall sigma:env, pi:stack.
           eval_fmla sigma pi (abstract_effects s p) ->
Claude Marche's avatar
Claude Marche committed
764
           eval_fmla sigma pi (abstract_effects s q)
atafat's avatar
atafat committed
765

766
767
768
769
  function wp (s:stmt) (q:fmla) : fmla =
    match s with
    | Sskip -> q
    | Sassert f ->
770
        (* asymmetric and *)
771
772
773
        Fand f (Fimplies f q)
    | Sseq s1 s2 -> wp s1 (wp s2 q)
    | Sassign x t ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
774
        let id = fresh_from q in
775
776
777
778
779
        Flet id t (msubst q x id)
    | Sif t s1 s2 ->
        Fand (Fimplies (Fterm t) (wp s1 q))
             (Fimplies (Fnot (Fterm t)) (wp s2 q))
    | Swhile cond inv body ->
780
781
        Fand inv
          (abstract_effects body
782
783
784
            (Fand
              (Fimplies (Fand (Fterm cond) inv) (wp body inv))
              (Fimplies (Fand (Fnot (Fterm cond)) inv) q)))
785
786
787

    end

MARCHE Claude's avatar
MARCHE Claude committed
788
  (* hypothese 4: invariance de la formule "forall w. f"
Claude Marche's avatar
Claude Marche committed
789
790
     par les effets de s si w = writes s
  *)
MARCHE Claude's avatar
MARCHE Claude committed
791
792
793
794
795
  axiom abstract_effects_writes :
     forall sigma:env, pi:stack, s:stmt, q:fmla.
        eval_fmla sigma pi (abstract_effects s q) ->
        eval_fmla sigma pi (wp s (abstract_effects s q))

796

MARCHE Claude's avatar
MARCHE Claude committed
797
(* ce lemme sert pour prouver distrib_conj, dans le cas de la sequence (et c'est tout !) *)
798
  lemma monotonicity:
799
    forall s "induction":stmt, p q:fmla.
800
      valid_fmla (Fimplies p q)
801
     ->	valid_fmla (Fimplies (wp s p) (wp s q) )
atafat's avatar
atafat committed
802

Claude Marche's avatar
Claude Marche committed
803
804
805
806
807
808
  (* remarque l'ordre des quantifications est essentiel, on n'a pas
       sigma,pi |= p -> q
     implique
       sigma,pi |= (wp s p) -> (wp s q)

     meme contre-exemple: sigma(x) = 42 alors true -> x=42
Andrei Paskevich's avatar
Andrei Paskevich committed
809
        mais
Claude Marche's avatar
Claude Marche committed
810
811
812
813
          wp (x := 7) true = true
          wp (x := 7) x=42 = 7=42
  *)

MARCHE Claude's avatar
MARCHE Claude committed
814
(* ce lemme sert pour wp_reduction dans le cas du while (et c'est tout !) *)
atafat's avatar
atafat committed
815
  lemma distrib_conj:
816
    forall s "induction":stmt, sigma:env, pi:stack, p q:fmla.
atafat's avatar
atafat committed
817
818
     (eval_fmla sigma pi (wp s p)) /\
     (eval_fmla sigma pi (wp s q)) ->
Claude Marche's avatar
Claude Marche committed
819
     eval_fmla sigma pi (wp s (Fand p q))
820
821

  lemma wp_reduction:
822
    forall sigma sigma':env, pi pi':stack, s "induction":stmt, s':stmt.
823
    one_step sigma pi s sigma' pi' s' ->
824
    forall q:fmla.
825
826
      eval_fmla sigma pi (wp s q) ->
      eval_fmla sigma' pi' (wp s' q)
827
828

  lemma progress:
829
    forall s "induction":stmt, sigma:env, pi:stack,
830
831
832
833
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      eval_fmla sigma pi (wp s q) ->
834
835
836
      s <> Sskip ->
      exists sigma':env, pi':stack, s':stmt.
      one_step sigma pi s sigma' pi' s'
837

838

839

840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
  predicate reducible (sigma:env) (pi:stack) (s:stmt) =
    exists sigma':env, pi':stack, s':stmt.
      one_step sigma pi s sigma' pi' s'

  lemma progress2:
    forall s:stmt, sigma:env, pi:stack,
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      eval_fmla sigma pi (wp s q) ->
      s <> Sskip -> reducible sigma pi s

  (** {3 main soundness result} *)

  lemma wp_soundness:
Claude Marche's avatar
Claude Marche committed
855
    forall n :int, sigma sigma':env, pi pi':stack, s s':stmt,
856
857
858
859
860
861
862
863
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      many_steps sigma pi s sigma' pi' s' n /\
      not (reducible sigma' pi' s') /\
      eval_fmla sigma pi (wp s q) ->
      s' = Sskip /\ eval_fmla sigma' pi' q

864
865
866
867
868
869
870
871
end


(***
Local Variables:
compile-command: "why3ide blocking_semantics3.mlw"
End:
*)