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

Last change on this file since 369 was 369, checked in by mulligan, 10 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.