src/jpeg.bend checks

raw source on the hub · import 0x57618559b9b26dd8415f821176a3e692/src/jpeg.bend as Jpeg

src/jpeg: baseline JPEG. Sequential 8-bit Huffman (SOF0), JFIF APP0, grayscale or YCbCr.

1 import

import Base

Types

type Pic source · line 7 · raw

Data

a decoded picture: width, height, and row-major samples, each packed 0xAARRGGBB with alpha 255

Pic

@w:U32 -> @h:U32 -> @pixels:List<&2, U32> -> Pic

type Huff source · line 11 · raw

Data

one Huffman table: canonical codes, lengths, and symbols

Huff

@codes:List<&2, U32> -> @lens:List<&2, U32> -> @syms:List<&2, U32> -> Huff

type Frame source · line 15 · raw

Data

SOF0 frame geometry. Sampling factors are 1, 2, or 4.

Frame

@w:U32 -> @h:U32 -> @nf:U32 -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @tq:List<&2, U32> -> @hmax:U32 -> @vmax:U32 -> Frame

type Scan source · line 20 · raw

Data

one SOS header

Scan

@ns:U32 -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @ss:U32 -> @se:U32 -> @ah:U32 -> Scan

type Tabs source · line 24 · raw

Data

four quant tables and four DC / AC Huffman tables

Tabs

@q0:List<&2, U32> -> @q1:List<&2, U32> -> @q2:List<&2, U32> -> @q3:List<&2, U32> -> @dc0:Huff -> @dc1:Huff -> @dc2:Huff -> @dc3:Huff -> @ac0:Huff -> @ac1:Huff -> @ac2:Huff -> @ac3:Huff -> Tabs

type Phase source · line 29 · raw

Data

marker walk: seeking, a marker byte, a length, a payload, or the entropy scan

Seek
```
Phase
```
Mark
```
Phase
```
LenHi
```
@mark:U32 -> Phase
```
LenLo
```
@mark:U32 -> @hi:U32 -> Phase
```

Pay

@mark:U32 -> @left:Nat -> @acc:List<&2, U32> -> Phase

Ent
```
Phase
```
EntFF
```
Phase
```
Stop
```
Phase
```

type St source · line 40 · raw

Data

parser state. kind 1 is a baseline frame. bad 1 rejects the file.

St

@phase:Phase -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @ri:U32 -> @kind:U32 -> @bad:U32 -> St

type Bits source · line 44 · raw

Data

bit reader. n bits remain in buf. ok is 0 after a truncated or marked stream.

Bits

@n:U32 -> @ok:U32 -> @buf:U32 -> @xs:List<&2, U32> -> Bits

type Ask source · line 48 · raw

Data

a Huffman lookup in progress

Ask

@hit:Maybe<&2, U32> -> @code:U32 -> @len:U32 -> @bits:Bits -> Ask

type Hit source · line 52 · raw

Data

one decoded Huffman symbol

Hit

@sym:U32 -> @bits:Bits -> @ok:U32 -> Hit

type Ac source · line 56 · raw

Data

AC run state inside one block

Ac

@k:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @done:U32 -> @ok:U32 -> Ac

type Blk source · line 60 · raw

Data

one decoded 8x8 block, level-shifted samples, and the DC predictor

Blk

@samples:List<&2, U32> -> @bits:Bits -> @pred:U32 -> @ok:U32 -> Blk

type Preds source · line 64 · raw

Data

DC predictors, one per scan component

Preds

@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> Preds

type Ctrl source · line 68 · raw

Data

where the current block sits in the frame

Ctrl

@comp:U32 -> @bi:U32 -> @mx:U32 -> @my:U32 -> @mcu:U32 -> @rst:U32 -> Ctrl

type Adv source · line 72 · raw

Data

the block that follows, and whether a restart marker comes first

Adv

@ctrl:Ctrl -> @due:U32 -> @expect:U32 -> Adv

type Geom source · line 76 · raw

Data

pixel rectangle one block sample covers

Geom

@ox:U32 -> @oy:U32 -> @pw:U32 -> @ph:U32 -> @w:U32 -> @h:U32 -> Geom

type Comps source · line 81 · raw

Data

SOF component lists while they are being read, and whether every component so far was read whole with sampling factors the decoder places

Comps

@ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @tq:List<&2, U32> -> @ok:Bool -> Comps

