Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 51 insertions, 0 deletions

diff --git a/flocq/Appli/Fappli_IEEE_bits.v b/flocq/Appli/Fappli_IEEE_bits.v
index a41fba9..937e8d4 100644
--- a/flocq/Appli/Fappli_IEEE_bits.v
+++ b/flocq/Appli/Fappli_IEEE_bits.v
@@ -248,6 +248,57 @@ discriminate.
 now apply Zlt_0_le_0_pred.
 Qed.
 
+Theorem bits_of_binary_float_range:
+  forall x, (0 <= bits_of_binary_float x < 2^(mw+ew+1))%Z.
+Proof.
+  intros. 
+Local Open Scope Z_scope.
+  assert (J: forall s m e,
+          0 <= m < 2^mw -> 0 <= e < 2^ew ->
+          0 <= join_bits s m e < 2^(mw+ew+1)).
+  {
+    intros. unfold join_bits. 
+    set (se := (if s then 2 ^ ew else 0) + e).
+    assert (0 <= se < 2^(ew+1)).
+    { rewrite (Zpower_plus radix2) by omega. change (radix2^1) with 2. simpl.
+      unfold se. destruct s; omega. }
+    assert (0 <= se * 2^mw <= (2^(ew+1) - 1) * 2^mw).
+    { split. apply Zmult_gt_0_le_0_compat; omega.
+      apply Zmult_le_compat_r; omega. }
+    rewrite Z.mul_sub_distr_r in H2.
+    replace (mw + ew + 1) with ((ew + 1) + mw) by omega. 
+    rewrite (Zpower_plus radix2) by omega. simpl. omega.
+  }
+  assert (D: forall p n, Z.of_nat (S (digits2_Pnat p)) <= n ->
+             0 <= Z.pos p < 2^n).
+  {
+    intros.  
+    generalize (digits2_Pnat_correct p). simpl. rewrite ! Zpower_nat_Z. intros [A B].
+    split. zify; omega. eapply Zlt_le_trans. eassumption. 
+    apply (Zpower_le radix2); auto.
+  } 
+  destruct x; unfold bits_of_binary_float.
+- apply J; omega.
+- apply J; omega. 
+- destruct n as [pl pl_range]. apply Z.ltb_lt in pl_range.
+  apply J. apply D. unfold prec, Z_of_nat' in pl_range; omega. omega.
+- unfold bounded in e0. apply Bool.andb_true_iff in e0; destruct e0 as [A B].
+  apply Z.leb_le in B.
+  unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A. 
+  assert (G: Z.of_nat (S (digits2_Pnat m)) <= prec) by (zify; omega).
+  assert (M: emin <= e) by (unfold emin; zify; omega). 
+  generalize (Zle_bool_spec (2^mw) (Z.pos m)); intro SPEC; inversion SPEC.
+  + apply J. 
+    * split. omega. generalize (D _ _ G). unfold prec. 
+      rewrite (Zpower_plus radix2) by omega.
+      change (radix2^1) with 2. simpl radix_val. omega.
+    * split. omega. unfold emin. replace (2^ew) with (2 * emax). omega.
+      symmetry. replace ew with (1 + (ew - 1)) by omega. 
+      apply (Zpower_plus radix2); omega.
+  + apply J. zify; omega. omega. 
+Local Close Scope Z_scope.
+Qed.
+
 Definition binary_float_of_bits_aux x :=
   let '(sx, mx, ex) := split_bits x in
   if Zeq_bool ex 0 then