PNG slice 2: IHDR decoding, with proved table

.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

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

Png.lean

@@ -1,3 +1,4 @@
 import Png.Crc32
 import Png.Value
 import Png.Parse
+import Png.Header

Png/Header.lean

@@ -0,0 +1,144 @@
+/-
+  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.
+-/
+
+import Png.Parse
+
+namespace Png
+
+/-- The decoded IHDR header: width and height as numbers, the
+    bit depth, the colour type, and the interlace method as
+    bytes. The compression and filter bytes are not held: each
+    is zero in every accepted file, and printing writes zero. -/
+structure Ihdr where
+  width : Nat
+  height : Nat
+  bitDepth : UInt8
+  colorType : UInt8
+  interlace : UInt8
+  deriving DecidableEq, Repr
+
+/-- The bit depths a colour type allows, by the colour type's
+    number. A number that is not a PNG colour type allows none. -/
+def allowedDepths (ct : Nat) : List Nat :=
+  if ct = 0 then [1, 2, 4, 8, 16]
+  else if ct = 2 then [8, 16]
+  else if ct = 3 then [1, 2, 4, 8]
+  else if ct = 4 then [8, 16]
+  else if ct = 6 then [8, 16]
+  else []
+
+/-- Does this depth go with this colour type? The two numbers
+    are the byte values. -/
+def pairAllowed (ct bd : Nat) : Bool :=
+  decide (bd ∈ allowedDepths ct)
+
+/-- The allowed (colour type, bit depth) pairs, written out in
+    full. The checker above is built from the per-type table;
+    the proof in `Proofs/Header.lean` shows the two agree on
+    every colour type byte and every bit depth byte. -/
+def allowedPairs : List (Nat × Nat) :=
+  [(0, 1), (0, 2), (0, 4), (0, 8), (0, 16),
+   (2, 8), (2, 16),
+   (3, 1), (3, 2), (3, 4), (3, 8),
+   (4, 8), (4, 16),
+   (6, 8), (6, 16)]
+
+/-- Does this bit depth go with this colour type? The two
+    arguments are the file's bytes. -/
+def checkPair (ct bd : UInt8) : Bool := pairAllowed ct.toNat bd.toNat
+
+/-- A header is well formed when the width and the height are
+    above zero and below 2^31, the interlace byte is 0 or 1, and
+    the bit depth is one the colour type allows. -/
+def WFHeader (h : Ihdr) : Prop :=
+  0 < h.width ∧ h.width < 2147483648 ∧
+  0 < h.height ∧ h.height < 2147483648 ∧
+  (h.interlace = 0 ∨ h.interlace = 1) ∧
+  checkPair h.colorType h.bitDepth = true
+
+/-- The 13 IHDR data bytes of a header: width and height big
+    endian, then bit depth, colour type, compression zero,
+    filter zero, interlace. -/
+def printIhdr (h : Ihdr) : List UInt8 :=
+  be32 h.width ++ be32 h.height ++ [h.bitDepth, h.colorType, 0, 0, h.interlace]
+
+/-- Read 13 bytes as a header. Anything but exactly 13 bytes is
+    rejected, and so is a header that breaks any of the rules at
+    the top of this file: a width or height of zero 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
+
+/-- The decoded header of a chunk list: the first chunk's data
+    read as a header, or `none` when there is no first chunk or
+    its data does not read as one. -/
+def headerOf (doc : Doc) : Option Ihdr :=
+  match doc with
+  | c :: _ => parseIhdr c.data
+  | [] => none
+
+/-- Read a whole file at both layers: the chunk list of slice 1,
+    and the header decoded from the first chunk's data. A file
+    whose first chunk is not a valid IHDR, in the slice 2 sense,
+    is rejected here even when slice 1 accepts it. -/
+def parseFile (bs : List UInt8) : Option (Ihdr × Doc) :=
+  match parse bs with
+  | some doc => (headerOf doc).map fun h => (h, doc)
+  | none => none
+
+/-- A document is fully well formed when it is well formed at
+    the chunk layer (the `WF` of slice 1), its first chunk's
+    data is the printed form of some header, and that header is
+    well formed. Stated with the witnesses out, in the shape of
+    `WF`. -/
+def WFFull (doc : Doc) : Prop :=
+  ∃ (hd : Ihdr) (head : Chunk) (mid : List Chunk),
+    doc = head :: mid ++ [iendChunk] ∧
+    head.typeBytes = ihdrType ∧ head.data = printIhdr hd ∧
+    WFHeader hd ∧
+    (∀ c ∈ doc, WFChunk c) ∧
+    (∀ c ∈ head :: mid, isIEND c = false)
+
+end Png

Proofs.lean

@@ -1,2 +1,4 @@
 import Proofs.RoundTrip
+import Proofs.Header
 import Proofs.Verify
+import Proofs.SpecProofs

Proofs/Header.lean

