 Timestamp:
 Jul 5, 2011, 9:51:31 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1040 r1054 434 434  long_jump: jump_length. 435 435 436 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. 437 438 definition find_right_call: Word → Word → nat × (option jump_length) ≝ 436 definition find_right_call: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝ 439 437 (* medium call: 11 bits, only in "current segment" *) 440 438 (* can this be done more efficiently with bit vector arithmetic? *) 441 439 λpc.λaddress. 442 let 〈 p1, p2〉 ≝ split ? 5 11 address in443 let 〈 a1, a2〉 ≝ split ? 5 11 pc in444 if eq_bv ? p1 a1 then (* we're in the same segment *)445 〈 2, Some ? medium_jump〉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 〈3, 2, address, Some ? medium_jump〉 446 444 else 447 〈3, Some ? long_jump〉. 448 445 〈3, 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 449 466 definition distance ≝ 450 467 λx.λy.if gtb x y then x  y else y  x. 451 468 452 definition find_right_jump: Word → Word → nat × (option jump_length) ≝469 definition find_right_jump: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝ 453 470 (* short jump: 8 bits signed *) 454 471 (* medium jump: 11 bits, forward only *) … … 457 474 let pa ≝ nat_of_bitvector ? address in 458 475 if ltb (distance pn pa) 127 then 459 〈2, Some ? short_jump〉476 〈2, 3, address, Some ? short_jump〉 460 477 else 461 478 find_right_call pc address. 462 479 463 definition find_right_relative_jump: Word → (BitVectorTrie Word 16) → 464 Identifier → nat × (option jump_length) ≝ 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)) ≝ 465 508 λpc.λlabels.λjmp. 466 509 match lookup_opt ? ? jmp labels with 467 [ None ⇒ 〈 2, Some ? short_jump〉468  Some a ⇒find_right_jump pc a ].510 [ None ⇒ 〈3, 3, pc, Some ? long_jump〉 511  Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ]. 469 512 470 definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝ 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 → ? ≝ 471 541 λpc.λlabels.λi. 472 542 match i with … … 480 550  CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp 481 551  DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp 482  _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ]. 483 552  _ ⇒ let l ≝ length ? (assembly_preinstruction ? (λx.zero ?) i) in 553 〈l, l, pc, None …〉 ]. 554 555 definition jgeq_opt ≝ 556 λa:jump_length.λb:option (Word × jump_length). 557 match a with 558 [ short_jump ⇒ match b with 559 [ None ⇒ (* XXX *) False 560  Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump 561 ] 562  medium_jump ⇒ match b with 563 [ None ⇒ (* XXX *) False 564  Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump ∨ j = medium_jump ] 565  long_jump ⇒ True 566 ]. 567 568 definition is_long_jump ≝ 569 λj.match j with 570 [ long_jump ⇒ true 571  _ ⇒ false 572 ]. 573 574 definition policy_safe ≝ 575 λp:BitVectorTrie (Word × Word × jump_length) 16. 576 forall ? ? p (λ_.λx.let 〈pc,addr,j〉 ≝ x in 577 match j with 578 [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127 579  medium_jump ⇒ \fst (split ? 5 11 addr) = \fst (split ? 5 11 pc) 580  long_jump ⇒ True 581 ] 582 ). 583 584 definition jump_expansion_policy ≝ 585 Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.policy_safe policy. 586 587 definition inject_jump_expansion_policy: 588 ∀x:BitVectorTrie (Word × Word × jump_length) 16. 589 policy_safe x → jump_expansion_policy ≝ inject …. 590 591 coercion inject_jump_expansion_policy: 592 ∀x:BitVectorTrie (Word × Word × jump_length) 16. 593 policy_safe x → jump_expansion_policy ≝ inject_jump_expansion_policy 594 on x:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy. 595 484 596 definition jump_expansion_policy_internal: pseudo_assembly_program → 485 (BitVectorTrie Word 16) → jump_expansion_policy → 486 ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝ 487 λprogram.λlabels.λpolicy. 488 let 〈pc, new_labels, new_policy, changed〉 ≝ 489 foldl ? ? (λacc.λi:labelled_instruction. 490 let 〈label, instr〉 ≝ i in 491 let 〈pc,labels,policy,c0〉 ≝ acc in 492 let 〈c1,new_labels〉 ≝ match label with 493 [ None ⇒ 〈c0,labels〉 494  Some l ⇒ 495 match update ? ? pc l labels with 496 [ None ⇒ 〈c0,labels〉 497  Some x ⇒ 〈true, x〉 ] ] in 498 let 〈pc_delta, jmp_len〉 ≝ match instr with 499 [ Call c ⇒ 500 match lookup_opt ? ? c new_labels with 501 [ None ⇒ 〈2, Some ? medium_jump〉 502  Some c_addr ⇒ find_right_call pc c_addr ] 503  Jmp j ⇒ 504 match lookup_opt ? ? j new_labels with 505 [ None ⇒ 〈2, Some ? short_jump〉 506  Some j_addr ⇒ find_right_jump pc j_addr ] 507  Instruction i ⇒ jep_relative pc new_labels i 508  Mov _ _ ⇒ 〈3, None …〉 509  Cost _ ⇒ 〈0, None …〉 510  Comment _ ⇒ 〈0, None …〉 ] in 511 let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 512 match jmp_len with 513 [ None ⇒ 〈new_pc, new_labels, policy, c1〉 514  Some j ⇒ 515 match update ? ? pc j policy with 516 [ None ⇒ 〈new_pc, new_labels, policy, c1〉 517  Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ] 518 ) 〈zero ?, labels, policy, false〉 (\snd program) in 519 〈labels, policy, changed〉. 520 597 (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy → 598 Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16). 599 let 〈x,p〉 ≝ res in policy_safe p ≝ 600 λprogram.λold_labels.λold_policy. 601 let res ≝ 602 foldl_strong (option Identifier × pseudo_instruction) 603 (λprefix.Σresult:(Word × Word) × ((BitVectorTrie (Word × Identifier) 16) × 604 (BitVectorTrie (Word × Word × jump_length) 16)). 605 let 〈x,y,z,p〉 ≝ result in policy_safe p 606 ) 607 (\snd program) 608 (λprefix.λi.λtl.λprf.λacc. 609 let 〈label, instr〉 ≝ i in 610 let 〈pc,orig_pc,labels,policy〉 ≝ acc in 611 let new_labels ≝ match label return λ_.(BitVectorTrie (Word × Identifier) 16) with 612 [ None ⇒ labels 613  Some l ⇒ insert ? ? orig_pc 〈pc,l〉 labels 614 ] in 615 let add_instr ≝ match instr with 616 [ Call c ⇒ 617 match lookup_opt ? ? c new_labels with 618 [ None ⇒ 〈3, 3, pc, Some ? long_jump〉 619  Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ] 620  Jmp j ⇒ 621 match lookup_opt ? ? j new_labels with 622 [ None ⇒ 〈3, 3, pc, Some ? long_jump〉 623  Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ] 624  Instruction i ⇒ jep_relative pc new_labels i 625  Mov _ _ ⇒ 〈3, 3, pc, None …〉 626  Cost _ ⇒ 〈0, 0, pc, None …〉 627  Comment _ ⇒ 〈0, 0, pc, None …〉 ] in 628 let 〈pc_delta, orig_pc_delta, addr, jmp_len〉 ≝ add_instr in 629 let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 630 let 〈new_orig_pc,ignore〉 ≝ add_16_with_carry orig_pc (bitvector_of_nat ? orig_pc_delta) false in 631 match jmp_len with 632 [ None ⇒ 〈new_pc, orig_pc, new_labels, policy〉 633  Some j ⇒ 〈new_pc, new_orig_pc, new_labels, insert ? ? orig_pc 〈pc, addr, j〉 policy〉 634 ] 635 ) 〈zero ?, zero ?, old_labels, eject … old_policy〉 in 636 let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in 637 〈nlabels, npolicy〉. 638 [ cases res in p res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb; 639 >Hb in Ha; normalize nodelta #H @H 640  generalize in match (sig2 … acc) >p1 >p2 >p3 #H 641 @(forall_insert … H) normalize nodelta normalize nodelta in p4; cases instr in p4; >p5 >p6 normalize nodelta 642 [5: #str >p9 #Heq cases (lookup_opt ? ? str ?) in Heq; normalize nodelta 643 [ #Heq2 lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) 644 #Heq3 destruct (Heq3) // 645  #x cases x x #i0 #c_addr normalize nodelta lapply (frc_ok pc c_addr) 646 cases (find_right_call pc c_addr) #x #y cases x #i0 #i1 x; cases y #ad #jmp y; 647 normalize nodelta #Heq #Heq2 648 >(proj1 ? ? Heq) in Heq2; #Heq2 649 <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) 650 >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq; 651 cases j normalize nodelta #Heq [ @⊥ ] @(proj2 ? ? Heq) 652 ] 653 2,3,6: [3: #x] #z >p9 #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 654 #ctd destruct (ctd) 655 1,4: 656 #pi 657 [1: cases label normalize nodelta [ #Hjep  #id #Hjep ] whd in Hjep: (??%??); cases pi in Hjep; 658 2: cases (lookup_opt ? ? pi ?) normalize nodelta >p9 659 [ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 660 #ctd destruct (ctd) // 661  #x cases x x #i0 #j_addr normalize nodelta lapply (frj_ok pc j_addr) 662 cases (find_right_jump pc j_addr) #x #y cases x #i0 #i1 x; cases y #ad #jump y; 663 normalize nodelta #Heq #Heq2 664 >(proj1 ? ? Heq) in Heq2; #Heq2 665 <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) 666 >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq; 667 cases j normalize nodelta #Heq @(proj2 ? ? Heq) 668 ] 669 ] 670 [1,2,3,6,7,33,34,38,39,40,43,44,70,71: #acc #x normalize nodelta #Heq 671 <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9; 672 #ctd destruct (ctd) 673 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: 674 #acc normalize nodelta #Heq 675 <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9; 676 #ctd destruct (ctd) 677 35,36,37,72,73,74: normalize nodelta #Heq 678 <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9; 679 #ctd destruct (ctd) 680 9,10,14,15: #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id) 681 whd in match (find_right_relative_jump pc labels j_id) 682 normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta 683 [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 684 #Heq2 destruct (Heq2) // 685 2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 686 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 687 ] 688 46,47,51,52: #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id) 689 whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id) 690 normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta 691 [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 692 #Heq2 destruct (Heq2) // 693 2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 694 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 695 ] 696 11,12,13,16,17: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id) 697 whd in match (find_right_relative_jump pc labels j_id) 698 normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta 699 [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 700 #Heq2 destruct (Heq2) // 701 2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 702 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 703 ] 704 48,49,50,53,54: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id) 705 whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id) 706 normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta 707 [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) 708 #Heq2 destruct (Heq2) // 709 2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok; 710 normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok) 711 ] 712 ] 713 ] 714  generalize in match (sig2 … acc) >p1 >p2 >p3 #H 715 @H 716  generalize in match (sig2 … old_policy) #H @H 717 ] 718 qed. 719 521 720 definition expand_relative_jump_internal: 522 721 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) → … … 591 790 ]. 592 791 593 definition expand_pseudo_instruction _safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝792 definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝ 594 793 λlookup_labels. 595 794 λlookup_datalabels. … … 648 847 649 848 let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program) 650 (old_labels: BitVectorTrie Word 16) (old_policy: BitVectorTrie jump_length 16) 651 on n: jump_expansion_policy ≝ 849 (old_labels: BitVectorTrie (Word × Identifier) 16) 850 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.policy_safe bla) 851 on n: BitVectorTrie jump_length 16 ≝ 652 852 match n with 653 [ O ⇒ old_policy 853 [ O ⇒ fold … 854 (λ_.λx.λacc.let 〈pc,i2,jmp_len〉 ≝ x in insert … pc jmp_len acc) 855 old_policy (Stub ? ?) 654 856  S n' ⇒ 655 let 〈new_labels, new_policy, ch〉 ≝ 656 jump_expansion_policy_internal program old_labels old_policy in 657 jump_expansion_internal n' program new_labels new_policy ]. 658 857 (* let 〈x,y〉 ≝ jump_expansion_policy_internal program old_labels old_policy in *) 858 jump_expansion_internal n' program (* x y *) 859 (\fst (jump_expansion_policy_internal program old_labels old_policy)) 860 (\snd (jump_expansion_policy_internal program old_labels old_policy)) 861 ]. 862 generalize in match (sig2 … (jump_expansion_policy_internal program old_labels old_policy)) 863 cases (jump_expansion_policy_internal program old_labels old_policy) 864 #a cases a #xx #pp normalize nodelta 865 #H #H2 normalize nodelta @H2 866 qed. 867 659 868 (**************************************** START OF POLICY ABSTRACTION ********************) 660 869 … … 665 874 let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in 666 875 lookup ? ? pc policy long_jump. 667 876 normalize // 877 qed. 878 668 879 definition assembly_1_pseudoinstruction_safe ≝ 669 880 λprogram: pseudo_assembly_program. … … 675 886 λi. 676 887 let expansion ≝ jump_expansion ppc in 677 match expand_pseudo_instruction _safelookup_labels lookup_datalabels pc expansion i with888 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with 678 889 [ None ⇒ None ? 679 890  Some pseudos ⇒ … … 715 926 program counters. It is at the heart of the proof. *) 716 927 (*CSC: code taken from build_maps *) 717 definition sigma00: pseudo_assembly_program → policy_type → list ? → ? →option (nat × (nat × (BitVectorTrie Word 16))) ≝928 definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 718 929 λinstr_list. 719 930 λjump_expansion: policy_type. 720 931 λl:list labelled_instruction. 721 λacc.722 932 foldl ?? 723 933 (λt,i. … … 733 943 let 〈pc,ignore〉 ≝ pc_ignore in 734 944 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ] 735 ]) accl.945 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l. 736 946 737 947 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) 738 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).948 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog). 739 949 740 950 definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝ 741 951 λprogram,jump_expansion,instr_list. 742 match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *)with952 match sigma00 program jump_expansion instr_list with 743 953 [ None ⇒ None … 744 954  Some result ⇒ … … 800 1010 801 1011 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 802 definition assembly_1_pseudoinstruction ':1012 definition assembly_1_pseudoinstruction: 803 1013 ∀program:pseudo_assembly_program.∀pol: policy program. 804 1014 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. … … 807 1017 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 808 1018 Σres:(nat × (list Byte)). 809 Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧810 1019 let 〈len,code〉 ≝ res in 811 1020 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = … … 827 1036 (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *) 828 1037 cases daemon 829  % [ >p %] 830 cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 1038  cases res in p ⊢ %; res; #len #code #EQ normalize nodelta; 831 1039 (* THIS SHOULD BE TRUE INSTEAD *) 832 1040 cases daemon] 833 1041 qed. 834 1042 835 definition assembly_1_pseudoinstruction:836 ∀program:pseudo_assembly_program.∀pol: policy program.837 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.838 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →839 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →840 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →841 nat × (list Byte)842 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.843 assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1844 prf2 prf3.845 846 lemma assembly_1_pseudoinstruction_ok1:847 ∀program:pseudo_assembly_program.∀pol: policy program.848 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.849 ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).850 ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).851 ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.852 Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)853 = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.854 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3855 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))856 #H1 #_ @H1857 qed.858 859 1043 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *) 860 1044 definition construct_costs': 861 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.862 Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i1045 ∀program. policy program → nat → nat → ? → ? → 1046 Σres:(nat × (BitVectorTrie Word 16)). True 863 1047 ≝ 864 1048 λprogram.λpol: policy program.λppc,pc,costs,i. … … 867 1051  Some res ⇒ res ]. 868 1052 [ cases daemon 869  >p%]1053  %] 870 1054 qed. 871 1055 872 1056 definition construct_costs ≝ 873 1057 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i). 874 875 (*876 axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.877 axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.878 879 let rec foldl_strong_internal880 (A: Type[0]) (P: list A → Type[0]) (l: list A) (suffix2: list A)881 (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl @suffix2 → P prefix → P (prefix @ [hd]))882 (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:883 l = prefix @ suffix @ suffix2 → P(prefix @ suffix) ≝884 match suffix return λl'. l = prefix @ l' @ suffix2 → P (prefix @ l') with885 [ nil ⇒ λprf. ?886  cons hd tl ⇒ λprf. ?887 ].888 [ > (append_nil ?)889 @ acc890  applyS (foldl_strong_internal A P l suffix2 H (prefix @ [hd]) tl ? ?)891 [ @(H prefix hd tl prf acc)892  >prf /2/]]893 qed.894 895 definition foldl_strong ≝896 λA: Type[0].897 λP: list A → Type[0].898 λl: list A.899 λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).900 λacc: P [ ].901 foldl_strong_internal A P l [ ] ? [ ] l acc ?.902 [ #prefix #hd #tl >append_nil @H903  >append_nil % ]904 qed.905 906 axiom foldl_strong_step:907 ∀A:Type[0].908 ∀P: list A → Type[0].909 ∀l: list A.910 ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).911 ∀acc: P [ ].912 ∀Q: ∀prefix. P prefix → Prop.913 ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.914 ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).915 Q [ ] acc →916 Q l (foldl_strong A P l H acc).917 (*918 #A #P #l #H #acc #Q #HQ #Hacc normalize;919 generalize in match920 (foldl_strong ?921 (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))922 l ? Hacc)923 [3: >suffix_of_ok %  2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]924 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)925 #K926 927 generalize in match928 (foldl_strong ?929 (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))930 [2: @H931 *)932 933 axiom foldl_elim:934 ∀A:Type[0].935 ∀B: Type[0].936 ∀H: A → B → A.937 ∀acc: A.938 ∀l: list B.939 ∀Q: A → Prop.940 (∀acc:A.∀b:B. Q acc → Q (H acc b)) →941 Q acc →942 Q (foldl A B H acc l).943 *)944 945 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.946 #A #a #b #EQ destruct //947 qed.948 949 lemma sigma00_strict:950 ∀instr_list,jump_expansion,l,acc. acc = None ? →951 sigma00 instr_list jump_expansion l acc = None ….952 #instr_list #jump_expansion #l elim l953 [ #acc #H >H %954  #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]955 qed.956 957 lemma sigma00_append:958 ∀instr_list,jump_expansion,l1,l2,acc.959 sigma00 instr_list jump_expansion (l1@l2) acc =960 sigma00 instr_list jump_expansion961 l2 (sigma00 instr_list jump_expansion l1 acc).962 whd in match sigma00; normalize nodelta;963 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append964 qed.965 966 lemma policy_ok_prefix_ok:967 ∀program.∀pol:policy program.∀suffix,prefix.968 prefix@suffix = \snd program →969 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….970 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);971 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol972 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0973 normalize nodelta >sigma00_append974 cases (sigma00 ?? prefix ?)975 [2: #x #_ % #abs destruct(abs)976  * #abs @⊥ @abs >sigma00_strict % ]977 qed.978 979 lemma policy_ok_prefix_hd_ok:980 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.981 (prefix@[hd])@suffix = \snd program →982 Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →983 let 〈ppc,pc_map〉 ≝ ppc_pc_map in984 let 〈program_counter, sigma_map〉 ≝ pc_map in985 let 〈label, i〉 ≝ hd in986 construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….987 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2988 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix989 (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)990 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta991 @pair_elim' #pc #map #EQ4 normalize nodelta992 @pair_elim' #l' #i' #EQ5 normalize nodelta993 cases (construct_costs_safe ??????) normalize994 [* #abs @⊥ @abs %  #X #_ % #abs destruct(abs)]995 qed.996 997 (*998 lemma tech_pc_sigma00_append_Some:999 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.1000 tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →1001 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.1002 #program #pol #prefix #costs #label #i #ppc #pc #H1003 whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;1004 whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;1005 generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)1006 whd in match sigma0; normalize nodelta;1007 >foldl_step1008 change with (? → match match sigma00 program pol prefix with [None ⇒ ?  Some res ⇒ ?] with [ None ⇒ ?  Some res ⇒ ? ] = ?)1009 whd in match tech_pc_sigma00 in H; normalize nodelta in H;1010 cases (sigma00 program pol prefix) in H ⊢ %1011 [ whd in ⊢ (??%% → ?) #abs destruct(abs)1012  * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)1013 1014 normalize nodelta; H;1015 1016 1017 generalize in match H; H;1018 generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ?  _ ⇒ ?] with [_ ⇒ ?  _ ⇒ ?]?)1019 [2: whd in ⊢ (??%%)1020 XXX1021 *)1022 1058 1023 1059 axiom construct_costs_sigma:
Note: See TracChangeset
for help on using the changeset viewer.