From c431ac28ef6732ae7ba2aec452a0c911e4ff7c6d Mon Sep 17 00:00:00 2001 From: shah Date: Mon, 26 Oct 2026 12:13:22 -0500 Subject: [PATCH 1/3] Add PNG chunk parser and printer, with proved round trip --- Main.lean | 34 +++++- Png.lean | 1 + Png/Header.lean | 141 +++++++++++++++++++++++ Proofs.lean | 1 + Proofs/Header.lean | 139 ++++++++++++++++++++++ Proofs/Verify.lean | 4 + README.md | 14 ++- SPEC.md | 49 +++++++- tests/TEST-RESULTS.md | 18 ++- tests/run_tests.py | 262 +++++++++++++++++++++++++++++++++++++++++- 10 files changed, 637 insertions(+), 26 deletions(-) create mode 100644 Png/Header.lean create mode 100644 Proofs/Header.lean diff --git a/Main.lean b/Main.lean index 188deba..e0c810b 100644 --- a/Main.lean +++ b/Main.lean @@ -7,10 +7,18 @@ parse 137,80,78,... prints ok:137,80,78,... or none - The one operation is `parse`. Its input is the byte codes of a - PNG file. Its answer is `ok:` and the byte codes of the - canonical reprint of the parsed chunk list, or `none` when the - file is rejected. + The operations are `parse` and `header`. The input of each is + the byte codes of a PNG file. `parse` answers `ok:` and the + byte codes of the canonical reprint of the parsed chunk list, + or `none` when the file is rejected. `header` reads the file + at both layers, the chunk list and the IHDR header decoded + from the first chunk's data (slice 2, `Png/Header.lean`), and + answers `ok:` and the codes of a text line naming the header + fields: the width, an `x`, the height, then ` d` and the bit + depth, ` t` and the colour type, ` i` and the interlace + method, as in `1920x1080 d8 t6 i0`. It answers `none` when + the file is rejected at either layer. The codes are the + character codes of that text. A request is an operation, then optionally one space and its numbers; with no numbers after the space, the input is empty. A @@ -48,6 +56,17 @@ def toBytes (ns : List Nat) : Option (List UInt8) := def showCodes (bs : List UInt8) : String := ",".intercalate (bs.map fun b => toString b.toNat) +/-- The byte codes of a text: the code of each character. The + texts built here hold digits, letters, and spaces only, so + every code is a byte. -/ +def textCodes (s : String) : List UInt8 := + s.toList.map fun c => c.toNat.toUInt8 + +/-- The header line: the fields of a decoded IHDR header as one + text, in the shape `1920x1080 d8 t6 i0`. -/ +def headerText (h : Ihdr) : String := + s!"{h.width}x{h.height} d{h.bitDepth.toNat} t{h.colorType.toNat} i{h.interlace.toNat}" + /-- The answer to one request, or `none` when the request is malformed. -/ def answer (op : String) (ns : List Nat) : Option String := @@ -59,6 +78,13 @@ def answer (op : String) (ns : List Nat) : Option String := match parse bs with | some v => some ("ok:" ++ showCodes (print v)) | none => some "none" + | "header" => + match toBytes ns with + | none => none + | some bs => + match parseFile bs with + | some (h, _) => some ("ok:" ++ showCodes (textCodes (headerText h))) + | none => some "none" | _ => none /-- The answer to one line: an operation, then optionally one space diff --git a/Png.lean b/Png.lean index e4d85f9..8da7389 100644 --- a/Png.lean +++ b/Png.lean @@ -1,3 +1,4 @@ import Png.Crc32 import Png.Value import Png.Parse +import Png.Header diff --git a/Png/Header.lean b/Png/Header.lean new file mode 100644 index 0000000..4178d74 --- /dev/null +++ b/Png/Header.lean @@ -0,0 +1,141 @@ +/- + Slice 2: the IHDR header, decoded. Slice 1 reads the chunk + layer and checks that the first chunk has type IHDR and 13 + data bytes; it does not look inside those bytes. This file + reads them. + + The 13 bytes hold: the width and the height, four bytes each, + big endian; then the bit depth, the colour type, the + compression method, the filter method, and the interlace + method, one byte each. + + The compression and filter bytes carry no choice in PNG: each + must be zero. So the header value does not hold them. They are + checked on reading and written as zero on printing. The + interlace byte is 0 (no interlace) or 1 (Adam7), and is held. + + A header is accepted only when the width and the height are + both above zero, the compression and filter bytes are zero, + the interlace byte is 0 or 1, and the bit depth is one the + colour type allows. The allowed pairs are the ones the PNG + specification names: + + colour type 0 (greyscale): depths 1, 2, 4, 8, 16 + colour type 2 (truecolour): depths 8, 16 + colour type 3 (indexed colour): depths 1, 2, 4, 8 + colour type 4 (greyscale, alpha): depths 8, 16 + colour type 6 (truecolour, alpha): depths 8, 16 + + Colour types other than 0, 2, 3, 4, 6 are not PNG colour + types, and allow no depth. +-/ + +import Png.Parse + +namespace Png + +/-- The decoded IHDR header: width and height as numbers, the + bit depth, the colour type, and the interlace method as + bytes. The compression and filter bytes are not held: each + is zero in every accepted file, and printing writes zero. -/ +structure Ihdr where + width : Nat + height : Nat + bitDepth : UInt8 + colorType : UInt8 + interlace : UInt8 + deriving DecidableEq, Repr + +/-- The bit depths a colour type allows, by the colour type's + number. A number that is not a PNG colour type allows none. -/ +def allowedDepths (ct : Nat) : List Nat := + if ct = 0 then [1, 2, 4, 8, 16] + else if ct = 2 then [8, 16] + else if ct = 3 then [1, 2, 4, 8] + else if ct = 4 then [8, 16] + else if ct = 6 then [8, 16] + else [] + +/-- Does this depth go with this colour type? The two numbers + are the byte values. -/ +def pairAllowed (ct bd : Nat) : Bool := + decide (bd ∈ allowedDepths ct) + +/-- The allowed (colour type, bit depth) pairs, written out in + full. The checker above is built from the per-type table; + the proof in `Proofs/Header.lean` shows the two agree on + every colour type byte and every bit depth byte. -/ +def allowedPairs : List (Nat × Nat) := + [(0, 1), (0, 2), (0, 4), (0, 8), (0, 16), + (2, 8), (2, 16), + (3, 1), (3, 2), (3, 4), (3, 8), + (4, 8), (4, 16), + (6, 8), (6, 16)] + +/-- Does this bit depth go with this colour type? The two + arguments are the file's bytes. -/ +def checkPair (ct bd : UInt8) : Bool := pairAllowed ct.toNat bd.toNat + +/-- A header is well formed when the width and the height are + above zero and below 2^32, the interlace byte is 0 or 1, and + the bit depth is one the colour type allows. -/ +def WFHeader (h : Ihdr) : Prop := + 0 < h.width ∧ h.width < 4294967296 ∧ + 0 < h.height ∧ h.height < 4294967296 ∧ + (h.interlace = 0 ∨ h.interlace = 1) ∧ + checkPair h.colorType h.bitDepth = true + +/-- The 13 IHDR data bytes of a header: width and height big + endian, then bit depth, colour type, compression zero, + filter zero, interlace. -/ +def printIhdr (h : Ihdr) : List UInt8 := + be32 h.width ++ be32 h.height ++ [h.bitDepth, h.colorType, 0, 0, h.interlace] + +/-- Read 13 bytes as a header. Anything but exactly 13 bytes is + rejected, and so is a header that breaks any of the rules at + the top of this file: a width or height of zero, a nonzero + compression or filter byte, an interlace byte above 1, or a + bit depth the colour type does not allow. -/ +def parseIhdr (bs : List UInt8) : Option Ihdr := + match bs with + | w1 :: w2 :: w3 :: w4 :: h1 :: h2 :: h3 :: h4 :: bd :: ct :: comp :: filt :: int :: rest => + if rest ≠ [] then none + else if u32 w1 w2 w3 w4 = 0 ∨ u32 h1 h2 h3 h4 = 0 then none + else if comp ≠ 0 ∨ filt ≠ 0 then none + else if int > 1 then none + else if checkPair ct bd then + some ⟨u32 w1 w2 w3 w4, u32 h1 h2 h3 h4, bd, ct, int⟩ + else none + | _ => none + +/-- The decoded header of a chunk list: the first chunk's data + read as a header, or `none` when there is no first chunk or + its data does not read as one. -/ +def headerOf (doc : Doc) : Option Ihdr := + match doc with + | c :: _ => parseIhdr c.data + | [] => none + +/-- Read a whole file at both layers: the chunk list of slice 1, + and the header decoded from the first chunk's data. A file + whose first chunk is not a valid IHDR, in the slice 2 sense, + is rejected here even when slice 1 accepts it. -/ +def parseFile (bs : List UInt8) : Option (Ihdr × Doc) := + match parse bs with + | some doc => (headerOf doc).map fun h => (h, doc) + | none => none + +/-- A document is fully well formed when it is well formed at + the chunk layer (the `WF` of slice 1), its first chunk's + data is the printed form of some header, and that header is + well formed. Stated with the witnesses out, in the shape of + `WF`. -/ +def WFFull (doc : Doc) : Prop := + ∃ (hd : Ihdr) (head : Chunk) (mid : List Chunk), + doc = head :: mid ++ [iendChunk] ∧ + head.typeBytes = ihdrType ∧ head.data = printIhdr hd ∧ + WFHeader hd ∧ + (∀ c ∈ doc, WFChunk c) ∧ + (∀ c ∈ head :: mid, isIEND c = false) + +end Png diff --git a/Proofs.lean b/Proofs.lean index b877d25..e63d117 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -1,2 +1,3 @@ import Proofs.RoundTrip +import Proofs.Header import Proofs.Verify diff --git a/Proofs/Header.lean b/Proofs/Header.lean new file mode 100644 index 0000000..f7d442d --- /dev/null +++ b/Proofs/Header.lean @@ -0,0 +1,139 @@ +/- + The slice 2 proofs: the IHDR header round trip, the exactness + of the (colour type, bit depth) table, and the file level + round trip that joins the header to the chunk layer of + slice 1. + + The table claim is `pairAllowed_iff`, with its byte form + `checkPair_iff`: the checker's answer agrees with the written + out list of allowed pairs for every colour type number and + every bit depth number. Colour types are bytes and bit depths + are bytes, so the numbers 0 to 255 are the whole of both, and + the proof settles the question for all of them: it splits on + the five colour types the PNG specification names, and in + each case the two sides come down to the same list of depths; + for every other colour type number both sides are empty. No + case is left to computation over the whole grid. + + The header round trip is `parseIhdr_print`. The file level + claim is `parseFile_print`: a fully well formed document + (chunk layer well formed, first chunk the printed form of a + well formed header) prints and reads back whole, header + included. +-/ + +import Png +import Proofs.RoundTrip + +namespace Png.Proofs + +open Png + +/-- One step of the header reader, stated for rewriting: 13 + bytes at the front of the input, with whatever follows. -/ +theorem parseIhdr_step (w1 w2 w3 w4 h1 h2 h3 h4 bd ct comp filt int : UInt8) + (rest : List UInt8) : + parseIhdr (w1 :: w2 :: w3 :: w4 :: h1 :: h2 :: h3 :: h4 + :: bd :: ct :: comp :: filt :: int :: rest) = + if rest ≠ [] then none + else if u32 w1 w2 w3 w4 = 0 ∨ u32 h1 h2 h3 h4 = 0 then none + else if comp ≠ 0 ∨ filt ≠ 0 then none + else if int > 1 then none + else if checkPair ct bd then + some ⟨u32 w1 w2 w3 w4, u32 h1 h2 h3 h4, bd, ct, int⟩ + else none := rfl + +/-- The printed form of a header is 13 bytes. -/ +theorem printIhdr_length (h : Ihdr) : (printIhdr h).length = 13 := by + simp [printIhdr, be32] + +/-- The header round trip: reading the printed bytes of a well + formed header gives the header back. -/ +theorem parseIhdr_print (h : Ihdr) (hwf : WFHeader h) : + parseIhdr (printIhdr h) = some h := by + obtain ⟨w, hh, bd, ct, il⟩ := h + obtain ⟨hw1, hw2, hh1, hh2, hil, hpair⟩ := hwf + have hw1' : 0 < w := hw1 + have hh1' : 0 < hh := hh1 + have hnl : ¬ (il > 1) := by + rcases hil with rfl | rfl <;> decide + have e : printIhdr ⟨w, hh, bd, ct, il⟩ = + (w / 16777216).toUInt8 :: (w / 65536).toUInt8 + :: (w / 256).toUInt8 :: w.toUInt8 + :: (hh / 16777216).toUInt8 :: (hh / 65536).toUInt8 + :: (hh / 256).toUInt8 :: hh.toUInt8 + :: bd :: ct :: 0 :: 0 :: il :: [] := rfl + rw [e, parseIhdr_step, u32_be32 w hw2, u32_be32 hh hh2] + rw [if_neg (by simp : ¬ (([] : List UInt8) ≠ []))] + rw [if_neg (by omega : ¬ (w = 0 ∨ hh = 0))] + rw [if_neg (by decide : ¬ ((0 : UInt8) ≠ 0 ∨ (0 : UInt8) ≠ 0))] + rw [if_neg hnl, if_pos hpair] + +/-- The table, exactly: a depth goes with a colour type under + the checker if and only if the pair is in the written out + list of allowed pairs. Stated for all numbers, so in + particular for every colour type byte and every bit depth + byte. -/ +theorem pairAllowed_iff : ∀ n m : Nat, + pairAllowed n m = true ↔ (n, m) ∈ allowedPairs := by + intro n m + by_cases h0 : n = 0 + · subst h0 + simp only [pairAllowed, decide_eq_true_eq] + show m ∈ [1, 2, 4, 8, 16] ↔ (0, m) ∈ allowedPairs + simp [allowedPairs] + by_cases h2 : n = 2 + · subst h2 + simp only [pairAllowed, decide_eq_true_eq] + show m ∈ [8, 16] ↔ (2, m) ∈ allowedPairs + simp [allowedPairs] + by_cases h3 : n = 3 + · subst h3 + simp only [pairAllowed, decide_eq_true_eq] + show m ∈ [1, 2, 4, 8] ↔ (3, m) ∈ allowedPairs + simp [allowedPairs] + by_cases h4 : n = 4 + · subst h4 + simp only [pairAllowed, decide_eq_true_eq] + show m ∈ [8, 16] ↔ (4, m) ∈ allowedPairs + simp [allowedPairs] + by_cases h6 : n = 6 + · subst h6 + simp only [pairAllowed, decide_eq_true_eq] + show m ∈ [8, 16] ↔ (6, m) ∈ allowedPairs + simp [allowedPairs] + · have hdep : allowedDepths n = [] := by + unfold allowedDepths + rw [if_neg h0, if_neg h2, if_neg h3, if_neg h4, if_neg h6] + simp only [pairAllowed, decide_eq_true_eq, hdep] + simp [allowedPairs, h0, h2, h3, h4, h6] + +/-- The table, in the byte form the parser uses: the check on + two bytes holds if and only if the pair of their values is + in the written out list. -/ +theorem checkPair_iff (ct bd : UInt8) : + checkPair ct bd = true ↔ (ct.toNat, bd.toNat) ∈ allowedPairs := + pairAllowed_iff ct.toNat bd.toNat + +/-- A fully well formed document is well formed at the chunk + layer. -/ +theorem wfFull_wf {doc : Doc} (h : WFFull doc) : WF doc := by + obtain ⟨hd, head, mid, hdoc, htype, hdata, -, hall, hnot⟩ := h + exact ⟨head, mid, hdoc, htype, + by rw [hdata]; exact printIhdr_length hd, hall, hnot⟩ + +/-- The file level round trip: printing a fully well formed + document and reading the file back at both layers gives the + document back, with its header. -/ +theorem parseFile_print {doc : Doc} (h : WFFull doc) : + ∃ hd : Ihdr, parseFile (print doc) = some (hd, doc) := by + have hwf : WF doc := wfFull_wf h + obtain ⟨hd, head, mid, hdoc, htype, hdata, hwfhd, hall, hnot⟩ := h + refine ⟨hd, ?_⟩ + unfold parseFile + rw [parse_print hwf] + show (headerOf doc).map (fun x => (x, doc)) = some (hd, doc) + rw [hdoc] + simp [headerOf, hdata, parseIhdr_print hd hwfhd] + +end Png.Proofs diff --git a/Proofs/Verify.lean b/Proofs/Verify.lean index fe6388e..975c7df 100644 --- a/Proofs/Verify.lean +++ b/Proofs/Verify.lean @@ -7,5 +7,9 @@ -/ import Proofs.RoundTrip +import Proofs.Header #print axioms Png.Proofs.parse_print +#print axioms Png.Proofs.parseIhdr_print +#print axioms Png.Proofs.checkPair_iff +#print axioms Png.Proofs.parseFile_print diff --git a/README.md b/README.md index 25a3027..ba3fc10 100644 --- a/README.md +++ b/README.md @@ -1,20 +1,23 @@ # png: a PNG chunk parser and printer, with a proved round trip -A PNG chunk parser and printer in Lean. It reads the chunk layer of a PNG file: the signature, then each chunk's length, type, data, and CRC-32 check. It does not decode pixels, and it does not inflate IDAT data. The main claim is proved: parsing what the printer wrote returns the same chunk list. The tests run the parser against real PNG files built with Python's zlib and against a strict oracle written from the rules; see `tests/TEST-RESULTS.md` for the counts. +A PNG chunk parser and printer in Lean. It reads the chunk layer of a PNG file: the signature, then each chunk's length, type, data, and CRC-32 check. Slice 2 adds a decoder for the IHDR header: the width, height, bit depth, colour type, and interlace method held in the first chunk's 13 data bytes, checked against the validity rules of the PNG specification. It does not decode pixels, and it does not inflate IDAT data. The main claims are proved: parsing what the printer wrote returns the same chunk list, reading the printed bytes of a well formed header returns the header, and the bit depth table the checker uses is exactly the table the specification names. The tests run the parser against real PNG files built with Python's zlib and against a strict oracle written from the rules; see `tests/TEST-RESULTS.md` for the counts. Status: in progress. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. ## What is proved -The definitions are in `Png/Value.lean` (the chunk type, the printer, and the well-formedness rules), `Png/Parse.lean` (the parser), and `Png/Crc32.lean` (the CRC-32). The proofs are in `Proofs/RoundTrip.lean`. +The definitions are in `Png/Value.lean` (the chunk type, the printer, and the well-formedness rules), `Png/Parse.lean` (the parser), `Png/Crc32.lean` (the CRC-32), and `Png/Header.lean` (the IHDR header value, its reader and printer, and the file level read). The proofs are in `Proofs/RoundTrip.lean` and `Proofs/Header.lean`. | Claim | Theorem | |-------|---------| | Parsing the printed form of a well formed chunk list gives the list back. | `Png.Proofs.parse_print` | | Reading back one printed chunk, with any bytes after it, gives the chunk and those bytes untouched. | `Png.Proofs.parseChunk_printChunk` | | Four bytes printed from a value below 2^32 read back as the value. | `Png.Proofs.u32_be32` | +| Reading the printed bytes of a well formed IHDR header gives the header back. | `Png.Proofs.parseIhdr_print` | +| The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair. | `Png.Proofs.checkPair_iff` | +| Printing a fully well formed document and reading it back at both layers gives the document back, header included. | `Png.Proofs.parseFile_print` | -A chunk list is well formed when it is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk; every chunk type is four ASCII letters; and every data length is below 2^31. `parse_print` checks against two of the standard axioms (`propext`, `Quot.sound`), which a reader can confirm with `#print axioms Png.Proofs.parse_print`. +A chunk list is well formed when it is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk; every chunk type is four ASCII letters; and every data length is below 2^31. A header is well formed when its width and height are above zero and below 2^32, its interlace byte is 0 or 1, and its bit depth is one its colour type allows. Each of these theorems checks against two of the standard axioms (`propext`, `Quot.sound`), which a reader can confirm with `#print axioms` on the theorem's name. The command-line tool in `Main.lean` calls these functions directly. @@ -22,7 +25,8 @@ The command-line tool in `Main.lean` calls these functions directly. - That the parser accepts every file the rules in `SPEC.md` allow, and rejects every file they forbid. The round trip does not need either, so neither is proved. The test suite checks that behaviour instead, and the results file records the outcome, including any failure. - That the CRC-32 here is the standard one. The round trip needs no such fact, since the parser and the printer compute the same function. The differential tests against Python zlib's `crc32` are what tie this function to the standard. -- Anything inside a chunk's data. The IHDR fields (width, height, bit depth, colour type) are not read, past the check that IHDR holds 13 bytes. IDAT data is not inflated. No pixel is ever decoded. +- That the header reader accepts every header the rules in `SPEC.md` allow, and rejects every header they forbid, beyond what the round trip and the table theorem cover. The tests check that behaviour instead: hand built headers for every colour type and allowed depth, the full colour type and depth enumeration against the table, and the rejection cases. +- Anything inside a chunk's data past the IHDR header. The data of every other chunk type is opaque here. IDAT data is not inflated. No pixel is ever decoded. - Chunk order past the first and last. Which types may appear, how many times, and in what order between IHDR and IEND is not checked. A chunk of type IEND that carries data is read as an ordinary chunk. ## What you must trust @@ -44,7 +48,7 @@ lake build echo "parse 137,80,78,71,13,10,26,10,0,0,0,13,73,72,68,82,0,0,0,1,0,0,0,1,8,2,0,0,0,144,119,83,222,0,0,0,0,73,69,78,68,174,66,96,130" | .lake/build/bin/png ``` -That request is a whole minimal PNG file as byte codes: the signature, an IHDR chunk for a 1 by 1 image, and IEND. The answer is `ok:` followed by the same codes, since the file is valid and reprints byte for byte. A file the parser rejects, such as the single code `120`, answers `none`. A malformed request answers `error`. See `SPEC.md` for the full protocol. +That request is a whole minimal PNG file as byte codes: the signature, an IHDR chunk for a 1 by 1 image, and IEND. The answer is `ok:` followed by the same codes, since the file is valid and reprints byte for byte. A file the parser rejects, such as the single code `120`, answers `none`. A malformed request answers `error`. The same file asked through `header`, with the word `header` in place of `parse`, answers `ok:49,120,49,32,100,56,32,116,50,32,105,48`: the codes of the text `1x1 d8 t2 i0`, the decoded header fields. See `SPEC.md` for the full protocol. ## Re-check it diff --git a/SPEC.md b/SPEC.md index ab1d12b..4c33fdd 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # Specification: png -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 reviewer who did not write this specification approves it, together with any statement file a reviewer adds later. No such file exists yet, so nothing here counts toward the verified bar yet. +A PNG chunk parser and printer in Lean, with (slice 2) a decoder for the IHDR header. It does not decode pixels, and it does not inflate IDAT data. A reviewer who did not write this specification approves it, together with any statement file a reviewer adds later. No such file exists yet, so nothing here counts toward the verified bar yet. Bytes are `List UInt8` throughout. @@ -26,7 +26,42 @@ The CRC-32 is the one PNG and ZIP share: the ISO 3309 polynomial, reflected, the 3. Reading stops at a chunk whose type is IEND and whose data is empty. That chunk must be the end of the input: any byte after it rejects the file, and running out of input before such a chunk rejects the file. 4. The first chunk read has type IHDR and a data length of 13. -A chunk of type IEND that carries data is an ordinary chunk at this layer: reading does not stop at it. No other rule about chunk order is checked: which types may appear, how many times, or in what order past the first and last, is outside this slice. The contents of the IHDR data, past its length, are not checked: width, height, bit depth, and colour type are read as data like any other. +A chunk of type IEND that carries data is an ordinary chunk at this layer: reading does not stop at it. No other rule about chunk order is checked: which types may appear, how many times, or in what order past the first and last, is outside this slice. At this layer the contents of the IHDR data, past its length, are not checked: width, height, bit depth, and colour type are read as data like any other. The header read of slice 2, below, is a second read on top of this one and does check them. + +## The IHDR header (slice 2) + +The first chunk's 13 data bytes hold, in order: + +- the width: four bytes, big endian. +- the height: four bytes, big endian. +- the bit depth: one byte. +- the colour type: one byte. +- the compression method: one byte. +- the filter method: one byte. +- the interlace method: one byte. + +The decoded header value holds the width and the height as numbers, and the bit depth, the colour type, and the interlace method as bytes. The compression and filter bytes are not held: the PNG specification gives them no choice (the only compression method is 0, the only filter method is 0), so reading checks that each is zero and printing writes zero. + +A header reads only when all of these hold: + +- the width is above zero, and the height is above zero. +- the compression byte is zero, and the filter byte is zero. +- the interlace byte is 0 or 1. +- the bit depth is one the colour type allows, by this table from the PNG specification: + +| Colour type | Meaning | Allowed bit depths | +|---|---|---| +| 0 | greyscale | 1, 2, 4, 8, 16 | +| 2 | truecolour | 8, 16 | +| 3 | indexed colour | 1, 2, 4, 8 | +| 4 | greyscale with alpha | 8, 16 | +| 6 | truecolour with alpha | 8, 16 | + +A colour type other than 0, 2, 3, 4, or 6 allows no bit depth, and reading anything but exactly 13 bytes is a rejection. + +Printing a header writes the 13 bytes back: width and height big endian, then bit depth, colour type, compression zero, filter zero, interlace. + +The file level read (`parseFile`) runs the chunk parse of slice 1 and then reads the first chunk's data as a header. A file whose first chunk is not a valid IHDR in this sense is rejected by that read even when the chunk layer accepts it: a file with a width of zero is the plainest case. ## Printing @@ -34,7 +69,13 @@ The printer writes the signature, then each chunk as its length, its type bytes, ## The claim -The proved claim is a round trip: for every well formed chunk list, parsing what the printer wrote returns the same list. Well formed means the list is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk (type IEND with no data); every chunk type is four ASCII letters; and every data length is below 2^31. +The proved claim of slice 1 is a round trip: for every well formed chunk list, parsing what the printer wrote returns the same list. Well formed means the list is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk (type IEND with no data); every chunk type is four ASCII letters; and every data length is below 2^31. + +Slice 2 adds three proved claims: + +- The header round trip: reading the printed bytes of a well formed header gives the header back. Well formed means the width and height are above zero and below 2^32, the interlace byte is 0 or 1, and the bit depth is one the colour type allows. +- The table is exact: the depth checker agrees with the table above, written out as a list of (colour type, bit depth) pairs, on every colour type byte and every bit depth byte. +- The file level round trip: a document that is well formed at the chunk layer and whose first chunk's data is the printed form of a well formed header prints and reads back whole, header included. No claim is made that the parser accepts every file the rules above allow, or rejects every file they forbid, beyond what the round trip needs. The test suite checks that behaviour against real PNG files built with Python's zlib and against a strict reading of these rules, and the results record the counts. @@ -42,4 +83,4 @@ The round trip needs no fact about CRC-32 itself: the parser and the printer com ## The command-line tool -`Main.lean` reads one request per line. The only operation is `parse`: the request is the word `parse`, a space, and the byte codes of a PNG file as comma-separated decimal numbers. The answer is `ok:` followed by the byte codes of the canonical reprint of the parsed chunk list, or `none` when the file is rejected. A malformed request line prints `error`. A code above 255 makes the request malformed, since no byte holds it. +`Main.lean` reads one request per line. The operations are `parse` and `header`: the request is the operation word, a space, and the byte codes of a PNG file as comma-separated decimal numbers. The `parse` answer is `ok:` followed by the byte codes of the canonical reprint of the parsed chunk list, or `none` when the file is rejected. The `header` answer is `ok:` followed by the codes of a text line naming the decoded header fields, or `none` when the file is rejected at either layer. The text is the width in decimal, the letter `x`, the height in decimal, a space, the letter `d`, the bit depth in decimal, a space, the letter `t`, the colour type in decimal, a space, the letter `i`, and the interlace method in decimal: for a 1920 by 1080 file at bit depth 8, colour type 6, no interlace, the text is `1920x1080 d8 t6 i0`, and the answer carries the character codes of that text. A malformed request line prints `error`. A code above 255 makes the request malformed, since no byte holds it. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index f9ac030..66fb8f0 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -16,15 +16,13 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Mutations of a 1140 byte file (300 sampled single byte flips): 300 inputs, 300 agreements - Malformed requests answered error: 12 of 12 - Requests with no codes answered none: 2 of 2 +- Real PNG files through `header`: 4 of 4 decoded to the fields they were built with +- Hand-built headers, every colour type and allowed depth: 15 of 15 accepted with their fields +- Header enumeration, 14 colour types by 9 depths against the allowed table: 126 of 126 agreements +- Header mutations rejected: 6 of 6 +- Random well formed headers: 200 of 200 decoded to the fields they were built with +- Random header files through `parse`: 200 of 200 reprinted byte for byte +- Malformed header requests answered error: 3 of 3 +- Header requests with no codes answered none: 2 of 2 - Named differences: none - Failures: 0 - -## Axiom check - -Recorded on 2026-10-26 against the head of this pull request, on Lean 4.35.0. The line below is the output printed for `Proofs/Verify.lean` during a clean `lake build` (17 jobs). - -```text -'Png.Proofs.parse_print' depends on axioms: [propext, Quot.sound] -``` - -No other axiom is named, and sorryAx is not named. diff --git a/tests/run_tests.py b/tests/run_tests.py index d3901ef..694c2a1 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1,7 +1,9 @@ #!/usr/bin/env python3 """Tests for the Lean PNG chunk parser and printer. -Four parts. +Five parts. Parts 1 to 4 are the slice 1 suite, unchanged. +Part 5 is slice 2: the IHDR header read through the `header` +request. 1. Real PNG files built with Python zlib: an IHDR chunk (the width, height, bit depth, and colour type are stated per file @@ -30,6 +32,19 @@ 4. Malformed request lines must be answered `error`. +5. The header read (slice 2). The same real files are asked + through `header`, and their decoded fields are checked. Hand + built headers cover every colour type with each depth the + PNG specification allows it. An enumeration crosses colour + types 0 to 12 and 255 with depths 0, 1, 2, 3, 4, 5, 8, 16, + and 255, settled by the allowed table written in this + harness. Mutations (a zero width, a zero height, a + compression byte of 1, a filter byte of 1, an interlace byte + of 2, a first chunk of length 12) must be rejected. Random + well formed headers are built into whole files and checked + through `header` for their fields and through `parse` for a + byte for byte reprint. + python3 tests/run_tests.py [--seed N] [--count N] The tool is driven one batch process per chunk of requests, input @@ -244,9 +259,9 @@ def real_png(width, height, colour_type, rng, split_idat=False, extra=()): return b"".join(parts) -def run_real(seed): +def real_files(seed): rng = random.Random(seed) - files = [ + return [ ("1x1, bit depth 8, colour type 2 (RGB)", real_png(1, 1, 2, rng)), ("4x3, bit depth 8, colour type 6 (RGBA)", real_png(4, 3, 6, rng)), ( @@ -258,6 +273,10 @@ def run_real(seed): real_png(7, 5, 2, rng, extra=[(b"tEXt", b"Title\x00A small test")]), ), ] + + +def run_real(seed): + files = real_files(seed) lines = [] failures = [] answers, problems = ask_all([request(data) for _, data in files]) @@ -496,6 +515,237 @@ def run_malformed(): return lines, failures +# ---------------------------------------------------------------- the +# header read (slice 2). The strict oracle for this part is the +# allowed table below, written from the PNG specification: a +# colour type allows exactly these bit depths. + + +ALLOWED = {0: [1, 2, 4, 8, 16], 2: [8, 16], 3: [1, 2, 4, 8], 4: [8, 16], 6: [8, 16]} + + +def ihdr_full(width, height, bit_depth, colour_type, comp=0, filt=0, interlace=0): + return struct.pack( + ">IIBBBBB", width, height, bit_depth, colour_type, comp, filt, interlace + ) + + +def header_request(data): + return "header " + codes(data) + + +def header_line(width, height, bit_depth, colour_type, interlace): + text = f"{width}x{height} d{bit_depth} t{colour_type} i{interlace}" + return "ok:" + codes(text.encode("ascii")) + + +def header_file(ihdr_bytes, idat_data=b"\x00\x01\x02\x03"): + return ( + SIG + + make_chunk(b"IHDR", ihdr_bytes) + + make_chunk(b"IDAT", zlib.compress(idat_data)) + + make_chunk(b"IEND", b"") + ) + + +def run_real_headers(seed): + """The real files of part 1, asked through `header`. Their + (width, height, bit depth, colour type, interlace) are known + from how they were built.""" + known = [(1, 1, 8, 2, 0), (4, 3, 8, 6, 0), (16, 16, 8, 0, 0), (7, 5, 8, 2, 0)] + files = real_files(seed) + lines = [] + failures = [] + answers, problems = ask_all([header_request(data) for _, data in files]) + for problem in problems: + failures.append(f"real headers: tool problem: {problem}") + agree = 0 + for (name, _), fields, ans in zip(files, known, answers): + want = header_line(*fields) + if ans == want: + agree += 1 + else: + failures.append(f"real header {name}: want {want!r}, got {ans!r}") + lines.append( + f"Real PNG files through `header`: {agree} of {len(files)} decoded " + "to the fields they were built with" + ) + return lines, failures + + +def run_header_types(): + """One file per allowed (colour type, bit depth) pair, the + interlace byte alternating, each checked for its fields.""" + cases = [] + for ctype in sorted(ALLOWED): + for depth in ALLOWED[ctype]: + interlace = (len(cases) % 2) + cases.append((3, 2, depth, ctype, interlace)) + lines = [] + failures = [] + answers, problems = ask_all( + [ + header_request( + header_file(ihdr_full(w, h, d, t, interlace=i)) + ) + for (w, h, d, t, i) in cases + ] + ) + for problem in problems: + failures.append(f"header types: tool problem: {problem}") + agree = 0 + for fields, ans in zip(cases, answers): + want = header_line(*fields) + if ans == want: + agree += 1 + else: + failures.append(f"header type {fields}: want {want!r}, got {ans!r}") + lines.append( + f"Hand-built headers, every colour type and allowed depth: " + f"{agree} of {len(cases)} accepted with their fields" + ) + return lines, failures + + +def run_header_grid(): + """The enumeration: colour types 0 to 12 and 255, against + depths 0, 1, 2, 3, 4, 5, 8, 16, 255. The table settles each.""" + types = list(range(13)) + [255] + depths = [0, 1, 2, 3, 4, 5, 8, 16, 255] + cases = [(t, d) for t in types for d in depths] + lines = [] + failures = [] + answers, problems = ask_all( + [ + header_request(header_file(ihdr_full(2, 2, d, t))) + for t, d in cases + ] + ) + for problem in problems: + failures.append(f"header grid: tool problem: {problem}") + agree = 0 + for (t, d), ans in zip(cases, answers): + want = header_line(2, 2, d, t, 0) if d in ALLOWED.get(t, []) else "none" + if ans == want: + agree += 1 + else: + failures.append(f"header grid type {t} depth {d}: want {want!r}, got {ans!r}") + lines.append( + f"Header enumeration, {len(types)} colour types by {len(depths)} " + f"depths against the allowed table: {agree} of {len(cases)} agreements" + ) + return lines, failures + + +def run_header_mutations(): + """Each of these files is one change away from a valid one, + and each must be rejected by the header read. The CRCs are + recomputed, so the rejection is for the header rule itself + (except the length 12 case, which the chunk layer rejects).""" + good = ihdr_full(4, 3, 8, 6) + cases = [ + ("a width of zero", header_file(ihdr_full(0, 3, 8, 6))), + ("a height of zero", header_file(ihdr_full(4, 0, 8, 6))), + ("a compression byte of 1", header_file(ihdr_full(4, 3, 8, 6, comp=1))), + ("a filter byte of 1", header_file(ihdr_full(4, 3, 8, 6, filt=1))), + ("an interlace byte of 2", header_file(ihdr_full(4, 3, 8, 6, interlace=2))), + ( + "a first chunk of length 12", + SIG + + make_chunk(b"IHDR", good[:12]) + + make_chunk(b"IDAT", zlib.compress(b"\x00\x01\x02\x03")) + + make_chunk(b"IEND", b""), + ), + ] + lines = [] + failures = [] + answers, problems = ask_all([header_request(data) for _, data in cases]) + for problem in problems: + failures.append(f"header mutations: tool problem: {problem}") + agree = 0 + for (name, _), ans in zip(cases, answers): + if ans == "none": + agree += 1 + else: + failures.append(f"header mutation {name}: want none, got {ans!r}") + lines.append(f"Header mutations rejected: {agree} of {len(cases)}") + return lines, failures + + +def run_header_random(seed, count=200): + """Random well formed headers, built into whole files. Each + file is checked through `header` for its fields and through + `parse` for a byte for byte reprint.""" + rng = random.Random(seed + 11) + cases = [] + for _ in range(count): + ctype = rng.choice(sorted(ALLOWED)) + depth = rng.choice(ALLOWED[ctype]) + width = rng.choice([1, 2, 17, 640, 65535, rng.randrange(1, 100001)]) + height = rng.choice([1, 3, 42, 480, 65535, rng.randrange(1, 100001)]) + interlace = rng.randrange(0, 2) + fields = (width, height, depth, ctype, interlace) + cases.append( + (fields, header_file(ihdr_full(width, height, depth, ctype, interlace=interlace))) + ) + lines = [] + failures = [] + answers, problems = ask_all([header_request(data) for _, data in cases]) + for problem in problems: + failures.append(f"random headers: tool problem: {problem}") + answers2, problems2 = ask_all([request(data) for _, data in cases]) + for problem in problems2: + failures.append(f"random headers, parse: tool problem: {problem}") + agree = 0 + for (fields, _), ans in zip(cases, answers): + want = header_line(*fields) + if ans == want: + agree += 1 + else: + failures.append(f"random header {fields}: want {want!r}, got {ans!r}") + lines.append( + f"Random well formed headers: {agree} of {len(cases)} decoded " + "to the fields they were built with" + ) + agree2 = 0 + for (_, data), ans in zip(cases, answers2): + want = "ok:" + codes(data) + if ans == want: + agree2 += 1 + else: + failures.append(f"random header file: want byte for byte reprint, got {ans!r}") + lines.append( + f"Random header files through `parse`: {agree2} of {len(cases)} " + "reprinted byte for byte" + ) + return lines, failures + + +def run_header_malformed(): + lines = [] + failures = [] + bad = ["header 256", "header 12a", "header 97 98"] + answers, problems = ask_all(bad) + for problem in problems: + failures.append(f"header malformed: tool problem: {problem}") + bad_ok = 0 + for line, ans in zip(bad, answers): + if ans == "error": + bad_ok += 1 + else: + failures.append(f"header malformed {line!r}: want error, got {ans!r}") + lines.append(f"Malformed header requests answered error: {bad_ok} of {len(bad)}") + none_ok = 0 + answers, _ = ask_all(["header", "header "]) + for ans in answers: + if ans == "none": + none_ok += 1 + else: + failures.append(f"empty header request: want none, got {ans!r}") + lines.append(f"Header requests with no codes answered none: {none_ok} of 2") + return lines, failures + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=SEED_DEFAULT) @@ -523,6 +773,12 @@ def main(): run_random(args.seed, args.count), run_mutations(args.seed), run_malformed(), + run_real_headers(args.seed), + run_header_types(), + run_header_grid(), + run_header_mutations(), + run_header_random(args.seed), + run_header_malformed(), ): lines, failures = part all_lines += lines From 3442498c8fac7ed1e7c2aafe658cc8d42e211779 Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 19:50:12 -0500 Subject: [PATCH 2/3] Cap width and height below 2^31 and restore the axiom record, per review --- Png/Header.lean | 13 +++++++----- Proofs/Header.lean | 6 +++++- README.md | 2 +- SPEC.md | 4 ++-- tests/TEST-RESULTS.md | 12 ++++++++++- tests/run_tests.py | 47 +++++++++++++++++++++++++++++++++++++------ 6 files changed, 68 insertions(+), 16 deletions(-) diff --git a/Png/Header.lean b/Png/Header.lean index 4178d74..52efc3c 100644 --- a/Png/Header.lean +++ b/Png/Header.lean @@ -15,7 +15,8 @@ interlace byte is 0 (no interlace) or 1 (Adam7), and is held. A header is accepted only when the width and the height are - both above zero, the compression and filter bytes are zero, + both above zero and below 2^31 (the PNG specification caps + each of them at 2^31 - 1), the compression and filter bytes are zero, the interlace byte is 0 or 1, and the bit depth is one the colour type allows. The allowed pairs are the ones the PNG specification names: @@ -77,11 +78,11 @@ def allowedPairs : List (Nat × Nat) := def checkPair (ct bd : UInt8) : Bool := pairAllowed ct.toNat bd.toNat /-- A header is well formed when the width and the height are - above zero and below 2^32, the interlace byte is 0 or 1, and + above zero and below 2^31, the interlace byte is 0 or 1, and the bit depth is one the colour type allows. -/ def WFHeader (h : Ihdr) : Prop := - 0 < h.width ∧ h.width < 4294967296 ∧ - 0 < h.height ∧ h.height < 4294967296 ∧ + 0 < h.width ∧ h.width < 2147483648 ∧ + 0 < h.height ∧ h.height < 2147483648 ∧ (h.interlace = 0 ∨ h.interlace = 1) ∧ checkPair h.colorType h.bitDepth = true @@ -93,7 +94,8 @@ def printIhdr (h : Ihdr) : List UInt8 := /-- Read 13 bytes as a header. Anything but exactly 13 bytes is rejected, and so is a header that breaks any of the rules at - the top of this file: a width or height of zero, a nonzero + the top of this file: a width or height of zero or of 2^31 + or more, a nonzero compression or filter byte, an interlace byte above 1, or a bit depth the colour type does not allow. -/ def parseIhdr (bs : List UInt8) : Option Ihdr := @@ -101,6 +103,7 @@ def parseIhdr (bs : List UInt8) : Option Ihdr := | w1 :: w2 :: w3 :: w4 :: h1 :: h2 :: h3 :: h4 :: bd :: ct :: comp :: filt :: int :: rest => if rest ≠ [] then none else if u32 w1 w2 w3 w4 = 0 ∨ u32 h1 h2 h3 h4 = 0 then none + else if u32 w1 w2 w3 w4 ≥ 2147483648 ∨ u32 h1 h2 h3 h4 ≥ 2147483648 then none else if comp ≠ 0 ∨ filt ≠ 0 then none else if int > 1 then none else if checkPair ct bd then diff --git a/Proofs/Header.lean b/Proofs/Header.lean index f7d442d..4fcd6c6 100644 --- a/Proofs/Header.lean +++ b/Proofs/Header.lean @@ -37,6 +37,7 @@ theorem parseIhdr_step (w1 w2 w3 w4 h1 h2 h3 h4 bd ct comp filt int : UInt8) :: bd :: ct :: comp :: filt :: int :: rest) = if rest ≠ [] then none else if u32 w1 w2 w3 w4 = 0 ∨ u32 h1 h2 h3 h4 = 0 then none + else if u32 w1 w2 w3 w4 ≥ 2147483648 ∨ u32 h1 h2 h3 h4 ≥ 2147483648 then none else if comp ≠ 0 ∨ filt ≠ 0 then none else if int > 1 then none else if checkPair ct bd then @@ -55,6 +56,8 @@ theorem parseIhdr_print (h : Ihdr) (hwf : WFHeader h) : obtain ⟨hw1, hw2, hh1, hh2, hil, hpair⟩ := hwf have hw1' : 0 < w := hw1 have hh1' : 0 < hh := hh1 + have hw2' : w < 2147483648 := hw2 + have hh2' : hh < 2147483648 := hh2 have hnl : ¬ (il > 1) := by rcases hil with rfl | rfl <;> decide have e : printIhdr ⟨w, hh, bd, ct, il⟩ = @@ -63,9 +66,10 @@ theorem parseIhdr_print (h : Ihdr) (hwf : WFHeader h) : :: (hh / 16777216).toUInt8 :: (hh / 65536).toUInt8 :: (hh / 256).toUInt8 :: hh.toUInt8 :: bd :: ct :: 0 :: 0 :: il :: [] := rfl - rw [e, parseIhdr_step, u32_be32 w hw2, u32_be32 hh hh2] + rw [e, parseIhdr_step, u32_be32 w (by omega), u32_be32 hh (by omega)] rw [if_neg (by simp : ¬ (([] : List UInt8) ≠ []))] rw [if_neg (by omega : ¬ (w = 0 ∨ hh = 0))] + rw [if_neg (by omega : ¬ (w ≥ 2147483648 ∨ hh ≥ 2147483648))] rw [if_neg (by decide : ¬ ((0 : UInt8) ≠ 0 ∨ (0 : UInt8) ≠ 0))] rw [if_neg hnl, if_pos hpair] diff --git a/README.md b/README.md index ba3fc10..2029841 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ The definitions are in `Png/Value.lean` (the chunk type, the printer, and the we | The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair. | `Png.Proofs.checkPair_iff` | | Printing a fully well formed document and reading it back at both layers gives the document back, header included. | `Png.Proofs.parseFile_print` | -A chunk list is well formed when it is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk; every chunk type is four ASCII letters; and every data length is below 2^31. A header is well formed when its width and height are above zero and below 2^32, its interlace byte is 0 or 1, and its bit depth is one its colour type allows. Each of these theorems checks against two of the standard axioms (`propext`, `Quot.sound`), which a reader can confirm with `#print axioms` on the theorem's name. +A chunk list is well formed when it is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk; every chunk type is four ASCII letters; and every data length is below 2^31. A header is well formed when its width and height are above zero and below 2^31, its interlace byte is 0 or 1, and its bit depth is one its colour type allows. Each of these theorems checks against two of the standard axioms (`propext`, `Quot.sound`), which a reader can confirm with `#print axioms` on the theorem's name. The command-line tool in `Main.lean` calls these functions directly. diff --git a/SPEC.md b/SPEC.md index 4c33fdd..9ae055d 100644 --- a/SPEC.md +++ b/SPEC.md @@ -44,7 +44,7 @@ The decoded header value holds the width and the height as numbers, and the bit A header reads only when all of these hold: -- the width is above zero, and the height is above zero. +- the width is above zero and below 2^31, and the height is above zero and below 2^31. The PNG specification caps each of them at 2^31 - 1. - the compression byte is zero, and the filter byte is zero. - the interlace byte is 0 or 1. - the bit depth is one the colour type allows, by this table from the PNG specification: @@ -73,7 +73,7 @@ The proved claim of slice 1 is a round trip: for every well formed chunk list, p Slice 2 adds three proved claims: -- The header round trip: reading the printed bytes of a well formed header gives the header back. Well formed means the width and height are above zero and below 2^32, the interlace byte is 0 or 1, and the bit depth is one the colour type allows. +- The header round trip: reading the printed bytes of a well formed header gives the header back. Well formed means the width and height are above zero and below 2^31, the interlace byte is 0 or 1, and the bit depth is one the colour type allows. - The table is exact: the depth checker agrees with the table above, written out as a list of (colour type, bit depth) pairs, on every colour type byte and every bit depth byte. - The file level round trip: a document that is well formed at the chunk layer and whose first chunk's data is the printed form of a well formed header prints and reads back whole, header included. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 66fb8f0..18dc907 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -19,10 +19,20 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Real PNG files through `header`: 4 of 4 decoded to the fields they were built with - Hand-built headers, every colour type and allowed depth: 15 of 15 accepted with their fields - Header enumeration, 14 colour types by 9 depths against the allowed table: 126 of 126 agreements -- Header mutations rejected: 6 of 6 +- Header mutations rejected: 10 of 10 - Random well formed headers: 200 of 200 decoded to the fields they were built with - Random header files through `parse`: 200 of 200 reprinted byte for byte - Malformed header requests answered error: 3 of 3 - Header requests with no codes answered none: 2 of 2 + +## Axiom check + +The output of `#print axioms` for the four named theorems, from `lake env lean Proofs/Verify.lean`: + +- 'Png.Proofs.parse_print' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.parseIhdr_print' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.checkPair_iff' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.parseFile_print' depends on axioms: [propext, Quot.sound] + - Named differences: none - Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py index 694c2a1..86d7af8 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -38,12 +38,13 @@ PNG specification allows it. An enumeration crosses colour types 0 to 12 and 255 with depths 0, 1, 2, 3, 4, 5, 8, 16, and 255, settled by the allowed table written in this - harness. Mutations (a zero width, a zero height, a - compression byte of 1, a filter byte of 1, an interlace byte - of 2, a first chunk of length 12) must be rejected. Random - well formed headers are built into whole files and checked - through `header` for their fields and through `parse` for a - byte for byte reprint. + harness. Mutations (a zero width, a zero height, a width of + 2^31, a height of 2^31, a width of 2^32 - 1, a height of + 2^32 - 1, a compression byte of 1, a filter byte of 1, an + interlace byte of 2, a first chunk of length 12) must be + rejected. Random well formed headers are built into whole + files and checked through `header` for their fields and + through `parse` for a byte for byte reprint. python3 tests/run_tests.py [--seed N] [--count N] @@ -646,6 +647,10 @@ def run_header_mutations(): cases = [ ("a width of zero", header_file(ihdr_full(0, 3, 8, 6))), ("a height of zero", header_file(ihdr_full(4, 0, 8, 6))), + ("a width of 2^31", header_file(ihdr_full(2**31, 3, 8, 6))), + ("a height of 2^31", header_file(ihdr_full(4, 2**31, 8, 6))), + ("a width of 2^32 - 1", header_file(ihdr_full(2**32 - 1, 3, 8, 6))), + ("a height of 2^32 - 1", header_file(ihdr_full(4, 2**32 - 1, 8, 6))), ("a compression byte of 1", header_file(ihdr_full(4, 3, 8, 6, comp=1))), ("a filter byte of 1", header_file(ihdr_full(4, 3, 8, 6, filt=1))), ("an interlace byte of 2", header_file(ihdr_full(4, 3, 8, 6, interlace=2))), @@ -792,6 +797,25 @@ def main(): timeout=120, ).stdout.strip() + # The axiom check: Proofs/Verify.lean prints the axioms of + # the four named theorems with `#print axioms`. Its output + # goes into the results file, in the Axiom check section. + axiom_run = subprocess.run( + ["lake", "env", "lean", "Proofs/Verify.lean"], + cwd=ROOT, + capture_output=True, + text=True, + timeout=600, + ) + axiom_lines = [ + line for line in axiom_run.stdout.strip().splitlines() if line.strip() + ] + if axiom_run.returncode != 0 or len(axiom_lines) != 4: + all_failures.append( + "axiom check: running Proofs/Verify.lean gave " + f"status {axiom_run.returncode} and {len(axiom_lines)} lines" + ) + out = ["# Test results", ""] out.append("Written by `tests/run_tests.py`. Rerun it to check these numbers.") out.append("") @@ -803,6 +827,17 @@ def main(): out.append(f"- Seed: {args.seed}") for line in all_lines: out.append(f"- {line}") + out.append("") + out.append("## Axiom check") + out.append("") + out.append( + "The output of `#print axioms` for the four named theorems, " + "from `lake env lean Proofs/Verify.lean`:" + ) + out.append("") + for line in axiom_lines: + out.append(f"- {line}") + out.append("") out.append("- Named differences: none") out.append(f"- Failures: {len(all_failures)}") for failure in all_failures[:50]: From 437849bf67c868665aba4e3b1c0092a5b78e6405 Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 20:47:24 -0500 Subject: [PATCH 3/3] Add the bar file set: Spec.lean, comparator.json, bar.toml, CI workflow --- .github/workflows/bar.yml | 21 +++++ Proofs.lean | 1 + Proofs/SpecProofs.lean | 139 +++++++++++++++++++++++++++++ README.md | 182 +++++++++++++++++++++++++++++--------- SPEC.md | 27 +++++- Spec.lean | 164 ++++++++++++++++++++++++++++++++++ bar.toml | 49 ++++++++++ comparator.json | 1 + lakefile.toml | 3 + 9 files changed, 545 insertions(+), 42 deletions(-) create mode 100644 .github/workflows/bar.yml create mode 100644 Proofs/SpecProofs.lean create mode 100644 Spec.lean create mode 100644 bar.toml create mode 100644 comparator.json diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.github/workflows/bar.yml @@ -0,0 +1,21 @@ +name: verified bar + +on: + push: + pull_request: + # Rerun when the spec reviewer approves, or an approval is dismissed. + pull_request_review: + types: [submitted, dismissed] + +jobs: + bar: + # pull-requests: read lets the check confirm the spec approval on GitHub. + permissions: + contents: read + pull-requests: read + # Both lines pin the same commit of Proven-Commons/mission: bar v2, as + # proposed in its pull request #2. Move both to a release tag once + # mission publishes one. + uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 + with: + bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 diff --git a/Proofs.lean b/Proofs.lean index e63d117..5a51e70 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -1,3 +1,4 @@ import Proofs.RoundTrip import Proofs.Header import Proofs.Verify +import Proofs.SpecProofs diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean new file mode 100644 index 0000000..f0809d9 --- /dev/null +++ b/Proofs/SpecProofs.lean @@ -0,0 +1,139 @@ +/- + Proofs of the statements in `Spec.lean`, under the same names. + + The round trips and the table are the theorems proved in + `Proofs/RoundTrip.lean` and `Proofs/Header.lean`. The refusals + are single inputs, checked in the kernel with `decide +kernel`: + no native evaluation, which the bar forbids. +-/ + +import Png +import Proofs.RoundTrip +import Proofs.Header + +open Png + +theorem Spec.parse_print {doc : Doc} (h : WF doc) : + parse (print doc) = some doc := + Png.Proofs.parse_print h + +theorem Spec.parseIhdr_print (h : Ihdr) (hwf : WFHeader h) : + parseIhdr (printIhdr h) = some h := + Png.Proofs.parseIhdr_print h hwf + +theorem Spec.checkPair_iff (ct bd : UInt8) : + checkPair ct bd = true ↔ + (ct.toNat, bd.toNat) ∈ allowedPairs := + Png.Proofs.checkPair_iff ct bd + +theorem Spec.parseFile_print {doc : Doc} (h : WFFull doc) : + ∃ hd : Ihdr, parseFile (print doc) = some (hd, doc) := + Png.Proofs.parseFile_print h + + +theorem Spec.rejects_bad_signature : + (parse ([118, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, 72, + 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 0, 180, 244, 174, + 198, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_bad_crc : + (parse ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, 72, + 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 0, 180, 244, 174, + 57, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_truncated_input : + (parse ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, 72, + 68, 82, 0, 0, 0, 4] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_first_chunk_length_12 : + (parse ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 12, 73, 72, + 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 240, 122, 129, + 218, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_zero_width : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 0, 0, 0, 0, 3, 8, 6, 0, 0, 0, 189, 31, + 14, 188, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_zero_height : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 0, 8, 6, 0, 0, 0, 50, 96, + 220, 104, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_width_at_cap : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 128, 0, 0, 0, 0, 0, 0, 3, 8, 6, 0, 0, 0, 29, 117, + 43, 171, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_height_at_cap : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 128, 0, 0, 0, 8, 6, 0, 0, 0, 84, 53, + 220, 39, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_illegal_depth : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 4, 2, 0, 0, 0, 254, 102, + 212, 144, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_unknown_colour_type : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 1, 0, 0, 0, 41, 35, + 150, 127, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_unknown_interlace : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 2, 90, 250, + 207, 234, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_nonzero_compression : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 1, 0, 0, 181, 54, + 196, 241, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_nonzero_filter : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 1, 0, 173, 239, + 159, 135, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_header_wrong_length : + (parseIhdr ([0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0] + : List UInt8)).isSome = false := by + decide +kernel diff --git a/README.md b/README.md index 2029841..a1feb33 100644 --- a/README.md +++ b/README.md @@ -1,25 +1,111 @@ -# png: a PNG chunk parser and printer, with a proved round trip +# png: a PNG chunk parser and printer, with proved round trips + +Status: in-progress + +A parser and printer for the chunk layer of PNG files, in Lean, +following the PNG specification. It reads the signature, then +each chunk's length, type, data, and CRC-32 check. Slice 2 adds +a decoder for the IHDR header: the width, height, bit depth, +colour type, and interlace method held in the first chunk's 13 +data bytes, checked against the validity rules of the PNG +specification. It does not decode pixels, and it does not +inflate IDAT data. The rules are written out in `SPEC.md`. + +The statements a reviewer approves are in `Spec.lean`, with +their proofs in `Proofs/SpecProofs.lean`. No reviewer has +approved them yet, so this project is not called verified. + +## How to run it + +`lake build` builds the library, the proofs, and the command +line tool. The tool reads one request per line: the word +`parse` or `header`, a space, and the file as comma-separated +decimal byte codes. `parse` answers `ok:` and the byte codes +of the canonical reprint of the parsed chunk list, or `none` +when the file is rejected. `header` reads the file at both +layers, the chunk list and the IHDR header decoded from the +first chunk's data, and answers `ok:` and the codes of a text +line naming the header fields, or `none` when the file is +rejected at either layer. A malformed request answers +`error`. -A PNG chunk parser and printer in Lean. It reads the chunk layer of a PNG file: the signature, then each chunk's length, type, data, and CRC-32 check. Slice 2 adds a decoder for the IHDR header: the width, height, bit depth, colour type, and interlace method held in the first chunk's 13 data bytes, checked against the validity rules of the PNG specification. It does not decode pixels, and it does not inflate IDAT data. The main claims are proved: parsing what the printer wrote returns the same chunk list, reading the printed bytes of a well formed header returns the header, and the bit depth table the checker uses is exactly the table the specification names. The tests run the parser against real PNG files built with Python's zlib and against a strict oracle written from the rules; see `tests/TEST-RESULTS.md` for the counts. +``` +lake build +echo "parse 137,80,78,71,13,10,26,10,0,0,0,13,73,72,68,82,0,0,0,1,0,0,0,1,8,2,0,0,0,144,119,83,222,0,0,0,0,73,69,78,68,174,66,96,130" | .lake/build/bin/png +``` -Status: in progress. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. +That request is a whole minimal PNG file as byte codes: the +signature, an IHDR chunk for a 1 by 1 image, and IEND. The +answer is `ok:` followed by the same codes, since the file is +valid and reprints byte for byte. A file the parser rejects, +such as the single code `120`, answers `none`. The same file +asked through `header`, with the word `header` in place of +`parse`, answers `ok:49,120,49,32,100,56,32,116,50,32,105,48`: +the codes of the text `1x1 d8 t2 i0`, the decoded header +fields. See `SPEC.md` for the full protocol. + +`python3 tests/run_tests.py` rebuilds the tool, runs the real +files, the hand built cases, the differential runs, and the +header sections, and writes the outcome to +`tests/TEST-RESULTS.md`. ## What is proved -The definitions are in `Png/Value.lean` (the chunk type, the printer, and the well-formedness rules), `Png/Parse.lean` (the parser), `Png/Crc32.lean` (the CRC-32), and `Png/Header.lean` (the IHDR header value, its reader and printer, and the file level read). The proofs are in `Proofs/RoundTrip.lean` and `Proofs/Header.lean`. +Each claim below names the theorem behind it. The theorems +are stated in `Spec.lean` (the challenge file, where they end +in `sorry`) and proved in `Proofs/SpecProofs.lean`, under the +same names. `comparator.json` lists all of them. | Claim | Theorem | |-------|---------| -| Parsing the printed form of a well formed chunk list gives the list back. | `Png.Proofs.parse_print` | -| Reading back one printed chunk, with any bytes after it, gives the chunk and those bytes untouched. | `Png.Proofs.parseChunk_printChunk` | -| Four bytes printed from a value below 2^32 read back as the value. | `Png.Proofs.u32_be32` | -| Reading the printed bytes of a well formed IHDR header gives the header back. | `Png.Proofs.parseIhdr_print` | -| The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair. | `Png.Proofs.checkPair_iff` | -| Printing a fully well formed document and reading it back at both layers gives the document back, header included. | `Png.Proofs.parseFile_print` | - -A chunk list is well formed when it is a first chunk, then any middle chunks, then the IEND chunk; the first chunk has type IHDR and 13 data bytes; no chunk before the last is the IEND chunk; every chunk type is four ASCII letters; and every data length is below 2^31. A header is well formed when its width and height are above zero and below 2^31, its interlace byte is 0 or 1, and its bit depth is one its colour type allows. Each of these theorems checks against two of the standard axioms (`propext`, `Quot.sound`), which a reader can confirm with `#print axioms` on the theorem's name. - -The command-line tool in `Main.lean` calls these functions directly. +| Parsing the printed form of a well formed chunk list gives the list back. | `Spec.parse_print` | +| Reading the printed bytes of a well formed IHDR header gives the header back. | `Spec.parseIhdr_print` | +| The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair. | `Spec.checkPair_iff` | +| Printing a fully well formed document and reading it back at both layers gives the document back, header included. | `Spec.parseFile_print` | +| A file whose first signature byte is wrong is refused. | `Spec.rejects_bad_signature` | +| A file whose IHDR chunk carries a CRC that does not match its type and data is refused. | `Spec.rejects_bad_crc` | +| A file cut short inside its first chunk is refused. | `Spec.rejects_truncated_input` | +| A file whose first chunk holds 12 data bytes is refused: an IHDR chunk holds 13. | `Spec.rejects_first_chunk_length_12` | +| A file with a width of zero is refused. | `Spec.rejects_zero_width` | +| A file with a height of zero is refused. | `Spec.rejects_zero_height` | +| A file with a width of 2^31 is refused: the width stays below 2^31. | `Spec.rejects_width_at_cap` | +| A file with a height of 2^31 is refused: the height stays below 2^31. | `Spec.rejects_height_at_cap` | +| A file with bit depth 4 on colour type 2 is refused: that colour type allows depths 8 and 16 only. | `Spec.rejects_illegal_depth` | +| A file with colour type 1 is refused: 1 is not a PNG colour type, and allows no bit depth. | `Spec.rejects_unknown_colour_type` | +| A file with an interlace byte of 2 is refused: the byte is 0 or 1. | `Spec.rejects_unknown_interlace` | +| A file with a compression byte of 1 is refused: the only compression method is 0. | `Spec.rejects_nonzero_compression` | +| A file with a filter byte of 1 is refused: the only filter method is 0. | `Spec.rejects_nonzero_filter` | +| The header reader refuses anything but exactly 13 bytes: here a valid header's first 12 bytes. | `Spec.rejects_header_wrong_length` | + +A chunk list is well formed when it is a first chunk, then +any middle chunks, then the IEND chunk; the first chunk has +type IHDR and 13 data bytes; no chunk before the last is the +IEND chunk; every chunk type is four ASCII letters; and every +data length is below 2^31. A header is well formed when its +width and height are above zero and below 2^31, its interlace +byte is 0 or 1, and its bit depth is one its colour type +allows. A document is fully well formed when it is well +formed at the chunk layer and its first chunk's data is the +printed form of a well formed header. + +The headline theorems rest on the proofs in +`Proofs/RoundTrip.lean` and `Proofs/Header.lean`, where they +are `Png.Proofs.parse_print`, `Png.Proofs.parseIhdr_print`, +`Png.Proofs.checkPair_iff`, and `Png.Proofs.parseFile_print`. +Each checks against two of the standard axioms (`propext`, +`Quot.sound`), which a reader can confirm with `#print +axioms`, or by running `lake env lean Proofs/Verify.lean`. +The refusal theorems are single inputs checked in the kernel +with `decide +kernel`. + +The definitions are in `Png/Value.lean` (the chunk type, the +printer, and the well formedness rules), `Png/Parse.lean` +(the parser), `Png/Crc32.lean` (the CRC-32), and +`Png/Header.lean` (the IHDR header value, its reader and +printer, and the file level read). The command line tool in +`Main.lean` calls `Png.parse`, `Png.print`, and +`Png.parseFile` directly, the same functions the theorems are +about. ## What is not proved @@ -31,33 +117,47 @@ The command-line tool in `Main.lean` calls these functions directly. ## What you must trust -- The Lean kernel, which checks the proofs. -- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. -- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. -- The operating system and hardware it runs on. -- Python's standard library, including zlib, as the oracle in the tests. The results file names the versions used. - -This project has no dependencies beyond Lean itself. - -## Run it - -Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: - -``` -lake build -echo "parse 137,80,78,71,13,10,26,10,0,0,0,13,73,72,68,82,0,0,0,1,0,0,0,1,8,2,0,0,0,144,119,83,222,0,0,0,0,73,69,78,68,174,66,96,130" | .lake/build/bin/png -``` - -That request is a whole minimal PNG file as byte codes: the signature, an IHDR chunk for a 1 by 1 image, and IEND. The answer is `ok:` followed by the same codes, since the file is valid and reprints byte for byte. A file the parser rejects, such as the single code `120`, answers `none`. A malformed request answers `error`. The same file asked through `header`, with the word `header` in place of `parse`, answers `ok:49,120,49,32,100,56,32,116,50,32,105,48`: the codes of the text `1x1 d8 t2 i0`, the decoded header fields. See `SPEC.md` for the full protocol. +- The Lean kernel (Lean 4.35.0, pinned in + `lean-toolchain`), which checks every proof. +- The Lean compiler, with the C compiler and linker shipped + with it, which turns the proved definitions into the + program that runs. +- The Lean runtime, which runs that program. +- The hardware the program runs on. +- Every dependency in `lake-manifest.json`: the manifest + lists no packages, so there are no library dependencies to + trust beyond the Lean toolchain itself. +- Lean's core library, including the compiled code it puts + in place of some definitions the proofs reason about. +- The operating system the program runs on. +- That `SPEC.md` states the reading of the PNG specification + you intend. The proofs are about the parser, printer, and + header reader in this repo following each other exactly; + the fidelity of the spec to the PNG specification is a + reading, pinned in `SPEC.md` where the PNG specification + leaves a choice open. +- Python's standard library, including zlib, as the oracle + in the tests. The results file names the versions used. +- The line handling in `Main.lean` (splitting a request + line, reading decimal codes). The tests drive it, and no + proof covers it. +- There are no exceptions to item 4 of the bar: the project + uses none of the features it forbids. ## Re-check it -Needs Linux, elan, and Python 3.11 or later. - -``` -lake build -grep -rn "sorry" --include="*.lean" Png Proofs Main.lean Png.lean Proofs.lean -python3 tests/run_tests.py -``` - -The grep should print nothing: there is no `sorry` anywhere. The test script rebuilds the tool, builds real PNG files with Python zlib, runs hand-built chunk cases, runs the differential tests with a fixed seed, and writes the counts to `tests/TEST-RESULTS.md`. +1. `lake comparator --paranoid`: builds the challenge file + `Spec.lean` and the proofs in a sandbox and checks that + each theorem named in `comparator.json` proves exactly + the statement in the challenge file, uses no axiom but + the three standard ones, and is accepted by Lean's kernel + and every other kernel shipped with Lean. +2. `python3 tests/run_tests.py`: the real files, the hand + built cases, the differential runs against the oracle, + the mutations, and the header sections, with counts and + any failures written to `tests/TEST-RESULTS.md`. +3. `lake build`: the library, the proofs, and the tool build + clean, and `lake env lean Proofs/Verify.lean` prints the + axiom list for the headline theorems. +4. Read `SPEC.md` against the PNG specification and check + the pinned readings are the ones you want. diff --git a/SPEC.md b/SPEC.md index 9ae055d..7515d58 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # Specification: png -A PNG chunk parser and printer in Lean, with (slice 2) a decoder for the IHDR header. It does not decode pixels, and it does not inflate IDAT data. A reviewer who did not write this specification approves it, together with any statement file a reviewer adds later. No such file exists yet, so nothing here counts toward the verified bar yet. +A PNG chunk parser and printer in Lean, with (slice 2) a decoder for the IHDR header. It does not decode pixels, and it does not inflate IDAT data. The claims below are stated as Lean theorems in `Spec.lean`. A reviewer who did not write this specification or those statements approves them; no reviewer has yet, so nothing here counts toward the verified bar. Bytes are `List UInt8` throughout. @@ -81,6 +81,31 @@ No claim is made that the parser accepts every file the rules above allow, or re The round trip needs no fact about CRC-32 itself: the parser and the printer compute the same function of the same bytes, so a printed file passes its own CRC checks by construction. That the function is the standard CRC-32 rests on the differential tests against Python zlib's `crc32`. +## Properties and their theorems + +Each property above names its theorem. The theorems are stated in `Spec.lean` and proved in `Proofs/SpecProofs.lean`, under the same names. `comparator.json` lists all of them. + +| Property | Theorem | +|----------|---------| +| Parsing the printed form of a well formed chunk list gives the list back | `Spec.parse_print` | +| Reading the printed bytes of a well formed IHDR header gives the header back | `Spec.parseIhdr_print` | +| The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair | `Spec.checkPair_iff` | +| Printing a fully well formed document and reading it back at both layers gives the document back, header included | `Spec.parseFile_print` | +| A file whose first signature byte is wrong is refused | `Spec.rejects_bad_signature` | +| A file whose IHDR chunk carries a CRC that does not match its type and data is refused | `Spec.rejects_bad_crc` | +| A file cut short inside its first chunk is refused | `Spec.rejects_truncated_input` | +| A file whose first chunk holds 12 data bytes is refused: an IHDR chunk holds 13 | `Spec.rejects_first_chunk_length_12` | +| A file with a width of zero is refused | `Spec.rejects_zero_width` | +| A file with a height of zero is refused | `Spec.rejects_zero_height` | +| A file with a width of 2^31 is refused: the width stays below 2^31 | `Spec.rejects_width_at_cap` | +| A file with a height of 2^31 is refused: the height stays below 2^31 | `Spec.rejects_height_at_cap` | +| A file with bit depth 4 on colour type 2 is refused: that colour type allows depths 8 and 16 only | `Spec.rejects_illegal_depth` | +| A file with colour type 1 is refused: 1 is not a PNG colour type, and allows no bit depth | `Spec.rejects_unknown_colour_type` | +| A file with an interlace byte of 2 is refused: the byte is 0 or 1 | `Spec.rejects_unknown_interlace` | +| A file with a compression byte of 1 is refused: the only compression method is 0 | `Spec.rejects_nonzero_compression` | +| A file with a filter byte of 1 is refused: the only filter method is 0 | `Spec.rejects_nonzero_filter` | +| The header reader refuses anything but exactly 13 bytes: here a valid header's first 12 bytes | `Spec.rejects_header_wrong_length` | + ## The command-line tool `Main.lean` reads one request per line. The operations are `parse` and `header`: the request is the operation word, a space, and the byte codes of a PNG file as comma-separated decimal numbers. The `parse` answer is `ok:` followed by the byte codes of the canonical reprint of the parsed chunk list, or `none` when the file is rejected. The `header` answer is `ok:` followed by the codes of a text line naming the decoded header fields, or `none` when the file is rejected at either layer. The text is the width in decimal, the letter `x`, the height in decimal, a space, the letter `d`, the bit depth in decimal, a space, the letter `t`, the colour type in decimal, a space, the letter `i`, and the interlace method in decimal: for a 1920 by 1080 file at bit depth 8, colour type 6, no interlace, the text is `1920x1080 d8 t6 i0`, and the answer carries the character codes of that text. A malformed request line prints `error`. A code above 255 makes the request malformed, since no byte holds it. diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..7ccb420 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,164 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the SHA-256 it had then. The proofs live in `Proofs` + (`Proofs/SpecProofs.lean`); `lake comparator` checks that each one + proves exactly the statement written here. The `sorry` below is + expected in this file only. + + The statements use only the definitions in `Png/Value.lean`, + `Png/Parse.lean`, `Png/Crc32.lean`, and `Png/Header.lean`, the + code under proof named in `bar.toml`. No definition of their own + is needed, so this project has no `Spec/Defs.lean`. +-/ + +import Png + +open Png + +/-! ## The round trips and the table + +The statements the slice stands on. Each one is the statement of +the proved theorem of the same shape in `Proofs/RoundTrip.lean` +or `Proofs/Header.lean`, over the same well formedness +predicates, `Png.WF`, `Png.WFHeader`, and `Png.WFFull`. -/ + +/-- Parsing the printed form of a well formed chunk list gives + the list back. So a printer that wrote nothing, or wrote + something shorter, fails this statement. -/ +theorem Spec.parse_print {doc : Doc} (h : WF doc) : + parse (print doc) = some doc := sorry + +/-- Reading the printed bytes of a well formed IHDR header gives + the header back. -/ +theorem Spec.parseIhdr_print (h : Ihdr) (hwf : WFHeader h) : + parseIhdr (printIhdr h) = some h := sorry + +/-- The depth checker agrees with the written out table of + allowed (colour type, bit depth) pairs on every byte pair. -/ +theorem Spec.checkPair_iff (ct bd : UInt8) : + checkPair ct bd = true ↔ + (ct.toNat, bd.toNat) ∈ allowedPairs := sorry + +/-- Printing a fully well formed document and reading it back at + both layers gives the document back, with its header. -/ +theorem Spec.parseFile_print {doc : Doc} (h : WFFull doc) : + ∃ hd : Ihdr, parseFile (print doc) = some (hd, doc) := sorry + +/-! ## Refused inputs + +Single inputs the reader refuses, one for each headline rule of +`SPEC.md`. Each input is one of the named rejection cases in the +test harness: the chunk layer cases stand as the harness builds +them for its `parse` requests, and the header cases are whole +files whose CRCs are recomputed, as the harness builds them for +its `header` requests, so the refusal is for the header rule +itself. The differential tests cover these rules on many more +inputs; these statements pin them so a reader of the +specification can check each rule against one concrete case. -/ + +/-- A file whose first signature byte is wrong is refused. -/ +theorem Spec.rejects_bad_signature : + (parse ([118, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, 72, + 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 0, 180, 244, 174, + 198, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file whose IHDR chunk carries a CRC that does not match + its type and data is refused. -/ +theorem Spec.rejects_bad_crc : + (parse ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, 72, + 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 0, 180, 244, 174, + 57, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file cut short inside its first chunk is refused: the + first twenty bytes of a valid file, and no more. -/ +theorem Spec.rejects_truncated_input : + (parse ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, 72, + 68, 82, 0, 0, 0, 4] : List UInt8)).isSome = false := sorry + +/-- A file whose first chunk holds 12 data bytes is refused: an + IHDR chunk holds 13. -/ +theorem Spec.rejects_first_chunk_length_12 : + (parse ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 12, 73, 72, + 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 240, 122, 129, + 218, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with a width of zero is refused. -/ +theorem Spec.rejects_zero_width : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 0, 0, 0, 0, 3, 8, 6, 0, 0, 0, 189, 31, + 14, 188, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with a height of zero is refused. -/ +theorem Spec.rejects_zero_height : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 0, 8, 6, 0, 0, 0, 50, 96, + 220, 104, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with a width of 2^31 is refused: the width stays + below 2^31. -/ +theorem Spec.rejects_width_at_cap : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 128, 0, 0, 0, 0, 0, 0, 3, 8, 6, 0, 0, 0, 29, 117, + 43, 171, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with a height of 2^31 is refused: the height stays + below 2^31. -/ +theorem Spec.rejects_height_at_cap : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 128, 0, 0, 0, 8, 6, 0, 0, 0, 84, 53, + 220, 39, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with bit depth 4 on colour type 2 is refused: that + colour type allows depths 8 and 16 only. -/ +theorem Spec.rejects_illegal_depth : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 4, 2, 0, 0, 0, 254, 102, + 212, 144, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with colour type 1 is refused: 1 is not a PNG colour + type, and allows no bit depth. -/ +theorem Spec.rejects_unknown_colour_type : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 1, 0, 0, 0, 41, 35, + 150, 127, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with an interlace byte of 2 is refused: the byte is + 0 or 1. -/ +theorem Spec.rejects_unknown_interlace : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0, 2, 90, 250, + 207, 234, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with a compression byte of 1 is refused: the only + compression method is 0. -/ +theorem Spec.rejects_nonzero_compression : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 1, 0, 0, 181, 54, + 196, 241, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- A file with a filter byte of 1 is refused: the only filter + method is 0. -/ +theorem Spec.rejects_nonzero_filter : + (parseFile ([137, 80, 78, 71, 13, 10, 26, 10, 0, 0, 0, 13, 73, + 72, 68, 82, 0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 1, 0, 173, 239, + 159, 135, 0, 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := sorry + +/-- The header reader refuses anything but exactly 13 bytes: + here a valid header's first 12 bytes. -/ +theorem Spec.rejects_header_wrong_length : + (parseIhdr ([0, 0, 0, 4, 0, 0, 0, 3, 8, 6, 0, 0] + : List UInt8)).isSome = false := sorry diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..ce857db --- /dev/null +++ b/bar.toml @@ -0,0 +1,49 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "png" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. +spec_authors = ["abu-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean"] +# The code under proof: the functions the statements are about. +code = [ + # The data types the statements are about. + "Png.Chunk", "Png.Doc", "Png.Ihdr", + # The byte forms and the printer. + "Png.signature", "Png.Chunk.typeBytes", "Png.isLetter", + "Png.ihdrType", "Png.iendType", "Png.iendChunk", "Png.isIEND", + "Png.be32", "Png.u32", "Png.chunkCrc", "Png.printChunk", + "Png.print", + # The CRC-32 the chunk checks use. + "Png.Crc32.step", "Png.Crc32.step8", "Png.Crc32.table", + "Png.Crc32.update", "Png.Crc32.crc32", + # Well formedness at the chunk layer. + "Png.WFChunk", "Png.WF", + # The chunk readers and the parser. + "Png.get4", "Png.parseChunk", "Png.parseChunks", "Png.parse", + # The IHDR header: the allowed table, the check, well + # formedness, the printer, the reader, and the file level read. + "Png.allowedDepths", "Png.pairAllowed", "Png.allowedPairs", + "Png.checkPair", "Png.WFHeader", "Png.printIhdr", + "Png.parseIhdr", "Png.headerOf", "Png.parseFile", "Png.WFFull", +] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/png/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..46b2955 --- /dev/null +++ b/comparator.json @@ -0,0 +1 @@ +{"challenge_module":"Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Proofs","theorem_names":["Spec.parse_print","Spec.parseIhdr_print","Spec.checkPair_iff","Spec.parseFile_print","Spec.rejects_bad_signature","Spec.rejects_bad_crc","Spec.rejects_truncated_input","Spec.rejects_first_chunk_length_12","Spec.rejects_zero_width","Spec.rejects_zero_height","Spec.rejects_width_at_cap","Spec.rejects_height_at_cap","Spec.rejects_illegal_depth","Spec.rejects_unknown_colour_type","Spec.rejects_unknown_interlace","Spec.rejects_nonzero_compression","Spec.rejects_nonzero_filter","Spec.rejects_header_wrong_length"]} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index 33d541c..03a3e2b 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,6 +8,9 @@ name = "Png" [[lean_lib]] name = "Proofs" +[[lean_lib]] +name = "Spec" + [[lean_exe]] name = "png" root = "Main"