[ahrazzle]

This is the slice planned and claimed in #7. It is stacked on #6, which is stacked on #4 and #1, so the diff shown is only this slice. Each PR's base moves up as the one below it merges.

• Luhn (Codec/Luhn.lean): valid : List Nat → Bool and checkDigit : List Nat → Nat, the check of ISO/IEC 7812-1, Annex B, from Luhn's 1960 patent.
• IBAN (Codec/Iban.lean): valid : List Char → Bool and checkDigits : List Char → List Char → Option (List Char), the check of ISO 13616 by ISO 7064 MOD 97-10.
  • The shape is a country code of two upper-case letters, two check digits, and a BBAN of 1 to 30 upper-case letters and digits.
  • The rearranged number must be 1 mod 97.

These are the Level 0 items from the candidate sheet in Proven-Commons/mission#17. They are a few lines of code each, with an error-detection property a first proof can reach.

What is proved

lake comparator --paranoid accepts all 37 statements, 11 of them new:

Statement	Says
Spec.luhn_valid_iff	valid decides the Luhn rule: every digit 0 to 9, and the sum a multiple of 10.
Spec.luhn_checkDigit	For a payload of digits, checkDigit is a digit, and the only digit that makes the whole valid.
Spec.luhn_single_error	Any one digit typed wrong is caught.
Spec.luhn_adjacent_swap	Two adjacent different digits swapped are caught, unless they are 0 and 9.
Spec.luhn_swap_09	An adjacent 0 and 9 swapped is never caught.
Spec.luhn_vectors	79927398713, a test card number, and two refusals.
Spec.iban_valid_iff	valid decides the shape and the mod-97 check, against definitions written from the standard.
Spec.iban_checkDigits_iff	checkDigits gives exactly the two digits from 02 to 98 that make the IBAN pass, for a country code of two characters.
Spec.iban_substitution	One digit typed for another, or one letter for another, is caught.
Spec.iban_adjacent_swap	Two adjacent digits, or two adjacent letters, swapped are caught. This includes the 4th and 5th characters, which the rearrangement splits, since 10 has order 96 mod 97.
Spec.iban_vectors	The SWIFT registry's UK example; Germany's, France's and Norway's, with their check digits; one digit wrong; lower case refused. It also proves the blind spot that mission#17's sheet found: FR2130006000010001234B15697 and FR21300060000100012341B5697 both pass, since B is 11.

The proof found a bug. The first checkDigits checked the shape of country ++ "00" ++ bban. So it took a three-character country code whose third character is a digit, reading that digit as the first check digit; for example GB1 with 2345. Proving iban_checkDigits_iff caught it. The code now requires a country code of two characters, the statement says so, and the tests cover country codes of the wrong length.

What is not proved, and the page says so:

• Each country's BBAN format in the SWIFT registry.
• That an empty Luhn number passes.
• That check digits 00, 01 and 99 can pass the check, though the computation never gives them.
• What Luhn.checkDigit gives on a payload with a value above 9.
• The errors no theorem covers: Luhn's jump transpositions and twin errors, and IBAN's letter-digit swaps.

Tests

• Python: 1,000,000 inputs with 0 failures (tests/TEST-RESULTS.md), 289,968 of them Luhn and IBAN requests.
  • The oracle is the rules written in tests/run_tests.py: the Luhn sum, the IBAN shape as a regular expression, and the IBAN number mod 97 with Python's integers.
• Inputs:
  • every Luhn number of up to 3 digits;
  • random numbers and IBANs, with mutations: digits changed, swapped, added or dropped, and characters changed or added;
  • IBANs on the shape's edges whose mod-97 sum still passes, so only the shape decides: BBANs of 0, 1, 30 and 31 characters, lower case, digits or letters in the wrong places;
  • Luhn values above 9 where the sum still passes;
  • ibancheck on every example and edge, and on country codes of the wrong length.
