source: src/ASM/Interpret.ma @ 1575

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

Changes to specifications on execute functions

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