source: src/Clight/SimplifyCasts.ma @ 2468

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

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

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