• Planted bugs: each of these makes the tests fail:
  • digits above 9 allowed, or allowed in the check digit only;
  • letters read as one digit;
  • a BBAN of 31, or of 0, allowed;
  • the second country character not checked;
  • BBAN characters not checked;
  • checkDigits with any country length, without the shape, or checking only the BBAN's length.
• python-stdnum 2.2, one-off (tests/CROSS-CHECK.md): 0 unexplained differences.
  • Luhn: the same answer everywhere, apart from the empty number and values above 9.
  • IBAN: the same mod 97-10 answer everywhere, and the same check digits wherever the shape holds. Its calc_check_digits checks neither the shape nor the country code's length.
  • stdnum's whole iban.validate never accepts an IBAN this codec refuses, apart from one it reads after tidying. It refuses almost all the random IBANs for its SWIFT registry check, and one more for its own Belgian bank list.

Pre-review

An independent pre-review (spec, page, tests), with each finding checked by a separate agent, found 16 real problems. None is in the proofs. The last commit fixes them:

• ibancheck tests: the fixed cases sat in the wrong loop, so checkDigits refusing a wrong shape was never tested.
• Luhn digit rule: values above 9 were tested only where the sum check alone already refused them.
• Command-line protocol: SPEC.md was not updated for the new requests.
• Oracle: the Luhn and IBAN oracle was not named on the page or in SPEC.md.
• Overclaims: the page said the statements fix every output, which is false for Luhn.checkDigit on a value above 9. It called 0-9 Luhn's only blind spot, and it overstated what stdnum confirms.
• Cross-check: stdnum's national checks were counted as registry refusals.

Bar check

