1 | include "Clight/Csyntax.ma". |
---|
2 | include "Clight/TypeComparison.ma". |
---|
3 | |
---|
4 | (* IG: used to prove preservation of the semantics. *) |
---|
5 | include "Clight/Cexec.ma". |
---|
6 | include "Clight/casts.ma". |
---|
7 | include "Clight/CexecSound.ma". |
---|
8 | |
---|
9 | include "Clight/frontend_misc.ma". |
---|
10 | |
---|
11 | |
---|
12 | (* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *) |
---|
13 | |
---|
14 | (* Attempt to remove unnecessary integer casts in Clight programs. |
---|
15 | |
---|
16 | This differs from the OCaml prototype by attempting to recursively determine |
---|
17 | whether subexpressions can be changed rather than using a fixed size pattern. |
---|
18 | As a result more complex expressions such as (char)((int)x + (int)y + (int)z) |
---|
19 | where x,y and z are chars can be simplified. |
---|
20 | |
---|
21 | A possible improvement that doesn't quite fit into this scheme would be to |
---|
22 | spot that casts can be removed in expressions like (int)x == (int)y where |
---|
23 | x and y have some smaller integer type. |
---|
24 | *) |
---|
25 | |
---|
26 | (* Attempt to squeeze integer constant into a given type. |
---|
27 | |
---|
28 | This might be too conservative --- if we're going to cast it anyway, can't |
---|
29 | I just ignore the fact that the integer doesn't fit? |
---|
30 | *) |
---|
31 | |
---|
32 | (* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size |
---|
33 | * m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal |
---|
34 | * to [exp]. If it fails, it returns None. *) |
---|
35 | let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝ |
---|
36 | match n return λn. BitVector (n+S m) → option (BitVector (S m)) with |
---|
37 | [ O ⇒ λv. Some ? v |
---|
38 | | S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ? |
---|
39 | ] v. |
---|
40 | |
---|
41 | lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'. |
---|
42 | #n #m #exp #v #v' #H whd in H:(??%?); lapply H -H |
---|
43 | cases (eq_b ? exp) |
---|
44 | [ 1: #H whd in H:(??%?); // |
---|
45 | | 2: #H normalize in H; destruct ] qed. |
---|
46 | |
---|
47 | lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'. |
---|
48 | reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v. |
---|
49 | #n #m elim n |
---|
50 | [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n // |
---|
51 | | 2: #n' #Hind #exp #v #v' #H >truncate_tail |
---|
52 | > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed. |
---|
53 | |
---|
54 | lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?. |
---|
55 | #n #m #exp #v elim (reduce_bits n m exp v) |
---|
56 | [ 1: %2 // |
---|
57 | | 2: #v' %1 @(ex_intro … v') // ] qed. |
---|
58 | |
---|
59 | (* pred_bitsize_of_intsize I32 = 31, … *) |
---|
60 | definition pred_bitsize_of_intsize : intsize → nat ≝ |
---|
61 | λsz. pred (bitsize_of_intsize sz). |
---|
62 | |
---|
63 | definition signed : signedness → bool ≝ |
---|
64 | λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ]. |
---|
65 | |
---|
66 | (* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg] |
---|
67 | * into an integer of size [sz'] of signedness [sg']. |
---|
68 | * - It first proceeds by comparing the source and target width: if the target width is strictly superior |
---|
69 | * to the source width, the conversion fails. |
---|
70 | * - If the size is equal, the argument is returned as-is. |
---|
71 | * - If the target type is strictly smaller than the source, it tries to squeeze the integer to |
---|
72 | * the desired size. |
---|
73 | *) |
---|
74 | let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝ |
---|
75 | let bit ≝ signed sg ∧ head' … i in |
---|
76 | (* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args. |
---|
77 | * if x < y, nat_compare x y = lt(x, y-(x+1)) |
---|
78 | * if x = y, nat_compare x y = eq x |
---|
79 | * if x > y, nat_compare x y = gt(x-(y+1), y) *) |
---|
80 | match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz') |
---|
81 | return λn,m,x.BitVector (S n) → option (BitVector (S m)) with |
---|
82 | [ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *) |
---|
83 | | nat_eq _ ⇒ λi. Some ? i |
---|
84 | | nat_gt x y ⇒ λi. |
---|
85 | (* Here, we have [x]=31-([y]+1) and [y] ∈ {15; 7} OR [x] = 15-(7+1) and [y] = 7. I.e.: x=15,y=15 or x=23,y=7 or x=7,y=7. |
---|
86 | * In [reduce_bits n m bit i], [i] is supposed to have type BitVector n + (S m). Since its type is here (S x) + (S y), |
---|
87 | * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent. |
---|
88 | * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits. |
---|
89 | * Otherwise, it tries to remove the (S x) first "0" bits. |
---|
90 | *) |
---|
91 | match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with |
---|
92 | [ Some i' ⇒ |
---|
93 | if signed sg' then |
---|
94 | if eq_b bit (head' … i') then |
---|
95 | Some ? i' |
---|
96 | else None ? |
---|
97 | else Some ? i' |
---|
98 | | None ⇒ None ? |
---|
99 | ] |
---|
100 | ] i. |
---|
101 | >(commutative_plus_faster (S x)) @refl |
---|
102 | qed. |
---|
103 | |
---|
104 | |
---|
105 | lemma eq_intsize_identity : ∀id. eq_intsize id id = true. |
---|
106 | * normalize // |
---|
107 | qed. |
---|
108 | |
---|
109 | lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s). |
---|
110 | * normalize // |
---|
111 | qed. |
---|
112 | |
---|
113 | lemma type_eq_identity : ∀t. type_eq t t = true. |
---|
114 | #t normalize elim (type_eq_dec t t) |
---|
115 | [ 1: #Heq normalize // |
---|
116 | | 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. |
---|
117 | |
---|
118 | lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false. |
---|
119 | #t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2) |
---|
120 | [ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2)) |
---|
121 | | 2: #Hneq' normalize // ] qed. |
---|
122 | |
---|
123 | definition size_le ≝ λsz1,sz2. |
---|
124 | match sz1 with |
---|
125 | [ I8 ⇒ True |
---|
126 | | I16 ⇒ |
---|
127 | match sz2 with |
---|
128 | [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ] |
---|
129 | | I32 ⇒ |
---|
130 | match sz2 with |
---|
131 | [ I32 ⇒ True | _ ⇒ False ] |
---|
132 | ]. |
---|
133 | |
---|
134 | definition size_lt ≝ λsz1,sz2. |
---|
135 | match sz1 with |
---|
136 | [ I8 ⇒ |
---|
137 | match sz2 with |
---|
138 | [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ] |
---|
139 | | I16 ⇒ |
---|
140 | match sz2 with |
---|
141 | [ I32 ⇒ True | _ ⇒ False ] |
---|
142 | | I32 ⇒ False |
---|
143 | ]. |
---|
144 | |
---|
145 | lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2. |
---|
146 | #sz1 #sz2 elim sz1 elim sz2 normalize // qed. |
---|
147 | |
---|
148 | lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)). |
---|
149 | * * normalize /2/ /3/ |
---|
150 | qed. |
---|
151 | |
---|
152 | lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1). |
---|
153 | * * normalize /2/ /3/ |
---|
154 | qed. |
---|
155 | |
---|
156 | (* This function already exists in prop, we want it in type. *) |
---|
157 | definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2). |
---|
158 | * * normalize // qed. |
---|
159 | |
---|
160 | lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False. |
---|
161 | * * normalize |
---|
162 | #H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. |
---|
163 | |
---|
164 | (* This defines necessary conditions for [src_expr] to be coerced to "target_ty". |
---|
165 | * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *) |
---|
166 | definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg. |
---|
167 | match size_lt_dec target_sz src_sz with |
---|
168 | [ inl Hlt ⇒ true |
---|
169 | | inr Hnlt ⇒ |
---|
170 | match sz_eq_dec target_sz src_sz with |
---|
171 | [ inl Hsz_eq ⇒ |
---|
172 | match sign_eq_dect src_sg target_sg with |
---|
173 | [ inl Hsg_eq ⇒ false |
---|
174 | | inr Hsg_neq ⇒ true |
---|
175 | ] |
---|
176 | | inr Hsz_neq ⇒ false |
---|
177 | ] |
---|
178 | ]. |
---|
179 | |
---|
180 | (* Inversion on necessary_conditions *) |
---|
181 | lemma necessary_conditions_spec : |
---|
182 | ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → |
---|
183 | ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)). |
---|
184 | #src_sz #src_sg #target_sz #target_sg |
---|
185 | whd in match (necessary_conditions ????); |
---|
186 | cases (size_lt_dec target_sz src_sz) normalize nodelta |
---|
187 | [ 1: #Hlt #_ %1 // |
---|
188 | | 2: #Hnlt |
---|
189 | cases (sz_eq_dec target_sz src_sz) normalize nodelta |
---|
190 | [ 2: #_ #Hcontr destruct |
---|
191 | | 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta |
---|
192 | [ 1: #_ #Hcontr destruct |
---|
193 | | 2: #Hsg_neq #_ %2 destruct /2/ ] |
---|
194 | ] |
---|
195 | ] qed. |
---|
196 | |
---|
197 | (* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an |
---|
198 | * integer value smaller but containing the same stuff than [r2] then all is well. |
---|
199 | * If the first evaluation is erroneous, we don't care about anything else. *) |
---|
200 | definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace). |
---|
201 | match r1 with |
---|
202 | [ OK res1 ⇒ |
---|
203 | let 〈val1, tr1〉 ≝ res1 in |
---|
204 | ∀v1. val1 = Vint src_sz v1 → |
---|
205 | match r2 with |
---|
206 | [ OK res2 ⇒ |
---|
207 | let 〈val2, tr2〉 ≝ res2 in |
---|
208 | ∃v2. (val2 = Vint dst_sz v2 ∧ |
---|
209 | v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz) |
---|
210 | | _ ⇒ False ] |
---|
211 | | Error errmsg1 ⇒ True |
---|
212 | ]. |
---|
213 | |
---|
214 | (* Simulation relation used for expression evaluation. *) |
---|
215 | inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ |
---|
216 | | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2 |
---|
217 | | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2. |
---|
218 | |
---|
219 | (* Trick to reduce checking time by eliminating a load of costly automation. |
---|
220 | It would be nice to do this by refactoring the type and code instead, but we |
---|
221 | don't want to spend lots of time on something that already works. *) |
---|
222 | |
---|
223 | lemma SimFailNicely : ∀A,err,r2. res_sim A (Error ? err) r2. |
---|
224 | #A #err #r2 @SimFail %{err} % |
---|
225 | qed. |
---|
226 | |
---|
227 | (* Invariant of simplify_expr *) |
---|
228 | inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝ |
---|
229 | (* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *) |
---|
230 | | Inv_eq : ∀result_flag. |
---|
231 | result_flag = false → |
---|
232 | typeof e1 = typeof e2 → |
---|
233 | res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) → |
---|
234 | res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) → |
---|
235 | simplify_inv ge en m e1 e2 target_sz target_sg result_flag |
---|
236 | (* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *) |
---|
237 | | Inv_coerce_ok : ∀src_sz,src_sg. |
---|
238 | (typeof e1) = (Tint src_sz src_sg) → |
---|
239 | (typeof e2) = (Tint target_sz target_sg) → |
---|
240 | (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → |
---|
241 | simplify_inv ge en m e1 e2 target_sz target_sg true. |
---|
242 | |
---|
243 | (* Invariant of simplify_inside *) |
---|
244 | definition conservation ≝ λe,result:expr. |
---|
245 | ∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result) |
---|
246 | ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) |
---|
247 | ∧ typeof e = typeof result. |
---|
248 | |
---|
249 | (* This lemma proves that simplify_int actually implements an integer cast. *) |
---|
250 | (* The case 4 can be merged with cases 7 and 8. *) |
---|
251 | |
---|
252 | lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i. |
---|
253 | * * |
---|
254 | [ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct // |
---|
255 | | 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct whd in Hsimp:(??%?); destruct *) |
---|
256 | | 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; |
---|
257 | normalize in match (signed ?) in Hsimp; |
---|
258 | normalize in match (S (plus ??)) in Hsimp; |
---|
259 | normalize in match (plus 7 8) in Hsimp; |
---|
260 | lapply Hsimp -Hsimp |
---|
261 | cases (head' bool 15 i) |
---|
262 | normalize in match (andb ??); |
---|
263 | [ 1,3: elim (reduce_bits_dec 8 7 true i) |
---|
264 | [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta |
---|
265 | [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl |
---|
266 | | 2: #H destruct normalize @refl ] |
---|
267 | | 2,4: #Heq >Heq normalize nodelta #H destruct ] |
---|
268 | | 2,4,5,6,7,8: |
---|
269 | elim (reduce_bits_dec 8 7 false i) |
---|
270 | [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) |
---|
271 | [ 1,3,4: cases (eq_b false ?) normalize nodelta |
---|
272 | #H destruct normalize @refl |
---|
273 | | 2,5,6: #H destruct normalize @refl ] |
---|
274 | | 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct |
---|
275 | ] |
---|
276 | ] |
---|
277 | | 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl |
---|
278 | | 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %; |
---|
279 | normalize in match (signed ?) in Hsimp; |
---|
280 | normalize in match (S (plus ??)) in Hsimp; |
---|
281 | normalize in match (plus 7 24) in Hsimp; |
---|
282 | lapply Hsimp -Hsimp |
---|
283 | cases (head' bool ? i) |
---|
284 | normalize in match (andb ??); |
---|
285 | [ 1,3,9,11: |
---|
286 | [ 1,2: (elim (reduce_bits_dec 24 7 true i)) | 3,4: (elim (reduce_bits_dec 16 15 true i)) ] |
---|
287 | [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta |
---|
288 | [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl |
---|
289 | | 2,4: #H destruct normalize @refl ] |
---|
290 | | 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ] |
---|
291 | | 2,4,5,6,7,8,10,12,13,14,15,16: |
---|
292 | [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i) |
---|
293 | | 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ] |
---|
294 | [ 1,3,5,7,9,11,13,15,17,19,21,23: |
---|
295 | * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq) |
---|
296 | [ 1,3,4,7,9,10: |
---|
297 | cases (eq_b false ?) normalize nodelta #H destruct normalize @refl |
---|
298 | | 2,5,6,8,11,12: #H destruct normalize @refl ] |
---|
299 | | 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct |
---|
300 | ] |
---|
301 | ] |
---|
302 | ] qed. |
---|
303 | |
---|
304 | (* Facts about cast_int_int *) |
---|
305 | |
---|
306 | |
---|
307 | lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)). |
---|
308 | #s1 #v normalize elim s1 normalize nodelta |
---|
309 | normalize in v; |
---|
310 | elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) |
---|
311 | [ 2,4: // |
---|
312 | | 1,3: #l * #r normalize nodelta #Eq1 |
---|
313 | <(vsplit_prod bool 16 16 … Eq1) |
---|
314 | elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) |
---|
315 | [ 2,4: // |
---|
316 | | 1,3: #lr * #rr normalize nodelta #Eq2 |
---|
317 | <(vsplit_prod bool 8 8 … Eq2) |
---|
318 | cut (v = (l @@ lr) @@ rr) |
---|
319 | [ 1,3 : destruct >(vector_associative_append ? 16 8) // |
---|
320 | | 2,4: #Hrewrite destruct |
---|
321 | <(vsplit_prod bool 24 8 … Hrewrite) @refl |
---|
322 | ] |
---|
323 | ] |
---|
324 | ] qed. |
---|
325 | |
---|
326 | lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v. |
---|
327 | #s1 #s2 * * #v elim s1 elim s2 |
---|
328 | normalize #H try @refl |
---|
329 | @(False_ind … H) |
---|
330 | qed. |
---|
331 | |
---|
332 | lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v. |
---|
333 | * * #v normalize // qed. |
---|
334 | |
---|
335 | lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v). |
---|
336 | #s1 #s2 #v >cast_decompose >cast_idempotent |
---|
337 | [ 1: @refl | 2: // ] |
---|
338 | qed. |
---|
339 | |
---|
340 | lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. |
---|
341 | size_lt c_sz a_sz → size_lt c_sz b_sz → |
---|
342 | (cast_int_int a_sz a_sg c_sz val = |
---|
343 | cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). |
---|
344 | * #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??); |
---|
345 | #Hlt1 #Hlt2 |
---|
346 | [ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27: |
---|
347 | @(False_ind … Hlt1) @(False_ind … Hlt2) |
---|
348 | | 13,25,26: >cast_identity elim a_sg elim b_sg normalize // |
---|
349 | | 22: normalize elim b_sg elim a_sg normalize |
---|
350 | normalize in val; |
---|
351 | elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉)) |
---|
352 | [ 2,4,6,8: normalize // |
---|
353 | | 1,3,5,7: #left * #right normalize #Eq1 |
---|
354 | <(vsplit_prod bool 16 16 … Eq1) |
---|
355 | elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉)) |
---|
356 | [ 2,4,6,8: // |
---|
357 | | 1,3,5,7: #rightleft * #rightright normalize #Eq2 |
---|
358 | <(vsplit_prod bool 8 8 … Eq2) |
---|
359 | cut (val = (left @@ rightleft) @@ rightright) |
---|
360 | [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) // |
---|
361 | | 2,4,6,8: #Hrewrite destruct |
---|
362 | <(vsplit_prod bool 24 8 … Hrewrite) @refl |
---|
363 | ] |
---|
364 | ] |
---|
365 | ] |
---|
366 | | 16: elim b_sg elim a_sg >cast_collapse @refl |
---|
367 | ] qed. |
---|
368 | |
---|
369 | lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val. |
---|
370 | size_le c_sz a_sz → size_le c_sz b_sz → |
---|
371 | (cast_int_int a_sz a_sg c_sz val = |
---|
372 | cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)). |
---|
373 | #a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b |
---|
374 | cases (size_lt_dec c_sz a_sz) |
---|
375 | cases (size_lt_dec c_sz b_sz) |
---|
376 | [ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb) |
---|
377 | | 2: #Hnltb #Hlta |
---|
378 | cases (size_not_lt_to_ge … Hnltb) |
---|
379 | [ 1: #Heq destruct >cast_identity // |
---|
380 | | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb)) |
---|
381 | ] |
---|
382 | | 3: #Hltb #Hnlta |
---|
383 | cases (size_not_lt_to_ge … Hnlta) |
---|
384 | [ 1: #Heq destruct >cast_idempotent // |
---|
385 | | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) |
---|
386 | ] |
---|
387 | | 4: #Hnltb #Hnlta |
---|
388 | cases (size_not_lt_to_ge … Hnlta) |
---|
389 | cases (size_not_lt_to_ge … Hnltb) |
---|
390 | [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity // |
---|
391 | | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb)) |
---|
392 | | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) |
---|
393 | | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta)) |
---|
394 | ] |
---|
395 | ] qed. |
---|
396 | |
---|
397 | let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝ |
---|
398 | match v with |
---|
399 | [ None ⇒ None ? |
---|
400 | | Some v ⇒ |
---|
401 | match v with |
---|
402 | [ Vint sz i ⇒ |
---|
403 | match sz_eq_dec sz expected_size with |
---|
404 | [ inl Heq ⇒ Some ?? |
---|
405 | | inr _ ⇒ None ? |
---|
406 | ] |
---|
407 | | _ ⇒ None ? |
---|
408 | ] |
---|
409 | ]. |
---|
410 | >Heq in i; #i @i qed. |
---|
411 | |
---|
412 | (* cast_int_int behaves as truncate (≃ vsplit) when downsizing *) |
---|
413 | (* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *) |
---|
414 | |
---|
415 | lemma vsplit_to_truncate : ∀m,n,i. (\snd (vsplit bool m n i)) = truncate m n i. |
---|
416 | #m #n #i normalize // qed. |
---|
417 | |
---|
418 | (* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *) |
---|
419 | |
---|
420 | lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → |
---|
421 | (addition_n (bitsize_of_intsize target_sz) |
---|
422 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
423 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
424 | = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
425 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt |
---|
426 | elim src_sz in Hlt lhs_int rhs_int; elim target_sz |
---|
427 | [ 1,2,3,5,6,9: normalize #H @(False_ind … H) |
---|
428 | | *: elim sg #_ |
---|
429 | normalize in match (bitsize_of_intsize ?); |
---|
430 | normalize in match (bitsize_of_intsize ?); |
---|
431 | #lint #rint |
---|
432 | normalize in match (cast_int_int ????); |
---|
433 | normalize in match (cast_int_int ????); |
---|
434 | whd in match (addition_n ???); |
---|
435 | whd in match (addition_n ???) in ⊢ (???%); |
---|
436 | >vsplit_to_truncate >vsplit_to_truncate |
---|
437 | <truncate_add_with_carries |
---|
438 | [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false); |
---|
439 | | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false); |
---|
440 | | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false); |
---|
441 | ] |
---|
442 | * #result #carry |
---|
443 | normalize nodelta // |
---|
444 | qed. |
---|
445 | |
---|
446 | lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz → |
---|
447 | (addition_n (bitsize_of_intsize target_sz) |
---|
448 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
449 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
450 | = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
451 | #src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct |
---|
452 | >cast_identity >cast_identity >cast_identity // qed. |
---|
453 | |
---|
454 | lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → |
---|
455 | (addition_n (bitsize_of_intsize target_sz) |
---|
456 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
457 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
458 | = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
459 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hle |
---|
460 | cases (sz_eq_dec target_sz src_sz) |
---|
461 | [ 1: #Heq @(integer_add_cast_eq … Heq) |
---|
462 | | 2: #Hneq cut (size_lt target_sz src_sz) |
---|
463 | [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // |
---|
464 | #_ * #H @(H … (refl ??)) |
---|
465 | | 2: #Hlt @(integer_add_cast_lt … Hlt) |
---|
466 | ] |
---|
467 | ] qed. |
---|
468 | |
---|
469 | lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl. |
---|
470 | #l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len |
---|
471 | @(ex_intro … tl) |
---|
472 | >Heq >Heq |
---|
473 | elim (vsplit_eq2 … tl) #l * #r #Eq |
---|
474 | normalize |
---|
475 | <(vsplit_prod bool n m tl l r Eq) |
---|
476 | <(vsplit_prod2 bool n m tl l r Eq) |
---|
477 | normalize // |
---|
478 | qed. |
---|
479 | |
---|
480 | |
---|
481 | lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i). |
---|
482 | #m elim m |
---|
483 | [ 1: #n #i normalize in i; |
---|
484 | whd in match (truncate ???); |
---|
485 | whd in match (truncate ???) in ⊢ (???%); |
---|
486 | <vsplit_zero <vsplit_zero // |
---|
487 | | 2: #m' #Hind #n #i normalize in i; |
---|
488 | elim (Vector_Sn … i) #hd * #tl #Heq |
---|
489 | whd in match (two_complement_negation (S ?) ?); |
---|
490 | >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?); |
---|
491 | whd in match (two_complement_negation ??) in ⊢ (??%?); |
---|
492 | lapply (Hind ? tl) #H |
---|
493 | whd in match (two_complement_negation ??) in H; |
---|
494 | (* trying to reduce add_with_carries *) |
---|
495 | normalize in match (S m'+n); |
---|
496 | whd in match (zero ?) in ⊢ (???%); |
---|
497 | >Heq in match (negation_bv ??) in ⊢ (???%); |
---|
498 | whd in match (negation_bv ??) in ⊢ (???%); |
---|
499 | >add_with_carries_unfold in ⊢ (???%); |
---|
500 | normalize in ⊢ (???%); |
---|
501 | cases hd normalize nodelta |
---|
502 | [ 1,2: <add_with_carries_unfold in ⊢ (???%); (* Good. Some progress. *) |
---|
503 | (* try to transform the rhs of H into what we need. *) |
---|
504 | whd in match (two_complement_negation ??) in H:(???%); |
---|
505 | lapply H -H |
---|
506 | generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true); |
---|
507 | * #Left #Right normalize nodelta |
---|
508 | #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒ ?]))))); |
---|
509 | #b >(vsplit_to_truncate (S m')) >truncate_tail |
---|
510 | cases b |
---|
511 | normalize nodelta |
---|
512 | normalize in match (tail ???); @H |
---|
513 | ] |
---|
514 | ] qed. (* This was painful. *) |
---|
515 | |
---|
516 | lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz → |
---|
517 | (subtraction (bitsize_of_intsize target_sz) |
---|
518 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
519 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
520 | = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
521 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hlt |
---|
522 | elim src_sz in Hlt lhs_int rhs_int; elim target_sz |
---|
523 | [ 1,2,3,5,6,9: normalize #H @(False_ind … H) |
---|
524 | | *: elim sg #_ |
---|
525 | normalize in match (bitsize_of_intsize ?); |
---|
526 | normalize in match (bitsize_of_intsize ?); |
---|
527 | #lint #rint |
---|
528 | normalize in match (cast_int_int ????); |
---|
529 | normalize in match (cast_int_int ????); |
---|
530 | whd in match (subtraction ???); |
---|
531 | whd in match (subtraction ???) in ⊢ (???%); |
---|
532 | >vsplit_to_truncate >vsplit_to_truncate |
---|
533 | >integer_neg_trunc <truncate_add_with_carries |
---|
534 | [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false); |
---|
535 | | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false); |
---|
536 | | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false); |
---|
537 | ] |
---|
538 | * #result #carry |
---|
539 | normalize nodelta // |
---|
540 | qed. |
---|
541 | |
---|
542 | lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz → |
---|
543 | (subtraction (bitsize_of_intsize target_sz) |
---|
544 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
545 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
546 | = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
547 | #src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct |
---|
548 | >cast_identity >cast_identity >cast_identity // |
---|
549 | qed. |
---|
550 | |
---|
551 | lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz → |
---|
552 | (subtraction (bitsize_of_intsize target_sz) |
---|
553 | (cast_int_int src_sz sg target_sz lhs_int) |
---|
554 | (cast_int_int src_sz sg target_sz rhs_int) |
---|
555 | = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)). |
---|
556 | #src_sz #target_sz #sg #lhs_int #rhs_int #Hle |
---|
557 | cases (sz_eq_dec target_sz src_sz) |
---|
558 | [ 1: #Heq @(integer_sub_cast_eq … Heq) |
---|
559 | | 2: #Hneq cut (size_lt target_sz src_sz) |
---|
560 | [ 1: elim target_sz in Hle Hneq; elim src_sz normalize // |
---|
561 | #_ * #H @(H … (refl ??)) |
---|
562 | | 2: #Hlt @(integer_sub_cast_lt … Hlt) |
---|
563 | ] |
---|
564 | ] qed. |
---|
565 | |
---|
566 | lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le sz' sz. |
---|
567 | * #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed. |
---|
568 | |
---|
569 | lemma smaller_integer_val_identity : ∀sz,sg,x. |
---|
570 | smaller_integer_val sz sz sg x x. |
---|
571 | #sz #sg * |
---|
572 | [ 2: #error // |
---|
573 | | 1: * #val #trace whd in match (smaller_integer_val ?????); |
---|
574 | #v1 #Hval %{v1} @conj try @conj try @conj // |
---|
575 | elim sz // |
---|
576 | ] qed. |
---|
577 | |
---|
578 | (* Inversion on exec_cast *) |
---|
579 | lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result. |
---|
580 | exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result → |
---|
581 | ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i). |
---|
582 | #castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result |
---|
583 | elim castee_val |
---|
584 | [ 1: | 2: #sz' #i | 3: | 4: #ptr ] |
---|
585 | [ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ] |
---|
586 | whd in ⊢ ((??%?) → ?); |
---|
587 | cases (sz_eq_dec sz' src_sz) |
---|
588 | [ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct |
---|
589 | %{i} /2/ |
---|
590 | | 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ] |
---|
591 | qed. |
---|
592 | |
---|
593 | |
---|
594 | (* Lemmas related to the Ebinop case *) |
---|
595 | |
---|
596 | lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg. |
---|
597 | * * // qed. |
---|
598 | |
---|
599 | lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg. |
---|
600 | * * // qed. |
---|
601 | |
---|
602 | lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true. |
---|
603 | * * normalize #H @conj try @refl assumption qed. |
---|
604 | |
---|
605 | (* Operations where it is safe to use a smaller integer type on the assumption |
---|
606 | that we would cast it down afterwards anyway. *) |
---|
607 | definition binop_simplifiable ≝ |
---|
608 | λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ]. |
---|
609 | |
---|
610 | (* Inversion principle for integer addition *) |
---|
611 | lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → |
---|
612 | ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)). |
---|
613 | #sz #sg #v1 #v2 #m #r |
---|
614 | elim v1 |
---|
615 | [ 1: | 2: #sz' #i | 3: | 4: #ptr ] |
---|
616 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
617 | >classify_add_int normalize nodelta #H destruct |
---|
618 | elim v2 in H; |
---|
619 | [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ] |
---|
620 | whd in ⊢ ((??%?) → ?); #H destruct |
---|
621 | elim (sz_eq_dec sz' sz'') |
---|
622 | [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ |
---|
623 | | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct |
---|
624 | ] qed. |
---|
625 | |
---|
626 | (* Inversion principle for integer subtraction. *) |
---|
627 | lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → |
---|
628 | ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)). |
---|
629 | #sz #sg #v1 #v2 #m #r |
---|
630 | elim v1 |
---|
631 | [ 1: | 2: #sz' #i | 3: | 4: #ptr ] |
---|
632 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
633 | >classify_sub_int normalize nodelta #H destruct |
---|
634 | elim v2 in H; |
---|
635 | [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ] |
---|
636 | whd in ⊢ ((??%?) → ?); #H destruct |
---|
637 | elim (sz_eq_dec sz' sz'') |
---|
638 | [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ |
---|
639 | | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct |
---|
640 | ] qed. |
---|
641 | |
---|
642 | definition is_int : val → Prop ≝ |
---|
643 | λv. |
---|
644 | match v with |
---|
645 | [ Vint _ _ ⇒ True |
---|
646 | | _ ⇒ False ]. |
---|
647 | |
---|
648 | (* "negative" (in the sense of ¬ Some) inversion principle for integer addition *) |
---|
649 | lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → |
---|
650 | ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ |
---|
651 | ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. |
---|
652 | #sz #sg #v1 #v2 #m |
---|
653 | elim v1 |
---|
654 | [ 1: | 2: #sz' #i | 3: | 4: #ptr ] |
---|
655 | [ 2: | *: #_ %1 %1 % #H @H ] |
---|
656 | elim v2 |
---|
657 | [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ] |
---|
658 | [ 2: | *: #_ %1 %2 % #H @H ] |
---|
659 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
660 | >classify_add_int normalize nodelta |
---|
661 | elim (sz_eq_dec sz' sz'') |
---|
662 | [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) |
---|
663 | | 2: #Hneq >intsize_eq_elim_false try assumption #_ |
---|
664 | %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // |
---|
665 | ] qed. |
---|
666 | |
---|
667 | (* "negative" inversion principle for integer subtraction *) |
---|
668 | lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? → |
---|
669 | ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ |
---|
670 | ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. |
---|
671 | #sz #sg #v1 #v2 #m |
---|
672 | elim v1 |
---|
673 | [ 1: | 2: #sz' #i | 3: | 4: #ptr ] |
---|
674 | [ 2: | *: #_ %1 %1 % #H @H ] |
---|
675 | elim v2 |
---|
676 | [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ] |
---|
677 | [ 2: | *: #_ %1 %2 % #H @H ] |
---|
678 | whd in ⊢ ((??%?) → ?); normalize nodelta |
---|
679 | >classify_sub_int normalize nodelta |
---|
680 | elim (sz_eq_dec sz' sz'') |
---|
681 | [ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd) |
---|
682 | | 2: #Hneq >intsize_eq_elim_false try assumption #_ |
---|
683 | %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // |
---|
684 | ] qed. |
---|
685 | |
---|
686 | lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. |
---|
687 | ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?. |
---|
688 | #op #sz #sg #v1 #v2 #m #H |
---|
689 | elim op normalize in match (binop_simplifiable ?); #H destruct |
---|
690 | elim v1 in H; |
---|
691 | [ 1,5: | 2,6: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,7: | 4,8: #ptr ] |
---|
692 | #_ |
---|
693 | whd in match (sem_binary_operation ??????); normalize nodelta |
---|
694 | >classify_add_int normalize nodelta // |
---|
695 | >classify_sub_int normalize nodelta // |
---|
696 | qed. |
---|
697 | |
---|
698 | notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)" |
---|
699 | with precedence 10 |
---|
700 | for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }. |
---|
701 | |
---|
702 | notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)" |
---|
703 | with precedence 10 |
---|
704 | for @{ match $t return λx.x = $t → ? with |
---|
705 | [ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}. |
---|
706 | match ${fresh a} return λx.x = ${fresh a} → ? with |
---|
707 | [ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a}) |
---|
708 | ] (refl ? $t) |
---|
709 | }. |
---|
710 | |
---|
711 | (* This function will make your eyes bleed. You've been warned. |
---|
712 | * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by |
---|
713 | * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either |
---|
714 | what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original |
---|
715 | expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper. |
---|
716 | * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable. |
---|
717 | * This function is slightly more conservative than the original one, but this should be incrementally |
---|
718 | * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction). |
---|
719 | * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something |
---|
720 | * more or less "modular", case-by-case wise. |
---|
721 | *) |
---|
722 | let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) |
---|
723 | : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ |
---|
724 | match e return λx. x = e → ? with |
---|
725 | [ Expr ed ty ⇒ λHexpr_eq. |
---|
726 | match ed return λx. ed = x → ? with |
---|
727 | [ Econst_int cst_sz i ⇒ λHdesc_eq. |
---|
728 | match ty return λx. x=ty → ? with |
---|
729 | [ Tint ty_sz sg ⇒ λHexprtype_eq. |
---|
730 | (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *) |
---|
731 | match sz_eq_dec cst_sz ty_sz with |
---|
732 | [ inl Hsz_eq ⇒ |
---|
733 | match type_eq_dec ty (Tint target_sz target_sg) with |
---|
734 | [ inl Hdonothing ⇒ «〈true, e〉, ?» |
---|
735 | | inr Hdosomething ⇒ |
---|
736 | (* Do the actual useful work *) |
---|
737 | match simplify_int cst_sz target_sz sg target_sg i return λx. (simplify_int cst_sz target_sz sg target_sg i) = x → ? with |
---|
738 | [ Some i' ⇒ λHsimpl_eq. |
---|
739 | «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?» |
---|
740 | | None ⇒ λ_. |
---|
741 | «〈false, e〉, ?» |
---|
742 | ] (refl ? (simplify_int cst_sz target_sz sg target_sg i)) |
---|
743 | ] |
---|
744 | | inr _ ⇒ (* The expression is ill-typed. *) |
---|
745 | «〈false, e〉, ?» |
---|
746 | ] |
---|
747 | | _ ⇒ λ_. |
---|
748 | «〈false, e〉, ?» |
---|
749 | ] (refl ? ty) |
---|
750 | | Ederef e1 ⇒ λHdesc_eq. |
---|
751 | let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
752 | «〈false, Expr (Ederef e2) ty〉, ?» |
---|
753 | | Eaddrof e1 ⇒ λHdesc_eq. |
---|
754 | let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
755 | «〈false, Expr (Eaddrof e2) ty〉, ?» |
---|
756 | | Eunop op e1 ⇒ λHdesc_eq. |
---|
757 | let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
758 | «〈false, Expr (Eunop op e2) ty〉, ?» |
---|
759 | | Ebinop op lhs rhs ⇒ λHdesc_eq. |
---|
760 | (* Type equality is enforced to prove the equalities needed in return by the invariant. *) |
---|
761 | match binop_simplifiable op |
---|
762 | return λx. (binop_simplifiable op) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) |
---|
763 | with |
---|
764 | [ true ⇒ λHop_simplifiable_eq. |
---|
765 | match assert_type_eq ty (typeof lhs) with |
---|
766 | [ OK Hty_eq_lhs ⇒ |
---|
767 | match assert_type_eq (typeof lhs) (typeof rhs) with |
---|
768 | [ OK Htylhs_eq_tyrhs ⇒ |
---|
769 | let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in |
---|
770 | let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in |
---|
771 | match desired_type_lhs ∧ desired_type_rhs |
---|
772 | return λx. (desired_type_lhs ∧ desired_type_rhs) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) |
---|
773 | with |
---|
774 | [ true ⇒ λHdesired_eq. |
---|
775 | «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?» |
---|
776 | | false ⇒ λHdesired_eq. |
---|
777 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
778 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
779 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
780 | ] (refl ? (desired_type_lhs ∧ desired_type_rhs)) |
---|
781 | | Error _ ⇒ |
---|
782 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
783 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
784 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
785 | ] |
---|
786 | | Error _ ⇒ |
---|
787 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
788 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
789 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
790 | ] |
---|
791 | | false ⇒ λHop_simplifiable_eq. |
---|
792 | let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in |
---|
793 | let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in |
---|
794 | «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» |
---|
795 | ] (refl ? (binop_simplifiable op)) |
---|
796 | | Ecast cast_ty castee ⇒ λHdesc_eq. |
---|
797 | match cast_ty return λx. x = cast_ty → ? with |
---|
798 | [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. |
---|
799 | match type_eq_dec ty cast_ty with |
---|
800 | [ inl Hcast_eq ⇒ |
---|
801 | match necessary_conditions cast_sz cast_sg target_sz target_sg |
---|
802 | return λx. x = (necessary_conditions cast_sz cast_sg target_sz target_sg) → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) |
---|
803 | with |
---|
804 | [ true ⇒ λHconditions. |
---|
805 | let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in |
---|
806 | match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) |
---|
807 | with |
---|
808 | [ true ⇒ λHdesired_eq. |
---|
809 | «〈true, castee1〉, ?» |
---|
810 | | false ⇒ λHdesired_eq. |
---|
811 | let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in |
---|
812 | match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) |
---|
813 | with |
---|
814 | [ true ⇒ λHdesired2_eq. |
---|
815 | «〈false, castee2〉, ?» |
---|
816 | | false ⇒ λHdesired2_eq. |
---|
817 | «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» |
---|
818 | ] (refl ? desired_type2) |
---|
819 | ] (refl ? desired_type) |
---|
820 | | false ⇒ λHconditions. |
---|
821 | let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in |
---|
822 | match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) |
---|
823 | with |
---|
824 | [ true ⇒ λHdesired2_eq. |
---|
825 | «〈false, castee2〉, ?» |
---|
826 | | false ⇒ λHdesired2_eq. |
---|
827 | «〈false, Expr (Ecast ty castee2) cast_ty〉, ?» |
---|
828 | ] (refl ? desired_type2) |
---|
829 | ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg)) |
---|
830 | | inr Hcast_neq ⇒ |
---|
831 | (* inconsistent types ... *) |
---|
832 | let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in |
---|
833 | «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» |
---|
834 | ] |
---|
835 | | _ ⇒ λHcast_ty_eq. |
---|
836 | let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in |
---|
837 | «〈false, Expr (Ecast cast_ty castee1) ty〉, ?» |
---|
838 | ] (refl ? cast_ty) |
---|
839 | | Econdition cond iftrue iffalse ⇒ λHdesc_eq. |
---|
840 | let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in |
---|
841 | match assert_type_eq ty (typeof iftrue) with |
---|
842 | [ OK Hty_eq_iftrue ⇒ |
---|
843 | match assert_type_eq (typeof iftrue) (typeof iffalse) with |
---|
844 | [ OK Hiftrue_eq_iffalse ⇒ |
---|
845 | let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr iftrue target_sz target_sg in |
---|
846 | let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in |
---|
847 | match desired_true ∧ desired_false |
---|
848 | return λx. (desired_true ∧ desired_false) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))) |
---|
849 | with |
---|
850 | [ true ⇒ λHdesired_eq. |
---|
851 | «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?» |
---|
852 | | false ⇒ λHdesired_eq. |
---|
853 | let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in |
---|
854 | let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in |
---|
855 | «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» |
---|
856 | ] (refl ? (desired_true ∧ desired_false)) |
---|
857 | | _ ⇒ |
---|
858 | let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in |
---|
859 | let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in |
---|
860 | «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» |
---|
861 | ] |
---|
862 | | _ ⇒ |
---|
863 | let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in |
---|
864 | let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in |
---|
865 | «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?» |
---|
866 | ] |
---|
867 | (* Could probably do better with these, too. *) |
---|
868 | | Eandbool lhs rhs ⇒ λHdesc_eq. |
---|
869 | let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in |
---|
870 | let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in |
---|
871 | «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?» |
---|
872 | | Eorbool lhs rhs ⇒ λHdesc_eq. |
---|
873 | let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in |
---|
874 | let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in |
---|
875 | «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?» |
---|
876 | (* Could also improve Esizeof *) |
---|
877 | | Efield rec_expr f ⇒ λHdesc_eq. |
---|
878 | let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in |
---|
879 | «〈false,Expr (Efield rec_expr1 f) ty〉, ?» |
---|
880 | | Ecost l e1 ⇒ λHdesc_eq. |
---|
881 | (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *) |
---|
882 | (* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *) |
---|
883 | match type_eq_dec ty (typeof e1) with |
---|
884 | [ inl Heq ⇒ |
---|
885 | let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in |
---|
886 | «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?» |
---|
887 | | inr Hneq ⇒ |
---|
888 | let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in |
---|
889 | «〈false, Expr (Ecost l e2) ty〉, ?» |
---|
890 | ] |
---|
891 | (* | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) |
---|
892 | (* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) |
---|
893 | (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact |
---|
894 | require to alter the semantics of [load_value_of_type]. *) |
---|
895 | | Evar id ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» |
---|
896 | | Esizeof t ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» |
---|
897 | ] (refl ? ed) |
---|
898 | ] (refl ? e) |
---|
899 | |
---|
900 | and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ |
---|
901 | match e return λx. x = e → ? with |
---|
902 | [ Expr ed ty ⇒ λHexpr_eq. |
---|
903 | match ed return λx. x = ed → ? with |
---|
904 | [ Ederef e1 ⇒ λHdesc_eq. |
---|
905 | let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
906 | «Expr (Ederef e2) ty, ?» |
---|
907 | | Eaddrof e1 ⇒ λHdesc_eq. |
---|
908 | let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
909 | «Expr (Eaddrof e2) ty, ?» |
---|
910 | | Eunop op e1 ⇒ λHdesc_eq. |
---|
911 | let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in |
---|
912 | «Expr (Eunop op e2) ty, ?» |
---|
913 | | Ebinop op lhs rhs ⇒ λHdesc_eq. |
---|
914 | let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in |
---|
915 | let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in |
---|
916 | «Expr (Ebinop op lhs1 rhs1) ty, ?» |
---|
917 | | Ecast cast_ty castee ⇒ λHdesc_eq. |
---|
918 | match type_eq_dec ty cast_ty with |
---|
919 | [ inl Hcast_eq ⇒ |
---|
920 | match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result |
---|
921 | with |
---|
922 | [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. |
---|
923 | let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in |
---|
924 | match success return λx. x = success → Σresult:expr. conservation e result |
---|
925 | with |
---|
926 | [ true ⇒ λHsuccess_eq. |
---|
927 | «castee1, ?» |
---|
928 | | false ⇒ λHsuccess_eq. |
---|
929 | «Expr (Ecast cast_ty castee1) ty, ?» |
---|
930 | ] (refl ? success) |
---|
931 | | _ ⇒ λHcast_ty_eq. |
---|
932 | «e, ?» |
---|
933 | ] (refl ? cast_ty) |
---|
934 | | inr Hcast_neq ⇒ |
---|
935 | «e, ?» |
---|
936 | ] |
---|
937 | | Econdition cond iftrue iffalse ⇒ λHdesc_eq. |
---|
938 | let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in |
---|
939 | let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in |
---|
940 | let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in |
---|
941 | «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?» |
---|
942 | | Eandbool lhs rhs ⇒ λHdesc_eq. |
---|
943 | let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in |
---|
944 | let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in |
---|
945 | «Expr (Eandbool lhs1 rhs1) ty, ?» |
---|
946 | | Eorbool lhs rhs ⇒ λHdesc_eq. |
---|
947 | let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in |
---|
948 | let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in |
---|
949 | «Expr (Eorbool lhs1 rhs1) ty, ?» |
---|
950 | | Efield rec_expr f ⇒ λHdesc_eq. |
---|
951 | let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in |
---|
952 | «Expr (Efield rec_expr1 f) ty, ?» |
---|
953 | | Ecost l e1 ⇒ λHdesc_eq. |
---|
954 | let «e2, Hequiv» as Eq ≝ simplify_inside e1 in |
---|
955 | «Expr (Ecost l e2) ty, ?» |
---|
956 | | _ ⇒ λHdesc_eq. |
---|
957 | «e, ?» |
---|
958 | ] (refl ? ed) |
---|
959 | ] (refl ? e). |
---|
960 | #ge #en #m |
---|
961 | [ 1,3,5,6,7,8,9,10,11: %1 try @refl |
---|
962 | cases (exec_expr ge en m e) #res |
---|
963 | try (@(SimOk ???) //) |
---|
964 | | 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/ |
---|
965 | (* |
---|
966 | whd in match (exec_expr ????); >eq_intsize_identity whd |
---|
967 | >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ] |
---|
968 | *) |
---|
969 | | 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/ |
---|
970 | whd in match (exec_expr ????); |
---|
971 | whd in match (exec_expr ????); |
---|
972 | >eq_intsize_identity >eq_intsize_identity whd |
---|
973 | #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj // |
---|
974 | [ 1: @(simplify_int_implements_cast … Hsimpl_eq) |
---|
975 | | 2: @(simplify_int_success_lt … Hsimpl_eq) ] |
---|
976 | (*| 14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res |
---|
977 | try (@(SimOk ???) //) *) |
---|
978 | | 12: elim (type_eq_dec ty (Tint target_sz target_sg)) |
---|
979 | [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg) |
---|
980 | destruct |
---|
981 | [ 1,2: // |
---|
982 | | 3: @smaller_integer_val_identity ] |
---|
983 | | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct |
---|
984 | @(SimOk ???) // |
---|
985 | ] |
---|
986 | | 13: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq |
---|
987 | [ 1: (* Proving preservation of the semantics for expressions. *) |
---|
988 | cases Hexpr_sim |
---|
989 | [ 2: (* Case where the evaluation of e1 as an expression fails *) |
---|
990 | normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely |
---|
991 | | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) |
---|
992 | #Hsim %1 * #val #trace normalize #Hstep |
---|
993 | cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ |
---|
994 | (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val)) |
---|
995 | [ 1: lapply Hstep -Hstep |
---|
996 | cases (exec_expr ge en m e1) |
---|
997 | [ 1: * #val' #trace' normalize nodelta |
---|
998 | cases val' normalize nodelta |
---|
999 | [ 1,2,3: #H1 destruct #H2 destruct #H3 destruct |
---|
1000 | | 4: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) |
---|
1001 | cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq; |
---|
1002 | normalize nodelta |
---|
1003 | [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ] |
---|
1004 | ] |
---|
1005 | | 2: normalize nodelta #errmesg #Hcontr destruct |
---|
1006 | ] |
---|
1007 | | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr |
---|
1008 | cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) |
---|
1009 | ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val)) |
---|
1010 | [ 1: @(ex_intro … e1_ptr) @conj |
---|
1011 | [ 1: @Hsim // | 2: // ] |
---|
1012 | | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr |
---|
1013 | normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl |
---|
1014 | ] |
---|
1015 | ] |
---|
1016 | ] |
---|
1017 | | 2: (* Proving the preservation of the semantics for lvalues. *) |
---|
1018 | cases Hexpr_sim |
---|
1019 | [ 2: (* Case where the evaluation of e1 as an lvalue fails *) |
---|
1020 | normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely |
---|
1021 | | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) |
---|
1022 | #Hsim %1 * * #block #offset #trace normalize #Hstep |
---|
1023 | cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset) |
---|
1024 | [ 1: lapply Hstep -Hstep |
---|
1025 | cases (exec_expr ge en m e1) |
---|
1026 | [ 1: * #val' #trace' normalize nodelta |
---|
1027 | cases val' normalize nodelta |
---|
1028 | [ 1,2,3: #H1 destruct #H2 destruct #H3 destruct |
---|
1029 | | 4: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) |
---|
1030 | destruct try @conj try @conj // |
---|
1031 | ] |
---|
1032 | | 2: normalize nodelta #errmesg #Hcontr destruct |
---|
1033 | ] |
---|
1034 | | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset |
---|
1035 | cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) ∧ pblock ptr1 = block ∧ poff ptr1 = offset) |
---|
1036 | [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim // |
---|
1037 | | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset |
---|
1038 | normalize >He2_exec normalize nodelta // |
---|
1039 | ] |
---|
1040 | ] |
---|
1041 | ] |
---|
1042 | ] |
---|
1043 | | 14: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq |
---|
1044 | [ 1: (* Proving preservation of the semantics for expressions. *) |
---|
1045 | cases Hlvalue_sim |
---|
1046 | [ 2: (* Case where the evaluation of e1 as an expression fails *) |
---|
1047 | * #err #Hfail whd in match (exec_expr ????); >Hfail @SimFailNicely |
---|
1048 | | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) |
---|
1049 | #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep |
---|
1050 | cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧ |
---|
1051 | (ty = Tpointer ptype) ∧ |
---|
1052 | val = Vptr (mk_pointer block offset)) |
---|
1053 | [ 1: lapply Hstep -Hstep |
---|
1054 | cases (exec_lvalue ge en m e1) |
---|
1055 | [ 1: * * #block #offset #trace' normalize nodelta |
---|
1056 | cases ty |
---|
1057 | [ 2: #sz #sg | 3: #ptr_ty | 4: #array_ty #array_sz | 5: #domain #codomain |
---|
1058 | | 6: #structname #fieldspec | 7: #unionname #fieldspec | 8: #id ] |
---|
1059 | normalize nodelta try (#Heq destruct) |
---|
1060 | @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty) |
---|
1061 | try @conj try @conj destruct // |
---|
1062 | | 2: normalize nodelta #errmesg #Hcontr destruct |
---|
1063 | ] |
---|
1064 | | 2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq |
---|
1065 | whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta |
---|
1066 | // |
---|
1067 | ] |
---|
1068 | ] |
---|
1069 | | 2: (* Proving preservation of the semantics of lvalues. *) |
---|
1070 | @SimFailNicely |
---|
1071 | ] |
---|
1072 | | 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq |
---|
1073 | [ 1: whd in match (exec_expr ge en m (Expr ??)); |
---|
1074 | whd in match (exec_expr ge en m (Expr ??)); |
---|
1075 | cases Hexpr_sim |
---|
1076 | [ 2: * #error #Hexec >Hexec normalize nodelta @SimFailNicely |
---|
1077 | | 1: cases (exec_expr ge en m e1) |
---|
1078 | [ 2: #error #Hexec normalize nodelta @SimFailNicely |
---|
1079 | | 1: * #val #trace #Hexec |
---|
1080 | >(Hexec ? (refl ? (OK ? 〈val,trace〉))) |
---|
1081 | normalize nodelta @SimOk #a >Htype_eq #H @H |
---|
1082 | ] |
---|
1083 | ] |
---|
1084 | | 2: @SimFailNicely |
---|
1085 | ] |
---|
1086 | | 16: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq |
---|
1087 | inversion (Hinv_lhs ge en m) |
---|
1088 | [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true |
---|
1089 | #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct |
---|
1090 | | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_ |
---|
1091 | inversion (Hinv_rhs ge en m) |
---|
1092 | [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_ |
---|
1093 | <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct |
---|
1094 | | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_ |
---|
1095 | @(Inv_coerce_ok ge en m … target_sz target_sg lhs_src_sz lhs_src_sg) |
---|
1096 | [ 1: >Htype_lhs // |
---|
1097 | | 2: // |
---|
1098 | | 3: whd in match (exec_expr ??? (Expr ??)); |
---|
1099 | whd in match (exec_expr ??? (Expr ??)); |
---|
1100 | (* Tidy up the type equations *) |
---|
1101 | >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct |
---|
1102 | lapply Hsmaller_rhs lapply Hsmaller_lhs |
---|
1103 | generalize in match rhs_src_sz; #src_sz |
---|
1104 | generalize in match rhs_src_sg; #src_sg |
---|
1105 | -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs |
---|
1106 | >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1 |
---|
1107 | (* Enumerate all the cases for the evaluation of the source expressions ... *) |
---|
1108 | cases (exec_expr ge en m lhs); |
---|
1109 | try // * #val_lhs #trace_lhs normalize nodelta |
---|
1110 | cases (exec_expr ge en m rhs); |
---|
1111 | try // * #val_rhs #trace_rhs normalize nodelta |
---|
1112 | whd in match (m_bind ?????); |
---|
1113 | (* specialize to the actual simplifiable operations. *) |
---|
1114 | cases op in Hop_simplifiable_eq; |
---|
1115 | [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ |
---|
1116 | [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m) |
---|
1117 | | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ] |
---|
1118 | cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m) |
---|
1119 | [ 1,3: #_ #_ #_ normalize @I ] |
---|
1120 | #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result))) |
---|
1121 | #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq |
---|
1122 | whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta |
---|
1123 | >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs |
---|
1124 | whd |
---|
1125 | #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq |
---|
1126 | lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq |
---|
1127 | cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq |
---|
1128 | lapply Hsmaller_lhs lapply Hsmaller_rhs |
---|
1129 | cases (exec_expr ge en m lhs1) normalize nodelta |
---|
1130 | [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ] |
---|
1131 | * #val_lhs1 #trace_lhs1 |
---|
1132 | cases (exec_expr ge en m rhs1) |
---|
1133 | [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ] |
---|
1134 | * #val_rhs1 #trace_rhs1 |
---|
1135 | whd in match (m_bind ?????); normalize nodelta |
---|
1136 | [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) |
---|
1137 | lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) |
---|
1138 | | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m) |
---|
1139 | lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ] |
---|
1140 | cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m) |
---|
1141 | [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?))) |
---|
1142 | (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *) |
---|
1143 | * |
---|
1144 | [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta |
---|
1145 | #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1))) |
---|
1146 | #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd |
---|
1147 | @(False_ind … (Habsurd I)) |
---|
1148 | | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta |
---|
1149 | #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2))) |
---|
1150 | #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd |
---|
1151 | @(False_ind … (Habsurd I)) |
---|
1152 | | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq |
---|
1153 | whd in ⊢ (% → % → ?); normalize nodelta |
---|
1154 | #Hsmaller_lhs #Hsmaller_rhs |
---|
1155 | elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) |
---|
1156 | #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le |
---|
1157 | elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) |
---|
1158 | #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ |
---|
1159 | destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz)) |
---|
1160 | ] |
---|
1161 | | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta |
---|
1162 | elim (Hinversion result (refl ? (Some ? result))) |
---|
1163 | #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq |
---|
1164 | elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) |
---|
1165 | #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le |
---|
1166 | elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2))) |
---|
1167 | #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_ |
---|
1168 | destruct |
---|
1169 | [ 1: %{(addition_n (bitsize_of_intsize target_sz) |
---|
1170 | (cast_int_int src_sz src_sg target_sz i1) |
---|
1171 | (cast_int_int src_sz src_sg target_sz i2))} |
---|
1172 | try @conj try @conj try @conj // |
---|
1173 | >integer_add_cast_le try // |
---|
1174 | | 2: %{(subtraction (bitsize_of_intsize target_sz) |
---|
1175 | (cast_int_int src_sz src_sg target_sz i1) |
---|
1176 | (cast_int_int src_sz src_sg target_sz i2))} |
---|
1177 | try @conj try @conj try @conj // |
---|
1178 | >integer_sub_cast_le try // |
---|
1179 | ] |
---|
1180 | ] ] ] ] |
---|
1181 | | 17,18,19,20: destruct %1 try @refl |
---|
1182 | elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs |
---|
1183 | elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs |
---|
1184 | [ 1,3,5,7: |
---|
1185 | whd in match (exec_expr ????); whd in match (exec_expr ????); |
---|
1186 | cases Hexpr_sim_lhs |
---|
1187 | [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely |
---|
1188 | | *: cases (exec_expr ge en m lhs) |
---|
1189 | [ 2,4,6,8: #error #_ @SimFailNicely |
---|
1190 | | *: * #lval #ltrace #Hsim_lhs normalize nodelta |
---|
1191 | cases Hexpr_sim_rhs |
---|
1192 | [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely |
---|
1193 | | *: cases (exec_expr ge en m rhs) |
---|
1194 | [ 2,4,6,8: #error #_ @SimFailNicely |
---|
1195 | | *: * #rval #rtrace #Hsim_rhs |
---|
1196 | whd in match (exec_expr ??? (Expr (Ebinop ???) ?)); |
---|
1197 | >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉))) |
---|
1198 | >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉))) |
---|
1199 | normalize nodelta |
---|
1200 | >Htype_eq_lhs >Htype_eq_rhs |
---|
1201 | @SimOk * #val #trace #H @H |
---|
1202 | ] |
---|
1203 | ] |
---|
1204 | ] |
---|
1205 | ] |
---|
1206 | | *: @SimFailNicely |
---|
1207 | ] |
---|
1208 | (* Jump to the cast cases *) |
---|
1209 | (*| 21,30,31,32,33,34,35,36: *) |
---|
1210 | | 21,27,28,29,30,31,32,33: |
---|
1211 | %1 try @refl |
---|
1212 | [ 1,4,7,10,13,16,19,22: destruct // ] |
---|
1213 | elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq |
---|
1214 | (* exec_expr simulation *) |
---|
1215 | [ 1,3,5,7,9,11,13,15: cases Hexec_sim |
---|
1216 | [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail whd in match (exec_expr ge en m ?); |
---|
1217 | >Hexec_fail @SimFailNicely |
---|
1218 | | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq |
---|
1219 | whd in match (exec_expr ge en m ?); #Hstep |
---|
1220 | cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉 |
---|
1221 | ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val) |
---|
1222 | [ 1,3,5,7,9,11,13,15: |
---|
1223 | lapply Hstep -Hstep cases (exec_expr ge en m castee) |
---|
1224 | [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct |
---|
1225 | | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta |
---|
1226 | #Hstep @(ex_intro … val1) |
---|
1227 | cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep; |
---|
1228 | [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct |
---|
1229 | | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct |
---|
1230 | @conj @refl |
---|
1231 | ] |
---|
1232 | ] |
---|
1233 | | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast |
---|
1234 | whd in match (exec_expr ge en m ?); |
---|
1235 | >(Hsim … Hexec_expr ) normalize nodelta |
---|
1236 | <Htype_eq >Hexec_cast // |
---|
1237 | ] |
---|
1238 | ] |
---|
1239 | | 2,4,6,8,10,12,14,16: destruct @SimFailNicely |
---|
1240 | ] |
---|
1241 | | 22: destruct inversion (Hcastee_inv ge en m) |
---|
1242 | [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 |
---|
1243 | <Hresult_flag_2 in Hresult_flag; #Hcontr destruct |
---|
1244 | | 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq |
---|
1245 | @(Inv_coerce_ok ??????? cast_sz cast_sg) |
---|
1246 | [ 1: // | 2: <Htype_castee1 // |
---|
1247 | | 3: whd in match (exec_expr ??? (Expr ??)); |
---|
1248 | >Htype_castee |
---|
1249 | (* Simplify the goal by culling impossible cases, using Hsmaller_val *) |
---|
1250 | cases (exec_expr ge en m castee) in Hsmaller_eval; |
---|
1251 | [ 2: #error // |
---|
1252 | | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta |
---|
1253 | lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m) |
---|
1254 | cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) |
---|
1255 | [ 2: #error #_ @I |
---|
1256 | | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result))) |
---|
1257 | #castee_int * #Hcastee_val_eq #Hresult_eq |
---|
1258 | whd in match (m_bind ?????); |
---|
1259 | #result_int #Hresult_eq2 |
---|
1260 | cases (exec_expr ge en m castee1) in Hsmaller; |
---|
1261 | [ 2: #error normalize in ⊢ (% → ?); #Habsurd |
---|
1262 | @(False_ind … (Habsurd castee_int Hcastee_val_eq)) |
---|
1263 | | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta |
---|
1264 | #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq) |
---|
1265 | #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq |
---|
1266 | destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)} |
---|
1267 | try @conj try @conj try @conj try // |
---|
1268 | [ 1: @cast_composition ] try assumption |
---|
1269 | elim (necessary_conditions_spec … (sym_eq … Hconditions)) |
---|
1270 | [ 2,4: * #Heq >Heq #_ elim target_sz // |
---|
1271 | | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ] |
---|
1272 | ] ] ] ] ] |
---|
1273 | | 23,25: destruct |
---|
1274 | inversion (Hcast2 ge en m) |
---|
1275 | [ 1,3: (* Impossible case. *) |
---|
1276 | #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult; |
---|
1277 | #Hcontr destruct |
---|
1278 | | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself. |
---|
1279 | We did not successfuly cast the subexpression to target_sz, though. *) |
---|
1280 | #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq |
---|
1281 | @(Inv_eq ???????) // |
---|
1282 | [ 1,3: >Htype_castee2 // |
---|
1283 | | 2,4: (* Prove simulation for exec_expr *) |
---|
1284 | whd in match (exec_expr ??? (Expr ??)); |
---|
1285 | cases (exec_expr ge en m castee) in Hsmaller_eval; |
---|
1286 | [ 2,4: (* erroneous evaluation of the original expression *) |
---|
1287 | #error #Hsmaller_eval @SimFailNicely |
---|
1288 | | 1,3: * #val #trace normalize nodelta >Htype_castee |
---|
1289 | lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) |
---|
1290 | cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg)) |
---|
1291 | [ 2,4: #error #_ #_ @SimFailNicely |
---|
1292 | | 1,3: #result #Hinversion elim (Hinversion result (refl ??)) |
---|
1293 | #val_int * #Hval_eq #Hresult_eq |
---|
1294 | cases (exec_expr ge en m castee2) |
---|
1295 | [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq)) |
---|
1296 | | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) |
---|
1297 | #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle |
---|
1298 | destruct @SimOk normalize #a #H @H ] |
---|
1299 | ] ] |
---|
1300 | ] ] |
---|
1301 | | 24,26: destruct |
---|
1302 | inversion (Hcast2 ge en m) |
---|
1303 | [ 2,4: (* Impossible case. *) |
---|
1304 | #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq |
---|
1305 | (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *) |
---|
1306 | letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq |
---|
1307 | -Habsurd_eq -Habsurd #Habsurd destruct |
---|
1308 | | 1,3: (* All our attempts at casting down the expression have failed. We still use the |
---|
1309 | resulting expression, as we may have discovered and simplified unrelated casts. *) |
---|
1310 | #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv |
---|
1311 | @(Inv_eq ???????) // |
---|
1312 | whd in match (exec_expr ??? (Expr ??)); |
---|
1313 | whd in match (exec_expr ??? (Expr ??)); |
---|
1314 | cases Hsim_expr |
---|
1315 | [ 2,4: * #error #Hexec_err >Hexec_err @SimFailNicely |
---|
1316 | | 1,3: #Hexec_ok |
---|
1317 | cases (exec_expr ge en m castee) in Hexec_ok; |
---|
1318 | [ 2,4: #error #Hsim @SimFailNicely |
---|
1319 | | 1,3: * #val #trace #Hsim normalize nodelta |
---|
1320 | >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta |
---|
1321 | @SimOk #a #H @H |
---|
1322 | ] |
---|
1323 | ] |
---|
1324 | ] |
---|
1325 | (* |
---|
1326 | | 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1327 | @(Inv_eq ???????) // |
---|
1328 | whd in match (exec_expr ??? (Expr ??)); |
---|
1329 | whd in match (exec_expr ??? (Expr ??)); |
---|
1330 | cases Hsim_expr |
---|
1331 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1332 | | 1: #Hexec_ok @SimOk * #val #trace |
---|
1333 | cases (exec_expr ge en m castee) in Hexec_ok; |
---|
1334 | [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct |
---|
1335 | | 1: * #val #trace #Hexec_ok normalize nodelta |
---|
1336 | >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) |
---|
1337 | >Htype_eq |
---|
1338 | normalize nodelta #H @H |
---|
1339 | ] |
---|
1340 | ] *) |
---|
1341 | | 34: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq |
---|
1342 | inversion (Htrue_inv ge en m) |
---|
1343 | [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false |
---|
1344 | #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct |
---|
1345 | | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true |
---|
1346 | inversion (Hfalse_inv ge en m) |
---|
1347 | [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false |
---|
1348 | #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct |
---|
1349 | | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false |
---|
1350 | >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg) |
---|
1351 | [ 1,2: // |
---|
1352 | | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??)); |
---|
1353 | elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq |
---|
1354 | cases Hexec_cond_sim |
---|
1355 | [ 2: * #error #Herror >Herror normalize @I |
---|
1356 | | 1: cases (exec_expr ge en m cond) |
---|
1357 | [ 2: #error #_ normalize @I |
---|
1358 | | 1: * #cond_val #cond_trace #Hcond_sim |
---|
1359 | >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) |
---|
1360 | normalize nodelta |
---|
1361 | >Htype_cond_eq |
---|
1362 | cases (exec_bool_of_val cond_val (typeof cond1)) * |
---|
1363 | [ 3,4: normalize // |
---|
1364 | | 1,2: normalize in match (m_bind ?????); |
---|
1365 | normalize in match (m_bind ?????); |
---|
1366 | -Hexec_cond_sim -Hcond_sim -cond_val |
---|
1367 | [ 1: (* true branch taken *) |
---|
1368 | cases (exec_expr ge en m iftrue) in Hsmaller_true; |
---|
1369 | [ 2: #error #_ @I |
---|
1370 | | 1: * #val_true_branch #trace_true_branch #Hsmaller |
---|
1371 | #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller |
---|
1372 | cases (exec_expr ge en m iftrue1) |
---|
1373 | [ 2: #error normalize in ⊢ (% → ?); #Hsmaller |
---|
1374 | @(False_ind … (Hsmaller val_true_branch Hval_true_branch)) |
---|
1375 | | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta |
---|
1376 | elim (Hsmaller val_true_branch Hval_true_branch) |
---|
1377 | #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle |
---|
1378 | %{val_true1_int} try @conj try @conj try @conj // |
---|
1379 | ] ] |
---|
1380 | | 2: (* false branch taken. Same proof as above, different arguments ... *) |
---|
1381 | cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg) |
---|
1382 | [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq |
---|
1383 | destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct |
---|
1384 | cases (exec_expr ge en m iffalse) in Hsmaller_false; |
---|
1385 | [ 2: #error #_ @I |
---|
1386 | | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller |
---|
1387 | #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller |
---|
1388 | cases (exec_expr ge en m iffalse1) |
---|
1389 | [ 2: #error normalize in ⊢ (% → ?); #Hsmaller |
---|
1390 | @(False_ind … (Hsmaller val_false_branch Hval_false_branch)) |
---|
1391 | | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta |
---|
1392 | elim (Hsmaller val_false_branch Hval_false_branch) |
---|
1393 | #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle |
---|
1394 | %{val_false1_int} try @conj try @conj try @conj // |
---|
1395 | ] ] |
---|
1396 | ] ] ] ] ] ] ] |
---|
1397 | | 35,36,37: destruct |
---|
1398 | elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq |
---|
1399 | elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq |
---|
1400 | elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq |
---|
1401 | %1 try @refl |
---|
1402 | [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
1403 | cases (exec_expr ge en m cond) in Hsim_expr_cond; |
---|
1404 | [ 2,4,6: #error #_ @SimFailNicely |
---|
1405 | | 1,3,5: * #cond_val #cond_trace normalize nodelta |
---|
1406 | cases (exec_expr ge en m cond1) |
---|
1407 | [ 2,4,6: #error * |
---|
1408 | [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) |
---|
1409 | #Habsurd destruct |
---|
1410 | | *: * #error #Habsurd destruct ] |
---|
1411 | | 1,3,5: * #cond_val1 #cond_trace1 * |
---|
1412 | [ 2,4,6: * #error #Habsurd destruct |
---|
1413 | | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) |
---|
1414 | #Hcond_eq normalize nodelta destruct (Hcond_eq) |
---|
1415 | >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1)) |
---|
1416 | [ 2,4,6: #error @SimFailNicely |
---|
1417 | | 1,3,5: * (* true branch *) |
---|
1418 | [ 1,3,5: |
---|
1419 | normalize in match (m_bind ?????); |
---|
1420 | normalize in match (m_bind ?????); |
---|
1421 | cases Hsim_expr_true |
---|
1422 | [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1423 | | 1,3,5: cases (exec_expr ge en m iftrue) |
---|
1424 | [ 2,4,6: #error #_ normalize nodelta @SimFailNicely |
---|
1425 | | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim |
---|
1426 | >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉))) |
---|
1427 | normalize nodelta @SimOk #a #H @H |
---|
1428 | ] |
---|
1429 | ] |
---|
1430 | | 2,4,6: |
---|
1431 | normalize in match (m_bind ?????); |
---|
1432 | normalize in match (m_bind ?????); |
---|
1433 | cases Hsim_expr_false |
---|
1434 | [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely |
---|
1435 | | 1,3,5: cases (exec_expr ge en m iffalse) |
---|
1436 | [ 2,4,6: #error #_ normalize nodelta @SimFailNicely |
---|
1437 | | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim |
---|
1438 | >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉))) |
---|
1439 | normalize nodelta @SimOk #a #H @H |
---|
1440 | ] |
---|
1441 | ] |
---|
1442 | ] |
---|
1443 | ] |
---|
1444 | ] |
---|
1445 | ] |
---|
1446 | ] |
---|
1447 | | 2,4,6: @SimFailNicely |
---|
1448 | ] |
---|
1449 | | 38,39: destruct |
---|
1450 | elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs |
---|
1451 | elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs |
---|
1452 | %1 try @refl |
---|
1453 | [ 1,3: whd in match (exec_expr ??? (Expr ??)); |
---|
1454 | whd in match (exec_expr ??? (Expr ??)); |
---|
1455 | cases Hsim_expr_lhs |
---|
1456 | [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely |
---|
1457 | | 1,3: cases (exec_expr ge en m lhs) |
---|
1458 | [ 2,4: #error #_ @SimFailNicely |
---|
1459 | | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta |
---|
1460 | >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉))) |
---|
1461 | normalize nodelta >Htype_eq_lhs |
---|
1462 | cases (exec_bool_of_val lhs_val (typeof lhs1)) |
---|
1463 | [ 2,4: #error normalize @SimFailNicely |
---|
1464 | | 1,3: * |
---|
1465 | whd in match (m_bind ?????); |
---|
1466 | whd in match (m_bind ?????); |
---|
1467 | [ 2,3: (* lhs evaluates to true *) |
---|
1468 | @SimOk #a #H @H |
---|
1469 | | 1,4: cases Hsim_expr_rhs |
---|
1470 | [ 2,4: * #error #Hexec >Hexec @SimFailNicely |
---|
1471 | | 1,3: cases (exec_expr ge en m rhs) |
---|
1472 | [ 2,4: #error #_ @SimFailNicely |
---|
1473 | | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim |
---|
1474 | >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉))) |
---|
1475 | normalize nodelta >Htype_eq_rhs |
---|
1476 | @SimOk #a #H @H |
---|
1477 | ] |
---|
1478 | ] |
---|
1479 | ] |
---|
1480 | ] |
---|
1481 | ] |
---|
1482 | ] |
---|
1483 | | 2,4: @SimFailNicely |
---|
1484 | ] |
---|
1485 | | 40: destruct |
---|
1486 | cases (type_eq_dec ty (Tint target_sz target_sg)) |
---|
1487 | [ 1: #Htype_eq >Htype_eq >type_eq_identity |
---|
1488 | @(Inv_coerce_ok ??????? target_sz target_sg) |
---|
1489 | [ 1,2: // |
---|
1490 | | 3: @smaller_integer_val_identity ] |
---|
1491 | | 2: #Hneq >(type_neq_not_identity … Hneq) |
---|
1492 | %1 // @SimOk #a #H @H |
---|
1493 | ] |
---|
1494 | | 41: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1495 | %1 try @refl |
---|
1496 | [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
1497 | whd in match (exec_lvalue ????) in Hsim_lvalue; |
---|
1498 | whd in match (exec_lvalue' ?????); |
---|
1499 | whd in match (exec_lvalue' ?????); |
---|
1500 | >Htype_eq |
---|
1501 | cases (typeof rec_expr1) normalize nodelta |
---|
1502 | [ 2: #sz #sg | 3: #ty | 4: #ty #n | 5: #tl #ty | 6: #id #fl | 7: #id #fl | 8: #ty ] |
---|
1503 | [ 1,2,3,4,7,8: @SimFailNicely |
---|
1504 | | 5,6: cases Hsim_lvalue |
---|
1505 | [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely |
---|
1506 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
1507 | [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely |
---|
1508 | | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) |
---|
1509 | whd in match (m_bind ?????); |
---|
1510 | @SimOk #a #H @H |
---|
1511 | ] |
---|
1512 | ] |
---|
1513 | ] |
---|
1514 | | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??)); |
---|
1515 | >Htype_eq |
---|
1516 | cases (typeof rec_expr1) normalize nodelta |
---|
1517 | [ 2: #sz #sg | 3: #ty | 4: #ty #n | 5: #tl #ty | 6: #id #fl | 7: #id #fl | 8: #ty ] |
---|
1518 | [ 1,2,3,4,7,8: @SimFailNicely |
---|
1519 | | 5,6: cases Hsim_lvalue |
---|
1520 | [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely |
---|
1521 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
1522 | [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely |
---|
1523 | | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a))) |
---|
1524 | whd in match (m_bind ?????); |
---|
1525 | @SimOk #a #H @H |
---|
1526 | ] |
---|
1527 | ] |
---|
1528 | ] |
---|
1529 | ] |
---|
1530 | | 42: destruct |
---|
1531 | inversion (Hinv ge en m) |
---|
1532 | [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_ |
---|
1533 | @(Inv_coerce_ok ??????? src_sz src_sg) |
---|
1534 | [ 1: >Htypeof_e1 // |
---|
1535 | | 2: >Htypeof_e2 // |
---|
1536 | | 3: whd in match (exec_expr ??? (Expr ??)); |
---|
1537 | whd in match (exec_expr ??? (Expr ??)); |
---|
1538 | cases (exec_expr ge en m e1) in Hsmaller; |
---|
1539 | [ 2: #error normalize // |
---|
1540 | | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq |
---|
1541 | cases (exec_expr ge en m e2) in Hsmaller; |
---|
1542 | [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq)) |
---|
1543 | | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq) |
---|
1544 | #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta |
---|
1545 | %{val2_int} try @conj try @conj try @conj // |
---|
1546 | ] |
---|
1547 | ] |
---|
1548 | ] |
---|
1549 | | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_ |
---|
1550 | >Hresult %1 try @refl |
---|
1551 | [ 1: >Htype_eq // |
---|
1552 | | 2: whd in match (exec_expr ??? (Expr ??)); |
---|
1553 | whd in match (exec_expr ??? (Expr ??)); |
---|
1554 | cases Hsim_expr |
---|
1555 | [ 2: * #error #Hexec_error >Hexec_error @SimFailNicely |
---|
1556 | | 1: cases (exec_expr ge en m e1) |
---|
1557 | [ 2: #error #_ @SimFailNicely |
---|
1558 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec |
---|
1559 | @SimOk #a #H @H |
---|
1560 | ] |
---|
1561 | ] |
---|
1562 | | 3: @SimFailNicely |
---|
1563 | ] |
---|
1564 | ] |
---|
1565 | | 43: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1566 | %1 try @refl |
---|
1567 | [ 1: whd in match (exec_expr ??? (Expr ??)); |
---|
1568 | whd in match (exec_expr ??? (Expr ??)); |
---|
1569 | cases Hsim_expr |
---|
1570 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1571 | | 1: cases (exec_expr ge en m e1) |
---|
1572 | [ 2: #error #_ @SimFailNicely |
---|
1573 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ] |
---|
1574 | ] |
---|
1575 | | 2: @SimFail /2 by ex_intro/ ] |
---|
1576 | (* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls |
---|
1577 | * simplify_expr *) |
---|
1578 | | 44, 45: (* trivial const_int, const_float and var cases *) |
---|
1579 | try @conj try @conj try @refl |
---|
1580 | @SimOk #a #H @H |
---|
1581 | | 46: (* Deref case *) destruct |
---|
1582 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1583 | try @conj try @conj |
---|
1584 | [ 1: |
---|
1585 | whd in match (exec_expr ??? (Expr ??)); |
---|
1586 | whd in match (exec_expr ??? (Expr ??)); |
---|
1587 | whd in match (exec_lvalue' ?????); |
---|
1588 | whd in match (exec_lvalue' ?????); |
---|
1589 | | 2: |
---|
1590 | whd in match (exec_lvalue ??? (Expr ??)); |
---|
1591 | whd in match (exec_lvalue ??? (Expr ??)); |
---|
1592 | ] |
---|
1593 | [ 1,2: |
---|
1594 | cases Hsim_expr |
---|
1595 | [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1596 | | 1,3: cases (exec_expr ge en m e1) |
---|
1597 | [ 2,4: #error #_ @SimFailNicely |
---|
1598 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] |
---|
1599 | | 3: // ] |
---|
1600 | | 47: (* Addrof *) destruct |
---|
1601 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1602 | try @conj try @conj |
---|
1603 | [ 1: |
---|
1604 | whd in match (exec_expr ??? (Expr ??)); |
---|
1605 | whd in match (exec_expr ??? (Expr ??)); |
---|
1606 | cases Hsim_lvalue |
---|
1607 | [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely |
---|
1608 | | 1: cases (exec_lvalue ge en m e1) |
---|
1609 | [ 2: #error #_ @SimFailNicely |
---|
1610 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] |
---|
1611 | | 2: @SimFailNicely |
---|
1612 | | 3: // ] |
---|
1613 | | 48: (* Unop *) destruct |
---|
1614 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1615 | try @conj try @conj |
---|
1616 | [ 1: |
---|
1617 | whd in match (exec_expr ??? (Expr ??)); |
---|
1618 | whd in match (exec_expr ??? (Expr ??)); |
---|
1619 | cases Hsim_expr |
---|
1620 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1621 | | 1: cases (exec_expr ge en m e1) |
---|
1622 | [ 2: #error #_ @SimFailNicely |
---|
1623 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk |
---|
1624 | >Htype_eq #a #H @H ] ] |
---|
1625 | | 2: @SimFailNicely |
---|
1626 | | 3: // ] |
---|
1627 | | 49: (* Binop *) destruct |
---|
1628 | elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs |
---|
1629 | elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs |
---|
1630 | try @conj try @conj |
---|
1631 | [ 1: |
---|
1632 | whd in match (exec_expr ??? (Expr ??)); |
---|
1633 | whd in match (exec_expr ??? (Expr ??)); |
---|
1634 | cases Hsim_expr_lhs |
---|
1635 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1636 | | 1: cases (exec_expr ge en m lhs) |
---|
1637 | [ 2: #error #_ @SimFailNicely |
---|
1638 | | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs |
---|
1639 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1640 | | 1: cases (exec_expr ge en m rhs) |
---|
1641 | [ 2: #error #_ @SimFailNicely |
---|
1642 | | 1: #rhs_value #Hsim_rhs |
---|
1643 | lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value))) |
---|
1644 | lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value))) |
---|
1645 | #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs |
---|
1646 | @SimOk #a #H @H |
---|
1647 | ] |
---|
1648 | ] |
---|
1649 | ] |
---|
1650 | ] |
---|
1651 | | 2: @SimFailNicely |
---|
1652 | | 3: // |
---|
1653 | ] |
---|
1654 | | 50: (* Cast, fallback case *) |
---|
1655 | try @conj try @conj try @refl |
---|
1656 | @SimOk #a #H @H |
---|
1657 | | 51: (* Cast, success case *) destruct |
---|
1658 | inversion (Htrans_inv ge en m) |
---|
1659 | [ 1: (* contradiction *) |
---|
1660 | #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true |
---|
1661 | <Hresult_flag_true in Hresult_flag; #Habsurd destruct |
---|
1662 | | 2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_ |
---|
1663 | try @conj try @conj try @conj |
---|
1664 | [ 1: whd in match (exec_expr ??? (Expr ??)); |
---|
1665 | cases (exec_expr ge en m castee) in Hsmaller; |
---|
1666 | [ 2: #error #_ @SimFailNicely |
---|
1667 | | 1: * #val #trace normalize nodelta >Hsrc_type_eq |
---|
1668 | lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m) |
---|
1669 | cases (exec_cast m val ??) |
---|
1670 | [ 2: #error #_ #_ @SimFailNicely |
---|
1671 | | 1: #result #Hinversion elim (Hinversion result (refl ??)) |
---|
1672 | #val_int * #Hval_eq #Hcast |
---|
1673 | cases (exec_expr ge en m castee1) |
---|
1674 | [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq)) |
---|
1675 | | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq) |
---|
1676 | #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle |
---|
1677 | @SimOk destruct normalize // ] |
---|
1678 | ] |
---|
1679 | ] |
---|
1680 | | 2: @SimFailNicely |
---|
1681 | | 3: >Htarget_type_eq // |
---|
1682 | ] |
---|
1683 | ] |
---|
1684 | | 52: (* Cast, "failure" case *) destruct |
---|
1685 | inversion (Htrans_inv ge en m) |
---|
1686 | [ 2: (* contradiction *) |
---|
1687 | #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd |
---|
1688 | lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct |
---|
1689 | | 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_ |
---|
1690 | try @conj try @conj try @conj |
---|
1691 | [ 1: whd in match (exec_expr ????); |
---|
1692 | whd in match (exec_expr ??? (Expr ??)); |
---|
1693 | cases Hsim_expr |
---|
1694 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1695 | | 1: cases (exec_expr ??? castee) |
---|
1696 | [ 2: #error #_ @SimFailNicely |
---|
1697 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok |
---|
1698 | @SimOk >Htype_eq #a #H @H ] |
---|
1699 | ] |
---|
1700 | | 2: @SimFailNicely |
---|
1701 | | 3: // |
---|
1702 | ] |
---|
1703 | ] |
---|
1704 | | 53,54,55,56,57,58,59,63: |
---|
1705 | try @conj try @conj try @refl |
---|
1706 | @SimOk #a #H @H |
---|
1707 | | 60: destruct |
---|
1708 | elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond |
---|
1709 | elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true |
---|
1710 | elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false |
---|
1711 | try @conj try @conj |
---|
1712 | [ 1: whd in match (exec_expr ??? (Expr ??)); |
---|
1713 | whd in match (exec_expr ??? (Expr ??)); |
---|
1714 | cases Hsim_exec_cond |
---|
1715 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1716 | | 1: cases (exec_expr ??? cond) |
---|
1717 | [ 2: #error #_ @SimFailNicely |
---|
1718 | | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉))) |
---|
1719 | #Hcond_ok >Hcond_ok >Htype_eq_cond |
---|
1720 | normalize nodelta |
---|
1721 | cases (exec_bool_of_val condb (typeof cond1)) |
---|
1722 | [ 2: #error @SimFailNicely |
---|
1723 | | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
1724 | normalize nodelta |
---|
1725 | [ 1: (* true branch taken *) |
---|
1726 | cases Hsim_exec_true |
---|
1727 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1728 | | 1: cases (exec_expr ??? iftrue) |
---|
1729 | [ 2: #error #_ @SimFailNicely |
---|
1730 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H |
---|
1731 | @SimOk #a #H @H |
---|
1732 | ] |
---|
1733 | ] |
---|
1734 | | 2: (* false branch taken *) |
---|
1735 | cases Hsim_exec_false |
---|
1736 | [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1737 | | 1: cases (exec_expr ??? iffalse) |
---|
1738 | [ 2: #error #_ @SimFailNicely |
---|
1739 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H |
---|
1740 | @SimOk #a #H @H |
---|
1741 | ] |
---|
1742 | ] |
---|
1743 | ] |
---|
1744 | ] |
---|
1745 | ] |
---|
1746 | ] |
---|
1747 | | 2: @SimFailNicely |
---|
1748 | | 3: // |
---|
1749 | ] |
---|
1750 | | 61,62: destruct |
---|
1751 | elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs |
---|
1752 | elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs |
---|
1753 | try @conj try @conj |
---|
1754 | whd in match (exec_expr ??? (Expr ??)); |
---|
1755 | whd in match (exec_expr ??? (Expr ??)); |
---|
1756 | [ 1,4: cases Hsim_exec_lhs |
---|
1757 | [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1758 | | 1,3: cases (exec_expr ??? lhs) |
---|
1759 | [ 2,4: #error #_ @SimFailNicely |
---|
1760 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs |
---|
1761 | normalize nodelta elim a #lhs_val #lhs_trace |
---|
1762 | cases (exec_bool_of_val lhs_val (typeof lhs1)) |
---|
1763 | [ 2,4: #error @SimFailNicely |
---|
1764 | | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
1765 | [ 2,3: @SimOk // |
---|
1766 | | 1,4: cases Hsim_exec_rhs |
---|
1767 | [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely |
---|
1768 | | 1,3: cases (exec_expr ??? rhs) |
---|
1769 | [ 2,4: #error #_ @SimFailNicely |
---|
1770 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs |
---|
1771 | @SimOk #a #H @H |
---|
1772 | ] |
---|
1773 | ] |
---|
1774 | ] |
---|
1775 | ] |
---|
1776 | ] |
---|
1777 | ] |
---|
1778 | | 2,5: @SimFailNicely |
---|
1779 | | 3,6: // |
---|
1780 | ] |
---|
1781 | | 64: (* record field *) destruct |
---|
1782 | elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1783 | try @conj try @conj |
---|
1784 | whd in match (exec_expr ??? (Expr ??)); |
---|
1785 | whd in match (exec_expr ??? (Expr ??)); |
---|
1786 | whd in match (exec_lvalue' ??? (Efield rec_expr f) ty); |
---|
1787 | whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); |
---|
1788 | [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta |
---|
1789 | [ 2: #sz #sg | 3: #ty' | 4: #ty #n | 5: #tl #ty' |
---|
1790 | | 6: #id #fl | 7: #id #fl | 8: #id ] |
---|
1791 | try (@SimFailNicely) |
---|
1792 | cases Hsim_lvalue |
---|
1793 | [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely |
---|
1794 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
1795 | [ 2,4: #error #_ @SimFailNicely |
---|
1796 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec |
---|
1797 | @SimOk #a #H @H ] |
---|
1798 | ] |
---|
1799 | | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *) |
---|
1800 | >Htype_eq cases (typeof rec_expr1) normalize nodelta |
---|
1801 | [ 2: #sz #sg | 3: #ty' | 4: #ty #n | 5: #tl #ty' |
---|
1802 | | 6: #id #fl | 7: #id #fl | 8: #id ] |
---|
1803 | try (@SimFailNicely) |
---|
1804 | cases Hsim_lvalue |
---|
1805 | [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely |
---|
1806 | | 1,3: cases (exec_lvalue ge en m rec_expr) |
---|
1807 | [ 2,4: #error #_ @SimFailNicely |
---|
1808 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec |
---|
1809 | @SimOk #a #H @H ] |
---|
1810 | ] |
---|
1811 | | 3: // ] |
---|
1812 | | 65: (* cost label *) destruct |
---|
1813 | elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
1814 | try @conj try @conj |
---|
1815 | whd in match (exec_expr ??? (Expr ??)); |
---|
1816 | whd in match (exec_expr ??? (Expr ??)); |
---|
1817 | [ 1: |
---|
1818 | cases Hsim_expr |
---|
1819 | [ 2: * #error #Hexec >Hexec @SimFailNicely |
---|
1820 | | 1: cases (exec_expr ??? e1) |
---|
1821 | [ 2: #error #_ @SimFailNicely |
---|
1822 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H |
---|
1823 | @SimOk #a #H @H ] |
---|
1824 | ] |
---|
1825 | | 2: @SimFail /2 by ex_intro/ |
---|
1826 | | 3: // |
---|
1827 | ] |
---|
1828 | ] qed. |
---|
1829 | |
---|
1830 | (* Propagate cast simplification through statements and programs. *) |
---|
1831 | |
---|
1832 | definition simplify_e ≝ λe. pi1 … (simplify_inside e). |
---|
1833 | |
---|
1834 | let rec simplify_statement (s:statement) : statement ≝ |
---|
1835 | match s with |
---|
1836 | [ Sskip ⇒ Sskip |
---|
1837 | | Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2) |
---|
1838 | | Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es) |
---|
1839 | | Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2) |
---|
1840 | | Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *) |
---|
1841 | | Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) |
---|
1842 | | Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) |
---|
1843 | | Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *) |
---|
1844 | | Sbreak ⇒ Sbreak |
---|
1845 | | Scontinue ⇒ Scontinue |
---|
1846 | | Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo) |
---|
1847 | | Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls) |
---|
1848 | | Slabel l s1 ⇒ Slabel l (simplify_statement s1) |
---|
1849 | | Sgoto l ⇒ Sgoto l |
---|
1850 | | Scost l s1 ⇒ Scost l (simplify_statement s1) |
---|
1851 | ] |
---|
1852 | and simplify_ls ls ≝ |
---|
1853 | match ls with |
---|
1854 | [ LSdefault s ⇒ LSdefault (simplify_statement s) |
---|
1855 | | LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls') |
---|
1856 | ]. |
---|
1857 | |
---|
1858 | definition simplify_function : function → function ≝ |
---|
1859 | λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)). |
---|
1860 | |
---|
1861 | definition simplify_fundef : clight_fundef → clight_fundef ≝ |
---|
1862 | λf. match f with |
---|
1863 | [ CL_Internal f ⇒ CL_Internal (simplify_function f) |
---|
1864 | | _ ⇒ f |
---|
1865 | ]. |
---|
1866 | |
---|
1867 | definition simplify_program : clight_program → clight_program ≝ |
---|
1868 | λp. transform_program … p (λ_.simplify_fundef). |
---|
1869 | |
---|
1870 | (* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *) |
---|
1871 | inductive cont_cast : cont → cont → Prop ≝ |
---|
1872 | | cc_stop : cont_cast Kstop Kstop |
---|
1873 | | cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k') |
---|
1874 | | cc_while : ∀e,s,k,k'. |
---|
1875 | cont_cast k k' → |
---|
1876 | cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') |
---|
1877 | | cc_dowhile : ∀e,s,k,k'. |
---|
1878 | cont_cast k k' → |
---|
1879 | cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') |
---|
1880 | | cc_for1 : ∀e,s1,s2,k,k'. |
---|
1881 | cont_cast k k' → |
---|
1882 | cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k') |
---|
1883 | | cc_for2 : ∀e,s1,s2,k,k'. |
---|
1884 | cont_cast k k' → |
---|
1885 | cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') |
---|
1886 | | cc_for3 : ∀e,s1,s2,k,k'. |
---|
1887 | cont_cast k k' → |
---|
1888 | cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k') |
---|
1889 | | cc_switch : ∀k,k'. |
---|
1890 | cont_cast k k' → cont_cast (Kswitch k) (Kswitch k') |
---|
1891 | | cc_call : ∀r,f,en,k,k'. |
---|
1892 | cont_cast k k' → |
---|
1893 | cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k'). |
---|
1894 | |
---|
1895 | lemma call_cont_cast : ∀k,k'. |
---|
1896 | cont_cast k k' → |
---|
1897 | cont_cast (call_cont k) (call_cont k'). |
---|
1898 | #k0 #k0' #K elim K /2/ |
---|
1899 | qed. |
---|
1900 | |
---|
1901 | inductive state_cast : state → state → Prop ≝ |
---|
1902 | | swc_state : ∀f,s,k,k',e,m. |
---|
1903 | cont_cast k k' → |
---|
1904 | state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m) |
---|
1905 | | swc_callstate : ∀fd,args,k,k',m. |
---|
1906 | cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m) |
---|
1907 | | swc_returnstate : ∀res,k,k',m. |
---|
1908 | cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m) |
---|
1909 | | swc_finalstate : ∀r. |
---|
1910 | state_cast (Finalstate r) (Finalstate r) |
---|
1911 | . |
---|
1912 | |
---|
1913 | record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { |
---|
1914 | rg_find_symbol: ∀s. |
---|
1915 | find_symbol ? ge s = find_symbol ? ge' s; |
---|
1916 | rg_find_funct: ∀v,f. |
---|
1917 | find_funct ? ge v = Some ? f → |
---|
1918 | find_funct ? ge' v = Some ? (t f); |
---|
1919 | rg_find_funct_ptr: ∀b,f. |
---|
1920 | find_funct_ptr ? ge b = Some ? f → |
---|
1921 | find_funct_ptr ? ge' b = Some ? (t f) |
---|
1922 | }. |
---|
1923 | |
---|
1924 | (* The return type of any function is invariant under cast simplification *) |
---|
1925 | lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f. |
---|
1926 | // qed. |
---|
1927 | |
---|
1928 | |
---|
1929 | definition expr_lvalue_ind_combined ≝ |
---|
1930 | λP,Q,ci,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. |
---|
1931 | conj ?? |
---|
1932 | (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx) |
---|
1933 | (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx). |
---|
1934 | |
---|
1935 | lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2. |
---|
1936 | #A #r0 #r1 #r2 * |
---|
1937 | [ 2: * #error #H >H #_ @SimFail /2 by ex_intro/ |
---|
1938 | | 1: cases r0 |
---|
1939 | [ 2: #error #_ #_ @SimFail /2 by ex_intro/ |
---|
1940 | | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ] |
---|
1941 | ] qed. |
---|
1942 | |
---|
1943 | lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → |
---|
1944 | (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ |
---|
1945 | (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). |
---|
1946 | #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined |
---|
1947 | [ 1: #sz #ty #i @SimOk #a normalize // |
---|
1948 | | 2: * |
---|
1949 | [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1 |
---|
1950 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
1951 | #ty #Hsim_lvalue try // |
---|
1952 | whd in match (Plvalue ???); |
---|
1953 | whd in match (exec_expr ????); |
---|
1954 | whd in match (exec_expr ????); |
---|
1955 | cases Hsim_lvalue |
---|
1956 | [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ |
---|
1957 | | *: cases (exec_lvalue' ge en m ? ty) |
---|
1958 | [ 2,4,6: #error #_ @SimFail /2 by ex_intro/ |
---|
1959 | | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
1960 | @SimOk // ] |
---|
1961 | ] |
---|
1962 | | 3: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); |
---|
1963 | cases (lookup SymbolTag block en v) normalize nodelta |
---|
1964 | [ 2: #block @SimOk // |
---|
1965 | | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk // |
---|
1966 | ] |
---|
1967 | | 4: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); |
---|
1968 | cases Hsim_expr |
---|
1969 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
1970 | | 1: cases (exec_expr ge en m e) |
---|
1971 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
1972 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
1973 | @SimOk // ] |
---|
1974 | ] |
---|
1975 | | 5: #ty #ed #ty' #Hsim_lvalue |
---|
1976 | whd in match (exec_expr ????); whd in match (exec_expr ????); |
---|
1977 | whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); |
---|
1978 | cases Hsim_lvalue |
---|
1979 | [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ |
---|
1980 | | 1: cases (exec_lvalue' ge en m ed ty') |
---|
1981 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
1982 | | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
1983 | @SimOk // ] |
---|
1984 | ] |
---|
1985 | | 6: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
1986 | cases Hsim |
---|
1987 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
1988 | | 1: cases (exec_expr ge en m e) |
---|
1989 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
1990 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
1991 | @SimOk // ] |
---|
1992 | ] |
---|
1993 | | 7: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
1994 | cases Hsim1 |
---|
1995 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
1996 | | 1: cases (exec_expr ge en m e1) |
---|
1997 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
1998 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
1999 | cases Hsim2 |
---|
2000 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
2001 | | 1: cases (exec_expr ge en m e2) |
---|
2002 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
2003 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
2004 | @SimOk // ] |
---|
2005 | ] |
---|
2006 | ] |
---|
2007 | ] |
---|
2008 | | 8: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
2009 | cases Hsim |
---|
2010 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
2011 | | 1: cases (exec_expr ge en m e) |
---|
2012 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
2013 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
2014 | @SimOk // ] |
---|
2015 | ] (* mergeable with 7 modulo intros *) |
---|
2016 | | 9: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
2017 | cases Hsim1 |
---|
2018 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
2019 | | 1: cases (exec_expr ge en m e1) |
---|
2020 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
2021 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta |
---|
2022 | cases (exec_bool_of_val (\fst a) (typeof e1)) |
---|
2023 | [ 2: #error @SimFail /2 by ex_intro/ |
---|
2024 | | 1: * |
---|
2025 | [ 1: (* true branch *) cases Hsim2 |
---|
2026 | | 2: (* false branch *) cases Hsim3 ] |
---|
2027 | [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
2028 | | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ] |
---|
2029 | [ 2,4: #error #_ @SimFail /2 by ex_intro/ |
---|
2030 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ] |
---|
2031 | ] |
---|
2032 | ] |
---|
2033 | ] |
---|
2034 | | 10,11: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); |
---|
2035 | cases Hsim1 |
---|
2036 | [ 2,4: * #error #Hfail >Hfail @SimFailNicely |
---|
2037 | | 1,3: cases (exec_expr ge en m e1) |
---|
2038 | [ 2,4: #error #_ @SimFailNicely |
---|
2039 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta |
---|
2040 | cases (exec_bool_of_val ??) |
---|
2041 | [ 2,4: #erro @SimFailNicely |
---|
2042 | | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2043 | [ 2,3: @SimOk // |
---|
2044 | | 1,4: cases Hsim2 |
---|
2045 | [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/ |
---|
2046 | | 1,3: cases (exec_expr ge en m e2) |
---|
2047 | [ 2,4: #error #_ @SimFail /2 by ex_intro/ |
---|
2048 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
2049 | @SimOk // ] |
---|
2050 | ] |
---|
2051 | ] |
---|
2052 | ] |
---|
2053 | ] |
---|
2054 | ] |
---|
2055 | | 12: #ty #sizeof_ty @SimOk normalize // |
---|
2056 | | 13: #ty #e #ty' #field #Hsim_lvalue |
---|
2057 | whd in match (exec_lvalue' ? en m (Efield ??) ty); |
---|
2058 | whd in match (exec_lvalue' ge' en m (Efield ??) ty); |
---|
2059 | normalize in match (typeof (Expr ??)); |
---|
2060 | cases ty' in Hsim_lvalue; normalize nodelta |
---|
2061 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
2062 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
2063 | #Hsim_lvalue |
---|
2064 | try (@SimFail /2 by ex_intro/) |
---|
2065 | normalize in match (exec_lvalue ge en m ?); |
---|
2066 | normalize in match (exec_lvalue ge' en m ?); |
---|
2067 | cases Hsim_lvalue |
---|
2068 | [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
2069 | | 1,3: cases (exec_lvalue' ge en m e ?) |
---|
2070 | [ 2,4: #error #_ @SimFail /2 by ex_intro/ |
---|
2071 | | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
2072 | @SimOk /2 by ex_intro/ ] |
---|
2073 | ] |
---|
2074 | | 14: #ty #lab #e #Hsim |
---|
2075 | whd in match (exec_expr ??? (Expr ??)); |
---|
2076 | whd in match (exec_expr ??? (Expr ??)); |
---|
2077 | cases Hsim |
---|
2078 | [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ |
---|
2079 | | 1: cases (exec_expr ge en m e) |
---|
2080 | [ 2: #error #_ @SimFail /2 by ex_intro/ |
---|
2081 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
2082 | @SimOk // ] |
---|
2083 | ] (* cf case 7, again *) |
---|
2084 | | 15: * |
---|
2085 | [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1 |
---|
2086 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
2087 | #ty normalize in match (is_not_lvalue ?); |
---|
2088 | [ 2,3,12: #Habsurd @(False_ind … Habsurd) ] #_ |
---|
2089 | @SimFailNicely |
---|
2090 | ] qed. |
---|
2091 | |
---|
2092 | lemma related_globals_expr_simulation : ∀ge,ge',en,m. |
---|
2093 | related_globals ? simplify_fundef ge ge' → |
---|
2094 | ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧ |
---|
2095 | typeof e = typeof (simplify_e e). |
---|
2096 | #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); |
---|
2097 | cases e #ed #ty cases ed |
---|
2098 | [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1 |
---|
2099 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
2100 | elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) |
---|
2101 | * * try // |
---|
2102 | cases (exec_expr ge en m (Expr ??)) |
---|
2103 | try (#error #_ #_ #_ @SimFailNicely) |
---|
2104 | * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
2105 | try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?)) |
---|
2106 | qed. |
---|
2107 | |
---|
2108 | lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. |
---|
2109 | related_globals ? simplify_fundef ge ge' → |
---|
2110 | ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧ |
---|
2111 | typeof e = typeof (simplify_e e). |
---|
2112 | #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); |
---|
2113 | cases e #ed #ty cases ed |
---|
2114 | [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1 |
---|
2115 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
2116 | elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) |
---|
2117 | * * try // |
---|
2118 | cases (exec_lvalue ge en m (Expr ??)) |
---|
2119 | try (#error #_ #_ #_ @SimFailNicely) |
---|
2120 | * #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq |
---|
2121 | (* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *) |
---|
2122 | cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); |
---|
2123 | lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1 |
---|
2124 | try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2) |
---|
2125 | qed. |
---|
2126 | |
---|
2127 | lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. |
---|
2128 | related_globals ? simplify_fundef ge ge' → |
---|
2129 | ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)). |
---|
2130 | #ge #ge' #en #m #Hrelated #args |
---|
2131 | elim args |
---|
2132 | [ 1: /3/ |
---|
2133 | | 2: #hd #tl #Hind normalize |
---|
2134 | elim (related_globals_expr_simulation ge ge' en m Hrelated hd) |
---|
2135 | * |
---|
2136 | [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/ |
---|
2137 | | 1: cases (exec_expr ge en m hd) |
---|
2138 | [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/ |
---|
2139 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq |
---|
2140 | cases Hind normalize |
---|
2141 | [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/ |
---|
2142 | | 1: cases (exec_exprlist ??? tl) |
---|
2143 | [ 2: #error #_ @SimFail /2 by refl, ex_intro/ |
---|
2144 | | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉))) |
---|
2145 | #Heq >Heq @SimOk // ] |
---|
2146 | ] |
---|
2147 | ] |
---|
2148 | ] |
---|
2149 | ] qed. |
---|
2150 | |
---|
2151 | lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd). |
---|
2152 | * // qed. |
---|
2153 | |
---|
2154 | lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func. |
---|
2155 | #ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func) |
---|
2156 | #func' #H lapply (H ge en m) * * #_ #_ // |
---|
2157 | qed. |
---|
2158 | |
---|
2159 | lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func. |
---|
2160 | #ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%); |
---|
2161 | >simplify_typeof_eq whd in match (simplify_e func); // qed. |
---|
2162 | |
---|
2163 | lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf. |
---|
2164 | * |
---|
2165 | [ 1: * #Habsurd elim (Habsurd (refl ? Sskip)) |
---|
2166 | | *: #a try #b try #c try #d try #e |
---|
2167 | whd in match (simplify_statement ?); |
---|
2168 | whd in match (is_Sskip ?); |
---|
2169 | try /2 by refl, ex_intro/ |
---|
2170 | ] qed. |
---|
2171 | |
---|
2172 | lemma call_cont_simplify : ∀k,k'. |
---|
2173 | cont_cast k k' → |
---|
2174 | cont_cast (call_cont k) (call_cont k'). |
---|
2175 | #k0 #k0' #K elim K /2/ |
---|
2176 | qed. |
---|
2177 | |
---|
2178 | lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)). |
---|
2179 | #l @(labeled_statements_ind … l) |
---|
2180 | [ 1: #default_statement // |
---|
2181 | | 2: #sz #i #s #tl #Hind |
---|
2182 | whd in match (seq_of_labeled_statement ?) in ⊢ (??%?); |
---|
2183 | whd in match (simplify_ls ?) in ⊢ (???%); |
---|
2184 | whd in match (seq_of_labeled_statement ?) in ⊢ (???%); |
---|
2185 | whd in match (simplify_statement ?) in ⊢ (??%?); |
---|
2186 | >Hind // |
---|
2187 | ] qed. |
---|
2188 | |
---|
2189 | lemma select_switch_simplify_elim : ∀sz,i,l. ∀P:option labeled_statements → option labeled_statements → Prop. |
---|
2190 | (P (None ?) (None ?)) → |
---|
2191 | (∀l'. P (Some ? l') (Some ? (simplify_ls l'))) → |
---|
2192 | P (select_switch sz i l) (select_switch sz i (simplify_ls l)). |
---|
2193 | #sz #i #l #P #NONE #SOME @(labeled_statements_ind … l) |
---|
2194 | [ 1: #default_statement // |
---|
2195 | | 2: #sz' #i' #s #tl #Hind |
---|
2196 | whd in match (simplify_ls ?); |
---|
2197 | whd in match (select_switch ???); whd in match (select_switch ???); |
---|
2198 | cases (sz_eq_dec sz sz') |
---|
2199 | [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true |
---|
2200 | cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta // |
---|
2201 | | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq) |
---|
2202 | @NONE |
---|
2203 | ] |
---|
2204 | ] qed. |
---|
2205 | |
---|
2206 | lemma elim_IH_aux : |
---|
2207 | ∀lab. ∀s:statement.∀k,k'. cont_cast k k' → |
---|
2208 | ∀Hind:(∀k:cont.∀k':cont. |
---|
2209 | cont_cast k k' → |
---|
2210 | match find_label lab s k with |
---|
2211 | [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont) |
---|
2212 | | Some (r:(statement×cont))⇒ |
---|
2213 | let 〈s',ks〉 ≝r in |
---|
2214 | ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉 |
---|
2215 | ∧ cont_cast ks ks']). |
---|
2216 | (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨ |
---|
2217 | (∃st,kst,kst'. find_label lab s k = Some ? 〈st,kst〉 ∧ find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement st,kst'〉 ∧ cont_cast kst kst'). |
---|
2218 | #lab #s #k #k' #Hcont_cast #Hind |
---|
2219 | lapply (Hind k k' Hcont_cast) |
---|
2220 | cases (find_label lab s k) |
---|
2221 | [ 1: normalize nodelta #Heq >Heq /3/ |
---|
2222 | | 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2 |
---|
2223 | %{st} %{kst} %{kst'} @conj try @conj // |
---|
2224 | ] qed. |
---|
2225 | |
---|
2226 | |
---|
2227 | lemma cast_find_label : ∀lab,s,k,k'. |
---|
2228 | cont_cast k k' → |
---|
2229 | match find_label lab s k with |
---|
2230 | [ Some r ⇒ |
---|
2231 | let 〈s',ks〉 ≝ r in |
---|
2232 | ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉 |
---|
2233 | ∧ cont_cast ks ks' |
---|
2234 | | None ⇒ |
---|
2235 | find_label lab (simplify_statement s) k' = None ? |
---|
2236 | ]. |
---|
2237 | #lab #s @(statement_ind2 ? (λls. |
---|
2238 | ∀k:cont |
---|
2239 | .∀k':cont |
---|
2240 | .cont_cast k k' |
---|
2241 | →match find_label_ls lab ls k with |
---|
2242 | [None⇒ |
---|
2243 | find_label_ls lab (simplify_ls ls) k' = None ? |
---|
2244 | |Some r ⇒ |
---|
2245 | let 〈s',ks〉 ≝r in |
---|
2246 | ∃ks':cont |
---|
2247 | .find_label_ls lab (simplify_ls ls) k' |
---|
2248 | =Some (statement×cont) 〈simplify_statement s',ks'〉 |
---|
2249 | ∧cont_cast ks ks'] |
---|
2250 | ) … s) |
---|
2251 | [ 1: #k #k' #Hcont_cast |
---|
2252 | whd in match (find_label ? Sskip ?); normalize nodelta @refl |
---|
2253 | | 2: #e1 #e2 #k #k' #Hcont_cast |
---|
2254 | whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl |
---|
2255 | | 3: #e0 #e #args #k #k' #Hcont_cast |
---|
2256 | whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl |
---|
2257 | | 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast |
---|
2258 | whd in match (find_label ? (Ssequence s1 s2) ?); |
---|
2259 | whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); |
---|
2260 | elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1) |
---|
2261 | [ 3: try ( @cc_seq // ) |
---|
2262 | | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2263 | normalize nodelta %{kst'} /2/ |
---|
2264 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
2265 | elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) |
---|
2266 | [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' |
---|
2267 | normalize nodelta %{kst'} /2/ |
---|
2268 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
2269 | ] ] |
---|
2270 | | 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast |
---|
2271 | whd in match (find_label ???); |
---|
2272 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2273 | elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1) |
---|
2274 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2275 | normalize nodelta %{kst'} /2/ |
---|
2276 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
2277 | elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) |
---|
2278 | [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' |
---|
2279 | normalize nodelta %{kst'} /2/ |
---|
2280 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
2281 | ] ] |
---|
2282 | | 6: #e #s #Hind_s #k #k' #Hcont_cast |
---|
2283 | whd in match (find_label ???); |
---|
2284 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2285 | elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s) |
---|
2286 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2287 | normalize nodelta %{kst'} /2/ |
---|
2288 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
2289 | | 3: @cc_while // ] |
---|
2290 | | 7: #e #s #Hind_s #k #k' #Hcont_cast |
---|
2291 | whd in match (find_label ???); |
---|
2292 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2293 | elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s) |
---|
2294 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2295 | normalize nodelta %{kst'} /2/ |
---|
2296 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
2297 | | 3: @cc_dowhile // ] |
---|
2298 | | 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast |
---|
2299 | whd in match (find_label ???); |
---|
2300 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2301 | elim (elim_IH_aux lab s1 |
---|
2302 | (Kseq (Sfor Sskip cond s2 s3) k) |
---|
2303 | (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k') |
---|
2304 | ? Hind_s1) |
---|
2305 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2306 | normalize nodelta %{kst'} /2/ |
---|
2307 | | 3: @cc_for1 // |
---|
2308 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
2309 | elim (elim_IH_aux lab s3 |
---|
2310 | (Kfor2 cond s2 s3 k) |
---|
2311 | (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') |
---|
2312 | ? Hind_s3) |
---|
2313 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2314 | normalize nodelta %{kst'} /2/ |
---|
2315 | | 3: @cc_for2 // |
---|
2316 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta |
---|
2317 | elim (elim_IH_aux lab s2 |
---|
2318 | (Kfor3 cond s2 s3 k) |
---|
2319 | (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') |
---|
2320 | ? Hind_s2) |
---|
2321 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2322 | normalize nodelta %{kst'} /2/ |
---|
2323 | | 3: @cc_for3 // |
---|
2324 | | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // |
---|
2325 | ] ] ] |
---|
2326 | | 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // |
---|
2327 | | 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta // |
---|
2328 | | 12: #e #ls #Hind #k #k' #Hcont_cast |
---|
2329 | whd in match (find_label ???); |
---|
2330 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2331 | (* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *) |
---|
2332 | lapply (Hind (Kswitch k) (Kswitch k') ?) |
---|
2333 | [ 1: @cc_switch // |
---|
2334 | | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta |
---|
2335 | [ 1: // |
---|
2336 | | 2: * #st #kst normalize nodelta // ] ] |
---|
2337 | | 13: #lab' #s0 #Hind #k #k' #Hcont_cast |
---|
2338 | whd in match (find_label ???); |
---|
2339 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2340 | cases (ident_eq lab lab') normalize nodelta |
---|
2341 | [ 1: #_ %{k'} /2/ |
---|
2342 | | 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) |
---|
2343 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2344 | normalize nodelta %{kst'} /2/ |
---|
2345 | | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] |
---|
2346 | ] |
---|
2347 | | 14: #l #k #k' #Hcont_cast // |
---|
2348 | | 15: #l #s0 #Hind #k #k' #Hcont_cast |
---|
2349 | whd in match (find_label ???); |
---|
2350 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2351 | elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) |
---|
2352 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2353 | normalize nodelta %{kst'} /2/ |
---|
2354 | | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] |
---|
2355 | | 16: #s0 #Hind #k #k' #Hcont_cast |
---|
2356 | whd in match (find_label ???); |
---|
2357 | whd in match (find_label ? (simplify_statement ?) ?); |
---|
2358 | elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) |
---|
2359 | [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' |
---|
2360 | normalize nodelta %{kst'} /2/ |
---|
2361 | | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] |
---|
2362 | | 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast |
---|
2363 | whd in match (simplify_ls ?); |
---|
2364 | whd in match (find_label_ls ???); |
---|
2365 | lapply Hind_ls |
---|
2366 | @(labeled_statements_ind … t) |
---|
2367 | [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?); |
---|
2368 | elim (elim_IH_aux lab s0 |
---|
2369 | (Kseq default_case k) |
---|
2370 | (Kseq (simplify_statement default_case) k') ? Hind_s0) |
---|
2371 | [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' |
---|
2372 | >Hrewrite >Hrewrite1 |
---|
2373 | normalize nodelta whd in match (find_label_ls ???); |
---|
2374 | >Hrewrite >Hrewrite1 normalize nodelta |
---|
2375 | %{kst'} /2/ |
---|
2376 | | 3: @cc_seq // |
---|
2377 | | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta |
---|
2378 | lapply (Hind_ls k k' Hcont_cast) |
---|
2379 | cases (find_label_ls lab (LSdefault default_case) k) |
---|
2380 | [ 1: normalize nodelta #Heq1 |
---|
2381 | whd in match (simplify_ls ?); |
---|
2382 | whd in match (find_label_ls lab ??); |
---|
2383 | whd in match (seq_of_labeled_statement ?); |
---|
2384 | whd in match (find_label_ls lab ??); |
---|
2385 | >Hrewrite1 normalize nodelta @Heq1 |
---|
2386 | | 2: * #st #kst normalize nodelta #H |
---|
2387 | whd in match (find_label_ls lab ??); |
---|
2388 | whd in match (simplify_ls ?); |
---|
2389 | whd in match (seq_of_labeled_statement ?); |
---|
2390 | >Hrewrite1 normalize nodelta @H |
---|
2391 | ] |
---|
2392 | ] |
---|
2393 | | 2: #sz' #i' #s' #tl' #Hind #A |
---|
2394 | |
---|
2395 | whd in match (seq_of_labeled_statement ?); |
---|
2396 | elim (elim_IH_aux lab s0 |
---|
2397 | (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k) |
---|
2398 | (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k') |
---|
2399 | ? |
---|
2400 | Hind_s0) |
---|
2401 | [ 3: @cc_seq // |
---|
2402 | | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta |
---|
2403 | lapply (A k k' Hcont_cast) |
---|
2404 | cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta |
---|
2405 | [ 1: #H whd in match (find_label_ls ???); |
---|
2406 | <simplify_ls_commute |
---|
2407 | whd in match (seq_of_labeled_statement ?); |
---|
2408 | >Heq2 normalize nodelta |
---|
2409 | assumption |
---|
2410 | | 2: * #st #kst normalize nodelta #H |
---|
2411 | whd in match (find_label_ls ???); |
---|
2412 | <simplify_ls_commute >Heq2 normalize nodelta @H |
---|
2413 | ] |
---|
2414 | | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast' |
---|
2415 | >Hrewrite normalize nodelta |
---|
2416 | %{kst'} @conj try // |
---|
2417 | whd in match (find_label_ls ???); |
---|
2418 | <simplify_ls_commute >Hrewrite1 // |
---|
2419 | ] |
---|
2420 | ] |
---|
2421 | ] qed. |
---|
2422 | |
---|
2423 | lemma cast_find_label_fn : ∀lab,f,k,k',s,ks. |
---|
2424 | cont_cast k k' → |
---|
2425 | find_label lab (fn_body f) k = Some ? 〈s,ks〉 → |
---|
2426 | ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉 |
---|
2427 | ∧ cont_cast ks ks'. |
---|
2428 | #lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab |
---|
2429 | whd in match (simplify_function ?); |
---|
2430 | lapply (cast_find_label lab body ?? Hcont_cast) |
---|
2431 | >Hfind_lab normalize nodelta // |
---|
2432 | qed. |
---|
2433 | |
---|
2434 | theorem cast_correction : ∀ge, ge'. |
---|
2435 | related_globals ? simplify_fundef ge ge' → |
---|
2436 | ∀s1, s1', tr, s2. |
---|
2437 | state_cast s1 s1' → |
---|
2438 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
2439 | ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧ |
---|
2440 | state_cast s2 s2'. |
---|
2441 | #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome |
---|
2442 | inversion Hs1_sim_s1' |
---|
2443 | [ 1: (* regular state *) |
---|
2444 | #f #stm #k #k' #en #m #Hcont_cast |
---|
2445 | lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related |
---|
2446 | lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related |
---|
2447 | cases stm |
---|
2448 | (* Perform the intros for the statements*) |
---|
2449 | [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body |
---|
2450 | | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body |
---|
2451 | | 14: #lab | 15: #cost #body ] |
---|
2452 | [ 1: (* Skip *) |
---|
2453 | #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 |
---|
2454 | whd in match (exec_step ??); whd in match (exec_step ??); |
---|
2455 | inversion Hcont_cast |
---|
2456 | [ 1: (* Kstop *) |
---|
2457 | #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta |
---|
2458 | [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim |
---|
2459 | [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_ |
---|
2460 | #Eq whd in match (ret ??) in Eq; destruct (Eq) |
---|
2461 | %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj |
---|
2462 | [ 1: // | 2: %3 %1 ] |
---|
2463 | | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd) |
---|
2464 | | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd) |
---|
2465 | | 4: #r #Habsurd destruct (Habsurd) ] |
---|
2466 | | 3,8: #irrelevant #Habsurd destruct |
---|
2467 | | *: #irrelevant1 #irrelevant2 #Habsurd destruct ] |
---|
2468 | | 2: (* Kseq stm' k' *) |
---|
2469 | #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
2470 | whd in match (ret ??) in Eq; destruct (Eq) |
---|
2471 | %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj |
---|
2472 | [ 1: // | 2: %1 // ] |
---|
2473 | | 3: (* Kwhile *) |
---|
2474 | #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
2475 | whd in match (ret ??) in Eq; destruct (Eq) |
---|
2476 | %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj |
---|
2477 | [ 1: // | 2: %1 // ] |
---|
2478 | | 4: (* Kdowhile *) |
---|
2479 | #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
2480 | elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond |
---|
2481 | [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct |
---|
2482 | | 1: cases (exec_expr ge en m cond) in Eq; |
---|
2483 | [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct |
---|
2484 | | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq |
---|
2485 | #Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) |
---|
2486 | #Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????); |
---|
2487 | (* case analysis on the outcome of the conditional *) |
---|
2488 | cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %; |
---|
2489 | [ 2: (* evaluation of the conditional fails *) |
---|
2490 | #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
2491 | | 1: * whd in match (bindIO ??????); |
---|
2492 | whd in match (bindIO ??????); |
---|
2493 | #Eq destruct (Eq) |
---|
2494 | [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} |
---|
2495 | @conj [ 1: // | 2: %1 // ] |
---|
2496 | | 2: %{(State (simplify_function f) Sskip k0' en m)} |
---|
2497 | @conj [ 1: // | 2: %1 // ] |
---|
2498 | ] |
---|
2499 | ] |
---|
2500 | ] |
---|
2501 | ] |
---|
2502 | | 5,6,7: |
---|
2503 | #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
2504 | whd in match (ret ??) in Eq ⊢ %; destruct (Eq) |
---|
2505 | [ 1: %{(State (simplify_function f) |
---|
2506 | (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) |
---|
2507 | k0' en m)} @conj |
---|
2508 | [ 1: // | 2: %1 // ] |
---|
2509 | | 2: %{(State (simplify_function f) |
---|
2510 | (simplify_statement step) |
---|
2511 | (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') |
---|
2512 | en m)} @conj |
---|
2513 | [ 1: // | 2: %1 @cc_for3 // ] |
---|
2514 | | 3: %{(State (simplify_function f) |
---|
2515 | (Sfor Sskip (simplify_e cond) (simplify_statement step) |
---|
2516 | (simplify_statement body)) |
---|
2517 | k0' en m)} @conj |
---|
2518 | [ 1: // | 2: %1 // ] |
---|
2519 | ] |
---|
2520 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq |
---|
2521 | whd in match (ret ??) in Eq ⊢ %; destruct (Eq) |
---|
2522 | %{(State (simplify_function f) Sskip k0' en m)} @conj |
---|
2523 | [ 1: // | 2: %1 // ] |
---|
2524 | | 9: (* Call *) |
---|
2525 | #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq |
---|
2526 | >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta |
---|
2527 | [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq) |
---|
2528 | %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0') |
---|
2529 | (free_list m (blocks_of_env en)))} @conj |
---|
2530 | [ 1: // | 2: %3 @cc_call // ] |
---|
2531 | | 3,8: #irrelevant #Habsurd destruct (Habsurd) |
---|
2532 | | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ] |
---|
2533 | ] |
---|
2534 | | 2: (* Assign *) |
---|
2535 | #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 |
---|
2536 | whd in match (simplify_statement ?); #Heq |
---|
2537 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2538 | (* Begin by making the simplify_e disappear using Hsim_related *) |
---|
2539 | elim (Hsim_lvalue_related lhs) * |
---|
2540 | [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2541 | | 1: cases (exec_lvalue ge en m lhs) in Heq; |
---|
2542 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2543 | | 1: * * #block #offset #trace |
---|
2544 | whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs |
---|
2545 | lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉))) |
---|
2546 | #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); |
---|
2547 | (* After [lhs], treat [rhs] *) |
---|
2548 | elim (Hsim_related rhs) * |
---|
2549 | [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2550 | | 1: cases (exec_expr ge en m rhs) in Heq; |
---|
2551 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2552 | | 1: * #val #trace |
---|
2553 | whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs |
---|
2554 | lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉))) |
---|
2555 | #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????); |
---|
2556 | <Htype_eq_lhs <Htype_eq_rhs |
---|
2557 | cases (opt_to_io ?????) in Heq; |
---|
2558 | [ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2559 | | 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd) |
---|
2560 | | 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq) |
---|
2561 | %{(State (simplify_function f) Sskip k' en mem)} @conj |
---|
2562 | [ 1: // | 2: %1 // ] |
---|
2563 | ] |
---|
2564 | ] |
---|
2565 | ] |
---|
2566 | ] |
---|
2567 | ] |
---|
2568 | | 3: (* Call *) |
---|
2569 | #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1 |
---|
2570 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2571 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2572 | elim (Hsim_related func) in Heq; * |
---|
2573 | [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2574 | | 1: cases (exec_expr ??? func) |
---|
2575 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2576 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq |
---|
2577 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2578 | elim (related_globals_exprlist_simulation ge ge' en m Hrelated args) |
---|
2579 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2580 | | 1: cases (exec_exprlist ge en m args) |
---|
2581 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2582 | | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq |
---|
2583 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2584 | elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a)) |
---|
2585 | cases (find_funct clight_fundef ge (\fst a)); |
---|
2586 | [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2587 | | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq |
---|
2588 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2589 | >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m) |
---|
2590 | cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func)) |
---|
2591 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2592 | | 1: #Htype_eq cases ret |
---|
2593 | [ 1: whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2594 | #Eq destruct (Eq) |
---|
2595 | %{(Callstate (simplify_fundef clfd) (\fst l) |
---|
2596 | (Kcall (None (block×offset×type)) (simplify_function f) en k') m)} |
---|
2597 | @conj |
---|
2598 | [ 1: // | 2: %2 @cc_call // ] |
---|
2599 | | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2600 | elim (Hsim_lvalue_related fptr) * |
---|
2601 | [ 2: * #error #Hfail >Hfail #_ |
---|
2602 | #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2603 | | 1: cases (exec_lvalue ge en m fptr) |
---|
2604 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2605 | | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a))) |
---|
2606 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2607 | #Heq destruct (Heq) |
---|
2608 | %{(Callstate (simplify_fundef clfd) (\fst l) |
---|
2609 | (Kcall (Some (block×offset×type) 〈\fst a,typeof (simplify_e fptr)〉) |
---|
2610 | (simplify_function f) en k') m)} |
---|
2611 | @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ] |
---|
2612 | ] ] ] ] ] ] ] ] ] |
---|
2613 | | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2614 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2615 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2616 | destruct (Heq) |
---|
2617 | %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)} |
---|
2618 | @conj |
---|
2619 | [ 1: // | 2: %1 @cc_seq // ] |
---|
2620 | | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2621 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2622 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2623 | elim (Hsim_related cond) in Heq; * |
---|
2624 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2625 | | 1: cases (exec_expr ge en m cond) |
---|
2626 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2627 | | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq |
---|
2628 | #Htype_eq_cond |
---|
2629 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2630 | >(simplify_typeof_eq ge en m) |
---|
2631 | cases (exec_bool_of_val condval (typeof cond)) |
---|
2632 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2633 | | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; |
---|
2634 | [ 1: destruct skip (condtrace) |
---|
2635 | %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj |
---|
2636 | [ 1: // | 2: <e0 %1 // ] |
---|
2637 | | 2: destruct skip (condtrace) |
---|
2638 | %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj |
---|
2639 | [ 1: // | 2: <e0 %1 // ] |
---|
2640 | ] ] ] ] |
---|
2641 | | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2642 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2643 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2644 | elim (Hsim_related cond) in Heq; * |
---|
2645 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2646 | | 1: cases (exec_expr ge en m cond) |
---|
2647 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2648 | | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq |
---|
2649 | #Htype_eq_cond |
---|
2650 | whd in match (bindIO ??????) in ⊢ (% → %); |
---|
2651 | >(simplify_typeof_eq ge en m) |
---|
2652 | cases (exec_bool_of_val condval (typeof cond)) |
---|
2653 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2654 | | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; |
---|
2655 | [ 1: destruct skip (condtrace) |
---|
2656 | %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)} |
---|
2657 | @conj |
---|
2658 | [ 1: // | 2: <e0 %1 @cc_while // ] |
---|
2659 | | 2: destruct skip (condtrace) |
---|
2660 | %{(State (simplify_function f) Sskip k' en m)} @conj |
---|
2661 | [ 1: // | 2: <e0 %1 // ] |
---|
2662 | ] ] ] ] |
---|
2663 | | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2664 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2665 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2666 | destruct (Heq) |
---|
2667 | %{(State (simplify_function f) (simplify_statement body) |
---|
2668 | (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj |
---|
2669 | [ 1: // | 2: %1 @cc_dowhile // ] |
---|
2670 | | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2671 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2672 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2673 | cases (is_Sskip init) in Heq; |
---|
2674 | [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite |
---|
2675 | normalize nodelta |
---|
2676 | whd in match (ret ??) in ⊢ (% → %); |
---|
2677 | #Eq destruct (Eq) |
---|
2678 | %{(State (simplify_function f) (simplify_statement init) |
---|
2679 | (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj |
---|
2680 | [ 1: // | 2: %1 @cc_for1 // ] |
---|
2681 | | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip |
---|
2682 | whd in match (simplify_statement ?); |
---|
2683 | whd in match (is_Sskip ?); |
---|
2684 | normalize nodelta |
---|
2685 | elim (Hsim_related cond) * |
---|
2686 | [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2687 | | 1: cases (exec_expr ge en m cond) |
---|
2688 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2689 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite |
---|
2690 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2691 | <Htype_eq_cond |
---|
2692 | cases (exec_bool_of_val ? (typeof cond)) |
---|
2693 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2694 | | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); |
---|
2695 | normalize nodelta #Heq destruct (Heq) |
---|
2696 | [ 1: %{(State (simplify_function f) (simplify_statement body) |
---|
2697 | (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)} |
---|
2698 | @conj [ 1: // | 2: %1 @cc_for2 // ] |
---|
2699 | | 2: %{(State (simplify_function f) Sskip k' en m)} @conj |
---|
2700 | [ 1: // | 2: %1 // ] |
---|
2701 | ] ] ] ] ] |
---|
2702 | | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2703 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2704 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2705 | inversion Hcont_cast in Heq; normalize nodelta |
---|
2706 | [ 1: #Hk #Hk' #_ |
---|
2707 | | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
2708 | | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
2709 | | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2710 | | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2711 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2712 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] |
---|
2713 | #H whd in match (ret ??) in H ⊢ %; |
---|
2714 | destruct (H) |
---|
2715 | [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ] |
---|
2716 | | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ] |
---|
2717 | | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2718 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2719 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2720 | inversion Hcont_cast in Heq; normalize nodelta |
---|
2721 | [ 1: #Hk #Hk' #_ |
---|
2722 | | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
2723 | | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
2724 | | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2725 | | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2726 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2727 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] |
---|
2728 | #H whd in match (ret ??) in H ⊢ %; |
---|
2729 | destruct (H) |
---|
2730 | [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 // |
---|
2731 | | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} |
---|
2732 | @conj try // %1 // |
---|
2733 | | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H; |
---|
2734 | [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2735 | | 1: cases (exec_expr ??? cond) |
---|
2736 | [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2737 | | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite |
---|
2738 | whd in match (m_bind ?????) in ⊢ (% → %); |
---|
2739 | <Htype_cond_eq |
---|
2740 | cases (exec_bool_of_val ? (typeof cond)) |
---|
2741 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2742 | | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????); |
---|
2743 | normalize nodelta #Heq destruct (Heq) |
---|
2744 | [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)} |
---|
2745 | @conj [ 1: // | 2: %1 // ] |
---|
2746 | | 2: %{(State (simplify_function f) Sskip k0' en m)} |
---|
2747 | @conj [ 1: // | 2: %1 // ] |
---|
2748 | ] ] ] ] |
---|
2749 | | 5: %{(State (simplify_function f) (simplify_statement step) |
---|
2750 | (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj |
---|
2751 | [ 1: // | 2: %1 @cc_for3 // ] |
---|
2752 | ] |
---|
2753 | | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2754 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2755 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2756 | cases retval in Heq; normalize nodelta |
---|
2757 | [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta |
---|
2758 | whd in match (ret ??) in ⊢ (% → %); |
---|
2759 | [ | #sz #sg | #ty' | #ty #n | #tl #ty' |
---|
2760 | | #id #fl | #id #fl | #id ] |
---|
2761 | #H destruct (H) |
---|
2762 | %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))} |
---|
2763 | @conj [ 1: // | 2: %3 @call_cont_simplify // ] |
---|
2764 | | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta |
---|
2765 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2766 | | 2: #_ elim (Hsim_related e) * |
---|
2767 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2768 | | 1: cases (exec_expr ??? e) |
---|
2769 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2770 | | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a))) |
---|
2771 | #Hrewrite >Hrewrite |
---|
2772 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2773 | #Heq destruct (Heq) |
---|
2774 | %{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env en)))} |
---|
2775 | @conj [ 1: // | 2: %3 @call_cont_simplify // ] |
---|
2776 | ] ] ] ] |
---|
2777 | | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2778 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2779 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2780 | elim (Hsim_related cond) in Heq; * |
---|
2781 | [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2782 | | 1: cases (exec_expr ??? cond) |
---|
2783 | [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2784 | | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a))) |
---|
2785 | #Hrewrite >Hrewrite |
---|
2786 | whd in match (bindIO ??????); whd in match (bindIO ??????); |
---|
2787 | cases (\fst a) normalize nodelta |
---|
2788 | [ 1,3,4,5: #a destruct (a) #b destruct (b) |
---|
2789 | | 2: #sz #i <Htype_eq_cond cases (typeof cond) |
---|
2790 | [ 1,3,4,5,6,7,8,9: normalize nodelta #a try #b try #c destruct] |
---|
2791 | #sz' #sg normalize nodelta cases (sz_eq_dec sz sz') |
---|
2792 | #SZ [2: normalize nodelta #E destruct ] |
---|
2793 | normalize nodelta @select_switch_simplify_elim |
---|
2794 | [ #H whd in H:(??%?); destruct ] |
---|
2795 | #l' whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
2796 | #Heq destruct (Heq) |
---|
2797 | %{(State (simplify_function f) |
---|
2798 | (seq_of_labeled_statement (simplify_ls l')) |
---|
2799 | (Kswitch k') en m)} @conj |
---|
2800 | [ 1: // |
---|
2801 | | 2: @(labeled_statements_ind … l') |
---|
2802 | [ 1: #default_s |
---|
2803 | whd in match (simplify_ls ?); |
---|
2804 | whd in match (select_switch sz i ?) in ⊢ (?%%); |
---|
2805 | whd in match (seq_of_labeled_statement ?) in ⊢ (?%%); |
---|
2806 | %1 @cc_switch // |
---|
2807 | | 2: #sz' #i' #top_case #tail #Hind |
---|
2808 | <simplify_ls_commute |
---|
2809 | %1 @cc_switch // |
---|
2810 | ] ] ] ] ] |
---|
2811 | | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2812 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2813 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2814 | destruct (Heq) |
---|
2815 | %{(State (simplify_function f) (simplify_statement body) k' en m)} |
---|
2816 | @conj %1 // |
---|
2817 | | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2818 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2819 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2820 | lapply (cast_find_label_fn lab f (call_cont k) (call_cont k')) |
---|
2821 | cases (find_label lab (fn_body f) (call_cont k)) in Heq; |
---|
2822 | normalize nodelta |
---|
2823 | [ 1: #Habsurd destruct (Habsurd) |
---|
2824 | | 2: * #st #kst normalize nodelta |
---|
2825 | #Heq whd in match (ret ??) in Heq; |
---|
2826 | #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try // |
---|
2827 | * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta |
---|
2828 | destruct (Heq) |
---|
2829 | %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj |
---|
2830 | [ 1: // | 2: %1 // ] |
---|
2831 | ] |
---|
2832 | | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2833 | whd in match (simplify_statement ?) in Heq ⊢ %; #Heq |
---|
2834 | whd in match (exec_step ??) in Heq ⊢ %; |
---|
2835 | destruct (Heq) |
---|
2836 | %{(State (simplify_function f) (simplify_statement body) k' en m)} |
---|
2837 | @conj |
---|
2838 | [ 1: // | 2: %1 // ] |
---|
2839 | ] |
---|
2840 | | 2: (* Call state *) |
---|
2841 | #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2842 | whd in match (exec_step ??) in ⊢ (% → %); |
---|
2843 | elim fd in Heq_s1'; normalize nodelta |
---|
2844 | [ 1: * #rettype #args #vars #body #Heq_s1' |
---|
2845 | whd in match (simplify_function ?); |
---|
2846 | cases (exec_alloc_variables empty_env ??) |
---|
2847 | #local_env #new_mem normalize nodelta |
---|
2848 | cases (exec_bind_parameters ????) |
---|
2849 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2850 | | 1: #new_mem_init |
---|
2851 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2852 | #Heq destruct (Heq) |
---|
2853 | %{(State (mk_function rettype args vars (simplify_statement body)) |
---|
2854 | (simplify_statement body) k' local_env new_mem_init)} @conj |
---|
2855 | [ 1: // | 2: %1 // ] |
---|
2856 | ] |
---|
2857 | | 2: #id #argtypes #rettype #Heq_s1' |
---|
2858 | cases (check_eventval_list args ?) |
---|
2859 | [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
2860 | | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2861 | #Habsurd destruct (Habsurd) ] |
---|
2862 | ] |
---|
2863 | | 3: (* Return state *) |
---|
2864 | #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2865 | whd in match (exec_step ??) in ⊢ (% → %); |
---|
2866 | inversion Hcont_cast |
---|
2867 | [ 1: #Hk #Hk' #_ |
---|
2868 | | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
2869 | | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ |
---|
2870 | | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2871 | | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2872 | | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ |
---|
2873 | | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ] |
---|
2874 | normalize nodelta |
---|
2875 | [ 1: cases res normalize nodelta |
---|
2876 | [ 2: * normalize nodelta #i |
---|
2877 | [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq) |
---|
2878 | %{(Finalstate i)} @conj [ 1: // | 2: // ] |
---|
2879 | | * : #Habsurd destruct (Habsurd) ] |
---|
2880 | | *: #a try #b destruct ] |
---|
2881 | | 9: elim r normalize nodelta |
---|
2882 | [ 2: * * #block #offset #typ normalize nodelta |
---|
2883 | cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????)) |
---|
2884 | [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
2885 | #Heq destruct (Heq) |
---|
2886 | %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj |
---|
2887 | [ 1: // | 2: %1 // ] |
---|
2888 | | 1: #output #resumption |
---|
2889 | whd in match (m_bind ?????); #Habsurd destruct (Habsurd) |
---|
2890 | | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
2891 | | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq) |
---|
2892 | %{(State (simplify_function f0) Sskip k0' en0 m)} @conj |
---|
2893 | [ 1: // | 2: %1 // ] |
---|
2894 | ] |
---|
2895 | | *: #Habsurd destruct (Habsurd) ] |
---|
2896 | | 4: (* Final state *) |
---|
2897 | #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; |
---|
2898 | whd in match (exec_step ??) in ⊢ (% → %); |
---|
2899 | #Habsurd destruct (Habsurd) |
---|
2900 | ] qed. |
---|