source: src/Clight/SimplifyCasts.ma @ 2441

Last change on this file since 2441 was 2441, checked in by garnier, 7 years ago

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

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