root/src/ASM/Interpret.ma

Revision 3101, 60.1 KB (checked in by mckinna, 6 weeks ago)

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