40 lines
850 B
Plaintext
40 lines
850 B
Plaintext
full_adder: THEORY
|
|
BEGIN
|
|
a, b, cin: VAR bit
|
|
|
|
% Auto-convert bit to nat when needed
|
|
CONVERSION+ b2n
|
|
|
|
fa_cout(a, b, cin) : bit =
|
|
(a AND b) OR (b AND cin) OR (a AND cin)
|
|
fa_sum(a, b, cin) : bit =
|
|
(a XOR b) XOR cin
|
|
|
|
fa_correct: LEMMA fa_sum(a, b, cin) = a + b + cin - 2 * fa_cout(a, b, cin)
|
|
END full_adder
|
|
|
|
|
|
adder[N:posnat]: THEORY
|
|
BEGIN
|
|
%IMPORTING full_adder
|
|
IMPORTING bv[N], full_adder
|
|
n: VAR below[N]
|
|
a, b: VAR bvec[N]
|
|
j: VAR upto[N]
|
|
|
|
nth_cin(j, a, b): RECURSIVE bit =
|
|
IF j = 0 THEN
|
|
FALSE
|
|
ELSE
|
|
fa_cout(a(j-1), b(j-1),
|
|
nth_cin(j-1, a, b))
|
|
ENDIF
|
|
MEASURE j
|
|
|
|
%adder_correct_n: LEMMA
|
|
%bvec2nat_rec(n, a) + bvec2nat_rec(n, b) + bool2bit(cin) =
|
|
%exp2(n+1) * bool2bit(fa_cout(n, a[n], b[n], nth_cin(n-1, a, b))) +
|
|
%bvec2nat_rec(n, fa_sum(a, b, cin))
|
|
|
|
END adder
|