source: src/Clight/SimplifyCasts.ma @ 2009

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

Proof of simulation completed for singe-step executions.

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