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

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

No more axioms but the paralogisms.

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