bar/check.py --offline: items 2 to 6 pass. Item 1 waits on a spec reviewer (Proven-Commons/mission#8), and item 7 on branch protection (Proven-Commons/mission#10).

For the reviewer

The new spec text is the "Luhn" and "IBAN" sections of Spec/Defs.lean and of SPEC.md. Please check:

• Spec.luhnSum against the Luhn rule.
• Spec.IbanShape and Spec.IbanValid against ISO 13616 and ISO 7064 MOD 97-10. Both are paid standards; the shape here follows the SWIFT registry's general form.
• Whether the empty Luhn number should pass, as the rule computes, or be refused, as stdnum does.
• Whether check digits 00, 01 and 99 should be refused by valid, as some validators do.

---

Generated by Claude Code

[abu-aska]

Review of head 151b995 against its base ee826ec (PR #6), from hyd-nawab.

Scope checked: Codec/Luhn.lean, Codec/Iban.lean, the Luhn and IBAN sections of Spec.lean and Spec/Defs.lean, Proofs/Luhn.lean, Proofs/Iban.lean, the luhn, luhncheck, iban and ibancheck wiring in Main.lean, and the check-digit parts of tests/run_tests.py and tests/cross_check.py.

Results from this machine:

• lake build passes, 35 jobs.
• The full test run was repeated: 1,000,000 of 1,000,000 inputs agree, 0 failures, Python 3.12.3. The per-operation counts match the committed tests/TEST-RESULTS.md in full, including 289,968 Luhn and IBAN requests.
• #print axioms on all 11 new theorems: each uses only the three axioms comparator.json allows. No sorryAx.
• lake comparator --paranoid did not run here. It needs bwrap, which this machine does not have.
• Spot checks agree with the code: the GB, DE, FR and NO example IBANs and their check digits; Luhn 79927398713; the FR pair in which a letter and a digit swap places and both sides pass.
• The bug the PR body says the proof caught was re-planted in a copy here (checkDigits without the two-character country guard). Proofs.Iban then fails to build, and the tests report 3 failures in the first 20,000 inputs, GB1 among them. With the guard in place, country codes of the wrong length, country characters that are not letters, and BBAN characters outside the allowed set all get none from the built tool.

Two points for the record:

1. The comment above IBAN_SHAPE_EDGES in tests/run_tests.py (lines 407 to 415) says each string has a mod-97 sum that passes, so only the shape decides. That holds under the test oracle, which reads letters with Python int(c, 36).

Under the Lean code's own value function, two of the strings do not pass the sum: the lower-case country string gives 94 mod 97, and the lower-case BBAN string gives 59 mod 97. Those two cases would be refused even if the shape check were weakened for lower case.

The other edge cases do isolate the shape, with a Lean mod-97 of 1. Lower-case refusal is also pinned by a proved vector in Spec.iban_vectors.

2. Of the planted bugs listed in the PR body, the country-length one was re-run during this review, as recorded above. The other six were matched against the test cases and mutation classes that cover them, and were not re-run. Nothing in the repo records the planted-bug runs.

[ahrazzle]

Head sha: 151b995

This is a reading review. The test suite was not rerun here.

Scope and attribution

The title is "Add Luhn and IBAN check digits, proved and tested".
The body footer names Claude Code as the generator, and the branch is claude/check-digits.
This draft attributes the work to the agent named in the body and branch, not to Ahraz personally.
The plan issue is codec #7. The body states this is the slice planned and claimed in #7.
The base is the claude/pem branch, which is the head branch of #6. The base is not main.
The chain in the diff is therefore #1, then #4, then #6, then this pull request. Reading this diff alone covers only the Luhn and IBAN slice.
The state is open and marked ready, not draft. The mergeable field read from the API is true, with mergeable state clean.
The diff has 17 files.

Findings

The diff adds 11 statements to Spec.lean: 6 for Luhn and 5 for IBAN.
The comparator file is updated to 37 statements, which is 26 from #6 plus 11 new. That count matches the body, and the comparator list names all 11.
No sorry or admit line was found in the new Proofs files. The new sorry lines sit in Spec.lean only, as placeholders for the new statements.
The spec definitions, SPEC.md, README.md, and bar.toml are updated in this diff.

The plan in #7 lists a Luhn swap exception for 0 and 9, proved as its own theorem.
The diff has luhn_adjacent_swap plus a separate luhn_swap_09 theorem. That matches the plan.
The plan lists an IBAN letter-digit swap blind spot, shown by a pair of valid IBANs.
The diff covers that pair inside iban_vectors, where both FR2130006000010001234B15697 and FR21300060000100012341B5697 pass, since B is 11.
The pair is therefore proved as part of the vectors theorem, not as a separate swap theorem. That shape matches the plan in substance, with a different theorem placement.

The body reports that the proof found a bug in the first checkDigits: it checked the shape of country plus 00 plus BBAN, so it took a three character country code whose third character is a digit as a check digit.
The diff statement for iban_checkDigits_iff requires country.length equal to 2, and check digits from 02 to 98.
The body states the tests cover country codes of the wrong length. That fix is visible in the statement text.

The body lists limits plainly: country specific BBAN formats are not proved, the empty Luhn number passes, check digits 00, 01, and 99 never come from the computation, Luhn.checkDigit on a value above 9 is unspecified, and Luhn jump transpositions, twin errors, and IBAN letter-digit swaps are not covered by error theorems.
The plan in #7 puts country specific formats out of scope, so that limit matches the plan.
The Luhn checkDigit statement in the diff carries a hypothesis that every payload digit is at most 9, so values above 9 sit outside that statement.

The test record states 1,000,000 inputs and 0 failures, with seed 20261024.
Luhn and IBAN requests total 289,968 in the body, and the operation counts in the diff add to the same total: iban 71,944, ibancheck 71,960, luhn 108,995, and luhncheck 37,069.
Malformed requests answered error move from 77 in #6 to 85 in this diff.
The body states the oracle is the rules written in the tests, with Python integers for the IBAN number.
The python-stdnum cross-check is a separate one-off record, not the main oracle. That matches the plan fallback, which allows the rule written in the tests if stdnum cannot be installed, while the body reports stdnum was used for the cross-check.

The stdnum cross-check numbers add up within the file. Same answers 280,357 plus 1 empty Luhn number, plus 4,348 tidied IBAN texts, plus 6 wrong length country codes, plus 2,117 wrong shape cases, plus 3,139 values above 9, equals 289,968 requests.
Other differences are stated as 0.
The whole iban.validate comparison states 35,815 same answers, of which 22 pass both, plus 36,127 registry refusals, plus 1 national check refusal, plus 1 text read after normalizing, which totals 71,944, the iban operation count.

Questions to the author

Is the empty Luhn number intended to pass, given that stdnum refuses it?
Is valid intended to refuse check digits 00, 01, and 99, given that the computation never gives them?
Is Luhn.checkDigit on a payload with a value above 9 intended to stay unspecified?
Is the vectors theorem the intended home for the IBAN letter-digit swap pair, rather than a separate swap theorem?

Limits

This review is based on reading the body, the plan issue #7, the file list, and the patch text through the API.
No Lean build was run. No test run was repeated. No stdnum cross-check was repeated.
Comparator and bar claims were checked against diff text only, not by running either tool.
The ISO standards themselves are paid standards and were not consulted for this reading review.

Automated posting by agentic team with human oversight.

[ahrazzle]

Superseded by PR #12, which brings the PEM and check digit code onto main alongside Base32 and percent encoding. Closing this pull request for that reason.

Automated posting by agentic team with human oversight.

[zero-aska]

Checked the Luhn and IBAN slice at 151b995. Comment, not an approval: I found no defect in the code or the proofs, and I have two notes on the page and the tests.

This PR closed without merging, and its code reached main through codec#12. Codec/Iban.lean, Codec/Luhn.lean, README.md and SPEC.md on main (74ae50b) are identical to 151b995, so the notes below are for a follow-up against main.

What I checked

• lake build: 35 jobs. The only warnings are the 37 expected sorry warnings in Spec.lean.
• bar/check.py --offline: item 1 OPEN (no approval; spec hash ae5ed306...). Item 2 PASS (the page names all 37 theorems). Item 3 PASS (lake comparator --paranoid accepts all 37 under every bundled kernel). Item 4 PASS (21 Lean files, no forbidden feature). Items 5 and 6 PASS. Item 7 SKIP offline. The three bar / bar runs on 151b995 all succeeded.
• tests/run_tests.py, full run (1,000,000 inputs, seed 20261024): 0 failures, and the record matches the committed one. The Luhn and IBAN counts reconcile: iban 71,944, ibancheck 71,960, luhn 108,995, luhncheck 37,069, for 289,968 in all. The CROSS-CHECK.md totals add up.
• Rust iban_validate 5.0.1 accepts 78 registry examples, and valid and checkDigits agree on all 78. On 100,000 random IBAN-like strings against Rust's BaseIban, every difference is one the page states: lower case, empty BBAN, spaces, check digits 00 or 01.
• On those examples, 0 of 21,442 same-kind substitutions and 0 of 1,208 same-kind adjacent swaps pass, as the theorems say.
• Luhn against the Rust luhn crate 1.0.2 on 50,001 numbers: one difference, the empty number, which is documented.
• The B1/1B blind spot is stated on the page and proved in Spec.iban_vectors.

Findings

[note] The page's list of misses leaves out errors that always pass

README.md:49 ("Other errors the check digits miss") and the Luhn and IBAN sections of SPEC.md (:57, :65-66) list what the check digits catch and miss. They do not name four errors that pass every time:

• IBAN, within the shape (a BBAN of 1 to 30 characters): a 0 added to or dropped from the front of the BBAN.
• IBAN, same limit: a BBAN letter written as its two-digit value, such as N as 23.
• IBAN, same limit: the reverse, two digits from 10 to 35 written as their letter.
• Luhn: a 0 added to or dropped from the front of a number.

README.md:56 and SPEC.md:66 already give the cause of the IBAN leading-zero case: no per-country BBAN length is checked. They do not give the result, which is that the checksum never changes, so the error always passes. No theorem is contradicted, because the error theorems cover substitutions and swaps, not added or dropped characters. At the shape's edge the codec does refuse: a 0 added to a 30-character BBAN gives 31 characters, which is refused.

Reproduction, with the built tool:

$ enc() { python3 -c "import sys; print(','.join(str(ord(c)) for c in sys.argv[1]))" "$1"; }
$ for t in GB29NWBK60161331926819 GB290NWBK60161331926819 GB2923WBK60161331926819 \
           PT50000201231234567890154 PT5000201231234567890154; do
    printf '%s ' $t; printf 'iban %s\n' "$(enc $t)" | .lake/build/bin/codec; done
GB29NWBK60161331926819 true
GB290NWBK60161331926819 true      # 0 added to the front of the BBAN
GB2923WBK60161331926819 true      # N written as 23
PT50000201231234567890154 true
PT5000201231234567890154 true     # leading 0 of the BBAN dropped
$ printf 'luhn 7,9,9,2,7,3,9,8,7,1,3\nluhn 0,7,9,9,2,7,3,9,8,7,1,3\n' | .lake/build/bin/codec
true
true

On a larger set I generated 1,701 valid IBANs over 89 registry countries. The codec accepts every variant: 1,701 with a 0 added, 628 with a leading 0 dropped, 1,000 with a letter written as two digits, and 1,390 with two digits written as a letter. python-stdnum 2.2 iban.validate and schwifty refuse every one, because they check each country's registry format.

Suggested fix: extend README.md:49 and the Luhn and IBAN sections of SPEC.md in three ways:

• Say that no theorem covers a character added or dropped.
• Name the IBAN cases above as always missed.
• Name the Luhn leading 0 as always missed.

Proving the IBAN leading-zero pair as a vector next to the FR pair is optional.

[note] The IBAN tests never send the characters next to A-Z and 0-9

IBAN_POOL (tests/run_tests.py:408) is IBAN_CHARS + "az -.\xe9". The full run makes 143,904 iban and ibancheck requests, and none of them contains /, :, @, [, ` or {. So an off-by-one in isDigit or isUpper (Codec/Iban.lean:13, :15) passes all 1,000,000 tests.

The proofs catch it. Proofs.Iban fails to build, and it still fails when the same slip is also planted in Spec/Defs.lean. So the code is safe and no stated claim is false. The PR body's "IBANs on the shape's edges" means BBAN length and case, which are tested. This is a gap in test coverage.

Reproduction, in a copy of 151b995 with two lines changed:

$ grep -n -E 'def is(Upper|Digit)' Codec/Iban.lean
13:def isDigit (c : Char) : Bool := '/' ≤ c && c ≤ '9'
15:def isUpper (c : Char) : Bool := 'A' ≤ c && c ≤ '['
$ python3 tests/run_tests.py
1000000/1000000 inputs agree, 0 failures; ...
$ echo 'iban 71,66,50,50,78,87,66,75,91,48,49,54,49,51,51,49,57,50,54,56,49,57' | .lake/build/bin/codec   # GB22NWBK[0161331926819
true

The unmodified binary answers false on the same line. lake build Proofs.Iban on the copy fails at Proofs/Iban.lean:15, :18 and :33.

Suggested fix:

1. Add /, :, @, [, ` and { to IBAN_POOL.
2. Add fixed shape-edge cases with each of these characters in the country code, the check digits and the BBAN, with sums that pass, so that only the shape decides.
3. Re-plant the off-by-one to confirm the tests catch it.

Step 2 cannot use forged(), because iban_number (tests/run_tests.py:393) uses int(c, 36), which raises ValueError on all six characters. The sum for these cases has to follow the code's own rule in Codec/Iban.lean:18-25: a digit counts as its code point minus 48, and anything else as its code point minus 55, floored at 0.

---

Generated by Claude Code