Revised specification of NaN payload behavior

When an FP arithmetic instruction produces a NaN result, the payload
of this NaN depends on the architecture.

Before, the payload behavior was specified by 3 architecture-dependent
parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32`
and `Archi.fpu_results_default_qNaN`.  This was adequate for
two-argument operations, but doesn't extend to FMA.

In preparation for FMA support, this commit generalizes the `Archi.choose`
functions from two arguments to any number of arguments.  In passing,
`Archi.fpu_results_default_qNaN` is no longer needed.

6 files changed, 209 insertions, 193 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index 39a424ec..e78ff6ce 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -16,7 +16,7 @@
 
 (** Architecture-dependent parameters for ARM *)
 
-Require Import ZArith.
+Require Import ZArith List.
 (*From Flocq*)
 Require Import Binary Bits.
 
@@ -34,30 +34,52 @@ Proof.
   unfold splitlong, ptr64; congruence.
 Qed.
 
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (false, iter_nat 22 _ xO xH).
+
+(** Choose the first signaling NaN, if any;
+    otherwise choose the first NaN;
+    otherwise use default. *)
+
+Definition choose_nan (is_signaling: positive -> bool) 
+                      (default: bool * positive)
+                      (l0: list (bool * positive)) : bool * positive :=
+  let fix choose_snan (l1: list (bool * positive)) :=
+    match l1 with
+    | nil =>
+        match l0 with nil => default | n :: _ => n end
+    | ((s, p) as n) :: l1 =>
+        if is_signaling p then n else choose_snan l1
+    end
+  in choose_snan l0.
+
+Lemma choose_nan_idem: forall is_signaling default n,
+  choose_nan is_signaling default (n :: n :: nil) =
+  choose_nan is_signaling default (n :: nil).
+Proof.
+  intros. destruct n as [s p]; unfold choose_nan; simpl.
+  destruct (is_signaling p); auto. 
+Qed.
 
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
-  (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
-      In all other cases, choose first NaN *)
-  (Pos.testbit pl1 51 && negb (Pos.testbit pl2 51))%bool.
+Definition choose_nan_64 :=
+  choose_nan (fun p => negb (Pos.testbit p 51)) default_nan_64.
 
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_32 :=
+  choose_nan (fun p => negb (Pos.testbit p 22)) default_nan_32.
 
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
-  (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
-      In all other cases, choose first NaN *)
-  (Pos.testbit pl1 22 && negb (Pos.testbit pl2 22))%bool.
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. intros; apply choose_nan_idem. Qed.
 
-Definition fpu_returns_default_qNaN := false.
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. intros; apply choose_nan_idem. Qed.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_nan_64 choose_binop_pl_64
-              default_nan_32 choose_binop_pl_32
-              fpu_returns_default_qNaN
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
               float_of_single_preserves_sNaN.
 
 (** Which ABI to use: either the standard ARM EABI with floats passed
diff --git a/lib/Floats.v b/lib/Floats.v
index 8b118c8d..98ccc173 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -94,17 +94,49 @@ Proof.
   destruct x as [[]|]; simpl; intros; discriminate.
 Qed.
 
-(** Relation between number of bits and base-2 logarithm *)
+(** Normalization of NaN payloads *)
 
-Lemma digits2_log2:
-  forall p, Z.pos (Digits.digits2_pos p) = Z.succ (Z.log2 (Z.pos p)).
+Lemma normalized_nan: forall prec n p,
+  Z.of_nat n = prec - 1 -> 1 < prec ->
+  nan_pl prec (Z.to_pos (P_mod_two_p p n)) = true.
 Proof.
-  assert (E: forall p, Digits.digits2_pos p = Pos.size p).
-  { induction p; simpl; rewrite ?IHp; auto. }
-  intros p. rewrite E.
-  destruct p; simpl; rewrite ?Pos.add_1_r; reflexivity.
+  intros. unfold nan_pl. apply Z.ltb_lt. rewrite Digits.Zpos_digits2_pos.
+  set (p' := P_mod_two_p p n).
+  assert (A: 0 <= p' < 2 ^ Z.of_nat n).
+  { rewrite <- two_power_nat_equiv; apply P_mod_two_p_range. }
+  assert (B: Digits.Zdigits radix2 p' <= prec - 1).
+  { apply Digits.Zdigits_le_Zpower. rewrite <- H. rewrite Z.abs_eq; tauto. }
+  destruct (zeq p' 0).
+- rewrite e. simpl; auto.
+- rewrite Z2Pos.id by omega. omega.
 Qed.
 
+(** Transform a Nan payload to a quiet Nan payload. *)
+
+Definition quiet_nan_64_payload (p: positive) :=
+  Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 51 1%positive))) 52%nat).
+
+Lemma quiet_nan_64_proof: forall p, nan_pl 53 (quiet_nan_64_payload p) = true.
+Proof. intros; apply normalized_nan; auto; omega. Qed.
+
+Definition quiet_nan_64 (sp: bool * positive) : {x :float | is_nan _ _ x = true} :=
+  let (s, p) := sp in
+  exist _ (B754_nan 53 1024 s (quiet_nan_64_payload p) (quiet_nan_64_proof p)) (eq_refl true).
+
+Definition default_nan_64 := quiet_nan_64 Archi.default_nan_64.
+
+Definition quiet_nan_32_payload (p: positive) :=
+  Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 22 1%positive))) 23%nat).
+
+Lemma quiet_nan_32_proof: forall p, nan_pl 24 (quiet_nan_32_payload p) = true.
+Proof. intros; apply normalized_nan; auto; omega. Qed.
+
+Definition quiet_nan_32 (sp: bool * positive) : {x :float32 | is_nan _ _ x = true} :=
+  let (s, p) := sp in
+  exist _ (B754_nan 24 128 s (quiet_nan_32_payload p) (quiet_nan_32_proof p)) (eq_refl true).
+
+Definition default_nan_32 := quiet_nan_32 Archi.default_nan_32.
+
 Local Notation __ := (eq_refl Datatypes.Lt).
 
 Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt).
@@ -119,29 +151,15 @@ Module Float.
 (** The following definitions are not part of the IEEE754 standard but
     apply to all architectures supported by CompCert. *)
 
-(** Transform a Nan payload to a quiet Nan payload. *)
-
-Lemma transform_quiet_nan_proof (p : positive) :
-  nan_pl 53 p = true ->
-  nan_pl 53 (Pos.lor p (iter_nat xO 51 1%positive)) = true.
-Proof.
-  unfold nan_pl. intros K.
-  simpl. rewrite Z.ltb_lt, digits2_log2 in *.
-  change (Z.pos (Pos.lor p 2251799813685248)) with (Z.lor (Z.pos p) 2251799813685248%Z).
-  rewrite Z.log2_lor by xomega.
-  now apply Z.max_case.
-Qed.
-
-Definition transform_quiet_nan s p H : {x :float | is_nan _ _ x = true} :=
-  exist _ (B754_nan 53 1024 s _ (transform_quiet_nan_proof p H)) (eq_refl true).
-
 (** Nan payload operations for single <-> double conversions. *)
 
+Definition expand_nan_payload (p: positive) := Pos.shiftl_nat p 29.
+
 Lemma expand_nan_proof (p : positive) :
   nan_pl 24 p = true ->
-  nan_pl 53 (Pos.shiftl_nat p 29) = true.
+  nan_pl 53 (expand_nan_payload p) = true.
 Proof.
-  unfold nan_pl. intros K.
+  unfold nan_pl, expand_nan_payload. intros K.
   rewrite Z.ltb_lt in *.
   unfold Pos.shiftl_nat, nat_rect, Digits.digits2_pos.
   fold (Digits.digits2_pos p).
@@ -149,38 +167,28 @@ Proof.
 Qed.
 
 Definition expand_nan s p H : {x | is_nan 53 1024 x = true} :=
-  exist _ (B754_nan 53 1024 s _ (expand_nan_proof p H)) (eq_refl true).
+  exist _ (B754_nan 53 1024 s (expand_nan_payload p) (expand_nan_proof p H)) (eq_refl true).
 
 Definition of_single_nan (f : float32) : { x : float | is_nan _ _ x = true } :=
   match f with
   | B754_nan s p H =>
     if Archi.float_of_single_preserves_sNaN
     then expand_nan s p H
-    else transform_quiet_nan s _ (expand_nan_proof p H)
-  | _ => Archi.default_nan_64
+    else quiet_nan_64 (s, expand_nan_payload p)
+  | _ => default_nan_64
   end.
 
-Lemma reduce_nan_proof (p : positive) :
-  nan_pl 53 p = true ->
-  nan_pl 24 (Pos.shiftr_nat p 29) = true.
-Proof.
-  unfold nan_pl. intros K.
-  rewrite Z.ltb_lt in *.
-  unfold Pos.shiftr_nat, nat_rect.
-  assert (H : forall x, Digits.digits2_pos (Pos.div2 x) = (Digits.digits2_pos x - 1)%positive)
-    by (destruct x; simpl; auto; rewrite Pplus_one_succ_r, Pos.add_sub; auto).
-  rewrite !H, !Pos2Z.inj_sub_max.
-  repeat (apply Z.max_lub_lt; [reflexivity |apply Z.lt_sub_lt_add_l]).
-  exact K.
-Qed.
-
-Definition reduce_nan s p H : {x : float32 | is_nan _ _ x = true} :=
-  exist _ (B754_nan 24 128 s _ (reduce_nan_proof p H)) (eq_refl true).
+Definition reduce_nan_payload (p: positive) :=
+  (* The [quiet_nan_64_payload p] before the right shift is redundant with
+     the [quiet_nan_32_payload p] performed after, in [to_single_nan].
+     However the former ensures that the result of the right shift is
+     not 0 and therefore representable as a positive. *)
+  Pos.shiftr_nat (quiet_nan_64_payload p) 29.
 
 Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } :=
   match f with
-  | B754_nan s p H => reduce_nan s _ (transform_quiet_nan_proof p H)
-  | _ => Archi.default_nan_32
+  | B754_nan s p H => quiet_nan_32 (s, reduce_nan_payload p)
+  | _ => default_nan_32
   end.
 
 (** NaN payload operations for opposite and absolute value. *)
@@ -188,34 +196,37 @@ Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } :=
 Definition neg_nan (f : float) : { x : float | is_nan _ _ x = true } :=
   match f with
   | B754_nan s p H => exist _ (B754_nan 53 1024 (negb s) p H) (eq_refl true)
-  | _ => Archi.default_nan_64
+  | _ => default_nan_64
   end.
 
 Definition abs_nan (f : float) : { x : float | is_nan _ _ x = true } :=
   match f with
   | B754_nan s p H => exist _ (B754_nan 53 1024 false p H) (eq_refl true)
-  | _ => Archi.default_nan_64
+  | _ => default_nan_64
   end.
 
-(** The NaN payload operations for two-argument arithmetic operations
-   are not part of the IEEE754 standard, but all architectures of
-   Compcert share a similar NaN behavior, parameterized by:
-- a "default" payload which occurs when an operation generates a NaN from
-  non-NaN arguments;
-- a choice function determining which of the payload arguments to choose,
-  when an operation is given two NaN arguments. *)
-
-Definition binop_nan (x y : float) : {x : float | is_nan 53 1024 x = true} :=
-  if Archi.fpu_returns_default_qNaN then Archi.default_nan_64 else
-  match x, y with
-  | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 =>
-      if Archi.choose_binop_pl_64 pl1 pl2
-      then transform_quiet_nan s2 pl2 H2
-      else transform_quiet_nan s1 pl1 H1
-  | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1
-  | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2
-  | _, _ => Archi.default_nan_64
-  end.
+(** When an arithmetic operation returns a NaN, the sign and payload
+  of this NaN are not fully specified by the IEEE standard, and vary
+  among the architectures supported by CompCert.  However, the following
+  behavior applies to all the supported architectures: the payload is either
+- a default payload, independent of the arguments, or
+- the payload of one of the NaN arguments, if any.
+
+For each supported architecture, the functions [Archi.choose_nan_64]
+and [Archi.choose_nan_32] determine the payload of the result as a
+function of the payloads of the NaN arguments.
+
+Additionally, signaling NaNs are converted to quiet NaNs, as required by the standard.
+*)
+
+Definition cons_pl (x: float) (l: list (bool * positive)) :=
+  match x with B754_nan s p _ => (s, p) :: l | _ => l end.
+
+Definition unop_nan (x: float) : {x : float | is_nan 53 1024 x = true} :=
+  quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])).
+
+Definition binop_nan (x y: float) : {x : float | is_nan 53 1024 x = true} :=
+  quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))).
 
 (** ** Operations over double-precision floats *)
 
@@ -302,19 +313,15 @@ Ltac smart_omega :=
 Theorem add_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x.
 Proof.
-  intros. apply Bplus_commut. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x, y; try reflexivity.
-  now destruct H.
+  intros. apply Bplus_commut.
+  destruct x, y; try reflexivity; now destruct H.
 Qed.
 
 Theorem mul_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x.
 Proof.
-  intros. apply Bmult_commut. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x, y; try reflexivity.
-  now destruct H.
+  intros. apply Bmult_commut.
+  destruct x, y; try reflexivity; now destruct H.
 Qed.
 
 (** Multiplication by 2 is diagonal addition. *)
@@ -324,9 +331,8 @@ Theorem mul2_add:
 Proof.
   intros. apply Bmult2_Bplus.
   intros x y Hx Hy. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x as [| |sx px Nx|]; try discriminate.
-  now destruct y, Archi.choose_binop_pl_64.
+  destruct x; try discriminate. simpl. rewrite Archi.choose_nan_64_idem. 
+  destruct y; reflexivity || discriminate.
 Qed.
 
 (** Divisions that can be turned into multiplication by an inverse. *)
@@ -338,9 +344,8 @@ Theorem div_mul_inverse:
 Proof.
   intros. apply Bdiv_mult_inverse. 2: easy.
   intros x0 y0 z0 Hx Hy Hz. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x0 as [| |sx px Nx|]; try discriminate.
-  now destruct y0, z0.
+  destruct x0; try discriminate.
+  destruct y0, z0; reflexivity || discriminate.
 Qed.
 
 (** Properties of comparisons. *)
@@ -919,45 +924,26 @@ End Float.
 
 Module Float32.
 
-(** ** NaN payload manipulations *)
-
-Lemma transform_quiet_nan_proof (p : positive) :
-  nan_pl 24 p = true ->
-  nan_pl 24 (Pos.lor p (iter_nat xO 22 1%positive)) = true.
-Proof.
-  unfold nan_pl. intros K.
-  simpl. rewrite Z.ltb_lt, digits2_log2 in *.
-  change (Z.pos (Pos.lor p 4194304)) with (Z.lor (Z.pos p) 4194304%Z).
-  rewrite Z.log2_lor by xomega.
-  now apply Z.max_case.
-Qed.
-
-Definition transform_quiet_nan s p H : {x : float32 | is_nan _ _ x = true} :=
-  exist _ (B754_nan 24 128 s _ (transform_quiet_nan_proof p H)) (eq_refl true).
-
 Definition neg_nan (f : float32) : { x : float32 | is_nan _ _ x = true } :=
   match f with
   | B754_nan s p H => exist _ (B754_nan 24 128 (negb s) p H) (eq_refl true)
-  | _ => Archi.default_nan_32
+  | _ => default_nan_32
   end.
 
 Definition abs_nan (f : float32) : { x : float32 | is_nan _ _ x = true } :=
   match f with
   | B754_nan s p H => exist _ (B754_nan 24 128 false p H) (eq_refl true)
-  | _ => Archi.default_nan_32
+  | _ => default_nan_32
   end.
 
-Definition binop_nan (x y : float32) : {x : float32 | is_nan _ _ x = true} :=
-  if Archi.fpu_returns_default_qNaN then Archi.default_nan_32 else
-  match x, y with
-  | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 =>
-      if Archi.choose_binop_pl_32 pl1 pl2
-      then transform_quiet_nan s2 pl2 H2
-      else transform_quiet_nan s1 pl1 H1
-  | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1
-  | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2
-  | _, _ => Archi.default_nan_32
-  end.
+Definition cons_pl (x: float32) (l: list (bool * positive)) :=
+  match x with B754_nan s p _ => (s, p) :: l | _ => l end.
+
+Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} :=
+  quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])).
+
+Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} :=
+  quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))).
 
 (** ** Operations over single-precision floats *)
 
@@ -1024,19 +1010,15 @@ Definition of_bits (b: int): float32 := b32_of_bits (Int.unsigned b).
 Theorem add_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x.
 Proof.
-  intros. apply Bplus_commut. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x, y; try reflexivity.
-  now destruct H.
+  intros. apply Bplus_commut. 
+  destruct x, y; try reflexivity; now destruct H.
 Qed.
 
 Theorem mul_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x.
 Proof.
-  intros. apply Bmult_commut. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x, y; try reflexivity.
-  now destruct H.
+  intros. apply Bmult_commut.
+  destruct x, y; try reflexivity; now destruct H.
 Qed.
 
 (** Multiplication by 2 is diagonal addition. *)
@@ -1046,9 +1028,8 @@ Theorem mul2_add:
 Proof.
   intros. apply Bmult2_Bplus.
   intros x y Hx Hy. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x as [| |sx px Nx|]; try discriminate.
-  now destruct y, Archi.choose_binop_pl_32.
+  destruct x; try discriminate. simpl. rewrite Archi.choose_nan_32_idem. 
+  destruct y; reflexivity || discriminate.
 Qed.
 
 (** Divisions that can be turned into multiplication by an inverse. *)
@@ -1060,9 +1041,8 @@ Theorem div_mul_inverse:
 Proof.
   intros. apply Bdiv_mult_inverse. 2: easy.
   intros x0 y0 z0 Hx Hy Hz. unfold binop_nan.
-  destruct Archi.fpu_returns_default_qNaN. easy.
-  destruct x0 as [| |sx px Nx|]; try discriminate.
-  now destruct y0, z0.
+  destruct x0; try discriminate.
+  destruct y0, z0; reflexivity || discriminate.
 Qed.
 
 (** Properties of comparisons. *)
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index d792e4fe..b99e4812 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -16,7 +16,7 @@
 
 (** Architecture-dependent parameters for PowerPC *)
 
-Require Import ZArith.
+Require Import ZArith List.
 (*From Flocq*)
 Require Import Binary Bits.
 
@@ -37,24 +37,28 @@ Proof.
   reflexivity.
 Qed.
 
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (false, iter_nat 22 _ xO xH).
 
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
-  false.                        (**r always choose first NaN *)
+(* Always choose the first NaN argument, if any *)
 
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_64 | n :: _ => n end.
 
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
-  false.                        (**r always choose first NaN *)
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_32 | n :: _ => n end.
 
-Definition fpu_returns_default_qNaN := false.
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
+
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
 
 Definition float_of_single_preserves_sNaN := true.
 
 Global Opaque ptr64 big_endian splitlong
-              default_nan_64 choose_binop_pl_64
-              default_nan_32 choose_binop_pl_32
-              fpu_returns_default_qNaN
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
               float_of_single_preserves_sNaN.
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 3758d686..e4078132 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -16,7 +16,7 @@
 
 (** Architecture-dependent parameters for RISC-V *)
 
-Require Import ZArith.
+Require Import ZArith List.
 (*From Flocq*)
 Require Import Binary Bits.
 
@@ -40,26 +40,28 @@ Qed.
    except the MSB, a.k.a. the quiet bit."
    Exceptions are operations manipulating signs. *)
 
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (false, iter_nat 22 _ xO xH).
 
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
-  false.                        (**r irrelevant *)
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+  default_nan_64.
 
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+  default_nan_32.
 
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
-  false.                        (**r irrelevant *)
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
 
-Definition fpu_returns_default_qNaN := true.
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_nan_64 choose_binop_pl_64
-              default_nan_32 choose_binop_pl_32
-              fpu_returns_default_qNaN
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
               float_of_single_preserves_sNaN.
 
 (** Whether to generate position-independent code or not *)
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index f10570e2..c6d66e09 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -16,7 +16,7 @@
 
 (** Architecture-dependent parameters for x86 in 32-bit mode *)
 
-Require Import ZArith.
+Require Import ZArith List.
 (*From Flocq*)
 Require Import Binary Bits.
 
@@ -34,24 +34,28 @@ Proof.
   unfold splitlong. destruct ptr64; simpl; congruence.
 Qed.
 
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 53 1024 true (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (true, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (true, iter_nat 22 _ xO xH).
 
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
-  false.                        (**r always choose first NaN *)
+(* Always choose the first NaN argument, if any *)
 
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_64 | n :: _ => n end.
 
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
-  false.                        (**r always choose first NaN *)
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_32 | n :: _ => n end.
 
-Definition fpu_returns_default_qNaN := false.
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
+
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_nan_64 choose_binop_pl_64
-              default_nan_32 choose_binop_pl_32
-              fpu_returns_default_qNaN
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
               float_of_single_preserves_sNaN.
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index 01eb36dd..8523fdce 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -16,7 +16,7 @@
 
 (** Architecture-dependent parameters for x86 in 64-bit mode *)
 
-Require Import ZArith.
+Require Import ZArith List.
 (*From Flocq*)
 Require Import Binary Bits.
 
@@ -34,24 +34,28 @@ Proof.
   unfold splitlong. destruct ptr64; simpl; congruence.
 Qed.
 
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 53 1024 true (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (true, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (true, iter_nat 22 _ xO xH).
 
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
-  false.                        (**r always choose first NaN *)
+(* Always choose the first NaN argument, if any *)
 
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
-  exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_64 | n :: _ => n end.
 
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
-  false.                        (**r always choose first NaN *)
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_32 | n :: _ => n end.
 
-Definition fpu_returns_default_qNaN := false.
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
+
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_nan_64 choose_binop_pl_64
-              default_nan_32 choose_binop_pl_32
-              fpu_returns_default_qNaN
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
               float_of_single_preserves_sNaN.