source: src/ASM/Interpret.ma @ 1948

Last change on this file since 1948 was 1948, checked in by mulligan, 8 years ago

Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so all lemmas and functions that accepted a sigma before now accept a weakened sigma coupled with a policy. ASM/AssemblyProof.ma compiles until main_thm.

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