source: src/ASM/Interpret.ma @ 928

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

Technical splitting.

File size: 28.9 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: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
162  λA, M: Type[0].
163  λaddr_of: A → (PreStatus M) → Word.
164  λinstr: preinstruction A.
165  λs: PreStatus M.
166  match instr with
167        [ ADD addr1 addr2 ⇒
168            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
169                                                   (get_arg_8 ? s false addr2) false 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        | ADDC addr1 addr2 ⇒
176            let old_cy_flag ≝ get_cy_flag ? s in
177            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
178                                                   (get_arg_8 ? s false addr2) old_cy_flag in
179            let cy_flag ≝ get_index' ? O ? flags in
180            let ac_flag ≝ get_index' ? 1 ? flags in
181            let ov_flag ≝ get_index' ? 2 ? flags in
182            let s ≝ set_arg_8 ? s ACC_A result in
183              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
184        | SUBB addr1 addr2 ⇒
185            let old_cy_flag ≝ get_cy_flag ? s in
186            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
187                                                   (get_arg_8 ? s false addr2) old_cy_flag in
188            let cy_flag ≝ get_index' ? O ? flags in
189            let ac_flag ≝ get_index' ? 1 ? flags in
190            let ov_flag ≝ get_index' ? 2 ? flags in
191            let s ≝ set_arg_8 ? s ACC_A result in
192              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
193        | ANL addr ⇒
194          match addr with
195            [ inl l ⇒
196              match l with
197                [ inl l' ⇒
198                  let 〈addr1, addr2〉 ≝ l' in
199                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
200                    set_arg_8 ? s addr1 and_val
201                | inr r ⇒
202                  let 〈addr1, addr2〉 ≝ r in
203                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
204                    set_arg_8 ? s addr1 and_val
205                ]
206            | inr r ⇒
207              let 〈addr1, addr2〉 ≝ r in
208              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
209                set_flags ? s and_val (None ?) (get_ov_flag ? s)
210            ]
211        | ORL addr ⇒
212          match addr with
213            [ inl l ⇒
214              match l with
215                [ inl l' ⇒
216                  let 〈addr1, addr2〉 ≝ l' in
217                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
218                    set_arg_8 ? s addr1 or_val
219                | inr r ⇒
220                  let 〈addr1, addr2〉 ≝ r in
221                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
222                    set_arg_8 ? s addr1 or_val
223                ]
224            | inr r ⇒
225              let 〈addr1, addr2〉 ≝ r in
226              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
227                set_flags ? s or_val (None ?) (get_ov_flag ? s)
228            ]
229        | XRL addr ⇒
230          match addr with
231            [ inl l' ⇒
232              let 〈addr1, addr2〉 ≝ l' in
233              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
234                set_arg_8 ? s addr1 xor_val
235            | inr r ⇒
236              let 〈addr1, addr2〉 ≝ r in
237              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
238                set_arg_8 ? s addr1 xor_val
239            ]
240        | INC addr ⇒
241            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
242                                                           registr;
243                                                           direct;
244                                                           indirect;
245                                                           dptr ]] x) → ? with
246              [ ACC_A ⇒ λacc_a: True.
247                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
248                  set_arg_8 ? s ACC_A result
249              | REGISTER r ⇒ λregister: True.
250                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
251                  set_arg_8 ? s (REGISTER r) result
252              | DIRECT d ⇒ λdirect: True.
253                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
254                  set_arg_8 ? s (DIRECT d) result
255              | INDIRECT i ⇒ λindirect: True.
256                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
257                  set_arg_8 ? s (INDIRECT i) result
258              | DPTR ⇒ λdptr: True.
259                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
260                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
261                let s ≝ set_8051_sfr ? s SFR_DPL bl in
262                  set_8051_sfr ? s SFR_DPH bu
263              | _ ⇒ λother: False. ⊥
264              ] (subaddressing_modein … addr)
265        | DEC addr ⇒
266           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
267             set_arg_8 ? s addr result
268        | MUL addr1 addr2 ⇒
269           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
270           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
271           let product ≝ acc_a_nat * acc_b_nat in
272           let ov_flag ≝ product ≥ 256 in
273           let low ≝ bitvector_of_nat 8 (product mod 256) in
274           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
275           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
276             set_8051_sfr ? s SFR_ACC_B high
277        | DIV addr1 addr2 ⇒
278           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
279           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
280             match acc_b_nat with
281               [ O ⇒ set_flags ? s false (None Bit) true
282               | S o ⇒
283                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
284                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
285                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
286                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
287                   set_flags ? s false (None Bit) false
288               ]
289        | DA addr ⇒
290            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
291              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
292                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
293                let cy_flag ≝ get_index' ? O ? flags in
294                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
295                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
296                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
297                    let new_acc ≝ nu @@ acc_nl' in
298                    let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
299                      set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
300                  else
301                    s
302              else
303                s
304        | CLR addr ⇒
305          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
306            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
307            | CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
308            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
309            | _ ⇒ λother: False. ⊥
310            ] (subaddressing_modein … addr)
311        | CPL addr ⇒
312          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
313            [ ACC_A ⇒ λacc_a: True.
314                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
315                let new_acc ≝ negation_bv ? old_acc in
316                  set_8051_sfr ? s SFR_ACC_A new_acc
317            | CARRY ⇒ λcarry: True.
318                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
319                let new_cy_flag ≝ ¬old_cy_flag in
320                  set_arg_1 ? s CARRY new_cy_flag
321            | BIT_ADDR b ⇒ λbit_addr: True.
322                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
323                let new_bit ≝ ¬old_bit in
324                  set_arg_1 ? s (BIT_ADDR b) new_bit
325            | _ ⇒ λother: False. ?
326            ] (subaddressing_modein … addr)
327        | SETB b ⇒ set_arg_1 ? s b false
328        | RL _ ⇒ (* DPM: always ACC_A *)
329            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
330            let new_acc ≝ rotate_left … 1 old_acc in
331              set_8051_sfr ? s SFR_ACC_A new_acc
332        | RR _ ⇒ (* DPM: always ACC_A *)
333            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
334            let new_acc ≝ rotate_right … 1 old_acc in
335              set_8051_sfr ? s SFR_ACC_A new_acc
336        | RLC _ ⇒ (* DPM: always ACC_A *)
337            let old_cy_flag ≝ get_cy_flag ? s in
338            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
339            let new_cy_flag ≝ get_index' ? O ? old_acc in
340            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
341            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
342              set_8051_sfr ? s SFR_ACC_A new_acc
343        | RRC _ ⇒ (* DPM: always ACC_A *)
344            let old_cy_flag ≝ get_cy_flag ? s in
345            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
346            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
347            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
348            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
349              set_8051_sfr ? s SFR_ACC_A new_acc
350        | SWAP _ ⇒ (* DPM: always ACC_A *)
351            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
352            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
353            let new_acc ≝ nl @@ nu in
354              set_8051_sfr ? s SFR_ACC_A new_acc
355        | PUSH addr ⇒
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 contents ≝ read_at_stack_pointer ? s in
365            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
366            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
367              set_arg_8 ? s addr contents
368        | XCH addr1 addr2 ⇒
369            let old_addr ≝ get_arg_8 ? s false addr2 in
370            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
371            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
372              set_arg_8 ? s addr2 old_acc
373        | XCHD addr1 addr2 ⇒
374            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
375            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
376            let new_acc ≝ acc_nu @@ arg_nl in
377            let new_arg ≝ arg_nu @@ acc_nl in
378            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
379              set_arg_8 ? s addr2 new_arg
380        | RET ⇒
381            let high_bits ≝ read_at_stack_pointer ? s in
382            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
383            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
384            let low_bits ≝ read_at_stack_pointer ? s in
385            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
386            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
387            let new_pc ≝ high_bits @@ low_bits in
388              set_program_counter ? s new_pc
389        | RETI ⇒
390            let high_bits ≝ read_at_stack_pointer ? s in
391            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
392            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
393            let low_bits ≝ read_at_stack_pointer ? s in
394            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
395            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
396            let new_pc ≝ high_bits @@ low_bits in
397              set_program_counter ? s new_pc
398        | MOVX addr ⇒
399          (* DPM: only copies --- doesn't affect I/O *)
400          match addr with
401            [ inl l ⇒
402              let 〈addr1, addr2〉 ≝ l in
403                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
404            | inr r ⇒
405              let 〈addr1, addr2〉 ≝ r in
406                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
407            ]
408        | MOV addr ⇒
409          match addr with
410            [ inl l ⇒
411              match l with
412                [ inl l' ⇒
413                  match l' with
414                    [ inl l'' ⇒
415                      match l'' with
416                        [ inl l''' ⇒
417                          match l''' with
418                            [ inl l'''' ⇒
419                              let 〈addr1, addr2〉 ≝ l'''' in
420                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
421                            | inr r'''' ⇒
422                              let 〈addr1, addr2〉 ≝ r'''' in
423                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
424                            ]
425                        | inr r''' ⇒
426                          let 〈addr1, addr2〉 ≝ r''' in
427                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
428                        ]
429                    | inr r'' ⇒
430                      let 〈addr1, addr2〉 ≝ r'' in
431                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
432                    ]
433                | inr r ⇒
434                  let 〈addr1, addr2〉 ≝ r in
435                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
436                ]
437            | inr r ⇒
438              let 〈addr1, addr2〉 ≝ r in
439                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
440            ]
441          | JC addr ⇒
442                  if get_cy_flag ? s then
443                      set_program_counter ? s (addr_of addr s)
444                  else
445                    s
446            | JNC addr ⇒
447                  if ¬(get_cy_flag ? s) then
448                      set_program_counter ? s (addr_of addr s)
449                  else
450                    s
451            | JB addr1 addr2 ⇒
452                  if get_arg_1 ? s addr1 false then
453                      set_program_counter ? s (addr_of addr2 s)
454                  else
455                    s
456            | JNB addr1 addr2 ⇒
457                  if ¬(get_arg_1 ? s addr1 false) then
458                      set_program_counter ? s (addr_of addr2 s)
459                  else
460                    s
461            | JBC addr1 addr2 ⇒
462                  let s ≝ set_arg_1 ? s addr1 false in
463                    if get_arg_1 ? s addr1 false then
464                        set_program_counter ? s (addr_of addr2 s)
465                    else
466                      s
467            | JZ addr ⇒
468                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
469                        set_program_counter ? s (addr_of addr s)
470                    else
471                      s
472            | JNZ addr ⇒
473                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
474                        set_program_counter ? s (addr_of addr s)
475                    else
476                      s
477            | CJNE addr1 addr2 ⇒
478                  match addr1 with
479                    [ inl l ⇒
480                        let 〈addr1, addr2'〉 ≝ l in
481                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
482                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
483                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
484                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
485                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
486                          else
487                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
488                    | inr r' ⇒
489                        let 〈addr1, addr2'〉 ≝ r' in
490                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
491                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
492                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
493                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
494                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
495                          else
496                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
497                    ]
498            | DJNZ addr1 addr2 ⇒
499              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
500              let s ≝ set_arg_8 ? s addr1 result in
501                if ¬(eq_bv ? result (zero 8)) then
502                    set_program_counter ? s (addr_of addr2 s)
503                else
504                  s
505        | NOP ⇒ s
506        ].
507    try assumption
508    try @I
509    try (
510      @ (execute_1_technical … (subaddressing_modein …))
511      @ I
512    )
513qed.
514
515definition execute_1_0: Status → instruction × Word × nat → Status ≝
516  λs,instr_pc_ticks.
517    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
518    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
519    let s ≝ set_clock ? s (clock ? s + ticks) in
520    let s ≝ set_program_counter ? s pc in
521    let s ≝
522      match instr with
523      [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?
524        (λx. λs.
525        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
526        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
527        | _ ⇒ λabsd. ⊥
528        ] (subaddressing_modein … x)) instr s
529      | ACALL addr ⇒
530          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
531            [ ADDR11 a ⇒ λaddr11: True.
532              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
533              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
534              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
535              let s ≝ write_at_stack_pointer ? s pc_bl in
536              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
537              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
538              let s ≝ write_at_stack_pointer ? s pc_bu in
539              let 〈thr, eig〉 ≝ split ? 3 8 a in
540              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
541              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
542                set_program_counter ? s new_addr
543            | _ ⇒ λother: False. ⊥
544            ] (subaddressing_modein … addr)
545        | LCALL addr ⇒
546          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
547            [ ADDR16 a ⇒ λaddr16: True.
548              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
549              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
550              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
551              let s ≝ write_at_stack_pointer ? s pc_bl in
552              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
553              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
554              let s ≝ write_at_stack_pointer ? s pc_bu in
555                set_program_counter ? s a
556            | _ ⇒ λother: False. ⊥
557            ] (subaddressing_modein … addr)
558        | MOVC addr1 addr2 ⇒
559          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
560            [ ACC_DPTR ⇒ λacc_dptr: True.
561              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
562              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
563              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
564              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
565                set_8051_sfr ? s SFR_ACC_A result
566            | ACC_PC ⇒ λacc_pc: True.
567              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
568              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
569              (* DPM: Under specified: does the carry from PC incrementation affect the *)
570              (*      addition of the PC with the DPTR? At the moment, no.              *)
571              let s ≝ set_program_counter ? s inc_pc in
572              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
573              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
574                set_8051_sfr ? s SFR_ACC_A result
575            | _ ⇒ λother: False. ⊥
576            ] (subaddressing_modein … addr2)
577        | JMP _ ⇒ (* DPM: always indirect_dptr *)
578          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
579          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
580          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
581          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
582            set_program_counter ? s new_pc
583        | LJMP addr ⇒
584          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
585            [ ADDR16 a ⇒ λaddr16: True.
586                set_program_counter ? s a
587            | _ ⇒ λother: False. ⊥
588            ] (subaddressing_modein … addr)
589        | SJMP addr ⇒
590          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
591            [ RELATIVE r ⇒ λrelative: True.
592                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
593                  set_program_counter ? s new_pc
594            | _ ⇒ λother: False. ⊥
595            ] (subaddressing_modein … addr)
596        | AJMP addr ⇒
597          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
598            [ ADDR11 a ⇒ λaddr11: True.
599              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
600              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
601              let bit ≝ get_index' ? O ? nl in
602              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
603              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
604              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
605                set_program_counter ? s new_pc
606            | _ ⇒ λother: False. ⊥
607            ] (subaddressing_modein … addr)
608      ]
609    in
610      s.
611    try assumption
612    try (
613      normalize
614      repeat (@ (le_S_S))
615      @ (le_O_n)
616    )
617    try (
618      @ (execute_1_technical … (subaddressing_modein …))
619      @ I
620    )
621    try (
622      normalize
623      @ I
624    )     
625qed.
626
627definition execute_1: Status → Status ≝
628  λs: Status.
629    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
630     execute_1_0 s instr_pc_ticks.
631
632let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
633  match l with
634  [ nil ⇒ ?
635  | cons hd tl ⇒
636    if pred hd then
637      acc
638    else
639      index_of_internal A pred tl (S acc)
640  ].
641  cases not_implemented.
642qed.
643
644definition index_of ≝
645  λA.
646  λeq.
647  λl.
648    index_of_internal A eq l 0.
649
650definition instruction_matches_identifier ≝
651  λy: Identifier.
652  λx: labelled_instruction.
653    match \fst x with
654    [ None ⇒ false
655    | Some x ⇒ eq_bv ? x y
656    ].
657
658definition address_of_word_labels_code_mem ≝
659  λcode_mem.
660  λid: Identifier.
661    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
662
663definition address_of_word_labels ≝
664  λps: PseudoStatus.
665  λid: Identifier.
666    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
667
668definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
669  λticks_of.
670  λs.
671  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
672  let ticks ≝ ticks_of (program_counter ? s) in
673  let s ≝ set_clock ? s (clock ? s + ticks) in
674  let s ≝ set_program_counter ? s pc in
675  let s ≝
676    match instr with
677    [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
678    | Comment cmt ⇒ s
679    | Cost cst ⇒ s
680    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
681    | Call call ⇒
682      let a ≝ address_of_word_labels s call in
683      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
684      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
685      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
686      let s ≝ write_at_stack_pointer ? s pc_bl in
687      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
688      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
689      let s ≝ write_at_stack_pointer ? s pc_bu in
690        set_program_counter ? s a
691    | Mov dptr ident ⇒
692      let preamble ≝ \fst (code_memory ? s) in
693      let data_labels ≝ construct_datalabels preamble in
694        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
695    ]
696  in
697    s.
698  normalize
699  @ I
700qed.
701
702let rec execute (n: nat) (s: Status) on n: Status ≝
703  match n with
704    [ O ⇒ s
705    | S o ⇒ execute o (execute_1 s)
706    ].
707
708let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat) (s: PseudoStatus) on n: PseudoStatus ≝
709  match n with
710    [ O ⇒ s
711    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
712    ].
Note: See TracBrowser for help on using the repository browser.