source: src/ASM/Interpret.ma @ 1519

Last change on this file since 1519 was 1519, checked in by campbell, 8 years ago

More syntax updates.

File size: 30.8 KB
Line 
1include "ASM/Status.ma".
2include "ASM/Fetch.ma".
3
4definition sign_extension: Byte → Word ≝
5  λc.
6    let b ≝ get_index_v ? 8 c 1 ? in
7      [[ b; b; b; b; b; b; b; b ]] @@ c.
8  normalize;
9  repeat (@ (le_S_S ?));
10  @ (le_O_n);
11qed.
12   
13lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
14 # a
15 # b
16 cases a
17 cases b
18 normalize
19 //
20 # K
21 cases (eq_true_false K)
22qed.
23
24lemma is_a_to_mem_to_is_in:
25 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
26 # he
27 # a
28 # m
29 # q
30 elim q
31 [ normalize
32   # _
33   # K
34   assumption
35 | # m'
36   # t
37   # q'
38   # II
39   # H1
40   # H2
41   normalize
42   change in H2: (??%?); with (orb ??)
43   cases (inclusive_disjunction_true … H2)
44   [ # K
45     < (eq_a_to_eq … K)
46     > H1
47     %
48   | # K
49     > II
50     try assumption
51     cases (is_a t a)
52     normalize
53     %
54   ]
55 ]
56qed.
57
58lemma execute_1_technical:
59  ∀n, m: nat.
60  ∀v: Vector addressing_mode_tag (S n).
61  ∀q: Vector addressing_mode_tag (S m).
62  ∀a: addressing_mode.
63    bool_to_Prop (is_in ? v a) →
64    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
65    bool_to_Prop (is_in ? q a).
66 # n
67 # m
68 # v
69 # q
70 # a
71 elim v
72 [ normalize
73   # K
74   cases K
75 | # n'
76   # he
77   # tl
78   # II
79   whd in ⊢ (% → ? → ?);
80   lapply (refl … (is_in … (he:::tl) a))
81   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
82   [ # K
83     # _
84     normalize in K;
85     whd in ⊢ (% → ?);
86     lapply (refl … (subvector_with … eq_a (he:::tl) q));
87     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
88     [ # K1
89       # _
90       change in K1; with ((andb ? (subvector_with …)) = true)
91       cases (conjunction_true … K1)
92       # K3
93       # K4
94       cases (inclusive_disjunction_true … K)
95       # K2
96       [ > (is_a_to_mem_to_is_in … K2 K3)
97         %
98       | @ II
99         [ > K2
100           %
101         | > K4
102           %
103         ]
104       ]
105     | # K1
106       # K2
107       (normalize in K2;)
108       cases K2;
109     ]
110   | # K1
111     # K2
112     normalize in K2;
113     cases K2
114   ]
115 ]
116qed.
117
118include alias "arithmetics/nat.ma".
119include alias "ASM/BitVectorTrie.ma".
120
121definition execute_1_preinstruction:
122 ∀ticks: nat × nat.
123 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
124  λticks.
125  λA, M: Type[0].
126  λaddr_of: A → (PreStatus M) → Word.
127  λinstr: preinstruction A.
128  λs: PreStatus M.
129  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
130  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
131  match instr with
132        [ ADD addr1 addr2 ⇒
133            let s ≝ add_ticks1 s in
134            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
135                                                   (get_arg_8 ? s false addr2) false in
136            let cy_flag ≝ get_index' ? O  ? flags in
137            let ac_flag ≝ get_index' ? 1 ? flags in
138            let ov_flag ≝ get_index' ? 2 ? flags in
139            let s ≝ set_arg_8 ? s ACC_A result in
140              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
141        | ADDC addr1 addr2 ⇒
142            let s ≝ add_ticks1 s in
143            let old_cy_flag ≝ get_cy_flag ? s in
144            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
145                                                   (get_arg_8 ? s false addr2) old_cy_flag in
146            let cy_flag ≝ get_index' ? O ? flags in
147            let ac_flag ≝ get_index' ? 1 ? flags in
148            let ov_flag ≝ get_index' ? 2 ? flags in
149            let s ≝ set_arg_8 ? s ACC_A result in
150              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
151        | SUBB addr1 addr2 ⇒
152            let s ≝ add_ticks1 s in
153            let old_cy_flag ≝ get_cy_flag ? s in
154            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
155                                                   (get_arg_8 ? s false addr2) old_cy_flag in
156            let cy_flag ≝ get_index' ? O ? flags in
157            let ac_flag ≝ get_index' ? 1 ? flags in
158            let ov_flag ≝ get_index' ? 2 ? flags in
159            let s ≝ set_arg_8 ? s ACC_A result in
160              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
161        | ANL addr ⇒
162          let s ≝ add_ticks1 s in
163          match addr with
164            [ inl l ⇒
165              match l with
166                [ inl l' ⇒
167                  let 〈addr1, addr2〉 ≝ l' in
168                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
169                    set_arg_8 ? s addr1 and_val
170                | inr r ⇒
171                  let 〈addr1, addr2〉 ≝ r in
172                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
173                    set_arg_8 ? s addr1 and_val
174                ]
175            | inr r ⇒
176              let 〈addr1, addr2〉 ≝ r in
177              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
178                set_flags ? s and_val (None ?) (get_ov_flag ? s)
179            ]
180        | ORL addr ⇒
181          let s ≝ add_ticks1 s in
182          match addr with
183            [ inl l ⇒
184              match l with
185                [ inl l' ⇒
186                  let 〈addr1, addr2〉 ≝ l' in
187                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
188                    set_arg_8 ? s addr1 or_val
189                | inr r ⇒
190                  let 〈addr1, addr2〉 ≝ r in
191                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
192                    set_arg_8 ? s addr1 or_val
193                ]
194            | inr r ⇒
195              let 〈addr1, addr2〉 ≝ r in
196              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
197                set_flags ? s or_val (None ?) (get_ov_flag ? s)
198            ]
199        | XRL addr ⇒
200          let s ≝ add_ticks1 s in
201          match addr with
202            [ inl l' ⇒
203              let 〈addr1, addr2〉 ≝ l' in
204              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
205                set_arg_8 ? s addr1 xor_val
206            | inr r ⇒
207              let 〈addr1, addr2〉 ≝ r in
208              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
209                set_arg_8 ? s addr1 xor_val
210            ]
211        | INC addr ⇒
212            let s ≝ add_ticks1 s in
213            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
214                                                           registr;
215                                                           direct;
216                                                           indirect;
217                                                           dptr ]] x) → ? with
218              [ ACC_A ⇒ λacc_a: True.
219                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
220                  set_arg_8 ? s ACC_A result
221              | REGISTER r ⇒ λregister: True.
222                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
223                  set_arg_8 ? s (REGISTER r) result
224              | DIRECT d ⇒ λdirect: True.
225                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
226                  set_arg_8 ? s (DIRECT d) result
227              | INDIRECT i ⇒ λindirect: True.
228                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
229                  set_arg_8 ? s (INDIRECT i) result
230              | DPTR ⇒ λdptr: True.
231                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
232                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
233                let s ≝ set_8051_sfr ? s SFR_DPL bl in
234                  set_8051_sfr ? s SFR_DPH bu
235              | _ ⇒ λother: False. ⊥
236              ] (subaddressing_modein … addr)
237        | DEC addr ⇒
238           let s ≝ add_ticks1 s in
239           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
240             set_arg_8 ? s addr result
241        | MUL addr1 addr2 ⇒
242           let s ≝ add_ticks1 s in
243           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
244           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
245           let product ≝ acc_a_nat * acc_b_nat in
246           let ov_flag ≝ product ≥ 256 in
247           let low ≝ bitvector_of_nat 8 (product mod 256) in
248           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
249           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
250             set_8051_sfr ? s SFR_ACC_B high
251        | DIV addr1 addr2 ⇒
252           let s ≝ add_ticks1 s in
253           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
254           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
255             match acc_b_nat with
256               [ O ⇒ set_flags ? s false (None Bit) true
257               | S o ⇒
258                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
259                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
260                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
261                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
262                   set_flags ? s false (None Bit) false
263               ]
264        | DA addr ⇒
265            let s ≝ add_ticks1 s in
266            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
267              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
268                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
269                let cy_flag ≝ get_index' ? O ? flags in
270                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
271                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
272                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
273                    let new_acc ≝ nu @@ acc_nl' in
274                    let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
275                      set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
276                  else
277                    s
278              else
279                s
280        | CLR addr ⇒
281          let s ≝ add_ticks1 s in
282          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
283            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
284            | CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
285            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
286            | _ ⇒ λother: False. ⊥
287            ] (subaddressing_modein … addr)
288        | CPL addr ⇒
289          let s ≝ add_ticks1 s in
290          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
291            [ ACC_A ⇒ λacc_a: True.
292                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
293                let new_acc ≝ negation_bv ? old_acc in
294                  set_8051_sfr ? s SFR_ACC_A new_acc
295            | CARRY ⇒ λcarry: True.
296                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
297                let new_cy_flag ≝ ¬old_cy_flag in
298                  set_arg_1 ? s CARRY new_cy_flag
299            | BIT_ADDR b ⇒ λbit_addr: True.
300                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
301                let new_bit ≝ ¬old_bit in
302                  set_arg_1 ? s (BIT_ADDR b) new_bit
303            | _ ⇒ λother: False. ?
304            ] (subaddressing_modein … addr)
305        | SETB b ⇒
306            let s ≝ add_ticks1 s in
307            set_arg_1 ? s b false
308        | RL _ ⇒ (* DPM: always ACC_A *)
309            let s ≝ add_ticks1 s in
310            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
311            let new_acc ≝ rotate_left … 1 old_acc in
312              set_8051_sfr ? s SFR_ACC_A new_acc
313        | RR _ ⇒ (* DPM: always ACC_A *)
314            let s ≝ add_ticks1 s in
315            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
316            let new_acc ≝ rotate_right … 1 old_acc in
317              set_8051_sfr ? s SFR_ACC_A new_acc
318        | RLC _ ⇒ (* DPM: always ACC_A *)
319            let s ≝ add_ticks1 s in
320            let old_cy_flag ≝ get_cy_flag ? s in
321            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
322            let new_cy_flag ≝ get_index' ? O ? old_acc in
323            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
324            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
325              set_8051_sfr ? s SFR_ACC_A new_acc
326        | RRC _ ⇒ (* DPM: always ACC_A *)
327            let s ≝ add_ticks1 s in
328            let old_cy_flag ≝ get_cy_flag ? s in
329            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
330            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
331            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
332            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
333              set_8051_sfr ? s SFR_ACC_A new_acc
334        | SWAP _ ⇒ (* DPM: always ACC_A *)
335            let s ≝ add_ticks1 s in
336            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
337            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
338            let new_acc ≝ nl @@ nu in
339              set_8051_sfr ? s SFR_ACC_A new_acc
340        | PUSH addr ⇒
341            let s ≝ add_ticks1 s in
342            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
343              [ DIRECT d ⇒ λdirect: True.
344                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
345                let s ≝ set_8051_sfr ? s SFR_SP new_sp in
346                  write_at_stack_pointer ? s d
347              | _ ⇒ λother: False. ⊥
348              ] (subaddressing_modein … addr)
349        | POP addr ⇒
350            let s ≝ add_ticks1 s in
351            let contents ≝ read_at_stack_pointer ? s in
352            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
353            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
354              set_arg_8 ? s addr contents
355        | XCH addr1 addr2 ⇒
356            let s ≝ add_ticks1 s in
357            let old_addr ≝ get_arg_8 ? s false addr2 in
358            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
359            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
360              set_arg_8 ? s addr2 old_acc
361        | XCHD addr1 addr2 ⇒
362            let s ≝ add_ticks1 s in
363            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
364            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
365            let new_acc ≝ acc_nu @@ arg_nl in
366            let new_arg ≝ arg_nu @@ acc_nl in
367            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
368              set_arg_8 ? s addr2 new_arg
369        | RET ⇒
370            let s ≝ add_ticks1 s in
371            let high_bits ≝ read_at_stack_pointer ? s in
372            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
373            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
374            let low_bits ≝ read_at_stack_pointer ? s in
375            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
376            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
377            let new_pc ≝ high_bits @@ low_bits in
378              set_program_counter ? s new_pc
379        | RETI ⇒
380            let s ≝ add_ticks1 s in
381            let high_bits ≝ read_at_stack_pointer ? s in
382            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
383            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
384            let low_bits ≝ read_at_stack_pointer ? s in
385            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
386            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
387            let new_pc ≝ high_bits @@ low_bits in
388              set_program_counter ? s new_pc
389        | MOVX addr ⇒
390          let s ≝ add_ticks1 s in
391          (* DPM: only copies --- doesn't affect I/O *)
392          match addr with
393            [ inl l ⇒
394              let 〈addr1, addr2〉 ≝ l in
395                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
396            | inr r ⇒
397              let 〈addr1, addr2〉 ≝ r in
398                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
399            ]
400        | MOV addr ⇒
401          let s ≝ add_ticks1 s in
402          match addr with
403            [ inl l ⇒
404              match l with
405                [ inl l' ⇒
406                  match l' with
407                    [ inl l'' ⇒
408                      match l'' with
409                        [ inl l''' ⇒
410                          match l''' with
411                            [ inl l'''' ⇒
412                              let 〈addr1, addr2〉 ≝ l'''' in
413                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
414                            | inr r'''' ⇒
415                              let 〈addr1, addr2〉 ≝ r'''' in
416                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
417                            ]
418                        | inr r''' ⇒
419                          let 〈addr1, addr2〉 ≝ r''' in
420                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
421                        ]
422                    | inr r'' ⇒
423                      let 〈addr1, addr2〉 ≝ r'' in
424                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
425                    ]
426                | inr r ⇒
427                  let 〈addr1, addr2〉 ≝ r in
428                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
429                ]
430            | inr r ⇒
431              let 〈addr1, addr2〉 ≝ r in
432                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
433            ]
434          | JC addr ⇒
435                  if get_cy_flag ? s then
436                   let s ≝ add_ticks1 s in
437                    set_program_counter ? s (addr_of addr s)
438                  else
439                   let s ≝ add_ticks2 s in
440                    s
441            | JNC addr ⇒
442                  if ¬(get_cy_flag ? s) then
443                   let s ≝ add_ticks1 s in
444                    set_program_counter ? s (addr_of addr s)
445                  else
446                   let s ≝ add_ticks2 s in
447                    s
448            | JB addr1 addr2 ⇒
449                  if get_arg_1 ? s addr1 false then
450                   let s ≝ add_ticks1 s in
451                    set_program_counter ? s (addr_of addr2 s)
452                  else
453                   let s ≝ add_ticks2 s in
454                    s
455            | JNB addr1 addr2 ⇒
456                  if ¬(get_arg_1 ? s addr1 false) then
457                   let s ≝ add_ticks1 s in
458                    set_program_counter ? s (addr_of addr2 s)
459                  else
460                   let s ≝ add_ticks2 s in
461                    s
462            | JBC addr1 addr2 ⇒
463                  let s ≝ set_arg_1 ? s addr1 false in
464                    if get_arg_1 ? s addr1 false then
465                     let s ≝ add_ticks1 s in
466                      set_program_counter ? s (addr_of addr2 s)
467                    else
468                     let s ≝ add_ticks2 s in
469                      s
470            | JZ addr ⇒
471                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
472                     let s ≝ add_ticks1 s in
473                      set_program_counter ? s (addr_of addr s)
474                    else
475                     let s ≝ add_ticks2 s in
476                      s
477            | JNZ addr ⇒
478                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
479                     let s ≝ add_ticks1 s in
480                      set_program_counter ? s (addr_of addr s)
481                    else
482                     let s ≝ add_ticks2 s in
483                      s
484            | CJNE addr1 addr2 ⇒
485                  match addr1 with
486                    [ inl l ⇒
487                        let 〈addr1, addr2'〉 ≝ l in
488                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
489                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
490                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
491                            let s ≝ add_ticks1 s in
492                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
493                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
494                          else
495                            let s ≝ add_ticks2 s in
496                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
497                    | inr r' ⇒
498                        let 〈addr1, addr2'〉 ≝ r' in
499                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
500                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
501                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
502                            let s ≝ add_ticks1 s in
503                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
504                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
505                          else
506                            let s ≝ add_ticks2 s in
507                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
508                    ]
509            | DJNZ addr1 addr2 ⇒
510              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
511              let s ≝ set_arg_8 ? s addr1 result in
512                if ¬(eq_bv ? result (zero 8)) then
513                 let s ≝ add_ticks1 s in
514                  set_program_counter ? s (addr_of addr2 s)
515                else
516                 let s ≝ add_ticks2 s in
517                  s
518        | NOP ⇒
519           let s ≝ add_ticks2 s in
520            s
521        ].
522    try assumption
523    try @I
524    try (
525      @ (execute_1_technical … (subaddressing_modein …))
526      @ I
527    )
528qed.
529
530definition execute_1_0: Status → instruction × Word × nat → Status ≝
531  λs,instr_pc_ticks.
532    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
533    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
534    let s ≝ set_program_counter ? s pc in
535    let s ≝
536      match instr with
537      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
538        (λx. λs.
539        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
540        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
541        | _ ⇒ λabsd. ⊥
542        ] (subaddressing_modein … x)) instr s
543      | ACALL addr ⇒
544          let s ≝ set_clock ? s (ticks + clock ? s) in
545          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
546            [ ADDR11 a ⇒ λaddr11: True.
547              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
548              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
549              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
550              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
551              let s ≝ write_at_stack_pointer ? s pc_bl in
552              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
553              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
554              let s ≝ write_at_stack_pointer ? s pc_bu in
555              let thr ≝ \fst (split ? 3 8 a) in
556              let eig ≝ \snd (split ? 3 8 a) in
557              let fiv ≝ \fst (split ? 5 3 pc_bu) in
558              let thr' ≝ \snd (split ? 5 3 pc_bu) in
559              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
560                set_program_counter ? s new_addr
561            | _ ⇒ λother: False. ⊥
562            ] (subaddressing_modein … addr)
563        | LCALL addr ⇒
564          let s ≝ set_clock ? s (ticks + clock ? s) in
565          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
566            [ ADDR16 a ⇒ λaddr16: True.
567              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
568              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
569              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
570              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
571              let s ≝ write_at_stack_pointer ? s pc_bl in
572              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
573              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
574              let s ≝ write_at_stack_pointer ? s pc_bu in
575                set_program_counter ? s a
576            | _ ⇒ λother: False. ⊥
577            ] (subaddressing_modein … addr)
578        | MOVC addr1 addr2 ⇒
579          let s ≝ set_clock ? s (ticks + clock ? s) in
580          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
581            [ ACC_DPTR ⇒ λacc_dptr: True.
582              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
583              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
584              let new_addr ≝ \snd (half_add ? dptr big_acc) in
585              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
586                set_8051_sfr ? s SFR_ACC_A result
587            | ACC_PC ⇒ λacc_pc: True.
588              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
589              let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
590              (* DPM: Under specified: does the carry from PC incrementation affect the *)
591              (*      addition of the PC with the DPTR? At the moment, no.              *)
592              let s ≝ set_program_counter ? s inc_pc in
593              let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
594              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
595                set_8051_sfr ? s SFR_ACC_A result
596            | _ ⇒ λother: False. ⊥
597            ] (subaddressing_modein … addr2)
598        | JMP _ ⇒ (* DPM: always indirect_dptr *)
599          let s ≝ set_clock ? s (ticks + clock ? s) in
600          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
601          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
602          let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
603          let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
604            set_program_counter ? s new_pc
605        | LJMP addr ⇒
606          let s ≝ set_clock ? s (ticks + clock ? s) in
607          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
608            [ ADDR16 a ⇒ λaddr16: True.
609                set_program_counter ? s a
610            | _ ⇒ λother: False. ⊥
611            ] (subaddressing_modein … addr)
612        | SJMP addr ⇒
613          let s ≝ set_clock ? s (ticks + clock ? s) in
614          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
615            [ RELATIVE r ⇒ λrelative: True.
616                let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
617                  set_program_counter ? s new_pc
618            | _ ⇒ λother: False. ⊥
619            ] (subaddressing_modein … addr)
620        | AJMP addr ⇒
621          let s ≝ set_clock ? s (ticks + clock ? s) in
622          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
623            [ ADDR11 a ⇒ λaddr11: True.
624              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
625              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
626              let nu ≝ \fst (split ? 4 4 pc_bu) in
627              let nl ≝ \snd (split ? 4 4 pc_bu) in
628              let bit ≝ get_index' ? O ? nl in
629              let relevant1 ≝ \fst (split ? 3 8 a) in
630              let relevant2 ≝ \snd (split ? 3 8 a) in
631              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
632              let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
633                set_program_counter ? s new_pc
634            | _ ⇒ λother: False. ⊥
635            ] (subaddressing_modein … addr)
636      ]
637    in
638      s.
639    try assumption
640    try (
641      normalize
642      repeat (@ (le_S_S))
643      @ (le_O_n)
644    )
645    try (
646      @ (execute_1_technical … (subaddressing_modein …))
647      @ I
648    )
649    try (
650      normalize
651      @ I
652    )     
653qed.
654
655definition execute_1: Status → Status ≝
656  λs: Status.
657    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
658     execute_1_0 s instr_pc_ticks.
659
660definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
661  λticks,s,instr,pc.
662  let s ≝ set_program_counter ? s pc in
663  let s ≝
664    match instr with
665    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
666    | Comment cmt ⇒
667       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
668        s
669    | Cost cst ⇒ s
670    | Jmp jmp ⇒
671       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
672        set_program_counter ? s (address_of_word_labels s jmp)
673    | Call call ⇒
674      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
675      let a ≝ address_of_word_labels s call in
676      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
677      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
678      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
679      let s ≝ write_at_stack_pointer ? s pc_bl in
680      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
681      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
682      let s ≝ write_at_stack_pointer ? s pc_bu in
683        set_program_counter ? s a
684    | Mov dptr ident ⇒
685      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
686      let preamble ≝ \fst (code_memory ? s) in
687      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
688        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
689    ]
690  in
691    s.
692  normalize
693  @ I
694qed.
695
696definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
697  λticks_of,s.
698  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
699  let ticks ≝ ticks_of (program_counter ? s) in
700   execute_1_pseudo_instruction0 ticks s instr pc.
701
702let rec execute (n: nat) (s: Status) on n: Status ≝
703  match n with
704    [ O ⇒ s
705    | S o ⇒ execute o (execute_1 s)
706    ].
707
708let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
709  match n with
710    [ O ⇒ s
711    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
712    ].
Note: See TracBrowser for help on using the repository browser.