source: src/ASM/Interpret.ma @ 981

Last change on this file since 981 was 936, checked in by sacerdot, 10 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.