Ignore:
Timestamp:
Jul 26, 2012, 5:02:52 PM (9 years ago)
Author:
garnier
Message:

Proof of correction for the semantics of expressions under memory injections terminated.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/switchRemoval.ma

    r2263 r2271  
    29802980] qed.
    29812981
     2982lemma cast_value_eq :
     2983 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 →
     2984  ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res →
     2985  ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'.
     2986#E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res
     2987@(value_eq_inversion … Hvalue_eq)
     2988[ 1: #v normalize #Habsurd destruct (Habsurd)
     2989| 2: #vsz #vi whd in match (exec_cast ????);
     2990     cases ty
     2991     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
     2992     normalize nodelta
     2993     [ 1,3,7,8,9: #Habsurd destruct (Habsurd)
     2994     | 2: @intsize_eq_elim_elim
     2995          [ 1: #Hneq #Habsurd destruct (Habsurd)
     2996          | 2: #Heq destruct (Heq) normalize nodelta
     2997               cases cast_ty
     2998               [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
     2999               | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
     3000               normalize nodelta
     3001               [ 1,7,8,9: #Habsurd destruct (Habsurd)
     3002               | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
     3003               | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/
     3004               | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
     3005                    @eq_bv_elim
     3006                    [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta
     3007                         whd in match (m_bind ?????);
     3008                         #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
     3009                    | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta
     3010                         whd in match (m_bind ?????);
     3011                         #Habsurd destruct (Habsurd) ] ]
     3012          ]
     3013     | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
     3014          @eq_bv_elim
     3015          [ 1,3,5: #Heq destruct (Heq) normalize nodelta
     3016               whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
     3017          | 2,4,6: #Hneq normalize nodelta
     3018               whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ]
     3019     ]
     3020| 3: #f whd in match (exec_cast ????);
     3021     cases ty
     3022     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
     3023     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
     3024     normalize nodelta
     3025     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
     3026     cases cast_ty
     3027     [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
     3028     | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
     3029     normalize nodelta
     3030     [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
     3031     #Heq destruct (Heq)
     3032     [ 1: /3 by ex_intro, conj, vint_eq/
     3033     | 2: /3 by ex_intro, conj, vfloat_eq/ ]
     3034| 4: whd in match (exec_cast ????);
     3035     cases ty
     3036     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
     3037     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
     3038     normalize
     3039     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
     3040     cases cast_ty normalize nodelta
     3041     [ 1,10,19: #Habsurd destruct (Habsurd)
     3042     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
     3043     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
     3044     | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
     3045     | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
     3046     | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
     3047     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
     3048     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
     3049     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
     3050| 5: #p1 #p2 #Hembed whd in match (exec_cast ????);
     3051     cases ty
     3052     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
     3053     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
     3054     normalize
     3055     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
     3056     cases cast_ty normalize nodelta
     3057     [ 1,10,19: #Habsurd destruct (Habsurd)
     3058     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
     3059     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
     3060     | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption
     3061     | 5,14,23: #carrayty #cn #Heq destruct (Heq)
     3062                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
     3063     | 6,15,24: #ctl #cretty #Heq destruct (Heq)
     3064                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
     3065     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
     3066     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
     3067     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
     3068qed.
     3069
     3070lemma bool_of_val_value_eq :
     3071 ∀E,v1,v2. value_eq E v1 v2 →
     3072   ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b.
     3073#E #v1 #v2 #Hvalue_eq #ty #b
     3074@(value_eq_inversion … Hvalue_eq) //
     3075[ 1: #v #H normalize in H; destruct (H)
     3076| 2: #p1 #p2 #Hembed #H @H ] qed.
    29823077 
    29833078(* Simulation relation on expressions *)
    … …  
    30973192     >Hopval_eq normalize destruct /2 by conj/
    30983193| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
    3099      #v1 #v2 #trace #Hvalue_eq (* TODO ... *) @cthulhu
    3100 | *: @cthulhu ] qed.
    3101 
    3102 (* TODO: Old cases, to be ported to memory injection.
    3103 | 8: #ty #op #e1 #e2 #Hind1 #Hind2
    3104      whd in match (exec_expr ge ???);   
    3105      whd in match (exec_expr ge' ???);
    3106      @(exec_expr_expr_elim … Hind1)
    3107      cases (exec_expr ge en1 m1 e2) in Hind2;
    3108      [ 2: #error normalize //
    3109      | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
    3110           #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
    3111           >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);
    3112 
    3113 
    3114 | 9: #ty #castty #e #Hind
    3115      whd in match (exec_expr ge ???);   
    3116      whd in match (exec_expr ge' ???);
    3117      cases Hind
    3118      [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3119      | 1: cases (exec_expr ge en m e)
    3120           [ 2: #error #_ @SimFail /2 by ex_intro/
    3121           | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
    3122           ]
    3123      ]
    3124 | 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
    3125      whd in match (exec_expr ge ???);   
    3126      whd in match (exec_expr ge' ???);
    3127      cases Hind1
    3128      [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3129      | 1: cases (exec_expr ge en m e1)
    3130           [ 2: #error #_ @SimFail /2 by ex_intro/
    3131           | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
    3132                normalize nodelta
    3133                cases (exec_bool_of_val ??)
    3134                [ 2: #error @SimFail /2 by ex_intro/
    3135                | 1: * whd in match (m_bind ?????); normalize nodelta
    3136                     [ 1: cases Hind2
    3137                          [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3138                          | 1: cases (exec_expr ge en m e2)
    3139                               [ 2: #error #_  @SimFail /2 by ex_intro/
    3140                               | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
    3141                                    @SimOk normalize nodelta #a2
    3142                                    whd in match (m_bind ?????); // ]
    3143                          ]
    3144                     | 2: cases Hind3
    3145                          [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3146                          | 1: cases (exec_expr ge en m e3)
    3147                               [ 2: #error #_  @SimFail /2 by ex_intro/
    3148                               | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
    3149                                    @SimOk normalize nodelta #a3
    3150                                    whd in match (m_bind ?????); // ]
    3151                          ]
    3152      ] ] ] ]                     
    3153 | 11: #ty #e1 #e2 #Hind1 #Hind2
    3154      whd in match (exec_expr ge ???);   
    3155      whd in match (exec_expr ge' ???);
    3156      cases Hind1
    3157      [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3158      | 1: cases (exec_expr ge en m e1)
    3159           [ 2: #error #_ @SimFail /2 by ex_intro/
    3160           | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
    3161                normalize nodelta
    3162                cases (exec_bool_of_val ??)
    3163                [ 2: #error @SimFail /2 by ex_intro/
    3164                | 1: * whd in match (m_bind ?????);
    3165                     [ 2: @SimOk // ]
    3166                     cases Hind2
    3167                     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3168                     | 1: cases (exec_expr ge en m e2)
    3169                          [ 2: #error #_  @SimFail /2 by ex_intro/
    3170                          | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
    3171                               @SimOk #a2
    3172                               whd in match (m_bind ?????); //
    3173      ] ] ] ] ]
    3174 | 12: #ty #e1 #e2 #Hind1 #Hind2
    3175      whd in match (exec_expr ge ???);   
    3176      whd in match (exec_expr ge' ???);
    3177      cases Hind1
    3178      [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3179      | 1: cases (exec_expr ge en m e1)
    3180           [ 2: #error #_ @SimFail /2 by ex_intro/
    3181           | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
    3182                normalize nodelta
    3183                cases (exec_bool_of_val ??)
    3184                [ 2: #error @SimFail /2 by ex_intro/
    3185                | 1: * whd in match (m_bind ?????);
    3186                     [ 1: @SimOk // ]
    3187                     cases Hind2
    3188                     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3189                     | 1: cases (exec_expr ge en m e2)
    3190                          [ 2: #error #_  @SimFail /2 by ex_intro/
    3191                          | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
    3192                               @SimOk #a2
    3193                               whd in match (m_bind ?????); //
    3194      ] ] ] ] ]
    3195 | 13: #ty #sizeof_ty
    3196      whd in match (exec_expr ge ???);   
    3197      whd in match (exec_expr ge' ???);
    3198      @SimOk //
    3199 | 14: #ty #e #ty' #fld #Hind
    3200      whd in match (exec_lvalue' ge ????);
    3201      whd in match (exec_lvalue' ge' ????);
    3202      whd in match (typeof ?);
    3203      cases ty' in Hind;
    3204      [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
    3205      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
    3206      normalize nodelta #Hind
    3207      try (@SimFail /2 by ex_intro/)
    3208      whd in match (exec_lvalue ????);
    3209      whd in match (exec_lvalue ????);     
    3210      cases Hind
    3211      [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3212      | 1,3: cases (exec_lvalue' ge en m e ?)
    3213          [ 2,4: #error #_ @SimFail /2 by ex_intro/
    3214          | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
    3215      ] ]
    3216 | 15: #ty #l #e #Hind
    3217      whd in match (exec_expr ge ???);
    3218      whd in match (exec_expr ge' ???);
    3219      cases Hind
    3220      [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
    3221      | 1: cases (exec_expr ge en m e)
    3222         [ 2: #error #_ @SimFail /2 by ex_intro/
    3223         | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
    3224      ] ]
     3194     #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty)
     3195     cases (exec_cast m1 v1 (typeof e) cast_ty)
     3196     [ 2: #error #_ normalize @I
     3197     | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????);
     3198          * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta
     3199          @conj // ]
     3200| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
     3201     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
     3202     lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1))
     3203     cases (exec_bool_of_val ? (typeof e1)) #b
     3204     [ 2: #_ normalize @I ]
     3205     #H lapply (H ? (refl ??)) #Hexec >Hexec normalize
     3206     cases b normalize nodelta
     3207     [ 1: (* true branch *)
     3208          cases (exec_expr ge en1 m1 e2) in Hsim2;
     3209          [ 2: #error normalize #_ @I
     3210          | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??))
     3211               * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize
     3212                    destruct @conj try // ]
     3213     | 2: (* false branch *)
     3214          cases (exec_expr ge en1 m1 e3) in Hsim3;
     3215          [ 2: #error normalize #_ @I
     3216          | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??))
     3217               * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize
     3218               destruct @conj // ] ]
     3219| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
     3220     @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq
     3221     lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1))     
     3222     cases (exec_bool_of_val v1 (typeof e1))
     3223     [ 2,4:  #error #_ normalize @I ]
     3224     #b cases b #H lapply (H ? (refl ??)) #Heq >Heq
     3225     whd in match (m_bind ?????);
     3226     whd in match (m_bind ?????);
     3227     [ 2,3: normalize @conj try @refl try @vint_eq ]
     3228     cases (exec_expr ge en1 m1 e2) in Hsim2;
     3229     [ 2,4: #error #_ normalize @I ]
     3230     * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??))
     3231     * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta
     3232     lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2))
     3233     cases (exec_bool_of_val v2 (typeof e2))
     3234     [ 2,4: #error #_ normalize @I ]
     3235     #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta
     3236     destruct @conj try @conj //
     3237     cases b2 whd in match (of_bool ?); @vint_eq
     3238| 13: #ty #ty' cases ty
     3239     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
     3240     | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     3241     whd in match (exec_expr ????); whd
     3242     * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉}
     3243     @conj try @refl @conj //
     3244| 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta
     3245    whd in match (exec_lvalue' ?????);
     3246    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
     3247    whd in match (typeof ?);
     3248    cases aggregty in Hsim;
     3249    [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
     3250    | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
     3251    normalize nodelta #Hsim
     3252    [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
     3253    whd in match (m_bind ?????);
     3254    whd in match (m_bind ?????);
     3255    whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
     3256    cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
     3257    [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
     3258    * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??))
     3259    * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq
     3260    whd in match (exec_lvalue ????); >Hexec normalize nodelta
     3261    [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj //
     3262         normalize @conj // ]
     3263    cases (field_offset i fl')
     3264    [ 2: #error normalize #Habsurd destruct (Habsurd) ]
     3265    #offset whd in match (m_bind ?????); #Heq destruct (Heq)
     3266    whd in match (m_bind ?????);
     3267    %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj
     3268    destruct // normalize nodelta @conj try @refl @vptr_eq
     3269    -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq
     3270    whd in match (pointer_translation ??);     
     3271    whd in match (pointer_translation ??);
     3272    cases (E b)
     3273    [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
     3274    * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq)
     3275    cut (offset_plus (mk_offset (offv o1+Z_of_signed_bitvector (bitsize_of_intsize I32) (repr I32 offset))) o'
     3276          = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset)))
     3277    [ normalize >associative_Zplus >(sym_Zplus ? (offv o')) in ⊢ (??%?); <associative_Zplus @refl ]
     3278    #Heq >Heq @refl
     3279| 15: #ty #l #e #Hsim
     3280     @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj //
    32253281| 16: *
    32263282  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    32273283  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
    32283284  #ty normalize in ⊢ (% → ?);
    3229   [ 1,2: #_ @SimOk #a normalize //
    3230   | 3,4,13: #H @(False_ind … H)
    3231   | *: #_ @SimFail /2 by ex_intro/
    3232   ]
    3233 ] qed. *)
     3285  [ 3,4,13: @False_ind
     3286  | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ]
     3287] qed.   
     3288
    32343289
    32353290(*
Note: See TracChangeset for help on using the changeset viewer.