feat: prove the JPEG round trip (IMG-JPG-3)

LAWS.bend

@@ -3378,3 +3378,46 @@ law jpeg_scan_some:
     Nat}
   {jpg.psome(Jpeg.decode.run(jpg.enc.frame(ww, hh), jpg.enc.scan(), jpg.enc.tabs(), Jenc.encode.pad(jpg.feed(
     jpg.tbits(tt <> rest), Jenc.encode.put0())), 0)) == True{} : Bool}
+
+# ---- wp14-jpeg-encoder ----
+
+# LAW: for every well-formed raster with both sides from 1 to 65535, decode_jpeg of encode_jpeg's bytes is some
+# raster. Every path of encode.arm (neutral, solid, encode.go) writes, through the encoder's bit writer, three blocks
+# per MCU that the decoder reads whole (each DC clipped to T.81's 8-bit range, so its difference has at most 11
+# bits), and the MCU count times 3 is decode.nblocks of the encoder's frame with no U32 wrap, so jpeg_scan_some
+# applies. With jpeg_round_trip_sized (a raster of r's size) and jpeg_decode_opaque (alpha 255) this is IMG-JPG-3
+# IMG-JPG-3
+law jpeg_round_trip_some:
+  for +ww: U32
+  for +hh: U32
+  for +px: List<&2, U32>
+  for +h_good: {Png.enc.good(ww, hh, px) == True{} : Bool}
+  for +h_w: {U32.is_le(ww, 65535) == True{} : Bool}
+  for +h_h: {U32.is_le(hh, 65535) == True{} : Bool}
+  {Maybe.is_some(&2, Img.Raster, jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px}))) == True{} : Bool}
+
+# a decode's samples, when it returned a raster, all have alpha 255
+def jpg.opq(mm: Maybe<&2, Img.Raster>) -> Bool:
+  match mm:
+    case None{}:
+      True{}
+    case Some{img}:
+      all.opaque(Img.pixels(img), True{})
+
+# a decode that is some raster of width w and height h, every sample of it with alpha 255
+def jpg.round(+mm: Maybe<&2, Img.Raster>, +ww: U32, +hh: U32) -> Bool:
+  Bool.and(Bool.and(Maybe.is_some(&2, Img.Raster, mm), jpg.sized(mm, ww, hh)), jpg.opq(mm))
+
+# LAW: for every well-formed raster r with both sides from 1 to 65535, decode_jpeg(encode_jpeg(r)) is some raster
+# of r's width and height, every sample of it with alpha 255: jpeg_round_trip_some, jpeg_round_trip_sized and
+# jpeg_decode_opaque together. It needs no bound on the samples: sides of at most 65535 keep the MCU count's
+# product, times 3, below 2^32
+# IMG-JPG-3
+law jpeg_round_trip:
+  for +ww: U32
+  for +hh: U32
+  for +px: List<&2, U32>
+  for +h_good: {Png.enc.good(ww, hh, px) == True{} : Bool}
+  for +h_w: {U32.is_le(ww, 65535) == True{} : Bool}
+  for +h_h: {U32.is_le(hh, 65535) == True{} : Bool}
+  {jpg.round(jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px})), ww, hh) == True{} : Bool}

PROOF.bend

@@ -22,6 +22,7 @@ import ./proof/wp10-jpeg-finish.bend as W10
 import ./proof/wp13-jpeg-planes.bend as W13
 import ./proof/wp11-png-finish.bend as W11
 import ./proof/wp12-jpeg-huffman.bend as W12
+import ./proof/wp14-jpeg-encoder.bend as W14
 
 # U32.or with 0xFF000000 first has alpha 255, whatever the other operand:
 # the 32 bits are taken apart four at a time, and Bool.or(True, b) is True.
@@ -6405,3 +6406,13 @@ def Laws.jpeg_huff_ac(pre, h_pre, sy, h_sy, post, h_post):
 
 def Laws.jpeg_scan_some(tt, rest, ww, hh, h_w, h_h, h_wf, h_n):
   W12.scan_some(tt, rest, ww, hh, h_w, h_h, h_wf, h_n)
