From The Twelf Project
% ============================================================
% == Bits and binary numbers ==
% == ==
% == A binary number is a list of bits with the LEAST ==
% == significant digit exposed. A cobinary number is a ==
% == list of bits with the MOST significant bits exposed. ==
% == This library assumes that binary numbers are used more ==
% == often than cobinary numbers, but cobinaries make it ==
% == much easier to do certain operations. ==
% ============================================================
bit : type.
bit/0 : bit.
bit/1 : bit.
%abbrev b0 = bit/0.
%abbrev b1 = bit/1.
binary : nat -> type.
binary/nil : binary nat/z.
binary/cons : bit -> binary N -> binary (s N).
%abbrev $ = binary/cons. %infix right 4 $.
%abbrev $nil = binary/nil.
%abbrev 0 : binary N -> binary (s N) = [B] binary/cons bit/0 B.
%abbrev 1 : binary N -> binary (s N) = [B] binary/cons bit/1 B.
cobinary : nat -> type.
cobinary/nil : cobinary z.
cobinary/cons : bit -> cobinary N -> cobinary (s N).
%abbrev & = cobinary/cons. %infix right 4 &.
%abbrev &nil = cobinary/nil.
% = Section 1 : Bit-pushing =
% ============================================================
% == Conversion from binaries to cobinaries, and back ==
% ==
% ==
binary->cobinary-help : nat-plus NA NB NC
-> binary NA -> cobinary NB -> cobinary NC -> type.
%mode binary->cobinary-help +D +N1 +N2 -N3.
binary->cobinary-help/z : binary->cobinary-help nat-plus/z $nil N2 N2.
binary->cobinary-help/s : binary->cobinary-help (nat-plus/s D) (Bit $ A) B C
<- nat-plus/s-alt D D2
<- binary->cobinary-help D2 A (Bit & B) C.
%worlds () (binary->cobinary-help _ _ _ _).
%total T (binary->cobinary-help _ T _ _).
binary->cobinary : binary N -> cobinary N -> type.
%mode binary->cobinary +N1 -N2.
binary->cobinary/i : binary->cobinary N1 N2
<- nat-plus/z-alt _ D
<- binary->cobinary-help D N1 &nil N2.
%worlds () (binary->cobinary _ _).
%total T (binary->cobinary T _).
cobinary->binary-help : nat-plus NA NB NC
-> cobinary NA -> binary NB -> binary NC -> type.
%mode cobinary->binary-help +D +N1 +N2 -N3.
cobinary->binary-help/z : cobinary->binary-help nat-plus/z &nil N2 N2.
cobinary->binary-help/s : cobinary->binary-help (nat-plus/s D) (Bit & A) B C
<- nat-plus/s-alt D D2
<- cobinary->binary-help D2 A (Bit $ B) C.
%worlds () (cobinary->binary-help _ _ _ _).
%total T (cobinary->binary-help _ T _ _).
cobinary->binary : cobinary N -> binary N -> type.
%mode cobinary->binary +N1 -N2.
cobinary->binary/i : cobinary->binary N1 N2
<- nat-plus/z-alt _ D
<- cobinary->binary-help D N1 $nil N2.
%worlds () (cobinary->binary _ _).
%total T (cobinary->binary T _).
% ============================================================
% == The "get a zero of the right size" predicate ==
% ============================================================
bin-zero : {N} binary N -> type.
%mode bin-zero +N -B.
bin-zero/z : bin-zero z $nil.
bin-zero/s : bin-zero (s N) (0 B) <- bin-zero N B.
%worlds () (bin-zero _ _).
%total T (bin-zero T _).
% ============================================================
% == The "are there more ones" test ==
% == ==
% == Returns the 1 bit if there are more ones, 0 otherwise ==
% ============================================================
bin-moreones : binary N -> bit -> type.
%mode bin-moreones +A -B.
bin-moreones/z : bin-moreones $nil bit/0.
bin-moreones/1 : bin-moreones (1 _) bit/1.
bin-moreones/0 : bin-moreones (0 B) R <- bin-moreones B R.
%worlds () (bin-moreones _ _).
%total T (bin-moreones T _).
% ============================================================
% == Truncate ==
% == ==
% == Takes a natural number N and a binary number B1, and ==
% == returns a N-digit binary number that is B1 with either ==
% == higher-order 0's added or higer-order digits lopped ==
% == off ==
% ============================================================
bin-truncate : {N} binary A -> binary N -> type.
%mode bin-truncate +N +B1 -B2.
bin-truncate/z : bin-truncate z _ $nil.
bin-truncate/s$nil : bin-truncate (s N) $nil (0 B) <- bin-truncate N $nil B.
bin-truncate/s0 : bin-truncate (s N) (0 B1) (0 B2) <- bin-truncate N B1 B2.
bin-truncate/s1 : bin-truncate (s N) (1 B1) (1 B2) <- bin-truncate N B1 B2.
%worlds () (bin-truncate _ _ _).
%total T (bin-truncate T _ _).
% ============================================================
% == Trim ==
% == ==
% == Takes a binary number and returns another with all the ==
% == higher order 0's lopped off ==
% ============================================================
bin-trim-help : binary N -> bit -> binary M -> type.
%mode bin-trim-help +B1 +B -B2.
bin-trim : binary N -> binary M -> type.
%mode bin-trim +B1 -B2.
bin-trim/done : bin-trim-help B bit/0 $nil.
bin-trim/more : bin-trim-help B1 bit/1 B2
<- bin-trim B1 B2.
bin-trim/$nil : bin-trim $nil $nil.
bin-trim/0 : bin-trim (0 B1) B2
<- bin-moreones B1 B
<- bin-trim-help (0 B1) B B2.
bin-trim/1 : bin-trim (1 B1) (1 B2)
<- bin-trim B1 B2.
%worlds () (bin-trim _ _) (bin-trim-help _ _ _).
% total (T1 T2) (bin-trim T1 _) (bin-trim-help T2 _ _).
% ============================================================
% == Equalize ==
% == Takes two binary numbers and makes them equal in size ==
% ============================================================
bin-eq-ize : binary N -> binary M -> binary P -> binary Q -> type.
%mode bin-eq-ize +B1 +B2 -B3 -B4.
bin-eq-ize/$$: bin-eq-ize $nil $nil $nil $nil.
bin-eq-ize/$0: bin-eq-ize $nil (0 B2) (0 B3) (0 B4)<- bin-eq-ize $nil B2 B3 B4.
bin-eq-ize/$1: bin-eq-ize $nil (1 B2) (0 B3) (1 B4)<- bin-eq-ize $nil B2 B3 B4.
bin-eq-ize/0$: bin-eq-ize (0 B1) $nil (0 B3) (0 B4)<- bin-eq-ize B1 $nil B3 B4.
bin-eq-ize/1$: bin-eq-ize (1 B1) $nil (1 B3) (0 B4)<- bin-eq-ize B1 $nil B3 B4.
bin-eq-ize/00: bin-eq-ize (0 B1) (0 B2) (0 B3) (0 B4)<- bin-eq-ize B1 B2 B3 B4.
bin-eq-ize/01: bin-eq-ize (0 B1) (1 B2) (0 B3) (1 B4)<- bin-eq-ize B1 B2 B3 B4.
bin-eq-ize/10: bin-eq-ize (1 B1) (0 B2) (1 B3) (0 B4)<- bin-eq-ize B1 B2 B3 B4.
bin-eq-ize/11: bin-eq-ize (1 B1) (1 B2) (1 B3) (1 B4)<- bin-eq-ize B1 B2 B3 B4.
%worlds () (bin-eq-ize _ _ _ _).
%total {T1 T2} (bin-eq-ize T1 T2 _ _).
% = Section 2 : Basic numerical operations =
% ============================================================
% == Plain Vanilla binary addition (with carry) ==
% == Always call with CARRY_IN = bit/0 in standard use ==
% == ==
% == Always call with CARRY_IN = bit/0 in standard use ==
% == Call with CARRY_IN = bit/1 to increment N1 ==
% ============================================================
bin-plusc : binary N -> binary N -> bit -> binary N -> bit -> type.
%mode bin-plusc +N1 +N2 +CARRY_IN -N2 -CARRY_OUT.
bin-plusc/z : bin-plusc $nil $nil C $nil C.
bin-plusc/1 : bin-plusc (0 N1)(0 N2) b0 (0 N3) C <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/2 : bin-plusc (0 N1)(0 N2) b1 (1 N3) C <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/3 : bin-plusc (0 N1)(1 N2) b0 (1 N3) C <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/4 : bin-plusc (0 N1)(1 N2) b1 (0 N3) C <- bin-plusc N1 N2 b1 N3 C.
bin-plusc/5 : bin-plusc (1 N1)(0 N2) b0 (1 N3) C <- bin-plusc N1 N2 b0 N3 C.
bin-plusc/6 : bin-plusc (1 N1)(0 N2) b1 (0 N3) C <- bin-plusc N1 N2 b1 N3 C.
bin-plusc/7 : bin-plusc (1 N1)(1 N2) b0 (0 N3) C <- bin-plusc N1 N2 b1 N3 C.
bin-plusc/8 : bin-plusc (1 N1)(1 N2) b1 (1 N3) C <- bin-plusc N1 N2 b1 N3 C.
%worlds () (bin-plusc _ _ _ _ _).
%total T (bin-plusc T _ _ _ _).
% ============================================================
% == Binary subtraction (with carry) ==
% == ==
% == The "borrow-out" digit, the second output of binary ==
% == subtraction, can be used as a less-than test. ==
% == ==
% == Always call with CARRY_IN = bit/0 in standard use ==
% == ==
% == If BORROW_OUT is 1, then N1 < N2 (N3 is undefined) ==
% == If BORROW_OUT is 0, then N1 >= N2 and N3 = N1 - N2 ==
% ============================================================
bin-minus : binary N -> binary M -> bit -> binary N -> bit -> type.
%mode bin-minus +N1 +N2 +BORROW_IN -N2 -BORROW_OUT.
bin-minus/l1 : bin-minus $nil (B2 $ N2) b1 $nil b1.
bin-minus/l0 : bin-minus $nil (B2 $ N2) b0 $nil BOUT
<- bin-moreones (B2 $ N2) BOUT.
bin-minus/g0 : bin-minus (B1 $ N1) $nil b0 (B1 $ N1) b0.
bin-minus/a5 : bin-minus (0 N1) $nil b1 (1 N3) C <- bin-minus N1 $nil b1 N3 C.
bin-minus/a7 : bin-minus (1 N1) $nil b1 (0 N3) C <- bin-minus N1 $nil b0 N3 C.
bin-minus/z : bin-minus $nil $nil C $nil C.
bin-minus/1 : bin-minus (0 N1)(0 N2) b0 (0 N3) C <- bin-minus N1 N2 b0 N3 C.
bin-minus/2 : bin-minus (0 N1)(1 N2) b0 (1 N3) C <- bin-minus N1 N2 b1 N3 C.
bin-minus/3 : bin-minus (1 N1)(0 N2) b0 (1 N3) C <- bin-minus N1 N2 b0 N3 C.
bin-minus/4 : bin-minus (1 N1)(1 N2) b0 (0 N3) C <- bin-minus N1 N2 b0 N3 C.
bin-minus/5 : bin-minus (0 N1)(0 N2) b1 (1 N3) C <- bin-minus N1 N2 b1 N3 C.
bin-minus/6 : bin-minus (0 N1)(1 N2) b1 (0 N3) C <- bin-minus N1 N2 b1 N3 C.
bin-minus/7 : bin-minus (1 N1)(0 N2) b1 (0 N3) C <- bin-minus N1 N2 b0 N3 C.
bin-minus/8 : bin-minus (1 N1)(1 N2) b1 (1 N3) C <- bin-minus N1 N2 b1 N3 C.
%worlds () (bin-minus _ _ _ _ _).
%total T (bin-minus T _ _ _ _).
% ===========================================================
% == Carryless binary addition (used for multiplcation) ==
% ===========================================================
bin-plus : binary M -> binary M -> bit -> binary (s M) -> type.
%mode bin-plus +N1 +N2 +CARRY_IN -N2.
bin-plus/z0 : bin-plus $nil $nil b0 (0 $nil).
bin-plus/z1 : bin-plus $nil $nil b1 (1 $nil).
bin-plus/s0 : bin-plus (0 N1)(0 N2) b0 (0 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s1 : bin-plus (0 N1)(0 N2) b1 (1 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s2 : bin-plus (0 N1)(1 N2) b0 (1 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s3 : bin-plus (0 N1)(1 N2) b1 (0 N3) <- bin-plus N1 N2 b1 N3.
bin-plus/s4 : bin-plus (1 N1)(0 N2) b0 (1 N3) <- bin-plus N1 N2 b0 N3.
bin-plus/s5 : bin-plus (1 N1)(0 N2) b1 (0 N3) <- bin-plus N1 N2 b1 N3.
bin-plus/s6 : bin-plus (1 N1)(1 N2) b0 (0 N3) <- bin-plus N1 N2 b1 N3.
bin-plus/s7 : bin-plus (1 N1)(1 N2) b1 (1 N3) <- bin-plus N1 N2 b1 N3.
%worlds () (bin-plus _ _ _ _).
%total T (bin-plus _ T _ _).
% ===========================================================
% == Bitwise nand ==
% ===========================================================
bin-nand : binary N -> binary N -> binary N -> type.
%mode bin-nand +A +B -C.
bin-nand/z : bin-nand $nil $nil $nil.
bin-nand/s0 : bin-nand (0 N1) (0 N2) (1 N3) <- bin-nand N1 N2 N3.
bin-nand/s1 : bin-nand (0 N1) (1 N2) (1 N3) <- bin-nand N1 N2 N3.
bin-nand/s2 : bin-nand (1 N1) (0 N2) (1 N3) <- bin-nand N1 N2 N3.
bin-nand/s3 : bin-nand (1 N1) (1 N2) (1 N3) <- bin-nand N1 N2 N3.
% = Section 3 : Advanced numerical operations =
% ===========================================================
% == Full multiplcation ==
% == ==
% == Utilizes a helper function for multiplying the second ==
% == number by the high-order bit of a first number, and ==
% == returning the first number without removing that bit ==
% ===========================================================
bin-times-highbit : nat-plus NA NB NC
-> binary (s NA) -> binary NB
-> binary NA -> binary NC -> type.
%mode bin-times-highbit +D +A +B -A' -C.
bin-times-highbit/0
: bin-times-highbit nat-plus/z (b0 $ $nil) B $nil Z <- bin-zero _ Z.
bin-times-highbit/1
: bin-times-highbit nat-plus/z (b1 $ $nil) B $nil B.
bin-times-highbit/s
: bin-times-highbit (nat-plus/s D) (Bit $ A) B (Bit $ A') (0 C)
<- bin-times-highbit D A B A' C.
%worlds () (bin-times-highbit _ _ _ _ _).
%total T (bin-times-highbit T _ _ _ _).
bin-times : nat-plus N M P -> binary N -> binary M -> binary P -> type.
%mode bin-times +D +B1 +B2 -B3.
bin-times/z : bin-times nat-plus/z $nil A (Z: binary N)
<- bin-zero N Z.
bin-times/s : bin-times (nat-plus/s (N:nat-plus NA NB NC)) A B C
<- bin-times-highbit N A B A2 B2
<- bin-times N A2 B C2
<- nat-plus-assoc N N'
<- bin-plus B2 C2 b0 C.
%worlds () (bin-times _ _ _ _).
%total T (bin-times T _ _ _).
% ===========================================================
% == Division with remainder ==
% == ==
% == Division needs a helper lemma that chooses, given the ==
% == output of a call to minus(NUM,DIV,NOUT), to tack a ==
% == 0 on to the result and proceed with NUM if ==
% == subtraction failed, and to tack on a 1 and proceed ==
% == with NOUT if subtraction failed. ==
% == ==
% == The division altorithm is very confusing and will ==
% == need exposition at a later time. ==
% ===========================================================
bin-longdiv-help : bit -> binary N -> binary N -> bit -> binary N -> type.
%mode bin-longdiv-help +BitOUT +NOUT +NUM -Bit -REMAINDER.
bin-longdiv-help/0 : bin-longdiv-help b0 NOUT _ b1 NOUT.
bin-longdiv-help/1 : bin-longdiv-help b1 _ NUM b0 NUM.
%worlds () (bin-longdiv-help _ _ _ _ _).
%total T (bin-longdiv-help T _ _ _ _).
bin-longdiv : nat-plus N1 (s N2) N3
-> cobinary N1 -> binary (s N2) -> binary M
-> cobinary (s N1) -> binary N3 -> type.
%mode bin-longdiv +D +NUMERATOR1 +NUMERATOR2 +DIVISOR -QUOTIENT -REMAINDER.
bin-longdiv/z : bin-longdiv nat-plus/z &nil NUM DIV (Bit & &nil) REMAINDER
<- bin-minus NUM DIV b0 NOUT BitOUT
<- bin-longdiv-help BitOUT NOUT NUM Bit REMAINDER.
bin-longdiv/s : bin-longdiv (nat-plus/s D1) (Bit1 & N1) NUM DIV (Bit2 & QUOT) R
<- bin-minus NUM DIV b0 NOUT BitOUT
<- bin-longdiv-help BitOUT NOUT NUM Bit2 NUM2
<- nat-plus/s-alt D1 D2
<- bin-longdiv D2 N1 (Bit1 $ NUM2) DIV QUOT R.
%worlds () (bin-longdiv _ _ _ _ _ _).
%total T (bin-longdiv _ T _ _ _ _).
bin-divmod : binary N -> binary M -> binary N -> binary N -> type.
%mode bin-divmod +NUMERATOR +DIVISOR -QUOTIENT -REMAINDER.
bin-divmod/z : bin-divmod $nil _ $nil $nil.
bin-divmod/s : bin-divmod (NUM : binary (s N)) DIV QUOT REM
<- binary->cobinary NUM (Bit & CONUM)
<- nat-plus/z-alt _ D
<- nat-plus/s-alt D D'
<- bin-longdiv D' CONUM (Bit $ $nil) DIV COQUOT REM
<- cobinary->binary COQUOT QUOT.
%worlds () (bin-divmod _ _ _ _).
%total T (bin-divmod T _ _ _).
% ***************************** TEST CASES *****************************
bin342 = [X] (0(1(1(0(1(0(1(0(1(0(0(0 X)))))))))))).
bin215 = (1(1(1(0(1(0(1(1(0(0(0 $nil))))))))))).
bin73530 = [X] (0(1(0(1(1(1(0(0(1(1(1(1(1(0(0(0(1 X))))))))))))))))).
deriv = nps(nps(nps(nps(nps(nps(nps(nps(nps(nps(nps(nps npz))))))))))).
%query 1 * Test : bin-times deriv (bin342 $nil) bin215 (bin73530 Zeroes).
%query 1 * Test : bin-divmod (bin73530 $nil) bin215 (bin342 Zeroes) R.
