Repository navigation
Bring PEM and check digits onto main - #12
Merged
Merged
Conversation
Codec.Pem.encode writes the strict form of RFC 7468 (Figure 3): the BEGIN line, the base 64 of the data in lines of 64 characters, the END line with the same label, each line ending in LF. It refuses a label the `label` rule does not allow. Codec.Pem.decode reads exactly one message in that form, with each line ending in LF, CR or CR LF, and refuses anything else: a different END label, blanks, headers, text around the message, other line lengths, and base 64 that is not exactly the encoding of the data. The spec writes the label rule, `eol`, the lines of a message and the strict form from the RFC's ABNF, and settles two points it leaves open: empty data is the two boundary lines alone, as Go and Python write it, and the base 64 is exactly codec's. Four statements, all proved: Spec.pem_encode_iff, Spec.pem_decode_iff, Spec.pem_decode_encode, and Spec.pem_vectors, which includes RFC 7468's Figure 15 written exactly as the RFC prints it. lake comparator --paranoid accepts all 26 theorems. The differential tests run 1,000,000 inputs, 135,034 of them PEM, with 0 failures, against ssl.DER_cert_to_PEM_cert and an encoder and strict parser written from the ABNF; eight planted bugs each make them fail. A one-off check against Go's encoding/pem finds no difference beyond Go's lax reading, its writing of any label, and its not taking a CR alone as a line end. Plan and claim: #5. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
From an independent pre-review: - The page said the encoder writes, and the decoder reads, "exactly the strict form". For empty data, which that form cannot express, both use the BEGIN and END lines alone; the claims and Spec.lean's docstrings now say so. The page also says that with LF line ends only the lax form allows that text, and that the standard form's text for empty data is refused. Figure 1 is the standard form, not a lax one. - The last line of base 64 is at most 64 characters, not always shorter. - SPEC.md's paragraph on valid inputs and its description of the tool now cover PEM, and Spec/Defs.lean's header names its one use of code, Base64.encode, which the base 64 statements pin down. - The page and the record name the PEM oracle as it is: an encoder and strict parser written in the tests from RFC 7468. Where that parser accepts a certificate, Python's ssl.PEM_cert_to_DER_cert must now read the same data. - The labels `,`, `A,B` and `A:B` join the tests, and `,` and `:` the mutations; Spec.pem_vectors gains `A,B`. An off-by-one at `,` in the label rule now fails both the tests and the proofs. - Go refuses a message with empty data under a label with `:`, taking the END line for a header; the cross-check counts it and the page names it, and its claim is scoped to the texts it tried. lake comparator --paranoid accepts all 26 theorems; 1,000,000 inputs, 0 failures. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Codec.Luhn and Codec.Iban, their spec in Spec/Defs.lean, eleven statements in Spec.lean, the tool's luhn, luhncheck, iban and ibancheck requests, the tests (1,000,000 inputs, 0 failures), a cross-check with python-stdnum, and the page. The Luhn proofs are done. The IBAN statements other than the vectors still end in sorry, so lake comparator fails on this commit; the proofs are being written and land next. Plan and claim: #7. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The IBAN statements are now proved, with no sorry left, and `lake comparator --paranoid` accepts all 37 theorems. Proving iban_checkDigits_iff found a bug: `checkDigits` checked the shape of country ++ "00" ++ bban, so a three-character country code whose third character is a digit passed, its digit read as the first of the check digits. `checkDigits` now requires a country code of two characters, and the statement says so. Planted bugs that the tests missed (digits above 9 in a Luhn number, a BBAN of 31 or of 0 characters, a second country character that is not a letter, BBAN characters not checked) are now caught: the tests add IBANs on the shape's edges whose mod-97 sum passes, so only the shape decides, and Luhn numbers with a value above 9. The cross-check counts the two kinds of request whose stdnum form is a different question. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
An independent pre-review (spec, page, tests), each finding checked by a separate agent, found 16 real problems. None is in the proofs. Tests: - The `ibancheck` cases for each example and shape edge sat in the wrong loop, so `checkDigits` refusing a wrong shape was never tested. They now run, with an empty BBAN, one of 31 characters, lower case, and digits or a dash in the country code, and mutated IBANs go to `ibancheck` too. - Luhn values above 9 now also come where the sum still passes, at a place doubled and not, so only the digit rule decides. - IBAN shape edges now put letters in the check-digit places, and `ibancheck` has malformed and surrogate requests. Cross-check: stdnum's own national checks are counted apart from the SWIFT registry, `ibancheck` shapes stdnum does not check get their own count, and the page says what stdnum confirms and what it does not. Page and SPEC.md: the Luhn and IBAN oracle is named where the others are; SPEC.md's command-line paragraph covers `ibancheck`, `luhn`, `luhncheck` and `iban`; `Luhn.checkDigit` is pinned down only for a payload of digits, and both say so; Luhn's adjacent-swap blind spot is no longer called its only one, and the errors no theorem covers are listed. `Spec.iban_vectors` gains the check digits of the German and French examples. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
This was referenced Oct 28, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Bring PEM and check digits onto main, alongside Base32 and percent encoding.
Main holds the initial import, percent encoding, and Base32. PR #6 merged PEM into the percent encoding branch, and PR #8, still open, holds check digits on top of PEM. Neither slice is on main. This change merges the check digits branch tip into main, resolving the two test file conflicts by keeping both the Base32 and percent sections and both the PEM and check digit oracles.
Local verification: Lean build passes, 38 jobs, with sorry only in Spec.lean as statement placeholders. The combined test run gives 1000000 inputs, 0 failures, with b32, pct, pem, luhn, and iban operations present. The combined TEST-RESULTS.md is included.