Changeset 2591


Ignore:
Timestamp:
Jan 28, 2013, 11:43:43 AM (6 years ago)
Author:
garnier
Message:

Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, for separate typechecking.

Location:
src/Clight
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2588 r2591  
    11include "Clight/toCminor.ma".
    2 include "Clight/toCminorOps.ma".
    32include "Clight/CexecInd.ma".
    43include "common/Globalenvs.ma".
     
    65include "Clight/abstract.ma".
    76include "Cminor/abstract.ma".
     7
     8(* Expr simulation. Contains important definitions for statements, too.  *)
     9include "Clight/toCminorCorrectnessExpr.ma".
    810
    911
     
    138140] qed.
    139141
    140 (* Local variables show up in the variable characterisation as local. *)
    141 
    142 lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
    143   characterise_vars globals f = 〈vartypes, stacksize〉 →
    144   Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
    145   ∃t. local_id vartypes id t.
    146 #globals * #ret #args #vars #body
    147 whd in match (characterise_vars ??); elim (args@vars)
    148 [ #vartypes #stacksize #id #_ *
    149 | * #hd #ty #tl #IH
    150   #vartypes #stacksize #id
    151   whd in match (foldr ?????);
    152   cases (foldr ? (Prod ??) ???) in IH ⊢ %;
    153   #vartypes' #stackspace' #IH
    154   whd in ⊢ (??(match % with [_⇒?])? → ?);
    155   cases (orb ??)
    156   #E whd in E:(??%?); destruct *
    157   [ 1,3: #E destruct %{(typ_of_type ty)}
    158     whd whd in match (lookup' ??); >lookup_add_hit //
    159   | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
    160     cases (identifier_eq ? id hd)
    161     [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
    162     | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
    163     ]
    164   ]
    165 ] qed.
     142
    166143
    167144(* Put knowledge that Globals are global into a more useful form than the
    168    one used for the invariant. *)
    169 
     145   one used for the invariant. *)   
     146(* XXX superfluous lemma ? Commenting it for now.
     147       if not superfluous : move to toCminorCorrectnessExpr.ma, after
     148       [characterise_vars_localid] *)
     149(*
    170150lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
    171151  characterise_vars globals f = 〈vartypes, stacksize〉 →
     
    184164| * #ty' whd in ⊢ (% → ?); >L *
    185165| whd >(opt_eq_from_res ???? L) % #E destruct
    186 ] qed.
    187 
     166] qed. *)
    188167
    189168(* Show how the global environments match up. *)
     
    255234] qed.
    256235
    257 (* Invariants used in simulation *)
    258 
    259 record clight_cminor_inv : Type[0] ≝ {
    260   globals : list (ident × region × type);
    261   ge_cl : genv_t clight_fundef;
    262   ge_cm : genv_t (fundef internal_function);
    263   eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
    264   trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
    265     ∃tmp_u,f',H1,H2.
    266       translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
    267       find_funct … ge_cm v = Some ? f'
    268 }.
    269 
    270 (* Perhaps we will have to be more precise on what is allocated, etc.
    271    cf [exec_alloc_variables]. For now this is conveniently hidden in
    272    the [value_eq E v v'] *)
    273 definition memory_matching ≝
    274   λE:embedding.
    275   λm,m':mem.
    276   λen:cl_env.
    277   λvenv:cm_env.
    278   λcminv:clight_cminor_inv.
    279   λsp:block.
    280   λvars:var_types.
    281   ∀id.
    282     match lookup SymbolTag ? en id with
    283     [ None ⇒
    284       match find_symbol ? (ge_cl cminv) id with
    285       [ None ⇒ True
    286       | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
    287       ]
    288     | Some cl_blo ⇒
    289          match lookup ?? vars id with
    290          [ Some kind ⇒
    291             let 〈vtype, type〉 ≝ kind in
    292             match vtype with
    293             [ Stack n ⇒
    294               E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
    295             | Local ⇒
    296               ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
    297                    ∃v'. lookup ?? venv id = Some ? v' ∧
    298                         value_eq E v v'
    299             | _ ⇒ False ]
    300         | None ⇒ False ]
    301     ].
    302 
    303 lemma load_value_of_type_by_ref :
    304   ∀ty,m,b,off,val.
    305     load_value_of_type ty m b off = Some ? val →
    306     typ_of_type ty ≃ ASTptr →
    307     access_mode ty ≃ By_reference →
    308     val = Vptr (mk_pointer b off).
    309 *
    310 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    311 | #structname #fieldspec | #unionname #fieldspec | #id ]
    312 #m #b #off #val
    313 [ 1,6,7: normalize #Habsurd destruct (Habsurd)
    314 | 4,5: normalize #Heq #_ #_ destruct @refl
    315 | 2: #_ normalize #Heq destruct
    316 | *: #Hload normalize #_ #H
    317       lapply (jmeq_to_eq ??? H) #Heq destruct
    318 ] qed.
    319 
    320 lemma load_value_of_type_by_value :
    321   ∀ty,m,b,off,val.
    322   access_mode ty = By_value (typ_of_type ty) →
    323   load_value_of_type ty m b off = Some ? val →
    324   loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
    325 
    326 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    327 | #structname #fieldspec | #unionname #fieldspec | #id ]
    328 #m #b #off #val
    329 normalize in match (access_mode ?);
    330 [ 1,4,5,6,7: #Habsurd destruct ]
    331 #_
    332 #H @H
    333 qed.
    334 
    335 lemma lookup_exec_alloc :
    336   ∀source_variables, initial_env, env, var_id, clb, m, m'.
    337   lookup ?? env var_id = Some ? clb →
    338   exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
    339   lookup ?? initial_env var_id = Some ? clb ∨
    340   Exists ? (λx. \fst x = var_id) source_variables.
    341 #source_variables
    342 elim source_variables
    343 [ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
    344      destruct (Hexec_alloc) %1 @Hlookup
    345 | 2: * #id #ty #tail #Hind
    346      #init_env #env #var #clb #m #m' #Hlookup     
    347      whd in ⊢ (??%? → ?);
    348      cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
    349      #Hexec_alloc
    350      @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
    351      [ 1: destruct (Heq) %2 %1 @refl ]
    352      cases (Hind … Hlookup Hexec_alloc)
    353      [ #Hlookup %1 <(lookup_add_miss SymbolTag ? init_env ?? blo (sym_neq ??? Hneq)) @Hlookup
    354      | #Hexists %2 %2 @Hexists ]
    355 ] qed.
    356 
    357 lemma characterise_vars_lookup_local :
    358   ∀globals,f,vartypes,stacksize,id,clb,env.
    359    characterise_vars globals f = 〈vartypes, stacksize〉 →
    360    lookup ?? env id = Some ? clb →
    361    (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
    362    ∃t. local_id vartypes id t.
    363 #globals #f #vartypes #stacksize #id #clb #env
    364 #Hchar #Hlookup * #m * #m' #Hexec
    365 cases (lookup_exec_alloc … Hlookup Hexec)
    366 [ normalize in ⊢ (% → ?); #Heq destruct
    367 | @(characterise_vars_localid … Hchar) ]
    368 qed.
    369 
    370 
    371 lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
    372   (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
    373   lookup ?? env' var_id = None ? →
    374   lookup ?? env var_id = None ? ∧
    375   ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
    376 #vars elim vars
    377 [ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
    378   #H @conj try @H % //
    379 | * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
    380   whd in ⊢ ((??%?) → ? → ?);
    381   cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
    382   normalize nodelta #Hexec #Hlookup
    383   lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
    384   cases env #env cases id' #id' cases var #var normalize
    385   @(eqb_elim … id' var)
    386   [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
    387        #Heq <Heq @conj try @Hlookup' % *
    388        [ #Heq' destruct (Heq') cases Hneq #H @H @refl
    389        | cases Hexists' #H @H ]
    390   | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
    391        lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
    392        >H1 in Hlookup'; #Heq destruct
    393   ]
    394 ] qed.
    395 
    396 lemma variable_not_in_env_but_in_vartypes_is_global :
    397   ∀env,env',f,vars,stacksize,globals,var_id.
    398   (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
    399   characterise_vars globals f =〈vars,stacksize〉 →
    400   lookup ?? env' var_id = None ? →       
    401   ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
    402   ∃r.allocty = Global r.
    403 #env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
    404 #Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
    405 lapply (characterise_vars_src … Hcharacterise var_id ?)
    406 [ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
    407  #Hlookup >Hlookup #_ #Habsurd destruct ]
    408 *
    409 [ 1: * #r * #ty' * #Hlookup' #Hex %{r}
    410      >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
    411 * #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
    412 @(match allocty
    413   return λx. allocty = x → ?
    414   with
    415   [ Global r ⇒ λ_. ?
    416   | Stack st' ⇒ λHalloc. ?
    417   | Local ⇒ λHalloc. ?
    418   ] (refl ? allocty))
    419 [ @False_ind ] normalize nodelta
    420 #Heq_typ
    421 (* Halloc is in contradiction with Hlookup_fail *)
    422 lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
    423 * #Hlookup' #Hnot_exists
    424 lapply (characterise_vars_all … Hcharacterise var_id t ?)
    425 [ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
    426 #Hexists @False_ind
    427 cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
    428 [ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
    429        * #id' #ty' #tl #Hind *
    430        [ 1,3: * #Heq #_ %1 @Heq
    431        | *: #H %2 @Hind @H ] ]
    432 #H cases Hnot_exists #H' @H' @H
    433 qed.
    434 
    435 (* avoid a case analysis on type inside of a big proof *)
    436 lemma match_type_inversion_aux : ∀ty,e,f.
    437  match ty in type return λty':type.(res (expr (typ_of_type ty'))) with 
    438   [Tvoid⇒Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
    439   |Tint (sz:intsize)   (sg:signedness)⇒ f sz sg
    440   |Tpointer (x:type)⇒
    441    Error (expr (typ_of_type (Tpointer x))) (msg TypeMismatch)
    442   |Tarray (x:type)   (y:ℕ)⇒
    443    Error (expr (typ_of_type (Tarray x y))) (msg TypeMismatch)
    444   |Tfunction (x:typelist)   (y:type)⇒
    445    Error (expr (typ_of_type (Tfunction x y))) (msg TypeMismatch)
    446   |Tstruct (x:ident)   (y:fieldlist)⇒
    447    Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
    448   |Tunion (x:ident)   (y:fieldlist)⇒
    449    Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
    450   |Tcomp_ptr (x:ident)⇒
    451    Error (expr (typ_of_type (Tcomp_ptr x))) (msg TypeMismatch)]
    452   = OK ? e →
    453   ∃sz,sg. ty = Tint sz sg ∧ (f sz sg ≃ OK ? e).
    454 *
    455 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    456 | #structname #fieldspec | #unionname #fieldspec | #id ]
    457 whd in match (typ_of_type Tvoid);
    458 #e #f normalize nodelta #Heq destruct
    459 %{sz} %{sg} % try @refl >Heq %
    460 qed.
    461 
    462 
    463 (* The two following lemmas are just noise. *)
    464 
    465 lemma expr_vars_fix_ptr_type :
    466   ∀ty',optlen.
    467   ∀e:expr (typ_of_type (ptr_type ty' optlen)).
    468   ∀P.
    469    expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
    470    expr_vars
    471     (typ_of_type
    472         match optlen 
    473         in option 
    474         return λ_:(option ℕ).type with 
    475         [None⇒Tpointer ty'
    476         |Some (n':ℕ)⇒ Tarray ty' n']) e P.
    477 #ty' * normalize
    478 [ 2: #n ]
    479 #e #P
    480 @expr_vars_mp //
    481 qed.
    482 
    483 lemma eval_expr_rewrite_aux :
    484   ∀genv.
    485   ∀optlen.
    486   ∀ty'.
    487   ∀e.
    488   ∀cm_env.
    489   ∀H.
    490   ∀sp.
    491   ∀m.
    492   ∀res.
    493   (eval_expr genv
    494              (typ_of_type
    495                  match optlen in option return λ_:(option ℕ).type with 
    496                  [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
    497              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 →
    498    eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
    499 #genv * [ 2: #n ] normalize nodelta
    500 #ty' normalize in match (typ_of_type ?);
    501 #e #cm_env whd in match (fix_ptr_type ???);
    502 #H #sp #m #res #H @H
    503 qed.
    504 
    505 lemma sign_ext_sign_ext_reduce :
    506   ∀i. sign_ext 32 16 (sign_ext 16 32 i) = i.
    507 #i @refl
    508 qed. 
    509 
    510 lemma sign_ext_zero_ext_reduce :
    511   ∀i. sign_ext 32 16 (zero_ext 16 32 i) = i.
    512 #i @refl
    513 qed.
    514 
    515 (* There are two zero_ext, and this causes the "disambiguator" to fail. So we do
    516  * the cleanup ourselves. *)
    517 
    518 definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext.
    519 definition zero_ext_val : ∀target_sz:intsize. val → val ≝ zero_ext.
    520 
    521 (* CM code uses 8 bit constants and upcasts them to target_size, CL uses 32 bit and
    522  * downcasts them to target_size. In the end, these are equal. We directly state what
    523  * we need. *)
    524 lemma value_eq_cl_cm_true :
    525   ∀E,sz.
    526   value_eq E
    527     (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 1)))
    528     (zero_ext_val sz (Vint I8 (repr I8 1))).
    529 #E * %2 qed.
    530 
    531 lemma value_eq_cl_cm_false :
    532   ∀E,sz.
    533   value_eq E
    534     (Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 0)))
    535     (zero_ext_val sz (Vint I8 (repr I8 0))).
    536 #E * %2 qed.
    537 
    538 lemma exec_bool_of_val_inversion : ∀v,ty,b.
    539   exec_bool_of_val v ty = OK ? b →
    540   (∃sz,sg,i. v = Vint sz i ∧ ty = Tint sz sg ∧ b = (¬eq_bv (bitsize_of_intsize sz) i (zero (bitsize_of_intsize sz)))) ∨
    541   (∃ty'. v = Vnull ∧ ty = Tpointer ty' ∧ b = false) ∨
    542   (∃ptr,ty'. v = Vptr ptr ∧ ty = Tpointer ty' ∧ b = true).
    543 #v #ty #b #Hexec
    544 cases v in Hexec;
    545 [ | #vsz #i | | #p ]
    546 cases ty
    547 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
    548 | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
    549 | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
    550 | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
    551 whd in ⊢ ((??%%) → ?);
    552 #Heq destruct (Heq)
    553 [ 2: %1 %2 %{ptr_ty} @conj try @conj try @refl
    554 | 3: %2 %{p} %{ptr_ty}  @conj try @conj try @refl
    555 | 1: %1 %1 %{sz} %{sg} lapply Heq -Heq
    556      cases vsz in i; #i cases sz whd in ⊢ ((??%?) → ?);
    557      #Heq destruct %{i} @conj try @conj try @refl
    558 ] qed.     
    559 
    560 (* This lemma is noise I extracted from the proof below, even though it is used only once.
    561    Better that than an ugly cut.
    562    We need the following lemma to feed another one down in the deref case. In essence,
    563    it says that the variables present in a cminor expression resulting from converting
    564    a clight deref are transmitted to the cminor counterpart of the pointer argument.
    565    This is made messy by the fact that clight to cminor implements different deref
    566    strategies for different kind of variables.   
    567 *)
    568 lemma translate_expr_deref_present:
    569       ∀vars:var_types.
    570       ∀ptrdesc:expr_descr.
    571       ∀ptrty:type.
    572       ∀derefty:type.
    573       ∀cm_deref.
    574       ∀Hcm_deref.
    575       ∀cm_ptr.
    576       ∀Hcm_ptr.
    577       ∀cm_env:env.
    578         translate_expr vars (Expr (Ederef (Expr ptrdesc ptrty)) derefty) =OK ? «cm_deref,Hcm_deref» →
    579         expr_vars (typ_of_type derefty) cm_deref (λid:ident.λty0:typ.present SymbolTag ? cm_env id) →
    580         translate_expr vars (Expr ptrdesc ptrty) =OK ? «cm_ptr,Hcm_ptr» →
    581         expr_vars ? cm_ptr (λid:ident.λty0:typ.present SymbolTag ? cm_env id).
    582   #cut_vars #ptrdesc #ptrty #derefty
    583   cases ptrty
    584   [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
    585   | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
    586   #cut_cm_deref #Hcut_cm_deref #cut_cm_ptr #Hcut_cm_ptr #cut_cm_env
    587   whd in match (translate_expr ??);
    588   cases (translate_expr cut_vars (Expr ptrdesc ?)) normalize nodelta
    589   [ 1,2,3,4,6,8,10,11,12,13,14,16: #err #Habsurd destruct (Habsurd) ]
    590   normalize in match (typ_of_type ?);
    591   * #cut_e' #Hcut_local_e'
    592   lapply Hcut_cm_deref -Hcut_cm_deref lapply cut_cm_deref -cut_cm_deref
    593   cases (access_mode derefty) normalize nodelta
    594   [ #invert_ty | | #invert_ty
    595   | #invert_ty | | #invert_ty
    596   | #invert_ty | | #invert_ty
    597   | #invert_ty | | #invert_ty ]
    598   [ 3,6,9,12: #cut_cm_deref #Hcut_cm_deref #Habsurd destruct (Habsurd) ]
    599   #cut_cm_deref #Hcut_cm_deref #Heq destruct (Heq)
    600   [ 1,3,5,7: whd in ⊢ (% → ?); ]
    601   #Hgoal #Heq destruct @Hgoal
    602 qed.
    603 
    604 (* TODOs : there are some glitches between clight and cminor :
    605  * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
    606       in the shortcut case, the cminor code returns directly the outcome of the
    607       evaluated expr, with a possibly different size.
    608    2) another glitch is for the integer/pointer additions: Clight always performs
    609       a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
    610       the sign of i, producing either a sign extension or a zero extension.
    611    3) something similar to 1) happens for binary comparison operators. Clight generates
    612       systematically a 32 bit value for the outcome of the comparison and lives with it,
    613       but toCminor actually generates something 8 bit and casts it back to the context type.
    614    4) we need some proof that we don't blow the stack during the transformation. Otherwise,
    615       a problem appears when we prove semantics preservation for pointer < comparison
    616       (we might wrap up the rhs and end SNAFU).
    617  *)
    618  
     236
     237(* This is the statement for expression simulation copied fro toCminorCorrectnessExpr.ma,
     238   for easier reference.
    619239lemma eval_expr_sim :
    620240  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
     
    656276   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
    657277   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
    658             value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
    659 #inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
    660 @expr_lvalue_ind_combined
    661 [ 7: (* binary ops *)
    662      #ty
    663      #op #e1 #e2
    664      #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
    665      cases (bind_inversion ????? Htranslate) -Htranslate
    666      * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
    667      cases (bind_inversion ????? Htranslate) -Htranslate
    668      * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
    669      whd in ⊢ ((??%?) → ?);
    670      #Htranslate_binop
    671      cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
    672      #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    673      #cl_val #trace #Hyp_present #Hexec
    674      (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
    675      lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
    676      lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
    677      lapply Hyp_present -Hyp_present
    678      lapply Htranslate_lhs -Htranslate_lhs
    679      lapply Htranslate_rhs -Htranslate_rhs
    680      lapply Hexpr_vars_lhs -Hexpr_vars_lhs
    681      lapply Hexpr_vars_rhs -Hexpr_vars_rhs
    682      lapply Hexec -Hexec
    683      lapply Htranslated_binop -Htranslated_binop
    684      lapply rhs -rhs lapply lhs -lhs
    685      (* end of dump *)
    686      cases op
    687      whd in ⊢ (? → ? → (??%?) → ?);
    688      [ 1: (* add *)
    689        lapply (classify_add_inversion (typeof e1) (typeof e2))
    690        * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    691        (* trying to factorise as much stuff as possible ... *)
    692        lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
    693        * [ 1: * ]
    694        [ 1: * #sz * #sg * *
    695        | 2: * #optlen * #ty' * #sz * #sg * *
    696        | 3: * #optlen * #sz * #sg * #ty' * * ]
    697        whd in match (typeof ?) in ⊢ (% → % → ?);
    698        #Htypeof_e1 #Htypeof_e2
    699        >Htypeof_e1 >Htypeof_e2
    700        #Hclassify
    701        lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
    702        normalize nodelta
    703        whd in match (typeof ?) in ⊢ (% → % → %);
    704        whd in match (typ_of_type (Tint ??));
    705        #lhs #rhs #Htyp_should_eq
    706        [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
    707        | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
    708        -Htyp_should_eq
    709        #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
    710        <Heq_e' -Heq_e'
    711        #Hexec
    712        #Hexpr_vars_rhs #Hexpr_vars_lhs
    713        #Htranslate_rhs #Htranslate_lhs
    714        * [ #Hyp_present_lhs #Hyp_present_rhs
    715          | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
    716          | * #Hyp_present_lhs #Hyp_present_cst #Hyp_present_rhs ]
    717        whd in match (typeof ?);
    718        #Hind_rhs #Hind_lhs
    719        cases (bind_inversion ????? Hexec) -Hexec
    720        * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    721        cases (bind_inversion ????? Hexec) -Hexec
    722        * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    723        cases (bind_inversion ????? Hexec) -Hexec
    724        #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    725        lapply (opt_to_res_inversion ???? Hsem) -Hsem
    726        whd in match (typeof ?); whd in match (typeof ?);
    727        #Hsem_binary
    728        [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    729        | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
    730        * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    731        [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    732        | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
    733        * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    734        whd in match (eval_expr ???????);
    735        whd in match (proj1 ???);
    736        [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
    737        [ 1,2: >Heval_lhs normalize nodelta
    738               whd in match (eval_expr ???????);
    739               whd in match (eval_expr ???????);
    740               >Heval_rhs normalize nodelta
    741               whd in match (m_bind ?????);
    742        | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
    743             whd in match (eval_expr ???????);
    744             whd in match (eval_expr ???????);
    745             >Heval_lhs normalize nodelta
    746        ]
    747        whd in match (proj1 ???); whd in match (proj2 ???);
    748        [ 2: (* standard int/int addition. *)
    749             whd in match (eval_binop ???????);
    750             whd in Hsem_binary:(??%?);
    751             lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    752             * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    753             cases (sem_add_ii_inversion … Hsem_binary_translated)
    754             #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
    755             #Hcm_lhs #Hcm_rhs #Hcm_val
    756             destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
    757             >intsize_eq_elim_true normalize nodelta
    758             %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
    759             @conj try @refl lapply Hsem_binary_translated
    760             whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
    761             >inttyp_eq_elim_true' normalize nodelta
    762             >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
    763        | *: (* pointer/int int/pointer addition *)
    764             whd in Hsem_binary:(??%?);
    765             lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    766             * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    767             (* >> *)             
    768             [ lapply (sem_add_pi_inversion … Hsem_binary_translated)
    769               * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
    770               [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
    771               | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
    772             | lapply (sem_add_ip_inversion … Hsem_binary_translated)
    773               * #cm_vsz * #cm_lhs_v * #Hcm_lhs *
    774               [ * #rhs_ptr * #Hcm_rhs_ptr #Hcm_val_shptr
    775               | * * #rhs_null #Hcm_lhs_zero #Hcm_val_null ]
    776             ]
    777             destruct
    778             whd in match (eval_unop ????);
    779             @(match sg
    780               return λs. sg = s → ?
    781               with
    782               [ Unsigned ⇒ λHsg. ?
    783               | Signed ⇒ λHsg. ?
    784               ] (refl ??)) normalize nodelta
    785             whd in match (eval_binop ???????);
    786             whd in match (m_bind ?????);
    787             [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
    788                             (short_multiplication (bitsize_of_intsize I16)
    789                             (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
    790                             (repr I16 (sizeof ty')))))}
    791             | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
    792                           (short_multiplication (bitsize_of_intsize I16)
    793                           (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
    794                           (repr I16 (sizeof ty')))))}
    795             | 5: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
    796                           (short_multiplication (bitsize_of_intsize I16)
    797                           (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
    798                           (repr I16 (sizeof ty')))))}
    799             | 6: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
    800                           (short_multiplication (bitsize_of_intsize I16)
    801                           (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
    802                           (repr I16 (sizeof ty')))))}
    803             ]
    804             [ 1,2,3,4: @conj whd in match (E0);
    805                         whd in match (Eapp trace_rhs ?);
    806                         whd in match (Eapp trace_lhs ?);
    807                         >(append_nil … trace_rhs) try @refl
    808                         >(append_nil … trace_lhs) try @refl
    809                         @(value_eq_triangle_diagram … Hvalue_eq_res)
    810                         whd in match (shift_pointer_n ?????);
    811                         whd in match (shift_offset_n ?????);
    812                         >Hsg normalize nodelta
    813                         >commutative_short_multiplication
    814                         whd in match (shift_pointer ???);
    815                         whd in match (shift_offset ???);
    816                         >sign_ext_same_size @refl
    817            | 5,7: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
    818            | 6,8: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]           
    819            >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
    820            >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
    821            normalize >append_nil try @refl
    822        ]
    823      | 2: (* subtraction cases: not quite identical to add. *)
    824        lapply (classify_sub_inversion (typeof e1) (typeof e2))
    825        * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    826        lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
    827        * [ 1: * ]
    828        [ 1: * #sz * #sg * *
    829        | 2: * #optlen * #ty' * #sz * #sg * *
    830        | 3: * #t1 * #t2 * #n1 * #n2 * * ]
    831        whd in match (typeof ?) in ⊢ (% → % → ?);
    832        #Htypeof_e1 #Htypeof_e2
    833        >Htypeof_e1 >Htypeof_e2
    834        #Hclassify
    835        lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
    836        normalize nodelta
    837        whd in match (typeof ?) in ⊢ (% → % → %);
    838        whd in match (typ_of_type (Tint ??));
    839        #lhs #rhs
    840        [ 1: #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
    841             -Htyp_should_eq
    842        | 2: #Htyp_should_eq cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq)
    843             -Htyp_should_eq
    844        | 3: #Haux cases (match_type_inversion_aux … Haux) #ty_sz * #ty_sg * -Haux
    845             #Hty_eq #Heq_aux destruct (Hty_eq) lapply (jmeq_to_eq ??? Heq_aux) -Heq_aux
    846             #Heq_e' destruct (Heq_e') ]
    847        [ 1,2: #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
    848               <Heq_e' -Heq_e' | ]
    849        #Hexec
    850        #Hexpr_vars_rhs #Hexpr_vars_lhs
    851        #Htranslate_rhs #Htranslate_lhs
    852        * [ #Hyp_present_lhs #Hyp_present_rhs
    853          | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
    854          | * #Hyp_present_lhs #Hyp_present_rhs #Hyp_present_cst ]
    855        whd in match (typeof ?);
    856        #Hind_rhs #Hind_lhs
    857        cases (bind_inversion ????? Hexec) -Hexec
    858        * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    859        cases (bind_inversion ????? Hexec) -Hexec
    860        * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    861        cases (bind_inversion ????? Hexec) -Hexec
    862        #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    863        lapply (opt_to_res_inversion ???? Hsem) -Hsem
    864        whd in match (typeof ?); whd in match (typeof ?);
    865        #Hsem_binary
    866        whd in match (eval_expr ???????);
    867        whd in match (proj1 ???);
    868        whd in match (eval_expr ???????);
    869        whd in match (eval_expr ???????);
    870        whd in match (proj1 ???);
    871        [ 1: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    872        | 2,3: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
    873        * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    874        [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    875        | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
    876        * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    877        [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
    878        [ 1,2: >Heval_lhs normalize nodelta
    879               whd in match (eval_expr ???????);
    880               whd in match (eval_expr ???????);
    881               whd in match (proj2 ???);
    882               [ >(eval_expr_rewrite_aux … Heval_rhs)
    883               | >Heval_rhs ]
    884               whd in match (m_bind ?????);
    885               normalize nodelta
    886        | 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    887             whd in match (eval_expr ???????);
    888             whd in match (proj2 ???);
    889             whd in match (eval_expr ???????);
    890             whd in match (proj1 ???);
    891             whd in match (eval_expr ???????);
    892             >Heval_rhs normalize nodelta
    893             whd in match (eval_unop ????);
    894        ]
    895        [ 1:       
    896         (* ptr/ptr sub *)
    897             whd in Hsem_binary:(??%?);
    898             lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    899             -Hsem_binary
    900             * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    901             lapply (sem_sub_pp_inversion … Hsem_binary_translated)
    902             * #ty_sz' * #ty_sg' * #Heq destruct (Heq) *
    903             [ (* regular pointers case *)
    904               * #lhs_ptr * #rhs_ptr * #resulting_offset * * * *
    905               #Hcm_lhs #Hcm_rhs #Hblocks_eq #Hoffset_eq #Hcm_val_eq
    906               whd in match (eval_binop ???????);
    907               >Hcm_lhs >Hcm_rhs normalize nodelta >Hblocks_eq >eq_block_b_b
    908               normalize nodelta
    909               whd in match (eval_expr ???????);
    910               whd in match (m_bind ?????);
    911               whd in match (eval_binop ???????);
    912               normalize in match (bitsize_of_intsize ?);
    913               normalize in match (S (7+pred_size_intsize I16*8)) in Hoffset_eq;
    914               >Hoffset_eq
    915               (* whd in match (pred_size_intsize ?); normalize in match (7+1*8); *)
    916               (* size mismatch between CL and CM. TODO *)
    917               >Hoffset_eq normalize nodelta
    918               whd in match (eval_unop ????);
    919               %{cm_val} >Hcm_val_eq
    920               whd in match (opt_to_res ???);
    921               whd in match (m_bind ?????); @conj
    922               [ 2: destruct assumption
    923               | 1: whd in match (zero_ext ? (Vint ??));
    924                    whd in match E0; whd in match (Eapp ? []); >append_nil
    925                    normalize in match (bitsize_of_intsize ?); try @refl ]
    926             | (* null pointers case *)
    927               * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct
    928               whd in match (eval_binop ???????); normalize nodelta
    929               whd in match (eval_expr ???????);
    930               whd in match (m_bind ?????);
    931               whd in match (eval_binop ???????); normalize nodelta
    932               >division_u_zero normalize nodelta
    933               whd in match (eval_unop ????);
    934               whd in match (opt_to_res ???);
    935               whd in match (m_bind ?????);
    936               whd in match (pred_size_intsize ?);
    937               %{(zero_ext ty_sz' (Vint I32 (zero (S (7+3*8)))))} @conj
    938               [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ]
    939               whd in Hsem_binary_translated:(??%?);
    940               normalize nodelta in Hsem_binary_translated:(??%?);
    941               lapply Hsem_binary_translated; -Hsem_binary_translated
    942               cases n1 cases n2
    943               [ | 2,3: #n | #n1 #n2 ] normalize nodelta
    944               #Heq destruct (Heq)
    945               whd in match (zero_ext ??);
    946               cases ty_sz' in Hvalue_eq_res; try //
    947             ]
    948        | 2: (* int/int sub *)
    949             whd in match (eval_binop ???????);
    950             whd in Hsem_binary:(??%?);
    951             lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    952             * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    953             cases (sem_sub_ii_inversion … Hsem_binary_translated)
    954             #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
    955             #Hcm_lhs #Hcm_rhs #Hcm_val
    956             destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
    957             >intsize_eq_elim_true normalize nodelta
    958             %{(Vint cm_vsz (subtraction (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
    959             @conj try @refl lapply Hsem_binary_translated
    960             whd in ⊢ ((??%?) → ?); normalize nodelta whd in match (classify_sub ??);
    961             >type_eq_dec_true normalize nodelta
    962             >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
    963        | 3: (* ptr/int sub *)
    964             whd in Hsem_binary:(??%?);
    965             lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary
    966             * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    967             lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated
    968             * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
    969             [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
    970             | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
    971             whd in match (eval_unop ????);
    972             -Heval_lhs -Heval_rhs destruct
    973             whd in match (proj2 ???);
    974             whd in match (proj1 ???);
    975             whd in match (proj2 ???);           
    976             whd in match (eval_expr ???????);
    977             @(match sg
    978               return λs. sg = s → ?
    979               with
    980               [ Unsigned ⇒ λHsg. ?
    981               | Signed ⇒ λHsg. ?
    982               ] (refl ??)) normalize nodelta
    983             whd in match (eval_unop ????);
    984             whd in match (m_bind ?????);
    985             whd in match (eval_binop ???????);
    986             [ 1,2:
    987                whd in match (neg_shift_pointer_n ?????) in Hvalue_eq_res;
    988                whd in match (neg_shift_offset_n ?????) in Hvalue_eq_res;
    989                whd in match (neg_shift_pointer ???);
    990                whd in match (neg_shift_offset ???);
    991                destruct (Hsg) normalize nodelta in Hvalue_eq_res;
    992                [ >sign_ext_sign_ext_reduce
    993                  %{(Vptr
    994                      (mk_pointer (pblock lhs_ptr)
    995                       (mk_offset
    996                          (subtraction offset_size (offv (poff lhs_ptr))
    997                            (short_multiplication (bitsize_of_intsize I16)
    998                               (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
    999                                  (repr I16 (sizeof ty')))))))}
    1000                   @conj
    1001                   [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
    1002                   | >commutative_short_multiplication @Hvalue_eq_res ]
    1003                | >sign_ext_zero_ext_reduce
    1004                  %{(Vptr
    1005                      (mk_pointer (pblock lhs_ptr)
    1006                       (mk_offset
    1007                          (subtraction offset_size (offv (poff lhs_ptr))
    1008                            (short_multiplication (bitsize_of_intsize I16)
    1009                               (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
    1010                                  (repr I16 (sizeof ty')))))))}
    1011                  @conj
    1012                   [ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
    1013                   | >commutative_short_multiplication @Hvalue_eq_res ]
    1014               ]                         
    1015             ]
    1016             [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
    1017               >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
    1018               >(sign_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32))
    1019             | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
    1020               >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
    1021               >(zero_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32)) ]
    1022             >(eq_bv_true … (zero 32)) normalize nodelta
    1023            %{Vnull} @conj try assumption
    1024            normalize >append_nil try @refl
    1025        ]     
    1026      | 3: (* mul *)
    1027        lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
    1028        [ 2,4: #Hclassify >Hclassify normalize nodelta
    1029             #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    1030        lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
    1031        whd in match (typeof ?); #e'
    1032        * #sz * #sg * *
    1033        whd in match (typeof ?) in ⊢ (% → % → ?);
    1034        #Htypeof_e1 #Htypeof_e2
    1035        >Htypeof_e1 >Htypeof_e2
    1036        whd in match (typeof ?) in ⊢ (% → % → % → ?);
    1037        #Hclassify
    1038        lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
    1039        normalize nodelta
    1040        whd in match (typ_of_type (Tint ??));
    1041        #lhs #rhs #Htyp_should_eq
    1042        cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
    1043        -Htyp_should_eq
    1044        #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
    1045        <Heq_e' -Heq_e'
    1046        #Hexec
    1047        #Hexpr_vars_rhs #Hexpr_vars_lhs
    1048        #Htranslate_rhs #Htranslate_lhs
    1049        * #Hyp_present_lhs #Hyp_present_rhs
    1050        #Hind_rhs #Hind_lhs
    1051        cases (bind_inversion ????? Hexec) -Hexec
    1052        * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    1053        cases (bind_inversion ????? Hexec) -Hexec
    1054        * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    1055        cases (bind_inversion ????? Hexec) -Hexec
    1056        #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1057        lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1058        whd in match (typeof ?); whd in match (typeof ?);
    1059        #Hsem_binary
    1060        lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    1061        * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    1062        lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    1063        * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1064        whd in match (eval_expr ???????);
    1065        whd in match (proj1 ???);
    1066        >Heval_lhs normalize nodelta
    1067        >Heval_rhs normalize nodelta
    1068        whd in match (m_bind ?????);
    1069        whd in match (eval_binop ???????);
    1070        whd in Hsem_binary:(??%?);
    1071        lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1072        * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1073        cases (sem_mul_inversion … Hsem_binary)
    1074        #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
    1075        #Hcm_lhs #Hcm_rhs #Hcm_val
    1076        destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
    1077        >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
    1078        >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    1079        >intsize_eq_elim_true normalize nodelta
    1080        %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
    1081        @conj try @refl
    1082        whd in Hsem_binary:(??%?);     
    1083        whd in match (classify_aop ??) in Hsem_binary:(??%?);
    1084        >type_eq_dec_true in Hsem_binary; normalize nodelta
    1085        >intsize_eq_elim_true #Heq destruct (Heq)
    1086        %2
    1087      | 4,5: (* div *)
    1088        lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
    1089        [ 2,4: #Hclassify >Hclassify normalize nodelta
    1090             #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    1091        lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
    1092        whd in match (typeof ?); #e'
    1093        * #sz * * * *
    1094        whd in match (typeof ?) in ⊢ (% → % → ?);
    1095        #Htypeof_e1 #Htypeof_e2
    1096        >Htypeof_e1 >Htypeof_e2
    1097        whd in match (typeof ?) in ⊢ (% → % → % → ?);
    1098        #Hclassify
    1099        lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
    1100        normalize nodelta
    1101        whd in match (typ_of_type (Tint ??));
    1102        #lhs #rhs #Htyp_should_eq
    1103        [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
    1104        | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
    1105        -Htyp_should_eq
    1106        #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
    1107        <Heq_e' -Heq_e'
    1108        #Hexec
    1109        #Hexpr_vars_rhs #Hexpr_vars_lhs
    1110        #Htranslate_rhs #Htranslate_lhs
    1111        * #Hyp_present_lhs #Hyp_present_rhs
    1112        #Hind_rhs #Hind_lhs
    1113        cases (bind_inversion ????? Hexec) -Hexec
    1114        * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    1115        cases (bind_inversion ????? Hexec) -Hexec
    1116        * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    1117        cases (bind_inversion ????? Hexec) -Hexec
    1118        #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1119        lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1120        whd in match (typeof ?); whd in match (typeof ?);
    1121        #Hsem_binary
    1122        lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    1123        * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    1124        lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    1125        * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1126        whd in match (eval_expr ???????);
    1127        whd in match (proj1 ???);
    1128        >Heval_lhs normalize nodelta
    1129        >Heval_rhs normalize nodelta
    1130        whd in match (m_bind ?????);
    1131        whd in match (eval_binop ???????);
    1132        whd in Hsem_binary:(??%?);
    1133        [ 1,3: (* div*)
    1134           lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1135           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1136           [ cases (sem_div_inversion_s … Hsem_binary)
    1137           | cases (sem_div_inversion_u … Hsem_binary) ]
    1138        | 2,4: (* mod *)
    1139           lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1140           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1141           [ cases (sem_mod_inversion_s … Hsem_binary)
    1142           | cases (sem_mod_inversion_u … Hsem_binary) ]
    1143        ]
    1144        #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
    1145        #Hcm_lhs #Hcm_rhs #Hcm_val
    1146        destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
    1147        >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
    1148        >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    1149        >intsize_eq_elim_true normalize nodelta
    1150        [ cases (division_s ???) in Hcm_val;
    1151        | cases (division_u ???) in Hcm_val;
    1152        | cases (modulus_s ???) in Hcm_val;
    1153        | cases (modulus_u ???) in Hcm_val; ]
    1154        normalize nodelta
    1155        [ 1,3,5,7: @False_ind ]
    1156        #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
    1157      | 6,7,8: (* and,or,xor *)
    1158        lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
    1159        [ 2,4,6: #Hclassify >Hclassify normalize nodelta
    1160             #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    1161        lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
    1162        whd in match (typeof ?); #e'
    1163        * #sz * #sg * *
    1164        whd in match (typeof ?) in ⊢ (% → % → ?);
    1165        #Htypeof_e1 #Htypeof_e2
    1166        >Htypeof_e1 >Htypeof_e2
    1167        whd in match (typeof ?) in ⊢ (% → % → % → ?);
    1168        #Hclassify
    1169        lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
    1170        normalize nodelta
    1171        whd in match (typ_of_type (Tint ??));
    1172        #lhs #rhs #Htyp_should_eq
    1173        cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
    1174        -Htyp_should_eq
    1175        #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
    1176        <Heq_e' -Heq_e'
    1177        #Hexec
    1178        #Hexpr_vars_rhs #Hexpr_vars_lhs
    1179        #Htranslate_rhs #Htranslate_lhs
    1180        * #Hyp_present_lhs #Hyp_present_rhs
    1181        #Hind_rhs #Hind_lhs
    1182        cases (bind_inversion ????? Hexec) -Hexec
    1183        * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    1184        cases (bind_inversion ????? Hexec) -Hexec
    1185        * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    1186        cases (bind_inversion ????? Hexec) -Hexec
    1187        #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1188        lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1189        whd in match (typeof ?); whd in match (typeof ?);
    1190        #Hsem_binary
    1191        lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    1192        * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    1193        lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    1194        * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1195        whd in match (eval_expr ???????);
    1196        whd in match (proj1 ???);
    1197        >Heval_lhs normalize nodelta
    1198        >Heval_rhs normalize nodelta
    1199        whd in match (m_bind ?????);
    1200        whd in match (eval_binop ???????);
    1201        whd in Hsem_binary:(??%?);
    1202        [ 1: (* and *)
    1203           lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1204            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1205           cases (sem_and_inversion … Hsem_binary)
    1206        | 2: (* or *)
    1207           lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1208            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1209           cases (sem_or_inversion … Hsem_binary)
    1210        | 3: (* xor *)
    1211           lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1212            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1213           cases (sem_xor_inversion … Hsem_binary)
    1214        ]
    1215        #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
    1216        #Hcm_lhs #Hcm_rhs #Hcm_val
    1217        destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
    1218        >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
    1219        >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    1220        >intsize_eq_elim_true normalize nodelta
    1221        [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
    1222        | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
    1223        | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
    1224        ]
    1225        @conj try @refl >Hcm_val %2
    1226      | 9,10: (* shl, shr *)
    1227        lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
    1228        [ 2,4: #Hclassify >Hclassify normalize nodelta
    1229             #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    1230        lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
    1231        whd in match (typeof ?); #e'
    1232        * #sz * * * *
    1233        whd in match (typeof ?) in ⊢ (% → % → ?);
    1234        #Htypeof_e1 #Htypeof_e2
    1235        >Htypeof_e1 >Htypeof_e2
    1236        whd in match (typeof ?) in ⊢ (% → % → % → ?);
    1237        #Hclassify
    1238        lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
    1239        normalize nodelta
    1240        whd in match (typ_of_type (Tint ??));
    1241        #lhs #rhs #Htyp_should_eq
    1242        [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
    1243        | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
    1244        -Htyp_should_eq
    1245        #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
    1246        <Heq_e' -Heq_e'
    1247        #Hexec
    1248        #Hexpr_vars_rhs #Hexpr_vars_lhs
    1249        #Htranslate_rhs #Htranslate_lhs
    1250        * #Hyp_present_lhs #Hyp_present_rhs
    1251        #Hind_rhs #Hind_lhs
    1252        cases (bind_inversion ????? Hexec) -Hexec
    1253        * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    1254        cases (bind_inversion ????? Hexec) -Hexec
    1255        * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    1256        cases (bind_inversion ????? Hexec) -Hexec
    1257        #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1258        lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1259        whd in match (typeof ?); whd in match (typeof ?);
    1260        #Hsem_binary
    1261        lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    1262        * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    1263        lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    1264        * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1265        whd in match (eval_expr ???????);
    1266        whd in match (proj1 ???);
    1267        >Heval_lhs normalize nodelta
    1268        >Heval_rhs normalize nodelta
    1269        whd in match (m_bind ?????);
    1270        whd in match (eval_binop ???????);
    1271        whd in Hsem_binary:(??%?);
    1272        [ 1,3: (* shl *)
    1273           lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1274           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1275           cases (sem_shl_inversion … Hsem_binary)
    1276           #sz1 * #sz2 * #lhs_i * #rhs_i * * *
    1277           #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
    1278           destruct (Hcl_lhs Hcl_rhs)
    1279           >(value_eq_int_inversion … Hvalue_eq_lhs)
    1280           >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    1281           >Hshift_ok normalize nodelta
    1282           %{(Vint sz1
    1283                (shift_left bool (bitsize_of_intsize sz1)
    1284                (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
    1285           @conj try @refl >Hcl_val %2
    1286        | *: (* shr, translated to mod /!\ *)     
    1287           lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
    1288           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1289           cases (sem_shr_inversion … Hsem_binary) normalize nodelta
    1290           #sz1 * #sz2 * #lhs_i * #rhs_i * * *
    1291           #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
    1292           destruct (Hcl_lhs Hcl_rhs)
    1293           >(value_eq_int_inversion … Hvalue_eq_lhs)
    1294           >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    1295           >Hshift_ok normalize nodelta >Hcl_val
    1296           /3 by ex_intro, conj, vint_eq/ ]
    1297      | *: (* comparison operators *)
    1298        lapply e' -e'
    1299        cases e1 #ed1 #ety1
    1300        cases e2 #ed2 #ety2
    1301        whd in match (typeof ?) in ⊢ (% → % → % → %);
    1302        #cm_expr whd in match (typeof ?);
    1303        inversion (classify_cmp ety1 ety2)
    1304        [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
    1305             lapply (jmeq_to_eq ??? Hety1) #Hety1'
    1306             lapply (jmeq_to_eq ??? Hety1) #Hety2'
    1307             destruct #Hclassify >Hclassify normalize nodelta
    1308             #cmexpr1 #cmexpr2
    1309             whd in ⊢ ((???%) → ?);
    1310             #Heq destruct (Heq)
    1311        | 1,4,7,10,13,16:
    1312             #sz #sg #Hety1 #Hety2 #Hclassify
    1313             lapply (jmeq_to_eq ??? Hety1) #Hety1'
    1314             lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
    1315             >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
    1316             whd in match (typeof ?) in ⊢ (% → % → % → %);
    1317             whd in match (typ_of_type ?) in ⊢ (% → % → ?);
    1318             cases sg #cmexpr1 #cmexpr2 normalize nodelta
    1319             #Hcast_to_bool #Hexec_expr
    1320             cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
    1321             #tysz * #tysg * #Htyis_int #Hcm_expr_aux
    1322             destruct (Htyis_int)
    1323             lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
    1324             destruct (Hcm_expr)
    1325             cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    1326             * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    1327             cases (bind_inversion ????? Hexec) -Hexec
    1328             * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    1329             cases (bind_inversion ????? Hexec) -Hexec
    1330             #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1331             lapply (opt_to_res_inversion ???? Hsem) -Hsem           
    1332             whd in match (typeof ?); whd in match (sem_binary_operation ???????);
    1333             normalize nodelta
    1334             #Hsem_cmp cases (some_inversion ????? Hsem_cmp) -Hsem_cmp
    1335             #cl_val' * #Hsem_cmp #Hcl_val_cast
    1336             destruct (Hcl_val_cast)
    1337             lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
    1338             * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
    1339             destruct (Hcl_lhs) destruct (Hcl_rhs)
    1340             #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
    1341             #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
    1342             * #Hyp_present_lhs #Hyp_present_rhs
    1343             #Hind_rhs #Hind_lhs
    1344             lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
    1345             * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
    1346             lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
    1347             * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1348             whd in match (eval_expr ???????);
    1349             whd in match (eval_expr ???????);
    1350             >Heval_lhs normalize nodelta
    1351             >Heval_rhs normalize nodelta
    1352             whd in match (m_bind ?????);
    1353             whd in match (eval_binop ???????);
    1354             >(value_eq_int_inversion … Hvalue_eq_lhs)
    1355             >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
    1356             >intsize_eq_elim_true normalize nodelta
    1357             destruct (Heq_bool)
    1358             whd in match (eval_unop ????);
    1359             whd in match (opt_to_res ???);
    1360             whd in match (m_bind ?????);
    1361             whd in match (of_bool ?);
    1362             [ %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
    1363             | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
    1364             | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
    1365             | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
    1366             | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
    1367             | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
    1368             | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
    1369             | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
    1370             | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
    1371             | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
    1372             | %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))}
    1373             | %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))} ]
    1374             @conj try @refl
    1375             whd in match (FE_of_bool ?); whd in match FEtrue; whd in match FEfalse;
    1376             [ 1,3,5,7,9,11:
    1377               cases (cmp_int ????) normalize nodelta
    1378             | *:
    1379               cases (cmpu_int ????) normalize nodelta ]           
    1380             try @value_eq_cl_cm_true
    1381             try @value_eq_cl_cm_false
    1382        | *: (* ptr comparison *)
    1383             #n #ty' #Hety1 #Hety2 #Hclassify
    1384             lapply (jmeq_to_eq ??? Hety1) #Hety1'
    1385             lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
    1386             >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
    1387             whd in match (typeof ?) in ⊢ (% → % → % → %);
    1388             #cmexpr1 #cmexpr2
    1389             #Hcast_to_bool #Hexec_expr
    1390             cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
    1391             #tysz * #tysg * #Htyis_int #Hcm_expr_aux
    1392             destruct (Htyis_int)
    1393             lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
    1394             destruct (Hcm_expr)
    1395             cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    1396             * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
    1397             cases (bind_inversion ????? Hexec) -Hexec
    1398             * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
    1399             cases (bind_inversion ????? Hexec) -Hexec
    1400             #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1401             lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1402             whd in match (typeof ?); whd in match (sem_binary_operation ???????);
    1403             #Hsem_cmp
    1404             cases (some_inversion ????? Hsem_cmp) -Hsem_cmp normalize nodelta
    1405             #cl_val' * #Hsem_cmp #Hcl_val_cast destruct (Hcl_val_cast);
    1406             #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
    1407             * #Hyp_present_lhs #Hyp_present_rhs
    1408             #Hind_rhs #Hind_lhs
    1409             lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
    1410             * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs -Hexec_rhs
    1411             lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
    1412             * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs -Hexec_lhs
    1413             lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp) -Hsem_cmp
    1414             -Hvalue_eq_lhs -Hvalue_eq_rhs
    1415             * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res
    1416             whd in match (eval_expr ???????);
    1417             whd in match (eval_expr ???????);
    1418             >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    1419             >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
    1420             whd in match (m_bind ?????);           
    1421             lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm
    1422             *
    1423             [ 2,4,6,8,10,12:
    1424               * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
    1425               whd in Hsem_cmp:(??%?); destruct
    1426             | *: *
    1427               [ 2,4,6,8,10,12:
    1428                 * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
    1429                 whd in Hsem_cmp:(??%?); destruct
    1430               | *: *
    1431                 [ 2,4,6,8,10,12:
    1432                   * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
    1433                   whd in Hsem_cmp:(??%?); destruct
    1434                 | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome
    1435                      whd in Hsem_cmp:(??%?); destruct
    1436                 ]
    1437               ]
    1438             ]
    1439             whd in match (eval_binop ???????);
    1440             normalize nodelta
    1441             whd in match (eval_unop ????);
    1442             whd in match (opt_to_res ???);
    1443             whd in match (m_bind ?????);
    1444             [ 1,2,3,4,5,6:
    1445               [ 1,4,6:
    1446                 %{(zero_ext tysz FEtrue)} @conj try @refl
    1447                 >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
    1448                 @value_eq_cl_cm_true
    1449               | 2,3,5:
    1450                 %{(zero_ext tysz FEfalse)} @conj try @refl
    1451                 >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
    1452                 @value_eq_cl_cm_false
    1453               ]
    1454             | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
    1455                  lapply Heq_block_outcome -Heq_block_outcome
    1456                  @(eq_block_elim … (pblock p1) (pblock p2))
    1457                  normalize nodelta
    1458                  whd in match (eval_unop ????);
    1459                  whd in match (opt_to_res ???);
    1460                  whd in match (m_bind ?????);
    1461                  [ 1,3,5,7,9,11:
    1462                    #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
    1463                    whd in match (eval_unop ????);
    1464                    whd in match (m_bind ?????);
    1465                    cases (cmp_offset ???) in Hvalue_eq_res; normalize nodelta
    1466                    #Hvalue_eq_res >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
    1467                    [ 1,3,5,7,9,11: %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
    1468                                    @value_eq_cl_cm_true
    1469                    | 2,4,6,8,10,12: %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
    1470                                     @value_eq_cl_cm_false
    1471                    ]
    1472                  | *:
    1473                    #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    1474                    >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
    1475                    [ %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
    1476                      @value_eq_cl_cm_false
    1477                    | %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
    1478                      @value_eq_cl_cm_true
    1479                    ]
    1480                 ]
    1481            ]
    1482        ]
    1483     ]
    1484 
    1485 | 1: (* Integer constant *)
    1486   #csz #ty cases ty
    1487   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1488   | #structname #fieldspec | #unionname #fieldspec | #id ]
    1489   #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
    1490   #val #trace #Hpresent #Hexec_cl
    1491   whd in Htranslate:(??%?);
    1492   [ 1,3,4,5,6,7,8: destruct ]
    1493   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))))
    1494   [ 2: * #H_err #H_neq_sz
    1495        lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
    1496        >Htranslate #Habsurd destruct (Habsurd) ]
    1497   * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
    1498   destruct (Heq_sz)
    1499   >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
    1500   whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
    1501   #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
    1502 | 2: *
    1503   [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
    1504   | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    1505   try /2 by I/
    1506   #ty whd in ⊢ (% → ?); #Hind
    1507   whd in match (Plvalue ???);
    1508   whd in match (typeof ?);
    1509   #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
    1510   whd in Hexec:(??%?);
    1511   whd in match (exec_lvalue' ?????) in Hexec:(??%?);
    1512   cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
    1513   whd in Hcl_success:(???%);
    1514   [ 1: (* var case *)
    1515        lapply Hcl_success -Hcl_success -Hind
    1516        (* Peform case analysis on presence of variable in local Clight env.
    1517         * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
    1518        @(match lookup SymbolTag block cl_env var_id
    1519          return λx.(lookup SymbolTag block cl_env var_id = x) → ?
    1520          with
    1521          [ None ⇒ λHcl_lookup. ?
    1522          | Some loc ⇒ λHcl_lookup. ?
    1523          ] (refl ? (lookup SymbolTag block cl_env var_id)))
    1524        normalize nodelta
    1525        [ 1: (* global case *)
    1526             #Hlookup_global
    1527             cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
    1528             * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
    1529             #Heq whd in Heq:(???%); destruct (Heq)
    1530             lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
    1531             * #var_id_alloctype * #var_id_type * #Heq
    1532             cases (variable_not_in_env_but_in_vartypes_is_global …
    1533                         Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
    1534             #r #Heq' destruct (Heq') normalize nodelta
    1535             lapply Hcl_load_success -Hcl_load_success
    1536             lapply Hyp_present -Hyp_present
    1537             lapply Hexpr_vars -Hexpr_vars
    1538             lapply cm_expr -cm_expr inversion (access_mode ty)
    1539             [ #typ_of_ty | | #typ_of_ty ]
    1540             #Heq_typ_of_type #Heq_access_mode
    1541             #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
    1542             whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1543             whd in match (eval_expr ???????);
    1544             whd in match (eval_expr ???????);
    1545             whd in match (eval_constant ????);
    1546             <(eq_sym … inv) >Hfind_symbol normalize nodelta
    1547             cases (bind_inversion ????? Hcl_load_success) #x *
    1548             #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
    1549             lapply (opt_to_res_inversion ???? Hopt_to_res)
    1550             #Hcl_load_success
    1551             [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
    1552                  @conj try @refl
    1553                  whd in Hcm_load_success:(??%?);
    1554                  lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
    1555                  >(load_value_of_type_by_ref … Hcl_load_success)
    1556                  try assumption %4
    1557                  lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
    1558                  >Hfind_symbol normalize nodelta #Heq_embedding
    1559                  whd in match (shift_offset ???);
    1560                  >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
    1561                  normalize nodelta @refl
    1562             | 1: cut (access_mode ty=By_value (typ_of_type ty))
    1563                  [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
    1564                    lapply Heq_access_mode <Heqt // ] #Haccess
    1565                  lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
    1566                  #Hvalid_ptr
    1567                  lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
    1568                  [ whd in ⊢ (??%?);
    1569                    lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
    1570                    >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
    1571                  * #val' * #Hcm_load_success #Hvalue_eq
    1572                  lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
    1573                  #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
    1574                  normalize %{val'} @conj try @refl assumption ]
    1575        | 2: (* local case *)
    1576             #Heq destruct (Heq)
    1577             lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
    1578             * #var_id_alloc_type * #var_id_type *
    1579             generalize in match var_id_alloc_type; * normalize nodelta
    1580             [ 1: #r #Hlookup_vartype
    1581                  lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
    1582                  * #typ whd in match (local_id ???);
    1583                  >Hlookup_vartype normalize nodelta @False_ind
    1584             | 2: (* Stack local *)
    1585                  lapply Hcl_load_success -Hcl_load_success
    1586                  lapply Hyp_present -Hyp_present
    1587                  lapply Hexpr_vars -Hexpr_vars
    1588                  lapply cm_expr -cm_expr inversion (access_mode ty)
    1589                  [ #typ_of_ty | | #typ_of_ty ]
    1590                  #Heq_typ_of_type #Heq_access_mode
    1591                  #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
    1592                  #stack_depth #Hlookup_vartype_success normalize nodelta
    1593                  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1594                  lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
    1595                  cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
    1596                  * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
    1597                  >Hlookup' normalize nodelta #Hembedding_eq
    1598                  cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
    1599                  #loaded_val * #Hload_val
    1600                  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1601                  lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
    1602                  #Hload_success whd in match (eval_expr ???????);
    1603                  cut (pointer_translation (mk_pointer cl_b zero_offset) E =
    1604                       Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
    1605                  [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
    1606                         >offset_plus_0 @refl ]
    1607                  #Hpointer_translation
    1608                  [ 2: (* By-ref *)
    1609                       whd in Hload_success:(??%?);
    1610                       lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
    1611                       #Heq_val
    1612                       >Heq_val
    1613                       %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
    1614                       @conj try @refl
    1615                       %4 whd in match (shift_offset ???);
    1616                       whd in match zero_offset;
    1617                       >commutative_addition_n >addition_n_0 @Hpointer_translation
    1618                  | 1: (* By value *)
    1619                       lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
    1620                       lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
    1621                       [ @(load_by_value_success_valid_pointer … Hload_success)
    1622                         lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
    1623                       * #cm_val * #Hload_in_cm #Hvalue_eq
    1624                       %{cm_val} @conj try assumption
    1625                       lapply (load_value_of_type_by_value … Hload_in_cm)
    1626                       [ lapply Heq_access_mode <Heq0 #Heq1
    1627                         @(jmeq_to_eq ??? Heq1) ]
    1628                       #Hloadv <Heq0
    1629                       whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
    1630                       >Hloadv @refl ]
    1631             | 3: (* Register local variable *)
    1632                  #Hlookup_eq
    1633                  lapply (res_inversion ?????? Hlookup_eq)
    1634                  * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
    1635                  #Htype_eq
    1636                  cases (type_should_eq_inversion
    1637                             var_id_type
    1638                             ty
    1639                             (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
    1640                             … Htype_eq) -Htype_eq
    1641                  (* Reverting all premises in order to perform type rewrite *)
    1642                  #Htype_eq
    1643                  lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
    1644                  lapply Hcl_load_success -Hcl_load_success
    1645                  lapply Hcl_lookup -Hcl_lookup
    1646                  lapply Hyp_present -Hyp_present
    1647                  lapply Hexpr_vars -Hexpr_vars
    1648                  lapply cm_expr
    1649                  destruct (Htype_eq)
    1650                  #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
    1651                  #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
    1652                  destruct (Hexpr_eq)
    1653                  whd in match (eval_expr ???????);
    1654                  whd in match (lookup_present ?????);
    1655                  lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
    1656                  >Hlookup' normalize nodelta #Hmatching
    1657                  cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
    1658                  #loaded_val * #Hload_val
    1659                  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1660                  lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
    1661                  #Hload_success
    1662                  cases (Hmatching … Hload_success) #val'
    1663                  * #Hlookup_in_cm #Hvalue_eq %{val'}
    1664                  cases Hyp_present
    1665                  >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
    1666                  (* seems ok *)
    1667             ]
    1668        ]
    1669   | 2: lapply Hcl_success -Hcl_success
    1670        lapply Htranslate_expr -Htranslate_expr
    1671        lapply Hind -Hind cases ty1
    1672        [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
    1673        | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
    1674        #Hind #Htranslate_expr #Hexec_cl
    1675        cases (bind_inversion ????? Htranslate_expr) (* -Htranslate_expr *)
    1676        * whd in match (typ_of_type ?); normalize nodelta
    1677        #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
    1678        whd in ⊢ ((???%) → ?);
    1679        [ 1,2,6,7: #Heq destruct (Heq) ]
    1680        lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
    1681        whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
    1682        #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
    1683        [ 1,3,5,7: @(translate_expr_deref_present … Htranslate_expr … Hyp_present … Htranslate_expr_ind) ]
    1684        whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
    1685        cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
    1686        #Hexec_cl_ind #Hcl_ptr
    1687        cut (∃ptr. cl_ptr = Vptr ptr)
    1688        [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
    1689                   #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
    1690        * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
    1691        #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
    1692        #Hind lapply (Hind (refl ??)) -Hind
    1693        * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
    1694        lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
    1695        destruct (Hcm_ptr) #Hpointer_translation
    1696        cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
    1697        whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
    1698        -Hopt_to_res
    1699        lapply Hexec_cm_ind -Hexec_cm_ind
    1700        lapply Hyp_present -Hyp_present
    1701        lapply Htranslate_expr -Htranslate_expr
    1702        lapply Hexpr_vars -Hexpr_vars
    1703        lapply cm_expr -cm_expr
    1704        cases ty (* Inversion (access_mode ty) fails for whatever reason. *)
    1705        [ | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
    1706        | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
    1707        | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2
    1708        | | #sz2 #sg2 | #ptr_ty2 | #array_ty2 #array_sz2 | #domain2 #codomain2 | #structname2 #fieldspec2 | #unionname2 #fieldspec2 | #id2 ]
    1709        whd in match (typ_of_type ?); whd in match (access_mode ?); normalize nodelta
    1710        #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_cm_ind #Hcl_load_success
    1711        #Heq destruct (Heq)
    1712        [ 3,4,8,9,13,14,18,19: (*  By reference *)
    1713            >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
    1714            lapply (load_value_of_type_by_ref … Hcl_load_success ??)
    1715            try @refl_jmeq
    1716            #Hval >Hval %4 assumption
    1717        | *: (* By_value *)
    1718            (* project Hcl_load_success in Cminor through memory_inj *)
    1719            lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
    1720            try @(load_by_value_success_valid_pointer … Hcl_load_success)
    1721            try @jmeq_to_eq
    1722            try assumption try @refl_jmeq
    1723            * #cm_val * #Hcm_load_success #Hvalue_eq
    1724            lapply (load_value_of_type_by_value … Hcm_load_success)
    1725            try @refl
    1726            #Hloadv_cm
    1727            whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
    1728            >Hloadv_cm normalize %{cm_val} @conj try @refl assumption ]
    1729   | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
    1730        lapply (refl ? (typeof e1))
    1731        cases (typeof e1) in ⊢ ((???%) → %);
    1732        [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
    1733        | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
    1734        #Heq_typeof normalize nodelta
    1735        [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
    1736        whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
    1737        normalize nodelta #Htranslate_expr
    1738        cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
    1739        * whd in match (typ_of_type ?); normalize nodelta
    1740        #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
    1741        [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
    1742          #cm_field_off * #Hcm_field_off
    1743        | lapply Htranslate_expr2 -Htranslate_expr2 ]
    1744        cases (bind_inversion ????? Hexec_cl) -Hexec_cl
    1745        * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
    1746        whd in Hexec_lvalue:(???%);
    1747        [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
    1748          #cl_field_off * #Hcl_field_off #Hoffset_eq ]
    1749        cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
    1750        #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1751        lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
    1752        [  (* Struct case *)
    1753          lapply Hcl_load_value -Hcl_load_value
    1754          lapply Hyp_present -Hyp_present
    1755          lapply Hexpr_vars -Hexpr_vars
    1756          lapply cm_expr -cm_expr
    1757          lapply Hind -Hind
    1758          cases ty
    1759          [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1760          | #structname #fieldspec | #unionname #fieldspec | #id ]
    1761          #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
    1762          normalize nodelta
    1763          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1764          whd in match (eval_expr ???????);
    1765          (* applying the arguments of the induction hypothesis progressively *)
    1766          lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddpi I16) cm_expr_ind
    1767                           (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
    1768          [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
    1769          lapply (Hind ?)
    1770          [ 1,3,5,7,9:
    1771             whd in ⊢ (??%?); >Heq_typeof normalize nodelta
    1772             >Htranslate_expr_ind whd in match (m_bind ?????);
    1773             >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
    1774          whd in Hoffset_eq:(???%); destruct (offset_eq)
    1775          cut (cl_field_off = cm_field_off)
    1776          [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
    1777            normalize #Heq destruct (Heq) @refl ]
    1778          #Heq destruct (Heq)
    1779          lapply (Hind cl_b cl_o trace ?)
    1780          [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
    1781          lapply (Hind ?) -Hind
    1782          [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
    1783            >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
    1784            @Hoffset_eq ]
    1785          * #cm_val' * #Heval_expr #Hvalue_eq
    1786          lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
    1787          * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
    1788          [ 1,2,5: (* by-value *)
    1789             lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
    1790             [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
    1791             * #cm_val * #Hcm_load_value #Hvalue_eq
    1792             lapply (load_value_of_type_by_value … Hcm_load_value)
    1793             [ 1,3,5: @refl ]
    1794             #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
    1795             try @refl try assumption
    1796          | 3,4: (* by-ref *)
    1797             whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
    1798             %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
    1799             whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
    1800          ]
    1801       | (* union case *)
    1802          lapply Hcl_load_value -Hcl_load_value
    1803          lapply Hyp_present -Hyp_present
    1804          lapply Hexpr_vars -Hexpr_vars
    1805          lapply cm_expr -cm_expr
    1806          lapply Hind -Hind
    1807          cases ty
    1808          [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1809          | #structname #fieldspec | #unionname #fieldspec | #id ]
    1810          whd in match (typ_of_type ?); normalize nodelta
    1811          #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
    1812          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1813          [ 1,2,5: (* by-value *)
    1814             whd in match (eval_expr ???????);
    1815             lapply (Hind cm_expr_ind Hexpr_vars ?)
    1816             [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
    1817             whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
    1818             -Hind #Hind
    1819             lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
    1820             whd in match (m_bind ?????); #Hind
    1821             cases (Hind (refl ??)) -Hind
    1822             #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
    1823             cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
    1824             destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
    1825             lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
    1826             [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
    1827             * #cm_val * #Hcm_load_value #Hvalue_eq           
    1828             lapply (load_value_of_type_by_value … Hcm_load_value)
    1829             [ 1,3,5: @refl ]
    1830             #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
    1831             try @refl assumption
    1832          | 3,4:
    1833             whd in Hexec_cl:(???%); destruct (Hexec_cl)
    1834             lapply (Hind cm_expr Hexpr_vars)
    1835             whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
    1836             lapply (Hind Htranslate_expr_ind) -Hind
    1837             whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
    1838             >Hexec_lvalue whd in match (m_bind ?????);
    1839             #Hind cases (Hind … Hyp_present (refl ??))
    1840             #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
    1841             try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
    1842             assumption ]
    1843     ]
    1844   ]
    1845 | 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
    1846      whd in Hexec_lvalue_var:(??%?);
    1847      (* check whether var is local or global *)
    1848      lapply (Hlocal_matching var)
    1849      lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
    1850      cases (lookup ?? cl_env var) in Hexec_lvalue_var;
    1851      normalize nodelta
    1852      [ 1: (* global *)
    1853           #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
    1854           cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
    1855           whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
    1856           lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
    1857           #Hembed
    1858           cases (bind_inversion ????? Htranslate_var) -Htranslate_var
    1859           * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
    1860           cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
    1861           normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1862           whd in match (eval_expr ???????);
    1863           whd in match (eval_constant ????);
    1864           <(eq_sym inv var) >Hfind_symbol normalize nodelta
    1865           %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
    1866           @conj try @refl %4 whd in match (pointer_translation ??);
    1867           >Hembed normalize nodelta whd in match (shift_offset ???);
    1868           >addition_n_0 @refl
    1869      | 2: (* local *)
    1870           #BL #Heq destruct (Heq) #_
    1871           @(match (lookup ?? vars var)
    1872             return λx. (lookup ?? vars var = x) → ?
    1873             with
    1874             [ None ⇒ ?
    1875             | Some kind ⇒ ?
    1876             ] (refl ??))
    1877           normalize nodelta
    1878           #Hlookup [ @False_ind ]
    1879           cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
    1880           #Hlookup
    1881           lapply (refl ? var_alloctype)
    1882           cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
    1883           [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
    1884           [ (* stack alloc*)
    1885             cases (bind_inversion ????? Htranslate_var) -Htranslate_var
    1886             * #var_alloctype' #var_type' * #Hlookup_vartype'           
    1887             whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
    1888             whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
    1889             whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
    1890             %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
    1891             @conj try @refl %4 whd in match (pointer_translation ??);
    1892             >Hembed @refl
    1893           | (* local alloc *)
    1894             cases (bind_inversion ????? Htranslate_var) -Htranslate_var
    1895             * #var_alloctype' #var_type' * #Hlookup_vartype'
    1896             whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
    1897             whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
    1898             whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
    1899 (*| 4: #e #ty*)
    1900 | 4:
    1901   * #ed #ety cases ety
    1902   [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
    1903   | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
    1904   whd in match (typeof ?);
    1905   #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
    1906   cases (bind_inversion ????? Htranslate) -Htranslate   
    1907   * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
    1908   cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
    1909   * #cl_val #trace0 * #Hexec_expr #Hcl_val
    1910   whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
    1911   whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1912   cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
    1913   [ 1,3,5,7: cases cl_val in Hcl_val; normalize
    1914     [ 1,5,9,13: #Heq destruct (Heq)
    1915     | 2,6,10,14: #sz #vec #Heq destruct (Heq)
    1916     | 3,7,11,15: #Heq destruct (Heq)
    1917     | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
    1918   * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
    1919   cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
    1920   #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
    1921   %{cm_val} @conj try @refl try assumption
    1922 | 5:
    1923   #ty cases ty
    1924   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1925   | #structname #fieldspec | #unionname #fieldspec | #id ]
    1926   #ed #ty' #Hind
    1927   whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
    1928   #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
    1929   cases (bind_inversion ????? Htranslate) -Htranslate
    1930   * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
    1931   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    1932   * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
    1933   whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1934   whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1935   cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
    1936   #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
    1937   %{cm_val} @conj try @refl assumption
    1938 | 6:
    1939   #ty *
    1940   [ cases ty
    1941     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1942     | #structname #fieldspec | #unionname #fieldspec | #id ]
    1943     #e #Hind
    1944     whd in match (typeof ?);
    1945     #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
    1946     #Htranslate
    1947     [ 3,4,5,8: destruct (Htranslate)
    1948     | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
    1949          cases sz normalize nodelta
    1950          #e' #Hexpr_vars #Htranslate
    1951          [ 1, 2: destruct (Htranslate) ] ]
    1952     #cl_val #trace #Hyp_present #Hexec_expr
    1953     cases (bind_inversion ????? Htranslate) -Htranslate
    1954     #cmop * #Htranslate_unop #Hexec_arg
    1955     cases (bind_inversion ????? Hexec_arg) -Hexec_arg
    1956     * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1957     cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    1958     * #cl_arg #cl_trace * #Hexec_cl
    1959     whd in ⊢ ((???%) → ?); #Hexec_unop
    1960     cases (bind_inversion ????? Hexec_unop) -Hexec_unop
    1961     #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1962     lapply (opt_to_res_inversion ???? Hopt) -Hopt
    1963     #Hsem_cl whd in match (eval_expr ???????);
    1964     cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
    1965     #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
    1966     lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
    1967     * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
    1968     whd in match (typ_of_type Tvoid);
    1969     lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
    1970     #H >H @refl
    1971   | *:
    1972     cases ty
    1973     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
    1974     | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
    1975     #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
    1976     #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
    1977     whd in Htranslate:(??%?);
    1978     [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
    1979     cases (bind_inversion ????? Htranslate) -Htranslate
    1980     #cmop * #Htranslate_unop #Hexec_arg
    1981     cases (bind_inversion ????? Hexec_arg) -Hexec_arg
    1982     * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1983     cases (bind_inversion ????? Hexec) -Hexec
    1984     * #cl_arg #cl_trace * #Hexec_cl
    1985     whd in ⊢ ((???%) → ?); #Hexec_unop
    1986     cases (bind_inversion ????? Hexec_unop) -Hexec_unop
    1987     #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1988     lapply (opt_to_res_inversion ???? Hopt) -Hopt
    1989     #Hcl_unop whd in match (eval_expr ???????);
    1990     cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
    1991     #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
    1992     lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
    1993     * #op_res * #Hcl_sem #Hvalue_eq
    1994     [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
    1995        %{op_res} @conj try @refl assumption
    1996     | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
    1997        %{op_res} @conj try @refl assumption
    1998     ]
    1999   ]
    2000 | 8: #ty #ty' * #ed #ety
    2001   cases ety
    2002   [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
    2003   | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
    2004   whd in match (typeof ?); whd in match (typ_of_type ?);
    2005   #Hind whd in match (typeof ?);
    2006   #cm_expr #Hexpr_vars #Htranslate
    2007   cases (bind_inversion ????? Htranslate) -Htranslate
    2008   * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
    2009   cases (bind_inversion ????? Htranslate) -Htranslate
    2010   * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
    2011   [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
    2012   cases (bind_inversion ????? Htranslate) -Htranslate
    2013   * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
    2014   #Heq destruct (Heq)
    2015   #cl_val #trace #Hyp_present #Hexec_cm
    2016   cases (bind_inversion ????? Hexec_cm) -Hexec_cm
    2017   * #cm_val #trace0 * #Hexec_cm #Hexec_cast
    2018   cases (bind_inversion ????? Hexec_cast) -Hexec_cast
    2019   #cast_val * #Hexec_cast
    2020   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    2021   cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
    2022   #Htype_eq
    2023   lapply Hexec_cast -Hexec_cast
    2024 (*  lapply Htyp_should_eq -Htyp_should_eq *)
    2025   lapply Htranslate_cast -Htranslate_cast
    2026   lapply Hexpr_vars_cast -Hexpr_vars_cast
    2027   lapply cm_cast -cm_cast
    2028   lapply Hyp_present -Hyp_present
    2029   lapply Hexpr_vars -Hexpr_vars
    2030   lapply cm_expr -cm_expr
    2031   <Htype_eq -Htype_eq
    2032   whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
    2033   whd in match (typeof ?); normalize nodelta
    2034   cases ty'
    2035   [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
    2036   | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
    2037   | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
    2038   #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
    2039   #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
    2040   whd in Htranslate_cast:(??%%);
    2041   whd in Hexpr_vars;
    2042   destruct (Htranslate_cast)
    2043   [ 1,2,3,4,7:
    2044     lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
    2045     * #cm_val' * #Heval_castee
    2046     lapply Hexec_cm -Hexec_cm
    2047     whd in Hexec_cast:(??%%);
    2048     cases cm_val in Hexec_cast; normalize nodelta
    2049     [ | #vsz #vi | | #vp
    2050     | | #vsz #vi | | #vp
    2051     | | #vsz #vi | | #vp
    2052     | | #vsz #vi | | #vp
    2053     | | #vsz #vi | | #vp ]
    2054     [ 2,6,10,14,18:
    2055     | *: #Habsurd destruct (Habsurd) ]
    2056     #Hexec_cast #Hexec_cm #Hvalue_eq
    2057     [ 1,2,3:
    2058       cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
    2059       #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
    2060     [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
    2061     [ 1,2,4,5:
    2062       cases (bind_inversion ????? Hexec_cast)
    2063       whd in match (typeof ?);
    2064       #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
    2065       whd in match (eq_rect_r ??????);
    2066       [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
    2067       @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
    2068       [ 2,4: #foo #Habsurd destruct (Habsurd) ]
    2069       #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
    2070       whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    2071       whd in match (typ_of_type ?); whd in match (eval_expr ???????);
    2072       >Heval_castee normalize nodelta whd in match (eval_unop ????);
    2073       >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
    2074       >Heq_vi >eq_bv_true normalize
    2075       %{Vnull} @conj try @refl %3
    2076     | 3: destruct (Hcl_val_eq)
    2077           whd in match (eval_expr ???????);
    2078           >Heval_castee normalize nodelta
    2079           whd in match (eval_unop ????);
    2080           cases esg normalize nodelta
    2081           whd in match (opt_to_res ???); whd in match (m_bind ?????);
    2082           [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
    2083           whd in match (eq_rect_r ??????);
    2084           -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
    2085           (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
    2086              this reason. *)
    2087           lapply Hvalue_eq -Hvalue_eq lapply vi -vi
    2088           cases esz normalize nodelta
    2089           #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
    2090           whd in match (sign_ext ??); whd in match (zero_ext ??);
    2091           %2
    2092     ]
    2093  | *:
    2094     lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
    2095     * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
    2096     %{cm_val'} @conj try @refl
    2097     lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
    2098     -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
    2099     cases cm_val
    2100     [ | #vsz #vi | | #vp
    2101     | | #vsz #vi | | #vp
    2102     | | #vsz #vi | | #vp
    2103     | | #vsz #vi | | #vp ]
    2104     #Hexec_cm #Hvalue_eq #Hexec_cast
    2105     whd in Hexec_cast:(??%%);
    2106     [ 1,5,9,13: destruct (Hexec_cast) ]
    2107     [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
    2108     lapply Hexec_cast -Hexec_cast
    2109     normalize cases (eq_v ?????) normalize
    2110     #Habsurd destruct (Habsurd)
    2111  ]
    2112 | 9: (* Econdition *) 
    2113   #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
    2114   #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
    2115   #Hexec_cm
    2116   cases (bind_inversion ????? Hexec_cm) -Hexec_cm
    2117   * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
    2118   cases (bind_inversion ????? Hexec_cm) -Hexec_cm
    2119   #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
    2120   cases (bind_inversion ????? Hexec_cm) -Hexec_cm
    2121   * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
    2122   whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    2123   cases (bind_inversion ????? Htranslate) -Htranslate
    2124   * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
    2125   cases (bind_inversion ????? Htranslate) -Htranslate
    2126   * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
    2127   cases (bind_inversion ????? Htranslate) -Htranslate
    2128   * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
    2129   lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
    2130   *  #Htypeof_e2_eq_ty
    2131   lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
    2132   lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
    2133   >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
    2134   #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
    2135   #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
    2136   cases (bind_inversion ????? Htranslate) -Htranslate
    2137   * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
    2138   cases (bind_inversion ????? Htranslate) -Htranslate 
    2139   * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
    2140   lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
    2141   * #Htypeof_e3_eq_ty
    2142   lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
    2143   lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
    2144   >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
    2145   #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
    2146   #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
    2147   lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
    2148   lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
    2149   lapply Hexec_bool_of_val -Hexec_bool_of_val
    2150   cases (typeof e1) normalize nodelta
    2151   [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
    2152   | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
    2153   #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
    2154   whd in Heq:(???%); destruct (Heq)
    2155   whd in match (eval_expr ???????);
    2156   whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
    2157   lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
    2158   >Heval_e1 normalize nodelta
    2159   lapply Hcm_ifthenelse -Hcm_ifthenelse
    2160   lapply Hexec_cond -Hexec_cond 
    2161   lapply Hexec_bool_of_val -Hexec_bool_of_val
    2162   lapply Hvalue_eq1 -Hvalue_eq1
    2163   cases cm_cond_val
    2164   [ | #vsz #vi | | #vp
    2165   | | #vsz #vi | | #vp
    2166   | | #vsz #vi | | #vp
    2167   | | #vsz #vi | | #vp ]
    2168   whd in ⊢ (? → (??%%) → ?);
    2169   [ 6:
    2170   | *: #_ #Habsurd destruct (Habsurd) ]
    2171   #Hvalue_eq1 #Hsz_check
    2172   lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
    2173   * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
    2174   #Heq destruct (Heq)
    2175   #Hexec_expr_e1
    2176   @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
    2177     return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
    2178     with
    2179     [ true ⇒ λHeq. ?
    2180     | false ⇒ λHeq. ?
    2181     ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
    2182   normalize nodelta
    2183   >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
    2184   whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
    2185   >Heq normalize nodelta
    2186   [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
    2187     cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
    2188     normalize %{cm_val3} @conj try @refl assumption
    2189   | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
    2190     cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
    2191     normalize %{cm_val2} @conj try @refl assumption ]
    2192 | 10: (* andbool *)
    2193   #ty
    2194   #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
    2195   cases ty
    2196   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    2197   | #structname #fieldspec | #unionname #fieldspec | #id ]
    2198   #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
    2199   (* decompose first slice of clight execution *)
    2200   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2201   * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
    2202   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2203 (* cut *) 
    2204   * * normalize nodelta #Hexec_bool_of_val
    2205   [ 2,4,6,8,10,12,14:
    2206     whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    2207   | 16: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
    2208   | *:
    2209     #Hexec_expr   
    2210     cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2211     * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
    2212     cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2213     #b2 * #Hexec_bool_of_val_e2
    2214     whd in ⊢ ((???%) → ?); #Heq
    2215     destruct (Heq) ]
    2216   cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
    2217   * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
    2218   cases (bind_inversion ????? Htranslate) -Htranslate
    2219   * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
    2220   cases (bind_inversion ????? Htranslate) -Htranslate
    2221   * #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
    2222   lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
    2223   * #Htypeof_e2_eq_ty
    2224   (* cleanup the type coercion *)
    2225   lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
    2226   lapply Hexpr_vars_wt -Hexpr_vars_wt
    2227   lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
    2228   lapply Hexpr_vars_e2 -Hexpr_vars_e2
    2229   lapply cm_expr_e2 -cm_expr_e2
    2230   >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty   
    2231   #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
    2232 
    2233   #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
    2234   lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
    2235   lapply Hexpr_vars_e1 -Hexpr_vars_e1
    2236   lapply cm_expr_e1 -cm_expr_e1
    2237   cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
    2238   [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
    2239          destruct >(Htypeof_e1) whd in match (typ_of_type ?);
    2240          #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
    2241          whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    2242   *
    2243   [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
    2244          destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
    2245          #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
    2246          #Habsurd destruct (Habsurd) ]
    2247   * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
    2248   destruct >Htypeof_e1 #Heq_bv
    2249   whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);   
    2250   #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
    2251   whd in match (typ_of_type ?);
    2252   whd in ⊢ ((???%) → ?); #Heq 
    2253   destruct (Heq) cases Hyp_present -Hyp_present
    2254   * #Hyp_present_e1 * * #Hyp_present_e2 normalize in ⊢ (% → % → % → ?);
    2255   * * *
    2256   lapply (Hind1 … Hyp_present_e1 Hexec_e1)
    2257   * #cm_val_1 * #Heval_expr1 #Hvalue_eq
    2258   whd in match (eval_expr ???????); whd in match (proj2 ???); whd in match (proj2 ???);
    2259   >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
    2260   whd in match (eval_bool_of_val ?);
    2261   <Heq_bv
    2262   whd in match (m_bind ?????);
    2263   [ %{(Vint sz (zero (bitsize_of_intsize sz)))}
    2264     >zero_ext_zero @conj try %2
    2265     whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
    2266   normalize nodelta
    2267   lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
    2268   -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
    2269   whd in match (eval_expr ???????); >Heval_expr2
    2270   normalize nodelta
    2271   cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
    2272   [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
    2273        destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
    2274        #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
    2275        whd in match (eval_bool_of_val ?);
    2276        whd in match (m_bind ?????); normalize nodelta
    2277        >zero_ext_one
    2278        %{(Vint sz (repr sz 1))} @conj try %2
    2279        whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
    2280   *
    2281   [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
    2282       >(value_eq_null_inversion … Hvalue_eq2)
    2283       whd in match (eval_bool_of_val ?);
    2284       whd in match (m_bind ?????);
    2285       normalize nodelta
    2286       %{(Vint sz (zero (bitsize_of_intsize sz)))}
    2287       >zero_ext_zero @conj try %2
    2288       whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
    2289   * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
    2290   destruct (Hcl_val_e2)
    2291   >(value_eq_int_inversion … Hvalue_eq2)
    2292   whd in match (eval_bool_of_val ?); <Heq_bv
    2293   cases b2 in Heq_bv; #Heq_bv
    2294   whd in match (m_bind ?????); normalize nodelta
    2295   [ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
    2296     >append_nil @conj try @refl >zero_ext_one %2
    2297   | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
    2298     >append_nil @conj try @refl >zero_ext_zero %2 ]
    2299 | 11: (* orbool, similar to andbool *)
    2300   #ty
    2301   #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
    2302   cases ty
    2303   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    2304   | #structname #fieldspec | #unionname #fieldspec | #id ]
    2305   #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
    2306   (* decompose first slice of clight execution *)
    2307   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2308   * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
    2309   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2310   * * normalize nodelta #Hexec_bool_of_val
    2311   [ 1,3,5,7,9,11,13,15:
    2312     whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    2313   | *:
    2314     #Hexec_expr   
    2315     cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2316     * #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
    2317     cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2318     #b2 * #Hexec_bool_of_val_e2
    2319     whd in ⊢ ((???%) → ?); #Heq
    2320     destruct (Heq) ]
    2321   cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
    2322   * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
    2323   cases (bind_inversion ????? Htranslate) -Htranslate
    2324   * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
    2325   cases (bind_inversion ????? Htranslate) -Htranslate
    2326   * #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
    2327   lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
    2328   * #Htypeof_e2_eq_ty
    2329   (* cleanup the type coercion *)
    2330   lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
    2331   lapply Hexpr_vars_wt -Hexpr_vars_wt
    2332   lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
    2333   lapply Hexpr_vars_e2 -Hexpr_vars_e2
    2334   lapply cm_expr_e2 -cm_expr_e2
    2335   >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty   
    2336   #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
    2337   #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
    2338   lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
    2339   lapply Hexpr_vars_e1 -Hexpr_vars_e1
    2340   lapply cm_expr_e1 -cm_expr_e1
    2341   cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
    2342   [ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
    2343          destruct >(Htypeof_e1) whd in match (typ_of_type ?);
    2344          #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
    2345          whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
    2346   *
    2347   [ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
    2348          destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
    2349          #cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
    2350          #Habsurd destruct (Habsurd) ]
    2351   * #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
    2352   destruct >Htypeof_e1 #Heq_bv
    2353   whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);   
    2354   #cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
    2355   whd in ⊢ ((???%) → ?); #Heq
    2356   destruct (Heq) cases Hyp_present -Hyp_present
    2357   * #Hyp_present_e1 * * * #Hyp_present_e2 * *
    2358   lapply (Hind1 … Hyp_present_e1 Hexec_e1)
    2359   * #cm_val_1 * #Heval_expr1 #Hvalue_eq
    2360   whd in match (eval_expr ???????);
    2361   >Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
    2362   whd in match (eval_bool_of_val ?);
    2363   <Heq_bv
    2364   whd in match (m_bind ?????);
    2365   [ %{(Vint sz (repr sz 1))}
    2366     >zero_ext_one @conj try %2
    2367     whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
    2368   normalize nodelta
    2369   lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
    2370   -Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
    2371   whd in match (eval_expr ???????); >Heval_expr2
    2372   normalize nodelta
    2373   cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
    2374   [ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
    2375        destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
    2376        #cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
    2377        whd in match (eval_bool_of_val ?);
    2378        whd in match (m_bind ?????); normalize nodelta
    2379        >zero_ext_one
    2380        %{(Vint sz (repr sz 1))} @conj try %2
    2381        whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
    2382   *
    2383   [ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
    2384       >(value_eq_null_inversion … Hvalue_eq2)
    2385       whd in match (eval_bool_of_val ?);
    2386       whd in match (m_bind ?????);
    2387       normalize nodelta
    2388       %{(Vint sz (zero (bitsize_of_intsize sz)))}
    2389       >zero_ext_zero @conj try %2
    2390       whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
    2391   * #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
    2392   destruct (Hcl_val_e2)
    2393   >(value_eq_int_inversion … Hvalue_eq2)
    2394   whd in match (eval_bool_of_val ?); <Heq_bv
    2395   cases b2 in Heq_bv; #Heq_bv
    2396   whd in match (m_bind ?????); normalize nodelta
    2397   [ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
    2398     >append_nil @conj try @refl >zero_ext_one %2
    2399   | %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
    2400     >append_nil @conj try @refl >zero_ext_zero %2 ]
    2401 | 12: (* sizeof *)
    2402   #ty cases ty
    2403   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    2404   | #structname #fieldspec | #unionname #fieldspec | #id ]
    2405   #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
    2406   whd in Hexec_expr:(??%?); destruct (Hexec_expr)
    2407   normalize in match (typ_of_type ?);
    2408   whd in Htranslate:(??%?); destruct (Htranslate)
    2409   whd in match (eval_expr ???????);
    2410   %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
    2411 | 13:
    2412   #ty #ed #ty' cases ty'
    2413   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    2414   | #structname #fieldspec | #unionname #fieldspec | #id ]
    2415   #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
    2416   #Hexec_lvalue
    2417   whd in Hexec_lvalue:(??%?); destruct
    2418   [ whd in Htranslate_addr:(??%?);
    2419     cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
    2420     * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
    2421     cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
    2422     #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
    2423     #Heq destruct (Heq)
    2424     cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
    2425   ]
    2426   cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
    2427   * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
    2428   [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
    2429        #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
    2430        cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
    2431        #cm_val_field * #Heval_cm #Hvalue_eq
    2432        whd in match (eval_expr ???????);
    2433        >Heval_cm normalize nodelta
    2434        whd in match (eval_expr ???????); whd in match (m_bind ?????);
    2435        whd in match (eval_binop ???????); normalize nodelta
    2436        cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
    2437        normalize nodelta #Hptr_translate
    2438        %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
    2439        @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
    2440        %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
    2441        cases (E cl_blo) in Hptr_translate; normalize nodelta
    2442        [ #H destruct (H) ]
    2443        * #BL #OFF normalize nodelta #Heq destruct (Heq)
    2444        >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
    2445        #H destruct (H)       
    2446        whd in match (shift_pointer ???);
    2447        whd in match (shift_offset ???) in ⊢ (???%);
    2448        >sign_ext_same_size
    2449        whd in match (offset_plus ??) in ⊢ (??%%);
    2450        <(associative_addition_n ? (offv off))
    2451        >(commutative_addition_n … (repr I16 field_off) (offv OFF))
    2452        >(associative_addition_n ? (offv off))
    2453        @refl       
    2454   | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
    2455        cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
    2456        #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
    2457        cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
    2458        #Hpointer_translation
    2459        %{cm_val} @conj try assumption
    2460        destruct @refl
    2461    ]
    2462 | 14: (* cost label *)
    2463   #ty (* cases ty
    2464   [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    2465   | #structname #fieldspec | #unionname #fieldspec | #id ] *)
    2466   #l * #ed #ety
    2467   whd in match (typeof ?); whd in match (typeof ?);
    2468   #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
    2469   cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
    2470   #Hexpr_vars * #Htranslate_ind #Htranslate
    2471   cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
    2472   * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
    2473   whd in match (typeof ?) in Htyp_should_eq:(??%?);
    2474   cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
    2475   #Htyp_eq
    2476   lapply Htranslate_ind -Htranslate_ind
    2477   lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
    2478   lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
    2479   lapply Hexpr_vars -Hexpr_vars lapply e' -e'
    2480   lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
    2481   <Htyp_eq
    2482   #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
    2483   #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
    2484   whd in match (eval_expr ???????);
    2485   cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
    2486   whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    2487   cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
    2488   #cm_val' * #Heval_expr' #Hvalue_eq
    2489   >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
    2490   >cons_to_append >(nil_append … cm_trace) @refl
    2491 | 15: *
    2492   [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
    2493   | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    2494   #ty normalize in ⊢ (% → ?);
    2495   [ 2,3,12: @False_ind
    2496   | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
    2497            normalize #Habsurd destruct (Habsurd) ]
    2498 ] qed.
     278            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).   
     279*)
     280
     281
    2499282
    2500283
Note: See TracChangeset for help on using the changeset viewer.