Changeset 2588


Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

Location:
src/Clight
Files:
1 added
12 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2560 r2588  
    1919    | _ ⇒ Error ? (msg TypeMismatch)
    2020    ]
    21 (*  | Vfloat f ⇒ match ty with
    22     [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
    23     | _ ⇒ Error ? (msg TypeMismatch)
    24     ]*)
    2521  | Vptr _ ⇒ match ty with
    2622    [ Tpointer _ ⇒ OK ? true
     
    3834  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    3935  | #ptr #ty %{ true} % //
    40 (*  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //; *)
    4136  | * #sg %{ false} % //
    4237  | #t %{ false} % //;
    43 (*  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;*)
    4438  ]
    4539qed.
     
    215209      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    216210      do 〈v2,tr2〉 ← exec_expr ge en m a2;
    217       do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
     211      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty);
    218212      OK ? 〈v,tr1⧺tr2〉
    219213  | Econdition a1 a2 a3 ⇒
     
    228222      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    229223      do b1 ← exec_bool_of_val v1 (typeof a1);
    230       match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
     224      match b1 return λ_.res (val×trace) with
     225      [ true ⇒
     226        match cast_bool_to_target ty (Some ? Vtrue) with
     227        [ None ⇒
     228          Error ? (msg BadlyTypedTerm)
     229        | Some vtr ⇒
     230          OK ? 〈vtr,tr1〉 ]
     231      | false ⇒
    231232        do 〈v2,tr2〉 ← exec_expr ge en m a2;
    232233        do b2 ← exec_bool_of_val v2 (typeof a2);
    233         OK ? 〈of_bool b2, tr1⧺tr2〉 ]
     234        match cast_bool_to_target ty (Some ? (of_bool b2)) with
     235        [ None ⇒
     236          Error ? (msg BadlyTypedTerm)
     237        | Some v2 ⇒
     238          OK ? 〈v2,tr1⧺tr2〉 ] ]
    234239  | Eandbool a1 a2 ⇒
    235240      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    236241      do b1 ← exec_bool_of_val v1 (typeof a1);
    237       match b1 return λ_.res (val×trace) with [ true ⇒
     242      match b1 return λ_.res (val×trace) with
     243      [ true ⇒
    238244        do 〈v2,tr2〉 ← exec_expr ge en m a2;
    239245        do b2 ← exec_bool_of_val v2 (typeof a2);
    240         OK ? 〈of_bool b2, tr1⧺tr2〉
    241       | false ⇒ OK ? 〈Vfalse,tr1〉 ]
     246        match cast_bool_to_target ty (Some ? (of_bool b2)) with
     247        [ None ⇒
     248          Error ? (msg BadlyTypedTerm)
     249        | Some v2 ⇒
     250          OK ? 〈v2, tr1⧺tr2〉
     251        ]
     252      | false ⇒
     253        match cast_bool_to_target ty (Some ? Vfalse) with
     254        [ None ⇒
     255          Error ? (msg BadlyTypedTerm)
     256        | Some vfls ⇒
     257          OK ? 〈vfls,tr1〉 ]
     258      ]
    242259  | Ecast ty' a ⇒
    243260      do 〈v,tr〉 ← exec_expr ge en m a;
     
    267284          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    268285          do delta ← field_offset i fList;
    269           OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
     286          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I16 delta)〉,tr〉
    270287      | Tunion id fList ⇒
    271288          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
  • src/Clight/CexecComplete.ma

    r2468 r2588  
    194194    >(yields_eq ??? H5)
    195195    @refl
    196 | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     196| #e1 #e2 #ty #v1 #tr #vres #H1 #H2 #Hcast #H3 whd in ⊢ (??%?);
    197197    >(yields_eq ??? H3) whd in ⊢ (??%?);
    198198    >(yields_eq ??? (bool_of_true ?? H2))
    199     @refl
    200 | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
     199    >Hcast @refl
     200| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #vres #H1 #H2 #H3 #H4 #Hcast #H5 #H6 whd in ⊢ (??%?);
    201201    >(yields_eq ??? H5) whd in ⊢ (??%?);
    202202    >(yields_eq ??? (bool_of_false ?? H2))
     
    204204    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
    205205    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
    206     @refl
    207 | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     206    >Hcast
     207    @refl
     208| #e1 #e2 #ty #v1 #tr #vres #H1 #H2 #Hcast #H3 whd in ⊢ (??%?);
    208209    >(yields_eq ??? H3) whd in ⊢ (??%?);
    209210    >(yields_eq ??? (bool_of_false ?? H2))
    210     @refl
    211 | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
     211    >Hcast
     212    @refl
     213| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #vres #H1 #H2 #H3 #H4 #Hcast #H5 #H6 whd in ⊢ (??%?);
    212214    >(yields_eq ??? H5) whd in ⊢ (??%?);
    213215    >(yields_eq ??? (bool_of_true ?? H2))
     
    215217    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
    216218    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
     219    >Hcast normalize
    217220    @refl
    218221| #e #ty #ty' #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
  • src/Clight/CexecSound.ma

    r2468 r2588  
    185185    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    186186    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
     187    normalize nodelta
    187188    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    188         @bind_OK #b2 #eb2
    189         @(eval_Eandbool_2 … He1 … He2)
    190         [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
    191     | @(eval_Eandbool_1 … He1) @(bool_of … Hb1)
     189        @bind_OK #b2 #eb2 whd in match (cast_bool_to_target ??);
     190        cases ty
     191        [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     192        try @I normalize nodelta
     193        @(eval_Eandbool_2 … (of_bool b2) … He1 … He2)
     194        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ]
     195    | cases ty
     196      [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     197      try @I
     198      @(eval_Eandbool_1 … He1) [ @(bool_of … Hb1) | @refl ]
    192199    ]
    193200| #ty #e1 #e2 #He1 #He2
    194201    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    195202    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    196     [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
     203    normalize nodelta
     204    [ cases ty
     205      [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     206      try @I
     207      @(eval_Eorbool_1 … He1) [ @(bool_of … Hb1) | @refl ]
    197208    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    198209        @bind_OK #b2 #eb2
    199         @(eval_Eorbool_2 … He1 … He2)
    200         [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
     210        cases ty
     211        [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     212        try @I
     213        @(eval_Eorbool_2 … (of_bool b2) … He1 … He2)
     214        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ]
    201215    ]
    202216| #ty #ty' cases ty try #sz try #sg try #x //
     
    235249| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    236250| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    237 | #a #b #c #d #e #f #g #bad destruct (bad);
    238 | #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
    239 | #a #b #c #d #e #f #g #bad destruct (bad);
    240 | #a #b #c #d #e #f #g #h #i #j #k #l #bad  destruct (bad);
     251| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
     252| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
     253| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
     254| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
    241255| #a #b #c #d #e #f #g #h #bad destruct (bad);
    242256| #a #b #c #d #e #f #bad destruct (bad);
  • src/Clight/Csem.ma

    r2569 r2588  
    129129].
    130130
    131 let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     131(* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma.
     132 * operation done on 32 bits and cast down to the target size using sign_ext or zero_ext, according to the
     133 * sign of the target type. We have to do the same in toCminor.ma
     134 * At least two things are ugly here : the fact that offsets are 32 bits (our arch is 8 bit right ?), and the downcast.
     135 * TODO: check the C standard to see if the following alternative is meaningful ?
     136 *   . the division can directly take as an argument a target size. There is also two [repr], one
     137 *     with type nat → bvint I32 (used here), one with type ∀sz. nat → bvint sz. Matching changes
     138 *     would have to be done in Cminor.
     139 *)
     140let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) (target:type) : option val ≝
    132141  match classify_sub t1 t2 with
    133142  [ sub_case_ii _ _ ⇒                (**r integer subtraction *)
     
    149158  | sub_case_pp _ _ ty _ ⇒             (**r pointer minus pointer *)
    150159      match v1 with
    151       [ Vptr ptr1 ⇒ match v2 with
     160      [ Vptr ptr1 ⇒
     161        match v2 with
    152162        [ Vptr ptr2 ⇒
    153163          if eq_block (pblock ptr1) (pblock ptr2) then
    154164            if eqb (sizeof ty) 0 then None ?
    155             else match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
    156                  [ None ⇒ None ?
    157                  | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
    158                  ]
     165            else match target with
     166                 [ Tint tsz tsg ⇒
     167                   match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
     168                   [ None ⇒ None ?
     169                   | Some v ⇒
     170                     Some ? (Vint tsz (zero_ext ?? v))
     171                     (*Some ? (Vint tsz v)  XXX choose size from result type? *)
     172                   ]
     173                 | _ ⇒ None ? ]
    159174          else None ?
    160175        | _ ⇒ None ? ]
    161       | Vnull ⇒ match v2 with [ Vnull ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
     176      | Vnull ⇒
     177        match v2 with
     178        [ Vnull ⇒
     179          match target with
     180          [ Tint tsz tsg ⇒
     181            Some ? (Vint tsz (*XXX*) (zero ?))
     182          | _ ⇒ None ? ]
     183        | _ ⇒ None ? ]
    162184      | _ ⇒ None ? ]
    163185  | sub_default _ _ ⇒ None ?
    164186  ].
     187
    165188
    166189let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     
    175198  | aop_default _ _ ⇒
    176199      None ?
    177 ].
     200  ].
    178201
    179202let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     
    285308  | _   ⇒ None ?
    286309  ].
    287  
     310
    288311let rec sem_cmp (c:comparison)
    289312                  (v1: val) (t1: type) (v2: val) (t2: type)
     
    327350  ].
    328351
     352definition cast_bool_to_target : type → option val → option val ≝
     353  λty,optv.
     354  match optv with
     355  [ None ⇒ None ?
     356  | Some v ⇒
     357    match ty with
     358    [ Tint sz sg ⇒
     359        Some ? (zero_ext sz v)
     360    | _ ⇒ None ? ]
     361  ].
     362
     363lemma cast_bool_to_target_inversion : ∀ty,v,vres.
     364  cast_bool_to_target ty (Some ? v) = Some ? vres →
     365  ∃sz,sg. ty = Tint sz sg ∧ vres = zero_ext sz v.
     366#ty #v #vres
     367cases ty
     368[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
     369whd in ⊢ ((??%%) → ?);
     370#Heq destruct
     371%{sz} %{sg} @conj try @refl
     372qed.
     373
    329374definition sem_unary_operation
    330375            : unary_operation → val → type → option val ≝
     
    339384    (op: binary_operation)
    340385    (v1: val) (t1: type) (v2: val) (t2:type)
    341     (m: mem): option val ≝
     386    (m: mem)
     387    (ty: type): option val ≝
    342388  match op with
    343389  [ Oadd ⇒ sem_add v1 t1 v2 t2
    344   | Osub ⇒ sem_sub v1 t1 v2 t2
     390  | Osub ⇒ sem_sub v1 t1 v2 t2 ty
    345391  | Omul ⇒ sem_mul v1 t1 v2 t2
    346392  | Omod ⇒ sem_mod v1 t1 v2 t2
     
    351397  | Oshl ⇒ sem_shl v1 v2
    352398  | Oshr ⇒ sem_shr v1 t1 v2 t2
    353   | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m
    354   | One ⇒ sem_cmp Cne v1 t1 v2 t2 m
    355   | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m
    356   | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m
    357   | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m
    358   | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m
     399  | Oeq ⇒ cast_bool_to_target ty (sem_cmp Ceq v1 t1 v2 t2 m)
     400  | One ⇒ cast_bool_to_target ty (sem_cmp Cne v1 t1 v2 t2 m)
     401  | Olt ⇒ cast_bool_to_target ty (sem_cmp Clt v1 t1 v2 t2 m)
     402  | Ogt ⇒ cast_bool_to_target ty (sem_cmp Cgt v1 t1 v2 t2 m)
     403  | Ole ⇒ cast_bool_to_target ty (sem_cmp Cle v1 t1 v2 t2 m)
     404  | Oge ⇒ cast_bool_to_target ty (sem_cmp Cge v1 t1 v2 t2 m)
    359405  ].
    360406
     
    554600      eval_expr ge e m a1 v1 tr1 →
    555601      eval_expr ge e m a2 v2 tr2 →
    556       sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v →
     602      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty = Some ? v →
    557603      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2)
    558604  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2.
     
    566612      eval_expr ge e m a3 v3 tr2 →
    567613      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2)
    568   | eval_Eorbool_1: ∀a1,a2,ty,v1,tr.
     614  | eval_Eorbool_1: ∀a1,a2,ty,v1,tr,vres.
    569615      eval_expr ge e m a1 v1 tr →
    570616      is_true v1 (typeof a1) →
    571       eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr
    572   | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     617      cast_bool_to_target ty (Some ? Vtrue) = Some ? vres →
     618      eval_expr ge e m (Expr (Eorbool a1 a2) ty) vres tr
     619  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2,vres.
    573620      eval_expr ge e m a1 v1 tr1 →
    574621      is_false v1 (typeof a1) →
    575622      eval_expr ge e m a2 v2 tr2 →
    576623      bool_of_val v2 (typeof a2) v →
    577       eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2)
    578   | eval_Eandbool_1: ∀a1,a2,ty,v1,tr.
     624      cast_bool_to_target ty (Some ? v) = Some ? vres →     
     625      eval_expr ge e m (Expr (Eorbool a1 a2) ty) vres (tr1⧺tr2)
     626  | eval_Eandbool_1: ∀a1,a2,ty,v1,tr,vres.
    579627      eval_expr ge e m a1 v1 tr →
    580628      is_false v1 (typeof a1) →
    581       eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr
    582   | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     629      cast_bool_to_target ty (Some ? Vfalse) = Some ? vres →           
     630      eval_expr ge e m (Expr (Eandbool a1 a2) ty) vres tr
     631  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2,vres.
    583632      eval_expr ge e m a1 v1 tr1 →
    584633      is_true v1 (typeof a1) →
    585634      eval_expr ge e m a2 v2 tr2 →
    586635      bool_of_val v2 (typeof a2) v →
    587       eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2)
     636      cast_bool_to_target ty (Some ? v) = Some ? vres →                 
     637      eval_expr ge e m (Expr (Eandbool a1 a2) ty) vres (tr1⧺tr2)
    588638  | eval_Ecast:   ∀a,ty,ty',v1,v,tr.
    589639      eval_expr ge e m a v1 tr →
     
    616666      eval_lvalue ge e m a l ofs tr →
    617667      typeof a = Tstruct id fList →
    618       field_offset i fList = OK ? delta →
    619       eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr
     668      field_offset i fList = OK ? delta → 
     669      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I16 delta)) tr
    620670 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
    621671      eval_lvalue ge e m a l ofs tr →
     
    634684  (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3))
    635685  (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3))
    636   (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2))
    637   (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
    638   (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2))
    639   (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
     686  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     687  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5))
     688  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     689  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5))
    640690  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    641691  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
     
    651701  | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    652702  | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3)
    653   | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
    654   | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    655   | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
    656   | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     703  | eval_Eorbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ eo1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
     704  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     705  | eval_Eandbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ ea1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
     706  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    657707  | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
    658708  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
     
    730780] qed.
    731781*)
     782
    732783let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    733784  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
     
    741792  (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3))
    742793  (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3))
    743   (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2))
    744   (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
    745   (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2))
    746   (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
     794  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     795  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5))
     796  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     797  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5))
    747798  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    748799  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
     
    763814  | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    764815  | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3)
    765   | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
    766   | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    767   | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
    768   | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     816  | eval_Eorbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ eo1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
     817  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     818  | eval_Eandbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ ea1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
     819  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    769820  | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
    770821  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H)
     
    781832  (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3))
    782833  (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3))
    783   (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2))
    784   (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
    785   (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2))
    786   (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
     834  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     835  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5))
     836  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     837  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5))
    787838  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    788839  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
  • src/Clight/SimplifyCasts.ma

    r2468 r2588  
    608608λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].
    609609
    610 (* Inversion principle for integer addition *)
    611 lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
     610(* Inversion principle for integer addition - wrapper around lemma in frontend_misc *)
     611lemma iadd_inv : ∀sz,sg,v1,v2,m,target_ty,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = Some ? r →
    612612                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)).
    613 #sz #sg #v1 #v2 #m #r
    614 elim v1
    615 [ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    616 whd in ⊢ ((??%?) → ?); normalize nodelta
    617 >classify_add_int normalize nodelta #H destruct
    618 elim v2 in H;
    619 [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    620 whd in ⊢ ((??%?) → ?); #H destruct
    621 elim (sz_eq_dec sz' sz'')
    622 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
    623 | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
    624 ] qed.
     613#sz #sg #v1 #v2 #m #ty #r whd @sem_add_ii_inversion qed.
    625614
    626615(* Inversion principle for integer subtraction. *)
    627 lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
    628                                     ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
    629 #sz #sg #v1 #v2 #m #r
    630 elim v1
    631 [ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    632 whd in ⊢ ((??%?) → ?); normalize nodelta
    633 >classify_sub_int normalize nodelta #H destruct
    634 elim v2 in H;
    635 [ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    636 whd in ⊢ ((??%?) → ?); #H destruct
    637 elim (sz_eq_dec sz' sz'')
    638 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
    639 | 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
    640 ] qed.
     616lemma isub_inv : ∀sz,sg,v1,v2,m,target_ty,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = Some ? r →
     617                                      ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
     618#sz #sg #v1 #v2 #m #ty #r whd @sem_sub_ii_inversion qed.
    641619
    642620definition is_int : val → Prop ≝
     
    647625
    648626(* "negative" (in the sense of ¬ Some) inversion principle for integer addition *)
    649 lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
     627lemma neg_iadd_inv : ∀sz,sg,v1,v2,m,target_ty. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ? →
    650628                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
    651629                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
    652 #sz #sg #v1 #v2 #m
     630#sz #sg #v1 #v2 #m #ty
    653631elim v1
    654632[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
     
    666644
    667645(* "negative" inversion principle for integer subtraction *)
    668 lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
     646lemma neg_isub_inv : ∀sz,sg,v1,v2,m,target_ty. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ? →
    669647                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
    670648                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
    671 #sz #sg #v1 #v2 #m
     649#sz #sg #v1 #v2 #m #target_ty
    672650elim v1
    673651[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
     
    684662] qed.
    685663
    686 lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m.
    687    ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
    688 #op #sz #sg #v1 #v2 #m #H
     664lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m,target_ty.
     665   ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ?.
     666#op #sz #sg #v1 #v2 #m #target_ty #H
    689667elim op normalize in match (binop_simplifiable ?); #H destruct
    690668elim v1 in H;
    691669[ 1,5: | 2,6: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,7: | 4,8: #ptr ]
    692670#_
    693 whd in match (sem_binary_operation ??????); normalize nodelta
     671whd in match (sem_binary_operation ???????); normalize nodelta
    694672>classify_add_int normalize nodelta //
    695673>classify_sub_int normalize nodelta //
     
    11141092                     cases op in Hop_simplifiable_eq;                 
    11151093                     [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_
    1116                      [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
    1117                      | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
    1118                      cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m)
     1094                     [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m (Tint src_sz src_sg))
     1095                     | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m (Tint src_sz src_sg)) ]
     1096                     cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m (Tint src_sz src_sg))
    11191097                     [ 1,3: #_ #_ #_ normalize @I ]
    11201098                     #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result)))
     
    11341112                     * #val_rhs1 #trace_rhs1
    11351113                     whd in match (m_bind ?????); normalize nodelta
    1136                      [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
    1137                           lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
    1138                      | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m)
    1139                           lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ]
    1140                      cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m)
     1114                     [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg))
     1115                          lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg))
     1116                     | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg))
     1117                          lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg)) ]
     1118                     cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg)
     1119                                                   val_rhs1 (Tint target_sz target_sg) m (Tint target_sz target_sg))
    11411120                     [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?)))
    11421121                            (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *)
     
    12701249                        [ 2,4: * #Heq >Heq #_ elim target_sz //
    12711250                        | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
    1272  ] ] ] ] ] 
     1251 ] ] ] ] ]
    12731252| 23,25: destruct
    12741253      inversion (Hcast2 ge en m)
     
    14611440                     normalize nodelta >Htype_eq_lhs
    14621441                     cases (exec_bool_of_val lhs_val (typeof lhs1))
    1463                        [ 2,4: #error normalize @SimFailNicely
     1442                     [ 2,4: #error normalize @SimFailNicely
    14641443                     | 1,3: *
    14651444                         whd in match (m_bind ?????);
  • src/Clight/frontend_misc.ma

    r2582 r2588  
    666666qed.
    667667
     668lemma zero_ext_same_size : ∀n,v. zero_ext n n v = v.
     669#n #v whd in match (zero_ext ???); >nat_compare_eq @refl
     670qed.
     671
    668672axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2.
    669673
    670674axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2.
     675
     676(* notice that we restrict source and target sizes to be ≠ 0 *)
     677axiom zero_ext_one : ∀sz1,sz2. zero_ext (bitsize_of_intsize sz1) (bitsize_of_intsize sz2) (repr sz1 1) = (repr sz2 1).
    671678
    672679axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?).
     
    24352442qed.
    24362443
     2444(* --------------------------------------------------------------------------- *)
     2445(* Inversion principles for binary operations *)
     2446(* --------------------------------------------------------------------------- *)
     2447
     2448lemma sem_add_ip_inversion :
     2449  ∀sz,sg,ty',optlen.
     2450  ∀v1,v2,res.
     2451  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
     2452  ∃sz',i. v1 = Vint sz' i ∧
     2453      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
     2454       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     2455#tsz #tsg #ty' * [ | #n ]
     2456*
     2457[ | #sz' #i' | | #p'
     2458| | #sz' #i' | | #p' ]
     2459#v2 #res
     2460whd in ⊢ ((??%?) → ?);
     2461#H destruct
     2462cases v2 in H;
     2463[ | #sz2' #i2' | | #p2'
     2464| | #sz2' #i2' | | #p2' ] normalize nodelta
     2465#H destruct
     2466[ 1,3:
     2467  lapply H -H
     2468  @(eq_bv_elim … i' (zero ?)) normalize nodelta
     2469  #Hi #Heq destruct (Heq)
     2470  %{sz'} %{(zero ?)} @conj destruct try @refl
     2471  %2 @conj try @conj try @refl
     2472| *: %{sz'} %{i'} @conj try @refl
     2473  %1 %{p2'} @conj try @refl
     2474] qed.
     2475
     2476(* symmetric of the upper one *)
     2477lemma sem_add_pi_inversion :
     2478  ∀sz,sg,ty',optlen.
     2479  ∀v1,v2,res.
     2480  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
     2481  ∃sz',i. v2 = Vint sz' i ∧
     2482      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
     2483       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     2484#tsz #tsg #ty' * [ | #n ]
     2485*
     2486[ | #sz' #i' | | #p'
     2487| | #sz' #i' | | #p' ]
     2488#v2 #res
     2489whd in ⊢ ((??%?) → ?);
     2490#H destruct
     2491cases v2 in H; normalize nodelta
     2492[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
     2493#H destruct
     2494[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
     2495  %{p'} @conj try @refl
     2496| *: lapply H -H
     2497  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
     2498  #Hi #Heq destruct (Heq)
     2499  %{sz2'} %{(zero ?)} @conj destruct try @refl
     2500  %2 @conj try @conj try @refl
     2501] qed.
     2502
     2503(* Know that addition on integers gives an integer. Notice that there is no correlation
     2504   between the size in the types and the size of the integer values. *)
     2505lemma sem_add_ii_inversion :
     2506  ∀sz,sg.
     2507  ∀v1,v2,res.
     2508  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     2509  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2510              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
     2511#sz #sg
     2512*
     2513[ | #sz' #i' | | #p' ]
     2514#v2 #res
     2515whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
     2516cases sz cases sg normalize nodelta
     2517#H destruct
     2518cases v2 in H; normalize nodelta
     2519#H1 destruct
     2520#H2 destruct #Heq %{sz'} lapply Heq -Heq
     2521cases sz' in i'; #i' 
     2522whd in match (intsize_eq_elim ???????);
     2523cases H1 in H2; #j' normalize nodelta
     2524#Heq destruct (Heq)
     2525%{i'} %{j'} @conj try @conj try @conj try @refl
     2526qed.
     2527
     2528lemma sem_sub_pp_inversion :
     2529  ∀ty1,ty2,n1,n2,target.
     2530  ∀v1,v2,res.
     2531  sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) target = Some ? res →
     2532  ∃sz,sg.
     2533    target = Tint sz sg ∧
     2534    ((∃p1,p2,i. v1 =  Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧
     2535             division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧
     2536             res = Vint sz (zero_ext ?? i)) ∨
     2537     (v1 =  Vnull ∧ v2 = Vnull ∧ res = Vint sz (zero ?))).
     2538#ty1 #ty2 #n1 #n2 #target
     2539cut (classify_sub (ptr_type ty1 n1) (ptr_type ty2 n2) =
     2540     sub_case_pp n1 n2 ty1 ty2)
     2541[ cases n1 cases n2     
     2542  [ | #n1 | #n2 | #n2 #n1 ] try @refl ]
     2543#Hclassify
     2544*
     2545[ | #sz #i | | #p ]
     2546#v2 #res
     2547whd in ⊢ ((??%?) → ?); normalize nodelta
     2548#H1 destruct
     2549lapply H1 -H1
     2550>Hclassify normalize nodelta
     2551[ 1,2: #H destruct ]
     2552cases v2 normalize nodelta
     2553[ | #sz' #i' | | #p'
     2554| | #sz' #i' | | #p' ]
     2555#H2 destruct
     2556cases target in H2;
     2557[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
     2558| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
     2559normalize nodelta
     2560#H destruct
     2561[ 2,4,5,6,7,8,9:
     2562  cases (eq_block (pblock p) (pblock p')) in H;
     2563  normalize nodelta #H destruct
     2564  cases (eqb (sizeof ty1) O) in H;
     2565  normalize nodelta #H destruct ]
     2566%{sz} %{sg} @conj try @refl
     2567try /4 by or_introl, or_intror, conj, refl/
     2568cases (if_opt_inversion ???? H)
     2569#Hblocks_eq -H
     2570@(eqb_elim … (sizeof ty1) 0) normalize nodelta
     2571[ #Heq_sizeof #Habsurd destruct ]
     2572#_ #Hdiv
     2573%1 %{p} %{p'}
     2574cases (division_u ???) in Hdiv; normalize nodelta
     2575[ #Habsurd destruct ] #i #Heq destruct
     2576%{i} try @conj try @conj try @conj try @conj try @refl
     2577try @(eq_block_to_refl … Hblocks_eq)
     2578qed.
     2579
     2580lemma sem_sub_pi_inversion :
     2581  ∀sz,sg,ty',optlen,target.
     2582  ∀v1,v2,res.
     2583  sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) target = Some ? res →
     2584  ∃sz',i. v2 = Vint sz' i ∧
     2585      ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨
     2586       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     2587#tsz #tsg #ty' * [ | #n ] #target
     2588*
     2589[ | #sz' #i' | | #p'
     2590| | #sz' #i' | | #p' ]
     2591#v2 #res
     2592whd in ⊢ ((??%?) → ?);
     2593#H destruct
     2594cases v2 in H; normalize nodelta
     2595[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
     2596#H destruct
     2597[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
     2598  %{p'} @conj try @refl
     2599| *: lapply H -H
     2600  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
     2601  #Hi #Heq destruct (Heq)
     2602  %{sz2'} %{(zero ?)} @conj destruct try @refl
     2603  %2 @conj try @conj try @refl
     2604] qed.
     2605
     2606lemma sem_sub_ii_inversion :
     2607  ∀sz,sg,ty.
     2608  ∀v1,v2,res.
     2609  sem_sub v1 (Tint sz sg) v2 (Tint sz sg) ty = Some ? res →
     2610  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2611              res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2).
     2612#sz #sg #ty *             
     2613[ | #sz' #i' | | #p' ]
     2614#v2 #res
     2615whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
     2616cases sz cases sg normalize nodelta
     2617#H destruct
     2618cases v2 in H; normalize nodelta
     2619#H1 destruct
     2620#H2 destruct #Heq %{sz'} lapply Heq -Heq
     2621cases sz' in i'; #i' 
     2622whd in match (intsize_eq_elim ???????);
     2623cases H1 in H2; #j' normalize nodelta
     2624#Heq destruct (Heq)
     2625%{i'} %{j'} @conj try @conj try @conj try @refl
     2626qed.
     2627
     2628
     2629lemma sem_mul_inversion :
     2630  ∀sz,sg.
     2631  ∀v1,v2,res.
     2632  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     2633  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2634              res = Vint sz' (short_multiplication ? i1 i2).
     2635#sz #sg *
     2636[ | #sz' #i' | | #p' ]
     2637#v2 #res
     2638whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2639cases sz cases sg normalize nodelta
     2640#H destruct
     2641cases v2 in H; normalize nodelta
     2642#H1 destruct
     2643#H2 destruct #Heq %{sz'} lapply Heq -Heq
     2644cases sz' in i'; #i' 
     2645whd in match (intsize_eq_elim ???????);
     2646cases H1 in H2; #j' normalize nodelta
     2647#Heq destruct (Heq)
     2648%{i'} %{j'} @conj try @conj try @conj try @refl
     2649qed.
     2650
     2651
     2652lemma sem_div_inversion_s :
     2653  ∀sz.
     2654  ∀v1,v2,res.
     2655  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
     2656  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2657              match division_s ? i1 i2 with
     2658              [ Some q ⇒  res =  (Vint sz' q)
     2659              | None ⇒ False ].
     2660#sz *
     2661[ | #sz' #i' | | #p' ]
     2662#v2 #res
     2663whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2664>type_eq_dec_true normalize nodelta
     2665#H destruct
     2666cases v2 in H; normalize nodelta
     2667[ | #sz2' #i2' | | #p2' ]
     2668#Heq destruct
     2669%{sz'}
     2670lapply Heq -Heq
     2671cases sz' in i'; #i' 
     2672whd in match (intsize_eq_elim ???????);
     2673cases sz2' in i2'; #i2' normalize nodelta
     2674whd in match (option_map ????); #Hdiv destruct
     2675%{i'} %{i2'} @conj try @conj try @conj try @refl
     2676cases (division_s ???) in Hdiv;
     2677[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2678qed.
     2679
     2680lemma sem_div_inversion_u :
     2681  ∀sz.
     2682  ∀v1,v2,res.
     2683  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
     2684  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2685              match division_u ? i1 i2 with
     2686              [ Some q ⇒  res =  (Vint sz' q)
     2687              | None ⇒ False ].
     2688#sz *
     2689[ | #sz' #i' | | #p' ]
     2690#v2 #res
     2691whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2692>type_eq_dec_true normalize nodelta
     2693#H destruct
     2694cases v2 in H; normalize nodelta
     2695[ | #sz2' #i2' | | #p2' ]
     2696#Heq destruct
     2697%{sz'}
     2698lapply Heq -Heq
     2699cases sz' in i'; #i' 
     2700whd in match (intsize_eq_elim ???????);
     2701cases sz2' in i2'; #i2' normalize nodelta
     2702whd in match (option_map ????); #Hdiv destruct
     2703%{i'} %{i2'} @conj try @conj try @conj try @refl
     2704cases (division_u ???) in Hdiv;
     2705[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2706qed.
     2707
     2708lemma sem_mod_inversion_s :
     2709  ∀sz.
     2710  ∀v1,v2,res.
     2711  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
     2712  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2713              match modulus_s ? i1 i2 with
     2714              [ Some q ⇒  res =  (Vint sz' q)
     2715              | None ⇒ False ].
     2716#sz *
     2717[ | #sz' #i' | | #p' ]
     2718#v2 #res
     2719whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2720>type_eq_dec_true normalize nodelta
     2721#H destruct
     2722cases v2 in H; normalize nodelta
     2723[ | #sz2' #i2' | | #p2' ]
     2724#Heq destruct
     2725%{sz'}
     2726lapply Heq -Heq
     2727cases sz' in i'; #i' 
     2728whd in match (intsize_eq_elim ???????);
     2729cases sz2' in i2'; #i2' normalize nodelta
     2730whd in match (option_map ????); #Hdiv destruct
     2731%{i'} %{i2'} @conj try @conj try @conj try @refl
     2732cases (modulus_s ???) in Hdiv;
     2733[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2734qed.
     2735
     2736lemma sem_mod_inversion_u :
     2737  ∀sz.
     2738  ∀v1,v2,res.
     2739  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
     2740  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2741              match modulus_u ? i1 i2 with
     2742              [ Some q ⇒  res =  (Vint sz' q)
     2743              | None ⇒ False ].
     2744#sz *
     2745[ | #sz' #i' | | #p' ]
     2746#v2 #res
     2747whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2748>type_eq_dec_true normalize nodelta
     2749#H destruct
     2750cases v2 in H; normalize nodelta
     2751[ | #sz2' #i2' | | #p2' ]
     2752#Heq destruct
     2753%{sz'}
     2754lapply Heq -Heq
     2755cases sz' in i'; #i' 
     2756whd in match (intsize_eq_elim ???????);
     2757cases sz2' in i2'; #i2' normalize nodelta
     2758whd in match (option_map ????); #Hdiv destruct
     2759%{i'} %{i2'} @conj try @conj try @conj try @refl
     2760cases (modulus_u ???) in Hdiv;
     2761[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2762qed.
     2763
     2764lemma sem_and_inversion :
     2765  ∀v1,v2,res.
     2766  sem_and v1 v2 = Some ? res →
     2767  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2768              res = Vint sz' (conjunction_bv ? i1 i2).
     2769*
     2770[ | #sz' #i' | | #p' ]
     2771#v2 #res
     2772whd in ⊢ ((??%?) → ?);
     2773#H destruct
     2774cases v2 in H; normalize nodelta
     2775[ | #sz2' #i2' | | #p2' ]
     2776#Heq destruct
     2777%{sz'}
     2778lapply Heq -Heq
     2779cases sz' in i'; #i' 
     2780whd in match (intsize_eq_elim ???????);
     2781cases sz2' in i2'; #i2' normalize nodelta
     2782#H destruct
     2783%{i'} %{i2'} @conj try @conj try @conj try @refl
     2784qed.
     2785
     2786lemma sem_or_inversion :
     2787  ∀v1,v2,res.
     2788  sem_or v1 v2 = Some ? res →
     2789  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2790              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
     2791*
     2792[ | #sz' #i' | | #p' ]
     2793#v2 #res
     2794whd in ⊢ ((??%?) → ?);
     2795#H destruct
     2796cases v2 in H; normalize nodelta
     2797[ | #sz2' #i2' | | #p2' ]
     2798#Heq destruct
     2799%{sz'}
     2800lapply Heq -Heq
     2801cases sz' in i'; #i' 
     2802whd in match (intsize_eq_elim ???????);
     2803cases sz2' in i2'; #i2' normalize nodelta
     2804#H destruct
     2805%{i'} %{i2'} @conj try @conj try @conj try @refl
     2806qed.
     2807
     2808lemma sem_xor_inversion :
     2809  ∀v1,v2,res.
     2810  sem_xor v1 v2 = Some ? res →
     2811  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2812              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
     2813*
     2814[ | #sz' #i' | | #p' ]
     2815#v2 #res
     2816whd in ⊢ ((??%?) → ?);
     2817#H destruct
     2818cases v2 in H; normalize nodelta
     2819[ | #sz2' #i2' | | #p2' ]
     2820#Heq destruct
     2821%{sz'}
     2822lapply Heq -Heq
     2823cases sz' in i'; #i' 
     2824whd in match (intsize_eq_elim ???????);
     2825cases sz2' in i2'; #i2' normalize nodelta
     2826#H destruct
     2827%{i'} %{i2'} @conj try @conj try @conj try @refl
     2828qed.
     2829
     2830lemma sem_shl_inversion :
     2831  ∀v1,v2,res.
     2832  sem_shl v1 v2 = Some ? res →
     2833  ∃sz1,sz2,i1,i2.
     2834              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
     2835              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
     2836                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
     2837              lt_u (bitsize_of_intsize sz2) i2
     2838                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
     2839*
     2840[ | #sz' #i' | | #p' ]
     2841#v2 #res
     2842whd in ⊢ ((??%?) → ?);
     2843#H destruct
     2844cases v2 in H; normalize nodelta
     2845[ | #sz2' #i2' | | #p2' ]
     2846#Heq destruct
     2847%{sz'} %{sz2'}
     2848lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
     2849%{i'} %{i2'}
     2850>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
     2851qed.
     2852
     2853lemma sem_shr_inversion :
     2854  ∀v1,v2,sz,sg,res.
     2855  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     2856  ∃sz1,sz2,i1,i2.
     2857              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
     2858              lt_u (bitsize_of_intsize sz2) i2
     2859                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
     2860              match sg with
     2861              [ Signed ⇒
     2862                 res =
     2863                   (Vint sz1
     2864                    (shift_right bool (7+pred_size_intsize sz1*8)
     2865                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
     2866                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
     2867              | Unsigned ⇒
     2868                 res =
     2869                   (Vint sz1
     2870                    (shift_right bool (7+pred_size_intsize sz1*8)
     2871                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
     2872              ].
     2873*
     2874[ | #sz' #i' | | #p' ]
     2875#v2 #sz * #res
     2876whd in ⊢ ((??%?) → ?);
     2877whd in match (classify_aop ??);
     2878>type_eq_dec_true normalize nodelta
     2879#H destruct
     2880cases v2 in H; normalize nodelta
     2881[ | #sz2' #i2' | | #p2'
     2882| | #sz2' #i2' | | #p2' ]
     2883#Heq destruct
     2884%{sz'} %{sz2'}
     2885lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
     2886%{i'} %{i2'}
     2887>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
     2888qed.
     2889
     2890
     2891
     2892lemma sem_cmp_int_inversion :
     2893  ∀v1,v2,sz,sg,op,m,res.
     2894   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
     2895   ∃sz,i1,i2. v1 = Vint sz i1 ∧
     2896              v2 = Vint sz i2 ∧
     2897    match sg with
     2898    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
     2899    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
     2900    ].
     2901#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
     2902whd in ⊢ ((??%?) → ?);
     2903whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
     2904cases v1
     2905[ | #sz #i | | #p ] normalize nodelta
     2906#H destruct
     2907cases v2 in H;
     2908[ | #sz' #i' | | #p' ] normalize nodelta
     2909#H destruct lapply H -H
     2910cases sz in i; #i
     2911cases sz' in i'; #i' cases sg normalize nodelta
     2912whd in match (intsize_eq_elim ???????); #H destruct
     2913[ 1,2: %{I8}
     2914| 3,4: %{I16}
     2915| 5,6: %{I32} ] 
     2916%{i} %{i'} @conj try @conj try @refl
     2917qed.
     2918
     2919
     2920lemma sem_cmp_ptr_inversion :
     2921  ∀v1,v2,ty',n,op,m,res.
     2922   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
     2923   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
     2924                 valid_pointer m p1 = true ∧
     2925                 valid_pointer m p2 = true ∧
     2926                 (if eq_block (pblock p1) (pblock p2)
     2927                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
     2928                  else sem_cmp_mismatch op) = Some ? res) ∨
     2929   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
     2930   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
     2931   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
     2932* [ | #sz #i | | #p ] normalize nodelta
     2933#v2 #ty' #n #op
     2934* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
     2935whd in match (classify_cmp ??); cases n normalize nodelta
     2936[ 2,4,6,8: #array_len ]
     2937whd in match (ptr_type ty' ?);
     2938whd in match (if_type_eq ?????);
     2939>type_eq_dec_true normalize nodelta
     2940#H destruct
     2941cases v2 in H; normalize nodelta
     2942[ | #sz' #i' | | #p'
     2943| | #sz' #i' | | #p'
     2944| | #sz' #i' | | #p'
     2945| | #sz' #i' | | #p' ]
     2946#H destruct
     2947try /6 by or_introl, or_intror, ex_intro, conj/
     2948[ 1: %1 %1 %2 %{p} @conj try @conj //
     2949| 3: %1 %1 %2 %{p} @conj try @conj //
     2950| *: %1 %1 %1 %{p} %{p'}
     2951     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
     2952     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
     2953     try @conj try @conj try @conj try @conj try @conj try @refl try @H
     2954     destruct
     2955] qed.
  • src/Clight/label.ma

    r2505 r2588  
    7979  〈Expr (Ecost l e) (typeof e), gen〉.
    8080
    81 definition const_int : nat → expr ≝
    82 λn. Expr (Econst_int ? (repr I32 n)) (Tint I32 Signed).
     81definition const_int : intsize → nat → expr ≝
     82λsz,n. Expr (Econst_int ? (repr sz n)) (Tint sz Signed).
    8383
    8484let rec label_expr (e:expr) (costgen:universe CostTag)
     
    119119| Eandbool e1 e2 ⇒
    120120    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     121    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     122    match ty with
     123    [ Tint sz sg ⇒
     124      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
     125      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
     126      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     127      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
     128      〈Econdition e1 e2 ef, costgen〉
     129    | _ ⇒ (* default on 32 bit consts if inconsistent type. *)
     130      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
     131      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
     132      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     133      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
     134      〈Econdition e1 e2 ef, costgen〉       
     135    ]
     136| Eorbool e1 e2 ⇒
     137    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    121138    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    122     let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    123     let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    124     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
    125     let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    126     〈Econdition e1 e2 ef, costgen〉
    127 | Eorbool e1 e2 ⇒
    128     let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    129     let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    130     let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    131     let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    132     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
    133     let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    134     〈Econdition e1 et e2, costgen〉
    135 
     139    match ty with
     140    [ Tint sz sg ⇒   
     141      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
     142      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
     143      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     144      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
     145      〈Econdition e1 et e2, costgen〉
     146    | _ ⇒
     147      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
     148      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
     149      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     150      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
     151      〈Econdition e1 et e2, costgen〉
     152    ]
    136153| Efield e' id ⇒
    137154    let 〈e',costgen〉 ≝ label_expr e' costgen in
  • src/Clight/labelSimulation.ma

    r2574 r2588  
    22include "Clight/labelSpecification.ma".
    33include "Clight/CexecInd.ma".
     4include "Clight/frontend_misc.ma".
    45
    56(* Useful for breaking up the labeling functions, because we don't care about
     
    4647  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
    4748#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
    48 qed. 
     49qed.
    4950
    5051
     
    162163  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    163164  @label_gen_elim #u2
    164   @label_gen_elim #u3
    165   @add_cost_expr_elim #u4 #l4
    166   @add_cost_expr_elim #u5 #l5
    167   @add_cost_expr_elim #u6 #l6
    168   @add_cost_expr_elim #u7 #l7
     165  @label_gen_elim #u3 normalize nodelta in EX;
    169166  [ cases (bind_inversion ????? EX) -EX * #v2 #tr2 * #EX2 #EX
    170167    cases (bind_inversion ????? EX) -EX * * #EX3 #EX
     168    (* >>> *)
     169    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     170    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     171    #Heq destruct normalize nodelta
     172    @add_cost_expr_elim #u4 #l4
     173    @add_cost_expr_elim #u5 #l5
     174    @add_cost_expr_elim #u6 #l6
     175    @add_cost_expr_elim #u7 #l7
     176    (* <<< *)
    171177    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    172178    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
     
    177183    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    178184    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    179     whd in EX:(??%%) ⊢ %; destruct % [ 1,3: normalize @refl | *: @twel_app // @twel_new whd in ⊢ (??%); <(E0_right tr2) @twel_app /2/ ]
     185    whd in EX:(??%%) ⊢ %; destruct %
     186    [ 1,3: normalize nodelta
     187           whd in match (m_bind ?????);
     188           whd in match (exec_expr ????);
     189           whd in match (exec_expr ????);
     190           >eq_intsize_true normalize nodelta
     191           [ >zero_ext_one | >zero_ext_zero ]
     192           @refl           
     193    | *: @twel_app // @twel_new whd in ⊢ (??%); <(E0_right tr2) @twel_app /2/ ]
    180194  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     195    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     196    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     197    #Heq destruct normalize nodelta
     198    @add_cost_expr_elim #u4 #l4
     199    @add_cost_expr_elim #u5 #l5
     200    @add_cost_expr_elim #u6 #l6
     201    @add_cost_expr_elim #u7 #l7
    181202    %{(tr1'⧺E0⧺Echarge l7)}
    182203    whd in ⊢ (?(??%?)?); >EX1'
    183204    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    184     whd in EX:(??%%); destruct % normalize // <(E0_right tr) @twel_app /2/
     205    whd in EX:(??%%); destruct % normalize nodelta
     206    whd in match (m_bind ?????);
     207    whd in match (exec_expr ????);
     208    whd in match (exec_expr ????);
     209    [ >eq_intsize_true ] normalize nodelta
     210    [ >zero_ext_zero @refl ]   
     211    <(E0_right tr) @twel_app /2/
    185212  ]
    186213| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
     
    190217  @label_gen_elim #u2
    191218  @label_gen_elim #u3
    192   @add_cost_expr_elim #u4 #l4
    193   @add_cost_expr_elim #u5 #l5
    194   @add_cost_expr_elim #u6 #l6
    195   @add_cost_expr_elim #u7 #l7
     219  normalize nodelta in EX;
    196220  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     221    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     222    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     223    #Heq destruct normalize nodelta 
     224    @add_cost_expr_elim #u4 #l4
     225    @add_cost_expr_elim #u5 #l5
     226    @add_cost_expr_elim #u6 #l6
     227    @add_cost_expr_elim #u7 #l7
    197228    %{(tr1'⧺Echarge l7)}
    198229    whd in ⊢ (?(??%?)?); >EX1'
    199     whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    200     whd in EX:(??%%) ⊢ %; destruct normalize % // <(E0_right tr) /3/
     230    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard normalize nodelta
     231    whd in match (m_bind ?????);
     232    whd in match (exec_expr ????);
     233    whd in match (exec_expr ????);
     234    >eq_intsize_true normalize nodelta
     235    % // <(E0_right tr) /3/
    201236  | cases (bind_inversion ????? EX) -EX * #v2 #tr2 * #EX2 #EX
    202237    cases (bind_inversion ????? EX) -EX * * #EX3 #EX
    203238    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    204239    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
     240    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     241    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     242    #Heq destruct normalize nodelta
     243    @add_cost_expr_elim #u4 #l4
     244    @add_cost_expr_elim #u5 #l5
     245    @add_cost_expr_elim #u6 #l6
     246    @add_cost_expr_elim #u7 #l7   
    205247    [ %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l4)} | %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l5)} ]
    206248    whd in ⊢ (?(??%?)?); >EX1'
     
    209251    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    210252    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    211     whd in EX:(??%%) ⊢ %; destruct normalize % [1,3: % | *: @twel_app // @twel_new <(E0_right tr2) @twel_app /2/ ]
     253    normalize nodelta
     254    whd in match (m_bind ?????);
     255    whd in match (exec_expr ????);
     256    whd in match (exec_expr ????);
     257    >eq_intsize_true normalize nodelta   
     258    % [ 1,3: [ >zero_ext_one | >zero_ext_zero ] >E0_right @refl
     259      | *: @twel_app // @twel_new >nil_append <(E0_right tr2) @twel_app /2/ ]
    212260  ]
    213261| #ty #ty' #v #tr normalize /3/
  • src/Clight/memoryInjections.ma

    r2578 r2588  
    464464qed.
    465465
     466lemma value_eq_int_inversion' :
     467  ∀E,sz,i,v. value_eq E v (Vint sz i) → v = (Vint sz i).
     468#E #sz #i #v #Heq inversion Heq
     469[ 1: #_ #Habsurd destruct (Habsurd)
     470| 2: #sz #i #Heq #Heq' #_ @refl
     471| 3: #_ #Habsurd destruct (Habsurd)
     472| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
     473qed.
     474
    466475lemma value_eq_null_inversion :
    467476  ∀E,v. value_eq E Vnull v → v = Vnull.
    468477#E #v #Heq inversion Heq //
    469478#p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd)
     479#Habsurd' destruct
     480qed.
     481
     482lemma value_eq_null_inversion' :
     483  ∀E,v. value_eq E v Vnull → v = Vnull.
     484#E #v #Heq inversion Heq //
     485#p1 #p2 #Htranslate #_ #Habsurd lapply (jmeq_to_eq ??? Habsurd)
    470486#Habsurd' destruct
    471487qed.
     
    17331749(* value_eq lifts to subtraction *)
    17341750lemma sub_value_eq :
    1735   ∀E,v1,v2,v1',v2',ty1,ty2.
     1751  ∀E,v1,v2,v1',v2',ty1,ty2,target.
    17361752   value_eq E v1 v2 →
    17371753   value_eq E v1' v2' →
    1738    ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
    1739            ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
    1740 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
     1754   ∀r1. (sem_sub v1 ty1 v1' ty2 target=Some val r1→
     1755           ∃r2:val.sem_sub v2 ty1 v2' ty2 target=Some val r2∧value_eq E r1 r2).
     1756#E #v1 #v2 #v1' #v2' #ty1 #ty2 #target #Hvalue_eq1 #Hvalue_eq2 #r1
    17411757@(value_eq_inversion E … Hvalue_eq1)
    17421758[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    1743 [ 1: whd in match (sem_sub ????); normalize nodelta
     1759[ 1: whd in match (sem_sub ?????); normalize nodelta
    17441760     cases (classify_sub ty1 ty2) normalize nodelta
    17451761     [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ]
    17461762     #Habsurd destruct (Habsurd)
    1747 | 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1763| 2: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
    17481764     cases (classify_sub ty1 ty2) normalize nodelta     
    17491765     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     
    17561772      | 2: #Heq destruct (Heq) normalize nodelta
    17571773           #Heq destruct (Heq)
    1758           /3 by ex_intro, conj, vint_eq/           
     1774          /3 by ex_intro, conj, vint_eq/
    17591775      ]
    17601776(*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     
    17671783     #Heq destruct (Heq)
    17681784     /3 by ex_intro, conj, vfloat_eq/ *)
    1769 | 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1785| 3: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
    17701786     cases (classify_sub ty1 ty2) normalize nodelta
    17711787     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     
    17761792     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
    17771793                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    1778      | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
    1779 | 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1794     | 2: cases target
     1795          [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1796          | #structname #fieldspec | #unionname #fieldspec | #id ]
     1797          normalize nodelta
     1798          #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
     1799| 4: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
    17801800     cases (classify_sub ty1 ty2) normalize nodelta
    17811801     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     
    18101830               cases (eqb (sizeof tsg) O) normalize nodelta
    18111831               [ 1: #Habsurd destruct (Habsurd)
    1812                | 2: >(sub_offset_translation 32 off1 off1' dest_off)
    1813                     cases (division_u 31
    1814                             (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
    1815                             (repr (sizeof tsg)))
     1832               | 2: cases target
     1833                    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1834                    | #structname #fieldspec | #unionname #fieldspec | #id ]
     1835                    normalize nodelta
     1836                    #Heq destruct (Heq)
     1837                    <(sub_offset_translation 32 off1 off1' dest_off)
     1838                    cases (division_u ?
     1839                            (sub_offset ? off1 off1')
     1840                            (repr (sizeof tsg))) in Heq;
    18161841                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
    1817                     | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
     1842                    | 2: #r1' cases sg normalize nodelta #Heq2 destruct (Heq2)
    18181843                         /3 by ex_intro, conj, vint_eq/ ]
    18191844    ] ] ]
    18201845] qed.
    1821 
    18221846
    18231847lemma mul_value_eq :
     
    20892113] qed.
    20902114
    2091 (* /!\ Warning TODO Warning /!\ *)
    2092 
    20932115(* Note that x and y are bounded below and above, similarly for the shifted offsets.
    20942116   This is enough to prove that there is no "wrap-around-the-end" problem,
    20952117   /provided we know that the block bounds are implementable by 2^16 bitvectors/.
    2096    We axiomatize it for now. Notice that this axiom is in fact not provable and implies False.
    2097    In order to be true, we need to prove that the (x+delta) and (y+delta) do not overflow.
    2098    This is provable from the fact that the original pointers in which the offsets reside are "valid".
    2099    This in turn is ensured by the memory injection.
    2100    /DO NOT USE IT ELSEWHERE, this is just a temporary stopgap./ *)
     2118   We axiomatize it for now. *)
    21012119axiom cmp_offset_translation :
    21022120  ∀op,delta,x,y.
  • src/Clight/switchRemoval.ma

    r2510 r2588  
    21242124(* Conservation of the semantics of binary operators under memory extensions.
    21252125   Tried to factorise it a bit but the play with indexes just becomes too messy.  *)
    2126 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable.
     2126lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,target_type,writeable.
    21272127  ∀Hext:sr_memext m1 m2 writeable. ∀res.
    2128   sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res →
    2129   sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res.
    2130 #op #v1 #v2 #e1 #e2 #m1 #m2 #writeable #Hmemext #res cases op
    2131 whd in match (sem_binary_operation ??????);
     2128  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 target_type = Some ? res →
     2129  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 target_type = Some ? res.
     2130#op #v1 #v2 #e1 #e2 #m1 #m2 #target_type #writeable #Hmemext #res cases op
     2131whd in match (sem_binary_operation ???????);
    21322132try //
    2133 whd in match (sem_binary_operation ??????);
     2133whd in match (sem_binary_operation ???????);
    21342134lapply (me_valid_pointers … Hmemext)
    21352135lapply (me_not_writeable_ptr … Hmemext)
     
    22822282     >(Hsim2 ? (refl ??))
    22832283     whd in match (m_bind ?????);
    2284      lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 writeable Hext)
    2285      cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1)
     2284     lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 ty writeable Hext)
     2285     cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1 ty)
    22862286     [ 1: #_ // ] #val #H >(H val (refl ??))
    22872287     normalize destruct @conj @refl
     
    23192319     whd in match (m_bind ?????);
    23202320     whd in match (m_bind ?????);
    2321      [ 2,3: normalize @conj try @refl ]
     2321     [ 2,3: cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl ]
    23222322     cases (exec_expr ge en1 m1 e2) in Hsim2;
    23232323     [ 2,4: #error #_ normalize @I ]
     
    23262326     cases (exec_bool_of_val v2 (typeof e2))
    23272327     [ 2,4: #error normalize @I ]
    2328      * normalize @conj @refl
     2328     *
     2329     whd in match (m_bind ?????);
     2330     cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl
    23292331| 12: #ty #ty' cases ty
    23302332     [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
  • src/Clight/toCminor.ma

    r2582 r2588  
    259259λty1,ty2,P,p.
    260260  do E ← assert_type_eq ty1 ty2;
    261   OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 
     261  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
     262 
     263(* associated reasoning principle *)
     264lemma type_should_eq_inversion :
     265  ∀ty1,ty2,P,f,res.
     266    type_should_eq ty1 ty2 P f = OK ? res →
     267    ty1 = ty2 ∧ f ≃ res.
     268#ty1 #ty2 #P #f #res normalize
     269cases (type_eq_dec ty1 ty2) normalize nodelta
     270[ 2: #Hneq #Habsurd destruct ]
     271#Heq #Heq2 @conj try assumption
     272destruct (Heq2) cases Heq normalize nodelta
     273@eq_to_jmeq @refl
     274qed. 
    262275
    263276(* same gig for regions *)
     
    274287  ].
    275288destruct %
     289qed.
     290
     291(* associated reasoning principle *)
     292lemma typ_should_eq_inversion :
     293  ∀ty1,ty2,P,a,x.
     294    typ_should_eq ty1 ty2 P a = OK ? x →
     295    ty1 = ty2 ∧ a ≃ x.
     296* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
     297[ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
     298| 3: cases sz cases sg #P #A #x normalize #H destruct
     299| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
     300cases sz cases sz2 cases sg cases sg2
     301#P #a #x #H normalize in H:(??%?); destruct (H)
     302try @conj try @refl try @refl_jmeq
    276303qed.
    277304
     
    340367    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddip I16) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))) (fix_ptr_type … e2))
    341368| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    342 ].
    343 
     369].
     370
     371
     372(* XXX Clight pointer/int subtraction uses neg_shift_pointer_n, which boils down to (sub32 lhs (mul32 (const32 sizeof_ty) (sext32/zext32 rhs))),
     373 * whereas Cminor uses neg_shift_pointer, which translates into (sub32 lhs (sext32 rhs)). We have to translate the multiplication as actual
     374 * Cminor code, yielding something like (sub32 lhs (sext32 (mulXX (constXX sizeof_ty) (sextXX/zextXX rhs)))). In the original translate_sub,
     375 * XX=16, which we can't prove equivalent in general. Moreover, Osubpi expects a /signed/ integer argument, whereas Clight does not care and
     376 * casesplits on the sign to select either a zero extension or a sign extension.
     377 * λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     378      corresponding cl value: Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) sg n2))  =
     379      mk_offset (sub32 lhs (mult32 (const32 (sizeof ty)) (sext32/zext32 rhs)))
     380
     381      cminor
     382      mk_offset (sub32 lhs (sext32 ))
     383 *)
    344384definition translate_sub ≝
    345385λty1,ty2,ty'.
     
    350390(* XXX could optimise cast as above *)
    351391| sub_case_pi n ty sz sg ⇒
    352     λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     392    (* XXX This is so ugly. *)
     393    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I32) (fix_ptr_type … e1)
     394                                                    (Op1 ?? (Ocastint ?? I32 Signed) (Op2 ??? (Omul I16 sg) (Op1 ?? (Ocastint ??? sg) e2)
     395                                                                                     (Cst ? (Ointconst I16 sg (repr I16 (sizeof ty)))))))
    353396(* XXX check in detail? *)
    354397| sub_case_pp n1 n2 ty1 ty2 ⇒
    355398    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
    356399    [ Tint sz sg ⇒
    357       (* XXX we make the constant unsigned to match CL semantics. *)
     400      (* XXX we make the constant unsigned to match CL semantics. We also use 32 bits, still for CL semantics. Documented in Csem.ma@sem_sub *)
    358401      (* OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2)))))) *)
    359          OK ? (Op1 ?? (Ocastint I16 Unsigned sz sg) (Op2 ??? (Odivu I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Unsigned (repr ? (sizeof ty2))))))     
     402         OK ? (Op1 ?? (Ocastint I32 Unsigned sz sg) (Op2 ??? (Odivu I32) (Op2 ??? (Osubpp I32) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I32 Unsigned (repr ? (sizeof ty1))))))
    360403    | _ ⇒ Error ? (msg TypeMismatch)
    361404    ]
     
    599642]. whd normalize nodelta @pi2
    600643qed.
     644
     645definition cm_zero ≝ λsz,sg. Cst ? (Ointconst sz sg (zero ?)).
     646definition cm_one  ≝ λsz,sg. Cst ? (Ointconst sz sg (repr sz 1)).
    601647
    602648(* Translate Clight exprs into Cminor ones.
     
    740786          with
    741787          [ ASTint sz1 _ ⇒ λe1'.
    742             OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
     788            (* Producing a nested comparison to match CL. *)
     789            OK ? «Cond ??? e1' (Cond ??? e2' (cm_one sz sg) (cm_zero sz sg)) (cm_zero sz sg), ?»
    743790          | _ ⇒ λ_. Error ? (msg TypeMismatch)
    744791          ] e1'
    745792      | _ ⇒ Error ? (msg TypeMismatch)
    746793      ]
    747 (*  | Eandbool e1 e2 ⇒
    748       do e1' ← translate_expr vars e1;
    749       do e2' ← translate_expr vars e2;
    750       match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
    751       [ Tint sz sg ⇒
    752         match sz
    753         return λsz'. (sz = sz') → res (Σe':CMexpr (typ_of_type ?). ?)
    754         with
    755         [ I32 ⇒ λHsz_eq.
    756           do e2' ← type_should_eq ? (Tint I32 sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    757           match typ_of_type (typeof e1)
    758           return λx.
    759             (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?)
    760           with
    761           [ ASTint sz1 _ ⇒ λe1'.
    762             OK ? «Cond ??? e1' e2' (Cst ? (Ointconst I32 sg (zero ?))), ?»
    763           | _ ⇒ λ_. Error ? (msg TypeMismatch)
    764           ] e1'
    765         | _ ⇒ λ_. Error ? (msg TypeMismatch)
    766         ] (refl ? sz)
    767       | _ ⇒ Error ? (msg TypeMismatch)
    768       ]*)
    769794  | Eorbool e1 e2 ⇒
    770795      do e1' ← translate_expr vars e1;
     
    775800        match typ_of_type (typeof e1)
    776801        return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
    777         [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?»
     802        [ ASTint _ _ ⇒ λe1'.
     803          OK ? «Cond ??? e1' (cm_one sz sg) (Cond ??? e2' (cm_one sz sg) (cm_zero sz sg)), ?»
    778804        | _ ⇒ λ_. Error ? (msg TypeMismatch)
    779805        ] e1'
     
    858884| @(translate_binop_vars … E) @pi2
    859885| % [ % ] @pi2
    860 | % [ % @pi2 ] whd @I
    861 | % [ % [ @pi2 | @I ] | @pi2 ]
     886| % [ % try @pi2 whd @conj try @conj try // @pi2 ] whd @I
     887| % [ % [ @pi2 | @I ] | % try @conj try // @pi2 ]
    862888| % [ @pi2 | @I ]
    863889| % [ @pi2 | @I ]
  • src/Clight/toCminorCorrectness.ma

    r2582 r2588  
    11include "Clight/toCminor.ma".
     2include "Clight/toCminorOps.ma".
     3include "Clight/CexecInd.ma".
     4include "common/Globalenvs.ma".
     5include "Clight/memoryInjections.ma".
     6include "Clight/abstract.ma".
     7include "Cminor/abstract.ma".
     8
    29
    310(* When we characterise the local Clight variables, those that are stack
     
    248255] qed.
    249256
    250 include "Clight/Cexec.ma".
    251 include "Clight/abstract.ma".
    252 include "Cminor/abstract.ma".
    253 
    254257(* Invariants used in simulation *)
    255258
     
    264267      find_funct … ge_cm v = Some ? f'
    265268}.
    266 
    267 include "Clight/CexecInd.ma".
    268 include "Clight/frontend_misc.ma".
    269 include "Clight/memoryInjections.ma".
    270269
    271270(* Perhaps we will have to be more precise on what is allocated, etc.
     
    301300        | None ⇒ False ]
    302301    ].
    303              
    304 lemma type_should_eq_inversion :
    305   ∀ty1,ty2,P,f,res.
    306     type_should_eq ty1 ty2 P f = OK ? res →
    307     ty1 = ty2 ∧ f ≃ res.
    308 #ty1 #ty2 #P #f #res normalize
    309 cases (type_eq_dec ty1 ty2) normalize nodelta
    310 [ 2: #Hneq #Habsurd destruct ]
    311 #Heq #Heq2 @conj try assumption
    312 destruct (Heq2) cases Heq normalize nodelta
    313 @eq_to_jmeq @refl
    314 qed.
    315 
    316 lemma typ_should_eq_inversion :
    317   ∀ty1,ty2,P,a,x.
    318     typ_should_eq ty1 ty2 P a = OK ? x →
    319     ty1 = ty2 ∧ a ≃ x.
    320 * [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
    321 [ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
    322 | 3: cases sz cases sg #P #A #x normalize #H destruct
    323 | 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
    324 cases sz cases sz2 cases sg cases sg2
    325 #P #a #x #H normalize in H:(??%?); destruct (H)
    326 try @conj try @refl try @refl_jmeq
    327 qed.
    328302
    329303lemma load_value_of_type_by_ref :
     
    459433qed.
    460434
    461 
    462 lemma translate_notbool_to_cminor :
    463   ∀t,sg,arg.
    464   ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
    465   ∀res. sem_unary_operation Onotbool arg t = Some ? res →
    466         eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
    467 *
    468 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    469 | #structname #fieldspec | #unionname #fieldspec | #id ]
    470 normalize in match (typ_of_type ?);
    471 #sg #arg #cmop
    472 whd in ⊢ (??%% → ?); #Heq destruct (Heq)
    473 cases arg
    474 [ | #vsz #vi | | #vp
    475 | | #vsz #vi | | #vp
    476 | | #vsz #vi | | #vp
    477 | | #vsz #vi | | #vp
    478 | | #vsz #vi | | #vp
    479 | | #vsz #vi | | #vp
    480 | | #vsz #vi | | #vp
    481 | | #vsz #vi | | #vp ]
    482 #res
    483 whd in ⊢ ((??%?) → ?);
    484 #Heq
    485 [ 6,11,12: | *: destruct (Heq) ]
    486 [ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
    487 | 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
    488      #H normalize nodelta #Heq destruct
    489      whd in match (eval_unop ????);
    490      cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
    491 ] qed.
    492 
    493 lemma translate_notint_to_cminor :
    494   ∀t,t',arg.
    495   ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
    496   ∀res. sem_unary_operation Onotint arg t = Some ? res →
    497         eval_unop (typ_of_type t) t' cmop arg = Some ? res.
    498 #ty *
    499 [ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
    500 #sz #sg #arg #cmop
    501 whd in match (translate_unop ???);
    502 @(match typ_eq (ASTint sz sg) (typ_of_type ty)
    503   with
    504   [ inl H ⇒ ?
    505   | inr H ⇒ ? ])
    506 normalize nodelta
    507 [ 2: #Heq destruct ]
    508 lapply H -H
    509 lapply cmop -cmop
    510 cases ty
    511 [ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
    512 | #structname #fieldspec | #unionname #fieldspec | #id ]
    513 normalize nodelta
    514 #cmop normalize in match (typ_of_type ?); #H destruct
    515 #H' normalize in H';
    516 destruct (H')
    517 #res
    518 whd in match (sem_unary_operation ???);
    519 cases arg
    520 [ | #vsz #vi | | #vp
    521 | | #vsz #vi | | #vp
    522 | | #vsz #vi | | #vp
    523 | | #vsz #vi | | #vp ]
    524 whd in match (sem_notint ?);
    525 #H destruct (H) @refl
    526 qed.
    527 
    528 
    529 lemma translate_negint_to_cminor :
    530   ∀t,t',arg.
    531   ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
    532   ∀res. sem_unary_operation Oneg arg t = Some ? res →
    533         eval_unop (typ_of_type t) t' cmop arg = Some ? res.
    534 #ty *
    535 [ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
    536 #sz #sg #arg #cmop
    537 whd in match (translate_unop ???);
    538 @(match typ_eq (ASTint sz sg) (typ_of_type ty)
    539   with
    540   [ inl H ⇒ ?
    541   | inr H ⇒ ? ])
    542 normalize nodelta
    543 [ 2: #Heq destruct ]
    544 lapply H -H
    545 lapply cmop -cmop
    546 cases ty
    547 [ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
    548 | #structname #fieldspec | #unionname #fieldspec | #id ]
    549 normalize nodelta
    550 #cmop normalize in match (typ_of_type ?); #H destruct
    551 #H' normalize in H';
    552 destruct (H')
    553 #res
    554 whd in match (sem_unary_operation ???);
    555 cases arg
    556 [ | #vsz #vi | | #vp
    557 | | #vsz #vi | | #vp
    558 | | #vsz #vi | | #vp
    559 | | #vsz #vi | | #vp ]
    560 whd in match (sem_neg ??);
    561 #H destruct (H)
    562 whd in match (eval_unop ????);
    563 cases (eq_intsize sz' vsz) in H; normalize nodelta
    564 #H destruct @refl
    565 qed.
    566 
    567 
    568 lemma translate_unop :
    569   ∀ty,sg,op,cmop.
    570   translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
    571   ∀arg,res. sem_unary_operation op arg ty = Some ? res →
    572             eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
    573 #ty #sg * #cmop #Htranslate #arg
    574 [ @translate_notbool_to_cminor assumption
    575 | @translate_notint_to_cminor assumption
    576 | @translate_negint_to_cminor assumption ]
    577 qed.
    578 
    579 lemma classify_add_inversion :
    580   ∀ty1,ty2.
    581     (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
    582     (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
    583     (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
    584     (classify_add ty1 ty2 = add_default ty1 ty2).
    585 #ty1 #ty2
    586 cases (classify_add ty1 ty2)
    587 [ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
    588 | #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
    589 | #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
    590 | #tya #tyb %2 @refl ]
    591 qed.
    592 
    593 lemma classify_sub_inversion :
    594   ∀ty1,ty2.
    595     (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_ii sz sg) ∨
    596     (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_pi n ty' sz sg) ∨
    597     (∃ty1',ty2',n1,n2. ty1 = ptr_type ty1' n1 ∧ ty2 = ptr_type ty2' n2 ∧ classify_sub ty1 ty2 ≃ sub_case_pp n1 n2 ty1' ty2') ∨
    598     (classify_sub ty1 ty2 = sub_default ty1 ty2).
    599 #ty1 #ty2
    600 cases (classify_sub ty1 ty2)
    601 [ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
    602 | #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
    603 | #n1 #n2 #t1 #t2 %1 %2 %{t1} %{t2} %{n1} %{n2} @conj try @conj try @refl @refl_jmeq
    604 | #tya #tyb %2 @refl ]
    605 qed.
    606 
    607 lemma classify_aop_inversion :
    608   ∀ty1,ty2.
    609     (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
    610     classify_aop ty1 ty2 = aop_default ty1 ty2.
    611 #ty1 #ty2
    612 cases (classify_aop ty1 ty2)
    613 [ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
    614 | #ty #ty' %2 @refl ]
    615 qed.
    616 
    617 lemma sem_add_ip_inversion :
    618   ∀sz,sg,ty',optlen.
    619   ∀v1,v2,res.
    620   sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
    621   ∃sz',i. v1 = Vint sz' i ∧
    622       ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
    623        (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    624 #tsz #tsg #ty' * [ | #n ]
    625 *
    626 [ | #sz' #i' | | #p'
    627 | | #sz' #i' | | #p' ]
    628 #v2 #res
    629 whd in ⊢ ((??%?) → ?);
    630 #H destruct
    631 cases v2 in H;
    632 [ | #sz2' #i2' | | #p2'
    633 | | #sz2' #i2' | | #p2' ] normalize nodelta
    634 #H destruct
    635 [ 1,3:
    636   lapply H -H
    637   @(eq_bv_elim … i' (zero ?)) normalize nodelta
    638   #Hi #Heq destruct (Heq)
    639   %{sz'} %{(zero ?)} @conj destruct try @refl
    640   %2 @conj try @conj try @refl
    641 | *: %{sz'} %{i'} @conj try @refl
    642   %1 %{p2'} @conj try @refl
    643 ] qed.
    644 
    645 (* symmetric of the upper one *)
    646 lemma sem_add_pi_inversion :
    647   ∀sz,sg,ty',optlen.
    648   ∀v1,v2,res.
    649   sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
    650   ∃sz',i. v2 = Vint sz' i ∧
    651       ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
    652        (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    653 #tsz #tsg #ty' * [ | #n ]
    654 *
    655 [ | #sz' #i' | | #p'
    656 | | #sz' #i' | | #p' ]
    657 #v2 #res
    658 whd in ⊢ ((??%?) → ?);
    659 #H destruct
    660 cases v2 in H; normalize nodelta
    661 [ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
    662 #H destruct
    663 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1
    664   %{p'} @conj try @refl
    665 | *: lapply H -H
    666   @(eq_bv_elim … i2' (zero ?)) normalize nodelta
    667   #Hi #Heq destruct (Heq)
    668   %{sz2'} %{(zero ?)} @conj destruct try @refl
    669   %2 @conj try @conj try @refl
    670 ] qed.
    671 
    672 (* Know that addition on integers gives an integer. Notice that there is no correlation
    673    between the size in the types and the size of the integer values. *)
    674 lemma sem_add_ii_inversion :
    675   ∀sz,sg.
    676   ∀v1,v2,res.
    677   sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    678   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    679               res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
    680 #sz #sg
    681 *
    682 [ | #sz' #i' | | #p' ]
    683 #v2 #res
    684 whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
    685 cases sz cases sg normalize nodelta
    686 #H destruct
    687 cases v2 in H; normalize nodelta
    688 #H1 destruct
    689 #H2 destruct #Heq %{sz'} lapply Heq -Heq
    690 cases sz' in i'; #i' 
    691 whd in match (intsize_eq_elim ???????);
    692 cases H1 in H2; #j' normalize nodelta
    693 #Heq destruct (Heq)
    694 %{i'} %{j'} @conj try @conj try @conj try @refl
    695 qed.
    696 
    697 lemma sem_sub_pp_inversion :
    698   ∀ty1,ty2,n1,n2.
    699   ∀v1,v2,res.
    700   sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) = Some ? res →
    701   (∃p1,p2,i. v1 =  Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧
    702              division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧
    703              res = Vint I32 i) ∨
    704   (v1 =  Vnull ∧ v2 = Vnull ∧ res = Vint I32 (zero ?)).
    705 #ty1 #ty2 #n1 #n2
    706 cases n1 cases n2
    707 [ | #n1 | #n2 | #n2 #n1 ]
    708 *
    709 [ | #sz #i | | #p
    710 | | #sz #i | | #p
    711 | | #sz #i | | #p
    712 | | #sz #i | | #p ]
    713 #v2 #res
    714 whd in ⊢ ((??%?) → ?);
    715 #H1 destruct
    716 cases v2 in H1;
    717 [ | #sz' #i' | | #p'
    718 | | #sz' #i' | | #p'
    719 | | #sz' #i' | | #p'
    720 | | #sz' #i' | | #p'
    721 | | #sz' #i' | | #p'
    722 | | #sz' #i' | | #p'
    723 | | #sz' #i' | | #p'
    724 | | #sz' #i' | | #p' ]
    725 normalize nodelta
    726 #H2 destruct
    727 try /4 by or_introl, or_intror, conj, refl/
    728 %1 %{p} %{p'}
    729 cases (if_opt_inversion ???? H2)
    730 #Hblocks_eq -H2
    731 @(eqb_elim … (sizeof ty1) 0) normalize nodelta
    732 #Heq_sizeof destruct #Heq destruct
    733 cases (division_u ???) in Heq; normalize nodelta
    734 #H3 destruct #H4 destruct
    735 %{H3} try @conj try @conj try @conj try @conj try @refl
    736 @(eq_block_to_refl … Hblocks_eq)
    737 qed.
    738 
    739 
    740 lemma sem_sub_pi_inversion :
    741   ∀sz,sg,ty',optlen.
    742   ∀v1,v2,res.
    743   sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
    744   ∃sz',i. v2 = Vint sz' i ∧
    745       ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨
    746        (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    747 #tsz #tsg #ty' * [ | #n ]
    748 *
    749 [ | #sz' #i' | | #p'
    750 | | #sz' #i' | | #p' ]
    751 #v2 #res
    752 whd in ⊢ ((??%?) → ?);
    753 #H destruct
    754 cases v2 in H; normalize nodelta
    755 [ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
    756 #H destruct
    757 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1
    758   %{p'} @conj try @refl
    759 | *: lapply H -H
    760   @(eq_bv_elim … i2' (zero ?)) normalize nodelta
    761   #Hi #Heq destruct (Heq)
    762   %{sz2'} %{(zero ?)} @conj destruct try @refl
    763   %2 @conj try @conj try @refl
    764 ] qed.
    765 
    766 
    767 lemma sem_sub_ii_inversion :
    768   ∀sz,sg.
    769   ∀v1,v2,res.
    770   sem_sub v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    771   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    772               res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2).
    773 #sz #sg *             
    774 [ | #sz' #i' | | #p' ]
    775 #v2 #res
    776 whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
    777 cases sz cases sg normalize nodelta
    778 #H destruct
    779 cases v2 in H; normalize nodelta
    780 #H1 destruct
    781 #H2 destruct #Heq %{sz'} lapply Heq -Heq
    782 cases sz' in i'; #i' 
    783 whd in match (intsize_eq_elim ???????);
    784 cases H1 in H2; #j' normalize nodelta
    785 #Heq destruct (Heq)
    786 %{i'} %{j'} @conj try @conj try @conj try @refl
    787 qed.
    788 
    789 
    790 lemma sem_mul_inversion :
    791   ∀sz,sg.
    792   ∀v1,v2,res.
    793   sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    794   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    795               res = Vint sz' (short_multiplication ? i1 i2).
    796 #sz #sg *
    797 [ | #sz' #i' | | #p' ]
    798 #v2 #res
    799 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    800 cases sz cases sg normalize nodelta
    801 #H destruct
    802 cases v2 in H; normalize nodelta
    803 #H1 destruct
    804 #H2 destruct #Heq %{sz'} lapply Heq -Heq
    805 cases sz' in i'; #i' 
    806 whd in match (intsize_eq_elim ???????);
    807 cases H1 in H2; #j' normalize nodelta
    808 #Heq destruct (Heq)
    809 %{i'} %{j'} @conj try @conj try @conj try @refl
    810 qed.
    811 
    812 
    813 lemma sem_div_inversion_s :
    814   ∀sz.
    815   ∀v1,v2,res.
    816   sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
    817   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    818               match division_s ? i1 i2 with
    819               [ Some q ⇒  res =  (Vint sz' q)
    820               | None ⇒ False ].
    821 #sz *
    822 [ | #sz' #i' | | #p' ]
    823 #v2 #res
    824 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    825 >type_eq_dec_true normalize nodelta
    826 #H destruct
    827 cases v2 in H; normalize nodelta
    828 [ | #sz2' #i2' | | #p2' ]
    829 #Heq destruct
    830 %{sz'}
    831 lapply Heq -Heq
    832 cases sz' in i'; #i' 
    833 whd in match (intsize_eq_elim ???????);
    834 cases sz2' in i2'; #i2' normalize nodelta
    835 whd in match (option_map ????); #Hdiv destruct
    836 %{i'} %{i2'} @conj try @conj try @conj try @refl
    837 cases (division_s ???) in Hdiv;
    838 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    839 qed.
    840 
    841 lemma sem_div_inversion_u :
    842   ∀sz.
    843   ∀v1,v2,res.
    844   sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
    845   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    846               match division_u ? i1 i2 with
    847               [ Some q ⇒  res =  (Vint sz' q)
    848               | None ⇒ False ].
    849 #sz *
    850 [ | #sz' #i' | | #p' ]
    851 #v2 #res
    852 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    853 >type_eq_dec_true normalize nodelta
    854 #H destruct
    855 cases v2 in H; normalize nodelta
    856 [ | #sz2' #i2' | | #p2' ]
    857 #Heq destruct
    858 %{sz'}
    859 lapply Heq -Heq
    860 cases sz' in i'; #i' 
    861 whd in match (intsize_eq_elim ???????);
    862 cases sz2' in i2'; #i2' normalize nodelta
    863 whd in match (option_map ????); #Hdiv destruct
    864 %{i'} %{i2'} @conj try @conj try @conj try @refl
    865 cases (division_u ???) in Hdiv;
    866 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    867 qed.
    868 
    869 lemma sem_mod_inversion_s :
    870   ∀sz.
    871   ∀v1,v2,res.
    872   sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
    873   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    874               match modulus_s ? i1 i2 with
    875               [ Some q ⇒  res =  (Vint sz' q)
    876               | None ⇒ False ].
    877 #sz *
    878 [ | #sz' #i' | | #p' ]
    879 #v2 #res
    880 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    881 >type_eq_dec_true normalize nodelta
    882 #H destruct
    883 cases v2 in H; normalize nodelta
    884 [ | #sz2' #i2' | | #p2' ]
    885 #Heq destruct
    886 %{sz'}
    887 lapply Heq -Heq
    888 cases sz' in i'; #i' 
    889 whd in match (intsize_eq_elim ???????);
    890 cases sz2' in i2'; #i2' normalize nodelta
    891 whd in match (option_map ????); #Hdiv destruct
    892 %{i'} %{i2'} @conj try @conj try @conj try @refl
    893 cases (modulus_s ???) in Hdiv;
    894 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    895 qed.
    896 
    897 lemma sem_mod_inversion_u :
    898   ∀sz.
    899   ∀v1,v2,res.
    900   sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
    901   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    902               match modulus_u ? i1 i2 with
    903               [ Some q ⇒  res =  (Vint sz' q)
    904               | None ⇒ False ].
    905 #sz *
    906 [ | #sz' #i' | | #p' ]
    907 #v2 #res
    908 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    909 >type_eq_dec_true normalize nodelta
    910 #H destruct
    911 cases v2 in H; normalize nodelta
    912 [ | #sz2' #i2' | | #p2' ]
    913 #Heq destruct
    914 %{sz'}
    915 lapply Heq -Heq
    916 cases sz' in i'; #i' 
    917 whd in match (intsize_eq_elim ???????);
    918 cases sz2' in i2'; #i2' normalize nodelta
    919 whd in match (option_map ????); #Hdiv destruct
    920 %{i'} %{i2'} @conj try @conj try @conj try @refl
    921 cases (modulus_u ???) in Hdiv;
    922 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    923 qed.
    924 
    925 lemma sem_and_inversion :
    926   ∀v1,v2,res.
    927   sem_and v1 v2 = Some ? res →
    928   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    929               res = Vint sz' (conjunction_bv ? i1 i2).
    930 *
    931 [ | #sz' #i' | | #p' ]
    932 #v2 #res
    933 whd in ⊢ ((??%?) → ?);
    934 #H destruct
    935 cases v2 in H; normalize nodelta
    936 [ | #sz2' #i2' | | #p2' ]
    937 #Heq destruct
    938 %{sz'}
    939 lapply Heq -Heq
    940 cases sz' in i'; #i' 
    941 whd in match (intsize_eq_elim ???????);
    942 cases sz2' in i2'; #i2' normalize nodelta
    943 #H destruct
    944 %{i'} %{i2'} @conj try @conj try @conj try @refl
    945 qed.
    946 
    947 lemma sem_or_inversion :
    948   ∀v1,v2,res.
    949   sem_or v1 v2 = Some ? res →
    950   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    951               res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
    952 *
    953 [ | #sz' #i' | | #p' ]
    954 #v2 #res
    955 whd in ⊢ ((??%?) → ?);
    956 #H destruct
    957 cases v2 in H; normalize nodelta
    958 [ | #sz2' #i2' | | #p2' ]
    959 #Heq destruct
    960 %{sz'}
    961 lapply Heq -Heq
    962 cases sz' in i'; #i' 
    963 whd in match (intsize_eq_elim ???????);
    964 cases sz2' in i2'; #i2' normalize nodelta
    965 #H destruct
    966 %{i'} %{i2'} @conj try @conj try @conj try @refl
    967 qed.
    968 
    969 lemma sem_xor_inversion :
    970   ∀v1,v2,res.
    971   sem_xor v1 v2 = Some ? res →
    972   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    973               res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
    974 *
    975 [ | #sz' #i' | | #p' ]
    976 #v2 #res
    977 whd in ⊢ ((??%?) → ?);
    978 #H destruct
    979 cases v2 in H; normalize nodelta
    980 [ | #sz2' #i2' | | #p2' ]
    981 #Heq destruct
    982 %{sz'}
    983 lapply Heq -Heq
    984 cases sz' in i'; #i' 
    985 whd in match (intsize_eq_elim ???????);
    986 cases sz2' in i2'; #i2' normalize nodelta
    987 #H destruct
    988 %{i'} %{i2'} @conj try @conj try @conj try @refl
    989 qed.
    990 
    991 lemma sem_shl_inversion :
    992   ∀v1,v2,res.
    993   sem_shl v1 v2 = Some ? res →
    994   ∃sz1,sz2,i1,i2.
    995               v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
    996               res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
    997                                   (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
    998               lt_u (bitsize_of_intsize sz2) i2
    999                    (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
    1000 *
    1001 [ | #sz' #i' | | #p' ]
    1002 #v2 #res
    1003 whd in ⊢ ((??%?) → ?);
    1004 #H destruct
    1005 cases v2 in H; normalize nodelta
    1006 [ | #sz2' #i2' | | #p2' ]
    1007 #Heq destruct
    1008 %{sz'} %{sz2'}
    1009 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
    1010 %{i'} %{i2'}
    1011 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
    1012 qed.
    1013 
    1014 lemma sem_shr_inversion :
    1015   ∀v1,v2,sz,sg,res.
    1016   sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    1017   ∃sz1,sz2,i1,i2.
    1018               v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
    1019               lt_u (bitsize_of_intsize sz2) i2
    1020                    (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
    1021               match sg with
    1022               [ Signed ⇒
    1023                  res =
    1024                    (Vint sz1
    1025                     (shift_right bool (7+pred_size_intsize sz1*8)
    1026                      (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
    1027                      (head' bool (7+pred_size_intsize sz1*8) i1)))               
    1028               | Unsigned ⇒
    1029                  res =
    1030                    (Vint sz1
    1031                     (shift_right bool (7+pred_size_intsize sz1*8)
    1032                      (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
    1033               ].
    1034 *
    1035 [ | #sz' #i' | | #p' ]
    1036 #v2 #sz * #res
    1037 whd in ⊢ ((??%?) → ?);
    1038 whd in match (classify_aop ??);
    1039 >type_eq_dec_true normalize nodelta
    1040 #H destruct
    1041 cases v2 in H; normalize nodelta
    1042 [ | #sz2' #i2' | | #p2'
    1043 | | #sz2' #i2' | | #p2' ]
    1044 #Heq destruct
    1045 %{sz'} %{sz2'}
    1046 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
    1047 %{i'} %{i2'}
    1048 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
    1049 qed.
    1050 
    1051 lemma complete_cmp_inversion :
    1052   ∀ty:type.
    1053   ∀e:expr (ASTint I8 Unsigned).
    1054   ∀r:expr (typ_of_type ty).
    1055    complete_cmp ty e = return r →
    1056    ∃sz,sg. ty = Tint sz sg ∧
    1057            r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
    1058 *
    1059 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1060 | #structname #fieldspec | #unionname #fieldspec | #id ]
    1061 #e whd in match (typ_of_type ?);
    1062 #r whd in ⊢ ((??%%) → ?);
    1063 #H destruct
    1064 %{sz} %{sg} @conj try @refl @refl_jmeq
    1065 qed.
    1066 
    1067 
    1068 lemma sem_cmp_int_inversion :
    1069   ∀v1,v2,sz,sg,op,m,res.
    1070    sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
    1071    ∃sz,i1,i2. v1 = Vint sz i1 ∧
    1072               v2 = Vint sz i2 ∧
    1073     match sg with
    1074     [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
    1075     | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
    1076     ].
    1077 #v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
    1078 whd in ⊢ ((??%?) → ?);
    1079 whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
    1080 cases v1
    1081 [ | #sz #i | | #p ] normalize nodelta
    1082 #H destruct
    1083 cases v2 in H;
    1084 [ | #sz' #i' | | #p' ] normalize nodelta
    1085 #H destruct lapply H -H
    1086 cases sz in i; #i
    1087 cases sz' in i'; #i' cases sg normalize nodelta
    1088 whd in match (intsize_eq_elim ???????); #H destruct
    1089 [ 1,2: %{I8}
    1090 | 3,4: %{I16}
    1091 | 5,6: %{I32} ] 
    1092 %{i} %{i'} @conj try @conj try @refl
    1093 qed.
    1094 
    1095 lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr.
    1096 #ty' * // qed.
    1097 
    1098 lemma sem_cmp_ptr_inversion :
    1099   ∀v1,v2,ty',n,op,m,res.
    1100    sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
    1101    (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
    1102                  valid_pointer m p1 = true ∧
    1103                  valid_pointer m p2 = true ∧
    1104                  (if eq_block (pblock p1) (pblock p2)
    1105                   then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
    1106                   else sem_cmp_mismatch op) = Some ? res) ∨
    1107    (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
    1108    (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
    1109    (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
    1110 * [ | #sz #i | | #p ] normalize nodelta
    1111 #v2 #ty' #n #op
    1112 * #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
    1113 whd in match (classify_cmp ??); cases n normalize nodelta
    1114 [ 2,4,6,8: #array_len ]
    1115 whd in match (ptr_type ty' ?);
    1116 whd in match (if_type_eq ?????);
    1117 >type_eq_dec_true normalize nodelta
    1118 #H destruct
    1119 cases v2 in H; normalize nodelta
    1120 [ | #sz' #i' | | #p'
    1121 | | #sz' #i' | | #p'
    1122 | | #sz' #i' | | #p'
    1123 | | #sz' #i' | | #p' ]
    1124 #H destruct
    1125 try /6 by or_introl, or_intror, ex_intro, conj/
    1126 [ 1: %1 %1 %2 %{p} @conj try @conj //
    1127 | 3: %1 %1 %2 %{p} @conj try @conj //
    1128 | *: %1 %1 %1 %{p} %{p'}
    1129      cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
    1130      cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
    1131      try @conj try @conj try @conj try @conj try @conj try @refl try @H
    1132      destruct
    1133 ] qed.
    1134 
    1135 lemma pointer_translation_eq_block :
    1136   ∀E,p1,p2,p1',p2'.
    1137   pointer_translation p1 E = Some ? p1' →
    1138   pointer_translation p2 E = Some ? p2' →
    1139   eq_block (pblock p1) (pblock p2) = true →
    1140   eq_block (pblock p1') (pblock p2') = true.
    1141 #E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
    1142 #H1 #H2 #Heq_block
    1143 lapply (eq_block_to_refl … Heq_block) #H destruct (H)
    1144 lapply H1 lapply H2 -H1 -H2
    1145 whd in ⊢ ((??%?) → (??%?) → ?);
    1146 cases (E b2) normalize nodelta
    1147 [ #Habsurd destruct ]
    1148 * #bx #ox normalize nodelta #Heq1 #Heq2 destruct
    1149 @eq_block_b_b
    1150 qed.
    1151 
    1152 
    1153435(* avoid a case analysis on type inside of a big proof *)
    1154436lemma match_type_inversion_aux : ∀ty,e,f.
     
    1178460qed.
    1179461
    1180  
    1181462
    1182463(* The two following lemmas are just noise. *)
     
    1222503qed.
    1223504
     505lemma sign_ext_sign_ext_reduce :
     506  ∀i. sign_ext 32 16 (sign_ext 16 32 i) = i.
     507#i @refl
     508qed. 
     509
     510lemma sign_ext_zero_ext_reduce :
     511  ∀i. sign_ext 32 16 (zero_ext 16 32 i) = i.
     512#i @refl
     513qed.
     514
     515(* There are two zero_ext, and this causes the "disambiguator" to fail. So we do
     516 * the cleanup ourselves. *)
     517
     518definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext.
     519definition zero_ext_val : ∀target_sz:intsize. val → val ≝ zero_ext.
     520
     521(* CM code uses 8 bit constants and upcasts them to target_size, CL uses 32 bit and
     522 * downcasts them to target_size. In the end, these are equal. We directly state what
     523 * we need. *)
     524lemma value_eq_cl_cm_true :
     525  ∀E,sz.
     526  value_eq E
     527    (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 1)))
     528    (zero_ext_val sz (Vint I8 (repr I8 1))).
     529#E * %2 qed.
     530
     531lemma value_eq_cl_cm_false :
     532  ∀E,sz.
     533  value_eq E
     534    (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 0)))
     535    (zero_ext_val sz (Vint I8 (repr I8 0))).
     536#E * %2 qed.
     537
     538lemma exec_bool_of_val_inversion : ∀v,ty,b.
     539  exec_bool_of_val v ty = OK ? b →
     540  (∃sz,sg,i. v = Vint sz i ∧ ty = Tint sz sg ∧ b = (¬eq_bv (bitsize_of_intsize sz) i (zero (bitsize_of_intsize sz)))) ∨
     541  (∃ty'. v = Vnull ∧ ty = Tpointer ty' ∧ b = false) ∨
     542  (∃ptr,ty'. v = Vptr ptr ∧ ty = Tpointer ty' ∧ b = true).
     543#v #ty #b #Hexec
     544cases v in Hexec;
     545[ | #vsz #i | | #p ]
     546cases ty
     547[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
     548| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
     549| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
     550| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
     551whd in ⊢ ((??%%) → ?);
     552#Heq destruct (Heq)
     553[ 2: %1 %2 %{ptr_ty} @conj try @conj try @refl
     554| 3: %2 %{p} %{ptr_ty}  @conj try @conj try @refl
     555| 1: %1 %1 %{sz} %{sg} lapply Heq -Heq
     556     cases vsz in i; #i cases sz whd in ⊢ ((??%?) → ?);
     557     #Heq destruct %{i} @conj try @conj try @refl
     558] qed.     
     559
     560(* This lemma is noise I extracted from the proof below, even though it is used only once.
     561   Better that than an ugly cut.
     562   We need the following lemma to feed another one down in the deref case. In essence,
     563   it says that the variables present in a cminor expression resulting from converting
     564   a clight deref are transmitted to the cminor counterpart of the pointer argument.
     565   This is made messy by the fact that clight to cminor implements different deref
     566   strategies for different kind of variables.   
     567*)
     568lemma translate_expr_deref_present:
     569      ∀vars:var_types.
     570      ∀ptrdesc:expr_descr.
     571      ∀ptrty:type.
     572      ∀derefty:type.
     573      ∀cm_deref.
     574      ∀Hcm_deref.
     575      ∀cm_ptr.
     576      ∀Hcm_ptr.
     577      ∀cm_env:env.
     578        translate_expr vars (Expr (Ederef (Expr ptrdesc ptrty)) derefty) =OK ? «cm_deref,Hcm_deref» →
     579        expr_vars (typ_of_type derefty) cm_deref (λid:ident.λty0:typ.present SymbolTag ? cm_env id) →
     580        translate_expr vars (Expr ptrdesc ptrty) =OK ? «cm_ptr,Hcm_ptr» →
     581        expr_vars ? cm_ptr (λid:ident.λty0:typ.present SymbolTag ? cm_env id).
     582  #cut_vars #ptrdesc #ptrty #derefty
     583  cases ptrty
     584  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
     585  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
     586  #cut_cm_deref #Hcut_cm_deref #cut_cm_ptr #Hcut_cm_ptr #cut_cm_env
     587  whd in match (translate_expr ??);
     588  cases (translate_expr cut_vars (Expr ptrdesc ?)) normalize nodelta
     589  [ 1,2,3,4,6,8,10,11,12,13,14,16: #err #Habsurd destruct (Habsurd) ]
     590  normalize in match (typ_of_type ?);
     591  * #cut_e' #Hcut_local_e'
     592  lapply Hcut_cm_deref -Hcut_cm_deref lapply cut_cm_deref -cut_cm_deref
     593  cases (access_mode derefty) normalize nodelta
     594  [ #invert_ty | | #invert_ty
     595  | #invert_ty | | #invert_ty
     596  | #invert_ty | | #invert_ty
     597  | #invert_ty | | #invert_ty ]
     598  [ 3,6,9,12: #cut_cm_deref #Hcut_cm_deref #Habsurd destruct (Habsurd) ]
     599  #cut_cm_deref #Hcut_cm_deref #Heq destruct (Heq)
     600  [ 1,3,5,7: whd in ⊢ (% → ?); ]
     601  #Hgoal #Heq destruct @Hgoal
     602qed.
    1224603
    1225604(* TODOs : there are some glitches between clight and cminor :
     
    1307686     cases op
    1308687     whd in ⊢ (? → ? → (??%?) → ?);
    1309      [ 1: (* add *)
     688     [ 1: (* add *) 
    1310689       lapply (classify_add_inversion (typeof e1) (typeof e2))
    1311690       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     
    1500879              whd in match (eval_expr ???????);
    1501880              whd in match (eval_expr ???????);
     881              whd in match (proj2 ???);
    1502882              [ >(eval_expr_rewrite_aux … Heval_rhs)
    1503883              | >Heval_rhs ]
     
    1506886       | 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    1507887            whd in match (eval_expr ???????);
     888            whd in match (proj2 ???);
     889            whd in match (eval_expr ???????);
     890            whd in match (proj1 ???);
    1508891            whd in match (eval_expr ???????);
    1509892            >Heval_rhs normalize nodelta
    1510893            whd in match (eval_unop ????);
    1511894       ]
    1512        [ 1: (* ptr/ptr sub *)
     895       [ 1:       
     896        (* ptr/ptr sub *)
    1513897            whd in Hsem_binary:(??%?);
    1514898            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     899            -Hsem_binary
    1515900            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1516             lapply (sem_sub_pp_inversion … Hsem_binary_translated) *
     901            lapply (sem_sub_pp_inversion … Hsem_binary_translated)
     902            * #ty_sz' * #ty_sg' * #Heq destruct (Heq) *
    1517903            [ (* regular pointers case *)
    1518904              * #lhs_ptr * #rhs_ptr * #resulting_offset * * * *
     
    1524910              whd in match (m_bind ?????);
    1525911              whd in match (eval_binop ???????);
     912              normalize in match (bitsize_of_intsize ?);
     913              normalize in match (S (7+pred_size_intsize I16*8)) in Hoffset_eq;
     914              >Hoffset_eq
     915              (* whd in match (pred_size_intsize ?); normalize in match (7+1*8); *)
    1526916              (* size mismatch between CL and CM. TODO *)
    1527               @cthulhu
     917              >Hoffset_eq normalize nodelta
     918              whd in match (eval_unop ????);
     919              %{cm_val} >Hcm_val_eq
     920              whd in match (opt_to_res ???);
     921              whd in match (m_bind ?????); @conj
     922              [ 2: destruct assumption
     923              | 1: whd in match (zero_ext ? (Vint ??));
     924                   whd in match E0; whd in match (Eapp ? []); >append_nil
     925                   normalize in match (bitsize_of_intsize ?); try @refl ]
    1528926            | (* null pointers case *)
    1529927              * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct
     
    1537935              whd in match (m_bind ?????);
    1538936              whd in match (pred_size_intsize ?);
    1539               %{(zero_ext ty_sz (Vint I16 (zero (S (7+1*8)))))} @conj
     937              %{(zero_ext ty_sz' (Vint I32 (zero (S (7+3*8)))))} @conj
    1540938              [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ]
    1541939              whd in Hsem_binary_translated:(??%?);
    1542940              normalize nodelta in Hsem_binary_translated:(??%?);
    1543               lapply Hsem_binary_translated; -Hsem_binary_translated;
     941              lapply Hsem_binary_translated; -Hsem_binary_translated
    1544942              cases n1 cases n2
    1545943              [ | 2,3: #n | #n1 #n2 ] normalize nodelta
    1546944              #Heq destruct (Heq)
    1547               (* size mismatch between CL and CM. TODO *)
    1548               @cthulhu
     945              whd in match (zero_ext ??);
     946              cases ty_sz' in Hvalue_eq_res; try //
    1549947            ]
    1550948       | 2: (* int/int sub *)
     
    1565963       | 3: (* ptr/int sub *)
    1566964            whd in Hsem_binary:(??%?);
    1567             lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     965            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary
    1568966            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1569967            lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated
     
    1573971            whd in match (eval_unop ????);
    1574972            -Heval_lhs -Heval_rhs destruct
     973            whd in match (proj2 ???);
     974            whd in match (proj1 ???);
    1575975            whd in match (proj2 ???);           
     976            whd in match (eval_expr ???????);
    1576977            @(match sg
    1577978              return λs. sg = s → ?
     
    1580981              | Signed ⇒ λHsg. ?
    1581982              ] (refl ??)) normalize nodelta
    1582             whd in match (eval_expr ???????);
     983            whd in match (eval_unop ????);
    1583984            whd in match (m_bind ?????);
    1584985            whd in match (eval_binop ???????);
    1585986            [ 1,2:
    1586                 %{(Vptr
    1587                   (neg_shift_pointer_n (bitsize_of_intsize cm_vsz) lhs_ptr (sizeof ty') sg
    1588                    cm_rhs_v))} try @conj try assumption
    1589                    (* TODO size mismatch (?) or insert zero/sign_ext in semantics *)
    1590                    (*            [ 1,2,3,4: @conj whd in match (E0);
    1591                         whd in match (Eapp trace_rhs ?);
    1592                         whd in match (Eapp trace_lhs ?);                     
    1593                         >(append_nil … trace_rhs) try @refl
    1594                         >(append_nil … trace_lhs) try @refl
    1595                         @(value_eq_triangle_diagram … Hvalue_eq_res)
    1596                         whd in match (shift_pointer_n ?????);
    1597                         whd in match (shift_offset_n ?????);
    1598                         >Hsg normalize nodelta
    1599                         >commutative_short_multiplication
    1600                         whd in match (shift_pointer ???);
    1601                         whd in match (shift_offset ???);
    1602                         >sign_ext_same_size @refl *)                   
    1603                 @cthulhu ]
     987               whd in match (neg_shift_pointer_n ?????) in Hvalue_eq_res;
     988               whd in match (neg_shift_offset_n ?????) in Hvalue_eq_res;
     989               whd in match (neg_shift_pointer ???);
     990               whd in match (neg_shift_offset ???);
     991               destruct (Hsg) normalize nodelta in Hvalue_eq_res;
     992               [ >sign_ext_sign_ext_reduce
     993                 %{(Vptr
     994                     (mk_pointer (pblock lhs_ptr)
     995                      (mk_offset
     996                         (subtraction offset_size (offv (poff lhs_ptr))
     997                           (short_multiplication (bitsize_of_intsize I16)
     998                              (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
     999                                 (repr I16 (sizeof ty')))))))}
     1000                  @conj
     1001                  [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
     1002                  | >commutative_short_multiplication @Hvalue_eq_res ]
     1003               | >sign_ext_zero_ext_reduce
     1004                 %{(Vptr
     1005                     (mk_pointer (pblock lhs_ptr)
     1006                      (mk_offset
     1007                         (subtraction offset_size (offv (poff lhs_ptr))
     1008                           (short_multiplication (bitsize_of_intsize I16)
     1009                              (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
     1010                                 (repr I16 (sizeof ty')))))))}
     1011                 @conj
     1012                  [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
     1013                  | >commutative_short_multiplication @Hvalue_eq_res ]
     1014              ]                         
     1015            ]
    16041016            [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
    1605             | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]
    1606             >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
    1607             >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
     1017              >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
     1018              >(sign_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32))
     1019            | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
     1020              >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
     1021              >(zero_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32)) ]
     1022            >(eq_bv_true … (zero 32)) normalize nodelta
     1023           %{Vnull} @conj try assumption
    16081024           normalize >append_nil try @refl
    16091025       ]     
     
    19131329            cases (bind_inversion ????? Hexec) -Hexec
    19141330            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1915             lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1916             whd in match (typeof ?); whd in match (sem_binary_operation ??????);
    1917             #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
     1331            lapply (opt_to_res_inversion ???? Hsem) -Hsem           
     1332            whd in match (typeof ?); whd in match (sem_binary_operation ???????);
     1333            normalize nodelta
     1334            #Hsem_cmp cases (some_inversion ????? Hsem_cmp) -Hsem_cmp
     1335            #cl_val' * #Hsem_cmp #Hcl_val_cast
     1336            destruct (Hcl_val_cast)
     1337            lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
    19181338            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
    19191339            destruct (Hcl_lhs) destruct (Hcl_rhs)
     
    19391359            whd in match (opt_to_res ???);
    19401360            whd in match (m_bind ?????);
    1941             (* finished modulo glitch in integer widths *)
    1942             @cthulhu
    1943        | *:
     1361            whd in match (of_bool ?);
     1362            [ %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
     1363            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
     1364            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
     1365            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
     1366            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
     1367            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
     1368            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
     1369            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
     1370            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
     1371            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
     1372            | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))}
     1373            | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))} ]
     1374            @conj try @refl
     1375            whd in match (FE_of_bool ?); whd in match FEtrue; whd in match FEfalse;
     1376            [ 1,3,5,7,9,11:
     1377              cases (cmp_int ????) normalize nodelta
     1378            | *:
     1379              cases (cmpu_int ????) normalize nodelta ]           
     1380            try @value_eq_cl_cm_true
     1381            try @value_eq_cl_cm_false
     1382       | *: (* ptr comparison *)
    19441383            #n #ty' #Hety1 #Hety2 #Hclassify
    19451384            lapply (jmeq_to_eq ??? Hety1) #Hety1'
     
    19611400            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    19621401            lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1963             whd in match (typeof ?); whd in match (sem_binary_operation ??????);
    1964             #Hsem_cmp (* cut > *)
     1402            whd in match (typeof ?); whd in match (sem_binary_operation ???????);
     1403            #Hsem_cmp
     1404            cases (some_inversion ????? Hsem_cmp) -Hsem_cmp normalize nodelta
     1405            #cl_val' * #Hsem_cmp #Hcl_val_cast destruct (Hcl_val_cast);
    19651406            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
    19661407            * #Hyp_present_lhs #Hyp_present_rhs
    19671408            #Hind_rhs #Hind_lhs
    19681409            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
    1969             * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1410            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs -Hexec_rhs
    19701411            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
    1971             * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1972             lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp)
     1412            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs -Hexec_lhs
     1413            lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp) -Hsem_cmp
    19731414            -Hvalue_eq_lhs -Hvalue_eq_rhs
    1974             * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res %{cm_val} @conj try assumption
    1975             lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm -Hsem_cmp
     1415            * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res
     1416            whd in match (eval_expr ???????);
     1417            whd in match (eval_expr ???????);
     1418            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
     1419            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
     1420            whd in match (m_bind ?????);           
     1421            lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm
    19761422            *
    19771423            [ 2,4,6,8,10,12:
    1978               * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1424              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
     1425              whd in Hsem_cmp:(??%?); destruct
    19791426            | *: *
    19801427              [ 2,4,6,8,10,12:
    1981                 * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1428                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
     1429                whd in Hsem_cmp:(??%?); destruct
    19821430              | *: *
    19831431                [ 2,4,6,8,10,12:
    1984                   * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
    1985                 | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
    1986             ] ] ]
    1987             whd in match (eval_expr ???????);
    1988             whd in match (eval_expr ???????);
    1989             whd in Hsem_cmp:(??%?);
    1990             destruct (Hsem_cmp)                       
    1991             >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    1992             >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
    1993             whd in match (m_bind ?????);
     1432                  * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
     1433                  whd in Hsem_cmp:(??%?); destruct
     1434                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome
     1435                     whd in Hsem_cmp:(??%?); destruct
     1436                ]
     1437              ]
     1438            ]
    19941439            whd in match (eval_binop ???????);
    1995             [ 1,2,3,4,5,6:
    1996               (* qed modulo integer width glitch *)
    1997               @cthulhu
     1440            normalize nodelta
     1441            whd in match (eval_unop ????);
     1442            whd in match (opt_to_res ???);
     1443            whd in match (m_bind ?????);
     1444            [ 1,2,3,4,5,6:
     1445              [ 1,4,6:
     1446                %{(zero_ext tysz FEtrue)} @conj try @refl
     1447                >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
     1448                @value_eq_cl_cm_true
     1449              | 2,3,5:
     1450                %{(zero_ext tysz FEfalse)} @conj try @refl
     1451                >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
     1452                @value_eq_cl_cm_false
     1453              ]
    19981454            | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
    19991455                 lapply Heq_block_outcome -Heq_block_outcome
    20001456                 @(eq_block_elim … (pblock p1) (pblock p2))
    20011457                 normalize nodelta
     1458                 whd in match (eval_unop ????);
     1459                 whd in match (opt_to_res ???);
     1460                 whd in match (m_bind ?????);
    20021461                 [ 1,3,5,7,9,11:
    20031462                   #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
    20041463                   whd in match (eval_unop ????);
    20051464                   whd in match (m_bind ?????);
    2006                    cases (cmp_offset ???) normalize nodelta
    2007                    (* glitch *)
    2008                    @cthulhu
     1465                   cases (cmp_offset ???) in Hvalue_eq_res; normalize nodelta
     1466                   #Hvalue_eq_res >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
     1467                   [ 1,3,5,7,9,11: %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
     1468                                   @value_eq_cl_cm_true
     1469                   | 2,4,6,8,10,12: %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
     1470                                    @value_eq_cl_cm_false
     1471                   ]
    20091472                 | *:
    20101473                   #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    2011                    whd in match (eval_unop ????);
    2012                    whd in match (m_bind ?????);
    2013                    @cthulhu
    2014                  ]
     1474                   >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
     1475                   [ %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
     1476                     @value_eq_cl_cm_false
     1477                   | %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
     1478                     @value_eq_cl_cm_true
     1479                   ]
     1480                ]
    20151481           ]
    20161482       ]
     
    22071673       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
    22081674       #Hind #Htranslate_expr #Hexec_cl
    2209        cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
     1675       cases (bind_inversion ????? Htranslate_expr) (* -Htranslate_expr *)
    22101676       * whd in match (typ_of_type ?); normalize nodelta
    22111677       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
     
    22151681       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
    22161682       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
    2217        [ 1,3,5,7: @cthulhu ]
     1683       [ 1,3,5,7: @(translate_expr_deref_present … Htranslate_expr … Hyp_present … Htranslate_expr_ind) ]
    22181684       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
    22191685       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
     
    22311697       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
    22321698       -Hopt_to_res
     1699       lapply Hexec_cm_ind -Hexec_cm_ind
    22331700       lapply Hyp_present -Hyp_present
     1701       lapply Htranslate_expr -Htranslate_expr
    22341702       lapply Hexpr_vars -Hexpr_vars
    22351703       lapply cm_expr -cm_expr
    2236        inversion (access_mode ty)
    2237        [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
    2238        lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
    2239        #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
     1704       cases ty (* Inversion (access_mode ty) fails for whatever reason. *)
     1705       [ | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
     1706       | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
     1707       | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
     1708       | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 ]
     1709       whd in match (typ_of_type ?); whd in match (access_mode ?); normalize nodelta
     1710       #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_cm_ind #Hcl_load_success
    22401711       #Heq destruct (Heq)
    2241        [ 1,2,3,4: (* By_value *)
     1712       [ 3,4,8,9,13,14,18,19: (*  By reference *)
     1713           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
     1714           lapply (load_value_of_type_by_ref … Hcl_load_success ??)
     1715           try @refl_jmeq
     1716           #Hval >Hval %4 assumption
     1717       | *: (* By_value *)
    22421718           (* project Hcl_load_success in Cminor through memory_inj *)
    22431719           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
    2244            [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
     1720           try @(load_by_value_success_valid_pointer … Hcl_load_success)
     1721           try @jmeq_to_eq
     1722           try assumption try @refl_jmeq
    22451723           * #cm_val * #Hcm_load_success #Hvalue_eq
    2246            lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
     1724           lapply (load_value_of_type_by_value … Hcm_load_success)
     1725           try @refl
    22471726           #Hloadv_cm
    22481727           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
    2249            >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
    2250       | *: (* By reference *)
    2251            >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
    2252            lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
    2253            #Hval >Hval %4 assumption ]
     1728           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption ]
    22541729  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
    22551730       lapply (refl ? (typeof e1))
     
    27162191    normalize %{cm_val2} @conj try @refl assumption ]
    27172192| 10: (* andbool *)
    2718   #ty cases ty
     2193  #ty
     2194  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
     2195  cases ty
    27192196  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    27202197  | #structname #fieldspec | #unionname #fieldspec | #id ]
    2721   #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
    27222198  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
    27232199  (* decompose first slice of clight execution *)
     
    27252201  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
    27262202  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2727   #b * #Hexec_bool_of_val #Hexec_expr
    2728   (* decompose translation to Cminor *)
     2203(* cut *) 
     2204  * * normalize nodelta #Hexec_bool_of_val
     2205  [ 2,4,6,8,10,12,14:
     2206    whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     2207  | 16: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
     2208  | *:
     2209    #Hexec_expr   
     2210    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     2211    * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
     2212    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     2213    #b2 * #Hexec_bool_of_val_e2
     2214    whd in ⊢ ((???%) → ?); #Heq
     2215    destruct (Heq) ]
    27292216  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
    27302217  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
    27312218  cases (bind_inversion ????? Htranslate) -Htranslate
    2732   * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
    2733   [ 2: | *: #Heq destruct (Heq) ]
    2734   (* discriminate I16 and I8 cases *)
    2735 (*  lapply Hyp_present -Hyp_present
    2736   lapply Hexpr_vars -Hexpr_vars
    2737   lapply cm_expr -cm_expr cases sz
    2738   #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
    2739   [ 1,2: #Habsurd destruct (Habsurd) ]   *)
    2740   (* go on with decomposition *)
    2741   #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
    2742   * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
     2219  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
     2220  cases (bind_inversion ????? Htranslate) -Htranslate
     2221  * #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
     2222  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
     2223  * #Htypeof_e2_eq_ty
    27432224  (* cleanup the type coercion *)
    2744   lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
    2745   * #Htypeof_e2_eq_ty
    27462225  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
    2747   lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
     2226  lapply Hexpr_vars_wt -Hexpr_vars_wt
    27482227  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
    27492228  lapply Hexpr_vars_e2 -Hexpr_vars_e2
    27502229  lapply cm_expr_e2 -cm_expr_e2
    2751   lapply Hexec_expr -Hexec_expr
    2752   >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
    2753   #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
    2754   #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
    2755   (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
    2756    * to proceed in decomposing translation. *)
     2230  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty   
     2231  #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
     2232
     2233  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
    27572234  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
    27582235  lapply Hexpr_vars_e1 -Hexpr_vars_e1
    27592236  lapply cm_expr_e1 -cm_expr_e1
    2760   lapply Hexec_bool_of_val -Hexec_bool_of_val
    2761   cases (typeof e1)
    2762   [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
    2763   | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
    2764   #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
    2765   normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    2766   (* translation decomposition terminated. Reduce goal *)
     2237  cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
     2238  [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
     2239         destruct >(Htypeof_e1) whd in match (typ_of_type ?);
     2240         #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
     2241         whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     2242  *
     2243  [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
     2244         destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
     2245         #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
     2246         #Habsurd destruct (Habsurd) ]
     2247  * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
     2248  destruct >Htypeof_e1 #Heq_bv
     2249  whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);   
     2250  #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
     2251  whd in match (typ_of_type ?);
     2252  whd in ⊢ ((???%) → ?); #Heq 
     2253  destruct (Heq) cases Hyp_present -Hyp_present
     2254  * #Hyp_present_e1 * * #Hyp_present_e2 normalize in ⊢ (% → % → % → ?);
     2255  * * *
     2256  lapply (Hind1 … Hyp_present_e1 Hexec_e1)
     2257  * #cm_val_1 * #Heval_expr1 #Hvalue_eq
     2258  whd in match (eval_expr ???????); whd in match (proj2 ???); whd in match (proj2 ???);
     2259  >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
     2260  whd in match (eval_bool_of_val ?);
     2261  <Heq_bv
     2262  whd in match (m_bind ?????);
     2263  [ %{(Vint sz (zero (bitsize_of_intsize sz)))}
     2264    >zero_ext_zero @conj try %2
     2265    whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
     2266  normalize nodelta
     2267  lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
     2268  -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
     2269  whd in match (eval_expr ???????); >Heval_expr2
     2270  normalize nodelta
     2271  cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
     2272  [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
     2273       destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
     2274       #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
     2275       whd in match (eval_bool_of_val ?);
     2276       whd in match (m_bind ?????); normalize nodelta
     2277       >zero_ext_one
     2278       %{(Vint sz (repr sz 1))} @conj try %2
     2279       whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
     2280  *
     2281  [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
     2282      >(value_eq_null_inversion … Hvalue_eq2)
     2283      whd in match (eval_bool_of_val ?);
     2284      whd in match (m_bind ?????);
     2285      normalize nodelta
     2286      %{(Vint sz (zero (bitsize_of_intsize sz)))}
     2287      >zero_ext_zero @conj try %2
     2288      whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
     2289  * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
     2290  destruct (Hcl_val_e2)
     2291  >(value_eq_int_inversion … Hvalue_eq2)
     2292  whd in match (eval_bool_of_val ?); <Heq_bv
     2293  cases b2 in Heq_bv; #Heq_bv
     2294  whd in match (m_bind ?????); normalize nodelta
     2295  [ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
     2296    >append_nil @conj try @refl >zero_ext_one %2
     2297  | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
     2298    >append_nil @conj try @refl >zero_ext_zero %2 ]
     2299| 11: (* orbool, similar to andbool *)
     2300  #ty
     2301  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
     2302  cases ty
     2303  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     2304  | #structname #fieldspec | #unionname #fieldspec | #id ]
     2305  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
     2306  (* decompose first slice of clight execution *)
     2307  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     2308  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
     2309  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     2310  * * normalize nodelta #Hexec_bool_of_val
     2311  [ 1,3,5,7,9,11,13,15:
     2312    whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     2313  | *:
     2314    #Hexec_expr   
     2315    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     2316    * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
     2317    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     2318    #b2 * #Hexec_bool_of_val_e2
     2319    whd in ⊢ ((???%) → ?); #Heq
     2320    destruct (Heq) ]
     2321  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
     2322  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
     2323  cases (bind_inversion ????? Htranslate) -Htranslate
     2324  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
     2325  cases (bind_inversion ????? Htranslate) -Htranslate
     2326  * #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
     2327  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
     2328  * #Htypeof_e2_eq_ty
     2329  (* cleanup the type coercion *)
     2330  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
     2331  lapply Hexpr_vars_wt -Hexpr_vars_wt
     2332  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
     2333  lapply Hexpr_vars_e2 -Hexpr_vars_e2
     2334  lapply cm_expr_e2 -cm_expr_e2
     2335  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty   
     2336  #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
     2337  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
     2338  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
     2339  lapply Hexpr_vars_e1 -Hexpr_vars_e1
     2340  lapply cm_expr_e1 -cm_expr_e1
     2341  cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
     2342  [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
     2343         destruct >(Htypeof_e1) whd in match (typ_of_type ?);
     2344         #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
     2345         whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     2346  *
     2347  [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
     2348         destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
     2349         #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
     2350         #Habsurd destruct (Habsurd) ]
     2351  * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
     2352  destruct >Htypeof_e1 #Heq_bv
     2353  whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);   
     2354  #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
     2355  whd in ⊢ ((???%) → ?); #Heq
     2356  destruct (Heq) cases Hyp_present -Hyp_present
     2357  * #Hyp_present_e1 * * * #Hyp_present_e2 * *
     2358  lapply (Hind1 … Hyp_present_e1 Hexec_e1)
     2359  * #cm_val_1 * #Heval_expr1 #Hvalue_eq
    27672360  whd in match (eval_expr ???????);
    2768   (* We need Hind1.  *)
    2769   cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
    2770   lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
     2361  >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
     2362  whd in match (eval_bool_of_val ?);
     2363  <Heq_bv
     2364  whd in match (m_bind ?????);
     2365  [ %{(Vint sz (repr sz 1))}
     2366    >zero_ext_one @conj try %2
     2367    whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
    27712368  normalize nodelta
    2772   (* peform case analysis to further reduce the goal. *)
    2773   lapply Hvalue_eq -Hvalue_eq
    2774   lapply Hexec_bool_of_val -Hexec_bool_of_val
    2775   whd in match (proj2 ???);
    2776   cases cl_val_e1
    2777   [ | #vsz #vi | | #vp
    2778   | | #vsz #vi | | #vp
    2779   | | #vsz #vi | | #vp
    2780   | | #vsz #vi | | #vp ]
    2781   whd in ⊢ ((??%%) → ?);
    2782   [ 6:
    2783   | *: #Heq destruct (Heq) ]
    2784   #Hsz_check #Hvalue_eq
    2785   lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
    2786   * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
    2787   (* preparing case analysis on b *)
    2788   lapply Hexec_expr -Hexec_expr
    2789   cases b normalize nodelta
    2790   [ 2: (* early exit *)
    2791        #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
    2792        #Heq_outcome destruct (Heq_outcome) -Heq_outcome
    2793        >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
    2794        <e0 whd in match (m_bind ?????);
    2795        @cthulhu
    2796        (* Pb: incompatible semantics for cl and cm.
    2797         * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
    2798           first operand is false (for andbool)
    2799           . solution 1 : change semantics to return actual value instead of Vfalse
    2800           . solution 2 : change toCminor to introduce another test in the program,
    2801             returning Vfalse in case of failure instead of actual value
    2802         *) ]
    2803   #Hexec_expr #Heq_outcome
    2804   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2805   * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
    2806   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2807   #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
    2808   #Heq destruct (Heq)
    2809   >(value_eq_int_inversion … Hvalue_eq)
    2810   whd in match (eval_bool_of_val ?);
    2811   destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
     2369  lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
     2370  -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
     2371  whd in match (eval_expr ???????); >Heval_expr2
    28122372  normalize nodelta
    2813   cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
    2814   >Heval_expr normalize nodelta
    2815   %{cm_val_e2} @conj try @refl 
    2816   whd in Hexec_bool_outcome:(??%%);
    2817   normalize nodelta in Hexec_bool_outcome:(??%%);
    2818   lapply Hvalue_eq2 -Hvalue_eq2
    2819   -Heval_expr
    2820   lapply Hexec_bool_outcome -Hexec_bool_outcome
    2821   cases cl_val_e2
    2822   [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
    2823   #Heq destruct (Heq)
    2824   cases (intsize_eq_elim_inversion ??????? Heq)
    2825   #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
    2826   cases outcome_bool normalize nodelta
    2827   (* Problem. cf prev case. *)
    2828   @cthulhu
    2829 | 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
     2373  cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
     2374  [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
     2375       destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
     2376       #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
     2377       whd in match (eval_bool_of_val ?);
     2378       whd in match (m_bind ?????); normalize nodelta
     2379       >zero_ext_one
     2380       %{(Vint sz (repr sz 1))} @conj try %2
     2381       whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
     2382  *
     2383  [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
     2384      >(value_eq_null_inversion … Hvalue_eq2)
     2385      whd in match (eval_bool_of_val ?);
     2386      whd in match (m_bind ?????);
     2387      normalize nodelta
     2388      %{(Vint sz (zero (bitsize_of_intsize sz)))}
     2389      >zero_ext_zero @conj try %2
     2390      whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
     2391  * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
     2392  destruct (Hcl_val_e2)
     2393  >(value_eq_int_inversion … Hvalue_eq2)
     2394  whd in match (eval_bool_of_val ?); <Heq_bv
     2395  cases b2 in Heq_bv; #Heq_bv
     2396  whd in match (m_bind ?????); normalize nodelta
     2397  [ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
     2398    >append_nil @conj try @refl >zero_ext_one %2
     2399  | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
     2400    >append_nil @conj try @refl >zero_ext_zero %2 ]
    28302401| 12: (* sizeof *)
    28312402  #ty cases ty
     
    28722443       * #BL #OFF normalize nodelta #Heq destruct (Heq)
    28732444       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
    2874        #H destruct (H)
    2875        (* again, mismatch in the size of the integers *)
    2876        @cthulhu
     2445       #H destruct (H)       
     2446       whd in match (shift_pointer ???);
     2447       whd in match (shift_offset ???) in ⊢ (???%);
     2448       >sign_ext_same_size
     2449       whd in match (offset_plus ??) in ⊢ (??%%);
     2450       <(associative_addition_n ? (offv off))
     2451       >(commutative_addition_n … (repr I16 field_off) (offv OFF))
     2452       >(associative_addition_n ? (offv off))
     2453       @refl       
    28772454  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
    28782455       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
Note: See TracChangeset for help on using the changeset viewer.