blocking_semantics_WP_wp_reduction_1.v 24.1 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.

(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
  y) with
  | (true, false) => false
  | (_, _) => true
  end.

(* Why3 assumption *)
Inductive datatype  :=
  | TYunit : datatype 
  | TYint : datatype 
  | TYbool : datatype .

(* Why3 assumption *)
Inductive value  :=
  | Vvoid : value 
  | Vint : Z -> value 
  | Vbool : bool -> value .

(* Why3 assumption *)
Inductive operator  :=
  | Oplus : operator 
  | Ominus : operator 
  | Omult : operator 
  | Ole : operator .

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
33
34
35
Parameter ident : Type.

Parameter result: ident.
MARCHE Claude's avatar
MARCHE Claude committed
36
37
38
39

(* Why3 assumption *)
Inductive term  :=
  | Tvalue : value -> term 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
40
41
  | Tvar : ident -> term 
  | Tderef : ident -> term 
MARCHE Claude's avatar
MARCHE Claude committed
42
43
44
45
46
47
48
49
  | Tbin : term -> operator -> term -> term .

(* Why3 assumption *)
Inductive fmla  :=
  | Fterm : term -> fmla 
  | Fand : fmla -> fmla -> fmla 
  | Fnot : fmla -> fmla 
  | Fimplies : fmla -> fmla -> fmla 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
50
51
  | Flet : ident -> term -> fmla -> fmla 
  | Fforall : ident -> datatype -> fmla -> fmla .
MARCHE Claude's avatar
MARCHE Claude committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

Parameter map : forall (a:Type) (b:Type), Type.

Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.

Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.

Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
  a2) = b1).

Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
  a2) = (get m a2)).

Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.

Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
  ((get (const b1:(map a b)) a1) = b1).

(* Why3 assumption *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
78
Definition env  := (map ident value).
MARCHE Claude's avatar
MARCHE Claude committed
79
80
81
82
83
84
85
86
87
88
89

(* Why3 assumption *)
Inductive list (a:Type) :=
  | Nil : list a
  | Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.

(* Why3 assumption *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
90
Definition stack  := (list (ident* value)%type).
MARCHE Claude's avatar
MARCHE Claude committed
91

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
92
Parameter get_stack: ident -> (list (ident* value)%type) -> value.
MARCHE Claude's avatar
MARCHE Claude committed
93

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
94
Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)),
MARCHE Claude's avatar
MARCHE Claude committed
95
96
97
98
99
100
  match pi with
  | Nil => ((get_stack i pi) = Vvoid)
  | (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) ->
      ((get_stack i pi) = (get_stack i r)))
  end.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
101
102
Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident*
  value)%type)), ((get_stack x (Cons (x, v) r)) = v).
MARCHE Claude's avatar
MARCHE Claude committed
103

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
104
Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident*
MARCHE Claude's avatar
MARCHE Claude committed
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
  value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
  r)).

Parameter eval_bin: value -> operator -> value -> value.

Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
  y) with
  | ((Vint x1), (Vint y1)) =>
      match op with
      | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
      | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
      | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
      | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
          ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))
      end
  | (_, _) => ((eval_bin x op y) = Vvoid)
  end.

(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
125
Fixpoint eval_term(sigma:(map ident value)) (pi:(list (ident* value)%type))
MARCHE Claude's avatar
MARCHE Claude committed
126
127
128
129
130
131
132
133
134
135
136
137
  (t:term) {struct t}: value :=
  match t with
  | (Tvalue v) => v
  | (Tvar id) => (get_stack id pi)
  | (Tderef id) => (get sigma id)
  | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
      pi t2))
  end.
Unset Implicit Arguments.

