source: src/ASM/Interpret.ma @ 2762

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