Skip to content

GitLab

why3
why3
Commit 9a94aeb8 authored by Clément Fumex's avatar Clément Fumex
Browse files
Options

+ remove a few wrong axioms 

+ simplify some others
+ add a realization of real.Truncate
+ add a, almost complete, realization (missing fma related axioms + some non-axiomatized definitions)
parent 05dc4e02
Hide whitespace changes
Inline Side-by-side
Showing with 4737 additions and 45 deletions
Makefile.in
View file @ 9a94aeb8
......@@ -890,7 +890,7 @@ COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
COQLIBS_BOOL_FILES = Bool
COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry Truncate
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
......@@ -914,13 +914,16 @@ COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES))
COQLIBS_BV_FILES = Pow2int BV_Gen
COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
COQLIBS_IEEEFLOAT_FILES = GenericFloat
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV)
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT)
drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@'
......@@ -947,6 +950,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory seq.'"$$f"' meta "realized_theory" "seq.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_BV_FILES); do \
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_IEEEFLOAT_FILES); do \
echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -974,12 +979,14 @@ install_no_local::
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_SEQ)) $(LIBDIR)/why3/coq/seq/
$(MKDIR_P) $(LIBDIR)/why3/coq/bv
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_BV)) $(LIBDIR)/why3/coq/bv/
$(MKDIR_P) $(LIBDIR)/why3/coq/ieee_float
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
ifeq (@enable_coq_fp_libs@,yes)
$(MKDIR_P) $(LIBDIR)/why3/coq/floating_point
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv headers-coq
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float headers-coq
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
......@@ -1011,6 +1018,9 @@ update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theorie
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o lib/coq/bv/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o lib/coq/ieee_float/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
......
lib/coq/ieee_float/GenericFloat.v 0 → 100644
View file @ 9a94aeb8
This source diff could not be displayed because it is too large. You can view the blob instead.
lib/coq/real/Truncate.v 0 → 100644
View file @ 9a94aeb8
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.FromInt.
Require Import Flocq.Core.Fcore.
Require Import Fourier.
(* Why3 goal *)
Notation truncate := Ztrunc.
(* Why3 goal *)
Lemma Truncate_int : forall (i:Z), ((truncate (Reals.Raxioms.IZR i)) = i).
intro i.
rewrite <-Z2R_IZR.
apply Ztrunc_Z2R.
Qed.
(* Why3 goal *)
Lemma Truncate_down_pos : forall (x:R), (0%R <= x)%R ->
(((Reals.Raxioms.IZR (truncate x)) <= x)%R /\
(x < (Reals.Raxioms.IZR ((truncate x) + 1%Z)%Z))%R).
intros x h.
rewrite (Ztrunc_floor x h), <-Z2R_IZR, <-Z2R_IZR.
split.
apply Zfloor_lb.
rewrite Z2R_plus; simpl.
apply Zfloor_ub.
Qed.
(* Why3 goal *)
Lemma Truncate_up_neg : forall (x:R), (x <= 0%R)%R ->
(((Reals.Raxioms.IZR ((truncate x) - 1%Z)%Z) < x)%R /\
(x <= (Reals.Raxioms.IZR (truncate x)))%R).
intros x h.
rewrite (Ztrunc_ceil x h), <-Z2R_IZR, <-Z2R_IZR.
split;[|apply Zceil_ub].
case (Req_dec (Z2R (Zfloor x)) x); intro.
rewrite <-H, Zceil_Z2R, H, Z2R_minus; simpl.
fourier.
rewrite (Zceil_floor_neq _ H).
rewrite Z2R_minus, Z2R_plus; simpl.
pose proof (Zfloor_lb x).
destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
fourier.
Qed.
(* Why3 goal *)
Lemma Real_of_truncate : forall (x:R),
((x - 1%R)%R <= (Reals.Raxioms.IZR (truncate x)))%R /\
((Reals.Raxioms.IZR (truncate x)) <= (x + 1%R)%R)%R.
intro x.
rewrite <-Z2R_IZR.
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
destruct (Req_dec (Z2R (Zfloor x)) x).
rewrite <-H at 2 3; rewrite Zceil_Z2R, H; split; fourier.
rewrite Zceil_floor_neq; auto.
pose proof (Zfloor_lb x);
pose proof (Zfloor_ub x).
rewrite Z2R_plus; simpl Z2R; split; fourier.
+ rewrite Ztrunc_floor by fourier.
pose proof (Zfloor_lb x);
pose proof (Zfloor_ub x).
split; fourier.
Qed.
(* Why3 goal *)
Lemma Truncate_monotonic : forall (x:R) (y:R), (x <= y)%R ->
((truncate x) <= (truncate y))%Z.
apply Ztrunc_le.
Qed.
(* Why3 goal *)
Lemma Truncate_monotonic_int1 : forall (x:R) (i:Z),
(x <= (Reals.Raxioms.IZR i))%R -> ((truncate x) <= i)%Z.
intros x i h.
rewrite <-Z2R_IZR in h.
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
apply Zceil_glb; assumption.
+ rewrite Ztrunc_floor by fourier.
apply le_Z2R.
apply Rle_trans with (r2:=x);[apply Zfloor_lb|assumption].
Qed.
(* Why3 goal *)
Lemma Truncate_monotonic_int2 : forall (x:R) (i:Z),
((Reals.Raxioms.IZR i) <= x)%R -> (i <= (truncate x))%Z.
intros x i h.
rewrite <-Z2R_IZR in h.
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
apply le_Z2R.
apply Rle_trans with (r2:=x);[assumption|apply Zceil_ub].
+ rewrite Ztrunc_floor by fourier.
apply Zfloor_lub; assumption.
Qed.
(* Why3 goal *)
Notation floor := Zfloor.
(* Why3 goal *)
Notation ceil := Zceil.
(* Why3 goal *)
Lemma Floor_int : forall (i:Z), ((floor (Reals.Raxioms.IZR i)) = i).
intro i; rewrite <-Z2R_IZR.
apply Zfloor_Z2R.
Qed.
(* Why3 goal *)
Lemma Ceil_int : forall (i:Z), ((ceil (Reals.Raxioms.IZR i)) = i).
intro i; rewrite <-Z2R_IZR.
apply Zceil_Z2R.
Qed.
(* Why3 goal *)
Lemma Floor_down : forall (x:R), ((Reals.Raxioms.IZR (floor x)) <= x)%R /\
(x < (Reals.Raxioms.IZR ((floor x) + 1%Z)%Z))%R.
intro x.
rewrite <-Z2R_IZR, <-Z2R_IZR; split.
apply Zfloor_lb.
rewrite Z2R_plus.
apply Zfloor_ub.
Qed.
Lemma ceil_lb: forall x, ((Z2R (ceil x) - 1) < x).
intro.
case (Req_dec (Z2R (Zfloor x)) x); intro.
rewrite <-H, Zceil_Z2R, H; simpl; fourier.
rewrite (Zceil_floor_neq _ H).
rewrite Z2R_plus; simpl.
pose proof (Zfloor_lb x).
destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
fourier.
Qed.
(* Why3 goal *)
Lemma Ceil_up : forall (x:R),
((Reals.Raxioms.IZR ((ceil x) - 1%Z)%Z) < x)%R /\
(x <= (Reals.Raxioms.IZR (ceil x)))%R.
intro x.
rewrite <-Z2R_IZR, <-Z2R_IZR; split; [|apply Zceil_ub].
rewrite Z2R_minus.
apply ceil_lb.
Qed.
(* Why3 goal *)
Lemma Floor_monotonic : forall (x:R) (y:R), (x <= y)%R ->
((floor x) <= (floor y))%Z.
apply Zfloor_le.
Qed.
(* Why3 goal *)
Lemma Ceil_monotonic : forall (x:R) (y:R), (x <= y)%R ->
((ceil x) <= (ceil y))%Z.
apply Zceil_le.
Qed.
theories/ieee_float.why
View file @ 9a94aeb8
......@@ -648,14 +648,6 @@ theory GenericFloat
lemma Max_r : forall x y:t. y .<= x -> (max x y) .= x
lemma Max_l : forall x y:t. x .<= y -> (max x y) .= y
(* FS: wrong for 0 and -0. Using eq instead makes them wrong for NaN and *)
(* NaN *)
(* lemma Min_comm : forall x y:t. min x y = min y x *)
(* lemma Max_comm : forall x y:t. max x y = max y x *)
lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z)
lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)
(* _____________ *)
use real.Truncate
......@@ -678,7 +670,7 @@ theory GenericFloat
(** big floats are ints *)
axiom big_float_is_int: forall m i.
is_finite i ->
(i .<= (of_int m (- max_representable_integer)) \/
(i .<= neg (of_int m max_representable_integer) \/
(of_int m max_representable_integer) .<= i) ->
is_int i
......@@ -706,12 +698,12 @@ theory GenericFloat
axiom ceil_lest: forall x y:t. x .<= y /\ is_int y -> (roundToIntegral RTP x) .<= y
axiom ceil_to_real: forall m:mode, x:t.
(.- (of_int m max_representable_integer)) .<= x .<= (of_int m max_representable_integer) ->
axiom ceil_to_real: forall x:t.
is_finite x ->
to_real (roundToIntegral RTP x) = FromInt.from_int (Truncate.ceil (to_real x))
axiom ceil_to_int: forall m:mode, x:t.
(.- (of_int m max_representable_integer)) .<= x .<= (of_int m max_representable_integer) ->
is_finite x ->
to_int m (roundToIntegral RTP x) = Truncate.ceil (to_real x)
(** floor *)
......@@ -720,12 +712,12 @@ theory GenericFloat
axiom floor_lest: forall x y:t. y .<= x /\ is_int y -> y .<= (roundToIntegral RTN x)
axiom floor_to_real: forall m:mode, x:t.
(.- (of_int m max_representable_integer)) .<= x .<= (of_int m max_representable_integer) ->
axiom floor_to_real: forall x:t.
is_finite x ->
to_real (roundToIntegral RTN x) = FromInt.from_int (Truncate.floor (to_real x))
axiom floor_to_int: forall m:mode, x:t.
(.- (of_int m max_representable_integer)) .<= x .<= (of_int m max_representable_integer) ->
is_finite x ->
to_int m (roundToIntegral RTN x) = Truncate.floor (to_real x)
(* Rna *)
......@@ -746,14 +738,6 @@ theory GenericFloat
forall x:t. ((roundToIntegral RTP x) .- x) .= (x .- (roundToIntegral RTN x)) ->
is_positive x -> roundToIntegral RNA x = roundToIntegral RTP x
axiom RNA_near_int:
forall i x:t. is_int i -> (.- half) .< x .< half ->
roundToIntegral RNA (i .+ x) = i
(* axiom rna_to_real: forall x:t. *)
(* is_finite x -> *)
(* to_real (roundToIntegralTiesToAway x) = FromInt.from_int (to_int x) *)
(* to_int *)
axiom to_int_roundToIntegral: forall m:mode, x:t.
to_int m x = to_int m (roundToIntegral m x)
......@@ -761,14 +745,6 @@ theory GenericFloat
axiom to_int_monotonic: forall m:mode, x y:t.
is_finite x -> is_finite y -> le x y -> to_int m x <= to_int m y
axiom to_int_monotonic_int1:
forall m:mode, x:t, i:int. is_finite x ->
lt x (of_int m i) -> to_int m x <= i
axiom to_int_monotonic_int2:
forall m:mode, x:t, i:int. is_finite x ->
lt (of_int m i) x -> i <= to_int m x
axiom to_int_of_int: forall m:mode, i:int.
(- max_representable_integer) <= i <= max_representable_integer ->
to_int m (of_int m i) = i
......@@ -838,12 +814,9 @@ end
theory Float32
use int.Int
use import real.Real
(* use bv.BV32 *)
type t
(* function from_bv BV32.t : t *)
constant max_representable_integer : int = 16777216
constant max_real : real = 0x1.FFFFFEp127
......@@ -852,8 +825,6 @@ theory Float32
constant max_real = max_real,
constant max_representable_integer = max_representable_integer
(* axiom half_bv: half = from_bv (BV32.of_uint 0x3F00_0000) *)
lemma round_bound_ne :
forall x:real [round RNE x].
x - 0x1p-24 * Abs.abs(x) - 0x1p-150 <= round RNE x <= x + 0x1p-24 * Abs.abs(x) + 0x1p-150
......@@ -864,15 +835,11 @@ theory Float32
end
theory Float64
use bv.BV64
use int.Int
use real.FromInt
use import real.Real
type t
(* function from_bv BV64.t : t *)
constant max_representable_integer : int = 9007199254740992
constant max_real : real = 0x1.FFFFFFFFFFFFFp1023
......@@ -881,8 +848,6 @@ theory Float64
constant max_real = max_real,
constant max_representable_integer = max_representable_integer
(* axiom half_bv: half = from_bv (BV64.of_uint 0x3FE0_0000_0000_0000) *)
lemma round_bound_ne :
forall x:real [round RNE x].
x - 0x1p-53 * Abs.abs(x) - 0x1p-1075 <= round RNE x <= x + 0x1p-53 * Abs.abs(x) + 0x1p-1075
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment