diff --git a/LAWS.bend b/LAWS.bend index 91e33cf..c88655b 100644 --- a/LAWS.bend +++ b/LAWS.bend @@ -1928,3 +1928,553 @@ law png_roundtrip_one: for h_nb: {U32.to_nat(nb) == spec.scan.len(ww, hh, all_opaque(px)) : Nat} for h_one: {U32.is_le(nb, 65535) == True{} : Bool} {spec.png.back(Img.encode_png(Img.raster(ww, hh, px))) == Some{Img.raster(ww, hh, px)} : Maybe<&2, Img.Raster>} + + +# ---- wp10-jpeg-finish ---- + +# LAW: painting one 8 by 8 block whose samples each cover pw by ph pixels, for every pw and ph (4 by 4 +# included) and onto any plane, one that earlier blocks painted included, writes its sample k over the +# pw by ph pixels at (ox + (k mod 8) * pw, oy + (k div 8) * ph) that lie inside the frame, row by row, +# and nothing else +# IMG-JPG-2 +law jpeg_block_cover_all: + for +pw: U32 + for +ph: U32 + for +ox: U32 + for +oy: U32 + for +ww: U32 + for +hh: U32 + for +samples: List<&2, U32> + for plane: Array + {Jpeg.decode.paint.use(Jpeg.Geom{ox, oy, pw, ph, ww, hh}, True{}, samples, plane) == + jpg.cover(8n, plane, samples, 0, ox, oy, pw, ph, ww, hh) : Array} + +# LAW: a SOF0 segment of one component whose sampling factor is outside 1, 2 and 4 makes decode_jpeg +# none, whatever came before its marker (fill bytes included), however much longer than the component +# its length field makes the segment, and whatever follows +# IMG-JPG-2 +law jpeg_refuse_factor1_any: + for +pre: List<&2, U32> + for +frame: Jpeg.Frame + for +scan: Jpeg.Scan + for +tabs: Jpeg.Tabs + for +ent: List<&2, U32> + for +ri: U32 + for +kind: U32 + for +bad: U32 + for h_walk: {Jpeg.decode.walk(pre, Jpeg.decode.st0()) == Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, ri, kind, + bad} : Jpeg.St} + for +lh: U32 + for +ll: U32 + for +yh: U32 + for +yl: U32 + for +xh: U32 + for +xl: U32 + for +c1: U32 + for +f1: U32 + for +q1: U32 + for +extra: List<&2, U32> + for h_len: {U32.is_lt(Jpeg.decode.u16(lh, ll), 2) == False{} : Bool} + for h_body: {U32.to_nat((Jpeg.decode.u16(lh, ll) - 2 : U32)) == List.length(&2, U32, List.append(&2, U32, + [8, yh, yl, xh, xl, 1, c1, f1, q1], extra)) : Nat} + for h_fac: {jpg.facs(f1) == False{} : Bool} + for +rest: List<&2, U32> + {Img.decode_jpeg(List.append(&2, U32, pre, lh <> ll <> List.append(&2, U32, List.append(&2, U32, + [8, yh, yl, xh, xl, 1, c1, f1, q1], extra), rest))) == None{} : Maybe<&2, Img.Raster>} + +# LAW: a SOF0 segment of three components, one of them with a sampling factor outside 1, 2 and 4, +# makes decode_jpeg none, whatever came before its marker (fill bytes included), however much longer +# than the components its length field makes the segment, and whatever follows +# IMG-JPG-2 +law jpeg_refuse_factor3_any: + for +pre: List<&2, U32> + for +frame: Jpeg.Frame + for +scan: Jpeg.Scan + for +tabs: Jpeg.Tabs + for +ent: List<&2, U32> + for +ri: U32 + for +kind: U32 + for +bad: U32 + for h_walk: {Jpeg.decode.walk(pre, Jpeg.decode.st0()) == Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, ri, kind, + bad} : Jpeg.St} + for +lh: U32 + for +ll: U32 + for +yh: U32 + for +yl: U32 + for +xh: U32 + for +xl: U32 + for +c1: U32 + for +f1: U32 + for +q1: U32 + for +c2: U32 + for +f2: U32 + for +q2: U32 + for +c3: U32 + for +f3: U32 + for +q3: U32 + for +extra: List<&2, U32> + for h_len: {U32.is_lt(Jpeg.decode.u16(lh, ll), 2) == False{} : Bool} + for h_body: {U32.to_nat((Jpeg.decode.u16(lh, ll) - 2 : U32)) == List.length(&2, U32, List.append(&2, U32, + [8, yh, yl, xh, xl, 3, c1, f1, q1, c2, f2, q2, c3, f3, q3], extra)) : Nat} + for h_fac: {Bool.and(Bool.and(jpg.facs(f1), jpg.facs(f2)), jpg.facs(f3)) == False{} : Bool} + for +rest: List<&2, U32> + {Img.decode_jpeg(List.append(&2, U32, pre, lh <> ll <> List.append(&2, U32, List.append(&2, U32, + [8, yh, yl, xh, xl, 3, c1, f1, q1, c2, f2, q2, c3, f3, q3], extra), rest))) == None{} : Maybe<&2, Img.Raster>} + +# LAW: a SOF0 segment whose component count is neither 1 nor 3 makes decode_jpeg none, whatever its +# components and their sampling factors, whatever came before its marker and whatever follows; with the +# two laws above, a SOF0 frame with a factor outside 1, 2 and 4 is none for every component count +# IMG-JPG-2 +law jpeg_refuse_count: + for +pre: List<&2, U32> + for +frame: Jpeg.Frame + for +scan: Jpeg.Scan + for +tabs: Jpeg.Tabs + for +ent: List<&2, U32> + for +ri: U32 + for +kind: U32 + for +bad: U32 + for h_walk: {Jpeg.decode.walk(pre, Jpeg.decode.st0()) == Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, ri, kind, + bad} : Jpeg.St} + for +lh: U32 + for +ll: U32 + for +yh: U32 + for +yl: U32 + for +xh: U32 + for +xl: U32 + for +nf: U32 + for h_nf: {Bool.or(U32.is_eq(nf, 1), U32.is_eq(nf, 3)) == False{} : Bool} + for +comps: List<&2, U32> + for h_len: {U32.is_lt(Jpeg.decode.u16(lh, ll), 2) == False{} : Bool} + for h_body: {U32.to_nat((Jpeg.decode.u16(lh, ll) - 2 : U32)) == List.length(&2, U32, 8 <> yh <> yl <> xh <> xl <> + nf <> comps) : Nat} + for +rest: List<&2, U32> + {Img.decode_jpeg(List.append(&2, U32, pre, lh <> ll <> List.append(&2, U32, 8 <> yh <> yl <> xh <> xl <> nf <> comps, + rest))) == None{} : Maybe<&2, Img.Raster>} + +# the sampling factor in fs (hs or vs) of the frame component that scan component comp names: the +# first frame component whose identifier is the one the scan lists for comp (jpeg_comp_index) +def jpg.fac.of(+comp: U32, +sids: List<&2, U32>, +ids: List<&2, U32>, +fs: List<&2, U32>) -> U32: + Jpeg.decode.at(fs, Jpeg.decode.index(ids, False{}, Jpeg.decode.at(sids, comp), 0)) + +# where the decoder puts data units bi, bi + 1, ... of scan component comp of a scan that lists the +# identifiers sids, in a frame whose components have identifiers ids and factors hs and vs +def jpg.blocks.of( + left: Nat, + +bi: U32, + +comp: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +mx: U32, + +my: U32, + +hmax: U32, + +vmax: U32, + +ww: U32, + +hh: U32 +) -> List<&2, Jpeg.Geom>: + match left: + case 0n: + [] + case 1n+pp: + Jpeg.decode.geom.go(comp, bi, mx, my, ww, hh, hmax, vmax, sids, ids, hs, vs) <> + jpg.blocks.of(pp, (bi + 1 : U32), comp, sids, ids, hs, vs, mx, my, hmax, vmax, ww, hh) + +# LAW: for every scan component, not only the frame's first, whose frame component has sampling factors +# hi and vi of 1, 2 or 4, the decoder places the component's hi * vi data units of an MCU in T.81 +# A.2.3's order, hi to a row, each sample covering hmax / hi by vmax / vi pixels +# IMG-JPG-2 +law jpeg_mcu_grid_comp: + for +comp: U32 + for +sids: List<&2, U32> + for +ids: List<&2, U32> + for +hs: List<&2, U32> + for +vs: List<&2, U32> + for h_hi: {jpg.fac(jpg.fac.of(comp, sids, ids, hs)) == True{} : Bool} + for h_vi: {jpg.fac(jpg.fac.of(comp, sids, ids, vs)) == True{} : Bool} + for +mx: U32 + for +my: U32 + for +hmax: U32 + for +vmax: U32 + for +ww: U32 + for +hh: U32 + {jpg.blocks.of(U32.to_nat((jpg.fac.of(comp, sids, ids, hs) * jpg.fac.of(comp, sids, ids, vs) : U32)), 0, comp, sids, + ids, hs, vs, mx, my, hmax, vmax, ww, hh) == jpg.grid(U32.to_nat(jpg.fac.of(comp, sids, ids, vs)), 0, + jpg.fac.of(comp, sids, ids, hs), mx, my, hmax, vmax, U32.div(hmax, jpg.fac.of(comp, sids, ids, hs)), + U32.div(vmax, jpg.fac.of(comp, sids, ids, vs)), ww, hh) : List<&2, Jpeg.Geom>} + +# the value a read of a plane finds +def jpg.val(pp: Array & U32) -> U32: + (_aa, vv) = pp + vv + +# LAW: the decoder reads a plane out point by point: sample k of the first nn points is the value +# Array.get finds at index k, for every plane and every k below nn +# IMG-JPG-2 +law jpeg_points_at: + for +nn: Nat + for plane: Array + for +kk: U32 + for h_kk: {Nat.is_lt(U32.to_nat(kk), nn) == True{} : Bool} + {List.get(&2, U32, Jpeg.decode.points(nn, plane), U32.to_nat(kk)) == Some{jpg.val(Array.get(U32, plane, kk))} : + Maybe<&2, U32>} + +# jj advanced by one, kk times, in U32 +def jpg.idx(kk: Nat, +jj: U32) -> U32: + match kk: + case 0n: + jj + case 1n+pp: + jpg.idx(pp, (jj + 1 : U32)) + +# where a block sits in the walk: scan component, data unit, MCU column, MCU row and MCU number (the +# restart count left at 0) +def jpg.pos(ctrl: Jpeg.Ctrl) -> Jpeg.Ctrl: + match ctrl: + case Jpeg.Ctrl{comp, bi, mx, my, mcu, _rst}: + Jpeg.Ctrl{comp, bi, mx, my, mcu, 0} + +# the positions of the next left blocks the decoder walks to from ctrl, each step its own decode.adv +def jpg.trace( + left: Nat, + +ctrl: Jpeg.Ctrl, + +frame: Jpeg.Frame, + +scan: Jpeg.Scan, + +ri: U32 +) -> List<&2, Jpeg.Ctrl>: + match left: + case 0n: + [] + case 1n+pp: + jpg.pos(ctrl) <> jpg.trace(pp, Jpeg.decode.adv.ctrl(Jpeg.decode.adv(ctrl, frame, scan, ri)), frame, scan, ri) + +# T.81 A.2.3: data units bi onward of scan component comp in MCU (mx, my), number mcu +def jpg.o.units( + left: Nat, + +comp: U32, + +bi: U32, + +mx: U32, + +my: U32, + +mcu: U32 +) -> List<&2, Jpeg.Ctrl>: + match left: + case 0n: + [] + case 1n+pp: + Jpeg.Ctrl{comp, bi, mx, my, mcu, 0} <> jpg.o.units(pp, comp, (bi + 1 : U32), mx, my, mcu) + +# scan components comp onward of one MCU, each with its frame component's hi * vi data units +def jpg.o.comps( + left: Nat, + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> List<&2, Jpeg.Ctrl>: + match left: + case 0n: + [] + case 1n+pp: + List.append(&2, Jpeg.Ctrl, jpg.o.units(U32.to_nat(jpg.units(comp, sids, ids, hs, vs)), comp, 0, + mx, my, mcu), jpg.o.comps(pp, (comp + 1 : U32), mx, my, mcu, sids, ids, hs, vs)) + +# MCUs mx onward of MCU row my, left to right, numbered from mcu, each with the scan's components in order +def jpg.o.row( + left: Nat, + +mx: U32, + +my: U32, + +mcu: U32, + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> List<&2, Jpeg.Ctrl>: + match left: + case 0n: + [] + case 1n+pp: + List.append(&2, Jpeg.Ctrl, jpg.o.comps(U32.to_nat(ns), 0, mx, my, mcu, sids, ids, hs, vs), + jpg.o.row(pp, (mx + 1 : U32), my, (mcu + 1 : U32), ns, sids, ids, hs, vs)) + +# MCU rows my onward, top to bottom, mw MCUs to a row, numbered from mcu +def jpg.o.rows( + left: Nat, + +my: U32, + +mcu: U32, + +mw: U32, + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> List<&2, Jpeg.Ctrl>: + match left: + case 0n: + [] + case 1n+pp: + List.append(&2, Jpeg.Ctrl, jpg.o.row(U32.to_nat(mw), 0, my, mcu, ns, sids, ids, hs, vs), + jpg.o.rows(pp, (my + 1 : U32), jpg.idx(U32.to_nat(mw), mcu), mw, ns, sids, ids, hs, vs)) + +# ok, and every scan component from comp on, left of them, has at least one data unit +def jpg.units.ok( + left: Nat, + +comp: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + ok: Bool +) -> Bool: + match left: + case 0n: + ok + case 1n+pp: + jpg.units.ok(pp, (comp + 1 : U32), sids, ids, hs, vs, Bool.and(ok, U32.is_lt(0, jpg.units(comp, sids, ids, hs, + vs)))) + +# LAW: from the first block of a scan, the decoder's walk (its own decode.adv at every step) visits the +# frame's MCUs in raster order, mw = ceil(w / 8 hmax) to a row and any number of rows, and inside each MCU +# the scan's components in order, each component's hi * vi data units in order (T.81 A.2.1 and A.2.3). +# The U32 counters for the data unit, the component and the MCU column never wrap: each stays below the +# count it is compared with, and the MCU row and number count up in step with the order's own. +# IMG-JPG-2 +law jpeg_walk_frame: + for +ww: U32 + for +hh: U32 + for +nf: U32 + for +ids: List<&2, U32> + for +hs: List<&2, U32> + for +vs: List<&2, U32> + for +tq: List<&2, U32> + for +hmax: U32 + for +vmax: U32 + for +ns: U32 + for +sids: List<&2, U32> + for +td: List<&2, U32> + for +ta: List<&2, U32> + for +ss: U32 + for +se: U32 + for +ah: U32 + for +ri: U32 + for +rst: U32 + for +mh: U32 + for h_ns: {U32.is_lt(0, ns) == True{} : Bool} + for h_mw: {U32.is_lt(0, Jpeg.decode.ceil(ww, (hmax * 8 : U32))) == True{} : Bool} + for h_units: {jpg.units.ok(U32.to_nat(ns), 0, sids, ids, hs, vs, True{}) == True{} : Bool} + {jpg.trace(List.length(&2, Jpeg.Ctrl, jpg.o.rows(U32.to_nat(mh), 0, 0, Jpeg.decode.ceil(ww, + (hmax * 8 : U32)), ns, sids, ids, hs, vs)), Jpeg.Ctrl{0, 0, 0, 0, 0, rst}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, + hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri) == jpg.o.rows(U32.to_nat(mh), 0, 0, + Jpeg.decode.ceil(ww, (hmax * 8 : U32)), ns, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + +# a byte list in which every 255 is followed by a 0 (T.81 F.1.2.3), ff saying the byte before xs was a +# 255 and ok that every 255 so far was +def jpg.stuffed(xs: List<&2, U32>, ff: Bool, ok: Bool) -> Bool: + match xs: + case Nil{}: + Bool.and(ok, Bool.not(ff)) + case +bb <> rest: + match ff: + case True{}: + jpg.stuffed(rest, False{}, Bool.and(ok, U32.is_eq(bb, 0))) + case False{}: + jpg.stuffed(rest, U32.is_eq(bb, 255), ok) + +# LAW: the entropy-coded bytes encode_jpeg writes, for every size and every samples, have every 255 +# followed by a 0 +# IMG-JPG-3 +law jpeg_enc_stuffed: + for +ww: U32 + for +hh: U32 + for px: List<&2, U32> + {jpg.stuffed(Jenc.encode.arm(ww, hh, px), False{}, True{}) == True{} : Bool} + +# the tables the decoder holds after reading encode_jpeg's DQT and two DHT segments: quantisation table 0 +# all ones, and the Annex K luminance DC and AC tables as table 0 of each class +def jpg.enc.tabs() -> Jpeg.Tabs: + Jpeg.Tabs{List.replicate(U32, 64n, 1), [], [], [], Jpeg.decode.canon(272n, 0n, Jenc.encode.dccounts(), + Jenc.encode.dcsyms(), 0, 0, [], [], []), Jpeg.decode.huff0(), Jpeg.decode.huff0(), Jpeg.decode.huff0(), + Jpeg.decode.canon(272n, 0n, Jenc.encode.accounts(), Jenc.encode.acsyms(), 0, 0, [], [], []), Jpeg.decode.huff0(), + Jpeg.decode.huff0(), Jpeg.decode.huff0()} + +# the frame encode_jpeg's SOF0 carries: its width and height, three components 1, 2 and 3, each sampled +# 1 by 1 with quantisation table 0 +def jpg.enc.frame(+ww: U32, +hh: U32) -> Jpeg.Frame: + Jpeg.Frame{ww, hh, 3, [1, 2, 3], [1, 1, 1], [1, 1, 1], [0, 0, 0], 1, 1} + +# the scan encode_jpeg's SOS opens: components 1, 2 and 3 with Huffman tables 0, all of 0 to 63 +def jpg.enc.scan() -> Jpeg.Scan: + Jpeg.Scan{3, [1, 2, 3], [0, 0, 0], [0, 0, 0], 0, 63, 0} + +# LAW: the decoder's marker walk over encode_jpeg's header (SOI, APP0, DQT, SOF0, two DHT, SOS) reaches +# the entropy-coded data with the frame carrying the encoder's width and height, whatever they are, the +# encoder's scan and tables, no restart interval, a baseline frame read and nothing refused +# IMG-JPG-3 +law jpeg_enc_header_walk: + for +ww: U32 + for +hh: U32 + {Jpeg.decode.walk(Jenc.encode.header(ww, hh, Jenc.encode.dccounts(), Jenc.encode.dcsyms(), Jenc.encode.accounts(), + Jenc.encode.acsyms()), Jpeg.decode.st0()) == Jpeg.St{Jpeg.Ent{}, jpg.enc.frame(ww, hh), jpg.enc.scan(), + jpg.enc.tabs(), [], 0, 1, 0} : Jpeg.St} + +# LAW: inside the entropy-coded data, the decoder's walk keeps every byte of stuffed data (the stuffed +# zeros too, which the bit reader drops) and stops at EOI, holding what it held +# IMG-JPG-3 +law jpeg_ent_walk: + for xs: List<&2, U32> + for h_stuffed: {jpg.stuffed(xs, False{}, True{}) == True{} : Bool} + for +frame: Jpeg.Frame + for +scan: Jpeg.Scan + for +tabs: Jpeg.Tabs + for +ent: List<&2, U32> + for +ri: U32 + for +kind: U32 + for +bad: U32 + {Jpeg.decode.walk(List.append(&2, U32, xs, [255, 217]), Jpeg.St{Jpeg.Ent{}, frame, scan, tabs, ent, ri, kind, bad}) == + Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, xs, ent), ri, kind, bad} : Jpeg.St} + +# decode_jpeg of encode_jpeg's bytes, when it wrote some +def jpg.back(mm: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Img.Raster>: + match mm: + case None{}: + None{} + case Some{bytes}: + Img.decode_jpeg(bytes) + +# LAW: for every well-formed raster with both sides from 1 to 65535, decode_jpeg of encode_jpeg's bytes is +# the decoder's scan decode of encode_jpeg's own entropy-coded bytes, in the frame of the raster's width and +# height, with the encoder's scan and tables: the marker walk, the unstuffing and the frame size are done +# IMG-JPG-3 +law jpeg_round_trip_scan: + 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.back(Img.encode_jpeg(Img.Raster{ww, hh, px})) == Img.decode_jpeg.out(Jpeg.decode.run(jpg.enc.frame(ww, + hh), jpg.enc.scan(), jpg.enc.tabs(), Jenc.encode.arm(ww, hh, Img.colours(px)), 0)) : Maybe<&2, Img.Raster>} + +# a decoded raster, if any, has width ww and height hh +def jpg.sized(mm: Maybe<&2, Img.Raster>, +ww: U32, +hh: U32) -> Bool: + match mm: + case None{}: + True{} + case Some{Img.Raster{rw, rh, _px}}: + Bool.and(U32.is_eq(rw, ww), U32.is_eq(rh, hh)) + +# LAW: the scan decode, whatever the bytes, tables and scan, returns no picture or one of its frame's +# width and height +# IMG-JPG-3 +law jpeg_run_sized: + for +ww: U32 + for +hh: U32 + for +nf: U32 + for +ids: List<&2, U32> + for +hs: List<&2, U32> + for +vs: List<&2, U32> + for +tq: List<&2, U32> + for +hmax: U32 + for +vmax: U32 + for +scan: Jpeg.Scan + for +tabs: Jpeg.Tabs + for +ent: List<&2, U32> + for +ri: U32 + {jpg.sized(Img.decode_jpeg.out(Jpeg.decode.run(Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, scan, tabs, ent, + ri)), ww, hh) == True{} : Bool} + +# LAW: for every well-formed raster with both sides from 1 to 65535, decode_jpeg of encode_jpeg's bytes is +# none or a raster of the raster's width and height; every sample of one has alpha 255 (jpeg_decode_opaque) +# IMG-JPG-3 +law jpeg_round_trip_sized: + 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.sized(jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px})), ww, hh) == True{} : Bool} + +# the data units of the scan's components from comp on, left of them: each one's hi * vi, summed +def jpg.usum( + left: Nat, + +comp: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> Nat: + match left: + case 0n: + 0n + case 1n+pp: + Nat.add(U32.to_nat(jpg.units(comp, sids, ids, hs, vs)), jpg.usum(pp, (comp + 1 : U32), sids, ids, hs, vs)) + +# LAW: the number of blocks the decoder reads, decode.nblocks (ceil(w / 8 hmax) * ceil(h / 8 vmax) MCUs times +# the frame's data units per MCU, all in U32), is the length of jpeg_walk_frame's order over ceil(h / 8 vmax) MCU rows, +# when the scan's components carry the frame's data units and the product fits a U32 (the witness top), so +# the walk visits every MCU of the frame and no counter wraps +# IMG-JPG-2 +law jpeg_walk_count: + for +ww: U32 + for +hh: U32 + for +ids: List<&2, U32> + for +hs: List<&2, U32> + for +vs: List<&2, U32> + for +hmax: U32 + for +vmax: U32 + for +ns: U32 + for +sids: List<&2, U32> + for +top: U32 + for h_ns: {U32.is_lt(0, ns) == True{} : Bool} + for h_units: {jpg.units.ok(U32.to_nat(ns), 0, sids, ids, hs, vs, True{}) == True{} : Bool} + for h_sum: {U32.to_nat(Jpeg.decode.blocks.sum(hs, vs, 0)) == jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs) : Nat} + for h_fit: {Nat.is_le(Nat.mul(Nat.mul(U32.to_nat(Jpeg.decode.ceil(ww, (hmax * 8 : U32))), + U32.to_nat(Jpeg.decode.ceil(hh, (vmax * 8 : U32)))), jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)), + U32.to_nat(top)) == True{} : Bool} + {U32.to_nat(Jpeg.decode.nblocks(ww, hh, hs, vs, hmax, vmax)) == List.length(&2, Jpeg.Ctrl, + jpg.o.rows(U32.to_nat(Jpeg.decode.ceil(hh, (vmax * 8 : U32))), 0, 0, Jpeg.decode.ceil(ww, (hmax * 8 : U32)), ns, + sids, ids, hs, vs)) : Nat} + +# one byte as its eight bits, the lowest first +type JByte is Data: + JByte{c0: Bool, c1: Bool, c2: Bool, c3: Bool, c4: Bool, c5: Bool, c6: Bool, c7: Bool} + +# a byte's value: its eight bits over 24 zero bits +def jpg.byte(bb: JByte) -> U32: + match bb: + case JByte{c0, c1, c2, c3, c4, c5, c6, c7}: + U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}} + +# the bytes' values, in order +def jpg.bytes(bs: List<&2, JByte>) -> List<&2, U32>: + match bs: + case Nil{}: + [] + case bb <> rest: + jpg.byte(bb) <> jpg.bytes(rest) + +# the values the decoder's bit reader reads, eight bits at a time, left times: got is the reader and the +# value just read +def jpg.read8(left: Nat, got: Jpeg.Bits & U32) -> List<&2, U32>: + match left: + case 0n: + [] + case 1n+pp: + (bits, vv) = got + vv <> jpg.read8(pp, Jpeg.decode.read.n(8, bits)) + +# LAW: stuffing and unstuffing are inverses: the decoder's bit reader, reading eight bits at a time from the +# encoder's stuffing of any bytes (encode.stuff.all, which puts a 0 after every 255), reads the bytes back, +# the stuffed zeros dropped, whatever the reader's ok flag +# IMG-JPG-3 +law jpeg_unstuff: + for +bs: List<&2, JByte> + for +ok: U32 + {jpg.read8(List.length(&2, JByte, bs), Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, 0, Jenc.encode.stuff.all( + List.reverse(&2, U32, jpg.bytes(bs)), [])})) == jpg.bytes(bs) : List<&2, U32>} diff --git a/PROOF.bend b/PROOF.bend index 88ca558..70ecd66 100644 --- a/PROOF.bend +++ b/PROOF.bend @@ -18,6 +18,7 @@ import ./src/jpeg_enc.bend as Jenc import ./proof/wp8-jpeg-numeric.bend as W8 import ./proof/wp9-png-roundtrip.bend as W9 import ./src/inflate.bend as Inf +import ./proof/wp10-jpeg-finish.bend as W10 # 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. @@ -2610,9 +2611,9 @@ def nf3.pk( match three: case True{}: +nn = U32.to_nat((ww * hh : U32)) - +ey = Jpeg.decode.emit(nn, (yy, 0), 0, [], False{}) - +eb = Jpeg.decode.emit(nn, (cb, 0), 0, [], False{}) - +er = Jpeg.decode.emit(nn, (cr, 0), 0, [], False{}) + +ey = Jpeg.decode.points(nn, yy) + +eb = Jpeg.decode.points(nn, cb) + +er = Jpeg.decode.points(nn, cr) (False{}, (ey, (eb, (er, rgbs.eq(ey, eb, er))))) case False{}: none.pk() @@ -2629,7 +2630,7 @@ def nf1.pk( ) -> pk.Ty(pic.px(Jpeg.decode.done.nf1(one, nf, ww, hh, yy, cb, cr))): match one: case True{}: - +ey = Jpeg.decode.emit(U32.to_nat((ww * hh : U32)), (yy, 0), 0, [], False{}) + +ey = Jpeg.decode.points(U32.to_nat((ww * hh : U32)), yy) (True{}, (ey, ([], ([], grays.eq(ey))))) case False{}: nf3.pk(U32.is_eq(nf, 3), ww, hh, yy, cb, cr) @@ -4755,97 +4756,6 @@ def Laws.jpeg_mcu_grid(hi, vi, h_hi, h_vi, mx, my, hmax, vmax, ww, hh): w8.grid.vi(2, vi, h_vi, mx, my, hmax, vmax, ww, hh, {==}, {==}, {==}), w8.grid.vi(4, vi, h_vi, mx, my, hmax, vmax, ww, hh, {==}, {==}, {==})) -# what jpeg_block_cover says for sample sizes pw and ph -def w8.cover.eq( - +pw: U32, - +ph: U32, - +ox: U32, - +oy: U32, - +ww: U32, - +hh: U32, - +samples: List<&2, U32>, - +nn: U32 -) -> Type: - {Jpeg.decode.paint.use(Jpeg.Geom{ox, oy, pw, ph, ww, hh}, True{}, samples, Jpeg.decode.plane(nn)) == - Laws.jpg.cover(8n, Jpeg.decode.plane(nn), samples, 0, ox, oy, pw, ph, ww, hh) : Array} - -# that statement unless the sizes are both 4, where nothing is claimed: the 4 by 4 case is never -# normalised, which keeps the gate fast -def w8.cover.if( - both4: Bool, - +pw: U32, - +ph: U32, - +ox: U32, - +oy: U32, - +ww: U32, - +hh: U32, - +samples: List<&2, U32>, - +nn: U32 -) -> Type: - match both4: - case True{}: - Unit - case False{}: - w8.cover.eq(pw, ph, ox, oy, ww, hh, samples, nn) - -# the motive of the case split on pw and ph -def w8.cover.ty( - +pw: U32, - +ph: U32, - +ox: U32, - +oy: U32, - +ww: U32, - +hh: U32, - +samples: List<&2, U32>, - +nn: U32 -) -> Type: - w8.cover.if(Bool.and(U32.is_eq(pw, 4), U32.is_eq(ph, 4)), pw, ph, ox, oy, ww, hh, samples, nn) - -# for one width pw of 1, 2 or 4: every allowed height, one concrete case each -def w8.cover.ph( - +pw: U32, - +ph: U32, - +h_ph: {Laws.jpg.fac(ph) == True{} : Bool}, - +ox: U32, - +oy: U32, - +ww: U32, - +hh: U32, - +samples: List<&2, U32>, - +nn: U32, - p1: w8.cover.ty(pw, 1, ox, oy, ww, hh, samples, nn), - p2: w8.cover.ty(pw, 2, ox, oy, ww, hh, samples, nn), - p4: w8.cover.ty(pw, 4, ox, oy, ww, hh, samples, nn) -) -> w8.cover.ty(pw, ph, ox, oy, ww, hh, samples, nn): - W8.fac_elim(vv => w8.cover.ty(pw, vv, ox, oy, ww, hh, samples, nn), ph, U32.is_eq(ph, 1), {==}, h_ph, p1, p2, p4) - -# with the premise that the sizes are not both 4, the case split's answer is the statement -def w8.cover.use( - both4: Bool, - +pw: U32, - +ph: U32, - +ox: U32, - +oy: U32, - +ww: U32, - +hh: U32, - +samples: List<&2, U32>, - +nn: U32, - h_44: {both4 == False{} : Bool}, - got: w8.cover.if(both4, pw, ph, ox, oy, ww, hh, samples, nn) -) -> w8.cover.eq(pw, ph, ox, oy, ww, hh, samples, nn): - match both4: - case False{}: - got - case True{}: - Empty.absurd(w8.cover.eq(pw, ph, ox, oy, ww, hh, samples, nn), - U32L.false_true(Equal.sym(Bool, True{}, False{}, h_44))) - -def Laws.jpeg_block_cover(pw, ph, h_pw, h_ph, h_44, ox, oy, ww, hh, samples, nn): - w8.cover.use(Bool.and(U32.is_eq(pw, 4), U32.is_eq(ph, 4)), pw, ph, ox, oy, ww, hh, samples, nn, h_44, - W8.fac_elim(vv => w8.cover.ty(vv, ph, ox, oy, ww, hh, samples, nn), pw, U32.is_eq(pw, 1), {==}, h_pw, - w8.cover.ph(1, ph, h_ph, ox, oy, ww, hh, samples, nn, {==}, {==}, {==}), - w8.cover.ph(2, ph, h_ph, ox, oy, ww, hh, samples, nn, {==}, {==}, {==}), - w8.cover.ph(4, ph, h_ph, ox, oy, ww, hh, samples, nn, {==}, {==}, Unit{}))) - # no Cb sample: no colour, whatever the Y and Cr samples def w8.rgb3.nb(aa: Maybe<&2, U32>, cc: Maybe<&2, U32>) -> {None{} == Laws.jpg.rgb3(aa, None{}, cc) : Maybe<&2, U32>}: match aa: @@ -5542,3 +5452,242 @@ def Laws.png_roundtrip_one(ww, hh, px, nb, h_ok, h_nb, h_one): +z_h = not.true(Nat.is_eq(U32.to_nat(hh), 0n), U32L.and_right(nw, nh, e_sides)) +e_good = rt.good.at(Png.enc.good(ww, hh, px), ww, hh, px, Laws.png_encodes(ww, hh, px, ok)) rt.pos(ww, hh, px, nb, e_good, e_la, h_nb, h_one, Wp4.nat_pos(U32.to_nat(ww), z_w), Wp4.nat_pos(U32.to_nat(hh), z_h)) + + +# ---- wp10-jpeg-finish ---- + +def Laws.jpeg_block_cover_all(pw, ph, ox, oy, ww, hh, samples, plane): + W10.cv.all(8n, plane, samples, 0, ox, oy, pw, ph, ww, hh) + +def Laws.jpeg_block_cover(pw, ph, _h_pw, _h_ph, _h_44, ox, oy, ww, hh, samples, nn): + W10.cv.all(8n, Jpeg.decode.plane(nn), samples, 0, ox, oy, pw, ph, ww, hh) + +def Laws.jpeg_mcu_grid_comp(comp, sids, ids, hs, vs, h_hi, h_vi, mx, my, hmax, vmax, ww, hh): + +hi = Laws.jpg.fac.of(comp, sids, ids, hs) + +vi = Laws.jpg.fac.of(comp, sids, ids, vs) + Equal.trans(List<&2, Jpeg.Geom>, Laws.jpg.blocks.of(U32.to_nat((hi * vi : U32)), 0, comp, sids, ids, hs, vs, mx, my, + hmax, vmax, ww, hh), Laws.jpg.blocks(U32.to_nat((hi * vi : U32)), 0, hi, vi, mx, my, hmax, vmax, ww, hh), + Laws.jpg.grid(U32.to_nat(vi), 0, hi, mx, my, hmax, vmax, U32.div(hmax, hi), U32.div(vmax, vi), ww, hh), + W10.grid.of(U32.to_nat((hi * vi : U32)), 0, comp, sids, ids, hs, vs, mx, my, hmax, vmax, ww, hh), + Laws.jpeg_mcu_grid(hi, vi, h_hi, h_vi, mx, my, hmax, vmax, ww, hh)) + +def Laws.jpeg_refuse_factor1_any( + pre, + frame, + scan, + tabs, + ent, + ri, + kind, + bad, + h_walk, + lh, + ll, + yh, + yl, + xh, + xl, + c1, + f1, + q1, + extra, + h_len, + h_body, + h_fac, + rest +): + +body = {List.append(&2, U32, [8, yh, yl, xh, xl, 1, c1, f1, q1], extra) : List<&2, U32>} + w8.tail(pre, lh <> ll <> List.append(&2, U32, body, rest), Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, ri, + kind, bad}, rest, scan, tabs, ent, ri, kind, h_walk, + W10.sof.seg(lh, ll, body, rest, frame, scan, tabs, ent, ri, kind, bad, h_len, h_body, + Equal.cong(Bool, Jpeg.St, ok => Jpeg.decode.read.sof.c(ok, Bool.and(Jpeg.decode.nf.ok(1), U32.is_eq(bad, 0)), + U32.is_eq(Jpeg.decode.vmax([U32.shrn(f1, 4n)], 0), 0), Jpeg.decode.u16(xh, xl), Jpeg.decode.u16(yh, yl), 1, + [c1], [U32.shrn(f1, 4n)], [U32.and(f1, 15)], [q1], scan, tabs, ent, ri, kind), Laws.jpg.facs(f1), False{}, + h_fac))) + +def Laws.jpeg_refuse_factor3_any( + pre, + frame, + scan, + tabs, + ent, + ri, + kind, + bad, + h_walk, + lh, + ll, + yh, + yl, + xh, + xl, + c1, + f1, + q1, + c2, + f2, + q2, + c3, + f3, + q3, + extra, + h_len, + h_body, + h_fac, + rest +): + +body = {List.append(&2, U32, [8, yh, yl, xh, xl, 3, c1, f1, q1, c2, f2, q2, c3, f3, q3], extra) : List<&2, U32>} + w8.tail(pre, lh <> ll <> List.append(&2, U32, body, rest), Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, ri, + kind, bad}, rest, scan, tabs, ent, ri, kind, h_walk, + W10.sof.seg(lh, ll, body, rest, frame, scan, tabs, ent, ri, kind, bad, h_len, h_body, + Equal.cong(Bool, Jpeg.St, ok => Jpeg.decode.read.sof.c(ok, Bool.and(Jpeg.decode.nf.ok(3), U32.is_eq(bad, 0)), + U32.is_eq(Jpeg.decode.vmax([U32.shrn(f1, 4n), U32.shrn(f2, 4n), U32.shrn(f3, 4n)], 0), 0), + Jpeg.decode.u16(xh, xl), Jpeg.decode.u16(yh, yl), 3, [c1, c2, c3], + [U32.shrn(f1, 4n), U32.shrn(f2, 4n), U32.shrn(f3, 4n)], [U32.and(f1, 15), U32.and(f2, 15), U32.and(f3, 15)], + [q1, q2, q3], scan, tabs, ent, ri, kind), + Bool.and(Bool.and(Laws.jpg.facs(f1), Laws.jpg.facs(f2)), Laws.jpg.facs(f3)), False{}, h_fac))) + +def Laws.jpeg_refuse_count( + pre, + frame, + scan, + tabs, + ent, + ri, + kind, + bad, + h_walk, + lh, + ll, + yh, + yl, + xh, + xl, + nf, + h_nf, + comps, + h_len, + h_body, + rest +): + +body = {8 <> yh <> yl <> xh <> xl <> nf <> comps : List<&2, U32>} + w8.tail(pre, lh <> ll <> List.append(&2, U32, body, rest), Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, ri, + kind, bad}, rest, scan, tabs, ent, ri, kind, h_walk, + W10.sof.seg(lh, ll, body, rest, frame, scan, tabs, ent, ri, kind, bad, h_len, h_body, + W10.sof.cnt(Jpeg.decode.read.cs(U32.to_nat(nf), comps, [], [], [], [], True{}), Jpeg.decode.u16(xh, xl), + Jpeg.decode.u16(yh, yl), nf, scan, tabs, ent, ri, kind, bad, h_nf))) + +def Laws.jpeg_points_at(nn, plane, kk, h_kk): + ee = W10.idx.of(kk) + %ee : {List.get(&2, U32, Jpeg.decode.points(nn, plane), U32.to_nat(kk)) == + Some{Laws.jpg.val(Array.get(U32, plane, _))} : Maybe<&2, U32>} + W10.emit.at(nn, U32.to_nat(kk), plane, 0, W10.dup(plane), h_kk) + +def Laws.jpeg_walk_frame( + ww, + hh, + nf, + ids, + hs, + vs, + tq, + hmax, + vmax, + ns, + sids, + td, + ta, + ss, + se, + ah, + ri, + rst, + mh, + h_ns, + h_mw, + h_units +): + W10.walk.frame(ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, rst, mh, h_ns, h_mw, + h_units) + +def Laws.jpeg_enc_stuffed(ww, hh, px): + W10.st.use(Jenc.encode.watch(U32.to_nat((ww * hh : U32)), px), ww, hh) + +# the decoder's state after the encoder's header, with the sizes as it reads them back +def w10.hdr.st(+ww: U32, +hh: U32) -> Jpeg.St: + Jpeg.St{Jpeg.Ent{}, Jpeg.Frame{ww, hh, 3, [1, 2, 3], [1, 1, 1], [1, 1, 1], [0, 0, 0], 1, 1}, Laws.jpg.enc.scan(), + Laws.jpg.enc.tabs(), [], 0, 1, 0} + +def Laws.jpeg_enc_header_walk(ww, hh): + +wr = Jpeg.decode.u16(U32.shrn(ww, 8n), U32.and(ww, 255)) + +hr = Jpeg.decode.u16(U32.shrn(hh, 8n), U32.and(hh, 255)) + Equal.trans(Jpeg.St, Jpeg.decode.walk(Jenc.encode.header(ww, hh, Jenc.encode.dccounts(), Jenc.encode.dcsyms(), + Jenc.encode.accounts(), Jenc.encode.acsyms()), Jpeg.decode.st0()), w10.hdr.st(wr, hr), w10.hdr.st(ww, hh), {==}, + Equal.trans(Jpeg.St, w10.hdr.st(wr, hr), w10.hdr.st(ww, hr), w10.hdr.st(ww, hh), Equal.cong(U32, Jpeg.St, + xx => w10.hdr.st(xx, hr), wr, ww, W10.u16.eq(ww)), Equal.cong(U32, Jpeg.St, xx => w10.hdr.st(ww, xx), hr, hh, + W10.u16.eq(hh)))) + +def Laws.jpeg_ent_walk(xs, h_stuffed, frame, scan, tabs, ent, ri, kind, bad): + W10.ent.go(xs, False{}, frame, scan, tabs, ent, ri, kind, bad, h_stuffed) + +def Laws.jpeg_round_trip_scan(ww, hh, px, h_good, h_w, h_h): + +cp = Img.colours(px) + +ee = Jenc.encode.arm(ww, hh, cp) + +hd = Jenc.encode.header(ww, hh, Jenc.encode.dccounts(), Jenc.encode.dcsyms(), Jenc.encode.accounts(), + Jenc.encode.acsyms()) + +rr = List.append(&2, U32, ee, [255, 217]) + +fr = Laws.jpg.enc.frame(ww, hh) + +sc = Laws.jpg.enc.scan() + +tb = Laws.jpg.enc.tabs() + +ent = {Jpeg.St{Jpeg.Ent{}, fr, sc, tb, [], 0, 1, 0} : Jpeg.St} + +stop = {Jpeg.St{Jpeg.Stop{}, fr, sc, tb, List.reverse.go(&2, U32, ee, []), 0, 1, 0} : Jpeg.St} + Equal.trans(Maybe<&2, Img.Raster>, Laws.jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px})), + Laws.jpg.back(Img.encode_jpeg.pick(True{}, ww, hh, cp)), Img.decode_jpeg.out(Jpeg.decode.run(fr, sc, tb, ee, 0)), + Equal.cong(Bool, Maybe<&2, Img.Raster>, bb => Laws.jpg.back(Img.encode_jpeg.pick(bb, ww, hh, cp)), + Png.enc.good(ww, hh, px), True{}, h_good), + Equal.trans(Maybe<&2, Img.Raster>, Img.decode_jpeg(Jenc.encode.pick(Jenc.encode.bad(ww, hh), ww, hh, cp)), + Img.decode_jpeg(Jenc.encode.pick(False{}, ww, hh, cp)), Img.decode_jpeg.out(Jpeg.decode.run(fr, sc, tb, ee, 0)), + Equal.cong(Bool, Maybe<&2, Img.Raster>, bb => Img.decode_jpeg(Jenc.encode.pick(bb, ww, hh, cp)), + Jenc.encode.bad(ww, hh), False{}, W7.bad_of_good(ww, hh, px, h_good, h_w, h_h)), + Equal.trans(Maybe<&2, Img.Raster>, w8.out(Jpeg.decode.walk(List.append(&2, U32, hd, rr), Jpeg.decode.st0())), + w8.out(Jpeg.decode.walk(rr, Jpeg.decode.walk(hd, Jpeg.decode.st0()))), + Img.decode_jpeg.out(Jpeg.decode.run(fr, sc, tb, ee, 0)), Equal.cong(Jpeg.St, Maybe<&2, Img.Raster>, + st => w8.out(st), Jpeg.decode.walk(List.append(&2, U32, hd, rr), Jpeg.decode.st0()), Jpeg.decode.walk(rr, + Jpeg.decode.walk(hd, Jpeg.decode.st0())), W8.walk_app(hd, rr, Jpeg.decode.st0())), + Equal.trans(Maybe<&2, Img.Raster>, w8.out(Jpeg.decode.walk(rr, Jpeg.decode.walk(hd, Jpeg.decode.st0()))), + w8.out(Jpeg.decode.walk(rr, ent)), Img.decode_jpeg.out(Jpeg.decode.run(fr, sc, tb, ee, 0)), + Equal.cong(Jpeg.St, Maybe<&2, Img.Raster>, st => w8.out(Jpeg.decode.walk(rr, st)), Jpeg.decode.walk(hd, + Jpeg.decode.st0()), ent, Laws.jpeg_enc_header_walk(ww, hh)), + Equal.trans(Maybe<&2, Img.Raster>, w8.out(Jpeg.decode.walk(rr, ent)), w8.out(stop), + Img.decode_jpeg.out(Jpeg.decode.run(fr, sc, tb, ee, 0)), Equal.cong(Jpeg.St, Maybe<&2, Img.Raster>, + st => w8.out(st), Jpeg.decode.walk(rr, ent), stop, Laws.jpeg_ent_walk(ee, Laws.jpeg_enc_stuffed(ww, hh, cp), fr, + sc, tb, [], 0, 1, 0)), Equal.cong(List<&2, U32>, Maybe<&2, Img.Raster>, xs => Img.decode_jpeg.out( + Jpeg.decode.run(fr, sc, tb, xs, 0)), List.reverse(&2, U32, List.reverse.go(&2, U32, ee, [])), ee, + Flt.rev_rev(ee))))))) + +def Laws.jpeg_run_sized(ww, hh, nf, ids, hs, vs, tq, hmax, vmax, scan, tabs, ent, ri): + W10.run.sized(ww, hh, nf, ids, hs, vs, tq, hmax, vmax, scan, tabs, ent, ri) + +def Laws.jpeg_round_trip_sized(ww, hh, px, h_good, h_w, h_h): + +ee = Jenc.encode.arm(ww, hh, Img.colours(px)) + Equal.trans(Bool, Laws.jpg.sized(Laws.jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px})), ww, hh), + Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.run(Laws.jpg.enc.frame(ww, hh), Laws.jpg.enc.scan(), + Laws.jpg.enc.tabs(), ee, 0)), ww, hh), True{}, Equal.cong(Maybe<&2, Img.Raster>, Bool, mm => Laws.jpg.sized(mm, ww, + hh), Laws.jpg.back(Img.encode_jpeg(Img.Raster{ww, hh, px})), Img.decode_jpeg.out(Jpeg.decode.run( + Laws.jpg.enc.frame(ww, hh), Laws.jpg.enc.scan(), Laws.jpg.enc.tabs(), ee, 0)), Laws.jpeg_round_trip_scan(ww, hh, + px, h_good, h_w, h_h)), Laws.jpeg_run_sized(ww, hh, 3, [1, 2, 3], [1, 1, 1], [1, 1, 1], [0, 0, 0], 1, 1, + Laws.jpg.enc.scan(), Laws.jpg.enc.tabs(), ee, 0)) + +def Laws.jpeg_walk_count(ww, hh, ids, hs, vs, hmax, vmax, ns, sids, top, h_ns, h_units, h_sum, h_fit): + W10.walk.count(Jpeg.decode.ceil(ww, (hmax * 8 : U32)), Jpeg.decode.ceil(hh, (vmax * 8 : U32)), + Jpeg.decode.blocks.sum(hs, vs, 0), ns, sids, ids, hs, vs, top, W10.usum.pos(ns, sids, ids, hs, vs, h_ns, h_units), + h_sum, h_fit) + +def Laws.jpeg_unstuff(bs, ok): + +xs = Laws.jpg.bytes(bs) + +nn = List.length(&2, Laws.JByte, bs) + Equal.trans(List<&2, U32>, Laws.jpg.read8(nn, Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, 0, + Jenc.encode.stuff.all(List.reverse(&2, U32, xs), [])})), Laws.jpg.read8(nn, Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, + 0, W10.stf(xs, [])})), xs, Equal.cong(List<&2, U32>, List<&2, U32>, zs => Laws.jpg.read8(nn, Jpeg.decode.read.n(8, + Jpeg.Bits{0, ok, 0, zs})), Jenc.encode.stuff.all(List.reverse(&2, U32, xs), []), W10.stf(xs, []), + W10.stall.rev(xs, [], [])), W10.rd.list(bs, ok, [])) diff --git a/SPEC.md b/SPEC.md index 0df640f..32478ea 100644 --- a/SPEC.md +++ b/SPEC.md @@ -69,8 +69,8 @@ What a sample means, for every decoder and encoder. | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | | 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 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 | pending | LAWS.bend jpeg_refuse_factor1; LAWS.bend jpeg_refuse_factor3; LAWS.bend jpeg_comp_index; LAWS.bend jpeg_walk_unit; LAWS.bend jpeg_walk_comp; LAWS.bend jpeg_walk_mcu; LAWS.bend jpeg_mcu_grid; LAWS.bend jpeg_block_cover; LAWS.bend jpeg_rgbs_at | -| IMG-JPG-3 | For every well-formed raster `r` with both sides nonzero and at most 65535, `decode_jpeg(encode_jpeg(r))` is some raster of `r`'s size with alpha 255. | Proved | pending | | +| IMG-JPG-2 | For a SOF0 frame 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 | pending | 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 | +| IMG-JPG-3 | For every well-formed raster `r` with both sides nonzero and at most 65535, `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 | | 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 | | | @@ -81,15 +81,15 @@ What a sample means, for every decoder and encoder. | ID | Proved so far | Missing | | :---- | :---- | :---- | -| IMG-JPG-2 | Refusal: a SOF0 segment of one or three components, one with a factor outside 1, 2 and 4, met where a segment may start, makes `decode_jpeg` none whatever precedes and follows it (`jpeg_refuse_factor1`, `jpeg_refuse_factor3`). Placement: a scan component takes the factors of the frame component whose identifier it names, the first with that identifier (`jpeg_comp_index`); the MCU walk goes from data unit `bi` of a scan component to `bi + 1` while the component has more units in the MCU, then to unit 0 of the next scan component, then to unit 0 of the first component of MCU `mcu + 1` (`jpeg_walk_unit`, `jpeg_walk_comp`, `jpeg_walk_mcu`); a component's `hi * vi` units of an MCU sit in T.81 A.2.3's grid, `hi` to a row, each sample covering `hmax / hi` by `vmax / vi` pixels (`jpeg_mcu_grid`); painting a block writes sample `k` over exactly the `pw` by `ph` pixels at `(ox + (k mod 8) * pw, oy + (k div 8) * ph)` inside the frame (`jpeg_block_cover`). Colour: sample `k` of the colour pass is `Jpeg.rgb` of point `k`'s Y, Cb and Cr (`jpeg_rgbs_at`) | that the walk's block count (`ceil(w / 8 hmax) * ceil(h / 8 vmax)` MCUs of the scan's units) makes the steps above reach every MCU, with the U32 counters `mx`, `my` and `mcu` not wrapping; that `decode.emit` reads plane point `k` as sample `k`, which needs `Array.get` after `Array.set` lemmas; `jpeg_mcu_grid` for a scan whose component is not the frame's first (it follows from `jpeg_comp_index` but is stated for one component); `jpeg_block_cover` for `pw = ph = 4` (left out because its proof takes about 100 s of the gate) and for a plane already painted; the refusal for a SOF0 segment with a length longer than its components, or reached after fill bytes | -| 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 | that `decode_jpeg` reads `encode_jpeg`'s output back to a raster at all: the marker walk over the encoder's header, the Huffman round trip of the entropy-coded data (bit writer against bit reader, byte stuffing, the Annex K tables), and the frame size carried through | +| IMG-JPG-2 | Refusal: a SOF0 segment with a factor outside 1, 2 and 4 makes `decode_jpeg` none, for one component or three, whatever precedes and follows it (`jpeg_refuse_factor1`, `jpeg_refuse_factor3`), and also after fill bytes before its marker and with a length field longer than its components (`jpeg_refuse_factor1_any`, `jpeg_refuse_factor3_any`); a SOF0 segment of any other component count is none whatever its factors (`jpeg_refuse_count`). Placement: a scan component takes the factors of the frame component whose identifier it names, the first with that identifier (`jpeg_comp_index`); the MCU walk goes from data unit `bi` to `bi + 1`, then to the next scan component, then to the next MCU (`jpeg_walk_unit`, `jpeg_walk_comp`, `jpeg_walk_mcu`); from the scan's first block the decoder's own walk visits the frame's MCUs in raster order, `ceil(w / 8 hmax)` to a row, and in each MCU the scan's components and their `hi * vi` units in T.81 order, the unit, component and column counters never wrapping (`jpeg_walk_frame`), and the U32 block count the decoder runs, `decode.nblocks`, is that order's length over `ceil(h / 8 vmax)` MCU rows when the scan carries the frame's data units and the count fits a U32 (`jpeg_walk_count`); the `hi * vi` units of any scan component sit in T.81 A.2.3's grid, `hi` to a row, each sample covering `hmax / hi` by `vmax / vi` pixels (`jpeg_mcu_grid`, `jpeg_mcu_grid_comp`); painting a block writes sample `k` over exactly the `pw` by `ph` pixels at `(ox + (k mod 8) * pw, oy + (k div 8) * ph)` inside the frame, for every sample size, 4 by 4 included, and onto every plane, one earlier blocks painted included (`jpeg_block_cover`, `jpeg_block_cover_all`); the decoder reads a plane out point by point, sample `k` being the value `Array.get` finds at index `k` (`jpeg_points_at`). Colour: sample `k` of the colour pass is `Jpeg.rgb` of point `k`'s Y, Cb and Cr (`jpeg_rgbs_at`) | that `Array.get` at an index finds the value the last `Array.set` at that index wrote, and a set at another index leaves it (the planes are perfect binary trees of `2^d` leaves, and the lemmas must follow the masked index down the tree), which joins the painting laws to `jpeg_points_at`. And the row is false as worded for frames of more than 2^31 points, which sides up to 65535 allow: `decode.plane` takes its depth from `U32.shl(nn)`, which wraps above 2^31, so the plane has fewer leaves than points and points alias (`decode.depth` is 0 at 2^31 + 1 points and 30 at 3 * 2^30), and past 2^32 points `w * h` itself wraps (a decision for the maintainer) | +| 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`) | that `decode.run` on the encoder's entropy-coded bytes is not none: that every Huffman lookup finds its symbol and every block ends by 64 coefficients, which is the bit writer (`encode.bits`, `encode.pack`, the pad with 1 bits: that the bytes it writes carry the codes' bits in order) against the bit reader reading codes of 1 to 16 bits across byte boundaries (the byte-aligned case is `jpeg_unstuff`), the Annex K tables `encode.huff` builds against the ones `decode.canon` builds and `decode.look` searches, and the encoder's three paths (neutral, solid, `encode.go`) each writing `ceil(w / 8) * ceil(h / 8)` MCUs of three blocks, each a DC code and magnitude, AC run and size codes and magnitudes, and EOB | | IMG-PIX-1 | The JPEG side. `Jpeg.rgb` and `Jpeg.gray` give alpha 255 for every input (`jpeg_rgb_opaque`, `jpeg_gray_opaque`); every sample `decode_jpeg` returns is packed by `Jpeg.gray`, or every one by `Jpeg.rgb` (`jpeg_decode_packed`); every sample it returns has alpha 255 (`jpeg_decode_opaque`); a gray sample carries its level's low byte in R, G and B (`jpeg_gray_level`) | that every sample `decode_png` returns is `0xAARRGGBB`: `png_walk` (IMG-PNG-9) reaches `decode_png` for files in the standard chunk order, not yet for files with ancillary chunks. `jpeg_decode_packed` does not say that the gray packing is the one chosen for a one-component frame | | IMG-PNG-2 | the one-block encoding: every raster `png_ok` accepts (both sides nonzero, `w * h` samples, `w * h` below 2^32) whose scanlines, `h * (1 + w * c)` bytes for c channels (3 when every sample is opaque, 4 otherwise), are at most 65535 decodes from its PNG to itself (`png_roundtrip_one`), through `png_walk`, `inflate_enc_zlib`, `unfilter_filter` with filter None, and `png_px_rgb` / `png_px_rgba` | the two wide paths `encode_png` takes past 65535 scanline bytes: `enc.seal.wide` (colour type 6, `enc.pour`) and `enc.wide.rgb` (colour type 2, `enc.rgb.go`) must be shown to write `zlib.stored(65535, raw)` with the IDAT CRC. And the row is false as worded, even with the approved bound of fewer than 2^32 samples: the scanline count `enc.nbytes` and the IDAT length are U32s, so a raster of 2^32 scanline bytes or more encodes to a file that does not decode (a decision for the maintainer) | | IMG-PNG-9 | `Png.px.of`, the pixel stage, packs unfiltered bytes as the row says for every colour type: gray, gray with a tRNS key, gray and alpha, RGB, RGB with a tRNS key, RGBA (`png_px_grey`, `png_px_grey_key`, `png_px_ga`, `png_px_rgb`, `png_px_rgb_key`, `png_px_rgba`), and each index it decodes as its palette entry with alpha from tRNS or 255 (`png_px_indexed`); the decoder's last stage is `px.of` of `Png.unfilter`'s output with the width and height kept (`png_samples_frame`); and the walker lift, `png_walk`: a file of the signature, IHDR (any nonzero width and height, bit depth 8, a colour type the row names, methods 0), PLTE and tRNS where section 11 allows them, any IDAT chunks and IEND, each chunk framed with its CRC-32 and shorter than 2^32 bytes, decodes to the raster `px.of` packs, for the IHDR colour type and the PLTE and tRNS data, from `Png.unfilter` of the concatenated IDAT data inflated | files whose chunks come in another order the decoder accepts: ancillary chunks (which the walker skips, closing the IDAT run) between the critical ones | -Every Proved row but IMG-JPG-1, IMG-JPG-4, IMG-JPG-5, IMG-PIX-2, IMG-RAS-1, IMG-RAS-2, IMG-RAS-3, IMG-RAS-4, IMG-RAS-5, IMG-PNG-1, IMG-PNG-3, IMG-PNG-4, IMG-PNG-5, IMG-PNG-6, IMG-PNG-7 and IMG-PNG-8 is pending; IMG-PIX-1, IMG-PNG-2 and IMG-PNG-9 have 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 but IMG-JPG-1, IMG-JPG-4, IMG-JPG-5, IMG-PIX-2, IMG-RAS-1, IMG-RAS-2, IMG-RAS-3, IMG-RAS-4, IMG-RAS-5, IMG-PNG-1, IMG-PNG-3, IMG-PNG-4, IMG-PNG-5, IMG-PNG-6, IMG-PNG-7 and IMG-PNG-8 is pending; IMG-PIX-1, IMG-PNG-2, IMG-PNG-9, IMG-JPG-2 and IMG-JPG-3 have 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). -IMG-PNG-2 is false as worded for rasters of 2^32 scanline bytes or more, which fewer than 2^32 samples do not rule out (above); no other 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). +IMG-PNG-2 is false as worded for rasters of 2^32 scanline bytes or more, which fewer than 2^32 samples do not rule out, and IMG-JPG-2 for frames of more than 2^31 points (both above); no other 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). ## Trust boundary diff --git a/docs/rfc/ezimg-law-inventory.md b/docs/rfc/ezimg-law-inventory.md index f11da07..1254222 100644 --- a/docs/rfc/ezimg-law-inventory.md +++ b/docs/rfc/ezimg-law-inventory.md @@ -329,4 +329,5 @@ requirement depends on. | WP6, the raster (IMG-RAS-1 to IMG-RAS-4) | done; IMG-RAS-2 to IMG-RAS-4 proved after rewording | U32 lemma library `proof/wp6-raster.bend`: `Word.cmp` is `Nat.cmp` of the words' numbers (`word_cmp_nat`, so `u32_lt`, `u32_le`, `u32_eq`); the adder, the subtractor and shift-and-add multiplication read as Nat when the result fits (`adc_nat`, `sbc_nat`, `mulgo_nat`), stated for U32 as `u32_add_below`, `u32_mul_below` (the exact result at most some U32's value) and `u32_sub_nat` (b <= a); `u32_index` (y * w + x does not wrap when x < w, y < h and w * h is some U32's value); Nat order, min, sub, take, drop and append lemmas. A closed 2^32 in a law is expanded in unary by the checker and overflows its stack, so the laws take w * h < 2^32 as a U32 `area` whose value is w * h. IMG-RAS-1: `fill_wf`, `fill_every`. IMG-RAS-2: `get_inside`, `get_inside_some`, `get_outside`, `set_inside`, `set_outside`. IMG-RAS-3: `crop_size`, `crop_wf`, `crop_at`, through a normal form of crop's case tree (`crop.nf_eq`) and the rows walk (`crop.rows_len`, `crop.rows_get`). IMG-RAS-4: `blit_size`, `blit_wf`, `blit_in`, `blit_out`, through the three parts of `blit.join` (`bj.top`, `bj.band`, `bj.bottom`) and one pasted row (`blit.row_left`, `row_mid`, `row_right`). No code change. Mutants: get with x and y swapped, set writing two samples, fill's count off by one and a wrong colour, get and set outside touching sample 0, crop's width off by one at the edge, crop's start and gap off by one, blit ignoring the offset (both axes, and x alone): each fails the gate in its law or its law's helper, and each makes a concrete instance of its law false. Left: IMG-RAS-2 to 4 for well-formed rasters with w * h of 2^32 or more, where they are false as worded (decision) | | WP8, JPEG numeric rows | done; IMG-JPG-6 and the new IMG-JPG-8 Trusted, IMG-JPG-2 and IMG-JPG-3 pending after rewording | IMG-JPG-6: `Jpeg.rgb.bits` rounded G's two terms separately with 16-bit constants and differed from T.871 on 3,320,385 of the 2^24 inputs, by 1; it now computes each channel exactly in millionths (`rgb.ch`: one division, one rounding, then the clamp), and a Python copy of the new U32 arithmetic matches exact T.871 on all 2^24 inputs; 48 of 108 JPEG probe decodes change, each channel by at most 1. A proof would need U32 division and products near 10^9 in Nat terms, and a unary comparison of 255 * 10^6 against 4 * 10^9 already exhausts the checker's memory, so the row moved to Trusted (maintainer decision). IMG-JPG-3 was false (round-trip error up to 7, a 2 by 2 raster suffices): split into the structural row, pending, and the Trusted bound IMG-JPG-8 (within 8; 7 measured before and after the conversion change, libjpeg reaches 4 with the same settings). IMG-JPG-2 reworded (sample values left to IMG-JPG-7) and proved in parts: `jpeg_refuse_factor1`, `jpeg_refuse_factor3` (a SOF0 segment with a factor outside 1, 2 and 4, after any prefix that leaves the walk at a segment boundary, makes `decode_jpeg` none), `jpeg_comp_index` (a scan component finds its frame component), `jpeg_walk_unit`, `jpeg_walk_comp`, `jpeg_walk_mcu` (the MCU walk's three steps), `jpeg_mcu_grid` (T.81 A.2.3 grid for every factor pair), `jpeg_block_cover` (sample replication, 4 by 4 left out for gate time) and `jpeg_rgbs_at` (the colour pass is pointwise). Code: factor and count checks as `U32.is_eq` Bools, `Comps.ok`, `decode.read.sof.c`; `decode.index` without its dummy accumulator. Lemmas in `proof/wp8-jpeg-numeric.bend` (`walk_app`, `walk_stop`, `fac_elim`). Each new law caught a planted mutant | | WP9, PNG round trip (IMG-PNG-2, IMG-PNG-9 lift) | done, both partial; IMG-PNG-2 false as worded past 2^32 scanline bytes (decision) | `png_walk` lifts the pixel stage to `decode_png`: a file of the signature, IHDR, PLTE and tRNS where allowed, any IDAT chunks and IEND, each chunk framed (`spec.chunk`: length, type, data, `crc.ref`) and shorter than 2^32 bytes, decodes to the raster `px.of` packs from `Png.unfilter` of the concatenated IDAT data inflated, with the IHDR colour type and the PLTE and tRNS data. `png_roundtrip_one` proves IMG-PNG-2 for every raster `png_ok` accepts whose scanlines fit one stored block (at most 65535 bytes): the encoder's file is `spec.png` with one IDAT (`seal.one.same`), then `png_walk`, `inflate_enc_zlib`, `unfilter_filter` with filter None, and `png_px_rgb` / `png_px_rgba` with the samples read back bit by bit (`be.back`: `be.u32` of `spec.be4`'s bytes is the word, 32 bits taken apart and 24 `Bool.or(b, False)` rewrites). Code, byte-identical on the probe outputs: `enc.r`, `enc.g`, `enc.b` mask with the constant first. Lemmas in `proof/wp9-png-roundtrip.bend`. Mutants (IDAT data appended in the wrong order, PLTE kept reversed, tRNS dropped at finish, IHDR width and height swapped, green written for blue, filter byte 1, alpha written 255): each fails the gate. Left: the wide paths (`enc.seal.wide` / `enc.pour`, `enc.wide.rgb` / `enc.rgb.go`), ancillary chunks for IMG-PNG-9, and the row's wording: `enc.nbytes` and the IDAT length are U32s, so a 32768 by 32768 raster with one non-opaque sample (2^30 samples) counts 32768 scanline bytes and takes the one-block path with a wrong LEN | +| WP10, JPEG placement and the round trip's structure (IMG-JPG-2, IMG-JPG-3) | done, both partial; IMG-JPG-2 false as worded above 2^31 points | IMG-JPG-2: `jpeg_block_cover_all` (every sample size, 4 by 4 included, onto any plane), `jpeg_mcu_grid_comp` (the A.2.3 grid for any scan component), `jpeg_refuse_factor1_any`, `jpeg_refuse_factor3_any` (fill bytes before the marker, a length longer than the components), `jpeg_refuse_count` (any other component count), `jpeg_points_at` (sample k of a plane's read-out is `Array.get` at k), `jpeg_walk_frame` (the decoder's own walk visits every MCU in raster order and each MCU's units in T.81 order, no counter wrapping) and `jpeg_walk_count` (the U32 block count `decode.nblocks` is that order's length when it fits). IMG-JPG-3: `jpeg_enc_stuffed`, `jpeg_unstuff` (the bit reader reads stuffed bytes back, eight bits at a time), `jpeg_enc_header_walk`, `jpeg_ent_walk`, `jpeg_round_trip_scan` (`decode_jpeg(encode_jpeg(r))` is the scan decode of the encoder's entropy-coded bytes in `r`'s frame), `jpeg_run_sized`, `jpeg_round_trip_sized` (none or a raster of `r`'s size). Code, byte-identical on all probe outputs and on crafted fill, marker and truncation cases: block painting written by rows, columns and pixels as the law-side cover is (`decode.splat`), which also drops `jpeg_block_cover`'s 1024-write normalisation from the gate; `decode.emit` reads a plane point by point in order (`decode.points`); `decode.nbits` and the entropy walk compare bytes with `U32.is_eq`, and `decode.nbits` ors the new bit in first; the encoder keeps raw bytes and stuffs once at the flush (`encode.stuff.all`), and dispatches on its tag with `U32.is_eq`; the block count is named (`decode.nblocks`). Lemmas in `proof/wp10-jpeg-finish.bend`, among them `dup` (two copies of an array, each equal to it: proofs are live, so an array cannot go to two lemmas) and the MCU-walk runs (`run.units` to `run.rows`). Mutants: a block column at `col * ph`, a scan component's factors taken from frame component `comp`, factor 3 accepted, a component count of 2 accepted, the read-out starting at point 1, an MCU row skipped, the block count summed from 1, a 255 not stuffed, the SOF width's low byte masked with 254, a stuffed 0 dropped by the walk, the entropy bytes not reversed, a gray picture's sides swapped, a colour picture's height as its width, a stuffed 255 read as 254: each fails its law or that law's lemma. Left: IMG-JPG-2's `Array.get` after `Array.set` lemmas, and the row is false for frames above 2^31 points (`decode.plane`'s depth wraps; decision); IMG-JPG-3's Huffman round trip, that `decode.run` of the encoder's bytes is not none. Gate about 4 m 20 s, main's 4 m 50 s | | 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` | diff --git a/proof/wp10-jpeg-finish.bend b/proof/wp10-jpeg-finish.bend new file mode 100644 index 0000000..8a2611c --- /dev/null +++ b/proof/wp10-jpeg-finish.bend @@ -0,0 +1,2312 @@ +# proof/wp10-jpeg-finish: lemmas for IMG-JPG-2's last parts (block painting, component placement, the +# SOF0 refusals, the MCU walk over the frame, reading the planes out) and IMG-JPG-3's intermediate laws +# (the encoder's header walked by the decoder, the entropy-coded data unstuffed). PROOF.bend imports this +# file as W10, so the gate checks it. +import Base +import ../LAWS.bend as Laws +import ../main.bend as Img +import ../src/jpeg.bend as Jpeg +import ../src/jpeg_enc.bend as Jenc +import ./u32.bend as U32L +import ./wp6-raster.bend as R +import ./wp7-jpeg-struct.bend as W7 +import ./wp8-jpeg-numeric.bend as W8 + +# ---- block painting (IMG-JPG-2) ---- + +# the decoder's pixel row of one sample's cover is jpg.cover.px's, write for write +def cv.px( + left: Nat, + -plane: Array, + +x0: U32, + +yy: U32, + +px: U32, + +ww: U32, + +hh: U32, + +vv: U32 +) -> {Jpeg.decode.splat.px(left, plane, x0, yy, px, ww, hh, vv) == Laws.jpg.cover.px(left, plane, x0, yy, px, ww, hh, + vv) : Array}: + match left: + case 0n: + {==} + case 1n+pp: + cv.px(pp, Jpeg.decode.splat.in(U32.is_lt((x0 + px : U32), ww), U32.is_lt(yy, hh), plane, (x0 + px : U32), yy, + ww, vv), x0, yy, (px + 1 : U32), ww, hh, vv) + +# the decoder's cover of one sample is jpg.cover.py's, row for row +def cv.py( + left: Nat, + -plane: Array, + +x0: U32, + +y0: U32, + +py: U32, + +pw: U32, + +ww: U32, + +hh: U32, + +vv: U32 +) -> {Jpeg.decode.splat.py(left, plane, x0, y0, py, pw, ww, hh, vv) == Laws.jpg.cover.py(left, plane, x0, y0, py, pw, + ww, hh, vv) : Array}: + match left: + case 0n: + {==} + case 1n+pp: + ee = cv.px(U32.to_nat(pw), plane, x0, (y0 + py : U32), 0, ww, hh, vv) + %ee : {Jpeg.decode.splat.py(pp, Jpeg.decode.splat.px(U32.to_nat(pw), plane, x0, (y0 + py : U32), 0, ww, hh, vv), + x0, y0, (py + 1 : U32), pw, ww, hh, vv) == Laws.jpg.cover.py(pp, _, x0, y0, (py + 1 : U32), pw, ww, hh, vv) : + Array} + cv.py(pp, Jpeg.decode.splat.px(U32.to_nat(pw), plane, x0, (y0 + py : U32), 0, ww, hh, vv), x0, y0, + (py + 1 : U32), pw, ww, hh, vv) + +# the decoder's block row is jpg.cover.col's, sample for sample +def cv.col( + left: Nat, + -plane: Array, + +samples: List<&2, U32>, + +row: U32, + +col: U32, + +ox: U32, + +oy: U32, + +pw: U32, + +ph: U32, + +ww: U32, + +hh: U32 +) -> {Jpeg.decode.splat.col(left, plane, samples, row, col, ox, oy, pw, ph, ww, hh) == + Laws.jpg.cover.col(left, plane, samples, row, col, ox, oy, pw, ph, ww, hh) : Array}: + match left: + case 0n: + {==} + case 1n+pp: + ee = cv.py(U32.to_nat(ph), plane, (ox + col * pw : U32), (oy + row * ph : U32), 0, pw, ww, hh, + Jpeg.decode.at(samples, (row * 8 + col : U32))) + %ee : {Jpeg.decode.splat.col(pp, Jpeg.decode.splat.py(U32.to_nat(ph), plane, (ox + col * pw : U32), + (oy + row * ph : U32), 0, pw, ww, hh, Jpeg.decode.at(samples, (row * 8 + col : U32))), samples, row, + (col + 1 : U32), ox, oy, pw, ph, ww, hh) == Laws.jpg.cover.col(pp, _, samples, row, (col + 1 : U32), ox, oy, + pw, ph, ww, hh) : Array} + cv.col(pp, Jpeg.decode.splat.py(U32.to_nat(ph), plane, (ox + col * pw : U32), (oy + row * ph : U32), 0, pw, + ww, hh, Jpeg.decode.at(samples, (row * 8 + col : U32))), samples, row, (col + 1 : U32), ox, oy, pw, ph, ww, hh) + +# the decoder's block is jpg.cover's, row for row +def cv.all( + left: Nat, + -plane: Array, + +samples: List<&2, U32>, + +row: U32, + +ox: U32, + +oy: U32, + +pw: U32, + +ph: U32, + +ww: U32, + +hh: U32 +) -> {Jpeg.decode.splat(left, plane, samples, row, ox, oy, pw, ph, ww, hh) == + Laws.jpg.cover(left, plane, samples, row, ox, oy, pw, ph, ww, hh) : Array}: + match left: + case 0n: + {==} + case 1n+pp: + ee = cv.col(8n, plane, samples, row, 0, ox, oy, pw, ph, ww, hh) + %ee : {Jpeg.decode.splat(pp, Jpeg.decode.splat.col(8n, plane, samples, row, 0, ox, oy, pw, ph, ww, hh), samples, + (row + 1 : U32), ox, oy, pw, ph, ww, hh) == Laws.jpg.cover(pp, _, samples, (row + 1 : U32), ox, oy, pw, ph, ww, + hh) : Array} + cv.all(pp, Jpeg.decode.splat.col(8n, plane, samples, row, 0, ox, oy, pw, ph, ww, hh), samples, + (row + 1 : U32), ox, oy, pw, ph, ww, hh) + +# ---- placement of any scan component (IMG-JPG-2) ---- + +# a scan component's placement is the placement of a one-component scan with its frame component's factors +def grid.of( + left: Nat, + +bi: U32, + +comp: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +mx: U32, + +my: U32, + +hmax: U32, + +vmax: U32, + +ww: U32, + +hh: U32 +) -> {Laws.jpg.blocks.of(left, bi, comp, sids, ids, hs, vs, mx, my, hmax, vmax, ww, hh) == Laws.jpg.blocks(left, bi, + Laws.jpg.fac.of(comp, sids, ids, hs), Laws.jpg.fac.of(comp, sids, ids, vs), mx, my, hmax, vmax, ww, hh) : + List<&2, Jpeg.Geom>}: + match left: + case 0n: + {==} + case 1n+pp: + ee = grid.of(pp, (bi + 1 : U32), comp, sids, ids, hs, vs, mx, my, hmax, vmax, ww, hh) + %ee : {Jpeg.decode.geom.go(comp, bi, mx, my, ww, hh, hmax, vmax, sids, ids, hs, vs) <> + Laws.jpg.blocks.of(pp, (bi + 1 : U32), comp, sids, ids, hs, vs, mx, my, hmax, vmax, ww, hh) == + Jpeg.decode.geom.go(0, bi, mx, my, ww, hh, hmax, vmax, [0], [0], [Laws.jpg.fac.of(comp, sids, ids, hs)], + [Laws.jpg.fac.of(comp, sids, ids, vs)]) <> _ : List<&2, Jpeg.Geom>} + {==} + +# ---- the SOF0 refusals (IMG-JPG-2) ---- + +# the state a refused frame header leaves the walk in (the same state as PROOF.bend's w8.stop) +def stop(+sc: Jpeg.Scan, +tb: Jpeg.Tabs, +en: List<&2, U32>, +ri: U32, +kd: U32) -> Jpeg.St: + Jpeg.St{Jpeg.Stop{}, Jpeg.decode.frame0(), sc, tb, en, ri, kd, 1} + +# the frame reader refuses a SOF0 body +def sof.Disp( + +body: List<&2, U32>, + +frame: Jpeg.Frame, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +ent: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32 +) -> Type: + {Jpeg.decode.dispatch(192, body, frame, scan, tabs, ent, ri, kind, bad) == stop(scan, tabs, ent, ri, kind) : + Jpeg.St} + +# a SOF0 segment read from just after its marker: when its body makes the frame reader refuse, the +# walk goes on stopped from the end of the body, whatever the body's length +def sof.seg( + +lh: U32, + +ll: U32, + +body: List<&2, U32>, + +rest: List<&2, U32>, + +frame: Jpeg.Frame, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +ent: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32, + h_len: {U32.is_lt(Jpeg.decode.u16(lh, ll), 2) == False{} : Bool}, + h_body: {U32.to_nat((Jpeg.decode.u16(lh, ll) - 2 : U32)) == List.length(&2, U32, body) : Nat}, + h_disp: sof.Disp(body, frame, scan, tabs, ent, ri, kind, bad) +) -> {Jpeg.decode.walk(lh <> ll <> List.append(&2, U32, body, rest), Jpeg.St{Jpeg.LenHi{192}, frame, scan, tabs, ent, + ri, kind, bad}) == Jpeg.decode.walk(rest, stop(scan, tabs, ent, ri, kind)) : Jpeg.St}: + +slb = {Jpeg.decode.step.len.b(U32.is_lt(Jpeg.decode.u16(lh, ll), 2), 192, Jpeg.decode.u16(lh, ll), frame, scan, tabs, + ent, ri, kind, bad) : Jpeg.St} + Equal.trans(Jpeg.St, Jpeg.decode.walk(List.append(&2, U32, body, rest), slb), + Jpeg.decode.walk(rest, Jpeg.decode.walk(body, slb)), Jpeg.decode.walk(rest, stop(scan, tabs, ent, ri, kind)), + W8.walk_app(body, rest, slb), + Equal.trans(Jpeg.St, Jpeg.decode.walk(rest, Jpeg.decode.walk(body, slb)), + Jpeg.decode.walk(rest, Jpeg.decode.dispatch(192, body, frame, scan, tabs, ent, ri, kind, bad)), + Jpeg.decode.walk(rest, stop(scan, tabs, ent, ri, kind)), + Equal.cong(Jpeg.St, Jpeg.St, st => Jpeg.decode.walk(rest, st), Jpeg.decode.walk(body, slb), + Jpeg.decode.dispatch(192, body, frame, scan, tabs, ent, ri, kind, bad), + W7.seg.read(U32.is_lt(Jpeg.decode.u16(lh, ll), 2), Jpeg.decode.u16(lh, ll), body, 192, frame, scan, tabs, ent, + ri, kind, bad, h_len, h_body)), + Equal.cong(Jpeg.St, Jpeg.St, st => Jpeg.decode.walk(rest, st), + Jpeg.decode.dispatch(192, body, frame, scan, tabs, ent, ri, kind, bad), stop(scan, tabs, ent, ri, kind), + h_disp))) + +# a frame header of a component count the decoder does not read: refused, whatever the components +def sof.cok( + cok: Bool, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +ent: List<&2, U32>, + +ri: U32, + +kind: U32 +) -> {Jpeg.decode.read.sof.c(cok, False{}, U32.is_eq(Jpeg.decode.vmax(hs, 0), 0), ww, hh, nf, ids, hs, vs, tq, scan, + tabs, ent, ri, kind) == stop(scan, tabs, ent, ri, kind) : Jpeg.St}: + match cok: + case True{}: + {==} + case False{}: + {==} + +# the components read, whatever they are, then a count the decoder does not read: refused +def sof.cnt( + cc: Jpeg.Comps, + +ww: U32, + +hh: U32, + +nf: U32, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +ent: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32, + h_nf: {Bool.or(U32.is_eq(nf, 1), U32.is_eq(nf, 3)) == False{} : Bool} +) -> {Jpeg.decode.read.sof.f(cc, ww, hh, nf, scan, tabs, ent, ri, kind, bad) == stop(scan, tabs, ent, ri, kind) : + Jpeg.St}: + match cc: + case Jpeg.Comps{+ids, +hs, +vs, +tq, cok}: + es = Equal.sym(Bool, Bool.or(U32.is_eq(nf, 1), U32.is_eq(nf, 3)), False{}, h_nf) + %es : {Jpeg.decode.read.sof.c(cok, Bool.and(_, U32.is_eq(bad, 0)), U32.is_eq(Jpeg.decode.vmax(hs, 0), 0), ww, + hh, nf, ids, hs, vs, tq, scan, tabs, ent, ri, kind) == stop(scan, tabs, ent, ri, kind) : Jpeg.St} + sof.cok(cok, ww, hh, nf, ids, hs, vs, tq, scan, tabs, ent, ri, kind) + +# ---- words and bytes ---- + +# Bool.and commutes +def band_comm(aa: Bool, bb: Bool) -> {Bool.and(aa, bb) == Bool.and(bb, aa) : Bool}: + match aa bb: + case True{} True{}: + {==} + case True{} False{}: + {==} + case False{} True{}: + {==} + case False{} False{}: + {==} + +# Word.and commutes +def wand_comm(nn: Nat, aw: Word(nn), bw: Word(nn)) -> {Word.and(nn, aw, bw) == Word.and(nn, bw, aw) : Word(nn)}: + match nn: + case 0n: + {==} + case 1n+pp: + match aw bw: + case WCon{+ab, +at} WCon{+bb, +bt}: + e1 = band_comm(ab, bb) + e2 = wand_comm(pp, at, bt) + %e1 : {WCon{Bool.and(ab, bb), Word.and(pp, at, bt)} == WCon{_, Word.and(pp, bt, at)} : Word(1n+pp)} + %e2 : {WCon{Bool.and(ab, bb), Word.and(pp, at, bt)} == WCon{Bool.and(ab, bb), _} : Word(1n+pp)} + {==} + +# U32.and commutes +def uand_comm(au: U32, bu: U32) -> {U32.and(au, bu) == U32.and(bu, au) : U32}: + match au bu: + case U32{aw} U32{bw}: + Equal.cong(Word(32n), U32, ww => U32{ww}, Word.and(32n, aw, bw), Word.and(32n, bw, aw), wand_comm(32n, aw, bw)) + +# or with False on the right is the bit +def bor_false(bb: Bool) -> {Bool.or(bb, False{}) == bb : Bool}: + match bb: + case True{}: + {==} + case False{}: + {==} + +# or with the zero word on the right is the word +def wor_zero(nn: Nat, aw: Word(nn)) -> {Word.or(nn, aw, Word.zero(nn)) == aw : Word(nn)}: + match nn: + case 0n: + match aw: + case WNil{}: + {==} + case 1n+pp: + match aw: + case WCon{+ab, +at}: + e1 = bor_false(ab) + e2 = wor_zero(pp, at) + es1 = Equal.sym(Bool, Bool.or(ab, False{}), ab, e1) + es2 = Equal.sym(Word(pp), Word.or(pp, at, Word.zero(pp)), at, e2) + %es1 : {WCon{_, Word.or(pp, at, Word.zero(pp))} == WCon{ab, at} : Word(1n+pp)} + %es2 : {WCon{ab, _} == WCon{ab, at} : Word(1n+pp)} + {==} + +# the decoder's u16 of a U32's bits 8 and up and its low byte (the mask first) is the U32, for every U32 +def u16_bits(ww: U32) -> {Jpeg.decode.u16(U32.shrn(ww, 8n), U32.and(255, ww)) == ww : U32}: + match ww: + case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, WCon{+b8, WCon{+b9, + WCon{+b10, WCon{+b11, WCon{+b12, WCon{+b13, WCon{+b14, WCon{+b15, WCon{+b16, WCon{+b17, WCon{+b18, WCon{+b19, + WCon{+b20, WCon{+b21, WCon{+b22, WCon{+b23, WCon{+b24, WCon{+b25, WCon{+b26, WCon{+b27, WCon{+b28, WCon{+b29, + WCon{+b30, WCon{+b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: + +tt = {WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, + WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, + WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}} : Word(24n)} + ee = Equal.sym(Word(24n), Word.or(24n, tt, Word.zero(24n)), tt, wor_zero(24n, tt)) + %ee : {U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, _}}}}}}}}} == U32{WCon{b0, + WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, + WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, + WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, + WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32} + {==} + +# ---- reading a plane out (IMG-JPG-2) ---- + +# the size walk keeps the array +def size.eq(aa: Array) -> {Array.size(U32, aa) == (aa, Laws.jpg.val(Array.size(U32, aa))) : + Array & U32}: + match aa: + case ALeaf{_x}: + {==} + case ANode{xs, ys}: + ee = Equal.sym(Array & U32, Array.size(U32, xs), (xs, Laws.jpg.val(Array.size(U32, xs))), size.eq(xs)) + %ee : {Array.size.node(U32, ys, _) == (ANode{xs, ys}, Laws.jpg.val(Array.size.node(U32, ys, _))) : + Array & U32} + {==} + +# a node of equal halves is equal +def node.eq( + -x1: Array, + -y1: Array, + -xs: Array, + -ys: Array, + ex: {x1 == xs : Array}, + ey: {y1 == ys : Array} +) -> {ANode{x1, y1} == ANode{xs, ys} : Array}: + sx = Equal.sym(Array, x1, xs, ex) + sy = Equal.sym(Array, y1, ys, ey) + %sx : {ANode{_, y1} == ANode{xs, ys} : Array} + %sy : {ANode{xs, _} == ANode{xs, ys} : Array} + {==} + +# two copies of an array, each equal to it +def Dup(-aa: Array) -> Type: + &b1: Array -> &b2: Array -> {b1 == aa : Array} & {b2 == aa : Array} + +# copies of an array known equal to another are copies of that one +def dup.tr(-bb: Array, -aa: Array, ee: {bb == aa : Array}, dd: Dup(bb)) -> Dup(aa): + %ee : Dup(_) + dd + +# copies of a node from copies of its halves +def dup.node(-xs: Array, -ys: Array, dx: Dup(xs), dy: Dup(ys)) -> Dup(ANode{xs, ys}): + (x1, x2, e1, e2) = dx + (y1, y2, f1, f2) = dy + (ANode{x1, y1}, ANode{x2, y2}, node.eq(x1, y1, xs, ys, e1, f1), node.eq(x2, y2, xs, ys, e2, f2)) + +# two copies of an array, each equal to it +def dup(aa: Array) -> Dup(aa): + match aa: + case ALeaf{+xx}: + (ALeaf{xx}, ALeaf{xx}, {==}, {==}) + case ANode{xs, ys}: + dup.node(xs, ys, dup(xs), dup(ys)) + +# the result of a read of the tree walk keeps the array: the reads below a node hand the node back +def getif.eq( + -xs: Array, + -ys: Array, + +hh: U32, + +ii: U32, + zz: Bool, + ihx: {Array.get.go(U32, xs, hh, ii) == (xs, Laws.jpg.val(Array.get.go(U32, xs, hh, ii))) : Array & U32}, + ihy: {Array.get.go(U32, ys, hh, U32.sub(ii, hh)) == (ys, Laws.jpg.val(Array.get.go(U32, ys, hh, U32.sub(ii, hh)))) : + Array & U32} +) -> {Array.get.if(U32, xs, ys, hh, ii, zz) == (ANode{xs, ys}, Laws.jpg.val(Array.get.if(U32, xs, ys, hh, ii, zz))) : + Array & U32}: + match zz: + case True{}: + sx = Equal.sym(Array & U32, Array.get.go(U32, xs, hh, ii), (xs, Laws.jpg.val(Array.get.go(U32, xs, hh, + ii))), ihx) + %sx : {Array.swap.lo(U32, ys, _) == (ANode{xs, ys}, Laws.jpg.val(Array.swap.lo(U32, ys, _))) : Array & U32} + {==} + case False{}: + sy = Equal.sym(Array & U32, Array.get.go(U32, ys, hh, U32.sub(ii, hh)), + (ys, Laws.jpg.val(Array.get.go(U32, ys, hh, U32.sub(ii, hh)))), ihy) + %sy : {Array.swap.hi(U32, xs, _) == (ANode{xs, ys}, Laws.jpg.val(Array.swap.hi(U32, xs, _))) : Array & U32} + {==} + +# the tree walk of a read hands the array back +def getgo.eq( + aa: Array, + +nn: U32, + +ii: U32 +) -> {Array.get.go(U32, aa, nn, ii) == (aa, Laws.jpg.val(Array.get.go(U32, aa, nn, ii))) : Array & U32}: + match aa: + case ALeaf{+_xx}: + {==} + case ANode{xs, ys}: + getif.eq(xs, ys, U32.shr(nn), ii, U32.is_lt(ii, U32.shr(nn)), getgo.eq(xs, U32.shr(nn), ii), + getgo.eq(ys, U32.shr(nn), U32.sub(ii, U32.shr(nn)))) + +# the tree walk of a read, at the array's own size and the masked index, hands the array back +def GoAt(-aa: Array, +ii: U32) -> Type: + {Array.get.go(U32, aa, Laws.jpg.val(Array.size(U32, aa)), U32.and(ii, U32.sub(Laws.jpg.val(Array.size(U32, aa)), + 1))) == (aa, Laws.jpg.val(Array.get.go(U32, aa, Laws.jpg.val(Array.size(U32, aa)), U32.and(ii, + U32.sub(Laws.jpg.val(Array.size(U32, aa)), 1))))) : Array & U32} + +# the tree walk of a read of bb, at the size read from cc, hands bb back +def GoAt2(-bb: Array, -cc: Array, +ii: U32) -> Type: + {Array.get.go(U32, bb, Laws.jpg.val(Array.size(U32, cc)), U32.and(ii, U32.sub(Laws.jpg.val(Array.size(U32, cc)), + 1))) == (bb, Laws.jpg.val(Array.get.go(U32, bb, Laws.jpg.val(Array.size(U32, cc)), U32.and(ii, + U32.sub(Laws.jpg.val(Array.size(U32, cc)), 1))))) : Array & U32} + +# the size walk's statement moved along an equality of arrays +def size.tr( + -bb: Array, + -aa: Array, + ee: {bb == aa : Array}, + hh: {Array.size(U32, bb) == (bb, Laws.jpg.val(Array.size(U32, bb))) : Array & U32} +) -> {Array.size(U32, aa) == (aa, Laws.jpg.val(Array.size(U32, aa))) : Array & U32}: + %ee : {Array.size(U32, _) == (_, Laws.jpg.val(Array.size(U32, _))) : Array & U32} + hh + +# the tree walk's statement moved along an equality of arrays +def getgo.tr( + -bb: Array, + -aa: Array, + +nn: U32, + +ii: U32, + ee: {bb == aa : Array}, + hh: {Array.get.go(U32, bb, nn, ii) == (bb, Laws.jpg.val(Array.get.go(U32, bb, nn, ii))) : Array & U32} +) -> {Array.get.go(U32, aa, nn, ii) == (aa, Laws.jpg.val(Array.get.go(U32, aa, nn, ii))) : Array & U32}: + %ee : {Array.get.go(U32, _, nn, ii) == (_, Laws.jpg.val(Array.get.go(U32, _, nn, ii))) : Array & U32} + hh + +# a read, once the size walk has handed the array back, hands it back too +def get.from( + -aa: Array, + +ii: U32, + hs: {Array.size(U32, aa) == (aa, Laws.jpg.val(Array.size(U32, aa))) : Array & U32}, + hg: GoAt(aa, ii) +) -> {Array.get(U32, aa, ii) == (aa, Laws.jpg.val(Array.get(U32, aa, ii))) : Array & U32}: + ss = Equal.sym(Array & U32, Array.size(U32, aa), (aa, Laws.jpg.val(Array.size(U32, aa))), hs) + %ss : {Array.get.at(U32, ii, _) == (aa, Laws.jpg.val(Array.get.at(U32, ii, _))) : Array & U32} + hg + +# the tree walk's statement at a size read from another copy, moved along both equalities +def getgo.tr2( + -bb: Array, + -cc: Array, + -aa: Array, + +ii: U32, + eb: {bb == aa : Array}, + ec: {cc == aa : Array}, + hh: GoAt2(bb, cc, ii) +) -> GoAt(aa, ii): + %eb : {Array.get.go(U32, _, Laws.jpg.val(Array.size(U32, aa)), U32.and(ii, U32.sub(Laws.jpg.val(Array.size(U32, + aa)), 1))) == + (_, Laws.jpg.val(Array.get.go(U32, _, Laws.jpg.val(Array.size(U32, aa)), U32.and(ii, + U32.sub(Laws.jpg.val(Array.size(U32, aa)), + 1))))) : Array & U32} + %ec : {Array.get.go(U32, bb, Laws.jpg.val(Array.size(U32, _)), U32.and(ii, U32.sub(Laws.jpg.val(Array.size(U32, + _)), 1))) == + (bb, Laws.jpg.val(Array.get.go(U32, bb, Laws.jpg.val(Array.size(U32, _)), U32.and(ii, + U32.sub(Laws.jpg.val(Array.size(U32, _)), + 1))))) : Array & U32} + hh + +# the tree walk hands the array back, at the size read from a second copy +def getgo.at( + -aa: Array, + +ii: U32, + dd: Dup(aa) +) -> GoAt(aa, ii): + (c1, c2, e1, e2) = dd + +nn = Laws.jpg.val(Array.size(U32, c2)) + getgo.tr2(c1, c2, aa, ii, e1, e2, getgo.eq(c1, nn, U32.and(ii, U32.sub(nn, 1)))) + +# a read hands the array back, from copies of it +def get.eq.d( + -aa: Array, + +ii: U32, + dd: Dup(aa) +) -> {Array.get(U32, aa, ii) == (aa, Laws.jpg.val(Array.get(U32, aa, ii))) : Array & U32}: + (b1, b2, e1, e2) = dd + get.from(aa, ii, size.tr(b1, aa, e1, size.eq(b1)), getgo.at(aa, ii, dup.tr(b2, aa, e2, dup(b2)))) + +# a read hands the array back +def get.eq(aa: Array, +ii: U32) -> {Array.get(U32, aa, ii) == (aa, Laws.jpg.val(Array.get(U32, aa, ii))) : + Array & U32}: + get.eq.d(aa, ii, dup(aa)) + +# the read statement moved along an equality of arrays +def get.tr( + -bb: Array, + -aa: Array, + +ii: U32, + ee: {bb == aa : Array}, + hh: {Array.get(U32, bb, ii) == (bb, Laws.jpg.val(Array.get(U32, bb, ii))) : Array & U32} +) -> {Array.get(U32, aa, ii) == (aa, Laws.jpg.val(Array.get(U32, aa, ii))) : Array & U32}: + %ee : {Array.get(U32, _, ii) == (_, Laws.jpg.val(Array.get(U32, _, ii))) : Array & U32} + hh + +# a plane read out from point jj on: element mm is the plane's point jj + mm +def emit.at( + nn: Nat, + mm: Nat, + -aa: Array, + +jj: U32, + dd: Dup(aa), + hm: {Nat.is_lt(mm, nn) == True{} : Bool} +) -> {List.get(&2, U32, Jpeg.decode.emit(nn, Array.get(U32, aa, jj), (jj + 1 : U32)), mm) == + Some{Laws.jpg.val(Array.get(U32, aa, Laws.jpg.idx(mm, jj)))} : Maybe<&2, U32>}: + match nn: + case 0n: + -_d = dd + Empty.absurd({List.get(&2, U32, Jpeg.decode.emit(0n, Array.get(U32, aa, jj), (jj + 1 : U32)), mm) == + Some{Laws.jpg.val(Array.get(U32, aa, Laws.jpg.idx(mm, + jj)))} : Maybe<&2, U32>}, U32L.false_true(Equal.trans(Bool, False{}, + Nat.is_lt(mm, 0n), True{}, R.lt_zero_false(mm), hm))) + case 1n+pp: + match mm: + case 0n: + (b1, _b2, e1, _e2) = dd + se = Equal.sym(Array & U32, Array.get(U32, aa, jj), (aa, Laws.jpg.val(Array.get(U32, aa, jj))), + get.tr(b1, aa, jj, e1, get.eq(b1, jj))) + %se : {List.get(&2, U32, Jpeg.decode.emit(1n+pp, _, (jj + 1 : U32)), 0n) == + Some{Laws.jpg.val(Array.get(U32, aa, jj))} : Maybe<&2, U32>} + {==} + case 1n+qq: + (b1, b2, e1, e2) = dd + se = Equal.sym(Array & U32, Array.get(U32, aa, jj), (aa, Laws.jpg.val(Array.get(U32, aa, jj))), + get.tr(b1, aa, jj, e1, get.eq(b1, jj))) + %se : {List.get(&2, U32, Jpeg.decode.emit(1n+pp, _, (jj + 1 : U32)), 1n+qq) == + Some{Laws.jpg.val(Array.get(U32, aa, Laws.jpg.idx(1n+qq, jj)))} : Maybe<&2, U32>} + emit.at(pp, qq, aa, (jj + 1 : U32), dup.tr(b2, aa, e2, dup(b2)), hm) + +# jj advanced one step at a time, mm times, is jj + mm when that stays within the U32 tt +def idx.nat( + +mm: Nat, + +jj: U32, + +tt: U32, + +hh: {Nat.is_le(Nat.add(U32.to_nat(jj), mm), U32.to_nat(tt)) == True{} : Bool} +) -> {U32.to_nat(Laws.jpg.idx(mm, jj)) == Nat.add(U32.to_nat(jj), mm) : Nat}: + match mm: + case 0n: + Equal.sym(Nat, Nat.add(U32.to_nat(jj), 0n), U32.to_nat(jj), R.add_zero(U32.to_nat(jj))) + case 1n+(+pp): + +jn = U32.to_nat(jj) + +h1 = {R.le_trans(Nat.add(jn, 1n), Nat.add(jn, 1n+pp), U32.to_nat(tt), R.le_add_mono(jn, 1n, 1n+pp, + R.le_zero(pp)), hh) : {Nat.is_le(Nat.add(jn, 1n), U32.to_nat(tt)) == True{} : Bool}} + +e1 = {R.u32_add_below(jj, 1, tt, h1) : {U32.to_nat((jj + 1 : U32)) == Nat.add(jn, 1n) : Nat}} + +ea = {Equal.trans(Nat, Nat.add(U32.to_nat((jj + 1 : U32)), pp), Nat.add(Nat.add(jn, 1n), pp), Nat.add(jn, 1n+pp), + Equal.cong(Nat, Nat, xx => Nat.add(xx, pp), U32.to_nat((jj + 1 : U32)), Nat.add(jn, 1n), e1), + R.add_assoc(jn, 1n, pp)) : {Nat.add(U32.to_nat((jj + 1 : U32)), pp) == Nat.add(jn, 1n+pp) : Nat}} + h2 = Equal.trans(Bool, Nat.is_le(Nat.add(U32.to_nat((jj + 1 : U32)), pp), U32.to_nat(tt)), + Nat.is_le(Nat.add(jn, 1n+pp), U32.to_nat(tt)), True{}, Equal.cong(Nat, Bool, xx => Nat.is_le(xx, + U32.to_nat(tt)), Nat.add(U32.to_nat((jj + 1 : U32)), pp), Nat.add(jn, 1n+pp), ea), hh) + Equal.trans(Nat, U32.to_nat(Laws.jpg.idx(pp, (jj + 1 : U32))), Nat.add(U32.to_nat((jj + 1 : U32)), pp), + Nat.add(jn, 1n+pp), idx.nat(pp, (jj + 1 : U32), tt, h2), ea) + +# the index reached by counting kk steps from 0 is kk +def idx.of(+kk: U32) -> {Laws.jpg.idx(U32.to_nat(kk), 0) == kk : U32}: + +kn = U32.to_nat(kk) + +ix = Laws.jpg.idx(kn, 0) + U32L.ueq(ix, kk, Equal.trans(Bool, U32.is_eq(ix, kk), Nat.is_eq(U32.to_nat(ix), kn), True{}, R.u32_eq(ix, kk), + Equal.trans(Bool, Nat.is_eq(U32.to_nat(ix), kn), Nat.is_eq(kn, kn), True{}, Equal.cong(Nat, Bool, + xx => Nat.is_eq(xx, kn), U32.to_nat(ix), kn, idx.nat(kn, 0, kk, R.le_refl(kn))), R.nat_eq_refl(kn)))) + +# ---- the MCU walk over the frame (IMG-JPG-2) ---- + +# the walk's next position, the restart count dropped +def nxt(+ctrl: Jpeg.Ctrl, +fr: Jpeg.Frame, +sc: Jpeg.Scan, +ri: U32) -> Jpeg.Ctrl: + Laws.jpg.pos(Jpeg.decode.adv.ctrl(Jpeg.decode.adv(ctrl, fr, sc, ri))) + +# the positions of the next left blocks, the restart count dropped at every step +def tr(left: Nat, +ctrl: Jpeg.Ctrl, +fr: Jpeg.Frame, +sc: Jpeg.Scan, +ri: U32) -> List<&2, Jpeg.Ctrl>: + match left: + case 0n: + [] + case 1n+pp: + Laws.jpg.pos(ctrl) <> tr(pp, nxt(ctrl, fr, sc, ri), fr, sc, ri) + +# the first MCU of the next MCU row, or the next MCU of this row +def mx.res(inb: Bool, +mcu: U32, +mx: U32, +my: U32) -> Jpeg.Ctrl: + match inb: + case True{}: + Jpeg.Ctrl{0, 0, mx, my, mcu, 0} + case False{}: + Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), mcu, 0} + +# where the walk goes from data unit bi of scan component comp: the next unit, the next component, +# or the next MCU, by whether the component and then the scan have more +def bi.res(more: Bool, next: Bool, inb: Bool, +comp: U32, +bi: U32, +mx: U32, +my: U32, +mcu: U32) -> Jpeg.Ctrl: + match more: + case True{}: + Jpeg.Ctrl{comp, (bi + 1 : U32), mx, my, mcu, 0} + case False{}: + match next: + case True{}: + Jpeg.Ctrl{(comp + 1 : U32), 0, mx, my, mcu, 0} + case False{}: + mx.res(inb, (mcu + 1 : U32), (mx + 1 : U32), my) + +# a new MCU starts at unit 0 of component 0, restart or not +def due.pos( + zero: Bool, + hit: Bool, + +mcu: U32, + +mx: U32, + +my: U32, + +rst: U32 +) -> {Laws.jpg.pos(Jpeg.decode.adv.ctrl(Jpeg.decode.adv.due.b(zero, hit, mcu, mx, my, rst))) == + Jpeg.Ctrl{0, 0, mx, my, mcu, 0} : Jpeg.Ctrl}: + match zero hit: + case True{} _hit: + {==} + case False{} True{}: + {==} + case False{} False{}: + {==} + +# the next MCU in this row, or the first of the next row +def mx.pos( + inb: Bool, + +mcu: U32, + +mx: U32, + +my: U32, + +rst: U32, + +ri: U32 +) -> {Laws.jpg.pos(Jpeg.decode.adv.ctrl(Jpeg.decode.adv.mx(inb, mcu, mx, my, rst, ri))) == mx.res(inb, mcu, mx, my) : + Jpeg.Ctrl}: + match inb: + case True{}: + due.pos(U32.is_eq(ri, 0), U32.is_eq(U32.mod(mcu, Jpeg.decode.ri.nz(ri)), 0), mcu, mx, my, rst) + case False{}: + due.pos(U32.is_eq(ri, 0), U32.is_eq(U32.mod(mcu, Jpeg.decode.ri.nz(ri)), 0), mcu, 0, (my + 1 : U32), rst) + +# after a component's last unit: the next component, or the next MCU +def comp.pos( + next: Bool, + +comp: U32, + +bi: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +rst: U32, + +ww: U32, + +hmax: U32, + +ri: U32 +) -> {Laws.jpg.pos(Jpeg.decode.adv.ctrl(Jpeg.decode.adv.comp(next, comp, mx, my, mcu, rst, ww, hmax, ri))) == + bi.res(False{}, next, U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), comp, bi, mx, my, mcu) : + Jpeg.Ctrl}: + match next: + case True{}: + {==} + case False{}: + mx.pos(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), (mx + 1 : U32), my, + rst, + ri) + +# one step of the walk from data unit bi +def bi.pos( + more: Bool, + +comp: U32, + +bi: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +rst: U32, + +ww: U32, + +hmax: U32, + +ns: U32, + +ri: U32 +) -> {Laws.jpg.pos(Jpeg.decode.adv.ctrl(Jpeg.decode.adv.bi(more, comp, bi, mx, my, mcu, rst, ww, hmax, ns, ri))) == + bi.res(more, U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), + comp, bi, mx, my, mcu) : Jpeg.Ctrl}: + match more: + case True{}: + {==} + case False{}: + comp.pos(U32.is_lt((comp + 1 : U32), ns), comp, bi, mx, my, mcu, rst, ww, hmax, ri) + +# one step of the walk, whatever the restart count: the next unit, component or MCU +def nxt.eq( + +comp: U32, + +bi: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +rst: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32 +) -> {nxt(Jpeg.Ctrl{comp, bi, mx, my, mcu, rst}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri) == bi.res(U32.is_lt((bi + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, + vs)), U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), comp, bi, + mx, my, mcu) : Jpeg.Ctrl}: + bi.pos(U32.is_lt((bi + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), comp, bi, mx, my, mcu, rst, ww, hmax, ns, + ri) + +# the walk from a position does not depend on the restart count it holds +def tr.pos( + left: Nat, + +ctrl: Jpeg.Ctrl, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32 +) -> {tr(left, ctrl, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, + ri) == + tr(left, Laws.jpg.pos(ctrl), Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri) : List<&2, Jpeg.Ctrl>}: + match left: + case 0n: + {==} + case 1n+pp: + match ctrl: + case Jpeg.Ctrl{+comp, +bi, +mx, +my, +mcu, +rst}: + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + +sc = {Jpeg.Scan{ns, sids, td, ta, ss, se, ah} : Jpeg.Scan} + +res = {bi.res(U32.is_lt((bi + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), U32.is_lt((comp + 1 : U32), + ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), comp, bi, mx, my, mcu) : Jpeg.Ctrl} + e1 = nxt.eq(comp, bi, mx, my, mcu, rst, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, + ri) + e0 = nxt.eq(comp, bi, mx, my, mcu, 0, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, + ri) + Equal.cong(Jpeg.Ctrl, List<&2, Jpeg.Ctrl>, cc => {Jpeg.Ctrl{comp, bi, mx, my, mcu, 0} <> tr(pp, cc, fr, sc, + ri) : + List<&2, Jpeg.Ctrl>}, nxt(Jpeg.Ctrl{comp, bi, mx, my, mcu, rst}, fr, sc, ri), + nxt(Jpeg.Ctrl{comp, bi, mx, my, mcu, 0}, fr, sc, ri), + Equal.trans(Jpeg.Ctrl, nxt(Jpeg.Ctrl{comp, bi, mx, my, mcu, rst}, fr, sc, ri), res, + nxt(Jpeg.Ctrl{comp, bi, mx, my, mcu, 0}, fr, sc, ri), e1, Equal.sym(Jpeg.Ctrl, + nxt(Jpeg.Ctrl{comp, bi, mx, my, mcu, 0}, fr, sc, ri), res, e0))) + +# the decoder's trace is the walk with the restart count dropped +def trace.tr( + +left: Nat, + +ctrl: Jpeg.Ctrl, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32 +) -> {Laws.jpg.trace(left, ctrl, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, + se, ah}, ri) == tr(left, ctrl, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, + se, ah}, ri) : List<&2, Jpeg.Ctrl>}: + match left: + case 0n: + {==} + case 1n+(+pp): + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + +sc = {Jpeg.Scan{ns, sids, td, ta, ss, se, ah} : Jpeg.Scan} + +nc = {Jpeg.decode.adv.ctrl(Jpeg.decode.adv(ctrl, fr, sc, ri)) : Jpeg.Ctrl} + Equal.cong(List<&2, Jpeg.Ctrl>, List<&2, Jpeg.Ctrl>, ll => {Laws.jpg.pos(ctrl) <> ll : List<&2, Jpeg.Ctrl>}, + Laws.jpg.trace(pp, nc, fr, sc, ri), tr(pp, Laws.jpg.pos(nc), fr, sc, ri), + Equal.trans(List<&2, Jpeg.Ctrl>, Laws.jpg.trace(pp, nc, fr, sc, ri), tr(pp, nc, fr, sc, ri), + tr(pp, Laws.jpg.pos(nc), fr, sc, ri), + trace.tr(pp, nc, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri), + tr.pos(pp, nc, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri))) + +# n is below n + 1 +def lt.succ(+nn: Nat) -> {Nat.is_lt(nn, 1n+nn) == True{} : Bool}: + match nn: + case 0n: + {==} + case 1n+pp: + lt.succ(pp) + +# n is not below n +def lt.irr(+nn: Nat) -> {Nat.is_lt(nn, nn) == False{} : Bool}: + match nn: + case 0n: + {==} + case 1n+pp: + lt.irr(pp) + +# one less than a number above 0 +def npred(nn: Nat) -> Nat: + match nn: + case 0n: + 0n + case 1n+pp: + pp + +# a number above 0 is one more than its predecessor +def succ.of(+nn: Nat, hh: {Nat.is_lt(0n, nn) == True{} : Bool}) -> {1n+npred(nn) == nn : Nat}: + match nn: + case 0n: + Empty.absurd({1n == 0n : Nat}, U32L.false_true(hh)) + case 1n+_pp: + {==} + +# a U32 above 0 is one more than its predecessor, as a number +def pos.nat(+uu: U32, hh: {U32.is_lt(0, uu) == True{} : Bool}) -> {1n+npred(U32.to_nat(uu)) == U32.to_nat(uu) : Nat}: + succ.of(U32.to_nat(uu), Equal.trans(Bool, Nat.is_lt(0n, U32.to_nat(uu)), U32.is_lt(0, uu), True{}, + Equal.sym(Bool, U32.is_lt(0, uu), Nat.is_lt(0n, U32.to_nat(uu)), R.u32_lt(0, uu)), hh)) + +# xx + 1 does not wrap while xx + 1 + qq is some U32's value +def inc.nat( + +xx: U32, + +uu: U32, + +qq: Nat, + +hb: {Nat.add(U32.to_nat(xx), 1n+qq) == U32.to_nat(uu) : Nat} +) -> {U32.to_nat((xx + 1 : U32)) == Nat.add(U32.to_nat(xx), 1n) : Nat}: + +bn = U32.to_nat(xx) + R.u32_add_below(xx, 1, uu, Equal.trans(Bool, Nat.is_le(Nat.add(bn, 1n), U32.to_nat(uu)), + Nat.is_le(Nat.add(bn, 1n), Nat.add(bn, 1n+qq)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.add(bn, 1n), zz), + U32.to_nat(uu), Nat.add(bn, 1n+qq), Equal.sym(Nat, Nat.add(bn, 1n+qq), U32.to_nat(uu), hb)), + R.le_add_mono(bn, 1n, 1n+qq, R.le_zero(qq)))) + +# a counter two or more below its bound: the next is still below it +def lt.more( + +xx: U32, + +uu: U32, + +pp: Nat, + +hb: {Nat.add(U32.to_nat(xx), 1n+(1n+pp)) == U32.to_nat(uu) : Nat} +) -> {U32.is_lt((xx + 1 : U32), uu) == True{} : Bool}: + +bn = U32.to_nat(xx) + +e1 = {inc.nat(xx, uu, 1n+pp, hb) : {U32.to_nat((xx + 1 : U32)) == Nat.add(bn, 1n) : Nat}} + Equal.trans(Bool, U32.is_lt((xx + 1 : U32), uu), Nat.is_lt(U32.to_nat((xx + 1 : U32)), U32.to_nat(uu)), True{}, + R.u32_lt((xx + 1 : U32), uu), Equal.trans(Bool, Nat.is_lt(U32.to_nat((xx + 1 : U32)), U32.to_nat(uu)), + Nat.is_lt(Nat.add(bn, 1n), Nat.add(bn, 1n+(1n+pp))), True{}, Equal.trans(Bool, + Nat.is_lt(U32.to_nat((xx + 1 : U32)), U32.to_nat(uu)), Nat.is_lt(Nat.add(bn, 1n), U32.to_nat(uu)), + Nat.is_lt(Nat.add(bn, 1n), Nat.add(bn, 1n+(1n+pp))), Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U32.to_nat(uu)), + U32.to_nat((xx + 1 : U32)), Nat.add(bn, 1n), e1), Equal.cong(Nat, Bool, zz => Nat.is_lt(Nat.add(bn, 1n), zz), + U32.to_nat(uu), Nat.add(bn, 1n+(1n+pp)), Equal.sym(Nat, Nat.add(bn, 1n+(1n+pp)), U32.to_nat(uu), hb))), + R.lt_add_mono(bn, 1n, 1n+(1n+pp), {==}))) + +# a counter one below its bound: the next is not below it +def lt.last( + +xx: U32, + +uu: U32, + +hb: {Nat.add(U32.to_nat(xx), 1n) == U32.to_nat(uu) : Nat} +) -> {U32.is_lt((xx + 1 : U32), uu) == False{} : Bool}: + +bn = U32.to_nat(xx) + +e1 = {inc.nat(xx, uu, 0n, hb) : {U32.to_nat((xx + 1 : U32)) == Nat.add(bn, 1n) : Nat}} + Equal.trans(Bool, U32.is_lt((xx + 1 : U32), uu), Nat.is_lt(U32.to_nat((xx + 1 : U32)), U32.to_nat(uu)), False{}, + R.u32_lt((xx + 1 : U32), uu), Equal.trans(Bool, Nat.is_lt(U32.to_nat((xx + 1 : U32)), U32.to_nat(uu)), + Nat.is_lt(U32.to_nat(uu), U32.to_nat(uu)), False{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U32.to_nat(uu)), + U32.to_nat((xx + 1 : U32)), U32.to_nat(uu), Equal.trans(Nat, U32.to_nat((xx + 1 : U32)), Nat.add(bn, 1n), + U32.to_nat(uu), e1, hb)), lt.irr(U32.to_nat(uu)))) + +# a counter two or more below its bound: the next is one or more below it +def lt.next( + +xx: U32, + +uu: U32, + +pp: Nat, + +hb: {Nat.add(U32.to_nat(xx), 1n+(1n+pp)) == U32.to_nat(uu) : Nat} +) -> {Nat.add(U32.to_nat((xx + 1 : U32)), 1n+pp) == U32.to_nat(uu) : Nat}: + +bn = U32.to_nat(xx) + Equal.trans(Nat, Nat.add(U32.to_nat((xx + 1 : U32)), 1n+pp), Nat.add(Nat.add(bn, 1n), 1n+pp), U32.to_nat(uu), + Equal.cong(Nat, Nat, zz => Nat.add(zz, 1n+pp), U32.to_nat((xx + 1 : U32)), Nat.add(bn, 1n), inc.nat(xx, uu, 1n+pp, + hb)), Equal.trans(Nat, Nat.add(Nat.add(bn, 1n), 1n+pp), Nat.add(bn, 1n+(1n+pp)), U32.to_nat(uu), + R.add_assoc(bn, 1n, 1n+pp), hb)) + +# the last of kk + 1 data units counted from 0 is one below their count +def last.nat( + +kk: Nat, + +uu: U32, + +hs: {1n+kk == U32.to_nat(uu) : Nat} +) -> {Nat.add(U32.to_nat(Laws.jpg.idx(kk, 0)), 1n) == U32.to_nat(uu) : Nat}: + +hle = {Equal.trans(Bool, Nat.is_le(kk, U32.to_nat(uu)), Nat.is_le(kk, 1n+kk), True{}, Equal.cong(Nat, Bool, + zz => Nat.is_le(kk, zz), U32.to_nat(uu), 1n+kk, Equal.sym(Nat, 1n+kk, U32.to_nat(uu), hs)), R.lt_le(kk, 1n+kk, + lt.succ(kk))) : {Nat.is_le(kk, U32.to_nat(uu)) == True{} : Bool}} + +ei = {idx.nat(kk, 0, uu, hle) : {U32.to_nat(Laws.jpg.idx(kk, 0)) == kk : Nat}} + Equal.trans(Nat, Nat.add(U32.to_nat(Laws.jpg.idx(kk, 0)), 1n), Nat.add(kk, 1n), U32.to_nat(uu), + Equal.cong(Nat, Nat, zz => Nat.add(zz, 1n), U32.to_nat(Laws.jpg.idx(kk, 0)), kk, ei), Equal.trans(Nat, + Nat.add(kk, 1n), 1n+Nat.add(kk, 0n), U32.to_nat(uu), R.add_succ(kk, 0n), Equal.trans(Nat, 1n+Nat.add(kk, 0n), + 1n+kk, U32.to_nat(uu), Equal.cong(Nat, Nat, zz => 1n+zz, Nat.add(kk, 0n), kk, R.add_zero(kk)), hs))) + +# a false accumulator stays false +def uok.false( + ll: Nat, + +comp: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> {Laws.jpg.units.ok(ll, comp, sids, ids, hs, vs, False{}) == False{} : Bool}: + match ll: + case 0n: + {==} + case 1n+pp: + uok.false(pp, (comp + 1 : U32), sids, ids, hs, vs) + +# a true answer had a true accumulator +def uok.acc( + ll: Nat, + +comp: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + ok: Bool, + hh: {Laws.jpg.units.ok(ll, comp, sids, ids, hs, vs, ok) == True{} : Bool} +) -> {ok == True{} : Bool}: + match ok: + case True{}: + {==} + case False{}: + Empty.absurd({False{} == True{} : Bool}, U32L.false_true(Equal.trans(Bool, False{}, Laws.jpg.units.ok(ll, comp, + sids, ids, hs, vs, False{}), True{}, Equal.sym(Bool, Laws.jpg.units.ok(ll, comp, sids, ids, hs, vs, False{}), + False{}, uok.false(ll, comp, sids, ids, hs, vs)), hh))) + +# the length of two lists of positions +def len.app( + xs: List<&2, Jpeg.Ctrl>, + -ys: List<&2, Jpeg.Ctrl> +) -> {List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, xs, ys)) == Nat.add(List.length(&2, Jpeg.Ctrl, xs), + List.length(&2, Jpeg.Ctrl, ys)) : Nat}: + match xs: + case Nil{}: + {==} + case _hd <> tl: + Equal.cong(Nat, Nat, zz => 1n+zz, List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, tl, ys)), + Nat.add(List.length(&2, Jpeg.Ctrl, tl), List.length(&2, Jpeg.Ctrl, ys)), len.app(tl, ys)) + +# appending positions is associative +def app.assoc( + xs: List<&2, Jpeg.Ctrl>, + -ys: List<&2, Jpeg.Ctrl>, + -zs: List<&2, Jpeg.Ctrl> +) -> {List.append(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, xs, ys), zs) == List.append(&2, Jpeg.Ctrl, xs, + List.append(&2, Jpeg.Ctrl, ys, zs)) : List<&2, Jpeg.Ctrl>}: + match xs: + case Nil{}: + {==} + case +hd <> tl: + Equal.cong(List<&2, Jpeg.Ctrl>, List<&2, Jpeg.Ctrl>, ll => {hd <> ll : List<&2, Jpeg.Ctrl>}, + List.append(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, tl, ys), zs), List.append(&2, Jpeg.Ctrl, tl, + List.append(&2, Jpeg.Ctrl, ys, zs)), app.assoc(tl, ys, zs)) + +# no positions appended +def app.nil(xs: List<&2, Jpeg.Ctrl>) -> {List.append(&2, Jpeg.Ctrl, xs, []) == xs : List<&2, Jpeg.Ctrl>}: + match xs: + case Nil{}: + {==} + case +hd <> tl: + Equal.cong(List<&2, Jpeg.Ctrl>, List<&2, Jpeg.Ctrl>, ll => {hd <> ll : List<&2, Jpeg.Ctrl>}, + List.append(&2, Jpeg.Ctrl, tl, []), tl, app.nil(tl)) + +# the walk from cc visits the positions ll, then goes on from ee: kk blocks after them are the walk from ee +def Run( + -ll: List<&2, Jpeg.Ctrl>, + +cc: Jpeg.Ctrl, + +ee: Jpeg.Ctrl, + +fr: Jpeg.Frame, + +sc: Jpeg.Scan, + +ri: U32, + +kk: Nat +) -> Type: + {tr(Nat.add(List.length(&2, Jpeg.Ctrl, ll), kk), cc, fr, sc, ri) == List.append(&2, Jpeg.Ctrl, ll, tr(kk, ee, fr, sc, + ri)) : List<&2, Jpeg.Ctrl>} + +# two runs, one after the other +def run.cat( + +l1: List<&2, Jpeg.Ctrl>, + +l2: List<&2, Jpeg.Ctrl>, + +c0: Jpeg.Ctrl, + +c1: Jpeg.Ctrl, + +c2: Jpeg.Ctrl, + +fr: Jpeg.Frame, + +sc: Jpeg.Scan, + +ri: U32, + +kk: Nat, + h1: Run(l1, c0, c1, fr, sc, ri, Nat.add(List.length(&2, Jpeg.Ctrl, l2), kk)), + h2: Run(l2, c1, c2, fr, sc, ri, kk) +) -> Run(List.append(&2, Jpeg.Ctrl, l1, l2), c0, c2, fr, sc, ri, kk): + +n1 = List.length(&2, Jpeg.Ctrl, l1) + +n2 = List.length(&2, Jpeg.Ctrl, l2) + +t2 = {tr(kk, c2, fr, sc, ri) : List<&2, Jpeg.Ctrl>} + Equal.trans(List<&2, Jpeg.Ctrl>, tr(Nat.add(List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), kk), c0, + fr, sc, ri), tr(Nat.add(n1, Nat.add(n2, kk)), c0, fr, sc, ri), List.append(&2, Jpeg.Ctrl, List.append(&2, + Jpeg.Ctrl, l1, l2), t2), Equal.cong(Nat, List<&2, Jpeg.Ctrl>, zz => tr(zz, c0, fr, sc, ri), + Nat.add(List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), kk), Nat.add(n1, Nat.add(n2, kk)), + Equal.trans(Nat, Nat.add(List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), kk), + Nat.add(Nat.add(n1, n2), kk), Nat.add(n1, Nat.add(n2, kk)), Equal.cong(Nat, Nat, zz => Nat.add(zz, kk), + List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), Nat.add(n1, n2), len.app(l1, l2)), + R.add_assoc(n1, n2, kk))), Equal.trans(List<&2, Jpeg.Ctrl>, tr(Nat.add(n1, Nat.add(n2, kk)), c0, fr, sc, ri), + List.append(&2, Jpeg.Ctrl, l1, tr(Nat.add(n2, kk), c1, fr, sc, ri)), List.append(&2, Jpeg.Ctrl, List.append(&2, + Jpeg.Ctrl, l1, l2), t2), h1, Equal.trans(List<&2, Jpeg.Ctrl>, List.append(&2, Jpeg.Ctrl, l1, tr(Nat.add(n2, kk), c1, + fr, sc, ri)), List.append(&2, Jpeg.Ctrl, l1, List.append(&2, Jpeg.Ctrl, l2, t2)), List.append(&2, Jpeg.Ctrl, + List.append(&2, Jpeg.Ctrl, l1, l2), t2), Equal.cong(List<&2, Jpeg.Ctrl>, List<&2, Jpeg.Ctrl>, + zz => List.append(&2, Jpeg.Ctrl, l1, zz), tr(Nat.add(n2, kk), c1, fr, sc, ri), List.append(&2, Jpeg.Ctrl, l2, t2), + h2), Equal.sym(List<&2, Jpeg.Ctrl>, List.append(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2), t2), + List.append(&2, Jpeg.Ctrl, l1, List.append(&2, Jpeg.Ctrl, l2, t2)), app.assoc(l1, l2, t2))))) + +# a run followed by no positions +def run.nil( + +ll: List<&2, Jpeg.Ctrl>, + +cc: Jpeg.Ctrl, + +ee: Jpeg.Ctrl, + +fr: Jpeg.Frame, + +sc: Jpeg.Scan, + +ri: U32, + +kk: Nat, + hh: Run(ll, cc, ee, fr, sc, ri, kk) +) -> Run(List.append(&2, Jpeg.Ctrl, ll, []), cc, ee, fr, sc, ri, kk): + es = Equal.sym(List<&2, Jpeg.Ctrl>, List.append(&2, Jpeg.Ctrl, ll, []), ll, app.nil(ll)) + %es : Run(_, cc, ee, fr, sc, ri, kk) + hh + +# a run whose end is known by another name +def run.end( + -ll: List<&2, Jpeg.Ctrl>, + +cc: Jpeg.Ctrl, + +e1: Jpeg.Ctrl, + +e2: Jpeg.Ctrl, + +fr: Jpeg.Frame, + +sc: Jpeg.Scan, + +ri: U32, + +kk: Nat, + hh: Run(ll, cc, e1, fr, sc, ri, kk), + ee: {e1 == e2 : Jpeg.Ctrl} +) -> Run(ll, cc, e2, fr, sc, ri, kk): + %ee : Run(ll, cc, _, fr, sc, ri, kk) + hh + +# the data units bi onward of a scan component, the last of them ll units on: the walk visits each, then +# goes where the decoder goes from the last +def run.units( + +ll: Nat, + +comp: U32, + +bi: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +kk: Nat, + +hb: {Nat.add(U32.to_nat(bi), 1n+ll) == U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)) : Nat} +) -> Run(Laws.jpg.o.units(1n+ll, comp, bi, mx, my, mcu), Jpeg.Ctrl{comp, bi, mx, my, mcu, 0}, + nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(ll, bi), mx, my, mcu, 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri), Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, kk): + match ll: + case 0n: + {==} + case 1n+(+pp): + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + +sc = {Jpeg.Scan{ns, sids, td, ta, ss, se, ah} : Jpeg.Scan} + +cc = {Jpeg.Ctrl{comp, bi, mx, my, mcu, 0} : Jpeg.Ctrl} + +c1 = {Jpeg.Ctrl{comp, (bi + 1 : U32), mx, my, mcu, 0} : Jpeg.Ctrl} + +nn = {Nat.add(List.length(&2, Jpeg.Ctrl, Laws.jpg.o.units(1n+pp, comp, (bi + 1 : U32), mx, my, mcu)), kk) : Nat} + +en = {Equal.trans(Jpeg.Ctrl, nxt(cc, fr, sc, ri), bi.res(U32.is_lt((bi + 1 : U32), Laws.jpg.units(comp, sids, + ids, hs, vs)), + U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bi, mx, my, mcu), c1, + nxt.eq(comp, bi, mx, my, mcu, 0, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, + ri), Equal.cong(Bool, Jpeg.Ctrl, mb => bi.res(mb, + U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bi, mx, my, mcu), + U32.is_lt((bi + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), True{}, lt.more(bi, Laws.jpg.units(comp, + sids, ids, hs, vs), pp, hb))) : {nxt(cc, fr, sc, ri) == c1 : Jpeg.Ctrl}} + Equal.trans(List<&2, Jpeg.Ctrl>, cc <> tr(nn, nxt(cc, fr, sc, ri), fr, sc, ri), cc <> tr(nn, c1, fr, sc, ri), + cc <> List.append(&2, Jpeg.Ctrl, Laws.jpg.o.units(1n+pp, comp, (bi + 1 : U32), mx, my, mcu), tr(kk, + nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(pp, (bi + 1 : U32)), mx, my, mcu, 0}, fr, sc, ri), fr, sc, ri)), + Equal.cong(Jpeg.Ctrl, List<&2, Jpeg.Ctrl>, dd => {cc <> tr(nn, dd, fr, sc, ri) : List<&2, Jpeg.Ctrl>}, + nxt(cc, fr, sc, ri), c1, en), + Equal.cong(List<&2, Jpeg.Ctrl>, List<&2, Jpeg.Ctrl>, zz => {cc <> zz : List<&2, Jpeg.Ctrl>}, tr(nn, c1, fr, + sc, ri), List.append(&2, Jpeg.Ctrl, + Laws.jpg.o.units(1n+pp, comp, (bi + 1 : U32), mx, my, mcu), tr(kk, nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(pp, + (bi + 1 : U32)), mx, my, mcu, 0}, fr, sc, ri), fr, sc, ri)), run.units(pp, comp, (bi + 1 : U32), mx, my, mcu, + ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, kk, lt.next(bi, + Laws.jpg.units(comp, sids, ids, hs, vs), pp, hb)))) + +# where the walk goes after a component's last unit, when the scan has more components +def comp.end.more( + +kk: Nat, + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +hs1: {1n+kk == U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)) : Nat}, + +hnext: {U32.is_lt((comp + 1 : U32), ns) == True{} : Bool} +) -> {nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(kk, 0), mx, my, mcu, 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri) == + Jpeg.Ctrl{(comp + 1 : U32), 0, mx, my, mcu, 0} : Jpeg.Ctrl}: + +bl = Laws.jpg.idx(kk, 0) + Equal.trans(Jpeg.Ctrl, nxt(Jpeg.Ctrl{comp, bl, mx, my, mcu, 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, + vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri), + bi.res(U32.is_lt((bl + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), U32.is_lt((comp + 1 : U32), ns), + U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), comp, + bl, mx, my, mcu), Jpeg.Ctrl{(comp + 1 : U32), 0, mx, my, mcu, 0}, nxt.eq(comp, bl, mx, my, mcu, 0, ww, hh, nf, + ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri), + Equal.trans(Jpeg.Ctrl, bi.res(U32.is_lt((bl + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), + U32.is_lt((comp + 1 : U32), ns), + U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bl, mx, my, mcu), bi.res(False{}, U32.is_lt((comp + 1 : U32), ns), + U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bl, mx, my, mcu), Jpeg.Ctrl{(comp + 1 : U32), 0, mx, my, mcu, 0}, + Equal.cong(Bool, Jpeg.Ctrl, mb => bi.res(mb, U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), + Jpeg.decode.ceil(ww, (hmax * 8 : U32))), + comp, bl, mx, my, mcu), U32.is_lt((bl + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, + vs)), False{}, lt.last(bl, Laws.jpg.units(comp, sids, ids, hs, vs), last.nat(kk, Laws.jpg.units(comp, sids, + ids, hs, vs), hs1))), + Equal.cong(Bool, Jpeg.Ctrl, nb => bi.res(False{}, nb, U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bl, mx, my, mcu), + U32.is_lt((comp + 1 : U32), ns), True{}, hnext))) + +# where the walk goes after the last component's last unit: the next MCU +def comp.end.last( + +kk: Nat, + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +hs1: {1n+kk == U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)) : Nat}, + +hnext: {U32.is_lt((comp + 1 : U32), ns) == False{} : Bool} +) -> {nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(kk, 0), mx, my, mcu, 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri) == + mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), (mx + 1 : U32), + my) : Jpeg.Ctrl}: + +bl = Laws.jpg.idx(kk, 0) + Equal.trans(Jpeg.Ctrl, nxt(Jpeg.Ctrl{comp, bl, mx, my, mcu, 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, + vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri), + bi.res(U32.is_lt((bl + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), U32.is_lt((comp + 1 : U32), ns), + U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), comp, + bl, mx, my, mcu), mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), (mcu + 1 : U32), (mx + 1 : U32), my), + nxt.eq(comp, bl, mx, my, mcu, 0, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, + ri), Equal.trans(Jpeg.Ctrl, bi.res(U32.is_lt((bl + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), + U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bl, mx, my, mcu), bi.res(False{}, + U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bl, mx, my, mcu), + mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), (mx + 1 : U32), + my), Equal.cong(Bool, Jpeg.Ctrl, + mb => bi.res(mb, U32.is_lt((comp + 1 : U32), ns), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), comp, bl, mx, my, mcu), + U32.is_lt((bl + 1 : U32), Laws.jpg.units(comp, sids, ids, hs, vs)), False{}, lt.last(bl, Laws.jpg.units(comp, + sids, ids, hs, vs), last.nat(kk, Laws.jpg.units(comp, sids, ids, hs, vs), hs1))), Equal.cong(Bool, + Jpeg.Ctrl, nb => bi.res(False{}, nb, U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), comp, bl, + mx, my, mcu), + U32.is_lt((comp + 1 : U32), ns), False{}, hnext))) + +# where the walk goes after the last of a component's units in an MCU +def units.End( + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +ee: Jpeg.Ctrl +) -> Type: + {nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(npred(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs))), 0), mx, my, mcu, 0}, + Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri) == ee : + Jpeg.Ctrl} + +# a scan component's units, counted as the decoder counts them: all of them, from unit 0 +def run.comp.units( + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +kk: Nat, + +ee: Jpeg.Ctrl, + +hpos: {U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, vs)) == True{} : Bool}, + hend: units.End(comp, mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, ee) +) -> Run(Laws.jpg.o.units(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)), comp, 0, mx, my, mcu), Jpeg.Ctrl{comp, + 0, mx, my, mcu, 0}, ee, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri, kk): + +k1 = npred(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs))) + +es = {pos.nat(Laws.jpg.units(comp, sids, ids, hs, vs), hpos) : {1n+k1 == U32.to_nat(Laws.jpg.units(comp, sids, + ids, hs, vs)) : Nat}} + %es : Run(Laws.jpg.o.units(_, comp, 0, mx, my, mcu), Jpeg.Ctrl{comp, 0, mx, my, mcu, 0}, ee, Jpeg.Frame{ww, hh, nf, + ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, + kk) + run.end(Laws.jpg.o.units(1n+k1, comp, 0, mx, my, mcu), Jpeg.Ctrl{comp, 0, mx, my, mcu, 0}, + nxt(Jpeg.Ctrl{comp, Laws.jpg.idx(k1, 0), mx, my, mcu, 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri), ee, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, + ri, kk, + run.units(k1, comp, 0, mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, + kk, es), hend) + +# the scan's components comp onward of one MCU, the last ll components on: the walk visits their units in +# order, then goes to the next MCU +def run.comps( + +ll: Nat, + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +kk: Nat, + +ok: Bool, + +hc: {Nat.add(U32.to_nat(comp), 1n+ll) == U32.to_nat(ns) : Nat}, + +hu: {Laws.jpg.units.ok(1n+ll, comp, sids, ids, hs, vs, ok) == True{} : Bool} +) -> Run(Laws.jpg.o.comps(1n+ll, comp, mx, my, mcu, sids, ids, hs, vs), Jpeg.Ctrl{comp, 0, mx, my, mcu, 0}, + mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), (mx + 1 : U32), + my), Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, kk): + match ll: + case 0n: + +hpos = {U32L.and_right(ok, U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, vs)), uok.acc(0n, + (comp + 1 : U32), sids, ids, hs, vs, Bool.and(ok, + U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, + vs))), hu)) : {U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, vs)) == True{} : Bool}} + +k1 = npred(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs))) + +em = {mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), + (mx + 1 : U32), my) : Jpeg.Ctrl} + run.nil(Laws.jpg.o.units(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)), comp, 0, mx, my, mcu), + Jpeg.Ctrl{comp, 0, mx, my, mcu, 0}, em, + Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri, kk, run.comp.units(comp, mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, + ss, se, ah, ri, kk, em, hpos, comp.end.last(k1, comp, mx, my, + mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, pos.nat(Laws.jpg.units(comp, + sids, ids, hs, vs), hpos), lt.last(comp, ns, hc)))) + case 1n+(+pp): + +hpos = {U32L.and_right(ok, U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, vs)), uok.acc(1n+pp, + (comp + 1 : U32), sids, ids, hs, vs, Bool.and(ok, + U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, + vs))), hu)) : {U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, vs)) == True{} : Bool}} + +k1 = npred(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs))) + +em = {mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), + (mx + 1 : U32), my) : Jpeg.Ctrl} + +c1 = {Jpeg.Ctrl{(comp + 1 : U32), 0, mx, my, mcu, 0} : Jpeg.Ctrl} + +l2 = {Laws.jpg.o.comps(1n+pp, (comp + 1 : U32), mx, my, mcu, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + run.cat(Laws.jpg.o.units(U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)), comp, 0, mx, my, mcu), l2, + Jpeg.Ctrl{comp, 0, mx, my, mcu, 0}, c1, + em, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri, kk, run.comp.units(comp, mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, + ss, se, ah, ri, Nat.add(List.length(&2, Jpeg.Ctrl, l2), + kk), c1, hpos, comp.end.more(k1, comp, mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, + ta, ss, se, ah, ri, pos.nat(Laws.jpg.units(comp, sids, ids, hs, vs), hpos), lt.more(comp, ns, pp, hc))), + run.comps(pp, (comp + 1 : U32), mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, + se, ah, ri, kk, Bool.and(ok, U32.is_lt(0, Laws.jpg.units(comp, sids, ids, hs, vs))), lt.next(comp, ns, + pp, hc), hu)) + +# the MCUs mx onward of MCU row my, the last ll MCUs on: the walk visits each MCU's units in order, then +# goes to the first MCU of the next row +def run.row( + +ll: Nat, + +mx: U32, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +kk: Nat, + +n1: Nat, + +hn: {1n+n1 == U32.to_nat(ns) : Nat}, + +hu: {Laws.jpg.units.ok(1n+n1, 0, sids, ids, hs, vs, True{}) == True{} : Bool}, + +hx: {Nat.add(U32.to_nat(mx), 1n+ll) == U32.to_nat(Jpeg.decode.ceil(ww, (hmax * 8 : U32))) : Nat} +) -> Run(Laws.jpg.o.row(1n+ll, mx, my, mcu, ns, sids, ids, hs, vs), Jpeg.Ctrl{0, 0, mx, my, mcu, 0}, + Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), Laws.jpg.idx(1n+ll, mcu), 0}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, + vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, kk): + match ll: + case 0n: + +em = {mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), + (mx + 1 : U32), my) : Jpeg.Ctrl} + +et = {Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), (mcu + 1 : U32), 0} : Jpeg.Ctrl} + %hn : Run(List.append(&2, Jpeg.Ctrl, Laws.jpg.o.comps(_, 0, mx, my, mcu, sids, ids, hs, vs), []), + Jpeg.Ctrl{0, 0, mx, my, mcu, 0}, et, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, + td, ta, ss, se, ah}, ri, kk) + run.nil(Laws.jpg.o.comps(1n+n1, 0, mx, my, mcu, sids, ids, hs, vs), Jpeg.Ctrl{0, 0, mx, my, mcu, 0}, et, + Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, kk, run.end(Laws.jpg.o.comps(1n+n1, 0, mx, my, mcu, sids, ids, + hs, vs), Jpeg.Ctrl{0, 0, mx, my, mcu, + 0}, em, et, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, + kk, run.comps(n1, 0, mx, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, + ri, kk, True{}, hn, hu), + Equal.cong(Bool, Jpeg.Ctrl, ib => mx.res(ib, (mcu + 1 : U32), (mx + 1 : U32), my), + U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), False{}, lt.last(mx, Jpeg.decode.ceil(ww, + (hmax * 8 : U32)), hx)))) + case 1n+(+pp): + +em = {mx.res(U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, (hmax * 8 : U32))), (mcu + 1 : U32), + (mx + 1 : U32), my) : Jpeg.Ctrl} + +c1 = {Jpeg.Ctrl{0, 0, (mx + 1 : U32), my, (mcu + 1 : U32), 0} : Jpeg.Ctrl} + +et = {Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), Laws.jpg.idx(1n+(1n+pp), mcu), 0} : Jpeg.Ctrl} + +l2 = {Laws.jpg.o.row(1n+pp, (mx + 1 : U32), my, (mcu + 1 : U32), ns, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + %hn : Run(List.append(&2, Jpeg.Ctrl, Laws.jpg.o.comps(_, 0, mx, my, mcu, sids, ids, hs, vs), l2), + Jpeg.Ctrl{0, 0, mx, my, mcu, 0}, et, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, + td, ta, ss, se, ah}, ri, kk) + run.cat(Laws.jpg.o.comps(1n+n1, 0, mx, my, mcu, sids, ids, hs, vs), l2, Jpeg.Ctrl{0, 0, mx, my, mcu, 0}, c1, et, + Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri, kk, run.end(Laws.jpg.o.comps(1n+n1, 0, mx, my, mcu, sids, ids, hs, vs), Jpeg.Ctrl{0, 0, mx, + my, mcu, 0}, em, c1, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri, Nat.add(List.length(&2, Jpeg.Ctrl, l2), kk), run.comps(n1, 0, mx, my, + mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, Nat.add(List.length(&2, + Jpeg.Ctrl, l2), kk), True{}, hn, hu), Equal.cong(Bool, Jpeg.Ctrl, + ib => mx.res(ib, (mcu + 1 : U32), (mx + 1 : U32), my), U32.is_lt((mx + 1 : U32), Jpeg.decode.ceil(ww, + (hmax * 8 : U32))), True{}, lt.more(mx, + Jpeg.decode.ceil(ww, + (hmax * 8 : U32)), pp, hx))), run.row(pp, (mx + 1 : U32), my, (mcu + 1 : U32), ww, hh, nf, ids, hs, vs, tq, + hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, kk, n1, hn, hu, lt.next(mx, + Jpeg.decode.ceil(ww, (hmax * 8 : U32)), pp, hx))) + +# where the walk is after mm MCU rows from row my, MCU number mcu, mw MCUs to a row +def rows.end(mm: Nat, +my: U32, +mcu: U32, +mw: U32) -> Jpeg.Ctrl: + match mm: + case 0n: + Jpeg.Ctrl{0, 0, 0, my, mcu, 0} + case 1n+pp: + rows.end(pp, (my + 1 : U32), Laws.jpg.idx(U32.to_nat(mw), mcu), mw) + +# MCU rows my onward, mm of them: the walk visits each row's MCUs in order +def run.rows( + +mm: Nat, + +my: U32, + +mcu: U32, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +kk: Nat, + +n1: Nat, + +hn: {1n+n1 == U32.to_nat(ns) : Nat}, + +hu: {Laws.jpg.units.ok(1n+n1, 0, sids, ids, hs, vs, True{}) == True{} : Bool}, + +w1: Nat, + +hw: {1n+w1 == U32.to_nat(Jpeg.decode.ceil(ww, (hmax * 8 : U32))) : Nat} +) -> Run(Laws.jpg.o.rows(mm, my, mcu, Jpeg.decode.ceil(ww, (hmax * 8 : U32)), ns, sids, ids, hs, vs), Jpeg.Ctrl{0, 0, + 0, my, mcu, 0}, + rows.end(mm, my, mcu, Jpeg.decode.ceil(ww, (hmax * 8 : U32))), Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, + vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, ri, kk): + match mm: + case 0n: + {==} + case 1n+(+pp): + +m2 = {Laws.jpg.idx(U32.to_nat(Jpeg.decode.ceil(ww, (hmax * 8 : U32))), mcu) : U32} + +c1 = {Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), m2, 0} : Jpeg.Ctrl} + +l2 = {Laws.jpg.o.rows(pp, (my + 1 : U32), m2, Jpeg.decode.ceil(ww, (hmax * 8 : U32)), ns, sids, ids, hs, + vs) : List<&2, Jpeg.Ctrl>} + +et = {rows.end(pp, (my + 1 : U32), m2, Jpeg.decode.ceil(ww, (hmax * 8 : U32))) : Jpeg.Ctrl} + %hw : Run(List.append(&2, Jpeg.Ctrl, Laws.jpg.o.row(_, 0, my, mcu, ns, sids, ids, hs, vs), l2), + Jpeg.Ctrl{0, 0, 0, my, mcu, 0}, et, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, + td, ta, ss, se, ah}, ri, kk) + run.cat(Laws.jpg.o.row(1n+w1, 0, my, mcu, ns, sids, ids, hs, vs), l2, Jpeg.Ctrl{0, 0, 0, my, mcu, 0}, c1, et, + Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, + ah}, ri, kk, run.end(Laws.jpg.o.row(1n+w1, 0, my, mcu, ns, sids, ids, hs, vs), Jpeg.Ctrl{0, 0, 0, my, + mcu, 0}, Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), Laws.jpg.idx(1n+w1, + mcu), 0}, c1, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, se, ah}, + ri, + Nat.add(List.length(&2, Jpeg.Ctrl, l2), kk), run.row(w1, 0, my, mcu, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, + ns, sids, td, ta, ss, se, ah, ri, Nat.add(List.length(&2, Jpeg.Ctrl, + l2), kk), n1, hn, hu, hw), Equal.cong(Nat, Jpeg.Ctrl, nn => {Jpeg.Ctrl{0, 0, 0, (my + 1 : U32), + Laws.jpg.idx(nn, + mcu), 0} : Jpeg.Ctrl}, 1n+w1, U32.to_nat(Jpeg.decode.ceil(ww, (hmax * 8 : U32))), hw)), run.rows(pp, + (my + 1 : U32), m2, + ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, kk, n1, hn, hu, w1, hw)) + +# jpeg_walk_frame: the decoder's trace from the scan's first block is the T.81 order +def walk.frame( + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +ns: U32, + +sids: List<&2, U32>, + +td: List<&2, U32>, + +ta: List<&2, U32>, + +ss: U32, + +se: U32, + +ah: U32, + +ri: U32, + +rst: U32, + +mh: U32, + +h_ns: {U32.is_lt(0, ns) == True{} : Bool}, + +h_mw: {U32.is_lt(0, Jpeg.decode.ceil(ww, (hmax * 8 : U32))) == True{} : Bool}, + +h_units: {Laws.jpg.units.ok(U32.to_nat(ns), 0, sids, ids, hs, vs, True{}) == True{} : Bool} +) -> {Laws.jpg.trace(List.length(&2, Jpeg.Ctrl, Laws.jpg.o.rows(U32.to_nat(mh), 0, 0, Jpeg.decode.ceil(ww, + (hmax * 8 : U32)), ns, sids, ids, hs, vs)), + Jpeg.Ctrl{0, 0, 0, 0, 0, rst}, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, Jpeg.Scan{ns, sids, td, ta, ss, + se, ah}, ri) == Laws.jpg.o.rows(U32.to_nat(mh), 0, 0, Jpeg.decode.ceil(ww, (hmax * 8 : U32)), ns, sids, ids, + hs, vs) : List<&2, Jpeg.Ctrl>}: + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + +sc = {Jpeg.Scan{ns, sids, td, ta, ss, se, ah} : Jpeg.Scan} + +ll = {Laws.jpg.o.rows(U32.to_nat(mh), 0, 0, Jpeg.decode.ceil(ww, (hmax * 8 : U32)), ns, sids, ids, hs, + vs) : List<&2, Jpeg.Ctrl>} + +ln = List.length(&2, Jpeg.Ctrl, ll) + +n1 = npred(U32.to_nat(ns)) + +hn = {pos.nat(ns, h_ns) : {1n+n1 == U32.to_nat(ns) : Nat}} + +c0 = {Jpeg.Ctrl{0, 0, 0, 0, 0, 0} : Jpeg.Ctrl} + +hu = {Equal.trans(Bool, Laws.jpg.units.ok(1n+n1, 0, sids, ids, hs, vs, True{}), Laws.jpg.units.ok(U32.to_nat(ns), + 0, sids, ids, hs, vs, True{}), True{}, Equal.cong(Nat, Bool, nn => Laws.jpg.units.ok(nn, 0, sids, ids, hs, vs, + True{}), 1n+n1, U32.to_nat(ns), hn), h_units) : {Laws.jpg.units.ok(1n+n1, 0, sids, ids, hs, vs, True{}) == True{} : + Bool}} + Equal.trans(List<&2, Jpeg.Ctrl>, Laws.jpg.trace(ln, Jpeg.Ctrl{0, 0, 0, 0, 0, rst}, fr, sc, ri), tr(ln, + Jpeg.Ctrl{0, 0, 0, 0, 0, rst}, fr, sc, ri), ll, trace.tr(ln, Jpeg.Ctrl{0, 0, 0, 0, 0, + rst}, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri), + Equal.trans(List<&2, Jpeg.Ctrl>, tr(ln, Jpeg.Ctrl{0, 0, 0, 0, 0, rst}, fr, sc, ri), tr(ln, c0, fr, sc, ri), ll, + tr.pos(ln, Jpeg.Ctrl{0, 0, 0, 0, 0, rst}, ww, hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, + ri), Equal.trans(List<&2, Jpeg.Ctrl>, tr(ln, c0, fr, sc, ri), + tr(Nat.add(ln, 0n), c0, fr, sc, ri), ll, Equal.cong(Nat, List<&2, Jpeg.Ctrl>, nn => tr(nn, c0, fr, sc, ri), ln, + Nat.add(ln, 0n), Equal.sym(Nat, Nat.add(ln, 0n), ln, R.add_zero(ln))), Equal.trans(List<&2, Jpeg.Ctrl>, + tr(Nat.add(ln, 0n), c0, fr, sc, ri), List.append(&2, Jpeg.Ctrl, ll, []), ll, run.rows(U32.to_nat(mh), 0, 0, ww, + hh, nf, ids, hs, vs, tq, hmax, vmax, ns, sids, td, ta, ss, se, ah, ri, + 0n, n1, hn, hu, npred(U32.to_nat(Jpeg.decode.ceil(ww, (hmax * 8 : U32)))), pos.nat(Jpeg.decode.ceil(ww, + (hmax * 8 : U32)), h_mw)), app.nil(ll))))) + +# ---- IMG-JPG-3: stuffing, the header walk, the entropy walk, the frame size ---- + +# a stuffed list stays refused once a 255 was not followed by a 0 +def st.false(xs: List<&2, U32>, ff: Bool) -> {Laws.jpg.stuffed(xs, ff, False{}) == False{} : Bool}: + match xs: + case Nil{}: + {==} + case +bb <> rest: + match ff: + case True{}: + st.false(rest, False{}) + case False{}: + st.false(rest, U32.is_eq(bb, 255)) + +# one byte stuffed in front of stuffed bytes keeps them stuffed +def st.put( + ff: Bool, + +bb: U32, + +acc: List<&2, U32>, + +ee: {U32.is_eq(bb, 255) == ff : Bool}, + hh: {Laws.jpg.stuffed(acc, False{}, True{}) == True{} : Bool} +) -> {Laws.jpg.stuffed(Jenc.encode.stuff.put(ff, bb, acc), False{}, True{}) == True{} : Bool}: + match ff: + case True{}: + es = Equal.sym(Bool, U32.is_eq(bb, 255), True{}, ee) + %es : {Laws.jpg.stuffed(0 <> acc, _, True{}) == True{} : Bool} + hh + case False{}: + es = Equal.sym(Bool, U32.is_eq(bb, 255), False{}, ee) + %es : {Laws.jpg.stuffed(acc, _, True{}) == True{} : Bool} + hh + +# every byte of a written list stuffed onto stuffed bytes gives stuffed bytes +def st.all( + out: List<&2, U32>, + +acc: List<&2, U32>, + hh: {Laws.jpg.stuffed(acc, False{}, True{}) == True{} : Bool} +) -> {Laws.jpg.stuffed(Jenc.encode.stuff.all(out, acc), False{}, True{}) == True{} : Bool}: + match out: + case Nil{}: + hh + case +bb <> rest: + st.all(rest, Jenc.encode.stuff.put(U32.is_eq(bb, 255), bb, acc), st.put(U32.is_eq(bb, 255), bb, acc, {==}, hh)) + +# the entropy-coded bytes the encoder flushes are stuffed, whatever it wrote +def st.pad(pp: Jenc.Put) -> {Laws.jpg.stuffed(Jenc.encode.pad(pp), False{}, True{}) == True{} : Bool}: + match pp: + case Jenc.Put{out, +buf, +nn}: + st.all(Jenc.encode.pad.n(U32.is_eq(nn, 0), out, buf, nn), [], {==}) + +# each of the encoder's three paths ends in a flush +def st.disp( + neu: Bool, + sol: Bool, + +color: U32, + px: List<&2, U32>, + +ww: U32, + +hh: U32 +) -> {Laws.jpg.stuffed(Jenc.encode.dispatch.b(neu, sol, color, px, ww, hh), False{}, True{}) == True{} : Bool}: + match neu: + case True{}: + st.pad(Jenc.encode.neutral.mcus(U32.to_nat((U32.div((ww + 7 : U32), 8) * U32.div((hh + 7 : U32), 8) : U32)), + Jenc.encode.put0())) + case False{}: + match sol: + case True{}: + st.pad(Jenc.encode.neutral.mcus(U32.to_nat(((U32.div((ww + 7 : U32), 8) * U32.div((hh + 7 : U32), 8) : U32) - + 1 : U32)), Jenc.encode.solid.y(Array.set(U32, Jpeg.decode.plane(1), 0, color), + Jenc.encode.book(Jenc.encode.dccounts(), Jenc.encode.dcsyms(), Jenc.encode.accounts(), + Jenc.encode.acsyms()), Jenc.encode.put0(), Jenc.encode.ctx()))) + case False{}: + st.pad(Jenc.encode.mcus(U32.to_nat((U32.div((ww + 7 : U32), 8) * U32.div((hh + 7 : U32), 8) : U32)), + (Jenc.encode.pix.load(U32.to_nat((ww * hh : U32)), px, Jpeg.decode.plane((ww * hh : U32)), 0), + Jenc.encode.book(Jenc.encode.dccounts(), Jenc.encode.dcsyms(), Jenc.encode.accounts(), + Jenc.encode.acsyms()), 0, 0, 0, Jenc.encode.put0()), 0, 0, U32.div((ww + 7 : U32), 8), ww, hh, + Jenc.encode.ctx())) + +# the watch's answer, whatever it is, dispatches to stuffed bytes +def st.use( + got: U32 & U32 & List<&2, U32>, + +ww: U32, + +hh: U32 +) -> {Laws.jpg.stuffed(Jenc.encode.arm.use(got, ww, hh), False{}, True{}) == True{} : Bool}: + match got: + case (+tag, +color, px): + st.disp(U32.is_eq(tag, 0), U32.is_eq(tag, 1), color, px, ww, hh) + +# the phase the entropy walk is in: after a 255, or not +def ent.ph(ff: Bool) -> Jpeg.Phase: + match ff: + case True{}: + Jpeg.EntFF{} + case False{}: + Jpeg.Ent{} + +# the bytes the entropy walk holds: a 255 just read is not yet among them +def ent.acc(ff: Bool, +en: List<&2, U32>) -> List<&2, U32>: + match ff: + case True{}: + 255 <> en + case False{}: + en + +# what the entropy walk holds after one byte: a 255 is held back until its pair is read +def ent.hold(ff: Bool, +bb: U32, +en: List<&2, U32>) -> List<&2, U32>: + match ff: + case True{}: + +_b = (bb - bb : U32) + en + case False{}: + bb <> en + +# the entropy walk from after one byte, as ent.go gives it +def ent.Ih( + ff: Bool, + +bb: U32, + +rest: List<&2, U32>, + +frame: Jpeg.Frame, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +en: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32 +) -> Type: + {Jpeg.decode.walk(List.append(&2, U32, rest, [255, 217]), Jpeg.St{ent.ph(ff), frame, scan, tabs, ent.hold(ff, bb, + en), ri, kind, bad}) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, rest, ent.acc(ff, + ent.hold(ff, bb, en))), ri, kind, bad} : Jpeg.St} + +# the entropy walk over one byte that is not after a 255: 255 opens a pair, any other is kept +def ent.one( + ff: Bool, + +bb: U32, + +rest: List<&2, U32>, + +frame: Jpeg.Frame, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +en: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32, + +ee: {U32.is_eq(bb, 255) == ff : Bool}, + ih: ent.Ih(ff, bb, rest, frame, scan, tabs, en, ri, kind, bad) +) -> {Jpeg.decode.walk(List.append(&2, U32, bb <> rest, [255, 217]), Jpeg.St{Jpeg.Ent{}, frame, scan, tabs, en, ri, + kind, bad}) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, bb <> rest, en), ri, kind, bad} : + Jpeg.St}: + match ff: + case True{}: + es = Equal.sym(Bool, U32.is_eq(bb, 255), True{}, ee) + eb = Equal.sym(U32, bb, 255, U32L.ueq(bb, 255, ee)) + %es : {Jpeg.decode.walk(List.append(&2, U32, rest, [255, 217]), Jpeg.decode.step.ent(_, bb, frame, scan, tabs, + en, ri, kind, bad)) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, rest, bb <> en), ri, + kind, bad} : Jpeg.St} + %eb : {Jpeg.decode.walk(List.append(&2, U32, rest, [255, 217]), Jpeg.decode.step.ent(True{}, bb, frame, scan, + tabs, en, ri, kind, bad)) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, rest, _ <> en), + ri, + kind, bad} : Jpeg.St} + ih + case False{}: + es = Equal.sym(Bool, U32.is_eq(bb, 255), False{}, ee) + %es : {Jpeg.decode.walk(List.append(&2, U32, rest, [255, 217]), Jpeg.decode.step.ent(_, bb, frame, scan, tabs, + en, ri, kind, bad)) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, rest, bb <> en), ri, + kind, bad} : Jpeg.St} + ih + +# after a 255 the next byte of stuffed bytes is 0 +def ent.zero( + zb: Bool, + rest: List<&2, U32>, + +hh: {Laws.jpg.stuffed(rest, False{}, zb) == True{} : Bool} +) -> {zb == True{} : Bool}: + match zb: + case True{}: + {==} + case False{}: + Empty.absurd({False{} == True{} : Bool}, U32L.false_true(Equal.trans(Bool, False{}, Laws.jpg.stuffed(rest, + False{}, False{}), True{}, Equal.sym(Bool, Laws.jpg.stuffed(rest, False{}, False{}), False{}, st.false(rest, + False{})), hh))) + +# the entropy walk over stuffed bytes, then EOI: every byte kept, in reverse, onto what it held, and a 255 +# it had just read put back in front of them +def ent.go( + +xs: List<&2, U32>, + ff: Bool, + +frame: Jpeg.Frame, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +en: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32, + +hh: {Laws.jpg.stuffed(xs, ff, True{}) == True{} : Bool} +) -> {Jpeg.decode.walk(List.append(&2, U32, xs, [255, 217]), Jpeg.St{ent.ph(ff), frame, scan, tabs, en, ri, kind, + bad}) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, xs, ent.acc(ff, en)), ri, kind, bad} : + Jpeg.St}: + match xs: + case Nil{}: + match ff: + case False{}: + {==} + case True{}: + Empty.absurd({Jpeg.decode.walk([255, 217], Jpeg.St{Jpeg.EntFF{}, frame, scan, tabs, en, ri, kind, bad}) == + Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, 255 <> en, ri, kind, bad} : Jpeg.St}, U32L.false_true(hh)) + case +bb <> +rest: + match ff: + case False{}: + ent.one(U32.is_eq(bb, 255), bb, rest, frame, scan, tabs, en, ri, kind, bad, {==}, ent.go(rest, + U32.is_eq(bb, 255), frame, scan, tabs, ent.hold(U32.is_eq(bb, 255), bb, en), ri, kind, bad, hh)) + case True{}: + +ez = {ent.zero(U32.is_eq(bb, 0), rest, hh) : {U32.is_eq(bb, 0) == True{} : Bool}} + eb = Equal.sym(U32, bb, 0, U32L.ueq(bb, 0, ez)) + %eb : {Jpeg.decode.walk(List.append(&2, U32, _ <> rest, [255, 217]), Jpeg.St{Jpeg.EntFF{}, frame, scan, tabs, + en, ri, kind, bad}) == Jpeg.St{Jpeg.Stop{}, frame, scan, tabs, List.reverse.go(&2, U32, _ <> rest, + 255 <> en), ri, kind, bad} : Jpeg.St} + h2 = Equal.trans(Bool, Laws.jpg.stuffed(rest, False{}, True{}), Laws.jpg.stuffed(rest, False{}, + U32.is_eq(bb, 0)), True{}, Equal.cong(Bool, Bool, zb => Laws.jpg.stuffed(rest, False{}, zb), True{}, + U32.is_eq(bb, 0), Equal.sym(Bool, U32.is_eq(bb, 0), True{}, ez)), hh) + ent.go(rest, False{}, frame, scan, tabs, 0 <> (255 <> en), ri, kind, bad, h2) + +# the decoder's u16 of the high and low bytes the encoder writes for a size is the size +def u16.eq(+ww: U32) -> {Jpeg.decode.u16(U32.shrn(ww, 8n), U32.and(ww, 255)) == ww : U32}: + Equal.trans(U32, Jpeg.decode.u16(U32.shrn(ww, 8n), U32.and(ww, 255)), Jpeg.decode.u16(U32.shrn(ww, 8n), + U32.and(255, ww)), ww, Equal.cong(U32, U32, xx => Jpeg.decode.u16(U32.shrn(ww, 8n), xx), U32.and(ww, 255), + U32.and(255, ww), uand_comm(ww, 255)), u16_bits(ww)) + +# a raster of width ww and height hh has that size +def sized.pic( + +ww: U32, + +hh: U32, + px: List<&2, U32> +) -> {Laws.jpg.sized(Some{Img.Raster{ww, hh, px}}, ww, hh) == True{} : Bool}: + Equal.trans(Bool, Bool.and(U32.is_eq(ww, ww), U32.is_eq(hh, hh)), Bool.and(True{}, U32.is_eq(hh, hh)), True{}, + Equal.cong(Bool, Bool, bb => Bool.and(bb, U32.is_eq(hh, hh)), U32.is_eq(ww, ww), True{}, U32L.u32_eq_refl(ww)), + U32L.u32_eq_refl(hh)) + +# three components: a colour picture of the frame's size, or none +def nf3.sized( + three: Bool, + +ww: U32, + +hh: U32, + yy: Array, + cb: Array, + cr: Array +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.done.nf3(three, ww, hh, yy, cb, cr)), ww, hh) == True{} : Bool}: + match three: + case True{}: + +nn = U32.to_nat((ww * hh : U32)) + sized.pic(ww, hh, Jpeg.decode.rgbs(Jpeg.decode.points(nn, yy), Jpeg.decode.points(nn, cb), + Jpeg.decode.points(nn, cr))) + case False{}: + -_y = yy + -_b = cb + -_r = cr + {==} + +# one component: a gray picture of the frame's size; any other count as above +def nf1.sized( + one: Bool, + +nf: U32, + +ww: U32, + +hh: U32, + yy: Array, + cb: Array, + cr: Array +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.done.nf1(one, nf, ww, hh, yy, cb, cr)), ww, hh) == True{} : + Bool}: + match one: + case True{}: + -_b = cb + -_r = cr + sized.pic(ww, hh, Jpeg.decode.grays(Jpeg.decode.points(U32.to_nat((ww * hh : U32)), yy))) + case False{}: + nf3.sized(U32.is_eq(nf, 3), ww, hh, yy, cb, cr) + +# the planes of a finished scan as a picture of the frame's size, or none +def dok.sized( + bad: Bool, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + yy: Array, + cb: Array, + cr: Array +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.done.ok(bad, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, + yy, cb, cr)), ww, hh) == True{} : Bool}: + match bad: + case True{}: + -_y = yy + -_b = cb + -_r = cr + {==} + case False{}: + nf1.sized(U32.is_eq(nf, 1), nf, ww, hh, yy, cb, cr) + +# the block loop ends in a picture of the frame's size, or none +def blocks.sized( + left: Nat, + blk: Jpeg.Blk, + +ctrl: Jpeg.Ctrl, + +preds: Jpeg.Preds, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +ri: U32, + yy: Array, + cb: Array, + cr: Array, + +ok: U32 +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.blocks(left, blk, ctrl, preds, Jpeg.Frame{ww, hh, nf, ids, hs, vs, + tq, hmax, vmax}, scan, tabs, ri, yy, cb, cr, ok)), ww, hh) == True{} : Bool}: + match left: + case 0n: + match blk: + case Jpeg.Blk{+samples, _bits, _pred, +bok}: + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + dok.sized(U32.is_eq((ok * bok : U32), 0), ww, hh, nf, ids, hs, vs, tq, hmax, vmax, + Jpeg.decode.paint.use(Jpeg.decode.geom(ctrl, fr, scan), U32.is_eq(Jpeg.decode.ctrl.comp(ctrl), 0), samples, + yy), Jpeg.decode.paint.use(Jpeg.decode.geom(ctrl, fr, scan), U32.is_eq(Jpeg.decode.ctrl.comp(ctrl), 1), + samples, cb), Jpeg.decode.paint.use(Jpeg.decode.geom(ctrl, fr, scan), U32.is_eq(Jpeg.decode.ctrl.comp(ctrl), + 2), samples, cr)) + case 1n+pp: + match blk: + case Jpeg.Blk{+samples, +bits, +pred, +bok}: + match ctrl: + case Jpeg.Ctrl{+comp, _bi, _mx, _my, _mcu, _rst}: + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + blocks.sized(pp, Jpeg.decode.block.next(bits, preds, pred, ctrl, fr, scan, tabs, ri), + Jpeg.decode.adv.ctrl(Jpeg.decode.adv(ctrl, fr, scan, ri)), + Jpeg.decode.preds.next(Jpeg.decode.adv.duef(Jpeg.decode.adv(ctrl, fr, scan, ri)), preds, comp, + pred), ww, + hh, nf, ids, hs, vs, tq, hmax, vmax, scan, tabs, ri, Jpeg.decode.paint.use(Jpeg.decode.geom(ctrl, fr, + scan), U32.is_eq(comp, 0), samples, yy), Jpeg.decode.paint.use(Jpeg.decode.geom(ctrl, fr, scan), + U32.is_eq(comp, 1), samples, cb), Jpeg.decode.paint.use(Jpeg.decode.geom(ctrl, fr, scan), + U32.is_eq(comp, 2), samples, cr), (ok * bok : U32)) + +# the scan decode from its first block: a picture of the frame's size, or none +def start.sized( + nn: Nat, + bits: Jpeg.Bits, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + +ri: U32, + yy: Array, + cb: Array, + cr: Array +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.start(nn, bits, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, + vmax}, scan, tabs, ri, yy, cb, cr)), ww, hh) == True{} : Bool}: + match nn: + case 0n: + -_s = bits + -_y = yy + -_b = cb + -_r = cr + {==} + case 1n+pp: + +fr = {Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax} : Jpeg.Frame} + blocks.sized(pp, Jpeg.decode.block.of(bits, 0, Jpeg.decode.pred.zero(), fr, scan, tabs), Jpeg.Ctrl{0, 0, 0, 0, 0, + 0}, Jpeg.decode.pred.zero(), ww, hh, nf, ids, hs, vs, tq, hmax, vmax, scan, tabs, ri, yy, cb, cr, 1) + +# a frame with a side of 0 is none; any other is decoded from its first block +def runn.sized( + empty: Bool, + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + ent: List<&2, U32>, + +ri: U32 +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.run.n(empty, ww, hh, Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, + vmax}, scan, tabs, ent, ri)), ww, hh) == True{} : Bool}: + match empty: + case True{}: + -_e = ent + {==} + case False{}: + start.sized(U32.to_nat(Jpeg.decode.nblocks(ww, hh, hs, vs, hmax, vmax)), Jpeg.Bits{0, 1, 0, ent}, ww, hh, nf, + ids, hs, vs, tq, hmax, vmax, scan, + tabs, ri, Jpeg.decode.plane((ww * hh : U32)), Jpeg.decode.plane((ww * hh : U32)), + Jpeg.decode.plane((ww * hh : U32))) + +# jpeg_run_sized: the scan decode is none or a picture of the frame's size +def run.sized( + +ww: U32, + +hh: U32, + +nf: U32, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +tq: List<&2, U32>, + +hmax: U32, + +vmax: U32, + +scan: Jpeg.Scan, + +tabs: Jpeg.Tabs, + ent: List<&2, U32>, + +ri: U32 +) -> {Laws.jpg.sized(Img.decode_jpeg.out(Jpeg.decode.run(Jpeg.Frame{ww, hh, nf, ids, hs, vs, tq, hmax, vmax}, scan, + tabs, ent, ri)), ww, hh) == True{} : Bool}: + runn.sized(Bool.or(U32.is_eq(ww, 0), U32.is_eq(hh, 0)), ww, hh, nf, ids, hs, vs, tq, hmax, vmax, scan, tabs, ent, ri) + +# ---- the decoder's block count (IMG-JPG-2) ---- + +# the length of a component's units in the order +def len.units( + +kk: Nat, + +comp: U32, + +bi: U32, + +mx: U32, + +my: U32, + +mcu: U32 +) -> {List.length(&2, Jpeg.Ctrl, Laws.jpg.o.units(kk, comp, bi, mx, my, mcu)) == kk : Nat}: + match kk: + case 0n: + {==} + case 1n+(+pp): + Equal.cong(Nat, Nat, nn => 1n+nn, List.length(&2, Jpeg.Ctrl, Laws.jpg.o.units(pp, comp, (bi + 1 : U32), mx, my, + mcu)), pp, len.units(pp, comp, (bi + 1 : U32), mx, my, mcu)) + +# the length of an MCU's components in the order: their data units summed +def len.comps( + +nn: Nat, + +comp: U32, + +mx: U32, + +my: U32, + +mcu: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> {List.length(&2, Jpeg.Ctrl, Laws.jpg.o.comps(nn, comp, mx, my, mcu, sids, ids, hs, vs)) == Laws.jpg.usum(nn, + comp, sids, ids, hs, vs) : Nat}: + match nn: + case 0n: + {==} + case 1n+(+pp): + +un = U32.to_nat(Laws.jpg.units(comp, sids, ids, hs, vs)) + +l1 = {Laws.jpg.o.units(un, comp, 0, mx, my, mcu) : List<&2, Jpeg.Ctrl>} + +l2 = {Laws.jpg.o.comps(pp, (comp + 1 : U32), mx, my, mcu, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + +s2 = Laws.jpg.usum(pp, (comp + 1 : U32), sids, ids, hs, vs) + Equal.trans(Nat, List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), Nat.add(List.length(&2, + Jpeg.Ctrl, l1), List.length(&2, Jpeg.Ctrl, l2)), Nat.add(un, s2), len.app(l1, l2), Equal.trans(Nat, + Nat.add(List.length(&2, Jpeg.Ctrl, l1), List.length(&2, Jpeg.Ctrl, l2)), Nat.add(un, List.length(&2, + Jpeg.Ctrl, l2)), Nat.add(un, s2), Equal.cong(Nat, Nat, xx => Nat.add(xx, List.length(&2, Jpeg.Ctrl, l2)), + List.length(&2, Jpeg.Ctrl, l1), un, len.units(un, comp, 0, mx, my, mcu)), Equal.cong(Nat, Nat, + xx => Nat.add(un, xx), List.length(&2, Jpeg.Ctrl, l2), s2, len.comps(pp, (comp + 1 : U32), mx, my, mcu, sids, + ids, hs, vs)))) + +# the length of an MCU row in the order: its MCUs times the data units of one +def len.row( + +kk: Nat, + +mx: U32, + +my: U32, + +mcu: U32, + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> {List.length(&2, Jpeg.Ctrl, Laws.jpg.o.row(kk, mx, my, mcu, ns, sids, ids, hs, vs)) == Nat.mul(kk, + Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)) : Nat}: + match kk: + case 0n: + {==} + case 1n+(+pp): + +uu = Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs) + +l1 = {Laws.jpg.o.comps(U32.to_nat(ns), 0, mx, my, mcu, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + +l2 = {Laws.jpg.o.row(pp, (mx + 1 : U32), my, (mcu + 1 : U32), ns, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + Equal.trans(Nat, List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), Nat.add(List.length(&2, + Jpeg.Ctrl, l1), List.length(&2, Jpeg.Ctrl, l2)), Nat.add(uu, Nat.mul(pp, uu)), len.app(l1, l2), + Equal.trans(Nat, Nat.add(List.length(&2, Jpeg.Ctrl, l1), List.length(&2, Jpeg.Ctrl, l2)), Nat.add(uu, + List.length(&2, Jpeg.Ctrl, l2)), Nat.add(uu, Nat.mul(pp, uu)), Equal.cong(Nat, Nat, xx => Nat.add(xx, + List.length(&2, Jpeg.Ctrl, l2)), List.length(&2, Jpeg.Ctrl, l1), uu, len.comps(U32.to_nat(ns), 0, mx, my, mcu, + sids, ids, hs, vs)), Equal.cong(Nat, Nat, xx => Nat.add(uu, xx), List.length(&2, Jpeg.Ctrl, l2), Nat.mul(pp, + uu), len.row(pp, (mx + 1 : U32), my, (mcu + 1 : U32), ns, sids, ids, hs, vs)))) + +# the length of the order over mm MCU rows +def len.rows( + +mm: Nat, + +my: U32, + +mcu: U32, + +mw: U32, + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> {List.length(&2, Jpeg.Ctrl, Laws.jpg.o.rows(mm, my, mcu, mw, ns, sids, ids, hs, vs)) == Nat.mul(mm, + Nat.mul(U32.to_nat(mw), Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs))) : Nat}: + match mm: + case 0n: + {==} + case 1n+(+pp): + +ru = Nat.mul(U32.to_nat(mw), Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)) + +l1 = {Laws.jpg.o.row(U32.to_nat(mw), 0, my, mcu, ns, sids, ids, hs, vs) : List<&2, Jpeg.Ctrl>} + +l2 = {Laws.jpg.o.rows(pp, (my + 1 : U32), Laws.jpg.idx(U32.to_nat(mw), mcu), mw, ns, sids, ids, hs, vs) : + List<&2, Jpeg.Ctrl>} + Equal.trans(Nat, List.length(&2, Jpeg.Ctrl, List.append(&2, Jpeg.Ctrl, l1, l2)), Nat.add(List.length(&2, + Jpeg.Ctrl, l1), List.length(&2, Jpeg.Ctrl, l2)), Nat.add(ru, Nat.mul(pp, ru)), len.app(l1, l2), + Equal.trans(Nat, Nat.add(List.length(&2, Jpeg.Ctrl, l1), List.length(&2, Jpeg.Ctrl, l2)), Nat.add(ru, + List.length(&2, Jpeg.Ctrl, l2)), Nat.add(ru, Nat.mul(pp, ru)), Equal.cong(Nat, Nat, xx => Nat.add(xx, + List.length(&2, Jpeg.Ctrl, l2)), List.length(&2, Jpeg.Ctrl, l1), ru, len.row(U32.to_nat(mw), 0, my, mcu, ns, + sids, ids, hs, vs)), Equal.cong(Nat, Nat, xx => Nat.add(ru, xx), List.length(&2, Jpeg.Ctrl, l2), Nat.mul(pp, + ru), len.rows(pp, (my + 1 : U32), Laws.jpg.idx(U32.to_nat(mw), mcu), mw, ns, sids, ids, hs, vs)))) + +# multiplication is associative +def mul.assoc(+aa: Nat, +bb: Nat, +cc: Nat) -> {Nat.mul(Nat.mul(aa, bb), cc) == Nat.mul(aa, Nat.mul(bb, cc)) : Nat}: + match aa: + case 0n: + {==} + case 1n+(+pp): + Equal.trans(Nat, Nat.mul(Nat.add(bb, Nat.mul(pp, bb)), cc), Nat.add(Nat.mul(bb, cc), Nat.mul(Nat.mul(pp, bb), + cc)), Nat.add(Nat.mul(bb, cc), Nat.mul(pp, Nat.mul(bb, cc))), R.mul_add(bb, Nat.mul(pp, bb), cc), + Equal.cong(Nat, Nat, xx => Nat.add(Nat.mul(bb, cc), xx), Nat.mul(Nat.mul(pp, bb), cc), Nat.mul(pp, + Nat.mul(bb, cc)), mul.assoc(pp, bb, cc))) + +# x is at most x times a positive number +def le.mulr(+xx: Nat, +uu: Nat, +hu: {1n+npred(uu) == uu : Nat}) -> {Nat.is_le(xx, Nat.mul(xx, uu)) == True{} : Bool}: + +u1 = npred(uu) + Equal.trans(Bool, Nat.is_le(xx, Nat.mul(xx, uu)), Nat.is_le(xx, Nat.add(xx, Nat.mul(xx, u1))), True{}, + Equal.cong(Nat, Bool, nn => Nat.is_le(xx, nn), Nat.mul(xx, uu), Nat.add(xx, Nat.mul(xx, u1)), Equal.trans(Nat, + Nat.mul(xx, uu), Nat.mul(xx, 1n+u1), Nat.add(xx, Nat.mul(xx, u1)), Equal.cong(Nat, Nat, nn => Nat.mul(xx, nn), uu, + 1n+u1, Equal.sym(Nat, 1n+u1, uu, hu)), R.mul_succ(xx, u1))), R.le_add_more(xx, xx, Nat.mul(xx, u1), + R.le_refl(xx))) + +# the scan has at least one data unit per MCU +def usum.pos( + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +h_ns: {U32.is_lt(0, ns) == True{} : Bool}, + +h_units: {Laws.jpg.units.ok(U32.to_nat(ns), 0, sids, ids, hs, vs, True{}) == True{} : Bool} +) -> {1n+npred(Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)) == Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, + hs, vs) : Nat}: + +n1 = npred(U32.to_nat(ns)) + +hn = {pos.nat(ns, h_ns) : {1n+n1 == U32.to_nat(ns) : Nat}} + +u0 = Laws.jpg.units(0, sids, ids, hs, vs) + +hu = {Equal.trans(Bool, Laws.jpg.units.ok(1n+n1, 0, sids, ids, hs, vs, True{}), Laws.jpg.units.ok(U32.to_nat(ns), + 0, sids, ids, hs, vs, True{}), True{}, Equal.cong(Nat, Bool, nn => Laws.jpg.units.ok(nn, 0, sids, ids, hs, vs, + True{}), 1n+n1, U32.to_nat(ns), hn), h_units) : {Laws.jpg.units.ok(1n+n1, 0, sids, ids, hs, vs, True{}) == True{} : + Bool}} + +hp = {uok.acc(n1, 1, sids, ids, hs, vs, U32.is_lt(0, u0), hu) : {U32.is_lt(0, u0) == True{} : Bool}} + +k0 = npred(U32.to_nat(u0)) + +rest = Laws.jpg.usum(n1, 1, sids, ids, hs, vs) + succ.of(Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs), Equal.trans(Bool, Nat.is_lt(0n, + Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)), Nat.is_lt(0n, Nat.add(U32.to_nat(u0), rest)), True{}, + Equal.cong(Nat, Bool, nn => Nat.is_lt(0n, Laws.jpg.usum(nn, 0, sids, ids, hs, vs)), U32.to_nat(ns), 1n+n1, + Equal.sym(Nat, 1n+n1, U32.to_nat(ns), hn)), Equal.cong(Nat, Bool, nn => Nat.is_lt(0n, Nat.add(nn, rest)), + U32.to_nat(u0), 1n+k0, Equal.sym(Nat, 1n+k0, U32.to_nat(u0), pos.nat(u0, hp))))) + +# the scan's data units per MCU are one more than their predecessor +def usum.Pos(+ns: U32, +sids: List<&2, U32>, +ids: List<&2, U32>, +hs: List<&2, U32>, +vs: List<&2, U32>) -> Type: + {1n+npred(Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)) == Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs) + : Nat} + +# the blocks of a frame of mw by mh MCUs, as a number +def fit.n( + +mw: U32, + +mh: U32, + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32> +) -> Nat: + Nat.mul(Nat.mul(U32.to_nat(mw), U32.to_nat(mh)), Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs)) + +# jpeg_walk_count: the decoder's U32 block count is the order's length +def walk.count( + +mw: U32, + +mh: U32, + +bs: U32, + +ns: U32, + +sids: List<&2, U32>, + +ids: List<&2, U32>, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +top: U32, + h_pos: usum.Pos(ns, sids, ids, hs, vs), + +h_sum: {U32.to_nat(bs) == Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs) : Nat}, + +h_fit: {Nat.is_le(fit.n(mw, mh, ns, sids, ids, hs, vs), U32.to_nat(top)) == True{} : Bool} +) -> {U32.to_nat((mw * mh * bs : U32)) == List.length(&2, Jpeg.Ctrl, Laws.jpg.o.rows(U32.to_nat(mh), 0, 0, mw, ns, + sids, ids, hs, vs)) : Nat}: + +uu = Laws.jpg.usum(U32.to_nat(ns), 0, sids, ids, hs, vs) + +wn = U32.to_nat(mw) + +hn = U32.to_nat(mh) + +in = {R.u32_mul_below(mw, mh, top, R.le_trans(Nat.mul(wn, hn), Nat.mul(Nat.mul(wn, hn), uu), U32.to_nat(top), + le.mulr(Nat.mul(wn, hn), uu, h_pos), h_fit)) : {U32.to_nat((mw * mh : U32)) == Nat.mul(wn, hn) : Nat}} + +eo = {Equal.trans(Nat, Nat.mul(U32.to_nat((mw * mh : U32)), U32.to_nat(bs)), Nat.mul(Nat.mul(wn, hn), + U32.to_nat(bs)), Nat.mul(Nat.mul(wn, hn), uu), Equal.cong(Nat, Nat, nn => Nat.mul(nn, U32.to_nat(bs)), + U32.to_nat((mw * mh : U32)), Nat.mul(wn, hn), in), Equal.cong(Nat, Nat, nn => Nat.mul(Nat.mul(wn, hn), nn), + U32.to_nat(bs), uu, h_sum)) : {Nat.mul(U32.to_nat((mw * mh : U32)), U32.to_nat(bs)) == Nat.mul(Nat.mul(wn, hn), uu) + : Nat}} + +out = {R.u32_mul_below((mw * mh : U32), bs, top, Equal.trans(Bool, Nat.is_le(Nat.mul(U32.to_nat((mw * mh : U32)), + U32.to_nat(bs)), U32.to_nat(top)), Nat.is_le(Nat.mul(Nat.mul(wn, hn), uu), U32.to_nat(top)), True{}, + Equal.cong(Nat, Bool, nn => Nat.is_le(nn, U32.to_nat(top)), Nat.mul(U32.to_nat((mw * mh : U32)), U32.to_nat(bs)), + Nat.mul(Nat.mul(wn, hn), uu), eo), h_fit)) : {U32.to_nat((mw * mh * bs : U32)) == Nat.mul(U32.to_nat((mw * mh : + U32)), U32.to_nat(bs)) : Nat}} + Equal.trans(Nat, U32.to_nat((mw * mh * bs : U32)), Nat.mul(Nat.mul(wn, hn), uu), List.length(&2, Jpeg.Ctrl, + Laws.jpg.o.rows(hn, 0, 0, mw, ns, sids, ids, hs, vs)), Equal.trans(Nat, U32.to_nat((mw * mh * bs : U32)), + Nat.mul(U32.to_nat((mw * mh : U32)), U32.to_nat(bs)), Nat.mul(Nat.mul(wn, hn), uu), out, eo), Equal.trans(Nat, + Nat.mul(Nat.mul(wn, hn), uu), Nat.mul(Nat.mul(hn, wn), uu), List.length(&2, Jpeg.Ctrl, Laws.jpg.o.rows(hn, 0, 0, + mw, ns, sids, ids, hs, vs)), Equal.cong(Nat, Nat, nn => Nat.mul(nn, uu), Nat.mul(wn, hn), Nat.mul(hn, wn), + R.mul_comm(wn, hn)), Equal.trans(Nat, Nat.mul(Nat.mul(hn, wn), uu), Nat.mul(hn, Nat.mul(wn, uu)), List.length(&2, + Jpeg.Ctrl, Laws.jpg.o.rows(hn, 0, 0, mw, ns, sids, ids, hs, vs)), mul.assoc(hn, wn, uu), Equal.sym(Nat, + List.length(&2, Jpeg.Ctrl, Laws.jpg.o.rows(hn, 0, 0, mw, ns, sids, ids, hs, vs)), Nat.mul(hn, Nat.mul(wn, uu)), + len.rows(hn, 0, 0, mw, ns, sids, ids, hs, vs))))) + +# ---- stuffing and unstuffing (IMG-JPG-3) ---- + +# bytes stuffed in order onto acc, the first byte first +def stf(xs: List<&2, U32>, +acc: List<&2, U32>) -> List<&2, U32>: + match xs: + case Nil{}: + acc + case +bb <> rest: + Jenc.encode.stuff.put(U32.is_eq(bb, 255), bb, stf(rest, acc)) + +# the encoder stuffing written bytes, newest first, is stuffing them in order +def stall.rev( + xs: List<&2, U32>, + +rr: List<&2, U32>, + +acc: List<&2, U32> +) -> {Jenc.encode.stuff.all(List.reverse.go(&2, U32, xs, rr), acc) == Jenc.encode.stuff.all(rr, stf(xs, acc)) : + List<&2, U32>}: + match xs: + case Nil{}: + {==} + case +bb <> rest: + stall.rev(rest, bb <> rr, acc) + +# a byte that is not 255, read by the bit reader: its eight bits, top first, each or-ed with False +def rd.plain( + h0: Bool, + +c0: Bool, + +c1: Bool, + +c2: Bool, + +c3: Bool, + +c4: Bool, + +c5: Bool, + +c6: Bool, + +c7: Bool, + +rest: List<&2, U32>, + +ok: U32 +) -> {Jpeg.decode.nbits(8n, True{}, W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7) <> rest, False{}, False{}, h0, 0, 0, ok, + 0) == (Jpeg.Bits{0, ok, 0, rest}, W7.byte.w(Bool.or(c0, False{}), Bool.or(c1, False{}), Bool.or(c2, False{}), + Bool.or(c3, False{}), Bool.or(c4, False{}), Bool.or(c5, False{}), Bool.or(c6, False{}), Bool.or(c7, False{}))) : + Jpeg.Bits & U32}: + {==} + +# one stuffed byte, read by the bit reader: the byte back, the reader at the bytes after it +def rd.z( + zz: Bool, + +c0: Bool, + +c1: Bool, + +c2: Bool, + +c3: Bool, + +c4: Bool, + +c5: Bool, + +c6: Bool, + +c7: Bool, + +rest: List<&2, U32>, + +ok: U32, + +ee: {U32.is_eq(W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7), 255) == zz : Bool} +) -> {Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, 0, Jenc.encode.stuff.put(zz, W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7), + rest)}) == (Jpeg.Bits{0, ok, 0, rest}, W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7)) : Jpeg.Bits & U32}: + match zz: + case False{}: + +bw = W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7) + +h0 = U32.is_eq(bw, 0) + Equal.trans(Jpeg.Bits & U32, Jpeg.decode.nbits(8n, True{}, bw <> rest, False{}, U32.is_eq(bw, 255), h0, 0, 0, + ok, 0), + Jpeg.decode.nbits(8n, True{}, bw <> rest, False{}, False{}, h0, 0, 0, ok, 0), (Jpeg.Bits{0, ok, 0, rest}, bw), + Equal.cong(Bool, Jpeg.Bits & U32, hb => Jpeg.decode.nbits(8n, True{}, bw <> rest, False{}, hb, h0, 0, 0, ok, 0), + U32.is_eq(bw, 255), False{}, ee), Equal.trans(Jpeg.Bits & U32, Jpeg.decode.nbits(8n, True{}, bw <> rest, + False{}, + False{}, h0, 0, 0, ok, 0), (Jpeg.Bits{0, ok, 0, rest}, W7.byte.w(Bool.or(c0, False{}), Bool.or(c1, False{}), + Bool.or(c2, False{}), Bool.or(c3, False{}), Bool.or(c4, False{}), Bool.or(c5, False{}), Bool.or(c6, False{}), + Bool.or(c7, False{}))), (Jpeg.Bits{0, ok, 0, rest}, bw), rd.plain(h0, c0, c1, c2, c3, c4, c5, c6, c7, rest, ok), + Equal.cong(U32, Jpeg.Bits & U32, vv => {(Jpeg.Bits{0, ok, 0, rest}, vv) : Jpeg.Bits & U32}, + W7.byte.w(Bool.or(c0, False{}), Bool.or(c1, False{}), Bool.or(c2, False{}), Bool.or(c3, False{}), + Bool.or(c4, False{}), Bool.or(c5, False{}), Bool.or(c6, False{}), Bool.or(c7, False{})), bw, + W7.or_byte(c0, c1, c2, c3, c4, c5, c6, c7)))) + case True{}: + +bw = W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7) + eb = Equal.sym(U32, bw, 255, U32L.ueq(bw, 255, ee)) + %eb : {Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, 0, _ <> (0 <> rest)}) == (Jpeg.Bits{0, ok, 0, rest}, _) : + Jpeg.Bits & U32} + {==} + +# the bit reader reads stuffed bytes back, eight bits at a time +def rd.list( + +bs: List<&2, Laws.JByte>, + +ok: U32, + +rest: List<&2, U32> +) -> {Laws.jpg.read8(List.length(&2, Laws.JByte, bs), Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, 0, + stf(Laws.jpg.bytes(bs), rest)})) == Laws.jpg.bytes(bs) : List<&2, U32>}: + match bs: + case Nil{}: + {==} + case +bb <> +tl: + match bb: + case Laws.JByte{+c0, +c1, +c2, +c3, +c4, +c5, +c6, +c7}: + +bw = W7.byte.w(c0, c1, c2, c3, c4, c5, c6, c7) + +st = stf(Laws.jpg.bytes(tl), rest) + Equal.trans(List<&2, U32>, Laws.jpg.read8(1n+List.length(&2, Laws.JByte, tl), Jpeg.decode.read.n(8, + Jpeg.Bits{0, ok, 0, Jenc.encode.stuff.put(U32.is_eq(bw, 255), bw, st)})), Laws.jpg.read8(1n+List.length(&2, + Laws.JByte, tl), (Jpeg.Bits{0, ok, 0, st}, bw)), bw <> Laws.jpg.bytes(tl), Equal.cong(Jpeg.Bits & U32, + List<&2, U32>, gg => Laws.jpg.read8(1n+List.length(&2, Laws.JByte, tl), gg), Jpeg.decode.read.n(8, + Jpeg.Bits{0, ok, 0, Jenc.encode.stuff.put(U32.is_eq(bw, 255), bw, st)}), (Jpeg.Bits{0, ok, 0, st}, bw), + rd.z(U32.is_eq(bw, 255), c0, c1, c2, c3, c4, c5, c6, c7, st, ok, {==})), Equal.cong(List<&2, U32>, + List<&2, U32>, ll => {bw <> ll : List<&2, U32>}, Laws.jpg.read8(List.length(&2, Laws.JByte, tl), + Jpeg.decode.read.n(8, Jpeg.Bits{0, ok, 0, st})), Laws.jpg.bytes(tl), rd.list(tl, ok, rest))) diff --git a/src/jpeg.bend b/src/jpeg.bend index 8fcb485..d6c7fe6 100644 --- a/src/jpeg.bend +++ b/src/jpeg.bend @@ -76,10 +76,6 @@ type Adv is Data: type Geom is Data: Geom{ox: U32, oy: U32, pw: U32, ph: U32, w: U32, h: U32} -# sample cursor inside an upsampled block -type Cursor is Data: - Cursor{k: U32, px: U32, py: U32} - # SOF component lists while they are being read, and whether every component # so far was read whole with sampling factors the decoder places type Comps is Data: @@ -489,36 +485,76 @@ def decode.look( case s <> st: decode.look.pref(decode.look(ct, lt, st, code, len), U32.is_eq(c, code), U32.is_eq(l, len), s) -def decode.nbits(left: Nat, eq: Bool, xs: List<&2, U32>, +nn: U32, +buf: U32, +ok: U32, +acc: U32) -> Bits & U32: +# whether a list of bytes opens with want. U32.is_eq, not a literal pattern, so a law reaches a +# symbolic byte. +def decode.head.is(xs: List<&2, U32>, +want: U32) -> Bool: + match xs: + case Nil{}: + False{} + case +bb <> _rest: + U32.is_eq(bb, want) + +# left more bits onto acc, most significant first. nn bits remain in buf, top bit first at bit 7; eq +# says buf is empty. ff says the byte before xs was a 255, and h255 and h0 whether xs opens with 255 +# or 0, each asked with U32.is_eq so a law reaches a symbolic byte. After a 255, 0 is a stuffed 255 +# (eight one bits) and 255 a fill byte; any other byte is a marker, and it or the end of the bytes +# reads zero bits and sets ok to 0. +def decode.nbits( + left: Nat, + eq: Bool, + xs: List<&2, U32>, + ff: Bool, + h255: Bool, + h0: Bool, + +nn: U32, + +buf: U32, + +ok: U32, + +acc: U32 +) -> Bits & U32: match left: case 0n: (Bits{nn, ok, buf, xs}, acc) case 1n+p: match eq: case False{}: - decode.nbits(p, U32.is_eq((nn - 1 : U32), 0), xs, (nn - 1 : U32), U32.and(U32.shl(buf), 255), ok, - U32.or(U32.shl(acc), U32.shrn(buf, 7n))) + decode.nbits(p, U32.is_eq((nn - 1 : U32), 0), xs, ff, h255, h0, (nn - 1 : U32), U32.and(255, U32.shl(buf)), + ok, U32.or(U32.shrn(buf, 7n), U32.shl(acc))) case True{}: match xs: case Nil{}: - decode.nbits(p, False{}, [], 7, 0, 0, U32.shl(acc)) - case 255 <> rest: - match rest: - case Nil{}: - decode.nbits(p, False{}, [], 7, 0, 0, U32.shl(acc)) - case 0 <> more: - decode.nbits(p, False{}, more, 7, 254, ok, U32.or(U32.shl(acc), 1)) - case 255 <> more: - decode.nbits(Succ{p}, True{}, more, 0, 0, ok, acc) - case _m <> more: - decode.nbits(p, False{}, more, 7, 0, 0, U32.shl(acc)) - case +b <> rest: - decode.nbits(p, False{}, rest, 7, U32.and(U32.shl(b), 255), ok, U32.or(U32.shl(acc), U32.shrn(b, 7n))) + decode.nbits(p, False{}, [], False{}, False{}, False{}, 7, 0, 0, U32.shl(acc)) + case +bb <> +rest: + match ff: + case False{}: + match h255: + case True{}: + decode.nbits(Succ{p}, True{}, rest, True{}, decode.head.is(rest, 255), decode.head.is(rest, 0), + 0, 0, ok, acc) + case False{}: + decode.nbits(p, False{}, rest, False{}, decode.head.is(rest, 255), decode.head.is(rest, 0), 7, + U32.and(255, U32.shl(bb)), ok, U32.or(U32.shrn(bb, 7n), U32.shl(acc))) + case True{}: + match h255: + case True{}: + decode.nbits(Succ{p}, True{}, rest, True{}, decode.head.is(rest, 255), decode.head.is(rest, 0), + 0, 0, ok, acc) + case False{}: + match h0: + case True{}: + decode.nbits(p, False{}, rest, False{}, decode.head.is(rest, 255), decode.head.is(rest, 0), + 7, 254, ok, U32.or(1, U32.shl(acc))) + case False{}: + decode.nbits(p, False{}, rest, False{}, decode.head.is(rest, 255), decode.head.is(rest, 0), + 7, 0, 0, U32.shl(acc)) + +# nn more bits from a reader, the first of them at the next byte when its buffer is empty +def decode.nbits.of(left: Nat, +xs: List<&2, U32>, +nn: U32, +buf: U32, +ok: U32) -> Bits & U32: + decode.nbits(left, U32.is_eq(nn, 0), xs, False{}, decode.head.is(xs, 255), decode.head.is(xs, 0), nn, buf, ok, 0) def decode.one(bits: Bits) -> Bits & U32: match bits: case Bits{+n, +ok, +buf, xs}: - decode.nbits(1n, U32.is_eq(n, 0), xs, n, buf, ok, 0) + decode.nbits.of(1n, xs, n, buf, ok) def decode.ask.bit(tab: Huff, got: Bits & U32, +code: U32, +len: U32) -> Ask: match tab: @@ -563,7 +599,7 @@ def decode.bits.of(bits: Bits) -> Nat & U32 & List<&2, U32> & U32 & U32: def decode.read.n(+cat: U32, bits: Bits) -> Bits & U32: match bits: case Bits{+n, +ok, +buf, xs}: - decode.nbits(U32.to_nat(cat), U32.is_eq(n, 0), xs, n, buf, ok, 0) + decode.nbits.of(U32.to_nat(cat), xs, n, buf, ok) def decode.extend.s(small: Bool, +mag: U32, +cat: U32) -> U32: match small: @@ -1040,26 +1076,6 @@ def decode.geom(ctrl: Ctrl, frame: Frame, scan: Scan) -> Geom: case Scan{_ns, +sids, _td, _ta, _ss, _se, _ah}: decode.geom.go(comp, bi, mx, my, w, h, hmax, vmax, sids, ids, hs, vs) -def decode.cursor.py(more: Bool, +kk: U32, +py: U32) -> Cursor: - match more: - case True{}: - Cursor{kk, 0, (py + 1 : U32)} - case False{}: - Cursor{(kk + 1 : U32), 0, 0} - -def decode.cursor.px(more: Bool, +kk: U32, +px: U32, +py: U32, +ph: U32) -> Cursor: - match more: - case True{}: - Cursor{kk, (px + 1 : U32), py} - case False{}: - decode.cursor.py(U32.is_lt((py + 1 : U32), ph), kk, py) - -def decode.cursor(+kk: U32, +px: U32, +py: U32, +pw: U32, +ph: U32) -> Cursor: - decode.cursor.px(U32.is_lt((px + 1 : U32), pw), kk, px, py, ph) - -def decode.splat.n(+pw: U32, +ph: U32) -> Nat: - U32.to_nat(((pw * ph : U32) * 64 : U32)) - def decode.splat.in(xin: Bool, yin: Bool, plane: Array, +xx: U32, +yy: U32, +ww: U32, +sample: U32) -> Array: match xin: case False{}: @@ -1071,12 +1087,52 @@ def decode.splat.in(xin: Bool, yin: Bool, plane: Array, +xx: U32, +yy: U32, case True{}: Array.set(U32, plane, (yy * ww + xx : U32), sample) -def decode.splat.put( +# one pixel row of the pixels a sample covers: columns x0 + px onward, left pixels left, each written +# only when it lies inside the frame +def decode.splat.px( + left: Nat, plane: Array, - +kk: U32, + +x0: U32, + +yy: U32, +px: U32, + +ww: U32, + +hh: U32, + +vv: U32 +) -> Array: + match left: + case 0n: + plane + case 1n+p: + decode.splat.px(p, decode.splat.in(U32.is_lt((x0 + px : U32), ww), U32.is_lt(yy, hh), plane, (x0 + px : U32), yy, + ww, vv), x0, yy, (px + 1 : U32), ww, hh, vv) + +# the pw by ph pixels one sample covers, from (x0, y0 + py), row by row +def decode.splat.py( + left: Nat, + plane: Array, + +x0: U32, + +y0: U32, +py: U32, - samples: List<&2, U32>, + +pw: U32, + +ww: U32, + +hh: U32, + +vv: U32 +) -> Array: + match left: + case 0n: + plane + case 1n+p: + decode.splat.py(p, decode.splat.px(U32.to_nat(pw), plane, x0, (y0 + py : U32), 0, ww, hh, vv), x0, y0, + (py + 1 : U32), pw, ww, hh, vv) + +# samples 8 * row + col onward of one block row, each over the pw by ph pixels at +# (ox + col * pw, oy + row * ph) +def decode.splat.col( + left: Nat, + plane: Array, + +samples: List<&2, U32>, + +row: U32, + +col: U32, +ox: U32, +oy: U32, +pw: U32, @@ -1084,15 +1140,19 @@ def decode.splat.put( +ww: U32, +hh: U32 ) -> Array: - +x = (ox + U32.mod(kk, 8) * pw + px : U32) - +y = (oy + U32.div(kk, 8) * ph + py : U32) - decode.splat.in(U32.is_lt(x, ww), U32.is_lt(y, hh), plane, x, y, ww, decode.at(samples, kk)) + match left: + case 0n: + plane + case 1n+p: + decode.splat.col(p, decode.splat.py(U32.to_nat(ph), plane, (ox + col * pw : U32), (oy + row * ph : U32), 0, pw, + ww, hh, decode.at(samples, (row * 8 + col : U32))), samples, row, (col + 1 : U32), ox, oy, pw, ph, ww, hh) +# the rows of an 8 by 8 block from row down, each sample replicated over pw by ph pixels def decode.splat( left: Nat, - cur: Cursor, - +samples: List<&2, U32>, plane: Array, + +samples: List<&2, U32>, + +row: U32, +ox: U32, +oy: U32, +pw: U32, @@ -1102,15 +1162,11 @@ def decode.splat( ) -> Array: match left: case 0n: - match cur: - case Cursor{_k, _px, _py}: - +_s = decode.drop(samples) - plane + +_s = decode.drop(samples) + plane case 1n+p: - match cur: - case Cursor{+k, +px, +py}: - decode.splat(p, decode.cursor(k, px, py, pw, ph), samples, - decode.splat.put(plane, k, px, py, samples, ox, oy, pw, ph, ww, hh), ox, oy, pw, ph, ww, hh) + decode.splat(p, decode.splat.col(8n, plane, samples, row, 0, ox, oy, pw, ph, ww, hh), samples, (row + 1 : U32), + ox, oy, pw, ph, ww, hh) def decode.paint.which( which: Bool, @@ -1128,7 +1184,7 @@ def decode.paint.which( +_s = decode.drop(samples) plane case True{}: - decode.splat(decode.splat.n(pw, ph), Cursor{0, 0, 0}, samples, plane, ox, oy, pw, ph, ww, hh) + decode.splat(8n, plane, samples, 0, ox, oy, pw, ph, ww, hh) def decode.paint.use(gg: Geom, which: Bool, samples: List<&2, U32>, plane: Array) -> Array: match gg: @@ -1164,36 +1220,23 @@ def decode.depth(+nn: U32) -> Nat: def decode.plane(+nn: U32) -> Array: Array.new(U32, decode.depth(nn), 0) -def decode.emit(left: Nat, got: Array & U32, +ii: U32, acc: List<&2, U32>, fresh: Bool) -> List<&2, U32>: +# the plane's points in order: got is the plane and the value of point ii - 1, just read, then the +# left - 1 points from ii on. One read past the last point is made and dropped. +def decode.emit(left: Nat, got: Array & U32, +ii: U32) -> List<&2, U32>: match left: case 0n: - match got: - case (a, +v): - match ii: - case _j: - match acc: - case ys: - match fresh: - case False{}: - +_a = decode.sink(a) - +_v = (v - v : U32) - List.reverse(&2, U32, ys) - case True{}: - +_a = decode.sink(a) - List.reverse(&2, U32, v <> ys) + (a, +v) = got + +_a = decode.sink(a) + +_v = (v - v : U32) + +_i = (ii - ii : U32) + [] case 1n+p: - match got: - case (a, +v): - match ii: - case +j: - match acc: - case ys: - match fresh: - case False{}: - +_v = (v - v : U32) - decode.emit(p, Array.get(U32, a, j), (j + 1 : U32), ys, True{}) - case True{}: - decode.emit(p, Array.get(U32, a, j), (j + 1 : U32), v <> ys, True{}) + (a, v) = got + v <> decode.emit(p, Array.get(U32, a, ii), (ii + 1 : U32)) + +# the first nn points of a plane, in order +def decode.points(+nn: Nat, plane: Array) -> List<&2, U32>: + decode.emit(nn, Array.get(U32, plane, 0), 1) # a sample's colour bits made opaque: alpha 255 over the low 24 bits. The # constant is the first operand, so a law over any sample sees its alpha @@ -1285,13 +1328,12 @@ def decode.done.drop(yy: Array, cb: Array, cr: Array) -> Maybe<&2 def decode.done.gray(+ww: U32, +hh: U32, yy: Array, cb: Array, cr: Array) -> Maybe<&2, Pic>: +_b = decode.sink(cb) +_c = decode.sink(cr) - Some{Pic{ww, hh, decode.grays(decode.emit(U32.to_nat((ww * hh : U32)), (yy, 0), 0, [], False{}))}} + Some{Pic{ww, hh, decode.grays(decode.points(U32.to_nat((ww * hh : U32)), yy))}} # a colour picture: each point's Y, Cb and Cr read out in order, then packed def decode.done.color(+ww: U32, +hh: U32, yy: Array, cb: Array, cr: Array) -> Maybe<&2, Pic>: +n = U32.to_nat((ww * hh : U32)) - Some{Pic{ww, hh, decode.rgbs(decode.emit(n, (yy, 0), 0, [], False{}), decode.emit(n, (cb, 0), 0, [], False{}), - decode.emit(n, (cr, 0), 0, [], False{}))}} + Some{Pic{ww, hh, decode.rgbs(decode.points(n, yy), decode.points(n, cb), decode.points(n, cr))}} # three components are colour; any other count is none def decode.done.nf3(three: Bool, +ww: U32, +hh: U32, yy: Array, cb: Array, cr: Array) -> Maybe<&2, Pic>: @@ -1410,6 +1452,18 @@ def decode.start( decode.blocks(p, decode.block.of(bits, 0, decode.pred.zero(), frame, scan, tabs), Ctrl{0, 0, 0, 0, 0, 0}, decode.pred.zero(), frame, scan, tabs, ri, yy, cb, cr, 1) +# the blocks a scan of the frame holds: ceil(w / 8 hmax) * ceil(h / 8 vmax) MCUs, each with the frame's +# components' hi * vi data units +def decode.nblocks( + +ww: U32, + +hh: U32, + +hs: List<&2, U32>, + +vs: List<&2, U32>, + +hmax: U32, + +vmax: U32 +) -> U32: + (decode.ceil(ww, (hmax * 8 : U32)) * decode.ceil(hh, (vmax * 8 : U32)) * decode.blocks.sum(hs, vs, 0) : U32) + def decode.run.n( empty: Bool, +ww: U32, @@ -1426,10 +1480,8 @@ def decode.run.n( case False{}: match frame: case Frame{_w, _h, _nf, _ids, +hs, +vs, _tq, +hmax, +vmax}: - +n = (decode.ceil(ww, (hmax * 8 : U32)) * decode.ceil(hh, (vmax * 8 : U32)) * decode.blocks.sum(hs, vs, 0) : - U32) - decode.start(U32.to_nat(n), Bits{0, 1, 0, ent}, frame, scan, tabs, ri, decode.plane((ww * hh : U32)), - decode.plane((ww * hh : U32)), decode.plane((ww * hh : U32))) + decode.start(U32.to_nat(decode.nblocks(ww, hh, hs, vs, hmax, vmax)), Bits{0, 1, 0, ent}, frame, scan, tabs, + ri, decode.plane((ww * hh : U32)), decode.plane((ww * hh : U32)), decode.plane((ww * hh : U32))) def decode.run(frame: Frame, scan: Scan, tabs: Tabs, ent: List<&2, U32>, +ri: U32) -> Maybe<&2, Pic>: match frame: @@ -2244,6 +2296,26 @@ def decode.ent.rst.b( case False{}: St{Stop{}, frame, scan, tabs, ent, ri, kind, 1} +# a byte of the entropy-coded data: 255 may open a stuffed pair or a marker, any other byte is data. +# Compares with U32.is_eq, not a literal pattern, so a law reaches a symbolic byte. +def decode.step.ent( + ff: Bool, + +bb: U32, + frame: Frame, + scan: Scan, + tabs: Tabs, + ent: List<&2, U32>, + +ri: U32, + +kind: U32, + +bad: U32 +) -> St: + match ff: + case True{}: + +_b = (bb - bb : U32) + St{EntFF{}, frame, scan, tabs, ent, ri, kind, bad} + case False{}: + St{Ent{}, frame, scan, tabs, bb <> ent, ri, kind, bad} + def decode.step.ph( phase: Phase, +bb: U32, @@ -2272,11 +2344,7 @@ def decode.step.ph( case Pay{+mark, +left, +acc}: decode.step.pay(left, bb, mark, acc, frame, scan, tabs, ent, ri, kind, bad) case Ent{}: - match bb: - case 255: - St{EntFF{}, frame, scan, tabs, ent, ri, kind, bad} - case _: - St{Ent{}, frame, scan, tabs, bb <> ent, ri, kind, bad} + decode.step.ent(U32.is_eq(bb, 255), bb, frame, scan, tabs, ent, ri, kind, bad) case EntFF{}: match bb: case 0: diff --git a/src/jpeg_enc.bend b/src/jpeg_enc.bend index 1848cd9..950f7a2 100644 --- a/src/jpeg_enc.bend +++ b/src/jpeg_enc.bend @@ -162,15 +162,9 @@ def encode.bad(+ww: U32, +hh: U32) -> Bool: def encode.put0() -> Put: Put{[], 0, 0} -def encode.stuff.ff(ff: Bool, out: List<&2, U32>, +bb: U32) -> Put: - match ff: - case True{}: - Put{0 <> (255 <> out), 0, 0} - case False{}: - Put{bb <> out, 0, 0} - +# a finished byte. Bytes are kept as written; encode.pad stuffs them once, at the end. def encode.stuff(out: List<&2, U32>, +bb: U32) -> Put: - encode.stuff.ff(U32.is_eq(bb, 255), out, bb) + Put{bb <> out, 0, 0} def encode.bit.n(full: Bool, out: List<&2, U32>, +nb: U32, +nn: U32) -> Put: match full: @@ -195,27 +189,36 @@ def encode.bits.go(left: Nat, pp: Put, +code: U32) -> Put: def encode.bits(pp: Put, +len: U32, +code: U32) -> Put: encode.bits.go(U32.to_nat(len), pp, code) -def encode.pad.byte(ff: Bool, out: List<&2, U32>, +byte: U32) -> List<&2, U32>: +# one byte put in front of the stuffed bytes after it: 255 is followed by a 0 +def encode.stuff.put(ff: Bool, +bb: U32, acc: List<&2, U32>) -> List<&2, U32>: match ff: case True{}: - List.reverse(&2, U32, 0 <> (255 <> out)) + bb <> (0 <> acc) case False{}: - List.reverse(&2, U32, byte <> out) + bb <> acc + +# the written bytes, newest first, stuffed and put in order onto acc: every 255 is followed by a 0 +# (T.81 F.1.2.3). U32.is_eq, not a literal pattern, so a law reaches a symbolic byte. +def encode.stuff.all(out: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>: + match out: + case Nil{}: + acc + case +bb <> rest: + encode.stuff.all(rest, encode.stuff.put(U32.is_eq(bb, 255), bb, acc)) def encode.pad.n(zz: Bool, out: List<&2, U32>, +buf: U32, +nn: U32) -> List<&2, U32>: match zz: case True{}: - List.reverse(&2, U32, out) + out case False{}: +sh = (8 - nn : U32) - +ones = (U32.shln(1, U32.to_nat(sh)) - 1 : U32) - encode.pad.byte(U32.is_eq(U32.or(U32.shln(buf, U32.to_nat(sh)), ones), 255), out, - U32.or(U32.shln(buf, U32.to_nat(sh)), ones)) + U32.or(U32.shln(buf, U32.to_nat(sh)), (U32.shln(1, U32.to_nat(sh)) - 1 : U32)) <> out +# the entropy-coded bytes: the open byte padded with 1 bits, then every byte stuffed, in order def encode.pad(pp: Put) -> List<&2, U32>: match pp: case Put{out, +buf, +n}: - encode.pad.n(U32.is_eq(n, 0), out, buf, n) + encode.stuff.all(encode.pad.n(U32.is_eq(n, 0), out, buf, n), []) def encode.drop(xs: List<&2, U32>) -> U32: Jpeg.decode.drop(xs) @@ -1640,18 +1643,25 @@ def encode.go(+ww: U32, +hh: U32, px: List<&2, U32>) -> List<&2, U32>: encode.put0()), 0, 0, mw, ww, hh, encode.ctx())) # the entropy-coded bytes, by what the watch found: neutral, one solid colour, or anything else -def encode.dispatch(+tag: U32, +color: U32, px: List<&2, U32>, +ww: U32, +hh: U32) -> List<&2, U32>: - match tag: - case 0: +def encode.dispatch.b(neu: Bool, sol: Bool, +color: U32, px: List<&2, U32>, +ww: U32, +hh: U32) -> List<&2, U32>: + match neu: + case True{}: +_c = (color - color : U32) +_d = encode.drop(px) + +_s = Bool.not(sol) encode.neutral(ww, hh) - case 1: - +_d = encode.drop(px) - encode.solid(ww, hh, color) - case _: - +_c = (color - color : U32) - encode.go(ww, hh, px) + case False{}: + match sol: + case True{}: + +_d = encode.drop(px) + encode.solid(ww, hh, color) + case False{}: + +_c = (color - color : U32) + encode.go(ww, hh, px) + +# the watch's tag, 0 neutral, 1 solid, 2 mixed, asked with U32.is_eq so a law reaches every tag +def encode.dispatch(+tag: U32, +color: U32, px: List<&2, U32>, +ww: U32, +hh: U32) -> List<&2, U32>: + encode.dispatch.b(U32.is_eq(tag, 0), U32.is_eq(tag, 1), color, px, ww, hh) # the watch's answer, dispatched def encode.arm.use(got: U32 & U32 & List<&2, U32>, +ww: U32, +hh: U32) -> List<&2, U32>: