source: Deliverables/D3.1/C-semantics/cerco/Interpret.ma @ 533

Last change on this file since 533 was 475, checked in by mulligan, 9 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
Line 
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.