src/png.bend checks

raw source on the hub · import 0x83c5c81fb41f55ca634bdc7bde39a51b/src/png.bend as Png

src/png: PNG decode and encode (ISO/IEC 15948 / W3C PNG). Chunks, IHDR, zlib method 0, and filter method 0. Decode reads 8-bit colour types 0, 2, 3, 4, and 6. Encode writes colour type 2 or 6, filter None, and a stored IDAT.

3 imports

import Base
import ./crc.bend as Crc
import ./inflate.bend as Inf

Types

type Pic source · line 9 · raw

Data

a decoded picture: width, height, and 0xAARRGGBB samples

Pic

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

type Ihdr source · line 13 · raw

Data

IHDR fields, in specification order

Ihdr

@+w:U32 -> @+h:U32 -> @+depth:U32 -> @+colour:U32 -> @+comp:U32 -> @+filter:U32 -> @+inter:U32 -> Ihdr

type Pz source · line 17 · raw

Data

chunk reader phase

ZLen
```
Pz
```
ZTyp
```
Pz
```
ZDat
```
Pz
```
ZCrc
```
Pz
```

type Pg source · line 24 · raw

Data

image state while chunks are read

Pg

@+w:U32 -> @+h:U32 -> @+depth:U32 -> @+colour:U32 -> @+comp:U32 -> @+filt:U32 -> @+inter:U32 -> @idat:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @idat_done:Bool -> @saw_trns:Bool -> @iend:Bool -> Pg

type Nx source · line 32 · raw

Data

a chunk was rejected, ended the image, or left more chunks

NBad
```
Nx
```
NEnd
```
@pg:Pg -> Nx
```
NMore
```
@pg:Pg -> Nx
```

type Uf source · line 38 · raw

Data

scanline phase

UFilt
```
Uf
```
UBody
```
Uf
```
UBad
```
Uf
```

type Key source · line 44 · raw

Data

transparency key carried by tRNS

KNone
```
Key
```
KBad
```
Key
```
KGrey
```
@+g:U32 -> Key
```
KRgb
```
@+r:U32 -> @+g:U32 -> @+b:U32 -> Key
```

Definitions

def be.u32 source · line 51 · raw

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

big-endian unsigned 32

def tag.ihdr source · line 55 · raw

U32

IHDR

def tag.idat source · line 59 · raw

U32

IDAT

def tag.iend source · line 63 · raw

U32

IEND

def tag.plte source · line 67 · raw

U32

PLTE

def tag.trns source · line 71 · raw

U32

tRNS

def tag.anc source · line 75 · raw

@+typ:U32 -> Bool

the ancillary bit of a chunk type (bit 5 of the first byte)

def png.col source · line 79 · raw

@+cc:U32 -> Bool

colour types this decoder accepts

def png.good source · line 86 · raw

@+ww:U32 -> @+hh:U32 -> @+dd:U32 -> @+cc:U32 -> @+comp:U32 -> @+ff:U32 -> @+ii:U32 -> Bool

IHDR constraints for the supported subset

def pg.empty source · line 96 · raw

Pg

an empty image state

def pg.ihdr source · line 100 · raw

@+ww:U32 -> @+hh:U32 -> @+dd:U32 -> @+cc:U32 -> @+comp:U32 -> @+ff:U32 -> @+ii:U32 -> Pg

state after a valid IHDR

def png.seal source · line 104 · raw

@pg:Pg -> Pg

close the IDAT sequence once a later chunk appears

def png.bpp.ix source · line 110 · raw

@z3:Bool -> U32

def png.bpp.one source · line 117 · raw

@z0:Bool -> @z3:Bool -> U32

def png.bpp6 source · line 124 · raw

@z6:Bool -> @+cc:U32 -> U32

def png.bpp4 source · line 131 · raw

@z4:Bool -> @z6:Bool -> @+cc:U32 -> U32

def png.bpp0 source · line 138 · raw

@z2:Bool -> @z4:Bool -> @z6:Bool -> @+cc:U32 -> U32

def png.bpp source · line 146 · raw

