source: src/Clight/SimplifyCasts.ma @ 2030

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

Cast simplification was too conservative, now reasonably aggressive.

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