ip_checksum_eqc.erl

%%% File    : ip_checksum_eqc.erl
%%% Author  : Ulf Norell <ulf.norell@quviq.com>,
%%%           Thomas Arts <thomas.arts@quviq.com>
%%% Description : QuickCheck properties for ip_checksum.erl
%%% Created : 7 Jun 2010 by Ulf Norell
-module(ip_checksum_eqc).

-include_lib("eqc/include/eqc.hrl").

-compile(export_all).

% == Testing IP checksum implementations ==

% In RFC 1071 efficient algorithms are discussed for computing the internet
% checksum, also known as IP checksum. Whenever you implement efficient
% algorithms, an error may sneak through.

% This article is meant to be used as test driven development specification for
% anyone that wants to implement one of the algorithms of RFC 1071 or even a new
% one to compute the IP checksum. The article can also be read as an example of
% specifying something without revealing its implementation details; a good
% example of using QuickCheck specifications.

% Whether you write your code in Erlang, C or Java, we assume that you can build
% an interface to a module called ip_checksum.erl in which Erlang functions
% either are the functions under test or call the functions under test.

% === IP Checksum ===

% The IP checksum is the 16 bit one's complement of the one's complement sum of
% all 16 bit words in the header.

% Ones complement is a way of representing negative numbers (see
% [http://en.wikipedia.org/wiki/Signed_number_representations#Ones.27_complement
% WikiPedia] for more details).

% The IP checksum uses 16 bit words. In 16 bits you can represent the numbers 0
% to 65535. The idea with ones complement is to use half the numbers in this
% interval for representing negative numbers.  Thus, 0 up to 32767 are the
% positive numbers and 65535 is -0, or an alternative representation of zero.
% The number 65534 is -1 etc. Until 32768 which is -32767. Hence the interval
% -32767 up to 32767 can be represented.

% In the remainder of this article we will present properties for functions that
% you probably would like to test. The properties are always parametrized by the
% word size.

% === Utility functions ===

% First we define some functions that will come in handy.

% The maximum number that can be represented in ''N'' bits. In the ones
% complement interpretation this will be the negative zero.
max_int(N) ->
  (1 bsl N) - 1.

negative_zero(N) ->
  max_int(N).

% === Ones complement ===

% The first function we might want to check is the ones' complement of a word,
% which in ones' complement representation corresponds to the negation.  We
% assume we have a function '''ip_checksum:negate/1''' implemented that takes a
% bit string as input and computes its ones' complement.

% Looking at the specification of ones' complement representation above we can
% see that adding the ones' complement representation of a number and the
% representation of its negation results in the representation of -0. For
% instance, the representation of -2 is 65533 and the representation of 2 is 2.
% Adding these we get 65535 which is the representation of -0. We use this
% property to test the implementation of the '''negate/2''' function.

prop_negate(N) ->
  ?FORALL(I, choose(0, max_int(N)),
  begin
    <<CI:N>> = ip_checksum:negate(<<I:N>>),
    equals(negative_zero(N), I + CI)
  end).

% The property above is parameterized by the word size N. We'll want to test
% our properties for a range of different word sizes, so we define a general
% function to transform a parameterized property to a property choosing random
% word sizes.

random_word_size(Prop) ->
  ?FORALL(N, choose(1, 64), Prop(N)).

prop_negate() ->
  random_word_size(fun prop_negate/1).

% === Padding ===

% It is not clear from the specification presented above, but if you need to
% compute the checksum of a list of bytes in base 16, then there should be an
% even number of bytes. Likewise, if we would like to do ones complement in 32
% bits base, we would need to extend a sequence of bytes such that it is
% divisible by 4.

% Extending a bit string such that it is divisible by the base is called padding.
% We assume that you implemented a padding function that added the necessary
% bits, given a bit string. We assume this function to be implemented as
% '''ip_checksum:pad/1''' taking a bit string as argument and returning a new
% bit string which is an extended version with as many zero bits as needed.

prop_padding() ->
  random_word_size(fun prop_padding/1).