@+cc:U32 -> U32

bytes per pixel for an 8-bit colour type

def parse_ihdr source · line 151 · raw

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

ISO/IEC 15948 / W3C PNG — IHDR is width, height, bit depth, colour type, compression method, filter method, and interlace method, each big-endian.

def uf.nth source · line 160 · raw

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

def uf.back source · line 171 · raw

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

the byte bpp back, or zero before the first pixel: xs holds the bytes before this one in the row, newest first, so it is too short there

def uf.bb source · line 174 · raw

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

def uf.drop source · line 181 · raw

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

def uf.push source · line 188 · raw

@prest:List<&2, U32> -> @phist:List<&2, U32> -> List<&2, U32>

def uf.abs.at source · line 191 · raw

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

def uf.abs source · line 198 · raw

@+xx:U32 -> @+yy:U32 -> U32

def uf.paeth.b source · line 201 · raw

@zb:Bool -> @+bb:U32 -> @+cc:U32 -> U32

def uf.paeth.at source · line 208 · raw

@za:Bool -> @zb:Bool -> @+aa:U32 -> @+bb:U32 -> @+cc:U32 -> U32

def uf.paeth source · line 216 · raw

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

PaethPredictor from the PNG specification

def uf.avg source · line 222 · raw

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

def uf.add source · line 226 · raw

@+ff:U32 -> @+pp:U32 -> U32

a reconstructed byte: filtered byte plus predictor, mod 256 (mask first)

def uf.p4 source · line 229 · raw

@z4:Bool -> @+aa:U32 -> @+bb:U32 -> @+cc:U32 -> U32

def uf.p3 source · line 236 · raw

@z3:Bool -> @z4:Bool -> @+aa:U32 -> @+bb:U32 -> @+cc:U32 -> U32

def uf.p2 source · line 243 · raw

@z2:Bool -> @z3:Bool -> @z4:Bool -> @+aa:U32 -> @+bb:U32 -> @+cc:U32 -> U32

def uf.p1 source · line 250 · raw

@z1:Bool -> @z2:Bool -> @z3:Bool -> @z4:Bool -> @+aa:U32 -> @+bb:U32 -> @+cc:U32 -> U32

def uf.pred source · line 257 · raw

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

def uf.recon source · line 260 · raw

@+ff:U32 -> @+ft:U32 -> @+bpp:U32 -> @prest:List<&2, U32> -> @phist:List<&2, U32> -> @cur:List<&2, U32> -> U32

def uf.phase source · line 270 · raw

@zz:Bool -> Uf

def uf.ok source · line 277 · raw

@+ww:U32 -> @+hh:U32 -> @+bpp:U32 -> Bool

def uf.done source · line 280 · raw

@rows:Nat -> @all:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def uf.go source · line 290 · raw

@xs:List<&2, U32> -> @ph:Uf -> @zlast:Bool -> @+bpp:U32 -> @+stride:U32 -> @rows:Nat -> @+prest:List<&2, U32> -> @+phist:List<&2, U32> -> @+cur:List<&2, U32> -> @all:List<&2, U32> -> @+left:U32 -> @+ft:U32 -> Maybe<&2, List<&2, U32>>

walk the filtered stream: a filter byte opens each row (UFilt), then its bytes (UBody). left counts the row's bytes after the current one, and zlast, whether it is zero, marks the row's last byte.

def uf.start source · line 336 · raw

@zz:Bool -> @raw:List<&2, U32> -> @+ww:U32 -> @+hh:U32 -> @+bpp:U32 -> Maybe<&2, List<&2, U32>>

def unfilter source · line 344 · raw

@raw:List<&2, U32> -> @+ww:U32 -> @+hh:U32 -> @+bpp:U32 -> Maybe<&2, List<&2, U32>>

ISO/IEC 15948 / W3C PNG — undo filter types None, Sub, Up, Average, and Paeth.

def px.pack source · line 349 · raw

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

def px.hit.at source · line 352 · raw

@zz:Bool -> U32

def px.hit source · line 359 · raw

@+ss:U32 -> @+kk:U32 -> U32