+
+# ---- wp14-jpeg-encoder ----
+
+def Laws.jpeg_round_trip_some(ww, hh, px, h_good, h_w, h_h):
+  W14.some_ok(ww, hh, px, h_good, h_w, h_h, Laws.jpeg_round_trip_scan(ww, hh, px, h_good, h_w, h_h))
+
+def Laws.jpeg_round_trip(ww, hh, px, h_good, h_w, h_h):
+  W14.round_ok(Laws.jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px})), ww, hh, Laws.jpeg_round_trip_some(ww, hh, px,
+    h_good, h_w, h_h), Laws.jpeg_round_trip_sized(ww, hh, px, h_good, h_w, h_h), W14.opq_back(Img.encode_jpeg(
+    Img.Raster{ww, hh, px}), bb => ii => ee => Laws.jpeg_decode_opaque(bb, ii, ee)))

SPEC.md

@@ -70,7 +70,7 @@ What a sample means, for every decoder and encoder.
 | :---- | :---- | :---- | :---- | :---- |
 | 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 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 | proved | 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; LAWS.bend jpeg_get_set; LAWS.bend jpeg_get_set_other; LAWS.bend jpeg_paint_at; LAWS.bend jpeg_plane_depth; LAWS.bend jpeg_blocks_paint; LAWS.bend jpeg_plane_at; LAWS.bend jpeg_place |
-| 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; LAWS.bend jpeg_bits_round_trip; LAWS.bend jpeg_huff_dc; LAWS.bend jpeg_huff_ac; LAWS.bend jpeg_scan_some |
+| 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 | proved | 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; LAWS.bend jpeg_bits_round_trip; LAWS.bend jpeg_huff_dc; LAWS.bend jpeg_huff_ac; LAWS.bend jpeg_scan_some; LAWS.bend jpeg_round_trip_some; LAWS.bend jpeg_round_trip |
 | 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 | | |
@@ -79,11 +79,9 @@ What a sample means, for every decoder and encoder.
 
 ## Left to prove
 
