source: src/ASM/Interpret.ma @ 3060

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

Bug fixed in the semantics of JMP.
The bug was due to a bug in the datasheets!

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