Changeset 833
 Timestamp:
 May 24, 2011, 11:19:53 PM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r832 r833 636 636 ]. 637 637 638 check lookup.639 640 638 definition assembly ≝ 641 639 λp. … … 653 651 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in 654 652 let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in 655 let to_flatten ≝ map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels x) instr_list in 656 (* 657 foldr ? ? (λx. λy. 653 let to_flatten ≝ 654 map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x)) instr_list 655 in 656 foldr ? ? (λx. λy. 658 657 match y with 659 658 [ None ⇒ None ? … … 663 662  Some x ⇒ Some ? (x @ lst) 664 663 ] 665 ]) (Some ? [ ]) to_flatten *) ? 666 ] 667 ]. 668 669 (* 670 if then (* 65536 *) 671 None ? 672 else 673 let flat_list ≝ flatten ? ( 674 map ? ? ( 675 assembly_1_pseudoinstruction ( 676 λx. lookup ? ? x labels (zero ?)) 677 (λx. lookup ? ? x datalabels (zero ?)) 678 (address_of labels)) instr_list) in 679 Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉 680 *) 681 682 (* 683 [2,3,4,5,6: 684 normalize; %; 685  whd in ⊢ (? (? ? ? %)); 686 cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16))) 687 # high 688 # low 689 whd in ⊢ (? (? ? ? %)) 690 cases (eq_bv 8 high (zero 8)) 691 [ normalize 692 % 693  elim not_implemented; 694 ] 695 ] 696 qed. *) 697 698 664 ]) (Some ? [ ]) to_flatten ]]. 699 665 700 666 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 
src/ASM/AssemblyProof.ma
r832 r833 79 79 (clock … ps)) ]. 80 80 81 (* RUSSEL **) 82 83 include "basics/jmeq.ma". 84 85 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. 86 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w]. 87 88 coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?. 89 coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. 90 91 (* END RUSSELL **) 92 93 definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus. 94 Σps':PseudoStatus.(code_memory … ps = code_memory … ps') 95 ≝ 96 λticks_of. 97 λs. 98 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 99 let ticks ≝ ticks_of (program_counter ? s) in 100 let s ≝ set_clock ? s (clock ? s + ticks) in 101 let s ≝ set_program_counter ? s pc in 102 let s ≝ 103 match instr with 104 [ Instruction instr ⇒ 105 Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s) 106  Comment cmt ⇒ Some PseudoStatus s 107  Cost cst ⇒ Some PseudoStatus s 108  Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp)) 109  Call call ⇒ 110 let a ≝ address_of_word_labels s call in 111 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 112 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 113 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 114 let s ≝ write_at_stack_pointer ? s pc_bl in 115 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 116 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 117 let s ≝ write_at_stack_pointer ? s pc_bu in 118 Some PseudoStatus (set_program_counter ? s a) 119  Mov dptr ident ⇒ 120 Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr) 121 ] 122 in 123 s. 124 [ 125 2,3,4: % 126  whd % 127 128 λticks_of. 129 λs. 130 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 131 let ticks ≝ ticks_of (program_counter ? s) in 132 let s ≝ set_clock ? s (clock ? s + ticks) in 133 let s ≝ set_program_counter ? s pc in 134 let s ≝ 135 match instr with 136 [ Instruction instr ⇒ 137 Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s) 138  Comment cmt ⇒ Some PseudoStatus s 139  Cost cst ⇒ Some PseudoStatus s 140  Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp)) 141  Call call ⇒ 142 let a ≝ address_of_word_labels s call in 143 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 144 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 145 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 146 let s ≝ write_at_stack_pointer ? s pc_bl in 147 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 148 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 149 let s ≝ write_at_stack_pointer ? s pc_bu in 150 Some PseudoStatus (set_program_counter ? s a) 151  Mov dptr ident ⇒ 152 Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr) 153 ] 154 in 155 s. 156 [2: % ] 157 normalize 158 @ I 159 qed. 160 161 162 163 definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus. 164 {{ ps':PseudoStatus  code_memory … ps = code_memory … ps' } 165 ≝ 166 λticks_of. 167 λs. 168 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 169 let ticks ≝ ticks_of (program_counter ? s) in 170 let s ≝ set_clock ? s (clock ? s + ticks) in 171 let s ≝ set_program_counter ? s pc in 172 let s ≝ 173 match instr with 174 [ Instruction instr ⇒ 175 Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s) 176  Comment cmt ⇒ Some PseudoStatus s 177  Cost cst ⇒ Some PseudoStatus s 178  Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp)) 179  Call call ⇒ 180 let a ≝ address_of_word_labels s call in 181 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 182 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 183 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 184 let s ≝ write_at_stack_pointer ? s pc_bl in 185 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 186 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 187 let s ≝ write_at_stack_pointer ? s pc_bu in 188 Some PseudoStatus (set_program_counter ? s a) 189  Mov dptr ident ⇒ 190 Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr) 191 ] 192 in 193 s. 194 [2: % ] 195 normalize 196 @ I 197 qed. 198 199 81 200 82 201 lemma execute_code_memory_unchanged: … … 94 213 cases (split ????) #z1 #z2 % 95 214  #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x 215 [ #x1 whd in ⊢ (??? (??%)) 96 216  *: cases not_implemented 97 217 ]
Note: See TracChangeset
for help on using the changeset viewer.