type Cols source · line 85 · raw

Data

the eight cosine columns of the A.3.3 matrix, one list per frequency

Cols

@c0:List<&2, U32> -> @c1:List<&2, U32> -> @c2:List<&2, U32> -> @c3:List<&2, U32> -> @c4:List<&2, U32> -> @c5:List<&2, U32> -> @c6:List<&2, U32> -> @c7:List<&2, U32> -> Cols

Definitions

def decode.sign source · line 89 · raw

@+aa:U32 -> U32

def decode.neg32 source · line 92 · raw

@+aa:U32 -> U32

def decode.abs.s source · line 95 · raw

@ss:U32 -> @+aa:U32 -> U32

def decode.abs source · line 102 · raw

@+aa:U32 -> U32

def decode.carry.b source · line 105 · raw

@cc:Bool -> U32

def decode.carry source · line 112 · raw

@+aa:U32 -> @+sum:U32 -> U32

def decode.neg64.c source · line 115 · raw

@zz:Bool -> @+nh:U32 -> @+nl:U32 -> Pair(U32, U32)

def decode.neg64 source · line 122 · raw

@+hh:U32 -> @+ll:U32 -> Pair(U32, U32)

def decode.split source · line 127 · raw

@+aa:U32 -> Pair(U32, U32)

def decode.widemul.pack source · line 130 · raw

@+neg:U32 -> @+hi:U32 -> @+lo:U32 -> Pair(U32, U32)

def decode.widemul.bb source · line 137 · raw

@+a0:U32 -> @+a1:U32 -> @bb:Pair(U32, U32) -> @+neg:U32 -> Pair(U32, U32)

def decode.widemul.aa source · line 148 · raw

@aa:Pair(U32, U32) -> @+bb:U32 -> @+neg:U32 -> Pair(U32, U32)

def decode.widemul.go source · line 152 · raw

@+aa:U32 -> @+bb:U32 -> @+neg:U32 -> Pair(U32, U32)

def decode.widemul source · line 155 · raw

@+aa:U32 -> @+bb:U32 -> Pair(U32, U32)

def decode.q17.res source · line 158 · raw

@+hh:U32 -> @+ll:U32 -> U32

def decode.q17.sign2 source · line 161 · raw

@neg:Bool -> @+res:U32 -> U32

def decode.q17.div source · line 168 · raw

@+hh:U32 -> @+ll:U32 -> @neg:Bool -> U32

def decode.q17.neg source · line 173 · raw

@pp:Pair(U32, U32) -> U32

def decode.q17.pos source · line 177 · raw

@pos:Bool -> @+hh:U32 -> @+ll:U32 -> U32

def decode.q17 source · line 184 · raw

@+hh:U32 -> @+ll:U32 -> U32

def decode.dot.end source · line 187 · raw

@+lo:U32 -> @+ah:U32 -> @+ph:U32 -> @+al:U32 -> U32

def decode.dot source · line 190 · raw

@cs:List<&2, U32> -> @ks:List<&2, U32> -> @have:Bool -> @prod:Pair(U32, U32) -> @+ah:U32 -> @+al:U32 -> U32

def decode.at.m source · line 222 · raw

@mm:Maybe<&2, U32> -> U32

def decode.at source · line 229 · raw

@xs:List<&2, U32> -> @+ii:U32 -> U32

def decode.column source · line 232 · raw

@+cs:List<&2, U32> -> @+xx:U32 -> List<&2, U32>

def decode.cols source · line 239 · raw

@+cs:List<&2, U32> -> Cols

one copy of each cosine column, reused for every row of the block

def decode.row8 source · line 243 · raw

@+row:List<&2, U32> -> @+cols:Cols -> List<&2, U32>

def decode.cos source · line 251 · raw

List<&2, U32>

def decode.pass source · line 259 · raw

@left:Nat -> @coeffs:List<&2, U32> -> @+cols:Cols -> @acc:List<&2, List<&2, U32>> -> List<&2, List<&2, U32>>

def decode.col source · line 275 · raw

@+rows:List<&2, List<&2, U32>> -> @+xx:U32 -> @acc:List<&2, U32> -> List<&2, U32>

def decode.backs source · line 282 · raw

@+rows:List<&2, List<&2, U32>> -> @+cols:Cols -> List<&2, List<&2, U32>>

def decode.rows.of source · line 288 · raw

