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 set "baseuri" "cic:/matita/freescale/word16".
29 (*include "/media/VIRTUOSO/freescale/byte8.ma".*)
30 include "freescale/byte8.ma".
32 (* ********************** *)
33 (* DEFINIZIONE DELLE WORD *)
34 (* ********************** *)
36 record word16 : Type ≝
43 notation "〈x:y〉" non associative with precedence 80
44 for @{ 'mk_word16 $x $y }.
45 interpretation "mk_word16" 'mk_word16 x y =
46 (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
49 definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
53 λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with
55 | false ⇒ match gt_b8 (w16h w1) (w16h w2) with
57 | false ⇒ lt_b8 (w16l w1) (w16l w2) ]].
60 definition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2).
63 definition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2).
66 definition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2).
70 λw1,w2:word16.mk_word16 (and_b8 (w16h w1) (w16h w2)) (and_b8 (w16l w1) (w16l w2)).
74 λw1,w2:word16.mk_word16 (or_b8 (w16h w1) (w16h w2)) (or_b8 (w16l w1) (w16l w2)).
78 λw1,w2:word16.mk_word16 (xor_b8 (w16h w1) (w16h w2)) (xor_b8 (w16l w1) (w16l w2)).
80 (* operatore rotazione destra con carry *)
82 λw:word16.λc:bool.match rcr_b8 (w16h w) c with
83 [ pairT wh' c' ⇒ match rcr_b8 (w16l w) c' with
84 [ pairT wl' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
86 (* operatore shift destro *)
88 λw:word16.match rcr_b8 (w16h w) false with
89 [ pairT wh' c' ⇒ match rcr_b8 (w16l w) c' with
90 [ pairT wl' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
92 (* operatore rotazione destra *)
94 λw:word16.match rcr_b8 (w16h w) false with
95 [ pairT wh' c' ⇒ match rcr_b8 (w16l w) c' with
96 [ pairT wl' c'' ⇒ match c'' with
97 [ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
98 | false ⇒ mk_word16 wh' wl' ]]].
100 (* operatore rotazione destra n-volte *)
101 let rec ror_w16_n (w:word16) (n:nat) on n ≝
104 | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
106 (* operatore rotazione sinistra con carry *)
108 λw:word16.λc:bool.match rcl_b8 (w16l w) c with
109 [ pairT wl' c' ⇒ match rcl_b8 (w16h w) c' with
110 [ pairT wh' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
112 (* operatore shift sinistro *)
114 λw:word16.match rcl_b8 (w16l w) false with
115 [ pairT wl' c' ⇒ match rcl_b8 (w16h w) c' with
116 [ pairT wh' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
118 (* operatore rotazione sinistra *)
120 λw:word16.match rcl_b8 (w16l w) false with
121 [ pairT wl' c' ⇒ match rcl_b8 (w16h w) c' with
122 [ pairT wh' c'' ⇒ match c'' with
123 [ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
124 | false ⇒ mk_word16 wh' wl' ]]].
126 (* operatore rotazione sinistra n-volte *)
127 let rec rol_w16_n (w:word16) (n:nat) on n ≝
130 | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
132 (* operatore not/complemento a 1 *)
134 λw:word16.mk_word16 (not_b8 (w16h w)) (not_b8 (w16l w)).
136 (* operatore somma con carry *)
137 definition plus_w16 ≝
138 λw1,w2:word16.λc:bool.
139 match plus_b8 (w16l w1) (w16l w2) c with
140 [ pairT l c' ⇒ match plus_b8 (w16h w1) (w16h w2) c' with
141 [ pairT h c'' ⇒ pairT ?? (mk_word16 h l) c'' ]].
143 (* operatore somma senza carry *)
144 definition plus_w16nc ≝
145 λw1,w2:word16.fstT ?? (plus_w16 w1 w2 false).
147 (* operatore carry della somma *)
148 definition plus_w16c ≝
149 λw1,w2:word16.sndT ?? (plus_w16 w1 w2 false).
151 (* operatore Most Significant Bit *)
152 definition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
154 (* word → naturali *)
155 definition nat_of_word16 ≝ λw:word16. 256 * (w16h w) + (nat_of_byte8 (w16l w)).
157 coercion cic:/matita/freescale/word16/nat_of_word16.con.
159 (* naturali → word *)
160 definition word16_of_nat ≝
161 λn.mk_word16 (byte8_of_nat (n / 256)) (byte8_of_nat n).
163 (* operatore predecessore *)
164 definition pred_w16 ≝
165 λw:word16.match eq_b8 (w16l w) (mk_byte8 x0 x0) with
166 [ true ⇒ mk_word16 (pred_b8 (w16h w)) (pred_b8 (w16l w))
167 | false ⇒ mk_word16 (w16h w) (pred_b8 (w16l w)) ].
169 (* operatore successore *)
170 definition succ_w16 ≝
171 λw:word16.match eq_b8 (w16l w) (mk_byte8 xF xF) with
172 [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w))
173 | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ].
175 (* operatore neg/complemento a 2 *)
176 definition compl_w16 ≝
177 λw:word16.match MSB_w16 w with
178 [ true ⇒ succ_w16 (not_w16 w)
179 | false ⇒ not_w16 (pred_w16 w) ].
182 operatore moltiplicazione senza segno: b*b=[0x0000,0xFE01]
183 ... in pratica (〈a,b〉*〈c,d〉) = (a*c)<<8+(a*d)<<4+(b*c)<<4+(b*d)
186 λb1,b2:byte8.match b1 with
187 [ mk_byte8 b1h b1l ⇒ match b2 with
188 [ mk_byte8 b2h b2l ⇒ match mul_ex b1l b2l with
189 [ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with
190 [ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
191 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
192 [ mk_byte8 t4_h t4_l ⇒
195 (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
198 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
200 λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
202 la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
204 [ true ⇒ tripleT ??? 〈xF,xF〉 (w16l w) true
205 | false ⇒ match eq_w16 w 〈〈x0,x0〉:〈x0,x0〉〉 with
206 (* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
207 [ true ⇒ tripleT ??? 〈x0,x0〉 〈x0,x0〉 false
208 (* 1) e' una divisione sensata che produrra' overflow/risultato *)
209 (* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
210 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
211 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
212 (* puo' essere sottratto al dividendo *)
213 | false ⇒ let rec aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
214 let w' ≝ plus_w16nc divd (compl_w16 divs) in
216 [ O ⇒ match le_w16 divs divd with
217 [ true ⇒ tripleT ??? (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
218 | false ⇒ tripleT ??? q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
219 | S c' ⇒ match le_w16 divs divd with
220 [ true ⇒ aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
221 | false ⇒ aux divd (ror_w16 divs) (ror_b8 molt) q c' ]]
222 in aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
224 (* operatore x in [inf,sup] *)
225 definition in_range ≝
226 λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
228 (* iteratore sulle word *)
229 definition forall_word16 ≝
233 P (mk_word16 bh bl ))).
235 (* ********************** *)
236 (* TEOREMI/LEMMMI/ASSIOMI *)
237 (* ********************** *)
239 (* TODO: dimostrare diversamente *)
240 axiom word16_of_nat_nat_of_word16: ∀b. word16_of_nat (nat_of_word16 b) = b.
242 (* TODO: dimostrare diversamente *)
243 axiom lt_nat_of_word16_65536: ∀b. nat_of_word16 b < (256 * 256).
245 (* TODO: dimostrare diversamente *)
246 axiom nat_of_word16_word16_of_nat: ∀n. nat_of_word16 (word16_of_nat n) = n \mod (256 * 256).
248 (* TODO: dimostrare diversamente *)
249 axiom eq_nat_of_word16_n_nat_of_word16_mod_n_65536:
250 ∀n. word16_of_nat n = word16_of_nat (n \mod (256 * 256)).
254 match plus_w16 b1 b2 c with
255 [ pairT r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_word16 r + nat_of_bool c' * (256 * 256)
260 (* TODO: dimostrare diversamente *)
262 ∀b. plus_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) b false = pairT ?? b false.
265 ∀x. plus_w16nc (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) x = x.
268 rewrite > plusw16_O_x;
272 (* TODO: dimostrare diversamente *)
273 axiom eq_nat_of_word16_mod: ∀b. nat_of_word16 b = nat_of_word16 b \mod (256 * 256).
275 (* TODO: dimostrare diversamente *)
277 ∀b1,b2:word16. nat_of_word16 (plus_w16nc b1 b2) = (b1 + b2) \mod (256 * 256).
279 (* TODO: dimostrare diversamente *)
280 axiom eq_eqw16_x0_x0_x0_x0_word16_of_nat_S_false:
281 ∀b. b < (256 * 256 - 1) → eq_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) (word16_of_nat (S b)) = false.
283 axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
285 (* TODO: dimostrare diversamente *)
286 axiom eq_w16pred_S_a_a:
287 ∀a. a < (256 * 256 - 1) → pred_w16 (word16_of_nat (S a)) = word16_of_nat a.
289 (* TODO: dimostrare diversamente *)
291 ∀x:word16.∀n.plus_w16nc (word16_of_nat (x*n)) x = word16_of_nat (x * S n).
293 (* TODO: dimostrare diversamente *)
294 axiom eq_plusw16c_x0_x0_x0_x0_x_false:
295 ∀x.plus_w16c (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) x = false.
297 (* TODO: dimostrare diversamente *)
298 axiom eqw16_true_to_eq: ∀b,b'. eq_w16 b b' = true → b=b'.
300 (* TODO: dimostrare diversamente *)
301 axiom eqw16_false_to_not_eq: ∀b,b'. eq_w16 b b' = false → b ≠ b'.
303 (* TODO: dimostrare diversamente *)
304 axiom word16_of_nat_mod: ∀n.word16_of_nat n = word16_of_nat (n \mod (256 * 256)).
309 lemma ok_mul_b8: ∀b1,b2:byte8. nat_of_word16 (mul_b8 b1 b2) = b1 * b2.
313 change in ⊢ (? ? (? %) ?) with
314 (match mul_ex b1l b2l with
315 [ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with
316 [ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
317 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
318 [ mk_byte8 t4_h t4_l ⇒
321 (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
323 lapply (ok_mul_ex b1l b2l) as ll;
324 lapply (ok_mul_ex b1h b2l) as hl;
325 lapply (ok_mul_ex b2h b1l) as lh;
326 lapply (ok_mul_ex b1h b2h) as hh;
327 elim (mul_ex b1l b2l) (t1_h t1_l);
328 change in ⊢ (? ? (? %) ?) with
329 (match mul_ex b1h b2l with
330 [ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
331 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
332 [ mk_byte8 t4_h t4_l ⇒
335 (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
337 elim (mul_ex b1h b2l) (t2_h t2_l);
338 change in ⊢ (? ? (? %) ?) with
339 (match mul_ex b2h b1l with
340 [ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
341 [ mk_byte8 t4_h t4_l ⇒
344 (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
346 elim (mul_ex b2h b1l) (t3_h t3_l);
347 change in ⊢ (? ? (? %) ?) with
348 (match mul_ex b1h b2h with
349 [ mk_byte8 t4_h t4_l ⇒
352 (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
354 elim (mul_ex b1h b2h) (t4_h t4_l);
355 change in ⊢ (? ? (? %) ?) with
358 (plus_w16nc 〈〈t4_h,t4_l〉:〈x0,x0〉〉 〈〈x0,t3_h〉:〈t3_l,x0〉〉) 〈〈x0,t2_h〉:〈t2_l,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉);
359 do 3 (rewrite > plusw16nc_ok);
360 unfold nat_of_word16;
362 simplify in ⊢ (? ? (? (? (? (? (? (? (? (? ? (? (? ? (? (? %))) ?)) ?) ?) ?) ?) ?) ?) ?) ?);
363 simplify in ⊢ (? ? (? (? (? (? (? (? (? ? (? (? ? (? (? %))) ?)) ?) ?) ?) ?) ?) ?) ?);
364 simplify in ⊢ (? ? (? (? (? (? (? (? (? ? (? ? (? (? %)))) ?) ?) ?) ?) ?) ?) ?);
365 whd in ⊢ (? ? (? (? (? (? (? (? (? ? (? ? %)) ?) ?) ?) ?) ?) ?) ?);
366 whd in ⊢ (? ? (? (? (? (? (? (? (? ? %) ?) ?) ?) ?) ?) ?) ?);
367 simplify in ⊢ (? ? (? (? ? (? (? ? (? (? ? (? %)) ?)) ?)) ?) ?);
368 simplify in ⊢ (? ? (? (? ? (? (? ? (? ? (? (? %)))) ?)) ?) ?);
369 simplify in ⊢ (? ? (? (? ? (? (? ? (? ? %)) ?)) ?) ?);
370 whd in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
371 simplify in ⊢ (? ? (? (? ? (? ? (? (? ? (? (? %))) ?))) ?) ?);
372 simplify in ⊢ (? ? (? (? ? (? ? (? ? (? (? %))))) ?) ?);
373 simplify in ⊢ (? ? ? (? (? (? ? (? %)) ?) ?));
374 simplify in ⊢ (? ? ? (? (? ? (? %)) ?));
375 simplify in ⊢ (? ? ? (? ? (? (? ? (? %)) ?)));
376 simplify in ⊢ (? ? ? (? ? (? ? (? %))));
377 simplify in ⊢ (? ? (? (? ? (? ? (? (? ? (? %)) ?))) ?) ?);
378 simplify in ⊢ (? ? (? (? ? (? ? (? ? (? %)))) ?) ?);
379 simplify in ⊢ (? ? (? (? (? (? ? (? ? (? ? (? %)))) ?) ?) ?) ?);
380 simplify in ⊢ (? ? (? (? (? (? ? (? ? (? (? ? (? %)) ?))) ?) ?) ?) ?);
381 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? (? ? (? %))) ?)) ?) ?) ?) ?);
382 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? (? (? ? (? %)) ?)) ?)) ?) ?) ?) ?);
383 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? ? (? ? (? %)))) ?) ?) ?) ?) ?) ?);
384 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? (? ? (? %))) ?)) ?) ?) ?) ?) ?) ?);
385 simplify in ⊢ (? ? (? (? (? (? (? (? (? (? ? (? (? ? (? %)) ?)) ?) ?) ?) ?) ?) ?) ?) ?);
386 simplify in ⊢ (? ? (? (? (? (? (? (? (? (? ? (? ? (? %))) ?) ?) ?) ?) ?) ?) ?) ?);
387 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? ? (? (? ? (? %)) ?))) ?) ?) ?) ?) ?) ?);
388 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? (? (? ? (? %)) ?)) ?)) ?) ?) ?) ?) ?) ?);
390 change in ⊢ (? ? (? (? ? %) ?) ?) with (16*nat_of_exadecim t1_h+nat_of_exadecim t1_l);
391 unfold nat_of_byte8 in H H1 H2 H3;
392 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? (? (? ? %) ?)) ?)) ?) ?) ?) ?) ?) ?);
393 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? ? (? ? %))) ?) ?) ?) ?) ?) ?);
394 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? (? (? ? %) ?)) ?)) ?) ?) ?) ?);
395 simplify in ⊢ (? ? (? (? (? (? ? (? ? (? ? %))) ?) ?) ?) ?);
398 simplify in ⊢ (? ? (? (? (? (? (? (? ? (? (? ? %) ?)) ?) ?) ?) ?) ?) ?);
399 simplify in ⊢ (? ? (? (? (? (? ? (? (? ? %) ?)) ?) ?) ?) ?);