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

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

Added subvector_with function.

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