Changeset 989
 Timestamp:
 Jun 17, 2011, 10:28:19 AM (9 years ago)
 Location:
 src/ASM
 Files:

 2 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)) ≝ 
src/ASM/AssemblyProof.ma
r988 r989 1670 1670 qed. 1671 1671 1672 axiom get_arg_8_set_low_internal_ram: 1673 ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z. 1674 1672 1675 lemma eq_rect_Type1_r: 1673 1676 ∀A: Type[1]. … … 1872 1875 #result #flags 1873 1876 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % *) 1874 5: (* Call *) #label #MAP1877 (* 5: (* Call *) #label #MAP 1875 1878 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP; 1876 1879 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta; … … 2060 2063  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2061 2064 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2062  (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta;2065 *)  (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta; 2063 2066 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1] 2064 2067 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2065 2068 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2066 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2069 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2067 2070 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2068 2071 >H2b >(eq_instruction_to_eq … H2a) … … 2070 2073 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; 2071 2074 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2 2072 normalize nodelta; #MAP; 2075 normalize nodelta; #MAP; (* 2073 2076 [1: change in ⊢ (? → %) with 2074 2077 ((let 〈result,flags〉 ≝ … … 2078 2081 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 2079 2082 false (DIRECT ARG2)) 2080 ? in ?) = ?) // 2081 [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2: 2082 [1,2:whd in MAP:(??(match % with [ _ ⇒ ?  _ ⇒ ?])?)] 2083 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2083 ? in ?) = ?) 2084 [2,3: %] 2085 change in ⊢ (???% → ?) with 2086 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?) 2087 >get_arg_8_set_clock *) 2088 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ? 2089 [2,4: #abs @⊥ normalize in abs; destruct (abs) 2090 *:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)] 2091 [ change in ⊢ (? → %) with 2092 ((let 〈result,flags〉 ≝ 2093 add_8_with_carry 2094 (get_arg_8 ? ps false ACC_A) 2095 (get_arg_8 ? 2096 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 2097 false (DIRECT ARG2)) 2098 ? in ?) = ?) 2099 >get_arg_8_set_low_internal_ram 2100 2101 cases (add_8_with_carry ???) 2102 2103 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2084 2104 #result #flags 2085 2105 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) %
Note: See TracChangeset
for help on using the changeset viewer.