source: src/ASM/Interpret.ma @ 1939

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

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

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