@+backs:List<&2, List<&2, U32>> -> List<&2, List<&2, U32>>

def decode.flat.row source · line 293 · raw

@xs:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

def decode.flat source · line 300 · raw

@rows:List<&2, List<&2, U32>> -> List<&2, U32>

def decode.clamp.hi source · line 307 · raw

@hi:Bool -> @+vv:U32 -> U32

def decode.clamp8.s source · line 314 · raw

@ss:U32 -> @+vv:U32 -> U32

def decode.clamp8 source · line 321 · raw

@+vv:U32 -> U32

def decode.level source · line 324 · raw

@xs:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

def decode.zeros source · line 331 · raw

@nn:Nat -> @acc:List<&2, U32> -> List<&2, U32>

def decode.idct source · line 338 · raw

@nat:List<&2, U32> -> List<&2, U32>

def decode.huff0 source · line 342 · raw

Huff

def decode.frame0 source · line 345 · raw

Frame

def decode.scan0 source · line 348 · raw

Scan

def decode.tabs0 source · line 351 · raw

Tabs

def decode.st0 source · line 355 · raw

St

def decode.nlist source · line 358 · raw

@xs:List<&2, U32> -> @+nn:U32 -> U32

def decode.drop source · line 365 · raw

@xs:List<&2, U32> -> U32

def decode.rev3 source · line 372 · raw

@ac:List<&2, U32> -> @al:List<&2, U32> -> @ay:List<&2, U32> -> Huff

def decode.canon.shift source · line 375 · raw

@+len:U32 -> @+code:U32 -> U32

def decode.canon source · line 382 · raw

@left:Nat -> @tick:Nat -> @counts:List<&2, U32> -> @symbols:List<&2, U32> -> @+code:U32 -> @+len:U32 -> @ac:List<&2, U32> -> @al:List<&2, U32> -> @ay:List<&2, U32> -> Huff

def decode.index.add source · line 421 · raw

@eq:Bool -> @+ii:U32 -> U32

def decode.index source · line 430 · raw

@xs:List<&2, U32> -> @eq:Bool -> @+want:U32 -> @+ii:U32 -> U32

the position of want in xs, the first if it is there more than once, 0 when it is absent. eq says the element before xs was want, and ii counts the elements before it. Matches with U32.is_eq, so a law reaches it.

def decode.look.pref source · line 446 · raw

@tail:Maybe<&2, U32> -> @eqc:Bool -> @eql:Bool -> @+ss:U32 -> Maybe<&2, U32>

def decode.look source · line 461 · raw

@codes:List<&2, U32> -> @lens:List<&2, U32> -> @syms:List<&2, U32> -> @+code:U32 -> @+len:U32 -> Maybe<&2, U32>

def decode.head.is source · line 490 · raw

@xs:List<&2, U32> -> @+want:U32 -> Bool

whether a list of bytes opens with want. U32.is_eq, not a literal pattern, so a law reaches a symbolic byte.

def decode.nbits source · line 502 · raw

@left:Nat -> @eq:Bool -> @xs:List<&2, U32> -> @ff:Bool -> @h255:Bool -> @h0:Bool -> @+nn:U32 -> @+buf:U32 -> @+ok:U32 -> @+acc:U32 -> Pair(Bits, U32)

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.of source · line 551 · raw

@left:Nat -> @+xs:List<&2, U32> -> @+nn:U32 -> @+buf:U32 -> @+ok:U32 -> Pair(Bits, U32)

nn more bits from a reader, the first of them at the next byte when its buffer is empty

def decode.one source · line 554 · raw

@bits:Bits -> Pair(Bits, U32)

def decode.ask.bit source · line 559 · raw

@tab:Huff -> @got:Pair(Bits, U32) -> @+code:U32 -> @+len:U32 -> Ask

def decode.ask source · line 567 · raw

@bits:Bits -> @+code:U32 -> @+len:U32 -> @tab:Huff -> Ask

def decode.huff.use source · line 570 · raw

@hit:Maybe<&2, U32> -> @bits:Bits -> Hit

def decode.huff source · line 579 · raw

@left:Nat -> @ask:Ask -> @+tab:Huff -> Hit

def decode.bits.of source · line 594 · raw

@bits:Bits -> Pair(Nat, Pair(U32, Pair(List<&2, U32>, Pair(U32, U32))))

def decode.read.n source · line 599 · raw

