Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2582 r2588  
    11include "Clight/toCminor.ma".
     2include "Clight/toCminorOps.ma".
     3include "Clight/CexecInd.ma".
     4include "common/Globalenvs.ma".
     5include "Clight/memoryInjections.ma".
     6include "Clight/abstract.ma".
     7include "Cminor/abstract.ma".
     8
    29
    310(* When we characterise the local Clight variables, those that are stack
     
    248255] qed.
    249256
    250 include "Clight/Cexec.ma".
    251 include "Clight/abstract.ma".
    252 include "Cminor/abstract.ma".
    253 
    254257(* Invariants used in simulation *)
    255258
     
    264267      find_funct … ge_cm v = Some ? f'
    265268}.
    266 
    267 include "Clight/CexecInd.ma".
    268 include "Clight/frontend_misc.ma".
    269 include "Clight/memoryInjections.ma".
    270269
    271270(* Perhaps we will have to be more precise on what is allocated, etc.
     
    301300        | None ⇒ False ]
    302301    ].
    303              
    304 lemma type_should_eq_inversion :
    305   ∀ty1,ty2,P,f,res.
    306     type_should_eq ty1 ty2 P f = OK ? res →
    307     ty1 = ty2 ∧ f ≃ res.
    308 #ty1 #ty2 #P #f #res normalize
    309 cases (type_eq_dec ty1 ty2) normalize nodelta
    310 [ 2: #Hneq #Habsurd destruct ]
    311 #Heq #Heq2 @conj try assumption
    312 destruct (Heq2) cases Heq normalize nodelta
    313 @eq_to_jmeq @refl
    314 qed.
    315 
    316 lemma typ_should_eq_inversion :
    317   ∀ty1,ty2,P,a,x.
    318     typ_should_eq ty1 ty2 P a = OK ? x →
    319     ty1 = ty2 ∧ a ≃ x.
    320 * [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
    321 [ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
    322 | 3: cases sz cases sg #P #A #x normalize #H destruct
    323 | 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
    324 cases sz cases sz2 cases sg cases sg2
    325 #P #a #x #H normalize in H:(??%?); destruct (H)
    326 try @conj try @refl try @refl_jmeq
    327 qed.
    328302
    329303lemma load_value_of_type_by_ref :
     
    459433qed.
    460434
    461 
    462 lemma translate_notbool_to_cminor :
    463   ∀t,sg,arg.
    464   ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
    465   ∀res. sem_unary_operation Onotbool arg t = Some ? res →
    466         eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
    467 *
    468 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    469 | #structname #fieldspec | #unionname #fieldspec | #id ]
    470 normalize in match (typ_of_type ?);
    471 #sg #arg #cmop
    472 whd in ⊢ (??%% → ?); #Heq destruct (Heq)
    473 cases arg
    474 [ | #vsz #vi | | #vp
    475 | | #vsz #vi | | #vp
    476 | | #vsz #vi | | #vp
    477 | | #vsz #vi | | #vp
    478 | | #vsz #vi | | #vp
    479 | | #vsz #vi | | #vp
    480 | | #vsz #vi | | #vp
    481 | | #vsz #vi | | #vp ]
    482 #res
    483 whd in ⊢ ((??%?) → ?);
    484 #Heq
    485 [ 6,11,12: | *: destruct (Heq) ]
    486 [ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
    487 | 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
    488      #H normalize nodelta #Heq destruct
    489      whd in match (eval_unop ????);
    490      cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
    491 ] qed.
    492 
    493 lemma translate_notint_to_cminor :
    494   ∀t,t',arg.
    495   ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
    496   ∀res. sem_unary_operation Onotint arg t = Some ? res →
    497         eval_unop (typ_of_type t) t' cmop arg = Some ? res.
    498 #ty *
    499 [ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
    500 #sz #sg #arg #cmop
    501 whd in match (translate_unop ???);
    502 @(match typ_eq (ASTint sz sg) (typ_of_type ty)
    503   with
    504   [ inl H ⇒ ?
    505   | inr H ⇒ ? ])
    506 normalize nodelta
    507 [ 2: #Heq destruct ]
    508 lapply H -H
    509 lapply cmop -cmop
    510 cases ty
    511 [ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
    512 | #structname #fieldspec | #unionname #fieldspec | #id ]
    513 normalize nodelta
    514 #cmop normalize in match (typ_of_type ?); #H destruct
    515 #H' normalize in H';
    516 destruct (H')
    517 #res
    518 whd in match (sem_unary_operation ???);
    519 cases arg
    520 [ | #vsz #vi | | #vp
    521 | | #vsz #vi | | #vp
    522 | | #vsz #vi | | #vp
    523 | | #vsz #vi | | #vp ]
    524 whd in match (sem_notint ?);
    525 #H destruct (H) @refl
    526 qed.
    527 
    528 
    529 lemma translate_negint_to_cminor :
    530   ∀t,t',arg.
    531   ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
    532   ∀res. sem_unary_operation Oneg arg t = Some ? res →
    533         eval_unop (typ_of_type t) t' cmop arg = Some ? res.
    534 #ty *
    535 [ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
    536 #sz #sg #arg #cmop
    537 whd in match (translate_unop ???);
    538 @(match typ_eq (ASTint sz sg) (typ_of_type ty)
    539   with
    540   [ inl H ⇒ ?
    541   | inr H ⇒ ? ])
    542 normalize nodelta
    543 [ 2: #Heq destruct ]
    544 lapply H -H
    545 lapply cmop -cmop
    546 cases ty
    547 [ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
    548 | #structname #fieldspec | #unionname #fieldspec | #id ]
    549 normalize nodelta
    550 #cmop normalize in match (typ_of_type ?); #H destruct
    551 #H' normalize in H';
    552 destruct (H')
    553 #res
    554 whd in match (sem_unary_operation ???);
    555 cases arg
    556 [ | #vsz #vi | | #vp
    557 | | #vsz #vi | | #vp
    558 | | #vsz #vi | | #vp
    559 | | #vsz #vi | | #vp ]
    560 whd in match (sem_neg ??);
    561 #H destruct (H)
    562 whd in match (eval_unop ????);
    563 cases (eq_intsize sz' vsz) in H; normalize nodelta
    564 #H destruct @refl
    565 qed.
    566 
    567 
    568 lemma translate_unop :
    569   ∀ty,sg,op,cmop.
    570   translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
    571   ∀arg,res. sem_unary_operation op arg ty = Some ? res →
    572             eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
    573 #ty #sg * #cmop #Htranslate #arg
    574 [ @translate_notbool_to_cminor assumption
    575 | @translate_notint_to_cminor assumption
    576 | @translate_negint_to_cminor assumption ]
    577 qed.
    578 
    579 lemma classify_add_inversion :
    580   ∀ty1,ty2.
    581     (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
    582     (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
    583     (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
    584     (classify_add ty1 ty2 = add_default ty1 ty2).
    585 #ty1 #ty2
    586 cases (classify_add ty1 ty2)
    587 [ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
    588 | #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
    589 | #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
    590 | #tya #tyb %2 @refl ]
    591 qed.
    592 
    593 lemma classify_sub_inversion :
    594   ∀ty1,ty2.
    595     (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_ii sz sg) ∨
    596     (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_pi n ty' sz sg) ∨
    597     (∃ty1',ty2',n1,n2. ty1 = ptr_type ty1' n1 ∧ ty2 = ptr_type ty2' n2 ∧ classify_sub ty1 ty2 ≃ sub_case_pp n1 n2 ty1' ty2') ∨
    598     (classify_sub ty1 ty2 = sub_default ty1 ty2).
    599 #ty1 #ty2
    600 cases (classify_sub ty1 ty2)
    601 [ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
    602 | #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
    603 | #n1 #n2 #t1 #t2 %1 %2 %{t1} %{t2} %{n1} %{n2} @conj try @conj try @refl @refl_jmeq
    604 | #tya #tyb %2 @refl ]
    605 qed.
    606 
    607 lemma classify_aop_inversion :
    608   ∀ty1,ty2.
    609     (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
    610     classify_aop ty1 ty2 = aop_default ty1 ty2.
    611 #ty1 #ty2
    612 cases (classify_aop ty1 ty2)
    613 [ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
    614 | #ty #ty' %2 @refl ]
    615 qed.
    616 
    617 lemma sem_add_ip_inversion :
    618   ∀sz,sg,ty',optlen.
    619   ∀v1,v2,res.
    620   sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
    621   ∃sz',i. v1 = Vint sz' i ∧
    622       ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
    623        (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    624 #tsz #tsg #ty' * [ | #n ]
    625 *
    626 [ | #sz' #i' | | #p'
    627 | | #sz' #i' | | #p' ]
    628 #v2 #res
    629 whd in ⊢ ((??%?) → ?);
    630 #H destruct
    631 cases v2 in H;
    632 [ | #sz2' #i2' | | #p2'
    633 | | #sz2' #i2' | | #p2' ] normalize nodelta
    634 #H destruct
    635 [ 1,3:
    636   lapply H -H
    637   @(eq_bv_elim … i' (zero ?)) normalize nodelta
    638   #Hi #Heq destruct (Heq)
    639   %{sz'} %{(zero ?)} @conj destruct try @refl
    640   %2 @conj try @conj try @refl
    641 | *: %{sz'} %{i'} @conj try @refl
    642   %1 %{p2'} @conj try @refl
    643 ] qed.
    644 
    645 (* symmetric of the upper one *)
    646 lemma sem_add_pi_inversion :
    647   ∀sz,sg,ty',optlen.
    648   ∀v1,v2,res.
    649   sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
    650   ∃sz',i. v2 = Vint sz' i ∧
    651       ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
    652        (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    653 #tsz #tsg #ty' * [ | #n ]
    654 *
    655 [ | #sz' #i' | | #p'
    656 | | #sz' #i' | | #p' ]
    657 #v2 #res
    658 whd in ⊢ ((??%?) → ?);
    659 #H destruct
    660 cases v2 in H; normalize nodelta
    661 [ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
    662 #H destruct
    663 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1
    664   %{p'} @conj try @refl
    665 | *: lapply H -H
    666   @(eq_bv_elim … i2' (zero ?)) normalize nodelta
    667   #Hi #Heq destruct (Heq)
    668   %{sz2'} %{(zero ?)} @conj destruct try @refl
    669   %2 @conj try @conj try @refl
    670 ] qed.
    671 
    672 (* Know that addition on integers gives an integer. Notice that there is no correlation
    673    between the size in the types and the size of the integer values. *)
    674 lemma sem_add_ii_inversion :
    675   ∀sz,sg.
    676   ∀v1,v2,res.
    677   sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    678   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    679               res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
    680 #sz #sg
    681 *
    682 [ | #sz' #i' | | #p' ]
    683 #v2 #res
    684 whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
    685 cases sz cases sg normalize nodelta
    686 #H destruct
    687 cases v2 in H; normalize nodelta
    688 #H1 destruct
    689 #H2 destruct #Heq %{sz'} lapply Heq -Heq
    690 cases sz' in i'; #i' 
    691 whd in match (intsize_eq_elim ???????);
    692 cases H1 in H2; #j' normalize nodelta
    693 #Heq destruct (Heq)
    694 %{i'} %{j'} @conj try @conj try @conj try @refl
    695 qed.
    696 
    697 lemma sem_sub_pp_inversion :
    698   ∀ty1,ty2,n1,n2.
    699   ∀v1,v2,res.
    700   sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) = Some ? res →
    701   (∃p1,p2,i. v1 =  Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧
    702              division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧
    703              res = Vint I32 i) ∨
    704   (v1 =  Vnull ∧ v2 = Vnull ∧ res = Vint I32 (zero ?)).
    705 #ty1 #ty2 #n1 #n2
    706 cases n1 cases n2
    707 [ | #n1 | #n2 | #n2 #n1 ]
    708 *
    709 [ | #sz #i | | #p
    710 | | #sz #i | | #p
    711 | | #sz #i | | #p
    712 | | #sz #i | | #p ]
    713 #v2 #res
    714 whd in ⊢ ((??%?) → ?);
    715 #H1 destruct
    716 cases v2 in H1;
    717 [ | #sz' #i' | | #p'
    718 | | #sz' #i' | | #p'
    719 | | #sz' #i' | | #p'
    720 | | #sz' #i' | | #p'
    721 | | #sz' #i' | | #p'
    722 | | #sz' #i' | | #p'
    723 | | #sz' #i' | | #p'
    724 | | #sz' #i' | | #p' ]
    725 normalize nodelta
    726 #H2 destruct
    727 try /4 by or_introl, or_intror, conj, refl/
    728 %1 %{p} %{p'}
    729 cases (if_opt_inversion ???? H2)
    730 #Hblocks_eq -H2
    731 @(eqb_elim … (sizeof ty1) 0) normalize nodelta
    732 #Heq_sizeof destruct #Heq destruct
    733 cases (division_u ???) in Heq; normalize nodelta
    734 #H3 destruct #H4 destruct
    735 %{H3} try @conj try @conj try @conj try @conj try @refl
    736 @(eq_block_to_refl … Hblocks_eq)
    737 qed.
    738 
    739 
    740 lemma sem_sub_pi_inversion :
    741   ∀sz,sg,ty',optlen.
    742   ∀v1,v2,res.
    743   sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
    744   ∃sz',i. v2 = Vint sz' i ∧
    745       ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨
    746        (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    747 #tsz #tsg #ty' * [ | #n ]
    748 *
    749 [ | #sz' #i' | | #p'
    750 | | #sz' #i' | | #p' ]
    751 #v2 #res
    752 whd in ⊢ ((??%?) → ?);
    753 #H destruct
    754 cases v2 in H; normalize nodelta
    755 [ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
    756 #H destruct
    757 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1
    758   %{p'} @conj try @refl
    759 | *: lapply H -H
    760   @(eq_bv_elim … i2' (zero ?)) normalize nodelta
    761   #Hi #Heq destruct (Heq)
    762   %{sz2'} %{(zero ?)} @conj destruct try @refl
    763   %2 @conj try @conj try @refl
    764 ] qed.
    765 
    766 
    767 lemma sem_sub_ii_inversion :
    768   ∀sz,sg.
    769   ∀v1,v2,res.
    770   sem_sub v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    771   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    772               res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2).
    773 #sz #sg *             
    774 [ | #sz' #i' | | #p' ]
    775 #v2 #res
    776 whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
    777 cases sz cases sg normalize nodelta
    778 #H destruct
    779 cases v2 in H; normalize nodelta
    780 #H1 destruct
    781 #H2 destruct #Heq %{sz'} lapply Heq -Heq
    782 cases sz' in i'; #i' 
    783 whd in match (intsize_eq_elim ???????);
    784 cases H1 in H2; #j' normalize nodelta
    785 #Heq destruct (Heq)
    786 %{i'} %{j'} @conj try @conj try @conj try @refl
    787 qed.
    788 
    789 
    790 lemma sem_mul_inversion :
    791   ∀sz,sg.
    792   ∀v1,v2,res.
    793   sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    794   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    795               res = Vint sz' (short_multiplication ? i1 i2).
    796 #sz #sg *
    797 [ | #sz' #i' | | #p' ]
    798 #v2 #res
    799 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    800 cases sz cases sg normalize nodelta
    801 #H destruct
    802 cases v2 in H; normalize nodelta
    803 #H1 destruct
    804 #H2 destruct #Heq %{sz'} lapply Heq -Heq
    805 cases sz' in i'; #i' 
    806 whd in match (intsize_eq_elim ???????);
    807 cases H1 in H2; #j' normalize nodelta
    808 #Heq destruct (Heq)
    809 %{i'} %{j'} @conj try @conj try @conj try @refl
    810 qed.
    811 
    812 
    813 lemma sem_div_inversion_s :
    814   ∀sz.
    815   ∀v1,v2,res.
    816   sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
    817   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    818               match division_s ? i1 i2 with
    819               [ Some q ⇒  res =  (Vint sz' q)
    820               | None ⇒ False ].
    821 #sz *
    822 [ | #sz' #i' | | #p' ]
    823 #v2 #res
    824 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    825 >type_eq_dec_true normalize nodelta
    826 #H destruct
    827 cases v2 in H; normalize nodelta
    828 [ | #sz2' #i2' | | #p2' ]
    829 #Heq destruct
    830 %{sz'}
    831 lapply Heq -Heq
    832 cases sz' in i'; #i' 
    833 whd in match (intsize_eq_elim ???????);
    834 cases sz2' in i2'; #i2' normalize nodelta
    835 whd in match (option_map ????); #Hdiv destruct
    836 %{i'} %{i2'} @conj try @conj try @conj try @refl
    837 cases (division_s ???) in Hdiv;
    838 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    839 qed.
    840 
    841 lemma sem_div_inversion_u :
    842   ∀sz.
    843   ∀v1,v2,res.
    844   sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
    845   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    846               match division_u ? i1 i2 with
    847               [ Some q ⇒  res =  (Vint sz' q)
    848               | None ⇒ False ].
    849 #sz *
    850 [ | #sz' #i' | | #p' ]
    851 #v2 #res
    852 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    853 >type_eq_dec_true normalize nodelta
    854 #H destruct
    855 cases v2 in H; normalize nodelta
    856 [ | #sz2' #i2' | | #p2' ]
    857 #Heq destruct
    858 %{sz'}
    859 lapply Heq -Heq
    860 cases sz' in i'; #i' 
    861 whd in match (intsize_eq_elim ???????);
    862 cases sz2' in i2'; #i2' normalize nodelta
    863 whd in match (option_map ????); #Hdiv destruct
    864 %{i'} %{i2'} @conj try @conj try @conj try @refl
    865 cases (division_u ???) in Hdiv;
    866 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    867 qed.
    868 
    869 lemma sem_mod_inversion_s :
    870   ∀sz.
    871   ∀v1,v2,res.
    872   sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
    873   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    874               match modulus_s ? i1 i2 with
    875               [ Some q ⇒  res =  (Vint sz' q)
    876               | None ⇒ False ].
    877 #sz *
    878 [ | #sz' #i' | | #p' ]
    879 #v2 #res
    880 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    881 >type_eq_dec_true normalize nodelta
    882 #H destruct
    883 cases v2 in H; normalize nodelta
    884 [ | #sz2' #i2' | | #p2' ]
    885 #Heq destruct
    886 %{sz'}
    887 lapply Heq -Heq
    888 cases sz' in i'; #i' 
    889 whd in match (intsize_eq_elim ???????);
    890 cases sz2' in i2'; #i2' normalize nodelta
    891 whd in match (option_map ????); #Hdiv destruct
    892 %{i'} %{i2'} @conj try @conj try @conj try @refl
    893 cases (modulus_s ???) in Hdiv;
    894 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    895 qed.
    896 
    897 lemma sem_mod_inversion_u :
    898   ∀sz.
    899   ∀v1,v2,res.
    900   sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
    901   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    902               match modulus_u ? i1 i2 with
    903               [ Some q ⇒  res =  (Vint sz' q)
    904               | None ⇒ False ].
    905 #sz *
    906 [ | #sz' #i' | | #p' ]
    907 #v2 #res
    908 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
    909 >type_eq_dec_true normalize nodelta
    910 #H destruct
    911 cases v2 in H; normalize nodelta
    912 [ | #sz2' #i2' | | #p2' ]
    913 #Heq destruct
    914 %{sz'}
    915 lapply Heq -Heq
    916 cases sz' in i'; #i' 
    917 whd in match (intsize_eq_elim ???????);
    918 cases sz2' in i2'; #i2' normalize nodelta
    919 whd in match (option_map ????); #Hdiv destruct
    920 %{i'} %{i2'} @conj try @conj try @conj try @refl
    921 cases (modulus_u ???) in Hdiv;
    922 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl
    923 qed.
    924 
    925 lemma sem_and_inversion :
    926   ∀v1,v2,res.
    927   sem_and v1 v2 = Some ? res →
    928   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    929               res = Vint sz' (conjunction_bv ? i1 i2).
    930 *
    931 [ | #sz' #i' | | #p' ]
    932 #v2 #res
    933 whd in ⊢ ((??%?) → ?);
    934 #H destruct
    935 cases v2 in H; normalize nodelta
    936 [ | #sz2' #i2' | | #p2' ]
    937 #Heq destruct
    938 %{sz'}
    939 lapply Heq -Heq
    940 cases sz' in i'; #i' 
    941 whd in match (intsize_eq_elim ???????);
    942 cases sz2' in i2'; #i2' normalize nodelta
    943 #H destruct
    944 %{i'} %{i2'} @conj try @conj try @conj try @refl
    945 qed.
    946 
    947 lemma sem_or_inversion :
    948   ∀v1,v2,res.
    949   sem_or v1 v2 = Some ? res →
    950   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    951               res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
    952 *
    953 [ | #sz' #i' | | #p' ]
    954 #v2 #res
    955 whd in ⊢ ((??%?) → ?);
    956 #H destruct
    957 cases v2 in H; normalize nodelta
    958 [ | #sz2' #i2' | | #p2' ]
    959 #Heq destruct
    960 %{sz'}
    961 lapply Heq -Heq
    962 cases sz' in i'; #i' 
    963 whd in match (intsize_eq_elim ???????);
    964 cases sz2' in i2'; #i2' normalize nodelta
    965 #H destruct
    966 %{i'} %{i2'} @conj try @conj try @conj try @refl
    967 qed.
    968 
    969 lemma sem_xor_inversion :
    970   ∀v1,v2,res.
    971   sem_xor v1 v2 = Some ? res →
    972   ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
    973               res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
    974 *
    975 [ | #sz' #i' | | #p' ]
    976 #v2 #res
    977 whd in ⊢ ((??%?) → ?);
    978 #H destruct
    979 cases v2 in H; normalize nodelta
    980 [ | #sz2' #i2' | | #p2' ]
    981 #Heq destruct
    982 %{sz'}
    983 lapply Heq -Heq
    984 cases sz' in i'; #i' 
    985 whd in match (intsize_eq_elim ???????);
    986 cases sz2' in i2'; #i2' normalize nodelta
    987 #H destruct
    988 %{i'} %{i2'} @conj try @conj try @conj try @refl
    989 qed.
    990 
    991 lemma sem_shl_inversion :
    992   ∀v1,v2,res.
    993   sem_shl v1 v2 = Some ? res →
    994   ∃sz1,sz2,i1,i2.
    995               v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
    996               res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
    997                                   (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
    998               lt_u (bitsize_of_intsize sz2) i2
    999                    (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
    1000 *
    1001 [ | #sz' #i' | | #p' ]
    1002 #v2 #res
    1003 whd in ⊢ ((??%?) → ?);
    1004 #H destruct
    1005 cases v2 in H; normalize nodelta
    1006 [ | #sz2' #i2' | | #p2' ]
    1007 #Heq destruct
    1008 %{sz'} %{sz2'}
    1009 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
    1010 %{i'} %{i2'}
    1011 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
    1012 qed.
    1013 
    1014 lemma sem_shr_inversion :
    1015   ∀v1,v2,sz,sg,res.
    1016   sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
    1017   ∃sz1,sz2,i1,i2.
    1018               v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
    1019               lt_u (bitsize_of_intsize sz2) i2
    1020                    (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
    1021               match sg with
    1022               [ Signed ⇒
    1023                  res =
    1024                    (Vint sz1
    1025                     (shift_right bool (7+pred_size_intsize sz1*8)
    1026                      (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
    1027                      (head' bool (7+pred_size_intsize sz1*8) i1)))               
    1028               | Unsigned ⇒
    1029                  res =
    1030                    (Vint sz1
    1031                     (shift_right bool (7+pred_size_intsize sz1*8)
    1032                      (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
    1033               ].
    1034 *
    1035 [ | #sz' #i' | | #p' ]
    1036 #v2 #sz * #res
    1037 whd in ⊢ ((??%?) → ?);
    1038 whd in match (classify_aop ??);
    1039 >type_eq_dec_true normalize nodelta
    1040 #H destruct
    1041 cases v2 in H; normalize nodelta
    1042 [ | #sz2' #i2' | | #p2'
    1043 | | #sz2' #i2' | | #p2' ]
    1044 #Heq destruct
    1045 %{sz'} %{sz2'}
    1046 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
    1047 %{i'} %{i2'}
    1048 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
    1049 qed.
    1050 
    1051 lemma complete_cmp_inversion :
    1052   ∀ty:type.
    1053   ∀e:expr (ASTint I8 Unsigned).
    1054   ∀r:expr (typ_of_type ty).
    1055    complete_cmp ty e = return r →
    1056    ∃sz,sg. ty = Tint sz sg ∧
    1057            r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
    1058 *
    1059 [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1060 | #structname #fieldspec | #unionname #fieldspec | #id ]
    1061 #e whd in match (typ_of_type ?);
    1062 #r whd in ⊢ ((??%%) → ?);
    1063 #H destruct
    1064 %{sz} %{sg} @conj try @refl @refl_jmeq
    1065 qed.
    1066 
    1067 
    1068 lemma sem_cmp_int_inversion :
    1069   ∀v1,v2,sz,sg,op,m,res.
    1070    sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
    1071    ∃sz,i1,i2. v1 = Vint sz i1 ∧
    1072               v2 = Vint sz i2 ∧
    1073     match sg with
    1074     [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
    1075     | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
    1076     ].
    1077 #v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
    1078 whd in ⊢ ((??%?) → ?);
    1079 whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
    1080 cases v1
    1081 [ | #sz #i | | #p ] normalize nodelta
    1082 #H destruct
    1083 cases v2 in H;
    1084 [ | #sz' #i' | | #p' ] normalize nodelta
    1085 #H destruct lapply H -H
    1086 cases sz in i; #i
    1087 cases sz' in i'; #i' cases sg normalize nodelta
    1088 whd in match (intsize_eq_elim ???????); #H destruct
    1089 [ 1,2: %{I8}
    1090 | 3,4: %{I16}
    1091 | 5,6: %{I32} ] 
    1092 %{i} %{i'} @conj try @conj try @refl
    1093 qed.
    1094 
    1095 lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr.
    1096 #ty' * // qed.
    1097 
    1098 lemma sem_cmp_ptr_inversion :
    1099   ∀v1,v2,ty',n,op,m,res.
    1100    sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
    1101    (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
    1102                  valid_pointer m p1 = true ∧
    1103                  valid_pointer m p2 = true ∧
    1104                  (if eq_block (pblock p1) (pblock p2)
    1105                   then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
    1106                   else sem_cmp_mismatch op) = Some ? res) ∨
    1107    (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
    1108    (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
    1109    (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
    1110 * [ | #sz #i | | #p ] normalize nodelta
    1111 #v2 #ty' #n #op
    1112 * #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
    1113 whd in match (classify_cmp ??); cases n normalize nodelta
    1114 [ 2,4,6,8: #array_len ]
    1115 whd in match (ptr_type ty' ?);
    1116 whd in match (if_type_eq ?????);
    1117 >type_eq_dec_true normalize nodelta
    1118 #H destruct
    1119 cases v2 in H; normalize nodelta
    1120 [ | #sz' #i' | | #p'
    1121 | | #sz' #i' | | #p'
    1122 | | #sz' #i' | | #p'
    1123 | | #sz' #i' | | #p' ]
    1124 #H destruct
    1125 try /6 by or_introl, or_intror, ex_intro, conj/
    1126 [ 1: %1 %1 %2 %{p} @conj try @conj //
    1127 | 3: %1 %1 %2 %{p} @conj try @conj //
    1128 | *: %1 %1 %1 %{p} %{p'}
    1129      cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
    1130      cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
    1131      try @conj try @conj try @conj try @conj try @conj try @refl try @H
    1132      destruct
    1133 ] qed.
    1134 
    1135 lemma pointer_translation_eq_block :
    1136   ∀E,p1,p2,p1',p2'.
    1137   pointer_translation p1 E = Some ? p1' →
    1138   pointer_translation p2 E = Some ? p2' →
    1139   eq_block (pblock p1) (pblock p2) = true →
    1140   eq_block (pblock p1') (pblock p2') = true.
    1141 #E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
    1142 #H1 #H2 #Heq_block
    1143 lapply (eq_block_to_refl … Heq_block) #H destruct (H)
    1144 lapply H1 lapply H2 -H1 -H2
    1145 whd in ⊢ ((??%?) → (??%?) → ?);
    1146 cases (E b2) normalize nodelta
    1147 [ #Habsurd destruct ]
    1148 * #bx #ox normalize nodelta #Heq1 #Heq2 destruct
    1149 @eq_block_b_b
    1150 qed.
    1151 
    1152 
    1153435(* avoid a case analysis on type inside of a big proof *)
    1154436lemma match_type_inversion_aux : ∀ty,e,f.
     
    1178460qed.
    1179461
    1180  
    1181462
    1182463(* The two following lemmas are just noise. *)
     
    1222503qed.
    1223504
     505lemma sign_ext_sign_ext_reduce :
     506  ∀i. sign_ext 32 16 (sign_ext 16 32 i) = i.
     507#i @refl
     508qed. 
     509
     510lemma sign_ext_zero_ext_reduce :
     511  ∀i. sign_ext 32 16 (zero_ext 16 32 i) = i.
     512#i @refl
     513qed.
     514
     515(* There are two zero_ext, and this causes the "disambiguator" to fail. So we do
     516 * the cleanup ourselves. *)
     517
     518definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext.
     519definition 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. *)
     524lemma 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
     531lemma 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
     538lemma 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
     544cases v in Hexec;
     545[ | #vsz #i | | #p ]
     546cases 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 ]
     551whd 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*)
     568lemma 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
     602qed.
    1224603
    1225604(* TODOs : there are some glitches between clight and cminor :
     
    1307686     cases op
    1308687     whd in ⊢ (? → ? → (??%?) → ?);
    1309      [ 1: (* add *)
     688     [ 1: (* add *) 
    1310689       lapply (classify_add_inversion (typeof e1) (typeof e2))
    1311690       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     
    1500879              whd in match (eval_expr ???????);
    1501880              whd in match (eval_expr ???????);
     881              whd in match (proj2 ???);
    1502882              [ >(eval_expr_rewrite_aux … Heval_rhs)
    1503883              | >Heval_rhs ]
     
    1506886       | 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    1507887            whd in match (eval_expr ???????);
     888            whd in match (proj2 ???);
     889            whd in match (eval_expr ???????);
     890            whd in match (proj1 ???);
    1508891            whd in match (eval_expr ???????);
    1509892            >Heval_rhs normalize nodelta
    1510893            whd in match (eval_unop ????);
    1511894       ]
    1512        [ 1: (* ptr/ptr sub *)
     895       [ 1:       
     896        (* ptr/ptr sub *)
    1513897            whd in Hsem_binary:(??%?);
    1514898            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     899            -Hsem_binary
    1515900            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1516             lapply (sem_sub_pp_inversion … Hsem_binary_translated) *
     901            lapply (sem_sub_pp_inversion … Hsem_binary_translated)
     902            * #ty_sz' * #ty_sg' * #Heq destruct (Heq) *
    1517903            [ (* regular pointers case *)
    1518904              * #lhs_ptr * #rhs_ptr * #resulting_offset * * * *
     
    1524910              whd in match (m_bind ?????);
    1525911              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); *)
    1526916              (* size mismatch between CL and CM. TODO *)
    1527               @cthulhu
     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 ]
    1528926            | (* null pointers case *)
    1529927              * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct
     
    1537935              whd in match (m_bind ?????);
    1538936              whd in match (pred_size_intsize ?);
    1539               %{(zero_ext ty_sz (Vint I16 (zero (S (7+1*8)))))} @conj
     937              %{(zero_ext ty_sz' (Vint I32 (zero (S (7+3*8)))))} @conj
    1540938              [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ]
    1541939              whd in Hsem_binary_translated:(??%?);
    1542940              normalize nodelta in Hsem_binary_translated:(??%?);
    1543               lapply Hsem_binary_translated; -Hsem_binary_translated;
     941              lapply Hsem_binary_translated; -Hsem_binary_translated
    1544942              cases n1 cases n2
    1545943              [ | 2,3: #n | #n1 #n2 ] normalize nodelta
    1546944              #Heq destruct (Heq)
    1547               (* size mismatch between CL and CM. TODO *)
    1548               @cthulhu
     945              whd in match (zero_ext ??);
     946              cases ty_sz' in Hvalue_eq_res; try //
    1549947            ]
    1550948       | 2: (* int/int sub *)
     
    1565963       | 3: (* ptr/int sub *)
    1566964            whd in Hsem_binary:(??%?);
    1567             lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     965            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary
    1568966            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
    1569967            lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated
     
    1573971            whd in match (eval_unop ????);
    1574972            -Heval_lhs -Heval_rhs destruct
     973            whd in match (proj2 ???);
     974            whd in match (proj1 ???);
    1575975            whd in match (proj2 ???);           
     976            whd in match (eval_expr ???????);
    1576977            @(match sg
    1577978              return λs. sg = s → ?
     
    1580981              | Signed ⇒ λHsg. ?
    1581982              ] (refl ??)) normalize nodelta
    1582             whd in match (eval_expr ???????);
     983            whd in match (eval_unop ????);
    1583984            whd in match (m_bind ?????);
    1584985            whd in match (eval_binop ???????);
    1585986            [ 1,2:
    1586                 %{(Vptr
    1587                   (neg_shift_pointer_n (bitsize_of_intsize cm_vsz) lhs_ptr (sizeof ty') sg
    1588                    cm_rhs_v))} try @conj try assumption
    1589                    (* TODO size mismatch (?) or insert zero/sign_ext in semantics *)
    1590                    (*            [ 1,2,3,4: @conj whd in match (E0);
    1591                         whd in match (Eapp trace_rhs ?);
    1592                         whd in match (Eapp trace_lhs ?);                     
    1593                         >(append_nil … trace_rhs) try @refl
    1594                         >(append_nil … trace_lhs) try @refl
    1595                         @(value_eq_triangle_diagram … Hvalue_eq_res)
    1596                         whd in match (shift_pointer_n ?????);
    1597                         whd in match (shift_offset_n ?????);
    1598                         >Hsg normalize nodelta
    1599                         >commutative_short_multiplication
    1600                         whd in match (shift_pointer ???);
    1601                         whd in match (shift_offset ???);
    1602                         >sign_ext_same_size @refl *)                   
    1603                 @cthulhu ]
     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            ]
    16041016            [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
    1605             | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]
    1606             >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
    1607             >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
     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
    16081024           normalize >append_nil try @refl
    16091025       ]     
     
    19131329            cases (bind_inversion ????? Hexec) -Hexec
    19141330            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1915             lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1916             whd in match (typeof ?); whd in match (sem_binary_operation ??????);
    1917             #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
     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
    19181338            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
    19191339            destruct (Hcl_lhs) destruct (Hcl_rhs)
     
    19391359            whd in match (opt_to_res ???);
    19401360            whd in match (m_bind ?????);
    1941             (* finished modulo glitch in integer widths *)
    1942             @cthulhu
    1943        | *:
     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 *)
    19441383            #n #ty' #Hety1 #Hety2 #Hclassify
    19451384            lapply (jmeq_to_eq ??? Hety1) #Hety1'
     
    19611400            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    19621401            lapply (opt_to_res_inversion ???? Hsem) -Hsem
    1963             whd in match (typeof ?); whd in match (sem_binary_operation ??????);
    1964             #Hsem_cmp (* cut > *)
     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);
    19651406            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
    19661407            * #Hyp_present_lhs #Hyp_present_rhs
    19671408            #Hind_rhs #Hind_lhs
    19681409            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
    1969             * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1410            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs -Hexec_rhs
    19701411            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
    1971             * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
    1972             lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp)
     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
    19731414            -Hvalue_eq_lhs -Hvalue_eq_rhs
    1974             * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res %{cm_val} @conj try assumption
    1975             lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm -Hsem_cmp
     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
    19761422            *
    19771423            [ 2,4,6,8,10,12:
    1978               * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1424              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
     1425              whd in Hsem_cmp:(??%?); destruct
    19791426            | *: *
    19801427              [ 2,4,6,8,10,12:
    1981                 * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
     1428                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
     1429                whd in Hsem_cmp:(??%?); destruct
    19821430              | *: *
    19831431                [ 2,4,6,8,10,12:
    1984                   * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
    1985                 | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
    1986             ] ] ]
    1987             whd in match (eval_expr ???????);
    1988             whd in match (eval_expr ???????);
    1989             whd in Hsem_cmp:(??%?);
    1990             destruct (Hsem_cmp)                       
    1991             >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
    1992             >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
    1993             whd in match (m_bind ?????);
     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            ]
    19941439            whd in match (eval_binop ???????);
    1995             [ 1,2,3,4,5,6:
    1996               (* qed modulo integer width glitch *)
    1997               @cthulhu
     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              ]
    19981454            | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
    19991455                 lapply Heq_block_outcome -Heq_block_outcome
    20001456                 @(eq_block_elim … (pblock p1) (pblock p2))
    20011457                 normalize nodelta
     1458                 whd in match (eval_unop ????);
     1459                 whd in match (opt_to_res ???);
     1460                 whd in match (m_bind ?????);
    20021461                 [ 1,3,5,7,9,11:
    20031462                   #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
    20041463                   whd in match (eval_unop ????);
    20051464                   whd in match (m_bind ?????);
    2006                    cases (cmp_offset ???) normalize nodelta
    2007                    (* glitch *)
    2008                    @cthulhu
     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                   ]
    20091472                 | *:
    20101473                   #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    2011                    whd in match (eval_unop ????);
    2012                    whd in match (m_bind ?????);
    2013                    @cthulhu
    2014                  ]
     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                ]
    20151481           ]
    20161482       ]
     
    22071673       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
    22081674       #Hind #Htranslate_expr #Hexec_cl
    2209        cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
     1675       cases (bind_inversion ????? Htranslate_expr) (* -Htranslate_expr *)
    22101676       * whd in match (typ_of_type ?); normalize nodelta
    22111677       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
     
    22151681       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
    22161682       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
    2217        [ 1,3,5,7: @cthulhu ]
     1683       [ 1,3,5,7: @(translate_expr_deref_present … Htranslate_expr … Hyp_present … Htranslate_expr_ind) ]
    22181684       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
    22191685       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
     
    22311697       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
    22321698       -Hopt_to_res
     1699       lapply Hexec_cm_ind -Hexec_cm_ind
    22331700       lapply Hyp_present -Hyp_present
     1701       lapply Htranslate_expr -Htranslate_expr
    22341702       lapply Hexpr_vars -Hexpr_vars
    22351703       lapply cm_expr -cm_expr
    2236        inversion (access_mode ty)
    2237        [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
    2238        lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
    2239        #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
     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
    22401711       #Heq destruct (Heq)
    2241        [ 1,2,3,4: (* By_value *)
     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 *)
    22421718           (* project Hcl_load_success in Cminor through memory_inj *)
    22431719           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
    2244            [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
     1720           try @(load_by_value_success_valid_pointer … Hcl_load_success)
     1721           try @jmeq_to_eq
     1722           try assumption try @refl_jmeq
    22451723           * #cm_val * #Hcm_load_success #Hvalue_eq
    2246            lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
     1724           lapply (load_value_of_type_by_value … Hcm_load_success)
     1725           try @refl
    22471726           #Hloadv_cm
    22481727           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
    2249            >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
    2250       | *: (* By reference *)
    2251            >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
    2252            lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
    2253            #Hval >Hval %4 assumption ]
     1728           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption ]
    22541729  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
    22551730       lapply (refl ? (typeof e1))
     
    27162191    normalize %{cm_val2} @conj try @refl assumption ]
    27172192| 10: (* andbool *)
    2718   #ty cases ty
     2193  #ty
     2194  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
     2195  cases ty
    27192196  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    27202197  | #structname #fieldspec | #unionname #fieldspec | #id ]
    2721   #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
    27222198  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
    27232199  (* decompose first slice of clight execution *)
     
    27252201  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
    27262202  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2727   #b * #Hexec_bool_of_val #Hexec_expr
    2728   (* decompose translation to Cminor *)
     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) ]
    27292216  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
    27302217  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
    27312218  cases (bind_inversion ????? Htranslate) -Htranslate
    2732   * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
    2733   [ 2: | *: #Heq destruct (Heq) ]
    2734   (* discriminate I16 and I8 cases *)
    2735 (*  lapply Hyp_present -Hyp_present
    2736   lapply Hexpr_vars -Hexpr_vars
    2737   lapply cm_expr -cm_expr cases sz
    2738   #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
    2739   [ 1,2: #Habsurd destruct (Habsurd) ]   *)
    2740   (* go on with decomposition *)
    2741   #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
    2742   * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
     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
    27432224  (* cleanup the type coercion *)
    2744   lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
    2745   * #Htypeof_e2_eq_ty
    27462225  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
    2747   lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
     2226  lapply Hexpr_vars_wt -Hexpr_vars_wt
    27482227  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
    27492228  lapply Hexpr_vars_e2 -Hexpr_vars_e2
    27502229  lapply cm_expr_e2 -cm_expr_e2
    2751   lapply Hexec_expr -Hexec_expr
    2752   >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
    2753   #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
    2754   #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
    2755   (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
    2756    * to proceed in decomposing translation. *)
     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)
    27572234  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
    27582235  lapply Hexpr_vars_e1 -Hexpr_vars_e1
    27592236  lapply cm_expr_e1 -cm_expr_e1
    2760   lapply Hexec_bool_of_val -Hexec_bool_of_val
    2761   cases (typeof e1)
    2762   [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
    2763   | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
    2764   #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
    2765   normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    2766   (* translation decomposition terminated. Reduce goal *)
     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
    27672360  whd in match (eval_expr ???????);
    2768   (* We need Hind1.  *)
    2769   cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
    2770   lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
     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 ]
    27712368  normalize nodelta
    2772   (* peform case analysis to further reduce the goal. *)
    2773   lapply Hvalue_eq -Hvalue_eq
    2774   lapply Hexec_bool_of_val -Hexec_bool_of_val
    2775   whd in match (proj2 ???);
    2776   cases cl_val_e1
    2777   [ | #vsz #vi | | #vp
    2778   | | #vsz #vi | | #vp
    2779   | | #vsz #vi | | #vp
    2780   | | #vsz #vi | | #vp ]
    2781   whd in ⊢ ((??%%) → ?);
    2782   [ 6:
    2783   | *: #Heq destruct (Heq) ]
    2784   #Hsz_check #Hvalue_eq
    2785   lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
    2786   * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
    2787   (* preparing case analysis on b *)
    2788   lapply Hexec_expr -Hexec_expr
    2789   cases b normalize nodelta
    2790   [ 2: (* early exit *)
    2791        #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
    2792        #Heq_outcome destruct (Heq_outcome) -Heq_outcome
    2793        >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
    2794        <e0 whd in match (m_bind ?????);
    2795        @cthulhu
    2796        (* Pb: incompatible semantics for cl and cm.
    2797         * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
    2798           first operand is false (for andbool)
    2799           . solution 1 : change semantics to return actual value instead of Vfalse
    2800           . solution 2 : change toCminor to introduce another test in the program,
    2801             returning Vfalse in case of failure instead of actual value
    2802         *) ]
    2803   #Hexec_expr #Heq_outcome
    2804   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2805   * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
    2806   cases (bind_inversion ????? Hexec_expr) -Hexec_expr
    2807   #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
    2808   #Heq destruct (Heq)
    2809   >(value_eq_int_inversion … Hvalue_eq)
    2810   whd in match (eval_bool_of_val ?);
    2811   destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
     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
    28122372  normalize nodelta
    2813   cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
    2814   >Heval_expr normalize nodelta
    2815   %{cm_val_e2} @conj try @refl 
    2816   whd in Hexec_bool_outcome:(??%%);
    2817   normalize nodelta in Hexec_bool_outcome:(??%%);
    2818   lapply Hvalue_eq2 -Hvalue_eq2
    2819   -Heval_expr
    2820   lapply Hexec_bool_outcome -Hexec_bool_outcome
    2821   cases cl_val_e2
    2822   [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
    2823   #Heq destruct (Heq)
    2824   cases (intsize_eq_elim_inversion ??????? Heq)
    2825   #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
    2826   cases outcome_bool normalize nodelta
    2827   (* Problem. cf prev case. *)
    2828   @cthulhu
    2829 | 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
     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 ]
    28302401| 12: (* sizeof *)
    28312402  #ty cases ty
     
    28722443       * #BL #OFF normalize nodelta #Heq destruct (Heq)
    28732444       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
    2874        #H destruct (H)
    2875        (* again, mismatch in the size of the integers *)
    2876        @cthulhu
     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       
    28772454  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
    28782455       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
Note: See TracChangeset for help on using the changeset viewer.