pack_stage: THEORY
 BEGIN

  IMPORTING adjexp_stage

  pack_stage_out_t: TYPE =
  [# result: bvec[64], 
     TINY: bit,
     OVF: bit,
     INX: bit,
	 UNF: bit,
	 OVFen: bit,
	 dbr: bit,
	 s: bit,
	 orig_s: bit,
   	 RM: bvec[2],
	 adj: adjexp_stage_out_t #]; %%% this passthrough is needed for rd2int;
		%%% rd2int does operate on the output of adjexp instead of the packed/exprd`ed
		%%% final result

  pack_stage(inp: adjexp_stage_out_t): pack_stage_out_t =
		LET f=inp`f3 ^ (51, 0),
			e=inp`e3 AND fill[11](inp`f3(52)),
			sgl=fill[1](inp`s) o e^(7,0) o f^(51,29),
			dbl=fill[1](inp`s) o e o f
		IN
      (# result:=mux_impl[64](sgl o f^(31,0), dbl, inp`dbr),
         TINY := inp`TINY,
         OVF := inp`OVF,
         INX := inp`INX OR inp`OVF AND NOT inp`OVFen,
		 UNF := inp`TINY AND (inp`UNFen OR inp`INX),
		 OVFen := inp`OVFen,
		 dbr := inp`dbr,
		 s   := inp`s,
		 orig_s := inp`orig_s,
		 RM  := inp`RM,
		 adj := inp #);

  pack_stage_passthrough: LEMMA FORALL(inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          packed = pack_stage(adjexp_stage(postnorm)) IN
		packed`RM=inp`RM AND packed`OVFen=inp`OVFen AND packed`dbr=inp`dbr AND
		packed`orig_s=inp`s;

  pack_sig_sgl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          packed = pack_stage(adjexp_stage(postnorm))
        IN
        rounder_prerequesites(x, inp, 8, 24) 
		IMPLIES
		packed`TINY = TINY[8,24](x) AND
		packed`OVF  = OVF[8,24](x, RM2mode(inp`RM)) AND
		packed`INX  = INX[8,24](x, RM2mode(inp`RM), inp`OVFen, inp`UNFen) AND
		packed`UNF  = UNF[8,24](x, RM2mode(inp`RM), inp`UNFen);

  pack_sig_dbl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          packed = pack_stage(adjexp_stage(postnorm))
        IN
        rounder_prerequesites(x, inp, 11,53)
		IMPLIES
		packed`TINY = TINY[11,53](x) AND
		packed`OVF  = OVF[11,53](x, RM2mode(inp`RM)) AND
		packed`INX  = INX[11,53](x, RM2mode(inp`RM), inp`OVFen, inp`UNFen) AND
		packed`UNF  = UNF[11,53](x, RM2mode(inp`RM), inp`UNFen);

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

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

  pack_correct_sgl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          packed = pack_stage(adjexp_stage(postnorm))
        IN
        rounder_prerequesites(x, inp, 8, 24) AND
         NOT (OVF[8, 24](x, RM2mode(inp`RM)) AND NOT inp`OVFen)
         IMPLIES
		  result_correct(packed`result, packed`OVF, packed`UNF, packed`INX)
						(RM2mode(inp`RM), inp`OVFen, inp`UNFen, inp`dbr)
						(x);

  pack_correct_dbl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET postnorm = postnorm_stage(sigrd_stage(repp_stage(ns_impl(inp)))),
          packed = pack_stage(adjexp_stage(postnorm))
        IN
        rounder_prerequesites(x, inp, 11, 53) AND
         NOT (OVF[11,53](x, RM2mode(inp`RM)) AND NOT inp`OVFen)
         IMPLIES
		  result_correct(packed`result, packed`OVF, packed`UNF, packed`INX)
						(RM2mode(inp`RM), inp`OVFen, inp`UNFen, inp`dbr)
						(x);
 END pack_stage