@+cat:U32 -> @bits:Bits -> Pair(Bits, U32)

def decode.extend.s source · line 604 · raw

@small:Bool -> @+mag:U32 -> @+cat:U32 -> U32

def decode.extend source · line 611 · raw

@+cat:U32 -> @+mag:U32 -> U32

def decode.ac.stored source · line 618 · raw

@full:Bool -> @+kk:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.store source · line 625 · raw

@got:Pair(Bits, U32) -> @+sz:U32 -> @+nk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.bad source · line 630 · raw

@zz:List<&2, U32> -> @bits:Bits -> Ac

def decode.ac.run.b source · line 633 · raw

@zzz:Bool -> @over:Bool -> @+sz:U32 -> @+nk:U32 -> @bits:Bits -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.run source · line 644 · raw

@+sym:U32 -> @bits:Bits -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.zrl.eq source · line 649 · raw

@eq:Bool -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.zrl.k source · line 656 · raw

@more:Bool -> @+nk:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.zrl source · line 663 · raw

@+kk:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.sym.b source · line 668 · raw

@eob:Bool -> @zrl:Bool -> @+sym:U32 -> @bits:Bits -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

an AC symbol: EOB (0), ZRL (240), or a run and size. U32.is_eq, not literal patterns, so a law reaches a symbolic symbol.

def decode.ac.sym source · line 682 · raw

@+sym:U32 -> @bits:Bits -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.step source · line 685 · raw

@hit:Hit -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.full source · line 690 · raw

@done:Bool -> @short:Bool -> @ac:Ac -> Ac

def decode.ac source · line 703 · raw

@left:Nat -> @ac:Ac -> @+tab:Huff -> Ac

def decode.zig source · line 720 · raw

List<&2, U32>

def decode.nat source · line 725 · raw

@zz:List<&2, U32> -> @quant:List<&2, U32> -> @zig:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

def decode.block.ac source · line 746 · raw

@ac:Ac -> @+pred:U32 -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.block.diff source · line 751 · raw

@got:Pair(Bits, U32) -> @+cat:U32 -> @+pred:U32 -> @+ok:U32 -> @ac:Huff -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.block.cat source · line 764 · raw

@zz:Bool -> @+sym:U32 -> @bits:Bits -> @+pred:U32 -> @+ok:U32 -> @ac:Huff -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.block.dc source · line 780 · raw

@hit:Hit -> @+pred:U32 -> @ac:Huff -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.qok.b source · line 785 · raw

@ok:Bool -> U32

def decode.qok source · line 792 · raw

@quant:List<&2, U32> -> U32

def decode.block.go source · line 795 · raw

@bits:Bits -> @+pred:U32 -> @dc:Huff -> @ac:Huff -> @+quant:List<&2, U32> -> Blk

def decode.dc.get source · line 798 · raw

@tabs:Tabs -> @+id:U32 -> Huff

def decode.ac.get source · line 811 · raw

@tabs:Tabs -> @+id:U32 -> Huff

def decode.q.get source · line 824 · raw

@tabs:Tabs -> @+id:U32 -> List<&2, U32>

def decode.pred.get source · line 837 · raw

@preds:Preds -> @+ii:U32 -> U32

def decode.pred.put source · line 850 · raw

@preds:Preds -> @+ii:U32 -> @+vv:U32 -> Preds

def decode.pred.zero source · line 863 · raw

Preds

def decode.preds.next source · line 866 · raw

@due:U32 -> @preds:Preds -> @+comp:U32 -> @+pred:U32 -> Preds

def decode.block.of source · line 875 · raw

@bits:Bits -> @+comp:U32 -> @preds:Preds -> @frame:Frame -> @scan:Scan -> @+tabs:Tabs -> Blk

def decode.rst.ok source · line 890 · raw

@eq:Bool -> @rest:List<&2, U32> -> Bits

def decode.rst.xs source · line 897 · raw

@xs:List<&2, U32> -> @+want:U32 -> Bits

def decode.rst source · line 904 · raw

@bits:Bits -> @+want:U32 -> Bits

def decode.restart source · line 909 · raw

@bits:Bits -> @+due:U32 -> @+expect:U32 -> Bits

def decode.ceil source · line 916 · raw

@+nn:U32 -> @+dd:U32 -> U32

def decode.ri.nz source · line 919 · raw

@+ri:U32 -> U32

