source: src/ASM/Interpret.ma @ 712

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

Changes to get things to typecheck.

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