Skip to content

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

Merged
ngngardner merged 18 commits into
mainfrom
claude/skills-marketplace-setup-hlbfz7
Sep 26, 2026
Merged

feat: prove the JPEG round trip (IMG-JPG-3)#70
ngngardner merged 18 commits into
mainfrom
claude/skills-marketplace-setup-hlbfz7

Conversation

@ngngardner

@ngngardner ngngardner commented Sep 26, 2026

Copy link
Copy Markdown
Contributor

Summary

IMG-JPG-3 is now proved. For every well-formed raster r with both sides from 1 to 65535, decode_jpeg(encode_jpeg(r)) is some raster of r's size with alpha 255. With this, every row in SPEC.md is proved or Trusted.

Laws

The new laws are in proof/wp14-jpeg-encoder.bend.

  • jpeg_round_trip_some: all three paths of encode.arm (neutral, solid, encode.go) write MCUs that jpeg_scan_some accepts.
    • Each MCU holds 3 blocks.
    • The MCU count times 3 equals decode.nblocks with no U32 wrap, because each side's MCU count fits in 14 bits.
  • jpeg_round_trip: combines that law with jpeg_round_trip_sized and jpeg_decode_opaque.
  • The law needs no samples bound. Sides of at most 65535 are enough, so it is stronger than the row's wording, which is unchanged.

Source changes (output is byte-identical)

  • DC clip (decision D13, option C): each block's DC is clipped to −1024..1023 before prediction and kept biased by 1024. A DC difference then has at most 11 bits.
    • The forward DCT's DC always lies in −1024..1015, so the clip never triggers.
    • The bias cancels in the difference.
  • Refactors so the laws reduce:
    • encode.cat.pick
    • encode.clip.b
    • encode.ac with ac.run/ac.at
    • the nibble-masked ac.step
    • pack.byte/span
  • W10's dispatch proof: it now uses the biased initial predictors.

Verification

  • bend PROOF.bend prints "All terms check."
  • bolt reports 0 errors.
  • Pillow interop: 0 hard failures in 40 cases.
  • Probe outputs against main's driver: 224 identical, 0 differing.
  • Four planted mutants were each caught by the gate: DC clip removed, EOB dropped, negative clip widened, and one extra MCU on the solid path.

🤖 Generated with Claude Code

https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP

Generated by Claude Code

claude added 18 commits September 25, 2026 20:04
@claude
feat: IMG-JPG-2 block painting for every size and plane, any scan com…
895a1db 
…ponent, overlong SOF0

