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/status_base.ma".
25 (* *********************************** *)
26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
27 (* *********************************** *)
29 nlemma symmetric_forallmemoryranged :
30 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀sel.∀addrl.
31 forall_memory_ranged t chk1 chk2 mem1 mem2 sel addrl =
32 forall_memory_ranged t chk2 chk1 mem2 mem1 sel addrl.
33 #t; #chk1; #chk2; #mem1; #mem2; #sel; #addrl;
35 ##[ ##1: nnormalize; napply refl_eq
38 ((eqc ? (mem_read t mem1 chk1 sel a)
39 (mem_read t mem2 chk2 sel a)) ⊗
40 (forall_memory_ranged t chk1 chk2 mem1 mem2 sel l)) =
41 ((eqc ? (mem_read t mem2 chk2 sel a)
42 (mem_read t mem1 chk1 sel a)) ⊗
43 (forall_memory_ranged t chk2 chk1 mem2 mem1 sel l)));
45 nrewrite > (symmetric_eqc ? … (mem_read t mem1 chk1 sel a) (mem_read t mem2 chk2 sel a));
50 nlemma anystatus_destruct_1 :
51 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
52 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
56 #y1; #y2; #y3; #y4; #H;
57 nchange with (match mk_any_status m t y1 y2 y3 y4
58 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
64 nlemma anystatus_destruct_2 :
65 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
66 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
70 #y1; #y2; #y3; #y4; #H;
71 nchange with (match mk_any_status m t y1 y2 y3 y4
72 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
78 nlemma anystatus_destruct_3 :
79 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
80 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
84 #y1; #y2; #y3; #y4; #H;
85 nchange with (match mk_any_status m t y1 y2 y3 y4
86 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
92 nlemma anystatus_destruct_4 :
93 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
94 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
98 #y1; #y2; #y3; #y4; #H;
99 nchange with (match mk_any_status m t y1 y2 y3 y4
100 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
106 nlemma eq_to_eqanystatus : ∀m,t.∀s1,s2:any_status m t.s1 = s2 → eq_anystatus m t s1 s2 = true.
108 #s1; ncases s1; #alu1; #mem1; #chk1; #clk1;
109 #s2; ncases s2; #alu2; #mem2; #chk2; #clk2;
111 nrewrite > (anystatus_destruct_1 … H);
112 nrewrite > (anystatus_destruct_2 … H);
113 nrewrite > (anystatus_destruct_3 … H);
114 nrewrite > (anystatus_destruct_4 … H);
116 ((eqc ? alu2 alu2) ⊗ (eqc ? mem2 mem2) ⊗ (eqc ? chk2 chk2) ⊗ (eqc ? clk2 clk2)) = true);
117 nrewrite > (eq_to_eqc ? alu2 alu2 (refl_eq …));
118 nrewrite > (eq_to_eqc ? mem2 mem2 (refl_eq …));
119 nrewrite > (eq_to_eqc ? chk2 chk2 (refl_eq …));
120 nrewrite > (eq_to_eqc ? clk2 clk2 (refl_eq …));
124 nlemma neqanystatus_to_neq : ∀m,t.∀s1,s2:any_status m t.eq_anystatus m t s1 s2 = false → s1 ≠ s2.
125 #m; #t; #s1; #s2; #H;
126 napply (not_to_not (s1 = s2) (eq_anystatus m t s1 s2 = true) …);
127 ##[ ##1: napply (eq_to_eqanystatus m t s1 s2)
128 ##| ##2: napply (eqfalse_to_neqtrue … H)
132 nlemma eqanystatus_to_eq : ∀m,t.∀s1,s2:any_status m t.eq_anystatus m t s1 s2 = true → s1 = s2.
134 #s1; ncases s1; #alu1; #mem1; #chk1; #clk1;
135 #s2; ncases s2; #alu2; #mem2; #chk2; #clk2;
137 ((eqc ? alu1 alu2) ⊗ (eqc ? mem1 mem2) ⊗ (eqc ? chk1 chk2) ⊗ (eqc ? clk1 clk2)) = true → ?);
139 nrewrite > (eqc_to_eq … (andb_true_true_r … H));
140 nletin H1 ≝ (andb_true_true_l … H);
141 nrewrite > (eqc_to_eq … (andb_true_true_r … H1));
142 nletin H2 ≝ (andb_true_true_l … H1);
143 nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
144 nrewrite > (eqc_to_eq … (andb_true_true_l … H2));
148 nlemma neq_to_neqanystatus : ∀m,t.∀s1,s2:any_status m t.s1 ≠ s2 → eq_anystatus m t s1 s2 = false.
149 #m; #t; #s1; #s2; #H;
150 napply (neqtrue_to_eqfalse (eq_anystatus m t s1 s2));
151 napply (not_to_not (eq_anystatus m t s1 s2 = true) (s1 = s2) ? H);
152 napply (eqanystatus_to_eq m t s1 s2).
155 nlemma decidable_anystatus : ∀m,t.∀x,y:any_status m t.decidable (x = y).
156 #m; #t; #x; #y; nnormalize;
157 napply (or2_elim (eq_anystatus m t x y = true) (eq_anystatus m t x y = false) ? (decidable_bexpr ?));
158 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqanystatus_to_eq … H))
159 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqanystatus_to_neq … H))
163 nlemma symmetric_eqanystatus : ∀m,t.symmetricT (any_status m t) bool (eq_anystatus m t).
165 #s1; ncases s1; #alu1; #mem1; #chk1; #clk1;
166 #s2; ncases s2; #alu2; #mem2; #chk2; #clk2;
168 ((eqc ? alu1 alu2) ⊗ (eqc ? mem1 mem2) ⊗ (eqc ? chk1 chk2) ⊗ (eqc ? clk1 clk2)) =
169 ((eqc ? alu2 alu1) ⊗ (eqc ? mem2 mem1) ⊗ (eqc ? chk2 chk1) ⊗ (eqc ? clk2 clk1)));
170 nrewrite > (symmetric_eqc … alu1 alu2);
171 nrewrite > (symmetric_eqc … mem1 mem2);
172 nrewrite > (symmetric_eqc … chk1 chk2);
173 nrewrite > (symmetric_eqc … clk1 clk2);
177 nlemma anystatus_is_comparable : mcu_type → memory_impl → comparable.
178 #m; #t; @ (any_status m t)
179 ##[ napply (mk_any_status m t (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
180 ##| napply forall_anystatus
181 ##| napply eq_anystatus
182 ##| napply eqanystatus_to_eq
183 ##| napply eq_to_eqanystatus
184 ##| napply neqanystatus_to_neq
185 ##| napply neq_to_neqanystatus
186 ##| napply decidable_anystatus
187 ##| napply symmetric_eqanystatus
191 unification hint 0 ≔ M:mcu_type, T:memory_impl ⊢
192 carr (anystatus_is_comparable M T) ≡ any_status M T.