Changeset 891 for src/Clight/CexecSound.ma
 Timestamp:
 Jun 7, 2011, 4:53:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r882 r891 3 3 (*include "Plogic/connectives.ma".*) 4 4 5 (* Is rather careful about using destruct because it currently uses excessive 6 normalization. *) 5 7 lemma exec_bool_of_val_sound: ∀v,ty,r. 6 8 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). 7 9 #v #ty #r 8 10 cases v; [  #i  #f  #r1  #r' #b #pc #of ] 9 cases ty; [ 2,11,20,29,38: #sz #sg  3,12,21,30,39: #sz  4,13,22,31,40: #r #ty  5,14,23,32,41: #r #ty #n  6,15,24,33,42: #args #rty  7,8,16,17,25,26,34,35,43,44: #id #fs  9,18,27,36,45: #r #id ] 10 #H whd in H:(??%?); destruct; 11 [ lapply (eq_spec i zero); elim (eq i zero); 12 [ #e >e @bool_of_val_false //; 13  #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/; 14 ] 15  elim (eq_dec f Fzero); 16 [ #e >e >(Feq_zero_true …) @bool_of_val_false //; 17  #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/; 18 ] 19  @bool_of_val_false // 20  (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H // 11 cases ty; [ 2,11,20,29,38: #sz #sg  3,12,21,30,39: #sz  4,13,22,31,40: #rg #ty  5,14,23,32,41: #r #ty #n  6,15,24,33,42: #args #rty  7,8,16,17,25,26,34,35,43,44: #id #fs  9,18,27,36,45: #r #id ] 12 #H whd in H:(??%?); 13 [ 2: lapply (eq_spec i zero) cases (eq i zero) in H ⊢ % 14 [ #E1 #E2 destruct @bool_of_val_false @is_false_int 15  #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E2  destruct @refl ] 16 ] 17  8: cases (eq_dec f Fzero) 18 [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float 19  #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne  destruct @refl ] 20 ] 21  14: >(?:r=false) [ @bool_of_val_false @is_false_pointer  destruct @refl ] 22  15: >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer  destruct @refl ] 23  *: destruct 21 24 ] qed. 22 25 … … 197 200 >Hv in He #He 198 201 @eval_Ederef [ 3: @He  *: skip ] 199  #ty #e'' #ty'' #He'' @bind2_OK #x cases x#loc #ofs #tr #H200 cases ty // * #pty202  #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H 203 cases ty // * #pty 201 204 cases loc in H ⊢ % * #loc' #H 202 205 whd try @I 203 @eval_Eaddrof >H in He'' #He'' @He''206 @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He'' 204 207  #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1 205 208 @opt_bind_OK #v #ev … … 221 224 @bind_OK #b 222 225 cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb 223 @bind2_OK #v #tr #Hv 226 @bind2_OK #v #tr #Hv whd in Hv:(??%?) 224 227 [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%; 225 228 @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb) … … 248 251  #ty #e' #ty' #i cases ty'; //; 249 252 [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H 250 @bind_OK #delta #Hdelta >H in He' #He'253 @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He' 251 254 @(eval_Efield_struct … He' (refl ??) Hdelta) 252  #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H 255  #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?) 253 256 >H in He' #He' 254 257 @(eval_Efield_union … He' (refl ??)) … … 300 303 cases (exec_lvalue ge en m e) in ⊢ (???% → %); 301 304 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H 302 @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ /2/]305 @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ] 303 306 lapply (addrof_exec_lvalue … H) #H' 304 307 lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
Note: See TracChangeset
for help on using the changeset viewer.