source: Deliverables/D4.1/Matita/new-matita-development/Interpret.ma @ 475

Last change on this file since 475 was 475, checked in by mulligan, 10 years ago

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

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