source: src/ASM/Interpret.ma @ 2279

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