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/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..9bd3a70 --- /dev/null +++ b/Png/Header.lean @@ -0,0 +1,127 @@ +/- + 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 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: + + 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. + + The file level read also turns a file away when a chunk after + the first has type IHDR: the PNG specification allows one IHDR + chunk, and it comes first. The chunk layer of slice 1 does not + look at this; only the file level read does. + + The written out table of allowed pairs, and well formedness of + a header and of a whole document, give the statements their + meaning and no code uses them, so they are part of the + specification, in `Png/Spec/Defs.lean`. +-/ + +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) + +/-- 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 + +/-- 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 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 := + 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 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 + some ⟨u32 w1 w2 w3 w4, u32 h1 h2 h3 h4, bd, ct, int⟩ + else none + | _ => none + +/-- Is this chunk an IHDR chunk, by its type bytes? -/ +def isIHDR (c : Chunk) : Bool := decide (c.typeBytes = ihdrType) + +/-- The decoded header of a chunk list: the first chunk's data + read as a header. It is `none` when there is no first chunk, + when any later chunk is also of type IHDR (the PNG + specification allows one IHDR chunk, and it comes first), or + when the first chunk's data does not read as a header. -/ +def headerOf (doc : Doc) : Option Ihdr := + match doc with + | c :: rest => if rest.any isIHDR then none else 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, + or that holds a second IHDR chunk, 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 + +end Png diff --git a/Png/Proofs.lean b/Png/Proofs.lean index 569a369..fe10eff 100644 --- a/Png/Proofs.lean +++ b/Png/Proofs.lean @@ -1,2 +1,6 @@ import Png.Proofs.RoundTrip +import Png.Proofs.Header +import Png.Proofs.Sound +import Png.Proofs.Layout import Png.Proofs.Verify +import Png.Proofs.SpecProofs diff --git a/Png/Proofs/Header.lean b/Png/Proofs/Header.lean new file mode 100644 index 0000000..c04df2f --- /dev/null +++ b/Png/Proofs/Header.lean @@ -0,0 +1,236 @@ +/- + 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`, and its converse + is `parseIhdr_sound`: a header the reader accepts is well + formed, and the bytes it read are its printed form. The file + level claim is `parseFile_print`: a fully well formed document + with header `hd` (chunk layer well formed, first chunk the + printed form of the well formed header `hd`, no second IHDR) + prints and reads back whole, and the header the read returns + is `hd` itself. Its converse, `parseFile_sound`, is in + `Png/Proofs/Sound.lean`. +-/ + +import Png +import Png.Spec.Defs +import Png.Proofs.RoundTrip + +namespace Png.Proofs + +open Png Png.Spec + +/-- 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 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 + 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 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 [ite_eq_right h0, ite_eq_right h2, ite_eq_right h3, ite_eq_right h4, ite_eq_right 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 + +/-- 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 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⟩ = + (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 (by omega), u32_be32 hh (by omega)] + rw [ite_eq_right (by simp : ¬ (([] : List UInt8) ≠ []))] + rw [ite_eq_right (by omega : ¬ (w = 0 ∨ hh = 0))] + rw [ite_eq_right (by omega : ¬ (w ≥ 2147483648 ∨ hh ≥ 2147483648))] + rw [ite_eq_right (by decide : ¬ ((0 : UInt8) ≠ 0 ∨ (0 : UInt8) ≠ 0))] + rw [ite_eq_right hnl, ite_eq_left ((checkPair_iff ct bd).mpr hpair)] + +/-- Four bytes read big endian and printed again are the same + four bytes. -/ +theorem be32_u32 (a b c d : UInt8) : be32 (u32 a b c d) = [a, b, c, d] := by + have ha := a.toNat_lt + have hb := b.toNat_lt + have hc := c.toNat_lt + have hd := d.toNat_lt + simp only [be32, u32, List.cons.injEq, and_true] + refine ⟨?_, ?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> rw [toUInt8_toNat] <;> omega + +/-- Four bytes read big endian give a value below 2^32. -/ +theorem u32_lt (a b c d : UInt8) : u32 a b c d < 4294967296 := by + have ha := a.toNat_lt + have hb := b.toNat_lt + have hc := c.toNat_lt + have hd := d.toNat_lt + simp only [u32] + omega + +/-- A byte that is not above 1 is 0 or 1. -/ +theorem uint8_le_one {i : UInt8} (h : ¬ i > 1) : i = 0 ∨ i = 1 := by + have h' : ¬ (1 : UInt8).toNat < i.toNat := + fun x => h (UInt8.lt_iff_toNat_lt.mpr x) + have : i.toNat = 0 ∨ i.toNat = 1 := by simp at h'; omega + rcases this with e | e + · left; exact UInt8.toNat_inj.mp (by simpa using e) + · right; exact UInt8.toNat_inj.mp (by simpa using e) + +/-- The header reader is sound: a header it accepts is well + formed, and the bytes it read are that header's printed form. + So every rejection rule holds of what it accepts: the width + and the height are above zero and below 2^31, the interlace + byte is 0 or 1, the depth is one the colour type allows (by + `checkPair_iff`, a pair of the written out table), there were + exactly 13 bytes, and the compression and filter bytes were + zero, since `printIhdr` writes zero there. -/ +theorem parseIhdr_sound {bs : List UInt8} {h : Ihdr} + (hp : parseIhdr bs = some h) : WFHeader h ∧ printIhdr h = bs := by + unfold parseIhdr at hp + split at hp + · rename_i w1 w2 w3 w4 h1 h2 h3 h4 bd ct comp filt int rest + split at hp + · cases hp + rename_i hr + split at hp + · cases hp + rename_i hz + split at hp + · cases hp + rename_i hb + split at hp + · cases hp + rename_i hc + split at hp + · cases hp + rename_i hi + split at hp + · rename_i hpair + cases hp + have hr' : rest = [] := Decidable.of_not_not hr + have hcomp : comp = 0 := Decidable.of_not_not (not_or.mp hc).1 + have hfilt : filt = 0 := Decidable.of_not_not (not_or.mp hc).2 + subst hr' hcomp hfilt + refine ⟨⟨(by omega : 0 < u32 w1 w2 w3 w4), + (by omega : u32 w1 w2 w3 w4 < 2147483648), + (by omega : 0 < u32 h1 h2 h3 h4), + (by omega : u32 h1 h2 h3 h4 < 2147483648), + uint8_le_one hi, (checkPair_iff ct bd).mp hpair⟩, ?_⟩ + show be32 (u32 w1 w2 w3 w4) ++ be32 (u32 h1 h2 h3 h4) + ++ [bd, ct, 0, 0, int] = _ + rw [be32_u32, be32_u32] + rfl + · cases hp + · cases hp + +/-- The header reader, exactly: it accepts the bytes `bs` with + header `h` if and only if `h` is well formed and `bs` is its + printed form. -/ +theorem parseIhdr_iff (bs : List UInt8) (h : Ihdr) : + parseIhdr bs = some h ↔ WFHeader h ∧ printIhdr h = bs := + ⟨parseIhdr_sound, fun ⟨hwf, hp⟩ => hp ▸ parseIhdr_print h hwf⟩ + +/-- A fully well formed document is well formed at the chunk + layer. -/ +theorem wfFull_wf {hd : Ihdr} {doc : Doc} (h : WFFull hd doc) : WF doc := by + obtain ⟨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 with header `hd` and reading the file back at both + layers gives back `hd` itself and the document. -/ +theorem parseFile_print {hd : Ihdr} {doc : Doc} (h : WFFull hd doc) : + parseFile (print doc) = some (hd, doc) := by + have hwf : WF doc := wfFull_wf h + obtain ⟨head, mid, hdoc, htype, hdata, hwfhd, hall, hnot, hone⟩ := h + have hany : (mid ++ [iendChunk]).any isIHDR = false := by + rw [List.any_eq_false] + intro c hc + rcases List.mem_append.mp hc with hm | hm + · simpa [isIHDR] using hone c hm + · rw [List.mem_singleton.mp hm] + decide + unfold parseFile + rw [parse_print hwf] + show (headerOf doc).map (fun x => (x, doc)) = some (hd, doc) + rw [hdoc] + simp [headerOf, hany, hdata, parseIhdr_print hd hwfhd] + +end Png.Proofs diff --git a/Png/Proofs/Layout.lean b/Png/Proofs/Layout.lean new file mode 100644 index 0000000..365a1cd --- /dev/null +++ b/Png/Proofs/Layout.lean @@ -0,0 +1,70 @@ +/- + The byte layout: the bytes the chunk printer and the header + printer write, stated with `Png.Spec.bigEndian4`, the four bytes of + a number most significant first, and the type bytes and the + letter test the chunk rules use. The round trips and their + converses tie each reader to its printer; these tie each + printer to the layout of the PNG specification, so that a + printer and a reader that agreed on some other layout (the + height before the width, say) would not meet the statements. + + The code writes four byte numbers with `be32`, which takes each + byte with `Nat.toUInt8`; `bigEndian4` writes them with + `UInt8.ofNat` of the base 256 digit. `be32_eq_bigEndian4` says + the two agree on every number. +-/ + +import Png +import Png.Spec.Defs + +namespace Png.Proofs + +open Png Png.Spec + +/-- A number's byte is the byte of its last base 256 digit. -/ +theorem toUInt8_eq_ofNat_mod (n : Nat) : n.toUInt8 = UInt8.ofNat (n % 256) := by + apply UInt8.toNat_inj.mp + simp [Nat.toUInt8] + +/-- The code's four bytes big endian are the specification's. -/ +theorem be32_eq_bigEndian4 (n : Nat) : be32 n = bigEndian4 n := by + unfold be32 bigEndian4 + rw [toUInt8_eq_ofNat_mod (n / 16777216), toUInt8_eq_ofNat_mod (n / 65536), + toUInt8_eq_ofNat_mod (n / 256), toUInt8_eq_ofNat_mod n] + +/-- The chunk layout: the signature, then each chunk as its + length, its four type bytes in order, its data, and its + CRC-32, the length and the CRC four bytes big endian. -/ +theorem print_layout (doc : Doc) : + print doc = [137, 80, 78, 71, 13, 10, 26, 10] ++ + doc.flatMap (fun c => + bigEndian4 c.data.length ++ [c.t1, c.t2, c.t3, c.t4] ++ c.data ++ + bigEndian4 (Crc32.crc32 ([c.t1, c.t2, c.t3, c.t4] ++ c.data)).toNat) := by + unfold print signature + congr 1 + apply congrArg (List.flatMap · doc) + funext c + simp only [printChunk, chunkCrc, Chunk.typeBytes, be32_eq_bigEndian4] + +/-- The IHDR layout: width, height, four bytes big endian each, + then bit depth, colour type, compression zero, filter zero, + and interlace. -/ +theorem printIhdr_layout (h : Ihdr) : + printIhdr h = bigEndian4 h.width ++ bigEndian4 h.height ++ + [h.bitDepth, h.colorType, 0, 0, h.interlace] := by + simp only [printIhdr, be32_eq_bigEndian4] + +/-- The letter test: A to Z, or a to z, by the byte's value. -/ +theorem isLetter_iff (b : UInt8) : + isLetter b = true ↔ + (65 ≤ b.toNat ∧ b.toNat ≤ 90) ∨ (97 ≤ b.toNat ∧ b.toNat ≤ 122) := by + simp [isLetter, UInt8.le_iff_toNat_le] + +/-- The IEND chunk test: type bytes I, E, N, D, and no data. -/ +theorem isIEND_iff (c : Chunk) : + isIEND c = true ↔ [c.t1, c.t2, c.t3, c.t4] = [73, 69, 78, 68] ∧ c.data = [] := by + unfold isIEND iendType Chunk.typeBytes + rw [Bool.and_eq_true, List.isEmpty_iff] + exact and_congr_left fun _ => decide_eq_true_iff + +end Png.Proofs diff --git a/Png/Proofs/RoundTrip.lean b/Png/Proofs/RoundTrip.lean index f55d727..4c6b941 100644 --- a/Png/Proofs/RoundTrip.lean +++ b/Png/Proofs/RoundTrip.lean @@ -17,10 +17,11 @@ -/ import Png +import Png.Spec.Defs namespace Png.Proofs -open Png +open Png Png.Spec /-- A byte printed from a number reads back as the number modulo 256. -/ @@ -100,19 +101,19 @@ theorem parseChunk_printChunk (c : Chunk) (r : List UInt8) :: ((c.data ++ be32 (chunkCrc c).toNat) ++ r) := rfl rw [e, parseChunk_step, u32_be32 c.data.length hlen32] have hge : ¬ c.data.length ≥ 2147483648 := by omega - rw [if_neg hge] + rw [ite_eq_right hge] have hletters : (isLetter c.t1 && isLetter c.t2 && isLetter c.t3 && isLetter c.t4) = true := by simp [h1, h2, h3, h4] - rw [if_pos hletters] + rw [ite_eq_left hletters] rw [List.append_assoc, List.take_left, List.drop_left, get4_be32 _ hcrc32] - rw [if_neg (by simp : ¬ c.data.length ≠ c.data.length)] + rw [ite_eq_right (by simp : ¬ c.data.length ≠ c.data.length)] show (if (chunkCrc c).toNat = (Crc32.crc32 ([c.t1, c.t2, c.t3, c.t4] ++ c.data)).toNat then some (⟨c.t1, c.t2, c.t3, c.t4, c.data⟩, r) else none) = some (c, r) - rw [if_pos (show (chunkCrc c).toNat + rw [ite_eq_left (show (chunkCrc c).toNat = (Crc32.crc32 ([c.t1, c.t2, c.t3, c.t4] ++ c.data)).toNat from rfl)] /-- One step of the chunk list reader, stated for rewriting. -/ @@ -171,7 +172,7 @@ theorem parseChunks_printChunks : ∀ (pre : Doc) (last : Chunk) = printChunk c ++ (pre ++ [last]).flatMap printChunk := by simp [List.flatMap_cons] rw [hform, parseChunks_succ, hpc] - simp only [hcnot, Bool.false_eq_true, if_false, hI, + simp only [hcnot, Bool.false_eq_true, ite_false, hI, List.cons_append] /-- The signature at the front of a printed document. -/ @@ -223,6 +224,6 @@ theorem parse_print {doc : Doc} (h : WF doc) : parse (print doc) = some doc := b show (if head.typeBytes = ihdrType ∧ head.data.length = 13 then some (head :: mid ++ [iendChunk]) else none) = some (head :: mid ++ [iendChunk]) - rw [if_pos ⟨htype, hlen13⟩] + rw [ite_eq_left ⟨htype, hlen13⟩] end Png.Proofs diff --git a/Png/Proofs/Sound.lean b/Png/Proofs/Sound.lean new file mode 100644 index 0000000..3ceb8f3 --- /dev/null +++ b/Png/Proofs/Sound.lean @@ -0,0 +1,243 @@ +/- + Soundness: the converse of the round trips. Whatever the + readers accept is the printed form of a well formed value, and + the value they return is that value. + + - `parse_sound`: a file the chunk parser accepts is the printed + form of the chunk list it returns, and that list is well + formed (`WF`). + - `parseFile_sound`: a file the file level read accepts is the + printed form of the chunk list it returns, and that list is + fully well formed with the header it returns (`WFFull`). + + With the round trips `parse_print` and `parseFile_print`, each + reader is pinned exactly (`parse_iff`, `parseFile_iff`): it + accepts a file if and only if the file is the printed form of a + well formed value, and then returns that value. So every rule + the well formedness predicates state is a rejection rule the + reader keeps: a file that breaks one is refused. + + The steps follow the readers: four bytes read and printed again + are the same bytes (`be32_u32`, in `Png/Proofs/Header.lean`); one + chunk the chunk reader accepts is a well formed chunk printed in + front of the rest of the input; a list of chunks read to IEND is + the printed list, ending in the IEND chunk; then the signature + and the IHDR check at the top level, and the header on top. +-/ + +import Png +import Png.Spec.Defs +import Png.Proofs.RoundTrip +import Png.Proofs.Header + +namespace Png.Proofs + +open Png Png.Spec + +/-- Four bytes the reader takes off the front of the input are + the printed form of the value it returns, and that value is + below 2^32. -/ +theorem get4_sound {bs : List UInt8} {n : Nat} {r : List UInt8} + (h : get4 bs = some (n, r)) : n < 4294967296 ∧ be32 n ++ r = bs := by + unfold get4 at h + split at h + · rename_i a b c d rest + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact ⟨u32_lt a b c d, by rw [be32_u32]; rfl⟩ + · cases h + +/-- One chunk the chunk reader accepts is a well formed chunk, + and the input was its printed form followed by the rest the + reader returns. -/ +theorem parseChunk_sound {bs : List UInt8} {c : Chunk} {r : List UInt8} + (h : parseChunk bs = some (c, r)) : WFChunk c ∧ printChunk c ++ r = bs := by + unfold parseChunk at h + split at h + · cases h + rename_i len rest1 hg + obtain ⟨_, hbs⟩ := get4_sound hg + split at h + · cases h + rename_i hlen + split at h + · rename_i t1 t2 t3 t4 rest2 + split at h + · rename_i hletters + dsimp only at h + split at h + · cases h + rename_i hdl + split at h + · cases h + rename_i crcVal rest3 hg2 + split at h + · rename_i hcrc + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + obtain ⟨_, hrest2⟩ := get4_sound hg2 + have hl : (rest2.take len).length = len := Decidable.of_not_not hdl + simp only [Bool.and_eq_true] at hletters + obtain ⟨⟨⟨l1, l2⟩, l3⟩, l4⟩ := hletters + refine ⟨⟨l1, l2, l3, l4, ?_⟩, ?_⟩ + · show (rest2.take len).length < 2147483648 + rw [hl] + exact Nat.lt_of_not_le hlen + rw [← hbs] + show be32 (rest2.take len).length ++ [t1, t2, t3, t4] ++ rest2.take len + ++ be32 (Crc32.crc32 ([t1, t2, t3, t4] ++ rest2.take len)).toNat ++ rest3 + = be32 len ++ (t1 :: t2 :: t3 :: t4 :: rest2) + rw [hl, ← hcrc, List.append_assoc, List.append_assoc, List.append_assoc, + hrest2, List.take_append_drop] + rfl + · cases h + · cases h + · cases h + +/-- A chunk the reader takes as the IEND chunk is the IEND + chunk. -/ +theorem isIEND_eq {c : Chunk} (h : isIEND c = true) : c = iendChunk := by + obtain ⟨t1, t2, t3, t4, data⟩ := c + simp only [isIEND, Chunk.typeBytes, iendType, Bool.and_eq_true, decide_eq_true_eq, + List.cons.injEq, and_true, List.isEmpty_iff] at h + obtain ⟨⟨rfl, rfl, rfl, rfl⟩, rfl⟩ := h + rfl + +/-- A chunk list the list reader accepts, at any fuel, is the + printed form of the list, every chunk in it is well formed, + and it ends in the IEND chunk with no IEND chunk before. -/ +theorem parseChunks_sound : ∀ (n : Nat) (bs : List UInt8) (cs : Doc), + parseChunks n bs = some cs → + cs.flatMap printChunk = bs ∧ (∀ c ∈ cs, WFChunk c) ∧ + ∃ pre : Doc, cs = pre ++ [iendChunk] ∧ ∀ c ∈ pre, isIEND c = false := by + intro n + induction n with + | zero => intro bs cs h; cases h + | succ n ih => + intro bs cs h + rw [parseChunks_succ] at h + split at h + · cases h + rename_i c rest hc + obtain ⟨hwf, hpr⟩ := parseChunk_sound hc + split at h + · rename_i hend + split at h + · rename_i hrest + simp only [Option.some.injEq] at h + subst h hrest + refine ⟨?_, ?_, [], ?_, ?_⟩ + · simpa using hpr + · intro x hx + rw [List.mem_singleton.mp hx] + exact hwf + · rw [isIEND_eq hend] + rfl + · intro x hx + cases hx + · cases h + · rename_i hnend + split at h + · cases h + rename_i cs' hcs + simp only [Option.some.injEq] at h + subst h + obtain ⟨hflat, hall, pre, hpre, hnot⟩ := ih rest cs' hcs + refine ⟨?_, ?_, c :: pre, ?_, ?_⟩ + · rw [List.flatMap_cons, hflat] + exact hpr + · intro x hx + rcases List.mem_cons.mp hx with rfl | hx + · exact hwf + · exact hall x hx + · rw [hpre] + rfl + · intro x hx + rcases List.mem_cons.mp hx with rfl | hx + · exact Bool.eq_false_iff.mpr hnend + · exact hnot x hx + +/-- The chunk parser is sound: a file it accepts is the printed + form of the chunk list it returns, and that list is well + formed. -/ +theorem parse_sound {bs : List UInt8} {doc : Doc} (h : parse bs = some doc) : + WF doc ∧ print doc = bs := by + unfold parse at h + split at h + · rename_i hsig + split at h + · rename_i c cs hcs + split at h + · rename_i hhead + simp only [Option.some.injEq] at h + subst h + obtain ⟨hflat, hall, pre, hpre, hnot⟩ := parseChunks_sound _ _ _ hcs + obtain ⟨htype, hlen⟩ := hhead + have hprint : print (c :: cs) = bs := by + show signature ++ (c :: cs).flatMap printChunk = bs + rw [hflat, ← hsig] + exact List.take_append_drop 8 bs + cases pre with + | nil => + have hc : c = iendChunk := (List.cons.inj hpre).1 + rw [hc] at htype + exact absurd htype (by decide) + | cons head mid => + have hpre' : c :: cs = head :: (mid ++ [iendChunk]) := hpre + have hc : c = head := (List.cons.inj hpre').1 + subst hc + exact ⟨⟨c, mid, hpre, htype, hlen, hall, hnot⟩, hprint⟩ + · cases h + · cases h + · cases h + +/-- The chunk parser, exactly: it accepts the file `bs` with the + chunk list `doc` if and only if `doc` is well formed and `bs` + is its printed form. -/ +theorem parse_iff (bs : List UInt8) (doc : Doc) : + parse bs = some doc ↔ WF doc ∧ print doc = bs := + ⟨parse_sound, fun ⟨hwf, hp⟩ => hp ▸ parse_print hwf⟩ + +/-- The file level read is sound: a file it accepts, with header + `hd` and chunk list `doc`, is the printed form of `doc`, and + `doc` is fully well formed with header `hd`. So the header it + returns is the one the first chunk's data is the printed form + of, and no later chunk is an IHDR chunk. -/ +theorem parseFile_sound {bs : List UInt8} {hd : Ihdr} {doc : Doc} + (h : parseFile bs = some (hd, doc)) : WFFull hd doc ∧ print doc = bs := by + unfold parseFile at h + split at h + · rename_i d hd' + cases hh : headerOf d with + | none => + rw [hh] at h + cases h + | some x => + rw [hh] at h + simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨hx, rfl⟩ := h + rw [hx] at hh + obtain ⟨hwf, hpr⟩ := parse_sound hd' + obtain ⟨head, mid, hdoc, htype, -, hall, hnot⟩ := hwf + rw [hdoc] at hh + have hh' : (if (mid ++ [iendChunk]).any isIHDR then none + else parseIhdr head.data) = some hd := hh + split at hh' + · cases hh' + rename_i hany + obtain ⟨hwfh, hprint⟩ := parseIhdr_sound hh' + refine ⟨⟨head, mid, hdoc, htype, hprint.symm, hwfh, hall, hnot, ?_⟩, hpr⟩ + intro c hc hct + apply hany + rw [List.any_eq_true] + exact ⟨c, List.mem_append_left _ hc, by simp [isIHDR, hct]⟩ + · cases h + +/-- The file level read, exactly: it accepts the file `bs` with + header `hd` and chunk list `doc` if and only if `doc` is fully + well formed with header `hd` and `bs` is its printed form. -/ +theorem parseFile_iff (bs : List UInt8) (hd : Ihdr) (doc : Doc) : + parseFile bs = some (hd, doc) ↔ WFFull hd doc ∧ print doc = bs := + ⟨parseFile_sound, fun ⟨hwf, hp⟩ => hp ▸ parseFile_print hwf⟩ + +end Png.Proofs diff --git a/Png/Proofs/SpecProofs.lean b/Png/Proofs/SpecProofs.lean new file mode 100644 index 0000000..c0cf9de --- /dev/null +++ b/Png/Proofs/SpecProofs.lean @@ -0,0 +1,217 @@ +/- + Proofs of the statements in `Png/Spec.lean`, under the same names. + + The round trips, the table, the soundness statements, and the + byte layout are the theorems proved in `Png/Proofs/RoundTrip.lean`, + `Png/Proofs/Header.lean`, `Png/Proofs/Sound.lean`, and + `Png/Proofs/Layout.lean`. The accepted and refused inputs are + single inputs, checked in the kernel with `decide +kernel`: + no native evaluation, which the bar forbids. +-/ + +import Png +import Png.Spec.Defs +import Png.Proofs.RoundTrip +import Png.Proofs.Header +import Png.Proofs.Sound +import Png.Proofs.Layout + +open Png Png.Spec + +theorem Png.Spec.parse_print {doc : Doc} (h : WF doc) : + parse (print doc) = some doc := + Png.Proofs.parse_print h + +theorem Png.Spec.parseIhdr_print (h : Ihdr) (hwf : WFHeader h) : + parseIhdr (printIhdr h) = some h := + Png.Proofs.parseIhdr_print h hwf + +theorem Png.Spec.checkPair_iff (ct bd : UInt8) : + checkPair ct bd = true ↔ + (ct.toNat, bd.toNat) ∈ allowedPairs := + Png.Proofs.checkPair_iff ct bd + +theorem Png.Spec.parseFile_print {hd : Ihdr} {doc : Doc} (h : WFFull hd doc) : + parseFile (print doc) = some (hd, doc) := + Png.Proofs.parseFile_print h + + +theorem Png.Spec.parse_sound {bs : List UInt8} {doc : Doc} + (h : parse bs = some doc) : WF doc ∧ print doc = bs := + Png.Proofs.parse_sound h + +theorem Png.Spec.parseIhdr_sound {bs : List UInt8} {h : Ihdr} + (hp : parseIhdr bs = some h) : WFHeader h ∧ printIhdr h = bs := + Png.Proofs.parseIhdr_sound hp + +theorem Png.Spec.parseFile_sound {bs : List UInt8} {hd : Ihdr} {doc : Doc} + (h : parseFile bs = some (hd, doc)) : + WFFull hd doc ∧ print doc = bs := + Png.Proofs.parseFile_sound h + + +theorem Png.Spec.print_layout (doc : Doc) : + print doc = [137, 80, 78, 71, 13, 10, 26, 10] ++ + doc.flatMap (fun c => + bigEndian4 c.data.length ++ [c.t1, c.t2, c.t3, c.t4] ++ c.data ++ + bigEndian4 (Crc32.crc32 ([c.t1, c.t2, c.t3, c.t4] ++ c.data)).toNat) := + Png.Proofs.print_layout doc + +theorem Png.Spec.printIhdr_layout (h : Ihdr) : + printIhdr h = bigEndian4 h.width ++ bigEndian4 h.height ++ + [h.bitDepth, h.colorType, 0, 0, h.interlace] := + Png.Proofs.printIhdr_layout h + +theorem Png.Spec.isLetter_iff (b : UInt8) : + isLetter b = true ↔ + (65 ≤ b.toNat ∧ b.toNat ≤ 90) ∨ (97 ≤ b.toNat ∧ b.toNat ≤ 122) := + Png.Proofs.isLetter_iff b + +theorem Png.Spec.ihdrType_eq : ihdrType = [73, 72, 68, 82] := rfl + +theorem Png.Spec.typeBytes_eq (c : Chunk) : + c.typeBytes = [c.t1, c.t2, c.t3, c.t4] := rfl + +theorem Png.Spec.isIEND_iff (c : Chunk) : + isIEND c = true ↔ [c.t1, c.t2, c.t3, c.t4] = [73, 69, 78, 68] ∧ c.data = [] := + Png.Proofs.isIEND_iff c + + +theorem Png.Spec.reads_real_file_header : + (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, 0, 180, 244, + 174, 198, 0, 0, 0, 62, 73, 68, 65, 84, 120, 156, 1, 51, 0, 204, + 255, 0, 248, 207, 45, 4, 205, 181, 169, 174, 98, 138, 255, 174, + 190, 27, 111, 191, 0, 254, 105, 254, 66, 198, 209, 157, 111, + 200, 221, 165, 145, 35, 173, 191, 75, 0, 216, 164, 157, 244, + 188, 239, 173, 101, 28, 78, 104, 79, 114, 243, 122, 31, 237, + 218, 28, 90, 62, 15, 23, 102, 0, 0, 0, 0, 73, 69, 78, 68, 174, + 66, 96, 130] : List UInt8)).map Prod.fst = + some { width := 4, height := 3, bitDepth := 8, colorType := 6, interlace := 0 } := by + decide +kernel + + +theorem Png.Spec.reads_header_1920x1080 : + parseIhdr ([0, 0, 7, 128, 0, 0, 4, 56, 8, 2, 0, 0, 0] + : List UInt8) = + some { width := 1920, height := 1080, bitDepth := 8, colorType := 2, interlace := 0 } := by + decide +kernel + + +theorem Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.Spec.rejects_second_ihdr : + (parseFile ([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, 13, 73, 72, 68, 82, 0, 0, 0, 2, 0, 0, 0, 2, + 8, 2, 0, 0, 0, 253, 212, 154, 115, 0, 0, 0, 12, 73, 68, 65, 84, + 120, 156, 99, 96, 96, 96, 0, 0, 0, 4, 0, 1, 246, 23, 56, 85, 0, + 0, 0, 0, 73, 69, 78, 68, 174, 66, 96, 130] + : List UInt8)).isSome = false := by + decide +kernel + + +theorem Png.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/Png/Proofs/Verify.lean b/Png/Proofs/Verify.lean index 9b45f93..6ddd768 100644 --- a/Png/Proofs/Verify.lean +++ b/Png/Proofs/Verify.lean @@ -1,11 +1,59 @@ /- - Axiom check for the headline theorem. Building this file prints - the axioms the proof depends on. The expected output is only the - three standard Lean axioms: `propext`, `Classical.choice`, + Axiom check. Building this file prints the axioms each proof + depends on: the headline theorems in `Png.Proofs`, then every + theorem `comparator.json` names, as proved in + `Png/Proofs/SpecProofs.lean`. The expected output is only the three + standard Lean axioms: `propext`, `Classical.choice`, `Quot.sound`, or a subset of them. Any other name here breaks - the verified bar. + the verified bar. `tests/run_tests.py` reads this output and + fails on any other name, or on a theorem with no line. -/ import Png.Proofs.RoundTrip +import Png.Proofs.Header +import Png.Proofs.Sound +import Png.Proofs.Layout +import Png.Proofs.SpecProofs #print axioms Png.Proofs.parse_print +#print axioms Png.Proofs.parseIhdr_print +#print axioms Png.Proofs.checkPair_iff +#print axioms Png.Proofs.parseFile_print +#print axioms Png.Proofs.parse_sound +#print axioms Png.Proofs.parseIhdr_sound +#print axioms Png.Proofs.parseFile_sound +#print axioms Png.Proofs.print_layout +#print axioms Png.Proofs.printIhdr_layout +#print axioms Png.Proofs.isLetter_iff +#print axioms Png.Proofs.isIEND_iff + +#print axioms Png.Spec.parse_print +#print axioms Png.Spec.parseIhdr_print +#print axioms Png.Spec.checkPair_iff +#print axioms Png.Spec.parseFile_print +#print axioms Png.Spec.parse_sound +#print axioms Png.Spec.parseIhdr_sound +#print axioms Png.Spec.parseFile_sound +#print axioms Png.Spec.print_layout +#print axioms Png.Spec.printIhdr_layout +#print axioms Png.Spec.isLetter_iff +#print axioms Png.Spec.ihdrType_eq +#print axioms Png.Spec.typeBytes_eq +#print axioms Png.Spec.isIEND_iff +#print axioms Png.Spec.reads_real_file_header +#print axioms Png.Spec.reads_header_1920x1080 +#print axioms Png.Spec.rejects_bad_signature +#print axioms Png.Spec.rejects_bad_crc +#print axioms Png.Spec.rejects_truncated_input +#print axioms Png.Spec.rejects_first_chunk_length_12 +#print axioms Png.Spec.rejects_zero_width +#print axioms Png.Spec.rejects_zero_height +#print axioms Png.Spec.rejects_width_at_cap +#print axioms Png.Spec.rejects_height_at_cap +#print axioms Png.Spec.rejects_illegal_depth +#print axioms Png.Spec.rejects_unknown_colour_type +#print axioms Png.Spec.rejects_unknown_interlace +#print axioms Png.Spec.rejects_nonzero_compression +#print axioms Png.Spec.rejects_nonzero_filter +#print axioms Png.Spec.rejects_second_ihdr +#print axioms Png.Spec.rejects_header_wrong_length diff --git a/Png/Spec.lean b/Png/Spec.lean new file mode 100644 index 0000000..dceadaf --- /dev/null +++ b/Png/Spec.lean @@ -0,0 +1,321 @@ +/- + 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 + `Png.Proofs` (`Png/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 the definitions in `Png/Value.lean`, + `Png/Parse.lean`, `Png/Crc32.lean`, and `Png/Header.lean`, the + code under proof named in `bar.toml`, and the well formedness + predicates, the written out table of allowed pairs, and four + bytes big endian (`Png.Spec.WF`, `Png.Spec.WFHeader`, + `Png.Spec.WFFull`, `Png.Spec.allowedPairs`, + `Png.Spec.bigEndian4`, and what they use), which are in + `Png/Spec/Defs.lean`. That file is part of the specification + too. +-/ + +import Png +import Png.Spec.Defs + +open Png Png.Spec + +/-! ## 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 `Png/Proofs/RoundTrip.lean` +or `Png/Proofs/Header.lean`, over the same well formedness +predicates, `Png.Spec.WF`, `Png.Spec.WFHeader`, and `Png.Spec.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 Png.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 Png.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 Png.Spec.checkPair_iff (ct bd : UInt8) : + checkPair ct bd = true ↔ + (ct.toNat, bd.toNat) ∈ allowedPairs := sorry + +/-- Printing a fully well formed document with header `hd` and + reading it back at both layers gives back that header, `hd` + itself, and the document. This holds relative to the printer: + the first chunk's data is `printIhdr hd`. So a reader that + returned some other header than the one `printIhdr` wrote, a + fixed one or one with the width and height swapped, fails + this statement. A change that swapped them in both the + printer and the reader would still meet it; that change fails + `Png.Spec.printIhdr_layout`, which fixes the bytes the printer + writes, and the accepted inputs below. -/ +theorem Png.Spec.parseFile_print {hd : Ihdr} {doc : Doc} (h : WFFull hd doc) : + parseFile (print doc) = some (hd, doc) := sorry + +/-! ## What the readers accept + +The converse of the round trips: each reader accepts only the +printed form of a well formed value, and returns that value. +With the round trips above, this pins each reader exactly, so +every rule the well formedness predicates state is a rule the +reader keeps when it refuses a file. -/ + +/-- A file the chunk parser accepts is the printed form of the + chunk list it returns, and that list is well formed. -/ +theorem Png.Spec.parse_sound {bs : List UInt8} {doc : Doc} + (h : parse bs = some doc) : WF doc ∧ print doc = bs := sorry + +/-- A header the header reader accepts is well formed, and the + bytes it read are that header's printed form. So a width or + height of zero or of 2^31 or more, a nonzero compression or + filter byte, an interlace byte above 1, a depth the colour + type does not allow, and any length but 13 are all refused. -/ +theorem Png.Spec.parseIhdr_sound {bs : List UInt8} {h : Ihdr} + (hp : parseIhdr bs = some h) : WFHeader h ∧ printIhdr h = bs := sorry + +/-- A file the file level read accepts, with header `hd` and + chunk list `doc`, is the printed form of `doc`, and `doc` is + fully well formed with header `hd`: its first chunk's data is + the printed form of `hd`, and no later chunk is an IHDR + chunk. -/ +theorem Png.Spec.parseFile_sound {bs : List UInt8} {hd : Ihdr} {doc : Doc} + (h : parseFile bs = some (hd, doc)) : + WFFull hd doc ∧ print doc = bs := sorry + +/-! ## The byte layout + +The round trips and their converses tie each reader to its +printer, but say nothing of the bytes the printer writes: a +printer and a reader that both put the height before the width, +or both wrote lengths least significant byte first, would meet +them. The statements here fix those bytes: the chunk layout, the +13 bytes of the header, the letters a chunk type may use, the +type bytes the rules compare, and the type bytes of IHDR and +IEND. With the round trips and the +converses above, they fix what each reader accepts and returns +for every input: the chunk parser accepts exactly the bytes +`Png.Spec.print_layout` gives for a well formed chunk list, and the +header reader accepts exactly the bytes `Png.Spec.printIhdr_layout` +gives for a well formed header, and returns that header. The one +function they leave as the code has it is the CRC-32. -/ + +/-- The bytes `print` writes for a chunk list: the eight + signature bytes, then each chunk in order as its data length + in four bytes big endian, its four type bytes, its data, and + the CRC-32 of its type bytes and data in four bytes big + endian. This is the chunk layout of the PNG specification. + The CRC-32 is the function in `Png/Crc32.lean`. -/ +theorem Png.Spec.print_layout (doc : Doc) : + print doc = [137, 80, 78, 71, 13, 10, 26, 10] ++ + doc.flatMap (fun c => + bigEndian4 c.data.length ++ [c.t1, c.t2, c.t3, c.t4] ++ c.data ++ + bigEndian4 (Crc32.crc32 ([c.t1, c.t2, c.t3, c.t4] ++ c.data)).toNat) := sorry + +/-- The 13 bytes `printIhdr` writes for a header, in order: the + width in four bytes big endian, the height in four bytes big + endian, the bit depth, the colour type, a compression byte of + zero, a filter byte of zero, and the interlace byte. This is + the IHDR layout of the PNG specification. With + `Png.Spec.parseIhdr_sound`, the width the header reader returns + is the value of the first four bytes it read, and the height + the value of the next four. -/ +theorem Png.Spec.printIhdr_layout (h : Ihdr) : + printIhdr h = bigEndian4 h.width ++ bigEndian4 h.height ++ + [h.bitDepth, h.colorType, 0, 0, h.interlace] := sorry + +/-- The letter test the chunk rules use (`Png.Spec.WFChunk`, and the + parser) holds of the ASCII letters, A to Z (65 to 90) and a + to z (97 to 122), and of no other byte. -/ +theorem Png.Spec.isLetter_iff (b : UInt8) : + isLetter b = true ↔ + (65 ≤ b.toNat ∧ b.toNat ≤ 90) ∨ (97 ≤ b.toNat ∧ b.toNat ≤ 122) := sorry + +/-- The type bytes the chunk rules require of the first chunk + are I, H, D, R, in ASCII. -/ +theorem Png.Spec.ihdrType_eq : ihdrType = [73, 72, 68, 82] := sorry + +/-- The type bytes the chunk rules compare with `ihdrType` + (`Png.Spec.WF`, `Png.Spec.WFFull`, and the readers) are a chunk's four + type bytes, in the order the chunk printer writes them. -/ +theorem Png.Spec.typeBytes_eq (c : Chunk) : + c.typeBytes = [c.t1, c.t2, c.t3, c.t4] := sorry + +/-- The IEND chunk, at which reading stops and which ends a well + formed chunk list, is a chunk with type bytes I, E, N, D, in + ASCII, and no data. -/ +theorem Png.Spec.isIEND_iff (c : Chunk) : + isIEND c = true ↔ [c.t1, c.t2, c.t3, c.t4] = [73, 69, 78, 68] ∧ c.data = [] := sorry + +/-! ## Accepted inputs + +Two inputs the readers accept, with the header each returns. The +width and the height differ in both, so a reader that swapped +them fails each statement. The test harness reads both inputs +from this file and checks the header each statement gives +against its own reading of the bytes, against the tool's `header` +answer, and, where libpng is installed, against libpng's. -/ + +/-- A real PNG file is read with its own header: 4 by 3, bit + depth 8, colour type 6 (truecolour with alpha), no interlace. + The file has an IHDR chunk, an IDAT chunk holding the + zlib compressed scanlines of random pixels, and IEND. It is + the 4 by 3 file among the test suite's real files. The test + harness checks that zlib inflates its IDAT data to three + scanlines of that width, and has libpng decode it in full. -/ +theorem Png.Spec.reads_real_file_header : + (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, 0, 180, 244, + 174, 198, 0, 0, 0, 62, 73, 68, 65, 84, 120, 156, 1, 51, 0, 204, + 255, 0, 248, 207, 45, 4, 205, 181, 169, 174, 98, 138, 255, 174, + 190, 27, 111, 191, 0, 254, 105, 254, 66, 198, 209, 157, 111, + 200, 221, 165, 145, 35, 173, 191, 75, 0, 216, 164, 157, 244, + 188, 239, 173, 101, 28, 78, 104, 79, 114, 243, 122, 31, 237, + 218, 28, 90, 62, 15, 23, 102, 0, 0, 0, 0, 73, 69, 78, 68, 174, + 66, 96, 130] : List UInt8)).map Prod.fst = + some { width := 4, height := 3, bitDepth := 8, colorType := 6, interlace := 0 } := sorry + +/-- The header reader reads the 13 bytes of a 1920 by 1080 + header, bit depth 8, colour type 2 (truecolour), no + interlace, as width 1920 (the first four bytes, 0, 0, 7, 128) + and height 1080 (the next four, 0, 0, 4, 56). -/ +theorem Png.Spec.reads_header_1920x1080 : + parseIhdr ([0, 0, 7, 128, 0, 0, 4, 56, 8, 2, 0, 0, 0] + : List UInt8) = + some { width := 1920, height := 1080, bitDepth := 8, colorType := 2, interlace := 0 } := 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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 Png.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 + +/-- A file with a second IHDR chunk is refused by the file level + read: here a 1 by 1 IHDR, then a 2 by 2 IHDR, then IDAT and + IEND. The PNG specification allows one IHDR chunk. -/ +theorem Png.Spec.rejects_second_ihdr : + (parseFile ([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, 13, 73, 72, 68, 82, 0, 0, 0, 2, 0, 0, 0, 2, + 8, 2, 0, 0, 0, 253, 212, 154, 115, 0, 0, 0, 12, 73, 68, 65, 84, + 120, 156, 99, 96, 96, 96, 0, 0, 0, 4, 0, 1, 246, 23, 56, 85, 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 Png.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/Png/Spec/Defs.lean b/Png/Spec/Defs.lean new file mode 100644 index 0000000..d392ca0 --- /dev/null +++ b/Png/Spec/Defs.lean @@ -0,0 +1,92 @@ +/- + The definitions the statements in `Png/Spec.lean` use besides the + code under proof: four bytes big endian (`bigEndian4`), the + IEND chunk as a value, well formedness at + the chunk layer (`WFChunk`, `WF`), the written out table of + allowed (colour type, bit depth) pairs, well formedness of a + header (`WFHeader`), and full well formedness of a document + with its header (`WFFull`). They give the statements their + meaning, and the readers and printers do not use them, so they + are part of the specification, with `Png/Spec.lean` and `SPEC.md`, + not of the code (`bar.toml` lists the code). A change here + changes the spec hash, and so voids an approval. +-/ + +import Png + +namespace Png.Spec + +open Png + +/-- A number as four bytes, most significant first (big endian): + its base 256 digits, from the 2^24 place down to the units. + The PNG specification writes every four byte number this way: + chunk lengths, CRCs, and the width and height in IHDR. A + number of 2^32 or more keeps only its lowest four digits; + the numbers PNG writes are below 2^31. -/ +def bigEndian4 (n : Nat) : List UInt8 := + [UInt8.ofNat (n / 16777216 % 256), UInt8.ofNat (n / 65536 % 256), + UInt8.ofNat (n / 256 % 256), UInt8.ofNat (n % 256)] + +/-- The IEND chunk itself: type bytes I, E, N, D, in ASCII, and + no data. The fields are named, so the value does not depend + on the order in which `Png.Chunk` declares them. -/ +def iendChunk : Chunk := { t1 := 73, t2 := 69, t3 := 78, t4 := 68, data := [] } + +/-- The per-chunk part of well formedness: each type byte is an + ASCII letter, and the data length stays below 2^31, as the PNG + specification bounds chunk lengths. -/ +def WFChunk (c : Chunk) : Prop := + isLetter c.t1 = true ∧ isLetter c.t2 = true ∧ + isLetter c.t3 = true ∧ isLetter c.t4 = true ∧ + c.data.length < 2147483648 + +/-- A document 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; and every chunk is a well formed chunk. -/ +def WF (doc : Doc) : Prop := + ∃ (head : Chunk) (mid : List Chunk), + doc = head :: mid ++ [iendChunk] ∧ + head.typeBytes = ihdrType ∧ head.data.length = 13 ∧ + (∀ c ∈ doc, WFChunk c) ∧ + (∀ c ∈ head :: mid, isIEND c = false) + +/-- The allowed (colour type, bit depth) pairs, written out in + full, as the PNG specification's table gives them. The + checker in `Png/Header.lean` is built from a per-type table; + `Png.Spec.checkPair_iff` says 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)] + +/-- A header is well formed when the width and the height are + above zero and below 2^31, the interlace byte is 0 or 1, and + the (colour type, bit depth) pair is in the table above. -/ +def WFHeader (h : Ihdr) : Prop := + 0 < h.width ∧ h.width < 2147483648 ∧ + 0 < h.height ∧ h.height < 2147483648 ∧ + (h.interlace = 0 ∨ h.interlace = 1) ∧ + (h.colorType.toNat, h.bitDepth.toNat) ∈ allowedPairs + +/-- A document is fully well formed, with header `hd`, when it + is well formed at the chunk layer (as in `WF`), its first + chunk's data is the printed form of `hd`, `hd` is well + formed, and no chunk after the first has type IHDR. The + header is a parameter, not a witness, so a statement over + `WFFull hd doc` can say which header a reader must return. + Stated in the shape of `WF`. -/ +def WFFull (hd : Ihdr) (doc : Doc) : Prop := + ∃ (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) ∧ + (∀ c ∈ mid, c.typeBytes ≠ ihdrType) + +end Png.Spec diff --git a/Png/Value.lean b/Png/Value.lean index 6870cce..6743357 100644 --- a/Png/Value.lean +++ b/Png/Value.lean @@ -14,6 +14,10 @@ length, type, data, and a CRC it computes as it goes. Its output is the canonical form the tests compare against: a file this parser accepts is reprinted byte for byte. + + Well formedness, the rule the round trip is stated over, is not + here: it gives the statements their meaning and no code uses it, + so it is part of the specification, in `Png/Spec/Defs.lean`. -/ import Png.Crc32 @@ -48,9 +52,6 @@ def ihdrType : List UInt8 := [73, 72, 68, 82] /-- The type bytes of the last chunk of every PNG file. -/ def iendType : List UInt8 := [73, 69, 78, 68] -/-- The IEND chunk itself: type IEND, no data. -/ -def iendChunk : Chunk := ⟨73, 69, 78, 68, []⟩ - /-- Is this chunk the IEND chunk: type IEND and no data? A chunk of type IEND that carries data is an ordinary chunk here. -/ def isIEND (c : Chunk) : Bool := @@ -80,23 +81,4 @@ def printChunk (c : Chunk) : List UInt8 := def print (doc : Doc) : List UInt8 := signature ++ doc.flatMap printChunk -/-- The per-chunk part of well formedness: each type byte is an - ASCII letter, and the data length stays below 2^31, as the PNG - specification bounds chunk lengths. -/ -def WFChunk (c : Chunk) : Prop := - isLetter c.t1 = true ∧ isLetter c.t2 = true ∧ - isLetter c.t3 = true ∧ isLetter c.t4 = true ∧ - c.data.length < 2147483648 - -/-- A document 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; and every chunk is a well formed chunk. -/ -def WF (doc : Doc) : Prop := - ∃ (head : Chunk) (mid : List Chunk), - doc = head :: mid ++ [iendChunk] ∧ - head.typeBytes = ihdrType ∧ head.data.length = 13 ∧ - (∀ c ∈ doc, WFChunk c) ∧ - (∀ c ∈ head :: mid, isIEND c = false) - end Png diff --git a/README.md b/README.md index ff496a1..5753aee 100644 --- a/README.md +++ b/README.md @@ -1,59 +1,243 @@ -# 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. No reviewer has approved the specification yet. + +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 `Png/Spec.lean`, over +the definitions in `Png/Spec/Defs.lean`, with their proofs in +`Png/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. 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. +``` +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 (`Png/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, checks the two accepted inputs stated in +`Png/Spec.lean`, compares the header read with libpng where a C +compiler and libpng are installed (`tests/libpng_header.c`), +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), and `Png/Crc32.lean` (the CRC-32). The proofs are in `Png/Proofs/RoundTrip.lean`. +Each claim below names the theorem behind it. The theorems +are stated in `Png/Spec.lean` (the challenge file, where they end +in `sorry`) and proved in `Png/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` | - -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`. - -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. | `Png.Spec.parse_print` | +| Reading the printed bytes of a well formed IHDR header gives the header back. | `Png.Spec.parseIhdr_print` | +| The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair. | `Png.Spec.checkPair_iff` | +| Printing a fully well formed document whose first chunk holds the printed header `hd`, and reading it back at both layers, gives back `hd` itself and the document. | `Png.Spec.parseFile_print` | +| A file the chunk parser accepts is the printed form of the chunk list it returns, and that list is well formed. | `Png.Spec.parse_sound` | +| A header the header reader accepts is well formed, and the bytes it read are its printed form. So a header that breaks any header rule is refused. | `Png.Spec.parseIhdr_sound` | +| A file the file level read accepts is the printed form of the chunk list it returns, and that list is fully well formed with the header the read returns. So a file that breaks any rule of either layer, or holds a second IHDR chunk, is refused. | `Png.Spec.parseFile_sound` | +| The chunk printer writes the eight signature bytes, then each chunk as its data length in four bytes big endian, its four type bytes, its data, and the CRC-32 of its type bytes and data in four bytes big endian. | `Png.Spec.print_layout` | +| The header printer writes the width in four bytes big endian, then the height in four bytes big endian, then the bit depth, the colour type, a compression byte of zero, a filter byte of zero, and the interlace byte. | `Png.Spec.printIhdr_layout` | +| The letter test the chunk rules use holds of the ASCII letters A to Z and a to z, and of no other byte. | `Png.Spec.isLetter_iff` | +| The type bytes required of the first chunk are I, H, D, R. | `Png.Spec.ihdrType_eq` | +| The type bytes the chunk rules compare are a chunk's four type bytes, in the order the printer writes them. | `Png.Spec.typeBytes_eq` | +| The IEND chunk, where reading stops, is a chunk with type bytes I, E, N, D and no data. | `Png.Spec.isIEND_iff` | +| A real 4 by 3 PNG file (an IHDR, an IDAT with zlib compressed pixels, and IEND) is read with its own header: width 4, height 3, bit depth 8, colour type 6, no interlace. | `Png.Spec.reads_real_file_header` | +| The 13 bytes of a 1920 by 1080 header are read as width 1920 and height 1080, bit depth 8, colour type 2, no interlace. | `Png.Spec.reads_header_1920x1080` | +| A file whose first signature byte is wrong is refused. | `Png.Spec.rejects_bad_signature` | +| A file whose IHDR chunk carries a CRC that does not match its type and data is refused. | `Png.Spec.rejects_bad_crc` | +| A file cut short inside its first chunk is refused. | `Png.Spec.rejects_truncated_input` | +| A file whose first chunk holds 12 data bytes is refused: an IHDR chunk holds 13. | `Png.Spec.rejects_first_chunk_length_12` | +| A file with a width of zero is refused. | `Png.Spec.rejects_zero_width` | +| A file with a height of zero is refused. | `Png.Spec.rejects_zero_height` | +| A file with a width of 2^31 is refused: the width stays below 2^31. | `Png.Spec.rejects_width_at_cap` | +| A file with a height of 2^31 is refused: the height stays below 2^31. | `Png.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. | `Png.Spec.rejects_illegal_depth` | +| A file with colour type 1 is refused: 1 is not a PNG colour type, and allows no bit depth. | `Png.Spec.rejects_unknown_colour_type` | +| A file with an interlace byte of 2 is refused: the byte is 0 or 1. | `Png.Spec.rejects_unknown_interlace` | +| A file with a compression byte of 1 is refused: the only compression method is 0. | `Png.Spec.rejects_nonzero_compression` | +| A file with a filter byte of 1 is refused: the only filter method is 0. | `Png.Spec.rejects_nonzero_filter` | +| A file with a second IHDR chunk is refused by the file level read: the PNG specification allows one IHDR chunk. | `Png.Spec.rejects_second_ihdr` | +| The header reader refuses anything but exactly 13 bytes: here a valid header's first 12 bytes. | `Png.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 with header `hd` +(`WFFull hd doc`) when it is well formed at the chunk layer, +its first chunk's data is the printed form of `hd`, a well +formed header, and no chunk after the first has type IHDR. +The header is a parameter of the predicate, so +the file level round trip names the header the read must +return. That holds relative to the printer: the read must +return the header whose `printIhdr` bytes the first chunk +holds. So a reader that answered a fixed header, or swapped the +width and the height while the printer did not, would not meet +it. A change that swapped them in both the printer and the +reader would still meet the round trips. What stops it is +`Png.Spec.printIhdr_layout`, which fixes the bytes the printer +writes (the width first, then the height, each four bytes big +endian), and the two accepted inputs, +`Png.Spec.reads_real_file_header` and +`Png.Spec.reads_header_1920x1080`, whose widths and heights +differ. + +Each reader is pinned to its rule in both directions. The +round trip says it accepts the printed form of every well +formed value and returns that value; the soundness theorem +says it accepts nothing else. So the chunk parser accepts a +file exactly when the file is `print doc` for a well formed +`doc`, and then returns `doc` (`Png.Spec.parse_print` with +`Png.Spec.parse_sound`); the header reader accepts 13 bytes +exactly when they are `printIhdr h` for a well formed `h` +(`Png.Spec.parseIhdr_print` with `Png.Spec.parseIhdr_sound`); +and the file level read accepts a file exactly when it is +`print doc` for a `doc` fully well formed with header `hd`, and +then returns `hd` and `doc` (`Png.Spec.parseFile_print` with +`Png.Spec.parseFile_sound`). Every rule in these predicates is +therefore a proved rejection rule. The named refusal theorems +in the table are worked examples of those rules, one input +each. + +The round trips and the soundness theorems are stated in terms +of the printers. The layout theorems fix what the printers +write: `Png.Spec.print_layout` the chunk layout, and +`Png.Spec.printIhdr_layout` the 13 header bytes. +`Png.Spec.isLetter_iff`, `Png.Spec.ihdrType_eq`, +`Png.Spec.typeBytes_eq`, and `Png.Spec.isIEND_iff` fix the +letters and type bytes the rules name. Together with the +round trips and the soundness theorems, they fix which bytes each +reader accepts and what it returns, for every input. The one +function they leave as the code has it is the CRC-32 (see +below). + +The headline theorems rest on the proofs in +`Png/Proofs/RoundTrip.lean`, `Png/Proofs/Header.lean`, +`Png/Proofs/Sound.lean`, and `Png/Proofs/Layout.lean`, where +they are `Png.Proofs.parse_print`, `Png.Proofs.parseIhdr_print`, +`Png.Proofs.checkPair_iff`, `Png.Proofs.parseFile_print`, +`Png.Proofs.parse_sound`, `Png.Proofs.parseIhdr_sound`, +`Png.Proofs.parseFile_sound`, `Png.Proofs.print_layout`, +`Png.Proofs.printIhdr_layout`, `Png.Proofs.isLetter_iff`, and +`Png.Proofs.isIEND_iff`. Each checks against at most two of the +standard axioms (`propext`, `Quot.sound`), which a reader can +confirm with `#print axioms`, or by running `lake env lean +Png/Proofs/Verify.lean`; the test harness reads that output for +every theorem `comparator.json` names, and records it. +The refusal theorems and the two accepted inputs are single +inputs checked in the kernel with `decide +kernel`, and +`Png.Spec.ihdrType_eq` and `Png.Spec.typeBytes_eq` hold by +definition. The test harness reads the two accepted inputs from +`Png/Spec.lean` and checks the header each states against its +own big endian reading of the bytes, the tool's `header` answer, +and libpng's. + +The code is in `Png/Value.lean` (the chunk type and the +printer), `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 well +formedness rules (`Png.Spec.WFChunk`, `Png.Spec.WF`, +`Png.Spec.WFHeader`, `Png.Spec.WFFull`), the written out table +of allowed pairs (`Png.Spec.allowedPairs`), and four bytes big +endian (`Png.Spec.bigEndian4`) give the statements their +meaning and no code uses them, so they are part of the +specification, in `Png/Spec/Defs.lean`, and a change to them +voids an approval. 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 -- 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. -- 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. +- That the well formedness rules (`WF`, `WFHeader`, `WFFull`, and the table of allowed pairs) and the byte layout the layout theorems state (`Png.Spec.print_layout`, `Png.Spec.printIhdr_layout`, with `Png.Spec.bigEndian4`) are the PNG specification's. The proofs tie each reader to its rule and each printer to the stated layout exactly, but that the rule and the layout say what the PNG specification says is a reading: `SPEC.md` states it in words, and the tests compare the readers against a strict oracle written in the harness from those rules, and the header read against libpng, file by file, the two accepted inputs of `Png/Spec.lean` among them. Where libpng and this reader differ, the test record names each difference and the rule behind it. +- That the CRC-32 here is the standard one. `Png.Spec.print_layout` states the chunk layout with the code's own CRC-32 function (`Png.Crc32.crc32`), and no theorem says that function is the standard CRC-32. 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. Two statements pin it on single inputs: `Png.Spec.reads_real_file_header` holds only if the function gives the three CRCs that zlib wrote into that file, and `Png.Spec.rejects_bad_crc` holds only if it does not give the wrong CRC that its file carries. +- 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, except for IHDR. Which types may appear, how many times, and in what order between IHDR and IEND is not checked, with one exception: the file level read (`header`) refuses a second IHDR chunk. The chunk layer (`parse`) does not, and reads it as an ordinary chunk. So an indexed colour file with no PLTE chunk is accepted, where libpng refuses it. +- A chunk of type IEND that carries data. The PNG specification gives IEND no data, but this reader reads such a chunk as an ordinary chunk, at both layers: the file is accepted when an IEND chunk with no data ends it, and refused when none does. libpng refuses such a chunk when it comes before IDAT, and reads a file that ends in one, with a warning. `SPEC.md` states this reading, and the test record names both differences. ## 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`. 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, and libpng as the oracle for the header read + where it is installed. The results file names the versions + used. +- The line handling in `Main.lean` (splitting a request + line, reading decimal codes) and the text of the `header` + answer. The tests drive them, and no proof covers them. +- 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 Main.lean Png.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 + `Png/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, the header sections, the accepted inputs + stated in `Png/Spec.lean`, and the libpng comparison of the + header read, with counts, named differences, 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 Png/Proofs/Verify.lean` prints the + axiom list for the headline theorems and for every theorem + `comparator.json` names. +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 ab1d12b..0ed4576 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. The claims below are stated as Lean theorems in `Png/Spec.lean`, over the well formedness rules, the table of allowed pairs, and four bytes big endian (`Png.Spec.bigEndian4`) in `Png/Spec/Defs.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. @@ -17,29 +17,129 @@ After the signature come chunks until the input ends. One chunk on the wire is: - the data: that many bytes. - a CRC: four bytes, big endian, holding the CRC-32 of the type bytes and the data bytes together. +Four bytes big endian means the base 256 digits of the number, most significant first (`Png.Spec.bigEndian4`). This layout is the one the printer writes, by `Png.Spec.print_layout`, and an ASCII letter is a byte from 65 to 90 or from 97 to 122, by `Png.Spec.isLetter_iff`. + The CRC-32 is the one PNG and ZIP share: the ISO 3309 polynomial, reflected, the register starting at all ones and inverted at the end. The implementation is the one in `Png/Crc32.lean`, shaped like the ZIP reader's in Proven-Commons/zip. ## The checks, in the order the parser makes them 1. The first eight bytes are the signature. 2. For each chunk, from the front: at least four bytes remain for the length; the length is below 2^31; at least four bytes remain for the type; each type byte is an ASCII letter; at least the length plus four bytes remain for the data and the CRC; the stored CRC equals the CRC-32 computed over the type bytes and the data. Any failure rejects the whole file. There is no partial read. -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. +3. Reading stops at a chunk whose type is IEND (the bytes 73, 69, 78, 68) and whose data is empty (`Png.Spec.isIEND_iff`). 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 (the bytes 73, 72, 68, 82, by `Png.Spec.ihdrType_eq`) 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, here and in the file level read below: reading does not stop at it. The PNG specification gives IEND an empty data field, so such a chunk is not the IEND chunk, and this reading follows from that: a file in which an IEND chunk with data is followed, at the end, by an IEND chunk with no data is accepted, and a file whose last chunk is an IEND chunk with data has no end and is rejected. libpng differs on two such files: it refuses an IEND chunk with data that comes before IDAT, as out of place, where this reader reads past it; and it reads a file that ends in an IEND chunk with data, with a warning, where this reader refuses it. The test record names both differences. No other rule about chunk order is checked at this layer: which types may appear, how many times, or in what order past the first and last, is outside it. The file level read of slice 2, below, adds one such rule: a single IHDR chunk. 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. -## Printing +## The IHDR header (slice 2) -The printer writes the signature, then each chunk as its length, its type bytes, its data, and the CRC it computes over the type bytes and the data. A file the parser accepts is reprinted byte for byte: the lengths and CRCs it carried were checked against the bytes, so printing writes the same values back. +The first chunk's 13 data bytes hold, in order: -## The claim +- 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. + +This order is stated as `Png.Spec.printIhdr_layout`, for the bytes the printer writes. With the soundness of the header reader (`Png.Spec.parseIhdr_sound`), the width the reader returns is the value of the first four bytes it read, big endian, and the height the value of the next four. `Png.Spec.reads_header_1920x1080` and `Png.Spec.reads_real_file_header` are worked examples, each with a width and a height that differ. + +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 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: + +| 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 | -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. +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. -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. +Printing a header writes the 13 bytes back: width and height big endian, then bit depth, colour type, compression zero, filter zero, interlace (`Png.Spec.printIhdr_layout`). + +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. + +The file level read also rejects a file in which any chunk after the first has type IHDR. The PNG specification allows one IHDR chunk, and it comes first (PNG third edition, 11.2), so a second one, wherever it stands, is a rejection; the header is never read from it. The chunk layer alone (`parse`) still reads such a file, since it does not count chunks. + +## Printing + +The printer writes the signature, then each chunk as its length, its type bytes, its data, and the CRC it computes over the type bytes and the data (`Png.Spec.print_layout`). A file the parser accepts is reprinted byte for byte: the lengths and CRCs it carried were checked against the bytes, so printing writes the same values back. This is proved: a file the parser accepts is the printed form of the chunk list read from it (`Png.Spec.parse_sound`). + +## The claim -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`. +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^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, whose first chunk's data is the printed form of a well formed header `hd`, and in which no later chunk has type IHDR, prints and reads back whole, and the header the read returns is `hd` itself, not merely some header. + +Each round trip has a proved converse, so each reader is pinned to its rule in both directions: + +- The chunk parser is sound: a file it accepts is the printed form of the chunk list it returns, and that list is well formed. With the round trip of slice 1, `parse` accepts a file exactly when it is the printed form of a well formed chunk list, and then returns that list. +- The header reader is sound: a header it accepts is well formed, and the 13 bytes it read are that header's printed form. So a width or height of zero or of 2^31 or more, a nonzero compression or filter byte, an interlace byte above 1, a depth the colour type does not allow (by the table claim), and any length but 13 are all refused. +- The file level read is sound: a file it accepts is the printed form of the chunk list it returns, that list is well formed at the chunk layer, its first chunk's data is the printed form of the header the read returns, that header is well formed, and no later chunk has type IHDR. + +So every rule of this specification that the well formedness rules state is a proved rejection rule. + +The round trips and their converses are stated in terms of the printers, so on their own they would also hold for a printer and a reader that agreed on some other layout, such as the height before the width. The layout claims close that: + +- The chunk printer writes the layout of the Chunks section above (`Png.Spec.print_layout`). +- The header printer writes the 13 bytes in the order of the IHDR section above (`Png.Spec.printIhdr_layout`). +- The letter test, the IHDR type bytes, the type bytes a chunk is compared by, and the IEND chunk test are the ones the checks above name (`Png.Spec.isLetter_iff`, `Png.Spec.ihdrType_eq`, `Png.Spec.typeBytes_eq`, `Png.Spec.isIEND_iff`). + +With the round trips and their converses, these fix which bytes each reader accepts and what it returns, for every input, up to the CRC-32 function, which the chunk layout names as the code has it. Two accepted inputs are stated as worked examples: a real 4 by 3 file is read as width 4, height 3, bit depth 8, colour type 6, no interlace (`Png.Spec.reads_real_file_header`), and the 13 bytes of a 1920 by 1080 header as width 1920 and height 1080 (`Png.Spec.reads_header_1920x1080`). The test harness reads both from `Png/Spec.lean` and checks them against its own reading of the bytes and against libpng. + +What is not proved is that the rules and the layout are the PNG specification's: that is the reading this document pins. The test suite checks the readers against real PNG files built with Python's zlib and against a strict reading of these rules written in the harness, checks the header read against libpng file by file where libpng is installed, and records the counts, with each difference from libpng named. + +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 is not proved: it rests on the differential tests against Python zlib's `crc32`, and on single inputs, since `Png.Spec.reads_real_file_header` holds only if the function gives the three CRCs zlib wrote into that file. + +## Properties and their theorems + +Each property above names its theorem. The theorems are stated in `Png/Spec.lean` and proved in `Png/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 | `Png.Spec.parse_print` | +| Reading the printed bytes of a well formed IHDR header gives the header back | `Png.Spec.parseIhdr_print` | +| The depth checker agrees with the written out table of allowed (colour type, bit depth) pairs on every byte pair | `Png.Spec.checkPair_iff` | +| Printing a fully well formed document whose first chunk holds the printed header `hd`, and reading it back at both layers, gives back `hd` itself and the document | `Png.Spec.parseFile_print` | +| A file the chunk parser accepts is the printed form of the chunk list it returns, and that list is well formed | `Png.Spec.parse_sound` | +| A header the header reader accepts is well formed, and the bytes it read are its printed form | `Png.Spec.parseIhdr_sound` | +| A file the file level read accepts is the printed form of the chunk list it returns, and that list is fully well formed with the header the read returns | `Png.Spec.parseFile_sound` | +| The chunk printer writes the signature, then each chunk as its length (four bytes big endian), its type bytes, its data, and its CRC-32 (four bytes big endian) | `Png.Spec.print_layout` | +| The header printer writes the width and the height, four bytes big endian each, then the bit depth, the colour type, zero, zero, and the interlace byte | `Png.Spec.printIhdr_layout` | +| The letter test holds of the bytes 65 to 90 and 97 to 122, and of no other | `Png.Spec.isLetter_iff` | +| The IHDR type bytes are 73, 72, 68, 82 | `Png.Spec.ihdrType_eq` | +| The type bytes the rules compare are a chunk's four type bytes, in order | `Png.Spec.typeBytes_eq` | +| The IEND chunk is type bytes 73, 69, 78, 68 with no data | `Png.Spec.isIEND_iff` | +| A real 4 by 3 file is read with header width 4, height 3, bit depth 8, colour type 6, no interlace | `Png.Spec.reads_real_file_header` | +| The 13 bytes of a 1920 by 1080 header are read as width 1920, height 1080 | `Png.Spec.reads_header_1920x1080` | +| A file whose first signature byte is wrong is refused | `Png.Spec.rejects_bad_signature` | +| A file whose IHDR chunk carries a CRC that does not match its type and data is refused | `Png.Spec.rejects_bad_crc` | +| A file cut short inside its first chunk is refused | `Png.Spec.rejects_truncated_input` | +| A file whose first chunk holds 12 data bytes is refused: an IHDR chunk holds 13 | `Png.Spec.rejects_first_chunk_length_12` | +| A file with a width of zero is refused | `Png.Spec.rejects_zero_width` | +| A file with a height of zero is refused | `Png.Spec.rejects_zero_height` | +| A file with a width of 2^31 is refused: the width stays below 2^31 | `Png.Spec.rejects_width_at_cap` | +| A file with a height of 2^31 is refused: the height stays below 2^31 | `Png.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 | `Png.Spec.rejects_illegal_depth` | +| A file with colour type 1 is refused: 1 is not a PNG colour type, and allows no bit depth | `Png.Spec.rejects_unknown_colour_type` | +| A file with an interlace byte of 2 is refused: the byte is 0 or 1 | `Png.Spec.rejects_unknown_interlace` | +| A file with a compression byte of 1 is refused: the only compression method is 0 | `Png.Spec.rejects_nonzero_compression` | +| A file with a filter byte of 1 is refused: the only filter method is 0 | `Png.Spec.rejects_nonzero_filter` | +| A file with a second IHDR chunk is refused by the file level read | `Png.Spec.rejects_second_ihdr` | +| The header reader refuses anything but exactly 13 bytes: here a valid header's first 12 bytes | `Png.Spec.rejects_header_wrong_length` | ## 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/bar.toml b/bar.toml new file mode 100644 index 0000000..15e2ca2 --- /dev/null +++ b/bar.toml @@ -0,0 +1,59 @@ +# 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. zero-aska +# changed it when carrying png#3 forward (the header in WFFull, the +# soundness statements, the single IHDR rule, the byte layout and the +# accepted inputs, and Png/Spec/Defs.lean). +spec_authors = ["abu-aska", "zero-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Png/Spec.lean", "Png/Spec/Defs.lean"] +# The code under proof: the functions the statements are about. Well +# formedness (Png.Spec.WFChunk, Png.Spec.WF, Png.Spec.WFHeader, +# Png.Spec.WFFull), the IEND chunk as a value, the written out table of +# allowed pairs, and four bytes big endian (Png.Spec.bigEndian4) only +# give the statements their meaning, so they are in the spec files +# above, not here. +code = [ + # The data types the statements are about, their constructors, and + # their fields. + "Png.Chunk", "Png.Chunk.mk", "Png.Chunk.t1", "Png.Chunk.t2", + "Png.Chunk.t3", "Png.Chunk.t4", "Png.Chunk.data", "Png.Doc", + "Png.Ihdr", "Png.Ihdr.mk", "Png.Ihdr.width", "Png.Ihdr.height", + "Png.Ihdr.bitDepth", "Png.Ihdr.colorType", "Png.Ihdr.interlace", + # The byte forms and the printer. + "Png.signature", "Png.Chunk.typeBytes", "Png.isLetter", + "Png.ihdrType", "Png.iendType", "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", + # The chunk readers and the parser. + "Png.get4", "Png.parseChunk", "Png.parseChunks", "Png.parse", + # The IHDR header: the depth check, the printer, the reader, and + # the file level read with its single IHDR rule. + "Png.allowedDepths", "Png.pairAllowed", "Png.checkPair", + "Png.printIhdr", "Png.parseIhdr", "Png.isIHDR", "Png.headerOf", + "Png.parseFile", +] + +# 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..6eecbca --- /dev/null +++ b/comparator.json @@ -0,0 +1 @@ +{"challenge_module":"Png.Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Png.Proofs","theorem_names":["Png.Spec.parse_print","Png.Spec.parseIhdr_print","Png.Spec.checkPair_iff","Png.Spec.parseFile_print","Png.Spec.parse_sound","Png.Spec.parseIhdr_sound","Png.Spec.parseFile_sound","Png.Spec.print_layout","Png.Spec.printIhdr_layout","Png.Spec.isLetter_iff","Png.Spec.ihdrType_eq","Png.Spec.typeBytes_eq","Png.Spec.isIEND_iff","Png.Spec.reads_real_file_header","Png.Spec.reads_header_1920x1080","Png.Spec.rejects_bad_signature","Png.Spec.rejects_bad_crc","Png.Spec.rejects_truncated_input","Png.Spec.rejects_first_chunk_length_12","Png.Spec.rejects_zero_width","Png.Spec.rejects_zero_height","Png.Spec.rejects_width_at_cap","Png.Spec.rejects_height_at_cap","Png.Spec.rejects_illegal_depth","Png.Spec.rejects_unknown_colour_type","Png.Spec.rejects_unknown_interlace","Png.Spec.rejects_nonzero_compression","Png.Spec.rejects_nonzero_filter","Png.Spec.rejects_second_ihdr","Png.Spec.rejects_header_wrong_length"]} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index b9dc45b..5f42e4c 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,11 +1,15 @@ name = "png" version = "0.1.0" license = "Apache-2.0" -defaultTargets = ["Png", "PngProofs", "png"] +defaultTargets = ["Png", "PngSpec", "PngProofs", "png"] [[lean_lib]] name = "Png" +[[lean_lib]] +name = "PngSpec" +roots = ["Png.Spec"] + [[lean_lib]] name = "PngProofs" roots = ["Png.Proofs"] diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index bf88b52..ad8276e 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,9 +2,11 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.12.3 `zlib` (crc32 and compress), plus a strict reading of the plan rules written in the harness +- Oracle: Python 3.13.17 `zlib` (crc32 and compress), plus a strict reading of the plan rules written in the harness; for the header read, also libpng where it is installed (below) - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261026 +- Inputs: 1485 +- Inputs counts every request of the sections below, up to the libpng comparison, which is counted on its own line - Real PNG files (zlib built): 4 of 4 accepted and reprinted byte for byte - Real PNG file: 1x1, bit depth 8, colour type 2 (RGB), 69 bytes - Real PNG file: 4x3, bit depth 8, colour type 6 (RGBA), 119 bytes @@ -16,15 +18,77 @@ 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 -- Named differences: none -- Failures: 0 +- 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: 10 of 10 +- Chunk order cases through `header`: 4 of 4 agreements +- The same cases through `parse`, the chunk layer: 4 of 4 agreements +- Headers at the cap, width or height 2^31 - 1, accepted: 3 of 3 +- 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 +- Accepted inputs stated in Png/Spec.lean, read from that file: 2 of 2 agree with the harness's own reading of the bytes +- Accepted inputs stated in Png/Spec.lean, through `header`: 2 of 2 answered with the stated header +- Accepted inputs stated in Png/Spec.lean, through libpng (built 1.6.43, running 1.6.43), decoded in full: 2 of 2 read with the stated header + +## libpng comparison of the header read + +Each file is read by libpng (`tests/libpng_header.c`, built against the system libpng, with its default width and height limits raised to 2^31 - 1) and by the tool's `header` request, and the two answers must agree: the same fields, or both refuse. The files: the real files, the colour type and depth grid, every allowed pair with and without Adam7 at three sizes, the header rule cases, 150 random well formed headers, and the chunk order cases. Whole files are decoded by libpng, image and all, except for the header rule cases, which libpng reads up to IDAT. + +- libpng header oracle (built 1.6.43, running 1.6.43, `tests/libpng_header.c`): 389 files, 386 agreements, 3 named differences +- Named differences: 3 +- Named difference, an IEND chunk with data before IDAT, a real IEND at the end (1): libpng refuses the file (IEND out of place); this reader accepts it; an IEND chunk that carries data is an ordinary chunk here (SPEC.md, Chunks) +- Named difference, an IEND chunk with data as the last chunk (1): libpng reads the file, with a warning; this reader refuses it; the file has no IEND chunk with empty data, which the PNG specification requires (SPEC.md, Chunks) +- Named difference, indexed colour with no PLTE chunk (1): libpng refuses the file (no PLTE before IDAT); this reader accepts it; which chunks must appear between IHDR and IEND is not checked (SPEC.md, Chunks) ## 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 `Png/Proofs/Verify.lean` during a clean `lake build` (17 jobs). +The output of `#print axioms` for the 11 headline theorems and the 30 theorems `comparator.json` names, from `lake env lean Png/Proofs/Verify.lean`. The harness reads the names, and fails on any axiom but `propext`, `Classical.choice`, `Quot.sound`. A self-test on planted output (a `sorryAx`, an axiom of a proof's own, a missing line) runs first. + +- '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] +- 'Png.Proofs.parse_sound' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.parseIhdr_sound' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.parseFile_sound' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.print_layout' depends on axioms: [propext, Quot.sound] +- 'Png.Proofs.printIhdr_layout' depends on axioms: [propext] +- 'Png.Proofs.isLetter_iff' depends on axioms: [propext] +- 'Png.Proofs.isIEND_iff' depends on axioms: [propext] +- 'Png.Spec.parse_print' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.parseIhdr_print' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.checkPair_iff' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.parseFile_print' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.parse_sound' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.parseIhdr_sound' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.parseFile_sound' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.print_layout' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.printIhdr_layout' depends on axioms: [propext] +- 'Png.Spec.isLetter_iff' depends on axioms: [propext] +- 'Png.Spec.ihdrType_eq' depends on axioms: [] +- 'Png.Spec.typeBytes_eq' depends on axioms: [] +- 'Png.Spec.isIEND_iff' depends on axioms: [propext] +- 'Png.Spec.reads_real_file_header' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.reads_header_1920x1080' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_bad_signature' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_bad_crc' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_truncated_input' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_first_chunk_length_12' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_zero_width' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_zero_height' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_width_at_cap' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_height_at_cap' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_illegal_depth' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_unknown_colour_type' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_unknown_interlace' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_nonzero_compression' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_nonzero_filter' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_second_ihdr' depends on axioms: [propext, Quot.sound] +- 'Png.Spec.rejects_header_wrong_length' depends on axioms: [propext, Quot.sound] -```text -'Png.Proofs.parse_print' depends on axioms: [propext, Quot.sound] -``` +## Outcome -No other axiom is named, and sorryAx is not named. +- Failures: 0 diff --git a/tests/libpng_header.c b/tests/libpng_header.c new file mode 100644 index 0000000..ee24ca0 --- /dev/null +++ b/tests/libpng_header.c @@ -0,0 +1,166 @@ +/* + The libpng oracle for the header tests in run_tests.py. + + Reads one request per line and prints one answer per line. A + request is a mode, a space, and the bytes of a PNG file in hex. + + info read the file with png_read_info, which reads the + signature and every chunk up to the first IDAT, + and checks the IHDR fields (png_check_IHDR). + full the same, then decode the image (png_read_image) + and read the rest of the file to IEND + (png_read_end), so chunks after IDAT are seen too. + version print the libpng version this was built against + and the one it runs with. + + The answer is `ok:` and the header fields as text, in the shape + the Lean tool's `header` request uses (`1920x1080 d8 t6 i0`), or + `none:` and libpng's error message. Warnings do not change the + answer; the count of them is added as ` warnings:N` when there + are any. + + libpng's default limits on width and height (one million each) + are raised to 2^31 - 1, the PNG specification's own cap, so that + the comparison is with the specification's rule and not with a + library default. Everything else is libpng's default handling. + + Built by tests/run_tests.py when a C compiler and the libpng + headers are present; the header oracle section is skipped, and + says so, when they are not. +*/ + +#include +#include +#include +#include + +struct source { + const unsigned char *data; + size_t len; + size_t pos; +}; + +static char error_text[512]; +static int warnings; + +static void read_bytes(png_structp png, png_bytep out, png_size_t n) { + struct source *src = (struct source *)png_get_io_ptr(png); + if (n > src->len - src->pos) { + png_error(png, "input ends early"); + } + memcpy(out, src->data + src->pos, n); + src->pos += n; +} + +static void on_error(png_structp png, png_const_charp msg) { + snprintf(error_text, sizeof error_text, "%s", msg); + png_longjmp(png, 1); +} + +static void on_warning(png_structp png, png_const_charp msg) { + (void)png; + (void)msg; + warnings++; +} + +static int hex_value(int c) { + if (c >= '0' && c <= '9') return c - '0'; + if (c >= 'a' && c <= 'f') return c - 'a' + 10; + if (c >= 'A' && c <= 'F') return c - 'A' + 10; + return -1; +} + +/* Rows of the decoded image; global so the error path can free them. */ +static png_bytep *rows; +static png_uint_32 row_count; + +static void free_rows(void) { + if (rows) { + for (png_uint_32 i = 0; i < row_count; i++) free(rows[i]); + free(rows); + } + rows = NULL; + row_count = 0; +} + +static void answer(int full, const unsigned char *data, size_t len) { + png_structp png; + png_infop info; + struct source src = {data, len, 0}; + png_uint_32 width, height; + int depth, ctype, interlace; + + error_text[0] = 0; + warnings = 0; + png = png_create_read_struct(PNG_LIBPNG_VER_STRING, NULL, on_error, on_warning); + if (!png) { + printf("none:could not create a read struct\n"); + return; + } + info = png_create_info_struct(png); + if (!info) { + png_destroy_read_struct(&png, NULL, NULL); + printf("none:could not create an info struct\n"); + return; + } + if (setjmp(png_jmpbuf(png))) { + free_rows(); + png_destroy_read_struct(&png, &info, NULL); + printf("none:%s\n", error_text); + return; + } + png_set_user_limits(png, 0x7fffffffU, 0x7fffffffU); + png_set_read_fn(png, &src, read_bytes); + png_read_info(png, info); + png_get_IHDR(png, info, &width, &height, &depth, &ctype, &interlace, NULL, NULL); + if (full) { + png_size_t rowbytes; + png_set_interlace_handling(png); + png_read_update_info(png, info); + rowbytes = png_get_rowbytes(png, info); + rows = (png_bytep *)calloc(height, sizeof *rows); + if (!rows) png_error(png, "out of memory"); + row_count = height; + for (png_uint_32 i = 0; i < height; i++) { + rows[i] = (png_bytep)malloc(rowbytes ? rowbytes : 1); + if (!rows[i]) png_error(png, "out of memory"); + } + png_read_image(png, rows); + png_read_end(png, NULL); + free_rows(); + } + png_destroy_read_struct(&png, &info, NULL); + printf("ok:%lux%lu d%d t%d i%d", (unsigned long)width, (unsigned long)height, depth, + ctype, interlace); + if (warnings) printf(" warnings:%d", warnings); + printf("\n"); +} + +int main(void) { + static char line[1 << 20]; + static unsigned char bytes[1 << 19]; + while (fgets(line, sizeof line, stdin)) { + size_t n = strlen(line); + while (n && (line[n - 1] == '\n' || line[n - 1] == '\r')) line[--n] = 0; + if (strcmp(line, "version") == 0) { + printf("ok:built %s, running %s\n", PNG_LIBPNG_VER_STRING, png_get_libpng_ver(NULL)); + } else if (strncmp(line, "info ", 5) == 0 || strncmp(line, "full ", 5) == 0) { + const char *hex = line + 5; + size_t len = strlen(hex); + size_t count = 0; + int bad = (len % 2 != 0) || (len / 2 > sizeof bytes); + for (size_t i = 0; !bad && i < len; i += 2) { + int hi = hex_value(hex[i]); + int lo = hex_value(hex[i + 1]); + if (hi < 0 || lo < 0) bad = 1; + else bytes[count++] = (unsigned char)(hi * 16 + lo); + } + if (bad) printf("error\n"); + else answer(line[0] == 'f', bytes, count); + } else { + printf("error\n"); + } + fflush(stdout); + } + return 0; +} diff --git a/tests/run_tests.py b/tests/run_tests.py index d3901ef..42f03a0 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1,7 +1,11 @@ #!/usr/bin/env python3 """Tests for the Lean PNG chunk parser and printer. -Four parts. +Seven parts. Parts 1 to 4 are the slice 1 suite, unchanged. +Part 5 is slice 2: the IHDR header read through the `header` +request. Part 6 checks the accepted inputs stated in +Png/Spec.lean. Part 7 compares the header read with libpng, where libpng is +installed. 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 +34,44 @@ 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 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, and a width or height of 2^31 - 1 accepted. A + second IHDR chunk must be rejected by `header` and read by + `parse`; an IEND chunk with data is an ordinary chunk at both + layers. 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. + +6. The accepted inputs stated in Png/Spec.lean + (Png.Spec.reads_real_file_header, a whole file, and + Png.Spec.reads_header_1920x1080, 13 header bytes, wrapped in + a file with an all zero image), read from that file. The + stated header must match the harness's own big endian + reading of the bytes, the image data must inflate to the + size that header gives, the tool's `header` answer must be + the stated header, and so must libpng's, decoding the whole + file, where libpng is installed. + +7. The libpng comparison. tests/libpng_header.c is built + against the system libpng (skipped, and said so, when there + is no C compiler or no libpng). Each file is read by libpng + and by `header`, and the answers must agree field for field, + or both refuse, except in the named differences listed in + LIBPNG_NAMED. The 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 libpng decodes), the + header rule cases, 150 random well formed headers, and the + chunk order cases. + python3 tests/run_tests.py [--seed N] [--count N] The tool is driven one batch process per chunk of requests, input @@ -39,7 +81,10 @@ """ import argparse +import json import random +import re +import shutil import struct import subprocess import sys @@ -136,8 +181,13 @@ def drain(stream, buf, cap): return answers, problem +ASKED = [0] + + def ask_all(lines): - """Chunked run_tool. Answers align with lines, or None entries.""" + """Chunked run_tool. Answers align with lines, or None entries. + Every request counts toward the record's Inputs.""" + ASKED[0] += len(lines) answers = [] problems = [] for i in range(0, len(lines), CHUNK): @@ -244,9 +294,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 +308,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 +550,772 @@ 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 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))), + ( + "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_chunk_order(): + """Chunk order cases the file level read settles. A second + IHDR chunk, right after the first or after IDAT, is refused + by `header` (the PNG specification allows one IHDR chunk), + while `parse`, the chunk layer, still reads it as an ordinary + chunk. An IEND chunk that carries data is an ordinary chunk at + both layers: before IDAT, with a real IEND at the end, the + file reads; as the last chunk, with no real IEND after it, + the file is refused.""" + ihdr1 = make_chunk(b"IHDR", ihdr_full(1, 1, 8, 2)) + ihdr2 = make_chunk(b"IHDR", ihdr_full(2, 2, 8, 2)) + idat = make_chunk(b"IDAT", zlib.compress(b"\x00\x00\x00\x00")) + iend = make_chunk(b"IEND", b"") + iend_data = make_chunk(b"IEND", b"\x01\x02") + # (name, file, header answer, chunk layer accepts?) + cases = [ + ("a second IHDR right after the first", SIG + ihdr1 + ihdr2 + idat + iend, "none", True), + ("a second IHDR after IDAT", SIG + ihdr1 + idat + ihdr2 + iend, "none", True), + ( + "an IEND chunk with data before IDAT, a real IEND at the end", + SIG + ihdr1 + iend_data + idat + iend, + header_line(1, 1, 8, 2, 0), + True, + ), + ("an IEND chunk with data as the last chunk", SIG + ihdr1 + idat + iend_data, "none", False), + ] + lines = [] + failures = [] + answers, problems = ask_all([header_request(data) for _, data, _, _ in cases]) + for problem in problems: + failures.append(f"chunk order: tool problem: {problem}") + agree = 0 + for (name, _, want, _), ans in zip(cases, answers): + if ans == want: + agree += 1 + else: + failures.append(f"chunk order {name}, header: want {want!r}, got {ans!r}") + lines.append(f"Chunk order cases through `header`: {agree} of {len(cases)} agreements") + answers, problems = ask_all([request(data) for _, data, _, _ in cases]) + for problem in problems: + failures.append(f"chunk order, parse: tool problem: {problem}") + agree = 0 + for (name, data, _, chunk_ok), ans in zip(cases, answers): + want = ("ok:" + codes(data)) if chunk_ok else "none" + if ans == want: + agree += 1 + else: + failures.append(f"chunk order {name}, parse: want {want[:60]!r}, got {ans!r}") + lines.append( + f"The same cases through `parse`, the chunk layer: {agree} of {len(cases)} agreements" + ) + 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_bounds(): + """The largest width and height the rules allow, 2^31 - 1, are + accepted with their fields: the cap is exact on both sides.""" + top = 2**31 - 1 + cases = [(top, 3, 8, 6, 0), (4, top, 8, 6, 0), (top, top, 8, 0, 1)] + 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 bounds: 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 bound {fields}: want {want!r}, got {ans!r}") + lines.append(f"Headers at the cap, width or height 2^31 - 1, accepted: {agree} of {len(cases)}") + return lines, failures + + +# ---------------------------------------------------------------- the +# libpng oracle for the header read. tests/libpng_header.c is built +# against the system libpng, when there is one, and each file below +# is read by libpng and by the Lean tool's `header` request. The +# answers must agree, field for field, except in the named +# differences listed here, each of which is a rule this reader +# leaves out on purpose (SPEC.md says so) or a place libpng is more +# lenient than the PNG specification. + +LIBPNG_SRC = ROOT / "tests" / "libpng_header.c" +LIBPNG_EXE = ROOT / ".lake" / "oracle" / "libpng_header" + +CHANNELS = {0: 1, 2: 3, 3: 1, 4: 2, 6: 4} +ADAM7 = [(0, 0, 8, 8), (4, 0, 8, 8), (0, 4, 4, 8), (2, 0, 4, 4), (0, 2, 2, 4), (1, 0, 2, 2), (0, 1, 1, 2)] + +# Named differences: case name -> (what libpng answers, why). +LIBPNG_NAMED = { + "indexed colour with no PLTE chunk": ( + "libpng refuses the file (no PLTE before IDAT); this reader accepts it", + "which chunks must appear between IHDR and IEND is not checked (SPEC.md, Chunks)", + ), + "an IEND chunk with data before IDAT, a real IEND at the end": ( + "libpng refuses the file (IEND out of place); this reader accepts it", + "an IEND chunk that carries data is an ordinary chunk here (SPEC.md, Chunks)", + ), + "an IEND chunk with data as the last chunk": ( + "libpng reads the file, with a warning; this reader refuses it", + "the file has no IEND chunk with empty data, which the PNG specification requires (SPEC.md, Chunks)", + ), +} + + +LIBPNG_BUILT = [] + + +def build_libpng(): + """Build the libpng oracle, once per run. Returns (version text, + None) or (None, the reason it could not be built).""" + if not LIBPNG_BUILT: + LIBPNG_BUILT.append(build_libpng_once()) + return LIBPNG_BUILT[0] + + +def build_libpng_once(): + cc = shutil.which("cc") or shutil.which("gcc") or shutil.which("clang") + if not cc: + return None, "no C compiler" + flags = ["-lpng16"] + if shutil.which("pkg-config"): + pc = subprocess.run( + ["pkg-config", "--cflags", "--libs", "libpng"], capture_output=True, text=True + ) + if pc.returncode == 0 and pc.stdout.split(): + flags = pc.stdout.split() + LIBPNG_EXE.parent.mkdir(parents=True, exist_ok=True) + build = subprocess.run( + [cc, "-O1", "-o", str(LIBPNG_EXE), str(LIBPNG_SRC), *flags], + capture_output=True, + text=True, + ) + if build.returncode != 0: + tail = " / ".join(build.stderr.strip().splitlines()[-2:]) + return None, f"libpng oracle did not build: {tail}" + run = subprocess.run([str(LIBPNG_EXE)], input="version\n", capture_output=True, text=True) + if run.returncode != 0 or not run.stdout.startswith("ok:"): + return None, "libpng oracle did not run" + return run.stdout[3:].strip(), None + + +def ask_libpng(requests): + run = subprocess.run( + [str(LIBPNG_EXE)], + input="".join(r + "\n" for r in requests), + capture_output=True, + text=True, + timeout=TIMEOUT, + ) + answers = run.stdout.split("\n") + if answers and answers[-1] == "": + answers.pop() + if run.returncode != 0 or len(answers) != len(requests): + return None + return answers + + +def raw_image(width, height, depth, colour_type, interlace): + """Filtered scanlines of an all zero image: a filter byte of 0, + then zero pixels, for each row of each Adam7 pass when the + image is interlaced.""" + bits = CHANNELS.get(colour_type, 1) * depth + + def rows(w, h): + return (b"\x00" * (1 + (w * bits + 7) // 8)) * h + + if interlace != 1: + return rows(width, height) + out = b"" + for x0, y0, dx, dy in ADAM7: + pw = (width - x0 + dx - 1) // dx if width > x0 else 0 + ph = (height - y0 + dy - 1) // dy if height > y0 else 0 + if pw and ph: + out += rows(pw, ph) + return out + + +def oracle_png(width, height, depth, colour_type, interlace=0, comp=0, filt=0, plte=True, raw=None): + """A whole file whose image data decodes, for colour types and + depths the table allows: indexed colour gets a one entry PLTE + chunk, and the IDAT chunk holds an all zero image.""" + if raw is None: + if colour_type in CHANNELS and depth in ALLOWED.get(colour_type, []): + raw = raw_image(width, height, depth, colour_type, interlace) + else: + raw = b"\x00" + parts = [SIG, make_chunk(b"IHDR", ihdr_full(width, height, depth, colour_type, comp, filt, interlace))] + if colour_type == 3 and plte: + parts.append(make_chunk(b"PLTE", b"\x00\x00\x00")) + parts.append(make_chunk(b"IDAT", zlib.compress(raw))) + parts.append(make_chunk(b"IEND", b"")) + return b"".join(parts) + + +def libpng_cases(seed): + """(name, mode, file) for the libpng comparison. `full` reads the + whole file and decodes the image; `info` reads up to IDAT and is + used where the image would be too large to decode.""" + cases = [] + for name, data in real_files(seed): + cases.append((f"real file: {name}", "full", data)) + for t in list(range(13)) + [255]: + for d in [0, 1, 2, 3, 4, 5, 8, 16, 255]: + cases.append((f"grid: colour type {t}, depth {d}", "full", oracle_png(3, 2, d, t))) + for t in sorted(ALLOWED): + for d in ALLOWED[t]: + for i in (0, 1): + for w, h in ((1, 1), (3, 2), (9, 9)): + cases.append((f"allowed pair: {w}x{h} d{d} t{t} i{i}", "full", oracle_png(w, h, d, t, i))) + top = 2**31 - 1 + z = b"\x00" # read up to IDAT only, so the image data is not looked at + for name, data in [ + ("a width of zero", oracle_png(0, 3, 8, 6, raw=z)), + ("a height of zero", oracle_png(4, 0, 8, 6, raw=z)), + ("a width of 2^31", oracle_png(2**31, 3, 8, 6, raw=z)), + ("a height of 2^31", oracle_png(4, 2**31, 8, 6, raw=z)), + ("a width of 2^32 - 1", oracle_png(2**32 - 1, 3, 8, 6, raw=z)), + ("a height of 2^32 - 1", oracle_png(4, 2**32 - 1, 8, 6, raw=z)), + ("a compression byte of 1", oracle_png(4, 3, 8, 6, comp=1, raw=z)), + ("a filter byte of 1", oracle_png(4, 3, 8, 6, filt=1, raw=z)), + ("an interlace byte of 2", oracle_png(4, 3, 8, 6, interlace=2, raw=z)), + ("a width of 2^31 - 1", oracle_png(top, 3, 8, 6, raw=z)), + ("a height of 2^31 - 1", oracle_png(4, top, 8, 6, raw=z)), + ("a width and height of 2^31 - 1, Adam7", oracle_png(top, top, 8, 0, 1, raw=z)), + ]: + cases.append((f"header rule: {name}", "info", data)) + for name, cut in [("an IHDR chunk of 12 bytes", 12), ("an IHDR chunk of 14 bytes", 14)]: + body = (ihdr_full(4, 3, 8, 6) + b"\x00")[:cut] + data = ( + SIG + + make_chunk(b"IHDR", body) + + make_chunk(b"IDAT", zlib.compress(raw_image(4, 3, 8, 6, 0))) + + make_chunk(b"IEND", b"") + ) + cases.append((f"header rule: {name}", "info", data)) + rng = random.Random(seed + 13) + for k in range(150): + t = rng.choice(sorted(ALLOWED)) + d = rng.choice(ALLOWED[t]) + w, h, i = rng.randrange(1, 40), rng.randrange(1, 40), rng.randrange(0, 2) + cases.append((f"random: {w}x{h} d{d} t{t} i{i}", "full", oracle_png(w, h, d, t, i))) + ihdr1 = make_chunk(b"IHDR", ihdr_full(1, 1, 8, 2)) + ihdr2 = make_chunk(b"IHDR", ihdr_full(2, 2, 8, 2)) + idat = make_chunk(b"IDAT", zlib.compress(raw_image(1, 1, 8, 2, 0))) + iend = make_chunk(b"IEND", b"") + iend_data = make_chunk(b"IEND", b"\x01\x02") + cases += [ + ("a second IHDR right after the first", "full", SIG + ihdr1 + ihdr2 + idat + iend), + ("a second IHDR after IDAT", "full", SIG + ihdr1 + idat + ihdr2 + iend), + ("an IEND chunk with data before IDAT, a real IEND at the end", "full", SIG + ihdr1 + iend_data + idat + iend), + ("an IEND chunk with data as the last chunk", "full", SIG + ihdr1 + idat + iend_data), + ("indexed colour with no PLTE chunk", "full", oracle_png(3, 2, 8, 3, plte=False)), + ] + return cases + + +def lean_header_text(ans): + """The Lean tool's `header` answer as the same text libpng's + answer uses: `ok:` and the fields, or `none`.""" + if ans is None or not ans.startswith("ok:"): + return ans + try: + return "ok:" + bytes(int(c) for c in ans[3:].split(",")).decode("ascii") + except ValueError: + return ans + + +def run_libpng(seed): + """Returns (lines, failures, inputs, named): the record lines, + the failures, the count of files compared, and the named + differences met, with their counts.""" + version, why = build_libpng() + if version is None: + return [f"libpng header oracle: skipped, {why}"], [], 0, {} + cases = libpng_cases(seed) + lp = ask_libpng([f"{mode} {data.hex()}" for _, mode, data in cases]) + if lp is None: + return [f"libpng header oracle ({version}): did not answer"], ["libpng oracle did not answer"], 0, {} + lean, problems = ask_all([header_request(data) for _, _, data in cases]) + failures = [f"libpng comparison: tool problem: {p}" for p in problems] + agree = 0 + named = {} + for (name, mode, _), want, got in zip(cases, lp, lean): + theirs = want.split(" warnings:")[0] + ours = lean_header_text(got) + same = (theirs.startswith("ok:") and ours == theirs) or ( + theirs.startswith("none:") and ours == "none" + ) + if same: + agree += 1 + elif name in LIBPNG_NAMED: + named[name] = named.get(name, 0) + 1 + else: + failures.append(f"libpng comparison {name} ({mode}): libpng {want!r}, this reader {ours!r}") + lines = [ + f"libpng header oracle ({version}, `tests/libpng_header.c`): {len(cases)} files, " + f"{agree} agreements, {sum(named.values())} named differences" + ] + for name in LIBPNG_NAMED: + if name in [c[0] for c in cases] and name not in named: + failures.append(f"libpng comparison {name}: the named difference did not occur") + return lines, failures, len(cases), named + + +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 + + +# ---------------------------------------------------------------- the +# accepted inputs stated in Png/Spec.lean. Two statements there give +# an input and the header the reader returns for it: +# Png.Spec.reads_real_file_header (a whole file) and +# Png.Spec.reads_header_1920x1080 (13 header bytes). The bytes and +# the fields are read from Png/Spec.lean itself, so the check is of +# the statements as written, and each is checked three ways: the +# harness's own reading of the bytes (big endian width and height, +# zlib for the CRCs and the image data), the tool's `header` answer, +# and libpng's answer where libpng is installed. + +SPEC_LEAN = ROOT / "Png" / "Spec.lean" + + +def lean_bytes(text): + return bytes(int(x) for x in text.replace("\n", " ").split(",")) + + +HEADER_FIELDS = ("width", "height", "bitDepth", "colorType", "interlace") + + +def lean_fields(text): + """The header a statement gives, written as a structure + instance with its five fields named, as (width, height, bit + depth, colour type, interlace).""" + got = dict( + (k, int(v)) for k, v in re.findall(r"(\w+)\s*:=\s*([0-9]+)", text) + ) + if sorted(got) != sorted(HEADER_FIELDS): + return None + return tuple(got[k] for k in HEADER_FIELDS) + + +def spec_examples(): + """(theorem, file, the 13 header bytes, the stated fields), read + from Png/Spec.lean. The header only statement is wrapped in a + whole file: its 13 bytes as the IHDR data, an IDAT chunk holding an + all zero image of that size, and IEND.""" + src = SPEC_LEAN.read_text(encoding="utf-8") + found = [] + m = re.search( + r"theorem Png\.Spec\.reads_real_file_header :\s*\(parseFile \(\[([0-9,\s]*)\]\s*" + r":\s*List UInt8\)\)\.map Prod\.fst =\s*some \{([^}]*)\}", + src, + ) + if m and lean_fields(m.group(2)): + data = lean_bytes(m.group(1)) + found.append(("Png.Spec.reads_real_file_header", data, data[16:29], lean_fields(m.group(2)))) + m = re.search( + r"theorem Png\.Spec\.reads_header_1920x1080 :\s*parseIhdr \(\[([0-9,\s]*)\]\s*" + r":\s*List UInt8\) =\s*some \{([^}]*)\}", + src, + ) + if m and lean_fields(m.group(2)): + ihdr = lean_bytes(m.group(1)) + w, h, d, t, i = lean_fields(m.group(2)) + data = ( + SIG + + make_chunk(b"IHDR", ihdr) + + make_chunk(b"IDAT", zlib.compress(raw_image(w, h, d, t, i))) + + make_chunk(b"IEND", b"") + ) + found.append(("Png.Spec.reads_header_1920x1080", data, ihdr, (w, h, d, t, i))) + return found + + +def own_reading(data, ihdr, fields): + """The harness's own reading of a stated input: None when it + agrees with the stated fields, else what is wrong.""" + w, h, d, t, i = fields + if len(ihdr) != 13: + return f"the header is {len(ihdr)} bytes, not 13" + got = struct.unpack(">IIBBBBB", ihdr) + if got != (w, h, d, t, 0, 0, i): + return f"the 13 bytes read big endian are {got}, not {(w, h, d, t, 0, 0, i)}" + chunks = oracle_parse(data) + if chunks is None: + return "the strict oracle refuses the file" + if chunks[0] != (b"IHDR", ihdr): + return "the file's IHDR data is not the stated 13 bytes" + image = zlib.decompress(b"".join(c for typ, c in chunks if typ == b"IDAT")) + want = len(raw_image(w, h, d, t, i)) + if len(image) != want: + return f"the image data inflates to {len(image)} bytes, not {want}" + return None + + +def run_spec_examples(): + lines = [] + failures = [] + cases = spec_examples() + if len(cases) != 2: + failures.append( + f"Png/Spec.lean accepted inputs: found {len(cases)} of the 2 statements; " + "the harness could not read them" + ) + own_ok = 0 + for name, data, ihdr, fields in cases: + wrong = own_reading(data, ihdr, fields) + if wrong is None: + own_ok += 1 + else: + failures.append(f"{name}: {wrong}") + lines.append( + f"Accepted inputs stated in Png/Spec.lean, read from that file: {own_ok} of " + f"{len(cases)} agree with the harness's own reading of the bytes" + ) + answers, problems = ask_all([header_request(data) for _, data, _, _ in cases]) + failures += [f"Png/Spec.lean accepted inputs: tool problem: {p}" for p in problems] + tool_ok = 0 + for (name, _, _, fields), ans in zip(cases, answers): + want = header_line(*fields) + if ans == want: + tool_ok += 1 + else: + failures.append(f"{name} through `header`: want {want!r}, got {ans!r}") + lines.append( + f"Accepted inputs stated in Png/Spec.lean, through `header`: {tool_ok} of " + f"{len(cases)} answered with the stated header" + ) + version, why = build_libpng() + if version is None: + lines.append(f"Accepted inputs stated in Png/Spec.lean, through libpng: skipped, {why}") + return lines, failures + lp = ask_libpng([f"full {data.hex()}" for _, data, _, _ in cases]) + if lp is None: + failures.append("Png/Spec.lean accepted inputs: the libpng oracle did not answer") + return lines, failures + lp_ok = 0 + for (name, _, _, fields), got in zip(cases, lp): + w, h, d, t, i = fields + want = f"ok:{w}x{h} d{d} t{t} i{i}" + if got.split(" warnings:")[0] == want: + lp_ok += 1 + else: + failures.append(f"{name} through libpng: want {want!r}, got {got!r}") + lines.append( + f"Accepted inputs stated in Png/Spec.lean, through libpng ({version}), " + f"decoded in full: {lp_ok} of {len(cases)} read with the stated header" + ) + return lines, failures + + +# ---------------------------------------------------------------- the +# axiom check. Png/Proofs/Verify.lean prints `#print axioms` for the +# headline theorems in Png.Proofs and for every theorem +# comparator.json names. Each must have its line, and each may +# depend on these three axioms and no other: a `sorryAx`, or any +# axiom a proof adds of its own, is a failure. + +AXIOMS_ALLOWED = ("propext", "Classical.choice", "Quot.sound") + +HEADLINE = [ + "Png.Proofs.parse_print", + "Png.Proofs.parseIhdr_print", + "Png.Proofs.checkPair_iff", + "Png.Proofs.parseFile_print", + "Png.Proofs.parse_sound", + "Png.Proofs.parseIhdr_sound", + "Png.Proofs.parseFile_sound", + "Png.Proofs.print_layout", + "Png.Proofs.printIhdr_layout", + "Png.Proofs.isLetter_iff", + "Png.Proofs.isIEND_iff", +] + + +def axiom_names(): + """The theorems the axiom check covers: the headline theorems, + then every theorem comparator.json names.""" + config = json.loads((ROOT / "comparator.json").read_text(encoding="utf-8")) + return HEADLINE + list(config["theorem_names"]) + + +def read_axioms(text): + """The axioms of each theorem in `#print axioms` output, by + name. A list may run over several lines.""" + found = {} + for m in re.finditer(r"'([^']+)' depends on axioms: \[([^\]]*)\]", text): + found[m.group(1)] = [a.strip() for a in m.group(2).split(",") if a.strip()] + for m in re.finditer(r"'([^']+)' does not depend on any axioms", text): + found[m.group(1)] = [] + return found + + +def axiom_failures(found, names): + failures = [] + for name in names: + if name not in found: + failures.append(f"axiom check: no `#print axioms` output for {name}") + continue + extra = [a for a in found[name] if a not in AXIOMS_ALLOWED] + if extra: + failures.append( + f"axiom check: {name} depends on {', '.join(extra)}, " + "beyond propext, Classical.choice, and Quot.sound" + ) + return failures + + +def axiom_self_test(): + """The check itself, on planted output: a theorem on sorryAx, one + on an axiom of its own, and a missing line must each fail, and + clean output must pass. Returns the failures of the check.""" + names = ["A.clean", "A.none", "A.sorry", "A.own"] + planted = ( + "'A.clean' depends on axioms: [propext,\n Classical.choice, Quot.sound]\n" + "'A.none' does not depend on any axioms\n" + "'A.sorry' depends on axioms: [propext, sorryAx]\n" + "'A.own' depends on axioms: [Quot.sound, A.myAxiom]\n" + ) + got = axiom_failures(read_axioms(planted), names + ["A.missing"]) + want = [ + "axiom check: A.sorry depends on sorryAx, beyond propext, Classical.choice, and Quot.sound", + "axiom check: A.own depends on A.myAxiom, beyond propext, Classical.choice, and Quot.sound", + "axiom check: no `#print axioms` output for A.missing", + ] + if got != want: + return [f"axiom check self-test: planted output gave {got!r}"] + return [] + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=SEED_DEFAULT) @@ -523,10 +1343,26 @@ 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_chunk_order(), + run_header_bounds(), + run_header_random(args.seed), + run_header_malformed(), + run_spec_examples(), ): lines, failures = part all_lines += lines all_failures += failures + # The record's Inputs: every request of the sections above. The + # libpng comparison below runs only where libpng is installed, so + # it is counted on its own line, and a run without libpng records + # the same Inputs. + inputs = ASKED[0] + libpng_lines, libpng_failures, libpng_inputs, named = run_libpng(args.seed) + all_failures += libpng_failures lean_version = subprocess.run( ["lake", "env", "lean", "--version"], @@ -536,18 +1372,87 @@ def main(): timeout=120, ).stdout.strip() + # The axiom check: Png/Proofs/Verify.lean prints the axioms of the + # headline theorems and of every theorem comparator.json names, + # with `#print axioms`. The names in that output are read, and + # any axiom beyond the three standard ones is a failure. The + # output goes into the results file, in the Axiom check section. + all_failures += axiom_self_test() + axiom_run = subprocess.run( + ["lake", "env", "lean", "Png/Proofs/Verify.lean"], + cwd=ROOT, + capture_output=True, + text=True, + timeout=600, + ) + if axiom_run.returncode != 0: + all_failures.append( + f"axiom check: running Png/Proofs/Verify.lean exited {axiom_run.returncode}" + ) + covered = axiom_names() + found = read_axioms(axiom_run.stdout) + all_failures += axiom_failures(found, covered) + axiom_lines = [ + f"'{name}' depends on axioms: [{', '.join(found[name])}]" + for name in covered + if name in found + ] + out = ["# Test results", ""] out.append("Written by `tests/run_tests.py`. Rerun it to check these numbers.") out.append("") out.append( f"- Oracle: Python {sys.version.split()[0]} `zlib` (crc32 and compress), " - "plus a strict reading of the plan rules written in the harness" + "plus a strict reading of the plan rules written in the harness; " + "for the header read, also libpng where it is installed (below)" ) out.append(f"- Lean: {lean_version}") out.append(f"- Seed: {args.seed}") + out.append(f"- Inputs: {inputs}") + out.append( + "- Inputs counts every request of the sections below, up to the libpng " + "comparison, which is counted on its own line" + ) for line in all_lines: out.append(f"- {line}") - out.append("- Named differences: none") + out.append("") + out.append("## libpng comparison of the header read") + out.append("") + out.append( + "Each file is read by libpng (`tests/libpng_header.c`, built against the " + "system libpng, with its default width and height limits raised to " + "2^31 - 1) and by the tool's `header` request, and the two answers must " + "agree: the same fields, or both refuse. The files: the real files, the " + "colour type and depth grid, every allowed pair with and without Adam7 at " + "three sizes, the header rule cases, 150 random well formed headers, and " + "the chunk order cases. Whole files are decoded by libpng, image and all, " + "except for the header rule cases, which libpng reads up to IDAT." + ) + out.append("") + for line in libpng_lines: + out.append(f"- {line}") + out.append(f"- Named differences: {sum(named.values())}") + for name, count in named.items(): + what, why = LIBPNG_NAMED[name] + out.append(f"- Named difference, {name} ({count}): {what}; {why}") + out.append("") + out.append("## Axiom check") + out.append("") + out.append( + f"The output of `#print axioms` for the {len(HEADLINE)} headline theorems " + f"and the {len(covered) - len(HEADLINE)} theorems `comparator.json` names, " + "from `lake env lean Png/Proofs/Verify.lean`. The harness reads the names, and " + "fails on any axiom but " + + ", ".join(f"`{a}`" for a in AXIOMS_ALLOWED) + + ". A self-test on planted output (a `sorryAx`, an axiom of a proof's own, " + "a missing line) runs first." + ) + out.append("") + for line in axiom_lines: + out.append(f"- {line}") + out.append("") + out.append("## Outcome") + out.append("") out.append(f"- Failures: {len(all_failures)}") for failure in all_failures[:50]: out.append(f"- FAILURE: {failure}")