source: src/ASM/Interpret.ma @ 1534

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

committing my changes to interpret to prevent any further conflicts

File size: 35.8 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 //
21 # K
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_args_8_ignores_clock:
129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
130#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
131#a #E >E //
132qed.
133
134example set_program_counter_ignores_clock:
135  ∀M: Type[0].
136  ∀s: PreStatus M.
137  ∀pc: Word.
138    clock M (set_program_counter … s pc) = clock … s.
139  #M #s #pc %
140qed.
141
142example set_low_internal_ram_ignores_clock:
143  ∀M: Type[0].
144  ∀s: PreStatus M.
145  ∀ram: BitVectorTrie Byte 7.
146    clock … (set_low_internal_ram … s ram) = clock … s.
147  #M #s #ram %
148qed.
149
150example set_8051_sfr_ignores_clock:
151  ∀M: Type[0].
152  ∀s: PreStatus M.
153  ∀sfr: SFR8051.
154  ∀v: Byte.
155    clock … (set_8051_sfr ? s sfr v) = clock … s.
156  #M #s #sfr #v %
157qed.
158
159axiom set_arg_8_ignores_clock:
160  ∀M: Type[0].
161  ∀s: PreStatus M.
162  ∀arg.
163  ∀val.
164    clock M (set_arg_8 … s arg val) = clock … s.
165 
166example clock_set_clock:
167  ∀M: Type[0].
168  ∀s: PreStatus M.
169  ∀v.
170    clock … (set_clock … s v) = v.
171  #M #s #v %
172qed.
173
174lemma tech_clocks_le:
175 ∀M,s.∀t:Σs'. clock M s ≤ clock M s'. clock … s ≤ clock … t.
176 #M #s * //
177qed.
178
179definition execute_1_preinstruction:
180 ∀ticks: nat × nat.
181 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
182 ∀s:PreStatus M. Σs': PreStatus M. clock M s ≤ clock … s' ≝
183  λticks.
184  λA, M: Type[0].
185  λaddr_of: A → (PreStatus M) → Word.
186  λinstr: preinstruction A.
187  λs: PreStatus M.
188  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
189  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
190  match instr return λx. Σs': PreStatus M. clock … s ≤ clock … s' with
191        [ ADD addr1 addr2 ⇒
192            let s ≝ add_ticks1 s in
193            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
194                                                   (get_arg_8 ? s false addr2) false in
195            let cy_flag ≝ get_index' ? O  ? flags in
196            let ac_flag ≝ get_index' ? 1 ? flags in
197            let ov_flag ≝ get_index' ? 2 ? flags in
198            let s ≝ set_arg_8 ? s ACC_A result in
199              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
200        | ADDC addr1 addr2 ⇒
201            let s ≝ add_ticks1 s in
202            let old_cy_flag ≝ get_cy_flag ? s in
203            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
204                                                   (get_arg_8 ? s false addr2) old_cy_flag in
205            let cy_flag ≝ get_index' ? O ? flags in
206            let ac_flag ≝ get_index' ? 1 ? flags in
207            let ov_flag ≝ get_index' ? 2 ? flags in
208            let s ≝ set_arg_8 ? s ACC_A result in
209              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
210        | SUBB addr1 addr2 ⇒
211            let s ≝ add_ticks1 s in
212            let old_cy_flag ≝ get_cy_flag ? s in
213            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
214                                                   (get_arg_8 ? s false addr2) old_cy_flag in
215            let cy_flag ≝ get_index' ? O ? flags in
216            let ac_flag ≝ get_index' ? 1 ? flags in
217            let ov_flag ≝ get_index' ? 2 ? flags in
218            let s ≝ set_arg_8 ? s ACC_A result in
219              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
220        | ANL addr ⇒
221          let s ≝ add_ticks1 s in
222          match addr with
223            [ inl l ⇒
224              match l with
225                [ inl l' ⇒
226                  let 〈addr1, addr2〉 ≝ l' in
227                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
228                    set_arg_8 ? s addr1 and_val
229                | inr r ⇒
230                  let 〈addr1, addr2〉 ≝ r 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                ]
234            | inr r ⇒
235              let 〈addr1, addr2〉 ≝ r in
236              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
237                set_flags ? s and_val (None ?) (get_ov_flag ? s)
238            ]
239        | ORL addr ⇒
240          let s ≝ add_ticks1 s in
241          match addr with
242            [ inl l ⇒
243              match l with
244                [ inl l' ⇒
245                  let 〈addr1, addr2〉 ≝ l' in
246                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
247                    set_arg_8 ? s addr1 or_val
248                | inr r ⇒
249                  let 〈addr1, addr2〉 ≝ r 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                ]
253            | inr r ⇒
254              let 〈addr1, addr2〉 ≝ r in
255              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
256                set_flags ? s or_val (None ?) (get_ov_flag ? s)
257            ]
258        | XRL addr ⇒
259          let s ≝ add_ticks1 s in
260          match addr with
261            [ inl l' ⇒
262              let 〈addr1, addr2〉 ≝ l' in
263              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
264                eject … (set_arg_8 ? s addr1 xor_val)
265            | inr r ⇒
266              let 〈addr1, addr2〉 ≝ r in
267              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
268                eject … (set_arg_8 ? s addr1 xor_val)
269            ]
270        | INC addr ⇒
271            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
272                                                           registr;
273                                                           direct;
274                                                           indirect;
275                                                           dptr ]] x) → Σs': PreStatus M. clock … s ≤ 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                 eject … (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                 eject … (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                 eject … (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                 eject … (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                  eject … (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             eject … (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             eject … (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                   eject … (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. clock … s ≤ clock … s' with
348            [ ACC_A ⇒ λacc_a: True.
349              let s ≝ add_ticks1 s in
350                eject … (set_arg_8 ? s ACC_A (zero 8))
351            | CARRY ⇒ λcarry: True.
352              let s ≝ add_ticks1 s in
353                eject … (set_arg_1 ? s CARRY false)
354            | BIT_ADDR b ⇒ λbit_addr: True.
355              let s ≝ add_ticks1 s in
356                eject … (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. clock … s ≤ 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                  eject … (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                  eject … (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                  eject … (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. clock … s ≤ 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        | _ ⇒ ?
443        ].
444        | RET ⇒
445            let s ≝ add_ticks1 s in
446            let high_bits ≝ read_at_stack_pointer ? s in
447            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
448            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
449            let low_bits ≝ read_at_stack_pointer ? s in
450            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
451            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
452            let new_pc ≝ high_bits @@ low_bits in
453              set_program_counter ? s new_pc
454        | RETI ⇒
455            let s ≝ add_ticks1 s in
456            let high_bits ≝ read_at_stack_pointer ? s in
457            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
458            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
459            let low_bits ≝ read_at_stack_pointer ? s in
460            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
461            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
462            let new_pc ≝ high_bits @@ low_bits in
463              set_program_counter ? s new_pc
464        | MOVX addr ⇒
465          let s ≝ add_ticks1 s in
466          (* DPM: only copies --- doesn't affect I/O *)
467          match addr with
468            [ inl l ⇒
469              let 〈addr1, addr2〉 ≝ l in
470                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
471            | inr r ⇒
472              let 〈addr1, addr2〉 ≝ r in
473                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
474            ]
475        | MOV addr ⇒
476          let s ≝ add_ticks1 s in
477          match addr 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                          match l''' with
486                            [ inl l'''' ⇒
487                              let 〈addr1, addr2〉 ≝ l'''' in
488                                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
489                            | inr r'''' ⇒
490                              let 〈addr1, addr2〉 ≝ r'''' in
491                                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
492                            ]
493                        | inr r''' ⇒
494                          let 〈addr1, addr2〉 ≝ r''' in
495                            eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
496                        ]
497                    | inr r'' ⇒
498                      let 〈addr1, addr2〉 ≝ r'' in
499                        eject … (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
500                    ]
501                | inr r ⇒
502                  let 〈addr1, addr2〉 ≝ r in
503                    eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
504                ]
505            | inr r ⇒
506              let 〈addr1, addr2〉 ≝ r in
507                eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
508            ]
509          | JC addr ⇒
510                  if get_cy_flag ? s then
511                    let s ≝ add_ticks1 s in
512                      set_program_counter ? s (addr_of addr s)
513                  else
514                    let s ≝ add_ticks2 s in
515                      s
516            | JNC addr ⇒
517                  if ¬(get_cy_flag ? s) then
518                   let s ≝ add_ticks1 s in
519                     eject … (set_program_counter ? s (addr_of addr s))
520                  else
521                   let s ≝ add_ticks2 s in
522                    s
523            | JB addr1 addr2 ⇒
524                  if get_arg_1 ? s addr1 false then
525                   let s ≝ add_ticks1 s in
526                    set_program_counter ? s (addr_of addr2 s)
527                  else
528                   let s ≝ add_ticks2 s in
529                    s
530            | JNB addr1 addr2 ⇒
531                  if ¬(get_arg_1 ? s addr1 false) then
532                   let s ≝ add_ticks1 s in
533                    set_program_counter ? s (addr_of addr2 s)
534                  else
535                   let s ≝ add_ticks2 s in
536                    s
537            | JBC addr1 addr2 ⇒
538                  let s ≝ set_arg_1 ? s addr1 false in
539                    if get_arg_1 ? s addr1 false then
540                     let s ≝ add_ticks1 s in
541                      set_program_counter ? s (addr_of addr2 s)
542                    else
543                     let s ≝ add_ticks2 s in
544                      s
545            | JZ addr ⇒
546                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
547                     let s ≝ add_ticks1 s in
548                      set_program_counter ? s (addr_of addr s)
549                    else
550                     let s ≝ add_ticks2 s in
551                      s
552            | JNZ addr ⇒
553                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
554                     let s ≝ add_ticks1 s in
555                      set_program_counter ? s (addr_of addr s)
556                    else
557                     let s ≝ add_ticks2 s in
558                      s
559            | CJNE addr1 addr2 ⇒
560                  match addr1 with
561                    [ inl l ⇒
562                        let 〈addr1, addr2'〉 ≝ l in
563                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
564                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
565                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
566                            let s ≝ add_ticks1 s in
567                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
568                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
569                          else
570                            let s ≝ add_ticks2 s in
571                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
572                    | inr r' ⇒
573                        let 〈addr1, addr2'〉 ≝ r' in
574                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
575                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
576                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
577                            let s ≝ add_ticks1 s in
578                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
579                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
580                          else
581                            let s ≝ add_ticks2 s in
582                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
583                    ]
584            | DJNZ addr1 addr2 ⇒
585              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
586              let s ≝ set_arg_8 ? s addr1 result in
587                if ¬(eq_bv ? result (zero 8)) then
588                 let s ≝ add_ticks1 s in
589                  set_program_counter ? s (addr_of addr2 s)
590                else
591                 let s ≝ add_ticks2 s in
592                  s
593        ]. (*14s*)
594(*    try assumption (*20s*)
595    try % (*6s*)
596    try (
597      @ (execute_1_technical … (subaddressing_modein …))
598      @ I
599    ) (*34s*) *)
600 [9: normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
601     >clock_set_clock //
602 |32,34: cases l #either normalize nodelta cases either
603      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
604      >clock_set_clock //
605 |36,48: cases addr #either normalize nodelta cases either
606      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
607      >clock_set_clock // (* XXX: change addr to l *)
608 |44: cases l2 #either normalize nodelta
609      [2: cases either #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
610          >clock_set_clock //
611      |1: cases either #addr cases addr #addr1 #addr2 normalize nodelta
612          >set_arg_8_ignores_clock >clock_set_clock //
613      ] (* XXX: change l2 to l *)
614 |5: cases (sub_8_with_carry (get_arg_8 M s1 true addr) (bitvector_of_nat 8 1) false)
615     #result #flags normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
616 |37: cases addr
617 |20,21,30,31: (* XXX: segfault here *)
618 |1,2,3: /by/ (*41s*)
619 |4,6,7,8,10,11,12,13,14,15: /by/ (*6s*)
620 |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*)
621 |33,35,39,41,43,54,55,56: /by/ (*6s*)
622 |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*)
623 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
624 |*:cases daemon]
625qed.
626
627(*CSC: indexing diverges, why?*)
628example set_program_counter_ignores_clock:
629  ∀M.∀s: PreStatus M.
630  ∀pc: Word.
631    clock … (set_program_counter … s pc) = clock … s.
632 //
633qed.
634
635lemma set_8051_sfr_ignores_clock:
636  ∀M.∀s: PreStatus M.
637  ∀sfr: SFR8051.
638  ∀v: Byte.
639    clock … (set_8051_sfr ? s sfr v) = clock … s.
640  //
641qed.
642
643lemma write_at_stack_pointer_ignores_clock:
644  ∀M.∀s: PreStatus M.
645  ∀sp: Byte.
646    clock … (write_at_stack_pointer … s sp) = clock … s.
647  #M #s #sp
648  change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
649   in match (write_at_stack_pointer ???);
650  normalize nodelta
651  cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
652  #nu #nl normalize nodelta;
653  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
654  [ normalize nodelta; %
655  | normalize nodelta; %
656  ]
657qed.
658
659definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
660  λs0,instr_pc_ticks.
661    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
662    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
663    let s ≝ set_program_counter ? s0 pc in
664      match instr return λ_.Σs': Status. clock … s0 ≤ clock … s' with
665      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
666        (λx. λs.
667        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
668        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
669        | _ ⇒ λabsd. ⊥
670        ] (subaddressing_modein … x)) instr s
671     | ACALL addr ⇒
672          let s ≝ set_clock ? s (ticks + clock ? s) in
673          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
674            [ ADDR11 a ⇒ λaddr11: True.
675              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
676              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
677              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
678              let s ≝ write_at_stack_pointer ? s pc_bl in
679              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
680              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
681              let s ≝ write_at_stack_pointer ? s pc_bu in
682              let 〈thr, eig〉 ≝ split ? 3 8 a in
683              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
684              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
685                set_program_counter ? s new_addr
686            | _ ⇒ λother: False. ⊥
687            ] (subaddressing_modein … addr)
688        | LCALL addr ⇒
689          let s ≝ set_clock ? s (ticks + clock ? s) in
690          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
691            [ ADDR16 a ⇒ λaddr16: True.
692              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
693              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
694              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
695              let s ≝ write_at_stack_pointer ? s pc_bl in
696              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
697              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
698              let s ≝ write_at_stack_pointer ? s pc_bu in
699                set_program_counter ? s a
700            | _ ⇒ λother: False. ⊥
701            ] (subaddressing_modein … addr)
702        | MOVC addr1 addr2 ⇒
703          let s ≝ set_clock ? s (ticks + clock ? s) in
704          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
705            [ ACC_DPTR ⇒ λacc_dptr: True.
706              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
707              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
708              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
709              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
710                set_8051_sfr ? s SFR_ACC_A result
711            | ACC_PC ⇒ λacc_pc: True.
712              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
713              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
714              (* DPM: Under specified: does the carry from PC incrementation affect the *)
715              (*      addition of the PC with the DPTR? At the moment, no.              *)
716              let s ≝ set_program_counter ? s inc_pc in
717              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
718              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
719                set_8051_sfr ? s SFR_ACC_A result
720            | _ ⇒ λother: False. ⊥
721            ] (subaddressing_modein … addr2)
722        | JMP _ ⇒ (* DPM: always indirect_dptr *)
723          let s ≝ set_clock ? s (ticks + clock ? s) in
724          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
725          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
726          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
727          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
728            set_program_counter ? s new_pc
729        | LJMP addr ⇒
730          let s ≝ set_clock ? s (ticks + clock ? s) in
731          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
732            [ ADDR16 a ⇒ λaddr16: True.
733                set_program_counter ? s a
734            | _ ⇒ λother: False. ⊥
735            ] (subaddressing_modein … addr)
736        | SJMP addr ⇒
737          let s ≝ set_clock ? s (ticks + clock ? s) in
738          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
739            [ RELATIVE r ⇒ λrelative: True.
740                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
741                  set_program_counter ? s new_pc
742            | _ ⇒ λother: False. ⊥
743            ] (subaddressing_modein … addr)
744        | AJMP addr ⇒
745          let s ≝ set_clock ? s (ticks + clock ? s) in
746          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
747            [ ADDR11 a ⇒ λaddr11: True.
748              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
749              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
750              let bit ≝ get_index' ? O ? nl in
751              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
752              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
753              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
754                set_program_counter ? s new_pc
755            | _ ⇒ λother: False. ⊥
756            ] (subaddressing_modein … addr)
757      ].
758    try assumption
759    try (
760      normalize
761      repeat (@ (le_S_S))
762      @ (le_O_n)
763    )
764    try (
765      @ (execute_1_technical … (subaddressing_modein …))
766      @ I
767    )
768    try (
769      normalize
770      @ I
771    )
772      ]. (*5s*)
773    try assumption (*12s*)
774    [1,2: >set_program_counter_ignores_clock normalize nodelta
775      >write_at_stack_pointer_ignores_clock
776      >set_8051_sfr_ignores_clock
777      >write_at_stack_pointer_ignores_clock
778      >set_8051_sfr_ignores_clock
779      change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/
780    |3,4,5,6: >set_program_counter_ignores_clock normalize nodelta
781     change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/
782    |7,8: >set_8051_sfr_ignores_clock normalize nodelta change with (? ≤ ?+?)
783      >set_program_counter_ignores_clock /by/]
784qed.
785
786definition execute_1: ∀s:Status. Σs':Status. clock … s ≤ clock … s' ≝
787  λs: Status.
788    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
789     execute_1_0 s instr_pc_ticks.
790
791definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
792  λticks,s,instr,pc.
793  let s ≝ set_program_counter ? s pc in
794  let s ≝
795    match instr with
796    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
797    | Comment cmt ⇒
798       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
799        s
800    | Cost cst ⇒ s
801    | Jmp jmp ⇒
802       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
803        set_program_counter ? s (address_of_word_labels s jmp)
804    | Call call ⇒
805      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
806      let a ≝ address_of_word_labels s call in
807      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
808      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
809      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
810      let s ≝ write_at_stack_pointer ? s pc_bl in
811      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
812      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
813      let s ≝ write_at_stack_pointer ? s pc_bu in
814        set_program_counter ? s a
815    | Mov dptr ident ⇒
816      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
817      let preamble ≝ \fst (code_memory ? s) in
818      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
819        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
820    ]
821  in
822    s.
823  normalize
824  @ I
825qed.
826
827definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
828  λticks_of,s.
829  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
830  let ticks ≝ ticks_of (program_counter ? s) in
831   execute_1_pseudo_instruction0 ticks s instr pc.
832
833let rec execute (n: nat) (s: Status) on n: Status ≝
834  match n with
835    [ O ⇒ s
836    | S o ⇒ execute o (execute_1 s)
837    ].
838
839let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
840  match n with
841    [ O ⇒ s
842    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
843    ].
Note: See TracBrowser for help on using the repository browser.