source: src/ASM/Interpret.ma @ 1928

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

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

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