diff options
| -rw-r--r-- | arm/Archi.v | 5 | ||||
| -rw-r--r-- | ia32/Archi.v | 5 | ||||
| -rw-r--r-- | lib/Floats.v | 91 | ||||
| -rw-r--r-- | powerpc/Archi.v | 5 |
4 files changed, 30 insertions, 76 deletions
diff --git a/arm/Archi.v b/arm/Archi.v index 00d9895..e4abf00 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -43,9 +43,12 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p (Pos.testbit (proj1_sig pl1) 22 && negb (Pos.testbit (proj1_sig pl2) 22))%bool. +Definition float_of_single_preserves_sNaN := false. + Global Opaque big_endian default_pl_64 choose_binop_pl_64 - default_pl_32 choose_binop_pl_32. + default_pl_32 choose_binop_pl_32 + float_of_single_preserves_sNaN. (** Which ABI to use: either the standard ARM EABI with floats passed in integer registers, or the "hardfloat" variant of the EABI diff --git a/ia32/Archi.v b/ia32/Archi.v index fff25cf..674b276 100644 --- a/ia32/Archi.v +++ b/ia32/Archi.v @@ -37,7 +37,10 @@ Program Definition default_pl_32 : bool * nan_pl 24 := Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := false. (**r always choose first NaN *) +Definition float_of_single_preserves_sNaN := false. + Global Opaque big_endian default_pl_64 choose_binop_pl_64 - default_pl_32 choose_binop_pl_32. + default_pl_32 choose_binop_pl_32 + float_of_single_preserves_sNaN. diff --git a/lib/Floats.v b/lib/Floats.v index bbc2a92..fbc78d9 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -146,9 +146,10 @@ Next Obligation. Qed. Lemma nan_payload_fequal: - forall prec p1 e1 p2 e2, p1 = p2 -> (exist _ p1 e1:nan_pl prec) = exist _ p2 e2. + forall prec (p1 p2: nan_pl prec), + proj1_sig p1 = proj1_sig p2 -> p1 = p2. Proof. - simpl; intros; subst. f_equal. apply Fcore_Zaux.eqbool_irrelevance. + intros. destruct p1, p2; simpl in H; subst. f_equal. apply Fcore_Zaux.eqbool_irrelevance. Qed. Lemma lor_idempotent: @@ -161,16 +162,14 @@ Qed. Lemma transform_quiet_pl_idempotent: forall pl, transform_quiet_pl (transform_quiet_pl pl) = transform_quiet_pl pl. Proof. - intros []; simpl; intros. apply nan_payload_fequal. - simpl. apply lor_idempotent. + intros. apply nan_payload_fequal; simpl. apply lor_idempotent. Qed. (** Nan payload operations for single <-> double conversions. *) -Definition of_single_pl (s:bool) (pl:nan_pl 24) : (bool * nan_pl 53). +Definition expand_pl (pl: nan_pl 24) : nan_pl 53. Proof. -Proof. - refine (s, transform_quiet_pl (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _)). + refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _). abstract ( destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_Pnat; fold (Fcore_digits.digits2_Pnat x); @@ -178,18 +177,26 @@ Proof. zify; omega). Defined. -Definition to_single_pl (s:bool) (pl:nan_pl 53) : (bool * nan_pl 24). -Proof. +Definition of_single_pl (s:bool) (pl:nan_pl 24) : (bool * nan_pl 53) := + (s, + if Archi.float_of_single_preserves_sNaN + then expand_pl pl + else transform_quiet_pl (expand_pl pl)). + +Definition reduce_pl (pl: nan_pl 53) : nan_pl 24. Proof. - refine (s, exist _ (Pos.shiftr_nat (proj1_sig (transform_quiet_pl pl)) 29) _). + refine (exist _ (Pos.shiftr_nat (proj1_sig pl) 29) _). abstract ( - destruct (transform_quiet_pl pl); unfold proj1_sig, Pos.shiftr_nat, nat_iter; + destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_iter; rewrite Z.ltb_lt in *; assert (forall x, Fcore_digits.digits2_Pnat (Pos.div2 x) = (Fcore_digits.digits2_Pnat x - 1)%nat) by (destruct x0; simpl; zify; omega); rewrite !H, <- !NPeano.Nat.sub_add_distr; zify; omega). Defined. +Definition to_single_pl (s:bool) (pl:nan_pl 53) : (bool * nan_pl 24) := + (s, reduce_pl (transform_quiet_pl pl)). + (** NaN payload operations for opposite and absolute value. *) Definition neg_pl (s:bool) (pl:nan_pl 53) := (negb s, pl). @@ -286,68 +293,6 @@ Ltac smart_omega := compute_this (Zpower_pos 2 1024); compute_this (Zpower_pos 2 53); compute_this (Zpower_pos 2 52); compute_this (Zpower_pos 2 32); zify; omega. -Lemma of_single_to_single_pl: - forall s pl, - prod_rect (fun _ => _) of_single_pl (prod_rect (fun _ => _) to_single_pl (of_single_pl s pl)) = of_single_pl s pl. -Proof. - destruct pl. unfold of_single_pl, to_single_pl. - unfold transform_quiet_pl, proj1_sig. simpl. - f_equal. apply nan_payload_fequal. - unfold Pos.shiftr_nat. simpl. - rewrite !lor_idempotent. reflexivity. -Qed. - -Lemma of_single_to_single_of_single: - forall f, of_single (to_single (of_single f)) = of_single f. -Proof. - intros. unfold of_single, to_single, b64_of_b32, b32_of_b64. - destruct (is_nan _ _ f) eqn:ISNAN. -- destruct f; try discriminate. - unfold Bconv. - rewrite <- of_single_to_single_pl at 2. - reflexivity. -- rewrite (Bconv_narrow_widen 24); auto; omega. -Qed. - -Lemma to_single_of_single_pl: - forall s pl, - prod_rect (fun _ => _) to_single_pl (prod_rect (fun _ => _) of_single_pl (to_single_pl s pl)) = to_single_pl s pl. -Proof. - destruct pl. unfold of_single_pl, to_single_pl. unfold prod_rect. - f_equal. apply nan_payload_fequal. - rewrite transform_quiet_pl_idempotent. - unfold transform_quiet_pl, proj1_sig. - change 51 with (29+22). - clear - x. revert x. unfold Pos.shiftr_nat, Pos.shiftl_nat. - induction (29)%nat. intro. simpl. apply lor_idempotent. - intro. - rewrite !nat_iter_succ_r with (f:=Pos.div2). - destruct x; simpl; try apply IHn. - clear IHn. induction n. reflexivity. - rewrite !nat_iter_succ_r with (f:=Pos.div2). auto. -Qed. - -Lemma to_single_of_single_to_single: - forall f, to_single (of_single (to_single f)) = to_single f. -Proof. - intros. unfold to_single, of_single, b32_of_b64, b64_of_b32. - destruct (is_nan _ _ f) eqn:ISNAN. -- destruct f; try discriminate. - unfold Bconv. - rewrite <- to_single_of_single_pl at 2. - reflexivity. -- rewrite (Bconv_narrow_widen 24); auto. omega. omega. - set (f' := Bconv 53 1024 24 128 __ __ to_single_pl mode_NE f). - destruct f; try discriminate; try reflexivity. - exploit (Bconv_correct 53 1024 24 128 __ __ to_single_pl mode_NE - (B754_finite 53 1024 b m e e0)). auto. - destruct Rlt_bool. - intros (A & B & C). apply is_finite_not_is_nan; auto. - fold f'. intros A. destruct f'; auto. - simpl in A. unfold binary_overflow in A. - destruct overflow_to_inf in A; destruct n; discriminate. -Qed. - (** Commutativity properties of addition and multiplication. *) Theorem add_commut: diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 070f7cc..058b057 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -37,6 +37,9 @@ Program Definition default_pl_32 : bool * nan_pl 24 := Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := false. (**r always choose first NaN *) +Definition float_of_single_preserves_sNaN := true. + Global Opaque big_endian default_pl_64 choose_binop_pl_64 - default_pl_32 choose_binop_pl_32. + default_pl_32 choose_binop_pl_32 + float_of_single_preserves_sNaN. |