Reify Z.mul_with_split_at_bitwidth

8 files changed, 51 insertions, 10 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 21b208f33..cfa7934ad 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -33,6 +33,7 @@ Section language.
                     with
                     | OpConst _ z => fun _ _ => const_of _ z
                     | Opp TZ TZ => fun _ args => neg_expr _ args
+                    | MulSplit _ _ _ _ _ => fun _ _ => I
                     | AddWithGetCarry _ _ _ _ _ _ => fun _ _ => I
                     | SubWithGetBorrow _ _ _ _ _ _ => fun _ _ => I
                     | _ => fun e _ => gen_expr _ e
@@ -370,6 +371,7 @@ Section language.
          | Opp _ _ as opc
          | IdWithAlt _ _ _ as opc
          | Zselect _ _ _ _ as opc
+         | MulSplit _ _ _ _ _ as opc
          | AddWithCarry _ _ _ _ as opc
          | AddWithGetCarry _ _ _ _ _ _ as opc
          | SubWithBorrow _ _ _ _ as opc
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index 66145080c..dc557f6ec 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -55,6 +55,8 @@ Module Import Bounds.
       := truncation_bounds {| lower := l ; upper := u |}.
     Definition t_map1 (f : Z -> Z) (x : t)
       := truncation_bounds (two_corners f x).
+    Definition t_map2' (f : Z -> Z -> Z) : t -> t -> t
+      := fun x y => four_corners f x y.
     Definition t_map2 (f : Z -> Z -> Z) : t -> t -> t
       := fun x y => truncation_bounds (four_corners f x y).
     Definition t_map3' (f : Z -> Z -> Z -> Z) : t -> t -> t -> t
@@ -66,6 +68,7 @@ Module Import Bounds.
     Definition add : t -> t -> t := t_map2 Z.add.
     Definition sub : t -> t -> t := t_map2 Z.sub.
     Definition mul : t -> t -> t := t_map2 Z.mul.
+    Definition mul' : t -> t -> t := t_map2' Z.mul.
     Definition shl : t -> t -> t := t_map2 Z.shiftl.
     Definition shr : t -> t -> t := t_map2 Z.shiftr.
     Definition max_abs_bound (x : t) : Z
