Changeset 2545

Timestamp:

Dec 7, 2012, 6:39:15 PM (8 years ago)

Author:

garnier

Message:

Comitting current progress of CL to CM

File:

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

src/Clight/toCminorCorrectness.ma

@@ -422 +422 @@
 
 lemma variable_not_in_env_but_in_vartypes_is_global :
-  ∀env,env',f,vars,stacksize,globals,var_id,allocty,ty.
+  ∀env,env',f,vars,stacksize,globals,var_id.
   (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
   characterise_vars globals f =〈vars,stacksize〉 →
   lookup ?? env' var_id = None ? →        
-  lookup' vars var_id = OK ? 〈allocty, ty〉 →
+  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
   ∃r.allocty = Global r.
-#env #env' #f #vars #stacksize #globals #var_id #allocty #ty #Hexec_alloc
-#Hcharacterise #Hlookup_fail #Hlookup_type_ok
+#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
+#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
 lapply (characterise_vars_src … Hcharacterise var_id ?)
 [ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
@@ -471 +471 @@
 qed.
 
+(* TODO convert Clight unary ops to front-end ops ops, then prove correspondence for operators (with equal values). *)
+
 
 lemma eval_expr_sim :
@@ -486 +488 @@
   ∀E:embedding.
   ∀minj:memory_inj E cl_m cm_m.
-  memory_matching E cl_m cm_m cl_env cm_env inv sp vars → 
+  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
+  (* clight expr to cminor expr *)
   (∀(e:expr).
-   ∀(e':CMexpr (typ_of_type (typeof e))). 
+   ∀(e':CMexpr (typ_of_type (typeof e))).
    ∀Hexpr_vars.
    translate_expr vars e = OK ? («e', Hexpr_vars») →
@@ -495 +498 @@
    ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
             value_eq E cl_val cm_val) ∧
+   (* clight /lvalue/ to cminor /expr/ *)
   (∀ed,ty.
-   ∀(e':CMexpr (typ_of_type ty)). 
+   ∀(e':CMexpr ASTptr).
    ∀Hexpr_vars.
-   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
+   translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
    ∀cl_blo,cl_off,trace,Hyp_present.
    exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
-   match E cl_blo with
-   [ Some loc ⇒
-     let 〈cm_blo, delta〉 ≝ loc in
-     match access_mode ty with
-     [ By_value t ⇒
-        (∃cm_val. loadv t cm_m (Vptr (mk_pointer cm_blo (offset_plus cl_off delta))) = Some ? cm_val ∧
-                  eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉)
-     | By_reference ⇒ 
-        eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m 
-          = OK ? 〈trace, Vptr (mk_pointer cm_blo (offset_plus cl_off delta))〉              
-     | By_nothing _ ⇒ True ]
-   | None ⇒ False ]).
-#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env
-#sp #cm_m #E #Hinj #Hlocal_matching
+   ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
+            value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
+#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
 @expr_lvalue_ind_combined
 [ 1: (* Integer constant *)
   #csz #ty cases ty
   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
-  | #structname #fieldspec | #unionname #fieldspec | #id ]  
+  | #structname #fieldspec | #unionname #fieldspec | #id ]
   #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
   #val #trace #Hpresent #Hexec_cl
@@ -564 +557 @@
             * #var_id_alloctype * #var_id_type * #Heq
             cases (variable_not_in_env_but_in_vartypes_is_global … 
-                        Hexec_alloc Hcharacterise Hcl_lookup Heq)
+                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
             #r #Heq' destruct (Heq') normalize nodelta
             lapply Hcl_load_success -Hcl_load_success
@@ -699 +692 @@
                  (* seems ok *)
             ]
-       ]       
-  | 2: whd in match (typeof ?) in Hind;
-       lapply (Hind cm_expr Hexpr_vars Htranslate_expr cl_b cl_o cl_t Hyp_present) -Hind
-       cases (bind_inversion ????? Hcl_success) -Hcl_success * #cl_subexpr_val #cl_trace *
-       #Hexec_expr
-       @(match cl_subexpr_val 
-         return λx. cl_subexpr_val = x → ?
-         with
-         [ Vundef ⇒ λHval_eq. ?
-         | Vint sz' i ⇒ λHval_eq. ?
-         | Vnull ⇒ λHval_eq. ?
-         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
+       ]
+  | 2: lapply Hcl_success -Hcl_success
+       lapply Htranslate_expr -Htranslate_expr
+       lapply Hind -Hind cases ty1
+       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
+       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
+       #Hind #Htranslate_expr #Hexec_cl
+       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
+       * whd in match (typ_of_type ?); normalize nodelta
+       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
        whd in ⊢ ((???%) → ?);
-       [ 1,2,3: #Habsurd destruct ] #Heq destruct (Heq) destruct (Hptr_eq)
-       whd in match (exec_lvalue' ?????) in Hind; #Hind
-       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val
-       * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 
-       lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hload_success
-       whd in Hexec_expr:(???%); whd in match (exec_lvalue' ?????) in Hind;
-       lapply Hind -Hind >Hexec_expr normalize nodelta
+       [ 1,2,6,7: #Heq destruct (Heq) ]
+       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
+       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
+       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
+       [ 1,3,5,7: @cthulhu ]
+       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
+       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
+       #Hexec_cl_ind #Hcl_ptr
+       cut (∃ptr. cl_ptr = Vptr ptr)
+       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
+                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
+       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
+       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
        #Hind lapply (Hind (refl ??)) -Hind
-       @(match E (pblock p) 
-         return λx. (E (pblock p) = x) → ?
-         with
-         [ None ⇒ λHembed. ?
-         | Some loc ⇒ λHembed. ? ] (refl ? (E (pblock p))))
-       normalize nodelta
-       [ 1: @False_ind ] 
-       cases loc in Hembed; normalize nodelta
-       lapply Hload_success -Hload_success
-       lapply Hexec_expr -Hexec_expr
+       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
+       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
+       destruct (Hcm_ptr) #Hpointer_translation
+       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
+       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
+       -Hopt_to_res
        lapply Hyp_present -Hyp_present
-       lapply Htranslate_expr -Htranslate_expr
        lapply Hexpr_vars -Hexpr_vars
        lapply cm_expr -cm_expr
-       cases ty
-       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
-       | #structname #fieldspec | #unionname #fieldspec | #id ]
-       normalize nodelta
-       #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_expr
-       #Hload_success #BL #OFF #Hembed
-       [ 1,6,7: normalize in Hload_success; #_ destruct
-       | 4,5: whd in match (typ_of_type ?); #Heval >Heval
-              %{(Vptr (mk_pointer BL (offset_plus (poff p) OFF)))}
-              @conj try @refl
-              lapply (load_value_of_type_by_ref … Hload_success ??) try //
-              #Heq >Heq %4 whd in ⊢ (??%%); >Hembed @refl
-       | *: * #cm_val * #Hloadv #Heval_expr >Heval_expr
-              lapply (mi_inj … Hinj … (pblock p) (poff p) BL (offset_plus (poff p) OFF) … Hload_success)
-              [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
-              | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
-              * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
-              %{cm_val'} @conj try assumption
-              whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
-              #Heq destruct @refl ]
+       inversion (access_mode ty)
+       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
+       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
+       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
+       #Heq destruct (Heq)
+       [ 1,2,3,4: (* By_value *)
+           (* project Hcl_load_success in Cminor through memory_inj *)
+           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
+           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
+           * #cm_val * #Hcm_load_success #Hvalue_eq
+           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
+           #Hloadv_cm 
+           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
+           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
+      | *: (* By reference *)
+           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
+           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
+           #Hval >Hval %4 assumption ]
   | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
        lapply (refl ? (typeof e1))
        cases (typeof e1) in ⊢ ((???%) → %);
-       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
-       | #structname #fieldspec | #unionname #fieldspec | #id ]
+       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
+       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
        #Heq_typeof normalize nodelta
-       [ 1,2,3,4,5,8: #Habsurd destruct ]
-       #Hexec_compound_clight
-       lapply (Hind … Htranslate_expr) -Hind -Htranslate_expr
-       cases (bind_inversion ????? Hexec_compound_clight) -Hexec_compound_clight
-       * * #CLB #CLO #CLTR
-       * #Hexec_lvalue #Hfield_offset whd in match (exec_lvalue' ?????);
-       >Hexec_lvalue normalize nodelta >Heq_typeof normalize nodelta
-       whd in match (m_bind ?????);
-       [ 2: normalize in Hfield_offset; destruct (Hfield_offset)
-            #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind
-            @(match E cl_b
-            return λx. (E cl_b = x) → ?
-            with
-            [ None ⇒ λHembed. ?
-            | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) normalize nodelta
-            [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta
-            lapply Hyp_present -Hyp_present
-            lapply Hexpr_vars -Hexpr_vars
-            lapply cm_expr -cm_expr
-            cases ty normalize nodelta
-            [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
-            | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
-            #cm_expr #Hexpr_vars #Hyp_present
-            [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void)
-                   #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res)
-                   normalize in ⊢ (% → ?); #Habsurd destruct                   
-            | 4,5: whd in match (typ_of_type ?); #Heval >Heval
-                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
-                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?);                   
-                   lapply (opt_to_res_inversion ???? Hopt_to_res)
-                   #Hload_success #Heq destruct (Heq)
-                   lapply (load_value_of_type_by_ref … Hload_success ??) try //
-                   #Hval_eq >Hval_eq                   
-                   %{(Vptr (mk_pointer BLO (offset_plus cl_o OFF)))}
-                   @conj try @refl
-                   %4 whd in ⊢ (??%%); >Hembed @refl
-            | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr
-                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
-                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
-                   lapply (opt_to_res_inversion ???? Hopt_to_res)
-                   #Hload_success
-                   lapply (mi_inj … Hinj … cl_b cl_o BLO (offset_plus cl_o OFF) … Hload_success)
-                   [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
-                   | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
-                   * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
-                   %{cm_val'} @conj try assumption
-                   whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
-                   #Heq destruct (Heq) @refl ]
-       | 1: cases (bind_inversion ????? Hfield_offset) -Hfield_offset #field_offset * #Hfield_offset_eq
-            #Heq whd in Heq:(???%); destruct (Heq) >Hfield_offset_eq normalize nodelta
-            #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind
-            @(match E cl_b
-            return λx. (E cl_b = x) → ?
-            with
-            [ None ⇒ λHembed. ?
-            | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b)))
-            normalize nodelta
-            [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta
-            lapply Hyp_present -Hyp_present
-            lapply Hexpr_vars -Hexpr_vars
-            lapply cm_expr -cm_expr
-            cases ty normalize nodelta
-            [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
-            | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]            
-            #cm_expr #Hexpr_vars #Hyp_present
-            [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void)
-                   #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res)
-                   normalize in ⊢ (% → ?); #Habsurd destruct
-            | 4,5: whd in match (typ_of_type ?); #Heval >Heval
-                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) -Hload_success_hyp
-                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?);                   
-                   lapply (opt_to_res_inversion ???? Hopt_to_res)
-                   #Hload_success #Heq destruct (Heq)
-                   lapply (load_value_of_type_by_ref … Hload_success ??) try //
-                   #Hval_eq >Hval_eq                   
-                   %{(Vptr (mk_pointer BLO (offset_plus (shift_offset (bitsize_of_intsize I32) CLO (repr I32 field_offset)) OFF)))}
-                   @conj try @refl
-                   %4 whd in ⊢ (??%%); >Hembed @refl
-            | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr
-                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
-                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
-                   lapply (opt_to_res_inversion ???? Hopt_to_res)
-                   #Hload_success
-                   lapply (mi_inj ??? Hinj
-                            cl_b
-                            (mk_offset
-                              (addition_n offset_size (offv CLO)
-                              (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset))))
-                            BLO (offset_plus (mk_offset
-                              (addition_n offset_size (offv CLO)
-                              (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) OFF) ? val ?? Hload_success)
-                   [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
-                   | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
-                   * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
-                   %{cm_val'} @conj try assumption
-                   whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
-                   #Heq destruct (Heq) @refl ]
-  ] ]
+       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
+       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
+       normalize nodelta #Htranslate_expr
+       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
+       * whd in match (typ_of_type ?); normalize nodelta
+       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
+       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
+         #cm_field_off * #Hcm_field_off 
+       | lapply Htranslate_expr2 -Htranslate_expr2 ]
+       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
+       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
+       whd in Hexec_lvalue:(???%);
+       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
+         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
+       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
+       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
+       [  (* Struct case *)
+         lapply Hcl_load_value -Hcl_load_value
+         lapply Hyp_present -Hyp_present
+         lapply Hexpr_vars -Hexpr_vars
+         lapply cm_expr -cm_expr
+         lapply Hind -Hind
+         cases ty
+         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
+         | #structname #fieldspec | #unionname #fieldspec | #id ]
+         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
+         normalize nodelta
+         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+         whd in match (eval_expr ???????);
+         (* applying the arguments of the induction hypothesis progressively *)
+         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
+                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
+         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
+         lapply (Hind ?)
+         [ 1,3,5,7,9:
+            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
+            >Htranslate_expr_ind whd in match (m_bind ?????);
+            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
+         whd in Hoffset_eq:(???%); destruct (offset_eq)
+         cut (cl_field_off = cm_field_off)
+         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
+           normalize #Heq destruct (Heq) @refl ]
+         #Heq destruct (Heq)
+         lapply (Hind cl_b cl_o trace ?)
+         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
+         lapply (Hind ?) -Hind
+         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
+           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
+           @Hoffset_eq ]
+         * #cm_val' * #Heval_expr #Hvalue_eq
+         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
+         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
+         [ 1,2,5: (* by-value *)
+            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
+            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
+            * #cm_val * #Hcm_load_value #Hvalue_eq
+            lapply (load_value_of_type_by_value … Hcm_load_value)
+            [ 1,3,5: @refl ]
+            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
+            try @refl try assumption
+         | 3,4: (* by-ref *)
+            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
+            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
+            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption 
+         ]
+      | (* union case *)
+         lapply Hcl_load_value -Hcl_load_value
+         lapply Hyp_present -Hyp_present
+         lapply Hexpr_vars -Hexpr_vars
+         lapply cm_expr -cm_expr
+         lapply Hind -Hind
+         cases ty
+         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
+         | #structname #fieldspec | #unionname #fieldspec | #id ]
+         whd in match (typ_of_type ?); normalize nodelta
+         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
+         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+         [ 1,2,5: (* by-value *)
+            whd in match (eval_expr ???????);
+            lapply (Hind cm_expr_ind Hexpr_vars ?)
+            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
+            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
+            -Hind #Hind
+            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
+            whd in match (m_bind ?????); #Hind
+            cases (Hind (refl ??)) -Hind
+            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
+            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
+            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
+            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
+            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
+            * #cm_val * #Hcm_load_value #Hvalue_eq            
+            lapply (load_value_of_type_by_value … Hcm_load_value)
+            [ 1,3,5: @refl ]
+            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
+            try @refl assumption
+         | 3,4:
+            whd in Hexec_cl:(???%); destruct (Hexec_cl)
+            lapply (Hind cm_expr Hexpr_vars)
+            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
+            lapply (Hind Htranslate_expr_ind) -Hind
+            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
+            >Hexec_lvalue whd in match (m_bind ?????);
+            #Hind cases (Hind … Hyp_present (refl ??))
+            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
+            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
+            assumption ]
+    ]
+  ]
 | 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
      whd in Hexec_lvalue_var:(??%?);
      (* check whether var is local or global *)
-     lapply (Hlocal_matching var) cases (lookup ?? cl_env var) in Hexec_lvalue_var;
+     lapply (Hlocal_matching var) 
+     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
+     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
      normalize nodelta
      [ 1: (* global *)
-          #Hexec_opt
+          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
           cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
           whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
-          >(opt_to_res_inversion ???? Hopt_to_res) normalize nodelta
-          #Hembed >Hembed normalize nodelta
-          (* Standard stuff. *)
-          @cthulhu
+          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
+          #Hembed
+          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
+          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
+          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
+          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+          whd in match (eval_expr ???????);
+          whd in match (eval_constant ????);
+          <(eq_sym inv var) >Hfind_symbol normalize nodelta 
+          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
+          @conj try @refl %4 whd in match (pointer_translation ??);
+          >Hembed normalize nodelta whd in match (shift_offset ???);
+          >addition_n_0 @refl
      | 2: (* local *)
-          @cthulhu
-     ]
+          #BL #Heq destruct (Heq) #_
+          @(match (lookup ?? vars var)
+            return λx. (lookup ?? vars var = x) → ?
+            with
+            [ None ⇒ ?
+            | Some kind ⇒ ?
+            ] (refl ??))
+          normalize nodelta
+          #Hlookup [ @False_ind ]
+          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
+          #Hlookup
+          lapply (refl ? var_alloctype)
+          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
+          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
+          [ (* stack alloc*)
+            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
+            * #var_alloctype' #var_type' * #Hlookup_vartype'            
+            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
+            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
+            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
+            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
+            @conj try @refl %4 whd in match (pointer_translation ??);
+            >Hembed @refl
+          | (* local alloc *)
+            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
+            * #var_alloctype' #var_type' * #Hlookup_vartype'
+            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
+            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
+            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
+(*| 4: #e #ty*)
+| 4:
+  * #ed #ety cases ety
+  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
+  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta  
+  whd in match (typeof ?);
+  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
+  cases (bind_inversion ????? Htranslate) -Htranslate    
+  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
+  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
+  * #cl_val #trace0 * #Hexec_expr #Hcl_val
+  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
+  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
+  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
+    [ 1,5,9,13: #Heq destruct (Heq)
+    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
+    | 3,7,11,15: #Heq destruct (Heq)
+    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
+  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
+  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
+  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
+  %{cm_val} @conj try @refl try assumption
+| 5: 
+  #ty cases ty
+  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
+  | #structname #fieldspec | #unionname #fieldspec | #id ]
+  #ed #ty' #Hind
+  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
+  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
+  cases (bind_inversion ????? Htranslate) -Htranslate
+  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
+  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
+  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
+  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
+  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
+  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
+  %{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 ]
+  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
+  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)
+  @cthulhu
 | *: @cthulhu
 ] qed.
+
+