fpadd: Theory
Begin


  Importing fpadder

  i1: Var add_stg1in_t;
  i2: Var add_stg2in_t;

  %% conversion functions
  add_input_1(i1): adder_in1_t =
      (# fa := i1`fa,
         ea := i1`ea,
         sa := i1`sa,
         fb := i1`fb,
         eb := i1`eb,
         sb := i1`sb,
         sub := i1`sub #);

  add_input_2(i2): adder_in3_t =
      (# es := i2`es,
         fa2 := i2`fa2,
         sa2 := i2`sa2,
         fb3 := i2`fb3,
         sb2 := i2`sb2,
         sx := i2`sx #);

  %% pipeline stage implementations
  add_stg1(i1): add_stg2in_t =
      LET f = adder_stage_2(adder_stage_1(add_input_1(i1))) IN
        (# es := f`es,
           fa2 := f`fa2,
           sa2 := f`sa2,
           fb3 := f`fb3,
           sb2 := f`sb2,
           sx := f`sx,
           RM := i1`RM,
           double := i1`double,
           mask := i1`mask #);

  add_stg2(i2): rd_rd1in_t =
      LET f = adder_stage_3(add_input_2(i2)) IN
        (# sr := f`ss,
           er := sext_impl[11,13](f`es),
           fr := f`fs,
           RM := i2`RM,
           double := i2`double,
           mask := i2`mask #);

  %% the adder
  fpadd(i: add_stg1in_t): rd_rd1in_t =
    add_stg2(add_stg1(i));

  %% equivalence to the 'small' adder
  fpadd_sr: Lemma
    fpadd(i1)`sr = fpadder(add_input_1(i1))`ss;

  fpadd_er: Lemma
    fpadd(i1)`er = sext_impl[11,13](fpadder(add_input_1(i1))`es);

  fpadd_fr: Lemma
    fpadd(i1)`fr = fpadder(add_input_1(i1))`fs;

  fpadd_value: LEMMA
    value[13](bv2fact[13, 56, 1](fpadd(i1)`sr, fpadd(i1)`er, fpadd(i1)`fr))
     =
     value[11]
         (bv2fact[11, 56, 1]
              (fpadder(add_input_1(i1))`ss,
               fpadder(add_input_1(i1))`es,
               fpadder(add_input_1(i1))`fs));

  %% correctness
  fpadd_correct: Theorem
    Forall (i1):
      Let a0 = bv2fact[11,53,0](i1`sa, i1`ea, i1`fa),
          b0 = bv2fact[11,53,0](i1`sb, i1`eb, i1`fb),
          a = value[11](a0),
          b = value[11](b0),
          out = fpadd(i1),
          sum = If i1`sub Then a - b Else a + b EndIf In
        sum /= 0 And if_i3e_number?[11,53](a0) And if_i3e_number?[11,53](b0) Implies
          Let sum_eta = eta_hat[11](sum) In
            alpha_eq[-53 + sum_eta`e](sum, 
                             value[13](bv2fact[13,56,1](out`sr, out`er, out`fr)));

  fpadd_correct_sgl: Theorem
    Forall (i1):
      Let a0 = bv2fact[11,53,0](i1`sa, i1`ea, i1`fa),
          b0 = bv2fact[11,53,0](i1`sb, i1`eb, i1`fb),
          a = value[11](a0),
          b = value[11](b0),
          out = fpadd(i1),
          sum = If i1`sub Then a - b Else a + b EndIf In
        sum /= 0 And if_i3e_number?[8,53](a0) And if_i3e_number?[8,53](b0) Implies
          Let sum_eta = eta_hat[11](sum) In
            alpha_eq[-53 + sum_eta`e](sum, 
                             value[13](bv2fact[13,56,1](out`sr, out`er, out`fr)));

End fpadd