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

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

Proof of missing lemma seems to be done, but won't Qed. My version of autotac seems to be behaving very strangely.

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