def decode.adv.due.b source · line 926 · raw

@zero:Bool -> @hit:Bool -> @+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> Adv

def decode.adv.due source · line 937 · raw

@+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> @+ri:U32 -> Adv

def decode.adv.mx source · line 940 · raw

@inb:Bool -> @+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> @+ri:U32 -> Adv

def decode.adv.mcu source · line 947 · raw

@+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ri:U32 -> Adv

def decode.adv.comp source · line 950 · raw

@more:Bool -> @+comp:U32 -> @+mx:U32 -> @+my:U32 -> @+mcu:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ri:U32 -> Adv

def decode.adv.bi source · line 967 · raw

@more:Bool -> @+comp:U32 -> @+bi:U32 -> @+mx:U32 -> @+my:U32 -> @+mcu:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ns:U32 -> @+ri:U32 -> Adv

def decode.adv.go source · line 986 · raw

@+comp:U32 -> @+bi:U32 -> @+mx:U32 -> @+my:U32 -> @+mcu:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ns:U32 -> @sids:List<&2, U32> -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @+ri:U32 -> Adv

def decode.adv source · line 1007 · raw

@ctrl:Ctrl -> @frame:Frame -> @scan:Scan -> @+ri:U32 -> Adv

def decode.block.next.go source · line 1016 · raw

@adv:Adv -> @bits:Bits -> @preds:Preds -> @+pred:U32 -> @+comp:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> Blk

def decode.block.next source · line 1033 · raw

@bits:Bits -> @preds:Preds -> @+pred:U32 -> @ctrl:Ctrl -> @+frame:Frame -> @+scan:Scan -> @tabs:Tabs -> @+ri:U32 -> Blk

def decode.geom.nz source · line 1047 · raw

@+nn:U32 -> U32

def decode.geom.go source · line 1057 · raw

@+comp:U32 -> @+bi:U32 -> @+mx:U32 -> @+my:U32 -> @+ww:U32 -> @+hh:U32 -> @+hmax:U32 -> @+vmax:U32 -> @sids:List<&2, U32> -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> Geom

where block bi of a component sits in its MCU: a component's hi * vi blocks run left to right, hi to a row, then top to bottom (T.81 A.2.3), so its column is bi mod hi and its row bi div hi

def decode.geom source · line 1080 · raw

@ctrl:Ctrl -> @frame:Frame -> @scan:Scan -> Geom

def decode.splat.in source · line 1089 · raw

@xin:Bool -> @yin:Bool -> @plane:Array<U32> -> @+xx:U32 -> @+yy:U32 -> @+ww:U32 -> @+sample:U32 -> Array<U32>

def decode.splat.px source · line 1102 · raw

@left:Nat -> @plane:Array<U32> -> @+x0:U32 -> @+yy:U32 -> @+px:U32 -> @+ww:U32 -> @+hh:U32 -> @+vv:U32 -> Array<U32>

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.py source · line 1120 · raw

@left:Nat -> @plane:Array<U32> -> @+x0:U32 -> @+y0:U32 -> @+py:U32 -> @+pw:U32 -> @+ww:U32 -> @+hh:U32 -> @+vv:U32 -> Array<U32>

the pw by ph pixels one sample covers, from (x0, y0 + py), row by row

def decode.splat.col source · line 1140 · raw

@left:Nat -> @plane:Array<U32> -> @+samples:List<&2, U32> -> @+row:U32 -> @+col:U32 -> @+ox:U32 -> @+oy:U32 -> @+pw:U32 -> @+ph:U32 -> @+ww:U32 -> @+hh:U32 -> Array<U32>

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 source · line 1161 · raw

@left:Nat -> @plane:Array<U32> -> @+samples:List<&2, U32> -> @+row:U32 -> @+ox:U32 -> @+oy:U32 -> @+pw:U32 -> @+ph:U32 -> @+ww:U32 -> @+hh:U32 -> Array<U32>

the rows of an 8 by 8 block from row down, each sample replicated over pw by ph pixels

def decode.paint.which source · line 1181 · raw

@which:Bool -> @samples:List<&2, U32> -> @plane:Array<U32> -> @+ox:U32 -> @+oy:U32 -> @+pw:U32 -> @+ph:U32 -> @+ww:U32 -> @+hh:U32 -> Array<U32>

def decode.paint.use source · line 1199 · raw

