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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/word16_lemmas.ma".
24 include "freescale/opcode_base_lemmas1.ma".
25 include "freescale/status.ma".
26 include "freescale/option_lemmas.ma".
27 include "freescale/prod_lemmas.ma".
29 (* *********************************** *)
30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
31 (* *********************************** *)
33 nlemma aluHC05_destruct_1 :
34 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
35 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
37 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
38 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
39 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
40 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
46 nlemma aluHC05_destruct_2 :
47 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
48 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
50 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
51 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
52 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
53 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
59 nlemma aluHC05_destruct_3 :
60 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
61 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
63 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
64 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
65 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
66 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
72 nlemma aluHC05_destruct_4 :
73 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
74 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
76 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
77 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
78 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
79 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
85 nlemma aluHC05_destruct_5 :
86 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
87 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
89 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
90 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
91 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
92 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
98 nlemma aluHC05_destruct_6 :
99 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
100 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
102 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
103 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
104 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
105 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
111 nlemma aluHC05_destruct_7 :
112 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
113 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
115 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
116 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
117 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
118 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
124 nlemma aluHC05_destruct_8 :
125 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
126 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
128 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
129 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
130 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
131 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
137 nlemma aluHC05_destruct_9 :
138 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
139 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
141 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
142 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
143 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
144 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
150 nlemma aluHC05_destruct_10 :
151 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
152 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
154 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
155 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
156 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
157 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
163 nlemma aluHC05_destruct_11 :
164 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
165 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
167 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
168 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
169 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
170 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
176 nlemma aluHC05_destruct_12 :
177 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
178 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
180 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
181 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
182 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
183 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
189 nlemma aluHC05_destruct_13 :
190 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
191 mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
193 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
194 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
195 nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
196 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
202 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
205 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
207 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
209 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
210 (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗ (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
211 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
212 (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
213 (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗ (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
214 (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
215 (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
216 nrewrite > (symmetric_eqb8 x1 y1);
217 nrewrite > (symmetric_eqb8 x2 y2);
218 nrewrite > (symmetric_eqw16 x3 y3);
219 nrewrite > (symmetric_eqw16 x4 y4);
220 nrewrite > (symmetric_eqw16 x5 y5);
221 nrewrite > (symmetric_eqw16 x6 y6);
222 nrewrite > (symmetric_eqw16 x7 y7);
223 nrewrite > (symmetric_eqbool x8 y8);
224 nrewrite > (symmetric_eqbool x9 y9);
225 nrewrite > (symmetric_eqbool x10 y10);
226 nrewrite > (symmetric_eqbool x11 y11);
227 nrewrite > (symmetric_eqbool x12 y12);
228 nrewrite > (symmetric_eqbool x13 y13);
232 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = alu2.
235 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
237 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
238 nchange in H:(%) with (
239 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
240 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
241 (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
242 (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
243 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
244 (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
245 (eq_bool x13 y13)) = true);
246 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
247 nletin H1 ≝ (andb_true_true_l ?? H);
248 nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r ?? (andb_true_true_l ?? H)));
249 nletin H2 ≝ (andb_true_true_l ?? H1);
250 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
251 nletin H3 ≝ (andb_true_true_l ?? H2);
252 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
253 nletin H4 ≝ (andb_true_true_l ?? H3);
254 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
255 nletin H5 ≝ (andb_true_true_l ?? H4);
256 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
257 nletin H6 ≝ (andb_true_true_l ?? H5);
258 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
259 nletin H7 ≝ (andb_true_true_l ?? H6);
260 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
261 nletin H8 ≝ (andb_true_true_l ?? H7);
262 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
263 nletin H9 ≝ (andb_true_true_l ?? H8);
264 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H9));
265 nletin H10 ≝ (andb_true_true_l ?? H9);
266 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H10));
267 nletin H11 ≝ (andb_true_true_l ?? H10);
268 nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H11));
269 nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H11));
273 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = true.
276 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
278 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
279 nrewrite > (aluHC05_destruct_1 ?????????????????????????? H);
280 nrewrite > (aluHC05_destruct_2 ?????????????????????????? H);
281 nrewrite > (aluHC05_destruct_3 ?????????????????????????? H);
282 nrewrite > (aluHC05_destruct_4 ?????????????????????????? H);
283 nrewrite > (aluHC05_destruct_5 ?????????????????????????? H);
284 nrewrite > (aluHC05_destruct_6 ?????????????????????????? H);
285 nrewrite > (aluHC05_destruct_7 ?????????????????????????? H);
286 nrewrite > (aluHC05_destruct_8 ?????????????????????????? H);
287 nrewrite > (aluHC05_destruct_9 ?????????????????????????? H);
288 nrewrite > (aluHC05_destruct_10 ?????????????????????????? H);
289 nrewrite > (aluHC05_destruct_11 ?????????????????????????? H);
290 nrewrite > (aluHC05_destruct_12 ?????????????????????????? H);
291 nrewrite > (aluHC05_destruct_13 ?????????????????????????? H);
293 ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
294 (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
295 (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
296 (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
297 (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
298 (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
299 (eq_bool y13 y13)) = true);
300 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
301 nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
302 nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
303 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
304 nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
305 nrewrite > (eq_to_eqw16 y6 y6 (refl_eq ??));
306 nrewrite > (eq_to_eqw16 y7 y7 (refl_eq ??));
307 nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
308 nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
309 nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
310 nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
311 nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
312 nrewrite > (eq_to_eqbool y13 y13 (refl_eq ??));
316 nlemma aluHC08_destruct_1 :
317 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
318 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
320 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
321 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
322 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
323 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
329 nlemma aluHC08_destruct_2 :
330 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
331 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
333 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
334 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
335 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
336 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
342 nlemma aluHC08_destruct_3 :
343 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
344 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
346 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
347 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
348 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
349 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
355 nlemma aluHC08_destruct_4 :
356 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
357 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
359 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
360 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
361 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
362 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
368 nlemma aluHC08_destruct_5 :
369 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
370 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
372 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
373 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
374 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
375 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
381 nlemma aluHC08_destruct_6 :
382 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
383 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
385 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
386 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
387 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
388 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
394 nlemma aluHC08_destruct_7 :
395 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
396 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
398 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
399 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
400 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
401 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
407 nlemma aluHC08_destruct_8 :
408 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
409 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
411 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
412 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
413 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
414 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
420 nlemma aluHC08_destruct_9 :
421 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
422 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
424 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
425 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
426 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
427 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
433 nlemma aluHC08_destruct_10 :
434 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
435 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
437 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
438 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
439 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
440 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
446 nlemma aluHC08_destruct_11 :
447 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
448 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
450 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
451 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
452 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
453 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
459 nlemma aluHC08_destruct_12 :
460 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
461 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
463 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
464 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
465 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
466 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
472 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
475 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
477 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
479 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
480 (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
481 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
482 ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
483 (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
484 (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
485 nrewrite > (symmetric_eqb8 x1 y1);
486 nrewrite > (symmetric_eqb8 x2 y2);
487 nrewrite > (symmetric_eqb8 x3 y3);
488 nrewrite > (symmetric_eqw16 x4 y4);
489 nrewrite > (symmetric_eqw16 x5 y5);
490 nrewrite > (symmetric_eqbool x6 y6);
491 nrewrite > (symmetric_eqbool x7 y7);
492 nrewrite > (symmetric_eqbool x8 y8);
493 nrewrite > (symmetric_eqbool x9 y9);
494 nrewrite > (symmetric_eqbool x10 y10);
495 nrewrite > (symmetric_eqbool x11 y11);
496 nrewrite > (symmetric_eqbool x12 y12);
500 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2.
503 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
505 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
506 nchange in H:(%) with (
507 ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
508 (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
509 (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
510 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
511 nletin H1 ≝ (andb_true_true_l ?? H);
512 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
513 nletin H2 ≝ (andb_true_true_l ?? H1);
514 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
515 nletin H3 ≝ (andb_true_true_l ?? H2);
516 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
517 nletin H4 ≝ (andb_true_true_l ?? H3);
518 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
519 nletin H5 ≝ (andb_true_true_l ?? H4);
520 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
521 nletin H6 ≝ (andb_true_true_l ?? H5);
522 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H6));
523 nletin H7 ≝ (andb_true_true_l ?? H6);
524 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
525 nletin H8 ≝ (andb_true_true_l ?? H7);
526 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
527 nletin H9 ≝ (andb_true_true_l ?? H8);
528 nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H9));
529 nletin H10 ≝ (andb_true_true_l ?? H9);
530 nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H10));
531 nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H10));
535 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true.
538 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
540 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
541 nrewrite > (aluHC08_destruct_1 ???????????????????????? H);
542 nrewrite > (aluHC08_destruct_2 ???????????????????????? H);
543 nrewrite > (aluHC08_destruct_3 ???????????????????????? H);
544 nrewrite > (aluHC08_destruct_4 ???????????????????????? H);
545 nrewrite > (aluHC08_destruct_5 ???????????????????????? H);
546 nrewrite > (aluHC08_destruct_6 ???????????????????????? H);
547 nrewrite > (aluHC08_destruct_7 ???????????????????????? H);
548 nrewrite > (aluHC08_destruct_8 ???????????????????????? H);
549 nrewrite > (aluHC08_destruct_9 ???????????????????????? H);
550 nrewrite > (aluHC08_destruct_10 ???????????????????????? H);
551 nrewrite > (aluHC08_destruct_11 ???????????????????????? H);
552 nrewrite > (aluHC08_destruct_12 ???????????????????????? H);
554 ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
555 (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
556 (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
557 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
558 nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
559 nrewrite > (eq_to_eqb8 y3 y3 (refl_eq ??));
560 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
561 nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
562 nrewrite > (eq_to_eqbool y6 y6 (refl_eq ??));
563 nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
564 nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
565 nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
566 nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
567 nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
568 nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
572 nlemma aluRS08_destruct_1 :
573 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
574 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
576 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
577 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
578 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
579 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
585 nlemma aluRS08_destruct_2 :
586 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
587 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
589 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
590 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
591 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
592 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
598 nlemma aluRS08_destruct_3 :
599 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
600 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
602 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
603 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
604 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
605 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
611 nlemma aluRS08_destruct_4 :
612 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
613 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
615 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
616 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
617 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
618 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
624 nlemma aluRS08_destruct_5 :
625 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
626 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
628 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
629 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
630 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
631 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
637 nlemma aluRS08_destruct_6 :
638 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
639 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
641 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
642 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
643 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
644 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
650 nlemma aluRS08_destruct_7 :
651 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
652 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
654 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
655 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
656 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
657 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
663 nlemma aluRS08_destruct_8 :
664 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
665 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
667 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
668 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
669 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
670 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
676 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
679 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
681 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
683 ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
684 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
685 (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
686 (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
687 ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
688 (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
689 (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
690 (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
691 nrewrite > (symmetric_eqb8 x1 y1);
692 nrewrite > (symmetric_eqw16 x2 y2);
693 nrewrite > (symmetric_eqw16 x3 y3);
694 nrewrite > (symmetric_eqw16 x4 y4);
695 nrewrite > (symmetric_eqb8 x5 y5);
696 nrewrite > (symmetric_eqb8 x6 y6);
697 nrewrite > (symmetric_eqbool x7 y7);
698 nrewrite > (symmetric_eqbool x8 y8);
702 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2.
705 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
707 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
708 nchange in H:(%) with (
709 ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
710 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
711 (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
712 (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
713 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
714 nletin H1 ≝ (andb_true_true_l ?? H);
715 nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
716 nletin H2 ≝ (andb_true_true_l ?? H1);
717 nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H2));
718 nletin H3 ≝ (andb_true_true_l ?? H2);
719 nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H3));
720 nletin H4 ≝ (andb_true_true_l ?? H3);
721 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H4));
722 nletin H5 ≝ (andb_true_true_l ?? H4);
723 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H5));
724 nletin H6 ≝ (andb_true_true_l ?? H5);
725 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
726 nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H6));
730 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true.
733 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
735 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
736 nrewrite > (aluRS08_destruct_1 ???????????????? H);
737 nrewrite > (aluRS08_destruct_2 ???????????????? H);
738 nrewrite > (aluRS08_destruct_3 ???????????????? H);
739 nrewrite > (aluRS08_destruct_4 ???????????????? H);
740 nrewrite > (aluRS08_destruct_5 ???????????????? H);
741 nrewrite > (aluRS08_destruct_6 ???????????????? H);
742 nrewrite > (aluRS08_destruct_7 ???????????????? H);
743 nrewrite > (aluRS08_destruct_8 ???????????????? H);
745 ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
746 (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
747 (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
748 (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
749 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
750 nrewrite > (eq_to_eqw16 y2 y2 (refl_eq ??));
751 nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
752 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
753 nrewrite > (eq_to_eqb8 y5 y5 (refl_eq ??));
754 nrewrite > (eq_to_eqb8 y6 y6 (refl_eq ??));
755 nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
756 nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
760 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
764 ##[ ##1: napply (refl_eq ??)
765 ##| ##2,3: nnormalize; #H; napply (refl_eq ??)
766 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
767 #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
769 ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
770 ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
771 nrewrite > (symmetric_eqb8 x1 y1);
772 nrewrite > (symmetric_eqanyop ? x2 y2);
773 nrewrite > (symmetric_eqinstrmode x3 y3);
774 nrewrite > (symmetric_eqb8 x4 y4);
775 nrewrite > (symmetric_eqw16 x5 y5);
780 nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk2.
784 ##[ ##1: nnormalize; #H; napply (refl_eq ??)
785 ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct ??? H1)
786 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
787 #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
788 nchange in H:(%) with (
789 ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
790 nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H));
791 nletin H1 ≝ (andb_true_true_l ?? H);
792 nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H1));
793 nletin H2 ≝ (andb_true_true_l ?? H1);
794 nrewrite > (eqinstrmode_to_eq ?? (andb_true_true_r ?? H2));
795 nletin H3 ≝ (andb_true_true_l ?? H2);
796 nrewrite > (eqanyop_to_eq ??? (andb_true_true_r ?? H3));
797 nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H3));
802 nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = true.
806 ##[ ##1: nnormalize; #H; napply (refl_eq ??)
807 ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ?? H1)
808 ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ?? H1)
809 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
810 #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
811 nrewrite > (quintuple_destruct_1 ??????????????? (option_destruct_some_some ??? H));
812 nrewrite > (quintuple_destruct_2 ??????????????? (option_destruct_some_some ??? H));
813 nrewrite > (quintuple_destruct_3 ??????????????? (option_destruct_some_some ??? H));
814 nrewrite > (quintuple_destruct_4 ??????????????? (option_destruct_some_some ??? H));
815 nrewrite > (quintuple_destruct_5 ??????????????? (option_destruct_some_some ??? H));
817 ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
818 nrewrite > (eq_to_eqb8 x1 x1 (refl_eq ??));
819 nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
820 nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq ??));
821 nrewrite > (eq_to_eqb8 x4 x4 (refl_eq ??));
822 nrewrite > (eq_to_eqw16 x5 x5 (refl_eq ??));
828 nlemma symmetric_forallmemoryranged :
829 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
830 forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
831 forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
832 #t; #chk1; #chk2; #mem1; #mem2; #addrl;
833 napply (list_ind word16 ??? addrl);
834 ##[ ##1: nnormalize; napply (refl_eq ??)
837 ((eq_option byte8 (mem_read t mem1 chk1 a)
838 (mem_read t mem2 chk2 a) eq_b8) ⊗
839 (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
840 ((eq_option byte8 (mem_read t mem2 chk2 a)
841 (mem_read t mem1 chk1 a) eq_b8) ⊗
842 (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
844 nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
849 nlemma anystatus_destruct_1 :
850 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
851 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
855 #y1; #y2; #y3; #y4; #H;
856 nchange with (match mk_any_status m t y1 y2 y3 y4
857 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
863 nlemma anystatus_destruct_2 :
864 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
865 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
869 #y1; #y2; #y3; #y4; #H;
870 nchange with (match mk_any_status m t y1 y2 y3 y4
871 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
877 nlemma anystatus_destruct_3 :
878 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
879 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
883 #y1; #y2; #y3; #y4; #H;
884 nchange with (match mk_any_status m t y1 y2 y3 y4
885 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
891 nlemma anystatus_destruct_4 :
892 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
893 mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
897 #y1; #y2; #y3; #y4; #H;
898 nchange with (match mk_any_status m t y1 y2 y3 y4
899 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
905 nlemma symmetric_eqstatus :
906 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
907 eq_status m t s1 s2 addrl = eq_status m t s2 s1 addrl.
910 ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
911 #s2; ncases s2; #y1; #y2; #y3; #y4;
913 ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
914 ((eq_alu_HC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
915 nrewrite > (symmetric_eqaluHC05 x1 y1)
916 ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
917 #s2; ncases s2; #y1; #y2; #y3; #y4;
919 ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
920 ((eq_alu_HC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
921 nrewrite > (symmetric_eqaluHC08 x1 y1)
922 ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
923 #s2; ncases s2; #y1; #y2; #y3; #y4;
925 ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
926 ((eq_alu_RS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
927 nrewrite > (symmetric_eqaluRS08 x1 y1)
929 nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
930 nrewrite > (symmetric_eqclk ? x4 y4);
934 nlemma eqstatus_to_eq :
935 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
936 (eq_status m t s1 s2 addrl = true) →
937 ((alu m t s1 = alu m t s2) ∧
938 (clk_desc m t s1 = clk_desc m t s2) ∧
939 ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
940 (mem_desc m t s1) (mem_desc m t s2) addrl) = true)).
943 ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
944 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
945 nchange in H:(%) with (
946 ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
947 nrewrite > (eqaluHC05_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
948 ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
949 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
950 nchange in H:(%) with (
951 ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
952 nrewrite > (eqaluHC08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
953 ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
954 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
955 nchange in H:(%) with (
956 ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
957 nrewrite > (eqaluRS08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
959 nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
960 nrewrite > (andb_true_true_r ?? (andb_true_true_l ?? H));
961 nrewrite > (eqclk_to_eq ??? (andb_true_true_r ?? H));
962 napply (conj ?? (conj ?? (refl_eq ??) (refl_eq ??)) (refl_eq ??)).
965 nlemma eq_to_eqstatus_strong :
966 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
967 s1 = s2 → (eq_status m t s1 s2 addrl = true).
970 ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
971 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
973 ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
974 nrewrite > (anystatus_destruct_1 ?????????? H);
975 nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
976 ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
977 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
979 ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
980 nrewrite > (anystatus_destruct_1 ?????????? H);
981 nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
982 ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
983 #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
985 ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
986 nrewrite > (anystatus_destruct_1 ?????????? H);
987 nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
989 nrewrite > (anystatus_destruct_2 ?????????? H);
990 nrewrite > (anystatus_destruct_3 ?????????? H);
991 nrewrite > (anystatus_destruct_4 ?????????? H);
992 nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
993 nchange with ((forall_memory_ranged ?????? ⊗ true) =true);
994 nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
995 nchange with (forall_memory_ranged ?????? = true);
996 napply (list_ind word16 ??? addrl);
997 ##[ ##1,3,5,7: nnormalize; napply (refl_eq ??)
998 ##| ##2,4,6,8: #a; #l'; #H;
1000 ((eq_option byte8 (mem_read t y2 y3 a)
1001 (mem_read t y2 y3 a) eq_b8) ⊗
1002 (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
1004 nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq ??));
1010 nlemma eq_to_eqstatus_weak :
1011 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1012 (alu m t s1 = alu m t s2) →
1013 (clk_desc m t s1 = clk_desc m t s2) →
1014 ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1015 (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
1016 (eq_status m t s1 s2 addrl = true).
1019 ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1020 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1021 nchange with (((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1022 nchange in H:(%) with (x1 = y1);
1024 nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
1025 ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
1026 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1027 nchange with (((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1028 nchange in H:(%) with (x1 = y1);
1030 nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
1031 ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1032 #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1033 nchange with (((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1034 nchange in H:(%) with (x1 = y1);
1036 nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
1038 nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
1040 nchange in H1:(%) with (x4 = y4);
1042 nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
1044 napply (refl_eq ??).