Merge pull request #235 from SkyLabsAI/paolo/extend-float-theory

Extend float theory

Author: pgiarrusso-sl

rocq-skylabs-brick/tests/float_simple_pred_support.v

@@ -36,7 +36,7 @@ Section pure_encoding_tests.
     rewrite /pure_encodes /=.
     split; [reflexivity|].
     split.
-    - replace (float_value.to_bits float_type.Ffloat16 f16_one) with f16_one_bits.
+    - replace (float_value.to_bits f16_one) with f16_one_bits.
       + rewrite /in_Z_to_bytes_bounds /f16_one_bits /=.
         change (0 <= 15360 /\ 15360 < 65536)%Z. lia.
       + symmetry. apply float_value.to_of_bits. change (0 <= 15360 < 65536)%Z. lia.
@@ -50,7 +50,7 @@ Section pure_encoding_tests.
     rewrite /pure_encodes /=.
     split; [reflexivity|].
     split.
-    - replace (float_value.to_bits float_type.Ffloat f32_one) with f32_one_bits.
+    - replace (float_value.to_bits f32_one) with f32_one_bits.
       + rewrite /in_Z_to_bytes_bounds /f32_one_bits /=.
         change (0 <= 1065353216 /\ 1065353216 < 4294967296)%Z. lia.
       + symmetry. apply float_value.to_of_bits.
@@ -65,7 +65,7 @@ Section pure_encoding_tests.
     rewrite /pure_encodes /=.
     split; [reflexivity|].
     split.
