Changeset 2146
 Timestamp:
 Jul 3, 2012, 3:09:50 AM (5 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2144 r2146 708 708 ∧ 709 709 (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨ 710 nat_of_bitvector … ppc= instr_list ∧ next_pc = zero …).710 S (nat_of_bitvector … ppc) = instr_list ∧ next_pc = zero …). 711 711 712 712 definition assembly: … … 720 720 let 〈assembled,costs〉 ≝ res in 721 721 assembled ≤ 2^16 ∧ 722 nat_of_bitvector … (sigma (bitvector_of_nat … (instr_list))) = assembled ∧ 722 (nat_of_bitvector … (sigma (bitvector_of_nat … (instr_list))) = assembled ∨ 723 sigma (bitvector_of_nat … (instr_list)) = zero … ∧ assembled = 2^16) ∧ 723 724 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 724 725 let datalabels ≝ construct_datalabels preamble in … … 733 734 nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j))) 734 735 assembled K 735 ≝ 736 ≝ ?. cases daemon(* 736 737 λp. 737 738 λsigma. … … 750 751 let 〈ppc,code〉 ≝ ppc_code in 751 752 ppc = bitvector_of_nat … (pre) ∧ 752 nat_of_bitvector … (sigma ppc) = code ∧ 753 (nat_of_bitvector … (sigma ppc) = code ∨ 754 sigma ppc = zero … ∧ code = 2^16) ∧ 753 755 ∀ppc'.∀ppc_ok'. 754 756 (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ pre = 2^16) → … … 847 849  >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse 848 850 [ //  <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]] 849 *) qed.851 *)*)qed. 850 852 851 853 definition assembly_unlabelled_program: 
src/ASM/AssemblyProof.ma
r2144 r2146 375 375 sigma_policy_specification program sigma policy → 376 376 ∀ppc1,ppc2. 377 nat_of_bitvector … ppc 1 < \snd program → nat_of_bitvector … ppc2 <\snd program →377 nat_of_bitvector … ppc2 ≤ \snd program → 378 378 nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 → 379 nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2). 379 (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨ 380 sigma ppc2 = zero … ∧ nat_of_bitvector … ppc2 = \snd program). 380 381 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2 381 #ppc 1_ok #ppc2_ok #LE382 #ppc2_ok #LE 382 383 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1) 383 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) 384 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) in ⊢ (?%(?%?)); 384 385 lapply (le_n … (nat_of_bitvector … ppc2)) 385 386 elim LE in ⊢ (?%? → %); 386 [ #_ % 387  #m #LE_ppc1_m #IH #BOUNDED @(transitive_le … (IH …)) IH 388 [@(transitive_le … BOUNDED) %2 %] 389 cut (m < \snd program) [ @(transitive_le … ppc2_ok) %2 /by/ ] #m_ok 390 cases (SIGMAOK2 (bitvector_of_nat … m) ?) 391 [2: >nat_of_bitvector_bitvector_of_nat_inverse /by/ 392 @(lt_to_le_to_lt … program_bounded) assumption ] 387 [ #_ % % 388  #m #LE_ppc1_m #IH #BOUNDED 389 cases (IH ?) 390 [3: @(transitive_le … BOUNDED) %2 % 391 2: * #_ #abs @⊥ <abs in ppc2_ok; #abs' 392 @(absurd ?? (not_le_Sn_n m)) 393 @(transitive_le … BOUNDED abs') ] 394 IH #IH 395 cut (m < \snd program) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1 396 cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2 397 cases (SIGMAOK2 (bitvector_of_nat … m) ?) SIGMAOK2 398 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ] 393 399 #_ * 394 [2: * #abs @⊥ @(absurd ?? (lt_to_not_eq … m_ok)) 395 >nat_of_bitvector_bitvector_of_nat_inverse in abs; [#H @H] 396 @(lt_to_le_to_lt … m_ok program_bounded) ] 397 #LT <add_bitvector_of_nat_Sm >add_commutative @(transitive_le … LT) %2 % 398 qed. 399 400 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *) 400 [ #LTsigma_m %1 @(transitive_le … IH) IH 401 <add_bitvector_of_nat_Sm >add_commutative 402 @(transitive_le … LTsigma_m) %2 % 403  * #EQ1 #EQ2 %2 % 404 [ <add_bitvector_of_nat_Sm >add_commutative assumption 405  <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption 406 ]]] 407 qed. 408 409 (*CSC: move elsewhere *) 410 axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n. 411 412 (* This is a non trivial consequence of fetch_assembly_pseudo + 413 load_code_memory_ok because the finite amount of memory. In 414 particular the case when the compiled program exhausts the 415 code memory is very tricky. *) 401 416 lemma assembly_ok: 402 417 ∀program. … … 457 472 [1: #j #H <load_code_memory_ok 458 473 [ @assembly_ok 459  cases (le_to_or_lt_eq … assembly_ok1) 460 [ #assembly_ok1' 474  cases assembly_ok3 assembly_ok3 475 [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ] 476 #EQlen_assembled' <EQlen_assembled' 477 cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok 478 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 479 whd in match instruction_size; normalize nodelta 480 >create_label_cost_refl 481 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 482 [>eq_assembly_1_pseudoinstruction 2: skip] #OK >OK <EQlen * 483 [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled'; 484 <add_bitvector_of_nat_Sm >add_commutative 485 >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 486 whd in ⊢ (??%? → ?); #EQlen_assembled' 487 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ] 488 cases (le_to_or_lt_eq … instr_list_ok) 489 [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero 490 whd in ⊢ (??%? → ?); #EQlen_assembled' 491 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ] 492 ] 493 #instr_list_ok' #NO_OVERFLOW 494 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))))) 495 [ @lt_to_lt_nat_of_bitvector_add 496 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 497 / by / 498  <EQlen cases daemon (*CSC: TRUE BECAUSE OF NO_OVERFLOW*) 499  assumption 500 ] 501  <EQlen <OK 502 cases (monotone_sigma ???? sigma_policy_witness 503 (add … ppc (bitvector_of_nat … 1)) 504 (bitvector_of_nat … (instr_list)) ??) try assumption 505 [ #H @H 506 3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse 507 try % assumption 508 4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption 509 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption 510 @(transitive_le … instr_list_ok') @le_S_S assumption 511  * #EQ1 @⊥ >EQ1 in EQlen_assembled'; 512 whd in ⊢ (??%? → ?); #EQlen_assembled' 513 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) 514 ] 515 ] 516 (* OLD CODE [ #assembly_ok1' 461 517 cut (nat_of_bitvector 16 (sigma ppc)+assembled≤assembled') 462 [ <assembly_ok3cases sigma_policy_witness #_ >EQprogram #sigma_ok518 [ cases sigma_policy_witness #_ >EQprogram #sigma_ok 463 519 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 464 #sigma_ok1 #sigma_ok2 465 cases daemon (*CSC: True, apply lemma above + monotonicity of sigma *) 520 whd in match instruction_size; normalize nodelta 521 >create_label_cost_refl 522 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 523 [>eq_assembly_1_pseudoinstruction 2: skip] #OK >OK <EQlen * 524 [ #JAP1 525 cut (nat_of_bitvector … (sigma ppc) + len < 2^16) 526 [cases daemon (*CSC: provable, needs lemma*)] #LT1 527 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len) 528 [2: @(le_to_lt_to_lt … LT1) / by / ] 529 cases assembly_ok3 530 [2: * #_ #abs @⊥ @(absurd … abs (lt_to_not_eq … assembly_ok1')) ] 531 #EQ_sigma_instr_list <EQ_sigma_instr_list 532 <nat_of_bitvector_add 533 [2: >nat_of_bitvector_bitvector_of_nat_inverse try assumption 534 @(transitive_le … LT1) @le_S_S / by / ] 535 <OK XXX 536 537 XXX cases daemon (*CSC: ???*) 538  assembly_ok3 #assembly_ok3 539 <assembly_ok3 540 (*CSC: we have to go by cases here!*) 541 <nat_of_bitvector_add 542 [2: cases daemon ] (*CSC: end of wrong part*) 543 544  545 ] 546 547 548 #JAP1 549 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len) 550 [2: cases daemon ] 551 cases assembly_ok3 552 [2: * #_ #EQ2 cases daemon (*CSC: ???*) 553  assembly_ok3 #assembly_ok3 554 <assembly_ok3 555 (*CSC: we have to go by cases here!*) 556 <nat_of_bitvector_add 557 [2: cases daemon ] (*CSC: end of wrong part*) 558 559 560 cases assembly_ok3 561 [2: * #_ #EQ2 cases daemon (*CSC: ???*) 562  assembly_ok3 #assembly_ok3 563 <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok 564 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 565 whd in match instruction_size; normalize nodelta 566 >create_label_cost_refl 567 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 568 [>eq_assembly_1_pseudoinstruction 2: skip] #OK #_ <EQlen 569 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len) 570 [2: cases daemon ] 571 <nat_of_bitvector_add 572 [2: cases daemon ] 573 <OK @(monotone_sigma2 … sigma_policy_witness) >EQprogram 574 cases daemon (*CSC: ???*) 575 ] 466 576  #LE2 467 577 cut (assembled < 2^16) … … 481 591 ] 482 592  #assembly_ok1' >assembly_ok1' / by / 483 ] 484 ] 593 ]*) 485 594 2: 486 595 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len … … 795 904 *) 796 905 797 (* DEAD CODE?798 lemma status_of_pseudo_status_failure_depends_only_on_code_memory:799 ∀M:internal_pseudo_address_map.800 ∀ps,ps': PseudoStatus.801 ∀pol.802 ∀prf:code_memory … ps = code_memory … ps'.803 let pol' ≝ ? in804 match status_of_pseudo_status M ps pol with805 [ None ⇒ status_of_pseudo_status M ps' pol' = None …806  Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w807 ].808 [2: <prf @pol]809 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ])810 generalize in match (refl … (assembly (code_memory … ps) pol))811 cases (assembly ??) in ⊢ (???% → %)812 [ #K whd whd in ⊢ (??%?) <H >K %813  #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]814 qed.815 *)816 817 906 (* XXX: check values returned for conditional jumps below! *) 818 907 definition ticks_of0:
Note: See TracChangeset
for help on using the changeset viewer.