source: src/ASM/Interpret.ma @ 1935

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

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

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