source: src/ASM/Interpret.ma @ 2056

Last change on this file since 2056 was 2056, checked in by sacerdot, 7 years ago

Repaired, ported to new fetch_pseudo_assembly.
The execute_n is commented out because it only exists in partial form
(see the comment in the code).

File size: 59.5 KB
Line 
1include "basics/lists/listb.ma".
2include "ASM/StatusProofs.ma".
3include "ASM/Fetch.ma".
4include "ASM/AbstractStatus.ma".
5
6definition sign_extension: Byte → Word ≝
7  λc.
8    let b ≝ get_index_v ? 8 c 1 ? in
9      [[ b; b; b; b; b; b; b; b ]] @@ c.
10  normalize
11  repeat (@le_S_S)
12  @le_O_n
13qed.
14   
15lemma execute_1_technical:
16  ∀n, m: nat.
17  ∀v: Vector addressing_mode_tag (S n).
18  ∀q: Vector addressing_mode_tag (S m).
19  ∀a: addressing_mode.
20    bool_to_Prop (is_in ? v a) →
21    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
22    bool_to_Prop (is_in ? q a).
23 # n
24 # m
25 # v
26 # q
27 # a
28 elim v
29 [ normalize
30   # K
31   cases K
32 | # n'
33   # he
34   # tl
35   # II
36   whd in ⊢ (% → ? → ?);
37   lapply (refl … (is_in … (he:::tl) a))
38   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
39   [ # K
40     # _
41     normalize in K;
42     whd in ⊢ (% → ?);
43     lapply (refl … (subvector_with … eq_a (he:::tl) q));
44     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
45     [ # K1
46       # _
47       change with ((andb ? (subvector_with …)) = true) in K1;
48       cases (conjunction_true … K1)
49       # K3
50       # K4
51       cases (inclusive_disjunction_true … K)
52       # K2
53       [ > (is_a_to_mem_to_is_in … K2 K3)
54         %
55       | @ II
56         [ > K2
57           %
58         | > K4
59           %
60         ]
61       ]
62     | # K1
63       # K2
64       normalize in K2;
65       cases K2;
66     ]
67   | # K1
68     # K2
69     normalize in K2;
70     cases K2
71   ]
72 ]
73qed.
74
75include alias "arithmetics/nat.ma".
76include alias "ASM/BitVectorTrie.ma".
77
78definition execute_1_preinstruction:
79  ∀ticks: nat × nat.
80  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
81  ∀s: PreStatus m cm. PreStatus m cm ≝
82  λticks: nat × nat.
83  λa, m: Type[0]. λcm.
84  λaddr_of: a → PreStatus m cm → Word.
85  λinstr: preinstruction a.
86  λs: PreStatus m cm.
87  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
88  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
89  match instr in preinstruction return λx. x = instr → PreStatus m cm with
90        [ ADD addr1 addr2 ⇒ λinstr_refl.
91            let s ≝ add_ticks1 s in
92            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
93                                                   (get_arg_8 … s false addr2) false in
94            let cy_flag ≝ get_index' ? O  ? flags in
95            let ac_flag ≝ get_index' ? 1 ? flags in
96            let ov_flag ≝ get_index' ? 2 ? flags in
97            let s ≝ set_arg_8 … s ACC_A result in
98              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
99        | ADDC addr1 addr2 ⇒ λinstr_refl.
100            let s ≝ add_ticks1 s in
101            let old_cy_flag ≝ get_cy_flag ?? s in
102            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
103                                                   (get_arg_8 … s false addr2) old_cy_flag in
104            let cy_flag ≝ get_index' ? O ? flags in
105            let ac_flag ≝ get_index' ? 1 ? flags in
106            let ov_flag ≝ get_index' ? 2 ? flags in
107            let s ≝ set_arg_8 … s ACC_A result in
108              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
109        | SUBB addr1 addr2 ⇒ λinstr_refl.
110            let s ≝ add_ticks1 s in
111            let old_cy_flag ≝ get_cy_flag ?? s in
112            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
113                                                   (get_arg_8 … s false addr2) old_cy_flag in
114            let cy_flag ≝ get_index' ? O ? flags in
115            let ac_flag ≝ get_index' ? 1 ? flags in
116            let ov_flag ≝ get_index' ? 2 ? flags in
117            let s ≝ set_arg_8 … s ACC_A result in
118              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
119        | ANL addr ⇒ λinstr_refl.
120          let s ≝ add_ticks1 s in
121          match addr with
122            [ inl l ⇒
123              match l with
124                [ inl l' ⇒
125                  let 〈addr1, addr2〉 ≝ l' in
126                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
127                    set_arg_8 … s addr1 and_val
128                | inr r ⇒
129                  let 〈addr1, addr2〉 ≝ r in
130                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
131                    set_arg_8 … s addr1 and_val
132                ]
133            | inr r ⇒
134              let 〈addr1, addr2〉 ≝ r in
135              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
136               set_flags … s and_val (None ?) (get_ov_flag ?? s)
137            ]
138        | ORL addr ⇒ λinstr_refl.
139          let s ≝ add_ticks1 s in
140          match addr with
141            [ inl l ⇒
142              match l with
143                [ inl l' ⇒
144                  let 〈addr1, addr2〉 ≝ l' in
145                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
146                    set_arg_8 … s addr1 or_val
147                | inr r ⇒
148                  let 〈addr1, addr2〉 ≝ r in
149                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
150                    set_arg_8 … s addr1 or_val
151                ]
152            | inr r ⇒
153              let 〈addr1, addr2〉 ≝ r in
154              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
155               set_flags … s or_val (None ?) (get_ov_flag … s)
156            ]
157        | XRL addr ⇒ λinstr_refl.
158          let s ≝ add_ticks1 s in
159          match addr with
160            [ inl l' ⇒
161              let 〈addr1, addr2〉 ≝ l' in
162              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
163                set_arg_8 … s addr1 xor_val
164            | inr r ⇒
165              let 〈addr1, addr2〉 ≝ r in
166              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
167                set_arg_8 … s addr1 xor_val
168            ]
169        | INC addr ⇒ λinstr_refl.
170            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
171              [ ACC_A ⇒ λacc_a: True.
172                let s' ≝ add_ticks1 s in
173                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
174                 set_arg_8 … s' ACC_A result
175              | REGISTER r ⇒ λregister: True.
176                let s' ≝ add_ticks1 s in
177                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
178                 set_arg_8 … s' (REGISTER r) result
179              | DIRECT d ⇒ λdirect: True.
180                let s' ≝ add_ticks1 s in
181                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
182                 set_arg_8 … s' (DIRECT d) result
183              | INDIRECT i ⇒ λindirect: True.
184                let s' ≝ add_ticks1 s in
185                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
186                 set_arg_8 … s' (INDIRECT i) result
187              | DPTR ⇒ λdptr: True.
188                let s' ≝ add_ticks1 s in
189                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
190                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
191                let s ≝ set_8051_sfr … s' SFR_DPL bl in
192                 set_8051_sfr … s' SFR_DPH bu
193              | _ ⇒ λother: False. ⊥
194              ] (subaddressing_modein … addr)
195        | NOP ⇒ λinstr_refl.
196           let s ≝ add_ticks2 s in
197            s
198        | DEC addr ⇒ λinstr_refl.
199           let s ≝ add_ticks1 s in
200           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
201             set_arg_8 … s addr result
202        | MUL addr1 addr2 ⇒ λinstr_refl.
203           let s ≝ add_ticks1 s in
204           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
205           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
206           let product ≝ acc_a_nat * acc_b_nat in
207           let ov_flag ≝ product ≥ 256 in
208           let low ≝ bitvector_of_nat 8 (product mod 256) in
209           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
210           let s ≝ set_8051_sfr … s SFR_ACC_A low in
211             set_8051_sfr … s SFR_ACC_B high
212        | DIV addr1 addr2 ⇒ λinstr_refl.
213           let s ≝ add_ticks1 s in
214           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
215           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
216             match acc_b_nat with
217               [ O ⇒ set_flags … s false (None Bit) true
218               | S o ⇒
219                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
220                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
221                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
222                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
223                   set_flags … s false (None Bit) false
224               ]
225        | DA addr ⇒ λinstr_refl.
226            let s ≝ add_ticks1 s in
227            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
228              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
229                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
230                let cy_flag ≝ get_index' ? O ? flags in
231                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
232                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
233                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
234                    let new_acc ≝ nu @@ acc_nl' in
235                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
236                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
237                  else
238                    s
239              else
240                s
241        | CLR addr ⇒ λinstr_refl.
242          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
243            [ ACC_A ⇒ λacc_a: True.
244              let s ≝ add_ticks1 s in
245               set_arg_8 … s ACC_A (zero 8)
246            | CARRY ⇒ λcarry: True.
247              let s ≝ add_ticks1 s in
248               set_arg_1 … s CARRY false
249            | BIT_ADDR b ⇒ λbit_addr: True.
250              let s ≝ add_ticks1 s in
251               set_arg_1 … s (BIT_ADDR b) false
252            | _ ⇒ λother: False. ⊥
253            ] (subaddressing_modein … addr)
254        | CPL addr ⇒ λinstr_refl.
255          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
256            [ ACC_A ⇒ λacc_a: True.
257                let s ≝ add_ticks1 s in
258                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
259                let new_acc ≝ negation_bv ? old_acc in
260                 set_8051_sfr … s SFR_ACC_A new_acc
261            | CARRY ⇒ λcarry: True.
262                let s ≝ add_ticks1 s in
263                let old_cy_flag ≝ get_arg_1 … s CARRY true in
264                let new_cy_flag ≝ ¬old_cy_flag in
265                 set_arg_1 … s CARRY new_cy_flag
266            | BIT_ADDR b ⇒ λbit_addr: True.
267                let s ≝ add_ticks1 s in
268                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
269                let new_bit ≝ ¬old_bit in
270                 set_arg_1 … s (BIT_ADDR b) new_bit
271            | _ ⇒ λother: False. ?
272            ] (subaddressing_modein … addr)
273        | SETB b ⇒ λinstr_refl.
274            let s ≝ add_ticks1 s in
275            set_arg_1 … s b false
276        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
277            let s ≝ add_ticks1 s in
278            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
279            let new_acc ≝ rotate_left … 1 old_acc in
280              set_8051_sfr … s SFR_ACC_A new_acc
281        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
282            let s ≝ add_ticks1 s in
283            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
284            let new_acc ≝ rotate_right … 1 old_acc in
285              set_8051_sfr … s SFR_ACC_A new_acc
286        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
287            let s ≝ add_ticks1 s in
288            let old_cy_flag ≝ get_cy_flag ?? s in
289            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
290            let new_cy_flag ≝ get_index' ? O ? old_acc in
291            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
292            let s ≝ set_arg_1 … s CARRY new_cy_flag in
293              set_8051_sfr … s SFR_ACC_A new_acc
294        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
295            let s ≝ add_ticks1 s in
296            let old_cy_flag ≝ get_cy_flag ?? s in
297            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
298            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
299            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
300            let s ≝ set_arg_1 … s CARRY new_cy_flag in
301              set_8051_sfr … s SFR_ACC_A new_acc
302        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
303            let s ≝ add_ticks1 s in
304            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
305            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
306            let new_acc ≝ nl @@ nu in
307              set_8051_sfr … s SFR_ACC_A new_acc
308        | PUSH addr ⇒ λinstr_refl.
309            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
310              [ DIRECT d ⇒ λdirect: True.
311                let s ≝ add_ticks1 s in
312                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
313                let s ≝ set_8051_sfr … s SFR_SP new_sp in
314                  write_at_stack_pointer … s d
315              | _ ⇒ λother: False. ⊥
316              ] (subaddressing_modein … addr)
317        | POP addr ⇒ λinstr_refl.
318            let s ≝ add_ticks1 s in
319            let contents ≝ read_at_stack_pointer ?? s in
320            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
321            let s ≝ set_8051_sfr … s SFR_SP new_sp in
322              set_arg_8 … s addr contents
323        | XCH addr1 addr2 ⇒ λinstr_refl.
324            let s ≝ add_ticks1 s in
325            let old_addr ≝ get_arg_8 … s false addr2 in
326            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
327            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
328              set_arg_8 … s addr2 old_acc
329        | XCHD addr1 addr2 ⇒ λinstr_refl.
330            let s ≝ add_ticks1 s in
331            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
332            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
333            let new_acc ≝ acc_nu @@ arg_nl in
334            let new_arg ≝ arg_nu @@ acc_nl in
335            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
336              set_arg_8 … s addr2 new_arg
337        | RET ⇒ λinstr_refl.
338            let s ≝ add_ticks1 s in
339            let high_bits ≝ read_at_stack_pointer ?? s in
340            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
341            let s ≝ set_8051_sfr … s SFR_SP new_sp in
342            let low_bits ≝ read_at_stack_pointer ?? s in
343            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
344            let s ≝ set_8051_sfr … s SFR_SP new_sp in
345            let new_pc ≝ high_bits @@ low_bits in
346              set_program_counter … s new_pc
347        | RETI ⇒ λinstr_refl.
348            let s ≝ add_ticks1 s in
349            let high_bits ≝ read_at_stack_pointer ?? s in
350            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
351            let s ≝ set_8051_sfr … s SFR_SP new_sp in
352            let low_bits ≝ read_at_stack_pointer ?? s in
353            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
354            let s ≝ set_8051_sfr … s SFR_SP new_sp in
355            let new_pc ≝ high_bits @@ low_bits in
356              set_program_counter … s new_pc
357        | MOVX addr ⇒ λinstr_refl.
358          let s ≝ add_ticks1 s in
359          (* DPM: only copies --- doesn't affect I/O *)
360          match addr with
361            [ inl l ⇒
362              let 〈addr1, addr2〉 ≝ l in
363                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
364            | inr r ⇒
365              let 〈addr1, addr2〉 ≝ r in
366                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
367            ]
368        | MOV addr ⇒ λinstr_refl.
369          let s ≝ add_ticks1 s in
370          match addr with
371            [ inl l ⇒
372              match l with
373                [ inl l' ⇒
374                  match l' with
375                    [ inl l'' ⇒
376                      match l'' with
377                        [ inl l''' ⇒
378                          match l''' with
379                            [ inl l'''' ⇒
380                              let 〈addr1, addr2〉 ≝ l'''' in
381                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
382                            | inr r'''' ⇒
383                              let 〈addr1, addr2〉 ≝ r'''' in
384                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
385                            ]
386                        | inr r''' ⇒
387                          let 〈addr1, addr2〉 ≝ r''' in
388                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
389                        ]
390                    | inr r'' ⇒
391                      let 〈addr1, addr2〉 ≝ r'' in
392                       set_arg_16 … s (get_arg_16 … s addr2) addr1
393                    ]
394                | inr r ⇒
395                  let 〈addr1, addr2〉 ≝ r in
396                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
397                ]
398            | inr r ⇒
399              let 〈addr1, addr2〉 ≝ r in
400               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
401            ]
402          | JC addr ⇒ λinstr_refl.
403                  if get_cy_flag ?? s then
404                    let s ≝ add_ticks1 s in
405                      set_program_counter … s (addr_of addr s)
406                  else
407                    let s ≝ add_ticks2 s in
408                      s
409            | JNC addr ⇒ λinstr_refl.
410                  if ¬(get_cy_flag ?? s) then
411                   let s ≝ add_ticks1 s in
412                     set_program_counter … s (addr_of addr s)
413                  else
414                   let s ≝ add_ticks2 s in
415                    s
416            | JB addr1 addr2 ⇒ λinstr_refl.
417                  if get_arg_1 … s addr1 false then
418                   let s ≝ add_ticks1 s in
419                    set_program_counter … s (addr_of addr2 s)
420                  else
421                   let s ≝ add_ticks2 s in
422                    s
423            | JNB addr1 addr2 ⇒ λinstr_refl.
424                  if ¬(get_arg_1 … s addr1 false) then
425                   let s ≝ add_ticks1 s in
426                    set_program_counter … s (addr_of addr2 s)
427                  else
428                   let s ≝ add_ticks2 s in
429                    s
430            | JBC addr1 addr2 ⇒ λinstr_refl.
431                  let s ≝ set_arg_1 … s addr1 false in
432                    if get_arg_1 … s addr1 false then
433                     let s ≝ add_ticks1 s in
434                      set_program_counter … s (addr_of addr2 s)
435                    else
436                     let s ≝ add_ticks2 s in
437                      s
438            | JZ addr ⇒ λinstr_refl.
439                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
440                     let s ≝ add_ticks1 s in
441                      set_program_counter … s (addr_of addr s)
442                    else
443                     let s ≝ add_ticks2 s in
444                      s
445            | JNZ addr ⇒ λinstr_refl.
446                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
447                     let s ≝ add_ticks1 s in
448                      set_program_counter … s (addr_of addr s)
449                    else
450                     let s ≝ add_ticks2 s in
451                      s
452            | CJNE addr1 addr2 ⇒ λinstr_refl.
453                  match addr1 with
454                    [ inl l ⇒
455                        let 〈addr1, addr2'〉 ≝ l in
456                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
457                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
458                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
459                            let s ≝ add_ticks1 s in
460                            let s ≝ set_program_counter … s (addr_of addr2 s) in
461                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
462                          else
463                            let s ≝ add_ticks2 s in
464                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
465                    | inr r' ⇒
466                        let 〈addr1, addr2'〉 ≝ r' in
467                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
468                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
469                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
470                            let s ≝ add_ticks1 s in
471                            let s ≝ set_program_counter … s (addr_of addr2 s) in
472                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
473                          else
474                            let s ≝ add_ticks2 s in
475                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
476                    ]
477            | DJNZ addr1 addr2 ⇒ λinstr_refl.
478              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
479              let s ≝ set_arg_8 … s addr1 result in
480                if ¬(eq_bv ? result (zero 8)) then
481                 let s ≝ add_ticks1 s in
482                  set_program_counter … s (addr_of addr2 s)
483                else
484                 let s ≝ add_ticks2 s in
485                  s
486            ] (refl … instr).
487    try (cases(other))
488    try assumption (*20s*)
489    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
490    try (
491      @(execute_1_technical … (subaddressing_modein …))
492      @I
493    ) (*66s*)
494qed.
495
496definition execute_1_preinstruction_ok':
497  ∀ticks: nat × nat.
498  ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a.
499  ∀s: PreStatus m cm.
500    Σs': PreStatus m cm.
501      (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in
502      (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
503        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝
504  λticks: nat × nat.
505  λa, m: Type[0]. λcm.
506  λaddr_of: a → PreStatus m cm → Word.
507  λinstr: preinstruction a.
508  λs: PreStatus m cm.
509  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
510  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
511  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
512    ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
513      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with
514        [ ADD addr1 addr2 ⇒ λinstr_refl.
515            let s ≝ add_ticks1 s in
516            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
517                                                   (get_arg_8 … s false addr2) false in
518            let cy_flag ≝ get_index' ? O  ? flags in
519            let ac_flag ≝ get_index' ? 1 ? flags in
520            let ov_flag ≝ get_index' ? 2 ? flags in
521            let s ≝ set_arg_8 … s ACC_A result in
522              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
523        | ADDC addr1 addr2 ⇒ λinstr_refl.
524            let s ≝ add_ticks1 s in
525            let old_cy_flag ≝ get_cy_flag ?? s in
526            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
527                                                   (get_arg_8 … s false addr2) old_cy_flag in
528            let cy_flag ≝ get_index' ? O ? flags in
529            let ac_flag ≝ get_index' ? 1 ? flags in
530            let ov_flag ≝ get_index' ? 2 ? flags in
531            let s ≝ set_arg_8 … s ACC_A result in
532              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
533        | SUBB addr1 addr2 ⇒ λinstr_refl.
534            let s ≝ add_ticks1 s in
535            let old_cy_flag ≝ get_cy_flag ?? s in
536            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
537                                                   (get_arg_8 … s false addr2) old_cy_flag in
538            let cy_flag ≝ get_index' ? O ? flags in
539            let ac_flag ≝ get_index' ? 1 ? flags in
540            let ov_flag ≝ get_index' ? 2 ? flags in
541            let s ≝ set_arg_8 … s ACC_A result in
542              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
543        | ANL addr ⇒ λinstr_refl.
544          let s ≝ add_ticks1 s in
545          match addr with
546            [ inl l ⇒
547              match l with
548                [ inl l' ⇒
549                  let 〈addr1, addr2〉 ≝ l' in
550                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
551                    set_arg_8 … s addr1 and_val
552                | inr r ⇒
553                  let 〈addr1, addr2〉 ≝ r in
554                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
555                    set_arg_8 … s addr1 and_val
556                ]
557            | inr r ⇒
558              let 〈addr1, addr2〉 ≝ r in
559              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
560               set_flags … s and_val (None ?) (get_ov_flag ?? s)
561            ]
562        | ORL addr ⇒ λinstr_refl.
563          let s ≝ add_ticks1 s in
564          match addr with
565            [ inl l ⇒
566              match l with
567                [ inl l' ⇒
568                  let 〈addr1, addr2〉 ≝ l' in
569                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
570                    set_arg_8 … s addr1 or_val
571                | inr r ⇒
572                  let 〈addr1, addr2〉 ≝ r in
573                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
574                    set_arg_8 … s addr1 or_val
575                ]
576            | inr r ⇒
577              let 〈addr1, addr2〉 ≝ r in
578              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
579               set_flags … s or_val (None ?) (get_ov_flag … s)
580            ]
581        | XRL addr ⇒ λinstr_refl.
582          let s ≝ add_ticks1 s in
583          match addr with
584            [ inl l' ⇒
585              let 〈addr1, addr2〉 ≝ l' in
586              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
587                set_arg_8 … s addr1 xor_val
588            | inr r ⇒
589              let 〈addr1, addr2〉 ≝ r in
590              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
591                set_arg_8 … s addr1 xor_val
592            ]
593        | INC addr ⇒ λinstr_refl.
594            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with
595              [ ACC_A ⇒ λacc_a: True. λEQaddr.
596                let s' ≝ add_ticks1 s in
597                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
598                 set_arg_8 … s' ACC_A result
599              | REGISTER r ⇒ λregister: True. λEQaddr.
600                let s' ≝ add_ticks1 s in
601                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
602                 set_arg_8 … s' (REGISTER r) result
603              | DIRECT d ⇒ λdirect: True. λEQaddr.
604                let s' ≝ add_ticks1 s in
605                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
606                 set_arg_8 … s' (DIRECT d) result
607              | INDIRECT i ⇒ λindirect: True. λEQaddr.
608                let s' ≝ add_ticks1 s in
609                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
610                 set_arg_8 … s' (INDIRECT i) result
611              | DPTR ⇒ λdptr: True. λEQaddr.
612                let s' ≝ add_ticks1 s in
613                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
614                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
615                let s ≝ set_8051_sfr … s' SFR_DPL bl in
616                 set_8051_sfr … s' SFR_DPH bu
617              | _ ⇒ λother: False. ⊥
618              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
619        | NOP ⇒ λinstr_refl.
620           let s ≝ add_ticks2 s in
621            s
622        | DEC addr ⇒ λinstr_refl.
623           let s ≝ add_ticks1 s in
624           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
625             set_arg_8 … s addr result
626        | MUL addr1 addr2 ⇒ λinstr_refl.
627           let s ≝ add_ticks1 s in
628           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
629           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
630           let product ≝ acc_a_nat * acc_b_nat in
631           let ov_flag ≝ product ≥ 256 in
632           let low ≝ bitvector_of_nat 8 (product mod 256) in
633           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
634           let s ≝ set_8051_sfr … s SFR_ACC_A low in
635             set_8051_sfr … s SFR_ACC_B high
636        | DIV addr1 addr2 ⇒ λinstr_refl.
637           let s ≝ add_ticks1 s in
638           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
639           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
640             match acc_b_nat with
641               [ O ⇒ set_flags … s false (None Bit) true
642               | S o ⇒
643                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
644                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
645                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
646                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
647                   set_flags … s false (None Bit) false
648               ]
649        | DA addr ⇒ λinstr_refl.
650            let s ≝ add_ticks1 s in
651            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
652              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
653                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
654                let cy_flag ≝ get_index' ? O ? flags in
655                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
656                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
657                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
658                    let new_acc ≝ nu @@ acc_nl' in
659                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
660                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
661                  else
662                    s
663              else
664                s
665        | CLR addr ⇒ λinstr_refl.
666          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
667            [ ACC_A ⇒ λacc_a: True. λEQaddr.
668              let s ≝ add_ticks1 s in
669               set_arg_8 … s ACC_A (zero 8)
670            | CARRY ⇒ λcarry: True. λEQaddr.
671              let s ≝ add_ticks1 s in
672               set_arg_1 … s CARRY false
673            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
674              let s ≝ add_ticks1 s in
675               set_arg_1 … s (BIT_ADDR b) false
676            | _ ⇒ λother: False. ⊥
677            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
678        | CPL addr ⇒ λinstr_refl.
679          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
680            [ ACC_A ⇒ λacc_a: True. λEQaddr.
681                let s ≝ add_ticks1 s in
682                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
683                let new_acc ≝ negation_bv ? old_acc in
684                 set_8051_sfr … s SFR_ACC_A new_acc
685            | CARRY ⇒ λcarry: True. λEQaddr.
686                let s ≝ add_ticks1 s in
687                let old_cy_flag ≝ get_arg_1 … s CARRY true in
688                let new_cy_flag ≝ ¬old_cy_flag in
689                 set_arg_1 … s CARRY new_cy_flag
690            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
691                let s ≝ add_ticks1 s in
692                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
693                let new_bit ≝ ¬old_bit in
694                 set_arg_1 … s (BIT_ADDR b) new_bit
695            | _ ⇒ λother: False. ?
696            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
697        | SETB b ⇒ λinstr_refl.
698            let s ≝ add_ticks1 s in
699            set_arg_1 … s b false
700        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
701            let s ≝ add_ticks1 s in
702            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
703            let new_acc ≝ rotate_left … 1 old_acc in
704              set_8051_sfr … s SFR_ACC_A new_acc
705        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
706            let s ≝ add_ticks1 s in
707            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
708            let new_acc ≝ rotate_right … 1 old_acc in
709              set_8051_sfr … s SFR_ACC_A new_acc
710        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
711            let s ≝ add_ticks1 s in
712            let old_cy_flag ≝ get_cy_flag ?? s in
713            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
714            let new_cy_flag ≝ get_index' ? O ? old_acc in
715            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
716            let s ≝ set_arg_1 … s CARRY new_cy_flag in
717              set_8051_sfr … s SFR_ACC_A new_acc
718        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
719            let s ≝ add_ticks1 s in
720            let old_cy_flag ≝ get_cy_flag ?? s in
721            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
722            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
723            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
724            let s ≝ set_arg_1 … s CARRY new_cy_flag in
725              set_8051_sfr … s SFR_ACC_A new_acc
726        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
727            let s ≝ add_ticks1 s in
728            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
729            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
730            let new_acc ≝ nl @@ nu in
731              set_8051_sfr … s SFR_ACC_A new_acc
732        | PUSH addr ⇒ λinstr_refl.
733            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with
734              [ DIRECT d ⇒ λdirect: True. λEQaddr.
735                let s ≝ add_ticks1 s in
736                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
737                let s ≝ set_8051_sfr … s SFR_SP new_sp in
738                  write_at_stack_pointer … s d
739              | _ ⇒ λother: False. ⊥
740              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
741        | POP addr ⇒ λinstr_refl.
742            let s ≝ add_ticks1 s in
743            let contents ≝ read_at_stack_pointer ?? s in
744            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
745            let s ≝ set_8051_sfr … s SFR_SP new_sp in
746              set_arg_8 … s addr contents
747        | XCH addr1 addr2 ⇒ λinstr_refl.
748            let s ≝ add_ticks1 s in
749            let old_addr ≝ get_arg_8 … s false addr2 in
750            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
751            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
752              set_arg_8 … s addr2 old_acc
753        | XCHD addr1 addr2 ⇒ λinstr_refl.
754            let s ≝ add_ticks1 s in
755            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
756            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
757            let new_acc ≝ acc_nu @@ arg_nl in
758            let new_arg ≝ arg_nu @@ acc_nl in
759            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
760              set_arg_8 … s addr2 new_arg
761        | RET ⇒ λinstr_refl.
762            let s ≝ add_ticks1 s in
763            let high_bits ≝ read_at_stack_pointer ?? s in
764            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
765            let s ≝ set_8051_sfr … s SFR_SP new_sp in
766            let low_bits ≝ read_at_stack_pointer ?? s in
767            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
768            let s ≝ set_8051_sfr … s SFR_SP new_sp in
769            let new_pc ≝ high_bits @@ low_bits in
770              set_program_counter … s new_pc
771        | RETI ⇒ λinstr_refl.
772            let s ≝ add_ticks1 s in
773            let high_bits ≝ read_at_stack_pointer ?? s in
774            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
775            let s ≝ set_8051_sfr … s SFR_SP new_sp in
776            let low_bits ≝ read_at_stack_pointer ?? s in
777            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
778            let s ≝ set_8051_sfr … s SFR_SP new_sp in
779            let new_pc ≝ high_bits @@ low_bits in
780              set_program_counter … s new_pc
781        | MOVX addr ⇒ λinstr_refl.
782          let s ≝ add_ticks1 s in
783          (* DPM: only copies --- doesn't affect I/O *)
784          match addr with
785            [ inl l ⇒
786              let 〈addr1, addr2〉 ≝ l in
787                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
788            | inr r ⇒
789              let 〈addr1, addr2〉 ≝ r in
790                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
791            ]
792        | MOV addr ⇒ λinstr_refl.
793          let s ≝ add_ticks1 s in
794          match addr with
795            [ inl l ⇒
796              match l with
797                [ inl l' ⇒
798                  match l' with
799                    [ inl l'' ⇒
800                      match l'' with
801                        [ inl l''' ⇒
802                          match l''' with
803                            [ inl l'''' ⇒
804                              let 〈addr1, addr2〉 ≝ l'''' in
805                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
806                            | inr r'''' ⇒
807                              let 〈addr1, addr2〉 ≝ r'''' in
808                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
809                            ]
810                        | inr r''' ⇒
811                          let 〈addr1, addr2〉 ≝ r''' in
812                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
813                        ]
814                    | inr r'' ⇒
815                      let 〈addr1, addr2〉 ≝ r'' in
816                       set_arg_16 … s (get_arg_16 … s addr2) addr1
817                    ]
818                | inr r ⇒
819                  let 〈addr1, addr2〉 ≝ r in
820                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
821                ]
822            | inr r ⇒
823              let 〈addr1, addr2〉 ≝ r in
824               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
825            ]
826          | JC addr ⇒ λinstr_refl.
827                  if get_cy_flag ?? s then
828                    let s ≝ add_ticks1 s in
829                      set_program_counter … s (addr_of addr s)
830                  else
831                    let s ≝ add_ticks2 s in
832                      s
833            | JNC addr ⇒ λinstr_refl.
834                  if ¬(get_cy_flag ?? s) then
835                   let s ≝ add_ticks1 s in
836                     set_program_counter … s (addr_of addr s)
837                  else
838                   let s ≝ add_ticks2 s in
839                    s
840            | JB addr1 addr2 ⇒ λinstr_refl.
841                  if get_arg_1 … s addr1 false then
842                   let s ≝ add_ticks1 s in
843                    set_program_counter … s (addr_of addr2 s)
844                  else
845                   let s ≝ add_ticks2 s in
846                    s
847            | JNB addr1 addr2 ⇒ λinstr_refl.
848                  if ¬(get_arg_1 … s addr1 false) then
849                   let s ≝ add_ticks1 s in
850                    set_program_counter … s (addr_of addr2 s)
851                  else
852                   let s ≝ add_ticks2 s in
853                    s
854            | JBC addr1 addr2 ⇒ λinstr_refl.
855                  let s ≝ set_arg_1 … s addr1 false in
856                    if get_arg_1 … s addr1 false then
857                     let s ≝ add_ticks1 s in
858                      set_program_counter … s (addr_of addr2 s)
859                    else
860                     let s ≝ add_ticks2 s in
861                      s
862            | JZ addr ⇒ λinstr_refl.
863                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
864                     let s ≝ add_ticks1 s in
865                      set_program_counter … s (addr_of addr s)
866                    else
867                     let s ≝ add_ticks2 s in
868                      s
869            | JNZ addr ⇒ λinstr_refl.
870                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
871                     let s ≝ add_ticks1 s in
872                      set_program_counter … s (addr_of addr s)
873                    else
874                     let s ≝ add_ticks2 s in
875                      s
876            | CJNE addr1 addr2 ⇒ λinstr_refl.
877                  match addr1 with
878                    [ inl l ⇒
879                        let 〈addr1, addr2'〉 ≝ l in
880                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
881                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
882                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
883                            let s ≝ add_ticks1 s in
884                            let s ≝ set_program_counter … s (addr_of addr2 s) in
885                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
886                          else
887                            let s ≝ add_ticks2 s in
888                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
889                    | inr r' ⇒
890                        let 〈addr1, addr2'〉 ≝ r' in
891                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
892                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
893                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
894                            let s ≝ add_ticks1 s in
895                            let s ≝ set_program_counter … s (addr_of addr2 s) in
896                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
897                          else
898                            let s ≝ add_ticks2 s in
899                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
900                    ]
901            | DJNZ addr1 addr2 ⇒ λinstr_refl.
902              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
903              let s ≝ set_arg_8 … s addr1 result in
904                if ¬(eq_bv ? result (zero 8)) then
905                 let s ≝ add_ticks1 s in
906                  set_program_counter … s (addr_of addr2 s)
907                else
908                 let s ≝ add_ticks2 s in
909                  s
910            ] (refl … instr).
911    try (cases(other))
912    try assumption (*20s*)
913    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
914    try (
915      @(execute_1_technical … (subaddressing_modein …))
916      @I
917    ) (*66s*)
918    whd in match execute_1_preinstruction;
919    normalize nodelta %
920    [21,22,23,24: (* DIV *)
921     normalize nodelta in p;
922    |7,8,9,10,11,12,13,14,15,16, (* INC *)
923     71,72,73,74,75,76, (* CLR *)
924     77,78,79,80,81,82, (* CPL *)
925     99,100: (* PUSH *)
926      lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b
927    |93,94: (* MOV *)
928      cases addr * normalize nodelta
929       [1,2,4,5: * normalize nodelta
930        [1,2,4,5: * normalize nodelta
931         [1,2,4,5: * normalize nodelta
932          [1,2,4,5: * normalize nodelta ]]]]
933       #arg1 #arg2
934    |65,66, (* ANL *)
935     67,68, (* ORL *)
936     95,96: (* MOVX*)
937      cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta
938    |59,60: (* CJNE *)
939      cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta
940      cases (¬(eq_bv ???)) normalize nodelta
941    |69,70: (* XRL *)
942      cases addr normalize nodelta * #addr1 #addr2 normalize nodelta
943    ]
944    try (>p normalize nodelta
945         try (>p1 normalize nodelta
946              try (>p2 normalize nodelta
947                   try (>p3 normalize nodelta
948                        try (>p4 normalize nodelta
949                             try (>p5 normalize nodelta))))))
950    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
951    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
952    try (@or_introl //)
953    try (@or_intror //)
954    try #_
955    try /demod nohyps by clock_set_clock,clock_set_8051_sfr,set_arg_8_ok,set_arg_1_ok,
956                         program_counter_set_8051_sfr,program_counter_set_arg_1/
957    try (% @I) try (@or_introl % @I) try (@or_intror % @I) //
958qed.
959
960lemma execute_1_preinstruction_ok:
961 ∀ticks,a,m,cm,f,i,s.
962  (clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
963  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
964    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
965 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) //
966qed.
967
968discriminator Prod.
969
970definition compute_target_of_unconditional_jump:
971    ∀program_counter: Word.
972    ∀i: instruction.
973      Word ≝
974  λprogram_counter.
975  λi.
976    match i with
977    [ LJMP addr ⇒
978        match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
979        [ ADDR16 a ⇒ λaddr16: True. a
980        | _ ⇒ λother: False. ⊥
981        ] (subaddressing_modein … addr)
982    | SJMP addr ⇒
983        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
984        [ RELATIVE r ⇒ λrelative: True.
985          let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in
986            new_pc
987        | _ ⇒ λother: False. ⊥
988        ] (subaddressing_modein … addr)
989    | AJMP addr ⇒
990        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
991        [ ADDR11 a ⇒ λaddr11: True.
992          let 〈pc_bu, pc_bl〉 ≝ vsplit ? 5 11 program_counter in
993          let new_addr ≝ pc_bu @@ a in
994            new_addr
995        | _ ⇒ λother: False. ⊥
996        ] (subaddressing_modein … addr)
997    | _ ⇒ zero ?
998    ].
999  //
1000qed.
1001
1002definition is_unconditional_jump:
1003    instruction → bool ≝
1004  λi: instruction.
1005    match i with
1006    [ LJMP _ ⇒ true
1007    | SJMP _ ⇒ true
1008    | AJMP _ ⇒ true
1009    | _ ⇒ false
1010    ].
1011
1012definition program_counter_after_other ≝
1013  λprogram_counter. (* XXX: program counter after fetching *)
1014  λinstruction.
1015    if is_unconditional_jump instruction then
1016      compute_target_of_unconditional_jump program_counter instruction
1017    else
1018      program_counter.
1019
1020definition addr_of_relative ≝
1021 λM,cm. λx:[[relative]]. λs: PreStatus M cm.
1022  match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
1023   [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
1024   | _ ⇒ λabsd. ⊥
1025   ] (subaddressing_modein … x).
1026 @absd
1027qed.
1028
1029include alias "arithmetics/nat.ma".
1030include alias "ASM/BitVectorTrie.ma".
1031include alias "ASM/Vector.ma".
1032
1033definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
1034  Σs': Status cm.
1035    And (clock ?? s' = \snd current + clock … s)
1036      (ASM_classify0 (\fst (\fst current)) = cl_other →
1037        program_counter ? ? s' =
1038          program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝
1039  λcm,s0,instr_pc_ticks.
1040    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
1041    let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
1042    let s ≝ set_program_counter … s0 pc in
1043      match instr return λx. x = instr → Σs:?.? with
1044      [ MOVC addr1 addr2 ⇒ λinstr_refl.
1045          let s ≝ set_clock ?? s (ticks + clock … s) in
1046          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
1047            [ ACC_DPTR ⇒ λacc_dptr: True.
1048              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1049              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
1050              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
1051              let result ≝ lookup ? ? new_addr cm (zero ?) in
1052                set_8051_sfr … s SFR_ACC_A result
1053            | ACC_PC ⇒ λacc_pc: True.
1054              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1055              (* DPM: Under specified: does the carry from PC incrementation affect the *)
1056              (*      addition of the PC with the DPTR? At the moment, no.              *)
1057              let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
1058              let result ≝ lookup ? ? new_addr cm (zero ?) in
1059                set_8051_sfr … s SFR_ACC_A result
1060            | _ ⇒ λother: False. ⊥
1061            ] (subaddressing_modein … addr2)
1062      | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
1063          let s ≝ set_clock ?? s (ticks + clock … s) in
1064          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
1065          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1066          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
1067          let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
1068            set_program_counter … s new_pc
1069      | LJMP addr ⇒ λinstr_refl.
1070          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
1071          let s ≝ set_clock ?? s (ticks + clock … s) in
1072            set_program_counter … s new_pc
1073      | SJMP addr ⇒ λinstr_refl.
1074          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
1075          let s ≝ set_clock ?? s (ticks + clock … s) in
1076            set_program_counter … s new_pc
1077      | AJMP addr ⇒ λinstr_refl.
1078          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
1079          let s ≝ set_clock ?? s (ticks + clock … s) in
1080            set_program_counter … s new_pc
1081      | ACALL addr ⇒ λinstr_refl.
1082          let s ≝ set_clock ?? s (ticks + clock … s) in
1083          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
1084            [ ADDR11 a ⇒ λaddr11: True.
1085              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1086              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1087              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
1088              let s ≝ write_at_stack_pointer … s pc_bl in
1089              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1090              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1091              let s ≝ write_at_stack_pointer … s pc_bu in
1092              let 〈thr, eig〉 ≝ vsplit ? 3 8 a in
1093              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
1094              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
1095                set_program_counter … s new_addr
1096            | _ ⇒ λother: False. ⊥
1097            ] (subaddressing_modein … addr)
1098      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
1099      | LCALL addr ⇒ λinstr_refl.
1100          let s ≝ set_clock ?? s (ticks + clock … s) in
1101          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
1102            [ ADDR16 a ⇒ λaddr16: True.
1103              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1104              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1105              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
1106              let s ≝ write_at_stack_pointer … s pc_bl in
1107              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1108              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1109              let s ≝ write_at_stack_pointer … s pc_bu in
1110                set_program_counter … s a
1111            | _ ⇒ λother: False. ⊥
1112            ] (subaddressing_modein … addr)
1113        ] (refl … instr). (*10s*)
1114  try assumption
1115  [1,2,3,4,5,6,7,8:
1116    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
1117    try //
1118    -s destruct(INSTR_PC) <instr_refl whd
1119    try (#absurd normalize in absurd; try destruct(absurd) try %) %
1120  |9:
1121    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
1122        (λx. λs.
1123        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
1124        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
1125        | _ ⇒ λabsd. ⊥
1126        ] (subaddressing_modein … x)) instr' s) try @absd
1127    #clock_proof #classify_proof %
1128    [1:
1129      cases clock_proof #clock_proof' >clock_proof'
1130      destruct(INSTR_PC_TICKS) %
1131    |2:
1132      -clock_proof <INSTR_PC_TICKS normalize nodelta
1133      cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
1134      [1:
1135        destruct(INSTR_PC) /2/
1136      |2:
1137        * #hyp1 #hyp2 >hyp1 normalize nodelta
1138      <instr_refl normalize nodelta #hyp >classify_proof -classify_proof
1139      try assumption >hyp2 %
1140    ]
1141  ]
1142qed.
1143
1144definition current_instruction_cost ≝
1145  λcm.λs: Status cm.
1146    \snd (fetch cm (program_counter … s)).
1147
1148definition execute_1': ∀cm.∀s:Status cm.
1149  Σs':Status cm.
1150    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1151      And (clock ?? s' = current_instruction_cost cm s + clock … s)
1152        (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1153          program_counter ? ? s' =
1154            program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝
1155  λcm. λs: Status cm.
1156  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1157    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
1158  %
1159  [1:
1160    cases(execute_1_0 cm s instr_pc_ticks)
1161    #the_status * #clock_assm #_ @clock_assm
1162  |2:
1163    cases(execute_1_0 cm s instr_pc_ticks)
1164    #the_status * #_ #classify_assm
1165    assumption
1166  ]
1167qed.
1168
1169definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
1170
1171lemma execute_1_ok: ∀cm.∀s.
1172  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
1173    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1174      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1175        program_counter ? cm (execute_1 cm s) =
1176          program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
1177(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
1178  #cm #s normalize nodelta
1179  whd in match execute_1; normalize nodelta @pi2
1180qed.
1181
1182lemma execute_1_ok_clock:
1183  ∀cm.
1184  ∀s.
1185    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
1186  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
1187qed-.
1188
1189definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
1190  λticks,cm,s,instr,pc.
1191  let s ≝ set_program_counter ?? s pc in
1192  let s ≝
1193    match instr with
1194    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
1195    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
1196    | Cost cst ⇒ s
1197    | Jmp jmp ⇒
1198       let s ≝ set_clock … s (\fst ticks + clock … s) in
1199        set_program_counter … s (address_of_word_labels cm jmp)
1200    | Call call ⇒
1201      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1202      let a ≝ address_of_word_labels cm call in
1203      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1204      let s ≝ set_8051_sfr … s SFR_SP new_sp in
1205      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
1206      let s ≝ write_at_stack_pointer … s pc_bl in
1207      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1208      let s ≝ set_8051_sfr … s SFR_SP new_sp in
1209      let s ≝ write_at_stack_pointer … s pc_bu in
1210        set_program_counter … s a
1211    | Mov dptr ident ⇒
1212      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1213      let the_preamble ≝ \fst cm in
1214      let data_labels ≝ construct_datalabels the_preamble in
1215        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
1216    ]
1217  in
1218    s.
1219  normalize
1220  @I
1221qed.
1222
1223definition execute_1_pseudo_instruction:
1224 (Word → nat × nat) → ∀cm. ∀s:PseudoStatus cm.
1225   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
1226    PseudoStatus cm
1227
1228  λticks_of,cm,s,pc_ok.
1229  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
1230  let ticks ≝ ticks_of (program_counter … s) in
1231   execute_1_pseudo_instruction0 ticks cm s instr pc.
1232
1233let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
1234  match n with
1235    [ O ⇒ s
1236    | S o ⇒ execute o … (execute_1 … s)
1237    ].
1238
1239(* CSC: No way to have a total function because of function pointers call!
1240   The new pc after the execution can fall outside the program length.
1241   Luckily, this function is never actually used because we are only
1242   interested in structured traces.
1243let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
1244  match n with
1245    [ O ⇒ s
1246    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
1247    ].
1248*)
Note: See TracBrowser for help on using the repository browser.