Repository navigation
Conversation
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
Both reviews of png#3 found that parseFile_print concluded `∃ hd, parseFile (print doc) = some (hd, doc)`, which a reader that answers a fixed header, or swaps width and height, also meets. WFFull now takes the header as a parameter, `WFFull hd doc`, and parseFile_print concludes `parseFile (print doc) = some (hd, doc)` in Proofs/Header.lean, Spec.lean and Proofs/SpecProofs.lean. The proof is the old one without the `refine ⟨hd, ?_⟩` step. Checked outside the repo: the wrongRead probe from the review (every header replaced by 1x1 d8 t0 i0) and a reader that swaps width and height no longer meet the statement. Lean rejects the review's proof script, and both readers provably fail it on a 2x1 header. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
The PNG specification (third edition, 11.2) allows one IHDR chunk, and it comes first. parseFile accepted a later IHDR and `header` answered the first one's fields, as review 1 item 4 found. - headerOf answers none when any chunk after the first has type IHDR (new Png.isIHDR), so parseFile and the `header` request refuse the file. The chunk layer, `parse`, is unchanged and still reads a second IHDR as an ordinary chunk. - WFFull gains the matching clause: no chunk after the first has type IHDR. parseFile_print still holds, with the clause used to show the later chunks hold no IHDR. - Spec.rejects_second_ihdr pins the review's file (IHDR 1x1, IHDR 2x2, IDAT, IEND), checked with decide +kernel. - tests: a chunk order section with both cases (a second IHDR right after the first, and one after IDAT), each refused by `header` and read by `parse`, plus two IEND-with-data cases. - SPEC.md and README.md say so. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
tests/run_tests.py failed the axiom check only on a nonzero exit or a line count other than 4. It never read the axiom names, so a proof that came to depend on sorryAx still gave "Failures: 0" (review of 437849b). - The harness now reads each `#print axioms` line and fails on any axiom but propext, Classical.choice and Quot.sound, and on a theorem with no line. - Proofs/Verify.lean prints the axioms of the four headline theorems and of every theorem comparator.json names; the harness takes the list from comparator.json, so a new theorem cannot be left out. - A self-test runs the check on planted output first: a sorryAx, an axiom of a proof's own, and a missing line must each fail. Checked by hand: with one decide +kernel proof in SpecProofs.lean replaced by sorry, the harness exits 1 with "depends on sorryAx". Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
Review 1 item 3 and the review of 437849b: no theorem tied the rejection branches of parseIhdr to the reader, and README.md said the round trip and the table theorem covered rejection, which neither does. New theorems, each on propext and Quot.sound only: - Png.Proofs.parseIhdr_sound (Proofs/Header.lean): parseIhdr bs = some h → WFHeader h ∧ printIhdr h = bs. - Png.Proofs.parse_sound (Proofs/Sound.lean): the chunk parser accepts only the printed form of a well formed chunk list. - Png.Proofs.parseFile_sound (Proofs/Sound.lean): the file level read accepts only `print doc` for a doc that is WFFull with the header it returns. - parseIhdr_iff, parse_iff and parseFile_iff join each to its round trip. Spec.lean states the three soundness theorems as Spec.parse_sound, Spec.parseIhdr_sound and Spec.parseFile_sound, proved in Proofs/SpecProofs.lean and named in comparator.json. README.md and SPEC.md now say each reader is pinned to its rule in both directions, and the "not proved" list keeps only what is left: that the rules are the PNG specification's. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
Bar reviewer checklist step 4: definitions used only to give the statements meaning belong in the spec files, not the bar.toml [spec] code list. A code entry is pinned by name only, so WF, WFHeader or WFFull could be changed after an approval without changing the spec hash, and every statement over them would change meaning with it. - Spec/Defs.lean (namespace Spec) now holds iendChunk, WFChunk, WF, allowedPairs, WFHeader and WFFull, with their bodies unchanged, except that WFHeader states the depth rule as membership in allowedPairs instead of through the code's checkPair. The two are equal by checkPair_iff, which the proofs now use where they took checkPair before. - Png/Value.lean and Png/Header.lean keep only code. - bar.toml: Spec/Defs.lean joins the spec files; the moved names leave the code list; Png.isIHDR joins it, with the constructors and fields of Chunk and Ihdr that the spec definitions use, as the statement walk needs. zero-aska joins spec_authors, since this carry-forward changed the specification under that account. - lakefile.toml builds Spec by default, so `lake build` checks the challenge file compiles. check.py --offline: the statement walk reports nothing outside the spec files and the code list, and lake comparator --paranoid accepts all 22 theorems under every bundled kernel. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
Lean 4.35 deprecates if_pos, if_neg and if_false in favour of ite_eq_left, ite_eq_right and ite_false, which have the same statements. The build now warns only on the expected sorry in each statement of the challenge file, Spec.lean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
Review 1 item 5b and the review of 437849b: the header sections had no original-reader oracle, only the ALLOWED table in the harness. libpng 1.6.43 is installed here, so the harness now uses it. - tests/libpng_header.c reads a file with png_read_info ("info") or decodes it whole, image and all, through png_read_end ("full"), and answers the header fields in the shape `header` uses. libpng's default width and height limits (one million) are raised to 2^31 - 1, the PNG specification's cap. - run_tests.py builds it when a C compiler and libpng are present, and otherwise records the section as skipped. 389 files: the real files, the colour type and depth grid, every allowed pair with and without Adam7 at three sizes (with an all zero image), the header rule cases, 150 random headers, and the chunk order cases. Each must agree with `header` field for field, or both refuse, except for three named differences, each a rule this reader leaves out on purpose or where libpng is more lenient: indexed colour with no PLTE, an IEND chunk with data before IDAT, and a file that ends in an IEND chunk with data. - A header bounds section: width or height 2^31 - 1 is accepted (review 1 asked for cases at 2^31 - 1, 2^31 and 2^32 - 1). - The record gains the Inputs field check.py reads (every request of the sections up to the libpng comparison, which runs only where libpng is installed and is counted on its own line), and the README status line says "in progress", as check.py looks for. - SPEC.md says what an IEND chunk with data does: it is an ordinary chunk at both layers, so a file ending in one has no end and is refused, and one followed by a real IEND is read. README.md lists it, and libpng's two differences, under what is not proved. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
…actly README.md's account of WFFull now lists the single IHDR clause, and the reflow of one paragraph. SPEC.md and README.md say which IEND case libpng refuses (an IEND chunk with data before IDAT) and which it reads with a warning (a file ending in one), as the test record shows, and SPEC.md names Spec.parse_sound for the byte for byte reprint claim. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
The round trips and their converses tie each reader to its printer, but say nothing of the bytes the printer writes. So a change that swapped the width and the height in both printIhdr and parseIhdr kept the spec hash and met every statement, and the tool then answered 1080x1920 for a 1920x1080 file. New statements in Spec.lean, proved in Proofs/Layout.lean and Proofs/SpecProofs.lean: - Spec.print_layout: print writes the signature, then each chunk as its length, its four type bytes, its data, and its CRC-32, the length and the CRC four bytes big endian. - Spec.printIhdr_layout: printIhdr writes the width, then the height, four bytes big endian each, then bit depth, colour type, zero, zero, interlace. - Spec.isLetter_iff, Spec.ihdrType_eq, Spec.isIEND_iff: the letter test, the IHDR type bytes, and the IEND chunk test the rules use. - Spec.reads_real_file_header: the real 4x3 test file is read as width 4, height 3, depth 8, colour type 6, no interlace. - Spec.reads_header_1920x1080: the 13 bytes of a 1920x1080 header are read as width 1920 and height 1080. Four bytes big endian is Spec.bigEndian4, a new spec definition in Spec/Defs.lean. The parseFile_print docstring now says its guarantee is relative to printIhdr. comparator.json names 29 theorems. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
The harness reads the two accepted inputs from Spec.lean and checks the header each states three ways: its own big endian reading of the bytes (with zlib for the CRCs and the image size), the tool's header answer, and libpng decoding the whole file. The axiom check covers the four new Png.Proofs layout lemmas. The record is regenerated: 1,485 inputs, 0 failures. README.md and SPEC.md name the new theorems, say the round trips hold relative to the printers and that the layout theorems fix the bytes, and list under what is not proved that the layout is the PNG specification's and that the CRC-32 function is the standard one. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
The layout statements fixed the bytes the printers write, but the well formedness rules compare a chunk's type with `ihdrType` through `Chunk.typeBytes`, which is code no statement fixed. A change that made `typeBytes` answer I, H, D, R for a chunk typed A, A, A, A, and had the printer, the CRC, and the IEND test use the four bytes directly, kept every proof in RoundTrip, Header, Sound, and Layout building unchanged, and the readers then accepted a file whose first chunk is AAAA, not IHDR. - Spec.typeBytes_eq: a chunk's type bytes are its four type bytes in order. Proved by definition in Proofs/SpecProofs.lean. - Spec.iendChunk in Spec/Defs.lean names its fields, so its value does not depend on the order `Png.Chunk` declares them in. comparator.json names 30 theorems. README.md and SPEC.md name the new theorem. The test record is regenerated: 1,485 inputs, 0 failures. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
png#5 moved the proof modules under Png on main. This merge brings it in and moves what this carry-forward added the same way, so the whole tree follows the convention decided in mission#22: - Modules: Spec.lean and Spec/Defs.lean are now Png/Spec.lean and Png/Spec/Defs.lean (Png.Spec, Png.Spec.Defs). Header, Sound, Layout and SpecProofs join RoundTrip and Verify under Png/Proofs/, and Png/Proofs.lean imports all six. The top-level Proofs.lean is gone, as on main. - Names: every statement and spec definition is Png.Spec.<name>: the 30 theorems, and WFChunk, WF, WFHeader, WFFull, allowedPairs, bigEndian4 and iendChunk. The helper lemmas stay Png.Proofs.<name>, as on main. - lakefile.toml: the libraries are Png, PngSpec (root Png.Spec) and PngProofs (root Png.Proofs), all in defaultTargets. - comparator.json: challenge Png.Spec, solution Png.Proofs, and the 30 new names. bar.toml: [spec] files take the moved paths. - README.md, SPEC.md, the comments in the Lean files (two of them in Png/Value.lean and Png/Header.lean, comments only), and tests/run_tests.py name the new paths and theorem names. The README conflict with main is resolved to this branch's text, which already replaced the lines main changed. The statements are unchanged: #check with pp.all of all 30 theorems gives the same text as on 3c64230, up to line breaks, once Png.Spec. is read as Spec. tests/TEST-RESULTS.md is regenerated: the same counts, 1,485 inputs and 0 failures, under the new paths and names. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd
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.
Carries #3 (abu-aska, IHDR decoding) forward on
fdn-claude/png-ihdr-carry, based on current main (png#5 merged), with the spec and proofs laid out underPngas mission#22 decided. abu-aska's commits (c431ac2, 3442498, 437849b) are kept unchanged; png#3's head is an ancestor of this branch.What the slice does
Slice 1 (on main) reads and prints the PNG chunk layer. Slice 2, from png#3, decodes the IHDR header: width, height, bit depth, colour type and interlace, checked against the PNG validity rules (width and height in 1 to 2^31 - 1, compression and filter 0, interlace 0 or 1, the allowed colour type and depth pairs). It adds a file-level read,
parseFile, that refuses a second IHDR chunk.What the carry-forward changed, past png#3
WFFull hd doctakes the header as a parameter, soPng.Spec.parseFile_printnames the header the read must return, not just some header.parse_sound,parseIhdr_sound,parseFile_sound. Together with the round trips, each reader accepts exactly the printed forms of well formed values, so every rule in the well formedness predicates is a proved rejection rule.printIhdrandparseIhdrkept the spec hash and met every statement, and the tool then answered 1080x1920 for a 1920x1080 file. These statements close that:Png.Spec.print_layout: the chunk printer writes the signature, then each chunk as length, type bytes, data and CRC-32, with length and CRC four bytes big endian.Png.Spec.printIhdr_layout: the header printer writes width, then height, each four bytes big endian, then depth, colour type, 0, 0, interlace.Png.Spec.isLetter_iff,Png.Spec.ihdrType_eq,Png.Spec.typeBytes_eq,Png.Spec.isIEND_iff: the letters and type bytes the rules use.Png.Spec.bigEndian4is a new spec definition inPng/Spec/Defs.lean.Png.Spec.reads_header_1920x1080: the 13 bytes0,0,7,128,0,0,4,56,8,2,0,0,0are read as width 1920, height 1080.Png.Spec.reads_real_file_header: a real 4x3 file is read with its own header.Png/Spec.leanand checks them against its own big endian reading, against the tool'sheaderanswer, and against libpng.#print axiomsfor every named theorem and fails on anything beyondpropext,Classical.choice,Quot.sound.Mutants this rejects
printIhdrandparseIhdr. The old round trips and converses still prove, butprintIhdr_layoutand both accepted inputs are false; their negations are proved bydecide +kernel. With those three proofs left assorry,lake comparator --paranoidrejects the build withIllegal axiom detected: 'sorryAx'. The tests fail too, since the tool answers the swapped header.Chunk.typeBytesreading AAAA as IHDR. The printer, CRC and IEND test use the raw bytes. Every proof excepttypeBytes_eqstill builds, and the reader then accepts a file whose first chunk is AAAA.Png.Spec.typeBytes_eqis false under this mutant.Layout (mission#22)
Png/Spec.lean,Png/Spec/Defs.lean, andPng/Proofs/{RoundTrip,Header,Sound,Layout,SpecProofs,Verify}.lean.Png.Spec.<name>; helper lemmas stayPng.Proofs.<name>.Png,PngSpec(rootPng.Spec) andPngProofs(rootPng.Proofs).comparator.json: challengePng.Spec, solutionPng.Proofs, 30 theorems.#checkwithpp.allis identical up to whitespace oncePng.Spec.is read asSpec..Checks (on head 0b377f4)
lake build: clean (26 jobs). The onlysorryis inPng/Spec.lean, as expected.python3 tests/run_tests.py: 1,485 inputs, 0 failures; libpng 1.6.43 oracle.--offline --run-tests:24c8577c859bcf1bea958f84dd6ab788da851de7f52ac4d0acdac09f2dbd96ef.What is not proved
SPEC.mdstates it, and the tests compare against a strict oracle and against libpng.Png.Crc32.crc32is the standard CRC-32. It is tested against zlib, and pinned on single inputs byreads_real_file_headerandrejects_bad_crc.headeranswer, and the line handling inMain.lean. These are tested, not proved.Review
The spec needs approval from a reviewer who did not write it:
SPEC.md,Png/Spec.lean,Png/Spec/Defs.lean. Spec authors are abu-aska and zero-aska. This PR supersedes png#3.Generated by Claude Code