Plan: check digits, Luhn and IBAN (ISO 7064 MOD 97-10), claimed by Claude #7

Claim: Claude, an AI agent, is taking this, starting now. Its pull requests come from the ahrazzle account. Mission#17 proposes these for codec as Level 0 items: short code with an error-detection property a first proof can reach. No one else has claimed them.

Why

Check digits guard card numbers and bank account numbers against typing errors. Each scheme's property is easy to state, and each has a known blind spot. That suits the academy: one proof where the property holds, and one theorem where it fails.

Luhn

The check digit of card numbers (ISO/IEC 7812-1) and many identifiers, from Luhn's 1960 patent.

• Codec.Luhn.valid : List Nat → Bool and Codec.Luhn.checkDigit : List Nat → Nat.
• Statements:
  • valid decides the Luhn sum, written in the spec from the rule: double every second digit from the right, subtract 9 from any result above 9, and require a sum that is a multiple of 10.
  • The check digit is the one digit that makes a payload valid.
  • Every single-digit error is caught.
  • Every swap of two adjacent different digits is caught, except 09 and 90.
  • That exception is proved as its own theorem.

IBAN

The check digits of ISO 13616, by ISO 7064 MOD 97-10.

• Codec.Iban.valid : List Char → Bool checks:
  • the shape: two letters, two digits, then up to 30 letters or digits;
  • the check digits: move the first four characters to the end, write each letter as 10 to 35, and read the whole as a number that must be 1 mod 97.
• Codec.Iban.checkDigits computes the two digits for a country code and a BBAN.
• Statements:
  • valid decides the rule as the spec writes it.
  • The computed digits make the IBAN valid, and they are the only digits from 02 to 98 that do.
  • A substitution of one digit for another digit is caught, and so is one of a letter for another letter.
  • A swap of two adjacent digits, or of two adjacent letters, is caught.
  • A swap of a letter and a digit is not always caught: a theorem shows a pair of valid IBANs that differ only by such a swap. One such pair is FR2130006000010001234B15697 and FR21300060000100012341B5697, as mission#17 found.
• Country-specific lengths and formats (the SWIFT registry) are out of scope.

Tests

• Luhn: differential tests against python-stdnum's luhn, if it can be installed, else against the rule written in the tests. All single-digit errors and adjacent swaps are run on random numbers.
• IBAN: differential tests against python-stdnum's iban.is_valid where available, against iso7064.mod_97_10, and against the IBAN examples SWIFT publishes.

It stacks on #6.

Completed by merged pull request #12.