rd_input: THEORY
 BEGIN


  IMPORTING rd_import

  rounder_input_t: TYPE =
  [# er: bvec[13],
     fr: bvec[57],
     OVFen: bit,
     UNFen: bit,
     dbr: bit,
     s: bit,
     RM: bvec[2] #];

  s: VAR bit;

  sign_ok: JUDGEMENT  b2n(s) HAS_TYPE sign_rep;

  rd_y(x: real, OVFen, UNFen: bit, N, P: above(1)): real =
      IF OVF_before[N, P](x) AND OVFen
        THEN x * 2 ^ -Alpha[N]
      ELSE IF TINY[N, P](x) AND UNFen THEN x * 2 ^ Alpha[N] ELSE x ENDIF
      ENDIF;

  rounder_prerequesites(x: nonzero_real, inp: rounder_input_t,
                        N, P: above(1)):
  bool =
      LET y = rd_y(x, inp`OVFen, inp`UNFen, N, P) IN
        x = sign[N](inp`s) * 2 ^ bv2int(inp`er) * bv2nat(inp`fr) * 2 ^ -55
         AND
         (((NOT inp`fr(56)) AND (NOT inp`fr(55))) IMPLIES
           bv2int(inp`er) <= emax[N])
          AND
          (inp`dbr = (N = 11)) AND
           (((TINY[N, P](x) AND inp`UNFen) OR
              (OVF_before[N, P](x) AND inp`OVFen))
             IMPLIES (2 ^ emin[N] < abs(y) AND abs(y) < 2 ^ emax[N]));

  rd_inp_sign: LEMMA FORALL(x: nonzero_real, inp: rounder_input_t, N, P: above(1)):
		rounder_prerequesites(x, inp, N, P) IMPLIES
			(inp`s IFF x<0);

  adder_input_prereq(inp: rounder_input_t, N,P: above(4)): bool =
		LET X=value[N]((# s:=inp`s::sign_rep, e:=bv2int(inp`er), f:=bv2nat(inp`fr) * 2^-55 #)) IN
		(inp`dbr = (N=11)) AND
		(bv2int(inp`er) <= emax[N]) AND
		(2^(emin[N]-Alpha[N]) < abs(X)  AND abs(X) < 2^(emax[N]+Alpha[N]));

  add_input_ok: LEMMA FORALL (inp: rounder_input_t, N,P: above(4)):
		adder_input_prereq(inp,N,P) IMPLIES
			rounder_prerequesites(X, inp, N, P)
			WHERE X=value[N]((# s:=inp`s::sign_rep, e:=bv2int(inp`er), f:=bv2nat(inp`fr) * 2^-55 #));


  muldiv_input_prereq(inp: rounder_input_t, N,P: above(4)): bool =
		LET X=value[N]((# s:=inp`s::sign_rep, e:=bv2int(inp`er), f:=bv2nat(inp`fr) * 2^-55 #)) IN
		(inp`dbr = (N=11)) AND
		1<=bv2nat(inp`fr) * 2^-55 AND bv2nat(inp`fr) * 2^-55<4 AND
		2^(emin[N]-Alpha[N]) < abs(X) AND abs(X) < 2^(emax[N]+Alpha[N]);

  muldiv_0xor1: LEMMA FORALL(x: nat): x<2 IMPLIES x=0 or x=1;

  muldiv_input_ok: LEMMA FORALL (inp: rounder_input_t, N,P: above(4)):
		muldiv_input_prereq(inp,N,P) IMPLIES
			rounder_prerequesites(X, inp, N, P)
			WHERE X=value[N]((# s:=inp`s::sign_rep, e:=bv2int(inp`er), f:=bv2nat(inp`fr) * 2^-55 #));
 END rd_input