source: src/ASM/Interpret.ma @ 936

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

Ticks are now handled correctly everywhere and the main proof takes care of
them.

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