source: src/ASM/Interpret.ma @ 1938

Last change on this file since 1938 was 1938, checked in by sacerdot, 8 years ago

Definitions moved to the right places, now everything compiles again.

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