source: src/ASM/Interpret.ma @ 985

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

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File size: 30.3 KB
RevLine 
[698]1include "ASM/Status.ma".
2include "ASM/Fetch.ma".
[475]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.
[712]117
118include alias "arithmetics/nat.ma".
[757]119include alias "ASM/BitVectorTrie.ma".
[712]120
[936]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.
[821]125  λA, M: Type[0].
[822]126  λaddr_of: A → (PreStatus M) → Word.
[820]127  λinstr: preinstruction A.
[821]128  λs: PreStatus M.
[936]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
[820]131  match instr with
[475]132        [ ADD addr1 addr2 ⇒
[936]133            let s ≝ add_ticks1 s in
[821]134            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
135                                                   (get_arg_8 ? s false addr2) false in
[475]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
[821]139            let s ≝ set_arg_8 ? s ACC_A result in
140              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]141        | ADDC addr1 addr2 ⇒
[936]142            let s ≝ add_ticks1 s in
[821]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
[475]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
[821]149            let s ≝ set_arg_8 ? s ACC_A result in
150              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]151        | SUBB addr1 addr2 ⇒
[936]152            let s ≝ add_ticks1 s in
[821]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
[475]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
[821]159            let s ≝ set_arg_8 ? s ACC_A result in
160              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]161        | ANL addr ⇒
[936]162          let s ≝ add_ticks1 s in
[475]163          match addr with
164            [ inl l ⇒
165              match l with
166                [ inl l' ⇒
167                  let 〈addr1, addr2〉 ≝ l' in
[821]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
[475]170                | inr r ⇒
171                  let 〈addr1, addr2〉 ≝ r in
[821]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
[475]174                ]
175            | inr r ⇒
176              let 〈addr1, addr2〉 ≝ r in
[822]177              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
[821]178                set_flags ? s and_val (None ?) (get_ov_flag ? s)
[475]179            ]
180        | ORL addr ⇒
[936]181          let s ≝ add_ticks1 s in
[475]182          match addr with
183            [ inl l ⇒
184              match l with
185                [ inl l' ⇒
186                  let 〈addr1, addr2〉 ≝ l' in
[821]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
[475]189                | inr r ⇒
190                  let 〈addr1, addr2〉 ≝ r in
[821]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
[475]193                ]
194            | inr r ⇒
195              let 〈addr1, addr2〉 ≝ r in
[821]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)
[475]198            ]
199        | XRL addr ⇒
[936]200          let s ≝ add_ticks1 s in
[475]201          match addr with
202            [ inl l' ⇒
203              let 〈addr1, addr2〉 ≝ l' in
[821]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
[475]206            | inr r ⇒
207              let 〈addr1, addr2〉 ≝ r in
[821]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
[475]210            ]
211        | INC addr ⇒
[936]212            let s ≝ add_ticks1 s in
[475]213            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
[757]214                                                           registr;
[475]215                                                           direct;
216                                                           indirect;
217                                                           dptr ]] x) → ? with
218              [ ACC_A ⇒ λacc_a: True.
[821]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
[475]221              | REGISTER r ⇒ λregister: True.
[821]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
[475]224              | DIRECT d ⇒ λdirect: True.
[821]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
[475]227              | INDIRECT i ⇒ λindirect: True.
[821]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
[475]230              | DPTR ⇒ λdptr: True.
[821]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
[475]235              | _ ⇒ λother: False. ⊥
236              ] (subaddressing_modein … addr)
237        | DEC addr ⇒
[936]238           let s ≝ add_ticks1 s in
[821]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
[475]241        | MUL addr1 addr2 ⇒
[936]242           let s ≝ add_ticks1 s in
[821]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
[475]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
[821]249           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
250             set_8051_sfr ? s SFR_ACC_B high
[475]251        | DIV addr1 addr2 ⇒
[936]252           let s ≝ add_ticks1 s in
[821]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
[475]255             match acc_b_nat with
[821]256               [ O ⇒ set_flags ? s false (None Bit) true
[475]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
[821]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
[475]263               ]
264        | DA addr ⇒
[936]265            let s ≝ add_ticks1 s in
[821]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
[475]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
[821]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)
[475]276                  else
277                    s
278              else
279                s
280        | CLR addr ⇒
[936]281          let s ≝ add_ticks1 s in
[475]282          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
[821]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
[475]286            | _ ⇒ λother: False. ⊥
287            ] (subaddressing_modein … addr)
288        | CPL addr ⇒
[936]289          let s ≝ add_ticks1 s in
[475]290          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
291            [ ACC_A ⇒ λacc_a: True.
[821]292                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]293                let new_acc ≝ negation_bv ? old_acc in
[821]294                  set_8051_sfr ? s SFR_ACC_A new_acc
[475]295            | CARRY ⇒ λcarry: True.
[821]296                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
[475]297                let new_cy_flag ≝ ¬old_cy_flag in
[821]298                  set_arg_1 ? s CARRY new_cy_flag
[475]299            | BIT_ADDR b ⇒ λbit_addr: True.
[821]300                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
[475]301                let new_bit ≝ ¬old_bit in
[821]302                  set_arg_1 ? s (BIT_ADDR b) new_bit
[475]303            | _ ⇒ λother: False. ?
304            ] (subaddressing_modein … addr)
[936]305        | SETB b ⇒
306            let s ≝ add_ticks1 s in
307            set_arg_1 ? s b false
[475]308        | RL _ ⇒ (* DPM: always ACC_A *)
[936]309            let s ≝ add_ticks1 s in
[821]310            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]311            let new_acc ≝ rotate_left … 1 old_acc in
[821]312              set_8051_sfr ? s SFR_ACC_A new_acc
[475]313        | RR _ ⇒ (* DPM: always ACC_A *)
[936]314            let s ≝ add_ticks1 s in
[821]315            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]316            let new_acc ≝ rotate_right … 1 old_acc in
[821]317              set_8051_sfr ? s SFR_ACC_A new_acc
[475]318        | RLC _ ⇒ (* DPM: always ACC_A *)
[936]319            let s ≝ add_ticks1 s in
[821]320            let old_cy_flag ≝ get_cy_flag ? s in
321            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]322            let new_cy_flag ≝ get_index' ? O ? old_acc in
323            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
[821]324            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
325              set_8051_sfr ? s SFR_ACC_A new_acc
[475]326        | RRC _ ⇒ (* DPM: always ACC_A *)
[936]327            let s ≝ add_ticks1 s in
[821]328            let old_cy_flag ≝ get_cy_flag ? s in
329            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]330            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
331            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
[821]332            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
333              set_8051_sfr ? s SFR_ACC_A new_acc
[475]334        | SWAP _ ⇒ (* DPM: always ACC_A *)
[936]335            let s ≝ add_ticks1 s in
[821]336            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]337            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
338            let new_acc ≝ nl @@ nu in
[821]339              set_8051_sfr ? s SFR_ACC_A new_acc
[475]340        | PUSH addr ⇒
[936]341            let s ≝ add_ticks1 s in
[475]342            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
343              [ DIRECT d ⇒ λdirect: True.
[821]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
[475]347              | _ ⇒ λother: False. ⊥
348              ] (subaddressing_modein … addr)
349        | POP addr ⇒
[936]350            let s ≝ add_ticks1 s in
[821]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
[475]355        | XCH addr1 addr2 ⇒
[936]356            let s ≝ add_ticks1 s in
[821]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
[475]361        | XCHD addr1 addr2 ⇒
[936]362            let s ≝ add_ticks1 s in
[821]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
[475]365            let new_acc ≝ acc_nu @@ arg_nl in
366            let new_arg ≝ arg_nu @@ acc_nl in
[821]367            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
368              set_arg_8 ? s addr2 new_arg
[475]369        | RET ⇒
[936]370            let s ≝ add_ticks1 s in
[821]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
[475]377            let new_pc ≝ high_bits @@ low_bits in
[821]378              set_program_counter ? s new_pc
[475]379        | RETI ⇒
[936]380            let s ≝ add_ticks1 s in
[821]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
[475]387            let new_pc ≝ high_bits @@ low_bits in
[821]388              set_program_counter ? s new_pc
[475]389        | MOVX addr ⇒
[936]390          let s ≝ add_ticks1 s in
[475]391          (* DPM: only copies --- doesn't affect I/O *)
392          match addr with
393            [ inl l ⇒
394              let 〈addr1, addr2〉 ≝ l in
[821]395                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]396            | inr r ⇒
397              let 〈addr1, addr2〉 ≝ r in
[821]398                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]399            ]
400        | MOV addr ⇒
[936]401          let s ≝ add_ticks1 s in
[475]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
[821]413                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]414                            | inr r'''' ⇒
415                              let 〈addr1, addr2〉 ≝ r'''' in
[821]416                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]417                            ]
418                        | inr r''' ⇒
419                          let 〈addr1, addr2〉 ≝ r''' in
[821]420                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]421                        ]
422                    | inr r'' ⇒
423                      let 〈addr1, addr2〉 ≝ r'' in
[821]424                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
[475]425                    ]
426                | inr r ⇒
427                  let 〈addr1, addr2〉 ≝ r in
[821]428                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
[475]429                ]
430            | inr r ⇒
431              let 〈addr1, addr2〉 ≝ r in
[821]432                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
[475]433            ]
[820]434          | JC addr ⇒
[821]435                  if get_cy_flag ? s then
[936]436                   let s ≝ add_ticks1 s in
437                    set_program_counter ? s (addr_of addr s)
[712]438                  else
[936]439                   let s ≝ add_ticks2 s in
[712]440                    s
441            | JNC addr ⇒
[821]442                  if ¬(get_cy_flag ? s) then
[936]443                   let s ≝ add_ticks1 s in
444                    set_program_counter ? s (addr_of addr s)
[712]445                  else
[936]446                   let s ≝ add_ticks2 s in
[712]447                    s
448            | JB addr1 addr2 ⇒
[821]449                  if get_arg_1 ? s addr1 false then
[936]450                   let s ≝ add_ticks1 s in
451                    set_program_counter ? s (addr_of addr2 s)
[712]452                  else
[936]453                   let s ≝ add_ticks2 s in
[712]454                    s
455            | JNB addr1 addr2 ⇒
[821]456                  if ¬(get_arg_1 ? s addr1 false) then
[936]457                   let s ≝ add_ticks1 s in
458                    set_program_counter ? s (addr_of addr2 s)
[712]459                  else
[936]460                   let s ≝ add_ticks2 s in
[712]461                    s
462            | JBC addr1 addr2 ⇒
[821]463                  let s ≝ set_arg_1 ? s addr1 false in
464                    if get_arg_1 ? s addr1 false then
[936]465                     let s ≝ add_ticks1 s in
466                      set_program_counter ? s (addr_of addr2 s)
[712]467                    else
[936]468                     let s ≝ add_ticks2 s in
[712]469                      s
470            | JZ addr ⇒
[821]471                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
[936]472                     let s ≝ add_ticks1 s in
473                      set_program_counter ? s (addr_of addr s)
[712]474                    else
[936]475                     let s ≝ add_ticks2 s in
[712]476                      s
477            | JNZ addr ⇒
[821]478                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
[936]479                     let s ≝ add_ticks1 s in
480                      set_program_counter ? s (addr_of addr s)
[712]481                    else
[936]482                     let s ≝ add_ticks2 s in
[712]483                      s
484            | CJNE addr1 addr2 ⇒
485                  match addr1 with
486                    [ inl l ⇒
[822]487                        let 〈addr1, addr2'〉 ≝ l in
[821]488                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
[822]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
[936]491                            let s ≝ add_ticks1 s in
[822]492                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
[821]493                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]494                          else
[936]495                            let s ≝ add_ticks2 s in
[821]496                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
[712]497                    | inr r' ⇒
[822]498                        let 〈addr1, addr2'〉 ≝ r' in
[821]499                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
[822]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
[936]502                            let s ≝ add_ticks1 s in
[822]503                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
[821]504                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]505                          else
[936]506                            let s ≝ add_ticks2 s in
[821]507                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
[712]508                    ]
509            | DJNZ addr1 addr2 ⇒
[821]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
[820]512                if ¬(eq_bv ? result (zero 8)) then
[936]513                 let s ≝ add_ticks1 s in
514                  set_program_counter ? s (addr_of addr2 s)
[820]515                else
[936]516                 let s ≝ add_ticks2 s in
[820]517                  s
[936]518        | NOP ⇒
519           let s ≝ add_ticks2 s in
520            s
[820]521        ].
522    try assumption
[856]523    try @I
[820]524    try (
525      @ (execute_1_technical … (subaddressing_modein …))
526      @ I
527    )
528qed.
529
[928]530definition execute_1_0: Status → instruction × Word × nat → Status ≝
531  λs,instr_pc_ticks.
532    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
[820]533    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
[821]534    let s ≝ set_program_counter ? s pc in
[820]535    let s ≝
536      match instr with
[936]537      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
[822]538        (λx. λs.
[820]539        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
[822]540        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
[820]541        | _ ⇒ λabsd. ⊥
542        ] (subaddressing_modein … x)) instr s
543      | ACALL addr ⇒
[936]544          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]545          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
546            [ ADDR11 a ⇒ λaddr11: True.
[821]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
[820]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
[821]557                set_program_counter ? s new_addr
[820]558            | _ ⇒ λother: False. ⊥
559            ] (subaddressing_modein … addr)
560        | LCALL addr ⇒
[936]561          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]562          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
563            [ ADDR16 a ⇒ λaddr16: True.
[821]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
[820]572            | _ ⇒ λother: False. ⊥
573            ] (subaddressing_modein … addr)
[757]574        | MOVC addr1 addr2 ⇒
[936]575          let s ≝ set_clock ? s (ticks + clock ? s) in
[757]576          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
577            [ ACC_DPTR ⇒ λacc_dptr: True.
[821]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
[757]580              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
[821]581              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
582                set_8051_sfr ? s SFR_ACC_A result
[757]583            | ACC_PC ⇒ λacc_pc: True.
[821]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
[757]586              (* DPM: Under specified: does the carry from PC incrementation affect the *)
587              (*      addition of the PC with the DPTR? At the moment, no.              *)
[821]588              let s ≝ set_program_counter ? s inc_pc in
[757]589              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
[821]590              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
591                set_8051_sfr ? s SFR_ACC_A result
[757]592            | _ ⇒ λother: False. ⊥
593            ] (subaddressing_modein … addr2)
[820]594        | JMP _ ⇒ (* DPM: always indirect_dptr *)
[936]595          let s ≝ set_clock ? s (ticks + clock ? s) in
[821]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
[820]598          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
[821]599          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
600            set_program_counter ? s new_pc
[820]601        | LJMP addr ⇒
[936]602          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]603          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
604            [ ADDR16 a ⇒ λaddr16: True.
[821]605                set_program_counter ? s a
[820]606            | _ ⇒ λother: False. ⊥
607            ] (subaddressing_modein … addr)
608        | SJMP addr ⇒
[936]609          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]610          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
611            [ RELATIVE r ⇒ λrelative: True.
[821]612                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
613                  set_program_counter ? s new_pc
[820]614            | _ ⇒ λother: False. ⊥
615            ] (subaddressing_modein … addr)
616        | AJMP addr ⇒
[936]617          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]618          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
619            [ ADDR11 a ⇒ λaddr11: True.
[821]620              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
[820]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
[821]625              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
626                set_program_counter ? s new_pc
[820]627            | _ ⇒ λother: False. ⊥
628            ] (subaddressing_modein … addr)
629      ]
[475]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
[928]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
[936]653definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
[822]654  λticks_of.
[820]655  λs.
[827]656  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
[825]657  let ticks ≝ ticks_of (program_counter ? s) in
[821]658  let s ≝ set_program_counter ? s pc in
[820]659  let s ≝
660    match instr with
[936]661    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
662    | Comment cmt ⇒
663       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
664        s
[820]665    | Cost cst ⇒ s
[936]666    | Jmp jmp ⇒
667       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
668        set_program_counter ? s (address_of_word_labels s jmp)
[820]669    | Call call ⇒
[936]670      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
[822]671      let a ≝ address_of_word_labels s call in
[821]672      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
673      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
674      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
675      let s ≝ write_at_stack_pointer ? s pc_bl 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 s ≝ write_at_stack_pointer ? s pc_bu in
679        set_program_counter ? s a
[910]680    | Mov dptr ident ⇒
[936]681      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
[910]682      let preamble ≝ \fst (code_memory ? s) in
683      let data_labels ≝ construct_datalabels preamble in
684        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
[820]685    ]
686  in
687    s.
688  normalize
689  @ I
690qed.
691
[475]692let rec execute (n: nat) (s: Status) on n: Status ≝
693  match n with
694    [ O ⇒ s
695    | S o ⇒ execute o (execute_1 s)
696    ].
[820]697
[936]698let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
[820]699  match n with
700    [ O ⇒ s
[822]701    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
[820]702    ].
Note: See TracBrowser for help on using the repository browser.