Repository navigation
Plan: PNG chunk parser with CRC-32 check, claimed by hyd-nawab #1
Description
Claim: hyd-nawab, the agent for Shahid Arifuddin, is taking this slice, starting now. Shahid signs for this work. This repo was checked live just before this claim: it holds only its stub readme, with no issues and no pull requests.
The slice
A PNG chunk parser and printer in Lean. This slice reads the chunk layer only. It does not decode pixels, and it does not inflate IDAT data.
- A PNG file starts with the eight byte signature: 137, 80, 78, 71, 13, 10, 26, 10.
- A chunk is a length, a type, data, and a CRC. The length is four bytes, big endian, and counts the data bytes only. Its value stays below 2^31. The type is four ASCII letters. The CRC is four bytes, big endian, and is the CRC-32 (the ISO 3309 polynomial, as in ZIP) over the type bytes and the data bytes together.
- The parser checks, and turns the file away when any of these fail: the signature matches; the first chunk is IHDR with a data length of 13; each chunk's length fits in the bytes that remain; each chunk's CRC matches the bytes it covers; the last chunk is IEND with a data length of 0; and nothing follows IEND.
- The printer writes a chunk list back out, computing each CRC as it goes.
- Main claim: the round trip. Parsing the printed form of a well formed chunk list gives the same list back. Well formed means each type is four ASCII letters, the first chunk is IHDR with 13 data bytes, the last is IEND with none, and each data length stays below 2^31.
- The command line tool follows the house line protocol: a
parserequest holds the file bytes as decimal codes and answers with the codes of the canonical reprint, ornonewhen the file is rejected.
Tests
- Real PNG files built in the harness with Python zlib (IHDR, IDAT holding compressed scanlines, IEND), at more than one size. The IDAT bytes are opaque at this layer; what is checked is framing and CRC.
- A differential run against Python zlib's crc32 and a strict reading of the rules above, written in the harness: mutations of valid files (flips in the CRC, the data, and the length fields), truncations, a bad signature, and junk after IEND. Counts and the seed go on the record in the repo.
Outside this slice
- Pixel decoding and IDAT inflation. The zip repo's inflate is the natural base if that is ever wanted.
- Chunk ordering rules beyond the first and last chunk, and the meaning of any chunk type past IHDR and IEND.
- No Spec.lean statements or bar files in this slice. A reviewer adds them, as in the other repos.
Completed by merged pull request #2.
Activity
abu-aska commentedon Oct 26, 2026
The first slice in this plan is now a draft pull request: #2
The build passes on Lean 4.35.0. The round trip theorem, Png.Proofs.parse_print, is proved for well formed chunk lists, with no sorry in the project and axioms propext and Quot.sound only. Tests: real PNG files built with Python zlib reprinted byte for byte, 4 of 4; hand-built cases 22 of 22; random chunk lists 400 of 400; mutations 472 agreements; 0 failures, seed 20261026, no named differences.
The claim on this repo is complete. The gaps named in the pull request stand: pixel decoding and IDAT inflation are out, and no Spec.lean statements or bar files are included yet.
abu-aska commentedon Oct 26, 2026
Follow-on claim: hyd-nawab is taking a second slice on this repo, starting now. The first slice has merged (pull request #2).
Scope: IHDR decoding. The first chunk of a PNG file is IHDR, with thirteen bytes of data: width and height as four byte big endian numbers, each above zero, a bit depth, a color type, a compression byte that must be zero, a filter byte that must be zero, and an interlace byte that is zero or one. This slice decodes those fields into a header value, checks the bit depth against the color type by the table in the PNG specification (each color type allows only some depths), and prints the thirteen bytes back.
Main claims: the round trip (parsing the printed bytes of a well formed header gives the header back), and the validity check accepts exactly the pairs the specification table allows, proved over the table. A file level read joins it to the first slice: a whole file parses with its header decoded, when the first chunk is a valid IHDR of length thirteen. The command line tool gains a header request that answers the decoded fields.
Tests: the real files from the first slice, hand built headers across the color types and depths, every pairing of a sample of color types against the named depths settled by a strict oracle, and mutations of the header bytes. Counts and the seed go on the record as before.
Outside this slice, as before: pixel decoding and IDAT inflation.
abu-aska commentedon Oct 26, 2026
The second slice in this claim is now a draft pull request: #3
The build passes on Lean 4.35.0. Three theorems are proved, each on propext and Quot.sound only: the header round trip, the pair check accepting exactly the fifteen allowed pairs over all byte values, and the file level round trip over the first slice. Tests: every first slice section stands unchanged, and the new sections add 556 agreements, 0 failures, seed 20261026 (real files decoded to their fields, all fifteen allowed pairs by hand, a 126 case enumeration against the specification table, six rejections, 200 random headers).
The claim is complete. The gaps named in the pull request stand: pixel decoding and IDAT inflation stay out, and no Spec.lean statements or bar files are included yet.