%% in Anlehung an P.S. Miner, NASA LARC round_frac[N: above(1), P:posnat]: THEORY BEGIN IMPORTING eta_props[N], fin_precision[N,P] mode: VAR rounding_mode; x: VAR real; prec: VAR nat; %%%% Rounding of infinitely precise reals to fractions %%%% with p fractional binary digits rd_to_pos(x): int = ceiling(x); rd_to_neg(x): int = floor(x); rd_to_zero(x): int = IF (x>=0) THEN floor(x) ELSE ceiling(x) ENDIF; rd_to_nearest(x): int = IF x-floor(x) < ceiling(x)-x THEN floor(x) ELSIF ceiling(x)-x < x-floor(x) THEN ceiling(x) ELSIF ceiling(x) = floor(x) THEN x ELSE 2*floor(ceiling(x)/2) ENDIF; rd_to_nearest_neg: LEMMA rd_to_nearest(x) = -rd_to_nearest(-x); round_frac(x, mode, prec): real = 2^-prec * CASES mode OF to_nearest: rd_to_nearest(x * 2^prec), to_neg: rd_to_neg(x * 2^prec), to_pos: rd_to_pos(x * 2^prec), to_zero: rd_to_zero(x * 2^prec) ENDCASES; round_to_even1: LEMMA abs(x - round_frac(x, to_nearest, 0)) <= 1/2; round_to_even2: LEMMA abs(x - round_frac(x, to_nearest, prec)) <= 2^(-1 + -prec); round_to_even3_l1: LEMMA abs(x - round_frac(x, to_nearest, 0)) = 1/2 IMPLIES integer?(round_frac(x, to_nearest, 0)/2); round_to_even3: LEMMA abs(x - round_frac(x, to_nearest, 0)) = 1/2 IMPLIES even?(round_frac(x, to_nearest, 0)); round_l0: LEMMA round_frac(0, mode, prec) = 0; round_l1: LEMMA abs( x - round_frac(x, mode, 0) ) < 1; round_l2: LEMMA abs( x - round_frac(x, mode, prec) ) < 2^-prec; %%%% Rounding of infinitely precise reals to reals with p %%%% signifcant binary digits. %%%% Example: for a real of magnitude 2^1000 with 30 significant %%%% digits, only the digits 1000-970 are of interest. round(x:real, mode:rounding_mode, prec:upfrom(1)): real = LET y=eta(x) IN 2^y`e * round_frac(x/2^y`e, mode, prec-1); round_even_distance: LEMMA FORALL (x: real, mode: rounding_mode, prec: upfrom(1)): abs(x - round(x, to_nearest, prec)) <= 2 ^ (eta(x)`e - prec); round_even_tie: LEMMA FORALL (x: real, mode: rounding_mode, prec: upfrom(1)): abs(x - round(x, to_nearest, prec)) = 2 ^ (eta(x)`e - prec) IMPLIES integer?(round(x, to_nearest, prec) * 1 / 4 * 2 ^ -(eta(x)`e - prec)); round_pos_neg_refl: LEMMA FORALL (x: real, prec: upfrom(1)): round(x, to_pos, prec) = -round(-x, to_neg, prec); round_pos_neg_refl2: LEMMA FORALL (x: real, prec: upfrom(1)): round(-x, to_pos, prec) = -round(x, to_neg, prec); round_neg_pos_refl: LEMMA FORALL (x: real, prec: upfrom(1)): round(-x, to_neg, prec) = -round(x, to_pos, prec); round_pos_neg_zero: LEMMA FORALL (x: real, prec: upfrom(1)): round(x, to_zero, prec) = IF x >= 0 THEN round(x, to_neg, prec) ELSE round(x, to_pos, prec) ENDIF; round_nearest_neg: LEMMA FORALL (x: real, prec: upfrom(1)): round(x, to_nearest, prec) = -round(-x, to_nearest, prec); round_nearest_refl: LEMMA FORALL (x: real, prec: upfrom(1)): round(-x, to_nearest, prec) = -round(x, to_nearest, prec); round_sign: LEMMA FORALL (x: real, mode: rounding_mode, prec: upfrom(1)): (x <= 0 IMPLIES round(x, mode, prec) <= 0) AND (x >= 0 IMPLIES round(x, mode, prec) >= 0); round_0: LEMMA FORALL (mode: rounding_mode, prec: upfrom(1)): round(0, mode, prec) = 0; round_zero_neg: LEMMA FORALL (x: real, prec: upfrom(1)): round(x, to_zero, prec) = -round(-x, to_zero, prec); round_zero_refl: LEMMA FORALL (x: real, prec: upfrom(1)): round(-x, to_zero, prec) = -round(x, to_zero, prec); END round_frac round_decomposition[N: above(1), P: posnat]: THEORY BEGIN IMPORTING round_frac[N,P]%, ieee_import mode: VAR rounding_mode; prec: VAR upfrom(1); sigrd_TCC_lem: LEMMA FORALL (y: (ii_i3e_number?[N]), mode, prec): 0 <= abs(round[N, P](value[N](y), mode, prec)) / 2 ^ y`e AND abs(round[N, P](value[N](y), mode, prec)) / 2 ^ y`e <= 2; sigrd(y: (ii_i3e_number?), mode, prec): { x: real | 0<=x and x<=2 } = abs(round(value(y), mode, prec))/2^y`e; sigrd_rewr: LEMMA FORALL (y: (ii_i3e_number?)): sigrd(y, mode, prec) = abs(round_frac(sign(y`s) * y`f, mode, prec-1)); sigrd_lem1: LEMMA FORALL (y: (ii_i3e_number?)): f_normal?(y) IMPLIES sigrd(y, mode, prec) >= 1; sigrd_lem2: LEMMA FORALL (y: (ii_i3e_number?), prec: upfrom(2)): y`f < 1 IMPLIES sigrd(y, mode, prec) <= 1; postnorm_TCC_lem: LEMMA FORALL (y: (ii_i3e_number?[N]), prec: subrange(1,P)): if_i3e_number?[N, P](IF sigrd(y, mode, prec) = 2 THEN (# s := y`s, e := y`e + 1, f := 1 #) ELSE (# s := IF sigrd(y,mode,prec)=0 THEN 0 ELSE y`s ENDIF, e := y`e, f := sigrd(y, mode, prec) #) ENDIF); %%%%%%% CAUTION: the parameter prec for the postnorm-function is here %%%%%%% only for historical reasons. It has *no* meaning. %%%%%%% The postnorm-function is only used with prec=P. postnorm(y: (ii_i3e_number?), mode: rounding_mode, prec: subrange(1,P)): (if_i3e_number?[N,P]) = LET f1=sigrd(y, mode, prec) IN IF f1=2 THEN (# s:=y`s, e:=y`e+1, f:=1 #) ELSE (# s:=IF f1=0 THEN 0 ELSE y`s ENDIF, e:=y`e, f:=f1 #) ENDIF; ii_postnorm_typ: LEMMA FORALL(x: real, prec: subrange(1,P)): if_i3e_number?[N,P](postnorm(eta(x), mode, prec)); ii_postnorm_val: LEMMA FORALL(x: real, prec: subrange(1,P)): value(postnorm(eta(x), mode, prec)) = round(x, mode, prec); ii_round_decomposition_p: THEOREM forall (x: real, prec: subrange(1,P)): eta(round(x, mode, prec)) = postnorm(eta(x), mode, prec); ii_round_decomposition: THEOREM forall (x: real): eta(round(x, mode, P)) = postnorm(eta(x), mode, P); eta_e_round: THEOREM FORALL (x: real): eta(round(x, mode, P))`e >= eta(x)`e; END round_decomposition round_correct[N: above(1), P: posnat]: THEORY BEGIN IMPORTING round_decomposition[N,P] mode: VAR rounding_mode; %%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%% We first show, that the result of the %%%%%%%%%%%%%%%%%%% rounding function is ieee-representable round_is_representable: LEMMA FORALL (x: real): if_i3e_number?[N,P](eta(round(x, mode,P))); %%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%% Next we show, that the four rounding-modes %%%%%%%%%%%%%%%%%%% work as defined in the standard round_pos_correct_l1: LEMMA FORALL (x:real, y: (if_i3e_number?[N,P])): (value(y)>=x IMPLIES value(y) >= round(x, to_pos, P)); %%% this is nearly equivalent to round(x, to_pos) = %%% min (y | y representable and y >= x) round_pos_correct: LEMMA FORALL (x:real, y: (if_i3e_number?[N,P])): round(x, to_pos, P) >= x AND (value(y)>=x IMPLIES abs(x-value(y)) >= abs(x-round(x, to_pos, P))); round_neg_correct: LEMMA FORALL (x:real, y: (if_i3e_number?[N,P])): round(x, to_neg, P) <= x AND (value(y)<=x IMPLIES abs(x-value(y)) >= abs(x-round(x, to_neg, P))); %%% this is equivalent to round(x, to_pos) = %%% max (y | y representable and y <= x) round_zero_correct: LEMMA FORALL (x:real, y: (if_i3e_number?[N,P])): abs(round(x, to_zero, P)) <= abs(x) AND (abs(value(y)) <= abs(x) IMPLIES abs(x - value(y)) >= abs(x - round(x, to_zero, P))); %%% this is equivalent to round(x, to_zero) = (STANDARD) round_nearest_correct: LEMMA FORALL (x:real, y: (if_i3e_number?[N,P])): abs(x - value(y)) >= abs(x - round(x, to_nearest, P)); round_nearest_correct_tie: LEMMA FORALL (x: real, y: (if_i3e_number?[N, P])): P>1 AND value(y) /= round(x, to_nearest, P) AND abs(x - value(y)) = abs(x - round(x, to_nearest, P)) IMPLIES integer?(eta(round(x, to_nearest, P))`f * 2 ^ (P - 1) / 2); %%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%% Last but not least, we show, that the representable numbers %%%%%%%%%%%%%%%%%%% are exactly the fixpoints of the rounding function round_fix: LEMMA FORALL (x: real): if_i3e_number?[N,P](eta(x)) IFF round(x, mode, P)=x; END round_correct