source: Deliverables/D4.1/Matita/Interpret.ma @ 370

Last change on this file since 370 was 370, checked in by mulligan, 9 years ago

Most of critical lemma done. Hole remaining that I can't coax matita into solving.

File size: 28.7 KB
Line 
1include "Status.ma".
2include "Fetch.ma".
3
4ndefinition sign_extension: Byte → Word ≝
5  λb.
6    zero eight @@ b.
7   
8nlemma inclusive_disjunction_true:
9  ∀b, c: Bool.
10    ((inclusive_disjunction b c) = true) → ((b = true) ∨ (c = true)).
11  #b c;
12  nelim b
13    [ nnormalize; #H; napply or_introl; @;
14  ##| nnormalize; /2/;
15  ##]
16nqed.
17
18nlemma execute_1_technical:
19  ∀n,m: Nat.
20  ∀v: Vector addressing_mode_tag (S n).
21  ∀q: Vector addressing_mode_tag (S m).
22  ∀a: addressing_mode.
23    bool_to_Prop (is_in ? v a) →
24    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
25    bool_to_Prop (is_in ? q a).
26 #n m v q a; nelim v
27  [ nnormalize; #K; ncases K
28  | #n' he tl II;
29    nwhd in ⊢ (% → ? → ?);
30    nlapply (refl … (is_in … (he:::tl) a));
31    ncases (is_in … (he:::tl) a) in ⊢ (???% → %)
32     [ #K; #_; nnormalize in K; nwhd in ⊢ (% → ?);
33       nlapply (refl … (subvector_with … eq_a (he:::tl) q));
34       ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
35       [ #K1; #_;
36        nchange in K1 with ((conjunction ? (subvector_with …)) = true);
37        nlapply (inclusive_disjunction_true (is_a he a) (is_in n' tl a));
38        #K2;
39        nlapply (K2 K);
40        #K3;
41     ##| #K1 K2; nnormalize in K2; ncases K2 ]
42   ##| #K1 K2; nnormalize in K2; ncases K2 ]
43
44
45nlet rec execute_1_technical
46 (m: Nat)
47 (a: addressing_mode)
48 (q: Vector addressing_mode_tag (S m))
49 (n: Nat)
50 (v: Vector addressing_mode_tag (S n))
51 on v : bool_to_Prop (is_in ? v a) →
52        bool_to_Prop (subvector_with ? ? ? eq_a v q) →
53        bool_to_Prop (is_in ? q a) ≝
54 match v with
55  [ Empty ⇒ ?
56  | Cons o he tl ⇒ ?
57  ].
58##[ @ | ndestruct |
59    nlapply (S_inj … H); #H2;
60    nrewrite > H2 in H1; #K2;
61 
62 
63  #n; nelim n
64   [ #m v; ninversion v [ #K; ncases (?: False);
65 
66 
67  nelim v
68   [ nnormalize;
69     #H1 H2;
70     ncases (is_in m q a);
71     nnormalize
72      [ @ | //;
73  //.
74
75  #N H V IH H1 H2.
76  nnormalize.
77  ncases (is_in m q a).
78  nnormalize.
79  napply I.
80  nnormalize.
81  //.
82nqed.
83
84nlemma execute_1_technical:
85  ∀n,m: Nat.
86  ∀v: Vector addressing_mode_tag (S n).
87  ∀q: Vector addressing_mode_tag (S m).
88  ∀a: addressing_mode.
89    bool_to_Prop (is_in ? v a) →
90    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
91    bool_to_Prop (is_in ? q a).
92  #n; nelim n
93   [ #m v; ninversion v [ #K; ncases (?: False);
94 
95 
96  nelim v
97   [ nnormalize;
98     #H1 H2;
99     ncases (is_in m q a);
100     nnormalize
101      [ @ | //;
102  //.
103
104  #N H V IH H1 H2.
105  nnormalize.
106  ncases (is_in m q a).
107  nnormalize.
108  napply I.
109  nnormalize.
110  //.
111nqed.
112   
113ndefinition execute_1: Status → Status ≝
114  λs.
115    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
116    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
117    let s ≝ set_clock s (clock s + ticks) in
118    let s ≝ set_program_counter s pc in
119    let s ≝
120      match instr with
121        [ ADD addr1 addr2 ⇒
122            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
123                                                   (get_arg_8 s false addr2) false in
124            let cy_flag ≝ get_index' ? Z  ? flags in
125            let ac_flag ≝ get_index' ? one ? flags in
126            let ov_flag ≝ get_index' ? two ? flags in
127            let s ≝ set_arg_8 s ACC_A result in
128              set_flags s cy_flag (Just Bit ac_flag) ov_flag
129        | ADDC addr1 addr2 ⇒
130            let old_cy_flag ≝ get_cy_flag s in
131            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
132                                                   (get_arg_8 s false addr2) old_cy_flag in
133            let cy_flag ≝ get_index' ? Z ? flags in
134            let ac_flag ≝ get_index' ? one ? flags in
135            let ov_flag ≝ get_index' ? two ? flags in
136            let s ≝ set_arg_8 s ACC_A result in
137              set_flags s cy_flag (Just Bit ac_flag) ov_flag
138        | SUBB addr1 addr2 ⇒
139            let old_cy_flag ≝ get_cy_flag s in
140            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
141                                                   (get_arg_8 s false addr2) old_cy_flag in
142            let cy_flag ≝ get_index' ? Z ? flags in
143            let ac_flag ≝ get_index' ? one ? flags in
144            let ov_flag ≝ get_index' ? two ? flags in
145            let s ≝ set_arg_8 s ACC_A result in
146              set_flags s cy_flag (Just Bit ac_flag) ov_flag
147        | ANL addr ⇒
148          match addr with
149            [ Left l ⇒
150              match l with
151                [ Left l' ⇒
152                  let 〈addr1, addr2〉 ≝ l' in
153                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
154                    set_arg_8 s addr1 and_val
155                | Right r ⇒
156                  let 〈addr1, addr2〉 ≝ r in
157                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
158                    set_arg_8 s addr1 and_val
159                ]
160            | Right r ⇒
161              let 〈addr1, addr2〉 ≝ r in
162              let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
163                set_flags s and_val (Nothing ?) (get_ov_flag s)
164            ]
165        | ORL addr ⇒
166          match addr with
167            [ Left l ⇒
168              match l with
169                [ Left l' ⇒
170                  let 〈addr1, addr2〉 ≝ l' in
171                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
172                    set_arg_8 s addr1 or_val
173                | Right r ⇒
174                  let 〈addr1, addr2〉 ≝ r in
175                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
176                    set_arg_8 s addr1 or_val
177                ]
178            | Right r ⇒
179              let 〈addr1, addr2〉 ≝ r in
180              let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
181                set_flags s or_val (Nothing ?) (get_ov_flag s)
182            ]
183        | XRL addr ⇒
184          match addr with
185            [ Left l' ⇒
186              let 〈addr1, addr2〉 ≝ l' in
187              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
188                set_arg_8 s addr1 xor_val
189            | Right r ⇒
190              let 〈addr1, addr2〉 ≝ r in
191              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
192                set_arg_8 s addr1 xor_val
193            ]
194        | INC addr ⇒
195            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
196                                                           register;
197                                                           direct;
198                                                           indirect;
199                                                           dptr ]] x) → ? with
200              [ ACC_A ⇒ λacc_a: True.
201                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
202                  set_arg_8 s ACC_A result
203              | REGISTER r ⇒ λregister: True.
204                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
205                  set_arg_8 s (REGISTER r) result
206              | DIRECT d ⇒ λdirect: True.
207                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
208                  set_arg_8 s (DIRECT d) result
209              | INDIRECT i ⇒ λindirect: True.
210                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
211                  set_arg_8 s (INDIRECT i) result
212              | DPTR ⇒ λdptr: True.
213                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
214                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
215                let s ≝ set_8051_sfr s SFR_DPL bl in
216                  set_8051_sfr s SFR_DPH bu
217              | _ ⇒ λother: False. ⊥
218              ] (subaddressing_modein … addr)
219       | DEC addr ⇒
220           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
221             set_arg_8 s addr result
222        | MUL addr1 addr2 ⇒
223           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
224           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
225           let product ≝ acc_a_nat * acc_b_nat in
226           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
227           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
228           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
229           let s ≝ set_8051_sfr s SFR_ACC_A low in
230             set_8051_sfr s SFR_ACC_B high
231        | DIV addr1 addr2 ⇒
232           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
233           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
234             match acc_b_nat with
235               [ Z ⇒ set_flags s false (Nothing Bit) true
236               | S o ⇒
237                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
238                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
239                 let s ≝ set_8051_sfr s SFR_ACC_A q in
240                 let s ≝ set_8051_sfr s SFR_ACC_B r in
241                   set_flags s false (Nothing Bit) false
242               ]
243        | DA addr ⇒
244            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
245              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
246                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
247                let cy_flag ≝ get_index' ? Z ? flags in
248                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
249                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
250                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
251                    let new_acc ≝ nu @@ acc_nl' in
252                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
253                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
254                  else
255                    s
256              else
257                s
258        | CLR addr ⇒
259          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
260            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
261            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
262            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
263            | _ ⇒ λother: False. ⊥
264            ] (subaddressing_modein … addr)
265        | CPL addr ⇒
266          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
267            [ ACC_A ⇒ λacc_a: True.
268                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
269                let new_acc ≝ negation_bv ? old_acc in
270                  set_8051_sfr s SFR_ACC_A new_acc
271            | CARRY ⇒ λcarry: True.
272                let old_cy_flag ≝ get_arg_1 s CARRY true in
273                let new_cy_flag ≝ negation old_cy_flag in
274                  set_arg_1 s CARRY new_cy_flag
275            | BIT_ADDR b ⇒ λbit_addr: True.
276                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
277                let new_bit ≝ negation old_bit in
278                  set_arg_1 s (BIT_ADDR b) new_bit
279            | _ ⇒ λother: False. ?
280            ] (subaddressing_modein … addr)
281        | SETB b ⇒ set_arg_1 s b false
282        | RL _ ⇒ (* DPM: always ACC_A *)
283            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
284            let new_acc ≝ rotate_left … one old_acc in
285              set_8051_sfr s SFR_ACC_A new_acc
286        | RR _ ⇒ (* DPM: always ACC_A *)
287            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
288            let new_acc ≝ rotate_right … one old_acc in
289              set_8051_sfr s SFR_ACC_A new_acc
290        | RLC _ ⇒ (* DPM: always ACC_A *)
291            let old_cy_flag ≝ get_cy_flag s in
292            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
293            let new_cy_flag ≝ get_index' ? Z ? old_acc in
294            let new_acc ≝ shift_left ? eight one old_acc old_cy_flag in
295            let s ≝ set_arg_1 s CARRY new_cy_flag in
296              set_8051_sfr s SFR_ACC_A new_acc
297        | RRC _ ⇒ (* DPM: always ACC_A *)
298            let old_cy_flag ≝ get_cy_flag s in
299            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
300            let new_cy_flag ≝ get_index' ? seven ? old_acc in
301            let new_acc ≝ shift_right ? eight one old_acc old_cy_flag in
302            let s ≝ set_arg_1 s CARRY new_cy_flag in
303              set_8051_sfr s SFR_ACC_A new_acc
304        | SWAP _ ⇒ (* DPM: always ACC_A *)
305            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
306            let 〈nu,nl〉 ≝ split ? four four old_acc in
307            let new_acc ≝ nl @@ nu in
308              set_8051_sfr s SFR_ACC_A new_acc
309        | PUSH addr ⇒
310            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
311              [ DIRECT d ⇒ λdirect: True.
312                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
313                let s ≝ set_8051_sfr s SFR_SP new_sp in
314                  write_at_stack_pointer s d
315              | _ ⇒ λother: False. ⊥
316              ] (subaddressing_modein … addr)
317        | POP addr ⇒
318            let contents ≝ read_at_stack_pointer s in
319            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
320            let s ≝ set_8051_sfr s SFR_SP new_sp in
321              set_arg_8 s addr contents
322        | XCH addr1 addr2 ⇒
323            let old_addr ≝ get_arg_8 s false addr2 in
324            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
325            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
326              set_arg_8 s addr2 old_acc
327        | XCHD addr1 addr2 ⇒
328            let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
329            let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
330            let new_acc ≝ acc_nu @@ arg_nl in
331            let new_arg ≝ arg_nu @@ acc_nl in
332            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
333              set_arg_8 s addr2 new_arg
334        | RET ⇒
335            let high_bits ≝ read_at_stack_pointer s in
336            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
337            let s ≝ set_8051_sfr s SFR_SP new_sp in
338            let low_bits ≝ read_at_stack_pointer s in
339            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
340            let s ≝ set_8051_sfr s SFR_SP new_sp in
341            let new_pc ≝ high_bits @@ low_bits in
342              set_program_counter s new_pc
343        | RETI ⇒
344            let high_bits ≝ read_at_stack_pointer s in
345            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
346            let s ≝ set_8051_sfr s SFR_SP new_sp in
347            let low_bits ≝ read_at_stack_pointer s in
348            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
349            let s ≝ set_8051_sfr s SFR_SP new_sp in
350            let new_pc ≝ high_bits @@ low_bits in
351              set_program_counter s new_pc
352        | Jump j ⇒
353          match j with
354            [ JC addr ⇒
355              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
356                [ RELATIVE r ⇒ λrel: True.
357                  if get_cy_flag s then
358                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
359                      set_program_counter s new_pc
360                  else
361                    s
362                | _ ⇒ λother: False. ⊥
363                ] (subaddressing_modein … addr)
364            | JNC addr ⇒
365              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
366                [ RELATIVE r ⇒ λrel: True.
367                  if negation (get_cy_flag s) then
368                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
369                      set_program_counter s new_pc
370                  else
371                    s
372                | _ ⇒ λother: False. ⊥
373                ] (subaddressing_modein … addr)
374            | JB addr1 addr2 ⇒
375              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
376                [ RELATIVE r ⇒ λrel: True.
377                  if get_arg_1 s addr1 false then
378                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
379                      set_program_counter s new_pc
380                  else
381                    s
382                | _ ⇒ λother: False. ⊥
383                ] (subaddressing_modein … addr2)
384            | JNB addr1 addr2 ⇒
385              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
386                [ RELATIVE r ⇒ λrel: True.
387                  if negation (get_arg_1 s addr1 false) then
388                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
389                      set_program_counter s new_pc
390                  else
391                    s
392                | _ ⇒ λother: False. ⊥
393                ] (subaddressing_modein … addr2)
394            | JBC addr1 addr2 ⇒
395              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
396                [ RELATIVE r ⇒ λrel: True.
397                  let s ≝ set_arg_1 s addr1 false in
398                    if get_arg_1 s addr1 false then
399                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
400                        set_program_counter s new_pc
401                    else
402                      s
403                | _ ⇒ λother: False. ⊥
404                ] (subaddressing_modein … addr2)
405            | JZ addr ⇒
406              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
407                [ RELATIVE r ⇒ λrel: True.
408                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
409                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
410                        set_program_counter s new_pc
411                    else
412                      s
413                | _ ⇒ λother: False. ⊥
414                ] (subaddressing_modein … addr)
415            | JNZ addr ⇒
416              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
417                [ RELATIVE r ⇒ λrel: True.
418                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
419                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
420                        set_program_counter s new_pc
421                    else
422                      s
423                | _ ⇒ λother: False. ⊥
424                ] (subaddressing_modein … addr)
425            | CJNE addr1 addr2 ⇒
426              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
427                [ RELATIVE r ⇒ λrelative: True.
428                  match addr1 with
429                    [ Left l ⇒
430                        let 〈addr1, addr2〉 ≝ l in
431                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
432                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
433                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
434                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
435                            let s ≝ set_program_counter s new_pc in
436                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
437                          else
438                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
439                    | Right r' ⇒
440                        let 〈addr1, addr2〉 ≝ r' in
441                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
442                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
443                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
444                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
445                            let s ≝ set_program_counter s new_pc in
446                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
447                          else
448                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
449                    ]
450                | _ ⇒ λother: False. ⊥
451                ] (subaddressing_modein … addr2)
452            | DJNZ addr1 addr2 ⇒
453              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
454                [ RELATIVE r ⇒ λrel: True.
455                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
456                    let s ≝ set_arg_8 s addr1 result in
457                      if negation (eq_bv ? result (zero eight)) then
458                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
459                          set_program_counter s new_pc
460                      else
461                        s
462                | _ ⇒ λother: False. ⊥
463                ] (subaddressing_modein … addr2)
464            ]
465        | JMP _ ⇒ (* DPM: always indirect_dptr *)
466          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
467          let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
468          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
469          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
470            set_program_counter s new_pc
471        | LJMP addr ⇒
472          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
473            [ ADDR16 a ⇒ λaddr16: True.
474                set_program_counter s a
475            | _ ⇒ λother: False. ⊥
476            ] (subaddressing_modein … addr)
477        | SJMP addr ⇒
478          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
479            [ RELATIVE r ⇒ λrelative: True.
480                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
481                  set_program_counter s new_pc
482            | _ ⇒ λother: False. ⊥
483            ] (subaddressing_modein … addr)
484        | AJMP addr ⇒
485          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
486            [ ADDR11 a ⇒ λaddr11: True.
487              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
488              let 〈nu, nl〉 ≝ split ? four four pc_bu in
489              let bit ≝ get_index' ? Z ? nl in
490              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
491              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
492              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
493                set_program_counter s new_pc
494            | _ ⇒ λother: False. ⊥
495            ] (subaddressing_modein … addr)
496        | MOVC addr1 addr2 ⇒
497          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
498            [ ACC_DPTR ⇒ λacc_dptr: True.
499              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
500              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
501              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
502              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
503                set_8051_sfr s SFR_ACC_A result
504            | ACC_PC ⇒ λacc_pc: True.
505              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
506              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in
507              (* DPM: Under specified: does the carry from PC incrementation affect the *)
508              (*      addition of the PC with the DPTR? At the moment, no.              *)
509              let s ≝ set_program_counter s inc_pc in
510              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
511              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
512                set_8051_sfr s SFR_ACC_A result
513            | _ ⇒ λother: False. ⊥
514            ] (subaddressing_modein … addr2)
515        | MOVX addr ⇒
516          (* DPM: only copies --- doesn't affect I/O *)
517          match addr with
518            [ Left l ⇒
519              let 〈addr1, addr2〉 ≝ l in
520                set_arg_8 s addr1 (get_arg_8 s false addr2)
521            | Right r ⇒
522              let 〈addr1, addr2〉 ≝ r in
523                set_arg_8 s addr1 (get_arg_8 s false addr2)
524            ]
525        | MOV addr ⇒
526          match addr with
527            [ Left l ⇒
528              match l with
529                [ Left l' ⇒
530                  match l' with
531                    [ Left l'' ⇒
532                      match l'' with
533                        [ Left l''' ⇒
534                          match l''' with
535                            [ Left l'''' ⇒
536                              let 〈addr1, addr2〉 ≝ l'''' in
537                                set_arg_8 s addr1 (get_arg_8 s false addr2)
538                            | Right r'''' ⇒
539                              let 〈addr1, addr2〉 ≝ r'''' in
540                                set_arg_8 s addr1 (get_arg_8 s false addr2)
541                            ]
542                        | Right r''' ⇒
543                          let 〈addr1, addr2〉 ≝ r''' in
544                            set_arg_8 s addr1 (get_arg_8 s false addr2)
545                        ]
546                    | Right r'' ⇒
547                      let 〈addr1, addr2〉 ≝ r'' in
548                        set_arg_16 s (get_arg_16 s addr2) addr1
549                    ]
550                | Right r ⇒
551                  let 〈addr1, addr2〉 ≝ r in
552                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
553                ]
554            | Right r ⇒
555              let 〈addr1, addr2〉 ≝ r in
556                set_arg_1 s addr1 (get_arg_1 s addr2 false)
557            ]
558        | LCALL addr ⇒
559          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
560            [ ADDR16 a ⇒ λaddr16: True.
561              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
562              let s ≝ set_8051_sfr s SFR_SP new_sp in
563              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
564              let s ≝ write_at_stack_pointer s pc_bl in
565              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
566              let s ≝ set_8051_sfr s SFR_SP new_sp in
567              let s ≝ write_at_stack_pointer s pc_bu in
568                set_program_counter s a
569            | _ ⇒ λother: False. ⊥
570            ] (subaddressing_modein … addr)
571        | ACALL addr ⇒
572          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
573            [ ADDR11 a ⇒ λaddr11: True.
574              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
575              let s ≝ set_8051_sfr s SFR_SP new_sp in
576              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
577              let s ≝ write_at_stack_pointer s pc_bl in
578              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
579              let s ≝ set_8051_sfr s SFR_SP new_sp in
580              let s ≝ write_at_stack_pointer s pc_bu in
581              let 〈thr, eig〉 ≝ split ? three eight a in
582              let 〈fiv, thr'〉 ≝ split ? five three pc_bu in
583              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
584                set_program_counter s new_addr
585            | _ ⇒ λother: False. ⊥
586            ] (subaddressing_modein … addr)
587        | NOP ⇒ s
588        ]
589    in
590      s.
591    ntry nassumption;
592    ntry (
593      nnormalize
594      nrepeat (napply (less_than_or_equal_monotone))
595      napply (less_than_or_equal_zero)
596    );
597    ntry (
598      napply (execute_1_technical … (subaddressing_modein …))
599      napply I
600    );
601    ntry (
602      nnormalize
603      napply I
604    );     
605nqed.
606
607nlet rec execute (n: Nat) (s: Status) on n: Status ≝
608  match n with
609    [ Z ⇒ s
610    | S o ⇒ execute o (execute_1 s)
611    ].
Note: See TracBrowser for help on using the repository browser.