Changeset 466
 Timestamp:
 Jan 20, 2011, 6:46:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r465 r466 4 4 ndefinition sign_extension: Byte → Word ≝ 5 5 λc. 6 let b ≝ get_index_v ? eight c one? in6 let b ≝ get_index_v ? 8 c 1 ? in 7 7 [[ b; b; b; b; b; b; b; b ]] @@ c. 8 8 nnormalize; 9 nrepeat (napply (le ss_than_or_equal_monotone?));10 napply (le ss_than_or_equal_zero);9 nrepeat (napply (le_S_S ?)); 10 napply (le_O_n); 11 11 nqed. 12 12 13 13 nlemma inclusive_disjunction_true: 14 ∀b, c: Bool.15 inclusive_disjunction b c= true → b = true ∨ c = true.14 ∀b, c: bool. 15 (orb b c) = true → b = true ∨ c = true. 16 16 #b c; 17 17 nelim b … … 22 22 23 23 nlemma conjunction_true: 24 ∀b, c: Bool.25 conjunctionb c = true → b = true ∧ c = true.24 ∀b, c: bool. 25 andb b c = true → b = true ∧ c = true. 26 26 #b c; 27 27 nelim b; nnormalize … … 37 37 nqed. 38 38 39 nlemma inclusive_disjunction_b_true: ∀b. inclusive_disjunctionb true = true.39 nlemma inclusive_disjunction_b_true: ∀b. orb b true = true. 40 40 #b; ncases b; @. 41 41 nqed. … … 46 46 [ nnormalize; #_; #K; nassumption 47 47  #m' t q' II H1 H2; nnormalize; 48 nchange in H2:(??%?) with ( inclusive_disjunction??);48 nchange in H2:(??%?) with (orb ??); 49 49 ncases (inclusive_disjunction_true … H2) 50 50 [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @ 51  #K; nrewrite > II; ntry nassumption; //]51  #K; nrewrite > II; ntry nassumption; ncases (is_a t a); nnormalize; @ ] 52 52 nqed. 53 53 … … 70 70 ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %) 71 71 [ #K1; #_; 72 nchange in K1 with (( conjunction? (subvector_with …)) = true);72 nchange in K1 with ((andb ? (subvector_with …)) = true); 73 73 ncases (conjunction_true … K1); #K3; #K4; 74 74 ncases (inclusive_disjunction_true … K); #K2 … … 82 82 λs. 83 83 let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in 84 let 〈 instr, pc 〉 ≝ 〈 f irst … instr_pc, second … instr_pc 〉 in84 let 〈 instr, pc 〉 ≝ 〈 fst … instr_pc, snd … instr_pc 〉 in 85 85 let s ≝ set_clock s (clock s + ticks) in 86 86 let s ≝ set_program_counter s pc in … … 90 90 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 91 91 (get_arg_8 s false addr2) false in 92 let cy_flag ≝ get_index' ? Z? flags in93 let ac_flag ≝ get_index' ? one? flags in94 let ov_flag ≝ get_index' ? two? flags in92 let cy_flag ≝ get_index' ? O ? flags in 93 let ac_flag ≝ get_index' ? 1 ? flags in 94 let ov_flag ≝ get_index' ? 2 ? flags in 95 95 let s ≝ set_arg_8 s ACC_A result in 96 96 set_flags s cy_flag (Some Bit ac_flag) ov_flag … … 99 99 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 100 100 (get_arg_8 s false addr2) old_cy_flag in 101 let cy_flag ≝ get_index' ? Z? flags in102 let ac_flag ≝ get_index' ? one? flags in103 let ov_flag ≝ get_index' ? two? flags in101 let cy_flag ≝ get_index' ? O ? flags in 102 let ac_flag ≝ get_index' ? 1 ? flags in 103 let ov_flag ≝ get_index' ? 2 ? flags in 104 104 let s ≝ set_arg_8 s ACC_A result in 105 105 set_flags s cy_flag (Some Bit ac_flag) ov_flag … … 108 108 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1) 109 109 (get_arg_8 s false addr2) old_cy_flag in 110 let cy_flag ≝ get_index' ? Z? flags in111 let ac_flag ≝ get_index' ? one? flags in112 let ov_flag ≝ get_index' ? two? flags in110 let cy_flag ≝ get_index' ? O ? flags in 111 let ac_flag ≝ get_index' ? 1 ? flags in 112 let ov_flag ≝ get_index' ? 2 ? flags in 113 113 let s ≝ set_arg_8 s ACC_A result in 114 114 set_flags s cy_flag (Some Bit ac_flag) ov_flag … … 121 121 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 122 122 set_arg_8 s addr1 and_val 123  rightr ⇒123  inr r ⇒ 124 124 let 〈addr1, addr2〉 ≝ r in 125 125 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 126 126 set_arg_8 s addr1 and_val 127 127 ] 128  rightr ⇒128  inr r ⇒ 129 129 let 〈addr1, addr2〉 ≝ r in 130 let and_val ≝ conjunction (get_cy_flag s)(get_arg_1 s addr2 true) in130 let and_val ≝ (get_cy_flag s) ∧ (get_arg_1 s addr2 true) in 131 131 set_flags s and_val (None ?) (get_ov_flag s) 132 132 ] … … 139 139 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 140 140 set_arg_8 s addr1 or_val 141  rightr ⇒141  inr r ⇒ 142 142 let 〈addr1, addr2〉 ≝ r in 143 143 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 144 144 set_arg_8 s addr1 or_val 145 145 ] 146  rightr ⇒146  inr r ⇒ 147 147 let 〈addr1, addr2〉 ≝ r in 148 let or_val ≝ inclusive_disjunction (get_cy_flag s)(get_arg_1 s addr2 true) in148 let or_val ≝ (get_cy_flag s) ∨ (get_arg_1 s addr2 true) in 149 149 set_flags s or_val (None ?) (get_ov_flag s) 150 150 ] … … 155 155 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 156 156 set_arg_8 s addr1 xor_val 157  rightr ⇒157  inr r ⇒ 158 158 let 〈addr1, addr2〉 ≝ r in 159 159 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in … … 167 167 dptr ]] x) → ? with 168 168 [ ACC_A ⇒ λacc_a: True. 169 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in169 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in 170 170 set_arg_8 s ACC_A result 171 171  REGISTER r ⇒ λregister: True. 172 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in172 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in 173 173 set_arg_8 s (REGISTER r) result 174 174  DIRECT d ⇒ λdirect: True. 175 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in175 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in 176 176 set_arg_8 s (DIRECT d) result 177 177  INDIRECT i ⇒ λindirect: True. 178 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in178 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in 179 179 set_arg_8 s (INDIRECT i) result 180 180  DPTR ⇒ λdptr: True. 181 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in182 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in181 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in 182 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in 183 183 let s ≝ set_8051_sfr s SFR_DPL bl in 184 184 set_8051_sfr s SFR_DPH bu 185 185  _ ⇒ λother: False. ⊥ 186 186 ] (subaddressing_modein … addr) 187  DEC addr ⇒188 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in187  DEC addr ⇒ 188 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in 189 189 set_arg_8 s addr result 190 190  MUL addr1 addr2 ⇒ 191 let acc_a_nat ≝ nat_of_bitvector eight(get_8051_sfr s SFR_ACC_A) in192 let acc_b_nat ≝ nat_of_bitvector eight(get_8051_sfr s SFR_ACC_B) in191 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in 192 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in 193 193 let product ≝ acc_a_nat * acc_b_nat in 194 let ov_flag ≝ product ≥ two_hundred_and_fifty_sixin195 let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in196 let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in194 let ov_flag ≝ product ≥ 256 in 195 let low ≝ bitvector_of_nat 8 (product mod 256) in 196 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 197 197 let s ≝ set_8051_sfr s SFR_ACC_A low in 198 198 set_8051_sfr s SFR_ACC_B high 199 199  DIV addr1 addr2 ⇒ 200 let acc_a_nat ≝ nat_of_bitvector eight(get_8051_sfr s SFR_ACC_A) in201 let acc_b_nat ≝ nat_of_bitvector eight(get_8051_sfr s SFR_ACC_B) in200 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in 201 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in 202 202 match acc_b_nat with 203 [ Z⇒ set_flags s false (None Bit) true203 [ O ⇒ set_flags s false (None Bit) true 204 204  S o ⇒ 205 let q ≝ bitvector_of_nat eight(acc_a_nat ÷ (S o)) in206 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in205 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 206 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 207 207 let s ≝ set_8051_sfr s SFR_ACC_A q in 208 208 let s ≝ set_8051_sfr s SFR_ACC_B r in … … 210 210 ] 211 211  DA addr ⇒ 212 let 〈 acc_nu, acc_nl 〉 ≝ split ? four four(get_8051_sfr s SFR_ACC_A) in213 if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine)(get_ac_flag s) then214 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in215 let cy_flag ≝ get_index' ? Z? flags in216 let 〈acc_nu', acc_nl'〉 ≝ split ? four fourresult in217 if (g reater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then218 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in212 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in 213 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then 214 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in 215 let cy_flag ≝ get_index' ? O ? flags in 216 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in 217 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 218 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 219 219 let new_acc ≝ nu @@ acc_nl' in 220 220 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in … … 226 226  CLR addr ⇒ 227 227 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 228 [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)228 [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8) 229 229  CARRY ⇒ λcarry: True. set_arg_1 s CARRY false 230 230  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false … … 239 239  CARRY ⇒ λcarry: True. 240 240 let old_cy_flag ≝ get_arg_1 s CARRY true in 241 let new_cy_flag ≝ negationold_cy_flag in241 let new_cy_flag ≝ ¬old_cy_flag in 242 242 set_arg_1 s CARRY new_cy_flag 243 243  BIT_ADDR b ⇒ λbit_addr: True. 244 244 let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in 245 let new_bit ≝ negationold_bit in245 let new_bit ≝ ¬old_bit in 246 246 set_arg_1 s (BIT_ADDR b) new_bit 247 247  _ ⇒ λother: False. ? … … 250 250  RL _ ⇒ (* DPM: always ACC_A *) 251 251 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 252 let new_acc ≝ rotate_left … oneold_acc in252 let new_acc ≝ rotate_left … 1 old_acc in 253 253 set_8051_sfr s SFR_ACC_A new_acc 254 254  RR _ ⇒ (* DPM: always ACC_A *) 255 255 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 256 let new_acc ≝ rotate_right … oneold_acc in256 let new_acc ≝ rotate_right … 1 old_acc in 257 257 set_8051_sfr s SFR_ACC_A new_acc 258 258  RLC _ ⇒ (* DPM: always ACC_A *) 259 259 let old_cy_flag ≝ get_cy_flag s in 260 260 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 261 let new_cy_flag ≝ get_index' ? Z? old_acc in262 let new_acc ≝ shift_left … oneold_acc old_cy_flag in261 let new_cy_flag ≝ get_index' ? O ? old_acc in 262 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 263 263 let s ≝ set_arg_1 s CARRY new_cy_flag in 264 264 set_8051_sfr s SFR_ACC_A new_acc … … 266 266 let old_cy_flag ≝ get_cy_flag s in 267 267 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 268 let new_cy_flag ≝ get_index' ? seven? old_acc in269 let new_acc ≝ shift_right … oneold_acc old_cy_flag in268 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 269 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 270 270 let s ≝ set_arg_1 s CARRY new_cy_flag in 271 271 set_8051_sfr s SFR_ACC_A new_acc 272 272  SWAP _ ⇒ (* DPM: always ACC_A *) 273 273 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 274 let 〈nu,nl〉 ≝ split ? four fourold_acc in274 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 275 275 let new_acc ≝ nl @@ nu in 276 276 set_8051_sfr s SFR_ACC_A new_acc … … 278 278 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 279 279 [ DIRECT d ⇒ λdirect: True. 280 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in280 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 281 281 let s ≝ set_8051_sfr s SFR_SP new_sp in 282 282 write_at_stack_pointer s d … … 285 285  POP addr ⇒ 286 286 let contents ≝ read_at_stack_pointer s in 287 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in287 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in 288 288 let s ≝ set_8051_sfr s SFR_SP new_sp in 289 289 set_arg_8 s addr contents … … 294 294 set_arg_8 s addr2 old_acc 295 295  XCHD addr1 addr2 ⇒ 296 let 〈acc_nu, acc_nl〉 ≝ split … four four(get_8051_sfr s SFR_ACC_A) in297 let 〈arg_nu, arg_nl〉 ≝ split … four four(get_arg_8 s false addr2) in296 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in 297 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in 298 298 let new_acc ≝ acc_nu @@ arg_nl in 299 299 let new_arg ≝ arg_nu @@ acc_nl in … … 302 302  RET ⇒ 303 303 let high_bits ≝ read_at_stack_pointer s in 304 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in304 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in 305 305 let s ≝ set_8051_sfr s SFR_SP new_sp in 306 306 let low_bits ≝ read_at_stack_pointer s in 307 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in307 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in 308 308 let s ≝ set_8051_sfr s SFR_SP new_sp in 309 309 let new_pc ≝ high_bits @@ low_bits in … … 311 311  RETI ⇒ 312 312 let high_bits ≝ read_at_stack_pointer s in 313 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in313 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in 314 314 let s ≝ set_8051_sfr s SFR_SP new_sp in 315 315 let low_bits ≝ read_at_stack_pointer s in 316 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in316 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in 317 317 let s ≝ set_8051_sfr s SFR_SP new_sp in 318 318 let new_pc ≝ high_bits @@ low_bits in … … 374 374 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 375 375 [ RELATIVE r ⇒ λrel: True. 376 if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then376 if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then 377 377 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 378 378 set_program_counter s new_pc … … 384 384 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 385 385 [ RELATIVE r ⇒ λrel: True. 386 if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then386 if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then 387 387 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 388 388 set_program_counter s new_pc … … 405 405 else 406 406 (set_flags s new_cy (None ?) (get_ov_flag s)) 407  rightr' ⇒407  inr r' ⇒ 408 408 let 〈addr1, addr2〉 ≝ r' in 409 409 let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1)) … … 421 421 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 422 422 [ RELATIVE r ⇒ λrel: True. 423 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in423 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in 424 424 let s ≝ set_arg_8 s addr1 result in 425 if negation (eq_bv ? result (zero eight)) then425 if negation (eq_bv ? result (zero 8)) then 426 426 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 427 427 set_program_counter s new_pc … … 433 433  JMP _ ⇒ (* DPM: always indirect_dptr *) 434 434 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 435 let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in435 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 436 436 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 437 437 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in … … 453 453 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 454 454 [ ADDR11 a ⇒ λaddr11: True. 455 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight(program_counter s) in456 let 〈nu, nl〉 ≝ split ? four fourpc_bu in457 let bit ≝ get_index' ? Z? nl in458 let 〈relevant1, relevant2〉 ≝ split ? three eighta in455 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 456 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 457 let bit ≝ get_index' ? O ? nl in 458 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 459 459 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 460 460 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in … … 465 465 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 466 466 [ ACC_DPTR ⇒ λacc_dptr: True. 467 let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in467 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 468 468 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 469 469 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in … … 471 471 set_8051_sfr s SFR_ACC_A result 472 472  ACC_PC ⇒ λacc_pc: True. 473 let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in474 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in473 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 474 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in 475 475 (* DPM: Under specified: does the carry from PC incrementation affect the *) 476 476 (* addition of the PC with the DPTR? At the moment, no. *) … … 487 487 let 〈addr1, addr2〉 ≝ l in 488 488 set_arg_8 s addr1 (get_arg_8 s false addr2) 489  rightr ⇒489  inr r ⇒ 490 490 let 〈addr1, addr2〉 ≝ r in 491 491 set_arg_8 s addr1 (get_arg_8 s false addr2) … … 504 504 let 〈addr1, addr2〉 ≝ l'''' in 505 505 set_arg_8 s addr1 (get_arg_8 s false addr2) 506  rightr'''' ⇒506  inr r'''' ⇒ 507 507 let 〈addr1, addr2〉 ≝ r'''' in 508 508 set_arg_8 s addr1 (get_arg_8 s false addr2) 509 509 ] 510  rightr''' ⇒510  inr r''' ⇒ 511 511 let 〈addr1, addr2〉 ≝ r''' in 512 512 set_arg_8 s addr1 (get_arg_8 s false addr2) 513 513 ] 514  rightr'' ⇒514  inr r'' ⇒ 515 515 let 〈addr1, addr2〉 ≝ r'' in 516 516 set_arg_16 s (get_arg_16 s addr2) addr1 517 517 ] 518  rightr ⇒518  inr r ⇒ 519 519 let 〈addr1, addr2〉 ≝ r in 520 520 set_arg_1 s addr1 (get_arg_1 s addr2 false) 521 521 ] 522  rightr ⇒522  inr r ⇒ 523 523 let 〈addr1, addr2〉 ≝ r in 524 524 set_arg_1 s addr1 (get_arg_1 s addr2 false) … … 527 527 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 528 528 [ ADDR16 a ⇒ λaddr16: True. 529 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in529 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 530 530 let s ≝ set_8051_sfr s SFR_SP new_sp in 531 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight(program_counter s) in531 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 532 532 let s ≝ write_at_stack_pointer s pc_bl in 533 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in533 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 534 534 let s ≝ set_8051_sfr s SFR_SP new_sp in 535 535 let s ≝ write_at_stack_pointer s pc_bu in … … 540 540 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 541 541 [ ADDR11 a ⇒ λaddr11: True. 542 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in542 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 543 543 let s ≝ set_8051_sfr s SFR_SP new_sp in 544 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight(program_counter s) in544 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 545 545 let s ≝ write_at_stack_pointer s pc_bl in 546 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in546 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 547 547 let s ≝ set_8051_sfr s SFR_SP new_sp in 548 548 let s ≝ write_at_stack_pointer s pc_bu in 549 let 〈thr, eig〉 ≝ split ? three eighta in550 let 〈fiv, thr'〉 ≝ split ? five threepc_bu in549 let 〈thr, eig〉 ≝ split ? 3 8 a in 550 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 551 551 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 552 552 set_program_counter s new_addr … … 560 560 ntry ( 561 561 nnormalize 562 nrepeat (napply (le ss_than_or_equal_monotone))563 napply (le ss_than_or_equal_zero)562 nrepeat (napply (le_S_S)) 563 napply (le_O_n) 564 564 ); 565 565 ntry ( … … 575 575 nlet rec execute (n: nat) (s: Status) on n: Status ≝ 576 576 match n with 577 [ Z⇒ s577 [ O ⇒ s 578 578  S o ⇒ execute o (execute_1 s) 579 579 ].
Note: See TracChangeset
for help on using the changeset viewer.