feat: prove IMG-JPG-2, the JPEG planes from Array.set to decode_jpeg's pixels

[ngngardner]

Summary

IMG-JPG-2 is now proved as worded, under the 2^31-point bound from #66. Its "Left to prove" row is removed.

Seven new direct laws:

• jpeg_get_set: Array.get at an index finds what the last Array.set there wrote.
• jpeg_get_set_other: a set at another index leaves the value alone, on the decoder's perfect-tree planes of 2^d leaves (d < 32).
• jpeg_plane_depth: for 1 to 2^31 points, the plane's depth is below 32 and has enough leaves. This covers the U32 shl wrap at exactly 2^31.
• jpeg_paint_at: after painting a block, pixel (x, y) holds the sample whose pw×ph area covers it.
• jpeg_blocks_paint: decode.blocks paints the k-th decoded unit at the k-th place of the walk, on its component's plane.
• jpeg_plane_at: reading a plane after those units at (x, y) gives jpg.point.
• jpeg_place: the row's placement clause as a law over decode_jpeg. Every returned pixel is gray of Y, or rgb of Y/Cb/Cr, taken from the placed units.

Together with jpeg_walk_frame (A.2.3 order), jpeg_mcu_grid_comp and the refusal laws, these cover the row. Where two samples could cover one pixel, the laws say the later one shows. The A.2.3 grid tiles the frame, so this doesn't arise, but the tiling arithmetic itself isn't a separate law.

Code: decode.depth tests for zero with U32.is_eq through a new helper, decode.depth.of. It returns the same value for every input.

Checks

• bend PROOF.bend prints All terms check.
  • Proof check takes about the same time as main: 257 s against 265 s.
• bolt v1.7.0 reports 0 errors. CI runs v1.8.0.
• Pillow: 0 hard failures of 40 cases.
• Probes: 224 identical, 0 differing, against a driver rebuilt from main.
• Each of these mutations fails a new law:
  • a pixel written one place to the right
  • the wrong depth
  • Cb painted with component 2's units
  • another component's block painted too
  • Cb and Cr swapped
• Array.set is compiled into the Bend binary and can't be mutated, so the two get/set laws were each checked against concrete wrong-write instances instead.

🤖 Generated with Claude Code

https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP

---

Generated by Claude Code