PNG slice 2: IHDR decoding (png#3 carried forward, Png layout)

.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,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

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