source: src/ASM/Interpret.ma @ 1527

Last change on this file since 1527 was 1527, checked in by sacerdot, 8 years ago

More on Russell.

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