-| ID | Proved so far | Missing |
-| :---- | :---- | :---- |
-| 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`). The encoder's bit writer (`encode.bits`, then the pad with 1 bits) writes any codes of 1 to 16 bits so that the decoder's bit reader reads them back in order across byte boundaries (`jpeg_bits_round_trip`); every symbol's code in the encoder's Annex K books (`encode.huff`), written between any codes, is decoded by the decoder's lookup (`decode.huff` over the table `decode.canon` builds) to that symbol, the reader left just after it (`jpeg_huff_dc`, `jpeg_huff_ac`); and `decode.run`, in the encoder's frame, scan and tables, returns a picture for any bits the encoder's writer (`encode.bit`, `encode.pad`) writes that are as many blocks as the frame has (`decode.nblocks`), each one the decoder reads whole: a DC code of the table with as many magnitude bits as its size, then AC codes of the table (EOB, ZRL with room for 16 zeros, or a run and nonzero size inside the block, with its magnitude bits) that end the block with EOB or at its 64th coefficient (`jpeg_scan_some`) | that `encode.arm`'s entropy-coded bytes are such bits: that the encoder's three paths (neutral, solid, `encode.go`) each write, through `encode.bits`, `encode.pack` and the pad, `ceil(w / 8) * ceil(h / 8)` MCUs of three blocks, each a DC code and magnitude and AC run and size codes and magnitudes of the tables ending with EOB or at 64 coefficients (DC differences below 2048 and AC coefficients below 1024 in magnitude, runs of at most 15 after ZRLs); and that for at most 2^31 samples this count, times 3, is `decode.nblocks` of the frame with no U32 wrap |
+No Proved row is left to prove.
 
-Every Proved row but IMG-JPG-1, IMG-JPG-2, IMG-JPG-4, IMG-JPG-5, IMG-PIX-1, IMG-PIX-2, IMG-RAS-1, IMG-RAS-2, IMG-RAS-3, IMG-RAS-4, IMG-RAS-5, IMG-PNG-1, IMG-PNG-2, IMG-PNG-3, IMG-PNG-4, IMG-PNG-5, IMG-PNG-6, IMG-PNG-7, IMG-PNG-8 and IMG-PNG-9 is pending; IMG-JPG-3 has 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).
+Every Proved row is proved; none is pending. The rollout in [docs/rfc/ezimg-spec.md](docs/rfc/ezimg-spec.md) ordered 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).
 
 No 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).
 

docs/rfc/ezimg-law-inventory.md

@@ -333,4 +333,5 @@ requirement depends on.
 | WP13, JPEG planes (IMG-JPG-2) | done; IMG-JPG-2 proved | `jpeg_get_set` (`Array.get` at an index finds what the last `Array.set` there wrote, in any array) and `jpeg_get_set_other` (on a perfect binary tree of 2^d leaves, d below 32, a set at one index below 2^d leaves what `Array.get` finds at another): the lemmas mirror an array as a data tree (`W13.Tr`, so a proof can use it twice), follow the index as `Array.swap.go` and `Array.get.go` walk it, and show the mask `i & (2^d - 1)` is `i` below 2^d (`mask_w`, the size of a perfect tree being the word of bit d, `size_bits`). `jpeg_plane_depth`: for 1 to 2^d points, d at most 31, `decode.depth` is below 32 and its 2^depth leaves are at least the points, the U32 shl wrap at exactly 2^31 points included (a bound on U32.log2 from below and above, `le1`, `le2`). `jpeg_paint_at`: painting a block onto such a plane leaves at pixel (x, y), point y * w + x, the sample whose pw by ph pixels take it in, the last in the block's order, else the old value (`jpg.block.at`). `jpeg_blocks_paint`: `decode.blocks` paints the k-th unit it decodes at `decode.geom` of the k-th place of its walk (`jpg.trace`) onto its component's plane. `jpeg_plane_at`: a plane after those units, read at (x, y), is `jpg.point`. `jpeg_place` composes them over `decode_jpeg`: for a frame of at most 2^31 points, pixel (x, y) of any raster it returns is gray of Y, or rgb of Y, Cb and Cr, each `jpg.point` over the decoded units from a zero plane; with `jpeg_walk_frame` (the walk is T.81 A.2.3's order), `jpeg_mcu_grid_comp` (each unit's A.2.3 grid place and sample size) and `jpeg_paint_at` (replication) that is the row. Where samples of different units would cover one pixel the later one shows; A.2.3's grid tiles the frame so none do, and that tiling arithmetic is not itself a law. Code, byte-identical on every probe: `decode.depth` tests zero with `U32.is_eq` instead of a literal pattern (`decode.depth.of`). Big Nat constants never appear in a checked type: the checker normalises `Nat.pow(2n, 32n)` even against itself, so the bound is `w * h <= 2^d, d <= 31`. Mutants: a pixel written one point on, the depth from nn - 1, Cb painted with component 2's units, a block of another component painted too, Cb and Cr swapped in the colour pass: each fails its law's proof; an `Array.set` one index on fails `jpeg_get_set` and one that also writes the next index fails `jpeg_get_set_other` on a concrete plane. Gate about 4 m 17 s, main's 4 m 25 s |
 | WP12, JPEG Huffman and scan (IMG-JPG-3) | done, partial; the encoder-side token structure is left | `jpeg_bits_round_trip`: codes of 1 to 16 bits written by `encode.bits` and padded by `encode.pad` are read back in order by `decode.read.n` across byte boundaries and stuffed bytes (a model writer and reader over byte-sized bit lists, `proof/wp12-jpeg-huffman.bend`). `jpeg_huff_dc`, `jpeg_huff_ac`: every Annex K symbol's code in `encode.huff`'s book, written between any codes, is decoded by `decode.huff` over `decode.canon`'s table to that symbol, the reader just after it (closed per-symbol checks over literal copies of the books and tables, grouped by code length so `decode.look` stays cheap). `jpeg_scan_some`: `decode.run`, in the encoder's frame, scan and tables, returns a picture for any bits `encode.bit` and `encode.pad` write that are as many well-formed blocks (DC code and magnitude, AC tokens ending with EOB or at the 64th coefficient) as `decode.nblocks` of the frame. Code: `decode.ac.sym` tests EOB and ZRL with `U32.is_eq` in a helper instead of literal patterns and `decode.ac.run` masks with the constant first, so the laws reduce on a symbolic symbol; `encode.pad.n` puts the constant first; outputs byte-identical on every probe. Left: that `encode.arm`'s bytes are such blocks (the neutral, solid and `encode.go` paths' token structure, with DC differences and AC coefficients in range) and that 3 * ceil(w / 8) * ceil(h / 8) equals `decode.nblocks` without wrap for at most 2^31 samples |
 | WP11, PNG round trip past one block and ancillary chunks (IMG-PNG-2, IMG-PNG-9, IMG-PIX-1) | done; IMG-PNG-2 proved after rewording, IMG-PNG-9 and IMG-PIX-1 proved | IMG-PNG-2 reworded to rasters of fewer than 2^29 samples (the bound is a U32 witness `a8` whose value is `8 w h`), and `png_roundtrip` proves it: below 65536 scanline bytes through `png_roundtrip_one`, above it through the two wide paths. Colour type 6 (`enc.seal.wide`, `enc.pour`): `pour.bs` and the `sim` simulation against `enc.feed` give `zlib.stored(65535, raw)` with the IDAT CRC (`wide.tail`); colour type 2 (`enc.wide.rgb`, `enc.rgb.go`): the `rg` simulation with fuel `n + 2k + 1` bytes, `afold.adler` (the running Adler sums are `Inf.adler.of`) and `rgb.tail` give the same chunk. The block count `enc.nblk` is ceil(n / 65535) by U32 div and mod (`nb.k`), the IDAT length `n + 5k + 6` does not wrap (`idat.len`, `tu.ok`: `n <= 5 w h` and `n + 5k + 6 <= 8 w h`), and `rt.tail`, the one-block proof's pixel stage, now shared by both paths. IMG-PNG-9 and the PNG side of IMG-PIX-1: `png_walk_anc` extends `png_walk` to ancillary chunks after IHDR, between PLTE and tRNS, after them and after the IDAT chunks (`anc.walk`: the walker skips each, closing the IDAT run), and to tRNS before PLTE, the one other order the decoder takes (colour type 2); with trailing bytes, a second IHDR, PLTE or tRNS, a critical unknown chunk or an IDAT after the run refused, these are every file `decode_png` accepts. No code change. Lemmas in `proof/wp11-png-finish.bend`; the IHDR's CRC over a symbolic width and height is slow to normalise, so the wide proofs state the layout stuck on flags (`core.f`, `core.t`, `wide.rt`) and unfold it once. Mutants: a stored block's NLEN high byte from LEN in `enc.pour`, colour type 2's Adler B sum missing a byte in `enc.rgb.go`, `enc.nblk` adding 2 for a partial block, the ancillary bit read as bit 4, and PLTE refused after tRNS: each fails its lemma (`pour.bs`, `rg`, `nb.at`, `anc.step`, `plte.late`). No row is known to be false. Gate about 6 m 40 s, main's 4 m 30 s (the W11 lemmas check in about 2 m 30 s, the W9 import included) |
+| WP14, JPEG encoder side (IMG-JPG-3) | done; IMG-JPG-3 proved | `jpeg_round_trip_some`: for every well-formed raster with both sides from 1 to 65535, `decode_jpeg(encode_jpeg(r))` is some raster. Each path of `encode.arm` (neutral, solid, `encode.go`) writes, through `encode.bits`, `encode.pack` and the pad, `ceil(w / 8) * ceil(h / 8)` MCUs of three blocks the decoder reads whole (DC code and magnitude, then AC run and size codes ending with EOB or at the 64th coefficient). That MCU count times 3 is `decode.nblocks` of the encoder's frame, with no U32 wrap, because each side's MCU count fits 14 bits (`count_ok`, a `Fits` witness keeps big numbers out of types). With `jpeg_scan_some` this gives the result. `jpeg_round_trip` joins it with `jpeg_round_trip_sized` and `jpeg_decode_opaque`: some raster of `r`'s width and height with alpha 255, which is the row as worded. The law needs no samples bound, because sides of at most 65535 already keep `mw * mh * 3` below 2^32; it is stronger than the row's 2^31 samples. The DC clip (option C): `encode.dcbias` clips each block's DC to -1024 to 1023 before prediction and keeps it biased by 1024 (0 to 2047, predictor starting at 1024), and a negative difference is written by its magnitude (`encode.dc.neg`), so every difference is below 2048 and has at most 11 bits. Output stays byte-identical: the bias cancels in the difference, and the clip never triggers. By hand, the forward DCT's DC is `sign(x) * floor((46341 |x| + 65536) / 2^17)` per pass, so a row pass over samples of -128 to 127 lies in -362 to 359, and the column pass gives -1024 to 1015, inside the clip. Probes stayed at 224 identical. Also landed from the saved encoder-side patch: the refactors `encode.cat.pick`, `encode.clip.b`, `encode.ac` with `ac.run`/`ac.at`, the nibble-masked `ac.step`, and `pack.byte`/`span`. W10's `st.disp` follows the initial predictors 1024. Mutants, each caught: the positive clip removed (`bias.b`), EOB dropped from `encode.ac` (`acl`), the negative clip widened to 1025 (`bias.b`), and one MCU too many on the solid path (W10 `st.disp`). Gate 451 s before, 545 s after. |
 | Phase 4b, cheap rows | next | IMG-PNG-3, IMG-PNG-8, IMG-JPG-1, IMG-RAS-1, IMG-RAS-2; these need ordering and product lemmas on U32 (`is_lt`, `is_le`, `*` without wrap) next to `ueq` |