feat: prove the JPEG frame walk, block painting and round trip up to the scan decode

[ngngardner]

Summary

Both rows stay pending.

IMG-JPG-2: eight new direct laws

• jpeg_block_cover_all: painting a block covers the right pixels for every factor pair, 4×4 included, on any plane.
  • Its proof is structural, so it no longer normalises 1024 writes.
• jpeg_mcu_grid_comp: the A.2.3 grid holds for any scan component.
• jpeg_refuse_factor1_any, jpeg_refuse_factor3_any and jpeg_refuse_count: bad factors are refused after fill bytes too, a length field longer than the components doesn't hide them, and component counts other than 1 or 3 are refused.
• jpeg_points_at: the plane read-out returns point k at index k.
• jpeg_walk_frame: decode.adv visits every MCU in raster order, and each component's units in T.81 order, with no counter wrapping.
• jpeg_walk_count: the block count equals the length of that walk.
• Still missing: Array.get-after-Array.set lemmas that join the painting laws to the read-out.
• The row is false as worded for frames above 2^31 points: decode.plane's depth uses a shift that wraps, so points alias. The wording is a decision for the maintainer.

IMG-JPG-3: seven new direct laws

• jpeg_enc_stuffed and jpeg_unstuff: the encoder's byte stuffing and the decoder's unstuffing are inverses.
• jpeg_enc_header_walk: the marker walk over the encoder's header reaches the entropy-coded data with the right frame.
• jpeg_ent_walk: the walk keeps stuffed data whole and stops at EOI.
• jpeg_round_trip_scan: decode_jpeg(encode_jpeg(r)) equals decode.run of the encoder's bytes, in r's frame.
• jpeg_run_sized and jpeg_round_trip_sized: the result is none or a raster of r's size.
• Still missing: the Huffman round trip, meaning decode.run on those bytes is not none.

Code changes (byte-identical)

• decode.splat paints by rows, columns and pixels. The Cursor type is removed.
• decode.emit reads the points in order, as decode.points.
• Byte tests use U32.is_eq.
• The encoder stores bytes raw and stuffs them once, at the flush.
• The block count is named decode.nblocks.
• Proof-only edits outside the block: WP7's uses of decode.emit now call decode.points, and WP8's jpeg_block_cover gets the structural proof. No law statement changed.

Checks

• bend PROOF.bend prints All terms check.
  • Gate time is about the same as main's; the faster block-cover proof offsets the new laws.
• bolt v1.7.0 reports 0 errors. CI runs v1.8.0.
• Pillow: 0 hard failures in 40 cases.
• Probes: 224 of 224 identical against a driver rebuilt from main.
  • A further 48 crafted JPEGs also decode identically: fill bytes in the scan, markers mid-scan, truncation, and a trailing 255.
• 14 planted mutations were each caught by their target law.

🤖 Generated with Claude Code

https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP

---

Generated by Claude Code