source: src/ASM/Interpret.ma @ 1964

Last change on this file since 1964 was 1964, checked in by tranquil, 8 years ago

introduced as_label_of_cost and adapted accordingly. Equality of cost mapping sums

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