Added valid and fixed padding.

[samuelemarro]

Using #16 as a starting point, I added support for both valid and fixed padding.
Fixed padding can be passed as Int64 (same padding for all edges), a tuple of size 2 (y_padding, x_padding) or a tuple of size 4 (top, bottom, left, right).
The implementation follows Tensorflow's conventions, but just to be sure I checked that it matches PyTorch's implementation too.
This is my first time working on MIPVerify, so I might have been a bit overzealous with the unit tests. If that's the case, I'll remove some of them.

Edit: passing -> padding

[vtjeng]

Thanks for the PR! I've described some suggested updates here.

In the meantime, I just wanted to understand a bit more about how you did the validation in Tensorflow and Pytorch --- would you share what you did, and perhaps an example set of commands corresponding to one of the unit tests you added?) It would be really helpful for other readers to have evidence that we're following the correct convention (I previously had an off-by-one issue when dealing with even-sized kernels).

[samuelemarro]

My original scripts were not exactly elegant, so here are two improved scripts to generate the convolution output.
This one's for Tensorflow:

import tensorflow as tf
import numpy as np

input_shape = [1, 5, 5, 1]
filter_shape = [3, 3, 1, 1]

# order='F' makes NumPy use column-major order, which is the same used by
# Julia
a = np.array(range(1, np.prod(input_shape) + 1)).reshape(input_shape, order='F')
a = tf.convert_to_tensor(a)

filter_ = np.ones(filter_shape)
stride = 1

# Standard padding types
# padding = 'VALID'
# padding = 'SAME'

# Padding in the form of [[0, 0], [pad_top, pad_bottom], [pad_left, pad_right], [0, 0]]
padding = [[0, 0], [1, 2], [3, 4], [0, 0]]

output = tf.nn.conv2d(a, filter_, stride, padding)

# This is the shape that is used to reshape raw_output to
# true_output
print(output.shape)

print('============')

# In the unit test, raw_output is transposed before being used.
# I followed the same convention, but this means that I first have to
# transpose Tensorflow's output so that the unit test will re-transpose it
# back to its original shape
raw_output = output.numpy().transpose()
print(raw_output)

# With all the extra dimensions, raw_output looks awful, so I
# squeeze it:
print(raw_output.squeeze())
print('============')

# To make it easier to copy to the unit tests, here's a small script:
for row in raw_output.squeeze():
    converted_row = [str(elem) for elem in row]
    print('\t'.join(converted_row), end=',\n')

# Depending on your console settings, some additional formatting might
# be necessary

And here's PyTorch's one. Note: PyTorch does not support "same" padding, so I didn't test it.

import torch
import torch.nn.functional as F
import numpy as np

input_shape = [1, 5, 5, 1]
filter_shape = [2, 3, 1, 1]

# dtype must be float because PyTorch does not support convolutions on integers
a = np.array(range(1, np.prod(input_shape) + 1), dtype=np.float).reshape(input_shape, order='F')

# PyTorch follows the BCHW format (channel-first)
a = a.transpose([0, 3, 1, 2])
a = torch.from_numpy(a)

# MIPVerify follows the filter format:
# (filter_height, filter_width, in_channels, out_channels)
# PyTorch expects the filter format:
# (out_channels, in_channels / groups, kernel_size[0], kernel_size[1])
# since groups=1, filter_height = kernel_size[0] and filter_width = kernel_size[1]
# (out_channels, in_channels, kernel_size[0], kernel_size[1])
torch_filter_shape = [filter_shape[3], filter_shape[2], filter_shape[0], filter_shape[1]]

filter_ = torch.from_numpy(np.ones(torch_filter_shape))

stride = 1
padding = (0, 0)

bias = torch.from_numpy(np.array([0])).long()

output = F.conv2d(a, filter_, bias, stride,
                        padding, 1, 1)

# Convert to a NumPy integer array
output = output.cpu().detach().int().numpy()

# Convert back to BHWC (channel-last)
output = output.transpose([0, 2, 3, 1])

print(output.shape)

# In the unit test, raw_output is transposed before being used.
# I followed the same convention, but this means that I first have to
# transpose PyTorch's output so that the unit test will re-transpose it
# back to its original shape
raw_output = output.transpose()
print(raw_output)
print('============')

# With all the extra dimensions, raw_output looks awful, so I
# squeeze it:
print(raw_output.squeeze())
print('============')

# To make it easier to copy to the unit tests, here's a small script:
for row in raw_output.squeeze():
    converted_row = [str(elem) for elem in row]
    print('\t'.join(converted_row), end=',\n')

[vtjeng]

Thank you for sharing the scripts (and spending the time to clean them up!) The comments are particularly helpful, and I'll use definitely be using it in the future if I'm trying to provide new functionality that matches the behavior on Pytorch. I might actually merge these scripts in to the repo as part of a later PR so that everything is fully repeatable.

[samuelemarro]

Glad to be of help!

[vtjeng]

codecov now erroneously thinks that coverage has dropped, but we manually confirm that the new tests added were run (268 -> 340).