source: Deliverables/D4.1/Matita/Interpret.ma @ 470

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

Finished moving development over to standard library.

File size: 28.0 KB
Line 
1include "Status.ma".
2include "Fetch.ma".
3
4ndefinition 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  nnormalize;
9  nrepeat (napply (le_S_S ?));
10  napply (le_O_n);
11nqed.
12   
13nlemma inclusive_disjunction_true:
14  ∀b, c: bool.
15    (orb b c) = true → b = true ∨ c = true.
16  #b c;
17  nelim b
18    [ nnormalize; #H; napply or_introl; @;
19  ##| nnormalize; /2/;
20  ##]
21nqed.
22
23nlemma conjunction_true:
24  ∀b, c: bool.
25    andb b c = true → b = true ∧ c = true.
26  #b c;
27  nelim b; nnormalize
28    [ /2/ | #K; ndestruct ]
29nqed.
30
31nlemma eq_true_false: false=true → False.
32 #K; ndestruct.
33nqed.
34
35nlemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
36 #a; #b; ncases a; ncases b; nnormalize; //; #K; ncases (eq_true_false K).
37nqed.
38
39nlemma inclusive_disjunction_b_true: ∀b. orb b true = true.
40 #b; ncases b; @.
41nqed.
42
43nlemma is_a_to_mem_to_is_in:
44 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
45 #he a m q; nelim q
46  [ nnormalize; #_; #K; nassumption
47  | #m' t q' II H1 H2; nnormalize;
48    nchange in H2:(??%?) with (orb ??);
49    ncases (inclusive_disjunction_true … H2)
50     [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @
51     | #K; nrewrite > II; ntry nassumption; ncases (is_a t a); nnormalize; @ ]
52nqed.
53
54nlemma execute_1_technical:
55  ∀n,m: nat.
56  ∀v: Vector addressing_mode_tag (S n).
57  ∀q: Vector addressing_mode_tag (S m).
58  ∀a: addressing_mode.
59    bool_to_Prop (is_in ? v a) →
60    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
61    bool_to_Prop (is_in ? q a).
62 #n m v q a; nelim v
63  [ nnormalize; #K; ncases K
64  | #n' he tl II;
65    nwhd in ⊢ (% → ? → ?);
66    nlapply (refl … (is_in … (he:::tl) a));
67    ncases (is_in … (he:::tl) a) in ⊢ (???% → %)
68     [ #K; #_; nnormalize in K; nwhd in ⊢ (% → ?);
69       nlapply (refl … (subvector_with … eq_a (he:::tl) q));
70       ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
71       [ #K1; #_;
72        nchange in K1 with ((andb ? (subvector_with …)) = true);
73        ncases (conjunction_true … K1); #K3; #K4;
74        ncases (inclusive_disjunction_true … K); #K2
75         [ nrewrite > (is_a_to_mem_to_is_in … K2 K3); @
76         | napply II [ nrewrite > K2; @ | nrewrite > K4; @]##]
77     ##| #K1 K2; nnormalize in K2; ncases K2 ]
78   ##| #K1 K2; nnormalize in K2; ncases K2 ]
79nqed.
80   
81ndefinition execute_1: Status → Status ≝
82  λs.
83    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
84    let 〈 instr, pc 〉 ≝ 〈 fst … instr_pc, snd … instr_pc 〉 in
85    let s ≝ set_clock s (clock s + ticks) in
86    let s ≝ set_program_counter s pc in
87    let s ≝
88      match instr with
89        [ ADD addr1 addr2 ⇒
90            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
91                                                   (get_arg_8 s false addr2) false in
92            let cy_flag ≝ get_index' ? O  ? flags in
93            let ac_flag ≝ get_index' ? 1 ? flags in
94            let ov_flag ≝ get_index' ? 2 ? flags in
95            let s ≝ set_arg_8 s ACC_A result in
96              set_flags s cy_flag (Some Bit ac_flag) ov_flag
97        | ADDC addr1 addr2 ⇒
98            let old_cy_flag ≝ get_cy_flag s in
99            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
100                                                   (get_arg_8 s false addr2) old_cy_flag in
101            let cy_flag ≝ get_index' ? O ? flags in
102            let ac_flag ≝ get_index' ? 1 ? flags in
103            let ov_flag ≝ get_index' ? 2 ? flags in
104            let s ≝ set_arg_8 s ACC_A result in
105              set_flags s cy_flag (Some Bit ac_flag) ov_flag
106        | SUBB addr1 addr2 ⇒
107            let old_cy_flag ≝ get_cy_flag s in
108            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
109                                                   (get_arg_8 s false addr2) old_cy_flag in
110            let cy_flag ≝ get_index' ? O ? flags in
111            let ac_flag ≝ get_index' ? 1 ? flags in
112            let ov_flag ≝ get_index' ? 2 ? flags in
113            let s ≝ set_arg_8 s ACC_A result in
114              set_flags s cy_flag (Some Bit ac_flag) ov_flag
115        | ANL addr ⇒
116          match addr with
117            [ inl l ⇒
118              match l with
119                [ inl l' ⇒
120                  let 〈addr1, addr2〉 ≝ l' in
121                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
122                    set_arg_8 s addr1 and_val
123                | inr r ⇒
124                  let 〈addr1, addr2〉 ≝ r in
125                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
126                    set_arg_8 s addr1 and_val
127                ]
128            | inr r ⇒
129              let 〈addr1, addr2〉 ≝ r in
130              let and_val ≝ (get_cy_flag s) ∧ (get_arg_1 s addr2 true) in
131                set_flags s and_val (None ?) (get_ov_flag s)
132            ]
133        | ORL addr ⇒
134          match addr with
135            [ inl l ⇒
136              match l with
137                [ inl l' ⇒
138                  let 〈addr1, addr2〉 ≝ l' in
139                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
140                    set_arg_8 s addr1 or_val
141                | inr r ⇒
142                  let 〈addr1, addr2〉 ≝ r in
143                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
144                    set_arg_8 s addr1 or_val
145                ]
146            | inr r ⇒
147              let 〈addr1, addr2〉 ≝ r in
148              let or_val ≝ (get_cy_flag s) ∨ (get_arg_1 s addr2 true) in
149                set_flags s or_val (None ?) (get_ov_flag s)
150            ]
151        | XRL addr ⇒
152          match addr with
153            [ inl l' ⇒
154              let 〈addr1, addr2〉 ≝ l' in
155              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
156                set_arg_8 s addr1 xor_val
157            | inr r ⇒
158              let 〈addr1, addr2〉 ≝ r in
159              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
160                set_arg_8 s addr1 xor_val
161            ]
162        | INC addr ⇒
163            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
164                                                           register;
165                                                           direct;
166                                                           indirect;
167                                                           dptr ]] x) → ? with
168              [ ACC_A ⇒ λacc_a: True.
169                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in
170                  set_arg_8 s ACC_A result
171              | REGISTER r ⇒ λregister: True.
172                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in
173                  set_arg_8 s (REGISTER r) result
174              | DIRECT d ⇒ λdirect: True.
175                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in
176                  set_arg_8 s (DIRECT d) result
177              | INDIRECT i ⇒ λindirect: True.
178                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in
179                  set_arg_8 s (INDIRECT i) result
180              | DPTR ⇒ λdptr: True.
181                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in
182                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in
183                let s ≝ set_8051_sfr s SFR_DPL bl in
184                  set_8051_sfr s SFR_DPH bu
185              | _ ⇒ λother: False. ⊥
186              ] (subaddressing_modein … addr)
187        | DEC addr ⇒
188           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in
189             set_arg_8 s addr result
190        | MUL addr1 addr2 ⇒
191           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
192           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
193           let product ≝ acc_a_nat * acc_b_nat in
194           let ov_flag ≝ product ≥ 256 in
195           let low ≝ bitvector_of_nat 8 (product mod 256) in
196           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
197           let s ≝ set_8051_sfr s SFR_ACC_A low in
198             set_8051_sfr s SFR_ACC_B high
199        | DIV addr1 addr2 ⇒
200           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
201           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
202             match acc_b_nat with
203               [ O ⇒ set_flags s false (None Bit) true
204               | S o ⇒
205                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
206                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
207                 let s ≝ set_8051_sfr s SFR_ACC_A q in
208                 let s ≝ set_8051_sfr s SFR_ACC_B r in
209                   set_flags s false (None Bit) false
210               ]
211        | DA addr ⇒
212            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in
213              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then
214                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in
215                let cy_flag ≝ get_index' ? O ? flags in
216                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
217                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
218                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
219                    let new_acc ≝ nu @@ acc_nl' in
220                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
221                      set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flag s)
222                  else
223                    s
224              else
225                s
226        | CLR addr ⇒
227          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
228            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8)
229            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
230            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
231            | _ ⇒ λother: False. ⊥
232            ] (subaddressing_modein … addr)
233        | CPL addr ⇒
234          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
235            [ ACC_A ⇒ λacc_a: True.
236                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
237                let new_acc ≝ negation_bv ? old_acc in
238                  set_8051_sfr s SFR_ACC_A new_acc
239            | CARRY ⇒ λcarry: True.
240                let old_cy_flag ≝ get_arg_1 s CARRY true in
241                let new_cy_flag ≝ ¬old_cy_flag in
242                  set_arg_1 s CARRY new_cy_flag
243            | BIT_ADDR b ⇒ λbit_addr: True.
244                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
245                let new_bit ≝ ¬old_bit in
246                  set_arg_1 s (BIT_ADDR b) new_bit
247            | _ ⇒ λother: False. ?
248            ] (subaddressing_modein … addr)
249        | SETB b ⇒ set_arg_1 s b false
250        | RL _ ⇒ (* DPM: always ACC_A *)
251            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
252            let new_acc ≝ rotate_left … 1 old_acc in
253              set_8051_sfr s SFR_ACC_A new_acc
254        | RR _ ⇒ (* DPM: always ACC_A *)
255            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
256            let new_acc ≝ rotate_right … 1 old_acc in
257              set_8051_sfr s SFR_ACC_A new_acc
258        | RLC _ ⇒ (* DPM: always ACC_A *)
259            let old_cy_flag ≝ get_cy_flag s in
260            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
261            let new_cy_flag ≝ get_index' ? O ? old_acc in
262            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
263            let s ≝ set_arg_1 s CARRY new_cy_flag in
264              set_8051_sfr s SFR_ACC_A new_acc
265        | RRC _ ⇒ (* DPM: always ACC_A *)
266            let old_cy_flag ≝ get_cy_flag s in
267            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
268            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
269            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
270            let s ≝ set_arg_1 s CARRY new_cy_flag in
271              set_8051_sfr s SFR_ACC_A new_acc
272        | SWAP _ ⇒ (* DPM: always ACC_A *)
273            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
274            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
275            let new_acc ≝ nl @@ nu in
276              set_8051_sfr s SFR_ACC_A new_acc
277        | PUSH addr ⇒
278            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
279              [ DIRECT d ⇒ λdirect: True.
280                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
281                let s ≝ set_8051_sfr s SFR_SP new_sp in
282                  write_at_stack_pointer s d
283              | _ ⇒ λother: False. ⊥
284              ] (subaddressing_modein … addr)
285        | POP addr ⇒
286            let contents ≝ read_at_stack_pointer s in
287            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
288            let s ≝ set_8051_sfr s SFR_SP new_sp in
289              set_arg_8 s addr contents
290        | XCH addr1 addr2 ⇒
291            let old_addr ≝ get_arg_8 s false addr2 in
292            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
293            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
294              set_arg_8 s addr2 old_acc
295        | XCHD addr1 addr2 ⇒
296            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in
297            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in
298            let new_acc ≝ acc_nu @@ arg_nl in
299            let new_arg ≝ arg_nu @@ acc_nl in
300            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
301              set_arg_8 s addr2 new_arg
302        | RET ⇒
303            let high_bits ≝ read_at_stack_pointer s in
304            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
305            let s ≝ set_8051_sfr s SFR_SP new_sp in
306            let low_bits ≝ read_at_stack_pointer s in
307            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
308            let s ≝ set_8051_sfr s SFR_SP new_sp in
309            let new_pc ≝ high_bits @@ low_bits in
310              set_program_counter s new_pc
311        | RETI ⇒
312            let high_bits ≝ read_at_stack_pointer s in
313            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
314            let s ≝ set_8051_sfr s SFR_SP new_sp in
315            let low_bits ≝ read_at_stack_pointer s in
316            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
317            let s ≝ set_8051_sfr s SFR_SP new_sp in
318            let new_pc ≝ high_bits @@ low_bits in
319              set_program_counter s new_pc
320        | Jump j ⇒
321          match j with
322            [ JC addr ⇒
323              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
324                [ RELATIVE r ⇒ λrel: True.
325                  if get_cy_flag s then
326                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
327                      set_program_counter s new_pc
328                  else
329                    s
330                | _ ⇒ λother: False. ⊥
331                ] (subaddressing_modein … addr)
332            | JNC addr ⇒
333              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
334                [ RELATIVE r ⇒ λrel: True.
335                  if ¬(get_cy_flag s) then
336                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
337                      set_program_counter s new_pc
338                  else
339                    s
340                | _ ⇒ λother: False. ⊥
341                ] (subaddressing_modein … addr)
342            | JB addr1 addr2 ⇒
343              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
344                [ RELATIVE r ⇒ λrel: True.
345                  if get_arg_1 s addr1 false then
346                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
347                      set_program_counter s new_pc
348                  else
349                    s
350                | _ ⇒ λother: False. ⊥
351                ] (subaddressing_modein … addr2)
352            | JNB addr1 addr2 ⇒
353              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
354                [ RELATIVE r ⇒ λrel: True.
355                  if ¬(get_arg_1 s addr1 false) then
356                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
357                      set_program_counter s new_pc
358                  else
359                    s
360                | _ ⇒ λother: False. ⊥
361                ] (subaddressing_modein … addr2)
362            | JBC addr1 addr2 ⇒
363              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
364                [ RELATIVE r ⇒ λrel: True.
365                  let s ≝ set_arg_1 s addr1 false in
366                    if get_arg_1 s addr1 false then
367                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
368                        set_program_counter s new_pc
369                    else
370                      s
371                | _ ⇒ λother: False. ⊥
372                ] (subaddressing_modein … addr2)
373            | JZ addr ⇒
374              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
375                [ RELATIVE r ⇒ λrel: True.
376                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
377                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
378                        set_program_counter s new_pc
379                    else
380                      s
381                | _ ⇒ λother: False. ⊥
382                ] (subaddressing_modein … addr)
383            | JNZ addr ⇒
384              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
385                [ RELATIVE r ⇒ λrel: True.
386                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
387                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
388                        set_program_counter s new_pc
389                    else
390                      s
391                | _ ⇒ λother: False. ⊥
392                ] (subaddressing_modein … addr)
393            | CJNE addr1 addr2 ⇒
394              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
395                [ RELATIVE r ⇒ λrelative: True.
396                  match addr1 with
397                    [ inl l ⇒
398                        let 〈addr1, addr2〉 ≝ l in
399                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
400                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
401                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
402                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
403                            let s ≝ set_program_counter s new_pc in
404                              set_flags s new_cy (None ?) (get_ov_flag s)
405                          else
406                            (set_flags s new_cy (None ?) (get_ov_flag s))
407                    | inr r' ⇒
408                        let 〈addr1, addr2〉 ≝ r' in
409                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
410                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
411                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
412                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
413                            let s ≝ set_program_counter s new_pc in
414                              set_flags s new_cy (None ?) (get_ov_flag s)
415                          else
416                            (set_flags s new_cy (None ?) (get_ov_flag s))
417                    ]
418                | _ ⇒ λother: False. ⊥
419                ] (subaddressing_modein … addr2)
420            | DJNZ addr1 addr2 ⇒
421              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
422                [ RELATIVE r ⇒ λrel: True.
423                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
424                    let s ≝ set_arg_8 s addr1 result in
425                      if ¬(eq_bv ? result (zero 8)) then
426                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
427                          set_program_counter s new_pc
428                      else
429                        s
430                | _ ⇒ λother: False. ⊥
431                ] (subaddressing_modein … addr2)
432            ]
433        | JMP _ ⇒ (* DPM: always indirect_dptr *)
434          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
435          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
436          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
437          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
438            set_program_counter s new_pc
439        | LJMP addr ⇒
440          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
441            [ ADDR16 a ⇒ λaddr16: True.
442                set_program_counter s a
443            | _ ⇒ λother: False. ⊥
444            ] (subaddressing_modein … addr)
445        | SJMP addr ⇒
446          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
447            [ RELATIVE r ⇒ λrelative: True.
448                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
449                  set_program_counter s new_pc
450            | _ ⇒ λother: False. ⊥
451            ] (subaddressing_modein … addr)
452        | AJMP addr ⇒
453          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
454            [ ADDR11 a ⇒ λaddr11: True.
455              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
456              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
457              let bit ≝ get_index' ? O ? nl in
458              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
459              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
460              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
461                set_program_counter s new_pc
462            | _ ⇒ λother: False. ⊥
463            ] (subaddressing_modein … addr)
464        | MOVC addr1 addr2 ⇒
465          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
466            [ ACC_DPTR ⇒ λacc_dptr: True.
467              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
468              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
469              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
470              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
471                set_8051_sfr s SFR_ACC_A result
472            | ACC_PC ⇒ λacc_pc: True.
473              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
474              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
475              (* DPM: Under specified: does the carry from PC incrementation affect the *)
476              (*      addition of the PC with the DPTR? At the moment, no.              *)
477              let s ≝ set_program_counter s inc_pc in
478              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
479              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
480                set_8051_sfr s SFR_ACC_A result
481            | _ ⇒ λother: False. ⊥
482            ] (subaddressing_modein … addr2)
483        | MOVX addr ⇒
484          (* DPM: only copies --- doesn't affect I/O *)
485          match addr with
486            [ inl l ⇒
487              let 〈addr1, addr2〉 ≝ l in
488                set_arg_8 s addr1 (get_arg_8 s false addr2)
489            | inr r ⇒
490              let 〈addr1, addr2〉 ≝ r in
491                set_arg_8 s addr1 (get_arg_8 s false addr2)
492            ]
493        | MOV addr ⇒
494          match addr with
495            [ inl l ⇒
496              match l with
497                [ inl l' ⇒
498                  match l' with
499                    [ inl l'' ⇒
500                      match l'' with
501                        [ inl l''' ⇒
502                          match l''' with
503                            [ inl l'''' ⇒
504                              let 〈addr1, addr2〉 ≝ l'''' in
505                                set_arg_8 s addr1 (get_arg_8 s false addr2)
506                            | inr r'''' ⇒
507                              let 〈addr1, addr2〉 ≝ r'''' in
508                                set_arg_8 s addr1 (get_arg_8 s false addr2)
509                            ]
510                        | inr r''' ⇒
511                          let 〈addr1, addr2〉 ≝ r''' in
512                            set_arg_8 s addr1 (get_arg_8 s false addr2)
513                        ]
514                    | inr r'' ⇒
515                      let 〈addr1, addr2〉 ≝ r'' in
516                        set_arg_16 s (get_arg_16 s addr2) addr1
517                    ]
518                | inr r ⇒
519                  let 〈addr1, addr2〉 ≝ r in
520                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
521                ]
522            | inr r ⇒
523              let 〈addr1, addr2〉 ≝ r in
524                set_arg_1 s addr1 (get_arg_1 s addr2 false)
525            ]
526        | LCALL addr ⇒
527          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
528            [ ADDR16 a ⇒ λaddr16: True.
529              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
530              let s ≝ set_8051_sfr s SFR_SP new_sp in
531              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
532              let s ≝ write_at_stack_pointer s pc_bl in
533              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
534              let s ≝ set_8051_sfr s SFR_SP new_sp in
535              let s ≝ write_at_stack_pointer s pc_bu in
536                set_program_counter s a
537            | _ ⇒ λother: False. ⊥
538            ] (subaddressing_modein … addr)
539        | ACALL addr ⇒
540          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
541            [ ADDR11 a ⇒ λaddr11: True.
542              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
543              let s ≝ set_8051_sfr s SFR_SP new_sp in
544              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
545              let s ≝ write_at_stack_pointer s pc_bl in
546              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
547              let s ≝ set_8051_sfr s SFR_SP new_sp in
548              let s ≝ write_at_stack_pointer s pc_bu in
549              let 〈thr, eig〉 ≝ split ? 3 8 a in
550              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
551              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
552                set_program_counter s new_addr
553            | _ ⇒ λother: False. ⊥
554            ] (subaddressing_modein … addr)
555        | NOP ⇒ s
556        ]
557    in
558      s.
559    ntry nassumption;
560    ntry (
561      nnormalize
562      nrepeat (napply (le_S_S))
563      napply (le_O_n)
564    );
565    ntry (
566      napply (execute_1_technical … (subaddressing_modein …))
567      napply I
568    );
569    ntry (
570      nnormalize
571      napply I
572    );     
573nqed.
574
575nlet rec execute (n: nat) (s: Status) on n: Status ≝
576  match n with
577    [ O ⇒ s
578    | S o ⇒ execute o (execute_1 s)
579    ].
Note: See TracBrowser for help on using the repository browser.