@gg:Geom -> @which:Bool -> @samples:List<&2, U32> -> @plane:Array<U32> -> Array<U32>

def decode.ctrl.comp source · line 1204 · raw

@ctrl:Ctrl -> U32

def decode.sink.leaf source · line 1209 · raw

@aa:Array<U32> -> U32

def decode.sink.p source · line 1216 · raw

@pp:Pair(Array<U32>, U32) -> U32

def decode.sink source · line 1220 · raw

@aa:Array<U32> -> U32

def decode.depth.of source · line 1225 · raw

@zero:Bool -> @+nn:U32 -> Nat

the depth of a plane of nn points: 0 for none, else log2(2 * nn - 1) in U32, so 2^depth >= nn while 2 * nn does not wrap

def decode.depth source · line 1233 · raw

@+nn:U32 -> Nat

U32.is_eq, not a literal pattern, so a law reaches every nn

def decode.plane source · line 1236 · raw

@+nn:U32 -> Array<U32>

def decode.emit source · line 1241 · raw

@left:Nat -> @got:Pair(Array<U32>, U32) -> @+ii:U32 -> 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.points source · line 1254 · raw

@+nn:Nat -> @plane:Array<U32> -> List<&2, U32>

the first nn points of a plane, in order

def opaque source · line 1260 · raw

@+xx:U32 -> U32

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 without a case split on the sample's bits.

def rgb.ch.hi source · line 1264 · raw

@+qq:U32 -> U32

a channel clamped from above: 255 for a quotient past it

def rgb.ch.lt source · line 1269 · raw

@lt:Bool -> @+pos:U32 -> @+neg:U32 -> U32

a channel whose value, plus one half, is below zero is 0; otherwise the whole millions in pos - neg

def rgb.ch source · line 1281 · raw

@+pos:U32 -> @+neg:U32 -> U32

one channel of T.871 rounded to nearest and clamped to 0..255, from its value in millionths split into what is added (pos, with the half for rounding already in) and what is subtracted (neg). For inputs 0..255 both stay below 2^32, so the arithmetic is exact: no fixed-point constant and one rounding per channel.

def rgb.bits source · line 1289 · raw

@+yy:U32 -> @+cb:U32 -> @+cr:U32 -> U32

YCbCr to colour bits, (R << 16) | (G << 8) | B, per JFIF T.871 exactly: R = Y + 1.402 (Cr - 128), G = Y - 0.344136 (Cb - 128) - 0.714136 (Cr - 128), B = Y + 1.772 (Cb - 128), each rounded to nearest and clamped. The 128 offsets are the constants 179456000 = 128 * 1402000, 135458816 = 128 * (344136 + 714136) and 226816000 = 128 * 1772000.

def rgb source · line 1296 · raw

@+yy:U32 -> @+cb:U32 -> @+cr:U32 -> U32

YCbCr to a packed opaque sample, 0xFFRRGGBB

def gray.bits source · line 1300 · raw

@+yy:U32 -> U32

a gray level's low byte in R, G and B

def gray source · line 1305 · raw

@+yy:U32 -> U32

a gray level as a packed opaque sample, 0xFFvvvvvv

def decode.grays source · line 1309 · raw

@ys:List<&2, U32> -> List<&2, U32>

every gray level of a picture as a packed opaque sample

def decode.rgbs source · line 1317 · raw

@ys:List<&2, U32> -> @bs:List<&2, U32> -> @rs:List<&2, U32> -> List<&2, U32>

every Y, Cb, Cr triple of a picture as a packed opaque sample, as many as the shortest list holds

def decode.done.drop source · line 1338 · raw

@yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

def decode.done.gray source · line 1344 · raw

@+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

def decode.done.color source · line 1350 · raw

@+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

a colour picture: each point's Y, Cb and Cr read out in order, then packed

def decode.done.nf3 source · line 1355 · raw

@three:Bool -> @+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

three components are colour; any other count is none

def decode.done.nf1 source · line 1363 · raw

@one:Bool -> @+nf:U32 -> @+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

one component is gray; the rest is decided by decode.done.nf3

def decode.done.nf source · line 1379 · raw

@+nf:U32 -> @+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

the picture by its component count. U32.is_eq, not a literal pattern, so a law reaches every count.

def decode.done.ok source · line 1383 · raw

@bad:Bool -> @frame:Frame -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

a failed scan is none; otherwise the picture by the frame's component count