Painting a block is now written as the law-side cover is (decode.splat by rows, columns and
pixels), so jpeg_block_cover_all proves it for every sample size, 4 by 4 included, and every
plane, and jpeg_block_cover gets a structural proof (the gate drops from about 140 s to 89 s).
jpeg_mcu_grid_comp states the A.2.3 grid for any scan component. jpeg_refuse_factor1_any,
jpeg_refuse_factor3_any and jpeg_refuse_count refuse a SOF0 with a bad factor or count after
any prefix ending at its marker (fill bytes included) and with any length longer than its
components. decode.nbits and the entropy walk compare bytes with U32.is_eq instead of literal
patterns. Decoded output is byte-identical on every probe and on crafted fill, marker and
truncation cases.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
feat: IMG-JPG-2 plane read-out and the MCU walk over the whole frame
245baca 
decode.emit reads a plane point by point in order (decode.points), without the reversed
accumulator; the output is the same. jpeg_points_at: sample k of the points is the value
Array.get finds at index k, for every plane, through lemmas that a read hands its array back.
jpeg_walk_frame: from the scan's first block, the decoder's own decode.adv visits the frame's
MCUs in raster order, mw = ceil(w / 8 hmax) to a row, and in each MCU the scan's components and
their hi * vi data units in T.81 order, with the unit, component and column counters never
wrapping. Decoded output is byte-identical on every probe.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
Merge origin/main (WP9, the PNG round trip) into the WP10 branch
a03f61f 
LAWS.bend and PROOF.bend keep both blocks at their ends, main's wp9 block first, and PROOF.bend
imports both lemma files.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
feat: IMG-JPG-3 round trip up to the scan decode, IMG-JPG-2 block count
737d76f 
jpeg_enc_stuffed: the encoder's entropy-coded bytes have every 255 followed by a 0. The encoder
now keeps raw bytes and stuffs them once at the flush (encode.stuff.all), and dispatches on its
tag with U32.is_eq; its output is the same. jpeg_enc_header_walk: the decoder's walk over the
encoder's header reaches the data with the encoder's frame, scan and tables, for every size.
jpeg_ent_walk: the walk keeps stuffed data whole and stops at EOI. jpeg_round_trip_scan:
decode_jpeg(encode_jpeg(r)) is the scan decode of the encoder's own entropy-coded bytes in r's
frame. jpeg_run_sized and jpeg_round_trip_sized: that decode is none or a raster of r's size.
jpeg_walk_count: the decoder's U32 block count, now named decode.nblocks, is the length of
jpeg_walk_frame's order when it fits a U32. SPEC.md records what is left of IMG-JPG-2 and
IMG-JPG-3, and that IMG-JPG-2 is false for frames above 2^31 points (the plane depth wraps).
Every probe output identical, Pillow check 40 of 40.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
feat: IMG-JPG-3 stuffing and unstuffing are inverses
5bbb3be 
jpeg_unstuff: the decoder's bit reader, reading eight bits at a time from the encoder's stuffing
of any bytes (encode.stuff.all), reads the bytes back with the stuffed zeros dropped. The reader
ors each new bit in before the shifted accumulator, so a symbolic byte's bits come out as the
byte after one rewrite per bit; the value is the same. Decoded output is byte-identical on
every probe; a stuffed 255 read as 254 fails the law.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
Merge remote-tracking branch 'origin/main' into claude/skills-marketp…
2e57468 
…lace-setup-hlbfz7-wp12-jpeg-huffman
@claude
Merge remote-tracking branch 'origin/main' into claude/skills-marketp…
f043867 
…lace-setup-hlbfz7-wp12-jpeg-huffman
@claude
feat: IMG-JPG-3 bit writer against bit reader, and the Annex K tables…
0ec5e59 
…' codes decode to their symbols

jpeg_bits_round_trip: codes of up to 16 bits written by the encoder's bit writer and padded
are read back by the decoder's bit reader, at every byte offset. jpeg_huff_dc and
jpeg_huff_ac: every code the encoder's books hold decodes, through decode.huff and
decode.look over the table decode.canon builds, to its symbol at any bit offset, the
reader left just after it. encode.pad.n puts the pad mask first in its U32.or, so the
pad byte is a word of the pending bits; the bytes are the same.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
feat: IMG-JPG-3 decode.run returns a picture for any well-formed bloc…
970d603 
…ks the encoder's writer writes

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
Merge remote-tracking branch 'origin/main' into claude/skills-marketp…
ff8438a 
…lace-setup-hlbfz7-wp12-jpeg-huffman

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
fix: IMG-JPG-3 scan proof takes its alias-typed hypotheses without co…
2a00193 
…pying

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
Merge remote-tracking branch 'origin/main' into claude/skills-marketp…
c63441f 
…lace-setup-hlbfz7-wp14-jpeg-encoder

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
refactor: JPEG encoder clips each DC to -1024..1023 before prediction…
e7b05e3 
…, and states its AC, size and pack steps so laws reduce

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
refactor: JPEG encoder keeps each clipped DC biased by 1024 and write…
dc229f1 
…s a negative difference by its magnitude

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
fix: W10's dispatch proof follows the encoder's biased initial DC pre…
fa1cb88 
…dictors

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
feat: IMG-JPG-3 encoder side: every path of encode.arm writes well-fo…
8361e3b 
…rmed blocks, as many as decode.nblocks

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
style: wp14 proofs meet bolt: one parameter per line, no unused param…
896a77c 
…eters, no repeated calls

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@claude
feat: prove IMG-JPG-3, decode_jpeg(encode_jpeg(r)) is some raster of …
15c9c1a 
…r's size with alpha 255

jpeg_round_trip joins jpeg_round_trip_some, jpeg_round_trip_sized and
jpeg_decode_opaque. SPEC.md marks IMG-JPG-3 proved; the inventory
records the DC clip and why output stays byte-identical.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
@ngngardner
ngngardner merged commit fea1894 into main Sep 26, 2026
1 check passed
@ngngardner
ngngardner deleted the claude/skills-marketplace-setup-hlbfz7 branch September 26, 2026 11:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ngngardner @claude