Changeset 2554


Ignore:
Timestamp:
Dec 13, 2012, 5:22:51 PM (7 years ago)
Author:
garnier
Message:

Proof of expression translation correctness "mostly" done for CL to CM. Some inconsistencies found in bit width for constants
regarding boolean operators need to be fixed (either by modifying CL semantics of by making CM code generation inefficient).
An inconsistency between clight and cminor expression evaluation was found for cost labels (placed before and after trace) - not
fixed yet, for fear of breaking proofs. One or two small lemmas missing, and most importantly, binary operators not done yet.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2500 r2554  
    371371
    372372
    373 (* A particular inversion. *)
     373(* particulars inversion. *)
    374374lemma value_eq_ptr_inversion :
    375375  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
     
    381381     %{p2} @conj try @refl try assumption
    382382] qed.
     383
     384lemma value_eq_int_inversion :
     385  ∀E,sz,i,v. value_eq E (Vint sz i) v → v = (Vint sz i).
     386#E #sz #i #v #Heq inversion Heq
     387[ 1: #Habsurd destruct (Habsurd)
     388| 2: #sz #i #Heq #Heq' #_ @refl
     389| 3: #Habsurd destruct (Habsurd)
     390| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
     391qed.
    383392
    384393(* A cleaner version of inversion for [value_eq] *)
  • src/Clight/toCminor.ma

    r2533 r2554  
    682682      ]
    683683  | Eunop op e1 ⇒
    684       do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
    685       do e1' ← translate_expr vars e1;
    686       OK ? «Op1 ?? op' e1', ?»
     684     match op
     685      return λx. (op = x) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
     686      with
     687      [ Onotbool ⇒ λHop.
     688        match typ_of_type ty
     689        return λy. (typ_of_type ty = y) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
     690        with
     691        [ ASTint sz sg ⇒  λHtyp_of_type.
     692          match sz
     693          return λz. (sz = z) → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars))
     694          with
     695          [ I32 ⇒ λHsz.
     696            do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
     697            do e1' ← translate_expr vars e1;
     698            OK ? «Op1 ?? op' e1', ?»
     699          | _ ⇒ λHsz.
     700            Error ? (msg TypeMismatch)
     701          ] (refl ? sz)
     702        | _ ⇒ λHtyp_of_type.
     703          Error ? (msg TypeMismatch)
     704        ] (refl ? (typ_of_type ty))       
     705      | _ ⇒ λHop.
     706        do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
     707        do e1' ← translate_expr vars e1;
     708        OK ? «Op1 ?? op' e1', ?»
     709      ] (refl ? op)
    687710  | Ebinop op e1 e2 ⇒
    688711      do e1' ← translate_expr vars e1;
     
    710733      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
    711734      [ Tint sz sg ⇒
    712         do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    713         match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?) with
    714         [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
    715         | _ ⇒ λ_.Error ? (msg TypeMismatch)
    716         ] e1'
     735          do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
     736          match typ_of_type (typeof e1)
     737          return λx.
     738            (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?)
     739          with
     740          [ ASTint sz1 _ ⇒ λe1'.
     741            OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
     742          | _ ⇒ λ_. Error ? (msg TypeMismatch)
     743          ] e1'
    717744      | _ ⇒ Error ? (msg TypeMismatch)
    718       ]     
     745      ]
     746(*  | Eandbool e1 e2 ⇒
     747      do e1' ← translate_expr vars e1;
     748      do e2' ← translate_expr vars e2;
     749      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
     750      [ Tint sz sg ⇒
     751        match sz
     752        return λsz'. (sz = sz') → res (Σe':CMexpr (typ_of_type ?). ?)
     753        with
     754        [ I32 ⇒ λHsz_eq.
     755          do e2' ← type_should_eq ? (Tint I32 sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
     756          match typ_of_type (typeof e1)
     757          return λx.
     758            (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?)
     759          with
     760          [ ASTint sz1 _ ⇒ λe1'.
     761            OK ? «Cond ??? e1' e2' (Cst ? (Ointconst I32 sg (zero ?))), ?»
     762          | _ ⇒ λ_. Error ? (msg TypeMismatch)
     763          ] e1'
     764        | _ ⇒ λ_. Error ? (msg TypeMismatch)
     765        ] (refl ? sz)
     766      | _ ⇒ Error ? (msg TypeMismatch)
     767      ]*)
    719768  | Eorbool e1 e2 ⇒
    720769      do e1' ← translate_expr vars e1;
     
    804853[ >E whd >Heq_c @refl
    805854| 2,3: @pi2
     855| cases e1' //
     856| cases e1' //
    806857| @(translate_binop_vars … E) @pi2
    807858| % [ % ] @pi2
  • src/Clight/toCminorCorrectness.ma

    r2545 r2554  
    471471qed.
    472472
    473 (* TODO convert Clight unary ops to front-end ops ops, then prove correspondence for operators (with equal values). *)
    474 
     473lemma typ_eq_elim :
     474  ∀t1,t2.
     475  ∀(P: (t1=t2)+(t1≠t2) → Prop).
     476  (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
     477#t1 #t2 #P #Hl #Hr
     478@(match typ_eq t1 t2
     479  with
     480  [ inl H ⇒ Hl H
     481  | inr H ⇒ Hr H ])
     482qed.
     483
     484
     485lemma translate_notbool_to_cminor :
     486  ∀t,sg,arg.
     487  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
     488  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
     489        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
     490*
     491[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     492| #structname #fieldspec | #unionname #fieldspec | #id ]
     493normalize in match (typ_of_type ?);
     494#sg #arg #cmop
     495whd in ⊢ (??%% → ?); #Heq destruct (Heq)
     496cases arg
     497[ | #vsz #vi | | #vp
     498| | #vsz #vi | | #vp
     499| | #vsz #vi | | #vp
     500| | #vsz #vi | | #vp
     501| | #vsz #vi | | #vp
     502| | #vsz #vi | | #vp
     503| | #vsz #vi | | #vp
     504| | #vsz #vi | | #vp ]
     505#res
     506whd in ⊢ ((??%?) → ?);
     507#Heq
     508[ 6,11,12: | *: destruct (Heq) ]
     509[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
     510| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
     511     #H normalize nodelta #Heq destruct
     512     whd in match (eval_unop ????);
     513     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
     514] qed.
     515
     516lemma translate_notint_to_cminor :
     517  ∀t,t',arg.
     518  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
     519  ∀res. sem_unary_operation Onotint arg t = Some ? res →
     520        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
     521#ty *
     522[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
     523#sz #sg #arg #cmop
     524whd in match (translate_unop ???);
     525@(match typ_eq (ASTint sz sg) (typ_of_type ty)
     526  with
     527  [ inl H ⇒ ?
     528  | inr H ⇒ ? ])
     529normalize nodelta
     530[ 2: #Heq destruct ]
     531lapply H -H
     532lapply cmop -cmop
     533cases ty
     534[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
     535| #structname #fieldspec | #unionname #fieldspec | #id ]
     536normalize nodelta
     537#cmop normalize in match (typ_of_type ?); #H destruct
     538#H' normalize in H';
     539destruct (H')
     540#res
     541whd in match (sem_unary_operation ???);
     542cases arg
     543[ | #vsz #vi | | #vp
     544| | #vsz #vi | | #vp
     545| | #vsz #vi | | #vp
     546| | #vsz #vi | | #vp ]
     547whd in match (sem_notint ?);
     548#H destruct (H) @refl
     549qed.
     550
     551
     552lemma translate_negint_to_cminor :
     553  ∀t,t',arg.
     554  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
     555  ∀res. sem_unary_operation Oneg arg t = Some ? res →
     556        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
     557#ty *
     558[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
     559#sz #sg #arg #cmop
     560whd in match (translate_unop ???);
     561@(match typ_eq (ASTint sz sg) (typ_of_type ty)
     562  with
     563  [ inl H ⇒ ?
     564  | inr H ⇒ ? ])
     565normalize nodelta
     566[ 2: #Heq destruct ]
     567lapply H -H
     568lapply cmop -cmop
     569cases ty
     570[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
     571| #structname #fieldspec | #unionname #fieldspec | #id ]
     572normalize nodelta
     573#cmop normalize in match (typ_of_type ?); #H destruct
     574#H' normalize in H';
     575destruct (H')
     576#res
     577whd in match (sem_unary_operation ???);
     578cases arg
     579[ | #vsz #vi | | #vp
     580| | #vsz #vi | | #vp
     581| | #vsz #vi | | #vp
     582| | #vsz #vi | | #vp ]
     583whd in match (sem_neg ??);
     584#H destruct (H)
     585whd in match (eval_unop ????);
     586cases (eq_intsize sz' vsz) in H; normalize nodelta
     587#H destruct @refl
     588qed.
     589
     590
     591lemma translate_unop :
     592  ∀ty,sg,op,cmop.
     593  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
     594  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
     595            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
     596#ty #sg * #cmop #Htranslate #arg
     597[ @translate_notbool_to_cminor assumption
     598| @translate_notint_to_cminor assumption
     599| @translate_negint_to_cminor assumption ]
     600qed.
     601
     602lemma classify_add_inversion :
     603  ∀ty1,ty2.
     604    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
     605    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
     606    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
     607    (classify_add ty1 ty2 = add_default ty1 ty2).
     608#ty1 #ty2
     609cases (classify_add ty1 ty2)
     610[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
     611| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
     612| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
     613| #tya #tyb %2 @refl ]
     614qed.
     615
     616lemma typ_should_eq_inversion : ∀ty1,ty2,P,a,x. typ_should_eq ty1 ty2 P a = OK ? x → ty1 = ty2.
     617* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
     618[ 4: #P #a #x normalize #H destruct (H) @refl
     619| 3: cases sz cases sg #P #A #x normalize #H destruct
     620| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
     621cases sz cases sz2 cases sg cases sg2
     622#P #a #x #H normalize in H:(??%?); destruct (H)
     623try @refl
     624qed.
     625
     626lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
     627*
     628[ * * normalize @refl
     629| @refl ]
     630qed.
     631
     632lemma intsize_eq_elim_inversion :
     633  ∀A:Type[0].
     634  ∀sz1,sz2.
     635  ∀elt1,f,errmsg,res. 
     636  intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res →
     637  ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
     638#A * * #elt1 #f #errmsg #res normalize #H destruct (H)
     639%{(refl ??)} normalize nodelta >H @refl
     640qed.
    475641
    476642lemma eval_expr_sim :
     
    9541120  %{cm_val} @conj try @refl assumption
    9551121| 6:
     1122  #ty *
     1123  [ cases ty
     1124    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1125    | #structname #fieldspec | #unionname #fieldspec | #id ]
     1126    #e #Hind
     1127    whd in match (typeof ?);
     1128    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
     1129    #Htranslate
     1130    [ 3,4,5,8: destruct (Htranslate)
     1131    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
     1132         cases sz normalize nodelta
     1133         #e' #Hexpr_vars #Htranslate
     1134         [ 1, 2: destruct (Htranslate) ] ]
     1135    #cl_val #trace #Hyp_present #Hexec_expr
     1136    cases (bind_inversion ????? Htranslate) -Htranslate
     1137    #cmop * #Htranslate_unop #Hexec_arg
     1138    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
     1139    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1140    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1141    * #cl_arg #cl_trace * #Hexec_cl
     1142    whd in ⊢ ((???%) → ?); #Hexec_unop
     1143    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
     1144    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1145    lapply (opt_to_res_inversion ???? Hopt) -Hopt
     1146    #Hsem_cl whd in match (eval_expr ???????);
     1147    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
     1148    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
     1149    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
     1150    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
     1151    whd in match (typ_of_type Tvoid);
     1152    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
     1153    #H >H @refl
     1154  | *:
     1155    cases ty
     1156    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
     1157    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
     1158    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
     1159    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
     1160    whd in Htranslate:(??%?);
     1161    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
     1162    cases (bind_inversion ????? Htranslate) -Htranslate
     1163    #cmop * #Htranslate_unop #Hexec_arg
     1164    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
     1165    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1166    cases (bind_inversion ????? Hexec) -Hexec
     1167    * #cl_arg #cl_trace * #Hexec_cl
     1168    whd in ⊢ ((???%) → ?); #Hexec_unop
     1169    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
     1170    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1171    lapply (opt_to_res_inversion ???? Hopt) -Hopt
     1172    #Hcl_unop whd in match (eval_expr ???????);
     1173    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
     1174    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
     1175    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
     1176    * #op_res * #Hcl_sem #Hvalue_eq
     1177    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
     1178       %{op_res} @conj try @refl assumption
     1179    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
     1180       %{op_res} @conj try @refl assumption
     1181    ]
     1182  ]
     1183| 7: (* binary ops *)
     1184     #ty
     1185     letin s ≝ (typ_of_type ty)
     1186     #op #e1 #e2
     1187     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
     1188     cases (bind_inversion ????? Htranslate) -Htranslate
     1189     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
     1190     cases (bind_inversion ????? Htranslate) -Htranslate
     1191     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
     1192     whd in ⊢ ((??%?) → ?);
     1193     cases op whd in match (translate_binop ??????);
     1194     @cthulhu (* PITA *)
     1195| 8: #ty #ty' * #ed #ety
     1196  cases ety
     1197  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
     1198  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
     1199  whd in match (typeof ?); whd in match (typ_of_type ?);
     1200  #Hind whd in match (typeof ?);
     1201  #cm_expr #Hexpr_vars #Htranslate
     1202  cases (bind_inversion ????? Htranslate) -Htranslate
     1203  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
     1204  cases (bind_inversion ????? Htranslate) -Htranslate
     1205  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
     1206  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
     1207  cases (bind_inversion ????? Htranslate) -Htranslate
     1208  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
     1209  #Heq destruct (Heq)
     1210  #cl_val #trace #Hyp_present #Hexec_cm
     1211  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
     1212  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
     1213  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
     1214  #cast_val * #Hexec_cast
     1215  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1216  lapply (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) #Htype_eq
     1217  lapply Hexec_cast -Hexec_cast
     1218  lapply Htyp_should_eq -Htyp_should_eq
     1219  lapply Htranslate_cast -Htranslate_cast
     1220  lapply Hexpr_vars_cast -Hexpr_vars_cast
     1221  lapply cm_cast -cm_cast
     1222  lapply Hyp_present -Hyp_present
     1223  lapply Hexpr_vars -Hexpr_vars
     1224  lapply cm_expr -cm_expr
     1225  <Htype_eq -Htype_eq
     1226  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?); >typ_eq_refl normalize nodelta
     1227  cases ty'
     1228  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
     1229  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
     1230  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
     1231  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast
     1232  whd in match (typ_of_type ?) in cm_castee cm_expr Hexpr_vars_castee;
     1233  whd in match (typeof ?) in Htranslate_cast Hexec_cast;
     1234  #Heq destruct (Heq)
     1235  whd in Htranslate_cast:(??%%);
     1236  whd in Hexpr_vars;
     1237  destruct (Htranslate_cast)
     1238  [ 1,2,3,4,7:
     1239    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
     1240    * #cm_val' * #Heval_castee #Hvalue_eq #Hexec_cast
     1241    lapply Hvalue_eq -Hvalue_eq lapply Hexec_cm -Hexec_cm
     1242    whd in Hexec_cast:(??%%);
     1243    cases cm_val in Hexec_cast; normalize nodelta
     1244    [ | #vsz #vi | | #vp
     1245    | | #vsz #vi | | #vp
     1246    | | #vsz #vi | | #vp
     1247    | | #vsz #vi | | #vp
     1248    | | #vsz #vi | | #vp ]
     1249    [ 2,6,10,14,18:
     1250    | *: #Habsurd destruct (Habsurd) ]
     1251    #Hexec_cast #Hexec_cm #Hvalue_eq
     1252    [ 1,2,3:
     1253      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
     1254      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
     1255    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
     1256    [ 1,2,4,5:
     1257      cases (bind_inversion ????? Hexec_cast)
     1258      whd in match (typeof ?);
     1259      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
     1260      whd in match (eq_rect_r ??????);
     1261      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
     1262      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
     1263      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
     1264      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
     1265      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1266      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
     1267      >Heval_castee normalize nodelta whd in match (eval_unop ????);
     1268      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
     1269      >Heq_vi >eq_bv_true normalize
     1270      %{Vnull} @conj try @refl %3
     1271    | 3: destruct (Hcl_val_eq)
     1272          whd in match (eval_expr ???????);
     1273          >Heval_castee normalize nodelta
     1274          whd in match (eval_unop ????);
     1275          cases esg normalize nodelta
     1276          whd in match (opt_to_res ???); whd in match (m_bind ?????);
     1277          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
     1278          whd in match (eq_rect_r ??????);
     1279          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
     1280          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
     1281             this reason. *)
     1282          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
     1283          cases esz normalize nodelta
     1284          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
     1285          whd in match (sign_ext ??); whd in match (zero_ext ??);
     1286          %2
     1287    ]
     1288 | *:
     1289    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
     1290    * #cm_val' * #Heval_expr #Hvalue_eq #Hexec_cast >Heval_expr
     1291    %{cm_val'} @conj try @refl
     1292    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
     1293    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
     1294    cases cm_val
     1295    [ | #vsz #vi | | #vp
     1296    | | #vsz #vi | | #vp
     1297    | | #vsz #vi | | #vp
     1298    | | #vsz #vi | | #vp ]
     1299    #Hexec_cm #Hvalue_eq #Hexec_cast
     1300    whd in Hexec_cast:(??%%);
     1301    [ 1,5,9,13: destruct (Hexec_cast) ]
     1302    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
     1303    lapply Hexec_cast -Hexec_cast 
     1304    normalize cases (eq_v ?????) normalize
     1305    #Habsurd destruct (Habsurd)
     1306 ]     
     1307| 9: (* Econdition *) 
     1308  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
     1309  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
     1310  #Hexec_cm
     1311  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
     1312  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
     1313  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
     1314  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
     1315  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
     1316  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
     1317  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1318  cases (bind_inversion ????? Htranslate) -Htranslate
     1319  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
     1320  cases (bind_inversion ????? Htranslate) -Htranslate
     1321  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
     1322  cases (bind_inversion ????? Htranslate) -Htranslate
     1323  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
     1324  lapply (type_should_eq_inversion (typeof e2) ty … Htypecheck) -Htypecheck
     1325  *  #Htypeof_e2_eq_ty
     1326  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
     1327  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
     1328  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
     1329  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
     1330  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
     1331  cases (bind_inversion ????? Htranslate) -Htranslate
     1332  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
     1333  cases (bind_inversion ????? Htranslate) -Htranslate 
     1334  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
     1335  lapply (type_should_eq_inversion (typeof e3) ty … Htypecheck) -Htypecheck
     1336  * #Htypeof_e3_eq_ty
     1337  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
     1338  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
     1339  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
     1340  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
     1341  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
     1342  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
     1343  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
     1344  lapply Hexec_bool_of_val -Hexec_bool_of_val
     1345  cases (typeof e1) normalize nodelta
     1346  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
     1347  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
     1348  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
     1349  whd in Heq:(???%); destruct (Heq)
     1350  whd in match (eval_expr ???????);
     1351  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
     1352  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
     1353  >Heval_e1 normalize nodelta
     1354  lapply Hcm_ifthenelse -Hcm_ifthenelse
     1355  lapply Hexec_cond -Hexec_cond 
     1356  lapply Hexec_bool_of_val -Hexec_bool_of_val
     1357  lapply Hvalue_eq1 -Hvalue_eq1
     1358  cases cm_cond_val
     1359  [ | #vsz #vi | | #vp
     1360  | | #vsz #vi | | #vp
     1361  | | #vsz #vi | | #vp
     1362  | | #vsz #vi | | #vp ]
     1363  whd in ⊢ (? → (??%%) → ?);
     1364  [ 6:
     1365  | *: #_ #Habsurd destruct (Habsurd) ]
     1366  #Hvalue_eq1 #Hsz_check
     1367  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
     1368  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
     1369  #Heq destruct (Heq)
     1370  #Hexec_expr_e1
     1371  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
     1372    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
     1373    with
     1374    [ true ⇒ λHeq. ?
     1375    | false ⇒ λHeq. ?
     1376    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
     1377  normalize nodelta
     1378  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
     1379  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
     1380  >Heq normalize nodelta
     1381  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
     1382    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
     1383    normalize %{cm_val3} @conj try @refl assumption
     1384  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
     1385    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
     1386    normalize %{cm_val2} @conj try @refl assumption ]
     1387| 10: (* andbool *)
    9561388  #ty cases ty
    957   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1389  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 
    9581390  | #structname #fieldspec | #unionname #fieldspec | #id ]
    959   whd in match (typeof ?);
    960   #op #e #Hind
    961   whd in match (typeof ?); whd in match (typ_of_type ?); 
    962   #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
     1391  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
     1392  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
     1393  (* decompose first slice of clight execution *)
     1394  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1395  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
     1396  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1397  #b * #Hexec_bool_of_val #Hexec_expr
     1398  (* decompose translation to Cminor *)
     1399  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
     1400  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
    9631401  cases (bind_inversion ????? Htranslate) -Htranslate
    964   #op * #Htranslate_unop #Hexec_arg
    965   cases (bind_inversion ????? Hexec_arg) -Hexec_arg
    966   * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    967   cases (bind_inversion ????? Hexec) -Hexec
    968   * #cl_val #cl_trace * #Hexec_cl
    969   whd in ⊢ ((???%) → ?); #Hexec_unop
    970   cases (bind_inversion ????? Hexec_unop) -Hexec_unop
    971   #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    972   lapply (opt_to_res_inversion ???? Hopt) -Hopt
    973   #Hsem_cl whd in match (eval_expr ???????);
    974   cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
    975   #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
    976   lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
     1402  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
     1403  [ 2: | *: #Heq destruct (Heq) ]
     1404  (* discriminate I16 and I8 cases *)
     1405(*  lapply Hyp_present -Hyp_present
     1406  lapply Hexpr_vars -Hexpr_vars
     1407  lapply cm_expr -cm_expr cases sz
     1408  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
     1409  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
     1410  (* go on with decomposition *)
     1411  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
     1412  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
     1413  (* cleanup the type coercion *)
     1414  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
     1415  * #Htypeof_e2_eq_ty
     1416  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
     1417  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
     1418  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
     1419  lapply Hexpr_vars_e2 -Hexpr_vars_e2
     1420  lapply cm_expr_e2 -cm_expr_e2
     1421  lapply Hexec_expr -Hexec_expr
     1422  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
     1423  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
     1424  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
     1425  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
     1426   * to proceed in decomposing translation. *)
     1427  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
     1428  lapply Hexpr_vars_e1 -Hexpr_vars_e1
     1429  lapply cm_expr_e1 -cm_expr_e1
     1430  lapply Hexec_bool_of_val -Hexec_bool_of_val
     1431  cases (typeof e1)
     1432  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
     1433  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
     1434  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
     1435  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1436  (* translation decomposition terminated. Reduce goal *)
     1437  whd in match (eval_expr ???????);
     1438  (* We need Hind1.  *)
     1439  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
     1440  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
     1441  normalize nodelta
     1442  (* peform case analysis to further reduce the goal. *)
     1443  lapply Hvalue_eq -Hvalue_eq
     1444  lapply Hexec_bool_of_val -Hexec_bool_of_val
     1445  whd in match (proj2 ???);
     1446  cases cl_val_e1
     1447  [ | #vsz #vi | | #vp
     1448  | | #vsz #vi | | #vp
     1449  | | #vsz #vi | | #vp
     1450  | | #vsz #vi | | #vp ]
     1451  whd in ⊢ ((??%%) → ?);
     1452  [ 6:
     1453  | *: #Heq destruct (Heq) ]
     1454  #Hsz_check #Hvalue_eq
     1455  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
     1456  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
     1457  (* preparing case analysis on b *)
     1458  lapply Hexec_expr -Hexec_expr
     1459  cases b normalize nodelta
     1460  [ 2: (* early exit *)
     1461       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
     1462       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
     1463       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
     1464       <e0 whd in match (m_bind ?????);
     1465       @cthulhu
     1466       (* Pb: incompatible semantics for cl and cm.
     1467        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
     1468          first operand is false (for andbool)
     1469          . solution 1 : change semantics to return actual value instead of Vfalse
     1470          . solution 2 : change toCminor to introduce another test in the program,
     1471            returning Vfalse in case of failure instead of actual value
     1472        *) ]
     1473  #Hexec_expr #Heq_outcome
     1474  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1475  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
     1476  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
     1477  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
     1478  #Heq destruct (Heq)
     1479  >(value_eq_int_inversion … Hvalue_eq)
     1480  whd in match (eval_bool_of_val ?);
     1481  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
     1482  normalize nodelta
     1483  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
     1484  >Heval_expr normalize nodelta
     1485  %{cm_val_e2} @conj try @refl 
     1486  whd in Hexec_bool_outcome:(??%%);
     1487  normalize nodelta in Hexec_bool_outcome:(??%%);
     1488  lapply Hvalue_eq2 -Hvalue_eq2
     1489  -Heval_expr
     1490  lapply Hexec_bool_outcome -Hexec_bool_outcome
     1491  cases cl_val_e2
     1492  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
     1493  #Heq destruct (Heq)
     1494  cases (intsize_eq_elim_inversion ??????? Heq)
     1495  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
     1496  cases outcome_bool normalize nodelta
     1497  (* Problem. cf prev case. *)
    9771498  @cthulhu
    978 | *: @cthulhu
     1499| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
     1500| 12: (* sizeof *)
     1501  #ty cases ty
     1502  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1503  | #structname #fieldspec | #unionname #fieldspec | #id ]
     1504  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
     1505  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
     1506  normalize in match (typ_of_type ?);
     1507  whd in Htranslate:(??%?); destruct (Htranslate)
     1508  whd in match (eval_expr ???????);
     1509  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
     1510| 13:
     1511  #ty #ed #ty' cases ty'
     1512  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1513  | #structname #fieldspec | #unionname #fieldspec | #id ]
     1514  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
     1515  #Hexec_lvalue
     1516  whd in Hexec_lvalue:(??%?); destruct
     1517  [ whd in Htranslate_addr:(??%?);
     1518    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
     1519    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
     1520    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
     1521    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
     1522    #Heq destruct (Heq)
     1523    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
     1524  ]
     1525  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
     1526  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
     1527  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
     1528       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
     1529       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
     1530       #cm_val_field * #Heval_cm #Hvalue_eq
     1531       whd in match (eval_expr ???????);
     1532       >Heval_cm normalize nodelta
     1533       whd in match (eval_expr ???????); whd in match (m_bind ?????);
     1534       whd in match (eval_binop ???????); normalize nodelta
     1535       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
     1536       normalize nodelta #Hptr_translate
     1537       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
     1538       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
     1539       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
     1540       cases (E cl_blo) in Hptr_translate; normalize nodelta
     1541       [ #H destruct (H) ]
     1542       * #BL #OFF normalize nodelta #Heq destruct (Heq)
     1543       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
     1544       #H destruct (H)
     1545       (* again, mismatch in the size of the integers *)
     1546       @cthulhu
     1547  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
     1548       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
     1549       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
     1550       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
     1551       #Hpointer_translation
     1552       %{cm_val} @conj try assumption
     1553       destruct @refl
     1554   ]
     1555| 14: (* cost label *)
     1556  #ty (* cases ty
     1557  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1558  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
     1559  #l * #ed #ety
     1560  whd in match (typeof ?); whd in match (typeof ?);
     1561  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
     1562  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
     1563  #Hexpr_vars * #Htranslate_ind #Htranslate
     1564  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
     1565  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
     1566  whd in match (typeof ?) in Htyp_should_eq:(??%?);
     1567  lapply (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
     1568  #Htyp_eq
     1569  lapply Htyp_should_eq -Htyp_should_eq
     1570  lapply Htranslate_ind -Htranslate_ind
     1571  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
     1572  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
     1573  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
     1574  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
     1575  <(Htyp_eq)
     1576  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
     1577  #Htranslate_ind
     1578  whd in ⊢ ((??%?) → ?); >typ_eq_refl normalize nodelta
     1579  whd in ⊢ ((??%%) → ?); #H destruct (H) whd in match (eval_expr ???????);
     1580  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
     1581  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1582  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
     1583  #cm_val' * #Heval_expr' #Hvalue_eq
     1584  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
     1585  (* Inconsistency in clight and cminor executable semantics for expressions~:
     1586     placement of the label is either before or after current trace.
     1587     To be resolved.
     1588   *)
     1589  @cthulhu
     1590| 15: *
     1591  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
     1592  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     1593  #ty normalize in ⊢ (% → ?);
     1594  [ 2,3,12: @False_ind
     1595  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
     1596           normalize #Habsurd destruct (Habsurd) ]
    9791597] qed.
    980 
    981 
    982 
    9831598
    9841599
Note: See TracChangeset for help on using the changeset viewer.