include "Clight/toCminor.ma". include "Clight/CexecInd.ma". include "common/Globalenvs.ma". include "Clight/toCminorOps.ma". include "Clight/memoryInjections.ma". include "Clight/Clight_abstract.ma". include "Cminor/Cminor_abstract.ma". record clight_cminor_inv : Type[0] ≝ { globals : list (ident × region × type); ge_cl : genv_t clight_fundef; ge_cm : genv_t (fundef internal_function); eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s; trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f → ∃tmp_u,f',H1,H2. translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧ find_funct … ge_cm v = Some ? f' }. (* Perhaps we will have to be more precise on what is allocated, etc. cf [exec_alloc_variables]. For now this is conveniently hidden in the [value_eq E v v'] *) definition memory_matching ≝ λE:embedding. λm,m':mem. λen:cl_env. λvenv:cm_env. λcminv:clight_cminor_inv. λsp:block. λvars:var_types. ∀id. match lookup SymbolTag ? en id with [ None ⇒ match find_symbol ? (ge_cl cminv) id with [ None ⇒ True | Some cl_blo ⇒ (* global symbols are mapped to themselves. Perhaps too strong. *) E cl_blo = Some ? 〈cl_blo, zero_offset〉 ] | Some cl_blo ⇒ match lookup ?? vars id with [ Some kind ⇒ let 〈vtype, type〉 ≝ kind in match vtype with [ Stack n ⇒ E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉 | Local ⇒ ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v → ∃v'. lookup ?? venv id = Some ? v' ∧ value_eq E v v' | _ ⇒ False ] | None ⇒ False ] ]. (* Local variables show up in the variable characterisation as local. *) lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id. characterise_vars globals f = 〈vartypes, stacksize〉 → Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) → ∃t. local_id vartypes id t. #globals * #ret #args #vars #body whd in match (characterise_vars ??); elim (args@vars) [ #vartypes #stacksize #id #_ * | * #hd #ty #tl #IH #vartypes #stacksize #id whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %; #vartypes' #stackspace' #IH whd in ⊢ (??(match % with [_⇒?])? → ?); cases (orb ??) #E whd in E:(??%?); destruct * [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit // | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC cases (identifier_eq ? id hd) [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit // | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss // ] ] ] qed. (* ---------------------------------- *) (* Auxilliary lemmas and definitions. *) lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id. (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) → lookup ?? env' var_id = None ? → lookup ?? env var_id = None ? ∧ ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). #vars elim vars [ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq) #H @conj try @H % // | * #id' #ty' #tl #Hind #env #env' #var * #m * #m' whd in ⊢ ((??%?) → ? → ?); cases (alloc m 0 (sizeof ty') (*XData*)) #m0 #b (* #Hregion *) normalize nodelta #Hexec #Hlookup lapply (Hind … (ex_intro … (ex_intro … Hexec)) Hlookup) cases env #env cases id' #id' cases var #var normalize @(eqb_elim … id' var) [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq)) #Heq H1 in Hlookup'; #Heq destruct ] ] qed. lemma variable_not_in_env_but_in_vartypes_is_global : ∀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 ? → ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 → ∃r.allocty = Global r. #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 * #Hlookup >Hlookup #_ #Habsurd destruct ] * [ 1: * #r * #ty' * #Hlookup' #Hex %{r} >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ] * #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta @(match allocty return λx. allocty = x → ? with [ Global r ⇒ λ_. ? | Stack st' ⇒ λHalloc. ? | Local ⇒ λHalloc. ? ] (refl ? allocty)) [ @False_ind ] normalize nodelta #Heq_typ (* Halloc is in contradiction with Hlookup_fail *) lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail) * #Hlookup' #Hnot_exists lapply (characterise_vars_all … Hcharacterise var_id t ?) [ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ] #Hexists @False_ind cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f)) [ 1,3: elim (fn_params f @ fn_vars f) in Hexists; // * #id' #ty' #tl #Hind * [ 1,3: * #Heq #_ %1 @Heq | *: #H %2 @Hind @H ] ] #H cases Hnot_exists #H' @H' @H qed. (* avoid a case analysis on type inside of a big proof *) lemma match_type_inversion_aux : ∀ty,e,f. match ty in type return λty':type.(res (expr (typ_of_type ty'))) with  [Tvoid⇒Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch) |Tint (sz:intsize)   (sg:signedness)⇒ f sz sg |Tpointer (x:type)⇒ Error (expr (typ_of_type (Tpointer x))) (msg TypeMismatch) |Tarray (x:type)   (y:ℕ)⇒ Error (expr (typ_of_type (Tarray x y))) (msg TypeMismatch) |Tfunction (x:typelist)   (y:type)⇒ Error (expr (typ_of_type (Tfunction x y))) (msg TypeMismatch) |Tstruct (x:ident)   (y:fieldlist)⇒ Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch) |Tunion (x:ident)   (y:fieldlist)⇒ Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch) |Tcomp_ptr (x:ident)⇒ Error (expr (typ_of_type (Tcomp_ptr x))) (msg TypeMismatch)] = OK ? e → ∃sz,sg. ty = Tint sz sg ∧ (f sz sg ≃ OK ? e). * [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] whd in match (typ_of_type Tvoid); #e #f normalize nodelta #Heq destruct %{sz} %{sg} % try @refl >Heq % qed. (* The two following lemmas are just noise. *) lemma expr_vars_fix_ptr_type : ∀ty',optlen. ∀e:expr (typ_of_type (ptr_type ty' optlen)). ∀P. expr_vars ASTptr (fix_ptr_type ty' optlen e) P → expr_vars (typ_of_type match optlen  in option  return λ_:(option ℕ).type with  [None⇒Tpointer ty' |Some (n':ℕ)⇒ Tarray ty' n']) e P. #ty' * normalize [ 2: #n ] #e #P @expr_vars_mp // qed. lemma eval_expr_rewrite_aux : ∀genv. ∀optlen. ∀ty'. ∀e. ∀cm_env. ∀H. ∀sp. ∀m. ∀res. (eval_expr genv (typ_of_type match optlen in option return λ_:(option ℕ).type with  [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n']) e cm_env (expr_vars_fix_ptr_type ty' optlen e (λid:ident.λty0:typ.present SymbolTag val cm_env id) H) sp m) = OK ? res → eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res. #genv * [ 2: #n ] normalize nodelta #ty' normalize in match (typ_of_type ?); #e #cm_env whd in match (fix_ptr_type ???); #H #sp #m #res #H @H qed. lemma sign_ext_sign_ext_reduce : ∀i. sign_ext 32 16 (sign_ext 16 32 i) = i. #i @refl qed. lemma sign_ext_zero_ext_reduce : ∀i. sign_ext 32 16 (zero_ext 16 32 i) = i. #i @refl qed. (* There are two zero_ext, and this causes the "disambiguator" to fail. So we do * the cleanup ourselves. *) definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext. definition zero_ext_val : ∀target_sz:intsize. val → val ≝ zero_ext. (* CM code uses 8 bit constants and upcasts them to target_size, CL uses 32 bit and * downcasts them to target_size. In the end, these are equal. We directly state what * we need. *) lemma value_eq_cl_cm_true : ∀E,sz. value_eq E (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 1))) (zero_ext_val sz (Vint I8 (repr I8 1))). #E * %2 qed. lemma value_eq_cl_cm_false : ∀E,sz. value_eq E (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 0))) (zero_ext_val sz (Vint I8 (repr I8 0))). #E * %2 qed. lemma exec_bool_of_val_inversion : ∀v,ty,b. exec_bool_of_val v ty = OK ? b → (∃sz,sg,i. v = Vint sz i ∧ ty = Tint sz sg ∧ b = (¬eq_bv (bitsize_of_intsize sz) i (zero (bitsize_of_intsize sz)))) ∨ (∃ty'. v = Vnull ∧ ty = Tpointer ty' ∧ b = false) ∨ (∃ptr,ty'. v = Vptr ptr ∧ ty = Tpointer ty' ∧ b = true). #v #ty #b #Hexec cases v in Hexec; [ | #vsz #i | | #p ] 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 | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) [ 2: %1 %2 %{ptr_ty} @conj try @conj try @refl | 3: %2 %{p} %{ptr_ty} @conj try @conj try @refl | 1: %1 %1 %{sz} %{sg} lapply Heq -Heq cases vsz in i; #i cases sz whd in ⊢ ((??%?) → ?); #Heq destruct %{i} @conj try @conj try @refl ] qed. (* This lemma is noise I extracted from the proof below, even though it is used only once. Better that than an ugly cut. We need the following lemma to feed another one down in the deref case. In essence, it says that the variables present in a cminor expression resulting from converting a clight deref are transmitted to the cminor counterpart of the dereferenced pointer. This is made messy by the fact that clight to cminor implements different deref strategies for different kind of variables. *) lemma translate_expr_deref_present: ∀vars:var_types. ∀ptrdesc:expr_descr. ∀ptrty:type. ∀derefty:type. ∀cm_deref. ∀Hcm_deref. ∀cm_ptr. ∀Hcm_ptr. ∀cm_env:env. translate_expr vars (Expr (Ederef (Expr ptrdesc ptrty)) derefty) =OK ? «cm_deref,Hcm_deref» → expr_vars (typ_of_type derefty) cm_deref (λid:ident.λty0:typ.present SymbolTag ? cm_env id) → translate_expr vars (Expr ptrdesc ptrty) =OK ? «cm_ptr,Hcm_ptr» → expr_vars ? cm_ptr (λid:ident.λty0:typ.present SymbolTag ? cm_env id). #cut_vars #ptrdesc #ptrty #derefty cases ptrty [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1 | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] #cut_cm_deref #Hcut_cm_deref #cut_cm_ptr #Hcut_cm_ptr #cut_cm_env whd in match (translate_expr ??); cases (translate_expr cut_vars (Expr ptrdesc ?)) normalize nodelta [ 1,2,3,4,6,8,10,11,12,13,14,16: #err #Habsurd destruct (Habsurd) ] normalize in match (typ_of_type ?); * #cut_e' #Hcut_local_e' lapply Hcut_cm_deref -Hcut_cm_deref lapply cut_cm_deref -cut_cm_deref cases (access_mode derefty) normalize nodelta [ #invert_ty | | #invert_ty | #invert_ty | | #invert_ty | #invert_ty | | #invert_ty | #invert_ty | | #invert_ty ] [ 3,6,9,12: #cut_cm_deref #Hcut_cm_deref #Habsurd destruct (Habsurd) ] #cut_cm_deref #Hcut_cm_deref #Heq destruct (Heq) [ 1,3,5,7: whd in ⊢ (% → ?); ] #Hgoal #Heq destruct @Hgoal qed. lemma load_value_of_type_by_ref : ∀ty,m,b,off,val. load_value_of_type ty m b off = Some ? val → typ_of_type ty ≃ ASTptr → access_mode ty ≃ By_reference → val = Vptr (mk_pointer b off). * [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] #m #b #off #val [ 1,6,7: normalize #Habsurd destruct (Habsurd) | 4,5: normalize #Heq #_ #_ destruct @refl | 2: #_ normalize #Heq destruct | *: #Hload normalize #_ #H lapply (jmeq_to_eq ??? H) #Heq destruct ] qed. lemma load_value_of_type_by_value : ∀ty,m,b,off,val. access_mode ty = By_value (typ_of_type ty) → load_value_of_type ty m b off = Some ? val → loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val. * [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] #m #b #off #val normalize in match (access_mode ?); [ 1,4,5,6,7: #Habsurd destruct ] #_ #H @H qed. lemma lookup_exec_alloc : ∀source_variables, initial_env, env, var_id, clb, m, m'. lookup ?? env var_id = Some ? clb → exec_alloc_variables initial_env m source_variables = 〈env,m'〉 → lookup ?? initial_env var_id = Some ? clb ∨ Exists ? (λx. \fst x = var_id) source_variables. #source_variables elim source_variables [ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc; destruct (Hexec_alloc) %1 @Hlookup | 2: * #id #ty #tail #Hind #init_env #env #var #clb #m #m' #Hlookup whd in ⊢ (??%? → ?); cases (alloc m 0 (sizeof ty) (*XData*)) #m0 #blo normalize nodelta #Hexec_alloc @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ]) [ 1: destruct (Heq) %2 %1 @refl ] cases (Hind … Hlookup Hexec_alloc) [ #Hlookup %1 <(lookup_add_miss SymbolTag ? init_env ?? blo (sym_neq ??? Hneq)) @Hlookup | #Hexists %2 %2 @Hexists ] ] qed. lemma characterise_vars_lookup_local : ∀globals,f,vartypes,stacksize,id,clb,env. characterise_vars globals f = 〈vartypes, stacksize〉 → lookup ?? env id = Some ? clb → (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) → ∃t. local_id vartypes id t. #globals #f #vartypes #stacksize #id #clb #env #Hchar #Hlookup * #m * #m' #Hexec cases (lookup_exec_alloc … Hlookup Hexec) [ normalize in ⊢ (% → ?); #Heq destruct | @(characterise_vars_localid … Hchar) ] qed. record clight_cminor_data (f : function) (INV : clight_cminor_inv) : Type[0] ≝ { alloc_type : var_types; stacksize : ℕ; alloc_hyp : characterise_vars (globals INV) f = 〈alloc_type, stacksize〉; (* environments *) cl_env : cl_env; cm_env : cm_env; (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *) cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉; (* CL and CM memories *) cl_m : mem; cm_m : mem; (* memory injection and matching *) E : embedding; injection : memory_inj E cl_m cm_m; stackptr : block; matching : memory_matching E cl_m cm_m cl_env cm_env INV stackptr alloc_type }. (* -------------------------------------------------------------------- *) (* Simulation proof for expression evaluation between Clight and Cminor *) lemma eval_expr_sim : (* [cl_cm_inv] maps CL globals to CM globals, including functions *) ∀cl_cm_inv : clight_cminor_inv. (* current function (defines local environment) *) ∀f : function. ∀data : clight_cminor_data f cl_cm_inv. (* clight expr to cminor expr *) (∀(e:expr). ∀(e':CMexpr (typ_of_type (typeof e))). ∀Hexpr_vars. translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») → ∀cl_val,trace,Hyp_present. exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 → ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ value_eq (E ?? data) cl_val cm_val) ∧ (* clight /lvalue/ to cminor /expr/ *) (∀ed,ty. ∀(e':CMexpr ASTptr). ∀Hexpr_vars. translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») → ∀cl_blo,cl_off,trace,Hyp_present. exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 → ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧ value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val). #inv #f * #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching @expr_lvalue_ind_combined [ 7: (* binary ops *) #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 ⊢ ((??%?) → ?); #Htranslate_binop cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq) #cl_val #trace #Hyp_present #Hexec (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *) lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1 lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2 lapply Hyp_present -Hyp_present lapply Htranslate_lhs -Htranslate_lhs lapply Htranslate_rhs -Htranslate_rhs lapply Hexpr_vars_lhs -Hexpr_vars_lhs lapply Hexpr_vars_rhs -Hexpr_vars_rhs lapply Hexec -Hexec lapply Htranslated_binop -Htranslated_binop lapply rhs -rhs lapply lhs -lhs (* end of dump *) cases op whd in ⊢ (? → ? → (??%?) → ?); [ 1: (* add *) lapply (classify_add_inversion (typeof e1) (typeof e2)) * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] (* trying to factorise as much stuff as possible ... *) lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' * [ 1: * ] [ 1: * #sz * #sg * * | 2: * #optlen * #ty' * #sz * #sg * * | 3: * #optlen * #sz * #sg * #ty' * * ] whd in match (typeof ?) in ⊢ (% → % → ?); #Htypeof_e1 #Htypeof_e2 >Htypeof_e1 >Htypeof_e2 #Hclassify lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify normalize nodelta whd in match (typeof ?) in ⊢ (% → % → %); whd in match (typ_of_type (Tint ??)); #lhs #rhs #Htyp_should_eq [ 1: cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq) | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ] -Htyp_should_eq #Heq_type Heval_lhs normalize nodelta whd in match (eval_expr ???????); whd in match (eval_expr ???????); >Heval_rhs normalize nodelta whd in match (m_bind ?????); | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta whd in match (eval_expr ???????); whd in match (eval_expr ???????); >Heval_lhs normalize nodelta ] whd in match (proj1 ???); whd in match (proj2 ???); [ 2: (* standard int/int addition. *) whd in match (eval_binop ???????); whd in Hsem_binary:(??%?); lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_add_ii_inversion … Hsem_binary_translated) #cm_vsz * #cm_lhs_v * #cm_rhs_v * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta >intsize_eq_elim_true normalize nodelta %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))} @conj try @refl lapply Hsem_binary_translated whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??); >inttyp_eq_elim_true' normalize nodelta >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res | *: (* pointer/int int/pointer addition *) whd in Hsem_binary:(??%?); lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res (* >> *) [ lapply (sem_add_pi_inversion … Hsem_binary_translated) * #cm_vsz * #cm_rhs_v * #Hcm_rhs * [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ] | lapply (sem_add_ip_inversion … Hsem_binary_translated) * #cm_vsz * #cm_lhs_v * #Hcm_lhs * [ * #rhs_ptr * #Hcm_rhs_ptr #Hcm_val_shptr | * * #rhs_null #Hcm_lhs_zero #Hcm_val_null ] ] destruct whd in match (eval_unop ????); @(match sg return λs. sg = s → ? with [ Unsigned ⇒ λHsg. ? | Signed ⇒ λHsg. ? ] (refl ??)) normalize nodelta whd in match (eval_binop ???????); whd in match (m_bind ?????); [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr (short_multiplication (bitsize_of_intsize I16) (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) (repr I16 (sizeof ty')))))} | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr (short_multiplication (bitsize_of_intsize I16) (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) (repr I16 (sizeof ty')))))} | 5: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr (short_multiplication (bitsize_of_intsize I16) (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v) (repr I16 (sizeof ty')))))} | 6: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr (short_multiplication (bitsize_of_intsize I16) (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v) (repr I16 (sizeof ty')))))} ] [ 1,2,3,4: @conj whd in match (E0); whd in match (Eapp trace_rhs ?); whd in match (Eapp trace_lhs ?); >(append_nil … trace_rhs) try @refl >(append_nil … trace_lhs) try @refl @(value_eq_triangle_diagram … Hvalue_eq_res) whd in match (shift_pointer_n ?????); whd in match (shift_offset_n ?????); >Hsg normalize nodelta >commutative_short_multiplication whd in match (shift_pointer ???); whd in match (shift_offset ???); >sign_ext_same_size @refl | 5,7: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) | 6,8: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ] >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption normalize >append_nil try @refl ] | 2: (* subtraction cases: not quite identical to add. *) lapply (classify_sub_inversion (typeof e1) (typeof e2)) * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' * [ 1: * ] [ 1: * #sz * #sg * * | 2: * #optlen * #ty' * #sz * #sg * * | 3: * #t1 * #t2 * #n1 * #n2 * * ] whd in match (typeof ?) in ⊢ (% → % → ?); #Htypeof_e1 #Htypeof_e2 >Htypeof_e1 >Htypeof_e2 #Hclassify lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify normalize nodelta whd in match (typeof ?) in ⊢ (% → % → %); whd in match (typ_of_type (Tint ??)); #lhs #rhs [ 1: #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq | 2: #Htyp_should_eq cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq | 3: #Haux cases (match_type_inversion_aux … Haux) #ty_sz * #ty_sg * -Haux #Hty_eq #Heq_aux destruct (Hty_eq) lapply (jmeq_to_eq ??? Heq_aux) -Heq_aux #Heq_e' destruct (Heq_e') ] [ 1,2: #Heq_type Heval_lhs normalize nodelta whd in match (eval_expr ???????); whd in match (eval_expr ???????); whd in match (proj2 ???); [ >(eval_expr_rewrite_aux … Heval_rhs) | >Heval_rhs ] whd in match (m_bind ?????); normalize nodelta | 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta whd in match (eval_expr ???????); whd in match (proj2 ???); whd in match (eval_expr ???????); whd in match (proj1 ???); whd in match (eval_expr ???????); >Heval_rhs normalize nodelta whd in match (eval_unop ????); ] [ 1: (* ptr/ptr sub *) whd in Hsem_binary:(??%?); lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary * #cm_val * #Hsem_binary_translated #Hvalue_eq_res lapply (sem_sub_pp_inversion … Hsem_binary_translated) * #ty_sz' * #ty_sg' * #Heq destruct (Heq) * [ (* regular pointers case *) * #lhs_ptr * #rhs_ptr * #resulting_offset * * * * #Hcm_lhs #Hcm_rhs #Hblocks_eq #Hoffset_eq #Hcm_val_eq whd in match (eval_binop ???????); >Hcm_lhs >Hcm_rhs normalize nodelta >Hblocks_eq >eq_block_b_b normalize nodelta whd in match (eval_expr ???????); whd in match (m_bind ?????); whd in match (eval_binop ???????); normalize in match (bitsize_of_intsize ?); normalize in match (S (7+pred_size_intsize I16*8)) in Hoffset_eq; >Hoffset_eq (* whd in match (pred_size_intsize ?); normalize in match (7+1*8); *) (* size mismatch between CL and CM. TODO *) >Hoffset_eq normalize nodelta whd in match (eval_unop ????); %{cm_val} >Hcm_val_eq whd in match (opt_to_res ???); whd in match (m_bind ?????); @conj [ 2: destruct assumption | 1: whd in match (zero_ext ? (Vint ??)); whd in match E0; whd in match (Eapp ? []); >append_nil normalize in match (bitsize_of_intsize ?); try @refl ] | (* null pointers case *) * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct whd in match (eval_binop ???????); normalize nodelta whd in match (eval_expr ???????); whd in match (m_bind ?????); whd in match (eval_binop ???????); normalize nodelta >division_u_zero normalize nodelta whd in match (eval_unop ????); whd in match (opt_to_res ???); whd in match (m_bind ?????); whd in match (pred_size_intsize ?); %{(zero_ext ty_sz' (Vint I32 (zero (S (7+3*8)))))} @conj [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ] whd in Hsem_binary_translated:(??%?); normalize nodelta in Hsem_binary_translated:(??%?); lapply Hsem_binary_translated; -Hsem_binary_translated cases n1 cases n2 [ | 2,3: #n | #n1 #n2 ] normalize nodelta #Heq destruct (Heq) whd in match (zero_ext ??); cases ty_sz' in Hvalue_eq_res; try // ] | 2: (* int/int sub *) whd in match (eval_binop ???????); whd in Hsem_binary:(??%?); lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_sub_ii_inversion … Hsem_binary_translated) #cm_vsz * #cm_lhs_v * #cm_rhs_v * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta >intsize_eq_elim_true normalize nodelta %{(Vint cm_vsz (subtraction (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))} @conj try @refl lapply Hsem_binary_translated whd in ⊢ ((??%?) → ?); normalize nodelta whd in match (classify_sub ??); >type_eq_dec_true normalize nodelta >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res | 3: (* ptr/int sub *) whd in Hsem_binary:(??%?); lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary * #cm_val * #Hsem_binary_translated #Hvalue_eq_res lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated * #cm_vsz * #cm_rhs_v * #Hcm_rhs * [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ] whd in match (eval_unop ????); -Heval_lhs -Heval_rhs destruct whd in match (proj2 ???); whd in match (proj1 ???); whd in match (proj2 ???); whd in match (eval_expr ???????); @(match sg return λs. sg = s → ? with [ Unsigned ⇒ λHsg. ? | Signed ⇒ λHsg. ? ] (refl ??)) normalize nodelta whd in match (eval_unop ????); whd in match (m_bind ?????); whd in match (eval_binop ???????); [ 1,2: whd in match (neg_shift_pointer_n ?????) in Hvalue_eq_res; whd in match (neg_shift_offset_n ?????) in Hvalue_eq_res; whd in match (neg_shift_pointer ???); whd in match (neg_shift_offset ???); destruct (Hsg) normalize nodelta in Hvalue_eq_res; [ >sign_ext_sign_ext_reduce %{(Vptr (mk_pointer (pblock lhs_ptr) (mk_offset (subtraction offset_size (offv (poff lhs_ptr)) (short_multiplication (bitsize_of_intsize I16) (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) (repr I16 (sizeof ty')))))))} @conj [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl | >commutative_short_multiplication @Hvalue_eq_res ] | >sign_ext_zero_ext_reduce %{(Vptr (mk_pointer (pblock lhs_ptr) (mk_offset (subtraction offset_size (offv (poff lhs_ptr)) (short_multiplication (bitsize_of_intsize I16) (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v) (repr I16 (sizeof ty')))))))} @conj [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl | >commutative_short_multiplication @Hvalue_eq_res ] ] ] [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) >(sign_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32)) | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) >(short_multiplication_zero 16 (repr I16 (sizeof ty'))) >(zero_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32)) ] >(eq_bv_true … (zero 32)) normalize nodelta %{Vnull} @conj try assumption normalize >append_nil try @refl ] | 3: (* mul *) lapply (classify_aop_inversion (typeof e1) (typeof e2)) * [ 2,4: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' * #sz * #sg * * whd in match (typeof ?) in ⊢ (% → % → ?); #Htypeof_e1 #Htypeof_e2 >Htypeof_e1 >Htypeof_e2 whd in match (typeof ?) in ⊢ (% → % → % → ?); #Hclassify lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify normalize nodelta whd in match (typ_of_type (Tint ??)); #lhs #rhs #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq #Heq_type Heval_lhs normalize nodelta >Heval_rhs normalize nodelta whd in match (m_bind ?????); whd in match (eval_binop ???????); whd in Hsem_binary:(??%?); lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_mul_inversion … Hsem_binary) #cm_vsz * #cm_lhs_v * #cm_rhs_v * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta >intsize_eq_elim_true normalize nodelta %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))} @conj try @refl whd in Hsem_binary:(??%?); whd in match (classify_aop ??) in Hsem_binary:(??%?); >type_eq_dec_true in Hsem_binary; normalize nodelta >intsize_eq_elim_true #Heq destruct (Heq) %2 | 4,5: (* div *) lapply (classify_aop_inversion (typeof e1) (typeof e2)) * [ 2,4: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' * #sz * * * * whd in match (typeof ?) in ⊢ (% → % → ?); #Htypeof_e1 #Htypeof_e2 >Htypeof_e1 >Htypeof_e2 whd in match (typeof ?) in ⊢ (% → % → % → ?); #Hclassify lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify normalize nodelta whd in match (typ_of_type (Tint ??)); #lhs #rhs #Htyp_should_eq [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq) | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ] -Htyp_should_eq #Heq_type Heval_lhs normalize nodelta >Heval_rhs normalize nodelta whd in match (m_bind ?????); whd in match (eval_binop ???????); whd in Hsem_binary:(??%?); [ 1,3: (* div*) lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res [ cases (sem_div_inversion_s … Hsem_binary) | cases (sem_div_inversion_u … Hsem_binary) ] | 2,4: (* mod *) lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res [ cases (sem_mod_inversion_s … Hsem_binary) | cases (sem_mod_inversion_u … Hsem_binary) ] ] #cm_vsz * #cm_lhs_v * #cm_rhs_v * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta >intsize_eq_elim_true normalize nodelta [ cases (division_s ???) in Hcm_val; | cases (division_u ???) in Hcm_val; | cases (modulus_s ???) in Hcm_val; | cases (modulus_u ???) in Hcm_val; ] normalize nodelta [ 1,3,5,7: @False_ind ] #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 | 6,7,8: (* and,or,xor *) lapply (classify_aop_inversion (typeof e1) (typeof e2)) * [ 2,4,6: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' * #sz * #sg * * whd in match (typeof ?) in ⊢ (% → % → ?); #Htypeof_e1 #Htypeof_e2 >Htypeof_e1 >Htypeof_e2 whd in match (typeof ?) in ⊢ (% → % → % → ?); #Hclassify lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify normalize nodelta whd in match (typ_of_type (Tint ??)); #lhs #rhs #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq #Heq_type Heval_lhs normalize nodelta >Heval_rhs normalize nodelta whd in match (m_bind ?????); whd in match (eval_binop ???????); whd in Hsem_binary:(??%?); [ 1: (* and *) lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_and_inversion … Hsem_binary) | 2: (* or *) lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_or_inversion … Hsem_binary) | 3: (* xor *) lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_xor_inversion … Hsem_binary) ] #cm_vsz * #cm_lhs_v * #cm_rhs_v * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta >intsize_eq_elim_true normalize nodelta [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))} | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))} | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))} ] @conj try @refl >Hcm_val %2 | 9,10: (* shl, shr *) lapply (classify_aop_inversion (typeof e1) (typeof e2)) * [ 2,4: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e' * #sz * * * * whd in match (typeof ?) in ⊢ (% → % → ?); #Htypeof_e1 #Htypeof_e2 >Htypeof_e1 >Htypeof_e2 whd in match (typeof ?) in ⊢ (% → % → % → ?); #Hclassify lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify normalize nodelta whd in match (typ_of_type (Tint ??)); #lhs #rhs #Htyp_should_eq [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq) | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ] -Htyp_should_eq #Heq_type Heval_lhs normalize nodelta >Heval_rhs normalize nodelta whd in match (m_bind ?????); whd in match (eval_binop ???????); whd in Hsem_binary:(??%?); [ 1,3: (* shl *) lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_shl_inversion … Hsem_binary) #sz1 * #sz2 * #lhs_i * #rhs_i * * * #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok destruct (Hcl_lhs Hcl_rhs) >(value_eq_int_inversion … Hvalue_eq_lhs) >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta >Hshift_ok normalize nodelta %{(Vint sz1 (shift_left bool (bitsize_of_intsize sz1) (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))} @conj try @refl >Hcl_val %2 | *: (* shr, translated to mod /!\ *) lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) * #cm_val * #Hsem_binary_translated #Hvalue_eq_res cases (sem_shr_inversion … Hsem_binary) normalize nodelta #sz1 * #sz2 * #lhs_i * #rhs_i * * * #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val destruct (Hcl_lhs Hcl_rhs) >(value_eq_int_inversion … Hvalue_eq_lhs) >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta >Hshift_ok normalize nodelta >Hcl_val /3 by ex_intro, conj, vint_eq/ ] | *: (* comparison operators *) lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?) in ⊢ (% → % → % → %); #cm_expr whd in match (typeof ?); inversion (classify_cmp ety1 ety2) [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2 lapply (jmeq_to_eq ??? Hety1) #Hety1' lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct #Hclassify >Hclassify normalize nodelta #cmexpr1 #cmexpr2 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) | 1,4,7,10,13,16: #sz #sg #Hety1 #Hety2 #Hclassify lapply (jmeq_to_eq ??? Hety1) #Hety1' lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta whd in match (typeof ?) in ⊢ (% → % → % → %); whd in match (typ_of_type ?) in ⊢ (% → % → ?); cases sg #cmexpr1 #cmexpr2 normalize nodelta #Hcast_to_bool #Hexec_expr cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool #tysz * #tysg * #Htyis_int #Hcm_expr_aux destruct (Htyis_int) lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux destruct (Hcm_expr) cases (bind_inversion ????? Hexec_expr) -Hexec_expr * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec cases (bind_inversion ????? Hexec) -Hexec * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec cases (bind_inversion ????? Hexec) -Hexec #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hsem) -Hsem whd in match (typeof ?); whd in match (sem_binary_operation ???????); normalize nodelta #Hsem_cmp cases (some_inversion ????? Hsem_cmp) -Hsem_cmp #cl_val' * #Hsem_cmp #Hcl_val_cast destruct (Hcl_val_cast) lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta destruct (Hcl_lhs) destruct (Hcl_rhs) #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs * #Hyp_present_lhs #Hyp_present_rhs #Hind_rhs #Hind_lhs lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs) * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs) * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs whd in match (eval_expr ???????); whd in match (eval_expr ???????); >Heval_lhs normalize nodelta >Heval_rhs normalize nodelta whd in match (m_bind ?????); whd in match (eval_binop ???????); >(value_eq_int_inversion … Hvalue_eq_lhs) >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta >intsize_eq_elim_true normalize nodelta destruct (Heq_bool) whd in match (eval_unop ????); whd in match (opt_to_res ???); whd in match (m_bind ?????); whd in match (of_bool ?); [ %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))} | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))} ] @conj try @refl whd in match (FE_of_bool ?); whd in match FEtrue; whd in match FEfalse; [ 1,3,5,7,9,11: cases (cmp_int ????) normalize nodelta | *: cases (cmpu_int ????) normalize nodelta ] try @value_eq_cl_cm_true try @value_eq_cl_cm_false | *: (* ptr comparison *) #n #ty' #Hety1 #Hety2 #Hclassify lapply (jmeq_to_eq ??? Hety1) #Hety1' lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta whd in match (typeof ?) in ⊢ (% → % → % → %); #cmexpr1 #cmexpr2 #Hcast_to_bool #Hexec_expr cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool #tysz * #tysg * #Htyis_int #Hcm_expr_aux destruct (Htyis_int) lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux destruct (Hcm_expr) cases (bind_inversion ????? Hexec_expr) -Hexec_expr * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec cases (bind_inversion ????? Hexec) -Hexec * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec cases (bind_inversion ????? Hexec) -Hexec #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hsem) -Hsem whd in match (typeof ?); whd in match (sem_binary_operation ???????); #Hsem_cmp cases (some_inversion ????? Hsem_cmp) -Hsem_cmp normalize nodelta #cl_val' * #Hsem_cmp #Hcl_val_cast destruct (Hcl_val_cast); #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs * #Hyp_present_lhs #Hyp_present_rhs #Hind_rhs #Hind_lhs lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs -Hexec_rhs lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs -Hexec_lhs lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp) -Hsem_cmp -Hvalue_eq_lhs -Hvalue_eq_rhs * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res whd in match (eval_expr ???????); whd in match (eval_expr ???????); >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta whd in match (m_bind ?????); lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm * [ 2,4,6,8,10,12: * * #Hcl_lhs #Hcl_rhs #Hsem_cmp whd in Hsem_cmp:(??%?); destruct | *: * [ 2,4,6,8,10,12: * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp whd in Hsem_cmp:(??%?); destruct | *: * [ 2,4,6,8,10,12: * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp whd in Hsem_cmp:(??%?); destruct | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome whd in Hsem_cmp:(??%?); destruct ] ] ] whd in match (eval_binop ???????); normalize nodelta whd in match (eval_unop ????); whd in match (opt_to_res ???); whd in match (m_bind ?????); [ 1,2,3,4,5,6: [ 1,4,6: %{(zero_ext tysz FEtrue)} @conj try @refl >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta @value_eq_cl_cm_true | 2,3,5: %{(zero_ext tysz FEfalse)} @conj try @refl >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta @value_eq_cl_cm_false ] | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta lapply Heq_block_outcome -Heq_block_outcome @(eq_block_elim … (pblock p1) (pblock p2)) normalize nodelta whd in match (eval_unop ????); whd in match (opt_to_res ???); whd in match (m_bind ?????); [ 1,3,5,7,9,11: #Hbocks_eq #Heq_cmp destruct (Heq_cmp) whd in match (eval_unop ????); whd in match (m_bind ?????); cases (cmp_offset ???) in Hvalue_eq_res; normalize nodelta #Hvalue_eq_res >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta [ 1,3,5,7,9,11: %{(zero_ext tysz (FE_of_bool true))} @conj try @refl @value_eq_cl_cm_true | 2,4,6,8,10,12: %{(zero_ext tysz (FE_of_bool false))} @conj try @refl @value_eq_cl_cm_false ] | *: #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta [ %{(zero_ext tysz (FE_of_bool false))} @conj try @refl @value_eq_cl_cm_false | %{(zero_ext tysz (FE_of_bool true))} @conj try @refl @value_eq_cl_cm_true ] ] ] ] ] | 1: (* Integer constant *) #csz #ty cases ty [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate #val #trace #Hpresent #Hexec_cl whd in Htranslate:(??%?); [ 1,3,4,5,6,7,8: destruct ] cases (intsize_eq_elim_dec csz sz (λsz0.λsz0'.res (Σe0':expr (typ_of_type (Tint sz0' sg)).expr_vars (typ_of_type (Tint sz0' sg)) e0' (local_id vars)))) [ 2: * #H_err #H_neq_sz lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch))) >Htranslate #Habsurd destruct (Habsurd) ] * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch))) destruct (Heq_sz) >Htranslate -Htranslate -H_ok #Heq destruct (Heq) whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl // | 2: * [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] try /2 by I/ #ty whd in ⊢ (% → ?); #Hind whd in match (Plvalue ???); whd in match (typeof ?); #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec whd in Hexec:(??%?); whd in match (exec_lvalue' ?????) in Hexec:(??%?); cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success whd in Hcl_success:(???%); [ 1: (* var case *) lapply Hcl_success -Hcl_success -Hind (* Peform case analysis on presence of variable in local Clight env. * if success, exec_expr/exec_lvalue tells us that it shoud be local. *) @(match lookup SymbolTag block cl_env var_id return λx.(lookup SymbolTag block cl_env var_id = x) → ? with [ None ⇒ λHcl_lookup. ? | Some loc ⇒ λHcl_lookup. ? ] (refl ? (lookup SymbolTag block cl_env var_id))) normalize nodelta [ 1: (* global case *) #Hlookup_global cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol #Heq whd in Heq:(???%); destruct (Heq) lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr * #var_id_alloctype * #var_id_type * #Heq cases (variable_not_in_env_but_in_vartypes_is_global … Hexec_alloc Hcharacterise Hcl_lookup ?? Heq) #r #Heq' destruct (Heq') normalize nodelta lapply Hcl_load_success -Hcl_load_success lapply Hyp_present -Hyp_present lapply Hexpr_vars -Hexpr_vars lapply cm_expr -cm_expr inversion (access_mode ty) [ #typ_of_ty | | #typ_of_ty ] #Heq_typ_of_type #Heq_access_mode #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????); whd in match (eval_expr ???????); whd in match (eval_constant ????); <(eq_sym … inv) >Hfind_symbol normalize nodelta cases (bind_inversion ????? Hcl_load_success) #x * #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val) lapply (opt_to_res_inversion ???? Hopt_to_res) #Hcl_load_success [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))} @conj try @refl whd in Hcm_load_success:(??%?); lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty >(load_value_of_type_by_ref … Hcl_load_success) try assumption %4 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta >Hfind_symbol normalize nodelta #Heq_embedding whd in match (shift_offset ???); >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding normalize nodelta @refl | 1: cut (access_mode ty=By_value (typ_of_type ty)) [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt lapply Heq_access_mode Hcl_lookup normalize nodelta >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ] * #val' * #Hcm_load_success #Hvalue_eq lapply (load_value_of_type_by_value … Haccess … Hcm_load_success) #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq Hloadv normalize %{val'} @conj try @refl assumption ] | 2: (* local case *) #Heq destruct (Heq) lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr * #var_id_alloc_type * #var_id_type * generalize in match var_id_alloc_type; * normalize nodelta [ 1: #r #Hlookup_vartype lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc) * #typ whd in match (local_id ???); >Hlookup_vartype normalize nodelta @False_ind | 2: (* Stack local *) lapply Hcl_load_success -Hcl_load_success lapply Hyp_present -Hyp_present lapply Hexpr_vars -Hexpr_vars lapply cm_expr -cm_expr inversion (access_mode ty) [ #typ_of_ty | | #typ_of_ty ] #Heq_typ_of_type #Heq_access_mode #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success #stack_depth #Hlookup_vartype_success normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq) >Hlookup' normalize nodelta #Hembedding_eq cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #loaded_val * #Hload_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hload_val) -Hload_val #Hload_success whd in match (eval_expr ???????); cut (pointer_translation (mk_pointer cl_b zero_offset) E = Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth)))) [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta >offset_plus_0 @refl ] #Hpointer_translation [ 2: (* By-ref *) whd in Hload_success:(??%?); lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode) #Heq_val >Heq_val %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))} @conj try @refl %4 whd in match (shift_offset ???); whd in match zero_offset; >commutative_addition_n >addition_n_0 @Hpointer_translation | 1: (* By value *) lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0 lapply (mi_inj … Hinj … Hpointer_translation … Hload_success) [ @(load_by_value_success_valid_pointer … Hload_success) lapply Heq_access_mode commutative_addition_n >addition_n_0 >Hloadv @refl ] | 3: (* Register local variable *) #Hlookup_eq lapply (res_inversion ?????? Hlookup_eq) * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq) #Htype_eq cases (type_should_eq_inversion var_id_type ty (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars)) … Htype_eq) -Htype_eq (* Reverting all premises in order to perform type rewrite *) #Htype_eq lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq lapply Hcl_load_success -Hcl_load_success lapply Hcl_lookup -Hcl_lookup lapply Hyp_present -Hyp_present lapply Hexpr_vars -Hexpr_vars lapply cm_expr destruct (Htype_eq) #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup' #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq destruct (Hexpr_eq) whd in match (eval_expr ???????); whd in match (lookup_present ?????); lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta >Hlookup' normalize nodelta #Hmatching cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #loaded_val * #Hload_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hload_val) -Hload_val #Hload_success cases (Hmatching … Hload_success) #val' * #Hlookup_in_cm #Hvalue_eq %{val'} cases Hyp_present >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption (* seems ok *) ] ] | 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,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: @(translate_expr_deref_present … Htranslate_expr … Hyp_present … Htranslate_expr_ind) ] 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 * #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 Hexec_cm_ind -Hexec_cm_ind lapply Hyp_present -Hyp_present lapply Htranslate_expr -Htranslate_expr lapply Hexpr_vars -Hexpr_vars lapply cm_expr -cm_expr cases ty (* Inversion (access_mode ty) fails for whatever reason. *) [ | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 ] whd in match (typ_of_type ?); whd in match (access_mode ?); normalize nodelta #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_cm_ind #Hcl_load_success #Heq destruct (Heq) [ 3,4,8,9,13,14,18,19: (* 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 ??) try @refl_jmeq #Hval >Hval %4 assumption | *: (* 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) try @(load_by_value_success_valid_pointer … Hcl_load_success) try @jmeq_to_eq try assumption try @refl_jmeq * #cm_val * #Hcm_load_success #Hvalue_eq lapply (load_value_of_type_by_value … Hcm_load_success) try @refl #Hloadv_cm whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta >Hloadv_cm normalize %{cm_val} @conj try @refl assumption ] | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success lapply (refl ? (typeof e1)) cases (typeof e1) in ⊢ ((???%) → %); [ | #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_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 (Oaddpi 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) 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 #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) 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 *) #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 ] #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 ] ] | 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) cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -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 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 >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 (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type 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 (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type 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 #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?); cases ty [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] #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 (* cut *) * * normalize nodelta #Hexec_bool_of_val [ 2,4,6,8,10,12,14: whd in ⊢ ((???%) → ?); #Heq destruct (Heq) | 16: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) | *: #Hexec_expr cases (bind_inversion ????? Hexec_expr) -Hexec_expr * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr cases (bind_inversion ????? Hexec_expr) -Hexec_expr #b2 * #Hexec_bool_of_val_e2 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta * #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 #Hexpr_vars_wt * #Htype_coercion lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion * #Htypeof_e2_eq_ty (* cleanup the type coercion *) lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2 lapply Hexpr_vars_wt -Hexpr_vars_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 >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2 #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq) 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 cases (exec_bool_of_val_inversion … Hexec_bool_of_val) [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd) destruct >(Htypeof_e1) whd in match (typ_of_type ?); #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] * [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd) destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val destruct >Htypeof_e1 #Heq_bv whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?); #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta whd in match (typ_of_type ?); whd in ⊢ ((???%) → ?); #Heq destruct (Heq) cases Hyp_present -Hyp_present * #Hyp_present_e1 * * #Hyp_present_e2 normalize in ⊢ (% → % → % → ?); * * * lapply (Hind1 … Hyp_present_e1 Hexec_e1) * #cm_val_1 * #Heval_expr1 #Hvalue_eq whd in match (eval_expr ???????); whd in match (proj2 ???); whd in match (proj2 ???); >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?); zero_ext_zero @conj try %2 whd in match E0; whd in match (Eapp ??); >append_nil @refl ] normalize nodelta lapply (Hind2 … Hyp_present_e2 … Hexec_e2) -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2 whd in match (eval_expr ???????); >Heval_expr2 normalize nodelta cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2) [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct cases (value_eq_ptr_inversion … Hvalue_eq2) #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2 whd in match (eval_bool_of_val ?); whd in match (m_bind ?????); normalize nodelta >zero_ext_one %{(Vint sz (repr sz 1))} @conj try %2 whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ] * [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct >(value_eq_null_inversion … Hvalue_eq2) whd in match (eval_bool_of_val ?); whd in match (m_bind ?????); normalize nodelta %{(Vint sz (zero (bitsize_of_intsize sz)))} >zero_ext_zero @conj try %2 whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ] * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv destruct (Hcl_val_e2) >(value_eq_int_inversion … Hvalue_eq2) whd in match (eval_bool_of_val ?); append_nil @conj try @refl >zero_ext_one %2 | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []); >append_nil @conj try @refl >zero_ext_zero %2 ] | 11: (* orbool, similar to andbool *) #ty #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?); cases ty [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] #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 * * normalize nodelta #Hexec_bool_of_val [ 1,3,5,7,9,11,13,15: whd in ⊢ ((???%) → ?); #Heq destruct (Heq) | *: #Hexec_expr cases (bind_inversion ????? Hexec_expr) -Hexec_expr * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr cases (bind_inversion ????? Hexec_expr) -Hexec_expr #b2 * #Hexec_bool_of_val_e2 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta * #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 #Hexpr_vars_wt * #Htype_coercion lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion * #Htypeof_e2_eq_ty (* cleanup the type coercion *) lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2 lapply Hexpr_vars_wt -Hexpr_vars_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 >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2 #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq) 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 cases (exec_bool_of_val_inversion … Hexec_bool_of_val) [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd) destruct >(Htypeof_e1) whd in match (typ_of_type ?); #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] * [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd) destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val destruct >Htypeof_e1 #Heq_bv whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?); #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) cases Hyp_present -Hyp_present * #Hyp_present_e1 * * * #Hyp_present_e2 * * lapply (Hind1 … Hyp_present_e1 Hexec_e1) * #cm_val_1 * #Heval_expr1 #Hvalue_eq whd in match (eval_expr ???????); >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?); zero_ext_one @conj try %2 whd in match E0; whd in match (Eapp ??); >append_nil @refl ] normalize nodelta lapply (Hind2 … Hyp_present_e2 … Hexec_e2) -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2 whd in match (eval_expr ???????); >Heval_expr2 normalize nodelta cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2) [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct cases (value_eq_ptr_inversion … Hvalue_eq2) #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2 whd in match (eval_bool_of_val ?); whd in match (m_bind ?????); normalize nodelta >zero_ext_one %{(Vint sz (repr sz 1))} @conj try %2 whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ] * [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct >(value_eq_null_inversion … Hvalue_eq2) whd in match (eval_bool_of_val ?); whd in match (m_bind ?????); normalize nodelta %{(Vint sz (zero (bitsize_of_intsize sz)))} >zero_ext_zero @conj try %2 whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ] * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv destruct (Hcl_val_e2) >(value_eq_int_inversion … Hvalue_eq2) whd in match (eval_bool_of_val ?); append_nil @conj try @refl >zero_ext_one %2 | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []); >append_nil @conj try @refl >zero_ext_zero %2 ] | 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) whd in match (shift_pointer ???); whd in match (shift_offset ???) in ⊢ (???%); >sign_ext_same_size whd in match (offset_plus ??) in ⊢ (??%%); <(associative_addition_n ? (offv off)) >(commutative_addition_n … (repr I16 field_off) (offv OFF)) >(associative_addition_n ? (offv off)) @refl | 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:(??%?); cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq) #Htyp_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 ?); Heval_expr' normalize nodelta %{cm_val'} @conj try assumption >cons_to_append >(nil_append … cm_trace) @refl | 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.