sig_add: Theory
Begin

  Importing adder_import

  sig_add_in_t: Type =
    [# fa2: bvec[53],
       fb3: bvec[56],
       sa2, sb2: bit,
       sx: bit #];

  sig_add_out_t: Type =
    [# fs: bvec[57],
       ss: bit #];

  i: Var sig_add_in_t;

  sig_add_impl(i): sig_add_out_t =
    Let add = add_sub_impl[58](fill[2](False) o i`fa2 o fill[3](False),
                           fill[2](False) o i`fb3,
                           i`sx) In
%% The following is wrong in MP00 %%
%%    (# ss1 := (i`sb2 And add`neg) Or (i`sa2 And Not (i`sb2 And add`neg)), %%
      (# ss := i`sa2 Xor add`neg,  %% right %%
         fs := abs_impl[58](add`s) #);

  % the sum is representable
  sig_add_sum_in_rng: Lemma
      in_rng_2s_comp[58]
          (If i`sx
           Then bv2int(fill[2](False) o i`fa2 o fill[3](False)) -
                bv2int(fill[2](False) o i`fb3)
           Else bv2int(fill[2](False) o i`fa2 o fill[3](False)) +
                bv2int(fill[2](False) o i`fb3)
           Endif);

  % valid input for abs_impl
  sig_add_impl_abs: Lemma
        bv2int(add_sub_impl(fill[2](False) o i`fa2 o fill[3](False),
                            fill[2](False) o i`fb3, i`sx)`s)
        =
        If i`sx
        Then bv2int(fill[2](False) o i`fa2 o fill[3](False)) -
             bv2int(fill[2](False) o i`fb3)
        Else bv2int(fill[2](False) o i`fa2 o fill[3](False)) +
             bv2int(fill[2](False) o i`fb3)
        Endif
      Implies
        add_sub_impl(fill[2](False) o i`fa2 o fill[3](False),
                 fill[2](False) o i`fb3, i`sx)`s
        /= fill[1](True) o fill[57](False);

  % sum output (obsolete)
  sig_add_impl_correct_fs: Lemma
      Let s = sig_add_impl(i),
          a_ = value[11](bv2fact[11,53,0](False, int2bv(0), i`fa2)),
          b_ = value[11](bv2fact[11,56,0](False, int2bv(0), i`fb3)),
          sum = If i`sx Then a_ - b_ Else a_ + b_ EndIf
        In
          abs(sum) = value[11](bv2fact[11,56,1](False, int2bv(0), s`fs));

  % sign output (obsolete)
  sig_add_impl_correct_ss1: Lemma
      Let s = sig_add_impl(i),
          a_ = value[11](bv2fact[11,53,0](i`sa2, int2bv(0), i`fa2)),
          b_ = value[11](bv2fact[11,56,0](i`sb2, int2bv(0), i`fb3)),
          sum = a_ + b_
        In
          i`sx = (i`sa2 Xor i`sb2) And sum /= 0 Implies
            s`ss = (sum < 0);

  % sum with sign(s)
  sig_add_impl_correct_sum: Lemma
      Let s = sig_add_impl(i),
          a_ = value[11](bv2fact[11,53,0](i`sa2, int2bv(0), i`fa2)),
          b_ = value[11](bv2fact[11,56,0](i`sb2, int2bv(0), i`fb3)),
          sum = a_ + b_
        In
          i`sx = (i`sa2 Xor i`sb2) Implies
            sum = value[11](bv2fact[11,56,1](s`ss, int2bv(0), s`fs));

End sig_add