feat: prove the JPEG bit writer, Huffman codes and scan decode for IMG-JPG-3 - #68
Merged
ngngardner merged 11 commits intoSep 26, 2026
Merged
Conversation
…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
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
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
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
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
…lace-setup-hlbfz7-wp12-jpeg-huffman
…lace-setup-hlbfz7-wp12-jpeg-huffman
…' 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
…ks the encoder's writer writes Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
…lace-setup-hlbfz7-wp12-jpeg-huffman Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
…pying Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
ngngardner
deleted the
claude/skills-marketplace-setup-hlbfz7-wp12-jpeg-huffman
branch
September 26, 2026 03:20
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
IMG-JPG-3 stays pending. This PR proves the decoder side of the Huffman round trip.
jpeg_bits_round_trip: codes of 1 to 16 bits written byencode.bitsand padded and stuffed byencode.padare read back in order by the decoder's bit reader, across byte boundaries.jpeg_huff_dcandjpeg_huff_ac: each Annex K symbol's code from the encoder's book decodes to that symbol throughdecode.huffoverdecode.canon's table, at any bit offset and between any codes.jpeg_scan_some: in the encoder's frame, scan and tables,decode.runreturns a picture for any well-formed block stream the encoder's writer writes. Well-formed means:decode.nblocksblocks;Still to prove, now in SPEC's "Left to prove" row:
encode.arm's bytes are such a block stream: the token structure of the encoder's three paths, and the ranges of the DC differences and AC coefficients;decode.nblocks.Those two facts plus feat: prove the JPEG frame walk, block painting and round trip up to the scan decode #65's
jpeg_round_trip_scanandjpeg_round_trip_sizedclose the row.Code changes, byte-identical:
encode.pad.nputs the constant first in its U32 or.decode.ac.symtests EOB and ZRL withU32.is_eq, through the helperdecode.ac.sym.b.decode.ac.runmasks with the constant first.Checks
bend PROOF.bendprintsAll terms check.It takes about 330 s on my machine, against 264 s on main.🤖 Generated with Claude Code
https://claude.ai/code/session_01A1bVZYFbhKkn2BKHKthcVP
Generated by Claude Code