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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/byte8_lemmas.ma".
28 include "freescale/word16.ma".
34 nlemma word16_destruct_1 :
36 mk_word16 x1 y1 = mk_word16 x2 y2 → x1 = x2.
37 #x1; #x2; #y1; #y2; #H;
38 nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]);
44 nlemma word16_destruct_2 :
46 mk_word16 x1 y1 = mk_word16 x2 y2 → y1 = y2.
47 #x1; #x2; #y1; #y2; #H;
48 nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]);
54 nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
59 nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4)));
60 nrewrite > (symmetric_eqb8 b1 b3);
61 nrewrite > (symmetric_eqb8 b2 b4);
65 nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
70 nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4)));
71 nrewrite > (symmetric_andb8 b1 b3);
72 nrewrite > (symmetric_andb8 b2 b4);
76 nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)).
84 nchange with (mk_word16 (and_b8 (and_b8 b1 b3) b5) (and_b8 (and_b8 b2 b4) b6) =
85 mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6)));
86 nrewrite < (associative_andb8 b1 b3 b5);
87 nrewrite < (associative_andb8 b2 b4 b6);
91 nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
96 nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4)));
97 nrewrite > (symmetric_orb8 b1 b3);
98 nrewrite > (symmetric_orb8 b2 b4);
102 nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)).
110 nchange with (mk_word16 (or_b8 (or_b8 b1 b3) b5) (or_b8 (or_b8 b2 b4) b6) =
111 mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6)));
112 nrewrite < (associative_orb8 b1 b3 b5);
113 nrewrite < (associative_orb8 b2 b4 b6);
117 nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
122 nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4)));
123 nrewrite > (symmetric_xorb8 b1 b3);
124 nrewrite > (symmetric_xorb8 b2 b4);
128 nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)).
136 nchange with (mk_word16 (xor_b8 (xor_b8 b1 b3) b5) (xor_b8 (xor_b8 b2 b4) b6) =
137 mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6)));
138 nrewrite < (associative_xorb8 b1 b3 b5);
139 nrewrite < (associative_xorb8 b2 b4 b6);
143 nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c.
150 match plus_b8_dc_dc b2 b4 c with
151 [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
152 [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]] =
153 match plus_b8_dc_dc b4 b2 c with
154 [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
155 [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]]);
156 nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
157 ncases (plus_b8_dc_dc b2 b4 c);
160 match plus_b8_dc_dc b1 b3 c1 with
161 [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ] =
162 match plus_b8_dc_dc b3 b1 c1 with
163 [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ]);
164 nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
168 nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c.
175 match plus_b8_dc_dc b2 b4 c with
176 [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
177 match plus_b8_dc_dc b4 b2 c with
178 [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
179 nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
180 ncases (plus_b8_dc_dc b2 b4 c);
182 nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉);
183 nrewrite > (symmetric_plusb8_dc_d b1 b3 c1);
187 nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c.
194 plus_b8_dc_c b1 b3 (plus_b8_dc_c b2 b4 c) =
195 plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c));
196 nrewrite > (symmetric_plusb8_dc_c b4 b2 c);
197 nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c));
201 nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1.
208 match plus_b8_d_dc b2 b4 with
209 [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
210 [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]] =
211 match plus_b8_d_dc b4 b2 with
212 [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
213 [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]]);
214 nrewrite > (symmetric_plusb8_d_dc b4 b2);
215 ncases (plus_b8_d_dc b2 b4);
218 match plus_b8_dc_dc b1 b3 c with
219 [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ] =
220 match plus_b8_dc_dc b3 b1 c with
221 [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ]);
222 nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
226 nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
233 match plus_b8_d_dc b2 b4 with
234 [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
235 match plus_b8_d_dc b4 b2 with
236 [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
237 nrewrite > (symmetric_plusb8_d_dc b4 b2);
238 ncases (plus_b8_d_dc b2 b4);
240 nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉);
241 nrewrite > (symmetric_plusb8_dc_d b1 b3 c);
245 nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
252 plus_b8_dc_c b1 b3 (plus_b8_d_c b2 b4) =
253 plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2));
254 nrewrite > (symmetric_plusb8_d_c b4 b2);
255 nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4));
259 nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
265 nchange with (match mul_ex e2 e4 with
266 [ mk_byte8 t1_h t1_l ⇒ match mul_ex e1 e4 with
267 [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
268 [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
269 [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
270 ]]]] = match mul_ex e4 e2 with
271 [ mk_byte8 t1_h t1_l ⇒ match mul_ex e3 e2 with
272 [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
273 [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
274 [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
276 nrewrite < (symmetric_mulex e2 e4);
277 ncases (mul_ex e2 e4);
279 nchange with (match mul_ex e1 e4 with
280 [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
281 [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
282 [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
283 ]]] = match mul_ex e3 e2 with
284 [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
285 [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
286 [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
288 ncases (mul_ex e3 e2);
290 ncases (mul_ex e1 e4);
292 nchange with (match mul_ex e1 e3 with
293 [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
294 ] = match mul_ex e3 e1 with
295 [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
297 nrewrite < (symmetric_mulex e1 e3);
298 ncases (mul_ex e1 e3);
300 nchange with ((plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉) =
301 (plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉));
302 nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉);
306 nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
311 nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true);
313 nrewrite < (eqb8_to_eq ?? (andb_true_true_l ?? H));
314 nrewrite < (eqb8_to_eq ?? (andb_true_true_r ?? H));
318 nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
324 nrewrite < (word16_destruct_1 ???? H);
325 nrewrite < (word16_destruct_2 ???? H);
326 nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true);
327 nrewrite > (eq_to_eqb8 b3 b3 (refl_eq ??));
328 nrewrite > (eq_to_eqb8 b4 b4 (refl_eq ??));