@@ -0,0 +1,143 @@
+/-
+  The slice 2 proofs: the IHDR header round trip, the exactness
+  of the (colour type, bit depth) table, and the file level
+  round trip that joins the header to the chunk layer of
+  slice 1.
+
+  The table claim is `pairAllowed_iff`, with its byte form
+  `checkPair_iff`: the checker's answer agrees with the written
+  out list of allowed pairs for every colour type number and
+  every bit depth number. Colour types are bytes and bit depths
+  are bytes, so the numbers 0 to 255 are the whole of both, and
+  the proof settles the question for all of them: it splits on
+  the five colour types the PNG specification names, and in
+  each case the two sides come down to the same list of depths;
+  for every other colour type number both sides are empty. No
+  case is left to computation over the whole grid.
+
+  The header round trip is `parseIhdr_print`. The file level
+  claim is `parseFile_print`: a fully well formed document
+  (chunk layer well formed, first chunk the printed form of a
+  well formed header) prints and reads back whole, header
+  included.
+-/
+
+import Png
+import Proofs.RoundTrip
+
+namespace Png.Proofs
+
+open Png
+
+/-- One step of the header reader, stated for rewriting: 13
+    bytes at the front of the input, with whatever follows. -/
+theorem parseIhdr_step (w1 w2 w3 w4 h1 h2 h3 h4 bd ct comp filt int : UInt8)
+    (rest : List UInt8) :
+    parseIhdr (w1 :: w2 :: w3 :: w4 :: h1 :: h2 :: h3 :: h4
+      :: bd :: ct :: comp :: filt :: int :: rest) =
+      if rest ≠ [] then none
+      else if u32 w1 w2 w3 w4 = 0 ∨ u32 h1 h2 h3 h4 = 0 then none
+      else if 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 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 [if_neg (by simp : ¬ (([] : List UInt8) ≠ []))]
+  rw [if_neg (by omega : ¬ (w = 0 ∨ hh = 0))]
+  rw [if_neg (by omega : ¬ (w ≥ 2147483648 ∨ hh ≥ 2147483648))]
+  rw [if_neg (by decide : ¬ ((0 : UInt8) ≠ 0 ∨ (0 : UInt8) ≠ 0))]
+  rw [if_neg hnl, if_pos hpair]
+
+/-- The table, exactly: a depth goes with a colour type under
+    the checker if and only if the pair is in the written out
+    list of allowed pairs. Stated for all numbers, so in
+    particular for every colour type byte and every bit depth
+    byte. -/
+theorem pairAllowed_iff : ∀ n m : Nat,
+    pairAllowed n m = true ↔ (n, m) ∈ allowedPairs := by
+  intro n m
+  by_cases h0 : n = 0
+  · subst h0
+    simp only [pairAllowed, decide_eq_true_eq]
+    show m ∈ [1, 2, 4, 8, 16] ↔ (0, m) ∈ allowedPairs
+    simp [allowedPairs]
+  by_cases h2 : n = 2
+  · subst h2
+    simp only [pairAllowed, decide_eq_true_eq]
+    show m ∈ [8, 16] ↔ (2, m) ∈ allowedPairs
+    simp [allowedPairs]
+  by_cases h3 : n = 3
+  · subst h3
+    simp only [pairAllowed, decide_eq_true_eq]
+    show m ∈ [1, 2, 4, 8] ↔ (3, m) ∈ allowedPairs
+    simp [allowedPairs]
+  by_cases h4 : n = 4
+  · subst h4
+    simp only [pairAllowed, decide_eq_true_eq]
+    show m ∈ [8, 16] ↔ (4, m) ∈ allowedPairs
+    simp [allowedPairs]
+  by_cases h6 : n = 6
+  · subst h6
+    simp only [pairAllowed, decide_eq_true_eq]
+    show m ∈ [8, 16] ↔ (6, m) ∈ allowedPairs
+    simp [allowedPairs]
+  · have hdep : allowedDepths n = [] := by
+      unfold allowedDepths
+      rw [if_neg h0, if_neg h2, if_neg h3, if_neg h4, if_neg h6]
+    simp only [pairAllowed, decide_eq_true_eq, hdep]
+    simp [allowedPairs, h0, h2, h3, h4, h6]
+
+/-- The table, in the byte form the parser uses: the check on
+    two bytes holds if and only if the pair of their values is
+    in the written out list. -/
+theorem checkPair_iff (ct bd : UInt8) :
+    checkPair ct bd = true ↔ (ct.toNat, bd.toNat) ∈ allowedPairs :=
+  pairAllowed_iff ct.toNat bd.toNat
+
+/-- A fully well formed document is well formed at the chunk
+    layer. -/
+theorem wfFull_wf {doc : Doc} (h : WFFull doc) : WF doc := by
+  obtain ⟨hd, head, mid, hdoc, htype, hdata, -, hall, hnot⟩ := h
+  exact ⟨head, mid, hdoc, htype,
+    by rw [hdata]; exact printIhdr_length hd, hall, hnot⟩
+
+/-- The file level round trip: printing a fully well formed
+    document and reading the file back at both layers gives the
+    document back, with its header. -/
+theorem parseFile_print {doc : Doc} (h : WFFull doc) :
+    ∃ hd : Ihdr, parseFile (print doc) = some (hd, doc) := by
+  have hwf : WF doc := wfFull_wf h
+  obtain ⟨hd, head, mid, hdoc, htype, hdata, hwfhd, hall, hnot⟩ := h
+  refine ⟨hd, ?_⟩
+  unfold parseFile
+  rw [parse_print hwf]
+  show (headerOf doc).map (fun x => (x, doc)) = some (hd, doc)
+  rw [hdoc]
+  simp [headerOf, hdata, parseIhdr_print hd hwfhd]
+
+end Png.Proofs