-(* operatore abs *)
-ndefinition abs_w16 ≝
-λw:word16.match getMSB_w16 w with
- [ true ⇒ compl_w16 w | false ⇒ w ].
-
-(* operatore x in [inf,sup] o in sup],[inf *)
-ndefinition inrange_w16 ≝
-λx,inf,sup:word16.
- match le_w16 inf sup with
- [ true ⇒ and_bool | false ⇒ or_bool ]
- (le_w16 inf x) (le_w16 x sup).
-
-(* operatore moltiplicazione senza segno *)
-(* 〈a1,a2〉 * 〈b1,b2〉 = (a1*b1) x0 x0 + x0 (a1*b2) x0 + x0 (a2*b1) x0 + x0 x0 (a2*b2) *)
-ndefinition mulu_b8_aux ≝
-λw.nat_it ? rol_w16 w nat4.
-
-ndefinition mulu_b8 ≝
-λb1,b2:byte8.
- plus_w16_d_d 〈(mulu_ex (cnH ? b1) (cnH ? b2)):〈x0,x0〉〉
- (plus_w16_d_d (mulu_b8_aux (extu_w16 (mulu_ex (cnH ? b1) (cnL ? b2))))
- (plus_w16_d_d (mulu_b8_aux (extu_w16 (mulu_ex (cnL ? b1) (cnH ? b2))))
- (extu_w16 (mulu_ex (cnL ? b1) (cnL ? b2))))).
-
-(* operatore moltiplicazione con segno *)
-(* x * y = sgn(x) * sgn(y) * |x| * |y| *)
-ndefinition muls_b8 ≝
-λb1,b2:byte8.
-(* ++/-- → +, +-/-+ → - *)
- match (getMSB_b8 b1) ⊙ (getMSB_b8 b2) with
- (* +- -+ → - *)
- [ true ⇒ compl_w16
- (* ++/-- → + *)
- | false ⇒ λx.x ] (mulu_b8 (abs_b8 b1) (abs_b8 b2)).
+(*
+ operatore moltiplicazione senza segno: b*b=[0x0000,0xFE01]
+ ... in pratica (〈a,b〉*〈c,d〉) = (a*c)<<8+(a*d)<<4+(b*c)<<4+(b*d)
+*)
+ndefinition mul_b8 ≝
+λb1,b2:byte8.match b1 with
+[ mk_byte8 b1h b1l ⇒ match b2 with
+[ mk_byte8 b2h b2l ⇒ match mul_ex b1l b2l with
+[ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with
+[ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
+[ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
+[ 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〉〉
+]]]]]].