Changeset 1970


Ignore:
Timestamp:
May 18, 2012, 9:18:07 PM (7 years ago)
Author:
garnier
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r1873 r1970  
    11include "Clight/Csyntax.ma".
    22include "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 ... *)
    39
    410(* Attempt to remove unnecessary integer casts in Clight programs.
     
    1420 *)
    1521
     22
     23
    1624(* Attempt to squeeze integer constant into a given type.
    1725
    1826   This might be too conservative --- if we're going to cast it anyway, can't
    1927   I just ignore the fact that the integer doesn't fit?
    20  *)
    21 
     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. *)
    2233let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
    2334match n return λn. BitVector (n+S m) → option (BitVector (S m)) with
     
    2637] v.
    2738
     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, … *)
    2858definition pred_bitsize_of_intsize : intsize → nat ≝
    2959λsz. pred (bitsize_of_intsize sz).
     
    3262λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ].
    3363
     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*)
    3472let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝
    3573  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) *)
    3678  match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz')
    3779      return λn,m,x.BitVector (S n) → option (BitVector (S m)) with
    3880  [ nat_lt _ _ ⇒ λi. None ?   (* refuse to make constants larger *)
    3981  | nat_eq _ ⇒ λi. Some ? i
    40   | nat_gt x y ⇒ λ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       *)
    4189      match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with
    42       [ Some i' ⇒ if signed sg' then if eq_b bit (head' … i') then Some ? i' else None ? else Some ? i'
     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'
    4396      | None ⇒ None ?
    4497      ]
     
    47100qed.
    48101
    49 (* Compare integer types to decide if we can omit casts. *)
    50 
    51 inductive inttype_cmp : Type[0] ≝
    52 | itc_le : inttype_cmp
    53 | itc_no : inttype_cmp.
    54 
    55 definition inttype_compare ≝
    56 λt1,t2.
    57 match t1 with
    58 [ Tint sz sg ⇒
    59   match t2 with
    60   [ Tint sz' sg' ⇒
    61       match sz with
    62       [ I8 ⇒ itc_le
    63       | I16 ⇒ match sz' with [ I8 ⇒ itc_no | _ ⇒ itc_le ]
    64       | I32 ⇒ match sz' with [ I32 ⇒ itc_le | _ ⇒ itc_no ]
     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
    65329      ]
    66   | _ ⇒ itc_no
     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 ⊢ (???%); %
    67446  ]
    68 | _ ⇒ itc_no
     447qed.
     448
     449
     450lemma split_zero2:
     451  ∀A,m.
     452  ∀v: Vector A m.
     453    〈[[]], v〉 = split' A 0 m v.
     454  #A #m #v
     455  elim v
     456  [ %
     457  | #n #hd #tl #ih
     458    normalize in ⊢ (???%); %
     459  ]
     460qed.
     461
     462(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
     463 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
     464axiom split_succ:
     465  ∀A, m, n.
     466  ∀l: Vector A m.
     467  ∀r: Vector A n.
     468  ∀v: Vector A (m + n).
     469  ∀hd.
     470    v = l@@r → (〈l, r〉 = split ? m n v → 〈hd:::l, r〉 = split ? (S m) n (hd:::v)).
     471
     472axiom split_succ2:
     473  ∀A, m, n.
     474  ∀l: Vector A m.
     475  ∀r: Vector A n.
     476  ∀v: Vector A (m + n).
     477  ∀hd.
     478    v = l@@r → (〈l, r〉 = split' ? m n v → 〈hd:::l, r〉 = split' ? (S m) n (hd:::v)).
     479     
     480lemma split_prod2:
     481  ∀A,m,n.
     482  ∀p: Vector A (m + n).
     483  ∀v: Vector A m.
     484  ∀q: Vector A n.
     485    p = v@@q → 〈v, q〉 = split' A m n p.
     486  #A #m
     487  elim m
     488  [ #n #p #v #q #hyp
     489    >hyp <(vector_append_zero A n q v)
     490    >(prod_vector_zero_eq_left A …)
     491    @split_zero2
     492  | #r #ih #n #p #v #q #hyp
     493    >hyp
     494    cases (Vector_Sn A r v)
     495    #hd #exists
     496    cases exists
     497    #tl #jmeq >jmeq
     498    @split_succ2 [1: % |2: @ih % ]
     499  ]
     500qed.
     501
     502lemma split_prod:
     503  ∀A,m,n.
     504  ∀p: Vector A (m + n).
     505  ∀v: Vector A m.
     506  ∀q: Vector A n.
     507    p = v@@q → 〈v, q〉 = split A m n p.
     508  #A #m
     509  elim m
     510  [ #n #p #v #q #hyp
     511    >hyp <(vector_append_zero A n q v)
     512    >(prod_vector_zero_eq_left A …)
     513    @split_zero
     514  | #r #ih #n #p #v #q #hyp
     515    >hyp
     516    cases (Vector_Sn A r v)
     517    #hd #exists
     518    cases exists
     519    #tl #jmeq >jmeq
     520    @split_succ [1: % |2: @ih % ]
     521  ]
     522qed.
     523
     524
     525(* Stolen from AssemblyProof.ma *)
     526lemma super_rewrite2:
     527 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
     528  ∀P: ∀m. Vector A m → Prop.
     529   n=m → v1 ≃ v2 → P n v1 → P m v2.
     530 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
     531qed.
     532
     533lemma vector_cons_append:
     534  ∀A: Type[0].
     535  ∀n: nat.
     536  ∀e: A.
     537  ∀v: Vector A n.
     538    e ::: v = [[ e ]] @@ v.
     539  # A # N # E # V
     540  elim V
     541  [ normalize %
     542  | # NN # AA # VV # IH
     543    normalize
     544    %
     545qed.
     546
     547lemma vector_cons_append2:
     548  ∀A: Type[0].
     549  ∀n, m: nat.
     550  ∀v: Vector A n.
     551  ∀q: Vector A m.
     552  ∀hd: A.
     553    hd:::(v@@q) = (hd:::v)@@q.
     554  #A #n #m #v #q
     555  elim v
     556  [ #hd %
     557  | #n' #hd' #tl' #ih #hd' <ih %
     558  ]
     559qed.
     560
     561lemma jmeq_cons_vector_monotone:
     562  ∀A: Type[0].
     563  ∀m, n: nat.
     564  ∀v: Vector A m.
     565  ∀q: Vector A n.
     566  ∀prf: m = n.
     567  ∀hd: A.
     568    v ≃ q → hd:::v ≃ hd:::q.
     569  #A #m #n #v #q #prf #hd #E
     570  @(super_rewrite2 A … E)
     571  [ assumption | % ]
     572qed.
     573
     574lemma vector_associative_append:
     575  ∀A: Type[0].
     576  ∀n, m, o:  nat.
     577  ∀v: Vector A n.
     578  ∀q: Vector A m.
     579  ∀r: Vector A o.
     580    ((v @@ q) @@ r)
     581    ≃
     582    (v @@ (q @@ r)).
     583  #A #n #m #o #v #q #r
     584  elim v
     585  [ %
     586  | #n' #hd #tl #ih
     587    <(vector_cons_append2 A … hd)
     588    @jmeq_cons_vector_monotone
     589    //
     590  ]
     591qed.
     592
     593lemma tail_eat_cons : ∀A. ∀n. ∀hd:A. ∀v:Vector A n. tail A n (hd ::: v) = v.
     594#A #n #hd #v normalize //
     595qed.
     596
     597lemma tail_eat_pad : ∀A. ∀padelt. ∀padlen, veclen. ∀v:Vector A veclen.
     598  tail A ? (pad_vector A padelt (S padlen) veclen v) = pad_vector A padelt padlen veclen v.
     599# A #padelt #padlen #veclen #v
     600normalize //
     601qed.
     602
     603lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
     604#s1 #v normalize elim s1 normalize nodelta
     605normalize in v;
     606elim (split_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
     607[ 2,4: //
     608| 1,3: #l * #r normalize nodelta #Eq1
     609       <(split_prod bool 16 16 … Eq1)
     610       elim (split_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
     611       [ 2,4: //
     612       | 1,3: #lr * #rr normalize nodelta #Eq2
     613              <(split_prod bool 8 8 … Eq2)
     614              cut (v = (l @@ lr) @@ rr)
     615              [ 1,3 : destruct >(vector_associative_append ? 16 8) //
     616              | 2,4: #Hrewrite destruct
     617                     <(split_prod bool 24 8 … Hrewrite) @refl
     618              ]
     619       ]
     620] qed.
     621
     622lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v.
     623#s1 #s2 * * #v elim s1 elim s2
     624normalize #H try @refl
     625@(False_ind … H)
     626qed.
     627
     628lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v.
     629* * #v normalize // qed.
     630
     631lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v).
     632#s1 #s2 #v >cast_decompose >cast_idempotent
     633[ 1: @refl | 2: // ]
     634qed.
     635
     636lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
     637   size_lt c_sz a_sz → size_lt c_sz b_sz →
     638   (cast_int_int a_sz a_sg c_sz val =
     639        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).       
     640* #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??);
     641#Hlt1 #Hlt2
     642[ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27:
     643  @(False_ind … Hlt1) @(False_ind … Hlt2)
     644| 13,25,26: >cast_identity elim a_sg elim b_sg normalize //
     645| 22: normalize elim b_sg elim a_sg normalize
     646      normalize in val;
     647      elim (split_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
     648      [ 2,4,6,8: normalize //
     649      | 1,3,5,7: #left * #right normalize #Eq1
     650                 <(split_prod bool 16 16 … Eq1)
     651                 elim (split_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
     652                 [ 2,4,6,8: //
     653                 | 1,3,5,7: #rightleft * #rightright normalize #Eq2
     654                            <(split_prod bool 8 8 … Eq2)
     655                            cut (val = (left @@ rightleft) @@ rightright)
     656                            [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
     657                            | 2,4,6,8: #Hrewrite destruct
     658                                       <(split_prod bool 24 8 … Hrewrite) @refl
     659                            ]
     660                 ]
     661     ]
     662| 16: elim b_sg elim a_sg >cast_collapse @refl
     663] qed.
     664
     665lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
     666   size_le c_sz a_sz → size_le c_sz b_sz →
     667   (cast_int_int a_sz a_sg c_sz val =
     668        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).
     669#a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b
     670cases (size_lt_dec c_sz a_sz)
     671cases (size_lt_dec c_sz b_sz)
     672[ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb)
     673| 2: #Hnltb #Hlta
     674  cases (size_not_lt_to_ge  … Hnltb)
     675  [ 1: #Heq destruct >cast_identity //
     676  | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb))
     677  ]
     678| 3: #Hltb #Hnlta 
     679  cases (size_not_lt_to_ge  … Hnlta)
     680  [ 1: #Heq destruct >cast_idempotent //
     681  | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
     682  ]
     683| 4: #Hnltb #Hnlta
     684  cases (size_not_lt_to_ge  … Hnlta) 
     685  cases (size_not_lt_to_ge  … Hnltb)
     686  [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity //
     687  | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb))
     688  | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
     689  | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
     690  ]
     691] qed.
     692
     693let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝
     694match v with
     695[ None ⇒ None ?
     696| Some v ⇒
     697  match v with
     698  [ Vint sz i ⇒
     699    match sz_eq_dec sz expected_size with
     700    [ inl Heq ⇒ Some ??
     701    | inr _ ⇒ None ?
     702    ]
     703  | _ ⇒ None ?
     704  ]
    69705].
     706>Heq in i; #i @i qed.
     707
     708(* cast_int_int behaves as truncate (≃ split) when downsizing *)
     709(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)
     710
     711lemma split_to_truncate : ∀m,n,i. (\snd  (split bool m n i)) = truncate  m n i.
     712#m #n #i normalize // qed.
     713
     714(* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *)
     715
     716lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
     717                               (addition_n (bitsize_of_intsize target_sz)
     718                                    (cast_int_int src_sz sg target_sz lhs_int)
     719                                    (cast_int_int src_sz sg target_sz rhs_int)
     720                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
     721#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
     722elim src_sz in Hlt lhs_int rhs_int; elim target_sz
     723[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
     724| *: elim sg #_
     725  normalize in match (bitsize_of_intsize ?);
     726  normalize in match (bitsize_of_intsize ?);
     727  #lint #rint
     728  normalize in match (cast_int_int ????);
     729  normalize in match (cast_int_int ????);
     730  whd in match (addition_n ???);
     731  whd in match (addition_n ???) in ⊢ (???%);
     732  >split_to_truncate >split_to_truncate
     733  <truncate_add_with_carries
     734  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
     735  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false);
     736  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false);
     737  ]
     738  * #result #carry
     739  normalize nodelta //
     740qed.
     741
     742lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
     743                               (addition_n (bitsize_of_intsize target_sz)
     744                                    (cast_int_int src_sz sg target_sz lhs_int)
     745                                    (cast_int_int src_sz sg target_sz rhs_int)
     746                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
     747#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
     748>cast_identity >cast_identity >cast_identity // qed.
     749
     750lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
     751                               (addition_n (bitsize_of_intsize target_sz)
     752                                    (cast_int_int src_sz sg target_sz lhs_int)
     753                                    (cast_int_int src_sz sg target_sz rhs_int)
     754                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
     755#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
     756cases (sz_eq_dec target_sz src_sz)
     757[ 1: #Heq @(integer_add_cast_eq … Heq)
     758| 2: #Hneq cut (size_lt target_sz src_sz)
     759     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
     760           #_ * #H @(H … (refl ??))
     761     | 2: #Hlt @(integer_add_cast_lt … Hlt)
     762     ]
     763] qed.
     764
     765lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl.
     766#l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len
     767@(ex_intro … tl)
     768>Heq >Heq
     769elim (split_eq2 … tl) #l * #r #Eq
     770normalize
     771 <(split_prod bool n m tl l r Eq)
     772 <(split_prod2 bool n m tl l r Eq)
     773 normalize //
     774qed.
     775
     776
     777lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i).
     778#m elim m
     779[ 1: #n #i normalize in i;
     780     whd in match (truncate ???);
     781     whd in match (truncate ???) in ⊢ (???%);
     782     <split_zero <split_zero //
     783| 2: #m' #Hind #n #i normalize in i;
     784     elim (Vector_Sn … i) #hd * #tl #Heq     
     785     whd in match (two_complement_negation (S ?) ?);     
     786     >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?);
     787     whd in match (two_complement_negation ??) in ⊢ (??%?);
     788     lapply (Hind ? tl) #H
     789     whd in match (two_complement_negation ??) in H;
     790(* trying to reduce add_with_carries *)     
     791     normalize in match (S m'+n);
     792     whd in match (zero ?) in ⊢ (???%);
     793     >Heq in match (negation_bv ??) in ⊢ (???%);
     794     whd in match (negation_bv ??) in ⊢ (???%);
     795     >add_with_carries_unfold in ⊢ (???%);
     796(*     >truncate_tail *)
     797     normalize in ⊢ (???%);
     798     cases hd normalize nodelta
     799     [ 1,2: <add_with_carries_unfold  in ⊢ (???%); (* Good. Some progress. *)
     800          (* try to transform the rhs of H into what we need. *)     
     801          whd in match (two_complement_negation ??) in H:(???%);
     802          lapply H -H
     803          generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true);
     804          * #Left #Right normalize nodelta
     805          #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒  ?])))));
     806          #b >(split_to_truncate (S m')) >truncate_tail
     807          cases b
     808          normalize nodelta
     809          normalize in match (tail ???); @H
     810     ]
     811] qed. (* This was painful. *)
     812     
     813lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
     814                               (subtraction (bitsize_of_intsize target_sz)
     815                                    (cast_int_int src_sz sg target_sz lhs_int)
     816                                    (cast_int_int src_sz sg target_sz rhs_int)
     817                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
     818#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
     819elim src_sz in Hlt lhs_int rhs_int; elim target_sz
     820[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
     821| *: elim sg #_
     822  normalize in match (bitsize_of_intsize ?);
     823  normalize in match (bitsize_of_intsize ?);
     824  #lint #rint
     825  normalize in match (cast_int_int ????);
     826  normalize in match (cast_int_int ????);
     827  whd in match (subtraction ???);
     828  whd in match (subtraction ???) in ⊢ (???%);
     829  >split_to_truncate >split_to_truncate
     830  >integer_neg_trunc <truncate_add_with_carries
     831  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
     832  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false);
     833  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false);
     834  ]
     835  * #result #carry
     836  normalize nodelta //
     837qed.
     838
     839lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
     840                               (subtraction (bitsize_of_intsize target_sz)
     841                                    (cast_int_int src_sz sg target_sz lhs_int)
     842                                    (cast_int_int src_sz sg target_sz rhs_int)
     843                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
     844#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
     845>cast_identity >cast_identity >cast_identity //
     846qed.
     847
     848lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
     849                               (subtraction (bitsize_of_intsize target_sz)
     850                                    (cast_int_int src_sz sg target_sz lhs_int)
     851                                    (cast_int_int src_sz sg target_sz rhs_int)
     852                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
     853#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
     854cases (sz_eq_dec target_sz src_sz)
     855[ 1: #Heq @(integer_sub_cast_eq … Heq)
     856| 2: #Hneq cut (size_lt target_sz src_sz)
     857     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
     858           #_ * #H @(H … (refl ??))
     859     | 2: #Hlt @(integer_sub_cast_lt … Hlt)
     860     ]
     861] qed.
     862     
     863lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg.
     864* * // qed.
     865
     866lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg.
     867* * // qed.
     868
     869(* This ought to be somewhere else. Lemma used in proving the correctness of the Binop case. *)
     870lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
     871* * normalize #H @conj // qed.
     872
     873lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le  sz' sz.
     874* #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.
    70875
    71876(* Operations where it is safe to use a smaller integer type on the assumption
    72877   that we would cast it down afterwards anyway. *)
    73 
    74878definition binop_simplifiable ≝
    75879λ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
     1291                                             >classify_add_int >classify_add_int 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 //
     1297                                             >integer_add_cast_le //                                             
     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
    761752
    771753(* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and
    781754   returns a flag stating whether the desired type was achieved and a simplified
    791755   version of e. *)
    80 
    811756let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
    821757match e with
     
    851760  [ Econst_int sz i ⇒
    861761    match ty with
    87     [ Tint _ sg ⇒
     1762    [ Tint ty_sz sg ⇒
    881763      match ty' with
    891764      [ Tint sz' sg' ⇒
    90         match simplify_int sz sz' sg sg' i with
    91         [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉
    92         | None ⇒ 〈false, e〉
     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〉
    931775        ]
    941776      | _ ⇒ 〈false, e〉 ]
     
    1951877definition simplify_program : clight_program → clight_program ≝
    1961878λ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 TracChangeset for help on using the changeset viewer.