source: src/ASM/Interpret.ma @ 2714

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

More progress in ASM towards implementing the new pseudoinstructions.

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