Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2450 r2468  
    303303  let 〈s,vars,u〉 ≝ x in u.
    304304
    305 axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
    306 
    307305(* Proof that switch_removal_switch_free does its job. *)
    308306lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)).
     
    344342  match ed with
    345343  [ Econst_int _ _ ⇒ least_identifier
    346   | Econst_float _ ⇒ least_identifier
    347344  | Evar id ⇒ id
    348345  | Ederef e1 ⇒ max_of_expr e1
     
    604601   Simulation proof and related voodoo.
    605602   ----------------------------------------------------------------------------*)
    606 
     603(*
    607604definition expr_lvalue_ind_combined ≝
    608605λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    609606conj ??
    610607 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    611  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     608 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).*)
    612609 
    613610let rec expr_ind2
     
    615612    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
    616613    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
    617     (Iconst_float : ∀f, t. Q (Econst_float f) t)
    618614    (Ivar : ∀id, t. Q (Evar id) t)
    619615    (Ideref : ∀e, t. P e → Q (Ederef e) t)
     
    630626    (e : expr) on e : P e ≝
    631627match e with
    632 [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ]
     628[ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ]
    633629
    634630and expr_desc_ind2
     
    636632    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
    637633    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
    638     (Iconst_float : ∀f, t. Q (Econst_float f) t)
    639634    (Ivar : ∀id, t. Q (Evar id) t)
    640635    (Ideref : ∀e, t. P e → Q (Ederef e) t)
     
    652647match ed with
    653648[ Econst_int sz i ⇒ Iconst_int sz i t
    654 | Econst_float f ⇒ Iconst_float f t
    655649| Evar id ⇒ Ivar id t
    656 | Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    657 | Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    658 | Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    659 | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
    660 | Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    661 | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
    662 | Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
    663 | Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
     650| Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
     651| Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
     652| Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
     653| Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
     654| Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
     655| Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
     656| Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
     657| Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
    664658| Esizeof sizeoft ⇒ Isizeof sizeoft t
    665 | Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
    666 | Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e)
     659| Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
     660| Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e)
    667661].
    668662
     
    18021796(* case analysis on access mode of [ty] *)
    18031797cases ty
    1804 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1805 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1798[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1799| #structname #fieldspec | #unionname #fieldspec | #id ]
    18061800whd in ⊢ ((??%?) → (?%?));
    1807 [ 1,5,6,7,8: #Habsurd destruct ]
     1801[ 1,4,5,6,7: #Habsurd destruct ]
    18081802whd in ⊢ (? → (??(λ_.?(??%?)?)));
    18091803lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m'
    18101804elim (fe_to_be_values ??)
    1811 [ 1,3,5,7: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize //
    1812 | 2,4,6,8: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H
    1813            cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq
    1814            lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq)
    1815            * #m_ext'' * #Hstore_eq2 #Hext2
    1816            lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' *
    1817            #Hstoren' #Hext3
    1818            %{m_ext'} @conj try assumption
    1819            whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta
    1820            @Hstoren'
     1805[ 1,3,5: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize //
     1806| 2,4,6: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H
     1807         cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq
     1808         lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq)
     1809         * #m_ext'' * #Hstore_eq2 #Hext2
     1810         lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' *
     1811         #Hstoren' #Hext3
     1812         %{m_ext'} @conj try assumption
     1813         whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta
     1814         @Hstoren'
    18211815] qed.
    18221816
     
    18391833#ty #off #v #m2'
    18401834cases ty
    1841 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1842 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1835[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1836| #structname #fieldspec | #unionname #fieldspec | #id ]
    18431837whd in ⊢ ((??%?) → ?);
    1844 [ 1,5,6,7,8: #Habsurd destruct ]
     1838[ 1,4,5,6,7: #Habsurd destruct ]
    18451839lapply Hext lapply m1 lapply m2 lapply m2' lapply off -Hext -m1 -m2 -m2' -off -ty
    18461840elim (fe_to_be_values ??)
    1847 [ 1,3,5,7: #o #m2' #m2 #m1 #Hext normalize #Heq destruct assumption
     1841[ 1,3,5: #o #m2' #m2 #m1 #Hext normalize #Heq destruct assumption
    18481842| *: #hd #tl #Hind #o #m2_end #m2 #m1 #Hext whd in match (storen ???); #Hbestorev
    18491843     cases (some_inversion ????? Hbestorev) #m2' * #Hbestorev #Hstoren
    18501844     lapply (bestorev_writeable_memory_ext … Hext …  o hd Hmem … Hbestorev) #Hext'
    18511845     @(Hind … Hstoren) //
    1852 ] qed.    
     1846] qed.   
    18531847
    18541848(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
     
    21592153[ 1,2: cases (classify_cmp (typeof e1) (typeof e2))
    21602154     normalize nodelta
    2161      [ 1,5: #sz #sg try //
    2162      | 2,6: #opt #ty
     2155     [ 1,4: #sz #sg try //
     2156     | 2,5: #opt #ty
    21632157          cases v1 normalize nodelta
    2164           [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
    2165           [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
    2166           | 7,8: #H @H ]
     2158          [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ]
     2159          [ 1,2,3,4: #Habsurd destruct (Habsurd)
     2160          | 5,6: #H @H ]
    21672161          cases v2 normalize nodelta
    2168           [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
    2169           [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
    2170           | 7,8: #H @H ]
     2162          [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ]
     2163          [ 1,2,3,4: #Habsurd destruct (Habsurd)
     2164          | 5,6: #H @H ]
    21712165          lapply (Hvalid ptr)
    21722166          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
     
    21772171          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
    21782172          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
    2179      | 3,7: #fsz #H @H
    2180      | 4,8: #ty1 #ty2 #H @H ]
     2173     | 3,6: #ty1 #ty2 #H @H ]
    21812174| 3,4: cases (classify_cmp (typeof e1) (typeof e2))
    21822175     normalize nodelta
    2183      [ 1,5: #sz #sg try //
    2184      | 2,6: #opt #ty
     2176     [ 1,4: #sz #sg try //
     2177     | 2,5: #opt #ty
    21852178          cases v1 normalize nodelta
    2186           [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
    2187           [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
    2188           | 7,8: #H @H ]
     2179          [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ]
     2180          [ 1,2,3,4: #Habsurd destruct (Habsurd)
     2181          | 5,6: #H @H ]
    21892182          cases v2 normalize nodelta
    2190           [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
    2191           [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
    2192           | 7,8: #H @H ]
     2183          [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ]
     2184          [ 1,2,3,4: #Habsurd destruct (Habsurd)
     2185          | 5,6: #H @H ]
    21932186          lapply (Hvalid ptr)
    21942187          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
     
    21992192          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
    22002193          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
    2201      | 3,7: #fsz #H @H
    2202      | 4,8: #ty1 #ty2 #H @H ]
     2194     | 3,6: #ty1 #ty2 #H @H ]     
    22032195| 5,6: cases (classify_cmp (typeof e1) (typeof e2))
    22042196     normalize nodelta
    2205      [ 1,5: #sz #sg try //
    2206      | 2,6: #opt #ty
     2197     [ 1,4: #sz #sg try //
     2198     | 2,5: #opt #ty
    22072199          cases v1 normalize nodelta
    2208           [ 1,6: | 2,7: #sz #i | 3,8: #fl | 4,9: | 5,10: #ptr ]
    2209           [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
    2210           | 7,8: #H @H ]
     2200          [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ]
     2201          [ 1,2,3,4: #Habsurd destruct (Habsurd)
     2202          | 5,6: #H @H ]
    22112203          cases v2 normalize nodelta
    2212           [ 1,6: | 2,7: #sz' #i' | 3,8: #fl' | 4,9: | 5,10: #ptr' ]
    2213           [ 1,2,3,4,5,6: #Habsurd destruct (Habsurd)
    2214           | 7,8: #H @H ]
     2204          [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ]
     2205          [ 1,2,3,4: #Habsurd destruct (Habsurd)
     2206          | 5,6: #H @H ]
    22152207          lapply (Hvalid ptr)
    22162208          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
     
    22212213          [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ]
    22222214          #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H
    2223      | 3,7: #fsz #H @H
    2224      | 4,8: #ty1 #ty2 #H @H ]
     2215     | 3,6: #ty1 #ty2 #H @H ]
    22252216] qed.
    22262217
     
    22382229[ 1: #csz #cty #i #a1
    22392230     whd in match (exec_expr ????); elim cty
    2240      [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2231     [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    22412232     normalize nodelta
    22422233     [ 2: cases (eq_intsize csz sz) normalize nodelta
    22432234          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
    22442235          | 2: #Habsurd destruct (Habsurd) ]
    2245      | 4,5,6: #_ #H destruct (H)
     2236     | 3,4,5: #_ #H destruct (H)
    22462237     | *: #H destruct (H) ]
    2247 | 2: #ty #fl #a1
    2248      whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
    2249 | 3: *
    2250   [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2251   | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2238| 2: *
     2239  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
     2240  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    22522241  #ty whd in ⊢ (% → ?); #Hind try @I
    22532242  whd in match (Plvalue ???);
     
    22662255                    >(H v (refl ??)) @refl
    22672256  ] ] ]
    2268 | 4: #v #ty whd * * #b #o #tr
     2257| 3: #v #ty whd * * #b #o #tr
    22692258     whd in match (exec_lvalue' ?????);
    22702259     whd in match (exec_lvalue' ?????); cases Hdisjoint *
     
    22802269               #H @H
    22812270          | 2: #blo #Hlookup2 <(Hlookup2 (refl ??)) #Heq normalize nodelta @Heq ] ]
    2282 | 5: #e #ty whd in ⊢ (% → %);
     2271| 4: #e #ty whd in ⊢ (% → %);
    22832272     whd in match (exec_lvalue' ?????);
    22842273     whd in match (exec_lvalue' ?????);
     
    22862275     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H
    22872276     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
    2288 | 6: #ty #e #ty'
     2277| 5: #ty #e #ty'
    22892278     #Hsim @(exec_lvalue_expr_elim … Hsim)
    22902279     cases ty
    2291      [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2280     [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    22922281     * #b #o normalize nodelta try /2 by I/
    22932282     #tr @conj try @refl
    2294 | 7: #ty #op #e
     2283| 6: #ty #op #e
    22952284     #Hsim @(exec_expr_expr_elim … Hsim) #v #trace
    22962285     cases (sem_unary_operation op v (typeof e)) normalize nodelta
    22972286     try @I
    22982287     #v @conj @refl
    2299 | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
     2288| 7: #ty #op #e1 #e2 #Hsim1 #Hsim2
    23002289     @(exec_expr_expr_elim … Hsim1) #v #trace
    23012290     cases (exec_expr ge en1 m1 e2) in Hsim2;
     
    23092298     [ 1: #_ // ] #val #H >(H val (refl ??))
    23102299     normalize destruct @conj @refl
    2311 | 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
     2300| 8: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
    23122301     #v #tr
    23132302     cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty)
     
    23172306     [ 2: //
    23182307     | 1: #v normalize @conj @refl ]
    2319 | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
     2308| 9: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
    23202309     @(exec_expr_expr_elim … Hsim1) #v #tr
    23212310     cases (exec_bool_of_val ? (typeof e1)) #b
     
    23352324          | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta
    23362325               @conj @refl ] ]
    2337 | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
     2326| 10,11: #ty #e1 #e2 #Hsim1 #Hsim2
    23382327     @(exec_expr_expr_elim … Hsim1) #v #tr
    23392328     cases (exec_bool_of_val v (typeof e1))
     
    23502339     [ 2,4: #error normalize @I ]
    23512340     * normalize @conj @refl
    2352 | 13: #ty #ty' cases ty
    2353      [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
    2354      | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     2341| 12: #ty #ty' cases ty
     2342     [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    23552343     whd in match (exec_expr ????); whd #a #H @H
    2356 | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr
     2344| 13: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr
    23572345    whd in match (exec_lvalue' ?????);
    23582346    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
    23592347    whd in match (typeof ?);
    23602348    cases aggregty in Hsim;
    2361     [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
    2362     | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
     2349    [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
    23632350    normalize nodelta #Hsim
    2364     [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
     2351    [ 1,2,3,4,5,8: #Habsurd destruct (Habsurd) ]
    23652352    whd in match (m_bind ?????);
    23662353    whd in match (m_bind ?????);
     
    23712358    whd in match (exec_lvalue ge' en2 m2 (Expr ed ?));   
    23722359     >(H ? (refl ??)) normalize nodelta #H @H
    2373 | 15: #ty #l #e #Hsim
     2360| 14: #ty #l #e #Hsim
    23742361     @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj //
    2375 | 16: *
    2376   [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2377   | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2362| 15: *
     2363  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
     2364  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    23782365  #ty normalize in ⊢ (% → ?);
    2379   [ 3,4,13: @False_ind
     2366  [ 2,3,12: @False_ind
    23802367  | *: #_ normalize #a1 #Habsurd @Habsurd ]
    23812368] qed.
     
    25682555| 1: * #val #trace cases val
    25692556     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
    2570      | 3: #fl | 4: | 5: #ptr ]
     2557     | 3: | 4: #ptr ]
    25712558     %2 #sz #n #tr % #H destruct (H)
    25722559] qed.
     
    28002787         whd in match (exec_step ??) in Hexec_step;
    28012788         (* IV. Case analysis on the return type *)
    2802          cases (fn_return sss_func) in Hexec_step;
    2803          [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    2804          | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     2789         cases (fn_return sss_func) in Hexec_step;         
     2790         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     2791         | #structname #fieldspec | #unionname #fieldspec | #id ]
    28052792         normalize nodelta
    28062793         whd in ⊢ ((??%?) → ?);
     
    28862873         >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify
    28872874         cases (fn_return sss_func) in Hexec; normalize nodelta
    2888          [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    2889          | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     2875         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     2876         | #structname #fieldspec | #unionname #fieldspec | #id ]         
     2877(*         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     2878         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] *)
    28902879         #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl
    28912880         /3 by sws_returnstate, swc_call, memext_free_extended_environment/
     
    31953184             >fn_return_simplify
    31963185             cases (fn_return sss_func) normalize nodelta
    3197              [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    3198              | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     3186             [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     3187             | #structname #fieldspec | #unionname #fieldspec | #id ]
    31993188             [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl
    32003189                  /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/
     
    32203209        cases condval normalize nodelta
    32213210        [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    3222         | 3: #f * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    3223         | 4: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    3224         | 5: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
     3211        | 3: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     3212        | 4: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
    32253213        #sz #i * #Hexec_eq #Heq
    32263214        cut (∃sg. typeof cond = Tint sz sg) whd in Heq:(??%%); destruct (Heq)
    32273215        [ 1: cases (typeof cond) in Heq; normalize nodelta
    3228              [ 1: | 2: #sz' #sg' | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
    3229              | 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
     3216             [ | #sz' #sg' | #ptrty | #arrayty #arraysz | #domain #codomain
     3217             | #structname #fieldspec | #unionname #fieldspec | #id ]
    32303218             [ 2: cases (sz_eq_dec ??) normalize nodelta #H
    32313219                  [ 2: #Habsurd destruct
Note: See TracChangeset for help on using the changeset viewer.