diff options
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifier.v | 2 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 7 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 28 | ||||
-rw-r--r-- | src/Compilers/Z/CommonSubexpressionElimination.v | 8 | ||||
-rw-r--r-- | src/Compilers/Z/Reify.v | 6 | ||||
-rw-r--r-- | src/Compilers/Z/Syntax.v | 4 | ||||
-rw-r--r-- | src/Compilers/Z/Syntax/Equality.v | 5 | ||||
-rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 1 |
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 _ _ _ _ |