-(*
- 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〉〉
-]]]]]].
+(* 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)).