exprd: THEORY
BEGIN
	IMPORTING pack_stage


	%%% Attention; here, the old sign (orig_sign) comes into play
	%%% for mult/div, it is sa XOR sb
	%%% for add/sub it is the sign of the exact sum a+-b;
	%%%    this is correct, since rd a-b = 0 IFF a=b (which is proved in unpack_add)
	%%%		which is handled as special case

	exprd(inp: pack_stage_out_t): [# out: fpu_out_t, adj: adjexp_stage_out_t #] =
		LET xmax_s = inp`orig_s o fill[7](TRUE) o fill[1](FALSE) o fill[23](TRUE),
			xmax_d = inp`orig_s o fill[10](TRUE) o fill[1](FALSE) o fill[52](TRUE),
			inf_s = inp`orig_s o fill[8](TRUE) o fill[23](FALSE),
			inf_d = inp`orig_s o fill[11](TRUE) o fill[52](FALSE),
			xmax = mux_impl[64](xmax_s o fill[32](TRUE), xmax_d, inp`dbr),
			inf = mux_impl[64](inf_s o fill[32](FALSE), inf_d, inp`dbr),
			infdes = (inp`RM(0) AND NOT inp`RM(1)) OR
					 (inp`RM(1) AND NOT (inp`orig_s XOR inp`RM(0))),
			ovfres = mux_impl[64](xmax, inf, infdes),
			finres = fill[1](inp`orig_s) o inp`result^(62,0),
					 %% ^-- here it happens; this isn't very beautiful,
					 %% but it facilitates the proofs of the above stages
			res_ = mux_impl[64](finres, ovfres, inp`OVF AND NOT inp`OVFen)
		IN
		(# out := (# result := res_,
		 		     exceptions := (# OVF:=inp`OVF, UNF:=inp`UNF, INX:=inp`INX, 
									DIVZ:=FALSE, INV:=FALSE, UNIMPL:=FALSE #),
					 double := inp`dbr #),
		   adj := inp`adj #);

	exprd_sign: LEMMA FORALL(inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out 
	  IN res`result(63) = inp`s;
	         
	exprd_sgl: LEMMA FORALL(s: bit):
		LET xmax_s = s o fill[7](TRUE) o fill[1](FALSE) o fill[23](TRUE) o fill[32](TRUE),
			inf_s = s o fill[8](TRUE) o fill[23](FALSE) o fill[32](FALSE) IN
		inf?(bv2ieee_bv[8,24](inf_s))
		AND value[8](ieeebv2fact(bv2ieee_bv[8,24](xmax_s))) = sign[8](s) * Xmax[8,24];
		
	exprd_dbl: LEMMA FORALL(s: bit):
		LET xmax_d = s o fill[10](TRUE) o fill[1](FALSE) o fill[52](TRUE),
			inf_d = s o fill[11](TRUE) o fill[52](FALSE) IN
		inf?(bv2ieee_bv[11,53](inf_d))
		AND value[11](ieeebv2fact(bv2ieee_bv[11,53](xmax_d))) = sign[11](s) * Xmax[11,53];


	%%%%%%%%%%%%%
	%%%%%% OVF & /OVFen
	%%%%%%%%%%%%%

	exprd_unmasked_ovf_sgl: LEMMA FORALL(x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out
	  IN
		  rounder_prerequesites(x, inp, 8, 24) AND
		  OVF[8,24](x, RM2mode(inp`RM)) AND NOT inp`OVFen IMPLIES
		IF (RM2mode(inp`RM)=to_nearest OR
		    RM2mode(inp`RM)=to_pos AND x>=0 OR
			RM2mode(inp`RM)=to_neg AND x<0)
		THEN
		 %% Case Infinity
			IF x>=0 THEN p_inf?[8,24](bv2ieee_bv[8,24](res`result))
					ELSE n_inf?[8,24](bv2ieee_bv[8,24](res`result)) 
			ENDIF
		ELSE
		 %% Case Xmax
			IF x>0 THEN value[8](ieeebv2fact(bv2ieee_bv[8,24](res`result))) = Xmax[8,24]
				   ELSE value[8](ieeebv2fact(bv2ieee_bv[8,24](res`result))) = -Xmax[8,24]
			ENDIF
		ENDIF;



	exprd_unmasked_ovf_dbl: LEMMA FORALL(x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out
	  IN
		  rounder_prerequesites(x, inp, 11, 53) AND
		  OVF[11,53](x, RM2mode(inp`RM)) AND NOT inp`OVFen IMPLIES
		IF (RM2mode(inp`RM)=to_nearest OR
		    RM2mode(inp`RM)=to_pos AND x>=0 OR
			RM2mode(inp`RM)=to_neg AND x<0)
		THEN
		 %% Case Infinity
			IF x>=0 THEN p_inf?[11,53](bv2ieee_bv[11,53](res`result))
					ELSE n_inf?[11,53](bv2ieee_bv[11,53](res`result)) 
			ENDIF
		ELSE
		 %% Case Xmax
			IF x>0 THEN value[11](ieeebv2fact(bv2ieee_bv[11,53](res`result))) = Xmax[11,53]
				   ELSE value[11](ieeebv2fact(bv2ieee_bv[11,53](res`result))) = -Xmax[11,53]
			ENDIF
		ENDIF;


	%%%%%%%%%%%%%
	%%%%%% / (OVF & /OVFen)
	%%%%%%%%%%%%%
		%%% Here we have to prove, that the change of the sign in circuit
		%%% exprd does no harm

	exprd_val_sgl: LEMMA FORALL(x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out
	  IN
		  rounder_prerequesites(x, inp, 8, 24) AND
		  NOT (OVF[8,24](x, RM2mode(inp`RM)) AND NOT inp`OVFen) IMPLIES
			value[8](ieeebv2fact(bv2ieee_bv[8,24](res`result))) =
				rd_result[8, 24](x, RM2mode(inp`RM), inp`OVFen, inp`UNFen);


	exprd_val_dbl: LEMMA FORALL(x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out
	  IN
		  rounder_prerequesites(x, inp, 11, 53) AND
		  NOT (OVF[11,53](x, RM2mode(inp`RM)) AND NOT inp`OVFen) IMPLIES
			value[11](ieeebv2fact(bv2ieee_bv[11,53](res`result))) =
				rd_result[11,53](x, RM2mode(inp`RM), inp`OVFen, inp`UNFen);

	exprd_correct_sgl: LEMMA  FORALL(x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out
	  IN
		  rounder_prerequesites(x, inp, 8, 24) IMPLIES
		  result_correct(res`result, res`exceptions`OVF, res`exceptions`UNF, res`exceptions`INX)
						(RM2mode(inp`RM), inp`OVFen, inp`UNFen, inp`dbr)
						(x);

	exprd_correct_dbl: LEMMA  FORALL(x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          res = exprd(pack_stage(adjexp_stage(postnorm)))`out
	  IN
		  rounder_prerequesites(x, inp, 11, 53) IMPLIES
		  result_correct(res`result, res`exceptions`OVF, res`exceptions`UNF, res`exceptions`INX)
						(RM2mode(inp`RM), inp`OVFen, inp`UNFen, inp`dbr)
						(x);

END exprd