1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/status/HC05_status_lemmas.ma".
24 include "emulator/status/HC08_status_lemmas.ma".
25 include "emulator/status/RS08_status_lemmas.ma".
26 include "emulator/status/IP2022_status_lemmas.ma".
27 include "emulator/status/status.ma".
28 include "common/option_lemmas.ma".
29 include "common/prod_lemmas.ma".
30 include "emulator/opcodes/pseudo_lemmas.ma".
32 (* *********************************** *)
33 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
34 (* *********************************** *)
36 nlemma symmetric_eqclk : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = eq_clk m clk2 clk1.
38 napply (symmetric_eqoption ? (eq_quintuple …) (symmetric_eqquintuple …));
39 ##[ ##1: napply symmetric_eqw16
40 ##| ##2: napply symmetric_eqb8
41 ##| ##3: napply (symmetric_eqim m)
42 ##| ##4: napply (symmetric_eqpseudo m)
43 ##| ##5: napply symmetric_eqb8
47 nlemma eqclk_to_eq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = true → clk1 = clk2.
49 napply (eqoption_to_eq ? (eq_quintuple …) (eqquintuple_to_eq …));
50 ##[ ##1: napply eqw16_to_eq
51 ##| ##2: napply eqb8_to_eq
52 ##| ##3: napply (eqim_to_eq m)
53 ##| ##4: napply (eqpseudo_to_eq m)
54 ##| ##5: napply eqb8_to_eq
58 nlemma eq_to_eqclk : ∀m.∀clk1,clk2.(clk1 = clk2) → (eq_clk m clk1 clk2 = true).
60 napply (eq_to_eqoption ? (eq_quintuple …) (eq_to_eqquintuple …));
61 ##[ ##1: napply eq_to_eqw16
62 ##| ##2: napply eq_to_eqb8
63 ##| ##3: napply (eq_to_eqim m)
64 ##| ##4: napply (eq_to_eqpseudo m)
65 ##| ##5: napply eq_to_eqb8
69 nlemma neqclk_to_neq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = false → clk1 ≠ clk2.
71 napply (neqoption_to_neq ? (eq_quintuple …) (neqquintuple_to_neq …));
72 ##[ ##1: napply neqw16_to_neq
73 ##| ##2: napply neqb8_to_neq
74 ##| ##3: napply (neqim_to_neq m)
75 ##| ##4: napply (neqpseudo_to_neq m)
76 ##| ##5: napply neqb8_to_neq
80 nlemma neq_to_neqclk : ∀m.∀clk1,clk2.(clk1 ≠ clk2) → (eq_clk m clk1 clk2 = false).
82 napply (neq_to_neqoption ? (eq_quintuple …) (neq_to_neqquintuple …));
83 ##[ ##1: napply neq_to_neqw16
84 ##| ##2: napply neq_to_neqb8
85 ##| ##3: napply (neq_to_neqim m)
86 ##| ##4: napply (neq_to_neqpseudo m)
87 ##| ##5: napply neq_to_neqb8
88 ##| ##6: napply decidable_w16
89 ##| ##7: napply decidable_b8
90 ##| ##8: napply (decidable_im m)
91 ##| ##9: napply (decidable_pseudo m)
92 ##| ##10: napply decidable_b8
96 nlemma decidable_clk : ∀m.∀clk1,clk2:option (aux_clk_type m).decidable (clk1 = clk2).
98 napply (decidable_option ? (decidable_quintuple …));
99 ##[ ##1: napply decidable_w16
100 ##| ##2: napply decidable_b8
101 ##| ##3: napply (decidable_im m)
102 ##| ##4: napply (decidable_pseudo m)
103 ##| ##5: napply decidable_b8
107 nlemma symmetric_forallmemoryranged :
108 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
109 forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
110 forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
111 #t; #chk1; #chk2; #mem1; #mem2; #addrl;
113 ##[ ##1: nnormalize; napply refl_eq
116 ((eq_option byte8 eq_b8 (mem_read t mem1 chk1 a)
117 (mem_read t mem2 chk2 a)) ⊗
118 (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
119 ((eq_option byte8 eq_b8 (mem_read t mem2 chk2 a)
120 (mem_read t mem1 chk1 a)) ⊗
121 (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
123 nrewrite > (symmetric_eqoption ? eq_b8 symmetric_eqb8 (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a));
128 nlemma anystatus_destruct_1 :
129 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
130 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
134 #y1; #y2; #y3; #y4; #H;
135 nchange with (match mk_any_status m t y1 y2 y3 y4
136 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
142 nlemma anystatus_destruct_2 :
143 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
144 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
148 #y1; #y2; #y3; #y4; #H;
149 nchange with (match mk_any_status m t y1 y2 y3 y4
150 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
156 nlemma anystatus_destruct_3 :
157 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
158 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
162 #y1; #y2; #y3; #y4; #H;
163 nchange with (match mk_any_status m t y1 y2 y3 y4
164 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
170 nlemma anystatus_destruct_4 :
171 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
172 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
176 #y1; #y2; #y3; #y4; #H;
177 nchange with (match mk_any_status m t y1 y2 y3 y4
178 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
184 naxiom symmetric_eqanystatus :
185 ∀addrl:list word32.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
186 eq_anystatus m t s1 s2 addrl = eq_anystatus m t s2 s1 addrl.
187 (* !!! si blocca su symmetric_eqalu_HC05 *)
188 (* #addrl; #m; ncases m; #t; #s1;
189 ##[ ##1: nelim s1; #x1; #x2; #x3; #x4;
190 #s2; nelim s2; #y1; #y2; #y3; #y4;
192 ((eq_HC05_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
193 ((eq_HC05_alu y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
194 nrewrite > (symmetric_eqaluHC05 x1 y1)
195 ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
196 #s2; ncases s2; #y1; #y2; #y3; #y4;
198 ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
199 ((eq_aluHC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
200 nrewrite > (symmetric_eqaluHC08 x1 y1)
201 ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
202 #s2; ncases s2; #y1; #y2; #y3; #y4;
204 ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
205 ((eq_aluRS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
206 nrewrite > (symmetric_eqaluRS08 x1 y1)
209 nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
210 nrewrite > (symmetric_eqclk ? x4 y4);
214 nlemma eqanystatus_to_eq :
215 ∀addrl:list word32.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
216 (eq_anystatus m t s1 s2 addrl = true) →
217 And3 (alu m t s1 = alu m t s2)
218 (clk_desc m t s1 = clk_desc m t s2)
219 ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
220 (mem_desc m t s1) (mem_desc m t s2) addrl) = true).
223 ncases s1; #x1; #x2; #x3; #x4;
224 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
225 ##[ ##1: nchange in H:(%) with (
226 ((eq_HC05_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
227 nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
228 ##| ##2,3: nchange in H:(%) with (
229 ((eq_HC08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
230 nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
231 ##| ##4: nchange in H:(%) with (
232 ((eq_RS08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
233 nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
234 ##| ##5: nchange in H:(%) with (
235 ((eq_IP2022_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
236 nrewrite > (eqaluIP2022_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
238 nchange with (And3 (y1 = y1) (x4 = y4) (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
239 nrewrite > (andb_true_true_r … (andb_true_true_l … H));
240 nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
241 napply (conj3 … (refl_eq ? y1) (refl_eq ? y4) (refl_eq ? true)).
244 naxiom eq_to_eqanystatus :
245 ∀addrl:list word32.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
246 (alu m t s1 = alu m t s2) →
247 (clk_desc m t s1 = clk_desc m t s2) →
248 ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
249 (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
250 (eq_anystatus m t s1 s2 addrl = true).
251 (* !!! si blocca su symmetric_eqalu_HC05 *)
253 ncases m; #s1; ncases s1; #x1; #x2; #x3; #x4;
254 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
255 ##[ ##1: nchange with (((eq_HC05_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
256 nchange in H:(%) with (x1 = y1);
258 nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
259 ##| ##2,3: nchange with (((eq_HC08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
260 nchange in H:(%) with (x1 = y1);
262 nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
263 ##| ##4: nchange with (((eq_RS08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
264 nchange in H:(%) with (x1 = y1);
266 nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
269 nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
271 nchange in H1:(%) with (x4 = y4);
273 nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));