def decode.done source · line 1393 · raw

@+ok:U32 -> @frame:Frame -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

the planes as a picture, or none when ok is 0

def decode.adv.ctrl source · line 1396 · raw

@adv:Adv -> Ctrl

def decode.adv.duef source · line 1401 · raw

@adv:Adv -> U32

def decode.blocks source · line 1406 · raw

@left:Nat -> @blk:Blk -> @+ctrl:Ctrl -> @+preds:Preds -> @+frame:Frame -> @+scan:Scan -> @+tabs:Tabs -> @+ri:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> @+ok:U32 -> Maybe<&2, Pic>

def decode.blocks.sum source · line 1440 · raw

@hs:List<&2, U32> -> @vs:List<&2, U32> -> @+nn:U32 -> U32

def decode.start source · line 1453 · raw

@nn:Nat -> @bits:Bits -> @+frame:Frame -> @+scan:Scan -> @+tabs:Tabs -> @+ri:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

def decode.nblocks source · line 1473 · raw

@+ww:U32 -> @+hh:U32 -> @+hs:List<&2, U32> -> @+vs:List<&2, U32> -> @+hmax:U32 -> @+vmax:U32 -> U32

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.run.n source · line 1483 · raw

@empty:Bool -> @+ww:U32 -> @+hh:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> Maybe<&2, Pic>

def decode.run source · line 1502 · raw

@frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> Maybe<&2, Pic>

def decode.finish.ok source · line 1507 · raw

@ok1:Bool -> @ok2:Bool -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> Maybe<&2, Pic>

def decode.finish.ph source · line 1526 · raw

@phase:Phase -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> Maybe<&2, Pic>

def decode.finish source · line 1542 · raw

@st:St -> Maybe<&2, Pic>

def decode.max.b source · line 1547 · raw

@gt:Bool -> @+aa:U32 -> @+bb:U32 -> U32

def decode.max source · line 1554 · raw

@+aa:U32 -> @+bb:U32 -> U32

def decode.vmax source · line 1557 · raw

@vs:List<&2, U32> -> @+mm:U32 -> U32

def decode.fac.ok source · line 1566 · raw

@+ff:U32 -> Bool

a sampling factor the decoder places: 1, 2 or 4 (IMG-JPG-2). A Bool of U32.is_eq, not a match on literals, so a law can case-split on it.

def decode.fac.pair source · line 1571 · raw

@+hv:U32 -> Bool

both sampling factors of one SOF component byte, H in the high nibble and V in the low nibble, are ones the decoder places

def decode.nf.ok source · line 1575 · raw

@+nf:U32 -> Bool

a component count the decoder reads: 1 (gray) or 3 (YCbCr)

def decode.u16 source · line 1578 · raw

@+hi:U32 -> @+lo:U32 -> U32

def decode.comps.rev source · line 1581 · raw

@cc:Comps -> Comps

def decode.read.cs source · line 1587 · raw

@left:Nat -> @xs:List<&2, U32> -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @tqs:List<&2, U32> -> @ok:Bool -> Comps

def decode.read.sof.ok source · line 1610 · raw

@good:Bool -> @zmax:Bool -> @+ww:U32 -> @+hh:U32 -> @+nf:U32 -> @ids:List<&2, U32> -> @+hs:List<&2, U32> -> @+vs:List<&2, U32> -> @tq:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> St

def decode.read.sof.c source · line 1643 · raw

@cok:Bool -> @good:Bool -> @zmax:Bool -> @+ww:U32 -> @+hh:U32 -> @+nf:U32 -> @ids:List<&2, U32> -> @+hs:List<&2, U32> -> @+vs:List<&2, U32> -> @tq:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> St

the components first: a factor outside 1, 2 and 4, or a short component list, refuses the file before the count and the refusals so far are asked

def decode.read.sof.f source · line 1666 · raw

@cc:Comps -> @+ww:U32 -> @+hh:U32 -> @+nf:U32 -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sof.p source · line 1684 · raw

@p8:Bool -> @xs:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

the SOF0 body after its precision byte: precision 8 goes on to the size and the components, any other stops

def decode.read.sof source · line 1706 · raw

@xs:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

an SOF0 body. The precision is compared with U32.is_eq, not a literal pattern, so a law reaches it.

def decode.take source · line 1721 · raw

