source: src/Clight/SimplifyCasts.ma @ 1986

Last change on this file since 1986 was 1974, checked in by garnier, 8 years ago

Progress on the cast simplification proof.

File size: 104.5 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
23
24(* Attempt to squeeze integer constant into a given type.
25
26   This might be too conservative --- if we're going to cast it anyway, can't
27   I just ignore the fact that the integer doesn't fit?
28*)
29
30(* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size
31 *  m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal
32 * to [exp]. If it fails, it returns None. *)
33let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
34match n return λn. BitVector (n+S m) → option (BitVector (S m)) with
35[ O ⇒ λv. Some ? v
36| S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ?
37] v.
38
39lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'.
40#n #m #exp #v #v' #H whd in H:(??%?); lapply H -H
41cases (eq_b ? exp)
42[ 1: #H whd in H:(??%?); //
43| 2: #H normalize in H; destruct ] qed.
44
45lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'.
46  reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v.
47#n #m elim n
48[ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >split_O_n //
49| 2: #n' #Hind #exp #v #v' #H >truncate_tail
50 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed.
51 
52lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?.
53#n #m #exp #v elim (reduce_bits n m exp v)
54[ 1: %2 //
55| 2: #v' %1 @(ex_intro … v') // ] qed.
56
57(* pred_bitsize_of_intsize I32 = 31, … *)
58definition pred_bitsize_of_intsize : intsize → nat ≝
59λsz. pred (bitsize_of_intsize sz).
60
61definition signed : signedness → bool ≝
62λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ].
63
64(* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg]
65 * into an integer of size [sz'] of signedness [sg'].
66 * - It first proceeds by comparing the source and target width: if the target width is strictly superior
67 *   to the source width, the conversion fails.
68 * - If the size is equal, the argument is returned as-is.
69 * - If the target type is strictly smaller than the source, it tries to squeeze the integer to
70 *   the desired size.
71*)
72let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝
73  let bit ≝ signed sg ∧ head' … i in
74  (* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args.
75   * if x < y, nat_compare x y = lt(x, y-(x+1)) 
76   * if x = y, nat_compare x y = eq x
77   * if x > y, nat_compare x y = gt(x-(y+1), y) *)
78  match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz')
79      return λn,m,x.BitVector (S n) → option (BitVector (S m)) with
80  [ nat_lt _ _ ⇒ λi. None ?   (* refuse to make constants larger *)
81  | nat_eq _ ⇒ λi. Some ? i
82  | nat_gt x y ⇒ λi.
83      (* Here, we have [x]=31-([y]+1) and [y] ∈ {15; 7} OR [x] = 15-(7+1) and [y] = 7. I.e.: x=15,y=15 or x=23,y=7 or x=7,y=7.
84       * In [reduce_bits n m bit i], [i] is supposed to have type BitVector n + (S m). Since its type is here (S x) + (S y),
85       * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent.
86       * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits.
87       * Otherwise, it tries to remove the (S x) first "0" bits.
88       *)
89      match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with
90      [ Some i' ⇒
91        if signed sg' then
92          if eq_b bit (head' … i') then
93            Some ? i'
94          else None ?
95        else Some ? i'
96      | None ⇒ None ?
97      ]
98  ] i.
99>(commutative_plus_faster (S x)) @refl
100qed.
101
102
103(* /!\ This lemma uses the "uniqueness of identity proofs" K axiom. I've tried doing a proper
104 * induction on t but it turns out to be a non-well-founded pandora box. /!\ *)
105lemma type_eq_dec_identity : ∀t. type_eq_dec t t = inl ?? (refl ? t).
106#t elim (type_eq_dec t t)
107[ 1: @streicherK //
108| 2: #H elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.
109
110
111lemma sign_eq_dec : ∀s1,s2:signedness. (s1 = s2) ∨ (s1 ≠ s2).
112* * /2/ %2 % #H destruct
113qed.
114
115lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
116* normalize //
117qed.
118
119lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
120* normalize //
121qed.
122
123lemma type_eq_identity : ∀t. type_eq t t = true.
124#t normalize elim (type_eq_dec t t)
125[ 1: #Heq normalize //
126| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.
127
128lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
129#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
130[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
131| 2: #Hneq' normalize // ] qed.
132
133lemma type_eq_eq : ∀t1, t2. type_eq t1 t2 = true → t1 = t2.
134#t1 #t2 whd in match (type_eq ??); cases (type_eq_dec t1 t2) normalize
135[ 1: // | 2: #_ #H destruct ] qed.
136
137definition size_le ≝ λsz1,sz2.
138match sz1 with
139[ I8 ⇒ True
140| I16 ⇒
141  match sz2 with
142  [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ]
143| I32 ⇒
144  match sz2 with
145  [ I32 ⇒ True | _ ⇒ False ]
146].
147
148definition size_lt ≝ λsz1,sz2.
149match sz1 with
150[ I8 ⇒
151  match sz2 with
152  [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ]
153| I16 ⇒
154  match sz2 with
155  [ I32 ⇒ True | _ ⇒ False ]
156| I32 ⇒ False
157].
158
159lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)).
160* * normalize /2/ /3/
161qed.
162
163lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1).
164* * normalize /2/ /3/
165qed.
166
167(* This function already exists in prop, we want it in type. *)
168definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2).
169* * normalize // qed.
170
171lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False.
172* * normalize
173#H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed.
174 
175
176(* This defines necessary conditions for [src_expr] to be coerced to "target_ty".
177 * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *)
178definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg.
179match size_lt_dec target_sz src_sz with
180[ inl Hlt ⇒ true
181| inr Hnlt ⇒
182  match sz_eq_dec target_sz src_sz with
183  [ inl Hsz_eq ⇒
184    match sign_eq_dect src_sg target_sg with
185    [ inl Hsg_eq ⇒ false
186    | inr Hsg_neq ⇒ true
187    ]           
188  | inr Hsz_neq ⇒ false
189  ]
190].
191
192(* Used to inject boolean functions in invariants. *)
193definition is_true : bool → Prop ≝ λb.
194match b with
195[ true ⇒ True
196| false ⇒ False ].
197
198(* An useful lemma to cull out recursive calls: the guard forces the target type to be different from the origin type. *)
199
200(* aux lemma *)
201lemma size_lt_dec_not_refl : ∀sz. ∃H. size_lt_dec sz sz = inr ??H.
202* normalize @(ex_intro … (nmk False (λauto:False.auto))) // qed.
203
204
205
206lemma necessary_conditions_spec :
207  ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) →
208      ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)).
209#src_sz #src_sg #target_sz #target_sg
210whd in match (necessary_conditions ????);
211cases (size_lt_dec target_sz src_sz) normalize nodelta
212[ 1: #Hlt #_ %1 //
213| 2: #Hnlt
214     cases (sz_eq_dec target_sz src_sz) normalize nodelta
215     [ 2: #_ #Hcontr destruct
216     | 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta
217       [ 1: #_ #Hcontr destruct
218       | 2: #Hsg_neq #_ %2 destruct /2/ ]
219     ]
220] qed.     
221
222
223
224(* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an
225 * integer value smaller but containing the same stuff than [r2] then all is well.
226 * If the two evaluations are erroneous, all is well too. *)
227definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res (val×trace).
228match r1 with
229[ OK res1 ⇒
230  match r2 with
231  [ OK res2 ⇒
232    let 〈v1, tr1〉 ≝ res1 in
233    let 〈v2, tr2〉 ≝ res2 in
234    match v1 with
235    [ Vint sz1 v1 ⇒
236       match v2 with
237       [ Vint sz2 v2 ⇒
238         match sz_eq_dec sz1 src_sz with
239         [ inl Hsrc_eq ⇒
240            match sz_eq_dec sz2 dst_sz with
241            [ inl Hdst_eq ⇒
242                v2 = cast_int_int sz1 sg sz2 v1
243                ∧ tr1 = tr2
244                ∧ size_le dst_sz src_sz
245            | inr _ ⇒ False ]
246         | inr _ ⇒ False ]
247       | _ ⇒ False ]
248    | _ ⇒ False ]
249  | _ ⇒ False ]
250| Error errmsg1 ⇒ True (* Simulation ... *)
251(*  match r2 with
252  [ OK _ ⇒ False
253  | Error errmsg2 ⇒ True (* Note that the two expressions may fail for different reasons ... Too lax maybe ? *)
254  ] *)
255].
256
257lemma smaller_integer_val_spec : ∀src_sz,dst_sz,sg,val1,val2,tr1,tr2.
258    smaller_integer_val src_sz dst_sz sg (OK ? 〈val1, tr1〉) (OK ? 〈val2, tr2〉) →
259    ∃v1,v2. val1 = Vint src_sz v1 ∧ val2 = Vint dst_sz v2 ∧
260    v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz.
261#src_sz #dst_sz #sg #val1 #val2 #tr1 #tr2
262whd in ⊢ (% → ?);
263elim val1 normalize nodelta
264[ 1: #Hcontr @(False_ind … Hcontr) | 3,4,5: #foo #Hcontr @(False_ind … Hcontr)
265| 2: #size1 #int1 cases val2
266     [ 1: #Hcontr @(False_ind … Hcontr) | 3,4,5: #foo #Hcontr @(False_ind … Hcontr)
267     | 2: #size2 #int2 normalize nodelta
268          cases (sz_eq_dec size1 src_sz)
269          cases (sz_eq_dec size2 dst_sz)
270          [ 2,3,4: #Hneq #Heq #Hcontr @(False_ind … Hcontr)
271          | 1: #Heq1 #Heq2 * * #Hcast #Htrace #H destruct
272               @(ex_intro … int1) @(ex_intro … (cast_int_int src_sz sg dst_sz int1))
273               try @conj try @conj try @conj try @conj try @conj try @conj //
274          ]
275     ]
276] qed.   
277   
278definition is_integer_type ≝ λty.
279match ty with
280[ Tint _ _ ⇒ True
281| _ ⇒ False
282].
283
284
285
286inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
287| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2
288| SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2.
289
290inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
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 : ∀src_sz,src_sg.
298     (typeof e1) = (Tint src_sz src_sg) →
299     (typeof e2) = (Tint target_sz target_sg) →     
300     (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
301     simplify_inv ge en m e1 e2 target_sz target_sg true.
302   
303
304(* This lemma proves that simplify_int actually implements an integer cast. This is central to the proof of correctness. *)
305(* The case 4 can be merged with cases 7 and 8.  *)
306lemma 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.
307* *
308[ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct //
309| 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct  whd in Hsimp:(??%?); destruct *)
310| 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
311    normalize in match (signed ?) in Hsimp;
312    normalize in match (S (plus ??)) in Hsimp;
313    normalize in match (plus 7 8) in Hsimp;
314    lapply Hsimp -Hsimp
315    cases (head' bool 15 i)
316    normalize in match (andb ??);
317    [ 1,3: elim (reduce_bits_dec 8 7 true i)
318      [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
319        [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl
320        | 2: #H destruct normalize @refl ]
321      | 2,4: #Heq >Heq normalize nodelta #H destruct ]
322    | 2,4,5,6,7,8:
323      elim (reduce_bits_dec 8 7 false i)
324      [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
325        [ 1,3,4: cases (eq_b false ?) normalize nodelta
326         #H destruct normalize @refl
327        | 2,5,6: #H destruct normalize @refl ]
328      | 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct
329      ]
330    ]
331| 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl
332| 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
333    normalize in match (signed ?) in Hsimp;
334    normalize in match (S (plus ??)) in Hsimp;   
335    normalize in match (plus 7 24) in Hsimp;
336    lapply Hsimp -Hsimp
337    cases (head' bool ? i)   
338    normalize in match (andb ??);
339    [ 1,3,9,11:
340      [ 1,2: (elim (reduce_bits_dec 24 7 true i)) | 3,4: (elim (reduce_bits_dec 16 15 true i)) ]
341      [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
342        [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl
343        | 2,4: #H destruct normalize @refl ]
344      | 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ]
345    | 2,4,5,6,7,8,10,12,13,14,15,16:
346      [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i)
347      | 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ]
348      [ 1,3,5,7,9,11,13,15,17,19,21,23:
349        * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
350        [ 1,3,4,7,9,10:
351          cases (eq_b false ?) normalize nodelta #H destruct normalize @refl
352        | 2,5,6,8,11,12: #H destruct normalize @refl ]
353      | 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct
354      ]
355    ]
356] qed.
357
358(* Facts about cast_int_int *)
359
360(* copied from AssemblyProof *)
361lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
362 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
363 #n #hd #tl #abs @⊥ destruct (abs)
364qed.
365
366lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
367 ∃hd.∃tl.v ≃ VCons A n hd tl.
368 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
369 [ #abs @⊥ destruct (abs)
370 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
371qed.
372
373lemma vector_append_zero:
374  ∀A,m.
375  ∀v: Vector A m.
376  ∀q: Vector A 0.
377    v = q@@v.
378  #A #m #v #q
379  >(Vector_O A q) %
380qed.
381
382lemma prod_eq_left:
383  ∀A: Type[0].
384  ∀p, q, r: A.
385    p = q → 〈p, r〉 = 〈q, r〉.
386  #A #p #q #r #hyp
387  >hyp %
388qed.
389
390lemma prod_eq_right:
391  ∀A: Type[0].
392  ∀p, q, r: A.
393    p = q → 〈r, p〉 = 〈r, q〉.
394  #A #p #q #r #hyp
395  >hyp %
396qed.
397
398corollary prod_vector_zero_eq_left:
399  ∀A, n.
400  ∀q: Vector A O.
401  ∀r: Vector A n.
402    〈q, r〉 = 〈[[ ]], r〉.
403  #A #n #q #r
404  generalize in match (Vector_O A q …);
405  #hyp
406  >hyp in ⊢ (??%?);
407  %
408qed.
409 
410lemma split_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
411# A #m #n elim m
412[ 1: normalize #v
413  elim (Vector_Sn ?? v) #hd * #tl #Eq
414  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
415  >Eq normalize //
416| 2: #n' #Hind #v
417  elim (Vector_Sn ?? v) #hd * #tl #Eq
418  elim (Hind tl)
419  #tl1 * #tl2 #Eq_tl
420  @(ex_intro … (hd ::: tl1))
421  @(ex_intro … tl2) 
422  destruct normalize //
423] qed.
424
425lemma split_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
426# A #m #n elim m
427[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
428| 2: #n' #Hind #v
429  elim (Vector_Sn ?? v) #hd * #tl #Eq
430  elim (Hind tl)
431  #tl1 * #tl2 #Eq_tl
432  @(ex_intro … (hd ::: tl1))
433  @(ex_intro … tl2) 
434  destruct normalize //
435] qed.
436
437lemma split_zero:
438  ∀A,m.
439  ∀v: Vector A m.
440    〈[[]], v〉 = split A 0 m v.
441  #A #m #v
442  elim v
443  [ %
444  | #n #hd #tl #ih
445    normalize in ⊢ (???%); %
446  ]
447qed.
448
449
450lemma split_zero2:
451  ∀A,m.
452  ∀v: Vector A m.
453    〈[[]], v〉 = split' A 0 m v.
454  #A #m #v
455  elim v
456  [ %
457  | #n #hd #tl #ih
458    normalize in ⊢ (???%); %
459  ]
460qed.
461
462(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
463 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
464axiom split_succ:
465  ∀A, m, n.
466  ∀l: Vector A m.
467  ∀r: Vector A n.
468  ∀v: Vector A (m + n).
469  ∀hd.
470    v = l@@r → (〈l, r〉 = split ? m n v → 〈hd:::l, r〉 = split ? (S m) n (hd:::v)).
471
472axiom split_succ2:
473  ∀A, m, n.
474  ∀l: Vector A m.
475  ∀r: Vector A n.
476  ∀v: Vector A (m + n).
477  ∀hd.
478    v = l@@r → (〈l, r〉 = split' ? m n v → 〈hd:::l, r〉 = split' ? (S m) n (hd:::v)).
479     
480lemma split_prod2:
481  ∀A,m,n.
482  ∀p: Vector A (m + n).
483  ∀v: Vector A m.
484  ∀q: Vector A n.
485    p = v@@q → 〈v, q〉 = split' A m n p.
486  #A #m
487  elim m
488  [ #n #p #v #q #hyp
489    >hyp <(vector_append_zero A n q v)
490    >(prod_vector_zero_eq_left A …)
491    @split_zero2
492  | #r #ih #n #p #v #q #hyp
493    >hyp
494    cases (Vector_Sn A r v)
495    #hd #exists
496    cases exists
497    #tl #jmeq >jmeq
498    @split_succ2 [1: % |2: @ih % ]
499  ]
500qed.
501
502lemma split_prod:
503  ∀A,m,n.
504  ∀p: Vector A (m + n).
505  ∀v: Vector A m.
506  ∀q: Vector A n.
507    p = v@@q → 〈v, q〉 = split A m n p.
508  #A #m
509  elim m
510  [ #n #p #v #q #hyp
511    >hyp <(vector_append_zero A n q v)
512    >(prod_vector_zero_eq_left A …)
513    @split_zero
514  | #r #ih #n #p #v #q #hyp
515    >hyp
516    cases (Vector_Sn A r v)
517    #hd #exists
518    cases exists
519    #tl #jmeq >jmeq
520    @split_succ [1: % |2: @ih % ]
521  ]
522qed.
523
524
525(* Stolen from AssemblyProof.ma *)
526lemma super_rewrite2:
527 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
528  ∀P: ∀m. Vector A m → Prop.
529   n=m → v1 ≃ v2 → P n v1 → P m v2.
530 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
531qed.
532
533lemma vector_cons_append:
534  ∀A: Type[0].
535  ∀n: nat.
536  ∀e: A.
537  ∀v: Vector A n.
538    e ::: v = [[ e ]] @@ v.
539  # A # N # E # V
540  elim V
541  [ normalize %
542  | # NN # AA # VV # IH
543    normalize
544    %
545qed.
546
547lemma vector_cons_append2:
548  ∀A: Type[0].
549  ∀n, m: nat.
550  ∀v: Vector A n.
551  ∀q: Vector A m.
552  ∀hd: A.
553    hd:::(v@@q) = (hd:::v)@@q.
554  #A #n #m #v #q
555  elim v
556  [ #hd %
557  | #n' #hd' #tl' #ih #hd' <ih %
558  ]
559qed.
560
561lemma jmeq_cons_vector_monotone:
562  ∀A: Type[0].
563  ∀m, n: nat.
564  ∀v: Vector A m.
565  ∀q: Vector A n.
566  ∀prf: m = n.
567  ∀hd: A.
568    v ≃ q → hd:::v ≃ hd:::q.
569  #A #m #n #v #q #prf #hd #E
570  @(super_rewrite2 A … E)
571  [ assumption | % ]
572qed.
573
574lemma vector_associative_append:
575  ∀A: Type[0].
576  ∀n, m, o:  nat.
577  ∀v: Vector A n.
578  ∀q: Vector A m.
579  ∀r: Vector A o.
580    ((v @@ q) @@ r)
581    ≃
582    (v @@ (q @@ r)).
583  #A #n #m #o #v #q #r
584  elim v
585  [ %
586  | #n' #hd #tl #ih
587    <(vector_cons_append2 A … hd)
588    @jmeq_cons_vector_monotone
589    //
590  ]
591qed.
592
593lemma tail_eat_cons : ∀A. ∀n. ∀hd:A. ∀v:Vector A n. tail A n (hd ::: v) = v.
594#A #n #hd #v normalize //
595qed.
596
597lemma tail_eat_pad : ∀A. ∀padelt. ∀padlen, veclen. ∀v:Vector A veclen.
598  tail A ? (pad_vector A padelt (S padlen) veclen v) = pad_vector A padelt padlen veclen v.
599# A #padelt #padlen #veclen #v
600normalize //
601qed.
602
603lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
604#s1 #v normalize elim s1 normalize nodelta
605normalize in v;
606elim (split_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
607[ 2,4: //
608| 1,3: #l * #r normalize nodelta #Eq1
609       <(split_prod bool 16 16 … Eq1)
610       elim (split_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
611       [ 2,4: //
612       | 1,3: #lr * #rr normalize nodelta #Eq2
613              <(split_prod bool 8 8 … Eq2)
614              cut (v = (l @@ lr) @@ rr)
615              [ 1,3 : destruct >(vector_associative_append ? 16 8) //
616              | 2,4: #Hrewrite destruct
617                     <(split_prod bool 24 8 … Hrewrite) @refl
618              ]
619       ]
620] qed.
621
622lemma 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.
623#s1 #s2 * * #v elim s1 elim s2
624normalize #H try @refl
625@(False_ind … H)
626qed.
627
628lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v.
629* * #v normalize // qed.
630
631lemma 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).
632#s1 #s2 #v >cast_decompose >cast_idempotent
633[ 1: @refl | 2: // ]
634qed.
635
636lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
637   size_lt c_sz a_sz → size_lt c_sz b_sz →
638   (cast_int_int a_sz a_sg c_sz val =
639        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).       
640* #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??);
641#Hlt1 #Hlt2
642[ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27:
643  @(False_ind … Hlt1) @(False_ind … Hlt2)
644| 13,25,26: >cast_identity elim a_sg elim b_sg normalize //
645| 22: normalize elim b_sg elim a_sg normalize
646      normalize in val;
647      elim (split_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
648      [ 2,4,6,8: normalize //
649      | 1,3,5,7: #left * #right normalize #Eq1
650                 <(split_prod bool 16 16 … Eq1)
651                 elim (split_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
652                 [ 2,4,6,8: //
653                 | 1,3,5,7: #rightleft * #rightright normalize #Eq2
654                            <(split_prod bool 8 8 … Eq2)
655                            cut (val = (left @@ rightleft) @@ rightright)
656                            [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
657                            | 2,4,6,8: #Hrewrite destruct
658                                       <(split_prod bool 24 8 … Hrewrite) @refl
659                            ]
660                 ]
661     ]
662| 16: elim b_sg elim a_sg >cast_collapse @refl
663] qed.
664
665lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
666   size_le c_sz a_sz → size_le c_sz b_sz →
667   (cast_int_int a_sz a_sg c_sz val =
668        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).
669#a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b
670cases (size_lt_dec c_sz a_sz)
671cases (size_lt_dec c_sz b_sz)
672[ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb)
673| 2: #Hnltb #Hlta
674  cases (size_not_lt_to_ge  … Hnltb)
675  [ 1: #Heq destruct >cast_identity //
676  | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb))
677  ]
678| 3: #Hltb #Hnlta 
679  cases (size_not_lt_to_ge  … Hnlta)
680  [ 1: #Heq destruct >cast_idempotent //
681  | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
682  ]
683| 4: #Hnltb #Hnlta
684  cases (size_not_lt_to_ge  … Hnlta) 
685  cases (size_not_lt_to_ge  … Hnltb)
686  [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity //
687  | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb))
688  | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
689  | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
690  ]
691] qed.
692
693let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝
694match v with
695[ None ⇒ None ?
696| Some v ⇒
697  match v with
698  [ Vint sz i ⇒
699    match sz_eq_dec sz expected_size with
700    [ inl Heq ⇒ Some ??
701    | inr _ ⇒ None ?
702    ]
703  | _ ⇒ None ?
704  ]
705].
706>Heq in i; #i @i qed.
707
708(* cast_int_int behaves as truncate (≃ split) when downsizing *)
709(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)
710
711lemma split_to_truncate : ∀m,n,i. (\snd  (split bool m n i)) = truncate  m n i.
712#m #n #i normalize // qed.
713
714(* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *)
715
716lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
717                               (addition_n (bitsize_of_intsize target_sz)
718                                    (cast_int_int src_sz sg target_sz lhs_int)
719                                    (cast_int_int src_sz sg target_sz rhs_int)
720                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
721#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
722elim src_sz in Hlt lhs_int rhs_int; elim target_sz
723[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
724| *: elim sg #_
725  normalize in match (bitsize_of_intsize ?);
726  normalize in match (bitsize_of_intsize ?);
727  #lint #rint
728  normalize in match (cast_int_int ????);
729  normalize in match (cast_int_int ????);
730  whd in match (addition_n ???);
731  whd in match (addition_n ???) in ⊢ (???%);
732  >split_to_truncate >split_to_truncate
733  <truncate_add_with_carries
734  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
735  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false);
736  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false);
737  ]
738  * #result #carry
739  normalize nodelta //
740qed.
741
742lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
743                               (addition_n (bitsize_of_intsize target_sz)
744                                    (cast_int_int src_sz sg target_sz lhs_int)
745                                    (cast_int_int src_sz sg target_sz rhs_int)
746                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
747#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
748>cast_identity >cast_identity >cast_identity // qed.
749
750lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
751                               (addition_n (bitsize_of_intsize target_sz)
752                                    (cast_int_int src_sz sg target_sz lhs_int)
753                                    (cast_int_int src_sz sg target_sz rhs_int)
754                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
755#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
756cases (sz_eq_dec target_sz src_sz)
757[ 1: #Heq @(integer_add_cast_eq … Heq)
758| 2: #Hneq cut (size_lt target_sz src_sz)
759     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
760           #_ * #H @(H … (refl ??))
761     | 2: #Hlt @(integer_add_cast_lt … Hlt)
762     ]
763] qed.
764
765lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl.
766#l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len
767@(ex_intro … tl)
768>Heq >Heq
769elim (split_eq2 … tl) #l * #r #Eq
770normalize
771 <(split_prod bool n m tl l r Eq)
772 <(split_prod2 bool n m tl l r Eq)
773 normalize //
774qed.
775
776
777lemma 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).
778#m elim m
779[ 1: #n #i normalize in i;
780     whd in match (truncate ???);
781     whd in match (truncate ???) in ⊢ (???%);
782     <split_zero <split_zero //
783| 2: #m' #Hind #n #i normalize in i;
784     elim (Vector_Sn … i) #hd * #tl #Heq     
785     whd in match (two_complement_negation (S ?) ?);     
786     >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?);
787     whd in match (two_complement_negation ??) in ⊢ (??%?);
788     lapply (Hind ? tl) #H
789     whd in match (two_complement_negation ??) in H;
790(* trying to reduce add_with_carries *)     
791     normalize in match (S m'+n);
792     whd in match (zero ?) in ⊢ (???%);
793     >Heq in match (negation_bv ??) in ⊢ (???%);
794     whd in match (negation_bv ??) in ⊢ (???%);
795     >add_with_carries_unfold in ⊢ (???%);
796(*     >truncate_tail *)
797     normalize in ⊢ (???%);
798     cases hd normalize nodelta
799     [ 1,2: <add_with_carries_unfold  in ⊢ (???%); (* Good. Some progress. *)
800          (* try to transform the rhs of H into what we need. *)     
801          whd in match (two_complement_negation ??) in H:(???%);
802          lapply H -H
803          generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true);
804          * #Left #Right normalize nodelta
805          #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒  ?])))));
806          #b >(split_to_truncate (S m')) >truncate_tail
807          cases b
808          normalize nodelta
809          normalize in match (tail ???); @H
810     ]
811] qed. (* This was painful. *)
812     
813lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
814                               (subtraction (bitsize_of_intsize target_sz)
815                                    (cast_int_int src_sz sg target_sz lhs_int)
816                                    (cast_int_int src_sz sg target_sz rhs_int)
817                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
818#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
819elim src_sz in Hlt lhs_int rhs_int; elim target_sz
820[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
821| *: elim sg #_
822  normalize in match (bitsize_of_intsize ?);
823  normalize in match (bitsize_of_intsize ?);
824  #lint #rint
825  normalize in match (cast_int_int ????);
826  normalize in match (cast_int_int ????);
827  whd in match (subtraction ???);
828  whd in match (subtraction ???) in ⊢ (???%);
829  >split_to_truncate >split_to_truncate
830  >integer_neg_trunc <truncate_add_with_carries
831  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
832  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false);
833  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false);
834  ]
835  * #result #carry
836  normalize nodelta //
837qed.
838
839lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
840                               (subtraction (bitsize_of_intsize target_sz)
841                                    (cast_int_int src_sz sg target_sz lhs_int)
842                                    (cast_int_int src_sz sg target_sz rhs_int)
843                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
844#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
845>cast_identity >cast_identity >cast_identity //
846qed.
847
848lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
849                               (subtraction (bitsize_of_intsize target_sz)
850                                    (cast_int_int src_sz sg target_sz lhs_int)
851                                    (cast_int_int src_sz sg target_sz rhs_int)
852                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
853#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
854cases (sz_eq_dec target_sz src_sz)
855[ 1: #Heq @(integer_sub_cast_eq … Heq)
856| 2: #Hneq cut (size_lt target_sz src_sz)
857     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
858           #_ * #H @(H … (refl ??))
859     | 2: #Hlt @(integer_sub_cast_lt … Hlt)
860     ]
861] qed.
862     
863lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg.
864* * // qed.
865
866lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg.
867* * // qed.
868
869(* This ought to be somewhere else. Lemma used in proving the correctness of the Binop case. *)
870lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
871* * normalize #H @conj // qed.
872
873lemma 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.
874* #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.
875
876(* Operations where it is safe to use a smaller integer type on the assumption
877   that we would cast it down afterwards anyway. *)
878definition binop_simplifiable ≝
879λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].
880
881notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)"
882 with precedence 10
883for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }.
884
885notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)"
886 with precedence 10
887for @{ match $t return λx.x = $t → ? with
888       [ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}.
889         match ${fresh a} return λx.x = ${fresh a} → ? with
890         [ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a})
891       ] (refl ? $t)
892      }.
893
894notation > "hvbox('do' «ident x, ident y» 'as' ident E ← t; break s)"
895 with precedence 48
896for @{ match $t with
897       [ Some ${fresh res} ⇒
898         match ${fresh res} return λx.x = ${fresh res} → ? with
899         [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}. $s
900         ] (refl ? ${fresh res})
901       | None ⇒ None ?
902       ] }.
903                       
904                       
905(* This function will make your eyes bleed. You've been warned.
906 * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by
907 * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either
908   what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original
909   expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper.
910 * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable.
911 * This function is slightly more conservative than the original one, but this should be incrementally
912 * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction).
913 * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something
914 * more or less "modular", case-by-case wise.
915 *)
916let rec simplify_expr2 (e:expr) (target_sz:intsize) (target_sg:signedness)
917  : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝
918match e return λx. x = e → ? with
919[ Expr ed ty ⇒ λHexpr_eq.
920  match ed return λx. ed = x → ? with
921  [ Econst_int cst_sz i ⇒ λHdesc_eq.
922    match ty return λx. x=ty → ? with
923    [ Tint ty_sz sg ⇒ λHexprtype_eq.
924      (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *)
925      match sz_eq_dec cst_sz ty_sz with
926      [ inl Hsz_eq ⇒       
927        match type_eq_dec ty (Tint target_sz target_sg) with
928        [ inl Hdonothing   ⇒ «〈true, e〉, ?»
929        | inr Hdosomething ⇒
930          (* Do the actual useful work *)
931          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
932          [ Some i' ⇒ λHsimpl_eq.
933            «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?»
934          | None    ⇒ λ_.
935            «〈false, e〉, ?»
936          ] (refl ? (simplify_int cst_sz target_sz sg target_sg i))
937        ]
938      | inr _ ⇒ (* The expression is ill-typed. *)
939        «〈false, e〉, ?»
940      ]
941    | _ ⇒ λ_.
942      «〈false, e〉, ?»
943    ] (refl ? ty)   
944  | Ederef e1 ⇒ λHdesc_eq.
945      let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in 
946      «〈false, Expr (Ederef e2) ty〉, ?»           
947  | Eaddrof e1 ⇒ λHdesc_eq.
948      let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
949      «〈false, Expr (Eaddrof e2) ty〉, ?»
950  | Eunop op e1 ⇒ λHdesc_eq.
951     let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
952      «〈false, Expr (Eunop op e2) ty〉, ?»
953  | Ebinop op lhs rhs ⇒ λHdesc_eq.
954      (* Type equality is enforced to prove the equalities needed in return by the invariant. *)
955      match binop_simplifiable op
956      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)))
957      with
958      [ true ⇒ λHop_simplifiable_eq.
959        match assert_type_eq ty (typeof lhs) with
960        [ OK Hty_eq_lhs ⇒
961            match assert_type_eq (typeof lhs) (typeof rhs) with
962            [ OK Htylhs_eq_tyrhs ⇒
963                let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr2 lhs target_sz target_sg in
964                let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr2 rhs target_sz target_sg in
965                match desired_type_lhs ∧ desired_type_rhs
966                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)))
967                with
968                [ true ⇒ λHdesired_eq.
969                  «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?»
970                | false ⇒ λHdesired_eq.
971                  let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
972                  let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
973                  «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
974                ] (refl ? (desired_type_lhs ∧ desired_type_rhs))
975            | Error _ ⇒
976                let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
977                let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
978                «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?» 
979            ]                   
980        | Error _ ⇒
981            let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
982            let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
983             «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»         
984        ]
985      | false ⇒ λHop_simplifiable_eq.
986        let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
987        let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
988          «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
989      ] (refl ? (binop_simplifiable op))
990  | Ecast cast_ty castee ⇒ λHdesc_eq.
991      match cast_ty return λx. x = cast_ty → ? with
992      [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
993        match type_eq_dec ty cast_ty with
994        [ inl Hcast_eq ⇒
995          match necessary_conditions cast_sz cast_sg target_sz target_sg
996          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)))
997          with
998          [ true ⇒ λHconditions.
999              let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr2 castee target_sz target_sg in
1000              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))
1001              with
1002              [ true ⇒ λHdesired_eq.
1003                «〈true, castee1〉, ?»
1004              | false ⇒ λHdesired_eq.
1005                let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr2 castee cast_sz cast_sg in
1006                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))
1007                with
1008                [ true ⇒ λHdesired2_eq.
1009                  «〈false, castee2〉, ?»
1010                | false ⇒ λHdesired2_eq.
1011                  «〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
1012                ] (refl ? desired_type2)
1013              ] (refl ? desired_type)
1014          | false ⇒ λHconditions.
1015              let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr2 castee cast_sz cast_sg in
1016              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))
1017              with
1018              [ true ⇒ λHdesired2_eq.
1019                «〈false, castee2〉, ?»
1020              | false ⇒ λHdesired2_eq.
1021                «〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
1022              ] (refl ? desired_type2)
1023          ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg))
1024        | inr Hcast_neq ⇒
1025          (* inconsistent types ... *)
1026          let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
1027          «〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
1028        ]
1029      | _ ⇒ λHcast_ty_eq.
1030        let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
1031        «〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
1032      ] (refl ? cast_ty)     
1033  | Econdition cond iftrue iffalse ⇒ λHdesc_eq.
1034      let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in
1035      match assert_type_eq ty (typeof iftrue) with
1036      [ OK Hty_eq_iftrue ⇒
1037          match assert_type_eq (typeof iftrue) (typeof iffalse) with
1038          [ OK Hiftrue_eq_iffalse ⇒
1039              let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue      ≝ simplify_expr2 iftrue target_sz target_sg in
1040              let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr2 iffalse target_sz target_sg in         
1041              match desired_true ∧ desired_false
1042              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)))
1043              with
1044              [ true ⇒ λHdesired_eq.
1045                «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?»
1046              | false ⇒ λHdesired_eq.
1047                let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
1048                let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
1049                «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»     
1050              ] (refl ? (desired_true ∧ desired_false))
1051          | _ ⇒
1052            let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
1053            let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
1054            «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»           
1055          ]
1056      | _ ⇒
1057        let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
1058        let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
1059        «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»     
1060      ]
1061    (* Could probably do better with these, too. *)
1062  | Eandbool lhs rhs ⇒ λHdesc_eq.
1063      let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
1064      let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
1065      «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?»
1066  | Eorbool lhs rhs ⇒ λHdesc_eq.
1067      let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
1068      let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
1069      «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?»
1070  (* Could also improve Esizeof *)
1071  | Efield rec_expr f ⇒ λHdesc_eq.
1072      let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in
1073      «〈false,Expr (Efield rec_expr1 f) ty〉, ?»
1074  | Ecost l e1 ⇒ λHdesc_eq.
1075      (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *)
1076      (* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *)
1077      match type_eq_dec ty (typeof e1) with
1078      [ inl Heq ⇒
1079        let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr2 e1 target_sz target_sg in
1080        «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?»
1081      | inr Heq ⇒
1082        let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in
1083        «〈false, Expr (Ecost l e2) ty〉, ?»
1084      ]               
1085  | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
1086  | Evar id        ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
1087  | Esizeof t      ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?»
1088  ] (refl ? ed)
1089] (refl ? e)
1090
1091and simplify_inside (e:expr) : Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
1092                                                    ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
1093                                                    ∧ typeof e = typeof result) ≝
1094match e return λx. x = e → ? with
1095[ Expr ed ty ⇒ λHexpr_eq.
1096  match ed return λx. x = ed → ? with
1097  [ Ederef e1 ⇒ λHdesc_eq.
1098    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
1099    «Expr (Ederef e2) ty, ?»
1100  | Eaddrof e1 ⇒ λHdesc_eq.
1101    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
1102    «Expr (Eaddrof e2) ty, ?»
1103  | Eunop op e1 ⇒ λHdesc_eq.
1104    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
1105    «Expr (Eunop op e2) ty, ?»
1106  | Ebinop op lhs rhs ⇒ λHdesc_eq.
1107    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
1108    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
1109    «Expr (Ebinop op lhs1 rhs1) ty, ?»
1110  | Ecast cast_ty castee ⇒ λHdesc_eq.
1111    match type_eq_dec ty cast_ty with
1112    [ inl Hcast_eq ⇒
1113       match cast_ty return λx. x = cast_ty → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
1114                                                     ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
1115                                                     ∧ typeof e = typeof result)
1116       with
1117       [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
1118          let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in
1119          match success return λx. x = success → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
1120                                                       ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
1121                                                       ∧ typeof e = typeof result)
1122         with
1123         [ true ⇒ λHsuccess_eq.
1124           «castee1, ?»
1125         | false ⇒ λHsuccess_eq.
1126           «Expr (Ecast cast_ty castee1) ty, ?»
1127          ] (refl ? success)
1128       | _ ⇒ λHcast_ty_eq.
1129          «e, ?»
1130       ] (refl ? cast_ty)
1131    | inr Hcast_neq ⇒
1132       «e, ?»   
1133    ]   
1134  | Econdition cond iftrue iffalse ⇒ λHdesc_eq.
1135    let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in
1136    let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in
1137    let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in
1138    «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?»   
1139  | Eandbool lhs rhs ⇒ λHdesc_eq.
1140    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
1141    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
1142    «Expr (Eandbool lhs1 rhs1) ty, ?»     
1143  | Eorbool lhs rhs ⇒ λHdesc_eq.
1144    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
1145    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
1146    «Expr (Eorbool lhs1 rhs1) ty, ?»
1147  | Efield rec_expr f ⇒ λHdesc_eq.
1148    let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in
1149    «Expr (Efield rec_expr1 f) ty, ?»   
1150  | Ecost l e1 ⇒ λHdesc_eq.
1151    let «e2, Hequiv» as Eq ≝ simplify_inside e1 in
1152    «Expr (Ecost l e2) ty, ?»       
1153  | _ ⇒ λHdesc_eq.
1154    «e, ?»
1155  ] (refl ? ed)
1156] (refl ? e).
1157#ge #en #m
1158[ 1,3,5,6,7,8,9,10,11,12: %1 //
1159     cases (exec_expr ge en m e) #res
1160     try (@(SimOk ???) //)
1161| 13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
1162     try (@(SimOk ???) //)
1163| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct //
1164     whd in match (exec_expr ????); >eq_intsize_identity whd
1165     >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]     
1166| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) //
1167     whd in match (exec_expr ????);
1168     whd in match (exec_expr ????);
1169     >eq_intsize_identity >eq_intsize_identity whd
1170     >sz_eq_identity >sz_eq_identity whd @conj try @conj //     
1171     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
1172     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
1173| 15: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1174    [ 1: (* Proving preservation of the semantics for expressions. *)
1175      cases Hexpr_sim
1176      [ 2: (* Case where the evaluation of e1 as an expression fails *)     
1177        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/
1178      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1179        #Hsim %1 * #val #trace normalize #Hstep
1180        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧
1181                   (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val))
1182        [ 1: lapply Hstep -Hstep
1183             cases (exec_expr ge en m e1)
1184             [ 1: * #val' #trace' normalize nodelta
1185                  cases val' normalize nodelta
1186                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
1187                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
1188                       cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq;
1189                       normalize nodelta
1190                       [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ]
1191                  ]
1192             | 2: normalize nodelta #errmesg #Hcontr destruct
1193             ]
1194        | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr
1195             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)
1196                       ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val))
1197             [ 1: @(ex_intro … e1_ptr) @conj
1198                  [ 1: @Hsim // | 2: // ]
1199             | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr
1200                normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl
1201             ]
1202        ]
1203     ]
1204   | 2: (* Proving the preservation of the semantics for lvalues. *)
1205      cases Hexpr_sim
1206      [ 2: (* Case where the evaluation of e1 as an lvalue fails *)
1207        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/
1208      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1209        #Hsim %1 * * #block #offset #trace normalize #Hstep       
1210        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset)
1211        [ 1: lapply Hstep -Hstep
1212             cases (exec_expr ge en m e1)
1213             [ 1: * #val' #trace' normalize nodelta
1214                  cases val' normalize nodelta
1215                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
1216                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
1217                       destruct try @conj try @conj //
1218                  ]
1219             | 2: normalize nodelta #errmesg #Hcontr destruct
1220             ]
1221        | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset
1222             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)  ∧ pblock ptr1 = block ∧ poff ptr1 = offset)
1223             [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim //
1224             | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset
1225                normalize >He2_exec normalize nodelta //
1226             ]
1227        ]
1228     ]
1229   ]
1230| 16: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1231    [ 1: (* Proving preservation of the semantics for expressions. *)
1232      cases Hlvalue_sim
1233      [ 2: (* Case where the evaluation of e1 as an expression fails *)     
1234        * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2/
1235      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1236        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
1237        cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
1238                                 (pointer_compat_dec block r = inl ?? pc) ∧
1239                                 (ty = Tpointer r ptype) ∧
1240                                  val = Vptr (mk_pointer r block pc offset))
1241        [ 1: lapply Hstep -Hstep
1242             cases (exec_lvalue ge en m e1)
1243             [ 1: * * #block #offset #trace' normalize nodelta
1244                  cases ty
1245                  [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
1246                  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
1247                  normalize nodelta try (#Heq destruct)
1248                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty)
1249                  cases (pointer_compat_dec block rg) in Heq; normalize
1250                  [ 2: #Hnotcompat #Hcontr destruct
1251                  | 1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ]
1252             | 2: normalize nodelta #errmesg #Hcontr destruct
1253             ]
1254        | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq
1255             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
1256             >Hptr_compat normalize nodelta //
1257        ]
1258     ]
1259   | 2: (* Proving preservation of the semantics of lvalues. *)
1260      normalize @SimFail /2/
1261   ]
1262| 17: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1263      [ 1: whd in match (exec_expr ge en m (Expr ??));
1264           whd in match (exec_expr ge en m (Expr ??));
1265           cases Hexpr_sim           
1266           [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2/
1267           | 1: cases (exec_expr ge en m e1)
1268                [ 2: #error #Hexec normalize nodelta @SimFail /2/
1269                | 1: * #val #trace #Hexec
1270                     >(Hexec ? (refl ? (OK ? 〈val,trace〉)))
1271                     normalize nodelta @SimOk #a >Htype_eq #H @H
1272                ]
1273           ]
1274      | 2: normalize @SimFail /2/
1275      ]   
1276| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
1277      inversion (Hinv_lhs ge en m)
1278      [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true
1279           #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct
1280      | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_
1281           inversion (Hinv_rhs ge en m)
1282           [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_
1283                <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct
1284           | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_
1285                @(Inv_coerce_ok  ge en m … target_sz target_sg lhs_src_sz lhs_src_sg)
1286                [ 1: >Htype_lhs //
1287                | 2: //
1288                | 3: whd in match (exec_expr ??? (Expr ??));
1289                     whd in match (exec_expr ??? (Expr ??));
1290                     (* Enumerate all the cases for the evaluation of the source expressions ... *)
1291                     cases (exec_expr ge en m lhs) in Hsmaller_lhs;
1292                     [ 2: #error normalize //
1293                     | 1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1)
1294                          [ 2: #error normalize #H @(False_ind … H)
1295                          | 1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs
1296                               elim (smaller_integer_val_spec … Hsmaller_lhs)
1297                               #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size
1298                               cases (exec_expr ge en m rhs) in Hsmaller_rhs;
1299                               [ 2: #error normalize //
1300                               | 1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1)
1301                                    [ 2: #error normalize #H @(False_ind … H)
1302                                    | 1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs
1303                                         elim (smaller_integer_val_spec … Hsmaller_rhs)
1304                                         #rhs_int * #rhs1_int * * * * #Hval_rhs #Hval_rhs1 #Hrhs_cast #Hrhs_trace #Hrhs_size
1305                                         whd in match (m_bind ?????);
1306                                         whd in match (m_bind ?????);
1307                                         <Htylhs_eq_tyrhs >Htype_lhs
1308                                         >Htype_lhs1 >Htype_rhs1
1309                                         cut (lhs_src_sz = rhs_src_sz ∧ lhs_src_sg = rhs_src_sg)
1310                                         [ 1: >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Hty_eq destruct (Hty_eq)
1311                                               @conj // ]
1312                                         * #Hsrc_sz_eq #Hsrc_sg_eq
1313                                         cases op in Hop_simplifiable_eq;
1314                                         normalize in match (binop_simplifiable ?);
1315                                         [ 3,4,5,6,7,8,9,10,11,12,13,14,15,16: #H destruct (H)
1316                                         | 1: #_ (* addition case *)
1317                                             >Hval_lhs >Hval_rhs destruct                                               
1318                                             whd in match (sem_binary_operation Oadd ?????);
1319                                             whd in match (sem_binary_operation Oadd ?????); normalize nodelta
1320                                             >classify_add_int >classify_add_int normalize nodelta
1321                                             >intsize_eq_elim_true >intsize_eq_elim_true
1322                                             whd in match (opt_to_res ???); whd in match (opt_to_res ???);
1323                                             whd in match (smaller_integer_val ?????); normalize nodelta
1324                                             >sz_eq_identity >sz_eq_identity normalize nodelta
1325                                             try @conj try @conj try //
1326                                             >integer_add_cast_le //                                             
1327                                         | 2: #_ (* subtraction case *)
1328                                             >Hval_lhs >Hval_rhs destruct       
1329                                             whd in match (sem_binary_operation Osub ?????);
1330                                             whd in match (sem_binary_operation Osub ?????); normalize nodelta
1331                                             >classify_sub_int >classify_sub_int normalize nodelta
1332                                             >intsize_eq_elim_true >intsize_eq_elim_true
1333                                             whd in match (opt_to_res ???); whd in match (opt_to_res ???);
1334                                             whd in match (smaller_integer_val ?????); normalize nodelta
1335                                             >sz_eq_identity >sz_eq_identity normalize nodelta
1336                                             try @conj try @conj try //
1337                                             >integer_sub_cast_le //
1338                                         ]
1339                                     ]
1340                                 ]
1341                             ]
1342                         ]
1343                     ]
1344                 ]
1345             ]
1346| 19,20,21,22: destruct %1 //
1347   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
1348   elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
1349   [ 1,3,5,7:
1350      whd in match (exec_expr ????); whd in match (exec_expr ????);
1351      cases Hexpr_sim_lhs
1352      [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
1353      | *: cases (exec_expr ge en m lhs)
1354           [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1355           | *: * #lval #ltrace #Hsim_lhs normalize nodelta           
1356                cases Hexpr_sim_rhs
1357                [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
1358                | *: cases (exec_expr ge en m rhs)
1359                     [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1360                     | *: * #rval #rtrace #Hsim_rhs
1361                          whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
1362                          >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉)))
1363                          >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉)))
1364                          normalize nodelta
1365                          >Htype_eq_lhs >Htype_eq_rhs
1366                          @SimOk * #val #trace #H @H
1367                     ]
1368                ]
1369           ]
1370      ]
1371   | *: normalize @SimFail /2 by refl, ex_intro/ 
1372   ]
1373(* Jump to the cast cases *)   
1374| 23,30,31,32,33,34,35,36: %1 try @refl
1375  [ 1,4,7,10,13,16,19,22: destruct // ]
1376  elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq
1377  (* exec_expr simulation *)
1378  [ 1,3,5,7,9,11,13,15: cases Hexec_sim
1379       [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFail whd in match (exec_expr ge en m ?);
1380            >Hexec_fail /2 by refl, ex_intro/
1381       | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq
1382            whd in match (exec_expr ge en m ?); #Hstep
1383            cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉
1384                    ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val)
1385            [ 1,3,5,7,9,11,13,15:
1386                 lapply Hstep -Hstep cases (exec_expr ge en m castee)
1387                 [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct
1388                 | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta
1389                      #Hstep @(ex_intro … val1)
1390                      cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep;
1391                      [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct
1392                      | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct
1393                           @conj @refl
1394                      ]
1395                 ]
1396            | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast
1397                 whd in match (exec_expr ge en m ?);
1398                 >(Hsim … Hexec_expr ) normalize nodelta
1399                 <Htype_eq >Hexec_cast //
1400            ]   
1401      ]
1402  | 2,4,6,8,10,12,14,16: destruct normalize @SimFail /2/
1403  ]
1404| 24: destruct inversion (Hcastee_inv ge en m)
1405  [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2
1406       <Hresult_flag_2 in Hresult_flag; #Hcontr destruct
1407  | 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq
1408       @(Inv_coerce_ok ??????? cast_sz cast_sg)
1409       [ 1: // | 2: <Htype_castee1 //
1410       | 3: whd in match (exec_expr ??? (Expr ??));
1411            >Htype_castee
1412            (* Simplify the goal by culling impossible cases, using Hsmaller_val *)
1413            cases (exec_expr ge en m castee) in Hsmaller_eval;
1414            [ 2: #error normalize //
1415            | 1: * #castee_val #castee_trace cases (exec_expr ge en m castee1)
1416              [ 2: #error normalize #Hcontr @(False_ind … Hcontr)
1417              | 1: * #castee1_val #castee1_trace #Hsmaller
1418                   elim (smaller_integer_val_spec … Hsmaller)
1419                   #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle
1420                   normalize nodelta destruct whd in match (exec_cast ????);
1421                   normalize nodelta >intsize_eq_elim_true whd
1422                   >sz_eq_identity >sz_eq_identity whd try @conj try @conj
1423                   [ 3: elim (necessary_conditions_spec … (sym_eq … Hconditions))
1424                        [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)
1425                        | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]
1426                   | 2: @refl
1427                   | 1: @cast_composition //
1428                        elim (necessary_conditions_spec … (sym_eq … Hconditions)) (* Clearly suboptimal stuff in this mess *)
1429                        [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)
1430                        | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]                       
1431                   ]
1432              ]
1433            ]
1434       ]
1435  ]
1436| 25,27: destruct
1437      inversion (Hcast2 ge en m)
1438      [ 1,3: (* Impossible case.  *)
1439           #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult;
1440           #Hcontr destruct
1441      | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself.
1442              We did not successfuly cast the subexpression to target_sz, though. *)
1443           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
1444           @(Inv_eq ???????) //
1445           [ 1,4: >Htype_castee2 normalize //
1446           | 2,5: (* Prove simulation for exec_expr *)
1447               whd in match (exec_expr ??? (Expr ??));
1448               cases (exec_expr ge en m castee) in Hsmaller_eval;
1449               [ 2,4: (* erroneous evaluation of the original expression *)
1450                     #error #Hsmaller_eval @SimFail @(ex_intro … error)
1451                     normalize nodelta //
1452               | 1,3: * #val #trace
1453                    cases (exec_expr ge en m castee2)
1454                    [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … Hsmaller_eval)
1455                    | 1,3: * #val1 #trace1 #Hsmaller_eval elim (smaller_integer_val_spec … Hsmaller_eval)
1456                         #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle
1457                         @SimOk * #val2 #trace2 normalize nodelta >Htype_castee
1458                         whd in match (exec_cast ????);
1459                         cases val in Hint1; normalize nodelta
1460                         [ 1,6: #Hint1 destruct | 3,4,5,8,9,10: #foo #Hint1 destruct
1461                         | 2,7: destruct cases src_sz in int1; #int1 * #int2 #Hint1
1462                              whd in match (intsize_eq_elim ???????);
1463                              whd in match (m_bind ?????);
1464                              [ 1,5,9,10,14,18: (* correct cases *) destruct #H @H
1465                              | 2,3,4,6,7,8,11,12,13,15,16,17: #Habsurd destruct ]
1466                         ]
1467                    ]
1468              ]
1469         | 3,6: normalize @SimFail /2/
1470         ]
1471    ]
1472| 26,28: destruct
1473      inversion (Hcast2 ge en m)
1474      [ 2,4: (* Impossible case. *)
1475            #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq
1476            (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *)
1477            letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq
1478            -Habsurd_eq -Habsurd #Habsurd destruct
1479      | 1,3: (* All our attempts at casting down the expression have failed. We still use the
1480               resulting expression, as we may have discovered and simplified unrelated casts. *)
1481            #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv
1482            @(Inv_eq ???????) //
1483            [ 1,3: (* Simulation for exec_expr *)
1484                 whd in match (exec_expr ??? (Expr ??));
1485                 whd in match (exec_expr ??? (Expr ??));
1486                 cases Hsim_expr
1487                 [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) //
1488                 | 1,3: #Hexec_ok
1489                      cases (exec_expr ge en m castee) in Hexec_ok;
1490                      [ 2,4: #error #Hsim @SimFail normalize nodelta /2/
1491                      | 1,3: * #val #trace #Hsim normalize nodelta
1492                           >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta
1493                           @SimOk #a #H @H
1494                      ]
1495                 ]
1496            | 2,4: normalize @SimFail /2/
1497            ]
1498      ]
1499| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1500      @(Inv_eq ???????) //
1501      whd in match (exec_expr ??? (Expr ??));
1502      whd in match (exec_expr ??? (Expr ??));
1503      [ 1: cases Hsim_expr
1504           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2/
1505           | 1: #Hexec_ok @SimOk * #val #trace
1506                cases (exec_expr ge en m castee) in Hexec_ok;
1507                [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct
1508                | 1: * #val #trace #Hexec_ok normalize nodelta
1509                     >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
1510                     >Htype_eq
1511                     normalize nodelta #H @H
1512                ]
1513           ]
1514      | 2: normalize @SimFail /2/
1515      ]
1516| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
1517      inversion (Htrue_inv ge en m)
1518      [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false
1519           #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct
1520      | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true
1521           inversion (Hfalse_inv ge en m)
1522           [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false
1523                #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct
1524           | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false
1525                >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg)
1526                [ 1,2: normalize //
1527                | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??));
1528                     elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq
1529                     cases Hexec_cond_sim
1530                     [ 2: * #error #Herror >Herror normalize @I
1531                     | 1: cases (exec_expr ge en m cond)
1532                          [ 2: #error #_ normalize @I
1533                          | 1: * #cond_val #cond_trace #Hcond_sim
1534                               >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1535                               
1536                               normalize nodelta
1537                               >Htype_cond_eq
1538                               cases (exec_bool_of_val cond_val (typeof cond1)) *
1539                               [ 3,4: normalize //
1540                               | 1,2: normalize in match (m_bind ?????);
1541                                      normalize in match (m_bind ?????);
1542                                      -Hexec_cond_sim -Hcond_sim -cond_val
1543                                      [ 1: (* true branch taken *)
1544                                           cases (exec_expr ge en m iftrue) in Hsmaller_true;
1545                                           [ 2: #error #_ @I
1546                                           | 1: * #val_true_branch #trace_true_branch
1547                                                cases (exec_expr ge en m iftrue1)
1548                                                [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)
1549                                                | 1: * #val_true1_branch #trace_true1_branch #Hsmaller
1550                                                     elim (smaller_integer_val_spec … Hsmaller)
1551                                                     #true_val * #true1_val * * * * #Htrue_val #Htrue1_val #Hcast
1552                                                     #Htrace_eq #Hsize_le normalize nodelta destruct
1553                                                     whd in match (smaller_integer_val ?????);
1554                                                     >sz_eq_identity normalize nodelta
1555                                                     >sz_eq_identity normalize nodelta
1556                                                     try @conj try @conj // ]
1557                                           ]
1558                                     | 2: (* false branch taken. Same proof as above, different arguments ... *)
1559                                           cases (exec_expr ge en m iffalse) in Hsmaller_false;
1560                                           [ 2: #error #_ @I
1561                                           | 1: * #val_false_branch #trace_false_branch
1562                                                cases (exec_expr ge en m iffalse1)
1563                                                [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)
1564                                                | 1: * #val_false1_branch #trace_false1_branch #Hsmaller
1565                                                     elim (smaller_integer_val_spec … Hsmaller)
1566                                                     #false_val * #false1_val * * * * #Hfalse_val #Hfalse1_val #Hcast
1567                                                     #Htrace_eq #Hsize_le normalize nodelta destruct
1568                                                     whd in match (smaller_integer_val ?????);
1569                                                     cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
1570                                                     [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
1571                                                          destruct (Htype_eq) @conj @refl
1572                                                     | 2: * #Hsize_eq #Hsg_eq destruct                                                     
1573                                                          >sz_eq_identity normalize nodelta
1574                                                          >sz_eq_identity normalize nodelta
1575                                                          try @conj try @conj try @refl assumption
1576                                                     ]
1577                                                ]
1578                                           ]
1579                                      ]
1580                              ]
1581                         ]
1582                    ]
1583               ]
1584          ]
1585     ]
1586| 38,39,40: destruct
1587   elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
1588   elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq
1589   elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq
1590   %1 try @refl
1591   [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
1592            cases (exec_expr ge en m cond) in Hsim_expr_cond;
1593            [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
1594            | 1,3,5: * #cond_val #cond_trace normalize nodelta
1595                cases (exec_expr ge en m cond1)
1596                [ 2,4,6: #error *
1597                         [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1598                                  #Habsurd destruct
1599                         | *: * #error #Habsurd destruct ]
1600                | 1,3,5: * #cond_val1 #cond_trace1 *
1601                         [ 2,4,6: * #error #Habsurd destruct
1602                         | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1603                             #Hcond_eq normalize nodelta destruct (Hcond_eq)
1604                             >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1))
1605                             [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro /
1606                             | 1,3,5: * (* true branch *)
1607                                [ 1,3,5:
1608                                 normalize in match (m_bind ?????);
1609                                 normalize in match (m_bind ?????);
1610                                 cases Hsim_expr_true
1611                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
1612                                 | 1,3,5: cases (exec_expr ge en m iftrue)
1613                                     [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1614                                     | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim
1615                                              >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉)))
1616                                              normalize nodelta @SimOk #a #H @H
1617                                     ]
1618                                 ]
1619                             | 2,4,6:
1620                                 normalize in match (m_bind ?????);
1621                                 normalize in match (m_bind ?????);                             
1622                                 cases Hsim_expr_false
1623                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
1624                                 | 1,3,5: cases (exec_expr ge en m iffalse)
1625                                     [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1626                                     | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim
1627                                              >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉)))
1628                                              normalize nodelta @SimOk #a #H @H
1629                                     ]
1630                                 ]
1631                               ]
1632                             ]
1633                          ]
1634                ]
1635            ]
1636   | 2,4,6: normalize @SimFail /2 by ex_intro/           
1637   ]
1638| 41,42: destruct
1639    elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1640    elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1641    %1 try @refl
1642    [ 1,3: whd in match (exec_expr ??? (Expr ??));
1643           whd in match (exec_expr ??? (Expr ??));
1644           cases Hsim_expr_lhs
1645           [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
1646           | 1,3: cases (exec_expr ge en m lhs)
1647              [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
1648              | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta
1649                     >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉)))
1650                     normalize nodelta >Htype_eq_lhs
1651                     cases (exec_bool_of_val lhs_val (typeof lhs1))
1652                       [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/
1653                     | 1,3: *
1654                         whd in match (m_bind ?????);
1655                         whd in match (m_bind ?????);                   
1656                         [ 2,3: (* lhs evaluates to true *)
1657                            @SimOk #a #H @H
1658                         | 1,4: cases Hsim_expr_rhs
1659                            [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/
1660                            | 1,3: cases (exec_expr ge en m rhs)
1661                                [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
1662                                | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim
1663                                       >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉)))
1664                                       normalize nodelta >Htype_eq_rhs
1665                                       @SimOk #a #H @H
1666                                ]
1667                            ]
1668                         ]
1669                      ]
1670            ]
1671         ]
1672   | 2,4: normalize @SimFail /2 by ex_intro/
1673   ]
1674| 43: destruct
1675      cases (type_eq_dec ty (Tint target_sz target_sg))
1676      [ 1: #Htype_eq >Htype_eq >type_eq_identity
1677           @(Inv_coerce_ok ??????? target_sz target_sg)
1678           [ 1,2: //
1679           | 3: cases target_sz cases target_sg normalize try @conj try @conj try @refl try @I ]
1680      | 2: #Hneq >(type_neq_not_identity … Hneq)
1681           %1 // @SimOk #a #H @H
1682      ]
1683| 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1684      %1 try @refl
1685      [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
1686           whd in match (exec_lvalue ????) in Hsim_lvalue;
1687           whd in match (exec_lvalue' ?????);
1688           whd in match (exec_lvalue' ?????);
1689           >Htype_eq
1690           cases (typeof rec_expr1) normalize nodelta
1691           [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
1692           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
1693           | 6,7: cases Hsim_lvalue
1694              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1695              | 1,3: cases (exec_lvalue ge en m rec_expr)
1696                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1697                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
1698                         whd in match (m_bind ?????);
1699                         @SimOk #a #H @H
1700                 ]
1701              ]
1702           ]
1703      | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??));
1704           >Htype_eq
1705           cases (typeof rec_expr1) normalize nodelta
1706           [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
1707           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
1708           | 6,7: cases Hsim_lvalue
1709              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1710              | 1,3: cases (exec_lvalue ge en m rec_expr)
1711                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1712                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
1713                         whd in match (m_bind ?????);
1714                         @SimOk #a #H @H
1715                 ]
1716              ]
1717           ]
1718     ]
1719| 45: destruct
1720   inversion (Hinv ge en m)
1721   [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_
1722         @(Inv_coerce_ok ??????? src_sz src_sg)
1723         [ 1: >Htypeof_e1 //
1724         | 2: >Htypeof_e2 //
1725         | 3: whd in match (exec_expr ??? (Expr ??));
1726              whd in match (exec_expr ??? (Expr ??));
1727              cases (exec_expr ge en m e1) in Hsmaller;
1728              [ 2: #error normalize //
1729              | 1: * #val1 #trace1 cases (exec_expr ge en m e2)
1730                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … Habsurd)
1731                   | 1: * #val2 #trace #Hsmaller
1732                        elim (smaller_integer_val_spec … Hsmaller)
1733                        #i1 * #i2 * * * * #Hval1 #Hval2 #Hcast #Htrace_eq #Hsize_le
1734                        normalize nodelta destruct whd in match (smaller_integer_val ?????);
1735                        >sz_eq_identity >sz_eq_identity normalize nodelta
1736                        try @conj try @conj try @conj try @refl assumption
1737                   ]
1738               ]
1739         ]
1740   | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_
1741        >Hresult %1 try @refl
1742        [ 1: >Htype_eq //
1743        | 2: whd in match (exec_expr ??? (Expr ??));
1744             whd in match (exec_expr ??? (Expr ??));
1745             cases Hsim_expr
1746             [ 2: * #error #Hexec_error >Hexec_error @SimFail /2 by ex_intro/
1747             | 1: cases (exec_expr ge en m e1)
1748                  [ 2: #error #_ @SimFail /2 by ex_intro/
1749                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
1750                        @SimOk #a #H @H
1751                  ]
1752             ]
1753        | 3: @SimFail /2 by ex_intro/
1754        ]
1755   ]
1756| 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1757      %1 try @refl
1758      [ 1: whd in match (exec_expr ??? (Expr ??));
1759           whd in match (exec_expr ??? (Expr ??));
1760           cases Hsim_expr
1761           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1762           | 1: cases (exec_expr ge en m e1)
1763                [ 2: #error #_ @SimFail /2 by ex_intro/
1764                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ]
1765           ]
1766      | 2: @SimFail /2 by ex_intro/ ]
1767(* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls
1768 * simplify_expr2 *)     
1769| 47, 48, 49: (* trivial const_int, const_float and var cases *)
1770  try @conj try @conj try @refl
1771  @SimOk #a #H @H
1772| 50: (* Deref case *) destruct
1773  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1774  try @conj try @conj
1775  [ 1:
1776    whd in match (exec_expr ??? (Expr ??));
1777    whd in match (exec_expr ??? (Expr ??));
1778    whd in match (exec_lvalue' ?????);
1779    whd in match (exec_lvalue' ?????); 
1780  | 2:
1781    whd in match (exec_lvalue ??? (Expr ??));
1782    whd in match (exec_lvalue ??? (Expr ??));
1783  ]
1784  [ 1,2: 
1785    cases Hsim_expr
1786    [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1787    | 1,3: cases (exec_expr ge en m e1)
1788         [ 2,4: #error #_ @SimFail /2 by ex_intro/
1789         | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
1790  | 3: // ]
1791| 51: (* Addrof *) destruct
1792  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1793  try @conj try @conj   
1794  [ 1:
1795    whd in match (exec_expr ??? (Expr ??));
1796    whd in match (exec_expr ??? (Expr ??));
1797    cases Hsim_lvalue
1798    [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
1799    | 1: cases (exec_lvalue ge en m e1)
1800       [ 2: #error #_ @SimFail /2 by ex_intro/
1801       | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
1802  | 2: @SimFail /2 by ex_intro/
1803  | 3: // ]
1804| 52: (* Unop *) destruct
1805  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1806  try @conj try @conj
1807  [ 1:
1808    whd in match (exec_expr ??? (Expr ??));
1809    whd in match (exec_expr ??? (Expr ??));
1810    cases Hsim_expr
1811    [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1812    | 1: cases (exec_expr ge en m e1)
1813         [ 2: #error #_ @SimFail /2 by ex_intro/
1814         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk
1815              >Htype_eq #a #H @H ] ]
1816  | 2: @SimFail /2 by ex_intro/             
1817  | 3: // ]
1818| 53: (* Binop *) destruct
1819  elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1820  elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1821  try @conj try @conj
1822  [ 1:
1823    whd in match (exec_expr ??? (Expr ??));
1824    whd in match (exec_expr ??? (Expr ??));
1825    cases Hsim_expr_lhs
1826    [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1827    | 1: cases (exec_expr ge en m lhs)
1828         [ 2: #error #_ @SimFail /2 by ex_intro/
1829         | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs
1830              [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1831              | 1: cases (exec_expr ge en m rhs)
1832                   [ 2: #error #_ @SimFail /2 by ex_intro/
1833                   | 1: #rhs_value #Hsim_rhs
1834                        lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value)))
1835                        lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value)))
1836                        #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs
1837                        @SimOk #a #H @H
1838                   ]
1839              ]
1840         ]
1841    ]
1842  | 2: @SimFail /2 by ex_intro/
1843  | 3: //
1844  ]
1845| 54: (* Cast, fallback case *)
1846  try @conj try @conj try @refl
1847  @SimOk #a #H @H
1848| 55: (* Cast, success case *) destruct
1849  inversion (Htrans_inv ge en m)
1850  [ 1: (* contradiction *)
1851       #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true
1852       <Hresult_flag_true in Hresult_flag; #Habsurd destruct
1853  | 2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_
1854       try @conj try @conj try @conj
1855       [ 1: whd in match (exec_expr ??? (Expr ??));
1856            cases (exec_expr ge en m castee) in Hsmaller;
1857            [ 2: #error #_ @SimFail /2 by ex_intro/
1858            | 1: * #val #trace cases (exec_expr ge en m castee1)
1859                 [ 2: #error #Habsurd @(False_ind … Habsurd)
1860                 | 1: * #val1 #trace1 #Hsmaller elim (smaller_integer_val_spec … Hsmaller)
1861                      #v1 * #v2 * * * * #Hval1 #Hval2 #Hcast #Htrace #Hle
1862                      >Hsrc_type_eq normalize nodelta cases val in Hval1;
1863                      [ 1: #Hval1 | 2: #sz #i #Hval1 | 3,4,5: #irrelevant #Hval1 ]
1864                      [ 1,3,4,5: normalize @SimFail /2 by ex_intro/ ]
1865                      whd in match (exec_cast ????);
1866                      cases (sz_eq_dec sz src_sz)
1867                      [ 2: #Hneq normalize nodelta
1868                           >(intsize_eq_elim_false (res ?) sz src_sz ???? Hneq)
1869                           @SimFail /2 by ex_intro/
1870                      | 1: #Heq <Heq normalize nodelta >intsize_eq_elim_true
1871                           destruct normalize
1872                           @SimOk #a #H @H
1873                      ]
1874                 ]
1875            ]
1876      | 2: @SimFail /2 by ex_intro/
1877      | 3: >Htarget_type_eq //
1878      ]
1879  ]
1880| 56: (* Cast, "failure" case *) destruct
1881  inversion (Htrans_inv ge en m)
1882  [ 2: (* contradiction *)
1883       #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd
1884       lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct
1885  | 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_
1886       try @conj try @conj try @conj
1887       [ 1: whd in match (exec_expr ????);
1888            whd in match (exec_expr ??? (Expr ??));
1889            cases Hsim_expr
1890            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1891            | 1: cases (exec_expr ??? castee)
1892                 [ 2: #error #_ @SimFail /2 by ex_intro/
1893                 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok
1894                       @SimOk >Htype_eq #a #H @H ]
1895            ]
1896       | 2: @SimFail /2 by ex_intro/
1897       | 3: //
1898       ]
1899  ]
1900| 57,58,59,60,61,62,63,64,68:       
1901  try @conj try @conj try @refl
1902  @SimOk #a #H @H
1903| 65: destruct
1904  elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond
1905  elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true
1906  elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false
1907  try @conj try @conj
1908  [ 1: whd in match (exec_expr ??? (Expr ??));
1909       whd in match (exec_expr ??? (Expr ??));
1910       cases Hsim_exec_cond
1911       [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1912       | 1: cases (exec_expr ??? cond)
1913            [ 2: #error #_ @SimFail /2 by ex_intro/
1914            | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉)))
1915                 #Hcond_ok >Hcond_ok >Htype_eq_cond
1916                 normalize nodelta
1917                 cases (exec_bool_of_val condb (typeof cond1))
1918                 [ 2: #error @SimFail /2 by ex_intro/
1919                 | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????);
1920                      normalize nodelta
1921                      [ 1: (* true branch taken *)
1922                           cases Hsim_exec_true
1923                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1924                           | 1: cases (exec_expr ??? iftrue)
1925                                [ 2: #error #_ @SimFail /2 by ex_intro/
1926                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
1927                                     @SimOk #a #H @H
1928                                ]
1929                           ]
1930                      | 2: (* false branch taken *)
1931                           cases Hsim_exec_false
1932                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1933                           | 1: cases (exec_expr ??? iffalse)
1934                                [ 2: #error #_ @SimFail /2 by ex_intro/
1935                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
1936                                     @SimOk #a #H @H
1937                                ]
1938                           ]
1939                      ]
1940                ]
1941           ]
1942      ]
1943  | 2: @SimFail /2 by ex_intro/
1944  | 3: //
1945  ]
1946| 66,67: destruct
1947  elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1948  elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1949  try @conj try @conj
1950  whd in match (exec_expr ??? (Expr ??));
1951  whd in match (exec_expr ??? (Expr ??));
1952  [ 1,4: cases Hsim_exec_lhs
1953       [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1954       | 1,3: cases (exec_expr ??? lhs)
1955            [ 2,4: #error #_ @SimFail /2 by ex_intro/
1956            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs
1957                   normalize nodelta elim a #lhs_val #lhs_trace
1958                   cases (exec_bool_of_val lhs_val (typeof lhs1))
1959                   [ 2,4: #error @SimFail /2 by ex_intro/
1960                   | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
1961                        [ 2,3: @SimOk //
1962                        | 1,4: cases Hsim_exec_rhs
1963                            [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
1964                            | 1,3: cases (exec_expr ??? rhs)
1965                               [ 2,4: #error #_ @SimFail /2 by ex_intro/
1966                               | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs
1967                                    @SimOk #a #H @H
1968                               ]
1969                            ]
1970                        ]
1971                   ]
1972             ]
1973        ]
1974  | 2,5: @SimFail /2 by ex_intro/
1975  | 3,6: //
1976  ]
1977| 69: (* record field *) destruct
1978   elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1979   try @conj try @conj   
1980   whd in match (exec_expr ??? (Expr ??));
1981   whd in match (exec_expr ??? (Expr ??));
1982   whd in match (exec_lvalue' ??? (Efield rec_expr f) ty);
1983   whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 
1984   [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
1985       [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
1986       | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
1987       try (@SimFail /2 by ex_intro/)
1988       cases Hsim_lvalue
1989       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
1990       | 1,3: cases (exec_lvalue ge en m rec_expr)
1991            [ 2,4: #error #_ @SimFail /2 by ex_intro/
1992            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
1993                   @SimOk #a #H @H ]
1994       ]
1995   | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
1996       >Htype_eq cases (typeof rec_expr1) normalize nodelta
1997       [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
1998       | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
1999       try (@SimFail /2 by ex_intro/)
2000       cases Hsim_lvalue
2001       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
2002       | 1,3: cases (exec_lvalue ge en m rec_expr)
2003            [ 2,4: #error #_ @SimFail /2 by ex_intro/
2004            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
2005                   @SimOk #a #H @H ]
2006       ]
2007   | 3: // ]
2008| 70: (* cost label *) destruct
2009   elim (Hequiv ge en m) *  #Hsim_expr #Hsim_lvalue #Htype_eq
2010   try @conj try @conj
2011   whd in match (exec_expr ??? (Expr ??));
2012   whd in match (exec_expr ??? (Expr ??));
2013   [ 1:
2014     cases Hsim_expr
2015     [ 2: * #error #Hexec >Hexec @SimFail /2 by ex_intro/
2016     | 1: cases (exec_expr ??? e1)
2017          [ 2: #error #_ @SimFail /2 by ex_intro/
2018          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
2019               @SimOk #a #H @H ]
2020     ]
2021   | 2: @SimFail /2 by ex_intro/
2022   | 3: //
2023   ]
2024] qed.   
2025
2026
2027(* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and
2028   returns a flag stating whether the desired type was achieved and a simplified
2029   version of e. *)
2030let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
2031match e with
2032[ Expr ed ty ⇒
2033  match ed with
2034  [ Econst_int sz i ⇒
2035    match ty with
2036    [ Tint ty_sz sg ⇒
2037      match ty' with
2038      [ Tint sz' sg' ⇒
2039        (* IG: checking that the displayed type size [ty_sz] and [sz] are equal ... *)
2040        match sz_eq_dec sz ty_sz with
2041        [ inl Heq ⇒
2042          match simplify_int sz sz' sg sg' i with
2043          [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉
2044          | None ⇒ 〈false, e〉
2045          ]
2046        | inr _ ⇒
2047          (* The expression is ill-typed. *)
2048          〈false, e〉
2049        ]
2050      | _ ⇒ 〈false, e〉 ]
2051    | _ ⇒ 〈false, e〉 ]
2052  | Ederef e1 ⇒
2053      let ty1 ≝ typeof e1 in
2054      〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉
2055  | Eaddrof e1 ⇒
2056      let ty1 ≝ typeof e1 in
2057      〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉
2058  | Eunop op e1 ⇒
2059      let ty1 ≝ typeof e1 in
2060      〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉
2061  | Ebinop op e1 e2 ⇒
2062      if binop_simplifiable op then
2063        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in
2064        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
2065        if desired_type1 ∧ desired_type2 then
2066          〈true, Expr (Ebinop op e1' e2') ty'〉
2067        else
2068          let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
2069          let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
2070            〈false, Expr (Ebinop op e1' e2') ty〉
2071      else
2072        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in
2073        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in
2074          〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉
2075  | Ecast ty e1 ⇒
2076      match inttype_compare ty' ty with
2077      [ itc_le ⇒
2078        let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
2079        if desired_type then 〈true, e1'〉 else
2080          let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
2081          if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
2082      | itc_no ⇒
2083        let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
2084        if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
2085      ]
2086  | Econdition e1 e2 e3 ⇒
2087      let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *)
2088      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
2089      let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in
2090      if desired_type2 ∧ desired_type3 then
2091        〈true, Expr (Econdition e1' e2' e3') ty'〉
2092      else
2093        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
2094        let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in
2095          〈false, Expr (Econdition e1' e2' e3') ty〉
2096    (* Could probably do better with these, too. *)
2097  | Eandbool e1 e2 ⇒
2098      let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
2099      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
2100        〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉
2101  | Eorbool e1 e2 ⇒
2102      let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
2103      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
2104        〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉
2105  (* Could also improve Esizeof *)
2106  | Efield e1 f ⇒
2107      let ty1 ≝ typeof e1 in
2108      〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉
2109  | Ecost l e1 ⇒
2110      let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
2111        〈desired_type, Expr (Ecost l e1') (typeof e1')〉
2112  | _ ⇒ 〈type_eq ty ty',e〉
2113  ]
2114].
2115
2116definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)).
2117
2118let rec simplify_statement (s:statement) : statement ≝
2119match s with
2120[ Sskip ⇒ Sskip
2121| Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2)
2122| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
2123| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
2124| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
2125| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
2126| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
2127| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
2128| Sbreak ⇒ Sbreak
2129| Scontinue ⇒ Scontinue
2130| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
2131| Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls)
2132| Slabel l s1 ⇒ Slabel l (simplify_statement s1)
2133| Sgoto l ⇒ Sgoto l
2134| Scost l s1 ⇒ Scost l (simplify_statement s1)
2135]
2136and simplify_ls ls ≝
2137match ls with
2138[ LSdefault s ⇒ LSdefault (simplify_statement s)
2139| LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls')
2140].
2141
2142definition simplify_function : function → function ≝
2143λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).
2144
2145definition simplify_fundef : clight_fundef → clight_fundef ≝
2146λf. match f with
2147  [ CL_Internal f ⇒ CL_Internal (simplify_function f)
2148  | _ ⇒ f
2149  ].
2150
2151definition simplify_program : clight_program → clight_program ≝
2152λp. transform_program … p simplify_fundef.
2153
2154
2155(* We have to prove that simplify_expr doesn't alter the semantics. Since expressions are pure,
2156 * we state that expressions before and after conversion should evaluate to the same value, or
2157 * fail in a similar way when placed into a given context. *)
2158
2159
2160let rec expr_ind2
2161    (P : expr → Prop) (Q : expr_descr → Prop)
2162    (IE : ∀ed. ∀t. Q ed → P (Expr ed t))
2163    (Iconst_int : ∀sz, i. Q (Econst_int sz i))
2164    (Iconst_float : ∀f. Q (Econst_float f))
2165    (Ivar : ∀id. Q (Evar id))
2166    (Ideref : ∀e. P e → Q (Ederef e))
2167    (Iaddrof : ∀e. P e → Q (Eaddrof e))
2168    (Iunop : ∀op,arg. P arg → Q (Eunop op arg))
2169    (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2))
2170    (Icast : ∀t. ∀e . P e →  Q (Ecast t e))
2171    (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3))
2172    (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2))
2173    (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2))
2174    (Isizeof : ∀t. Q (Esizeof t))
2175    (Ifield : ∀e,f. P e → Q (Efield e f))
2176    (Icost : ∀c,e. P e → Q (Ecost c e))
2177    (e : expr) on e : P e ≝
2178match e with
2179[ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed) ]
2180
2181and expr_desc_ind2
2182    (P : expr → Prop) (Q : expr_descr → Prop)
2183    (IE : ∀ed. ∀t. Q ed → P (Expr ed t))
2184    (Iconst_int : ∀sz, i. Q (Econst_int sz i))
2185    (Iconst_float : ∀f. Q (Econst_float f))
2186    (Ivar : ∀id. Q (Evar id))
2187    (Ideref : ∀e. P e → Q (Ederef e))
2188    (Iaddrof : ∀e. P e → Q (Eaddrof e))
2189    (Iunop : ∀op,arg. P arg → Q (Eunop op arg))
2190   
2191    (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2))
2192    (Icast : ∀t. ∀e . P e →  Q (Ecast t e))
2193    (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3))
2194    (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2))
2195    (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2))
2196    (Isizeof : ∀t. Q (Esizeof t))
2197    (Ifield : ∀e,f. P e → Q (Efield e f))
2198    (Icost : ∀c,e. P e → Q (Ecost c e))
2199    (ed : expr_descr) on ed : Q ed ≝
2200match ed with
2201[ Econst_int sz i ⇒ Iconst_int sz i
2202| Econst_float f ⇒ Iconst_float f
2203| Evar id ⇒ Ivar id
2204| Ederef e ⇒ Ideref e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
2205| Eaddrof e ⇒ Iaddrof e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
2206| Eunop op e ⇒ Iunop op e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
2207| Ebinop op e1 e2 ⇒ Ibinop op e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
2208| Ecast t e ⇒ Icast t e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
2209| Econdition e1 e2 e3 ⇒ Icond e1 e2 e3  (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
2210| Eandbool e1 e2 ⇒ Iandbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
2211| Eorbool e1 e2 ⇒ Iorbool e1 e2 (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
2212| Esizeof t ⇒ Isizeof t
2213| Efield e field ⇒ Ifield e field (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
2214| Ecost c e ⇒ Icost c e (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof
Note: See TracBrowser for help on using the repository browser.