Exploring the overlap between ISBNs and magic squares

isbn_magic_square_mashup.snt

# A Sentient program to encode ISBN-10s, ISBN-13s, their check
# digits and how they relate.

# Declare all parts of the ISBN including check digits.
int5 ten0, ten1, ten2, ten3, ten4, ten5, ten6, ten7, ten8;
int5 ten_check_digit, thirteen_check_digit;

# State that all digits must be between 0 and 9 inclusive aside
# from ISBN-10 check digits which can include 10.
invariant ten0 >= 0, ten0 <= 9;
invariant ten1 >= 0, ten1 <= 9;
invariant ten2 >= 0, ten2 <= 9;
invariant ten3 >= 0, ten3 <= 9;
invariant ten4 >= 0, ten4 <= 9;
invariant ten5 >= 0, ten5 <= 9;
invariant ten6 >= 0, ten6 <= 9;
invariant ten7 >= 0, ten7 <= 9;
invariant ten8 >= 0, ten8 <= 9;
invariant ten_check_digit >= 0, ten_check_digit <= 10;
invariant thirteen_check_digit >= 0, thirteen_check_digit <= 9;

# Collect all digits in an ISBN-10.
tenDigit = [
  ten0,
  ten1,
  ten2,
  ten3,
  ten4,
  ten5,
  ten6,
  ten7,
  ten8,
  ten_check_digit
];

# Declare how to verify ISBN-10s (including their check digits).
#
# 1. Add together each digit, multiplying by their index;
# 2. Take the result modulo 11;
# 3. State that the result must be 0.
ten_total  = ten0;
ten_total += ten1 * 2;
ten_total += ten2 * 3;
ten_total += ten3 * 4;
ten_total += ten4 * 5;
ten_total += ten5 * 6;
ten_total += ten6 * 7;
ten_total += ten7 * 8;
ten_total += ten8 * 9;
ten_total += ten_check_digit * 10;

invariant ten_total % 11 == 0;

# Declare how to verify ISBN-13s (including their check digit).
#
# 1. Add all even-numbered digits;
# 2. Add all odd-numbered digits and multiply by 3;
# 3. Add both sums together modulo 10;
# 4. State that the result must equal 0
even_digits  = 9;
even_digits += 8;
even_digits += ten1;
even_digits += ten3;
even_digits += ten5;
even_digits += ten7;
even_digits += thirteen_check_digit;

odd_digits  = 7;
odd_digits += ten0;
odd_digits += ten2;
odd_digits += ten4;
odd_digits += ten6;
odd_digits += ten8;

invariant (even_digits + odd_digits * 3) % 10 == 0;

# Collect together all the digits in an ISBN-13.
thirteenDigit = [
  9,
  7,
  8,
  ten0,
  ten1,
  ten2,
  ten3,
  ten4,
  ten5,
  ten6,
  ten7,
  ten8,
  thirteen_check_digit
];

# Expose thirteenDigit and tenDigit in the result.
#expose thirteenDigit, tenDigit;

#invariant tenDigit.last == thirteenDigit.last;
#invariant thirteenDigit == thirteenDigit.reverse;

array9<int4> numberOfDigits;
array9<int18> numbers;

offset = 0;
numbers.each(function^ (n, i) {
  d0, p = thirteenDigit.get(i + offset);
  d1, p = thirteenDigit.get(i + offset + 1);
  d2, p = thirteenDigit.get(i + offset + 2);
  d3, p = thirteenDigit.get(i + offset + 3);
  d4, p = thirteenDigit.get(i + offset + 4);

  digits = numberOfDigits[i];

  sum = d0;
  sum = digits >= 1 ? sum * 10 + d1 : sum;
  sum = digits >= 2 ? sum * 10 + d2 : sum;
  sum = digits >= 3 ? sum * 10 + d3 : sum;
  sum = digits >= 4 ? sum * 10 + d4 : sum;

  invariant n == sum;

  offset += digits;
});

numberOfDigits.each(function (d) {
  invariant !d.negative?;
});

invariant numberOfDigits.sum == 4;

square = [
  [numbers[0], numbers[1], numbers[2]],
  [numbers[3], numbers[4], numbers[5]],
  [numbers[6], numbers[7], numbers[8]]
];

function magic_square?(square, target) {
  magic = true;

  square.each(function^ (row) {
    magic &&= row.sum == target;
    magic &&= row.all?(*positive?);
  });

  square.transpose.each(function^ (column) {
    magic &&= column.sum == target;
  });

  left_diagonal = square.map(function (row, index) {
    return row[index];
  });

  right_diagonal = square.map(function (row, index) {
    return row.reverse[index];
  });

  magic &&= left_diagonal.sum == target;
  #magic &&= right_diagonal.sum == target;

  return magic;
};

int target;

invariant magic_square?(square, target);
invariant numbers.uniq?;

# The @mudge 'magic' criterion:
invariant tenDigit.last == thirteenDigit.last;

expose square, target;