source: src/ASM/Interpret.ma @ 2168

Last change on this file since 2168 was 2160, checked in by mulligan, 7 years ago

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

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