source: src/ASM/Interpret.ma @ 3039

Last change on this file since 3039 was 3039, checked in by tranquil, 7 years ago
  • merged and extended MovSuccessor? and Mov in one instruction (Mov dst

ident offset)

  • JMP now correctly uses ACCDPTR argument
  • LINToASM: ADDRESS now translate to a symbolical Mov (now a preamble

is generated), and globals initialization is fixed accordingly

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