Changeset 1309
 Timestamp:
 Oct 6, 2011, 6:09:18 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1103 r1309 408 408 qed. 409 409 410 definition is_relative_jump ≝411 λi: preinstruction Identifier.412 match i with413 [ JC _ ⇒ True414  JNC _ ⇒ True415  JB _ _ ⇒ True416  JNB _ _ ⇒ True417  JBC _ _ ⇒ True418  JZ _ ⇒ True419  JNZ _ ⇒ True420  CJNE _ _ ⇒ True421  DJNZ _ _ ⇒ True422  _ ⇒ False423 ].424 425 definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝426 λi.427 match i with428 [ Instruction j ⇒ is_relative_jump j429  _ ⇒ False ].430 431 410 inductive jump_length: Type[0] ≝ 432 411  short_jump: jump_length … … 434 413  long_jump: jump_length. 435 414 436 definition find_right_call: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝ 437 (* medium call: 11 bits, only in "current segment" *) 438 (* can this be done more efficiently with bit vector arithmetic? *) 439 λpc.λaddress. 440 let 〈a1, a2〉 ≝ split ? 5 11 address in 441 let 〈p1, p2〉 ≝ split ? 5 11 pc in 442 if eq_bv ? a1 p1 then (* we're in the same segment *) 443 〈2, 2, address, Some ? medium_jump〉 444 else 445 〈2, 3, address, Some ? long_jump〉. 446 447 (* lemma frc_ok: 448 ∀pc.∀j_addr. 449 let 〈i1,i2,addr,jl〉 ≝ find_right_call pc j_addr in 450 addr = j_addr ∧ 451 match jl with 452 [ None ⇒ False (* doesn't happen *) 453  Some j ⇒ match j with 454 [ short_jump ⇒ False (* doesn't happen either *) 455  medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc) 456  long_jump ⇒ True 457 ] 458 ]. 459 #pc #j_addr whd in match (find_right_call pc j_addr) cases (split ????) cases (split ????) 460 #p1 #p2 #a1 #a2 normalize nodelta 461 lapply (refl ? (eq_bv 5 a1 p1)) cases (eq_bv 5 a1 p1) in ⊢ (???% → %) #H normalize 462 [ %1 [ @refl  @(eq_bv_eq … H) ] 463  %1 [ @refl  // ] ] 464 qed. *) 465 466 definition distance ≝ 467 λx.λy.if gtb x y then x  y else y  x. 468 469 definition find_right_jump: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝ 470 (* short jump: 8 bits signed *) 471 (* medium jump: 11 bits, forward only *) 472 λpc.λaddress. 473 let pn ≝ nat_of_bitvector ? pc in 474 let pa ≝ nat_of_bitvector ? address in 475 if ltb (distance pn pa) 127 then 476 〈2, 2, address, Some ? short_jump〉 477 else 478 find_right_call pc address. 479 480 (* lemma frj_ok: 481 ∀pc.∀j_addr. 482 let 〈i1,i2,addr,jl〉 ≝ find_right_jump pc j_addr in 483 addr = j_addr ∧ 484 match jl with 485 [ None ⇒ False (* doesn't happen *) 486  Some j ⇒ match j with 487 [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? j_addr) < 127 488  medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc) 489  long_jump ⇒ True 490 ] 491 ]. 492 #pc #j_addr whd in match (find_right_jump pc j_addr) 493 lapply (refl ? (ltb (distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 j_addr)) 127)) 494 cases (ltb (distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 j_addr)) 127) in ⊢ (???% → %) #H 495 normalize nodelta 496 [ %1 [ @refl  whd @(leb_true_to_le … H) ] 497  lapply (frc_ok pc j_addr) cases (find_right_call ??) normalize nodelta #x #y cases x 498 #i1 #i2 cases y #addr #jl normalize nodelta cases jl normalize 499 [ // 500  #jl cases jl normalize 501 [1: #f @⊥ @(proj2 ? ? f) 2,3: // ] 502 ] 503 ] 504 qed. *) 505 506 definition find_right_relative_jump: Word → (BitVectorTrie (Word × Identifier) 16) → 507 Identifier → (nat × nat) × (Word × (option jump_length)) ≝ 508 λpc.λlabels.λjmp. 509 match lookup_opt ? ? jmp labels with 510 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉 511  Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ]. 512 513 (* lemma frrj_ok: 514 ∀pc.∀labels.∀j_id. 515 let 〈i1,i2,addr,jl〉 ≝ find_right_relative_jump pc labels j_id in 516 match lookup_opt ? ? j_id labels with 517 [ None ⇒ True (* long jump *) 518  Some x ⇒ let 〈ignore,j_addr〉 ≝ x in addr = j_addr ∧ match jl with 519 [ None ⇒ False (* doesn't happen *) 520  Some j ⇒ match j with 521 [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? j_addr) < 127 522  medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc) 523  long_jump ⇒ True 524 ] 525 ] 526 ]. 527 #pc #labels #j_id whd in match (find_right_relative_jump pc labels j_id) 528 cases (lookup_opt ? ? j_id labels) normalize nodelta 529 [ // 530  #x cases x #y #j_addr x; normalize nodelta lapply (frj_ok pc j_addr) 531 cases (find_right_jump ??) #x cases x #i1 #i2 x #x cases x #i3 #z x; cases z 532 normalize nodelta 533 [ // 534  #jl cases jl normalize nodelta 535 [1,3: // 2: #H @H ] 536 ] 537 ] 538 qed. *) 539 540 definition jep_relative: Word → (BitVectorTrie (Word × Identifier) 16) → preinstruction Identifier → ? ≝ 541 λpc.λlabels.λi. 542 match i with 543 [ JC jmp ⇒ find_right_relative_jump pc labels jmp 544  JNC jmp ⇒ find_right_relative_jump pc labels jmp 545  JB baddr jmp ⇒ find_right_relative_jump pc labels jmp 546  JZ jmp ⇒ find_right_relative_jump pc labels jmp 547  JNZ jmp ⇒ find_right_relative_jump pc labels jmp 548  JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp 549  JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp 550  CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp 551  DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp 552  _ ⇒ let l ≝ length ? (assembly_preinstruction ? (λx.zero ?) i) in 553 〈l, l, pc, None …〉 ]. 554 555 definition is_long_jump ≝ 556 λj.match j with 557 [ long_jump ⇒ true 558  _ ⇒ false 559 ]. 560 561 definition policy_safe ≝ 562 (λ_:Word.λx:Word×Word×jump_length.let 〈pc,addr,j〉 ≝ x in 563 match j with 564 [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127 565  medium_jump ⇒ \fst (split ? 5 11 addr) = \fst (split ? 5 11 pc) 566  long_jump ⇒ True 567 ] 568 ). 569 570 definition jump_expansion_policy ≝ 571 Σpolicy:BitVectorTrie (Word × Word × jump_length) 16. 572 forall ? ? policy policy_safe. 573 574 definition inject_jump_expansion_policy: 575 ∀p:BitVectorTrie (Word × Word × jump_length) 16. 576 forall ? ? p policy_safe → jump_expansion_policy ≝ inject …. 577 578 coercion inject_jump_expansion_policy: 579 ∀p:BitVectorTrie (Word × Word × jump_length) 16. 580 forall ? ? p policy_safe → jump_expansion_policy ≝ inject_jump_expansion_policy 581 on p:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy. 582 583 (* the jump length in a is greater than or equal to the jump length in b *) 584 definition jump_length_decrease ≝ 585 λa:jump_length.λb:jump_length. 586 match a with 587 [ short_jump ⇒ b = short_jump 588  medium_jump ⇒ b = short_jump ∨ b = medium_jump 589  long_jump ⇒ True 590 ]. 591 592 definition jump_expansion_policy_internal: pseudo_assembly_program → 593 (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy → 594 Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16). 595 let 〈x,p〉 ≝ res in 596 True ≝ 597 λprogram.λold_labels.λold_policy. 598 let res ≝ 599 foldl_strong (option Identifier × pseudo_instruction) 600 (λprefix.Σres.True) 601 (\snd program) 602 (λprefix.λi.λtl.λprf.λacc. 603 let 〈label, instr〉 ≝ i in 604 let 〈pc,orig_pc,labels,policy〉 ≝ acc in 605 let new_labels ≝ match label return λ_.(BitVectorTrie (Word × Identifier) 16) with 606 [ None ⇒ labels 607  Some l ⇒ insert ? ? orig_pc 〈pc,l〉 labels 608 ] in 609 let add_instr ≝ match instr with 610 [ Call c ⇒ 611 match lookup_opt ? ? c new_labels with 612 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉 613  Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ] 614  Jmp j ⇒ 615 match lookup_opt ? ? j new_labels with 616 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉 617  Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ] 618  Instruction i ⇒ jep_relative pc new_labels i 619  Mov _ _ ⇒ 〈3, 3, pc, None …〉 620  Cost _ ⇒ 〈0, 0, pc, None …〉 621  Comment _ ⇒ 〈0, 0, pc, None …〉 ] in 622 let 〈pc_delta, orig_pc_delta, addr, jmp_len〉 ≝ add_instr in 623 let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 624 let 〈new_orig_pc,ignore〉 ≝ add_16_with_carry orig_pc (bitvector_of_nat ? orig_pc_delta) false in 625 match jmp_len with 626 [ None ⇒ 〈new_pc, orig_pc, new_labels, policy〉 627  Some j ⇒ 〈new_pc, new_orig_pc, new_labels, insert ? ? orig_pc 〈pc, addr, j〉 policy〉 628 ] 629 ) 〈zero ?, zero ?, old_labels, eject … old_policy〉 in 630 let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in 631 〈nlabels, npolicy〉. 632 //. 633 (* [ cases res in p res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb; 634 >Hb in Ha; normalize nodelta #H @H 635  generalize in match (sig2 … acc) >p1 >p2 >p3 #H 636 @(forall_insert … H) normalize nodelta normalize nodelta in p4; cases instr in p4; >p5 >p6 normalize nodelta 637 [5: #str >p9 #Heq cases (lookup_opt ? ? str ?) in Heq; normalize nodelta 638 [ #Heq2 lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) 639 #Heq3 destruct (Heq3) // 640  #x cases x x #i0 #c_addr normalize nodelta lapply (frc_ok pc c_addr) 641 cases (find_right_call pc c_addr) #x #y cases x #i0 #i1 x; cases y #ad #jmp y; 642 normalize nodelta #Heq #Heq2 643 >(proj1 ? ? Heq) in Heq2; #Heq2 644 <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) 645 >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq; 646 cases j normalize nodelta #Heq [ @⊥ ] @(proj2 ? ? Heq) 647 ] 648 2,3,6: [3: #x] #z >p9 #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 649 #ctd destruct (ctd) 650 1,4: 651 #pi 652 [1: cases label normalize nodelta [ #Hjep  #id #Hjep ] whd in Hjep: (??%??); cases pi in Hjep; 653 2: cases (lookup_opt ? ? pi ?) normalize nodelta >p9 654 [ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 655 #ctd destruct (ctd) // 656  #x cases x x #i0 #j_addr normalize nodelta lapply (frj_ok pc j_addr) 657 cases (find_right_jump pc j_addr) #x #y cases x #i0 #i1 x; cases y #ad #jump y; 658 normalize nodelta #Heq #Heq2 659 >(proj1 ? ? Heq) in Heq2; #Heq2 660 <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) 661 >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq; 662 cases j normalize nodelta #Heq @(proj2 ? ? Heq) 663 ] 664 ] 665 [1,2,3,6,7,33,34,38,39,40,43,44,70,71: #acc #x normalize nodelta #Heq 666 <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9; 667 #ctd destruct (ctd) 668 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: 669 #acc normalize nodelta #Heq 670 <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9; 671 #ctd destruct (ctd) 672 35,36,37,72,73,74: normalize nodelta #Heq 673 <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9; 674 #ctd destruct (ctd) 675 9,10,14,15: #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id) 676 whd in match (find_right_relative_jump pc labels j_id) 677 normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta 678 [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 679 #Heq2 destruct (Heq2) // 680 2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 681 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 682 ] 683 46,47,51,52: #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id) 684 whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id) 685 normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta 686 [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 687 #Heq2 destruct (Heq2) // 688 2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 689 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 690 ] 691 11,12,13,16,17: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id) 692 whd in match (find_right_relative_jump pc labels j_id) 693 normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta 694 [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 695 #Heq2 destruct (Heq2) // 696 2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 697 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 698 ] 699 48,49,50,53,54: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id) 700 whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id) 701 normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta 702 [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 703 #Heq2 destruct (Heq2) // 704 2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 705 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 706 ] 707 ] 708 ] 709  generalize in match (sig2 … acc) >p1 >p2 >p3 #H 710 @H 711  generalize in match (sig2 … old_policy) #H @H 712 ] *) 713 qed. 714 715 (* lemma short_jumps_ok: 716 ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy. 717 forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p)) 718 (λk.λx.let 〈pc,addr,j〉 ≝ x in 719 j = short_jump → 720 distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127). 721 #program #l #p @lookup_forall 722 #x #b cases x x #x cases x #pc #addr #j #Hl normalize nodelta 723 cases j in Hl; #Hl #Hj 724 [2,3: destruct (Hj) 725 Hj; cases (jump_expansion_policy_internal program l p) in Hl; 726 #res cases res res #r #res normalize nodelta #Hf #Hl 727 normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl) 728 normalize #H @H 729 ] 730 qed. *) 731 732 (* lemma medium_jumps_ok: 733 ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy. 734 forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p)) 735 (λk.λx.let 〈pc,addr,j〉 ≝ x in 736 j = medium_jump → 737 distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127). 738 #program #l #p @lookup_forall 739 #x #b cases x x #x cases x #pc #addr #j #Hl normalize nodelta 740 cases j in Hl; #Hl #Hj 741 [2,3: destruct (Hj) 742 Hj; cases (jump_expansion_policy_internal program l p) in Hl; 743 #res cases res res #r #res normalize nodelta #Hf #Hl 744 normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl) 745 normalize #H @H 746 ] 747 qed. *) 748 415 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *) 416 definition jump_expansion_policy ≝ BitVectorTrie (Word × jump_length) 16. 417 749 418 definition expand_relative_jump_internal: 750 419 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) → … … 819 488 ]. 820 489 821 definition expand_pseudo_instruction : ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝490 definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝ 822 491 λlookup_labels. 823 492 λlookup_datalabels. … … 875 544 qed. 876 545 877 let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program) 878 (old_labels: BitVectorTrie (Word × Identifier) 16) 879 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16. 880 forall ? ? bla policy_safe) 881 on n: BitVectorTrie jump_length 16 ≝ 882 match n with 883 [ O ⇒ fold … 884 (λ_.λx.λacc.let 〈pc,i2,jmp_len〉 ≝ x in insert … pc jmp_len acc) 885 old_policy (Stub ? ?) 886  S n' ⇒ 887 jump_expansion_internal n' program 888 (\fst (jump_expansion_policy_internal program old_labels old_policy)) 889 (\snd (jump_expansion_policy_internal program old_labels old_policy)) 890 ]. 891 generalize in match (sig2 … (jump_expansion_policy_internal program old_labels old_policy)) 892 cases (jump_expansion_policy_internal program old_labels old_policy) 893 #a cases a #xx #pp normalize nodelta 894 #H #H2 normalize nodelta @H2 895 qed. 896 897 898 546 (* label_trie: identifier ↦ 〈instruction number, address〉 *) 547 definition label_trie ≝ BitVectorTrie (nat × Word) 16. 548 549 definition add_instruction_size: Word → jump_length → pseudo_instruction → Word ≝ 550 λpc.λjmp_len.λinstr. 551 let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in 552 let bv: list (BitVector 8) ≝ match ilist with 553 [ None ⇒ (* hmm, this shouldn't happen *) [ ] 554  Some l ⇒ flatten … (map … assembly1 l) 555 ] in 556 let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (bv)) false in 557 new_pc. 558 559 definition create_label_trie: list labelled_instruction → jump_expansion_policy → 560 label_trie ≝ 561 λprogram.λpolicy. 562 let 〈final_n, final_pc, final_labels〉 ≝ 563 foldl_strong (option Identifier × pseudo_instruction) 564 (λprefix.Σres.True) 565 program 566 (λprefix.λx.λtl.λprf.λacc. 567 let 〈n,pc,labels〉 ≝ acc in 568 let 〈label,instr〉 ≝ x in 569 let new_labels ≝ 570 match label with 571 [ None ⇒ labels 572  Some l ⇒ insert … l 〈n, pc〉 labels 573 ] in 574 let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, long_jump〉 in 575 let new_pc ≝ add_instruction_size pc jmp_len instr in 576 〈S n, new_pc, new_labels〉 577 ) 〈0, zero ?, Stub ? ?〉 in 578 final_labels. 579 @I 580 qed. 581 582 definition select_reljump_length: label_trie → Word → Identifier → jump_length ≝ 583 λlabels.λpc.λlbl. 584 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 585 if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *) 586 then short_jump 587 else long_jump. 588 589 definition select_call_length: label_trie → Word → Identifier → jump_length ≝ 590 λlabels.λpc.λlbl. 591 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 592 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 593 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 594 if eq_bv ? fst_5_addr fst_5_pc 595 then medium_jump 596 else long_jump. 597 598 definition select_jump_length: label_trie → Word → Identifier → jump_length ≝ 599 λlabels.λpc.λlbl. 600 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 601 if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *) 602 then short_jump 603 else 604 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 605 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 606 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 607 if eq_bv ? fst_5_addr fst_5_pc 608 then medium_jump 609 else long_jump. 899 610 611 definition jump_expansion_step_instruction: label_trie → Word → 612 preinstruction Identifier → option jump_length ≝ 613 λlabels.λpc.λi. 614 match i with 615 [ JC j ⇒ Some ? (select_reljump_length labels pc j) 616  JNC j ⇒ Some ? (select_reljump_length labels pc j) 617  JZ j ⇒ Some ? (select_reljump_length labels pc j) 618  JNZ j ⇒ Some ? (select_reljump_length labels pc j) 619  JB _ j ⇒ Some ? (select_reljump_length labels pc j) 620  JBC _ j ⇒ Some ? (select_reljump_length labels pc j) 621  JNB _ j ⇒ Some ? (select_reljump_length labels pc j) 622  CJNE _ j ⇒ Some ? (select_reljump_length labels pc j) 623  DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j) 624  _ ⇒ None ? 625 ]. 626 627 definition max_length: jump_length → jump_length → jump_length ≝ 628 λj1.λj2. 629 match j1 with 630 [ long_jump ⇒ long_jump 631  medium_jump ⇒ 632 match j2 with 633 [ long_jump ⇒ long_jump 634  _ ⇒ medium_jump 635 ] 636  short_jump ⇒ j2 637 ]. 638 639 definition jump_expansion_step: list labelled_instruction → 640 jump_expansion_policy → jump_expansion_policy ≝ 641 λprogram.λpolicy. 642 let labels ≝ create_label_trie program policy in 643 let 〈final_n, final_pc, final_policy〉 ≝ 644 foldl_strong (option Identifier × pseudo_instruction) 645 (λprefix.Σres.True) 646 program 647 (λprefix.λx.λtl.λprf.λacc. 648 let 〈n, pc, policy〉 ≝ acc in 649 let 〈label,instr〉 ≝ x in 650 let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in 651 let add_instr ≝ 652 match instr with 653 [ Instruction i ⇒ jump_expansion_step_instruction labels pc i 654  Call c ⇒ Some ? (select_call_length labels pc c) 655  Jmp j ⇒ Some ? (select_jump_length labels pc j) 656  _ ⇒ None ? 657 ] in 658 let 〈new_pc, new_policy〉 ≝ 659 let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in 660 match add_instr with 661 [ None ⇒ (* i.e. it's not a jump *) 662 〈add_instruction_size pc long_jump instr, policy〉 663  Some ai ⇒ 664 let new_length ≝ max_length old_length ai in 665 〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉 666 ] in 667 〈S n, new_pc, new_policy〉 668 ) 〈0, zero ?, Stub ? ?〉 in 669 final_policy. 670 @I 671 qed. 672 673 definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝ 674 λprogram. 675 Stub ? ?. 676 900 677 (**************************************** START OF POLICY ABSTRACTION ********************) 901 678 … … 904 681 definition jump_expansion': pseudo_assembly_program → policy_type ≝ 905 682 λprogram.λpc. 906 let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in 907 lookup ? ? pc policy long_jump. 908 normalize // 909 qed. 910 683 let policy ≝ jump_expansion_internal (\snd program) in 684 let 〈n,j〉 ≝ lookup ? ? pc policy 〈zero ?, long_jump〉 in 685 j. 686 911 687 definition assembly_1_pseudoinstruction_safe ≝ 912 688 λprogram: pseudo_assembly_program. … … 918 694 λi. 919 695 let expansion ≝ jump_expansion ppc in 920 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with696 match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with 921 697 [ None ⇒ None ? 922 698  Some pseudos ⇒ … … 958 734 program counters. It is at the heart of the proof. *) 959 735 (*CSC: code taken from build_maps *) 960 definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝736 definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 961 737 λinstr_list. 962 738 λjump_expansion: policy_type. 963 739 λl:list labelled_instruction. 740 λacc. 964 741 foldl ?? 965 742 (λt,i. … … 975 752 let 〈pc,ignore〉 ≝ pc_ignore in 976 753 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ] 977 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉)l.754 ]) acc l. 978 755 979 756 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) 980 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) .757 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉). 981 758 982 759 definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝ 983 760 λprogram,jump_expansion,instr_list. 984 match sigma00 program jump_expansion instr_list with761 match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with 985 762 [ None ⇒ None … 986 763  Some result ⇒ … … 1042 819 1043 820 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 1044 definition assembly_1_pseudoinstruction :821 definition assembly_1_pseudoinstruction': 1045 822 ∀program:pseudo_assembly_program.∀pol: policy program. 1046 823 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. … … 1049 826 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 1050 827 Σres:(nat × (list Byte)). 828 Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧ 1051 829 let 〈len,code〉 ≝ res in 1052 830 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = … … 1068 846 (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *) 1069 847 cases daemon 1070  cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 848  % [ >p %] 849 cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 1071 850 (* THIS SHOULD BE TRUE INSTEAD *) 1072 851 cases daemon] 1073 852 qed. 1074 853 854 definition assembly_1_pseudoinstruction: 855 ∀program:pseudo_assembly_program.∀pol: policy program. 856 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 857 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 858 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) → 859 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 860 nat × (list Byte) 861 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3. 862 assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 863 prf2 prf3. 864 865 lemma assembly_1_pseudoinstruction_ok1: 866 ∀program:pseudo_assembly_program.∀pol: policy program. 867 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 868 ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)). 869 ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)). 870 ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi. 871 Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3) 872 = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi. 873 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3 874 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)) 875 #H1 #_ @H1 876 qed. 877 1075 878 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 1076 879 definition construct_costs': 1077 ∀program. policy program → nat → nat → ? → ? →1078 Σres:(nat × (BitVectorTrie Word 16)). True880 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i. 881 Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i 1079 882 ≝ 1080 883 λprogram.λpol: policy program.λppc,pc,costs,i. … … 1083 886  Some res ⇒ res ]. 1084 887 [ cases daemon 1085  %]888  >p %] 1086 889 qed. 1087 890 1088 891 definition construct_costs ≝ 1089 892 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i). 893 894 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. 895 #A #a #b #EQ destruct // 896 qed. 897 898 lemma sigma00_strict: 899 ∀instr_list,jump_expansion,l,acc. acc = None ? → 900 sigma00 instr_list jump_expansion l acc = None …. 901 #instr_list #jump_expansion #l elim l 902 [ #acc #H >H % 903  #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ] 904 qed. 905 906 lemma sigma00_append: 907 ∀instr_list,jump_expansion,l1,l2,acc. 908 sigma00 instr_list jump_expansion (l1@l2) acc = 909 sigma00 instr_list jump_expansion 910 l2 (sigma00 instr_list jump_expansion l1 acc). 911 whd in match sigma00; normalize nodelta; 912 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append 913 qed. 914 915 lemma policy_ok_prefix_ok: 916 ∀program.∀pol:policy program.∀suffix,prefix. 917 prefix@suffix = \snd program → 918 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None …. 919 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%); 920 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol 921 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0 922 normalize nodelta >sigma00_append 923 cases (sigma00 ?? prefix ?) 924 [2: #x #_ % #abs destruct(abs) 925  * #abs @⊥ @abs >sigma00_strict % ] 926 qed. 927 928 lemma policy_ok_prefix_hd_ok: 929 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map. 930 (prefix@[hd])@suffix = \snd program → 931 Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) → 932 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 933 let 〈program_counter, sigma_map〉 ≝ pc_map in 934 let 〈label, i〉 ≝ hd in 935 construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None …. 936 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2 937 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix 938 (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?) 939 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta 940 @pair_elim' #pc #map #EQ4 normalize nodelta 941 @pair_elim' #l' #i' #EQ5 normalize nodelta 942 cases (construct_costs_safe ??????) normalize 943 [* #abs @⊥ @abs %  #X #_ % #abs destruct(abs)] 944 qed. 945 946 (* 947 lemma tech_pc_sigma00_append_Some: 948 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc. 949 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 → 950 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. 951 #program #pol #prefix #costs #label #i #ppc #pc #H 952 whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta; 953 whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %; 954 generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) 955 whd in match sigma0; normalize nodelta; 956 >foldl_step 957 change with (? → match match sigma00 program pol prefix with [None ⇒ ?  Some res ⇒ ?] with [ None ⇒ ?  Some res ⇒ ? ] = ?) 958 whd in match tech_pc_sigma00 in H; normalize nodelta in H; 959 cases (sigma00 program pol prefix) in H ⊢ % 960 [ whd in ⊢ (??%% → ?) #abs destruct(abs) 961  * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H) 962 963 normalize nodelta; H; 964 965 966 generalize in match H; H; 967 generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ?  _ ⇒ ?] with [_ ⇒ ?  _ ⇒ ?]?) 968 [2: whd in ⊢ (??%%) 969 XXX 970 *) 1090 971 1091 972 axiom construct_costs_sigma:
Note: See TracChangeset
for help on using the changeset viewer.