source: src/ASM/Interpret.ma @ 825

Last change on this file since 825 was 825, checked in by mulligan, 9 years ago

lots of refactoring, finally got something to prove

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