Changeset 2554 for src/Clight/toCminorCorrectness.ma

Timestamp:

Dec 13, 2012, 5:22:51 PM (8 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.

File:

• src/Clight/toCminorCorrectness.ma (modified) (2 diffs)

src/Clight/toCminorCorrectness.ma

@@ -471 +471 @@
 qed.
 
-(* TODO convert Clight unary ops to front-end ops ops, then prove correspondence for operators (with equal values). *)
-
+lemma typ_eq_elim :
+  ∀t1,t2.
+  ∀(P: (t1=t2)+(t1≠t2) → Prop).
+  (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
+#t1 #t2 #P #Hl #Hr
+@(match typ_eq t1 t2
+  with
+  [ inl H ⇒ Hl H
+  | inr H ⇒ Hr H ])
+qed.
+
+
+lemma translate_notbool_to_cminor :
+  ∀t,sg,arg.
+  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
+  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
+        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
+*
+[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
+| #structname #fieldspec | #unionname #fieldspec | #id ]
+normalize in match (typ_of_type ?);
+#sg #arg #cmop
+whd in ⊢ (??%% → ?); #Heq destruct (Heq)
+cases arg
+[ | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp ]
+#res
+whd in ⊢ ((??%?) → ?);
+#Heq
+[ 6,11,12: | *: destruct (Heq) ]
+[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
+| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
+     #H normalize nodelta #Heq destruct
+     whd in match (eval_unop ????);
+     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
+] qed.
+
+lemma translate_notint_to_cminor :
+  ∀t,t',arg.
+  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
+  ∀res. sem_unary_operation Onotint arg t = Some ? res →
+        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
+#ty *
+[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
+#sz #sg #arg #cmop
+whd in match (translate_unop ???);
+@(match typ_eq (ASTint sz sg) (typ_of_type ty)
+  with
+  [ inl H ⇒ ?
+  | inr H ⇒ ? ])
+normalize nodelta
+[ 2: #Heq destruct ]
+lapply H -H
+lapply cmop -cmop
+cases ty
+[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
+| #structname #fieldspec | #unionname #fieldspec | #id ]
+normalize nodelta
+#cmop normalize in match (typ_of_type ?); #H destruct
+#H' normalize in H';
+destruct (H')
+#res
+whd in match (sem_unary_operation ???);
+cases arg
+[ | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp ]
+whd in match (sem_notint ?);
+#H destruct (H) @refl
+qed.
+
+
+lemma translate_negint_to_cminor :
+  ∀t,t',arg.
+  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
+  ∀res. sem_unary_operation Oneg arg t = Some ? res →
+        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
+#ty *
+[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
+#sz #sg #arg #cmop
+whd in match (translate_unop ???);
+@(match typ_eq (ASTint sz sg) (typ_of_type ty)
+  with
+  [ inl H ⇒ ?
+  | inr H ⇒ ? ])
+normalize nodelta
+[ 2: #Heq destruct ]
+lapply H -H
+lapply cmop -cmop
+cases ty
+[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
+| #structname #fieldspec | #unionname #fieldspec | #id ]
+normalize nodelta
+#cmop normalize in match (typ_of_type ?); #H destruct
+#H' normalize in H';
+destruct (H')
+#res
+whd in match (sem_unary_operation ???);
+cases arg
+[ | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp
+| | #vsz #vi | | #vp ]
+whd in match (sem_neg ??);
+#H destruct (H)
+whd in match (eval_unop ????);
+cases (eq_intsize sz' vsz) in H; normalize nodelta
+#H destruct @refl
+qed.
+
+
+lemma translate_unop :
+  ∀ty,sg,op,cmop.
+  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
+  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
+            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
+#ty #sg * #cmop #Htranslate #arg
+[ @translate_notbool_to_cminor assumption
+| @translate_notint_to_cminor assumption
+| @translate_negint_to_cminor assumption ]
+qed.
+
+lemma classify_add_inversion :
+  ∀ty1,ty2. 
+    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
+    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
+    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
+    (classify_add ty1 ty2 = add_default ty1 ty2).
+#ty1 #ty2
+cases (classify_add ty1 ty2)
+[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
+| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
+| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
+| #tya #tyb %2 @refl ]
+qed.
+
+lemma typ_should_eq_inversion : ∀ty1,ty2,P,a,x. typ_should_eq ty1 ty2 P a = OK ? x → ty1 = ty2.
+* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
+[ 4: #P #a #x normalize #H destruct (H) @refl
+| 3: cases sz cases sg #P #A #x normalize #H destruct
+| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ] 
+cases sz cases sz2 cases sg cases sg2
+#P #a #x #H normalize in H:(??%?); destruct (H)
+try @refl
+qed.
+
+lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
+* 
+[ * * normalize @refl
+| @refl ]
+qed. 
+
+lemma intsize_eq_elim_inversion :
+  ∀A:Type[0].
+  ∀sz1,sz2.
+  ∀elt1,f,errmsg,res.  
+  intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res → 
+  ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
+#A * * #elt1 #f #errmsg #res normalize #H destruct (H)
+%{(refl ??)} normalize nodelta >H @refl
+qed.
 
 lemma eval_expr_sim :
@@ -954 +1120 @@
   %{cm_val} @conj try @refl assumption
 | 6:
+  #ty *
+  [ cases ty
+    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 
+    | #structname #fieldspec | #unionname #fieldspec | #id ]
+    #e #Hind
+    whd in match (typeof ?);
+    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
+    #Htranslate
+    [ 3,4,5,8: destruct (Htranslate)
+    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
+         cases sz normalize nodelta
+         #e' #Hexpr_vars #Htranslate
+         [ 1, 2: destruct (Htranslate) ] ]
+    #cl_val #trace #Hyp_present #Hexec_expr
+    cases (bind_inversion ????? Htranslate) -Htranslate
+    #cmop * #Htranslate_unop #Hexec_arg
+    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
+    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
+    * #cl_arg #cl_trace * #Hexec_cl
+    whd in ⊢ ((???%) → ?); #Hexec_unop
+    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
+    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+    lapply (opt_to_res_inversion ???? Hopt) -Hopt
+    #Hsem_cl whd in match (eval_expr ???????);
+    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
+    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
+    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
+    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
+    whd in match (typ_of_type Tvoid);
+    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
+    #H >H @refl
+  | *:
+    cases ty
+    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
+    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
+    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?);  
+    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
+    whd in Htranslate:(??%?);
+    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
+    cases (bind_inversion ????? Htranslate) -Htranslate
+    #cmop * #Htranslate_unop #Hexec_arg
+    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
+    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+    cases (bind_inversion ????? Hexec) -Hexec
+    * #cl_arg #cl_trace * #Hexec_cl
+    whd in ⊢ ((???%) → ?); #Hexec_unop
+    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
+    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+    lapply (opt_to_res_inversion ???? Hopt) -Hopt
+    #Hcl_unop whd in match (eval_expr ???????);
+    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
+    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
+    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
+    * #op_res * #Hcl_sem #Hvalue_eq
+    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
+       %{op_res} @conj try @refl assumption
+    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
+       %{op_res} @conj try @refl assumption
+    ]
+  ]
+| 7: (* binary ops *)
+     #ty
+     letin s ≝ (typ_of_type ty)
+     #op #e1 #e2
+     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
+     cases (bind_inversion ????? Htranslate) -Htranslate
+     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
+     cases (bind_inversion ????? Htranslate) -Htranslate
+     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
+     whd in ⊢ ((??%?) → ?);
+     cases op whd in match (translate_binop ??????);
+     @cthulhu (* PITA *)
+| 8: #ty #ty' * #ed #ety
+  cases ety
+  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain 
+  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
+  whd in match (typeof ?); whd in match (typ_of_type ?);
+  #Hind whd in match (typeof ?);
+  #cm_expr #Hexpr_vars #Htranslate
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate  
+  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
+  #Heq destruct (Heq)
+  #cl_val #trace #Hyp_present #Hexec_cm
+  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
+  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
+  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
+  #cast_val * #Hexec_cast
+  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
+  lapply (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) #Htype_eq
+  lapply Hexec_cast -Hexec_cast
+  lapply Htyp_should_eq -Htyp_should_eq
+  lapply Htranslate_cast -Htranslate_cast
+  lapply Hexpr_vars_cast -Hexpr_vars_cast
+  lapply cm_cast -cm_cast
+  lapply Hyp_present -Hyp_present
+  lapply Hexpr_vars -Hexpr_vars
+  lapply cm_expr -cm_expr
+  <Htype_eq -Htype_eq
+  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?); >typ_eq_refl normalize nodelta
+  cases ty'
+  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
+  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
+  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
+  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast
+  whd in match (typ_of_type ?) in cm_castee cm_expr Hexpr_vars_castee;
+  whd in match (typeof ?) in Htranslate_cast Hexec_cast;
+  #Heq destruct (Heq)
+  whd in Htranslate_cast:(??%%);
+  whd in Hexpr_vars;
+  destruct (Htranslate_cast)
+  [ 1,2,3,4,7:
+    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
+    * #cm_val' * #Heval_castee #Hvalue_eq #Hexec_cast
+    lapply Hvalue_eq -Hvalue_eq lapply Hexec_cm -Hexec_cm
+    whd in Hexec_cast:(??%%);
+    cases cm_val in Hexec_cast; normalize nodelta
+    [ | #vsz #vi | | #vp 
+    | | #vsz #vi | | #vp
+    | | #vsz #vi | | #vp
+    | | #vsz #vi | | #vp
+    | | #vsz #vi | | #vp ]
+    [ 2,6,10,14,18:
+    | *: #Habsurd destruct (Habsurd) ]
+    #Hexec_cast #Hexec_cm #Hvalue_eq
+    [ 1,2,3:
+      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
+      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
+    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
+    [ 1,2,4,5:
+      cases (bind_inversion ????? Hexec_cast)
+      whd in match (typeof ?);
+      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
+      whd in match (eq_rect_r ??????);
+      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
+      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
+      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
+      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
+      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
+      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
+      >Heval_castee normalize nodelta whd in match (eval_unop ????);
+      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
+      >Heq_vi >eq_bv_true normalize
+      %{Vnull} @conj try @refl %3
+    | 3: destruct (Hcl_val_eq)
+          whd in match (eval_expr ???????);
+          >Heval_castee normalize nodelta
+          whd in match (eval_unop ????);
+          cases esg normalize nodelta
+          whd in match (opt_to_res ???); whd in match (m_bind ?????);
+          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
+          whd in match (eq_rect_r ??????);
+          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
+          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
+             this reason. *)
+          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
+          cases esz normalize nodelta
+          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
+          whd in match (sign_ext ??); whd in match (zero_ext ??);
+          %2
+    ]
+ | *:
+    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
+    * #cm_val' * #Heval_expr #Hvalue_eq #Hexec_cast >Heval_expr
+    %{cm_val'} @conj try @refl
+    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq 
+    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
+    cases cm_val
+    [ | #vsz #vi | | #vp 
+    | | #vsz #vi | | #vp
+    | | #vsz #vi | | #vp
+    | | #vsz #vi | | #vp ]
+    #Hexec_cm #Hvalue_eq #Hexec_cast
+    whd in Hexec_cast:(??%%);
+    [ 1,5,9,13: destruct (Hexec_cast) ]
+    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
+    lapply Hexec_cast -Hexec_cast  
+    normalize cases (eq_v ?????) normalize
+    #Habsurd destruct (Habsurd)
+ ]     
+| 9: (* Econdition *)  
+  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?); 
+  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
+  #Hexec_cm
+  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
+  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
+  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
+  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
+  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
+  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
+  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
+  lapply (type_should_eq_inversion (typeof e2) ty … Htypecheck) -Htypecheck
+  *  #Htypeof_e2_eq_ty
+  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
+  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
+  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2  
+  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
+  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate  
+  cases (bind_inversion ????? Htranslate) -Htranslate  
+  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
+  lapply (type_should_eq_inversion (typeof e3) ty … Htypecheck) -Htypecheck
+  * #Htypeof_e3_eq_ty
+  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
+  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
+  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
+  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
+  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
+  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1  
+  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
+  lapply Hexec_bool_of_val -Hexec_bool_of_val
+  cases (typeof e1) normalize nodelta
+  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain 
+  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
+  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
+  whd in Heq:(???%); destruct (Heq)
+  whd in match (eval_expr ???????);
+  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
+  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
+  >Heval_e1 normalize nodelta
+  lapply Hcm_ifthenelse -Hcm_ifthenelse
+  lapply Hexec_cond -Hexec_cond  
+  lapply Hexec_bool_of_val -Hexec_bool_of_val
+  lapply Hvalue_eq1 -Hvalue_eq1
+  cases cm_cond_val
+  [ | #vsz #vi | | #vp 
+  | | #vsz #vi | | #vp
+  | | #vsz #vi | | #vp
+  | | #vsz #vi | | #vp ]
+  whd in ⊢ (? → (??%%) → ?);
+  [ 6:
+  | *: #_ #Habsurd destruct (Habsurd) ]
+  #Hvalue_eq1 #Hsz_check
+  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
+  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
+  #Heq destruct (Heq)
+  #Hexec_expr_e1
+  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) 
+    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
+    with
+    [ true ⇒ λHeq. ?
+    | false ⇒ λHeq. ?
+    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
+  normalize nodelta
+  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
+  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
+  >Heq normalize nodelta
+  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
+    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
+    normalize %{cm_val3} @conj try @refl assumption
+  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
+    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
+    normalize %{cm_val2} @conj try @refl assumption ]
+| 10: (* andbool *)
   #ty cases ty
-  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
+  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 
   | #structname #fieldspec | #unionname #fieldspec | #id ]
-  whd in match (typeof ?);
-  #op #e #Hind
-  whd in match (typeof ?); whd in match (typ_of_type ?);  
-  #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
+  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
+  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
+  (* decompose first slice of clight execution *)
+  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
+  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
+  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
+  #b * #Hexec_bool_of_val #Hexec_expr
+  (* decompose translation to Cminor *)
+  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
+  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
   cases (bind_inversion ????? Htranslate) -Htranslate
-  #op * #Htranslate_unop #Hexec_arg
-  cases (bind_inversion ????? Hexec_arg) -Hexec_arg
-  * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
-  cases (bind_inversion ????? Hexec) -Hexec
-  * #cl_val #cl_trace * #Hexec_cl
-  whd in ⊢ ((???%) → ?); #Hexec_unop
-  cases (bind_inversion ????? Hexec_unop) -Hexec_unop
-  #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
-  lapply (opt_to_res_inversion ???? Hopt) -Hopt
-  #Hsem_cl whd in match (eval_expr ???????);
-  cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
-  #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
-  lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
+  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
+  [ 2: | *: #Heq destruct (Heq) ]
+  (* discriminate I16 and I8 cases *)
+(*  lapply Hyp_present -Hyp_present
+  lapply Hexpr_vars -Hexpr_vars
+  lapply cm_expr -cm_expr cases sz
+  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
+  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
+  (* go on with decomposition *)
+  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
+  (* cleanup the type coercion *)
+  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
+  * #Htypeof_e2_eq_ty
+  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
+  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
+  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
+  lapply Hexpr_vars_e2 -Hexpr_vars_e2
+  lapply cm_expr_e2 -cm_expr_e2
+  lapply Hexec_expr -Hexec_expr
+  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
+  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
+  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
+  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
+   * to proceed in decomposing translation. *)
+  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
+  lapply Hexpr_vars_e1 -Hexpr_vars_e1
+  lapply cm_expr_e1 -cm_expr_e1
+  lapply Hexec_bool_of_val -Hexec_bool_of_val
+  cases (typeof e1)
+  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
+  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
+  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
+  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
+  (* translation decomposition terminated. Reduce goal *)
+  whd in match (eval_expr ???????);
+  (* We need Hind1.  *)
+  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
+  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
+  normalize nodelta
+  (* peform case analysis to further reduce the goal. *)
+  lapply Hvalue_eq -Hvalue_eq
+  lapply Hexec_bool_of_val -Hexec_bool_of_val
+  whd in match (proj2 ???);
+  cases cl_val_e1
+  [ | #vsz #vi | | #vp 
+  | | #vsz #vi | | #vp
+  | | #vsz #vi | | #vp
+  | | #vsz #vi | | #vp ]
+  whd in ⊢ ((??%%) → ?);
+  [ 6:
+  | *: #Heq destruct (Heq) ]
+  #Hsz_check #Hvalue_eq
+  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
+  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
+  (* preparing case analysis on b *)
+  lapply Hexec_expr -Hexec_expr
+  cases b normalize nodelta
+  [ 2: (* early exit *)
+       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
+       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
+       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
+       <e0 whd in match (m_bind ?????);
+       @cthulhu
+       (* Pb: incompatible semantics for cl and cm.
+        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
+          first operand is false (for andbool)
+          . solution 1 : change semantics to return actual value instead of Vfalse
+          . solution 2 : change toCminor to introduce another test in the program,
+            returning Vfalse in case of failure instead of actual value
+        *) ]
+  #Hexec_expr #Heq_outcome
+  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
+  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
+  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
+  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
+  #Heq destruct (Heq)
+  >(value_eq_int_inversion … Hvalue_eq)
+  whd in match (eval_bool_of_val ?);
+  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
+  normalize nodelta
+  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
+  >Heval_expr normalize nodelta
+  %{cm_val_e2} @conj try @refl  
+  whd in Hexec_bool_outcome:(??%%);
+  normalize nodelta in Hexec_bool_outcome:(??%%);
+  lapply Hvalue_eq2 -Hvalue_eq2
+  -Heval_expr
+  lapply Hexec_bool_outcome -Hexec_bool_outcome
+  cases cl_val_e2
+  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
+  #Heq destruct (Heq)
+  cases (intsize_eq_elim_inversion ??????? Heq)
+  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
+  cases outcome_bool normalize nodelta
+  (* Problem. cf prev case. *)
   @cthulhu
-| *: @cthulhu
+| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
+| 12: (* sizeof *)
+  #ty cases ty
+  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 
+  | #structname #fieldspec | #unionname #fieldspec | #id ]
+  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
+  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
+  normalize in match (typ_of_type ?);
+  whd in Htranslate:(??%?); destruct (Htranslate)
+  whd in match (eval_expr ???????);
+  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
+| 13: 
+  #ty #ed #ty' cases ty'
+  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 
+  | #structname #fieldspec | #unionname #fieldspec | #id ]
+  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
+  #Hexec_lvalue
+  whd in Hexec_lvalue:(??%?); destruct
+  [ whd in Htranslate_addr:(??%?);
+    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
+    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
+    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
+    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
+    #Heq destruct (Heq)
+    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
+  ]
+  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
+  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue    
+  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
+       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
+       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
+       #cm_val_field * #Heval_cm #Hvalue_eq
+       whd in match (eval_expr ???????); 
+       >Heval_cm normalize nodelta
+       whd in match (eval_expr ???????); whd in match (m_bind ?????);
+       whd in match (eval_binop ???????); normalize nodelta
+       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
+       normalize nodelta #Hptr_translate
+       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
+       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
+       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
+       cases (E cl_blo) in Hptr_translate; normalize nodelta
+       [ #H destruct (H) ]
+       * #BL #OFF normalize nodelta #Heq destruct (Heq)
+       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
+       #H destruct (H)
+       (* again, mismatch in the size of the integers *)
+       @cthulhu
+  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
+       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
+       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
+       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
+       #Hpointer_translation
+       %{cm_val} @conj try assumption
+       destruct @refl
+   ]
+| 14: (* cost label *)
+  #ty (* cases ty
+  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain 
+  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
+  #l * #ed #ety
+  whd in match (typeof ?); whd in match (typeof ?);
+  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
+  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
+  #Hexpr_vars * #Htranslate_ind #Htranslate
+  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
+  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
+  whd in match (typeof ?) in Htyp_should_eq:(??%?);
+  lapply (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
+  #Htyp_eq
+  lapply Htyp_should_eq -Htyp_should_eq
+  lapply Htranslate_ind -Htranslate_ind
+  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
+  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
+  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
+  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
+  <(Htyp_eq)
+  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
+  #Htranslate_ind
+  whd in ⊢ ((??%?) → ?); >typ_eq_refl normalize nodelta
+  whd in ⊢ ((??%%) → ?); #H destruct (H) whd in match (eval_expr ???????);
+  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
+  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
+  #cm_val' * #Heval_expr' #Hvalue_eq
+  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
+  (* Inconsistency in clight and cminor executable semantics for expressions~:
+     placement of the label is either before or after current trace. 
+     To be resolved.
+   *)
+  @cthulhu
+| 15: *
+  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
+  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
+  #ty normalize in ⊢ (% → ?);
+  [ 2,3,12: @False_ind
+  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
+           normalize #Habsurd destruct (Habsurd) ]
 ] qed.
-
-
-