@@ -177,6 +180,8 @@ Module Import Bounds.
     Definition sub_with_get_borrow : t -> t -> t -> t * t
       := fun c x y
          => get_borrow (sub_with_borrow' c x y).
+    Definition mul_split : t -> t -> t * t
+      := fun x y => get_carry (mul' x y).
   End with_bitwidth2.
 
   Module Export Notations.
@@ -212,6 +217,8 @@ Module Import Bounds.
        | Opp _ T => fun x => opp (bit_width_of_base_type T) x
        | IdWithAlt _ _ T => fun xy => id_with_alt (bit_width_of_base_type T) (fst xy) (snd xy)
        | Zselect _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in zselect (bit_width_of_base_type T) c x y
+       | MulSplit carry_boundary_bit_width _ _ T1 T2
+         => fun xy => mul_split (bit_width_of_base_type T1) (bit_width_of_base_type T2) carry_boundary_bit_width (fst xy) (snd xy)
        | AddWithCarry _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in add_with_carry (bit_width_of_base_type T) c x y
        | AddWithGetCarry carry_boundary_bit_width _ _ _ T1 T2
          => fun cxy => let '(c, x, y) := eta3 cxy in
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index e7ec688d3..3c3ac61b2 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -326,9 +326,17 @@ Local Arguments Z.add !_ !_.
 Local Existing Instances Z.add_le_Proper Z.sub_le_flip_le_Proper Z.log2_up_le_Proper Z.pow_Zpos_le_Proper Z.sub_le_eq_Proper Z.add_with_carry_le_Proper.
 Local Hint Extern 1 => progress cbv beta iota : typeclass_instances.
 Local Ltac ibbio_do_cbv :=
-  cbv [Bounds.interp_op Zinterp_op Z.add_with_get_carry SmartFlatTypeMapUnInterp Bounds.add_with_get_carry Bounds.sub_with_get_borrow Bounds.get_carry Bounds.get_borrow Z.get_carry cast_const]; cbn [fst snd].
+  cbv [Bounds.interp_op Zinterp_op Z.add_with_get_carry SmartFlatTypeMapUnInterp Bounds.add_with_get_carry Bounds.sub_with_get_borrow Bounds.get_carry Bounds.get_borrow Z.get_carry cast_const Bounds.mul_split]; cbn [fst snd].
 Local Ltac ibbio_prefin_by_apply :=
   [ > | intros; apply is_bounded_by_truncation_bounds | simpl; reflexivity ].
+Local Ltac handle_mul :=
+  apply monotone_four_corners_genb; try (split; auto);
+  unfold Basics.flip;
+  let x := fresh "x" in
+  intro x;
+  exists (0 <=? x);
+  break_match; Z.ltb_to_lt;
+  intros ???; nia.
 Lemma is_bounded_by_interp_op t tR (opc : op t tR)
       (bs : interp_flat_type Bounds.interp_base_type _)
       (v : interp_flat_type interp_base_type _)
@@ -347,6 +355,12 @@ Proof.
     | split; ibbio_do_cbv;
       [ eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _);
         ibbio_prefin_by_apply
+      | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v / _))   (v:=ZToInterp _);
+        ibbio_prefin_by_apply ]
+    | apply is_bounded_by_truncation_bounds
+    | split; ibbio_do_cbv;
+      [ eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _);
+        ibbio_prefin_by_apply
       | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (-(v / _)))   (v:=ZToInterp _);
         ibbio_prefin_by_apply ] ];
     repeat first [ progress simpl in *
@@ -361,13 +375,7 @@ Proof.
                    end ].
   { apply (@monotone_four_corners true true _ _); split; auto. }
   { apply (@monotone_four_corners true false _ _); split; auto. }
-  { apply monotone_four_corners_genb; try (split; auto);
-      unfold Basics.flip;
-      let x := fresh "x" in
-      intro x;
-        exists (0 <=? x);
-        break_match; Z.ltb_to_lt;
-          intros ???; nia. }
+  { handle_mul. }
   { apply monotone_four_corners_genb; try (split; auto);
       [ eexists; apply Z.shiftl_le_Proper1
       | exists true; apply Z.shiftl_le_Proper2 ]. }
