source: src/ASM/Interpret.ma @ 1587

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

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

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