dalu_galu : THEORY

  BEGIN

%  Contains definitions and verification of correctness conditions for
%  derivation of Taylor's SRT divider using DRS.  Since all the
%  replacements are for combinational functions, stream
%  representations are not required.
%
% - Paul S. Miner                | email: p.s.miner@larc.nasa.gov
% - 1 South Wright St. / MS 130  |   fax: (757) 864-4234
% - NASA Langley Research Center | phone: (757) 864-6201
% - Hampton, Virginia 23681-0001 |  

     
  importing trat

%%%
%(define galu
%  (lambda (qsign rin1 md1)
%    (if qsign
%	(add rin1 md1)
%	(sub (sub rin1 md1) (expt 2 -6)))))

  galu(qs:bool, rin1:rat, md1:rat): rat = 
    if qs then rin1 + md1 else rin1 - md1 - 2^(-6) endif

%%%
% If arguments to galu are limited to 6 bits of precision to the 
% right of the binary point, then the computed result has at most 6
% bits of precision to the right of the binary point.

  JUDGEMENT galu has_type [bool,trat(6),trat(6) -> trat(6)]

%%%
%(define dalu
%  (lambda (qsign rin md)
%    (if qsign
%	(add rin md)
%	(sub rin md))))

  dalu(qs:bool, rin: rat, md: rat): rat =
    if qs then rin + md else rin - md endif
   
  new_p,pp : var rat
  d1 : var nonneg_rat
  q  : var subrange(-2,2)
  ctl: var bool

%
%  CC's from DRS derivation of Taylor's Circuit
%    "pr-taylor"


%%%
% (equiv? new-p (sub new-p zero))
%
% Proven using (assert)

  newp_subzero: LEMMA
     new_p = new_p - 0

%%%
% (equiv? (sub pp dz) (dalu (lt? q zero) pp (abs dz)))
%
% Proven using (grind)

  dalu_sub: LEMMA
   LET dz = IF ctl THEN q * d1 ELSE 0 ENDIF IN
     pp - dz = dalu(q < 0, pp, abs(dz))


%%%
% (equiv? (approx (sub pp dz)) (galu (lt? q zero) pp (approx-6 (abs dz))))
%
%  In this case, we interpret equiv? to be the equivalence class of
%  those values that satisfy the inequalities constraining approx,
%  namely:
%   FORALL (p:real):  approx(p) <= p & p <= approx(p) + 1/64
%
%  note that tfloor(6) = approx-6
%
% Proven using (grind)

  galu_sub: THEOREM
   LET dz = IF ctl THEN q * d1 ELSE 0 ENDIF IN
     galu( q < 0, pp, tfloor(6)(abs(dz))) <= pp - dz &
        pp - dz  <= galu( q < 0, pp, tfloor(6)(abs(dz))) + 2^(-6)



%%%
% (equiv?
%  (approx-6 (galu (lt? q zero) pp (approx-6 md)))
%  (galu (lt? q zero) (approx-6 pp) (approx-6 md)))
%
%  note that tfloor(6) = approx-6
%
% Proven using (grind)

  approx6_galu: THEOREM
   LET dz = IF ctl THEN q * d1 ELSE 0 ENDIF IN
     tfloor(6)(galu( q < 0, pp, tfloor(6)(abs(dz))))
        = galu( q < 0, tfloor(6)(pp), tfloor(6)(abs(dz)))

%%%
% (equiv? (abs zero) zero)
%
% Proven using (expand "abs")
  zero: LEMMA
     abs(0) = 0 

%%%
% (equiv? (abs (mul q d1)) (mul (abs q) d1))
%
% Proven using (grind)
  abs_mul_q: LEMMA
     abs(q * d1) = abs(q) * d1

  END dalu_galu