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

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

All 450 proof obligations closed.

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