source: src/ASM/Interpret.ma @ 1573

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

more complicated than it appears :(

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