Library Interval.Language.Lang_expr
From Coq Require Import PrimInt63 Sint63 Floats PArray.
From Coq Require Import Bool List Reals Lia Lra.
From Flocq Require Import Core PrimFloat BinarySingleNaN Operations.
Require Generic_proof.
Local Open Scope R_scope.
From Coq Require Import Bool List Reals Lia Lra.
From Flocq Require Import Core PrimFloat BinarySingleNaN Operations.
Require Generic_proof.
Local Open Scope R_scope.
Signed computer integers: operations and constants
Definition Zcmod a b := let c := Z.quot b 2 in
((a + c) mod b - c)%Z.
Infix "cmod" := Zcmod (at level 40, no associativity) : Z_scope.
Lemma mod_mul_add_mod : ∀ a b m n c, (b ≠ 0)%Z → (∃ k, b = (k × c)%Z) →
((a mod b × m + n) mod c = (a × m + n) mod c)%Z.
Corollary cmod_mul_add_mod : ∀ a b m n c, (b ≠ 0)%Z → (∃ k, b = (k × c)%Z) →
((a cmod b × m + n) mod c = (a × m + n) mod c)%Z.
Corollary mod_add_mod : ∀ a b n c, (b ≠ 0)%Z → (∃ k, b = (k × c)%Z) →
((a mod b + n) mod c = (a + n) mod c)%Z.
Corollary mod_mul_mod : ∀ a b n c, (b ≠ 0)%Z → (∃ k, b = (k × c)%Z) →
((a mod b × n) mod c = (a × n) mod c)%Z.
Corollary cmod_add_mod : ∀ a b n c, (b ≠ 0)%Z → (∃ k, b = (k × c)%Z) →
((a cmod b + n) mod c = (a + n) mod c)%Z.
Corollary cmod_mul_mod : ∀ a b n c, (b ≠ 0)%Z → (∃ k, b = (k × c)%Z) →
((a cmod b × n) mod c = (a × n) mod c)%Z.
Lemma cmod_cmod : ∀ a b, (0 < b)%Z → (a cmod b)%Z = Sint63.cmod a b.
Lemma cmod_bounded : ∀ a b, (0 < b)%Z →
(- (b / 2) ≤ a cmod b ≤ b - b / 2 - 1)%Z.
Module Type Size.
Parameter bits : positive.
End Size.
Module Size32 <: Size.
Definition bits := 32%positive.
End Size32.
Module Size63 <: Size.
Definition bits := 63%positive.
End Size63.
Module Size64 <: Size.
Definition bits := 64%positive.
End Size64.
Module SI (S : Size).
Definition bits := S.bits.
Definition N := Z.pow_pos 2 bits.
Definition norm n := Zcmod n N.
Definition in_bounds n := (- (N/2) ≤ n ≤ N/2 - 1)%Z.
Lemma in_bounds_norm : ∀ n, in_bounds (norm n).
Lemma norm_in_bounds : ∀ n, in_bounds n → norm n = n.
Definition add n1 n2 := norm (n1 + n2)%Z.
Definition sub n1 n2 := norm (n1 - n2)%Z.
Definition mul n1 n2 := norm (n1 × n2)%Z.
Definition div n1 n2 := norm (n1 / n2)%Z. Definition quot n1 n2 := norm (Z.quot n1 n2).
End SI.
Module Int32 := SI Size32.
Module Int63 := SI Size63.
Module Int64 := SI Size64.
Real numbers: operations and constants
Notation Rpow2 := (bpow radix2).
Module Type Format.
Parameter prec : positive.
Parameter emax : Z.
End Format.
Module Format64 <: Format.
Definition prec := 53%positive.
Definition emax := 1024%Z.
End Format64.
Module RoundedR (F : Format).
Definition prec := Z.pos F.prec.
Definition emax := F.emax.
Definition emin := (3 - prec - emax)%Z.
Definition Rnd m := (round radix2 (FLT_exp emin prec) (round_mode m)).
Delimit Scope rnd_scope with rnd.
Notation rnd := (Rnd mode_NE).
Notation "x + y" := (rnd (x + y)) : rnd_scope.
Notation "x - y" := (rnd (x - y)) : rnd_scope.
Notation "x * y" := (rnd (x × y)) : rnd_scope.
Notation "x / y" := (rnd (x / y)) : rnd_scope.
Definition fma {md} x y z := Rnd md (x × y + z).
Definition sqrt {md} x := Rnd md (sqrt x).
Definition ldexp {md} x e := Rnd md (x × Rpow2 e).
Definition nearbyint {md} x := round radix2 (FIX_exp 0) (round_mode md) x.
Notation trunc := (@nearbyint mode_ZR).
Lemma nearbyint_IZR : ∀ md x, @nearbyint md x = IZR ((round_mode md) x).
Definition maxval := IZR (radix2 ^ prec - 1)%Z × Rpow2 (emax - prec)%Z.
Definition minval := Rpow2 emin.
Lemma maxval_lt : maxval < Rpow2 emax.
Lemma minval_gt : minval > 0.
End RoundedR.
Module Rrnd := RoundedR Format64.
On primitive arrays
Definition float_max x y := if ltb x y then y else x.
Definition float_min x y := if ltb x y then x else y.
Definition finite_array a :=
snd (N.iter (Z.to_N (Uint63.to_Z (PArray.length a)))
(fun '(i, b) ⇒ (Z.succ i, b && is_finite_SF (Prim2SF (get a (of_Z i))))) (0%Z, true)).
Definition float_array_max_partial a i := snd (N.iter (Z.to_N i)
(fun '(n, x) ⇒ (Z.succ n, float_max x (PArray.get a (Uint63.of_Z n)))) (0%Z, neg_infinity)).
Definition float_array_min_partial a i := snd (N.iter (Z.to_N i)
(fun '(n, x) ⇒ (Z.succ n, float_min x (PArray.get a (Uint63.of_Z n)))) (0%Z, infinity)).
Definition float_array_max a := float_array_max_partial a (Uint63.to_Z (PArray.length a)).
Definition float_array_min a := float_array_min_partial a (Uint63.to_Z (PArray.length a)).
Lemma finite_array_correct : ∀ a, finite_array a = true → ∀ i,
(Uint63.to_Z i < Uint63.to_Z (PArray.length a))%Z → is_finite (Prim2B a.[i]) = true.
Lemma float_array_max_partial_correct : ∀ a, finite_array a = true → ∀ i,
(Uint63.to_Z i ≤ Uint63.to_Z (PArray.length a))%Z →
let f := float_array_max_partial a (Uint63.to_Z i) in
((0 < Uint63.to_Z i)%Z → is_finite (Prim2B f) = true) ∧ ∀ j,
(0 ≤ Uint63.to_Z j < Uint63.to_Z i)%Z → PrimFloat.leb a.[j] f = true.
Lemma float_array_min_partial_correct : ∀ a, finite_array a = true → ∀ i,
(Uint63.to_Z i ≤ Uint63.to_Z (PArray.length a))%Z →
let f := float_array_min_partial a (Uint63.to_Z i) in
((0 < Uint63.to_Z i)%Z → is_finite (Prim2B f) = true) ∧ ∀ j,
(0 ≤ Uint63.to_Z j < Uint63.to_Z i)%Z → PrimFloat.leb f a.[j] = true.
Floating point numbers: operations and constants
Definition HPrec_gt_0 : Prec_gt_0 Rrnd.prec := Hprec.
Definition HPrec_lt_emax : Prec_lt_emax Rrnd.prec Rrnd.emax := Hmax.
Definition binnorm md m e := @binary_normalize _ _ HPrec_gt_0 HPrec_lt_emax md m e false.
Definition FPadd md x y := @Bplus _ _ HPrec_gt_0 HPrec_lt_emax md x y.
Definition FPsub md x y := @Bminus _ _ HPrec_gt_0 HPrec_lt_emax md x y.
Definition FPmul md x y := @Bmult _ _ HPrec_gt_0 HPrec_lt_emax md x y.
Definition FPdiv md x y := @Bdiv _ _ HPrec_gt_0 HPrec_lt_emax md x y.
Definition FPfma md x y z := @Bfma _ _ HPrec_gt_0 HPrec_lt_emax md x y z.
Definition FPnearbyint md x := @Bnearbyint _ _ HPrec_lt_emax md x.
Definition FPtrunc x := @Btrunc Rrnd.prec Rrnd.emax x.
Definition FPldexp md x e := @Bldexp _ _ HPrec_gt_0 HPrec_lt_emax md x e.
Definition FPsqrt md x := @Bsqrt _ _ HPrec_gt_0 HPrec_lt_emax md x.
Typed arithmetic expression trees
Inductive ExprType := Integer | BinFloat .
Definition evalExprTypePrim T := match T with
| Integer ⇒ PrimInt63.int
| BinFloat ⇒ PrimFloat.float
end.
Fixpoint evalExprTypePrim_list Tl : Set := match Tl with
| nil ⇒ unit
| T :: Tl' ⇒ evalExprTypePrim T × evalExprTypePrim_list Tl' end.
Fixpoint nthExprTypePrim {Tl DefaultT} n
(l : evalExprTypePrim_list Tl) (default : evalExprTypePrim DefaultT) :=
match n with
| O ⇒ match Tl return evalExprTypePrim_list Tl → evalExprTypePrim (nth O Tl DefaultT) with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ fst l'
end l
| S n' ⇒ match Tl return evalExprTypePrim_list Tl → evalExprTypePrim (nth (S n') Tl DefaultT) with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ nthExprTypePrim n' (snd l') default
end l
end.
Definition evalExprTypeFloat T := match T with
| Integer ⇒ Z
| BinFloat ⇒ binary_float Rrnd.prec Rrnd.emax
end.
Fixpoint evalExprTypeFloat_list Tl : Set := match Tl with
| nil ⇒ unit
| T :: Tl' ⇒ evalExprTypeFloat T × evalExprTypeFloat_list Tl' end.
Fixpoint nthExprTypeFloat {Tl DefaultT} n
(l : evalExprTypeFloat_list Tl) (default : evalExprTypeFloat DefaultT) :=
match n with
| O ⇒ match Tl return evalExprTypeFloat_list Tl → evalExprTypeFloat (nth O Tl DefaultT) with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ match T with
| Integer ⇒ fun l' ⇒ Int32.norm (fst l')
| BinFloat ⇒ fun l' ⇒ fst l'
end
end l
| S n' ⇒ match Tl return evalExprTypeFloat_list Tl → evalExprTypeFloat (nth (S n') Tl DefaultT) with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ nthExprTypeFloat n' (snd l') default
end l
end.
Definition evalExprTypeRounded T := match T with
| Integer ⇒ Z
| BinFloat ⇒ R
end.
Fixpoint evalExprTypeRounded_list Tl : Set := match Tl with
| nil ⇒ unit
| T :: Tl' ⇒ evalExprTypeRounded T × evalExprTypeRounded_list Tl' end.
Fixpoint evalExprTypeRounded_fun (Tl : list ExprType) := match Tl with
| nil ⇒ Prop
| T :: Tl' ⇒ evalExprTypeRounded T → evalExprTypeRounded_fun Tl' end.
Fixpoint uncurrify {Tl} :=
match Tl return evalExprTypeRounded_fun Tl → evalExprTypeRounded_list Tl → Prop with
| nil ⇒ fun f l ⇒ f
| _ :: Tl' ⇒ fun f l ⇒ uncurrify (f (fst l)) (snd l) end.
Fixpoint nthExprTypeRounded {Tl DefaultT} n
(l : evalExprTypeRounded_list Tl) (default : evalExprTypeRounded DefaultT) :=
match n with
| O ⇒ match Tl return evalExprTypeRounded_list Tl → evalExprTypeRounded (nth O Tl DefaultT) with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ fst l'
end l
| S n' ⇒ match Tl return evalExprTypeRounded_list Tl → evalExprTypeRounded (nth (S n') Tl DefaultT) with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ nthExprTypeRounded n' (snd l') default
end l
end.
Fixpoint evalExprTypeReal_list (Tl : list ExprType) : Set := match Tl with
| nil ⇒ unit
| _ :: Tl' ⇒ R × evalExprTypeReal_list Tl' end.
Fixpoint nthExprTypeReal {Tl} n (l : evalExprTypeReal_list Tl) (default : R) :=
match n with
| O ⇒ match Tl return evalExprTypeReal_list Tl → _ with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ fst l'
end l
| S n' ⇒ match Tl return evalExprTypeReal_list Tl → _ with
| nil ⇒ fun l' ⇒ default
| T :: Tl' ⇒ fun l' ⇒ nthExprTypeReal n' (snd l') default
end l
end.
Definition P2C {T} : evalExprTypePrim T → evalExprTypeFloat T :=
match T with
| Integer ⇒ fun x ⇒ Sint63.to_Z x
| BinFloat ⇒ fun x ⇒ Prim2B x
end.
Fixpoint P2C_list {Tl} : evalExprTypePrim_list Tl → evalExprTypeFloat_list Tl :=
match Tl with
| nil ⇒ fun l ⇒ tt
| _ :: _ ⇒ fun l ⇒ (P2C (fst l), P2C_list (snd l))
end.
Definition C2M {T} : evalExprTypeFloat T → evalExprTypeRounded T :=
match T with
| Integer ⇒ fun x ⇒ x
| BinFloat ⇒ fun x ⇒ B2R x
end.
Fixpoint C2M_list {Tl} : evalExprTypeFloat_list Tl → evalExprTypeRounded_list Tl :=
match Tl with
| nil ⇒ fun l ⇒ tt
| _ :: _ ⇒ fun l ⇒ (C2M (fst l), C2M_list (snd l))
end.
Definition M2R {T} : evalExprTypeRounded T → R :=
match T with
| Integer ⇒ fun x ⇒ IZR x
| BinFloat ⇒ fun x ⇒ x
end.
Fixpoint M2R_list {Tl} : evalExprTypeRounded_list Tl → evalExprTypeReal_list Tl :=
match Tl with
| nil ⇒ fun l ⇒ tt
| _ :: _ ⇒ fun l ⇒ (M2R (fst l), M2R_list (snd l))
end.
Definition P2M {T} : evalExprTypePrim T → evalExprTypeRounded T :=
match T with
| Integer ⇒ fun x ⇒ Sint63.to_Z x
| BinFloat ⇒ fun x ⇒ SF2R radix2 (Prim2SF x)
end.
Fixpoint P2M_list {Tl} : evalExprTypePrim_list Tl → evalExprTypeRounded_list Tl :=
match Tl with
| nil ⇒ fun l ⇒ tt
| _ :: _ ⇒ fun l ⇒ (P2M (fst l), P2M_list (snd l))
end.
Inductive ArithOp := ADD | SUB | MUL | DIV.
Definition PIOpToFunction OP := match OP with
| ADD ⇒ PrimInt63.add
| SUB ⇒ PrimInt63.sub
| MUL ⇒ PrimInt63.mul
| DIV ⇒ PrimInt63.divs end.
Definition PFOpToFunction OP := match OP with
| ADD ⇒ PrimFloat.add
| SUB ⇒ PrimFloat.sub
| MUL ⇒ PrimFloat.mul
| DIV ⇒ PrimFloat.div end.
Definition SIOpToFunction OP := match OP with
| ADD ⇒ Int32.add
| SUB ⇒ Int32.sub
| MUL ⇒ Int32.mul
| DIV ⇒ Int32.quot end.
Definition FPOpToFunction OP := match OP with
| ADD ⇒ FPadd
| SUB ⇒ FPsub
| MUL ⇒ FPmul
| DIV ⇒ FPdiv end.
Definition ZOpToFunction OP := match OP with
| ADD ⇒ Z.add
| SUB ⇒ Z.sub
| MUL ⇒ Z.mul
| DIV ⇒ Z.quot end.
Definition ROpToFunction OP := match OP with
| ADD ⇒ Rplus
| SUB ⇒ Rminus
| MUL ⇒ Rmult
| DIV ⇒ Rdiv end.
Definition RrndOpToFunction OP md x y :=
match OP with
| ADD ⇒ @Rrnd.Rnd md (x + y)
| SUB ⇒ @Rrnd.Rnd md (x - y)
| MUL ⇒ @Rrnd.Rnd md (x × y)
| DIV ⇒ @Rrnd.Rnd md (x / y)
end.
Inductive ArithExpr : list ExprType → ExprType → Type :=
| Int: ∀ {Tl}, Z → ArithExpr Tl Integer
| BinFl: ∀ {Tl}, PrimFloat.float → ArithExpr Tl BinFloat
| Var: ∀ {Tl} n, ArithExpr Tl (nth n Tl Integer)
| Op: ∀ {Tl T}, ArithOp →
ArithExpr Tl T →
ArithExpr Tl T → ArithExpr Tl T
| OpExact: ∀ {Tl}, ArithOp →
ArithExpr Tl BinFloat →
ArithExpr Tl BinFloat → ArithExpr Tl BinFloat
| Fma: ∀ {Tl}, ArithExpr Tl BinFloat →
ArithExpr Tl BinFloat →
ArithExpr Tl BinFloat → ArithExpr Tl BinFloat
| FmaExact: ∀ {Tl}, ArithExpr Tl BinFloat →
ArithExpr Tl BinFloat →
ArithExpr Tl BinFloat → ArithExpr Tl BinFloat
| Nearbyint: ∀ {Tl}, ArithExpr Tl BinFloat → ArithExpr Tl BinFloat
| FastNearbyint: ∀ {Tl}, ArithExpr Tl BinFloat → ArithExpr Tl BinFloat
| FastNearbyintToInt: ∀ {Tl}, ArithExpr Tl BinFloat → ArithExpr Tl Integer
| TruncToInt: ∀ {Tl}, ArithExpr Tl BinFloat → ArithExpr Tl Integer
| FloatInj: ∀ {Tl}, ArithExpr Tl Integer → ArithExpr Tl BinFloat
| Sqrt: ∀ {Tl T}, ArithExpr Tl T → ArithExpr Tl T
| Let: ∀ {Tl T1 T2}, ArithExpr Tl T1 →
ArithExpr (T1 :: Tl) T2 → ArithExpr Tl T2
| ArrayAcc: ∀ {Tl}, array PrimFloat.float →
ArithExpr Tl Integer → ArithExpr Tl BinFloat
| Assert: ∀ {Tl T}, (evalExprTypeRounded T → evalExprTypeRounded_fun Tl) →
ArithExpr Tl T → ArithExpr Tl T
| Postcond: ∀ {Tl T}, (evalExprTypeRounded T → evalExprTypeRounded_fun Tl) →
ArithExpr Tl T → ArithExpr Tl T.
Arguments Op {Tl} & {T} OP t1 t2.
Arguments OpExact {Tl} & OP t1 t2.
Arguments Fma {Tl} & t1 t2 t3.
Arguments FmaExact {Tl} & t1 t2 t3.
Arguments Nearbyint {Tl} & t.
Arguments FastNearbyint {Tl} & t.
Arguments FastNearbyintToInt {Tl} & t.
Arguments TruncToInt {Tl} & t.
Arguments FloatInj {Tl} & t.
Arguments Sqrt {Tl} & {T} t.
Arguments Let {Tl} & {T1 T2} t1 t2.
Arguments ArrayAcc {Tl} & a t.
Arguments Assert {Tl} & {T} P t.
Arguments Postcond {Tl} & {T} P t.
Fixpoint evalPrim {Tl T} (t: ArithExpr Tl T) {struct t}
: evalExprTypePrim_list Tl → evalExprTypePrim T
:= match t with
| Int _ p ⇒ fun l ⇒ Uint63.of_Z p
| BinFl _ x ⇒ fun l ⇒ x
| Var _ n ⇒ fun l ⇒ @nthExprTypePrim _ Integer n l (Uint63.of_Z 0)
| Op Tl' T' OP t1 t2 ⇒ fun l ⇒
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → evalExprTypePrim T' with
| Integer ⇒ fun t1' t2' ⇒ PIOpToFunction OP (evalPrim t1' l) (evalPrim t2' l)
| BinFloat ⇒ fun t1' t2' ⇒ PFOpToFunction OP (evalPrim t1' l) (evalPrim t2' l)
end t1 t2
| OpExact _ OP t1 t2 ⇒ fun l ⇒ PFOpToFunction OP (evalPrim t1 l) (evalPrim t2 l)
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ fun l ⇒ B2Prim (FPfma mode_NE (Prim2B (evalPrim t1 l)) (Prim2B (evalPrim t2 l)) (Prim2B (evalPrim t3 l)))
| Nearbyint _ t ⇒ fun l ⇒ B2Prim (FPnearbyint mode_NE (Prim2B (evalPrim t l)))
| FastNearbyint _ t ⇒ fun l ⇒ (evalPrim t l + 0x1.8p52 - 0x1.8p52)%float
| FastNearbyintToInt _ t ⇒ fun l ⇒ (normfr_mantissa (fst (frshiftexp (evalPrim t l + 0x1.8p52)%float)) - 6755399441055744)%uint63
| TruncToInt _ t ⇒ fun l ⇒ Uint63.of_Z (FPtrunc (Prim2B (evalPrim t l)))
| FloatInj _ t ⇒ fun l ⇒ let x := evalPrim t l in let absx := Sint63.abs x in
let f := PrimFloat.of_uint63 absx in if (0 <=? x)%sint63 then f else PrimFloat.opp f
| Sqrt Tl' T' t ⇒ fun l ⇒
match T' return ArithExpr Tl' T' → evalExprTypePrim T' with
| Integer ⇒ fun t' ⇒ Uint63.sqrt (evalPrim t' l)
| BinFloat ⇒ fun t' ⇒ PrimFloat.sqrt (evalPrim t' l)
end t
| Let _ _ _ t1 t2 ⇒ fun l ⇒ let x := evalPrim t1 l in evalPrim t2 (x, l)
| ArrayAcc _ a t ⇒ fun l ⇒ get a (evalPrim t l)
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l ⇒ evalPrim t l
end.
Fixpoint evalFloat {Tl T} (t: ArithExpr Tl T) {struct t}
: evalExprTypeFloat_list Tl → mode → evalExprTypeFloat T
:= match t in ArithExpr Tl'' T'' return evalExprTypeFloat_list Tl'' → mode → evalExprTypeFloat T'' with
| Int _ p ⇒ fun l md ⇒ Int32.norm p
| BinFl _ x ⇒ fun l md ⇒ Prim2B x
| Var _ n ⇒ fun l md ⇒ @nthExprTypeFloat _ Integer n l 0%Z
| Op Tl' T' OP t1 t2 ⇒ fun l md ⇒
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → evalExprTypeFloat T' with
| Integer ⇒ fun t1' t2' ⇒ SIOpToFunction OP (evalFloat t1' l md) (evalFloat t2' l md)
| BinFloat ⇒ fun t1' t2' ⇒ FPOpToFunction OP md (evalFloat t1' l md) (evalFloat t2' l md)
end t1 t2
| OpExact _ OP t1 t2 ⇒ fun l md ⇒ FPOpToFunction OP md (evalFloat t1 l md) (evalFloat t2 l md)
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒ FPfma md (evalFloat t1 l md) (evalFloat t2 l md) (evalFloat t3 l md)
| Nearbyint _ t ⇒ fun l md ⇒ FPnearbyint mode_NE (evalFloat t l md)
| FastNearbyint _ t ⇒ fun l md ⇒ FPsub mode_NE (FPadd mode_NE (evalFloat t l md) (Prim2B 0x1.8p52%float)) (Prim2B 0x1.8p52%float)
| FastNearbyintToInt _ t ⇒ fun l md ⇒ Int32.norm (FPtrunc (FPsub mode_NE (FPadd mode_NE (evalFloat t l md) (Prim2B 0x1.8p52%float)) (Prim2B 0x1.8p52%float)))
| TruncToInt _ t ⇒ fun l md ⇒ Int32.norm (FPtrunc (evalFloat t l md))
| FloatInj _ t ⇒ fun l md ⇒ binnorm mode_NE (evalFloat t l md) 0
| Sqrt Tl' T' t ⇒ fun l md ⇒
match T' return ArithExpr Tl' T' → evalExprTypeFloat T' with
| Integer ⇒ fun t' ⇒ Z.sqrt (evalFloat t' l md)
| BinFloat ⇒ fun t' ⇒ FPsqrt md (evalFloat t' l md)
end t
| Let _ _ _ t1 t2 ⇒ fun l md ⇒ let x := evalFloat t1 l md in evalFloat t2 (x, l) md
| ArrayAcc _ a t ⇒ fun l md ⇒ Prim2B (get a (of_Z (evalFloat t l md)))
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l md ⇒ evalFloat t l md
end.
Fixpoint evalRounded {Tl T} (t: ArithExpr Tl T) {struct t}
: evalExprTypeRounded_list Tl → mode → evalExprTypeRounded T
:= match t in ArithExpr Tl'' T'' return evalExprTypeRounded_list Tl'' → mode → evalExprTypeRounded T'' with
| Int _ p ⇒ fun l md ⇒ p
| BinFl _ x ⇒ fun l md ⇒ SF2R radix2 (Prim2SF x)
| Var _ n ⇒ fun l md ⇒ @nthExprTypeRounded _ Integer n l 0%Z
| Op Tl' T' OP t1 t2 ⇒ fun l md ⇒
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → evalExprTypeRounded T' with
| Integer ⇒ fun t1' t2' ⇒ ZOpToFunction OP (evalRounded t1' l md) (evalRounded t2' l md)
| BinFloat ⇒ fun t1' t2' ⇒ RrndOpToFunction OP md (evalRounded t1' l md) (evalRounded t2' l md)
end t1 t2
| OpExact _ OP t1 t2 ⇒ fun l md ⇒ ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md)
| Fma _ t1 t2 t3 ⇒ fun l md ⇒ @Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md)
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒ (evalRounded t1 l md) × (evalRounded t2 l md) + (evalRounded t3 l md)
| Nearbyint _ t
| FastNearbyint _ t ⇒ fun l md ⇒ @Rrnd.nearbyint mode_NE (evalRounded t l md)
| FastNearbyintToInt _ t ⇒ fun l md ⇒ ZnearestE (evalRounded t l md)
| TruncToInt _ t ⇒ fun l md ⇒ Ztrunc (evalRounded t l md)
| FloatInj _ t ⇒ fun l md ⇒ IZR (evalRounded t l md)
| Sqrt Tl' T' t ⇒ fun l md ⇒
match T' return ArithExpr Tl' T' → evalExprTypeRounded T' with
| Integer ⇒ fun t' ⇒ Z.sqrt (evalRounded t' l md)
| BinFloat ⇒ fun t' ⇒ @Rrnd.sqrt md (evalRounded t' l md)
end t
| Let _ _ _ t1 t2 ⇒ fun l md ⇒ let x := evalRounded t1 l md in evalRounded t2 (x, l) md
| ArrayAcc _ a t ⇒ fun l md ⇒ SF2R radix2 (Prim2SF (get a (of_Z (evalRounded t l md))))
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l md ⇒ evalRounded t l md
end.
Fixpoint evalExact {Tl T} (t: ArithExpr Tl T) {struct t}
: evalExprTypeRounded_list Tl → evalExprTypeRounded T
:= match t with
| Int _ p ⇒ fun l ⇒ p
| BinFl _ x ⇒ fun l ⇒ SF2R radix2 (Prim2SF x)
| Var _ n ⇒ fun l ⇒ @nthExprTypeRounded _ Integer n l 0%Z
| Op Tl' T' OP t1 t2 ⇒ fun l ⇒
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → evalExprTypeRounded T' with
| Integer ⇒ fun t1' t2' ⇒ ZOpToFunction OP (evalExact t1' l) (evalExact t2' l)
| BinFloat ⇒ fun t1' t2' ⇒ ROpToFunction OP (evalExact t1' l) (evalExact t2' l)
end t1 t2
| OpExact _ OP t1 t2 ⇒ fun l ⇒ ROpToFunction OP (evalExact t1 l) (evalExact t2 l)
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ fun l ⇒ (evalExact t1 l) × (evalExact t2 l) + (evalExact t3 l)
| Nearbyint _ t
| FastNearbyint _ t ⇒ fun l ⇒ 0
| FastNearbyintToInt _ t ⇒ fun l ⇒ 0%Z
| TruncToInt _ t ⇒ fun l ⇒ 0%Z
| FloatInj _ t ⇒ fun l ⇒ IZR (evalExact t l)
| Sqrt Tl' T' t ⇒ fun l ⇒
match T' return ArithExpr Tl' T' → evalExprTypeRounded T' with
| Integer ⇒ fun t' ⇒ Z.sqrt (evalExact t' l)
| BinFloat ⇒ fun t' ⇒ sqrt (evalExact t' l)
end t
| Let _ _ _ t1 t2 ⇒ fun l ⇒ let x := evalExact t1 l in evalExact t2 (x, l)
| ArrayAcc _ a t ⇒ fun l ⇒ 0
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l ⇒ evalExact t l
end.
Fixpoint evalReal {Tl T} (t: ArithExpr Tl T) {struct t}
: evalExprTypeReal_list Tl → _
:= match t with
| Int _ p ⇒ fun l md ⇒ IZR p
| BinFl _ x ⇒ fun l md ⇒ B2R (Prim2B x)
| Var _ n ⇒ fun l md ⇒ nthExprTypeReal n l 0
| Op Tl' T' OP t1 t2 ⇒ fun l md ⇒
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → _ with
| Integer ⇒ fun t1' t2' ⇒ match OP with
| DIV ⇒ Rrnd.trunc (evalReal t1' l md / evalReal t2' l md)
| _ ⇒ ROpToFunction OP (evalReal t1' l md) (evalReal t2' l md)
end
| BinFloat ⇒ fun t1' t2' ⇒ RrndOpToFunction OP md (evalReal t1' l md) (evalReal t2' l md)
end t1 t2
| OpExact _ OP t1 t2 ⇒ fun l md ⇒ ROpToFunction OP (evalReal t1 l md) (evalReal t2 l md)
| Fma _ t1 t2 t3 ⇒ fun l md ⇒ @Rrnd.fma md (evalReal t1 l md) (evalReal t2 l md) (evalReal t3 l md)
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒ evalReal t1 l md × evalReal t2 l md + evalReal t3 l md
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t ⇒ fun l md ⇒ @Rrnd.nearbyint mode_NE (evalReal t l md)
| TruncToInt _ t ⇒ fun l md ⇒ Rrnd.trunc (evalReal t l md)
| FloatInj _ t ⇒ fun l md ⇒ evalReal t l md
| Sqrt Tl' T' t ⇒ fun l md ⇒
match T' return ArithExpr Tl' T' → _ with
| Integer ⇒ fun t' ⇒ Rrnd.trunc (sqrt (evalReal t' l md))
| BinFloat ⇒ fun t' ⇒ @Rrnd.sqrt md (evalReal t' l md)
end t
| Let _ _ _ t1 t2 ⇒ fun l md ⇒ let x := evalReal t1 l md in evalReal t2 (x, l) md
| ArrayAcc _ a t ⇒ fun l md ⇒ SF2R radix2 (Prim2SF (get a (of_Z (Ztrunc (evalReal t l md)))))
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l md ⇒ evalReal t l md
end.
Definition convertibleFloat {T} : evalExprTypeFloat T → Prop :=
match T with
| Integer ⇒ fun n ⇒ Int32.in_bounds n
| BinFloat ⇒ fun f ⇒ @is_finite Rrnd.prec Rrnd.emax f = true
end.
Definition convertiblePrim {T} : evalExprTypePrim T → Prop :=
match T with
| Integer ⇒ fun n ⇒ Int32.in_bounds (to_Z n)
| BinFloat ⇒ fun f ⇒ @is_finite_SF (Prim2SF f) = true
end.
Fixpoint convertibleFloat_list {Tl} : evalExprTypeFloat_list Tl → Prop :=
match Tl with
| nil ⇒ fun lC ⇒ True
| T :: _ ⇒ fun lC ⇒ convertibleFloat (fst lC) ∧ convertibleFloat_list (snd lC)
end.
Fixpoint convertiblePrim_list {Tl} : evalExprTypePrim_list Tl → Prop :=
match Tl with
| nil ⇒ fun lC ⇒ True
| T :: _ ⇒ fun lC ⇒ convertiblePrim (fst lC) ∧ convertiblePrim_list (snd lC)
end.
Definition isConversionFloat {T} : evalExprTypeFloat T → evalExprTypeRounded T → Prop :=
match T with
| Integer ⇒ fun n1 n2 ⇒ n1 = n2
| BinFloat ⇒ fun f r ⇒ @B2R Rrnd.prec Rrnd.emax f = r
end.
Definition isConversionPrim {T} : evalExprTypePrim T → evalExprTypeRounded T → Prop :=
match T with
| Integer ⇒ fun n1 n2 ⇒ Sint63.to_Z n1 = n2
| BinFloat ⇒ fun f r ⇒ @SF2R radix2 (Prim2SF f) = r
end.
Definition eqExprTypeFloat {T} (e1 : evalExprTypeFloat T) (e2 : evalExprTypeRounded T) :=
convertibleFloat e1 ∧ isConversionFloat e1 e2.
Definition eqExprTypePrim {T} (e1 : evalExprTypePrim T) (e2 : evalExprTypeRounded T) :=
convertiblePrim e1 ∧ isConversionPrim e1 e2.
Fixpoint assertions {Tl T} (t : ArithExpr Tl T) : evalExprTypeRounded_list Tl → _ :=
match t with
| Int _ _
| BinFl _ _
| Var _ _
| ArrayAcc _ _ _ ⇒ fun l md ⇒ True
| Op _ _ _ t1 t2
| OpExact _ _ t1 t2
⇒ fun l md ⇒ assertions t1 l md
∧ assertions t2 l md
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒ assertions t1 l md
∧ assertions t2 l md
∧ assertions t3 l md
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t
| TruncToInt _ t
| FloatInj _ t
| Sqrt _ _ t ⇒ fun l md ⇒ assertions t l md
| Let _ _ _ t1 t2 ⇒ fun l md ⇒ assertions t1 l md
∧ let x := evalRounded t1 l md in
assertions t2 (x, l) md
| Assert _ _ P t ⇒ fun l md ⇒ let P' := P (evalExact t l) in
uncurrify P' l ∧ assertions t l md
| Postcond _ _ _ t ⇒ fun l md ⇒ assertions t l md
end.
Fixpoint wellDefined {Tl T} (t: ArithExpr Tl T) : evalExprTypeRounded_list Tl → _ :=
match t with
| Int _ _
| BinFl _ _
| Var _ _ ⇒ fun l md ⇒ True
| Op _ T' OP t1 t2 ⇒ fun l md ⇒
let P := wellDefined t1 l md ∧ wellDefined t2 l md in
match OP with
| DIV ⇒ P ∧ evalRounded t2 l md ≠ match T' with Integer ⇒ 0%Z | _ ⇒ 0 end
| _ ⇒ P
end
| OpExact _ OP t1 t2 ⇒ fun l md ⇒
let P := wellDefined t1 l md ∧ wellDefined t2 l md in
match OP with
| DIV ⇒ P ∧ evalRounded t2 l md ≠ 0
| _ ⇒ P
end
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒
wellDefined t1 l md ∧ wellDefined t2 l md ∧ wellDefined t3 l md
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t
| TruncToInt _ t
| FloatInj _ t ⇒ fun l md ⇒ wellDefined t l md
| Sqrt Tl' T' t ⇒ fun l md ⇒ wellDefined t l md ∧
match T' return ArithExpr Tl' T' → _ with
| Integer ⇒ fun t' ⇒ 0 ≤ IZR (evalRounded t' l md)
| _ ⇒ fun t' ⇒ 0 ≤ evalRounded t' l md
end t
| Let _ _ _ t1 t2 ⇒ fun l md ⇒
wellDefined t1 l md ∧ wellDefined t2 (evalRounded t1 l md, l) md
| ArrayAcc _ _ t
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l md ⇒ wellDefined t l md
end.
Fixpoint operationsExact {Tl T} (t: ArithExpr Tl T) : evalExprTypeRounded_list Tl → _ :=
match t with
| Int _ _
| BinFl _ _
| Var _ _ ⇒ fun l md ⇒ True
| Op Tl' T' OP t1 t2 ⇒ fun l md ⇒
operationsExact t1 l md ∧ operationsExact t2 l md ∧
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → _ with
| Integer ⇒ fun t1' t2' ⇒
- IZR (Int32.N / 2) ≤ IZR (ZOpToFunction OP (evalRounded t1' l md) (evalRounded t2' l md)) ≤ IZR (Int32.N / 2 - 1)
| BinFloat ⇒ fun t1' t2' ⇒ Rabs (RrndOpToFunction OP md (evalRounded t1' l md) (evalRounded t2' l md)) ≤ Rrnd.maxval
end t1 t2
| OpExact _ OP t1 t2 ⇒ fun l md ⇒
operationsExact t1 l md ∧ operationsExact t2 l md ∧
Rabs (ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md)) ≤ Rrnd.maxval ∧
RrndOpToFunction OP md (evalRounded t1 l md) (evalRounded t2 l md)
= ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md)
| Fma _ t1 t2 t3 ⇒ fun l md ⇒
operationsExact t1 l md ∧ operationsExact t2 l md ∧ operationsExact t3 l md ∧
Rabs (@Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md)) ≤ Rrnd.maxval
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒
operationsExact t1 l md ∧ operationsExact t2 l md ∧ operationsExact t3 l md ∧
Rabs ((evalRounded t1 l md) × (evalRounded t2 l md) + (evalRounded t3 l md)) ≤ Rrnd.maxval ∧
@Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md) =
(evalRounded t1 l md) × (evalRounded t2 l md) + (evalRounded t3 l md)
| Nearbyint _ t ⇒ fun l md ⇒ operationsExact t l md
| FastNearbyint _ t ⇒ fun l md ⇒ operationsExact t l md ∧
-2251799813685248 ≤ evalRounded t l md ≤ 2251799813685247
| FastNearbyintToInt _ t ⇒ fun l md ⇒ operationsExact t l md ∧
-2147483648 ≤ evalRounded t l md ≤ 2147483647
| TruncToInt _ t ⇒ fun l md ⇒ operationsExact t l md ∧
(- Int32.N / 2 ≤ Ztrunc (evalRounded t l md) ≤ Int32.N / 2 - 1)%Z
| FloatInj _ t ⇒ fun l md ⇒ operationsExact t l md ∧ Rabs (IZR (evalRounded t l md)) ≤ Rpow2 53
| Sqrt _ _ t ⇒ fun l md ⇒ operationsExact t l md
| ArrayAcc _ a t ⇒ fun l md ⇒ operationsExact t l md ∧
(0 ≤ evalRounded t l md < Uint63.to_Z (PArray.length a))%Z
| Let _ _ _ t1 t2 ⇒ fun l md ⇒
operationsExact t1 l md ∧ operationsExact t2 (evalRounded t1 l md, l) md
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l md ⇒ operationsExact t l md
end.
Fixpoint wellBehaved {Tl T} (t: ArithExpr Tl T) : evalExprTypeRounded_list Tl → _ :=
match t with
| Int _ _
| BinFl _ _
| Var _ _ ⇒ fun l md ⇒ True
| Op Tl' T' OP t1 t2 ⇒ fun l md ⇒ wellBehaved t1 l md ∧ wellBehaved t2 l md ∧ let P :=
match T' return ArithExpr Tl' T' → ArithExpr Tl' T' → _ with
| Integer ⇒ fun t1' t2' ⇒ - IZR (Int32.N / 2) ≤ IZR (ZOpToFunction OP (evalRounded t1' l md) (evalRounded t2' l md)) ≤ IZR (Int32.N / 2 - 1)
| BinFloat ⇒ fun t1' t2' ⇒ Rabs (RrndOpToFunction OP md (evalRounded t1' l md) (evalRounded t2' l md)) ≤ Rrnd.maxval end t1 t2 in
match OP with
| DIV ⇒ P ∧ evalRounded t2 l md ≠ match T' with Integer ⇒ 0%Z | _ ⇒ 0 end
| _ ⇒ P
end
| OpExact _ OP t1 t2 ⇒ fun l md ⇒ let P := wellBehaved t1 l md ∧ wellBehaved t2 l md ∧
Rabs (ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md)) ≤ Rrnd.maxval ∧
RrndOpToFunction OP md (evalRounded t1 l md) (evalRounded t2 l md) = ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md) in
match OP with
| DIV ⇒ P ∧ evalRounded t2 l md ≠ 0
|_ ⇒ P
end
| Fma _ t1 t2 t3 ⇒ fun l md ⇒
wellBehaved t1 l md ∧ wellBehaved t2 l md ∧ wellBehaved t3 l md ∧
Rabs (@Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md)) ≤ Rrnd.maxval
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒
wellBehaved t1 l md ∧ wellBehaved t2 l md ∧ wellBehaved t3 l md ∧
Rabs ((evalRounded t1 l md) × (evalRounded t2 l md) + (evalRounded t3 l md)) ≤ Rrnd.maxval ∧
@Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md) =
(evalRounded t1 l md) × (evalRounded t2 l md) + (evalRounded t3 l md)
| Nearbyint _ t ⇒ fun l md ⇒ wellBehaved t l md
| FastNearbyint _ t ⇒ fun l md ⇒ wellBehaved t l md ∧
-2251799813685248 ≤ evalRounded t l md ≤ 2251799813685247
| FastNearbyintToInt _ t ⇒ fun l md ⇒ wellBehaved t l md ∧
-2147483648 ≤ evalRounded t l md ≤ 2147483647
| TruncToInt _ t ⇒ fun l md ⇒ wellBehaved t l md ∧
(- Int32.N / 2 ≤ Ztrunc (evalRounded t l md) ≤ Int32.N / 2 - 1)%Z
| FloatInj _ t ⇒ fun l md ⇒ wellBehaved t l md ∧ Rabs (IZR (evalRounded t l md)) ≤ Rpow2 53
| Sqrt Tl' T' t ⇒ fun l md ⇒ wellBehaved t l md ∧
match T' return ArithExpr Tl' T' → _ with
| Integer ⇒ fun t' ⇒ 0 ≤ IZR (evalRounded t' l md)
| _ ⇒ fun t' ⇒ 0 ≤ evalRounded t' l md
end t
| Let _ _ _ t1 t2 ⇒ fun l md ⇒ wellBehaved t1 l md ∧ wellBehaved t2 (evalRounded t1 l md, l) md
| ArrayAcc _ a t ⇒ fun l md ⇒ wellBehaved t l md ∧
(0 ≤ evalRounded t l md < Uint63.to_Z (PArray.length a))%Z
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ fun l md ⇒ wellBehaved t l md
end.
Fixpoint postconditions {Tl T} (t : ArithExpr Tl T) : evalExprTypeRounded_list Tl → _ :=
match t with
| Int _ _
| BinFl _ _
| Var _ _ ⇒ fun l md ⇒ True
| Op _ _ _ t1 t2
| OpExact _ _ t1 t2
⇒ fun l md ⇒ postconditions t1 l md
∧ postconditions t2 l md
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ fun l md ⇒ postconditions t1 l md
∧ postconditions t2 l md
∧ postconditions t3 l md
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t
| TruncToInt _ t
| FloatInj _ t
| Sqrt _ _ t ⇒ fun l md ⇒ postconditions t l md
| Let _ _ _ t1 t2 ⇒ fun l md ⇒ postconditions t1 l md
∧ let x := evalRounded t1 l md in
postconditions t2 (x, l) md
| ArrayAcc _ a t ⇒ fun l md ⇒ True
| Assert _ _ _ t ⇒ fun l md ⇒ postconditions t l md
| Postcond _ _ P t ⇒ fun l md ⇒ let P' := P (evalRounded t l md) in
uncurrify P' l ∧ postconditions t l md
end.
Definition fullyCorrect {Tl T} (t: ArithExpr Tl T) l md :=
assertions t l md → (wellBehaved t l md ∧ postconditions t l md).
Fixpoint wellFormed {Tl T} (t: ArithExpr Tl T) := match t with
| Int _ n ⇒ (- Z.pow_pos 2 (Int32.bits - 1) <=? n)%Z
&& (n <? Z.pow_pos 2 (Int32.bits - 1))%Z
| BinFl _ x ⇒ is_finite_SF (Prim2SF x)
| Var _ _ ⇒ true
| Op _ _ _ t1 t2
| OpExact _ _ t1 t2
⇒ wellFormed t1 && wellFormed t2
| Fma _ t1 t2 t3
| FmaExact _ t1 t2 t3 ⇒ wellFormed t1 && wellFormed t2 && wellFormed t3
| Let _ _ _ t1 t2 ⇒ wellFormed t1 && wellFormed t2
| ArrayAcc _ a t ⇒ wellFormed t && finite_array a
| Nearbyint _ t
| FastNearbyint _ t
| FastNearbyintToInt _ t
| TruncToInt _ t
| FloatInj _ t
| Sqrt _ _ t
| Assert _ _ _ t
| Postcond _ _ _ t ⇒ wellFormed t
end.
Lemma Ztrunc_div_ : ∀ x y : Z, Ztrunc (IZR x / IZR y) = (x ÷ y)%Z.
Lemma Zfloor_add : ∀ x n, (Zfloor x + n)%Z = Zfloor (x + IZR n).
Lemma Zfloor_mul : ∀ x, 0 ≤ x → Z.le (Zfloor x × Zfloor x)%Z (Zfloor (x × x)).
Lemma trunc_sqrt: ∀ n, Zfloor (sqrt (IZR n)) = Z.sqrt n.
Lemma evalReal_evalRounded {Tl T} :
∀ (t: ArithExpr Tl T) (lM : evalExprTypeRounded_list Tl) md,
let lR := M2R_list lM in
evalReal t lR md = M2R (evalRounded t lM md).
Lemma wellBehaved_decompose {Tl T} :
∀ (t: ArithExpr Tl T) (l : evalExprTypeRounded_list Tl) md,
wellBehaved t l md ↔ wellDefined t l md ∧ operationsExact t l md.
Lemma equivFloat_Int {Tl} : ∀ n (lC : evalExprTypeFloat_list Tl) md,
(- Z.pow_pos 2 (Int32.bits - 1) ≤ n < Z.pow_pos 2 (Int32.bits - 1))%Z →
let lM := C2M_list lC in
eqExprTypeFloat (evalFloat (Int n) lC md) (evalRounded (Int n) lM md).
Lemma equivPrim_Int {Tl} : ∀ n (lP : evalExprTypePrim_list Tl),
(- Z.pow_pos 2 (Int32.bits - 1) ≤ n < Z.pow_pos 2 (Int32.bits - 1))%Z →
let lM := P2M_list lP in
eqExprTypePrim (evalPrim (Int n) lP) (evalRounded (Int n) lM mode_NE).
Lemma equivFloat_Op_ADD_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
Rabs (@Rrnd.Rnd md (evalRounded t1 lM md + evalRounded t2 lM md)) ≤ Rrnd.maxval →
eqExprTypeFloat (evalFloat (Op ADD t1 t2) lC md) (evalRounded (Op ADD t1 t2) lM md).
Lemma Prim2SF2R_Prim2B2R : ∀ x, SF2R radix2 (Prim2SF x) = B2R (Prim2B x).
Lemma equivPrim_Op_ADD_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
Rabs (@Rrnd.Rnd mode_NE (evalRounded t1 lM mode_NE + evalRounded t2 lM mode_NE)) ≤ Rrnd.maxval →
eqExprTypePrim (evalPrim (Op ADD t1 t2) lP) (evalRounded (Op ADD t1 t2) lM mode_NE).
Lemma equivFloat_Op_SUB_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
Rabs (@Rrnd.Rnd md (evalRounded t1 lM md - evalRounded t2 lM md)) ≤ Rrnd.maxval →
eqExprTypeFloat (evalFloat (Op SUB t1 t2) lC md) (evalRounded (Op SUB t1 t2) lM md).
Lemma equivPrim_Op_SUB_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
Rabs (@Rrnd.Rnd mode_NE (evalRounded t1 lM mode_NE - evalRounded t2 lM mode_NE)) ≤ Rrnd.maxval →
eqExprTypePrim (evalPrim (Op SUB t1 t2) lP) (evalRounded (Op SUB t1 t2) lM mode_NE).
Lemma equivFloat_Op_MUL_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
Rabs (@Rrnd.Rnd md (evalRounded t1 lM md × evalRounded t2 lM md)) ≤ Rrnd.maxval →
eqExprTypeFloat (evalFloat (Op MUL t1 t2) lC md) (evalRounded (Op MUL t1 t2) lM md).
Lemma equivPrim_Op_MUL_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
Rabs (@Rrnd.Rnd mode_NE (evalRounded t1 lM mode_NE × evalRounded t2 lM mode_NE)) ≤ Rrnd.maxval →
eqExprTypePrim (evalPrim (Op MUL t1 t2) lP) (evalRounded (Op MUL t1 t2) lM mode_NE).
Lemma equivFloat_Op_DIV_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
evalRounded t2 lM md ≠ 0 →
Rabs (@Rrnd.Rnd md (evalRounded t1 lM md / evalRounded t2 lM md)) ≤ Rrnd.maxval →
eqExprTypeFloat (evalFloat (Op DIV t1 t2) lC md) (evalRounded (Op DIV t1 t2) lM md).
Lemma equivPrim_Op_DIV_BinFloat {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
evalRounded t2 lM mode_NE ≠ 0 →
Rabs (@Rrnd.Rnd mode_NE (evalRounded t1 lM mode_NE / evalRounded t2 lM mode_NE)) ≤ Rrnd.maxval →
eqExprTypePrim (evalPrim (Op DIV t1 t2) lP) (evalRounded (Op DIV t1 t2) lM mode_NE).
Lemma equivFloat_Op_ADD_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
- IZR (Int32.N / 2) ≤ IZR ((evalRounded t1 lM md) + (evalRounded t2 lM md)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypeFloat (evalFloat (Op ADD t1 t2) lC md) (evalRounded (Op ADD t1 t2) lM md).
Lemma equivPrim_Op_ADD_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
- IZR (Int32.N / 2) ≤ IZR ((evalRounded t1 lM mode_NE) + (evalRounded t2 lM mode_NE)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypePrim (evalPrim (Op ADD t1 t2) lP) (evalRounded (Op ADD t1 t2) lM mode_NE).
Lemma equivFloat_Op_SUB_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
- IZR (Int32.N / 2) ≤ IZR ((evalRounded t1 lM md) - (evalRounded t2 lM md)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypeFloat (evalFloat (Op SUB t1 t2) lC md) (evalRounded (Op SUB t1 t2) lM md).
Lemma equivPrim_Op_SUB_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
- IZR (Int32.N / 2) ≤ IZR ((evalRounded t1 lM mode_NE) - (evalRounded t2 lM mode_NE)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypePrim (evalPrim (Op SUB t1 t2) lP) (evalRounded (Op SUB t1 t2) lM mode_NE).
Lemma equivFloat_Op_MUL_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
- IZR (Int32.N / 2) ≤ IZR ((evalRounded t1 lM md) × (evalRounded t2 lM md)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypeFloat (evalFloat (Op MUL t1 t2) lC md) (evalRounded (Op MUL t1 t2) lM md).
Lemma equivPrim_Op_MUL_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
- IZR (Int32.N / 2) ≤ IZR ((evalRounded t1 lM mode_NE) × (evalRounded t2 lM mode_NE)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypePrim (evalPrim (Op MUL t1 t2) lP) (evalRounded (Op MUL t1 t2) lM mode_NE).
Lemma equivFloat_Op_DIV_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
(evalRounded t2 lM md ≠ 0)%Z →
- IZR (Int32.N / 2) ≤ IZR (Z.quot (evalRounded t1 lM md) (evalRounded t2 lM md)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypeFloat (evalFloat (Op DIV t1 t2) lC md) (evalRounded (Op DIV t1 t2) lM md).
Lemma equivPrim_Op_DIV_Integer {Tl} : ∀ (t1 t2 : ArithExpr Tl Integer)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
(evalRounded t2 lM mode_NE ≠ 0)%Z →
- IZR (Int32.N / 2) ≤ IZR (Z.quot (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE)) ≤ IZR (Int32.N / 2 - 1) →
eqExprTypePrim (evalPrim (Op DIV t1 t2) lP) (evalRounded (Op DIV t1 t2) lM mode_NE).
Lemma equivFloat_OpExact {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat) OP
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
match OP with DIV ⇒ evalRounded t2 lM md ≠ 0 | _ ⇒ True end →
Rabs (ROpToFunction OP (evalRounded t1 lM md) (evalRounded t2 lM md)) ≤ Rrnd.maxval →
RrndOpToFunction OP md (evalRounded t1 lM md) (evalRounded t2 lM md) = ROpToFunction OP (evalRounded t1 lM md) (evalRounded t2 lM md) →
eqExprTypeFloat (evalFloat (OpExact OP t1 t2) lC md) (evalRounded (OpExact OP t1 t2) lM md).
Lemma equivPrim_OpExact {Tl} : ∀ (t1 t2 : ArithExpr Tl BinFloat) OP
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
match OP with DIV ⇒ evalRounded t2 lM mode_NE ≠ 0 | _ ⇒ True end →
Rabs (ROpToFunction OP (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE)) ≤ Rrnd.maxval →
RrndOpToFunction OP mode_NE (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) = ROpToFunction OP (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) →
eqExprTypePrim (evalPrim (OpExact OP t1 t2) lP) (evalRounded (OpExact OP t1 t2) lM mode_NE).
Lemma equivFloat_Fma {Tl} : ∀ (t1 t2 t3 : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
eqExprTypeFloat (evalFloat t3 lC md) (evalRounded t3 lM md) →
Rabs (@Rrnd.fma md (evalRounded t1 lM md) (evalRounded t2 lM md) (evalRounded t3 lM md)) ≤ Rrnd.maxval →
eqExprTypeFloat (evalFloat (Fma t1 t2 t3) lC md) (evalRounded (Fma t1 t2 t3) lM md).
Lemma equivPrim_Fma {Tl} : ∀ (t1 t2 t3 : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
eqExprTypePrim (evalPrim t3 lP) (evalRounded t3 lM mode_NE) →
Rabs (@Rrnd.fma mode_NE (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) (evalRounded t3 lM mode_NE)) ≤ Rrnd.maxval →
eqExprTypePrim (evalPrim (Fma t1 t2 t3) lP) (evalRounded (Fma t1 t2 t3) lM mode_NE).
Lemma equivFloat_FmaExact {Tl} : ∀ (t1 t2 t3 : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) →
eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) →
eqExprTypeFloat (evalFloat t3 lC md) (evalRounded t3 lM md) →
Rabs (evalRounded t1 lM md × evalRounded t2 lM md + evalRounded t3 lM md) ≤ Rrnd.maxval →
(@Rrnd.fma md (evalRounded t1 lM md) (evalRounded t2 lM md) (evalRounded t3 lM md))
= evalRounded t1 lM md × evalRounded t2 lM md + evalRounded t3 lM md→
eqExprTypeFloat (evalFloat (FmaExact t1 t2 t3) lC md) (evalRounded (FmaExact t1 t2 t3) lM md).
Lemma equivPrim_FmaExact {Tl} : ∀ (t1 t2 t3 : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) →
eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) →
eqExprTypePrim (evalPrim t3 lP) (evalRounded t3 lM mode_NE) →
Rabs (evalRounded t1 lM mode_NE × evalRounded t2 lM mode_NE + evalRounded t3 lM mode_NE) ≤ Rrnd.maxval →
(@Rrnd.fma mode_NE (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) (evalRounded t3 lM mode_NE))
= evalRounded t1 lM mode_NE × evalRounded t2 lM mode_NE + evalRounded t3 lM mode_NE →
eqExprTypePrim (evalPrim (FmaExact t1 t2 t3) lP) (evalRounded (FmaExact t1 t2 t3) lM mode_NE).
Lemma equivFloat_Nearbyint {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
eqExprTypeFloat (evalFloat (Nearbyint t) lC md) (evalRounded (Nearbyint t) lM md).
Lemma equivPrim_Nearbyint {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
eqExprTypePrim (evalPrim (Nearbyint t) lP) (evalRounded (Nearbyint t) lM mode_NE).
Lemma ZnearestE_plus_even : ∀ x n, Z.even n = true → (ZnearestE x + n = ZnearestE (x + IZR n))%Z.
Lemma aux_2 : generic_format radix2 (fexp prec emax) (Rpow2 53 - 1).
Lemma aux_3 : ∀ x', x' ≤ Rpow2 53 - 1 →
round radix2 (fexp prec emax) ZnearestE x' < Rpow2 53.
Lemma aux_4 : ∀ (x : binary_float prec emax),
-2251799813685248 ≤ B2R x ≤ 2251799813685247 →
Rpow2 52 ≤ B2R x + B2R (Prim2B 6755399441055744) ≤ Rpow2 53 - 1.
Lemma fastnearbyint_correct : ∀ x, is_finite (Prim2B x) = true →
-2251799813685248 ≤ B2R (Prim2B x) ≤ 2251799813685247 →
Uint63.to_Z (normfr_mantissa (fst (frshiftexp (x + 6755399441055744)))) =
(ZnearestE (SF2R radix2 (Prim2SF x)) + 6755399441055744)%Z.
Lemma equivFloat_FastNearbyint {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
-2251799813685248 ≤ evalRounded t lM md ≤ 2251799813685247 →
eqExprTypeFloat (evalFloat (FastNearbyint t) lC md) (evalRounded (FastNearbyint t) lM md).
Lemma equivPrim_FastNearbyint {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
-2251799813685248 ≤ evalRounded t lM mode_NE ≤ 2251799813685247 →
eqExprTypePrim (evalPrim (FastNearbyint t) lP) (evalRounded (FastNearbyint t) lM mode_NE).
Lemma equivFloat_FastNearbyintToInt {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
(-2147483648 ≤ evalRounded t lM md ≤ 2147483647)%R →
eqExprTypeFloat (evalFloat (FastNearbyintToInt t) lC md) (evalRounded (FastNearbyintToInt t) lM md).
Lemma equivPrim_FastNearbyintToInt {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
-2147483648 ≤ evalRounded t lM mode_NE ≤ 2147483647 →
eqExprTypePrim (evalPrim (FastNearbyintToInt t) lP) (evalRounded (FastNearbyintToInt t) lM mode_NE).
Lemma equivFloat_TruncToInt {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
(- Int32.N / 2 ≤ Ztrunc (evalRounded t lM md) ≤ Int32.N / 2 - 1)%Z →
eqExprTypeFloat (evalFloat (TruncToInt t) lC md) (evalRounded (TruncToInt t) lM md).
Lemma equivPrim_TruncToInt {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
(- Int32.N / 2 ≤ Ztrunc (evalRounded t lM mode_NE) ≤ Int32.N / 2 - 1)%Z →
eqExprTypePrim (evalPrim (TruncToInt t) lP) (evalRounded (TruncToInt t) lM mode_NE).
Lemma PrimInt63_opp_involutive : ∀ x, (- - x)%uint63 = x.
Lemma PrimInt63_opp_inj : ∀ x y, (- x)%uint63 = (- y)%uint63 → x = y.
Lemma lesb_ltb : ∀ x, lesb 0 x = Uint63.ltb x min_int.
Lemma generic_format_fexp_IZR : ∀ n prec emax, (0 < prec)%Z → (3 - prec < emax)%Z →
(Z.abs n ≤ 2 ^ prec)%Z → generic_format radix2 (fexp prec emax) (IZR n).
Lemma equivFloat_FloatInj {Tl} : ∀ (t : ArithExpr Tl Integer)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
Rabs (IZR (evalRounded t lM md)) ≤ Rpow2 53 →
eqExprTypeFloat (evalFloat (FloatInj t) lC md) (evalRounded (FloatInj t) lM md).
Lemma equivPrim_FloatInj {Tl} : ∀ (t : ArithExpr Tl Integer)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
Rabs (IZR (evalRounded t lM mode_NE)) ≤ Rpow2 53 →
eqExprTypePrim (evalPrim (FloatInj t) lP) (evalRounded (FloatInj t) lM mode_NE).
Lemma Uint63_to_Z_sqrt : ∀ x, Uint63.to_Z (Uint63.sqrt x) = Z.sqrt (Uint63.to_Z x).
Lemma Uint63_sqrt_small : ∀ x, (Uint63.sqrt x <? min_int = true)%uint63.
Lemma in_bounds_to_Z_Uint63_sqrt : ∀ x,
(Uint63.to_Z x ≤ 2 ^ 62 - 1)%Z →
Int32.in_bounds (Uint63.to_Z (Uint63.sqrt x)).
Lemma equivFloat_Sqrt_Integer {Tl} : ∀ (t : ArithExpr Tl Integer)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
(0 ≤ evalRounded t lM md)%Z →
eqExprTypeFloat (evalFloat (Sqrt t) lC md) (evalRounded (Sqrt t) lM md).
Lemma equivPrim_Sqrt_Integer {Tl} : ∀ (t : ArithExpr Tl Integer)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
(0 ≤ evalRounded t lM mode_NE)%Z →
eqExprTypePrim (evalPrim (Sqrt t) lP) (evalRounded (Sqrt t) lM mode_NE).
Lemma equivFloat_Sqrt_BinFloat {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
0 ≤ evalRounded t lM md →
eqExprTypeFloat (evalFloat (Sqrt t) lC md) (evalRounded (Sqrt t) lM md).
Lemma equivPrim_Sqrt_BinFloat {Tl} : ∀ (t : ArithExpr Tl BinFloat)
(lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
0 ≤ evalRounded t lM mode_NE →
eqExprTypePrim (evalPrim (Sqrt t) lP) (evalRounded (Sqrt t) lM mode_NE).
Lemma equivFloat_ArrayAcc {Tl} : ∀ (t : ArithExpr Tl Integer) a
(lC : evalExprTypeFloat_list Tl) md,
finite_array a = true → let lM := C2M_list lC in
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) →
(0 ≤ evalRounded t lM md < Uint63.to_Z (PArray.length a))%Z →
eqExprTypeFloat (evalFloat (ArrayAcc a t) lC md) (evalRounded (ArrayAcc a t) lM md).
Lemma equivPrim_ArrayAcc {Tl} : ∀ (t : ArithExpr Tl Integer) a
(lP : evalExprTypePrim_list Tl),
finite_array a = true → let lM := P2M_list lP in
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) →
(0 ≤ evalRounded t lM mode_NE < Uint63.to_Z (PArray.length a))%Z →
eqExprTypePrim (evalPrim (ArrayAcc a t) lP) (evalRounded (ArrayAcc a t) lM mode_NE).
Theorem equivFloat {Tl T} :
∀ (t: ArithExpr Tl T) (lC : evalExprTypeFloat_list Tl) md,
convertibleFloat_list lC → let lM := C2M_list lC in
wellBehaved t lM md → wellFormed t = true →
eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md).
Theorem equivPrim {Tl T} :
∀ (t: ArithExpr Tl T) (lP : evalExprTypePrim_list Tl),
convertiblePrim_list lP → let lM := P2M_list lP in
wellBehaved t lM mode_NE → wellFormed t = true →
eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE).