fp_rd2int: THEORY
BEGIN

	IMPORTING fp_misc_import


	%%%%%%%%%%%%%%%%%%%%%%%%
	%%%%%%%%%%%%%%%%%%%%%%%% Round small values (e<0)
	%%%%%%%%%%%%%%%%%%%%%%%% this is only needed for rd2int in fp_fmt
	rd2int_small_impl(s: bit, e: bvec[11], f: bvec[53], RM: bvec[2], dbl: bit): bvec[64] = 
			LET E_eq_min1 = equal_impl[11](e, fill[11](TRUE)),
				f_eq_1	  = f(52) AND zero_impl[52](f^(51,0)),
				RD2ONE = (NOT RM(0) AND RM(1) AND NOT s) OR %% to_pos and x's=pos
						 (RM(0) AND RM(1) AND s) OR         %% to_neg and x`s=neg
						 (RM(0) AND NOT RM(1) AND E_eq_min1 AND NOT f_eq_1) 
															%% mode = to_nearest AND x`e=-1 AND x`f/=1
			IN
			IF RD2ONE THEN
				IF NOT dbl THEN
					fill[1](s) o fill[1](FALSE) o fill[7](TRUE) o fill[23](FALSE) o fill[32](FALSE)
				ELSE
					fill[1](s) o fill[1](FALSE) o fill[10](TRUE) o fill[52](FALSE)
				ENDIF
			ELSE %% rd 2 zero
					fill[64](FALSE)
					%%% here we use the same ugly trick as in rounding; we tie the sign of zero
					%%% to pos; this is corrected before delivering the result to the cpu
			ENDIF;


	rd2int_small_tcc1: LEMMA FORALL(s: bool):
		ieee_number?[8, 24](Sbv2ieee_bv(fill[1](s) o fill[1](FALSE) o fill[7](TRUE) o
                        fill[23](FALSE) o fill[32](FALSE)));
	rd2int_small_tcc2: LEMMA FORALL(s: bool):
		ieee_number?[8, 24](Sbv2ieee_bv(fill[64](FALSE)));
	rd2int_small_tcc3: LEMMA FORALL(s: bool):
		ieee_number?[11,53](Dbv2ieee_bv(fill[1](s) o fill[1](FALSE) o fill[10](TRUE) o fill[52](FALSE)));
	rd2int_small_tcc4: LEMMA FORALL(s: bool):
		ieee_number?[11,53](Dbv2ieee_bv(fill[64](FALSE)));

	rd2int_small_sgl: LEMMA FORALL (s: bit, e: bvec[11], f: bvec[53], RM: bvec[2], 
							  X: (ff_i3e_number?[8,24])):
			X=(# s:=b2n(s), e:=bv2int(e), f:=bv2nat(f)*2^-52 #) AND nonzero?[8](X) AND X`e<0
		IMPLIES 
			LET R=rd2int_small_impl(s,e,f,RM,FALSE) IN
			rd2int[8,24](X, RM2mode(RM)) = Sieeebv2fact(Sbv2ieee_bv(R));

	rd2int_small_dbl: LEMMA FORALL (s: bit, e: bvec[11], f: bvec[53], RM: bvec[2], 
							  X: (ff_i3e_number?[11,53])):
			X=(# s:=b2n(s), e:=bv2int(e), f:=bv2nat(f)*2^-52 #) AND nonzero?[11](X) AND X`e<0
		IMPLIES 
			LET R=rd2int_small_impl(s,e,f,RM,TRUE) IN
			rd2int[11,53](X, RM2mode(RM)) = Dieeebv2fact(Dbv2ieee_bv(R));


	%%%%%%%%%%%%%%%%%%%%%%%%
	%%%%%%%%%%%%%%%%%%%%%%%% Round small values (e<0) to integer format
	%%%%%%%%%%%%%%%%%%%%%%%% this is only needed for rd2int in int_fmt
	rd2int_small_int_impl(s: bit, e: bvec[11], f: bvec[53], RM: bvec[2]): bvec[32] =
			LET E_eq_min1 = equal_impl[11](e, fill[11](TRUE)),
				f_zero    = zero_impl[52](f^(51,0)),
				f_eq_1	  = f(52) AND f_zero,
				f_eq_0	  = NOT f(52) AND f_zero,
				RD2ONE = (NOT RM(0) AND RM(1) AND NOT s) OR %% to_pos and x's=pos
						 (RM(0) AND RM(1) AND s) OR         %% to_neg and x`s=neg
						 (RM(0) AND NOT RM(1) AND E_eq_min1 AND NOT f_eq_1) 
															%% mode = to_nearest AND x`e=-1 AND x`f/=1
			IN
			IF RD2ONE AND NOT f_eq_0 THEN
				fill[31](s) o fill[1](TRUE)
			ELSE
				fill[32](FALSE)
			ENDIF;

	rd2int_small_int_sgl: LEMMA FORALL (s: bit, e: bvec[11], f: bvec[53], RM: bvec[2], 
							  X: (ff_i3e_number?[8,24])):
			X=(# s:=b2n(s), e:=bv2int(e), f:=bv2nat(f)*2^-52 #) AND X`e<0
		IMPLIES 
			value[8](rd2int[8,24](X, RM2mode(RM))) = bv2int(rd2int_small_int_impl(s,e,f,RM));

	rd2int_small_int_dbl: LEMMA FORALL (s: bit, e: bvec[11], f: bvec[53], RM: bvec[2], 
							  X: (ff_i3e_number?[11,53])):
			X=(# s:=b2n(s), e:=bv2int(e), f:=bv2nat(f)*2^-52 #) AND X`e<0
		IMPLIES 
			value[11](rd2int[11,53](X, RM2mode(RM))) = bv2int(rd2int_small_int_impl(s,e,f,RM));

	%%%%%%%%%%%%%% Round medium values (0<=e<P-1); 
	%%%%%%%%%%%%%% this is were rd2int happens
	%%%%%%%%%%%%%% this stage is placed in front of rd_stg1
	rd2int_stg(e: bvec[11], dbl: bit): bvec[13] =
		LET C=IF dbl THEN int2bv[13](-1074) ELSE int2bv[13](-149) ENDIF IN
		add_impl[13](sext_impl[11,13](e), C, FALSE)`s;


	rd2int_stg_corr_sgl: LEMMA FORALL(e: bvec[11]): 
			bv2int(rd2int_stg(e, FALSE)) = bv2int(e) + emin[8]+1-24;
	rd2int_stg_corr_dbl: LEMMA FORALL(e: bvec[11]): 
			bv2int(rd2int_stg(e, TRUE)) = bv2int(e) + emin[11]+1-53;


	%%%%%%% Decide wether number is small, large or medium
	rd2int_range(e: bvec[11], dbl: bit): [# small, large: bool #] =
			LET CONST = IF dbl THEN int2bv[11](-52) ELSE int2bv[11](-23) ENDIF IN
			(# small := e(10),
			   large := NOT add_impl[11](e, CONST, FALSE)`neg #);

	rd2int_range_small: LEMMA FORALL(e: bvec[11], dbl: bit):
			rd2int_range(e,dbl)`small = (bv2int(e) < 0);
	rd2int_range_sgl: LEMMA FORALL(e: bvec[11]):
			rd2int_range(e,FALSE)`large = (bv2int(e) >= 24-1);
	rd2int_range_dbl: LEMMA FORALL(e: bvec[11]):
			rd2int_range(e,TRUE)`large = (bv2int(e) >= 53-1);


	%%%%%%% Extract 32-bit integer from f3 (output of adjust-exp)
	rd2int_extract(s: bit, f: bvec[53]): [# ovf: bit, i: bvec[32] #] =
		LET ovf1 = NOT zero_impl[21](f^(52,32)),
			f0   = fill[1](FALSE) o f^(31,0),
			fneg = neg_impl[33](f0),
			muxxed = IF s THEN fneg ELSE f0 ENDIF IN
		(# ovf := ovf1 OR (muxxed(32) XOR muxxed(31)),
		   i   := muxxed^(31,0) #);

	rd2int_extract_correct: LEMMA FORALL (s:bit, f: bvec[53]):
		LET I=bv2nat(f)*sign[8](b2n(s)),
			R=rd2int_extract(s,f) IN
		R`ovf = NOT in_rng_2s_comp[32](I) AND
		(in_rng_2s_comp[32](I) IMPLIES I=bv2int(R`i));


	%%%%%%%%%%%%%%%%
	%%%%%%%%%%%%%%%% The combinatorial rd2int_fmt function
	%%%%%%%%%%%%%%%%

	rd2int_fmt_comb(I: fpu_inp_t): fpu_out_t =
		LET dbl=is_CVTd2i(I`op),
			U=unpack_impl(dbl, FALSE, I`F1),
			US=spec_unpack_impl(U`s, U`einf, U`ez, U`fz, U`h(51)),
			RNG=rd2int_range(U`e, TRUE),
			SML=rd2int_small_int_impl(U`s, U`e, U`f, I`RM),
			MED=rd2int_stg(U`e, TRUE),
			RD=rd_stg2(rd_stg1((# sr:=U`s, er:=MED, fr:=fill[1](FALSE) o U`f o fill[3](FALSE), 
								  RM:=I`RM, double:=TRUE, mask:=fill[6](FALSE) #)))`adj,
			OUT=rd2int_extract(RD`s, RD`f3)
		IN
			(# result:=IF RNG`small THEN SML ELSE OUT`i ENDIF o fill[32](FALSE),
			   exceptions := (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE, UNIMPL:=FALSE,
								INV:=RNG`large OR (NOT RNG`large AND NOT RNG`small AND OUT`ovf) OR
									 US`INF OR US`QNAN OR US`SNAN #),
			   double := FALSE #);


	rd2int_sgl_dbl: LEMMA FORALL(x: (ii_i3e_number?[8]), mode: rounding_mode):
			0<=x`e AND x`e<52 IMPLIES
			LET X53=(# s:=x`s, e:=x`e, f:=x`f #)::(ii_i3e_number?[11]) IN
			value[8](rd2int[8,24](x, mode)) = value[11](rd2int[11,53](X53, mode));

	rd2int_fmt_correct_med_sgl: LEMMA FORALL(I: fpu_inp_t): 
			is_CVTs2i(I`op) AND Sieee_number?(Sbv2ieee_bv(I`F1)) 
		    IMPLIES LET x=Sieeebv2fact(Sbv2ieee_bv(I`F1)),
						RES=rd2int_fmt_comb(I),
						INT=value[8](rd2int[8,24](x, RM2mode(I`RM))) IN
			0<=x`e AND x`e<52 IMPLIES
				(RES`exceptions`INV = NOT in_rng_2s_comp[32](INT)) AND
				(in_rng_2s_comp[32](INT) IMPLIES bv2int(RES`result^(63,32)) = INT);

	rd2int_fmt_correct_med_dbl: LEMMA FORALL(I: fpu_inp_t): 
			is_CVTd2i(I`op) AND Dieee_number?(Dbv2ieee_bv(I`F1)) 
		    IMPLIES LET x=Dieeebv2fact(Dbv2ieee_bv(I`F1)),
						RES=rd2int_fmt_comb(I),
						INT=value[11](rd2int[11,53](x, RM2mode(I`RM))) IN
			0<=x`e AND x`e<52 IMPLIES
				(RES`exceptions`INV = NOT in_rng_2s_comp[32](INT)) AND
				(in_rng_2s_comp[32](INT) IMPLIES bv2int(RES`result^(63,32)) = INT);

	rd2int_fmt_correct_sgl: LEMMA FORALL(I: fpu_inp_t): 
			LET RES=rd2int_fmt_comb(I) IN
			is_CVTs2i(I`op) IMPLIES
				IF Sieee_number?(Sbv2ieee_bv(I`F1)) THEN
					 LET x=Sieeebv2fact(Sbv2ieee_bv(I`F1)),
 						 INT=value[8](rd2int[8,24](x, RM2mode(I`RM))) IN
					(RES`exceptions`INV = NOT in_rng_2s_comp[32](INT)) AND
					(in_rng_2s_comp[32](INT) IMPLIES bv2int(RES`result^(63,32)) = INT)
				ELSE
					RES`exceptions`INV	
				ENDIF
				AND NOT (RES`exceptions`OVF OR RES`exceptions`UNF OR RES`exceptions`INX OR
	   					 RES`exceptions`DIVZ OR RES`exceptions`UNIMPL);


	rd2int_fmt_correct_dbl: LEMMA FORALL(I: fpu_inp_t): 
			LET RES=rd2int_fmt_comb(I) IN
			is_CVTd2i(I`op) IMPLIES
				IF Dieee_number?(Dbv2ieee_bv(I`F1)) THEN
					 LET x=Dieeebv2fact(Dbv2ieee_bv(I`F1)),
 						 INT=value[11](rd2int[11,53](x, RM2mode(I`RM))) IN
					(RES`exceptions`INV = NOT in_rng_2s_comp[32](INT)) AND
					(in_rng_2s_comp[32](INT) IMPLIES bv2int(RES`result^(63,32)) = INT)
				ELSE
					RES`exceptions`INV	
				ENDIF
				AND NOT (RES`exceptions`OVF OR RES`exceptions`UNF OR RES`exceptions`INX OR
	   					 RES`exceptions`DIVZ OR RES`exceptions`UNIMPL);

END fp_rd2int