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

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

Work-in-progress: correction proof for the cast removal on expressions.

File size: 91.7 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.
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
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
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 cast_ty with
1112    [ Tint cast_sz cast_sg ⇒
1113      let «〈success, castee〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in
1114      match success with
1115      [ true ⇒
1116        «castee, ?»
1117      | false ⇒
1118        «Expr (Ecast cast_ty castee) ty, ?»
1119      ]
1120    | _ ⇒
1121      «e, ?»
1122    ]
1123  | _ ⇒ λHdesc_eq.
1124    (* TODO, replace this stub by the actual recursive calls to simplify_inside. Should be non-problematic. *)
1125    «e, ?»
1126  ] (refl ? ed)
1127] (refl ? e).
1128#ge #en #m
1129[ 1,3,5,6,7,8,9,10,11,12: %1 //
1130     cases (exec_expr ge en m e) #res
1131     try (@(SimOk ???) //)
1132| 13,14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
1133     try (@(SimOk ???) //)
1134| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct //
1135     whd in match (exec_expr ????); >eq_intsize_identity whd
1136     >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]
1137| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) //
1138     whd in match (exec_expr ????);
1139     whd in match (exec_expr ????);
1140     >eq_intsize_identity >eq_intsize_identity whd
1141     >sz_eq_identity >sz_eq_identity whd @conj try @conj //
1142     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
1143     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
1144| 15: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1145    [ 1: (* Proving preservation of the semantics for expressions. *)
1146      cases Hexpr_sim
1147      [ 2: (* Case where the evaluation of e1 as an expression fails *)
1148        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/
1149      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1150        #Hsim %1 * #val #trace normalize #Hstep
1151        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧
1152                   (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val))
1153        [ 1: lapply Hstep -Hstep
1154             cases (exec_expr ge en m e1)
1155             [ 1: * #val' #trace' normalize nodelta
1156                  cases val' normalize nodelta
1157                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
1158                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
1159                       cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq;
1160                       normalize nodelta
1161                       [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ]
1162                  ]
1163             | 2: normalize nodelta #errmesg #Hcontr destruct
1164             ]
1165        | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr
1166             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)
1167                       ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val))
1168             [ 1: @(ex_intro … e1_ptr) @conj
1169                  [ 1: @Hsim // | 2: // ]
1170             | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr
1171                normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl
1172             ]
1173        ]
1174     ]
1175   | 2: (* Proving the preservation of the semantics for lvalues. *)
1176      cases Hexpr_sim
1177      [ 2: (* Case where the evaluation of e1 as an lvalue fails *)
1178        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2/
1179      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1180        #Hsim %1 * * #block #offset #trace normalize #Hstep
1181        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset)
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                       destruct try @conj try @conj //
1189                  ]
1190             | 2: normalize nodelta #errmesg #Hcontr destruct
1191             ]
1192        | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset
1193             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)  ∧ pblock ptr1 = block ∧ poff ptr1 = offset)
1194             [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim //
1195             | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset
1196                normalize >He2_exec normalize nodelta //
1197             ]
1198        ]
1199     ]
1200   ]
1201| 16: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1202    [ 1: (* Proving preservation of the semantics for expressions. *)
1203      cases Hlvalue_sim
1204      [ 2: (* Case where the evaluation of e1 as an expression fails *)
1205        * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2/
1206      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1207        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
1208        cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
1209                                 (pointer_compat_dec block r = inl ?? pc) ∧
1210                                 (ty = Tpointer r ptype) ∧
1211                                  val = Vptr (mk_pointer r block pc offset))
1212        [ 1: lapply Hstep -Hstep
1213             cases (exec_lvalue ge en m e1)
1214             [ 1: * * #block #offset #trace' normalize nodelta
1215                  cases ty
1216                  [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
1217                  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
1218                  normalize nodelta try (#Heq destruct)
1219                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty)
1220                  cases (pointer_compat_dec block rg) in Heq; normalize
1221                  [ 2: #Hnotcompat #Hcontr destruct
1222                  | 1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ]
1223             | 2: normalize nodelta #errmesg #Hcontr destruct
1224             ]
1225        | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq
1226             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
1227             >Hptr_compat normalize nodelta //
1228        ]
1229     ]
1230   | 2: (* Proving preservation of the semantics of lvalues. *)
1231      normalize @SimFail /2/
1232   ]
1233| 17: destruct %1 // elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1234      [ 1: whd in match (exec_expr ge en m (Expr ??));
1235           whd in match (exec_expr ge en m (Expr ??));
1236           cases Hexpr_sim
1237           [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2/
1238           | 1: cases (exec_expr ge en m e1)
1239                [ 2: #error #Hexec normalize nodelta @SimFail /2/
1240                | 1: * #val #trace #Hexec
1241                     >(Hexec ? (refl ? (OK ? 〈val,trace〉)))
1242                     normalize nodelta @SimOk #a >Htype_eq #H @H
1243                ]
1244           ]
1245      | 2: normalize @SimFail /2/
1246      ]
1247| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
1248      inversion (Hinv_lhs ge en m)
1249      [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true
1250           #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct
1251      | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_
1252           inversion (Hinv_rhs ge en m)
1253           [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_
1254                <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct
1255           | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_
1256                @(Inv_coerce_ok  ge en m … target_sz target_sg lhs_src_sz lhs_src_sg)
1257                [ 1: >Htype_lhs //
1258                | 2: //
1259                | 3: whd in match (exec_expr ??? (Expr ??));
1260                     whd in match (exec_expr ??? (Expr ??));
1261                     (* Enumerate all the cases for the evaluation of the source expressions ... *)
1262                     cases (exec_expr ge en m lhs) in Hsmaller_lhs;
1263                     [ 2: #error normalize //
1264                     | 1: * #val_lhs #trace_lhs normalize nodelta cases (exec_expr ge en m lhs1)
1265                          [ 2: #error normalize #H @(False_ind … H)
1266                          | 1: * #val_lhs1 #trace_lhs1 #Hsmaller_lhs
1267                               elim (smaller_integer_val_spec … Hsmaller_lhs)
1268                               #lhs_int * #lhs1_int * * * * #Hval_lhs #Hval_lhs1 #Hlhs_cast #Hlhs_trace #Hlhs_size
1269                               cases (exec_expr ge en m rhs) in Hsmaller_rhs;
1270                               [ 2: #error normalize //
1271                               | 1: * #val_rhs #trace_rhs normalize nodelta cases (exec_expr ge en m rhs1)
1272                                    [ 2: #error normalize #H @(False_ind … H)
1273                                    | 1: * #val_rhs1 #trace_rhs1 #Hsmaller_rhs
1274                                         elim (smaller_integer_val_spec … Hsmaller_rhs)
1275                                         #rhs_int * #rhs1_int * * * * #Hval_rhs #Hval_rhs1 #Hrhs_cast #Hrhs_trace #Hrhs_size
1276                                         whd in match (m_bind ?????);
1277                                         whd in match (m_bind ?????);
1278                                         <Htylhs_eq_tyrhs >Htype_lhs
1279                                         >Htype_lhs1 >Htype_rhs1
1280                                         cut (lhs_src_sz = rhs_src_sz ∧ lhs_src_sg = rhs_src_sg)
1281                                         [ 1: >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Hty_eq destruct (Hty_eq)
1282                                               @conj // ]
1283                                         * #Hsrc_sz_eq #Hsrc_sg_eq
1284                                         cases op in Hop_simplifiable_eq;
1285                                         normalize in match (binop_simplifiable ?);
1286                                         [ 3,4,5,6,7,8,9,10,11,12,13,14,15,16: #H destruct (H)
1287                                         | 1: #_ (* addition case *)
1288                                             >Hval_lhs >Hval_rhs destruct
1289                                             whd in match (sem_binary_operation Oadd ?????);
1290                                             whd in match (sem_binary_operation Oadd ?????); normalize nodelta
1292                                             >intsize_eq_elim_true >intsize_eq_elim_true
1293                                             whd in match (opt_to_res ???); whd in match (opt_to_res ???);
1294                                             whd in match (smaller_integer_val ?????); normalize nodelta
1295                                             >sz_eq_identity >sz_eq_identity normalize nodelta
1296                                             try @conj try @conj try //
1298                                         | 2: #_ (* subtraction case *)
1299                                             >Hval_lhs >Hval_rhs destruct
1300                                             whd in match (sem_binary_operation Osub ?????);
1301                                             whd in match (sem_binary_operation Osub ?????); normalize nodelta
1302                                             >classify_sub_int >classify_sub_int normalize nodelta
1303                                             >intsize_eq_elim_true >intsize_eq_elim_true
1304                                             whd in match (opt_to_res ???); whd in match (opt_to_res ???);
1305                                             whd in match (smaller_integer_val ?????); normalize nodelta
1306                                             >sz_eq_identity >sz_eq_identity normalize nodelta
1307                                             try @conj try @conj try //
1308                                             >integer_sub_cast_le //
1309                                         ]
1310                                     ]
1311                                 ]
1312                             ]
1313                         ]
1314                     ]
1315                 ]
1316             ]
1317| 19,20,21,22: destruct %1 //
1318   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
1319   elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
1320   [ 1,3,5,7:
1321      whd in match (exec_expr ????); whd in match (exec_expr ????);
1322      cases Hexpr_sim_lhs
1323      [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
1324      | *: cases (exec_expr ge en m lhs)
1325           [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1326           | *: * #lval #ltrace #Hsim_lhs normalize nodelta
1327                cases Hexpr_sim_rhs
1328                [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
1329                | *: cases (exec_expr ge en m rhs)
1330                     [ 2,4,6,8: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1331                     | *: * #rval #rtrace #Hsim_rhs
1332                          whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
1333                          >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉)))
1334                          >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉)))
1335                          normalize nodelta
1336                          >Htype_eq_lhs >Htype_eq_rhs
1337                          @SimOk * #val #trace #H @H
1338                     ]
1339                ]
1340           ]
1341      ]
1342   | *: normalize @SimFail /2 by refl, ex_intro/
1343   ]
1344(* Jump to the cast cases *)
1345| 23,30,31,32,33,34,35,36: %1 try @refl
1346  [ 1,4,7,10,13,16,19,22: destruct // ]
1347  elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq
1348  (* exec_expr simulation *)
1349  [ 1,3,5,7,9,11,13,15: cases Hexec_sim
1350       [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFail whd in match (exec_expr ge en m ?);
1351            >Hexec_fail /2 by refl, ex_intro/
1352       | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq
1353            whd in match (exec_expr ge en m ?); #Hstep
1354            cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉
1355                    ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val)
1356            [ 1,3,5,7,9,11,13,15:
1357                 lapply Hstep -Hstep cases (exec_expr ge en m castee)
1358                 [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct
1359                 | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta
1360                      #Hstep @(ex_intro … val1)
1361                      cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep;
1362                      [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct
1363                      | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct
1364                           @conj @refl
1365                      ]
1366                 ]
1367            | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast
1368                 whd in match (exec_expr ge en m ?);
1369                 >(Hsim … Hexec_expr ) normalize nodelta
1370                 <Htype_eq >Hexec_cast //
1371            ]
1372      ]
1373  | 2,4,6,8,10,12,14,16: destruct normalize @SimFail /2/
1374  ]
1375| 24: destruct inversion (Hcastee_inv ge en m)
1376  [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2
1377       <Hresult_flag_2 in Hresult_flag; #Hcontr destruct
1378  | 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq
1379       @(Inv_coerce_ok ??????? cast_sz cast_sg)
1380       [ 1: // | 2: <Htype_castee1 //
1381       | 3: whd in match (exec_expr ??? (Expr ??));
1382            >Htype_castee
1383            (* Simplify the goal by culling impossible cases, using Hsmaller_val *)
1384            cases (exec_expr ge en m castee) in Hsmaller_eval;
1385            [ 2: #error normalize //
1386            | 1: * #castee_val #castee_trace cases (exec_expr ge en m castee1)
1387              [ 2: #error normalize #Hcontr @(False_ind … Hcontr)
1388              | 1: * #castee1_val #castee1_trace #Hsmaller
1389                   elim (smaller_integer_val_spec … Hsmaller)
1390                   #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle
1391                   normalize nodelta destruct whd in match (exec_cast ????);
1392                   normalize nodelta >intsize_eq_elim_true whd
1393                   >sz_eq_identity >sz_eq_identity whd try @conj try @conj
1394                   [ 3: elim (necessary_conditions_spec … (sym_eq … Hconditions))
1395                        [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)
1396                        | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]
1397                   | 2: @refl
1398                   | 1: @cast_composition //
1399                        elim (necessary_conditions_spec … (sym_eq … Hconditions)) (* Clearly suboptimal stuff in this mess *)
1400                        [ 1: elim target_sz elim cast_sz normalize #Hlt try @I @(False_ind … Hlt)
1401                        | 2: * #Hcast_eq #_ >Hcast_eq elim target_sz // ]
1402                   ]
1403              ]
1404            ]
1405       ]
1406  ]
1407| 25,27: destruct
1408      inversion (Hcast2 ge en m)
1409      [ 1,3: (* Impossible case.  *)
1410           #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult;
1411           #Hcontr destruct
1412      | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself.
1413              We did not successfuly cast the subexpression to target_sz, though. *)
1414           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
1415           @(Inv_eq ???????) //
1416           [ 1,4: >Htype_castee2 normalize //
1417           | 2,5: (* Prove simulation for exec_expr *)
1418               whd in match (exec_expr ??? (Expr ??));
1419               cases (exec_expr ge en m castee) in Hsmaller_eval;
1420               [ 2,4: (* erroneous evaluation of the original expression *)
1421                     #error #Hsmaller_eval @SimFail @(ex_intro … error)
1422                     normalize nodelta //
1423               | 1,3: * #val #trace
1424                    cases (exec_expr ge en m castee2)
1425                    [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … Hsmaller_eval)
1426                    | 1,3: * #val1 #trace1 #Hsmaller_eval elim (smaller_integer_val_spec … Hsmaller_eval)
1427                         #int1 * #int2 * * * * #Hint1 #Hint2 #Hcast #Htrace #Hle
1428                         @SimOk * #val2 #trace2 normalize nodelta >Htype_castee
1429                         whd in match (exec_cast ????);
1430                         cases val in Hint1; normalize nodelta
1431                         [ 1,6: #Hint1 destruct | 3,4,5,8,9,10: #foo #Hint1 destruct
1432                         | 2,7: destruct cases src_sz in int1; #int1 * #int2 #Hint1
1433                              whd in match (intsize_eq_elim ???????);
1434                              whd in match (m_bind ?????);
1435                              [ 1,5,9,10,14,18: (* correct cases *) destruct #H @H
1436                              | 2,3,4,6,7,8,11,12,13,15,16,17: #Habsurd destruct ]
1437                         ]
1438                    ]
1439              ]
1440         | 3,6: normalize @SimFail /2/
1441         ]
1442    ]
1443| 26,28: destruct
1444      inversion (Hcast2 ge en m)
1445      [ 2,4: (* Impossible case. *)
1446            #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq
1447            (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *)
1448            letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq
1449            -Habsurd_eq -Habsurd #Habsurd destruct
1450      | 1,3: (* All our attempts at casting down the expression have failed. We still use the
1451               resulting expression, as we may have discovered and simplified unrelated casts. *)
1452            #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv
1453            @(Inv_eq ???????) //
1454            [ 1,3: (* Simulation for exec_expr *)
1455                 whd in match (exec_expr ??? (Expr ??));
1456                 whd in match (exec_expr ??? (Expr ??));
1457                 cases Hsim_expr
1458                 [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) //
1459                 | 1,3: #Hexec_ok
1460                      cases (exec_expr ge en m castee) in Hexec_ok;
1461                      [ 2,4: #error #Hsim @SimFail normalize nodelta /2/
1462                      | 1,3: * #val #trace #Hsim normalize nodelta
1463                           >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta
1464                           @SimOk #a #H @H
1465                      ]
1466                 ]
1467            | 2,4: normalize @SimFail /2/
1468            ]
1469      ]
1470| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1471      @(Inv_eq ???????) //
1472      whd in match (exec_expr ??? (Expr ??));
1473      whd in match (exec_expr ??? (Expr ??));
1474      [ 1: cases Hsim_expr
1475           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2/
1476           | 1: #Hexec_ok @SimOk * #val #trace
1477                cases (exec_expr ge en m castee) in Hexec_ok;
1478                [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct
1479                | 1: * #val #trace #Hexec_ok normalize nodelta
1480                     >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
1481                     >Htype_eq
1482                     normalize nodelta #H @H
1483                ]
1484           ]
1485      | 2: normalize @SimFail /2/
1486      ]
1487| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
1488      inversion (Htrue_inv ge en m)
1489      [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false
1490           #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct
1491      | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true
1492           inversion (Hfalse_inv ge en m)
1493           [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false
1494                #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct
1495           | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false
1496                >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg)
1497                [ 1,2: normalize //
1498                | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??));
1499                     elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq
1500                     cases Hexec_cond_sim
1501                     [ 2: * #error #Herror >Herror normalize @I
1502                     | 1: cases (exec_expr ge en m cond)
1503                          [ 2: #error #_ normalize @I
1504                          | 1: * #cond_val #cond_trace #Hcond_sim
1505                               >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1506
1507                               normalize nodelta
1508                               >Htype_cond_eq
1509                               cases (exec_bool_of_val cond_val (typeof cond1)) *
1510                               [ 3,4: normalize //
1511                               | 1,2: normalize in match (m_bind ?????);
1512                                      normalize in match (m_bind ?????);
1513                                      -Hexec_cond_sim -Hcond_sim -cond_val
1514                                      [ 1: (* true branch taken *)
1515                                           cases (exec_expr ge en m iftrue) in Hsmaller_true;
1516                                           [ 2: #error #_ @I
1517                                           | 1: * #val_true_branch #trace_true_branch
1518                                                cases (exec_expr ge en m iftrue1)
1519                                                [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)
1520                                                | 1: * #val_true1_branch #trace_true1_branch #Hsmaller
1521                                                     elim (smaller_integer_val_spec … Hsmaller)
1522                                                     #true_val * #true1_val * * * * #Htrue_val #Htrue1_val #Hcast
1523                                                     #Htrace_eq #Hsize_le normalize nodelta destruct
1524                                                     whd in match (smaller_integer_val ?????);
1525                                                     >sz_eq_identity normalize nodelta
1526                                                     >sz_eq_identity normalize nodelta
1527                                                     try @conj try @conj // ]
1528                                           ]
1529                                     | 2: (* false branch taken. Same proof as above, different arguments ... *)
1530                                           cases (exec_expr ge en m iffalse) in Hsmaller_false;
1531                                           [ 2: #error #_ @I
1532                                           | 1: * #val_false_branch #trace_false_branch
1533                                                cases (exec_expr ge en m iffalse1)
1534                                                [ 2: #error normalize in ⊢ (% → ?); #H @(False_ind … H)
1535                                                | 1: * #val_false1_branch #trace_false1_branch #Hsmaller
1536                                                     elim (smaller_integer_val_spec … Hsmaller)
1537                                                     #false_val * #false1_val * * * * #Hfalse_val #Hfalse1_val #Hcast
1538                                                     #Htrace_eq #Hsize_le normalize nodelta destruct
1539                                                     whd in match (smaller_integer_val ?????);
1540                                                     cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
1541                                                     [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
1542                                                          destruct (Htype_eq) @conj @refl
1543                                                     | 2: * #Hsize_eq #Hsg_eq destruct
1544                                                          >sz_eq_identity normalize nodelta
1545                                                          >sz_eq_identity normalize nodelta
1546                                                          try @conj try @conj try @refl assumption
1547                                                     ]
1548                                                ]
1549                                           ]
1550                                      ]
1551                              ]
1552                         ]
1553                    ]
1554               ]
1555          ]
1556     ]
1557| 38,39,40: destruct
1558   elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
1559   elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq
1560   elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq
1561   %1 try @refl
1562   [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
1563            cases (exec_expr ge en m cond) in Hsim_expr_cond;
1564            [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
1565            | 1,3,5: * #cond_val #cond_trace normalize nodelta
1566                cases (exec_expr ge en m cond1)
1567                [ 2,4,6: #error *
1568                         [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1569                                  #Habsurd destruct
1570                         | *: * #error #Habsurd destruct ]
1571                | 1,3,5: * #cond_val1 #cond_trace1 *
1572                         [ 2,4,6: * #error #Habsurd destruct
1573                         | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1574                             #Hcond_eq normalize nodelta destruct (Hcond_eq)
1575                             >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1))
1576                             [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro /
1577                             | 1,3,5: * (* true branch *)
1578                                [ 1,3,5:
1579                                 normalize in match (m_bind ?????);
1580                                 normalize in match (m_bind ?????);
1581                                 cases Hsim_expr_true
1582                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
1583                                 | 1,3,5: cases (exec_expr ge en m iftrue)
1584                                     [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1585                                     | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim
1586                                              >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉)))
1587                                              normalize nodelta @SimOk #a #H @H
1588                                     ]
1589                                 ]
1590                             | 2,4,6:
1591                                 normalize in match (m_bind ?????);
1592                                 normalize in match (m_bind ?????);
1593                                 cases Hsim_expr_false
1594                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
1595                                 | 1,3,5: cases (exec_expr ge en m iffalse)
1596                                     [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
1597                                     | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim
1598                                              >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉)))
1599                                              normalize nodelta @SimOk #a #H @H
1600                                     ]
1601                                 ]
1602                               ]
1603                             ]
1604                          ]
1605                ]
1606            ]
1607   | 2,4,6: normalize @SimFail /2 by ex_intro/
1608   ]
1609| 41,42: destruct
1610    elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1611    elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1612    %1 try @refl
1613    [ 1,3: whd in match (exec_expr ??? (Expr ??));
1614           whd in match (exec_expr ??? (Expr ??));
1615           cases Hsim_expr_lhs
1616           [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
1617           | 1,3: cases (exec_expr ge en m lhs)
1618              [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
1619              | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta
1620                     >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉)))
1621                     normalize nodelta >Htype_eq_lhs
1622                     cases (exec_bool_of_val lhs_val (typeof lhs1))
1623                       [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/
1624                     | 1,3: *
1625                         whd in match (m_bind ?????);
1626                         whd in match (m_bind ?????);
1627                         [ 2,3: (* lhs evaluates to true *)
1628                            @SimOk #a #H @H
1629                         | 1,4: cases Hsim_expr_rhs
1630                            [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/
1631                            | 1,3: cases (exec_expr ge en m rhs)
1632                                [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
1633                                | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim
1634                                       >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉)))
1635                                       normalize nodelta >Htype_eq_rhs
1636                                       @SimOk #a #H @H
1637                                ]
1638                            ]
1639                         ]
1640                      ]
1641            ]
1642         ]
1643   | 2,4: normalize @SimFail /2 by ex_intro/
1644   ]
1645| 43: destruct
1646      cases (type_eq_dec ty (Tint target_sz target_sg))
1647      [ 1: #Htype_eq >Htype_eq >type_eq_identity
1648           @(Inv_coerce_ok ??????? target_sz target_sg)
1649           [ 1,2: //
1650           | 3: cases target_sz cases target_sg normalize try @conj try @conj try @refl try @I ]
1651      | 2: #Hneq >(type_neq_not_identity … Hneq)
1652           %1 // @SimOk #a #H @H
1653      ]
1654| 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1655      %1 try @refl
1656      [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
1657           whd in match (exec_lvalue ????) in Hsim_lvalue;
1658           whd in match (exec_lvalue' ?????);
1659           whd in match (exec_lvalue' ?????);
1660           >Htype_eq
1661           cases (typeof rec_expr1) normalize nodelta
1662           [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
1663           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
1664           | 6,7: cases Hsim_lvalue
1665              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1666              | 1,3: cases (exec_lvalue ge en m rec_expr)
1667                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1668                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
1669                         whd in match (m_bind ?????);
1670                         @SimOk #a #H @H
1671                 ]
1672              ]
1673           ]
1674      | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??));
1675           >Htype_eq
1676           cases (typeof rec_expr1) normalize nodelta
1677           [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
1678           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
1679           | 6,7: cases Hsim_lvalue
1680              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1681              | 1,3: cases (exec_lvalue ge en m rec_expr)
1682                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
1683                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
1684                         whd in match (m_bind ?????);
1685                         @SimOk #a #H @H
1686                 ]
1687              ]
1688           ]
1689     ]
1690| 45: destruct
1691   inversion (Hinv ge en m)
1692   [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_
1693         @(Inv_coerce_ok ??????? src_sz src_sg)
1694         [ 1: >Htypeof_e1 //
1695         | 2: >Htypeof_e2 //
1696         | 3: whd in match (exec_expr ??? (Expr ??));
1697              whd in match (exec_expr ??? (Expr ??));
1698              cases (exec_expr ge en m e1) in Hsmaller;
1699              [ 2: #error normalize //
1700              | 1: * #val1 #trace1 cases (exec_expr ge en m e2)
1701                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … Habsurd)
1702                   | 1: * #val2 #trace #Hsmaller
1703                        elim (smaller_integer_val_spec … Hsmaller)
1704                        #i1 * #i2 * * * * #Hval1 #Hval2 #Hcast #Htrace_eq #Hsize_le
1705                        normalize nodelta destruct whd in match (smaller_integer_val ?????);
1706                        >sz_eq_identity >sz_eq_identity normalize nodelta
1707                        try @conj try @conj try @conj try @refl assumption
1708                   ]
1709               ]
1710         ]
1711   | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_
1712        >Hresult %1 try @refl
1713        [ 1: >Htype_eq //
1714        | 2: whd in match (exec_expr ??? (Expr ??));
1715             whd in match (exec_expr ??? (Expr ??));
1716             cases Hsim_expr
1717             [ 2: * #error #Hexec_error >Hexec_error normalize nodelta @SimFail /2 by ex_intro/
1718             | 1: cases (exec_expr ge en m e1)
1719                  [ 2: #error #_ normalize nodelta @SimFail /2 by ex_intro/
1720                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
1721                        normalize nodelta @SimOk #a #H @H
1722                  ]
1723             ]
1724        | 3: normalize @SimFail /2 by ex_intro/
1725        ]
1726   ]
1727| 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1728      whd in match (exec_expr ??? (Expr ??));
1729      whd in match (exec_expr ??? (Expr ??));
1730      %1 try @refl
1731        [ 1: >Htype_eq //
1732        | 2: whd in match (exec_expr ??? (Expr ??));
1733             whd in match (exec_expr ??? (Expr ??));
1734             cases Hsim_expr
1735             [ 2: * #error #Hexec_error >Hexec_error normalize nodelta @SimFail /2 by ex_intro/
1736             | 1: cases (exec_expr ge en m e1)
1737                  [ 2: #error #_ normalize nodelta @SimFail /2 by ex_intro/
1738                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
1739                        normalize nodelta @SimOk #a #H @H
1740                  ]
1741             ]
1742        | 3: normalize @SimFail
1743        ]
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753(* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and
1754   returns a flag stating whether the desired type was achieved and a simplified
1755   version of e. *)
1756let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
1757match e with
1758[ Expr ed ty ⇒
1759  match ed with
1760  [ Econst_int sz i ⇒
1761    match ty with
1762    [ Tint ty_sz sg ⇒
1763      match ty' with
1764      [ Tint sz' sg' ⇒
1765        (* IG: checking that the displayed type size [ty_sz] and [sz] are equal ... *)
1766        match sz_eq_dec sz ty_sz with
1767        [ inl Heq ⇒
1768          match simplify_int sz sz' sg sg' i with
1769          [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉
1770          | None ⇒ 〈false, e〉
1771          ]
1772        | inr _ ⇒
1773          (* The expression is ill-typed. *)
1774          〈false, e〉
1775        ]
1776      | _ ⇒ 〈false, e〉 ]
1777    | _ ⇒ 〈false, e〉 ]
1778  | Ederef e1 ⇒
1779      let ty1 ≝ typeof e1 in
1780      〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉
1781  | Eaddrof e1 ⇒
1782      let ty1 ≝ typeof e1 in
1783      〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉
1784  | Eunop op e1 ⇒
1785      let ty1 ≝ typeof e1 in
1786      〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉
1787  | Ebinop op e1 e2 ⇒
1788      if binop_simplifiable op then
1789        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in
1790        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
1791        if desired_type1 ∧ desired_type2 then
1792          〈true, Expr (Ebinop op e1' e2') ty'〉
1793        else
1794          let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
1795          let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
1796            〈false, Expr (Ebinop op e1' e2') ty〉
1797      else
1798        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in
1799        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in
1800          〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉
1801  | Ecast ty e1 ⇒
1802      match inttype_compare ty' ty with
1803      [ itc_le ⇒
1804        let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
1805        if desired_type then 〈true, e1'〉 else
1806          let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
1807          if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
1808      | itc_no ⇒
1809        let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
1810        if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
1811      ]
1812  | Econdition e1 e2 e3 ⇒
1813      let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *)
1814      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
1815      let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in
1816      if desired_type2 ∧ desired_type3 then
1817        〈true, Expr (Econdition e1' e2' e3') ty'〉
1818      else
1819        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
1820        let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in
1821          〈false, Expr (Econdition e1' e2' e3') ty〉
1822    (* Could probably do better with these, too. *)
1823  | Eandbool e1 e2 ⇒
1824      let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
1825      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
1826        〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉
1827  | Eorbool e1 e2 ⇒
1828      let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
1829      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
1830        〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉
1831  (* Could also improve Esizeof *)
1832  | Efield e1 f ⇒
1833      let ty1 ≝ typeof e1 in
1834      〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉
1835  | Ecost l e1 ⇒
1836      let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
1837        〈desired_type, Expr (Ecost l e1') (typeof e1')〉
1838  | _ ⇒ 〈type_eq ty ty',e〉
1839  ]
1840].
1841
1842definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)).
1843
1844let rec simplify_statement (s:statement) : statement ≝
1845match s with
1846[ Sskip ⇒ Sskip
1847| Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2)
1848| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
1849| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
1850| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
1851| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
1852| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
1853| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
1854| Sbreak ⇒ Sbreak
1855| Scontinue ⇒ Scontinue
1856| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
1857| Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls)
1858| Slabel l s1 ⇒ Slabel l (simplify_statement s1)
1859| Sgoto l ⇒ Sgoto l
1860| Scost l s1 ⇒ Scost l (simplify_statement s1)
1861]
1862and simplify_ls ls ≝
1863match ls with
1864[ LSdefault s ⇒ LSdefault (simplify_statement s)
1865| LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls')
1866].
1867
1868definition simplify_function : function → function ≝
1869λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).
1870
1871definition simplify_fundef : clight_fundef → clight_fundef ≝
1872λf. match f with
1873  [ CL_Internal f ⇒ CL_Internal (simplify_function f)
1874  | _ ⇒ f
1875  ].
1876
1877definition simplify_program : clight_program → clight_program ≝
1878λp. transform_program … p simplify_fundef.
1879
1880
1881(* We have to prove that simplify_expr doesn't alter the semantics. Since expressions are pure,
1882 * we state that expressions before and after conversion should evaluate to the same value, or
1883 * fail in a similar way when placed into a given context. *)
1884
1885
1886let rec expr_ind2
1887    (P : expr → Prop) (Q : expr_descr → Prop)
1888    (IE : ∀ed. ∀t. Q ed → P (Expr ed t))
1889    (Iconst_int : ∀sz, i. Q (Econst_int sz i))
1890    (Iconst_float : ∀f. Q (Econst_float f))
1891    (Ivar : ∀id. Q (Evar id))
1892    (Ideref : ∀e. P e → Q (Ederef e))
1893    (Iaddrof : ∀e. P e → Q (Eaddrof e))
1894    (Iunop : ∀op,arg. P arg → Q (Eunop op arg))
1895    (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2))
1896    (Icast : ∀t. ∀e . P e →  Q (Ecast t e))
1897    (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3))
1898    (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2))
1899    (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2))
1900    (Isizeof : ∀t. Q (Esizeof t))
1901    (Ifield : ∀e,f. P e → Q (Efield e f))
1902    (Icost : ∀c,e. P e → Q (Ecost c e))
1903    (e : expr) on e : P e ≝
1904match e with
1905[ 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) ]
1906
1907and expr_desc_ind2
1908    (P : expr → Prop) (Q : expr_descr → Prop)
1909    (IE : ∀ed. ∀t. Q ed → P (Expr ed t))
1910    (Iconst_int : ∀sz, i. Q (Econst_int sz i))
1911    (Iconst_float : ∀f. Q (Econst_float f))
1912    (Ivar : ∀id. Q (Evar id))
1913    (Ideref : ∀e. P e → Q (Ederef e))
1914    (Iaddrof : ∀e. P e → Q (Eaddrof e))
1915    (Iunop : ∀op,arg. P arg → Q (Eunop op arg))
1916
1917    (Ibinop : ∀op,arg1,arg2. P arg1 → P arg2 → Q (Ebinop op arg1 arg2))
1918    (Icast : ∀t. ∀e . P e →  Q (Ecast t e))
1919    (Icond : ∀e1,e2,e3. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3))
1920    (Iandbool : ∀e1,e2. P e1 → P e2 → Q (Eandbool e1 e2))
1921    (Iorbool : ∀e1,e2. P e1 → P e2 → Q (Eorbool e1 e2))
1922    (Isizeof : ∀t. Q (Esizeof t))
1923    (Ifield : ∀e,f. P e → Q (Efield e f))
1924    (Icost : ∀c,e. P e → Q (Ecost c e))
1925    (ed : expr_descr) on ed : Q ed ≝
1926match ed with
1927[ Econst_int sz i ⇒ Iconst_int sz i
1928| Econst_float f ⇒ Iconst_float f
1929| Evar id ⇒ Ivar id
1930| 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)
1931| 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)
1932| 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)
1933| 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)
1934| 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)
1935| 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)
1936| 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)
1937| 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)
1938| Esizeof t ⇒ Isizeof t
1939| 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)
1940| 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.