source: src/ASM/Interpret.ma @ 1526

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

Using Russell to prove some properties.

File size: 31.6 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
134definition execute_1_preinstruction:
135 ∀ticks: nat × nat.
136 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
137  ∀s:PreStatus M. Σs':PreStatus M. clock … s ≤ clock … s' ≝
138  λticks.
139  λA, M: Type[0].
140  λaddr_of: A → (PreStatus M) → Word.
141  λinstr: preinstruction A.
142  λs: PreStatus M.
143  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
144  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
145  match instr with
146        [ ADD addr1 addr2 ⇒
147            let s ≝ add_ticks1 s in
148            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
149                                                   (get_arg_8 ? s false addr2) false in
150            let cy_flag ≝ get_index' ? O  ? flags in
151            let ac_flag ≝ get_index' ? 1 ? flags in
152            let ov_flag ≝ get_index' ? 2 ? flags in
153            let s ≝ set_arg_8 ? s ACC_A result in
154              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
155        | ADDC addr1 addr2 ⇒
156            let s ≝ add_ticks1 s in
157            let old_cy_flag ≝ get_cy_flag ? s in
158            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
159                                                   (get_arg_8 ? s false addr2) old_cy_flag in
160            let cy_flag ≝ get_index' ? O ? flags in
161            let ac_flag ≝ get_index' ? 1 ? flags in
162            let ov_flag ≝ get_index' ? 2 ? flags in
163            let s ≝ set_arg_8 ? s ACC_A result in
164              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
165        | SUBB addr1 addr2 ⇒
166            let s ≝ add_ticks1 s in
167            let old_cy_flag ≝ get_cy_flag ? s in
168            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
169                                                   (get_arg_8 ? s false addr2) old_cy_flag in
170            let cy_flag ≝ get_index' ? O ? flags in
171            let ac_flag ≝ get_index' ? 1 ? flags in
172            let ov_flag ≝ get_index' ? 2 ? flags in
173            let s ≝ set_arg_8 ? s ACC_A result in
174              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
175        | ANL addr ⇒
176          let s ≝ add_ticks1 s in
177          match addr with
178            [ inl l ⇒
179              match l with
180                [ inl l' ⇒
181                  let 〈addr1, addr2〉 ≝ l' in
182                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
183                    set_arg_8 ? s addr1 and_val
184                | inr r ⇒
185                  let 〈addr1, addr2〉 ≝ r in
186                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
187                    set_arg_8 ? s addr1 and_val
188                ]
189            | inr r ⇒
190              let 〈addr1, addr2〉 ≝ r in
191              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
192                set_flags ? s and_val (None ?) (get_ov_flag ? s)
193            ]
194        | ORL addr ⇒
195          let s ≝ add_ticks1 s in
196          match addr with
197            [ inl l ⇒
198              match l with
199                [ inl l' ⇒
200                  let 〈addr1, addr2〉 ≝ l' in
201                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
202                    set_arg_8 ? s addr1 or_val
203                | inr r ⇒
204                  let 〈addr1, addr2〉 ≝ r in
205                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
206                    set_arg_8 ? s addr1 or_val
207                ]
208            | inr r ⇒
209              let 〈addr1, addr2〉 ≝ r in
210              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
211                set_flags ? s or_val (None ?) (get_ov_flag ? s)
212            ]
213        | XRL addr ⇒
214          let s ≝ add_ticks1 s in
215          match addr with
216            [ inl l' ⇒
217              let 〈addr1, addr2〉 ≝ l' in
218              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
219                set_arg_8 ? s addr1 xor_val
220            | inr r ⇒
221              let 〈addr1, addr2〉 ≝ r in
222              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
223                set_arg_8 ? s addr1 xor_val
224            ]
225        | INC addr ⇒
226            let s' ≝ add_ticks1 s in
227            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
228                                                           registr;
229                                                           direct;
230                                                           indirect;
231                                                           dptr ]] x) → Σs'.clock … s ≤ clock … s' with
232              [ ACC_A ⇒ λacc_a: True.
233                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
234                 eject … (set_arg_8 ? s' ACC_A result)
235              | REGISTER r ⇒ λregister: True.
236                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
237                 eject … (set_arg_8 ? s' (REGISTER r) result)
238              | DIRECT d ⇒ λdirect: True.
239                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
240                 eject … (set_arg_8 ? s' (DIRECT d) result)
241              | INDIRECT i ⇒ λindirect: True.
242                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
243                 eject … (set_arg_8 ? s' (INDIRECT i) result)
244              | DPTR ⇒ λdptr: True.
245                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
246                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
247                let s ≝ set_8051_sfr ? s' SFR_DPL bl in
248                  set_8051_sfr ? s' SFR_DPH bu
249              | _ ⇒ λother: False. ⊥
250              ] (subaddressing_modein … addr)
251        | DEC addr ⇒
252           let s ≝ add_ticks1 s in
253           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
254             set_arg_8 ? s addr result
255        | MUL addr1 addr2 ⇒
256           let s ≝ add_ticks1 s in
257           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
258           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
259           let product ≝ acc_a_nat * acc_b_nat in
260           let ov_flag ≝ product ≥ 256 in
261           let low ≝ bitvector_of_nat 8 (product mod 256) in
262           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
263           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
264             set_8051_sfr ? s SFR_ACC_B high
265        | DIV addr1 addr2 ⇒
266           let s ≝ add_ticks1 s in
267           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
268           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
269             match acc_b_nat with
270               [ O ⇒ set_flags ? s false (None Bit) true
271               | S o ⇒
272                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
273                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
274                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
275                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
276                   set_flags ? s false (None Bit) false
277               ]
278        | DA addr ⇒
279            let s ≝ add_ticks1 s in
280            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
281              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
282                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
283                let cy_flag ≝ get_index' ? O ? flags in
284                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
285                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
286                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
287                    let new_acc ≝ nu @@ acc_nl' in
288                    let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
289                      set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
290                  else
291                    s
292              else
293                s
294        | CLR addr ⇒
295          let s ≝ add_ticks1 s in
296          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
297            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
298            | CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
299            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
300            | _ ⇒ λother: False. ⊥
301            ] (subaddressing_modein … addr)
302        | CPL addr ⇒
303          let s ≝ add_ticks1 s in
304          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
305            [ ACC_A ⇒ λacc_a: True.
306                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
307                let new_acc ≝ negation_bv ? old_acc in
308                  set_8051_sfr ? s SFR_ACC_A new_acc
309            | CARRY ⇒ λcarry: True.
310                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
311                let new_cy_flag ≝ ¬old_cy_flag in
312                  set_arg_1 ? s CARRY new_cy_flag
313            | BIT_ADDR b ⇒ λbit_addr: True.
314                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
315                let new_bit ≝ ¬old_bit in
316                  set_arg_1 ? s (BIT_ADDR b) new_bit
317            | _ ⇒ λother: False. ?
318            ] (subaddressing_modein … addr)
319        | SETB b ⇒
320            let s ≝ add_ticks1 s in
321            set_arg_1 ? s b false
322        | RL _ ⇒ (* DPM: always ACC_A *)
323            let s ≝ add_ticks1 s in
324            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
325            let new_acc ≝ rotate_left … 1 old_acc in
326              set_8051_sfr ? s SFR_ACC_A new_acc
327        | RR _ ⇒ (* 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_right … 1 old_acc in
331              set_8051_sfr ? s SFR_ACC_A new_acc
332        | RLC _ ⇒ (* DPM: always ACC_A *)
333            let s ≝ add_ticks1 s in
334            let old_cy_flag ≝ get_cy_flag ? s in
335            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
336            let new_cy_flag ≝ get_index' ? O ? old_acc in
337            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
338            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
339              set_8051_sfr ? s SFR_ACC_A new_acc
340        | RRC _ ⇒ (* DPM: always ACC_A *)
341            let s ≝ add_ticks1 s in
342            let old_cy_flag ≝ get_cy_flag ? s in
343            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
344            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
345            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
346            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
347              set_8051_sfr ? s SFR_ACC_A new_acc
348        | SWAP _ ⇒ (* DPM: always ACC_A *)
349            let s ≝ add_ticks1 s in
350            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
351            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
352            let new_acc ≝ nl @@ nu in
353              set_8051_sfr ? s SFR_ACC_A new_acc
354        | PUSH addr ⇒
355            let s ≝ add_ticks1 s in
356            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
357              [ DIRECT d ⇒ λdirect: True.
358                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
359                let s ≝ set_8051_sfr ? s SFR_SP new_sp in
360                  write_at_stack_pointer ? s d
361              | _ ⇒ λother: False. ⊥
362              ] (subaddressing_modein … addr)
363        | POP addr ⇒
364            let s ≝ add_ticks1 s in
365            let contents ≝ read_at_stack_pointer ? s in
366            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
367            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
368              set_arg_8 ? s addr contents
369        | XCH addr1 addr2 ⇒
370            let s ≝ add_ticks1 s in
371            let old_addr ≝ get_arg_8 ? s false addr2 in
372            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
373            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
374              set_arg_8 ? s addr2 old_acc
375        | XCHD addr1 addr2 ⇒
376            let s ≝ add_ticks1 s in
377            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
378            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
379            let new_acc ≝ acc_nu @@ arg_nl in
380            let new_arg ≝ arg_nu @@ acc_nl in
381            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
382              set_arg_8 ? s addr2 new_arg
383        | RET ⇒
384            let s ≝ add_ticks1 s in
385            let high_bits ≝ read_at_stack_pointer ? s in
386            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
387            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
388            let low_bits ≝ read_at_stack_pointer ? s in
389            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
390            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
391            let new_pc ≝ high_bits @@ low_bits in
392              set_program_counter ? s new_pc
393        | RETI ⇒
394            let s ≝ add_ticks1 s in
395            let high_bits ≝ read_at_stack_pointer ? s in
396            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
397            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
398            let low_bits ≝ read_at_stack_pointer ? s in
399            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
400            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
401            let new_pc ≝ high_bits @@ low_bits in
402              set_program_counter ? s new_pc
403        | MOVX addr ⇒
404          let s ≝ add_ticks1 s in
405          (* DPM: only copies --- doesn't affect I/O *)
406          match addr with
407            [ inl l ⇒
408              let 〈addr1, addr2〉 ≝ l in
409                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
410            | inr r ⇒
411              let 〈addr1, addr2〉 ≝ r in
412                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
413            ]
414        | MOV addr ⇒
415          let s ≝ add_ticks1 s in
416          match addr with
417            [ inl l ⇒
418              match l with
419                [ inl l' ⇒
420                  match l' with
421                    [ inl l'' ⇒
422                      match l'' with
423                        [ inl l''' ⇒
424                          match l''' with
425                            [ inl l'''' ⇒
426                              let 〈addr1, addr2〉 ≝ l'''' in
427                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
428                            | inr r'''' ⇒
429                              let 〈addr1, addr2〉 ≝ r'''' in
430                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
431                            ]
432                        | inr r''' ⇒
433                          let 〈addr1, addr2〉 ≝ r''' in
434                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
435                        ]
436                    | inr r'' ⇒
437                      let 〈addr1, addr2〉 ≝ r'' in
438                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
439                    ]
440                | inr r ⇒
441                  let 〈addr1, addr2〉 ≝ r in
442                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
443                ]
444            | inr r ⇒
445              let 〈addr1, addr2〉 ≝ r in
446                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
447            ]
448          | JC addr ⇒
449                  if get_cy_flag ? s then
450                   let s ≝ add_ticks1 s in
451                    set_program_counter ? s (addr_of addr s)
452                  else
453                   let s ≝ add_ticks2 s in
454                    s
455            | JNC addr ⇒
456                  if ¬(get_cy_flag ? s) then
457                   let s ≝ add_ticks1 s in
458                    set_program_counter ? s (addr_of addr s)
459                  else
460                   let s ≝ add_ticks2 s in
461                    s
462            | JB addr1 addr2 ⇒
463                  if get_arg_1 ? s addr1 false then
464                   let s ≝ add_ticks1 s in
465                    set_program_counter ? s (addr_of addr2 s)
466                  else
467                   let s ≝ add_ticks2 s in
468                    s
469            | JNB addr1 addr2 ⇒
470                  if ¬(get_arg_1 ? s addr1 false) then
471                   let s ≝ add_ticks1 s in
472                    set_program_counter ? s (addr_of addr2 s)
473                  else
474                   let s ≝ add_ticks2 s in
475                    s
476            | JBC addr1 addr2 ⇒
477                  let s ≝ set_arg_1 ? s addr1 false in
478                    if get_arg_1 ? s addr1 false then
479                     let s ≝ add_ticks1 s in
480                      set_program_counter ? s (addr_of addr2 s)
481                    else
482                     let s ≝ add_ticks2 s in
483                      s
484            | JZ addr ⇒
485                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
486                     let s ≝ add_ticks1 s in
487                      set_program_counter ? s (addr_of addr s)
488                    else
489                     let s ≝ add_ticks2 s in
490                      s
491            | JNZ addr ⇒
492                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
493                     let s ≝ add_ticks1 s in
494                      set_program_counter ? s (addr_of addr s)
495                    else
496                     let s ≝ add_ticks2 s in
497                      s
498            | CJNE addr1 addr2 ⇒
499                  match addr1 with
500                    [ inl l ⇒
501                        let 〈addr1, addr2'〉 ≝ l in
502                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
503                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
504                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
505                            let s ≝ add_ticks1 s in
506                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
507                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
508                          else
509                            let s ≝ add_ticks2 s in
510                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
511                    | inr r' ⇒
512                        let 〈addr1, addr2'〉 ≝ r' in
513                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
514                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
515                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
516                            let s ≝ add_ticks1 s in
517                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
518                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
519                          else
520                            let s ≝ add_ticks2 s in
521                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
522                    ]
523            | DJNZ addr1 addr2 ⇒
524              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
525              let s ≝ set_arg_8 ? s addr1 result in
526                if ¬(eq_bv ? result (zero 8)) then
527                 let s ≝ add_ticks1 s in
528                  set_program_counter ? s (addr_of addr2 s)
529                else
530                 let s ≝ add_ticks2 s in
531                  s
532        | NOP ⇒
533           let s ≝ add_ticks2 s in
534            s
535        ]. (*67s*)
536    try assumption (*180s*)
537    try % (*41s*)
538    try (
539      @ (execute_1_technical … (subaddressing_modein …))
540      @ I
541    ) (*132s*)
542 [(*1:/by/,2,3: /by/*)
543 |4:
544 |6,7,8,10,11,12,13,14,15: /by/ (*56s*)
545 |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*73s*)
546 |33,35,39,41,43,54,55,56: /by/ (*48s*)
547 |
548 (* 31,32,34,36,44,48 facili *)
549 (* 4,5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
550qed.
551
552include "ASM/JMCoercions.ma".
553
554definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
555  λs,instr_pc_ticks.
556    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
557    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
558    let s ≝ set_program_counter ? s pc in
559    let s ≝
560      match instr with
561      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
562        (λx. λs.
563        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
564        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
565        | _ ⇒ λabsd. ⊥
566        ] (subaddressing_modein … x)) instr s
567      | _ ⇒ ?
568      ] in 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    in
664      s.
665    try assumption
666    try (
667      normalize
668      repeat (@ (le_S_S))
669      @ (le_O_n)
670    )
671    try (
672      @ (execute_1_technical … (subaddressing_modein …))
673      @ I
674    )
675    try (
676      normalize
677      @ I
678    )     
679qed.
680
681definition execute_1: Status → Status ≝
682  λs: Status.
683    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
684     execute_1_0 s instr_pc_ticks.
685
686definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
687  λticks,s,instr,pc.
688  let s ≝ set_program_counter ? s pc in
689  let s ≝
690    match instr with
691    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
692    | Comment cmt ⇒
693       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
694        s
695    | Cost cst ⇒ s
696    | Jmp jmp ⇒
697       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
698        set_program_counter ? s (address_of_word_labels s jmp)
699    | Call call ⇒
700      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
701      let a ≝ address_of_word_labels s call in
702      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
703      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
704      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
705      let s ≝ write_at_stack_pointer ? s pc_bl in
706      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
707      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
708      let s ≝ write_at_stack_pointer ? s pc_bu in
709        set_program_counter ? s a
710    | Mov dptr ident ⇒
711      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
712      let preamble ≝ \fst (code_memory ? s) in
713      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
714        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
715    ]
716  in
717    s.
718  normalize
719  @ I
720qed.
721
722definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
723  λticks_of,s.
724  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
725  let ticks ≝ ticks_of (program_counter ? s) in
726   execute_1_pseudo_instruction0 ticks s instr pc.
727
728let rec execute (n: nat) (s: Status) on n: Status ≝
729  match n with
730    [ O ⇒ s
731    | S o ⇒ execute o (execute_1 s)
732    ].
733
734let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
735  match n with
736    [ O ⇒ s
737    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
738    ].
Note: See TracBrowser for help on using the repository browser.