# source:src/ASM/Interpret.ma@1324

Last change on this file since 1324 was 1037, checked in by sacerdot, 9 years ago

Main theorem: comments are working again.

File size: 30.5 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).
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
133            let s ≝ add_ticks1 s in
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
142            let s ≝ add_ticks1 s in
143            let old_cy_flag ≝ get_cy_flag ? s in
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
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
162          let s ≝ add_ticks1 s in
164            [ inl l ⇒
165              match l with
166                [ inl l' ⇒
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 ⇒
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 ⇒
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            ]
181          let s ≝ add_ticks1 s in
183            [ inl l ⇒
184              match l with
185                [ inl l' ⇒
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 ⇒
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 ⇒
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            ]
200          let s ≝ add_ticks1 s in
202            [ inl l' ⇒
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 ⇒
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            ]
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. ⊥
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
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
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               ]
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
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
286            | _ ⇒ λother: False. ⊥
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
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. ?
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
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. ⊥
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
356            let s ≝ add_ticks1 s 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
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
390          let s ≝ add_ticks1 s in
391          (* DPM: only copies --- doesn't affect I/O *)
393            [ inl l ⇒
396            | inr r ⇒
399            ]
401          let s ≝ add_ticks1 s in
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'''' ⇒
414                            | inr r'''' ⇒
417                            ]
418                        | inr r''' ⇒
421                        ]
422                    | inr r'' ⇒
425                    ]
426                | inr r ⇒
429                ]
430            | inr r ⇒
433            ]
435                  if get_cy_flag ? s then
436                   let s ≝ add_ticks1 s in
438                  else
439                   let s ≝ add_ticks2 s in
440                    s
442                  if ¬(get_cy_flag ? s) then
443                   let s ≝ add_ticks1 s in
445                  else
446                   let s ≝ add_ticks2 s in
447                    s
449                  if get_arg_1 ? s addr1 false then
450                   let s ≝ add_ticks1 s in
452                  else
453                   let s ≝ add_ticks2 s in
454                    s
456                  if ¬(get_arg_1 ? s addr1 false) then
457                   let s ≝ add_ticks1 s in
459                  else
460                   let s ≝ add_ticks2 s in
461                    s
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
467                    else
468                     let s ≝ add_ticks2 s in
469                      s
471                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
472                     let s ≝ add_ticks1 s in
474                    else
475                     let s ≝ add_ticks2 s in
476                      s
478                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
479                     let s ≝ add_ticks1 s in
481                    else
482                     let s ≝ add_ticks2 s in
483                      s
486                    [ inl l ⇒
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
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' ⇒
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
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                    ]
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
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
544          let s ≝ set_clock ? s (ticks + clock ? s) in
545          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
547              let 〈carry, new_sp〉 ≝ 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, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
550              let s ≝ write_at_stack_pointer ? s pc_bl in
551              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
552              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
553              let s ≝ write_at_stack_pointer ? s pc_bu in
554              let 〈thr, eig〉 ≝ split ? 3 8 a in
555              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
556              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
558            | _ ⇒ λother: False. ⊥
561          let s ≝ set_clock ? s (ticks + clock ? s) in
562          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
564              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
565              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
566              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
567              let s ≝ write_at_stack_pointer ? s pc_bl in
568              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
569              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
570              let s ≝ write_at_stack_pointer ? s pc_bu in
571                set_program_counter ? s a
572            | _ ⇒ λother: False. ⊥
575          let s ≝ set_clock ? s (ticks + clock ? s) in
576          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
577            [ ACC_DPTR ⇒ λacc_dptr: True.
578              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
579              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
581              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
582                set_8051_sfr ? s SFR_ACC_A result
583            | ACC_PC ⇒ λacc_pc: True.
584              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
585              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
586              (* DPM: Under specified: does the carry from PC incrementation affect the *)
587              (*      addition of the PC with the DPTR? At the moment, no.              *)
588              let s ≝ set_program_counter ? s inc_pc in
590              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
591                set_8051_sfr ? s SFR_ACC_A result
592            | _ ⇒ λother: False. ⊥
594        | JMP _ ⇒ (* DPM: always indirect_dptr *)
595          let s ≝ set_clock ? s (ticks + clock ? s) in
596          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
597          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
599          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
600            set_program_counter ? s new_pc
602          let s ≝ set_clock ? s (ticks + clock ? s) in
603          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
605                set_program_counter ? s a
606            | _ ⇒ λother: False. ⊥
609          let s ≝ set_clock ? s (ticks + clock ? s) in
610          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
611            [ RELATIVE r ⇒ λrelative: True.
612                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
613                  set_program_counter ? s new_pc
614            | _ ⇒ λother: False. ⊥
617          let s ≝ set_clock ? s (ticks + clock ? s) in
618          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
620              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
621              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
622              let bit ≝ get_index' ? O ? nl in
623              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
624              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
625              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
626                set_program_counter ? s new_pc
627            | _ ⇒ λother: False. ⊥
629      ]
630    in
631      s.
632    try assumption
633    try (
634      normalize
635      repeat (@ (le_S_S))
636      @ (le_O_n)
637    )
638    try (
639      @ (execute_1_technical … (subaddressing_modein …))
640      @ I
641    )
642    try (
643      normalize
644      @ I
645    )
646qed.
647
648definition execute_1: Status → Status ≝
649  λs: Status.
650    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
651     execute_1_0 s instr_pc_ticks.
652
653definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
654  λticks,s,instr,pc.
655  let s ≝ set_program_counter ? s pc in
656  let s ≝
657    match instr with
658    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
659    | Comment cmt ⇒
660       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
661        s
662    | Cost cst ⇒ s
663    | Jmp jmp ⇒
664       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
665        set_program_counter ? s (address_of_word_labels s jmp)
666    | Call call ⇒
667      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
668      let a ≝ address_of_word_labels s call in
669      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
670      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
671      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
672      let s ≝ write_at_stack_pointer ? s pc_bl in
673      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
674      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
675      let s ≝ write_at_stack_pointer ? s pc_bu in
676        set_program_counter ? s a
677    | Mov dptr ident ⇒
678      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
679      let preamble ≝ \fst (code_memory ? s) in
680      let data_labels ≝ construct_datalabels preamble in
681        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
682    ]
683  in
684    s.
685  normalize
686  @ I
687qed.
688
689definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
690  λticks_of,s.
691  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
692  let ticks ≝ ticks_of (program_counter ? s) in
693   execute_1_pseudo_instruction0 ticks s instr pc.
694
695let rec execute (n: nat) (s: Status) on n: Status ≝
696  match n with
697    [ O ⇒ s
698    | S o ⇒ execute o (execute_1 s)
699    ].
700
701let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
702  match n with
703    [ O ⇒ s
704    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
705    ].
Note: See TracBrowser for help on using the repository browser.