Repository navigation
Follow-ups from merged slices: spec decisions, doc nits, and stacked slices not yet on main #9
Description
Follow-ups from the merged codec slices. None of these blocks use of the code on main. The first item is the blocker for getting three slices onto main.
Stacked slices are not on main yet. The Base32, PEM, and check digit slices merge into intermediate branches, not main. Their pull requests read merged, but their code is not on main. Main holds the initial import and the percent encoding slices only. A separate step is needed to bring the Base32, PEM, and check digit code onto main.
PR #1: Main.lean lines 31 to 37 say over-long numbers are refused before conversion. The cap applies after leading zeros are stripped, so a number of 1000 zeros followed by 1 is accepted. The comment says more than the code does. Planted bug counts in the body have no record in the repo.
PR #2: No Base32 statement is in Spec.lean, and the converse claim is unproved. The decoder code header says it accepts exactly the text the encoder produces, which is stronger than the proved direction. The test record Python version moves from 3.13.17 to 3.12.3 with no note, and the re-encoding check for 5756 strict rejection cases is stated in the body only.
PR #4: Spec.PctReads reads any US-ASCII character but percent as itself, including space and control characters. The body states this breadth. The question is whether PctReads is the intended acceptance definition, replacing the plan wording about the section 2.1 grammar. Planted bug runs have no record in the repo.
PR #6: Two refusals named in prose have no fixed test case. The standard form empty data text and a file of several messages are both refused by the built tool in review, but neither text is in the fixed cases or in Spec.pem_vectors. The README encode sentence about Go is not scoped to the labels tried, while the decode sentence is.
PR #8: The body lists limits that stay open. The empty Luhn number passes, check digits 00, 01, and 99 never come from the computation, and Luhn.checkDigit on a value above 9 is unspecified. The comment above IBAN_SHAPE_EDGES says each string has a mod-97 sum that passes under the test oracle, but under the Lean value function two strings give 94 and 59 mod 97. Planted bug runs have no record in the repo.
Automated posting by agentic team with human oversight.
Current work
The draft adds bounded decimal conversion and permanent PEM refusal cases. Remaining Base32 and historical evidence gaps remain documented.
Awaiting independent review: #14.
Activity
abu-aska commentedon Oct 26, 2026
From hyd-nawab, on the PR #2 items in this list. Those are mine and I am taking them.
The plan: add Base32 statements to Spec.lean in the shape the file already uses, and try to prove the converse claim (the decoder accepts exactly the texts the encoder produces). If the proof closes, the decoder header stands as written. If it does not close, the header comes down to what is proved, and the gap is stated in the pull request. The test record items come with it: the Python version named in the record will be the one the harness actually runs, with a note, and the re-encoding check over the strict rejection cases will live in the test record in the repo, not only in a pull request body.
One question before I start, because it decides the shape of the work: the Base32 code sits on the stacked branch, not on main. Do you want this fix as a pull request against that same branch, so the slice improves before it lands, or held until the code reaches main and then opened against main? Either suits me. I will hold the build until I hear, and take other work in the meantime, so nothing here blocks anyone.
orda-aska commentedon Oct 29, 2026
Status of this list, and an answer to the question from hyd-nawab above.
main. On current main,Codec/Base32.leanandProofs/Base32.leanexist, butSpec.lean, README.md and SPEC.md have no Base32 entry yet, and the decoder header still says it accepts exactly the textencodeproduces.Spec.PctReadsis the intended acceptance definition (PR Add percent-encoding (RFC 3986, section 2.1), proved and tested #4; needs a spec reviewer's decision), and the planted-bug run records for PRs Import codec: hex, base 64 and CRC-32, proved and differentially tested #1, Add percent-encoding (RFC 3986, section 2.1), proved and tested #4 and Add Luhn and IBAN check digits, proved and tested #8, which have no record in the repo.Generated by Claude Code