repp: THEORY
 BEGIN

  IMPORTING ns_impl

  repp_impl(fn: bvec[128], dbr: bit): bvec[55] =
      LET or_single = NOT zero_impl[103](fn ^ (102, 0)),
          or_double = NOT zero_impl[74](fn ^ (73, 0)),
          single = fn ^ (127, 103) o fill[1](or_single) o fill[29](FALSE),
          double = fn ^ (127, 74) o fill[1](or_double)
        IN mux_impl[55](single, double, dbr);

  repp_impl_correct_single: LEMMA
    FORALL (fn: bvec[128]):
      alpha_rep[-24](bv2nat(fn) * 2 ^ -127) =
       bv2nat(repp_impl(fn, FALSE)) * 2 ^ -54;

  repp_impl_correct_double: LEMMA
    FORALL (fn: bvec[128]):
      alpha_rep[-53](bv2nat(fn) * 2 ^ -127) =
       bv2nat(repp_impl(fn, TRUE)) * 2 ^ -54;
 END repp

repp_stage: THEORY
 BEGIN

  IMPORTING repp

  repp_stage_out_t: TYPE = rd_rd2in_t;
%  [# f1: bvec[55],
%     en: bvec[11],
%     eni: bvec[11],
%     TINY: bit,
%     OVF1: bit,
%     UNFen: bit,
%     OVFen: bit,
%     dbr: bit,
%     s: bit,
%     RM: bvec[2] #];

  repp_stage(inp: ns_stage_out_t): repp_stage_out_t =
      (# f1 := repp_impl(inp`fn, inp`dbr),
         en := inp`en,
         eni := inp`eni,
         TINY := inp`TINY,
         OVF1 := inp`OVF1,
         UNFen := inp`UNFen,
         OVFen := inp`OVFen,
         dbr := inp`dbr,
         s := inp`s,
         RM := inp`RM #);

  repp_stage_passthrough: LEMMA
    FORALL (inp: rounder_input_t):
      LET out = repp_stage(ns_impl(inp)) IN
        out`dbr = inp`dbr AND
         out`s = inp`s AND out`RM = inp`RM AND
		 out`UNFen=inp`UNFen AND out`OVFen=inp`OVFen;

  repp_stage_tiny_ovf_sgl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET rep = repp_stage(ns_impl(inp)) IN
        rounder_prerequesites(x, inp, 8, 24) IMPLIES
         rep`TINY = TINY[8, 24](x) AND rep`OVF1 = OVF_before[8, 24](x);

  repp_stage_tiny_ovf_dbl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET rep = repp_stage(ns_impl(inp)) IN
        rounder_prerequesites(x, inp, 11, 53) IMPLIES
         rep`TINY = TINY[11, 53](x) AND rep`OVF1 = OVF_before[11, 53](x);

  repp_lem: LEMMA
    FORALL (f1, f2: nonneg_real, s: int | s = 1 OR s = -1, alpha, k: int):
      f2 = alpha_rep[-k](f1) IMPLIES
       alpha_rep[alpha - k](f1 * s * 2 ^ alpha) =
        alpha_rep[alpha - k](f2 * s * 2 ^ alpha);

  repp_stage_sgl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET rep = repp_stage(ns_impl(inp)),
          y = rd_y(x, inp`OVFen, inp`UNFen, 8, 24)
        IN
        (NOT (OVF_before[8, 24](x) AND NOT inp`OVFen)) AND
         rounder_prerequesites(x, inp, 8, 24)
         IMPLIES
  		   bv2nat(rep`eni^(7,0))  = bv2nat(rep`en^(7,0))+1 AND
             alpha_eq[val_bias(rep`en ^ (7, 0)) - 24](y,
                           sign[8](inp`s) * 2 ^ val_bias(rep`en ^ (7, 0))
                            * bv2nat(rep`f1)
                            * 2 ^ -54)
            AND
            ii_i3e_number?[8]
                ((# s := b2n(rep`s),
                    e := val_bias(rep`en ^ (7, 0)),
                    f := bv2nat(rep`f1) * 2 ^ -54 #))
             AND rep`f1 ^ (28, 0) = fill[29](FALSE);

  repp_stage_dbl: LEMMA
    FORALL (x: nonzero_real, inp: rounder_input_t):
      LET rep = repp_stage(ns_impl(inp)),
          y = rd_y(x, inp`OVFen, inp`UNFen, 11, 53)
        IN
        (NOT (OVF_before[11, 53](x) AND NOT inp`OVFen)) AND
         rounder_prerequesites(x, inp, 11, 53)
         IMPLIES
  	 	   bv2nat(rep`eni)  = bv2nat(rep`en)+1 AND
            alpha_eq[val_bias(rep`en) - 53](y,
                           sign[11](inp`s) * 2 ^ val_bias(rep`en) *
                            bv2nat(rep`f1)
                            * 2 ^ -54)
            AND
            ii_i3e_number?[11]
                ((# s := b2n(rep`s),
                    e := val_bias(rep`en),
                    f := bv2nat(rep`f1) * 2 ^ -54 #));
 END repp_stage