source: src/ASM/Interpret.ma @ 1581

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

Dangling de Bruijn pointer when trying to propagate russell to set_arg_1

File size: 37.2 KB
RevLine 
[1522]1include "ASM/Status.ma".
[698]2include "ASM/Fetch.ma".
[1526]3include "ASM/JMCoercions.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 //
21 # K
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
[1526]122
123lemma set_flags_ignores_clock:
[1534]124 ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).
[1526]125//
126qed.
127
[1547]128lemma set_arg_8_ignores_clock:
[1526]129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
130#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
131#a #E >E //
[1527]132qed.
[1526]133
[1547]134lemma set_program_counter_ignores_clock:
[1534]135  ∀M: Type[0].
136  ∀s: PreStatus M.
137  ∀pc: Word.
138    clock M (set_program_counter … s pc) = clock … s.
139  #M #s #pc %
140qed.
141
[1547]142lemma set_low_internal_ram_ignores_clock:
[1534]143  ∀M: Type[0].
144  ∀s: PreStatus M.
145  ∀ram: BitVectorTrie Byte 7.
146    clock … (set_low_internal_ram … s ram) = clock … s.
147  #M #s #ram %
148qed.
149
[1547]150lemma set_8051_sfr_ignores_clock:
[1534]151  ∀M: Type[0].
152  ∀s: PreStatus M.
153  ∀sfr: SFR8051.
154  ∀v: Byte.
155    clock … (set_8051_sfr ? s sfr v) = clock … s.
156  #M #s #sfr #v %
157qed.
158 
[1547]159lemma clock_set_clock:
[1534]160  ∀M: Type[0].
161  ∀s: PreStatus M.
162  ∀v.
163    clock … (set_clock … s v) = v.
164  #M #s #v %
165qed.
166
[936]167definition execute_1_preinstruction:
[1577]168  ∀ticks: nat × nat.
169  ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a →
170  ∀s: PreStatus m.
171    Σs': PreStatus m.
172      Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) ≝
173  λticks: nat × nat.
174  λa, m: Type[0].
175  λaddr_of: a → PreStatus m → Word.
176  λinstr: preinstruction a.
177  λs: PreStatus m.
178  let add_ticks1 ≝ λs: PreStatus m. set_clock … s (\fst ticks + clock … s) in
179  let add_ticks2 ≝ λs: PreStatus m. set_clock … s (\snd ticks + clock … s) in
180  match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
[475]181        [ ADD addr1 addr2 ⇒
[936]182            let s ≝ add_ticks1 s in
[821]183            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
184                                                   (get_arg_8 ? s false addr2) false in
[475]185            let cy_flag ≝ get_index' ? O  ? flags in
186            let ac_flag ≝ get_index' ? 1 ? flags in
187            let ov_flag ≝ get_index' ? 2 ? flags in
[821]188            let s ≝ set_arg_8 ? s ACC_A result in
189              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]190        | ADDC addr1 addr2 ⇒
[936]191            let s ≝ add_ticks1 s in
[821]192            let old_cy_flag ≝ get_cy_flag ? s in
193            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
194                                                   (get_arg_8 ? s false addr2) old_cy_flag in
[475]195            let cy_flag ≝ get_index' ? O ? flags in
196            let ac_flag ≝ get_index' ? 1 ? flags in
197            let ov_flag ≝ get_index' ? 2 ? flags in
[821]198            let s ≝ set_arg_8 ? s ACC_A result in
199              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]200        | SUBB addr1 addr2 ⇒
[936]201            let s ≝ add_ticks1 s in
[821]202            let old_cy_flag ≝ get_cy_flag ? s in
203            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
204                                                   (get_arg_8 ? s false addr2) old_cy_flag in
[475]205            let cy_flag ≝ get_index' ? O ? flags in
206            let ac_flag ≝ get_index' ? 1 ? flags in
207            let ov_flag ≝ get_index' ? 2 ? flags in
[821]208            let s ≝ set_arg_8 ? s ACC_A result in
209              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]210        | ANL addr ⇒
[936]211          let s ≝ add_ticks1 s in
[475]212          match addr with
213            [ inl l ⇒
214              match l with
215                [ inl l' ⇒
216                  let 〈addr1, addr2〉 ≝ l' in
[821]217                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
[1577]218                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
[475]219                | inr r ⇒
220                  let 〈addr1, addr2〉 ≝ r in
[821]221                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
[1577]222                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val)
[475]223                ]
224            | inr r ⇒
225              let 〈addr1, addr2〉 ≝ r in
[822]226              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
[1577]227                eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s and_val (None ?) (get_ov_flag ? s))
[475]228            ]
229        | ORL addr ⇒
[936]230          let s ≝ add_ticks1 s in
[475]231          match addr with
232            [ inl l ⇒
[1577]233              match l return λ_. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
[475]234                [ inl l' ⇒
235                  let 〈addr1, addr2〉 ≝ l' in
[821]236                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
[1577]237                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
[475]238                | inr r ⇒
239                  let 〈addr1, addr2〉 ≝ r in
[821]240                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
[1577]241                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val)
[475]242                ]
243            | inr r ⇒
244              let 〈addr1, addr2〉 ≝ r in
[821]245              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
[1577]246                eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s or_val (None ?) (get_ov_flag ? s))
[475]247            ]
248        | XRL addr ⇒
[936]249          let s ≝ add_ticks1 s in
[475]250          match addr with
251            [ inl l' ⇒
252              let 〈addr1, addr2〉 ≝ l' in
[821]253              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
[1577]254                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
[475]255            | inr r ⇒
256              let 〈addr1, addr2〉 ≝ r in
[821]257              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
[1577]258                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val)
[475]259            ]
260        | INC addr ⇒
[1577]261            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
[475]262              [ ACC_A ⇒ λacc_a: True.
[1534]263                let s' ≝ add_ticks1 s in
[1526]264                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
[1577]265                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' ACC_A result)
[475]266              | REGISTER r ⇒ λregister: True.
[1534]267                let s' ≝ add_ticks1 s in
[1526]268                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
[1577]269                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (REGISTER r) result)
[475]270              | DIRECT d ⇒ λdirect: True.
[1534]271                let s' ≝ add_ticks1 s in
[1526]272                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
[1577]273                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (DIRECT d) result)
[475]274              | INDIRECT i ⇒ λindirect: True.
[1534]275                let s' ≝ add_ticks1 s in
[1526]276                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
[1577]277                 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (INDIRECT i) result)
[475]278              | DPTR ⇒ λdptr: True.
[1534]279                let s' ≝ add_ticks1 s in
[1526]280                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
281                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
282                let s ≝ set_8051_sfr ? s' SFR_DPL bl in
[1577]283                  eject (PreStatus m) (λx. clock … s' = clock … x) (set_8051_sfr ? s' SFR_DPH bu)
[475]284              | _ ⇒ λother: False. ⊥
285              ] (subaddressing_modein … addr)
[1534]286        | NOP ⇒
287           let s ≝ add_ticks2 s in
288            s
[475]289        | DEC addr ⇒
[936]290           let s ≝ add_ticks1 s in
[821]291           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
[1577]292             eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr result)
[475]293        | MUL addr1 addr2 ⇒
[936]294           let s ≝ add_ticks1 s in
[821]295           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
296           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
[475]297           let product ≝ acc_a_nat * acc_b_nat in
298           let ov_flag ≝ product ≥ 256 in
299           let low ≝ bitvector_of_nat 8 (product mod 256) in
300           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
[821]301           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
[1577]302             set_8051_sfr ? s SFR_ACC_B high
[475]303        | DIV addr1 addr2 ⇒
[936]304           let s ≝ add_ticks1 s in
[821]305           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
306           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
[475]307             match acc_b_nat with
[821]308               [ O ⇒ set_flags ? s false (None Bit) true
[475]309               | S o ⇒
310                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
311                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
[821]312                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
313                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
[1577]314                   set_flags ? s false (None Bit) false
[475]315               ]
316        | DA addr ⇒
[936]317            let s ≝ add_ticks1 s in
[1534]318            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
[821]319              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
320                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
[475]321                let cy_flag ≝ get_index' ? O ? flags in
322                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
323                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
324                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
325                    let new_acc ≝ nu @@ acc_nl' in
[821]326                    let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
327                      set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
[475]328                  else
329                    s
330              else
331                s
332        | CLR addr ⇒
[1577]333          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
[1534]334            [ ACC_A ⇒ λacc_a: True.
335              let s ≝ add_ticks1 s in
[1577]336                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s ACC_A (zero 8))
[1534]337            | CARRY ⇒ λcarry: True.
338              let s ≝ add_ticks1 s in
[1577]339                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY false)
[1534]340            | BIT_ADDR b ⇒ λbit_addr: True.
341              let s ≝ add_ticks1 s in
[1577]342                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) false)
[475]343            | _ ⇒ λother: False. ⊥
344            ] (subaddressing_modein … addr)
345        | CPL addr ⇒
[1577]346          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
[475]347            [ ACC_A ⇒ λacc_a: True.
[1534]348                let s ≝ add_ticks1 s in
[821]349                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]350                let new_acc ≝ negation_bv ? old_acc in
[1577]351                  eject (PreStatus m) (λx. clock … s = clock … x) (set_8051_sfr ? s SFR_ACC_A new_acc)
[475]352            | CARRY ⇒ λcarry: True.
[1534]353                let s ≝ add_ticks1 s in
[821]354                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
[475]355                let new_cy_flag ≝ ¬old_cy_flag in
[1577]356                  eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY new_cy_flag)
[475]357            | BIT_ADDR b ⇒ λbit_addr: True.
[1534]358                let s ≝ add_ticks1 s in
[821]359                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
[475]360                let new_bit ≝ ¬old_bit in
[1577]361                  eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) new_bit)
[475]362            | _ ⇒ λother: False. ?
363            ] (subaddressing_modein … addr)
[936]364        | SETB b ⇒
365            let s ≝ add_ticks1 s in
366            set_arg_1 ? s b false
[475]367        | RL _ ⇒ (* DPM: always ACC_A *)
[936]368            let s ≝ add_ticks1 s in
[821]369            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]370            let new_acc ≝ rotate_left … 1 old_acc in
[821]371              set_8051_sfr ? s SFR_ACC_A new_acc
[475]372        | RR _ ⇒ (* DPM: always ACC_A *)
[936]373            let s ≝ add_ticks1 s in
[821]374            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]375            let new_acc ≝ rotate_right … 1 old_acc in
[821]376              set_8051_sfr ? s SFR_ACC_A new_acc
[475]377        | RLC _ ⇒ (* DPM: always ACC_A *)
[936]378            let s ≝ add_ticks1 s in
[821]379            let old_cy_flag ≝ get_cy_flag ? s in
380            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]381            let new_cy_flag ≝ get_index' ? O ? old_acc in
382            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
[821]383            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
384              set_8051_sfr ? s SFR_ACC_A new_acc
[475]385        | RRC _ ⇒ (* DPM: always ACC_A *)
[936]386            let s ≝ add_ticks1 s in
[821]387            let old_cy_flag ≝ get_cy_flag ? s in
388            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]389            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
390            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
[821]391            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
392              set_8051_sfr ? s SFR_ACC_A new_acc
[475]393        | SWAP _ ⇒ (* DPM: always ACC_A *)
[936]394            let s ≝ add_ticks1 s in
[821]395            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]396            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
397            let new_acc ≝ nl @@ nu in
[821]398              set_8051_sfr ? s SFR_ACC_A new_acc
[475]399        | PUSH addr ⇒
[1577]400            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with
[475]401              [ DIRECT d ⇒ λdirect: True.
[1534]402                let s ≝ add_ticks1 s in
[821]403                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
404                let s ≝ set_8051_sfr ? s SFR_SP new_sp in
405                  write_at_stack_pointer ? s d
[475]406              | _ ⇒ λother: False. ⊥
407              ] (subaddressing_modein … addr)
408        | POP addr ⇒
[936]409            let s ≝ add_ticks1 s in
[821]410            let contents ≝ read_at_stack_pointer ? s in
411            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
412            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
413              set_arg_8 ? s addr contents
[475]414        | XCH addr1 addr2 ⇒
[936]415            let s ≝ add_ticks1 s in
[821]416            let old_addr ≝ get_arg_8 ? s false addr2 in
417            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
418            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
[1577]419              eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr2 old_acc)
[475]420        | XCHD addr1 addr2 ⇒
[936]421            let s ≝ add_ticks1 s in
[821]422            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
423            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
[475]424            let new_acc ≝ acc_nu @@ arg_nl in
425            let new_arg ≝ arg_nu @@ acc_nl in
[821]426            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
427              set_arg_8 ? s addr2 new_arg
[475]428        | RET ⇒
[936]429            let s ≝ add_ticks1 s in
[821]430            let high_bits ≝ read_at_stack_pointer ? s in
431            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
432            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
433            let low_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
[475]436            let new_pc ≝ high_bits @@ low_bits in
[821]437              set_program_counter ? s new_pc
[475]438        | RETI ⇒
[936]439            let s ≝ add_ticks1 s in
[821]440            let high_bits ≝ read_at_stack_pointer ? s in
441            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
442            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
443            let low_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
[475]446            let new_pc ≝ high_bits @@ low_bits in
[821]447              set_program_counter ? s new_pc
[475]448        | MOVX addr ⇒
[936]449          let s ≝ add_ticks1 s in
[475]450          (* DPM: only copies --- doesn't affect I/O *)
451          match addr with
452            [ inl l ⇒
453              let 〈addr1, addr2〉 ≝ l in
[1577]454                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
[475]455            | inr r ⇒
456              let 〈addr1, addr2〉 ≝ r in
[1577]457                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
[475]458            ]
459        | MOV addr ⇒
[936]460          let s ≝ add_ticks1 s in
[475]461          match addr with
462            [ inl l ⇒
463              match l with
464                [ inl l' ⇒
465                  match l' with
466                    [ inl l'' ⇒
467                      match l'' with
468                        [ inl l''' ⇒
469                          match l''' with
470                            [ inl l'''' ⇒
471                              let 〈addr1, addr2〉 ≝ l'''' in
[1577]472                                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
[475]473                            | inr r'''' ⇒
474                              let 〈addr1, addr2〉 ≝ r'''' in
[1577]475                                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
[475]476                            ]
477                        | inr r''' ⇒
478                          let 〈addr1, addr2〉 ≝ r''' in
[1577]479                            eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
[475]480                        ]
481                    | inr r'' ⇒
482                      let 〈addr1, addr2〉 ≝ r'' in
[1577]483                        eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
[475]484                    ]
485                | inr r ⇒
486                  let 〈addr1, addr2〉 ≝ r in
[1577]487                    eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
[475]488                ]
489            | inr r ⇒
490              let 〈addr1, addr2〉 ≝ r in
[1577]491                eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
[475]492            ]
[820]493          | JC addr ⇒
[821]494                  if get_cy_flag ? s then
[1534]495                    let s ≝ add_ticks1 s in
496                      set_program_counter ? s (addr_of addr s)
[712]497                  else
[1534]498                    let s ≝ add_ticks2 s in
499                      s
[712]500            | JNC addr ⇒
[821]501                  if ¬(get_cy_flag ? s) then
[936]502                   let s ≝ add_ticks1 s in
[1577]503                     set_program_counter ? s (addr_of addr s)
[712]504                  else
[936]505                   let s ≝ add_ticks2 s in
[712]506                    s
507            | JB addr1 addr2 ⇒
[821]508                  if get_arg_1 ? s addr1 false then
[936]509                   let s ≝ add_ticks1 s in
510                    set_program_counter ? s (addr_of addr2 s)
[712]511                  else
[936]512                   let s ≝ add_ticks2 s in
[712]513                    s
514            | JNB addr1 addr2 ⇒
[821]515                  if ¬(get_arg_1 ? s addr1 false) then
[936]516                   let s ≝ add_ticks1 s in
517                    set_program_counter ? s (addr_of addr2 s)
[712]518                  else
[936]519                   let s ≝ add_ticks2 s in
[712]520                    s
521            | JBC addr1 addr2 ⇒
[821]522                  let s ≝ set_arg_1 ? s addr1 false in
523                    if get_arg_1 ? s addr1 false then
[936]524                     let s ≝ add_ticks1 s in
525                      set_program_counter ? s (addr_of addr2 s)
[712]526                    else
[936]527                     let s ≝ add_ticks2 s in
[712]528                      s
529            | JZ addr ⇒
[821]530                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
[936]531                     let s ≝ add_ticks1 s in
532                      set_program_counter ? s (addr_of addr s)
[712]533                    else
[936]534                     let s ≝ add_ticks2 s in
[712]535                      s
536            | JNZ addr ⇒
[821]537                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
[936]538                     let s ≝ add_ticks1 s in
539                      set_program_counter ? s (addr_of addr s)
[712]540                    else
[936]541                     let s ≝ add_ticks2 s in
[712]542                      s
543            | CJNE addr1 addr2 ⇒
544                  match addr1 with
545                    [ inl l ⇒
[822]546                        let 〈addr1, addr2'〉 ≝ l in
[821]547                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
[822]548                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
549                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
[936]550                            let s ≝ add_ticks1 s in
[822]551                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
[1577]552                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]553                          else
[936]554                            let s ≝ add_ticks2 s in
[1577]555                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]556                    | inr r' ⇒
[822]557                        let 〈addr1, addr2'〉 ≝ r' in
[821]558                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
[822]559                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
560                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
[936]561                            let s ≝ add_ticks1 s in
[822]562                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
[1577]563                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]564                          else
[936]565                            let s ≝ add_ticks2 s in
[1577]566                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]567                    ]
568            | DJNZ addr1 addr2 ⇒
[821]569              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
570              let s ≝ set_arg_8 ? s addr1 result in
[820]571                if ¬(eq_bv ? result (zero 8)) then
[936]572                 let s ≝ add_ticks1 s in
573                  set_program_counter ? s (addr_of addr2 s)
[820]574                else
[936]575                 let s ≝ add_ticks2 s in
[820]576                  s
[1547]577        ]. (*15s*)
[1577]578    try (destruct(other))
[1547]579    try assumption (*20s*)
[1527]580    try % (*6s*)
[820]581    try (
582      @ (execute_1_technical … (subaddressing_modein …))
583      @ I
[1547]584    ) (*66s*)
[1577]585    try (<set_arg_8_ignores_clock normalize nodelta /demod/ %)
586    try (/demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ %)
587    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %)
588    try (normalize nodelta <set_flags_ignores_clock /demod/ %)
589    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)
590    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
591    try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
[1581]592    [5: /demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock
[1577]593(* XXX: weird open goals here *)
594(*    [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta
595    try (normalize nodelta /demod/ %)
596    try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus)
597
598    try (normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)*)
599    cases daemon
[820]600qed.
601
[1533]602lemma write_at_stack_pointer_ignores_clock:
603  ∀M.∀s: PreStatus M.
604  ∀sp: Byte.
605    clock … (write_at_stack_pointer … s sp) = clock … s.
606  #M #s #sp
607  change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
608   in match (write_at_stack_pointer ???);
609  normalize nodelta
610  cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
611  #nu #nl normalize nodelta;
612  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
[1577]613  normalize nodelta; %
[1533]614qed.
615
[1575]616definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat.
[1577]617  Σs': Status. clock … s' = \snd current + clock … s ≝
[1527]618  λs0,instr_pc_ticks.
[928]619    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
[820]620    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
[1527]621    let s ≝ set_program_counter ? s0 pc in
[1577]622      match instr return λ_. Σs': Status. clock … s' = ticks + clock … s0 with
[1575]623      [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?
[822]624        (λx. λs.
[1575]625        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
[822]626        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
[820]627        | _ ⇒ λabsd. ⊥
[1547]628        ] (subaddressing_modein … x)) instr s)
[1575]629      | MOVC addr1 addr2 ⇒
[936]630          let s ≝ set_clock ? s (ticks + clock ? s) in
[1577]631          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
[757]632            [ ACC_DPTR ⇒ λacc_dptr: True.
[821]633              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
634              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
[1534]635              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
[821]636              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
637                set_8051_sfr ? s SFR_ACC_A result
[757]638            | ACC_PC ⇒ λacc_pc: True.
[821]639              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
[1534]640              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
[757]641              (* DPM: Under specified: does the carry from PC incrementation affect the *)
642              (*      addition of the PC with the DPTR? At the moment, no.              *)
[821]643              let s ≝ set_program_counter ? s inc_pc in
[1534]644              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
[821]645              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
646                set_8051_sfr ? s SFR_ACC_A result
[757]647            | _ ⇒ λother: False. ⊥
648            ] (subaddressing_modein … addr2)
[1575]649      | JMP _ ⇒ (* DPM: always indirect_dptr *)
[936]650          let s ≝ set_clock ? s (ticks + clock ? s) in
[821]651          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
652          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
[1534]653          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
654          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
[821]655            set_program_counter ? s new_pc
[1575]656      | LJMP addr ⇒
[936]657          let s ≝ set_clock ? s (ticks + clock ? s) in
[1577]658          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
[820]659            [ ADDR16 a ⇒ λaddr16: True.
[821]660                set_program_counter ? s a
[820]661            | _ ⇒ λother: False. ⊥
662            ] (subaddressing_modein … addr)
[1575]663      | SJMP addr ⇒
[936]664          let s ≝ set_clock ? s (ticks + clock ? s) in
[1577]665          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
[820]666            [ RELATIVE r ⇒ λrelative: True.
[1534]667                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
[821]668                  set_program_counter ? s new_pc
[820]669            | _ ⇒ λother: False. ⊥
670            ] (subaddressing_modein … addr)
[1575]671      | AJMP addr ⇒
[936]672          let s ≝ set_clock ? s (ticks + clock ? s) in
[1577]673          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
[820]674            [ ADDR11 a ⇒ λaddr11: True.
[1534]675              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
676              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
[820]677              let bit ≝ get_index' ? O ? nl in
[1534]678              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
[820]679              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
[1534]680              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
[821]681                set_program_counter ? s new_pc
[820]682            | _ ⇒ λother: False. ⊥
683            ] (subaddressing_modein … addr)
[1575]684      | ACALL addr ⇒
685          let s ≝ set_clock ? s (ticks + clock ? s) in
[1577]686          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
[1575]687            [ ADDR11 a ⇒ λaddr11: True.
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 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
691              let s ≝ write_at_stack_pointer ? s pc_bl in
692              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
693              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
694              let s ≝ write_at_stack_pointer ? s pc_bu in
695              let 〈thr, eig〉 ≝ split ? 3 8 a in
696              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
697              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
698                set_program_counter ? s new_addr
699            | _ ⇒ λother: False. ⊥
700            ] (subaddressing_modein … addr)
701        | LCALL addr ⇒
702          let s ≝ set_clock ? s (ticks + clock ? s) in
[1577]703          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with
[1575]704            [ ADDR16 a ⇒ λaddr16: True.
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 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
708              let s ≝ write_at_stack_pointer ? s pc_bl in
709              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
710              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
711              let s ≝ write_at_stack_pointer ? s pc_bu in
712                set_program_counter ? s a
713            | _ ⇒ λother: False. ⊥
714            ] (subaddressing_modein … addr)
[1547]715      ]. (*10s*)
[1577]716    try (cases(other))
717    [2: normalize nodelta
718        >set_program_counter_ignores_clock
719        >write_at_stack_pointer_ignores_clock
720        >set_8051_sfr_ignores_clock
721        >write_at_stack_pointer_ignores_clock
722        >set_8051_sfr_ignores_clock >clock_set_clock
723        >set_program_counter_ignores_clock %
724    |*:  cases daemon
725    ]
[1575]726(*
[1547]727    [||||||||*:try assumption]
728    [1,2,3,4,5,7: @sig2 (*7s*)
729    |8: cases (execute_1_preinstruction ??????) #a * #H @H]
730    [2,3: >set_program_counter_ignores_clock normalize nodelta
[1533]731      >write_at_stack_pointer_ignores_clock
732      >set_8051_sfr_ignores_clock
733      >write_at_stack_pointer_ignores_clock
[1547]734      >set_8051_sfr_ignores_clock >clock_set_clock
735      >set_program_counter_ignores_clock
736      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H] (*Andrea: ???*)
737    |1,4,5,6: >set_program_counter_ignores_clock normalize nodelta
738     >clock_set_clock >set_program_counter_ignores_clock
739     cut (∀n,m. n+m-m = n) [1,3,5,7:#n #m /by/ |*: #H @H] (*Andrea: ???*)
740    |7: >set_8051_sfr_ignores_clock normalize nodelta
741      >clock_set_clock >set_program_counter_ignores_clock
742      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]
743    |8: >set_8051_sfr_ignores_clock normalize nodelta
744      >set_program_counter_ignores_clock >clock_set_clock
745      >set_program_counter_ignores_clock
[1575]746      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]] *)
[475]747qed.
748
[1547]749definition current_instruction_cost ≝
[1573]750  λs: Status.
751    \snd (fetch (code_memory … s) (program_counter … s)).
[1547]752
[1575]753definition execute_1: ∀s:Status.
[1577]754  Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝
[928]755  λs: Status.
756    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
757     execute_1_0 s instr_pc_ticks.
758
[1037]759definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
760  λticks,s,instr,pc.
[821]761  let s ≝ set_program_counter ? s pc in
[820]762  let s ≝
763    match instr with
[936]764    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
765    | Comment cmt ⇒
766       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
767        s
[820]768    | Cost cst ⇒ s
[936]769    | Jmp jmp ⇒
770       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
771        set_program_counter ? s (address_of_word_labels s jmp)
[820]772    | Call call ⇒
[936]773      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
[822]774      let a ≝ address_of_word_labels s call in
[821]775      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
776      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
777      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
778      let s ≝ write_at_stack_pointer ? s pc_bl in
779      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
780      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
781      let s ≝ write_at_stack_pointer ? s pc_bu in
782        set_program_counter ? s a
[910]783    | Mov dptr ident ⇒
[936]784      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
[1541]785      let the_preamble ≝ \fst (code_memory ? s) in
786      let data_labels ≝ construct_datalabels the_preamble in
[1515]787        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
[820]788    ]
789  in
790    s.
791  normalize
[1577]792  @I
[820]793qed.
794
[1037]795definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
796  λticks_of,s.
797  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
798  let ticks ≝ ticks_of (program_counter ? s) in
799   execute_1_pseudo_instruction0 ticks s instr pc.
800
[475]801let rec execute (n: nat) (s: Status) on n: Status ≝
802  match n with
803    [ O ⇒ s
804    | S o ⇒ execute o (execute_1 s)
805    ].
[820]806
[936]807let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
[820]808  match n with
809    [ O ⇒ s
[822]810    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
[820]811    ].
Note: See TracBrowser for help on using the repository browser.