source: src/ASM/Interpret.ma @ 1710

Last change on this file since 1710 was 1710, checked in by mulligan, 9 years ago

changes from friday afternoon

File size: 36.5 KB
RevLine 
[1666]1include "ASM/StatusProofs.ma".
[1709]2include "common/StructuredTraces.ma".
[698]3include "ASM/Fetch.ma".
[475]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
[1588]21 try %
[475]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
[1522]43   change with (orb ??) in H2: (??%?);
[475]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
[1519]80   whd in ⊢ (% → ? → ?);
[475]81   lapply (refl … (is_in … (he:::tl) a))
[1519]82   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
[475]83   [ # K
84     # _
85     normalize in K;
[1519]86     whd in ⊢ (% → ?);
87     lapply (refl … (subvector_with … eq_a (he:::tl) q));
88     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
[475]89     [ # K1
90       # _
[1522]91       change with ((andb ? (subvector_with …)) = true) in K1;
[475]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
[1522]108       normalize in K2;
[475]109       cases K2;
110     ]
111   | # K1
112     # K2
113     normalize in K2;
114     cases K2
115   ]
116 ]
117qed.
[712]118
119include alias "arithmetics/nat.ma".
[757]120include alias "ASM/BitVectorTrie.ma".
[712]121
[1710]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
[1709]139definition ASM_classify0: instruction → status_class ≝
[1710]140  λi.
[1709]141  match i with
[1710]142   [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
[1709]143   | ACALL _ ⇒ cl_call
144   | LCALL _ ⇒ cl_call
145   | JMP _ ⇒ cl_call
146   | AJMP _ ⇒ cl_jump
147   | LJMP _ ⇒ cl_jump
148   | SJMP _ ⇒ cl_jump
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
[1588]167definition execute_1_preinstruction':
[1577]168  ∀ticks: nat × nat.
[1710]169  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
[1666]170  ∀s: PreStatus m cm.
171    Σs': PreStatus m cm.
[1709]172      And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
[1710]173        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝
[1577]174  λticks: nat × nat.
[1666]175  λa, m: Type[0]. λcm.
176  λaddr_of: a → PreStatus m cm → Word.
[1577]177  λinstr: preinstruction a.
[1666]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
[1710]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.
[936]185            let s ≝ add_ticks1 s in
[1666]186            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
187                                                   (get_arg_8 … s false addr2) false in
[475]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
[1666]191            let s ≝ set_arg_8 … s ACC_A result in
192              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[1710]193        | ADDC addr1 addr2 ⇒ λinstr_refl.
[936]194            let s ≝ add_ticks1 s in
[1666]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
[475]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
[1666]201            let s ≝ set_arg_8 … s ACC_A result in
202              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[1710]203        | SUBB addr1 addr2 ⇒ λinstr_refl.
[936]204            let s ≝ add_ticks1 s in
[1666]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
[475]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
[1666]211            let s ≝ set_arg_8 … s ACC_A result in
212              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[1710]213        | ANL addr ⇒ λinstr_refl.
[936]214          let s ≝ add_ticks1 s in
[475]215          match addr with
216            [ inl l ⇒
217              match l with
218                [ inl l' ⇒
219                  let 〈addr1, addr2〉 ≝ l' in
[1666]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
[475]222                | inr r ⇒
223                  let 〈addr1, addr2〉 ≝ r in
[1666]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
[475]226                ]
227            | inr r ⇒
228              let 〈addr1, addr2〉 ≝ r in
[1666]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)
[475]231            ]
[1710]232        | ORL addr ⇒ λinstr_refl.
[936]233          let s ≝ add_ticks1 s in
[475]234          match addr with
235            [ inl l ⇒
[1588]236              match l with
[475]237                [ inl l' ⇒
238                  let 〈addr1, addr2〉 ≝ l' in
[1666]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
[475]241                | inr r ⇒
242                  let 〈addr1, addr2〉 ≝ r in
[1666]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
[475]245                ]
246            | inr r ⇒
247              let 〈addr1, addr2〉 ≝ r in
[1666]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)
[475]250            ]
[1710]251        | XRL addr ⇒ λinstr_refl.
[936]252          let s ≝ add_ticks1 s in
[475]253          match addr with
254            [ inl l' ⇒
255              let 〈addr1, addr2〉 ≝ l' in
[1666]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
[475]258            | inr r ⇒
259              let 〈addr1, addr2〉 ≝ r in
[1666]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
[475]262            ]
[1710]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
[475]265              [ ACC_A ⇒ λacc_a: True.
[1534]266                let s' ≝ add_ticks1 s in
[1666]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
[475]269              | REGISTER r ⇒ λregister: True.
[1534]270                let s' ≝ add_ticks1 s in
[1666]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
[475]273              | DIRECT d ⇒ λdirect: True.
[1534]274                let s' ≝ add_ticks1 s in
[1666]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
[475]277              | INDIRECT i ⇒ λindirect: True.
[1534]278                let s' ≝ add_ticks1 s in
[1666]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
[475]281              | DPTR ⇒ λdptr: True.
[1534]282                let s' ≝ add_ticks1 s in
[1666]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
[475]287              | _ ⇒ λother: False. ⊥
288              ] (subaddressing_modein … addr)
[1710]289        | NOP ⇒ λinstr_refl.
[1534]290           let s ≝ add_ticks2 s in
291            s
[1710]292        | DEC addr ⇒ λinstr_refl.
[936]293           let s ≝ add_ticks1 s in
[1666]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
[1710]296        | MUL addr1 addr2 ⇒ λinstr_refl.
[936]297           let s ≝ add_ticks1 s in
[1666]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
[475]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
[1666]304           let s ≝ set_8051_sfr … s SFR_ACC_A low in
305             set_8051_sfr … s SFR_ACC_B high
[1710]306        | DIV addr1 addr2 ⇒ λinstr_refl.
[936]307           let s ≝ add_ticks1 s in
[1666]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
[475]310             match acc_b_nat with
[1666]311               [ O ⇒ set_flags … s false (None Bit) true
[475]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
[1666]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
[475]318               ]
[1710]319        | DA addr ⇒ λinstr_refl.
[936]320            let s ≝ add_ticks1 s in
[1666]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
[475]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
[1666]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)
[475]331                  else
332                    s
333              else
334                s
[1710]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
[1534]337            [ ACC_A ⇒ λacc_a: True.
338              let s ≝ add_ticks1 s in
[1666]339               set_arg_8 … s ACC_A (zero 8)
[1534]340            | CARRY ⇒ λcarry: True.
341              let s ≝ add_ticks1 s in
[1666]342               set_arg_1 … s CARRY false
[1534]343            | BIT_ADDR b ⇒ λbit_addr: True.
344              let s ≝ add_ticks1 s in
[1666]345               set_arg_1 … s (BIT_ADDR b) false
[475]346            | _ ⇒ λother: False. ⊥
347            ] (subaddressing_modein … addr)
[1710]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
[475]350            [ ACC_A ⇒ λacc_a: True.
[1534]351                let s ≝ add_ticks1 s in
[1666]352                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]353                let new_acc ≝ negation_bv ? old_acc in
[1666]354                 set_8051_sfr … s SFR_ACC_A new_acc
[475]355            | CARRY ⇒ λcarry: True.
[1534]356                let s ≝ add_ticks1 s in
[1666]357                let old_cy_flag ≝ get_arg_1 … s CARRY true in
[475]358                let new_cy_flag ≝ ¬old_cy_flag in
[1666]359                 set_arg_1 … s CARRY new_cy_flag
[475]360            | BIT_ADDR b ⇒ λbit_addr: True.
[1534]361                let s ≝ add_ticks1 s in
[1666]362                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
[475]363                let new_bit ≝ ¬old_bit in
[1666]364                 set_arg_1 … s (BIT_ADDR b) new_bit
[475]365            | _ ⇒ λother: False. ?
366            ] (subaddressing_modein … addr)
[1710]367        | SETB b ⇒ λinstr_refl.
[936]368            let s ≝ add_ticks1 s in
[1666]369            set_arg_1 … s b false
[1710]370        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]371            let s ≝ add_ticks1 s in
[1666]372            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]373            let new_acc ≝ rotate_left … 1 old_acc in
[1666]374              set_8051_sfr … s SFR_ACC_A new_acc
[1710]375        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]376            let s ≝ add_ticks1 s in
[1666]377            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]378            let new_acc ≝ rotate_right … 1 old_acc in
[1666]379              set_8051_sfr … s SFR_ACC_A new_acc
[1710]380        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]381            let s ≝ add_ticks1 s in
[1666]382            let old_cy_flag ≝ get_cy_flag ?? s in
383            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]384            let new_cy_flag ≝ get_index' ? O ? old_acc in
385            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
[1666]386            let s ≝ set_arg_1 … s CARRY new_cy_flag in
387              set_8051_sfr … s SFR_ACC_A new_acc
[1710]388        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]389            let s ≝ add_ticks1 s in
[1666]390            let old_cy_flag ≝ get_cy_flag ?? s in
391            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]392            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
393            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
[1666]394            let s ≝ set_arg_1 … s CARRY new_cy_flag in
395              set_8051_sfr … s SFR_ACC_A new_acc
[1710]396        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]397            let s ≝ add_ticks1 s in
[1666]398            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]399            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
400            let new_acc ≝ nl @@ nu in
[1666]401              set_8051_sfr … s SFR_ACC_A new_acc
[1710]402        | PUSH addr ⇒ λinstr_refl.
403            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
[475]404              [ DIRECT d ⇒ λdirect: True.
[1534]405                let s ≝ add_ticks1 s in
[1666]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
[475]409              | _ ⇒ λother: False. ⊥
410              ] (subaddressing_modein … addr)
[1710]411        | POP addr ⇒ λinstr_refl.
[936]412            let s ≝ add_ticks1 s in
[1666]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
[1710]417        | XCH addr1 addr2 ⇒ λinstr_refl.
[936]418            let s ≝ add_ticks1 s in
[1666]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
[1710]423        | XCHD addr1 addr2 ⇒ λinstr_refl.
[936]424            let s ≝ add_ticks1 s in
[1666]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
[475]427            let new_acc ≝ acc_nu @@ arg_nl in
428            let new_arg ≝ arg_nu @@ acc_nl in
[1710]429            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
[1666]430              set_arg_8 … s addr2 new_arg
[1710]431        | RET ⇒ λinstr_refl.
[936]432            let s ≝ add_ticks1 s in
[1666]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
[475]439            let new_pc ≝ high_bits @@ low_bits in
[1666]440              set_program_counter … s new_pc
[1710]441        | RETI ⇒ λinstr_refl.
[936]442            let s ≝ add_ticks1 s in
[1666]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
[475]449            let new_pc ≝ high_bits @@ low_bits in
[1666]450              set_program_counter … s new_pc
[1710]451        | MOVX addr ⇒ λinstr_refl.
[936]452          let s ≝ add_ticks1 s in
[475]453          (* DPM: only copies --- doesn't affect I/O *)
454          match addr with
455            [ inl l ⇒
456              let 〈addr1, addr2〉 ≝ l in
[1666]457                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]458            | inr r ⇒
459              let 〈addr1, addr2〉 ≝ r in
[1666]460                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]461            ]
[1710]462        | MOV addr ⇒ λinstr_refl.
[936]463          let s ≝ add_ticks1 s in
[475]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
[1666]475                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]476                            | inr r'''' ⇒
477                              let 〈addr1, addr2〉 ≝ r'''' in
[1666]478                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]479                            ]
480                        | inr r''' ⇒
481                          let 〈addr1, addr2〉 ≝ r''' in
[1666]482                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]483                        ]
484                    | inr r'' ⇒
485                      let 〈addr1, addr2〉 ≝ r'' in
[1666]486                       set_arg_16 … s (get_arg_16 … s addr2) addr1
[475]487                    ]
488                | inr r ⇒
489                  let 〈addr1, addr2〉 ≝ r in
[1666]490                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
[475]491                ]
492            | inr r ⇒
493              let 〈addr1, addr2〉 ≝ r in
[1666]494               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
[475]495            ]
[1710]496          | JC addr ⇒ λinstr_refl.
[1666]497                  if get_cy_flag ?? s then
[1534]498                    let s ≝ add_ticks1 s in
[1666]499                      set_program_counter … s (addr_of addr s)
[712]500                  else
[1534]501                    let s ≝ add_ticks2 s in
502                      s
[1710]503            | JNC addr ⇒ λinstr_refl.
[1666]504                  if ¬(get_cy_flag ?? s) then
[936]505                   let s ≝ add_ticks1 s in
[1666]506                     set_program_counter … s (addr_of addr s)
[712]507                  else
[936]508                   let s ≝ add_ticks2 s in
[712]509                    s
[1710]510            | JB addr1 addr2 ⇒ λinstr_refl.
[1666]511                  if get_arg_1 … s addr1 false then
[936]512                   let s ≝ add_ticks1 s in
[1666]513                    set_program_counter … s (addr_of addr2 s)
[712]514                  else
[936]515                   let s ≝ add_ticks2 s in
[712]516                    s
[1710]517            | JNB addr1 addr2 ⇒ λinstr_refl.
[1666]518                  if ¬(get_arg_1 … s addr1 false) then
[936]519                   let s ≝ add_ticks1 s in
[1666]520                    set_program_counter … s (addr_of addr2 s)
[712]521                  else
[936]522                   let s ≝ add_ticks2 s in
[712]523                    s
[1710]524            | JBC addr1 addr2 ⇒ λinstr_refl.
[1666]525                  let s ≝ set_arg_1 … s addr1 false in
526                    if get_arg_1 … s addr1 false then
[936]527                     let s ≝ add_ticks1 s in
[1666]528                      set_program_counter … s (addr_of addr2 s)
[712]529                    else
[936]530                     let s ≝ add_ticks2 s in
[712]531                      s
[1710]532            | JZ addr ⇒ λinstr_refl.
[1666]533                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
[936]534                     let s ≝ add_ticks1 s in
[1666]535                      set_program_counter … s (addr_of addr s)
[712]536                    else
[936]537                     let s ≝ add_ticks2 s in
[712]538                      s
[1710]539            | JNZ addr ⇒ λinstr_refl.
[1666]540                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
[936]541                     let s ≝ add_ticks1 s in
[1666]542                      set_program_counter … s (addr_of addr s)
[712]543                    else
[936]544                     let s ≝ add_ticks2 s in
[712]545                      s
[1710]546            | CJNE addr1 addr2 ⇒ λinstr_refl.
[712]547                  match addr1 with
548                    [ inl l ⇒
[822]549                        let 〈addr1, addr2'〉 ≝ l in
[1666]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
[936]553                            let s ≝ add_ticks1 s in
[1666]554                            let s ≝ set_program_counter … s (addr_of addr2 s) in
555                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]556                          else
[936]557                            let s ≝ add_ticks2 s in
[1666]558                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]559                    | inr r' ⇒
[822]560                        let 〈addr1, addr2'〉 ≝ r' in
[1666]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
[936]564                            let s ≝ add_ticks1 s in
[1666]565                            let s ≝ set_program_counter … s (addr_of addr2 s) in
566                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]567                          else
[936]568                            let s ≝ add_ticks2 s in
[1666]569                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]570                    ]
[1710]571            | DJNZ addr1 addr2 ⇒ λinstr_refl.
[1666]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
[820]574                if ¬(eq_bv ? result (zero 8)) then
[936]575                 let s ≝ add_ticks1 s in
[1666]576                  set_program_counter … s (addr_of addr2 s)
[820]577                else
[936]578                 let s ≝ add_ticks2 s in
[820]579                  s
[1710]580            ] (refl … instr).
[1582]581    try (cases(other))
[1547]582    try assumption (*20s*)
[1588]583    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
[820]584    try (
[1710]585      @(execute_1_technical … (subaddressing_modein …))
586      @I
[1547]587    ) (*66s*)
[1710]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/ %
[820]594qed.
595
[1588]596definition execute_1_preinstruction:
597  ∀ticks: nat × nat.
[1666]598  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
599  PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
[1588]600 
601lemma execute_1_preinstruction_ok:
[1666]602 ∀ticks,a,m,cm,f,i,s.
[1710]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).
[1666]606 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
[1588]607qed.
608
[1709]609discriminator Prod.
610
[1666]611definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
[1709]612  Σs': Status cm.
613    And (clock ?? s' = \snd current + clock … s)
614      (ASM_classify0 (\fst (\fst current)) = cl_other →
615        program_counter ? ? s' = \snd (\fst current)) ≝
[1666]616  λcm,s0,instr_pc_ticks.
[1709]617    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
618    let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
[1666]619    let s ≝ set_program_counter … s0 pc in
[1709]620      match instr return λx. x = instr → Σs:?.? with
621      [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
[822]622        (λx. λs.
[1575]623        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
[1666]624        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
[820]625        | _ ⇒ λabsd. ⊥
[1709]626        ] (subaddressing_modein … x)) instr' s
627      | MOVC addr1 addr2 ⇒ λinstr_refl.
628          let s ≝ set_clock ?? s (ticks + clock … s) in
629          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
[757]630            [ ACC_DPTR ⇒ λacc_dptr: True.
[1666]631              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
632              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
[1534]633              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
[1666]634              let result ≝ lookup ? ? new_addr cm (zero ?) in
635                set_8051_sfr … s SFR_ACC_A result
[757]636            | ACC_PC ⇒ λacc_pc: True.
[1666]637              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
[757]638              (* DPM: Under specified: does the carry from PC incrementation affect the *)
639              (*      addition of the PC with the DPTR? At the moment, no.              *)
[1709]640              let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
[1666]641              let result ≝ lookup ? ? new_addr cm (zero ?) in
642                set_8051_sfr … s SFR_ACC_A result
[757]643            | _ ⇒ λother: False. ⊥
644            ] (subaddressing_modein … addr2)
[1709]645      | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
646          let s ≝ set_clock ?? s (ticks + clock … s) in
[1666]647          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
648          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
[1534]649          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
[1666]650          let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
651            set_program_counter … s new_pc
[1709]652      | LJMP addr ⇒ λinstr_refl.
653          let s ≝ set_clock ?? s (ticks + clock … s) in
654          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
[820]655            [ ADDR16 a ⇒ λaddr16: True.
[1666]656                set_program_counter … s a
[820]657            | _ ⇒ λother: False. ⊥
658            ] (subaddressing_modein … addr)
[1709]659      | SJMP addr ⇒ λinstr_refl.
660          let s ≝ set_clock ?? s (ticks + clock … s) in
661          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
[820]662            [ RELATIVE r ⇒ λrelative: True.
[1666]663                let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in
664                  set_program_counter … s new_pc
[820]665            | _ ⇒ λother: False. ⊥
666            ] (subaddressing_modein … addr)
[1709]667      | AJMP addr ⇒ λinstr_refl.
668          let s ≝ set_clock ?? s (ticks + clock … s) in
669          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
[820]670            [ ADDR11 a ⇒ λaddr11: True.
[1666]671              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
[1534]672              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
[820]673              let bit ≝ get_index' ? O ? nl in
[1534]674              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
[820]675              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
[1666]676              let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in
677                set_program_counter … s new_pc
[820]678            | _ ⇒ λother: False. ⊥
679            ] (subaddressing_modein … addr)
[1709]680      | ACALL addr ⇒ λinstr_refl.
681          let s ≝ set_clock ?? s (ticks + clock … s) in
682          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
[1575]683            [ ADDR11 a ⇒ λaddr11: True.
[1666]684              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
685              let s ≝ set_8051_sfr … s SFR_SP new_sp in
686              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
687              let s ≝ write_at_stack_pointer … s pc_bl in
688              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
689              let s ≝ set_8051_sfr … s SFR_SP new_sp in
690              let s ≝ write_at_stack_pointer … s pc_bu in
[1575]691              let 〈thr, eig〉 ≝ split ? 3 8 a in
692              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
693              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
[1666]694                set_program_counter … s new_addr
[1575]695            | _ ⇒ λother: False. ⊥
696            ] (subaddressing_modein … addr)
[1709]697        | LCALL addr ⇒ λinstr_refl.
698          let s ≝ set_clock ?? s (ticks + clock … s) in
699          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
[1575]700            [ ADDR16 a ⇒ λaddr16: True.
[1666]701              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
702              let s ≝ set_8051_sfr … s SFR_SP new_sp in
703              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
704              let s ≝ write_at_stack_pointer … s pc_bl in
705              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
706              let s ≝ set_8051_sfr … s SFR_SP new_sp in
707              let s ≝ write_at_stack_pointer … s pc_bu in
708                set_program_counter … s a
[1575]709            | _ ⇒ λother: False. ⊥
710            ] (subaddressing_modein … addr)
[1709]711        ] (refl … instr). (*10s*)
712  try assumption
713  [1,2,3,4,5,6,7,8:
714    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
715    try //
716    destruct(INSTR_PC) <instr_refl
717    #absurd normalize in absurd; try destruct(absurd) try %
718  |9:
[1710]719    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
[1588]720        (λx. λs.
721        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
[1666]722        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
[1588]723        | _ ⇒ λabsd. ⊥
[1710]724        ] (subaddressing_modein … x)) instr' s) try @absd
725    #clock_proof #classify_proof %
726    [1:
727      cases clock_proof #clock_proof' >clock_proof'
728      destruct(INSTR_PC_TICKS) %
729    |2:
730      #classify_assm -clock_proof >classify_proof -classify_proof
731      [1:
732        normalize nodelta normalize <INSTR_PC_TICKS
733        destruct(INSTR_PC) %
734      |2:
735        <classify_assm <INSTR_PC_TICKS destruct <e0 %
736      ]
737    ]
738  ]
[475]739qed.
740
[1547]741definition current_instruction_cost ≝
[1666]742  λcm.λs: Status cm.
743    \snd (fetch cm (program_counter … s)).
[1547]744
[1666]745definition execute_1': ∀cm.∀s:Status cm.
[1710]746  Σs':Status cm.
747    And (clock ?? s' = current_instruction_cost cm s + clock … s)
748      (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝
[1666]749  λcm. λs: Status cm.
[1710]750  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
751    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
752  %
753  [1:
754    cases(execute_1_0 cm s instr_pc_ticks)
755    #the_status * #clock_assm #_ @clock_assm
756  |2:
757    cases(execute_1_0 cm s instr_pc_ticks)
758    #the_status * #_ #classify_assm #classify_assm'
759    lapply(classify_assm ?)
760    [1:
761      change with (
762        ASM_classify cm s = cl_other
763      )
764      assumption
765    |2:
766      #program_counter_refl >program_counter_refl %
767    ]
768  ]
769qed.
[928]770
[1666]771definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
[1588]772
[1710]773lemma execute_1_ok: ∀cm.∀s.
774  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
775    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)).
[1666]776 #cm #s whd in match execute_1; normalize nodelta @pi2
[1588]777qed-. (*x Andrea: indexing takes ages here *)
778
[1666]779definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
780  λticks,cm,s,instr,pc.
781  let s ≝ set_program_counter ?? s pc in
[820]782  let s ≝
783    match instr with
[1666]784    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
785    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
[820]786    | Cost cst ⇒ s
[936]787    | Jmp jmp ⇒
[1666]788       let s ≝ set_clock … s (\fst ticks + clock … s) in
789        set_program_counter … s (address_of_word_labels cm jmp)
[820]790    | Call call ⇒
[1666]791      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
792      let a ≝ address_of_word_labels cm call in
793      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
794      let s ≝ set_8051_sfr … s SFR_SP new_sp in
795      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
796      let s ≝ write_at_stack_pointer … s pc_bl in
797      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
798      let s ≝ set_8051_sfr … s SFR_SP new_sp in
799      let s ≝ write_at_stack_pointer … s pc_bu in
800        set_program_counter … s a
[910]801    | Mov dptr ident ⇒
[1666]802      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
803      let the_preamble ≝ \fst cm in
[1541]804      let data_labels ≝ construct_datalabels the_preamble in
[1666]805        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
[820]806    ]
807  in
808    s.
809  normalize
[1577]810  @I
[820]811qed.
812
[1666]813definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝
814  λticks_of,cm,s.
815  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
816  let ticks ≝ ticks_of (program_counter … s) in
817   execute_1_pseudo_instruction0 ticks cm s instr pc.
[1037]818
[1666]819let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
[475]820  match n with
821    [ O ⇒ s
[1666]822    | S o ⇒ execute o … (execute_1 … s)
[475]823    ].
[820]824
[1666]825let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
[820]826  match n with
827    [ O ⇒ s
[1666]828    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
829    ].
Note: See TracBrowser for help on using the repository browser.