diff --git a/SPEC.md b/SPEC.md index 32478ea..599fb41 100644 --- a/SPEC.md +++ b/SPEC.md @@ -69,19 +69,19 @@ What a sample means, for every decoder and encoder. | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | | IMG-JPG-1 | `decode_jpeg` returns none for every input that opens with SOI, then segments other than frame headers (DHT, DQT, SOS, DRI, COM, APP0 to APP15) each with a length field that fits its body, then a frame header other than SOF0 or an SOF0 segment whose sample precision is not 8, whatever follows. | Proved | proved | LAWS.bend jpeg_refuse_sofn; LAWS.bend jpeg_refuse_precision | -| IMG-JPG-2 | For a SOF0 frame whose components' sampling factors are each 1, 2 or 4, `decode_jpeg` places each component's samples in the order T.81 A.2.3 gives and replicates each sample over the pixels its sampling covers; for a factor outside 1, 2 and 4, `decode_jpeg` returns none. The sample values themselves are IMG-JPG-7's. | Proved | pending | LAWS.bend jpeg_refuse_factor1; LAWS.bend jpeg_refuse_factor3; LAWS.bend jpeg_refuse_factor1_any; LAWS.bend jpeg_refuse_factor3_any; LAWS.bend jpeg_refuse_count; LAWS.bend jpeg_comp_index; LAWS.bend jpeg_walk_unit; LAWS.bend jpeg_walk_comp; LAWS.bend jpeg_walk_mcu; LAWS.bend jpeg_walk_frame; LAWS.bend jpeg_walk_count; LAWS.bend jpeg_mcu_grid; LAWS.bend jpeg_mcu_grid_comp; LAWS.bend jpeg_block_cover; LAWS.bend jpeg_block_cover_all; LAWS.bend jpeg_points_at; LAWS.bend jpeg_rgbs_at | -| IMG-JPG-3 | For every well-formed raster `r` with both sides nonzero and at most 65535, `decode_jpeg(encode_jpeg(r))` is some raster of `r`'s size with alpha 255. | Proved | pending | LAWS.bend jpeg_enc_stuffed; LAWS.bend jpeg_unstuff; LAWS.bend jpeg_enc_header_walk; LAWS.bend jpeg_ent_walk; LAWS.bend jpeg_round_trip_scan; LAWS.bend jpeg_run_sized; LAWS.bend jpeg_round_trip_sized | +| IMG-JPG-2 | For a SOF0 frame of at most 2^31 points whose components' sampling factors are each 1, 2 or 4, `decode_jpeg` places each component's samples in the order T.81 A.2.3 gives and replicates each sample over the pixels its sampling covers; for a factor outside 1, 2 and 4, `decode_jpeg` returns none. The sample values themselves are IMG-JPG-7's. | Proved | pending | LAWS.bend jpeg_refuse_factor1; LAWS.bend jpeg_refuse_factor3; LAWS.bend jpeg_refuse_factor1_any; LAWS.bend jpeg_refuse_factor3_any; LAWS.bend jpeg_refuse_count; LAWS.bend jpeg_comp_index; LAWS.bend jpeg_walk_unit; LAWS.bend jpeg_walk_comp; LAWS.bend jpeg_walk_mcu; LAWS.bend jpeg_walk_frame; LAWS.bend jpeg_walk_count; LAWS.bend jpeg_mcu_grid; LAWS.bend jpeg_mcu_grid_comp; LAWS.bend jpeg_block_cover; LAWS.bend jpeg_block_cover_all; LAWS.bend jpeg_points_at; LAWS.bend jpeg_rgbs_at | +| IMG-JPG-3 | For every well-formed raster `r` with both sides nonzero and at most 65535 and at most 2^31 samples, `decode_jpeg(encode_jpeg(r))` is some raster of `r`'s size with alpha 255. | Proved | pending | LAWS.bend jpeg_enc_stuffed; LAWS.bend jpeg_unstuff; LAWS.bend jpeg_enc_header_walk; LAWS.bend jpeg_ent_walk; LAWS.bend jpeg_round_trip_scan; LAWS.bend jpeg_run_sized; LAWS.bend jpeg_round_trip_sized | | IMG-JPG-4 | `encode_jpeg(r)` is none exactly when `encode_png(r)` is none. | Proved | proved | LAWS.bend jpeg_png_refuse_alike | | IMG-JPG-5 | When `encode_jpeg(r)` is some, it begins with SOI and ends with EOI; when both sides of `r` are at most 65535 it is SOI, APP0 with the JFIF identifier, DQT, SOF0 carrying `r`'s width and height, two DHT, SOS, the entropy-coded data and EOI. | Proved | proved | LAWS.bend jpeg_enc_layout; LAWS.bend jpeg_enc_ends | | IMG-JPG-6 | `Jpeg.rgb(y, cb, cr)` equals the T.871 YCbCr to RGB conversion, rounded to nearest and clamped to 0 to 255, for every `y`, `cb`, `cr` from 0 to 255. | Trusted | | | | IMG-JPG-7 | `decode_jpeg` reads baseline files other encoders (libjpeg, Pillow) write to within the IDCT accuracy of T.81 Annex A.3.3. | Trusted | | | -| IMG-JPG-8 | For every well-formed raster `r` with both sides nonzero and at most 65535, every colour channel of `decode_jpeg(encode_jpeg(r))` is within 8 of `r`'s. | Trusted | | | +| IMG-JPG-8 | For every well-formed raster `r` with both sides nonzero and at most 65535 and at most 2^31 samples, every colour channel of `decode_jpeg(encode_jpeg(r))` is within 8 of `r`'s. | Trusted | | | ## Left to prove | ID | Proved so far | Missing | | :---- | :---- | :---- | -| IMG-JPG-2 | Refusal: a SOF0 segment with a factor outside 1, 2 and 4 makes `decode_jpeg` none, for one component or three, whatever precedes and follows it (`jpeg_refuse_factor1`, `jpeg_refuse_factor3`), and also after fill bytes before its marker and with a length field longer than its components (`jpeg_refuse_factor1_any`, `jpeg_refuse_factor3_any`); a SOF0 segment of any other component count is none whatever its factors (`jpeg_refuse_count`). Placement: a scan component takes the factors of the frame component whose identifier it names, the first with that identifier (`jpeg_comp_index`); the MCU walk goes from data unit `bi` to `bi + 1`, then to the next scan component, then to the next MCU (`jpeg_walk_unit`, `jpeg_walk_comp`, `jpeg_walk_mcu`); from the scan's first block the decoder's own walk visits the frame's MCUs in raster order, `ceil(w / 8 hmax)` to a row, and in each MCU the scan's components and their `hi * vi` units in T.81 order, the unit, component and column counters never wrapping (`jpeg_walk_frame`), and the U32 block count the decoder runs, `decode.nblocks`, is that order's length over `ceil(h / 8 vmax)` MCU rows when the scan carries the frame's data units and the count fits a U32 (`jpeg_walk_count`); the `hi * vi` units of any scan component sit in T.81 A.2.3's grid, `hi` to a row, each sample covering `hmax / hi` by `vmax / vi` pixels (`jpeg_mcu_grid`, `jpeg_mcu_grid_comp`); painting a block writes sample `k` over exactly the `pw` by `ph` pixels at `(ox + (k mod 8) * pw, oy + (k div 8) * ph)` inside the frame, for every sample size, 4 by 4 included, and onto every plane, one earlier blocks painted included (`jpeg_block_cover`, `jpeg_block_cover_all`); the decoder reads a plane out point by point, sample `k` being the value `Array.get` finds at index `k` (`jpeg_points_at`). Colour: sample `k` of the colour pass is `Jpeg.rgb` of point `k`'s Y, Cb and Cr (`jpeg_rgbs_at`) | that `Array.get` at an index finds the value the last `Array.set` at that index wrote, and a set at another index leaves it (the planes are perfect binary trees of `2^d` leaves, and the lemmas must follow the masked index down the tree), which joins the painting laws to `jpeg_points_at`. And the row is false as worded for frames of more than 2^31 points, which sides up to 65535 allow: `decode.plane` takes its depth from `U32.shl(nn)`, which wraps above 2^31, so the plane has fewer leaves than points and points alias (`decode.depth` is 0 at 2^31 + 1 points and 30 at 3 * 2^30), and past 2^32 points `w * h` itself wraps (a decision for the maintainer) | +| IMG-JPG-2 | Refusal: a SOF0 segment with a factor outside 1, 2 and 4 makes `decode_jpeg` none, for one component or three, whatever precedes and follows it (`jpeg_refuse_factor1`, `jpeg_refuse_factor3`), and also after fill bytes before its marker and with a length field longer than its components (`jpeg_refuse_factor1_any`, `jpeg_refuse_factor3_any`); a SOF0 segment of any other component count is none whatever its factors (`jpeg_refuse_count`). Placement: a scan component takes the factors of the frame component whose identifier it names, the first with that identifier (`jpeg_comp_index`); the MCU walk goes from data unit `bi` to `bi + 1`, then to the next scan component, then to the next MCU (`jpeg_walk_unit`, `jpeg_walk_comp`, `jpeg_walk_mcu`); from the scan's first block the decoder's own walk visits the frame's MCUs in raster order, `ceil(w / 8 hmax)` to a row, and in each MCU the scan's components and their `hi * vi` units in T.81 order, the unit, component and column counters never wrapping (`jpeg_walk_frame`), and the U32 block count the decoder runs, `decode.nblocks`, is that order's length over `ceil(h / 8 vmax)` MCU rows when the scan carries the frame's data units and the count fits a U32 (`jpeg_walk_count`); the `hi * vi` units of any scan component sit in T.81 A.2.3's grid, `hi` to a row, each sample covering `hmax / hi` by `vmax / vi` pixels (`jpeg_mcu_grid`, `jpeg_mcu_grid_comp`); painting a block writes sample `k` over exactly the `pw` by `ph` pixels at `(ox + (k mod 8) * pw, oy + (k div 8) * ph)` inside the frame, for every sample size, 4 by 4 included, and onto every plane, one earlier blocks painted included (`jpeg_block_cover`, `jpeg_block_cover_all`); the decoder reads a plane out point by point, sample `k` being the value `Array.get` finds at index `k` (`jpeg_points_at`). Colour: sample `k` of the colour pass is `Jpeg.rgb` of point `k`'s Y, Cb and Cr (`jpeg_rgbs_at`) | that `Array.get` at an index finds the value the last `Array.set` at that index wrote, and a set at another index leaves it (the planes are perfect binary trees of `2^d` leaves, and the lemmas must follow the masked index down the tree), which joins the painting laws to `jpeg_points_at`. The row is worded for frames of at most 2^31 points: above that `decode.plane`'s depth, taken from `U32.shl(nn)`, wraps and points alias | | IMG-JPG-3 | Alpha 255 holds for every sample `decode_jpeg` returns (`jpeg_decode_opaque`, IMG-PIX-1), and `encode_jpeg`'s bytes have the layout IMG-JPG-5 proves. The encoder's entropy-coded bytes have every 255 followed by a 0, for every size and samples (`jpeg_enc_stuffed`), and the decoder's bit reader, reading eight bits at a time from the encoder's stuffing of any bytes, reads the bytes back with the stuffed zeros dropped (`jpeg_unstuff`); the decoder's marker walk over the encoder's header reaches the entropy-coded data with the frame carrying the encoder's width and height, its scan and its tables, a baseline frame read and nothing refused (`jpeg_enc_header_walk`); inside the data the walk keeps every byte of stuffed data and stops at EOI (`jpeg_ent_walk`); so for every well-formed raster with both sides from 1 to 65535, `decode_jpeg(encode_jpeg(r))` is the decoder's scan decode, `decode.run`, of the encoder's own entropy-coded bytes in the frame of `r`'s width and height (`jpeg_round_trip_scan`); that scan decode is none or a picture of its frame's width and height, whatever the bytes (`jpeg_run_sized`); so `decode_jpeg(encode_jpeg(r))` is none or a raster of `r`'s size (`jpeg_round_trip_sized`) | that `decode.run` on the encoder's entropy-coded bytes is not none: that every Huffman lookup finds its symbol and every block ends by 64 coefficients, which is the bit writer (`encode.bits`, `encode.pack`, the pad with 1 bits: that the bytes it writes carry the codes' bits in order) against the bit reader reading codes of 1 to 16 bits across byte boundaries (the byte-aligned case is `jpeg_unstuff`), the Annex K tables `encode.huff` builds against the ones `decode.canon` builds and `decode.look` searches, and the encoder's three paths (neutral, solid, `encode.go`) each writing `ceil(w / 8) * ceil(h / 8)` MCUs of three blocks, each a DC code and magnitude, AC run and size codes and magnitudes, and EOB | | IMG-PIX-1 | The JPEG side. `Jpeg.rgb` and `Jpeg.gray` give alpha 255 for every input (`jpeg_rgb_opaque`, `jpeg_gray_opaque`); every sample `decode_jpeg` returns is packed by `Jpeg.gray`, or every one by `Jpeg.rgb` (`jpeg_decode_packed`); every sample it returns has alpha 255 (`jpeg_decode_opaque`); a gray sample carries its level's low byte in R, G and B (`jpeg_gray_level`) | that every sample `decode_png` returns is `0xAARRGGBB`: `png_walk` (IMG-PNG-9) reaches `decode_png` for files in the standard chunk order, not yet for files with ancillary chunks. `jpeg_decode_packed` does not say that the gray packing is the one chosen for a one-component frame | | IMG-PNG-2 | the one-block encoding: every raster `png_ok` accepts (both sides nonzero, `w * h` samples, `w * h` below 2^32) whose scanlines, `h * (1 + w * c)` bytes for c channels (3 when every sample is opaque, 4 otherwise), are at most 65535 decodes from its PNG to itself (`png_roundtrip_one`), through `png_walk`, `inflate_enc_zlib`, `unfilter_filter` with filter None, and `png_px_rgb` / `png_px_rgba` | the two wide paths `encode_png` takes past 65535 scanline bytes: `enc.seal.wide` (colour type 6, `enc.pour`) and `enc.wide.rgb` (colour type 2, `enc.rgb.go`) must be shown to write `zlib.stored(65535, raw)` with the IDAT CRC. And the row is false as worded, even with the approved bound of fewer than 2^32 samples: the scanline count `enc.nbytes` and the IDAT length are U32s, so a raster of 2^32 scanline bytes or more encodes to a file that does not decode (a decision for the maintainer) | @@ -89,7 +89,7 @@ What a sample means, for every decoder and encoder. Every Proved row but IMG-JPG-1, IMG-JPG-4, IMG-JPG-5, IMG-PIX-2, IMG-RAS-1, IMG-RAS-2, IMG-RAS-3, IMG-RAS-4, IMG-RAS-5, IMG-PNG-1, IMG-PNG-3, IMG-PNG-4, IMG-PNG-5, IMG-PNG-6, IMG-PNG-7 and IMG-PNG-8 is pending; IMG-PIX-1, IMG-PNG-2, IMG-PNG-9, IMG-JPG-2 and IMG-JPG-3 have the partial laws above. The rollout in [docs/rfc/ezimg-spec.md](docs/rfc/ezimg-spec.md) orders them: the behavior changes first (IMG-PIX-1 needed BC-1, which has landed; IMG-JPG-2 needed BC-2 and IMG-JPG-4 needed BC-3, which have landed), then refusals and frames (IMG-PNG-3, IMG-PNG-8, IMG-JPG-1, IMG-RAS-1, IMG-RAS-2), then content (IMG-PNG-5, IMG-PNG-7, IMG-PNG-6, IMG-PNG-9, IMG-PNG-4, IMG-RAS-3, IMG-RAS-4, and the headline IMG-PNG-2), and the JPEG content rows last (IMG-PIX-1, IMG-JPG-5, IMG-JPG-2, IMG-JPG-6, IMG-JPG-3). -IMG-PNG-2 is false as worded for rasters of 2^32 scanline bytes or more, which fewer than 2^32 samples do not rule out, and IMG-JPG-2 for frames of more than 2^31 points (both above); no other row is known to be false. IMG-JPG-2 covers every sampling layout the frame parser accepts, which BC-2 made decode correctly (REVIEW-13). +IMG-PNG-2 is false as worded for rasters of 2^32 scanline bytes or more, which fewer than 2^32 samples do not rule out (above); no other row is known to be false. IMG-JPG-2 covers every sampling layout the frame parser accepts, which BC-2 made decode correctly (REVIEW-13). ## Trust boundary