source: src/Clight/SimplifyCasts.ma @ 2011

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

Minor cleanup.

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