source: src/ASM/Interpret.ma @ 1588

Last change on this file since 1588 was 1588, checked in by sacerdot, 8 years ago

All goals generated by Russell for execute_1* are now closed, mostly by
automation. Since automation does not work on equational goals that contain
equations, I was forced to change every (?) Russel definition into triples:
fun' with Sigma type as a type; fun as @eject of fun'; fun_ok as @sig2 of fun'.

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