 Timestamp:
 Jan 28, 2013, 11:43:43 AM (8 years ago)
 Location:
 src/Clight
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2588 r2591 1 1 include "Clight/toCminor.ma". 2 include "Clight/toCminorOps.ma".3 2 include "Clight/CexecInd.ma". 4 3 include "common/Globalenvs.ma". … … 6 5 include "Clight/abstract.ma". 7 6 include "Cminor/abstract.ma". 7 8 (* Expr simulation. Contains important definitions for statements, too. *) 9 include "Clight/toCminorCorrectnessExpr.ma". 8 10 9 11 … … 138 140 ] qed. 139 141 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 166 143 167 144 (* 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 (* 170 150 lemma characterise_vars_global : ∀globals,f,vartypes,stacksize. 171 151 characterise_vars globals f = 〈vartypes, stacksize〉 → … … 184 164  * #ty' whd in ⊢ (% → ?); >L * 185 165  whd >(opt_eq_from_res ???? L) % #E destruct 186 ] qed. 187 166 ] qed. *) 188 167 189 168 (* Show how the global environments match up. *) … … 255 234 ] qed. 256 235 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. 619 239 lemma eval_expr_sim : 620 240 (* [cl_cm_inv] maps CL globals to CM globals, including functions *) … … 656 276 exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 657 277 ∃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: (* Byref *) 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: (* byvalue *) 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: (* byref *) 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: (* byvalue *) 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 2499 282 2500 283
Note: See TracChangeset
for help on using the changeset viewer.