@@ -396,6 +404,10 @@ Proof.
       split; assumption. }
   { destruct_head Bounds.t; cbv [Bounds.zselect' Z.zselect].
     break_innermost_match; split_min_max; omega. }
+  { handle_mul. }
+  { apply Z.mod_bound_min_max; auto. }
+  { handle_mul. }
+  { auto with zarith. }
   { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
   { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
   { apply Z.mod_bound_min_max; auto. }
diff --git a/src/Compilers/Z/CommonSubexpressionElimination.v b/src/Compilers/Z/CommonSubexpressionElimination.v
index e1f506c15..c2b4775c6 100644
--- a/src/Compilers/Z/CommonSubexpressionElimination.v
+++ b/src/Compilers/Z/CommonSubexpressionElimination.v
@@ -22,6 +22,7 @@ Inductive symbolic_op :=
 | SOpp
 | SIdWithAlt
 | SZselect
+| SMulSplit (bitwidth : Z)
 | SAddWithCarry
 | SAddWithGetCarry (bitwidth : Z)
 | SSubWithBorrow
@@ -55,6 +56,8 @@ Definition symbolic_op_leb (x y : symbolic_op) : bool
      | _, SIdWithAlt => false
      | SZselect, _ => true
      | _, SZselect => false
+     | SMulSplit _, _ => true
+     | _, SMulSplit _ => false
      | SAddWithCarry, _ => true
      | _, SAddWithCarry => false
      | SAddWithGetCarry _, _ => true
@@ -82,6 +85,7 @@ Definition symbolize_op s d (opc : op s d) : symbolic_op
      | Opp T Tout => SOpp
      | IdWithAlt T1 T2 Tout => SIdWithAlt
      | Zselect T1 T2 T3 Tout => SZselect
+     | MulSplit bitwidth T1 T2 Tout1 Tout2 => SMulSplit bitwidth
      | AddWithCarry T1 T2 T3 Tout => SAddWithCarry
      | AddWithGetCarry bitwidth T1 T2 T3 Tout1 Tout2 => SAddWithGetCarry bitwidth
      | SubWithBorrow T1 T2 T3 Tout => SSubWithBorrow
@@ -101,6 +105,8 @@ Definition denote_symbolic_op s d (opc : symbolic_op) : option (op s d)
      | SOpp, Tbase _, Tbase _ => Some (Opp _ _)
      | SIdWithAlt, Prod (Tbase _) (Tbase _), Tbase _ => Some (IdWithAlt _ _ _)
      | SZselect, Prod (Prod (Tbase _) (Tbase _)) (Tbase _), Tbase _ => Some (Zselect _ _ _ _)
+     | SMulSplit bitwidth, Prod (Tbase _) (Tbase _), Prod (Tbase _) (Tbase _)
+       => Some (MulSplit bitwidth _ _ _ _)
      | SAddWithCarry, Prod (Prod (Tbase _) (Tbase _)) (Tbase _), Tbase _ => Some (AddWithCarry _ _ _ _)
      | SAddWithGetCarry bitwidth, Prod (Prod (Tbase _) (Tbase _)) (Tbase _), Prod (Tbase _) (Tbase _)
        => Some (AddWithGetCarry bitwidth _ _ _ _ _)
@@ -118,6 +124,7 @@ Definition denote_symbolic_op s d (opc : symbolic_op) : option (op s d)
      | SOpConst _, _, _
      | SIdWithAlt, _, _
      | SZselect, _, _
+     | SMulSplit _, _, _
      | SAddWithCarry, _, _
      | SAddWithGetCarry _, _, _
      | SSubWithBorrow, _, _
@@ -191,6 +198,7 @@ Definition normalize_symbolic_expr_mod_c (opc : symbolic_op) (args : symbolic_ex
      | SOpp
      | SIdWithAlt
      | SZselect
+     | SMulSplit _
      | SAddWithCarry
      | SAddWithGetCarry _
      | SSubWithBorrow
diff --git a/src/Compilers/Z/Reify.v b/src/Compilers/Z/Reify.v
index 66a10a882..b9dc6477b 100644
--- a/src/Compilers/Z/Reify.v
+++ b/src/Compilers/Z/Reify.v
@@ -34,6 +34,12 @@ Ltac base_reify_op op op_head extra ::=
                fail 100 "Error: In Reflection.Z.base_reify_op: can only reify" c "applied to" uZ "not" T
           | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is id_with_alt but body is wrong:" extra
           end
+     | @Z.mul_split_at_bitwidth
+       => lazymatch extra with
+          | @Z.mul_split_at_bitwidth ?bit_width _ _
+            => constr:(reify_op op op_head 3 (MulSplit bit_width TZ TZ TZ TZ))
+          | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is Z.mul_split_with_bitwidth but body is wrong:" extra
+          end
      | @Z.add_with_get_carry
        => lazymatch extra with
           | @Z.add_with_get_carry ?bit_width _ _ _
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v
index 53fb60c95..818fa1ad5 100644
--- a/src/Compilers/Z/Syntax.v
+++ b/src/Compilers/Z/Syntax.v
@@ -30,6 +30,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type :=
 | Opp T Tout : op (Tbase T) (Tbase Tout)
 | IdWithAlt T1 T2 Tout : op (Tbase T1 * Tbase T2) (Tbase Tout)
 | Zselect T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout)
+| MulSplit (bitwidth : Z) T1 T2 Tout1 Tout2 : op (Tbase T1 * Tbase T2) (Tbase Tout1 * Tbase Tout2)
 | AddWithCarry T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout)
 | AddWithGetCarry (bitwidth : Z) T1 T2 T3 Tout1 Tout2 : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout1 * Tbase Tout2)
 | SubWithBorrow T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout)