@left:Nat -> @xs:List<&2, U32> -> @acc:List<&2, U32> -> Pair(List<&2, U32>, List<&2, U32>)

def decode.q.put source · line 1732 · raw

@tabs:Tabs -> @+id:U32 -> @vals:List<&2, U32> -> Tabs

def decode.read.dqt source · line 1745 · raw

@xs:List<&2, U32> -> @ok:Bool -> @phase:Nat -> @+id:U32 -> @acc:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.sum.counts source · line 1794 · raw

@xs:List<&2, U32> -> @+nn:U32 -> U32

def decode.huff.put.dc source · line 1801 · raw

@+id:U32 -> @hh:Huff -> @q0:List<&2, U32> -> @q1:List<&2, U32> -> @q2:List<&2, U32> -> @q3:List<&2, U32> -> @dc0:Huff -> @dc1:Huff -> @dc2:Huff -> @dc3:Huff -> @ac0:Huff -> @ac1:Huff -> @ac2:Huff -> @ac3:Huff -> Tabs

def decode.huff.put.ac source · line 1827 · raw

@+id:U32 -> @hh:Huff -> @q0:List<&2, U32> -> @q1:List<&2, U32> -> @q2:List<&2, U32> -> @q3:List<&2, U32> -> @dc0:Huff -> @dc1:Huff -> @dc2:Huff -> @dc3:Huff -> @ac0:Huff -> @ac1:Huff -> @ac2:Huff -> @ac3:Huff -> Tabs

def decode.huff.put source · line 1853 · raw

@tabs:Tabs -> @+cls:U32 -> @+id:U32 -> @hh:Huff -> Tabs

def decode.read.dht source · line 1862 · raw

@xs:List<&2, U32> -> @ok:Bool -> @sym:Bool -> @phase:Nat -> @+cls:U32 -> @+id:U32 -> @+counts:List<&2, U32> -> @+syms:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.scan.rev source · line 1953 · raw

@sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> Scan

def decode.read.sos.ok source · line 1956 · raw

@ss0:Bool -> @se63:Bool -> @ah0:Bool -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sos.end source · line 1985 · raw

@xs:List<&2, U32> -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sos.cs source · line 2005 · raw

@left:Nat -> @xs:List<&2, U32> -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sos source · line 2030 · raw

@xs:List<&2, U32> -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.dri source · line 2045 · raw

@xs:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.app0.den source · line 2060 · raw

@xz:Bool -> @yz:Bool -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.app0.id source · line 2082 · raw

@jfif:Bool -> @+xh:U32 -> @+xl:U32 -> @+yh:U32 -> @+yl:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

an APP0 body that opens with the JFIF identifier has its density checked; any other is skipped

def decode.read.app0 source · line 2104 · raw

@xs:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

an APP0 body. The identifier is compared with U32.is_eq, not literal patterns, so a law reaches it.

def decode.dispatch source · line 2121 · raw

@+mark:U32 -> @xs:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.between source · line 2148 · raw

@+bb:U32 -> @+lo:U32 -> @+hi:U32 -> Bool

def decode.mark.range.b source · line 2151 · raw

@sof:Bool -> @app:Bool -> @rst:Bool -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.mark.range source · line 2178 · raw

@+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.mark source · line 2191 · raw

@+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.pay0 source · line 2225 · raw

@left:Nat -> @+mark:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.len.b source · line 2242 · raw

@small:Bool -> @+mark:U32 -> @+len:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.last source · line 2260 · raw

@left:Nat -> @+bb:U32 -> @+mark:U32 -> @acc:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.pay source · line 2279 · raw

@left:Nat -> @+bb:U32 -> @+mark:U32 -> @acc:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.ent.rst.b source · line 2298 · raw

@rst:Bool -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.ent source · line 2317 · raw

@ff:Bool -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

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.ph source · line 2335 · raw

@phase:Phase -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step source · line 2377 · raw

@+bb:U32 -> @st:St -> St

def decode.walk source · line 2382 · raw

@xs:List<&2, U32> -> @st:St -> St

def soi source · line 2390 · raw

List<&2, U32>

the JPEG start-of-image marker, FF D8

def eoi source · line 2394 · raw

List<&2, U32>

the JPEG end-of-image marker, FF D9

def decode source · line 2398 · raw

@bytes:List<&2, U32> -> Maybe<&2, Pic>

baseline JPEG bytes, or none when the frame is not sequential Huffman