# source:src/ASM/Interpret.ma@1984

Last change on this file since 1984 was 1971, checked in by sacerdot, 8 years ago
1. Interpret.ma: we need to prove \sigma (execute_preinstruction s) = execute_preinstruction (\sigma s)

Thus execute_preinstruction cannot be defined using Russell.
Changed, but the proof of the properties still uses Russell
(with a trick...)

1. AssemblyProofSplit?: the preinstruction case of the main theorem moved to a main lemma which is also proved using the Russell trick. This seems very promising ATM.
File size: 69.9 KB
Line
1include "basics/lists/listb.ma".
2include "ASM/StatusProofs.ma".
3include "ASM/Fetch.ma".
4include "ASM/AbstractStatus.ma".
5
6definition sign_extension: Byte → Word ≝
7  λc.
8    let b ≝ get_index_v ? 8 c 1 ? in
9      [[ b; b; b; b; b; b; b; b ]] @@ c.
10  normalize
11  repeat (@le_S_S)
12  @le_O_n
13qed.
14
15lemma eq_a_to_eq:
16  ∀a,b.
17    eq_a a b = true → a = b.
18 #a #b
19 cases a cases b
20 #K
21 try cases (eq_true_false K)
22 %
23qed.
24
25lemma is_a_to_mem_to_is_in:
26 ∀he,a,m,q.
27   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
28 #he #a #m #q
29 elim q
30 [1:
31   #_ #K assumption
32 |2:
33   #m' #t #q' #II #H1 #H2
34   normalize
35   change with (orb ??) in H2:(??%?);
36   cases (inclusive_disjunction_true … H2)
37   [1:
38     #K
39     <(eq_a_to_eq … K) >H1 %
40   |2:
41     #K
42     >II
43     try assumption
44     cases (is_a t a)
45     normalize
46     %
47   ]
48 ]
49qed.
50
51lemma execute_1_technical:
52  ∀n, m: nat.
53  ∀v: Vector addressing_mode_tag (S n).
54  ∀q: Vector addressing_mode_tag (S m).
55  ∀a: addressing_mode.
56    bool_to_Prop (is_in ? v a) →
57    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
58    bool_to_Prop (is_in ? q a).
59 # n
60 # m
61 # v
62 # q
63 # a
64 elim v
65 [ normalize
66   # K
67   cases K
68 | # n'
69   # he
70   # tl
71   # II
72   whd in ⊢ (% → ? → ?);
73   lapply (refl … (is_in … (he:::tl) a))
74   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
75   [ # K
76     # _
77     normalize in K;
78     whd in ⊢ (% → ?);
79     lapply (refl … (subvector_with … eq_a (he:::tl) q));
80     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
81     [ # K1
82       # _
83       change with ((andb ? (subvector_with …)) = true) in K1;
84       cases (conjunction_true … K1)
85       # K3
86       # K4
87       cases (inclusive_disjunction_true … K)
88       # K2
89       [ > (is_a_to_mem_to_is_in … K2 K3)
90         %
91       | @ II
92         [ > K2
93           %
94         | > K4
95           %
96         ]
97       ]
98     | # K1
99       # K2
100       normalize in K2;
101       cases K2;
102     ]
103   | # K1
104     # K2
105     normalize in K2;
106     cases K2
107   ]
108 ]
109qed.
110
111include alias "arithmetics/nat.ma".
112include alias "ASM/BitVectorTrie.ma".
113
114definition execute_1_preinstruction:
115  ∀ticks: nat × nat.
116  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
117  ∀s: PreStatus m cm. PreStatus m cm ≝
118  λticks: nat × nat.
119  λa, m: Type[0]. λcm.
120  λaddr_of: a → PreStatus m cm → Word.
121  λinstr: preinstruction a.
122  λs: PreStatus m cm.
123  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
124  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
125  match instr in preinstruction return λx. x = instr → PreStatus m cm with
126        [ ADD addr1 addr2 ⇒ λinstr_refl.
127            let s ≝ add_ticks1 s in
128            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
129                                                   (get_arg_8 … s false addr2) false in
130            let cy_flag ≝ get_index' ? O  ? flags in
131            let ac_flag ≝ get_index' ? 1 ? flags in
132            let ov_flag ≝ get_index' ? 2 ? flags in
133            let s ≝ set_arg_8 … s ACC_A result in
134              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
135        | ADDC addr1 addr2 ⇒ λinstr_refl.
136            let s ≝ add_ticks1 s in
137            let old_cy_flag ≝ get_cy_flag ?? s in
138            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
139                                                   (get_arg_8 … s false addr2) old_cy_flag in
140            let cy_flag ≝ get_index' ? O ? flags in
141            let ac_flag ≝ get_index' ? 1 ? flags in
142            let ov_flag ≝ get_index' ? 2 ? flags in
143            let s ≝ set_arg_8 … s ACC_A result in
144              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
145        | SUBB addr1 addr2 ⇒ λinstr_refl.
146            let s ≝ add_ticks1 s in
147            let old_cy_flag ≝ get_cy_flag ?? s in
148            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
149                                                   (get_arg_8 … s false addr2) old_cy_flag in
150            let cy_flag ≝ get_index' ? O ? flags in
151            let ac_flag ≝ get_index' ? 1 ? flags in
152            let ov_flag ≝ get_index' ? 2 ? flags in
153            let s ≝ set_arg_8 … s ACC_A result in
154              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
155        | ANL addr ⇒ λinstr_refl.
156          let s ≝ add_ticks1 s in
157          match addr with
158            [ inl l ⇒
159              match l with
160                [ inl l' ⇒
161                  let 〈addr1, addr2〉 ≝ l' in
162                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
163                    set_arg_8 … s addr1 and_val
164                | inr r ⇒
165                  let 〈addr1, addr2〉 ≝ r in
166                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
167                    set_arg_8 … s addr1 and_val
168                ]
169            | inr r ⇒
170              let 〈addr1, addr2〉 ≝ r in
171              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
172               set_flags … s and_val (None ?) (get_ov_flag ?? s)
173            ]
174        | ORL addr ⇒ λinstr_refl.
175          let s ≝ add_ticks1 s in
176          match addr with
177            [ inl l ⇒
178              match l with
179                [ inl l' ⇒
180                  let 〈addr1, addr2〉 ≝ l' in
181                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
182                    set_arg_8 … s addr1 or_val
183                | inr r ⇒
184                  let 〈addr1, addr2〉 ≝ r in
185                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
186                    set_arg_8 … s addr1 or_val
187                ]
188            | inr r ⇒
189              let 〈addr1, addr2〉 ≝ r in
190              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
191               set_flags … s or_val (None ?) (get_ov_flag … s)
192            ]
193        | XRL addr ⇒ λinstr_refl.
194          let s ≝ add_ticks1 s in
195          match addr with
196            [ inl l' ⇒
197              let 〈addr1, addr2〉 ≝ l' in
198              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
199                set_arg_8 … s addr1 xor_val
200            | inr r ⇒
201              let 〈addr1, addr2〉 ≝ r in
202              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
203                set_arg_8 … s addr1 xor_val
204            ]
205        | INC addr ⇒ λinstr_refl.
206            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
207              [ ACC_A ⇒ λacc_a: True.
208                let s' ≝ add_ticks1 s in
209                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
210                 set_arg_8 … s' ACC_A result
211              | REGISTER r ⇒ λregister: True.
212                let s' ≝ add_ticks1 s in
213                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
214                 set_arg_8 … s' (REGISTER r) result
215              | DIRECT d ⇒ λdirect: True.
216                let s' ≝ add_ticks1 s in
217                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
218                 set_arg_8 … s' (DIRECT d) result
219              | INDIRECT i ⇒ λindirect: True.
220                let s' ≝ add_ticks1 s in
221                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
222                 set_arg_8 … s' (INDIRECT i) result
223              | DPTR ⇒ λdptr: True.
224                let s' ≝ add_ticks1 s in
225                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
226                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
227                let s ≝ set_8051_sfr … s' SFR_DPL bl in
228                 set_8051_sfr … s' SFR_DPH bu
229              | _ ⇒ λother: False. ⊥
230              ] (subaddressing_modein … addr)
231        | NOP ⇒ λinstr_refl.
232           let s ≝ add_ticks2 s in
233            s
234        | DEC addr ⇒ λinstr_refl.
235           let s ≝ add_ticks1 s in
236           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
237             set_arg_8 … s addr result
238        | MUL addr1 addr2 ⇒ λinstr_refl.
239           let s ≝ add_ticks1 s in
240           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
241           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
242           let product ≝ acc_a_nat * acc_b_nat in
243           let ov_flag ≝ product ≥ 256 in
244           let low ≝ bitvector_of_nat 8 (product mod 256) in
245           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
246           let s ≝ set_8051_sfr … s SFR_ACC_A low in
247             set_8051_sfr … s SFR_ACC_B high
248        | DIV addr1 addr2 ⇒ λinstr_refl.
249           let s ≝ add_ticks1 s in
250           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
251           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
252             match acc_b_nat with
253               [ O ⇒ set_flags … s false (None Bit) true
254               | S o ⇒
255                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
256                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
257                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
258                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
259                   set_flags … s false (None Bit) false
260               ]
261        | DA addr ⇒ λinstr_refl.
262            let s ≝ add_ticks1 s in
263            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
264              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
265                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
266                let cy_flag ≝ get_index' ? O ? flags in
267                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
268                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
269                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
270                    let new_acc ≝ nu @@ acc_nl' in
271                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
272                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
273                  else
274                    s
275              else
276                s
277        | CLR addr ⇒ λinstr_refl.
278          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
279            [ ACC_A ⇒ λacc_a: True.
280              let s ≝ add_ticks1 s in
281               set_arg_8 … s ACC_A (zero 8)
282            | CARRY ⇒ λcarry: True.
283              let s ≝ add_ticks1 s in
284               set_arg_1 … s CARRY false
285            | BIT_ADDR b ⇒ λbit_addr: True.
286              let s ≝ add_ticks1 s in
287               set_arg_1 … s (BIT_ADDR b) false
288            | _ ⇒ λother: False. ⊥
289            ] (subaddressing_modein … addr)
290        | CPL addr ⇒ λinstr_refl.
291          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
292            [ ACC_A ⇒ λacc_a: True.
293                let s ≝ add_ticks1 s in
294                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
295                let new_acc ≝ negation_bv ? old_acc in
296                 set_8051_sfr … s SFR_ACC_A new_acc
297            | CARRY ⇒ λcarry: True.
298                let s ≝ add_ticks1 s in
299                let old_cy_flag ≝ get_arg_1 … s CARRY true in
300                let new_cy_flag ≝ ¬old_cy_flag in
301                 set_arg_1 … s CARRY new_cy_flag
302            | BIT_ADDR b ⇒ λbit_addr: True.
303                let s ≝ add_ticks1 s in
304                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
305                let new_bit ≝ ¬old_bit in
306                 set_arg_1 … s (BIT_ADDR b) new_bit
307            | _ ⇒ λother: False. ?
308            ] (subaddressing_modein … addr)
309        | SETB b ⇒ λinstr_refl.
310            let s ≝ add_ticks1 s in
311            set_arg_1 … s b false
312        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
313            let s ≝ add_ticks1 s in
314            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
315            let new_acc ≝ rotate_left … 1 old_acc in
316              set_8051_sfr … s SFR_ACC_A new_acc
317        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
318            let s ≝ add_ticks1 s in
319            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
320            let new_acc ≝ rotate_right … 1 old_acc in
321              set_8051_sfr … s SFR_ACC_A new_acc
322        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
323            let s ≝ add_ticks1 s in
324            let old_cy_flag ≝ get_cy_flag ?? s in
325            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
326            let new_cy_flag ≝ get_index' ? O ? old_acc in
327            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
328            let s ≝ set_arg_1 … s CARRY new_cy_flag in
329              set_8051_sfr … s SFR_ACC_A new_acc
330        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
331            let s ≝ add_ticks1 s in
332            let old_cy_flag ≝ get_cy_flag ?? s in
333            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
334            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
335            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
336            let s ≝ set_arg_1 … s CARRY new_cy_flag in
337              set_8051_sfr … s SFR_ACC_A new_acc
338        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
339            let s ≝ add_ticks1 s in
340            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
341            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
342            let new_acc ≝ nl @@ nu in
343              set_8051_sfr … s SFR_ACC_A new_acc
344        | PUSH addr ⇒ λinstr_refl.
345            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
346              [ DIRECT d ⇒ λdirect: True.
347                let s ≝ add_ticks1 s in
348                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
349                let s ≝ set_8051_sfr … s SFR_SP new_sp in
350                  write_at_stack_pointer … s d
351              | _ ⇒ λother: False. ⊥
352              ] (subaddressing_modein … addr)
353        | POP addr ⇒ λinstr_refl.
354            let s ≝ add_ticks1 s in
355            let contents ≝ read_at_stack_pointer ?? s in
356            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
357            let s ≝ set_8051_sfr … s SFR_SP new_sp in
358              set_arg_8 … s addr contents
359        | XCH addr1 addr2 ⇒ λinstr_refl.
360            let s ≝ add_ticks1 s in
361            let old_addr ≝ get_arg_8 … s false addr2 in
362            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
363            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
364              set_arg_8 … s addr2 old_acc
365        | XCHD addr1 addr2 ⇒ λinstr_refl.
366            let s ≝ add_ticks1 s in
367            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
368            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
369            let new_acc ≝ acc_nu @@ arg_nl in
370            let new_arg ≝ arg_nu @@ acc_nl in
371            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
372              set_arg_8 … s addr2 new_arg
373        | RET ⇒ λinstr_refl.
374            let s ≝ add_ticks1 s in
375            let high_bits ≝ read_at_stack_pointer ?? s in
376            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
377            let s ≝ set_8051_sfr … s SFR_SP new_sp in
378            let low_bits ≝ read_at_stack_pointer ?? s in
379            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
380            let s ≝ set_8051_sfr … s SFR_SP new_sp in
381            let new_pc ≝ high_bits @@ low_bits in
382              set_program_counter … s new_pc
383        | RETI ⇒ λinstr_refl.
384            let s ≝ add_ticks1 s in
385            let high_bits ≝ read_at_stack_pointer ?? s in
386            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
387            let s ≝ set_8051_sfr … s SFR_SP new_sp in
388            let low_bits ≝ read_at_stack_pointer ?? s in
389            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
390            let s ≝ set_8051_sfr … s SFR_SP new_sp in
391            let new_pc ≝ high_bits @@ low_bits in
392              set_program_counter … s new_pc
393        | MOVX addr ⇒ λinstr_refl.
394          let s ≝ add_ticks1 s in
395          (* DPM: only copies --- doesn't affect I/O *)
396          match addr with
397            [ inl l ⇒
398              let 〈addr1, addr2〉 ≝ l in
399                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
400            | inr r ⇒
401              let 〈addr1, addr2〉 ≝ r in
402                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
403            ]
404        | MOV addr ⇒ λinstr_refl.
405          let s ≝ add_ticks1 s in
406          match addr with
407            [ inl l ⇒
408              match l with
409                [ inl l' ⇒
410                  match l' with
411                    [ inl l'' ⇒
412                      match l'' with
413                        [ inl l''' ⇒
414                          match l''' with
415                            [ inl l'''' ⇒
416                              let 〈addr1, addr2〉 ≝ l'''' in
417                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
418                            | inr r'''' ⇒
419                              let 〈addr1, addr2〉 ≝ r'''' in
420                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
421                            ]
422                        | inr r''' ⇒
423                          let 〈addr1, addr2〉 ≝ r''' in
424                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
425                        ]
426                    | inr r'' ⇒
427                      let 〈addr1, addr2〉 ≝ r'' in
428                       set_arg_16 … s (get_arg_16 … s addr2) addr1
429                    ]
430                | inr r ⇒
431                  let 〈addr1, addr2〉 ≝ r in
432                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
433                ]
434            | inr r ⇒
435              let 〈addr1, addr2〉 ≝ r in
436               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
437            ]
438          | JC addr ⇒ λinstr_refl.
439                  if get_cy_flag ?? s then
440                    let s ≝ add_ticks1 s in
441                      set_program_counter … s (addr_of addr s)
442                  else
443                    let s ≝ add_ticks2 s in
444                      s
445            | JNC addr ⇒ λinstr_refl.
446                  if ¬(get_cy_flag ?? s) then
447                   let s ≝ add_ticks1 s in
448                     set_program_counter … s (addr_of addr s)
449                  else
450                   let s ≝ add_ticks2 s in
451                    s
452            | JB addr1 addr2 ⇒ λinstr_refl.
453                  if get_arg_1 … s addr1 false then
454                   let s ≝ add_ticks1 s in
455                    set_program_counter … s (addr_of addr2 s)
456                  else
457                   let s ≝ add_ticks2 s in
458                    s
459            | JNB addr1 addr2 ⇒ λinstr_refl.
460                  if ¬(get_arg_1 … s addr1 false) then
461                   let s ≝ add_ticks1 s in
462                    set_program_counter … s (addr_of addr2 s)
463                  else
464                   let s ≝ add_ticks2 s in
465                    s
466            | JBC addr1 addr2 ⇒ λinstr_refl.
467                  let s ≝ set_arg_1 … s addr1 false in
468                    if get_arg_1 … s addr1 false then
469                     let s ≝ add_ticks1 s in
470                      set_program_counter … s (addr_of addr2 s)
471                    else
472                     let s ≝ add_ticks2 s in
473                      s
474            | JZ addr ⇒ λinstr_refl.
475                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
476                     let s ≝ add_ticks1 s in
477                      set_program_counter … s (addr_of addr s)
478                    else
479                     let s ≝ add_ticks2 s in
480                      s
481            | JNZ addr ⇒ λinstr_refl.
482                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
483                     let s ≝ add_ticks1 s in
484                      set_program_counter … s (addr_of addr s)
485                    else
486                     let s ≝ add_ticks2 s in
487                      s
488            | CJNE addr1 addr2 ⇒ λinstr_refl.
489                  match addr1 with
490                    [ inl l ⇒
491                        let 〈addr1, addr2'〉 ≝ l in
492                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
493                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
494                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
495                            let s ≝ add_ticks1 s in
496                            let s ≝ set_program_counter … s (addr_of addr2 s) in
497                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
498                          else
499                            let s ≝ add_ticks2 s in
500                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
501                    | inr r' ⇒
502                        let 〈addr1, addr2'〉 ≝ r' in
503                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
504                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
505                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
506                            let s ≝ add_ticks1 s in
507                            let s ≝ set_program_counter … s (addr_of addr2 s) in
508                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
509                          else
510                            let s ≝ add_ticks2 s in
511                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
512                    ]
513            | DJNZ addr1 addr2 ⇒ λinstr_refl.
514              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
515              let s ≝ set_arg_8 … s addr1 result in
516                if ¬(eq_bv ? result (zero 8)) then
517                 let s ≝ add_ticks1 s in
518                  set_program_counter … s (addr_of addr2 s)
519                else
520                 let s ≝ add_ticks2 s in
521                  s
522            ] (refl … instr).
523    try (cases(other))
524    try assumption (*20s*)
525    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
526    try (
527      @(execute_1_technical … (subaddressing_modein …))
528      @I
529    ) (*66s*)
530qed.
531
532definition execute_1_preinstruction_ok':
533  ∀ticks: nat × nat.
534  ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a.
535  ∀s: PreStatus m cm.
536    Σs': PreStatus m cm.
537      (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in
538      (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
539        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝
540  λticks: nat × nat.
541  λa, m: Type[0]. λcm.
542  λaddr_of: a → PreStatus m cm → Word.
543  λinstr: preinstruction a.
544  λs: PreStatus m cm.
545  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
546  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
547  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
548    ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
549      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with
550        [ ADD addr1 addr2 ⇒ λinstr_refl.
551            let s ≝ add_ticks1 s in
552            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
553                                                   (get_arg_8 … s false addr2) false in
554            let cy_flag ≝ get_index' ? O  ? flags in
555            let ac_flag ≝ get_index' ? 1 ? flags in
556            let ov_flag ≝ get_index' ? 2 ? flags in
557            let s ≝ set_arg_8 … s ACC_A result in
558              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
559        | ADDC addr1 addr2 ⇒ λinstr_refl.
560            let s ≝ add_ticks1 s in
561            let old_cy_flag ≝ get_cy_flag ?? s in
562            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
563                                                   (get_arg_8 … s false addr2) old_cy_flag in
564            let cy_flag ≝ get_index' ? O ? flags in
565            let ac_flag ≝ get_index' ? 1 ? flags in
566            let ov_flag ≝ get_index' ? 2 ? flags in
567            let s ≝ set_arg_8 … s ACC_A result in
568              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
569        | SUBB addr1 addr2 ⇒ λinstr_refl.
570            let s ≝ add_ticks1 s in
571            let old_cy_flag ≝ get_cy_flag ?? s in
572            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
573                                                   (get_arg_8 … s false addr2) old_cy_flag in
574            let cy_flag ≝ get_index' ? O ? flags in
575            let ac_flag ≝ get_index' ? 1 ? flags in
576            let ov_flag ≝ get_index' ? 2 ? flags in
577            let s ≝ set_arg_8 … s ACC_A result in
578              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
579        | ANL addr ⇒ λinstr_refl.
580          let s ≝ add_ticks1 s in
581          match addr with
582            [ inl l ⇒
583              match l with
584                [ inl l' ⇒
585                  let 〈addr1, addr2〉 ≝ l' in
586                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
587                    set_arg_8 … s addr1 and_val
588                | inr r ⇒
589                  let 〈addr1, addr2〉 ≝ r in
590                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
591                    set_arg_8 … s addr1 and_val
592                ]
593            | inr r ⇒
594              let 〈addr1, addr2〉 ≝ r in
595              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
596               set_flags … s and_val (None ?) (get_ov_flag ?? s)
597            ]
598        | ORL addr ⇒ λinstr_refl.
599          let s ≝ add_ticks1 s in
600          match addr with
601            [ inl l ⇒
602              match l with
603                [ inl l' ⇒
604                  let 〈addr1, addr2〉 ≝ l' in
605                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
606                    set_arg_8 … s addr1 or_val
607                | inr r ⇒
608                  let 〈addr1, addr2〉 ≝ r in
609                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
610                    set_arg_8 … s addr1 or_val
611                ]
612            | inr r ⇒
613              let 〈addr1, addr2〉 ≝ r in
614              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
615               set_flags … s or_val (None ?) (get_ov_flag … s)
616            ]
617        | XRL addr ⇒ λinstr_refl.
618          let s ≝ add_ticks1 s in
619          match addr with
620            [ inl l' ⇒
621              let 〈addr1, addr2〉 ≝ l' in
622              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
623                set_arg_8 … s addr1 xor_val
624            | inr r ⇒
625              let 〈addr1, addr2〉 ≝ r in
626              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
627                set_arg_8 … s addr1 xor_val
628            ]
629        | INC addr ⇒ λinstr_refl.
630            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with
631              [ ACC_A ⇒ λacc_a: True. λEQaddr.
632                let s' ≝ add_ticks1 s in
633                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
634                 set_arg_8 … s' ACC_A result
635              | REGISTER r ⇒ λregister: True. λEQaddr.
636                let s' ≝ add_ticks1 s in
637                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
638                 set_arg_8 … s' (REGISTER r) result
639              | DIRECT d ⇒ λdirect: True. λEQaddr.
640                let s' ≝ add_ticks1 s in
641                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
642                 set_arg_8 … s' (DIRECT d) result
643              | INDIRECT i ⇒ λindirect: True. λEQaddr.
644                let s' ≝ add_ticks1 s in
645                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
646                 set_arg_8 … s' (INDIRECT i) result
647              | DPTR ⇒ λdptr: True. λEQaddr.
648                let s' ≝ add_ticks1 s in
649                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
650                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
651                let s ≝ set_8051_sfr … s' SFR_DPL bl in
652                 set_8051_sfr … s' SFR_DPH bu
653              | _ ⇒ λother: False. ⊥
654              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
655        | NOP ⇒ λinstr_refl.
656           let s ≝ add_ticks2 s in
657            s
658        | DEC addr ⇒ λinstr_refl.
659           let s ≝ add_ticks1 s in
660           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
661             set_arg_8 … s addr result
662        | MUL addr1 addr2 ⇒ λinstr_refl.
663           let s ≝ add_ticks1 s in
664           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
665           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
666           let product ≝ acc_a_nat * acc_b_nat in
667           let ov_flag ≝ product ≥ 256 in
668           let low ≝ bitvector_of_nat 8 (product mod 256) in
669           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
670           let s ≝ set_8051_sfr … s SFR_ACC_A low in
671             set_8051_sfr … s SFR_ACC_B high
672        | DIV addr1 addr2 ⇒ λinstr_refl.
673           let s ≝ add_ticks1 s in
674           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
675           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
676             match acc_b_nat with
677               [ O ⇒ set_flags … s false (None Bit) true
678               | S o ⇒
679                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
680                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
681                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
682                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
683                   set_flags … s false (None Bit) false
684               ]
685        | DA addr ⇒ λinstr_refl.
686            let s ≝ add_ticks1 s in
687            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
688              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
689                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
690                let cy_flag ≝ get_index' ? O ? flags in
691                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
692                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
693                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
694                    let new_acc ≝ nu @@ acc_nl' in
695                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
696                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
697                  else
698                    s
699              else
700                s
701        | CLR addr ⇒ λinstr_refl.
702          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
703            [ ACC_A ⇒ λacc_a: True. λEQaddr.
704              let s ≝ add_ticks1 s in
705               set_arg_8 … s ACC_A (zero 8)
706            | CARRY ⇒ λcarry: True. λEQaddr.
707              let s ≝ add_ticks1 s in
708               set_arg_1 … s CARRY false
709            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
710              let s ≝ add_ticks1 s in
711               set_arg_1 … s (BIT_ADDR b) false
712            | _ ⇒ λother: False. ⊥
713            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
714        | CPL addr ⇒ λinstr_refl.
715          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
716            [ ACC_A ⇒ λacc_a: True. λEQaddr.
717                let s ≝ add_ticks1 s in
718                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
719                let new_acc ≝ negation_bv ? old_acc in
720                 set_8051_sfr … s SFR_ACC_A new_acc
721            | CARRY ⇒ λcarry: True. λEQaddr.
722                let s ≝ add_ticks1 s in
723                let old_cy_flag ≝ get_arg_1 … s CARRY true in
724                let new_cy_flag ≝ ¬old_cy_flag in
725                 set_arg_1 … s CARRY new_cy_flag
726            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
727                let s ≝ add_ticks1 s in
728                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
729                let new_bit ≝ ¬old_bit in
730                 set_arg_1 … s (BIT_ADDR b) new_bit
731            | _ ⇒ λother: False. ?
732            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
733        | SETB b ⇒ λinstr_refl.
734            let s ≝ add_ticks1 s in
735            set_arg_1 … s b false
736        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
737            let s ≝ add_ticks1 s in
738            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
739            let new_acc ≝ rotate_left … 1 old_acc in
740              set_8051_sfr … s SFR_ACC_A new_acc
741        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
742            let s ≝ add_ticks1 s in
743            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
744            let new_acc ≝ rotate_right … 1 old_acc in
745              set_8051_sfr … s SFR_ACC_A new_acc
746        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
747            let s ≝ add_ticks1 s in
748            let old_cy_flag ≝ get_cy_flag ?? s in
749            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
750            let new_cy_flag ≝ get_index' ? O ? old_acc in
751            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
752            let s ≝ set_arg_1 … s CARRY new_cy_flag in
753              set_8051_sfr … s SFR_ACC_A new_acc
754        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
755            let s ≝ add_ticks1 s in
756            let old_cy_flag ≝ get_cy_flag ?? s in
757            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
758            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
759            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
760            let s ≝ set_arg_1 … s CARRY new_cy_flag in
761              set_8051_sfr … s SFR_ACC_A new_acc
762        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
763            let s ≝ add_ticks1 s in
764            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
765            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
766            let new_acc ≝ nl @@ nu in
767              set_8051_sfr … s SFR_ACC_A new_acc
768        | PUSH addr ⇒ λinstr_refl.
769            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with
770              [ DIRECT d ⇒ λdirect: True. λEQaddr.
771                let s ≝ add_ticks1 s in
772                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
773                let s ≝ set_8051_sfr … s SFR_SP new_sp in
774                  write_at_stack_pointer … s d
775              | _ ⇒ λother: False. ⊥
776              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
777        | POP addr ⇒ λinstr_refl.
778            let s ≝ add_ticks1 s in
779            let contents ≝ read_at_stack_pointer ?? s in
780            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
781            let s ≝ set_8051_sfr … s SFR_SP new_sp in
782              set_arg_8 … s addr contents
783        | XCH addr1 addr2 ⇒ λinstr_refl.
784            let s ≝ add_ticks1 s in
785            let old_addr ≝ get_arg_8 … s false addr2 in
786            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
787            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
788              set_arg_8 … s addr2 old_acc
789        | XCHD addr1 addr2 ⇒ λinstr_refl.
790            let s ≝ add_ticks1 s in
791            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
792            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
793            let new_acc ≝ acc_nu @@ arg_nl in
794            let new_arg ≝ arg_nu @@ acc_nl in
795            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
796              set_arg_8 … s addr2 new_arg
797        | RET ⇒ λinstr_refl.
798            let s ≝ add_ticks1 s in
799            let high_bits ≝ read_at_stack_pointer ?? s in
800            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
801            let s ≝ set_8051_sfr … s SFR_SP new_sp in
802            let low_bits ≝ read_at_stack_pointer ?? s in
803            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
804            let s ≝ set_8051_sfr … s SFR_SP new_sp in
805            let new_pc ≝ high_bits @@ low_bits in
806              set_program_counter … s new_pc
807        | RETI ⇒ λinstr_refl.
808            let s ≝ add_ticks1 s in
809            let high_bits ≝ read_at_stack_pointer ?? s in
810            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
811            let s ≝ set_8051_sfr … s SFR_SP new_sp in
812            let low_bits ≝ read_at_stack_pointer ?? s in
813            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
814            let s ≝ set_8051_sfr … s SFR_SP new_sp in
815            let new_pc ≝ high_bits @@ low_bits in
816              set_program_counter … s new_pc
817        | MOVX addr ⇒ λinstr_refl.
818          let s ≝ add_ticks1 s in
819          (* DPM: only copies --- doesn't affect I/O *)
820          match addr with
821            [ inl l ⇒
822              let 〈addr1, addr2〉 ≝ l in
823                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
824            | inr r ⇒
825              let 〈addr1, addr2〉 ≝ r in
826                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
827            ]
828        | MOV addr ⇒ λinstr_refl.
829          let s ≝ add_ticks1 s in
830          match addr with
831            [ inl l ⇒
832              match l with
833                [ inl l' ⇒
834                  match l' with
835                    [ inl l'' ⇒
836                      match l'' with
837                        [ inl l''' ⇒
838                          match l''' with
839                            [ inl l'''' ⇒
840                              let 〈addr1, addr2〉 ≝ l'''' in
841                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
842                            | inr r'''' ⇒
843                              let 〈addr1, addr2〉 ≝ r'''' in
844                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
845                            ]
846                        | inr r''' ⇒
847                          let 〈addr1, addr2〉 ≝ r''' in
848                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
849                        ]
850                    | inr r'' ⇒
851                      let 〈addr1, addr2〉 ≝ r'' in
852                       set_arg_16 … s (get_arg_16 … s addr2) addr1
853                    ]
854                | inr r ⇒
855                  let 〈addr1, addr2〉 ≝ r in
856                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
857                ]
858            | inr r ⇒
859              let 〈addr1, addr2〉 ≝ r in
860               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
861            ]
862          | JC addr ⇒ λinstr_refl.
863                  if get_cy_flag ?? s then
864                    let s ≝ add_ticks1 s in
865                      set_program_counter … s (addr_of addr s)
866                  else
867                    let s ≝ add_ticks2 s in
868                      s
869            | JNC addr ⇒ λinstr_refl.
870                  if ¬(get_cy_flag ?? s) then
871                   let s ≝ add_ticks1 s in
872                     set_program_counter … s (addr_of addr s)
873                  else
874                   let s ≝ add_ticks2 s in
875                    s
876            | JB addr1 addr2 ⇒ λinstr_refl.
877                  if get_arg_1 … s addr1 false then
878                   let s ≝ add_ticks1 s in
879                    set_program_counter … s (addr_of addr2 s)
880                  else
881                   let s ≝ add_ticks2 s in
882                    s
883            | JNB addr1 addr2 ⇒ λinstr_refl.
884                  if ¬(get_arg_1 … s addr1 false) then
885                   let s ≝ add_ticks1 s in
886                    set_program_counter … s (addr_of addr2 s)
887                  else
888                   let s ≝ add_ticks2 s in
889                    s
890            | JBC addr1 addr2 ⇒ λinstr_refl.
891                  let s ≝ set_arg_1 … s addr1 false in
892                    if get_arg_1 … s addr1 false then
893                     let s ≝ add_ticks1 s in
894                      set_program_counter … s (addr_of addr2 s)
895                    else
896                     let s ≝ add_ticks2 s in
897                      s
898            | JZ addr ⇒ λinstr_refl.
899                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
900                     let s ≝ add_ticks1 s in
901                      set_program_counter … s (addr_of addr s)
902                    else
903                     let s ≝ add_ticks2 s in
904                      s
905            | JNZ addr ⇒ λinstr_refl.
906                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
907                     let s ≝ add_ticks1 s in
908                      set_program_counter … s (addr_of addr s)
909                    else
910                     let s ≝ add_ticks2 s in
911                      s
912            | CJNE addr1 addr2 ⇒ λinstr_refl.
913                  match addr1 with
914                    [ inl l ⇒
915                        let 〈addr1, addr2'〉 ≝ l in
916                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
917                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
918                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
919                            let s ≝ add_ticks1 s in
920                            let s ≝ set_program_counter … s (addr_of addr2 s) in
921                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
922                          else
923                            let s ≝ add_ticks2 s in
924                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
925                    | inr r' ⇒
926                        let 〈addr1, addr2'〉 ≝ r' in
927                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
928                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
929                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
930                            let s ≝ add_ticks1 s in
931                            let s ≝ set_program_counter … s (addr_of addr2 s) in
932                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
933                          else
934                            let s ≝ add_ticks2 s in
935                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
936                    ]
937            | DJNZ addr1 addr2 ⇒ λinstr_refl.
938              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
939              let s ≝ set_arg_8 … s addr1 result in
940                if ¬(eq_bv ? result (zero 8)) then
941                 let s ≝ add_ticks1 s in
942                  set_program_counter … s (addr_of addr2 s)
943                else
944                 let s ≝ add_ticks2 s in
945                  s
946            ] (refl … instr).
947    try (cases(other))
948    try assumption (*20s*)
949    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
950    try (
951      @(execute_1_technical … (subaddressing_modein …))
952      @I
953    ) (*66s*)
954    whd in match execute_1_preinstruction;
955    normalize nodelta %
956    [21,22,23,24: (* DIV *)
957     normalize nodelta in p;
958    |7,8,9,10,11,12,13,14,15,16, (* INC *)
959     71,72,73,74,75,76, (* CLR *)
960     77,78,79,80,81,82, (* CPL *)
961     99,100: (* PUSH *)
962      lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b
963    |93,94: (* MOV *)
964      cases addr * normalize nodelta
965       [1,2,4,5: * normalize nodelta
966        [1,2,4,5: * normalize nodelta
967         [1,2,4,5: * normalize nodelta
968          [1,2,4,5: * normalize nodelta ]]]]
969       #arg1 #arg2
970    |65,66, (* ANL *)
971     67,68, (* ORL *)
972     95,96: (* MOVX*)
973      cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta
974    |59,60: (* CJNE *)
975      cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta
976      cases (¬(eq_bv ???)) normalize nodelta
977    |69,70: (* XRL *)
978      cases addr normalize nodelta * #addr1 #addr2 normalize nodelta
979    ]
980    try (>p normalize nodelta
981         try (>p1 normalize nodelta
982              try (>p2 normalize nodelta
983                   try (>p3 normalize nodelta
984                        try (>p4 normalize nodelta
985                             try (>p5 normalize nodelta))))))
986    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
987    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
988    try (@or_introl //)
989    try (@or_intror //)
990    try (#_ /demod/ %)
991    try (#_ //)
992    [ <set_arg_8_ok @or_introl //
993    |*: <set_arg_1_ok @or_introl // ]
994qed.
995
996lemma execute_1_preinstruction_ok:
997 ∀ticks,a,m,cm,f,i,s.
998  (clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
999  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
1000    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
1001 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) //
1002qed.
1003
1004discriminator Prod.
1005
1006definition compute_target_of_unconditional_jump:
1007    ∀program_counter: Word.
1008    ∀i: instruction.
1009      Word ≝
1010  λprogram_counter.
1011  λi.
1012    match i with
1013    [ LJMP addr ⇒
1014        match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
1015        [ ADDR16 a ⇒ λaddr16: True. a
1016        | _ ⇒ λother: False. ⊥
1017        ] (subaddressing_modein … addr)
1018    | SJMP addr ⇒
1019        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
1020        [ RELATIVE r ⇒ λrelative: True.
1021          let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in
1022            new_pc
1023        | _ ⇒ λother: False. ⊥
1024        ] (subaddressing_modein … addr)
1025    | AJMP addr ⇒
1026        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
1027        [ ADDR11 a ⇒ λaddr11: True.
1028          let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in
1029          let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
1030          let bit ≝ get_index' ? O ? nl in
1031          let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
1032          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
1033          let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
1034            new_pc
1035        | _ ⇒ λother: False. ⊥
1036        ] (subaddressing_modein … addr)
1037    | _ ⇒ zero ?
1038    ].
1039  //
1040qed.
1041
1042definition is_unconditional_jump:
1043    instruction → bool ≝
1044  λi: instruction.
1045    match i with
1046    [ LJMP _ ⇒ true
1047    | SJMP _ ⇒ true
1048    | AJMP _ ⇒ true
1049    | _ ⇒ false
1050    ].
1051
1052let rec member_addressing_mode_tag
1053  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
1054    on v: Prop ≝
1055  match v with
1056  [ VEmpty ⇒ False
1057  | VCons n' hd tl ⇒
1058      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
1059  ].
1060
1061lemma is_a_decidable:
1062  ∀hd.
1063  ∀element.
1064    is_a hd element = true ∨ is_a hd element = false.
1065  #hd #element //
1066qed.
1067
1068lemma mem_decidable:
1069  ∀n: nat.
1070  ∀v: Vector addressing_mode_tag n.
1071  ∀element: addressing_mode_tag.
1072    mem … eq_a n v element = true ∨
1073      mem … eq_a … v element = false.
1074  #n #v #element //
1075qed.
1076
1077lemma eq_a_elim:
1078  ∀tag.
1079  ∀hd.
1080  ∀P: bool → Prop.
1081    (tag = hd → P (true)) →
1082      (tag ≠ hd → P (false)) →
1083        P (eq_a tag hd).
1084  #tag #hd #P
1085  cases tag
1086  cases hd
1087  #true_hyp #false_hyp
1088  try @false_hyp
1089  try @true_hyp
1090  try %
1091  #absurd destruct(absurd)
1092qed.
1093
1094lemma is_a_true_to_is_in:
1095  ∀n: nat.
1096  ∀x: addressing_mode.
1097  ∀tag: addressing_mode_tag.
1098  ∀supervector: Vector addressing_mode_tag n.
1099  mem addressing_mode_tag eq_a n supervector tag →
1100    is_a tag x = true →
1101      is_in … supervector x.
1102  #n #x #tag #supervector
1103  elim supervector
1104  [1:
1105    #absurd cases absurd
1106  |2:
1107    #n' #hd #tl #inductive_hypothesis
1108    whd in match (mem … eq_a (S n') (hd:::tl) tag);
1109    @eq_a_elim normalize nodelta
1110    [1:
1111      #tag_hd_eq #irrelevant
1112      whd in match (is_in (S n') (hd:::tl) x);
1113      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
1114      @I
1115    |2:
1116      #tag_hd_neq
1117      whd in match (is_in (S n') (hd:::tl) x);
1118      change with (
1119        mem … eq_a n' tl tag)
1120          in match (fold_right … n' ? false tl);
1121      #mem_hyp #is_a_hyp
1122      cases(is_a hd x)
1123      [1:
1124        normalize nodelta //
1125      |2:
1126        normalize nodelta
1127        @inductive_hypothesis assumption
1128      ]
1129    ]
1130  ]
1131qed.
1132
1133lemma is_in_subvector_is_in_supervector:
1134  ∀m, n: nat.
1135  ∀subvector: Vector addressing_mode_tag m.
1136  ∀supervector: Vector addressing_mode_tag n.
1137  ∀element: addressing_mode.
1138    subvector_with … eq_a subvector supervector →
1139      is_in m subvector element → is_in n supervector element.
1140  #m #n #subvector #supervector #element
1141  elim subvector
1142  [1:
1143    #subvector_with_proof #is_in_proof
1144    cases is_in_proof
1145  |2:
1146    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
1147    whd in match (is_in … (hd':::tl') element);
1148    cases (is_a_decidable hd' element)
1149    [1:
1150      #is_a_true >is_a_true
1151      #irrelevant
1152      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
1153      @(is_a_true_to_is_in … is_a_true)
1154      lapply(subvector_with_proof)
1155      cases(mem … eq_a n supervector hd') //
1156    |2:
1157      #is_a_false >is_a_false normalize nodelta
1158      #assm
1159      @inductive_hypothesis
1160      [1:
1161        generalize in match subvector_with_proof;
1162        whd in match (subvector_with … eq_a (hd':::tl') supervector);
1163        cases(mem_decidable n supervector hd')
1164        [1:
1165          #mem_true >mem_true normalize nodelta
1166          #assm assumption
1167        |2:
1168          #mem_false >mem_false #absurd
1169          cases absurd
1170        ]
1171      |2:
1172        assumption
1173      ]
1174    ]
1175  ]
1176qed.
1177
1178let rec subaddressing_mode_elim_type
1179  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
1180    (Q: addressing_mode → T → Prop)
1181      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
1182      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
1183      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
1184      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
1185      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
1186      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
1187      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
1188      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
1189      (p_dptr:                               is_in m fixed_v DPTR              → T)
1190      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
1191      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
1192      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
1193      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
1194      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
1195      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
1196      (p_carry:                              is_in m fixed_v CARRY             → T)
1197      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
1198      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
1199      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
1200        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
1201      on v: Prop ≝
1202  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
1203  [ VEmpty         ⇒ λm_refl. λv_refl.
1204      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
1205        Q addr (
1206        match addr return λx: addressing_mode. is_in … fixed_v x → T with
1207        [ ADDR11 x          ⇒ p_addr11 x
1208        | ADDR16 x          ⇒ p_addr16 x
1209        | DIRECT x          ⇒ p_direct x
1210        | INDIRECT x        ⇒ p_indirect x
1211        | EXT_INDIRECT x    ⇒ p_ext_indirect x
1212        | ACC_A             ⇒ p_acc_a
1213        | REGISTER x        ⇒ p_register x
1214        | ACC_B             ⇒ p_acc_b
1215        | DPTR              ⇒ p_dptr
1216        | DATA x            ⇒ p_data x
1217        | DATA16 x          ⇒ p_data16 x
1218        | ACC_DPTR          ⇒ p_acc_dptr
1219        | ACC_PC            ⇒ p_acc_pc
1220        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
1221        | INDIRECT_DPTR     ⇒ p_indirect_dptr
1222        | CARRY             ⇒ p_carry
1223        | BIT_ADDR x        ⇒ p_bit_addr x
1224        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
1225        | RELATIVE x        ⇒ p_relative x
1226        ] p)
1227  | VCons n' hd tl ⇒ λm_refl. λv_refl.
1228    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
1229      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
1230        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
1231          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
1232            p_bit_addr p_n_bit_addr p_relative n' tl ?
1233    in
1234    match hd return λa: addressing_mode_tag. a = hd → ? with
1235    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
1236    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
1237    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
1238    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
1239    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
1240    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
1241    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
1242    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
1243    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
1244    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
1245    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
1246    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
1247    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
1248    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
1249    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
1250    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
1251    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
1252    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
1253    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
1254    ] (refl … hd)
1255  ] (refl … n) (refl_jmeq … v).
1256  [20:
1257    generalize in match proof; destruct
1258    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
1259    cases (mem … eq_a m fixed_v hd) normalize nodelta
1260    [1:
1261      whd in match (subvector_with … eq_a tl fixed_v);
1262      #assm assumption
1263    |2:
1264      normalize in ⊢ (% → ?);
1265      #absurd cases absurd
1266    ]
1267  ]
1268  @(is_in_subvector_is_in_supervector … proof)
1269  destruct @I
1270qed.
1271
1272(* XXX: todo *)
1273lemma subaddressing_mode_elim':
1274  ∀T: Type[2].
1275  ∀n: nat.
1276  ∀o: nat.
1277  ∀v1: Vector addressing_mode_tag n.
1278  ∀v2: Vector addressing_mode_tag o.
1279  ∀Q: addressing_mode → T → Prop.
1280  ∀fixed_v: Vector addressing_mode_tag (n + o).
1281  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
1282  ∀fixed_v_proof: fixed_v = v1 @@ v2.
1283  ∀subaddressing_mode_proof.
1284    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
1285      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
1286  #T #n #o #v1 #v2
1287  elim v1 cases v2
1288  [1:
1289    #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
1290    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
1291    #subaddressing_mode_proof destruct normalize
1292    #addr #absurd cases absurd
1293  |2:
1294    #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
1295    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
1296    destruct normalize in match ([[]]@@hd:::tl);
1297  ]
1298  cases daemon
1299qed.
1300
1301(* XXX: todo *)
1302lemma subaddressing_mode_elim:
1303  ∀T: Type[2].
1304  ∀m: nat.
1305  ∀n: nat.
1306  ∀Q: addressing_mode → T → Prop.
1307  ∀fixed_v: Vector addressing_mode_tag m.
1308  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
1309  ∀v: Vector addressing_mode_tag n.
1310  ∀proof.
1311    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
1312      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
1313  #T #m #n #Q #fixed_v
1314  elim fixed_v
1315  [1:
1316    #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
1317    #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
1318    normalize
1319  |2:
1320  ]
1321  cases daemon
1322qed.
1323
1324definition program_counter_after_other ≝
1325  λprogram_counter. (* XXX: program counter after fetching *)
1326  λinstruction.
1327    if is_unconditional_jump instruction then
1328      compute_target_of_unconditional_jump program_counter instruction
1329    else
1330      program_counter.
1331
1332definition addr_of_relative ≝
1333 λM,cm. λx:[[relative]]. λs: PreStatus M cm.
1334  match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
1335   [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
1336   | _ ⇒ λabsd. ⊥
1337   ] (subaddressing_modein … x).
1338 @absd
1339qed.
1340
1341definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
1342  Σs': Status cm.
1343    And (clock ?? s' = \snd current + clock … s)
1344      (ASM_classify0 (\fst (\fst current)) = cl_other →
1345        program_counter ? ? s' =
1346          program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝
1347  λcm,s0,instr_pc_ticks.
1348    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
1349    let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
1350    let s ≝ set_program_counter … s0 pc in
1351      match instr return λx. x = instr → Σs:?.? with
1352      [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
1353        (addr_of_relative … cm) instr' s
1354      | MOVC addr1 addr2 ⇒ λinstr_refl.
1355          let s ≝ set_clock ?? s (ticks + clock … s) in
1356          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
1357            [ ACC_DPTR ⇒ λacc_dptr: True.
1358              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1359              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
1360              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
1361              let result ≝ lookup ? ? new_addr cm (zero ?) in
1362                set_8051_sfr … s SFR_ACC_A result
1363            | ACC_PC ⇒ λacc_pc: True.
1364              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1365              (* DPM: Under specified: does the carry from PC incrementation affect the *)
1366              (*      addition of the PC with the DPTR? At the moment, no.              *)
1367              let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
1368              let result ≝ lookup ? ? new_addr cm (zero ?) in
1369                set_8051_sfr … s SFR_ACC_A result
1370            | _ ⇒ λother: False. ⊥
1371            ] (subaddressing_modein … addr2)
1372      | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
1373          let s ≝ set_clock ?? s (ticks + clock … s) in
1374          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
1375          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1376          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
1377          let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
1378            set_program_counter … s new_pc
1379      | LJMP addr ⇒ λinstr_refl.
1380          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
1381          let s ≝ set_clock ?? s (ticks + clock … s) in
1382            set_program_counter … s new_pc
1383      | SJMP addr ⇒ λinstr_refl.
1384          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
1385          let s ≝ set_clock ?? s (ticks + clock … s) in
1386            set_program_counter … s new_pc
1387      | AJMP addr ⇒ λinstr_refl.
1388          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
1389          let s ≝ set_clock ?? s (ticks + clock … s) in
1390            set_program_counter … s new_pc
1391      | ACALL addr ⇒ λinstr_refl.
1392          let s ≝ set_clock ?? s (ticks + clock … s) in
1393          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
1394            [ ADDR11 a ⇒ λaddr11: True.
1395              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1396              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1397              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
1398              let s ≝ write_at_stack_pointer … s pc_bl in
1399              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1400              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1401              let s ≝ write_at_stack_pointer … s pc_bu in
1402              let 〈thr, eig〉 ≝ split ? 3 8 a in
1403              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
1404              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
1405                set_program_counter … s new_addr
1406            | _ ⇒ λother: False. ⊥
1407            ] (subaddressing_modein … addr)
1408        | LCALL addr ⇒ λinstr_refl.
1409          let s ≝ set_clock ?? s (ticks + clock … s) in
1410          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
1411            [ ADDR16 a ⇒ λaddr16: True.
1412              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1413              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1414              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
1415              let s ≝ write_at_stack_pointer … s pc_bl in
1416              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1417              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1418              let s ≝ write_at_stack_pointer … s pc_bu in
1419                set_program_counter … s a
1420            | _ ⇒ λother: False. ⊥
1421            ] (subaddressing_modein … addr)
1422        ] (refl … instr). (*10s*)
1423  try assumption
1424  [1,2,3,4,5,6,7,8:
1425    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
1426    try //
1427    -s destruct(INSTR_PC) <instr_refl whd
1428    try (#absurd normalize in absurd; try destruct(absurd) try %) %
1429  |9:
1430    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
1431        (λx. λs.
1432        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
1433        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
1434        | _ ⇒ λabsd. ⊥
1435        ] (subaddressing_modein … x)) instr' s) try @absd
1436    #clock_proof #classify_proof %
1437    [1:
1438      cases clock_proof #clock_proof' >clock_proof'
1439      destruct(INSTR_PC_TICKS) %
1440    |2:
1441      -clock_proof <INSTR_PC_TICKS normalize nodelta
1442      cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
1443      [1:
1444        destruct(INSTR_PC) /2/
1445      |2:
1446        * #hyp1 #hyp2 >hyp1 normalize nodelta
1447      <instr_refl normalize nodelta #hyp >classify_proof -classify_proof
1448      try assumption >hyp2 %
1449    ]
1450  ]
1451qed.
1452
1453definition current_instruction_cost ≝
1454  λcm.λs: Status cm.
1455    \snd (fetch cm (program_counter … s)).
1456
1457definition execute_1': ∀cm.∀s:Status cm.
1458  Σs':Status cm.
1459    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1460      And (clock ?? s' = current_instruction_cost cm s + clock … s)
1461        (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1462          program_counter ? ? s' =
1463            program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝
1464  λcm. λs: Status cm.
1465  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1466    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
1467  %
1468  [1:
1469    cases(execute_1_0 cm s instr_pc_ticks)
1470    #the_status * #clock_assm #_ @clock_assm
1471  |2:
1472    cases(execute_1_0 cm s instr_pc_ticks)
1473    #the_status * #_ #classify_assm
1474    assumption
1475  ]
1476qed.
1477
1478definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
1479
1480lemma execute_1_ok: ∀cm.∀s.
1481  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1482    (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
1483      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1484        program_counter ? cm (execute_1 cm s) =
1485          program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
1486(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
1487  #cm #s normalize nodelta
1488  whd in match execute_1; normalize nodelta @pi2
1489qed.
1490
1491lemma execute_1_ok_clock:
1492  ∀cm.
1493  ∀s.
1494    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
1495  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
1496qed-.
1497
1498definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
1499  λticks,cm,s,instr,pc.
1500  let s ≝ set_program_counter ?? s pc in
1501  let s ≝
1502    match instr with
1503    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
1504    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
1505    | Cost cst ⇒ s
1506    | Jmp jmp ⇒
1507       let s ≝ set_clock … s (\fst ticks + clock … s) in
1508        set_program_counter … s (address_of_word_labels cm jmp)
1509    | Call call ⇒
1510      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1511      let a ≝ address_of_word_labels cm call in
1512      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1513      let s ≝ set_8051_sfr … s SFR_SP new_sp in
1514      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
1515      let s ≝ write_at_stack_pointer … s pc_bl in
1516      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1517      let s ≝ set_8051_sfr … s SFR_SP new_sp in
1518      let s ≝ write_at_stack_pointer … s pc_bu in
1519        set_program_counter … s a
1520    | Mov dptr ident ⇒
1521      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1522      let the_preamble ≝ \fst cm in
1523      let data_labels ≝ construct_datalabels the_preamble in
1524        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
1525    ]
1526  in
1527    s.
1528  normalize
1529  @I
1530qed.
1531
1532definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝
1533  λticks_of,cm,s.
1534  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
1535  let ticks ≝ ticks_of (program_counter … s) in
1536   execute_1_pseudo_instruction0 ticks cm s instr pc.
1537
1538let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
1539  match n with
1540    [ O ⇒ s
1541    | S o ⇒ execute o … (execute_1 … s)
1542    ].
1543
1544let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
1545  match n with
1546    [ O ⇒ s
1547    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
1548    ].
Note: See TracBrowser for help on using the repository browser.