@@ -86,8 +87,9 @@ Definition Zinterp_op src dst (f : op src dst)
      | Land _ _ _ => fun xy => Z.land (fst xy) (snd xy)
      | Lor _ _ _ => fun xy => Z.lor (fst xy) (snd xy)
      | Opp _ _ => fun x => Z.opp x
-     | Zselect _ _ _ _ => fun ctf => let '(c, t, f) := eta3 ctf in Z.zselect c t f
      | IdWithAlt _ _ _ => fun xy => id_with_alt (fst xy) (snd xy)
+     | Zselect _ _ _ _ => fun ctf => let '(c, t, f) := eta3 ctf in Z.zselect c t f
+     | MulSplit bitwidth _ _ _ _ => fun xy => Z.mul_split_at_bitwidth bitwidth (fst xy) (snd xy)
      | AddWithCarry _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_carry c x y
      | AddWithGetCarry bitwidth _ _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_get_carry bitwidth c x y
      | SubWithBorrow _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.sub_with_borrow c x y
diff --git a/src/Compilers/Z/Syntax/Equality.v b/src/Compilers/Z/Syntax/Equality.v
index 900121456..caa209e52 100644
--- a/src/Compilers/Z/Syntax/Equality.v
+++ b/src/Compilers/Z/Syntax/Equality.v
@@ -45,6 +45,8 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
        => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq Tout Tout'
      | Zselect T1 T2 T3 Tout, Zselect T1' T2' T3' Tout'
        => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq T3 T3' && base_type_beq Tout Tout'
+     | MulSplit bitwidth T1 T2 Tout1 Tout2, MulSplit bitwidth' T1' T2' Tout1' Tout2'
+       => Z.eqb bitwidth bitwidth' && base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq Tout1 Tout1' && base_type_beq Tout2 Tout2'
      | AddWithCarry T1 T2 T3 Tout, AddWithCarry T1' T2' T3' Tout'
        => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq T3 T3' && base_type_beq Tout Tout'
      | AddWithGetCarry bitwidth T1 T2 T3 Tout1 Tout2, AddWithGetCarry bitwidth' T1' T2' T3' Tout1' Tout2'
@@ -62,12 +64,13 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
      | Land _ _ _, _
      | Lor _ _ _, _
      | Opp _ _, _
+     | IdWithAlt _ _ _, _
      | Zselect _ _ _ _, _
+     | MulSplit _ _ _ _ _, _
      | AddWithCarry _ _ _ _, _
      | AddWithGetCarry _ _ _ _ _ _, _
      | SubWithBorrow _ _ _ _, _
      | SubWithGetBorrow _ _ _ _ _ _, _
-     | IdWithAlt _ _ _, _
        => false
      end%bool.
 
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index 06b78ccd8..41b0e33be 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -80,6 +80,7 @@ Definition genericize_op {var' src dst} (opc : op src dst) {f}
      | Opp _ _ => fun _ _ => Opp _ _
      | IdWithAlt _ _ _ => fun _ _ => IdWithAlt _ _ _
      | Zselect _ _ _ _ => fun _ _ => Zselect _ _ _ _
+     | MulSplit bitwidth _ _ _ _ => fun _ _ => MulSplit bitwidth _ _ _ _
      | AddWithCarry _ _ _ _ => fun _ _ => AddWithCarry _ _ _ _
      | AddWithGetCarry bitwidth _ _ _ _ _ => fun _ _ => AddWithGetCarry bitwidth _ _ _ _ _
      | SubWithBorrow _ _ _ _ => fun _ _ => SubWithBorrow _ _ _ _