source: src/ASM/Interpret.ma @ 1709

Last change on this file since 1709 was 1709, checked in by mulligan, 8 years ago

Changes to the execution of the MOVC instruction

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