Changeset 3457
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3449 r3457 1 include " Traces.ma".1 include "costs.ma". 2 2 include "basics/lists/list.ma". 3 3 include "../src/utilities/option.ma". … … 11 11 %{a} %{(refl …)} // 12 12 qed. 13 14 record monoid: Type[1] ≝15 { carrier :> Type[0]16 ; op: carrier → carrier → carrier17 ; e: carrier18 ; neutral: ∀x. op … x e = x19 ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)20 }.21 13 22 14 record assembler_params : Type[1] ≝ … … 345 337 qed. 346 338 339 definition asm_concrete_trans_sys ≝ 340 λp,p',prog.mk_concrete_transition_sys … 341 (asm_operational_semantics p p' prog) (m … p') (cost …). 342 347 343 definition emits_labels ≝ 348 344 λp.λinstr : AssemblerInstr p.match instr with … … 355 351 ]. 356 352 357 358 let rec block_cost (p : assembler_params) (p' : sem_params p) 359 (prog: AssemblerProgram p) (program_counter: ℕ) 353 definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝ 354 λp,p',prog,st.fetch … prog (pc … st). 355 356 definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m. 357 mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t 358 … (fetch_state p p' prog) instr_m. 359 360 361 let rec block_cost (p : assembler_params) 362 (prog: AssemblerProgram p) (abs_t : monoid) 363 (instr_m : AssemblerInstr p → abs_t) 364 (program_counter: ℕ) 360 365 (program_size: ℕ) 361 on program_size: option (m … p')≝366 on program_size: option abs_t ≝ 362 367 match program_size with 363 368 [ O ⇒ None ? 364 369  S program_size' ⇒ 365 370 if eqb program_counter (\snd prog) then 366 return e … (m … p')371 return e … abs_t 367 372 else 368 373 ! instr ← fetch … prog program_counter; 369 374 ! n ← (match emits_labels … instr with 370 [ Some f ⇒ block_cost … prog (f program_counter) program_size'375 [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size' 371 376  None ⇒ return e … 372 377 ]); 373 return (op … (m … p') (cost_of p p'instr) n)378 return (op … abs_t (instr_m … instr) n) 374 379 ]. 375 380 … … 405 410 ]. 406 411 407 definition static_analisys : ∀p : assembler_params.∀ p' : sem_params p.408 ∀mT : cost_map_T DEQCostLabel (m … p').AssemblerProgram p → option mT ≝409 λp, p',mT,prog.412 definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → 413 ∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝ 414 λp,abs_t,instr_m,mT,prog. 410 415 let 〈instrs,final〉 ≝ prog in 411 416 let prog_size ≝ S (instrs) in 412 m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost … progw prog_size;417 m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 413 418 return set_map … m z k) (labels_pc … instrs O) 414 419 (empty_map ?? mT). 415 420 416 421 (*falso: necessita di no_duplicates*) 417 axiom static_analisys_ok : ∀p, p',mT,prog,lbl,pc,map.418 static_analisys p p'mT prog = return map →422 axiom static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map. 423 static_analisys p abs_t instr_m mT prog = return map → 419 424 mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) → 420 get_map … map lbl = block_cost … prog pc (S ((\fst prog))).425 get_map … map lbl = block_cost … prog abs_t instr_m pc (S ((\fst prog))). 421 426 422 427 include "Simulation.ma". 423 428 424 record terminated_trace (S : abstract_status) (L_s1,R_s2) (trace: raw_trace S L_s1 R_s2) 425 : Prop ≝ 426 { R_label : option ActionLabel 427 ; R_post_state : option S 428 ; R_fin_ok : match R_label with 429 [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ? 430  Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧ 429 record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝ 430 { R_post_step : option (ActionLabel × S) 431 ; R_fin_ok : match R_post_step with 432 [ None ⇒ bool_to_Prop (as_final … R_s2) 433  Some x ⇒ let 〈l,R_post_state〉≝ x in 434 (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ 431 435 (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧ 432 ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'436 as_execute … l R_s2 R_post_state 433 437 ] 434 438 }. 435 439 436 lemma static_dynamic : ∀p,p',prog,k,mT,map. 437 static_analisys p p' mT prog = return map → 438 ∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. 439 pre_measurable_trace … t → terminated_trace … t → 440 block_cost … prog (pc … st1) (S ((\fst prog))) = return k → 441 op … (m … p') (cost … st1) 442 (foldr ?? (λlbl,k1.op … (opt_safe … (get_map … map lbl) ?) k1) 443 k (get_costlabels_of_trace … t)) = cost … st2. 444 [2: cases daemon] 445 #p #p' #prog #k #mT #map #EQmap #st1 #st2 #t elim t 446 [ #st #_ ** [#r_lab] normalize nodelta #opt_r_state 447 [ * whd in ⊢ (?% → ?); #final_st #_ whd in ⊢ (??%? → ?); >final_st 440 axiom vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → 441 eval_vmstate p p' prog st1 = return 〈l,st2〉. 442 443 coercion vm_step_to_eval. 444 445 definition big_op: ∀M: monoid. list M → M ≝ 446 λM. foldl … (op … M) (e … M). 447 448 lemma big_op_associative: 449 ∀M:monoid. ∀l1,l2. 450 big_op M (l1@l2) = op M (big_op … l1) (big_op … l2). 451 #M #l1 whd in match big_op; normalize nodelta 452 generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1 453 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c) 454 generalize in match c in ⊢ (??%? → ???%); lapply c c lapply(e M) 455 elim l2 normalize 456 [ #c #c1 #c2 #EQ @sym_eq // 457  #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [%  <is_associative % ] 458 ] 459  #x #xs #IH #c #l2 @IH 460 ] 461 qed. 462 463 lemma act_big_op : ∀M,B. ∀act : monoid_action M B. 464 ∀l1,l2,x. 465 act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x). 466 #M #B #act #l1 elim l1 467 [ #l2 #x >act_neutral // 468  #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2)); 469 >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl); 470 >big_op_associative >act_op in ⊢ (???%); % 471 ] 472 qed. 473 474 lemma static_dynamic : ∀p,p',prog. 475 ∀abs_t : abstract_transition_sys (m … p').∀instr_m. 476 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. 477 static_analisys p ? instr_m mT prog = return map1 → 478 ∀st1,st2 : vm_state p p'. 479 ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2. 480 ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. 481 ∀k. 482 pre_measurable_trace … t → 483 block_cost p prog … instr_m (pc … st1) (S ((\fst prog))) = return k → 484 ∀a1.rel_galois … good st1 a1 → 485 let stop_state ≝ match R_post_step … ter with [None ⇒ st2  Some x ⇒ \snd x ] in 486 ∀costs. 487 costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace … t) → 488 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)). 489 [2: @hide_prf cases daemon] 490 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t 491 lapply ter ter elim t 492 [ #st #ter inversion(R_post_step … ter) normalize nodelta [ * #lbl #st3 ] 493 #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta 494 [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st 448 495 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 449 >neutral % 450  ** #H1 #H2 * #post_st * #EQ destruct * #H3 #H4 whd in ⊢ (??%? → ?); 451 >H3 normalize nodelta #H cases(bind_inversion ????? H) H 452 #i * #EQi #H cases(bind_inversion ????? H) H #el 496 #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 497  ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta 498 #H cases(bind_inversion ????? H) H * 499 [ #seq * [#lbl1] 500  #newpc 501  #cond #newpc #ltrue #lfalse 502  #lin #io #lout 503  #f 504  505 ] 506 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; 507 normalize nodelta >EQfetch >m_return_bind normalize nodelta 508 cases(asm_is_io ??) normalize nodelta 509 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 510 2,4,8,9,12,14: #H cases(bind_inversion ????? H) H #x * #_ 511 [3: cases x normalize nodelta 512 6: #H cases(bind_inversion ????? H) H #y * #_ 513 ] 514 ] 515 whd in ⊢ (??%% → ?); #EQ destruct 516 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 517 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 518 #a1 #good_st_a1 whd in match (map ????); #costs #EQ >EQ >neutral_r 519 >act_neutral 520 @(instr_map_ok … good … EQfetch … good_st_a1) /2/ 521 ] 522  st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 523 #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); 524 whd #costs <map_append #EQ destruct >big_op_associative >act_op @IH 525 [ 526 inversion H in ⊢ ?; 527 [ #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 528  #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 529 #EQ1 #EQ2 #EQ3 #EQ4 destruct 530  #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 531 #EQ1 #EQ2 #EQ3 #EQ4 destruct 532  #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 533 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 534  #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 535 ] // 536  whd in H2 : (??%?); >H3 in H2; normalize nodelta #H 537 cases(bind_inversion ????? H) #i * #EQi whd in match (emits_labels ??); 538 539 inversion l [#fn #lbl  * [#lbl]  * [#lbl] ] #EQlbl normalize nodelta 540 inversion (R_post_step ???) [2,4,6,8,10,12,14,16: * #post_lbl #post_state] 541 #EQR_post_step normalize nodelta lapply (IH ter) IH 542 >EQR_post_step normalize nodelta #IH 543 whd in match (foldl ?????); 544 [ >act_op @IH 545 try (> act_op) 546 547 548 549 550 551 552 whd in ⊢ (??%% → ?); [ >H1 in ⊢ (% → ?);  >H1 in ⊢ (% → ?);  >H1 in ⊢ (% → ?);] 553 normalize nodelta lapply(vm_step_to_eval … H2) whd in match eval_vmstate; 554 normalize nodelta #H cases(bind_inversion ????? H) H * normalize nodelta 555 [1,7,13: #seq * [2,4,6: #lbl1] 556 2,8,14: #newpc 557 3,9,15: #cond #newpc #ltrue #lfalse 558 4,10,16: #lin #io #lout 559 5,11,17: #f 560 *: 561 ] * normalize nodelta #EQfetch 562 [13,14,15: whd in s1_noio : (?(??%?)); >EQfetch in s1_noio; 563 normalize nodelta cases(asm_is_io ???) normalize nodelta 564 [1,3,5: * #H @⊥ @H % ] #_ 565 *: cases(asm_is_io ???) normalize nodelta 566 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: 567 whd in ⊢ (??%% → ?); #EQ destruct] 568 [13 569 570 #i * #EQi #H cases(bind_inversion ????? H) H #el 453 571 inversion H4 454 572 [ #s1 #s2 #i1 * [ #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
Note: See TracChangeset
for help on using the changeset viewer.