Changeset 989 for src/ASM/Assembly.ma
 Timestamp:
 Jun 17, 2011, 10:28:19 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r987 r989 657 657 jump_expansion_internal n' program new_labels new_policy ]. 658 658 659 (**************************************** START OF POLICY ABSTRACTION ********************) 660 659 661 definition policy_type ≝ Word → jump_length. 660 662 … … 798 800 → False. 799 801 800 definition build_maps ≝ 802 definition build_maps: 803 ∀pseudo_program.∀pol:policy pseudo_program. 804 Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)). 805 let 〈labels,costs〉 ≝ res in 806 ∀id. occurs_exactly_once id (\snd pseudo_program) → 807 lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) 808 ≝ 801 809 λpseudo_program.λpol:policy pseudo_program. 802 810 let result ≝ … … 838 846 let 〈pc, costs〉 ≝ pc_costs in 839 847 〈labels, costs〉. 840 [ 3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //841  whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2848 [4: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ // 849 2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 842 850 cases construct in p4 #PC #CODE #JMEQ % [% [%]] 843 851 [ @(construct_costs_sigma … IHn1) [4: <JMEQ % *: skip] … … 852 860  #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: IHn1; /2/] 853 861 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 IHn1; //]]] 854  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 855 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ] 862 3: (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 863 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) 864  generalize in match (sig2 … result) >p normalize nodelta; >p1 normalize nodelta; 865 >p2; normalize nodelta; * #_; #H @H] 856 866 qed. 857 858 (*859 lemma build_maps_ok:860 ∀p:pseudo_assembly_program.861 let 〈labels,costs〉 ≝ build_maps' p in862 ∀pc.863 (nat_of_bitvector … pc) < length … (\snd p) →864 lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).865 #p cases p #preamble #instr_list866 elim instr_list867 [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]868  #hd #tl #IH869 whd in ⊢ (match % with [ _ ⇒ ?])870 ]871 qed.872 *)873 867 874 868 definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset
for help on using the changeset viewer.