 Timestamp:
 Dec 12, 2012, 2:43:03 PM (7 years ago)
 Location:
 src/joint
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2538 r2553 124 124 125 125 definition joint_classify_final : 126 ∀p : evaluation_params. joint_fin_step p → status_class ≝127 λp,st mt.126 ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝ 127 λp,st,stmt. 128 128 match stmt with 129 129 [ GOTO _ ⇒ cl_other 130 130  RETURN ⇒ cl_return 131  TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *) 131  TAILCALL _ f args ⇒ 132 match (! bl ← block_of_call … (ev_genv p) f st ; 133 fetch_function … (ev_genv p) bl) with 134 [ OK id_fn ⇒ 135 match \snd id_fn with 136 [ Internal _ ⇒ cl_tailcall 137  External _ ⇒ cl_return 138 ] 139  Error _ ⇒ cl_other 140 ] 132 141 ]. 133 142 134 143 definition joint_classify : 135 ∀p : evaluation_params.state_pc p → status_class ≝144 ∀p : evaluation_params.state_pc p → option status_class ≝ 136 145 λp,st. 137 match fetch_statement … (ev_genv p) (pc … st) with 138 [ OK i_f_s ⇒ 139 match \snd i_f_s with 140 [ sequential s _ ⇒ joint_classify_step p st s 141  final s ⇒ joint_classify_final p s 142  FCOND _ _ _ _ ⇒ cl_jump 143 ] 144  Error _ ⇒ cl_other 146 ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ; 147 match s with 148 [ sequential s _ ⇒ Some ? (joint_classify_step p st s) 149  final s ⇒ Some ? (joint_classify_final p st s) 150  FCOND _ _ _ _ ⇒ Some ? cl_jump 145 151 ]. 146 152 … … 179 185 180 186 lemma joint_classify_call : ∀p : evaluation_params.∀st. 181 joint_classify p st = cl_call →187 joint_classify p st = Some ? cl_call → 182 188 ∃i_f,f',args,dest,next,bl,i',fd'. 183 189 fetch_statement … (ev_genv p) (pc … st) = … … 187 193 #p #st 188 194 whd in match joint_classify; normalize nodelta 189 inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta190 [2: #e #_ #ABS destruct(ABS) ]195 inversion (fetch_statement … (ev_genv p) (pc … st)) 196 [2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] 191 197 * #i_f * [2,3: [ * [ #lbl   #fl #f #args ]  #fl #a #ltrue #lfalse ] #_ 192 normalize in ⊢ (%→?); #ABS destruct(ABS) ] 193 @cond_call_other 194 [ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS) 195 3: #s #no_call #nxt #_ whd in match joint_classify_step; 196 normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS) 197 ] 198 #f' #args #dest #nxt #fetch 198 >m_return_bind normalize nodelta 199 [3: whd in match joint_classify_final; normalize nodelta 200 generalize in ⊢ (??(?? (match % with [ _ ⇒ ?  _ ⇒ ?]))?→?); * [* #i' * #fd  #e ] 201 normalize nodelta ] 202 #ABS destruct(ABS) ] 203 @cond_call_other [ #a #lbl  #f' #args #dest  #s #s_no_call ] #nxt #fetch >m_return_bind 204 normalize nodelta 205 [ normalize in ⊢ (%→?); #ABS destruct(ABS) 206 3: whd in match joint_classify_step; 207 normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS) 208 ] 199 209 whd in match joint_classify_step; whd in match joint_classify_seq; 200 210 normalize nodelta … … 215 225 216 226 definition joint_after_ret : ∀p:evaluation_params. 217 (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝227 (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝ 218 228 λp,s1,s2. 219 229 match fetch_statement … (ev_genv p) (pc … s1) with … … 228 238 229 239 definition joint_call_ident : ∀p:evaluation_params. 230 (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝240 (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝ 231 241 (* this is a definition without a dummy ident : 232 242 λp,st. … … 283 293 ]. 284 294 295 definition joint_tailcall_ident : ∀p:evaluation_params. 296 (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝ 297 λp,st. 298 let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) 299 match fetch_statement … (ev_genv p) (pc … st) with 300 [ OK x ⇒ 301 match \snd x with 302 [ final s ⇒ 303 match s with 304 [ TAILCALL _ f' args ⇒ 305 match 306 (! bl ← block_of_call … (ev_genv p) f' st; 307 fetch_internal_function … (ev_genv p) bl) with 308 [ OK i_f ⇒ \fst i_f 309  _ ⇒ dummy 310 ] 311  _ ⇒ dummy 312 ] 313  _ ⇒ dummy 314 ] 315  _ ⇒ dummy 316 ]. 317 285 318 definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. 286 319 *#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim … … 342 375 (* as_after_return ≝ *) (joint_after_ret p) 343 376 (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) (exit p) s ≠ None ?) 344 (* as_call_ident ≝ *) (joint_call_ident p). 377 (* as_call_ident ≝ *) (joint_call_ident p) 378 (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 
src/joint/lineariseProof.ma
r2551 r2553 1024 1024 *) 1025 1025 1026 axiom symbol_for_block_transf : 1026 lemma symbol_for_block_match: 1027 ∀M:matching.∀initV,initW. 1028 (∀v,w. match_var_entry M v w → 1029 size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 1030 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 1031 ∀MATCH:match_program … M p p'. 1032 ∀b: block. 1033 symbol_for_block … (globalenv … initW p') b = 1034 symbol_for_block … (globalenv … initV p) b. 1035 * #A #B #V #W #match_fn #match_var #initV #initW #H 1036 #p #p' * #Mvars #Mfn #Mmain 1037 #b 1038 whd in match symbol_for_block; normalize nodelta 1039 whd in match globalenv in ⊢ (???%); normalize nodelta 1040 whd in match (globalenv_allocmem ????); 1041 change with (add_globals ?????) in match (foldl ?????); 1042 >(proj1 … (add_globals_match … initW … Mvars)) 1043 [ % *:] 1044 [ * #idr #v * #idr' #w #MVE % 1045 [ inversion MVE 1046 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % 1047  @(H … MVE) 1048 ] 1049  @(matching_fns_get_same_blocks … Mfn) 1050 #f #g @match_funct_entry_id 1051 ] 1052 qed. 1053 1054 lemma symbol_for_block_transf : 1027 1055 ∀A,B,V,init.∀prog_in : program A V. 1028 1056 ∀trans : ∀vars.A vars → B vars. 1029 1057 let prog_out ≝ transform_program … prog_in trans in 1030 ∀bl, i. 1031 symbol_for_block … (globalenv … init prog_in) bl = Some ? i → 1032 symbol_for_block … (globalenv … init prog_out) bl = Some ? i. 1058 ∀bl. 1059 symbol_for_block … (globalenv … init prog_out) bl = 1060 symbol_for_block … (globalenv … init prog_in) bl. 1061 #A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?)) 1062 #v0 #w0 * // 1063 qed. 1033 1064 1034 1065 lemma fetch_function_transf : … … 1047 1078 #H @('bind_inversion H) H #fd #eq_find_funct 1048 1079 whd in ⊢ (??%?→?); #EQ destruct(EQ) 1049 >(symbol_for_block_transf A B … eq_symbol_for_block)>m_return_bind1080 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind 1050 1081 >(find_funct_ptr_transf A B … eq_find_funct) % 1051 1082 qed. … … 1280 1311 normalize // 1281 1312 qed. 1282 check pc_of_label 1313 1283 1314 lemma fetch_statement_sigma_commute: 1284 1315 ∀p,p',graph_prog,pc,f,fn,stmt. … … 1288 1319 fetch_statement (make_sem_graph_params p p') … 1289 1320 (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → 1290 (*All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma1321 All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma 1291 1322 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl). 1292 1323 pc_of_label (make_sem_lin_params p p') … … … 1294 1325 (pc_block pc) 1295 1326 lbl = return sigma_pc … prf) 1296 (stmt_explicit_labels … stmt) ∧ *)1327 (stmt_explicit_labels … stmt) ∧ 1297 1328 match stmt with 1298 1329 [ sequential s nxt ⇒ … … 1351 1382 #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) 1352 1383 lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt) 1353 [@lin_pt_spec@(pi2 … (\fst (linearise_int_fun … fn)))] * #H1 (* #H2 % 1354 [ @In_All 1355 #lab #lab_in 1356 lapply (All_In ??? lab H1 ?) 1357 [ @Exists_append_r assumption ] 1358 inversion (sigma graph_fun lab) [#_ * #ABS @⊥ @ABS %] 1359 #lin_pt #EQsigma #_ 1360 % 1361 [ @hide_prf whd % 1362  whd in match sigma_pc; normalize nodelta 1363 @opt_safe_elim #pc_lin 1364 ] whd in match sigma_pc_opt; 1365 normalize nodelta >(eqZb_false … Hbl) >fetchfn normalize nodelta 1366 >m_return_bind >point_of_pc_of_point >EQsigma 1367 #EQ whd in EQ : (??%?); destruct(EQ) 1368 whd in match pc_of_label; normalize nodelta 1369 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1370 inversion (point_of_label ????) 1371 [2: #lin_pt' #EQ lapply (all_labels_in … EQ) >EQsigma 1372 #EQ' destruct % ] 1373 change with (If ? then with prf do ? else ? = ? → ?) 1374 @If_elim <(lin_code_has_label … (mk_lin_params p)) 1375 [ #_ whd in ⊢ (??%?→?); #EQ destruct ] 1376 #ABS cases (absurd ?? ABS) 1377 lapply (pi2 … (\fst (linearise_int_fun … graph_fun)) … ) 1378 [2: 1379 normalize nodelta 1380 1381 >m_return_bind whd in ⊢ (?(??%?)); 1382 % #ABS destruct(ABS) 1383 1384 >(eqZb_false … Hbl) normalize nodelta >fetchfn 1385 >m_return_bind >point_of_pc_of_point inversion(sigma graph_fun lab) in lab_spec; 1386 [ #_ * #ABS @⊥ @ABS %] #linear_pt #linear_pt_spec #_ >m_return_bind 1387 whd in match pc_of_label; normalize nodelta 1388 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1389 1390 ] lapply H2 *) 1391 cases (stmt) in H1; [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 1384 [@lin_pt_spec@(pi2 … (\fst (linearise_int_fun … fn)))] * #H1 #H2 % 1385 [ cases stmt in H2; 1386 [ * [#s#a#lbl]#nxt  #s  *] 1387 normalize nodelta 1388 [ * #stmt_at_EQ #_  ** #stmt_at_EQ #_  #stmt_at_EQ ] 1389 cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ) 1390 #H #_ 1391 [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn) 1392 3: cases H H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H 1393 ] 1394 ] 1395 cases (stmt) in H1 H2; [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 1392 1396 #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta 1393 1397 >pc_block_sigma_commute … … 1460 1464  >H3 >m_return_bind % 1461 1465 ] 1462 qed. 1466 qed. 1463 1467 1464 1468 … … 1468 1472 qed. 1469 1473 1474 lemma res_to_opt_preserve : ∀X,Y,P,F,m,n. 1475 res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n). 1476 #X #Y #P #F #m #n #H #x #EQ 1477 cases (H x ?) 1478 [ #prf #EQ' %{prf} >EQ' % 1479  cases m in EQ; normalize #x #EQ destruct % 1480 ] 1481 qed. 1482 1483 lemma sigma_pc_exit : 1484 ∀p,p',graph_prog,sigma,pc,prf. 1485 let exit ≝ mk_program_counter «mk_block Code (1), refl …» one in 1486 pc = exit → 1487 sigma_pc p p' graph_prog sigma pc prf = exit. 1488 #p #p' #graph_prog #sigma #pc #prf 1489 whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' 1490 #EQ1 #EQ2 destruct 1491 whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?); 1492 destruct % 1493 qed. 1494 1495 (* this should make things easier for ops using memory (where pc cant happen) *) 1496 definition bv_no_pc : beval → Prop ≝ 1497 λbv.match bv with [ BVpc _ _ ⇒ False  _ ⇒ True ]. 1498 1499 lemma bv_pc_other : 1500 ∀P : beval → Prop. 1501 (∀pc,p.P (BVpc pc p)) → 1502 (∀bv.bv_no_pc bv → P bv) → 1503 ∀bv.P bv. 1504 #P #H1 #H2 * /2/ qed. 1505 1506 lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf. 1507 bv_no_pc bv → 1508 sigma_beval p p' graph_prog sigma bv prf = bv. 1509 #p #p' #graph_prog #sigma * 1510 [ #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p ] 1511 #prf * whd in match sigma_beval; normalize nodelta 1512 @opt_safe_elim #bv' normalize #EQ destruct(EQ) % 1513 qed. 1514 1515 lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv. 1516 bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?. 1517 #p #p' #graph_prog #sigma * 1518 [ #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p ] * 1519 % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed. 1520 1521 lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by. 1522 * [ #a #b #c #p  #p  #p #pa  #p #pa ] #e #by 1523 whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. 1524 1525 lemma sigma_pc_no_exit : 1526 ∀p,p',graph_prog,sigma,pc,prf. 1527 let exit ≝ mk_program_counter «mk_block Code (1), refl …» one in 1528 pc ≠ exit → 1529 sigma_pc p p' graph_prog sigma pc prf ≠ exit. 1530 #p #p' #graph_prog #sigma #pc #prf 1531 @(eqZb_elim (block_id (pc_block pc)) (1)) 1532 [ #Hbl 1533 whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc' 1534 whd in match sigma_pc_opt; normalize nodelta 1535 >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ] 1536 #NEQ #_ inversion (sigma_pc ??????) 1537 ** #r #id #EQr #off #EQ 1538 lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ' 1539 % #ABS destruct(ABS) cases NEQ #H @H H 1540 cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') % 1541 qed. 1470 1542 1471 1543 definition linearise_status_rel: … … 1491 1563 >EQ2 1492 1564 whd in ⊢ (%→%); 1565 whd in match (exit ?); 1566 letin exit_pc ≝ (mk_program_counter «mk_block Code (1), refl …» one) 1493 1567 #H lapply (opt_to_opt_safe … H) 1494 1568 @opt_safe_elim H #res #_ whd in match is_final; normalize nodelta … … 1496 1570 #H @('bind_inversion H) H 1497 1571 ** #id #int_f #stmt 1498 #stmt_spec lapply(fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)1572 #stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec) 1499 1573 cases stmt in stmt_spec; stmt normalize nodelta 1500 [1,3: [ #a #b #_ #a #b #c #d #e] #_ # ABS whd in ABS : (???%); destruct(ABS)]1501 #fin_step cases(fin_step) fin_stepnormalize nodelta1502 [1,3: [#l #a #b #c] #_ #_ # ABS whd in ABS: (???%); destruct(ABS)]1503 #fetch_graph_spec # fetch_lin_spec1574 [1,3: [ #a #b #_ #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] 1575 * normalize nodelta 1576 [1,3: [#l #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)] 1577 #fetch_graph_spec #_ #fetch_lin_spec 1504 1578 #H >fetch_lin_spec >m_return_bind normalize nodelta 1505 @('bind_inversion H) H #state_pc #state_pc_spec 1506 elim(pop_frame_commute 1507 p p' graph_prog sigma gss ? id int_f ? (hide_prf … (proj2 … prf)) … state_pc_spec) 1508 #wf_state_pc normalize nodelta #sigma_state_pc_commute >sigma_state_pc_commute 1509 >m_return_bind @eq_program_counter_elim normalize nodelta 1510 [2: #_ #EQ whd in EQ : (???%); destruct(EQ)] #state_pc_spec #H 1511 @eq_program_counter_elim normalize nodelta 1512 [2: * #ABS @⊥ @ABS whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 1513 @opt_safe_elim #next_pc @eqZb_elim normalize nodelta >state_pc_spec 1514 [2: * #ABS1 @⊥ @ABS1 normalize %] #_ #EQ whd in EQ : (??%?); destruct(EQ) % 1515  #_ @('bind_inversion H) H #list_val #list_val_spec 1516 elim(read_result_commute p p' graph_prog sigma gss ? ? ? ? ? list_val_spec) 1517 [2: @hide_prf @(proj2 … prf)] #wf_lm #EQ >EQ EQ >m_return_bind 1518 whd in match Word_of_list_beval in ⊢ (% → ?); normalize nodelta 1519 #H @('bind_inversion H) H * #b1 #l1 #b1_l1_spec #H 1520 cases list_val in list_val_spec wf_lm b1_l1_spec; list_val normalize nodelta 1521 [ #_ #l #ABS whd in ABS : (???%); destruct(ABS)] 1522 #b2 #l2 #b2_l2_spec #wf_b2_l2 #H1 @('bind_inversion H1) H1 1523 #bt whd in match Byte_of_val; normalize nodelta 1524 cases (b2) in b2_l2_spec wf_b2_l2; b2 normalize nodelta 1525 [1,2,3,5,6,7: [#a #b #c  #p  #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (???%); destruct(ABS)] 1526 #by #by_l2_spec #wf_by_l2 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); 1527 destruct(EQ) @('bind_inversion H) H * #by1 #l3 1528 cases l1 in by_l2_spec wf_by_l2; l1 normalize nodelta [ #_ #a #ABS whd in ABS : (???%); destruct(ABS)] 1529 #val #l1 #b1_val_l1_spec #wf_b1_val_l1 #H @('bind_inversion H) H #by1 1530 cases val in b1_val_l1_spec wf_b1_val_l1; val 1531 [1,2,3,5,6,7: [#a #b #c  #p  #p #p'] #a #b [6: #_ #a] whd in match Byte_of_val; normalize nodelta 1532 #ABS whd in ABS : (???%); destruct(ABS)] 1533 #by2 #b1_by2_l1_spec #wf_b1_by2_l1 whd in match Byte_of_val; normalize nodelta 1534 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ) 1535 #H @('bind_inversion H) H * #by2 #l2 1536 cases(l3) in b1_by2_l1_spec wf_b1_by2_l1; l3 normalize nodelta 1537 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)] 1538 #val #l1 #b1_by1_val_l1_spec #wf_b1_by1_val_l1 #H @('bind_inversion H) H 1539 #by3 cases val in b1_by1_val_l1_spec wf_b1_by1_val_l1; val normalize nodelta 1540 [1,2,3,5,6,7: [#a #b #c  #p  #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (??%%); destruct(ABS)] 1541 #by3 #b1_by1_by3_l1_spec #wf_b1_by1_by3_l1 #EQ whd in EQ : (???%); destruct(EQ) 1542 #EQ whd in EQ : (???%); destruct(EQ) #H @('bind_inversion H) H * 1543 #by3 #l1 cases l2 in b1_by1_by3_l1_spec wf_b1_by1_by3_l1; l2 normalize nodelta 1544 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)] 1545 #val #l2 #_ #wf_b1_by1_by2_val #H @('bind_inversion H) H #by4 1546 cases val in wf_b1_by1_by2_val; val normalize nodelta 1547 [1,2,3,5,6,7: [ #a #b #c #p  #p #p'#p #pa] #a #ABS whd in ABS : (???%); destruct(ABS)] 1548 #by5 #wf_list #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ) cases l1 in wf_list; l1 normalize nodelta [2: #val #l #a #ABS whd in ABS : (???%); destruct(ABS)] 1549 #wf_list #EQ whd in EQ : (???%); destruct(EQ) 1550 @opt_safe_elim #l #H normalize in H; destruct(H) normalize % #ABS destruct(ABS) 1579 letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes)) 1580 letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes)) 1581 cut (preserving … res_preserve … 1582 (sigma_state … gss) 1583 (λl.λ_ : True.l) 1584 (λst. 1585 do st' ← pop_frame … graph_ge id int_f st; 1586 if eq_program_counter (pc … st') exit_pc then 1587 do vals ← read_result … graph_ge (joint_if_result … int_f) st ; 1588 Word_of_list_beval vals 1589 else 1590 Error ? [ ]) 1591 (λst. 1592 do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st; 1593 if eq_program_counter (pc … st') exit_pc then 1594 do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ; 1595 Word_of_list_beval vals 1596 else 1597 Error ? [ ])) 1598 [ #st #prf @mfr_bind [3: @pop_frame_commute *:] 1599 #st' #prf' @eq_program_counter_elim 1600 [ #EQ_pc >(sigma_pc_exit … EQ_pc) normalize nodelta 1601 @mfr_bind [3: @read_result_commute *:] 1602 #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv' 1603 @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … 1604 (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) 1605 [ 1606  * lbv lbv' #by1 #lbv #lbv_prf 1607 @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … 1608 (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) 1609 [ @opt_safe_elim #lbv' #EQ_lbv' 1610 * lbv #by2 #lbv #lbv_prf 1611 @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … 1612 (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) 1613 [ @opt_safe_elim #lbv' #EQ_lbv' 1614 * lbv #by3 #lbv #lbv_prf 1615 @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe … 1616 (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉)) 1617 [ @opt_safe_elim #lbv' #EQ_lbv' 1618 * lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ] 1619 #lbv_prf @mfr_return % 1620 ]]]] 1621 cases lbv in EQ_lbv'; 1622 try (#H @res_preserve_error) 1623 lbv #by1 #lbv #H @('bind_inversion H) H #by1' #EQby1' 1624 #H @('bind_inversion H) H #tl' #EQtl' 1625 whd in ⊢ (??%?→?); #EQ destruct(EQ) 1626 @(mfr_bind … (λby.λ_:True.by)) 1627 [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1'; 1628 whd in ⊢ (??%%→?); #EQ destruct(EQ) % 1629 *: #by1 * @mfr_return_eq 1630 change with (m_list_map ????? = ?) in EQtl'; 1631 [1,3,5,7: % 1632 *: @opt_safe_elim #lbv'' 1633 ] >EQtl' #EQ destruct % 1634 ] 1635  #_ @res_preserve_error 1636 ] 1637 ] 1638 #PRESERVE 1639 cases (PRESERVE … (proj2 … prf) … H) * 1640 #EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS) 1551 1641 qed. 1552 1642 … … 1565 1655 #EQ >EQ // 1566 1656 qed.*) 1567 1568 (* this should make things easier for ops using memory (where pc cant happen) *)1569 definition bv_no_pc : beval → Prop ≝1570 λbv.match bv with [ BVpc _ _ ⇒ False  _ ⇒ True ].1571 1572 lemma bv_pc_other :1573 ∀P : beval → Prop.1574 (∀pc,p.P (BVpc pc p)) →1575 (∀bv.bv_no_pc bv → P bv) →1576 ∀bv.P bv.1577 #P #H1 #H2 * /2/ qed.1578 1579 lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.1580 bv_no_pc bv →1581 sigma_beval p p' graph_prog sigma bv prf = bv.1582 #p #p' #graph_prog #sigma *1583 [ #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p ]1584 #prf * whd in match sigma_beval; normalize nodelta1585 @opt_safe_elim #bv' normalize #EQ destruct(EQ) %1586 qed.1587 1588 lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.1589 bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.1590 #p #p' #graph_prog #sigma *1591 [ #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p ] *1592 % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.1593 1657 1594 1658 lemma is_push_sigma_commute : … … 1624 1688 qed. 1625 1689 1626 lemma byte_of_val_inv : 1627 ∀e,bv,v.Byte_of_val e bv = return v → bv = BVByte v. 1628 #e * 1629 [ #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p ] #v 1630 whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. 1631 1632 lemma bit_of_val_inv : 1690 lemma Bit_of_val_inv : 1633 1691 ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v. 1634 1692 #e * … … 1654 1712 #v #EQ %{I} 1655 1713 >sigma_bv_no_pc try assumption 1656 >( byte_of_val_inv … EQ) %1714 >(Byte_of_val_inv … EQ) % 1657 1715 qed. 1658 1716 … … 1668 1726 [2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ] 1669 1727 #v #EQ %{I} >sigma_bv_no_pc try assumption 1670 >( byte_of_val_inv … EQ) %1728 >(Byte_of_val_inv … EQ) % 1671 1729 qed. 1672 1730 … … 1986 2044 qed. 1987 2045 1988 lemma eval_seq_no_call_no_goto :2046 lemma eval_seq_no_call_no_goto_ok : 1989 2047 ∀p,p',graph_prog. 1990 2048 let lin_prog ≝ linearise p graph_prog in … … 2019 2077 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 2020 2078 whd in match joint_classify_step; normalize nodelta 2021 @no_call_otherassumption2079 >no_call_other try % assumption 2022 2080  whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind 2023 2081 whd in match eval_statement_no_pc; normalize nodelta … … 2030 2088 qed. 2031 2089 2032 lemma eval_seq_no_call_goto :2090 lemma eval_seq_no_call_goto_ok : 2033 2091 ∀p,p',graph_prog. 2034 2092 let lin_prog ≝ linearise p graph_prog in … … 2046 2104 (succ_pc (make_sem_graph_params p p') … 2047 2105 (pc … st) nxt) in 2048 (? : Prop) →2106 ∀prf'. 2049 2107 fetch_statement (make_sem_lin_params p p') … 2050 2108 (globalenv_noinit … lin_prog) 2051 2109 (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = 2052 2110 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → 2111 pc_of_label (make_sem_lin_params p p') ? 2112 (globalenv_noinit ? (linearise p … graph_prog)) 2113 (pc_block (pc … st)) 2114 nxt = return sigma_pc p p' graph_prog sigma 2115 (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' → 2053 2116 ∃prf''. 2054 2117 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) … … 2057 2120 bool_to_Prop (taaf_non_empty … taf). 2058 2121 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call 2059 #prf #EQfetch' #EQeval #prf' #EQsucc_pc 2122 #prf #EQfetch' #EQeval #prf' #EQsucc_pc #EQ_pc_of_label 2060 2123 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)] 2061 2124 #prf'' #EQeval' 2062 2125 % [ @hide_prf % assumption ] 2063 %{(taaf_step … (taa_ base …) …)} [3: % ]2064 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta2126 %{(taaf_step … (taa_step … (taa_base …)) …)} [7: % ] 2127 [4: whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 2065 2128 whd in match joint_classify_step; normalize nodelta 2066 @no_call_other assumption 2067  whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind 2129 >no_call_other try % assumption 2130 3: whd whd in match eval_state; normalize nodelta >EQfetch' in ⊢ (??%?); 2131 >m_return_bind in ⊢ (??%?); 2068 2132 whd in match eval_statement_no_pc; normalize nodelta 2069 >EQeval' >m_return_bind2133 >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2070 2134 whd in match eval_statement_advance; normalize nodelta 2071 >no_call_advance [2: assumption ] 2072 whd in match (next ???); 2073 >EQsucc_pc % 2135 >no_call_advance in ⊢ (??%?); [2: assumption ] 2136 whd in match (next ???) in ⊢ (??%?); 2137 >EQsucc_pc in ⊢ (??%?); % 2138 1: whd whd in ⊢ (??%?); >EQsucc_pc % 2139 5: %* #H @H H whd in ⊢ (??%?); >EQsucc_pc % 2140 2: whd whd in match eval_state; normalize nodelta 2141 >EQsucc_pc >m_return_bind >m_return_bind whd in match eval_statement_advance; 2142 normalize nodelta whd in match goto; normalize nodelta 2143 whd in match (pc_block ?); >pc_block_sigma_commute 2144 >EQ_pc_of_label % 2145 *: 2074 2146 ] 2075 2147 qed. 2076 2148 2077 2078 2079 2080 [ assumption 2081  assu 2082 2149 lemma eval_call_ok : 2150 ∀p,p',graph_prog. 2151 let lin_prog ≝ linearise p graph_prog in 2152 ∀stack_sizes. 2153 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 2154 ∀st,st',f,fn,called,args,dest,nxt. 2155 ∀prf : well_formed_state_pc … gss st. 2083 2156 fetch_statement (make_sem_lin_params p p') … 2084 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 2085 return 〈f, \fst (linearise_int_fun … fn), 2086 sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ 2087 ∃prf'. 2088 let nxt_pc ≝ in 2089 let sigma_nxt ≝ in 2090 (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … 2091 (globalenv_noinit … lin_prog) nxt_pc = 2092 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) 2157 (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) = 2158 return 〈f, \fst (linearise_int_fun … fn), 2159 sequential … (CALL (mk_lin_params p) … called args dest ) it〉 → 2160 eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 2161 (CALL … called args dest) nxt st = return st' → 2162 (* let st_pc' ≝ mk_state_pc ? st' 2163 (succ_pc (make_sem_graph_params p p') … 2164 (pc … st) nxt) in 2165 ∀prf'. 2166 fetch_statement (make_sem_lin_params p p') … 2167 (globalenv_noinit … lin_prog) 2168 (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = 2169 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → 2170 pc_of_label (make_sem_lin_params p p') ? 2171 (globalenv_noinit ? (linearise p … graph_prog)) 2172 (pc_block (pc … st)) 2173 nxt = return sigma_pc p p' graph_prog sigma 2174 (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*) 2175 let st2_pre_call ≝ sigma_state_pc … gss st prf in 2176 ∃is_call, is_call'. 2177 ∃prf'. 2178 let st2_after_call ≝ sigma_state_pc … gss st' prf' in 2179 joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» = 2180 joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧ 2181 eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) 2182 st2_pre_call = return st2_after_call. 2183 cases daemon 2184 qed. 2185 2186 lemma eval_goto_ok : 2187 lemma eval_tailcall_ok : 2188 lemma eval_cond_cond_ok : 2189 lemma eval_cond_fcond_ok : 2190 lemma eval_return_ok : 2191 2093 2192 2094 2193 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.