source: src/ASM/Interpret.ma @ 2280

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

Proof repaired.

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