# source:src/Clight/SimplifyCasts.ma@2768

Last change on this file since 2768 was 2722, checked in by campbell, 7 years ago

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

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