source: src/ASM/Interpret.ma @ 1666

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

PreStatus? datatype change: the code_memory field is not a left parameter.
This greatly simplify the dependent type madness due to policy depending
on the code_memory and not really on the status. On the other hand it
makes the rest of the code uglier.

Note: the changes have not been propagated yet to ASMCosts, CostsProof? and
Interpret2. The AssemlyProof? is almost repaired.

File size: 33.8 KB
RevLine 
[1666]1include "ASM/StatusProofs.ma".
[698]2include "ASM/Fetch.ma".
[475]3
4definition sign_extension: Byte → Word ≝
5  λc.
6    let b ≝ get_index_v ? 8 c 1 ? in
7      [[ b; b; b; b; b; b; b; b ]] @@ c.
8  normalize;
9  repeat (@ (le_S_S ?));
10  @ (le_O_n);
11qed.
12   
13lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
14 # a
15 # b
16 cases a
17 cases b
18 normalize
19 # K
[1588]20 try %
[475]21 cases (eq_true_false K)
22qed.
23
24lemma is_a_to_mem_to_is_in:
25 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
26 # he
27 # a
28 # m
29 # q
30 elim q
31 [ normalize
32   # _
33   # K
34   assumption
35 | # m'
36   # t
37   # q'
38   # II
39   # H1
40   # H2
41   normalize
[1522]42   change with (orb ??) in H2: (??%?);
[475]43   cases (inclusive_disjunction_true … H2)
44   [ # K
45     < (eq_a_to_eq … K)
46     > H1
47     %
48   | # K
49     > II
50     try assumption
51     cases (is_a t a)
52     normalize
53     %
54   ]
55 ]
56qed.
57
58lemma execute_1_technical:
59  ∀n, m: nat.
60  ∀v: Vector addressing_mode_tag (S n).
61  ∀q: Vector addressing_mode_tag (S m).
62  ∀a: addressing_mode.
63    bool_to_Prop (is_in ? v a) →
64    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
65    bool_to_Prop (is_in ? q a).
66 # n
67 # m
68 # v
69 # q
70 # a
71 elim v
72 [ normalize
73   # K
74   cases K
75 | # n'
76   # he
77   # tl
78   # II
[1519]79   whd in ⊢ (% → ? → ?);
[475]80   lapply (refl … (is_in … (he:::tl) a))
[1519]81   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
[475]82   [ # K
83     # _
84     normalize in K;
[1519]85     whd in ⊢ (% → ?);
86     lapply (refl … (subvector_with … eq_a (he:::tl) q));
87     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
[475]88     [ # K1
89       # _
[1522]90       change with ((andb ? (subvector_with …)) = true) in K1;
[475]91       cases (conjunction_true … K1)
92       # K3
93       # K4
94       cases (inclusive_disjunction_true … K)
95       # K2
96       [ > (is_a_to_mem_to_is_in … K2 K3)
97         %
98       | @ II
99         [ > K2
100           %
101         | > K4
102           %
103         ]
104       ]
105     | # K1
106       # K2
[1522]107       normalize in K2;
[475]108       cases K2;
109     ]
110   | # K1
111     # K2
112     normalize in K2;
113     cases K2
114   ]
115 ]
116qed.
[712]117
118include alias "arithmetics/nat.ma".
[757]119include alias "ASM/BitVectorTrie.ma".
[712]120
[1588]121definition execute_1_preinstruction':
[1577]122  ∀ticks: nat × nat.
[1666]123  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
124  ∀s: PreStatus m cm.
125    Σs': PreStatus m cm.
126      Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝
[1577]127  λticks: nat × nat.
[1666]128  λa, m: Type[0]. λcm.
129  λaddr_of: a → PreStatus m cm → Word.
[1577]130  λinstr: preinstruction a.
[1666]131  λs: PreStatus m cm.
132  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
133  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
134  match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s) with
[475]135        [ ADD addr1 addr2 ⇒
[936]136            let s ≝ add_ticks1 s in
[1666]137            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
138                                                   (get_arg_8 … s false addr2) false in
[475]139            let cy_flag ≝ get_index' ? O  ? flags in
140            let ac_flag ≝ get_index' ? 1 ? flags in
141            let ov_flag ≝ get_index' ? 2 ? flags in
[1666]142            let s ≝ set_arg_8 … s ACC_A result in
143              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[475]144        | ADDC addr1 addr2 ⇒
[936]145            let s ≝ add_ticks1 s in
[1666]146            let old_cy_flag ≝ get_cy_flag ?? s in
147            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
148                                                   (get_arg_8 … s false addr2) old_cy_flag in
[475]149            let cy_flag ≝ get_index' ? O ? flags in
150            let ac_flag ≝ get_index' ? 1 ? flags in
151            let ov_flag ≝ get_index' ? 2 ? flags in
[1666]152            let s ≝ set_arg_8 … s ACC_A result in
153              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[475]154        | SUBB addr1 addr2 ⇒
[936]155            let s ≝ add_ticks1 s in
[1666]156            let old_cy_flag ≝ get_cy_flag ?? s in
157            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
158                                                   (get_arg_8 … s false addr2) old_cy_flag in
[475]159            let cy_flag ≝ get_index' ? O ? flags in
160            let ac_flag ≝ get_index' ? 1 ? flags in
161            let ov_flag ≝ get_index' ? 2 ? flags in
[1666]162            let s ≝ set_arg_8 … s ACC_A result in
163              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[475]164        | ANL addr ⇒
[936]165          let s ≝ add_ticks1 s in
[475]166          match addr with
167            [ inl l ⇒
168              match l with
169                [ inl l' ⇒
170                  let 〈addr1, addr2〉 ≝ l' in
[1666]171                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
172                    set_arg_8 … s addr1 and_val
[475]173                | inr r ⇒
174                  let 〈addr1, addr2〉 ≝ r in
[1666]175                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
176                    set_arg_8 … s addr1 and_val
[475]177                ]
178            | inr r ⇒
179              let 〈addr1, addr2〉 ≝ r in
[1666]180              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
181               set_flags … s and_val (None ?) (get_ov_flag ?? s)
[475]182            ]
183        | ORL addr ⇒
[936]184          let s ≝ add_ticks1 s in
[475]185          match addr with
186            [ inl l ⇒
[1588]187              match l with
[475]188                [ inl l' ⇒
189                  let 〈addr1, addr2〉 ≝ l' in
[1666]190                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
191                    set_arg_8 … s addr1 or_val
[475]192                | inr r ⇒
193                  let 〈addr1, addr2〉 ≝ r in
[1666]194                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
195                    set_arg_8 … s addr1 or_val
[475]196                ]
197            | inr r ⇒
198              let 〈addr1, addr2〉 ≝ r in
[1666]199              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
200               set_flags … s or_val (None ?) (get_ov_flag … s)
[475]201            ]
202        | XRL addr ⇒
[936]203          let s ≝ add_ticks1 s in
[475]204          match addr with
205            [ inl l' ⇒
206              let 〈addr1, addr2〉 ≝ l' in
[1666]207              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
208                set_arg_8 … s addr1 xor_val
[475]209            | inr r ⇒
210              let 〈addr1, addr2〉 ≝ r in
[1666]211              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
212                set_arg_8 … s addr1 xor_val
[475]213            ]
214        | INC addr ⇒
[1666]215            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
[475]216              [ ACC_A ⇒ λacc_a: True.
[1534]217                let s' ≝ add_ticks1 s in
[1666]218                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
219                 set_arg_8 … s' ACC_A result
[475]220              | REGISTER r ⇒ λregister: True.
[1534]221                let s' ≝ add_ticks1 s in
[1666]222                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
223                 set_arg_8 … s' (REGISTER r) result
[475]224              | DIRECT d ⇒ λdirect: True.
[1534]225                let s' ≝ add_ticks1 s in
[1666]226                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
227                 set_arg_8 … s' (DIRECT d) result
[475]228              | INDIRECT i ⇒ λindirect: True.
[1534]229                let s' ≝ add_ticks1 s in
[1666]230                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
231                 set_arg_8 … s' (INDIRECT i) result
[475]232              | DPTR ⇒ λdptr: True.
[1534]233                let s' ≝ add_ticks1 s in
[1666]234                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
235                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
236                let s ≝ set_8051_sfr … s' SFR_DPL bl in
237                 set_8051_sfr … s' SFR_DPH bu
[475]238              | _ ⇒ λother: False. ⊥
239              ] (subaddressing_modein … addr)
[1534]240        | NOP ⇒
241           let s ≝ add_ticks2 s in
242            s
[475]243        | DEC addr ⇒
[936]244           let s ≝ add_ticks1 s in
[1666]245           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
246             set_arg_8 … s addr result
[475]247        | MUL addr1 addr2 ⇒
[936]248           let s ≝ add_ticks1 s in
[1666]249           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
250           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
[475]251           let product ≝ acc_a_nat * acc_b_nat in
252           let ov_flag ≝ product ≥ 256 in
253           let low ≝ bitvector_of_nat 8 (product mod 256) in
254           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
[1666]255           let s ≝ set_8051_sfr … s SFR_ACC_A low in
256             set_8051_sfr … s SFR_ACC_B high
[475]257        | DIV addr1 addr2 ⇒
[936]258           let s ≝ add_ticks1 s in
[1666]259           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
260           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
[475]261             match acc_b_nat with
[1666]262               [ O ⇒ set_flags … s false (None Bit) true
[475]263               | S o ⇒
264                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
265                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
[1666]266                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
267                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
268                   set_flags … s false (None Bit) false
[475]269               ]
270        | DA addr ⇒
[936]271            let s ≝ add_ticks1 s in
[1666]272            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
273              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
274                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
[475]275                let cy_flag ≝ get_index' ? O ? flags in
276                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
277                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
278                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
279                    let new_acc ≝ nu @@ acc_nl' in
[1666]280                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
281                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
[475]282                  else
283                    s
284              else
285                s
286        | CLR addr ⇒
[1666]287          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
[1534]288            [ ACC_A ⇒ λacc_a: True.
289              let s ≝ add_ticks1 s in
[1666]290               set_arg_8 … s ACC_A (zero 8)
[1534]291            | CARRY ⇒ λcarry: True.
292              let s ≝ add_ticks1 s in
[1666]293               set_arg_1 … s CARRY false
[1534]294            | BIT_ADDR b ⇒ λbit_addr: True.
295              let s ≝ add_ticks1 s in
[1666]296               set_arg_1 … s (BIT_ADDR b) false
[475]297            | _ ⇒ λother: False. ⊥
298            ] (subaddressing_modein … addr)
299        | CPL addr ⇒
[1666]300          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
[475]301            [ ACC_A ⇒ λacc_a: True.
[1534]302                let s ≝ add_ticks1 s in
[1666]303                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]304                let new_acc ≝ negation_bv ? old_acc in
[1666]305                 set_8051_sfr … s SFR_ACC_A new_acc
[475]306            | CARRY ⇒ λcarry: True.
[1534]307                let s ≝ add_ticks1 s in
[1666]308                let old_cy_flag ≝ get_arg_1 … s CARRY true in
[475]309                let new_cy_flag ≝ ¬old_cy_flag in
[1666]310                 set_arg_1 … s CARRY new_cy_flag
[475]311            | BIT_ADDR b ⇒ λbit_addr: True.
[1534]312                let s ≝ add_ticks1 s in
[1666]313                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
[475]314                let new_bit ≝ ¬old_bit in
[1666]315                 set_arg_1 … s (BIT_ADDR b) new_bit
[475]316            | _ ⇒ λother: False. ?
317            ] (subaddressing_modein … addr)
[936]318        | SETB b ⇒
319            let s ≝ add_ticks1 s in
[1666]320            set_arg_1 … s b false
[475]321        | RL _ ⇒ (* DPM: always ACC_A *)
[936]322            let s ≝ add_ticks1 s in
[1666]323            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]324            let new_acc ≝ rotate_left … 1 old_acc in
[1666]325              set_8051_sfr … s SFR_ACC_A new_acc
[475]326        | RR _ ⇒ (* DPM: always ACC_A *)
[936]327            let s ≝ add_ticks1 s in
[1666]328            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]329            let new_acc ≝ rotate_right … 1 old_acc in
[1666]330              set_8051_sfr … s SFR_ACC_A new_acc
[475]331        | RLC _ ⇒ (* DPM: always ACC_A *)
[936]332            let s ≝ add_ticks1 s in
[1666]333            let old_cy_flag ≝ get_cy_flag ?? s in
334            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]335            let new_cy_flag ≝ get_index' ? O ? old_acc in
336            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
[1666]337            let s ≝ set_arg_1 … s CARRY new_cy_flag in
338              set_8051_sfr … s SFR_ACC_A new_acc
[475]339        | RRC _ ⇒ (* DPM: always ACC_A *)
[936]340            let s ≝ add_ticks1 s in
[1666]341            let old_cy_flag ≝ get_cy_flag ?? s in
342            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]343            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
344            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
[1666]345            let s ≝ set_arg_1 … s CARRY new_cy_flag in
346              set_8051_sfr … s SFR_ACC_A new_acc
[475]347        | SWAP _ ⇒ (* DPM: always ACC_A *)
[936]348            let s ≝ add_ticks1 s in
[1666]349            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]350            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
351            let new_acc ≝ nl @@ nu in
[1666]352              set_8051_sfr … s SFR_ACC_A new_acc
[475]353        | PUSH addr ⇒
[1666]354            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with
[475]355              [ DIRECT d ⇒ λdirect: True.
[1534]356                let s ≝ add_ticks1 s in
[1666]357                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
358                let s ≝ set_8051_sfr … s SFR_SP new_sp in
359                  write_at_stack_pointer … s d
[475]360              | _ ⇒ λother: False. ⊥
361              ] (subaddressing_modein … addr)
362        | POP addr ⇒
[936]363            let s ≝ add_ticks1 s in
[1666]364            let contents ≝ read_at_stack_pointer ?? s in
365            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
366            let s ≝ set_8051_sfr … s SFR_SP new_sp in
367              set_arg_8 … s addr contents
[475]368        | XCH addr1 addr2 ⇒
[936]369            let s ≝ add_ticks1 s in
[1666]370            let old_addr ≝ get_arg_8 … s false addr2 in
371            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
372            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
373              set_arg_8 … s addr2 old_acc
[475]374        | XCHD addr1 addr2 ⇒
[936]375            let s ≝ add_ticks1 s in
[1666]376            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
377            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
[475]378            let new_acc ≝ acc_nu @@ arg_nl in
379            let new_arg ≝ arg_nu @@ acc_nl in
[1666]380            let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
381              set_arg_8 … s addr2 new_arg
[475]382        | RET ⇒
[936]383            let s ≝ add_ticks1 s in
[1666]384            let high_bits ≝ read_at_stack_pointer ?? s in
385            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
386            let s ≝ set_8051_sfr … s SFR_SP new_sp in
387            let low_bits ≝ read_at_stack_pointer ?? s in
388            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
389            let s ≝ set_8051_sfr … s SFR_SP new_sp in
[475]390            let new_pc ≝ high_bits @@ low_bits in
[1666]391              set_program_counter … s new_pc
[475]392        | RETI ⇒
[936]393            let s ≝ add_ticks1 s in
[1666]394            let high_bits ≝ read_at_stack_pointer ?? s in
395            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
396            let s ≝ set_8051_sfr … s SFR_SP new_sp in
397            let low_bits ≝ read_at_stack_pointer ?? s in
398            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
399            let s ≝ set_8051_sfr … s SFR_SP new_sp in
[475]400            let new_pc ≝ high_bits @@ low_bits in
[1666]401              set_program_counter … s new_pc
[475]402        | MOVX addr ⇒
[936]403          let s ≝ add_ticks1 s in
[475]404          (* DPM: only copies --- doesn't affect I/O *)
405          match addr with
406            [ inl l ⇒
407              let 〈addr1, addr2〉 ≝ l in
[1666]408                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]409            | inr r ⇒
410              let 〈addr1, addr2〉 ≝ r in
[1666]411                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]412            ]
413        | MOV addr ⇒
[936]414          let s ≝ add_ticks1 s in
[475]415          match addr with
416            [ inl l ⇒
417              match l with
418                [ inl l' ⇒
419                  match l' with
420                    [ inl l'' ⇒
421                      match l'' with
422                        [ inl l''' ⇒
423                          match l''' with
424                            [ inl l'''' ⇒
425                              let 〈addr1, addr2〉 ≝ l'''' in
[1666]426                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]427                            | inr r'''' ⇒
428                              let 〈addr1, addr2〉 ≝ r'''' in
[1666]429                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]430                            ]
431                        | inr r''' ⇒
432                          let 〈addr1, addr2〉 ≝ r''' in
[1666]433                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]434                        ]
435                    | inr r'' ⇒
436                      let 〈addr1, addr2〉 ≝ r'' in
[1666]437                       set_arg_16 … s (get_arg_16 … s addr2) addr1
[475]438                    ]
439                | inr r ⇒
440                  let 〈addr1, addr2〉 ≝ r in
[1666]441                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
[475]442                ]
443            | inr r ⇒
444              let 〈addr1, addr2〉 ≝ r in
[1666]445               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
[475]446            ]
[820]447          | JC addr ⇒
[1666]448                  if get_cy_flag ?? s then
[1534]449                    let s ≝ add_ticks1 s in
[1666]450                      set_program_counter … s (addr_of addr s)
[712]451                  else
[1534]452                    let s ≝ add_ticks2 s in
453                      s
[712]454            | JNC addr ⇒
[1666]455                  if ¬(get_cy_flag ?? s) then
[936]456                   let s ≝ add_ticks1 s in
[1666]457                     set_program_counter … s (addr_of addr s)
[712]458                  else
[936]459                   let s ≝ add_ticks2 s in
[712]460                    s
461            | JB addr1 addr2 ⇒
[1666]462                  if get_arg_1 … s addr1 false then
[936]463                   let s ≝ add_ticks1 s in
[1666]464                    set_program_counter … s (addr_of addr2 s)
[712]465                  else
[936]466                   let s ≝ add_ticks2 s in
[712]467                    s
468            | JNB addr1 addr2 ⇒
[1666]469                  if ¬(get_arg_1 … s addr1 false) then
[936]470                   let s ≝ add_ticks1 s in
[1666]471                    set_program_counter … s (addr_of addr2 s)
[712]472                  else
[936]473                   let s ≝ add_ticks2 s in
[712]474                    s
475            | JBC addr1 addr2 ⇒
[1666]476                  let s ≝ set_arg_1 … s addr1 false in
477                    if get_arg_1 … s addr1 false then
[936]478                     let s ≝ add_ticks1 s in
[1666]479                      set_program_counter … s (addr_of addr2 s)
[712]480                    else
[936]481                     let s ≝ add_ticks2 s in
[712]482                      s
483            | JZ addr ⇒
[1666]484                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
[936]485                     let s ≝ add_ticks1 s in
[1666]486                      set_program_counter … s (addr_of addr s)
[712]487                    else
[936]488                     let s ≝ add_ticks2 s in
[712]489                      s
490            | JNZ addr ⇒
[1666]491                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
[936]492                     let s ≝ add_ticks1 s in
[1666]493                      set_program_counter … s (addr_of addr s)
[712]494                    else
[936]495                     let s ≝ add_ticks2 s in
[712]496                      s
497            | CJNE addr1 addr2 ⇒
498                  match addr1 with
499                    [ inl l ⇒
[822]500                        let 〈addr1, addr2'〉 ≝ l in
[1666]501                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
502                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
503                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
[936]504                            let s ≝ add_ticks1 s in
[1666]505                            let s ≝ set_program_counter … s (addr_of addr2 s) in
506                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]507                          else
[936]508                            let s ≝ add_ticks2 s in
[1666]509                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]510                    | inr r' ⇒
[822]511                        let 〈addr1, addr2'〉 ≝ r' in
[1666]512                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
513                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
514                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
[936]515                            let s ≝ add_ticks1 s in
[1666]516                            let s ≝ set_program_counter … s (addr_of addr2 s) in
517                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]518                          else
[936]519                            let s ≝ add_ticks2 s in
[1666]520                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]521                    ]
522            | DJNZ addr1 addr2 ⇒
[1666]523              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
524              let s ≝ set_arg_8 … s addr1 result in
[820]525                if ¬(eq_bv ? result (zero 8)) then
[936]526                 let s ≝ add_ticks1 s in
[1666]527                  set_program_counter … s (addr_of addr2 s)
[820]528                else
[936]529                 let s ≝ add_ticks2 s in
[820]530                  s
[1666]531 |_ ⇒ ?            ]. (*15s*)
[1582]532    try (cases(other))
[1547]533    try assumption (*20s*)
[1588]534    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
[820]535    try (
536      @ (execute_1_technical … (subaddressing_modein …))
537      @ I
[1547]538    ) (*66s*)
[1588]539    normalize nodelta /2 by or_introl, or_intror/ (*35s*)
[1666]540    (*CSC: the times are now much longer. I suspect because the inclusion of
541      all StatusProofs makes the search space larger :-( *)
[820]542qed.
543
[1588]544definition execute_1_preinstruction:
545  ∀ticks: nat × nat.
[1666]546  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a →
547  PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'.
[1588]548 
549lemma execute_1_preinstruction_ok:
[1666]550 ∀ticks,a,m,cm,f,i,s.
551  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
552  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s.
553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
[1588]554qed.
555
[1666]556definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
557  Σs': Status cm. clock ?? s' = \snd current + clock … s ≝
558  λcm,s0,instr_pc_ticks.
[928]559    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
[820]560    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
[1666]561    let s ≝ set_program_counter … s0 pc in
562      match instr return λ_.Status cm with
563      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
[822]564        (λx. λs.
[1575]565        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
[1666]566        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
[820]567        | _ ⇒ λabsd. ⊥
[1588]568        ] (subaddressing_modein … x)) instr s
[1575]569      | MOVC addr1 addr2 ⇒
[1666]570          let s ≝ set_clock … s (ticks + clock … s) in
571          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
[757]572            [ ACC_DPTR ⇒ λacc_dptr: True.
[1666]573              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
574              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
[1534]575              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
[1666]576              let result ≝ lookup ? ? new_addr cm (zero ?) in
577                set_8051_sfr … s SFR_ACC_A result
[757]578            | ACC_PC ⇒ λacc_pc: True.
[1666]579              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
580              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in
[757]581              (* DPM: Under specified: does the carry from PC incrementation affect the *)
582              (*      addition of the PC with the DPTR? At the moment, no.              *)
[1666]583              let s ≝ set_program_counter … s inc_pc in
[1534]584              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
[1666]585              let result ≝ lookup ? ? new_addr cm (zero ?) in
586                set_8051_sfr … s SFR_ACC_A result
[757]587            | _ ⇒ λother: False. ⊥
588            ] (subaddressing_modein … addr2)
[1575]589      | JMP _ ⇒ (* DPM: always indirect_dptr *)
[1666]590          let s ≝ set_clock … s (ticks + clock … s) in
591          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
592          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
[1534]593          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
[1666]594          let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
595            set_program_counter … s new_pc
[1575]596      | LJMP addr ⇒
[1666]597          let s ≝ set_clock … s (ticks + clock … s) in
598          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
[820]599            [ ADDR16 a ⇒ λaddr16: True.
[1666]600                set_program_counter … s a
[820]601            | _ ⇒ λother: False. ⊥
602            ] (subaddressing_modein … addr)
[1575]603      | SJMP addr ⇒
[1666]604          let s ≝ set_clock … s (ticks + clock … s) in
605          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
[820]606            [ RELATIVE r ⇒ λrelative: True.
[1666]607                let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in
608                  set_program_counter … s new_pc
[820]609            | _ ⇒ λother: False. ⊥
610            ] (subaddressing_modein … addr)
[1575]611      | AJMP addr ⇒
[1666]612          let s ≝ set_clock … s (ticks + clock … s) in
613          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
[820]614            [ ADDR11 a ⇒ λaddr11: True.
[1666]615              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
[1534]616              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
[820]617              let bit ≝ get_index' ? O ? nl in
[1534]618              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
[820]619              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
[1666]620              let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in
621                set_program_counter … s new_pc
[820]622            | _ ⇒ λother: False. ⊥
623            ] (subaddressing_modein … addr)
[1575]624      | ACALL addr ⇒
[1666]625          let s ≝ set_clock … s (ticks + clock … s) in
626          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
[1575]627            [ ADDR11 a ⇒ λaddr11: True.
[1666]628              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
629              let s ≝ set_8051_sfr … s SFR_SP new_sp in
630              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
631              let s ≝ write_at_stack_pointer … s pc_bl in
632              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
633              let s ≝ set_8051_sfr … s SFR_SP new_sp in
634              let s ≝ write_at_stack_pointer … s pc_bu in
[1575]635              let 〈thr, eig〉 ≝ split ? 3 8 a in
636              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
637              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
[1666]638                set_program_counter … s new_addr
[1575]639            | _ ⇒ λother: False. ⊥
640            ] (subaddressing_modein … addr)
641        | LCALL addr ⇒
[1666]642          let s ≝ set_clock … s (ticks + clock … s) in
643          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
[1575]644            [ ADDR16 a ⇒ λaddr16: True.
[1666]645              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
646              let s ≝ set_8051_sfr … s SFR_SP new_sp in
647              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
648              let s ≝ write_at_stack_pointer … s pc_bl in
649              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
650              let s ≝ set_8051_sfr … s SFR_SP new_sp in
651              let s ≝ write_at_stack_pointer … s pc_bu in
652                set_program_counter … s a
[1575]653            | _ ⇒ λother: False. ⊥
654            ] (subaddressing_modein … addr)
[1666]655        ]. (*10s*)
[1547]656    [||||||||*:try assumption]
[1606]657    [1,2,3,4,5,7: @pi2 (*35s*)
[1666]658    |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] …
[1588]659        (λx. λs.
660        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
[1666]661        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
[1588]662        | _ ⇒ λabsd. ⊥
663        ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H
664    |*: normalize nodelta try // (*17s*)
[1666]665        >clock_set_program_counter // (* Andrea:??*) ]
[475]666qed.
667
[1547]668definition current_instruction_cost ≝
[1666]669  λcm.λs: Status cm.
670    \snd (fetch cm (program_counter … s)).
[1547]671
[1666]672definition execute_1': ∀cm.∀s:Status cm.
673  Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝
674  λcm. λs: Status cm.
675    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
676     execute_1_0 cm s instr_pc_ticks.
[928]677
[1666]678definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
[1588]679
[1666]680lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
681 #cm #s whd in match execute_1; normalize nodelta @pi2
[1588]682qed-. (*x Andrea: indexing takes ages here *)
683
[1666]684definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
685  λticks,cm,s,instr,pc.
686  let s ≝ set_program_counter ?? s pc in
[820]687  let s ≝
688    match instr with
[1666]689    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
690    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
[820]691    | Cost cst ⇒ s
[936]692    | Jmp jmp ⇒
[1666]693       let s ≝ set_clock … s (\fst ticks + clock … s) in
694        set_program_counter … s (address_of_word_labels cm jmp)
[820]695    | Call call ⇒
[1666]696      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
697      let a ≝ address_of_word_labels cm call in
698      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
699      let s ≝ set_8051_sfr … s SFR_SP new_sp in
700      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
701      let s ≝ write_at_stack_pointer … s pc_bl in
702      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
703      let s ≝ set_8051_sfr … s SFR_SP new_sp in
704      let s ≝ write_at_stack_pointer … s pc_bu in
705        set_program_counter … s a
[910]706    | Mov dptr ident ⇒
[1666]707      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
708      let the_preamble ≝ \fst cm in
[1541]709      let data_labels ≝ construct_datalabels the_preamble in
[1666]710        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
[820]711    ]
712  in
713    s.
714  normalize
[1577]715  @I
[820]716qed.
717
[1666]718definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝
719  λticks_of,cm,s.
720  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
721  let ticks ≝ ticks_of (program_counter … s) in
722   execute_1_pseudo_instruction0 ticks cm s instr pc.
[1037]723
[1666]724let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
[475]725  match n with
726    [ O ⇒ s
[1666]727    | S o ⇒ execute o … (execute_1 … s)
[475]728    ].
[820]729
[1666]730let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
[820]731  match n with
732    [ O ⇒ s
[1666]733    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
734    ].
Note: See TracBrowser for help on using the repository browser.