-    - replace (float_value.to_bits float_type.Ffloat128 f128_one) with f128_one_bits.
+    - replace (float_value.to_bits f128_one) with f128_one_bits.
       + rewrite /in_Z_to_bytes_bounds /f128_one_bits /=.
         change (0 <= 85065399433376081038215121361612832768 /\
                 85065399433376081038215121361612832768 <

rocq-skylabs-brick/tests/float_support.v

@@ -268,17 +268,17 @@ Qed.
 
 Example float_to_of_bits_roundtrips bits :
   (0 <= bits < 2 ^ float_type.bit_width float_type.Ffloat)%Z ->
-  float_value.to_bits float_type.Ffloat
+  float_value.to_bits
     (float_value.of_bits float_type.Ffloat bits) = bits.
 Proof. apply float_value.to_of_bits. Qed.
 
-Example double_of_to_bits_roundtrip f :
+Example double_of_to_bits_roundtrip (f : float_type.car float_type.Fdouble) :
   float_value.of_bits float_type.Fdouble
-    (float_value.to_bits float_type.Fdouble f) = f.
+    (float_value.to_bits f) = f.
 Proof. apply float_value.of_to_bits. Qed.
 
 Example float128_nan_payload_bits_preserved :
-  float_value.to_bits float_type.Ffloat128 f128_nan_payload = f128_nan_payload_bits.
+  float_value.to_bits f128_nan_payload = f128_nan_payload_bits.
 Proof.
   apply float_value.to_of_bits.
   change (0 <= 170138587312039964317873038467719495681 <
@@ -356,16 +356,16 @@ Proof.
 Qed.
 
 Example float_nan_compare_unordered :
-  float_value.value_compare float_type.Ffloat f32_nan f32_nan = None.
+  float_value.value_compare f32_nan f32_nan = None.
 Proof. vm_compute; reflexivity. Qed.
 
 Example double_nan_compare_unordered :
-  float_value.value_compare float_type.Fdouble f64_nan f64_nan = None.
+  float_value.value_compare f64_nan f64_nan = None.
 Proof. vm_compute; reflexivity. Qed.
 
 Example float_nan_payload_add_preserved :
-  float_value.to_bits float_type.Ffloat
-    (float_value.add float_type.Ffloat f32_nan_payload f32_one) =
+  float_value.to_bits
+    (float_value.add f32_nan_payload f32_one) =
   f32_nan_payload_bits.
 Proof. vm_compute; reflexivity. Qed.
 
@@ -383,22 +383,22 @@ Proof. vm_compute; reflexivity. Qed.
 
 Example raw_float16_intro {σ : genv} :
   raw_bytes_of_val σ Tfloat16 (Vfloat float_type.Ffloat16 f16_one)
-    (float_raw_bytes σ float_type.Ffloat16 f16_one).
+    (float_raw_bytes σ f16_one).
 Proof. apply raw_bytes_of_val_float_intro. Qed.
 
 Example raw_float_intro {σ : genv} :
   raw_bytes_of_val σ Tfloat (Vfloat float_type.Ffloat f32_one)
-    (float_raw_bytes σ float_type.Ffloat f32_one).
+    (float_raw_bytes σ f32_one).
 Proof. apply raw_bytes_of_val_float_intro. Qed.
 
 Example raw_double_intro {σ : genv} :
   raw_bytes_of_val σ Tdouble (Vfloat float_type.Fdouble f64_one)
-    (float_raw_bytes σ float_type.Fdouble f64_one).
+    (float_raw_bytes σ f64_one).
 Proof. apply raw_bytes_of_val_float_intro. Qed.
 
 Example raw_float128_intro {σ : genv} :
   raw_bytes_of_val σ Tfloat128 (Vfloat float_type.Ffloat128 f128_one)
-    (float_raw_bytes σ float_type.Ffloat128 f128_one).
+    (float_raw_bytes σ f128_one).
 Proof. apply raw_bytes_of_val_float_intro. Qed.
 
 Example float16_bits_compatible :
@@ -422,7 +422,7 @@ Example longdouble_raw_bits_not_binary128_compatible :
 Proof. intros [_ Hwidth]. vm_compute in Hwidth. discriminate. Qed.
 
 Example float_to_bits_has_unsigned_type {σ : genv} :
-  has_type_prop (Vint (float_value.to_bits float_type.Ffloat f32_one))
+  has_type_prop (Vint (float_value.to_bits f32_one))
     (Tnum int_rank.Iint Unsigned).
 Proof.
   apply float_to_bits_has_type_unsigned.

rocq-skylabs-brick/theories/lang/cpp/logic/raw.v

@@ -66,12 +66,12 @@ Axiom raw_byte_of_int_eq : ∀ {σ : genv} sz x rs,
   ∃ l, decodes_uint l x /\ raw_int_byte <$> l = rs /\ length l = N.to_nat (int_rank.bytesN sz).
 
 Lemma raw_bytes_of_val_float_intro {σ : genv} ft (f : float_type.car ft) :
-  raw_bytes_of_val σ (Tfloat_ ft) (Vfloat ft f) (float_raw_bytes σ ft f).
+  raw_bytes_of_val σ (Tfloat_ ft) (Vfloat ft f) (float_raw_bytes σ f).
 Proof. apply raw_bytes_of_val_float. reflexivity. Qed.
 
 Lemma raw_bytes_of_val_float_elim {σ : genv} ft (f : float_type.car ft) rs :
   raw_bytes_of_val σ (Tfloat_ ft) (Vfloat ft f) rs ->
-  rs = float_raw_bytes σ ft f.
+  rs = float_raw_bytes σ f.
 Proof. apply raw_bytes_of_val_float. Qed.
 
 Definition float_bits_compatible (sz : int_rank.t) (ft : float_type.t) : Prop :=
@@ -87,7 +87,7 @@ Qed.
 
 Lemma float_to_bits_has_type_unsigned {σ : genv} sz ft (f : float_type.car ft) :
   float_bits_compatible sz ft ->
-  has_type_prop (Vint (float_value.to_bits ft f)) (Tnum sz Unsigned).
+  has_type_prop (Vint (float_value.to_bits f)) (Tnum sz Unsigned).
 Proof.
   intros [Hbits Hwidth].
   rewrite -has_int_type.

rocq-skylabs-brick/theories/lang/cpp/model/simple_pred.v

@@ -430,8 +430,8 @@ Module SimpleCPP.
           match v with
           | Vfloat ft' f =>
               ft = ft' /\
-              in_Z_to_bytes_bounds (float_type.bitsize ft') Unsigned (float_value.to_bits ft' f) /\
-              vs = Z_to_bytes (float_type.bitsize ft') Unsigned (float_value.to_bits ft' f)
+              in_Z_to_bytes_bounds (float_type.bitsize ft') Unsigned (float_value.to_bits f) /\
+              vs = Z_to_bytes (float_type.bitsize ft') Unsigned (float_value.to_bits f)
           | Vundef => pure_encodes_undef (float_type.bitsize ft) vs
           | _ => False
           end

rocq-skylabs-brick/theories/lang/cpp/semantics/cast.v

@@ -296,7 +296,7 @@ Definition conv_float {σ : genv} (tu : translation_unit) (from to : type) (v v'
   | Tfloat_ _ , Tnum _ _ =>
       match v with
       | Vfloat f z =>
-          match float_value.to_int f z with
+          match float_value.to_int z with
           | Some n => v' = Vint n /\ has_type_prop (Vint n) to
           | None => False
           end
@@ -432,7 +432,7 @@ Section conv_float.
 
   Lemma conv_float_to_int ty sz sgn ft (fv : float_type.car ft) z :
       representation_type tu ty = Tnum sz sgn ->
-      float_value.to_int ft fv = Some z ->
+      float_value.to_int fv = Some z ->
       has_type_prop (Vint z) ty ->
       conv_float tu (Tfloat_ ft) ty (Vfloat ft fv) (Vint z).
   Proof using Hmod.
@@ -459,7 +459,7 @@ Section conv_float.
 
   Lemma conv_float_to_enum nm sz sgn ft (fv : float_type.car ft) z :
       representation_type tu (Tenum nm) = Tnum sz sgn ->
-      float_value.to_int ft fv = Some z ->
+      float_value.to_int fv = Some z ->
       has_type_prop (Vint z) (Tenum nm) ->
       conv_float tu (Tfloat_ ft) (Tenum nm) (Vfloat ft fv) (Vint z).
   Proof using Hmod.

rocq-skylabs-brick/theories/lang/cpp/semantics/characters.v

@@ -70,7 +70,7 @@ Definition Z_to_char_bits (ct : char_type.t) (z : Z) : N :=
 
 Definition float_to_char (σ : genv) (ft : float_type.t) (ct : char_type.t)
     (f : float_type.car ft) : option N :=
-  match float_value.to_int ft f with
+  match float_value.to_int f with
   | Some z => if char_float_boundb σ ct z then Some (Z_to_char_bits ct z) else None
   | None => None
   end.
@@ -450,7 +450,7 @@ Lemma float_to_char_has_type {σ : genv} ft ct (f : float_type.car ft) n :
   has_type_prop (Vchar n) (Tchar_ ct).
 Proof.
   rewrite /float_to_char.
-  destruct (float_value.to_int ft f) as [z|] eqn:HtoZ; try discriminate.
+  destruct (float_value.to_int f) as [z|] eqn:HtoZ; try discriminate.
   destruct (char_float_boundb σ ct z) eqn:Hbound; inversion 1; subst.
   apply has_type_prop_char'.
   apply Z_to_char_bits_bounded.

rocq-skylabs-brick/theories/lang/cpp/semantics/operator.v

@@ -151,7 +151,7 @@ Axiom eval_minus_int : forall ty a c,
     eval_unop Uminus ty ty (Vint a) (Vint c).
 Axiom eval_minus_float : forall f a,
     eval_unop Uminus (Tfloat_ f) (Tfloat_ f)
-      (Vfloat f a) (Vfloat f (float_value.opp f a)).
+      (Vfloat f a) (Vfloat f (float_value.opp a)).
 
 (** * Binary Operators *)
 
@@ -194,10 +194,10 @@ Let eval_float_op (bo : BinOp)
     eval_binop_pure bo (Tfloat_ f) (Tfloat_ f) (Tfloat_ f)
       (Vfloat f a) (Vfloat f b) (Vfloat f c).
 
-Axiom eval_float_add : Hnf (eval_float_op Badd float_value.add).
-Axiom eval_float_sub : Hnf (eval_float_op Bsub float_value.sub).
-Axiom eval_float_mul : Hnf (eval_float_op Bmul float_value.mul).
-Axiom eval_float_div : Hnf (eval_float_op Bdiv float_value.div).
+Axiom eval_float_add : Hnf (eval_float_op Badd (@float_value.add)).
+Axiom eval_float_sub : Hnf (eval_float_op Bsub (@float_value.sub)).
+Axiom eval_float_mul : Hnf (eval_float_op Bmul (@float_value.mul)).
+Axiom eval_float_div : Hnf (eval_float_op Bdiv (@float_value.div)).
 
 (* The binary operator / divides the first operand by the second, after usual
    arithmetic conversions.
@@ -418,12 +418,12 @@ Arguments eval_ge _ {_}.
     eval_binop_pure bo (Tfloat_ f) (Tfloat_ f) ty'
       (Vfloat f av) (Vfloat f bv) (Vbool (o f av bv)).
 
-Axiom eval_float_eq : Hnf (eval_float_rel_op float_value.eqb Beq).
-Axiom eval_float_neq : Hnf (eval_float_rel_op float_value.neqb Bneq).
-Axiom eval_float_lt : Hnf (eval_float_rel_op float_value.ltb Blt).
-Axiom eval_float_gt : Hnf (eval_float_rel_op float_value.gtb Bgt).
-Axiom eval_float_le : Hnf (eval_float_rel_op float_value.leb Ble).
-Axiom eval_float_ge : Hnf (eval_float_rel_op float_value.geb Bge).
+Axiom eval_float_eq  : Hnf (eval_float_rel_op (@float_value.eqb) Beq).
+Axiom eval_float_neq : Hnf (eval_float_rel_op (@float_value.neqb) Bneq).
+Axiom eval_float_lt  : Hnf (eval_float_rel_op (@float_value.ltb) Blt).
+Axiom eval_float_gt  : Hnf (eval_float_rel_op (@float_value.gtb) Bgt).
+Axiom eval_float_le  : Hnf (eval_float_rel_op (@float_value.leb) Ble).
+Axiom eval_float_ge  : Hnf (eval_float_rel_op (@float_value.geb) Bge).
 
 (* Special cases for <decltype(nullptr)> because they are not generally comparable *)
 Axiom eval_eq_nullptr :

rocq-skylabs-brick/theories/lang/cpp/semantics/values.v

@@ -242,23 +242,23 @@ Module Type RAW_BYTES_VAL
   Axiom raw_bytes_of_val_sizeof : forall {σ ty v rs},
       raw_bytes_of_val σ ty v rs -> size_of σ ty = Some (N.of_nat $ length rs).
 
-  Definition float_raw_bytes (σ : genv) ft (f : float_type.car ft) : list raw_byte :=
+  Definition float_raw_bytes (σ : genv) {ft} (f : float_type.car ft) : list raw_byte :=
     raw_int_byte <$> _Z_to_bytes (N.to_nat (float_type.bytesN ft))
-      (genv_byte_order σ) Unsigned (float_value.to_bits ft f).
+      (genv_byte_order σ) Unsigned (float_value.to_bits f).
 
   Lemma float_raw_bytes_length σ ft (f : float_type.car ft) :
-    length (float_raw_bytes σ ft f) = N.to_nat (float_type.bytesN ft).
+    length (float_raw_bytes σ f) = N.to_nat (float_type.bytesN ft).
   Proof. by rewrite /float_raw_bytes length_fmap _Z_to_bytes_length. Qed.
 
   (** Float raw-byte support is intentionally narrow: the byte sequence is the
       deterministic object-size encoding of [float_value.to_bits].  Equality of
       such encodings for values of the same float type determines the value. *)
   Axiom raw_bytes_of_val_float : forall {σ ft} (f : float_type.car ft) rs,
       raw_bytes_of_val σ (Tfloat_ ft) (Vfloat ft f) rs <->
-      rs = float_raw_bytes σ ft f.
+      rs = float_raw_bytes σ f.
 
   #[global] Declare Instance float_raw_bytes_inj : forall {σ ft},
-      Inj (=) (=) (float_raw_bytes σ ft).
+      Inj (=) (=) (float_raw_bytes σ (ft := ft)).
 
   (* TODO Maybe add?
     Axiom raw_bytes_of_val_int : forall σ sz z rs,

rocq-skylabs-brick/theories/lang/cpp/syntax/compare.v

@@ -1962,7 +1962,7 @@ Module Expr.
       | Eunresolved_string_literal t => t
       | Eint n t => Box_Eint n t
       | Ebool b => b
-      | Efloat ft v => Box_Efloat ft (float_value.to_bits ft v)
+      | Efloat ft v => Box_Efloat ft (float_value.to_bits v)
       | Eunop op e t => Box_Eunop op e t
       | Ebinop op l r t => Box_Ebinop op l r t
       | Ederef e t => Box_Ederef e t