prop_padding(N) ->
  ?FORALL(BitString, bitstring(),
  begin
    Bits = bit_size(BitString),
    <<B:Bits/bits, Padded/bits>> = ip_checksum:pad(BitString,N),
    Zeros = bit_size(Padded),
    % If this property fails we need to know what the pad function actually
    % returned in order to understand what went wrong. This is what the
    % ?WHENFAIL macro is for.
    ?WHENFAIL(io:format("B      = ~w\nPadded = ~w\nZeros  = ~w\n",
                        [B, Padded, Zeros]),
      ((Bits + Zeros) rem N) == 0 andalso   % the new length is divisible by N
          B == BitString          andalso   % we don't change the bit string
          <<0:Zeros>> == Padded   andalso   % we pad with zeros
          Zeros < N                         % we don't pad more than we have to
    )
  end).

% Confident that the padding function works we can write a generator for
% correctly padded bit strings.
padded_bitstring(N) ->
  ?LET(Bits, bitstring(), ip_checksum:pad(Bits, N)).

% An alternative definition of this generator would not use the padding
% function, but rather first generate the length of the bit string and then
% pass that to the bit string generator (see below). The advantage of the former
% definition is that it behaves better when shrinking. The version below will
% regenerate the bit string everytime the length is getting shorter.
padded_bitstring_2(N) ->
  ?LET(Len, nat(), bitstring(N * Len)).

% === Ones complement sum ===

% The ones complement sum is computed by adding a number of words in ones
% complement representation. We assume this function to be implemented as
% '''ip_checksum:sum/2''' which takes a bit string as first argument and a
% word size as second argument. We assume that padding is done outside the
% sum function and only test that the function works for bit strings of
% which the length is divisible by the given word size.

% Because of our test driven development method, we have already tested the
% '''negate/1''' function and therefore trust this function in our property.
% Remember that adding the representations of a number and its negation yields
% -0. This is in fact also true if we use one's complement addition rather than
% simply adding the representations (which is not the same thing). So if we
% concatenate a bit string with the negation of its sum, the sum of the
% resulting bit string should be -0 if our implementation of '''sum/2''' is
% correct. By testing the sum function in this way we don't have to worry about
% specifying the intricacies of ones' complement arithmetic (except for the
% fact that X + (-X) = -0).

prop_sum() -> 
  random_word_size(fun prop_sum/1).

prop_sum(N) ->
  ?FORALL(Bin, padded_bitstring(N),
  begin
    Sum  = ip_checksum:sum(Bin, N),
    CSum = ip_checksum:negate(Sum),
    equals(ip_checksum:sum(<<CSum/bits, Bin/bits>>, N),
           <<(negative_zero(N)):N>>)
  end).

% === Checksum ===

% After computing ones' complement sum, one has to take the ones' complement of
% the result to compute the checksum. Of course, we have all ingredients in
% house to do so, but in case you implement both functions as one you would
% like to test the final result '''ip_checksum:checksum/2''' with a bit string
% and word size as arguments.

% We first test that the '''checksum/2''' function takes care of padding, by
% checking that padding the bitstring before passing it to '''checksum/2'''
% doesn't change the result.

prop_checksum_pad() ->
  random_word_size(fun prop_checksum_pad/1).

prop_checksum_pad(N) ->
  ?FORALL(Bits, bitstring(),
    equals(ip_checksum:checksum(Bits, N),
           ip_checksum:checksum(ip_checksum:pad(Bits, N), N))).

% We can test the '''checksum/2''' function in the same way as we tested
% '''sum/2''' above. Taking a bit string and prepending its checksum should
% result in a bit string whose checksum is zero. Here's why:
%
%   % definition of checksum
%   checksum(Bits) == -sum(Bits)
%
%   checksum(checksum(Bits) ++ Bits) == {def. of checksum}
%   -sum(-sum(Bits) ++ Bits)         == {sum(Xs ++ Ys) == sum(Xs) + sum(Ys)}
%   -(-sum(Bits) + sum(Bits))        == {adding -X and X}
%   -(-0)                            ==
%   0
%
% Note that due to padding, the property doesn't hold if we append the checksum
% rather than prepending it.

prop_checksum() ->
  random_word_size(fun prop_checksum/1).

prop_checksum(N) ->
  ?FORALL(Bin, bitstring(),
  begin
    Sum = ip_checksum:checksum(Bin, N),
    equals(ip_checksum:checksum(<<Sum/bits, Bin/bits>>, N),
           <<0:N>>)
  end).