(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
138
Fixpoint eval_fmla(sigma:(map ident value)) (pi:(list (ident* value)%type))
MARCHE Claude's avatar
MARCHE Claude committed
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
  (f:fmla) {struct f}: Prop :=
  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 f1) => ~ (eval_fmla sigma pi f1)
  | (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
  | (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi)
      f1)
  | (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x,
      (Vint n)) pi) f1)
  | (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x,
      (Vbool b)) pi) f1)
  | (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
  end.
Unset Implicit Arguments.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
155
Parameter subst_term: term -> ident -> ident -> term.
MARCHE Claude's avatar
MARCHE Claude committed
156

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
157
Axiom subst_term_def : forall (e:term) (r:ident) (v:ident),
MARCHE Claude's avatar
MARCHE Claude committed
158
159
160
161
162
163
164
165
166
167
  match e with
  | ((Tvalue _)|(Tvar _)) => ((subst_term e r v) = e)
  | (Tderef x) => ((r = x) -> ((subst_term e r v) = (Tvar v))) /\
      ((~ (r = x)) -> ((subst_term e r v) = e))
  | (Tbin e1 op e2) => ((subst_term e r v) = (Tbin (subst_term e1 r v) op
      (subst_term e2 r v)))
  end.

(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
168
Fixpoint fresh_in_term(id:ident) (t:term) {struct t}: Prop :=
MARCHE Claude's avatar
MARCHE Claude committed
169
170
171
172
173
174
175
176
  match t with
  | (Tvalue _) => True
  | (Tvar v) => ~ (id = v)
  | (Tderef _) => True
  | (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
  end.
Unset Implicit Arguments.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
177
178
Axiom eval_subst_term : forall (sigma:(map ident value)) (pi:(list (ident*
  value)%type)) (e:term) (x:ident) (v:ident), (fresh_in_term v e) ->
MARCHE Claude's avatar
MARCHE Claude committed
179
180
181
  ((eval_term sigma pi (subst_term e x v)) = (eval_term (set sigma x
  (get_stack v pi)) pi e)).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
182
183
184
Axiom eval_term_change_free : forall (t:term) (sigma:(map ident value))
  (pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id
  t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
MARCHE Claude's avatar
MARCHE Claude committed
185
186
187

(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
188
Fixpoint fresh_in_fmla(id:ident) (f:fmla) {struct f}: Prop :=
MARCHE Claude's avatar
MARCHE Claude committed
189
190
191
192
193
194
195
196
197
198
199
200
201
  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 f1) => (fresh_in_fmla id f1)
  | (Flet y t f1) => (~ (id = y)) /\ ((fresh_in_term id t) /\
      (fresh_in_fmla id f1))
  | (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
  end.
Unset Implicit Arguments.

(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
202
Fixpoint subst(f:fmla) (x:ident) (v:ident) {struct f}: fmla :=
MARCHE Claude's avatar
MARCHE Claude committed
203
204
205
206
207
208
209
210
211
212
  match f with
  | (Fterm e) => (Fterm (subst_term e x v))
  | (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
  | (Fnot f1) => (Fnot (subst f1 x v))
  | (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
  | (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
  | (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
  end.
Unset Implicit Arguments.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
213
214
Axiom subst_fresh : forall (f:fmla) (x:ident) (v:ident), (fresh_in_fmla x
  f) -> ((subst f x v) = f).
MARCHE Claude's avatar
MARCHE Claude committed
215

216
217
218
Axiom let_subst : forall (t:term) (f:fmla) (x:ident) (id:ident) (id':ident),
  ((subst (Flet x t f) id id') = (Flet x (subst_term t id id') (subst f id
  id'))).
MARCHE Claude's avatar
MARCHE Claude committed
219

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
220
221
222
223
Axiom eval_subst : forall (f:fmla) (sigma:(map ident value)) (pi:(list
  (ident* value)%type)) (x:ident) (v:ident), (fresh_in_fmla v f) ->
  ((eval_fmla sigma pi (subst f x v)) <-> (eval_fmla (set sigma x
  (get_stack v pi)) pi f)).
MARCHE Claude's avatar
MARCHE Claude committed
224

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
225
226
227
228
Axiom eval_swap : forall (f:fmla) (sigma:(map ident value)) (pi:(list (ident*
  value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
  (~ (id1 = id2)) -> ((eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2) pi))
  f) <-> (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi)) f)).
MARCHE Claude's avatar
MARCHE Claude committed
229

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
230
231
232
Axiom eval_change_free : forall (f:fmla) (sigma:(map ident value)) (pi:(list
  (ident* value)%type)) (id:ident) (v:value), (fresh_in_fmla id f) ->
  ((eval_fmla sigma (Cons (id, v) pi) f) <-> (eval_fmla sigma pi f)).
MARCHE Claude's avatar
MARCHE Claude committed
233

MARCHE Claude's avatar
MARCHE Claude committed
234
(* Why3 assumption *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
235
236
Definition valid_fmla(p:fmla): Prop := forall (sigma:(map ident value))
  (pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
MARCHE Claude's avatar
MARCHE Claude committed
237

238
Axiom let_equiv : forall (id:ident) (id':ident) (t:term) (f:fmla),
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
239
  forall (sigma:(map ident value)) (pi:(list (ident* value)%type)),
240
  (eval_fmla sigma pi (Flet id' t (subst f id id'))) -> (eval_fmla sigma pi
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
241
  (Flet id t f)).
MARCHE Claude's avatar
MARCHE Claude committed
242

MARCHE Claude's avatar
MARCHE Claude committed
243
244
245
246
(* Why3 assumption *)
Inductive expr  :=
  | Evalue : value -> expr 
  | Ebin : expr -> operator -> expr -> expr 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
247
248
249
  | Evar : ident -> expr 
  | Ederef : ident -> expr 
  | Eassign : ident -> expr -> expr 
MARCHE Claude's avatar
MARCHE Claude committed
250
  | Eseq : expr -> expr -> expr 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
251
  | Elet : ident -> expr -> expr -> expr 
MARCHE Claude's avatar
MARCHE Claude committed
252
253
254
255
  | Eif : expr -> expr -> expr -> expr 
  | Eassert : fmla -> expr 
  | Ewhile : expr -> fmla -> expr -> expr .

MARCHE Claude's avatar
MARCHE Claude committed
256
257
(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
258
Fixpoint fresh_in_expr(id:ident) (e:expr) {struct e}: Prop :=
MARCHE Claude's avatar
MARCHE Claude committed
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
  match e with
  | (Evalue _) => True
  | ((Eseq e1 e2)|(Ebin e1 _ e2)) => (fresh_in_expr id e1) /\
      (fresh_in_expr id e2)
  | (Evar v) => ~ (id = v)
  | (Ederef _) => True
  | (Eassign _ e1) => (fresh_in_expr id e1)
  | (Elet v e1 e2) => (~ (id = v)) /\ ((fresh_in_expr id e1) /\
      (fresh_in_expr id e2))
  | (Eif e1 e2 e3) => (fresh_in_expr id e1) /\ ((fresh_in_expr id e2) /\
      (fresh_in_expr id e3))
  | (Eassert f) => (fresh_in_fmla id f)
  | (Ewhile cond inv body) => (fresh_in_expr id cond) /\ ((fresh_in_fmla id
      inv) /\ (fresh_in_expr id body))
  end.
Unset Implicit Arguments.

MARCHE Claude's avatar
MARCHE Claude committed
276
(* Why3 assumption *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
277
278
279
280
281
282
283
284
Inductive one_step : (map ident value) -> (list (ident* value)%type) -> expr
  -> (map ident value) -> (list (ident* value)%type) -> expr -> Prop :=
  | one_step_var : forall (sigma:(map ident value)) (pi:(list (ident*
      value)%type)) (v:ident), (one_step sigma pi (Evar v) sigma pi
      (Evalue (get_stack v pi)))
  | one_step_deref : forall (sigma:(map ident value)) (pi:(list (ident*
      value)%type)) (v:ident), (one_step sigma pi (Ederef v) sigma pi
      (Evalue (get sigma v)))
285
286
287
288
289
290
291
292
293
294
295
296
  | one_step_bin_ctxt1 : forall (sigma:(map ident value)) (sigma':(map ident
      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
      value)%type)) (op:operator) (e1:expr) (e1':expr) (e2:expr),
      (one_step sigma pi e1 sigma' pi' e1') -> (one_step sigma pi (Ebin e1 op
      e2) sigma' pi' (Ebin e1' op e2))
  | one_step_bin_ctxt2 : forall (sigma:(map ident value)) (sigma':(map ident
      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
      value)%type)) (op:operator) (v1:value) (e2:expr) (e2':expr),
      (one_step sigma pi e2 sigma' pi' e2') -> (one_step sigma pi
      (Ebin (Evalue v1) op e2) sigma' pi' (Ebin (Evalue v1) op e2'))
  | one_step_bin_value : forall (sigma:(map ident value)) (sigma':(map ident
      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
297
      value)%type)) (op:operator) (v1:value) (v2:value), (one_step sigma pi
298
      (Ebin (Evalue v1) op (Evalue v2)) sigma' pi' (Evalue (eval_bin v1 op
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
299
      v2)))
300
301
302
303
  | one_step_assign_ctxt : forall (sigma:(map ident value)) (sigma':(map
      ident value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
      value)%type)) (x:ident) (e:expr) (e':expr), (one_step sigma pi e sigma'
      pi' e') -> (one_step sigma pi (Eassign x e) sigma' pi' (Eassign x e'))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
304
305
306
  | one_step_assign_value : forall (sigma:(map ident value)) (pi:(list
      (ident* value)%type)) (x:ident) (v:value), (one_step sigma pi
      (Eassign x (Evalue v)) (set sigma x v) pi (Evalue Vvoid))
307
308
309
310
311
  | one_step_seq_ctxt : forall (sigma:(map ident value)) (sigma':(map ident
      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
      value)%type)) (e1:expr) (e1':expr) (e2:expr), (one_step sigma pi e1
      sigma' pi' e1') -> (one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1'
      e2))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
312
  | one_step_seq_value : forall (sigma:(map ident value)) (pi:(list (ident*
MARCHE Claude's avatar
MARCHE Claude committed
313
314
      value)%type)) (e:expr), (one_step sigma pi (Eseq (Evalue Vvoid) e)
      sigma pi e)
315
316
317
318
319
  | one_step_let_ctxt : forall (sigma:(map ident value)) (sigma':(map ident
      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
      value)%type)) (id:ident) (e1:expr) (e1':expr) (e2:expr),
      (one_step sigma pi e1 sigma' pi' e1') -> (one_step sigma pi (Elet id e1
      e2) sigma' pi' (Elet id e1' e2))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
320
321
322
  | one_step_let_value : forall (sigma:(map ident value)) (pi:(list (ident*
      value)%type)) (id:ident) (v:value) (e:expr), (one_step sigma pi
      (Elet id (Evalue v) e) sigma (Cons (id, v) pi) e)
323
324
325
326
327
  | one_step_if_ctxt : forall (sigma:(map ident value)) (sigma':(map ident
      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
      value)%type)) (e1:expr) (e1':expr) (e2:expr) (e3:expr), (one_step sigma
      pi e1 sigma' pi' e1') -> (one_step sigma pi (Eif e1 e2 e3) sigma' pi'
      (Eif e1' e2 e3))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
328
  | one_step_if_true : forall (sigma:(map ident value)) (pi:(list (ident*
MARCHE Claude's avatar
MARCHE Claude committed
329
330
      value)%type)) (e1:expr) (e2:expr), (one_step sigma pi
      (Eif (Evalue (Vbool true)) e1 e2) sigma pi e1)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
331
  | one_step_if_false : forall (sigma:(map ident value)) (pi:(list (ident*
MARCHE Claude's avatar
MARCHE Claude committed
332
333
      value)%type)) (e1:expr) (e2:expr), (one_step sigma pi
      (Eif (Evalue (Vbool false)) e1 e2) sigma pi e2)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
334
  | one_step_assert : forall (sigma:(map ident value)) (pi:(list (ident*
MARCHE Claude's avatar
MARCHE Claude committed
335
336
      value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
      (Eassert f) sigma pi (Evalue Vvoid))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
337
338
339
340
  | one_step_while : forall (sigma:(map ident value)) (pi:(list (ident*
      value)%type)) (cond:expr) (inv:fmla) (body:expr), (eval_fmla sigma pi
      inv) -> (one_step sigma pi (Ewhile cond inv body) sigma pi (Eif cond
      (Eseq body (Ewhile cond inv body)) (Evalue Vvoid))).
MARCHE Claude's avatar
MARCHE Claude committed
341
342

(* Why3 assumption *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
343
344
345
346
Inductive many_steps : (map ident value) -> (list (ident* value)%type)
  -> expr -> (map ident value) -> (list (ident* value)%type) -> expr
  -> Z -> Prop :=
  | many_steps_refl : forall (sigma:(map ident value)) (pi:(list (ident*
MARCHE Claude's avatar
MARCHE Claude committed
347
      value)%type)) (e:expr), (many_steps sigma pi e sigma pi e 0%Z)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
348
349
350
351
352
353
354
355
356
357
  | many_steps_trans : forall (sigma1:(map ident value)) (sigma2:(map ident
      value)) (sigma3:(map ident value)) (pi1:(list (ident* value)%type))
      (pi2:(list (ident* value)%type)) (pi3:(list (ident* value)%type))
      (e1:expr) (e2:expr) (e3:expr) (n:Z), (one_step sigma1 pi1 e1 sigma2 pi2
      e2) -> ((many_steps sigma2 pi2 e2 sigma3 pi3 e3 n) ->
      (many_steps sigma1 pi1 e1 sigma3 pi3 e3 (n + 1%Z)%Z)).

Axiom steps_non_neg : forall (sigma1:(map ident value)) (sigma2:(map ident
  value)) (pi1:(list (ident* value)%type)) (pi2:(list (ident* value)%type))
  (e1:expr) (e2:expr) (n:Z), (many_steps sigma1 pi1 e1 sigma2 pi2 e2 n) ->
MARCHE Claude's avatar
MARCHE Claude committed
358
359
  (0%Z <= n)%Z.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
360
361
362
363
364
365
Axiom many_steps_seq : forall (sigma1:(map ident value)) (sigma3:(map ident
  value)) (pi1:(list (ident* value)%type)) (pi3:(list (ident* value)%type))
  (e1:expr) (e2:expr) (n:Z), (many_steps sigma1 pi1 (Eseq e1 e2) sigma3 pi3
  (Evalue Vvoid) n) -> exists sigma2:(map ident value), exists pi2:(list
  (ident* value)%type), exists n1:Z, exists n2:Z, (many_steps sigma1 pi1 e1
  sigma2 pi2 (Evalue Vvoid) n1) /\ ((many_steps sigma2 pi2 e2 sigma3 pi3
MARCHE Claude's avatar
MARCHE Claude committed
366
367
  (Evalue Vvoid) n2) /\ (n = ((1%Z + n1)%Z + n2)%Z)).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
368
369
370
371
372
373
374
375
376
Axiom many_steps_let : forall (sigma1:(map ident value)) (sigma3:(map ident
  value)) (pi1:(list (ident* value)%type)) (pi3:(list (ident* value)%type))
  (id:ident) (e1:expr) (e2:expr) (v2:value) (n:Z), (many_steps sigma1 pi1
  (Elet id e1 e2) sigma3 pi3 (Evalue v2) n) -> exists sigma2:(map ident
  value), exists pi2:(list (ident* value)%type), exists v1:value,
  exists n1:Z, exists n2:Z, (many_steps sigma1 pi1 e1 sigma2 pi2 (Evalue v1)
  n1) /\ ((many_steps sigma2 (Cons (id, v1) pi2) e2 sigma3 pi3 (Evalue v2)
  n2) /\ (n = ((1%Z + n1)%Z + n2)%Z)).

377
378
379
380
381
Axiom one_step_change_free : forall (e:expr) (e':expr) (sigma:(map ident
  value)) (sigma':(map ident value)) (pi:(list (ident* value)%type))
  (pi':(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_expr id
  e) -> ((one_step sigma (Cons (id, v) pi) e sigma' pi' e') ->
  (one_step sigma pi e sigma' pi' e')).
MARCHE Claude's avatar
MARCHE Claude committed
382

MARCHE Claude's avatar
MARCHE Claude committed
383
384
(* Why3 assumption *)
Definition valid_triple(p:fmla) (e:expr) (q:fmla): Prop := forall (sigma:(map
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
385
  ident value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p) ->
386
387
388
  forall (sigma':(map ident value)) (pi':(list (ident* value)%type))
  (v:value) (n:Z), (many_steps sigma pi e sigma' pi' (Evalue v) n) ->
  (eval_fmla sigma' (Cons (result, v) pi') q).
MARCHE Claude's avatar
MARCHE Claude committed
389
390
391

(* Why3 assumption *)
Definition total_valid_triple(p:fmla) (e:expr) (q:fmla): Prop :=
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
392
  forall (sigma:(map ident value)) (pi:(list (ident* value)%type)),
393
394
395
  (eval_fmla sigma pi p) -> exists sigma':(map ident value), exists pi':(list
  (ident* value)%type), exists v:value, exists n:Z, (many_steps sigma pi e
  sigma' pi' (Evalue v) n) /\ (eval_fmla sigma' (Cons (result, v) pi') q).
MARCHE Claude's avatar
MARCHE Claude committed
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478

Parameter set1 : forall (a:Type), Type.

Parameter mem: forall (a:Type), a -> (set1 a) -> Prop.
Implicit Arguments mem.

(* Why3 assumption *)
Definition infix_eqeq (a:Type)(s1:(set1 a)) (s2:(set1 a)): Prop :=
  forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.

Axiom extensionality : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
  (infix_eqeq s1 s2) -> (s1 = s2).

(* Why3 assumption *)
Definition subset (a:Type)(s1:(set1 a)) (s2:(set1 a)): Prop := forall (x:a),
  (mem x s1) -> (mem x s2).
Implicit Arguments subset.

Axiom subset_trans : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a))
  (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).

Parameter empty: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.

(* Why3 assumption *)
Definition is_empty (a:Type)(s:(set1 a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.

Axiom empty_def1 : forall (a:Type), (is_empty (empty :(set1 a))).

Parameter add: forall (a:Type), a -> (set1 a) -> (set1 a).
Implicit Arguments add.

Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set1 a)),
  (mem x (add y s)) <-> ((x = y) \/ (mem x s)).

Parameter remove: forall (a:Type), a -> (set1 a) -> (set1 a).
Implicit Arguments remove.

Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set1 a)), (mem x
  (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).

Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set1 a)),
  (subset (remove x s) s).

Parameter union: forall (a:Type), (set1 a) -> (set1 a) -> (set1 a).
Implicit Arguments union.

Axiom union_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
  (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).

Parameter inter: forall (a:Type), (set1 a) -> (set1 a) -> (set1 a).
Implicit Arguments inter.

Axiom inter_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
  (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).

Parameter diff: forall (a:Type), (set1 a) -> (set1 a) -> (set1 a).
Implicit Arguments diff.

Axiom diff_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
  (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).

Axiom subset_diff : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
  (subset (diff s1 s2) s1).

Parameter choose: forall (a:Type), (set1 a) -> a.
Implicit Arguments choose.

Axiom choose_def : forall (a:Type), forall (s:(set1 a)), (~ (is_empty s)) ->
  (mem (choose s) s).

Parameter all: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments all.
Unset Contextual Implicit.

Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set1 a))).

(* Why3 assumption *)
479
Definition assigns(sigma:(map ident value)) (a:(set1 ident)) (sigma':(map
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
480
  ident value)): Prop := forall (i:ident), (~ (mem i a)) -> ((get sigma
481
  i) = (get sigma' i)).
MARCHE Claude's avatar
MARCHE Claude committed
482

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
483
Axiom assigns_refl : forall (sigma:(map ident value)) (a:(set1 ident)),
MARCHE Claude's avatar
MARCHE Claude committed
484
485
  (assigns sigma a sigma).

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
486
487
488
Axiom assigns_trans : forall (sigma1:(map ident value)) (sigma2:(map ident
  value)) (sigma3:(map ident value)) (a:(set1 ident)), ((assigns sigma1 a
  sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
MARCHE Claude's avatar
MARCHE Claude committed
489

490
Axiom assigns_union_left : forall (sigma:(map ident value)) (sigma':(map
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
491
  ident value)) (s1:(set1 ident)) (s2:(set1 ident)), (assigns sigma s1
492
  sigma') -> (assigns sigma (union s1 s2) sigma').
MARCHE Claude's avatar
MARCHE Claude committed
493

494
Axiom assigns_union_right : forall (sigma:(map ident value)) (sigma':(map
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
495
  ident value)) (s1:(set1 ident)) (s2:(set1 ident)), (assigns sigma s2
496
  sigma') -> (assigns sigma (union s1 s2) sigma').
MARCHE Claude's avatar
MARCHE Claude committed
497
498
499

(* Why3 assumption *)
Set Implicit Arguments.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
500
Fixpoint expr_writes(e:expr) (w:(set1 ident)) {struct e}: Prop :=
MARCHE Claude's avatar
MARCHE Claude committed
501
502
503
504
505
506
507
508
509
510
511
512
  match e with
  | ((Evalue _)|((Evar _)|((Ederef _)|(Eassert _)))) => True
  | (Ebin e1 _ e2) => (expr_writes e1 w) /\ (expr_writes e2 w)
  | (Eassign id _) => (mem id w)
  | (Eseq e1 e2) => (expr_writes e1 w) /\ (expr_writes e2 w)
  | (Elet id e1 e2) => (expr_writes e1 w) /\ (expr_writes e2 w)
  | (Eif e1 e2 e3) => (expr_writes e1 w) /\ ((expr_writes e2 w) /\
      (expr_writes e3 w))
  | (Ewhile cond _ body) => (expr_writes cond w) /\ (expr_writes body w)
  end.
Unset Implicit Arguments.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
513
Parameter fresh_from: fmla -> expr -> ident.
MARCHE Claude's avatar
MARCHE Claude committed
514
515
516
517
518
519

Axiom fresh_from_fmla : forall (e:expr) (f:fmla),
  (fresh_in_fmla (fresh_from f e) f).

Axiom fresh_from_expr : forall (e:expr) (f:fmla),
  (fresh_in_expr (fresh_from f e) e).
MARCHE Claude's avatar
MARCHE Claude committed
520
521
522
523
524
525
526

Parameter abstract_effects: expr -> fmla -> fmla.

(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint wp(e:expr) (q:fmla) {struct e}: fmla :=
  match e with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
527
528
529
  | (Evalue v) => (Flet result (Tvalue v) q)
  | (Evar v) => (Flet result (Tvar v) q)
  | (Ederef x) => (Flet result (Tderef x) q)
MARCHE Claude's avatar
MARCHE Claude committed
530
531
  | (Eassert f) => (Fand f (Fimplies f q))
  | (Eseq e1 e2) => (wp e1 (wp e2 q))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
532
  | (Elet id e1 e2) => (wp e1 (Flet id (Tvar result) (wp e2 q)))
MARCHE Claude's avatar
MARCHE Claude committed
533
  | (Ebin e1 op e2) => let t1 := (fresh_from q e) in let t2 :=
534
      (fresh_from (Fand (Fterm (Tvar t1)) q) e) in let q' := (Flet result
MARCHE Claude's avatar
MARCHE Claude committed
535
      (Tbin (Tvar t1) op (Tvar t2)) q) in let f := (wp e2 (Flet t2
536
537
538
      (Tvar result) q')) in (wp e1 (Flet t1 (Tvar result) f))
  | (Eassign x e1) => let id := (fresh_from q e1) in let q' := (Flet result
      (Tvalue Vvoid) q) in (wp e1 (Flet id (Tvar result) (subst q' x id)))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
539
540
  | (Eif e1 e2 e3) => let f := (Fand (Fimplies (Fterm (Tvar result)) (wp e2
      q)) (Fimplies (Fnot (Fterm (Tvar result))) (wp e3 q))) in (wp e1 f)
MARCHE Claude's avatar
MARCHE Claude committed
541
  | (Ewhile cond inv body) => (Fand inv (abstract_effects body (wp cond
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
542
543
      (Fand (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv))
      (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q)))))
MARCHE Claude's avatar
MARCHE Claude committed
544
545
546
  end.
Unset Implicit Arguments.

547
548
549
Axiom wp_subst : forall (e:expr) (q:fmla) (id:ident) (id':ident),
  (fresh_in_expr id e) -> ((subst (wp e q) id id') = (wp e (subst q id
  id'))).
MARCHE Claude's avatar
MARCHE Claude committed
550

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
551
552
553
554
555
Axiom wp_implies : forall (p:fmla) (q:fmla), (forall (sigma:(map ident
  value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p) ->
  (eval_fmla sigma pi q)) -> forall (sigma:(map ident value)) (pi:(list
  (ident* value)%type)) (e:expr), (eval_fmla sigma pi (wp e p)) ->
  (eval_fmla sigma pi (wp e q)).
MARCHE Claude's avatar
MARCHE Claude committed
556

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
557
558
559
Axiom wp_conj : forall (sigma:(map ident value)) (pi:(list (ident*
  value)%type)) (e:expr) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp e (Fand p
  q))) <-> ((eval_fmla sigma pi (wp e p)) /\ (eval_fmla sigma pi (wp e q))).
MARCHE Claude's avatar
MARCHE Claude committed
560
561
562

Require Why3.
Ltac ae := why3 "alt-ergo" timelimit 2.
MARCHE Claude's avatar
MARCHE Claude committed
563
Ltac ae10 := why3 "alt-ergo" timelimit 10.
564
Ltac cvc10 := why3 "cvc3" timelimit 10.
MARCHE Claude's avatar
MARCHE Claude committed
565
566

(* Why3 goal *)
567
568
569
570
Theorem wp_reduction : forall (sigma:(map ident value)) (sigma':(map ident
  value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type))
  (e:expr) (e':expr), (one_step sigma pi e sigma' pi' e') -> forall (q:fmla),
  (eval_fmla sigma pi (wp e q)) -> (eval_fmla sigma' pi' (wp e' q)).
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
571

MARCHE Claude's avatar
MARCHE Claude committed
572
573
574
575
576
induction 1.
(* case 1: var *)
auto.
(* case 2: deref *)
auto.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
577
(* case 3: e_1 bin_op e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
578
intros q.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
579
simpl in *.
MARCHE Claude's avatar
MARCHE Claude committed
580
581
pose (t1 := fresh_from q (Ebin e1 op e2)).
fold t1.
582
pose (t1' := fresh_from q (Ebin e1' op e2)).
MARCHE Claude's avatar
MARCHE Claude committed
583
584
585
fold t1'.
pose (t2 := fresh_from (Fand (Fterm (Tvar t1)) q) (Ebin e1 op e2)).
fold t2.
586
pose (t2' := fresh_from (Fand (Fterm (Tvar t1')) q) (Ebin e1' op e2)).
MARCHE Claude's avatar
MARCHE Claude committed
587
588
fold t2'.
intros h.
MARCHE Claude's avatar
MARCHE Claude committed
589
apply IHone_step.
MARCHE Claude's avatar
MARCHE Claude committed
590
apply wp_implies with (2:=h).
591
intros sigma'' pi''.
MARCHE Claude's avatar
MARCHE Claude committed
592
intro.
593
apply let_equiv with (id':=t1).
MARCHE Claude's avatar
MARCHE Claude committed
594
595
596
597
598
599
600
rewrite wp_subst.
rewrite let_subst.
rewrite let_subst.
rewrite subst_fresh.
rewrite (subst_term_def (Tbin (Tvar t1') op (Tvar t2'))).
rewrite (subst_term_def (Tvar t1') t1' t1).
rewrite (subst_term_def (Tvar t2') t1' t1).
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
601
rewrite (subst_term_def (Tvar result) t1' t1).
MARCHE Claude's avatar
MARCHE Claude committed
602

MARCHE Claude's avatar
MARCHE Claude committed
603
admit. (* needs lemmas on fresh_from *)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
604
605
606
607
admit.
admit.
(* case 4: v_1 bin_op e_2 *)
intros q h.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
608

MARCHE Claude's avatar
MARCHE Claude committed
609
610
admit. 

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
611
(* case 5: v_1 bin_op v_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
612
613
614
intros q h.
admit. 

MARCHE Claude's avatar
MARCHE Claude committed
615
616
(* case x := e -> x := e' *)
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
617

MARCHE Claude's avatar
MARCHE Claude committed
618
(* case x := v -> void *)
MARCHE Claude's avatar
MARCHE Claude committed
619
620
admit.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
621
(* case Eseq e_1 e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
622
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
623
624

(* case Eseq void e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
625
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
626
627

(* case Elet id e_1 e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
628
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
629
630

(* case Elet id v_1 e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
631
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
632
633

(* case Eif e_1 e_2 e_3*)
MARCHE Claude's avatar
MARCHE Claude committed
634
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
635
636

(* case Eif true e_1 e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
637
admit.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
638
639

(* case Eif false e_1 e_2 *)
MARCHE Claude's avatar
MARCHE Claude committed
640
641
admit.

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
642
643
(* case Eassert f *)
admit.
MARCHE Claude's avatar
MARCHE Claude committed
644

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
645
646
(* case Ewhile cond inv body *)
admit.
MARCHE Claude's avatar
MARCHE Claude committed
647

MARCHE Claude's avatar
MARCHE Claude committed
648
649
Qed.

650