source: src/ASM/Interpret.ma @ 2051

Last change on this file since 2051 was 2051, checked in by mulligan, 7 years ago

Finished the Jmp case in the main theorem.

File size: 59.1 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: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝
1224  λticks_of,cm,s.
1225  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
1226  let ticks ≝ ticks_of (program_counter … s) in
1227   execute_1_pseudo_instruction0 ticks cm s instr pc.
1228
1229let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
1230  match n with
1231    [ O ⇒ s
1232    | S o ⇒ execute o … (execute_1 … s)
1233    ].
1234
1235let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
1236  match n with
1237    [ O ⇒ s
1238    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
1239    ].
Note: See TracBrowser for help on using the repository browser.