def px.rgb.hit source · line 362 · raw

@+rr:U32 -> @+gg:U32 -> @+bb:U32 -> @+kr:U32 -> @+kg:U32 -> @+kb:U32 -> U32

def px.grey source · line 365 · raw

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

def px.rgb source · line 376 · raw

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

def px.ga source · line 387 · raw

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

def px.rgba source · line 396 · raw

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

def px.at source · line 405 · raw

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

def px.use source · line 414 · raw

@mm:Maybe<&2, U32> -> @kk:(@_:U32 -> Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>

def px.idx source · line 421 · raw

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

def pal.make source · line 430 · raw

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

the palette's entries, 0xAARRGGBB, each alpha from tRNS while it lasts and 255 after; none when PLTE is not whole entries

def png.le source · line 441 · raw

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

def pal.gate source · line 445 · raw

@zz:Bool -> @pxs:List<&2, U32> -> Maybe<&2, List<&2, U32>>

the palette, when tRNS has no more entries than it

def pal.ready source · line 453 · raw

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

check tRNS against the palette's length

def px.indexed.at source · line 460 · raw

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

def px.indexed source · line 467 · raw

@samples:List<&2, U32> -> @plte:List<&2, U32> -> @+trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def key.grey source · line 470 · raw

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

def key.rgb source · line 479 · raw

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

def key.none source · line 488 · raw

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

def px.ga.ok source · line 495 · raw

@key:Key -> @samples:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.rgba.ok source · line 502 · raw

@key:Key -> @samples:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.rgba.go source · line 509 · raw

@samples:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.k4 source · line 512 · raw

@z6:Bool -> @samples:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.k3 source · line 519 · raw

@z4:Bool -> @z6:Bool -> @samples:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.k2 source · line 532 · raw

@z2:Bool -> @z4:Bool -> @z6:Bool -> @samples:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.k0 source · line 546 · raw

@z0:Bool -> @z2:Bool -> @z4:Bool -> @z6:Bool -> @samples:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def px.of source · line 561 · raw

@+colour:U32 -> @samples:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def png.mod3 source · line 566 · raw

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

def png.ihdr.ok source · line 570 · raw

@zz:Bool -> @+ww:U32 -> @+hh:U32 -> @+dd:U32 -> @+cc:U32 -> @+comp:U32 -> @+ff:U32 -> @+ii:U32 -> Nx

def png.ihdr.put source · line 577 · raw

@mm:Maybe<&2, Ihdr> -> Nx

def png.allow source · line 584 · raw

@zz:Bool -> @pg:Pg -> Nx

def pg.idat source · line 591 · raw

@pg:Pg -> @extra:List<&2, U32> -> Pg

def pg.plte source · line 597 · raw

@pg:Pg -> @bytes:List<&2, U32> -> Pg

def pg.trns source · line 602 · raw

@pg:Pg -> @bytes:List<&2, U32> -> Pg

def pg.iend source · line 607 · raw

@pg:Pg -> Pg

def png.idat.try source · line 612 · raw

@zz:Bool -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.on.ihdr source · line 619 · raw

@ihdr:Bool -> @data:List<&2, U32> -> Nx

def png.on.idat source · line 626 · raw

@ihdr:Bool -> @idat_done:Bool -> @need:Bool -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.plte.ok source · line 633 · raw

@+cc:U32 -> Bool

def png.trns.ok source · line 636 · raw

@+cc:U32 -> @saw_plte:Bool -> Bool

def png.on.plte source · line 642 · raw

@ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @+colour:U32 -> @+data:List<&2, U32> -> @pg:Pg -> Nx

def png.on.trns source · line 652 · raw

@ihdr:Bool -> @saw_trns:Bool -> @saw_idat:Bool -> @+colour:U32 -> @saw_plte:Bool -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.iend.ok source · line 670 · raw

@zz:Bool -> @pg:Pg -> Nx

def png.iend.at source · line 677 · raw

@zempty:Bool -> @zpal:Bool -> @pg:Pg -> Nx

def png.on.iend source · line 684 · raw

@ihdr:Bool -> @+colour:U32 -> @saw_plte:Bool -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.other.at source · line 691 · raw

@anc:Bool -> @pg:Pg -> Nx

def png.on.other source · line 698 · raw

@ihdr:Bool -> @anc:Bool -> @pg:Pg -> Nx

def png.apply.tr source · line 705 · raw

@ztrns:Bool -> @anc:Bool -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @saw_trns:Bool -> @+colour:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.apply.pl source · line 722 · raw

@zplte:Bool -> @ztrns:Bool -> @anc:Bool -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @saw_trns:Bool -> @+colour:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.apply.ie source · line 740 · raw

@ziend:Bool -> @zplte:Bool -> @ztrns:Bool -> @anc:Bool -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @saw_trns:Bool -> @+colour:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.apply.id source · line 759 · raw

@zidat:Bool -> @ziend:Bool -> @zplte:Bool -> @ztrns:Bool -> @anc:Bool -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @idat_done:Bool -> @saw_trns:Bool -> @+colour:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.apply.go source · line 780 · raw

@zihdr:Bool -> @zidat:Bool -> @ziend:Bool -> @zplte:Bool -> @ztrns:Bool -> @anc:Bool -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @idat_done:Bool -> @saw_trns:Bool -> @+colour:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.apply.at source · line 802 · raw

@iend:Bool -> @zihdr:Bool -> @zidat:Bool -> @ziend:Bool -> @zplte:Bool -> @ztrns:Bool -> @anc:Bool -> @ihdr:Bool -> @saw_plte:Bool -> @saw_idat:Bool -> @idat_done:Bool -> @saw_trns:Bool -> @+colour:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.apply source · line 826 · raw

@+typ:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.judge.at source · line 837 · raw

@zz:Bool -> @+typ:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.judge source · line 844 · raw

@+got:U32 -> @crc:List<&2, U32> -> @+typ:U32 -> @data:List<&2, U32> -> @pg:Pg -> Nx

def png.pgof source · line 847 · raw

@nx:Nx -> Pg

def png.zp source · line 856 · raw

@zz:Bool -> Pz

def png.pic source · line 863 · raw

@mm:Maybe<&2, List<&2, U32>> -> @+ww:U32 -> @+hh:U32 -> Maybe<&2, Pic>

def png.pack source · line 870 · raw

@mm:Maybe<&2, List<&2, U32>> -> @+ww:U32 -> @+hh:U32 -> @+colour:U32 -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, Pic>

def png.samples source · line 884 · raw

@mm:Maybe<&2, List<&2, U32>> -> @+ww:U32 -> @+hh:U32 -> @+colour:U32 -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, Pic>

def png.finish.go source · line 898 · raw

@zenc:Bool -> @+ww:U32 -> @+hh:U32 -> @+colour:U32 -> @idat:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, Pic>

def png.finish.at source · line 913 · raw

@zz:Bool -> @zenc:Bool -> @+ww:U32 -> @+hh:U32 -> @+colour:U32 -> @idat:List<&2, U32> -> @plte:List<&2, U32> -> @trns:List<&2, U32> -> Maybe<&2, Pic>

def png.finish source · line 929 · raw

@pg:Pg -> Maybe<&2, Pic>

def png.crc source · line 935 · raw

@nx:Nx -> @empty:Bool -> @more:Maybe<&2, Pic> -> Maybe<&2, Pic>

def png.go source · line 947 · raw

@xs:List<&2, U32> -> @pz:Pz -> @zlast:Bool -> @+left:U32 -> @+typ:U32 -> @crc:List<&2, U32> -> @data:List<&2, U32> -> @pg:Pg -> Maybe<&2, Pic>

one byte of a PNG chunk stream. zlast is the last data byte of the chunk.

def decode source · line 981 · raw

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

ISO/IEC 15948 / W3C PNG — chunks after the signature, CRC-32 over type and data, then IDAT inflated as zlib DEFLATE (compression method 0).

def enc.byte source · line 987 · raw

@+nn:U32 -> U32

the low byte

def enc.hi source · line 991 · raw

@+nn:U32 -> U32

the next byte up

def enc.be source · line 995 · raw

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

four bytes, big-endian

def enc.a source · line 999 · raw

@+cc:U32 -> U32

alpha of a 0xAARRGGBB sample

def enc.r source · line 1003 · raw

@+cc:U32 -> U32

red of a 0xAARRGGBB sample

def enc.g source · line 1007 · raw

@+cc:U32 -> U32

green of a 0xAARRGGBB sample

def enc.b source · line 1011 · raw

@+cc:U32 -> U32

blue of a 0xAARRGGBB sample

def enc.push.rgb source · line 1015 · raw

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

one opaque pixel, newest-first, so a later reverse is R, G, B

def enc.push.rgba source · line 1019 · raw

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

one pixel, newest-first, so a later reverse is R, G, B, A

def enc.push source · line 1023 · raw

@op:Bool -> @+cc:U32 -> @acc:List<&2, U32> -> List<&2, U32>

the channels of one sample

def enc.pred source · line 1031 · raw

@nn:Nat -> Nat

one less, or zero

def enc.len source · line 1039 · raw

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

how many bytes, counted in a word

def enc.cat.go source · line 1047 · raw

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

a reversed prefix, consed onto the suffix

def enc.cat source · line 1055 · raw

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

xs, then ys

def enc.nch source · line 1059 · raw

@op:Bool -> U32

channels written for one sample

def enc.raw source · line 1070 · raw

@px:List<&2, U32> -> @left:Nat -> @+ww:Nat -> @+op:Bool -> @acc:List<&2, U32> -> @+nn:U32 -> Pair(List<&2, U32>, U32)

scanlines, filter None, newest-first. left is 0 at the first sample of a row, where the filter byte is written; otherwise it is the samples still to come after this one. n is how many bytes are in acc. One reverse at the end puts the bytes in order.

def enc.head source · line 1088 · raw

@fin:Bool -> @+len:U32 -> @+nlen:U32 -> List<&2, U32>

the five-byte stored-block header: BFINAL, then LEN and NLEN, little-endian

def enc.stored source · line 1096 · raw

@fin:Bool -> @+data:List<&2, U32> -> List<&2, U32>

one stored DEFLATE block. data is chronological.

def enc.feed source · line 1102 · raw

@xs:List<&2, U32> -> @zz:Bool -> @+room:U32 -> @+max:U32 -> @acc:List<&2, U32> -> List<&2, U32>

stored blocks of at most max bytes. z means this byte opens a block. acc is the open block, newest-first.

def enc.blocks.fit source · line 1121 · raw

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

one final stored block when the payload already fits

def enc.blocks source · line 1129 · raw

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

stored DEFLATE blocks, each at most max bytes, the last one final

def enc.chunk source · line 1134 · raw

@+tag:U32 -> @+data:List<&2, U32> -> List<&2, U32>

a chunk: length, type, data, and CRC-32 over the type and the data

def enc.ihdr source · line 1141 · raw

@+ww:U32 -> @+hh:U32 -> @+ct:U32 -> List<&2, U32>

IHDR: width, height, depth 8, colour type, method 0, filter 0, interlace 0

def enc.sig source · line 1145 · raw

List<&2, U32>

the eight-byte signature

def enc.ct source · line 1149 · raw

@op:Bool -> U32

colour type 2 when opaque, otherwise 6

def enc.zlib source · line 1158 · raw

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

zlib wrapper, CMF/FLG 120 1, around stored DEFLATE blocks and an Adler-32. n is the length of raw, already counted while the scanlines were built.

def enc.nblk.at source · line 1163 · raw

@zz:Bool -> @+qq:U32 -> U32

how many stored blocks cover n raw bytes

def enc.nblk source · line 1171 · raw

@+nn:U32 -> U32

ceil(n / 65535). An exact multiple stays q.

def enc.idat.ln source · line 1175 · raw

@+nn:U32 -> U32

IDAT data length: zlib header, stored-block headers, raw bytes, Adler-32

def enc.crc.list source · line 1179 · raw

@xs:List<&2, U32> -> @+cc:U32 -> @acc:List<&2, U32> -> Pair(U32, List<&2, U32>)

CRC-32 and cons chronological bytes onto a newest-first accumulator

def enc.cap.at source · line 1187 · raw

@zz:Bool -> @+nn:U32 -> U32

the stored-block length: the bytes still open, at most 65535

def enc.cap source · line 1195 · raw

@+nn:U32 -> U32

min(n, 65535)

def enc.bf.at source · line 1199 · raw

@zz:Bool -> U32

BFINAL is 1 when this block holds every byte still open

def enc.bf source · line 1207 · raw

@+nn:U32 -> U32

1 when n fits in one stored block, otherwise 0

def enc.pour source · line 1214 · raw

@xs:List<&2, U32> -> @znew:Bool -> @zlast:Bool -> @+room:U32 -> @+left:U32 -> @+len:U32 -> @+bf:U32 -> @+cc:U32 -> @acc:List<&2, U32> -> Pair(U32, List<&2, U32>)

stored blocks, newest-first, CRC running over headers and data. znew means this byte opens a block of length len with BFINAL bf. zlast means this data byte closes the block. room is the data bytes left in the open block, including this one. left counts raw bytes still to come, including h.

def enc.seal.crc source · line 1263 · raw

@pp:Pair(U32, List<&2, U32>) -> @ie:List<&2, U32> -> List<&2, U32>

Adler-32, then the CRC field, then IEND, then one reverse of the whole file

def enc.seal.adler source · line 1270 · raw

@pp:Pair(U32, List<&2, U32>) -> @+sum:U32 -> @ie:List<&2, U32> -> List<&2, U32>

the four Adler bytes belong to the IDAT data and to its CRC

def enc.seal.run source · line 1276 · raw

@pp:Pair(U32, List<&2, U32>) -> @raw:List<&2, U32> -> @+nn:U32 -> @+sum:U32 -> @ie:List<&2, U32> -> List<&2, U32>

zlib header, then the stored blocks

def enc.seal.body source · line 1288 · raw

@pp:Pair(U32, List<&2, U32>) -> @raw:List<&2, U32> -> @+nn:U32 -> @+sum:U32 -> @ie:List<&2, U32> -> List<&2, U32>

IDAT type, then the zlib stream

def enc.add.at source · line 1300 · raw

@zz:Bool -> @+tt:U32 -> U32

Adler-32 reduced once. The sum stays below twice the modulus.

def enc.add source · line 1308 · raw

@+ss:U32 -> @+xx:U32 -> U32

one Adler-32 add, modulo 65521

def enc.rgb.fin source · line 1313 · raw

@+cc:U32 -> @acc:List<&2, U32> -> @+aa:U32 -> @+bb:U32 -> Pair(Pair(U32, List<&2, U32>), U32)

the running CRC, the newest-first bytes, and the packed Adler-32

def enc.rgb.go source · line 1320 · raw

@fuel:Nat -> @zblock:Bool -> @zdone:Bool -> @zspan:Bool -> @zneed:Bool -> @filt:Bool -> @zred:Bool -> @zgrn:Bool -> @zlast:Bool -> @px:List<&2, U32> -> @+col:U32 -> @+row:U32 -> @+ww:U32 -> @+need:U32 -> @+cc:U32 -> @acc:List<&2, U32> -> @+aa:U32 -> @+bb:U32 -> @+left:U32 -> @+len:U32 -> Pair(Pair(U32, List<&2, U32>), U32)

stored blocks for colour type 2, one decreasing step at a time. zblock opens a block and zspan counts its raw bytes. The other flags are the cursor: a filter byte, red, green, or the last sample of the row. Block headers match enc.pour. Adler-32 covers the raw bytes only.

def enc.wide.rgb.out source · line 1459 · raw

@pp:Pair(Pair(U32, List<&2, U32>), U32) -> @ie:List<&2, U32> -> List<&2, U32>

def enc.wide.rgb.z source · line 1465 · raw

@pp:Pair(U32, List<&2, U32>) -> @px:List<&2, U32> -> @+ww:U32 -> @+nn:U32 -> @ie:List<&2, U32> -> List<&2, U32>

zlib header, then the stored blocks written from the samples

def enc.wide.rgb.go source · line 1482 · raw

@pp:Pair(U32, List<&2, U32>) -> @px:List<&2, U32> -> @+ww:U32 -> @+nn:U32 -> @ie:List<&2, U32> -> List<&2, U32>

IDAT type, then the zlib stream

def enc.wide.rgb source · line 1496 · raw

@+ww:U32 -> @+hh:U32 -> @px:List<&2, U32> -> @+nn:U32 -> List<&2, U32>

a colour-type-2 picture whose filtered bytes do not fit in one stored block. Each filter and channel byte is consed into its stored block, with Adler-32 and the IDAT CRC, so the raw scanline list is not built.

def enc.seal.wide source · line 1505 · raw

@+ww:U32 -> @+hh:U32 -> @op:Bool -> @+raw:List<&2, U32> -> @+nn:U32 -> List<&2, U32>

one picture whose filtered bytes do not fit in a single stored block. Signature, IHDR, the IDAT length, and the payload are consed newest-first and reversed once. Adler-32 stays a separate pass over the raw bytes.

def enc.seal.one source · line 1519 · raw

@+ww:U32 -> @+hh:U32 -> @op:Bool -> @+raw:List<&2, U32> -> @+nn:U32 -> List<&2, U32>

signature, IHDR, IDAT, IEND when the raw bytes fit in one stored block

def enc.seal.at source · line 1525 · raw

@zz:Bool -> @+ww:U32 -> @+hh:U32 -> @op:Bool -> @raw:List<&2, U32> -> @+nn:U32 -> List<&2, U32>

one stored block when the payload fits; several blocks written once otherwise

def enc.seal source · line 1540 · raw

@+ww:U32 -> @+hh:U32 -> @op:Bool -> @got:Pair(List<&2, U32>, U32) -> List<&2, U32>

signature, IHDR, IDAT, IEND

def enc.opaque source · line 1546 · raw

@px:List<&2, U32> -> @zz:Bool -> Bool

every sample so far is opaque, and z carries that fact forward

def enc.area source · line 1556 · raw

@+ww:U32 -> @+hh:U32 -> Bool

width times height fits in a U32

def enc.good source · line 1560 · raw

@+ww:U32 -> @+hh:U32 -> @px:List<&2, U32> -> Bool

a positive area whose sample list covers it

def enc.nbytes source · line 1566 · raw

@op:Bool -> @+ww:U32 -> @+hh:U32 -> U32

filtered bytes: one per row, plus the channels of every sample

def enc.paint.wide source · line 1571 · raw

@op:Bool -> @+ww:U32 -> @+hh:U32 -> @px:List<&2, U32> -> @+nn:U32 -> List<&2, U32>

colour type 6, and a colour type 2 that fits in one block, still build the raw list. A larger colour type 2 writes its stored blocks from the samples.

def enc.paint.at source · line 1584 · raw

@zz:Bool -> @+ww:U32 -> @+hh:U32 -> @+op:Bool -> @px:List<&2, U32> -> @+nn:U32 -> List<&2, U32>

def enc.paint source · line 1599 · raw

@+ww:U32 -> @+hh:U32 -> @+op:Bool -> @px:List<&2, U32> -> List<&2, U32>

the PNG bytes of a picture already known to be in range

def enc.open source · line 1604 · raw

@zz:Bool -> @+ww:U32 -> @+hh:U32 -> @+px:List<&2, U32> -> Maybe<&2, List<&2, U32>>

the bytes, or none when the picture is not encodable

def enc.file source · line 1613 · raw

@+ww:U32 -> @+hh:U32 -> @+px:List<&2, U32> -> Maybe<&2, List<&2, U32>>

ISO/IEC 15948 / W3C PNG — an 8-bit encoding, interlace 0, filter None. Colour type 2 when every sample is opaque, otherwise colour type 6.