source: src/ASM/Interpret.ma @ 1606

Last change on this file since 1606 was 1606, checked in by sacerdot, 6 years ago

Porting to last library of Matita.

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