zlib.bend checks

raw source on the hub · import 0xfa97cc8246066bff0b9237beb9af14d2/zlib.bend as Zlib

DEFLATE, gzip, and zlib decoding (RFC 1951, 1952, 1950) over byte strings.

1 import

import Base

Types

type Br source · line 17 · raw

Data

Bit reader. over counts bytes read past the end; any over means the input was cut short.

Br

@s:String -> @buf:U32 -> @cnt:U32 -> @over:U32 -> Br

type Ht source · line 90 · raw

Data

Huffman codes as a trie: one step per bit. A read bit picks o (1) or z (0). Bad: two codes collided, so the code set was over-subscribed.

HtNone
```
Ht
```
HtBad
```
Ht
```
HtLeaf
```
@sym:U32 -> Ht
```
HtNode
```
@z:Ht -> @o:Ht -> Ht
```

type Ow source · line 293 · raw

Data

Output: the 32 KiB window (indexes wrap), the write position, the byte count, and the bytes, reversed.

Ow
```
@w:U32 -> @n:U32 -> @racc:String -> Ow
```

type Mo source · line 300 · raw

Data

MoHead
```
Mo
```
MoCodes
```
@lit:Ht -> @dist:Ht -> Mo
```
MoDone
```
Mo
```
MoBad
```
Mo
```

type Is source · line 306 · raw

Data

Is

@br:Br -> @o:Ow -> @mode:Mo -> @last:Bool -> Is

type Cd source · line 389 · raw

Data

Lengths so far (reversed), how many, the last one (for code 16), and whether it went wrong.

Cd

@br:Br -> @acc:List<&2, U32> -> @n:U32 -> @prev:U32 -> @bad:Bool -> Cd

type Inflated source · line 620 · raw

Data

out: the bytes; rest: the input after the stream; n: len(out) mod 2^32.

Inflated

@out:String -> @rest:String -> @n:U32 -> Inflated

Definitions

def byte source · line 6 · raw

@h:Char -> U32

def bits source · line 10 · raw

@+n:U32 -> Nat

def mask source · line 13 · raw

@+n:U32 -> U32

def br.new source · line 20 · raw

@s:String -> Br

def br.pull source · line 23 · raw

@b:Br -> Br

def br.pull.if source · line 31 · raw

@b:Br -> @short:Bool -> Br

def br.short source · line 38 · raw

@+b:Br -> @+n:U32 -> Bool

def br.fill source · line 43 · raw

@fuel:Nat -> @+b:Br -> @+n:U32 -> Br

n is at most 16, so three bytes always fill the buffer.

def br.cut source · line 50 · raw

@b:Br -> @+n:U32 -> Pair(Br, U32)

def br.take source · line 54 · raw

@b:Br -> @+n:U32 -> Pair(Br, U32)

def br.drop.of source · line 57 · raw

@r:Pair(Br, U32) -> Br

def br.drop source · line 61 · raw

@b:Br -> @+n:U32 -> Br

def br.align source · line 65 · raw

@+b:Br -> Br

RFC 1951 §3.2.4: a stored block starts on a byte boundary.

def br.ok source · line 69 · raw

@+b:Br -> Bool

def br.bytes source · line 73 · raw

@k:Nat -> @+buf:U32 -> String

def br.rest.of source · line 80 · raw

@b:Br -> String

def br.rest source · line 85 · raw

@+b:Br -> String

Whole bytes still in the buffer go back in front of the unread input.

def ht.left source · line 96 · raw

@t:Ht -> Ht

def ht.right source · line 107 · raw

@t:Ht -> Ht

def ht.leaf source · line 118 · raw

@t:Ht -> @+sym:U32 -> Ht

def ht.ins source · line 129 · raw

@path:List<&2, Bool> -> @+t:Ht -> @+sym:U32 -> Ht

def ht.path source · line 141 · raw

@n:Nat -> @+code:U32 -> @acc:List<&2, Bool> -> List<&2, Bool>

The code's bits, most significant first: the order the stream sends them.

def cnt.add source · line 149 · raw

@ar:Pair(Array<U32>, U32) -> @+len:U32 -> Array<U32>

Canonical codes (RFC 1951 §3.2.2): count lengths, find each length's first code, then assign in symbol order.

def cnt.go source · line 153 · raw

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

def nx.set source · line 160 · raw

@+i:U32 -> @cv:Pair(Array<U32>, U32) -> @n:Array<U32> -> @+code:U32 -> Pair(Array<U32>, Pair(Array<U32>, U32))

def nx.step source · line 165 · raw

@+i:U32 -> @st:Pair(Array<U32>, Pair(Array<U32>, U32)) -> Pair(Array<U32>, Pair(Array<U32>, U32))

def nx.go source · line 169 · raw

@k:Nat -> @+i:U32 -> @st:Pair(Array<U32>, Pair(Array<U32>, U32)) -> Pair(Array<U32>, Pair(Array<U32>, U32))

def as.put source · line 176 · raw

@+l:U32 -> @+sym:U32 -> @nv:Pair(Array<U32>, U32) -> @t:Ht -> Pair(Array<U32>, Ht)

def as.one.nz source · line 180 · raw

@+l:U32 -> @+sym:U32 -> @n:Array<U32> -> @t:Ht -> @zero:Bool -> Pair(Array<U32>, Ht)

def as.one source · line 187 · raw

@+l:U32 -> @+sym:U32 -> @st:Pair(Array<U32>, Ht) -> Pair(Array<U32>, Ht)

def as.go source · line 191 · raw

@xs:List<&2, U32> -> @+sym:U32 -> @st:Pair(Array<U32>, Ht) -> Pair(Array<U32>, Ht)

def ht.of source · line 198 · raw

@st:Pair(Array<U32>, Ht) -> Ht

def ht.assign source · line 202 · raw

@xs:List<&2, U32> -> @st:Pair(Array<U32>, Pair(Array<U32>, U32)) -> Ht

def ht.build source · line 207 · raw

@+lens:List<&2, U32> -> Ht

lens[i] is the code length of symbol i; 0 means the symbol is unused.

def ht.step source · line 211 · raw

@z:Ht -> @o:Ht -> @bv:Pair(Br, U32) -> Pair(Ht, Br)

No code: 9999, never a symbol.

def ht.dec source · line 216 · raw

@fuel:Nat -> @st:Pair(Ht, Br) -> Pair(Br, U32)

A code is at most 15 bits (§3.2.7), so 16 steps always reach a leaf or a miss.

def ht.decode source · line 233 · raw

@t:Ht -> @b:Br -> Pair(Br, U32)

def nth source · line 236 · raw

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

def rep source · line 243 · raw

@k:Nat -> @+v:U32 -> @acc:List<&2, U32> -> List<&2, U32>

def take.n source · line 250 · raw

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

def drop.n source · line 261 · raw

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

def len.base source · line 273 · raw

List<&2, U32>

RFC 1951 §3.2.5

def len.extra source · line 276 · raw

List<&2, U32>

def dist.base source · line 279 · raw

List<&2, U32>

def dist.extra source · line 282 · raw

List<&2, U32>

def fixed.lit source · line 286 · raw

Ht

RFC 1951 §3.2.6

def fixed.dist source · line 289 · raw

Ht

def out.put source · line 296 · raw

@win:Array<U32> -> @+c:U32 -> @o:Ow -> Pair(Array<U32>, Ow)

def inf.next source · line 309 · raw

@last:Bool -> Mo

def inf.bad source · line 316 · raw

@win:Array<U32> -> @b:Br -> @o:Ow -> Pair(Array<U32>, Is)

def sb.put2 source · line 320 · raw

@p:Pair(Array<U32>, Ow) -> @b:Br -> Pair(Array<U32>, Pair(Br, Ow))

Stored block (§3.2.4): LEN, then NLEN (its complement), then LEN raw bytes.

def sb.put source · line 324 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @o:Ow -> Pair(Array<U32>, Pair(Br, Ow))

def sb.byte source · line 328 · raw

@st:Pair(Array<U32>, Pair(Br, Ow)) -> Pair(Array<U32>, Pair(Br, Ow))

def sb.go source · line 332 · raw

@k:Nat -> @st:Pair(Array<U32>, Pair(Br, Ow)) -> Pair(Array<U32>, Pair(Br, Ow))

def sb.done source · line 339 · raw

@t:Pair(Array<U32>, Pair(Br, Ow)) -> @+last:Bool -> Pair(Array<U32>, Is)

def sb.ok source · line 343 · raw

@win:Array<U32> -> @b:Br -> @+len:U32 -> @o:Ow -> @+last:Bool -> @ok:Bool -> Pair(Array<U32>, Is)

def sb.nlen source · line 350 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @+len:U32 -> @o:Ow -> @+last:Bool -> Pair(Array<U32>, Is)

def sb.len source · line 354 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @o:Ow -> @+last:Bool -> Pair(Array<U32>, Is)

def inf.stored source · line 358 · raw

@win:Array<U32> -> @b:Br -> @o:Ow -> @+last:Bool -> Pair(Array<U32>, Is)

def cl.slot source · line 363 · raw

List<&2, U32>

Dynamic block (§3.2.7): code lengths for the code-length code, then the lengths themselves. cl.slot[i]: where symbol i's length sits in the order the stream sends them.

def cl.place source · line 366 · raw

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

def cl.push source · line 373 · raw

@bv:Pair(Br, U32) -> @acc:List<&2, U32> -> Pair(Br, List<&2, U32>)

def cl.one source · line 377 · raw

@st:Pair(Br, List<&2, U32>) -> Pair(Br, List<&2, U32>)

def cl.read source · line 381 · raw

@k:Nat -> @st:Pair(Br, List<&2, U32>) -> Pair(Br, List<&2, U32>)

def cd.fill source · line 392 · raw

@+b:Br -> @+acc:List<&2, U32> -> @+n:U32 -> @+v:U32 -> @+cnt:U32 -> @+total:U32 -> Cd

def cd.rep source · line 395 · raw

@bv:Pair(Br, U32) -> @+v:U32 -> @+base:U32 -> @acc:List<&2, U32> -> @+n:U32 -> @+total:U32 -> Cd

def cd.prev source · line 399 · raw

@b:Br -> @acc:List<&2, U32> -> @+n:U32 -> @+prev:U32 -> @+total:U32 -> @ok:Bool -> Cd

def cd.z18 source · line 406 · raw

@b:Br -> @acc:List<&2, U32> -> @+n:U32 -> @+total:U32 -> @ok:Bool -> Cd

def cd.z17 source · line 413 · raw

@b:Br -> @acc:List<&2, U32> -> @+n:U32 -> @+s:U32 -> @+total:U32 -> @ok:Bool -> Cd

def cd.c16 source · line 420 · raw

@b:Br -> @acc:List<&2, U32> -> @+n:U32 -> @+prev:U32 -> @+s:U32 -> @+total:U32 -> @ok:Bool -> Cd

def cd.lit source · line 427 · raw

@b:Br -> @acc:List<&2, U32> -> @+n:U32 -> @+prev:U32 -> @+s:U32 -> @+total:U32 -> @ok:Bool -> Cd

def cd.sym source · line 434 · raw

@bv:Pair(Br, U32) -> @acc:List<&2, U32> -> @+n:U32 -> @+prev:U32 -> @+total:U32 -> Cd

def cd.step.go source · line 438 · raw

@+cl:Ht -> @+total:U32 -> @stop:Bool -> @cs:Cd -> Cd

def cd.stop source · line 447 · raw

@+st:Cd -> @+total:U32 -> Bool

def cd.go source · line 452 · raw

@k:Nat -> @+cl:Ht -> @+total:U32 -> @+st:Cd -> Cd

Each step adds at least one length, so total steps suffice.

def dyn.tables source · line 459 · raw

@b:Br -> @+lens:List<&2, U32> -> @+hlit:U32 -> @bad:Bool -> Pair(Br, Mo)

def dyn.done source · line 466 · raw

@st:Cd -> @+hlit:U32 -> @+total:U32 -> Pair(Br, Mo)

def dyn.lens source · line 470 · raw

@st:Pair(Br, List<&2, U32>) -> @+hlit:U32 -> @+hdist:U32 -> Pair(Br, Mo)

def dyn.clen source · line 476 · raw

@bv:Pair(Br, U32) -> @+hlit:U32 -> @+hdist:U32 -> Pair(Br, Mo)

def dyn.hdist source · line 480 · raw

@bv:Pair(Br, U32) -> @+hlit:U32 -> Pair(Br, Mo)

def dyn.hlit source · line 484 · raw

@bv:Pair(Br, U32) -> Pair(Br, Mo)

def dyn.read source · line 488 · raw

@b:Br -> Pair(Br, Mo)

def cp.put source · line 492 · raw

@av:Pair(Array<U32>, U32) -> @o:Ow -> Pair(Array<U32>, Ow)

A match copies len bytes from d back; the window's indexes wrap, so w - d needs no mask.

def cp.one source · line 496 · raw

@+d:U32 -> @st:Pair(Array<U32>, Ow) -> Pair(Array<U32>, Ow)

def cp.go source · line 501 · raw

@k:Nat -> @+d:U32 -> @st:Pair(Array<U32>, Ow) -> Pair(Array<U32>, Ow)

def inf.codes source · line 508 · raw

@p:Pair(Array<U32>, Ow) -> @b:Br -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> Pair(Array<U32>, Is)

def ow.n source · line 512 · raw

@+o:Ow -> U32

def inf.far source · line 517 · raw

@win:Array<U32> -> @b:Br -> @+o:Ow -> @+len:U32 -> @+d:U32 -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> @ok:Bool -> Pair(Array<U32>, Is)

RFC 1951 §3.2.5: a distance may not reach before the first byte out.

def inf.dx source · line 524 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @+db:U32 -> @+len:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> Pair(Array<U32>, Is)

def inf.ds source · line 529 · raw

@win:Array<U32> -> @b:Br -> @+ds:U32 -> @+len:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> @ok:Bool -> Pair(Array<U32>, Is)

def inf.d source · line 536 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @+len:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> Pair(Array<U32>, Is)

def inf.lx source · line 540 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @+lb:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> Pair(Array<U32>, Is)

def inf.ls source · line 544 · raw

@win:Array<U32> -> @b:Br -> @+s:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> @ok:Bool -> Pair(Array<U32>, Is)

def inf.end source · line 552 · raw

@win:Array<U32> -> @b:Br -> @+s:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> @eob:Bool -> Pair(Array<U32>, Is)

def inf.lit source · line 559 · raw

@win:Array<U32> -> @b:Br -> @+s:U32 -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> @ok:Bool -> Pair(Array<U32>, Is)

def inf.sym source · line 566 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @+o:Ow -> @+lit:Ht -> @+dist:Ht -> @+last:Bool -> Pair(Array<U32>, Is)

def inf.dyn source · line 570 · raw

@win:Array<U32> -> @bm:Pair(Br, Mo) -> @o:Ow -> @+last:Bool -> Pair(Array<U32>, Is)

def inf.t2 source · line 574 · raw

@win:Array<U32> -> @b:Br -> @o:Ow -> @+last:Bool -> @is2:Bool -> Pair(Array<U32>, Is)

def inf.t1 source · line 581 · raw

@win:Array<U32> -> @b:Br -> @o:Ow -> @+last:Bool -> @+t:U32 -> @is1:Bool -> Pair(Array<U32>, Is)

def inf.t0 source · line 588 · raw

@win:Array<U32> -> @b:Br -> @o:Ow -> @+last:Bool -> @+t:U32 -> @is0:Bool -> Pair(Array<U32>, Is)

def inf.head source · line 596 · raw

@win:Array<U32> -> @bv:Pair(Br, U32) -> @o:Ow -> Pair(Array<U32>, Is)

§3.2.3: BFINAL, then BTYPE.

def inf.go source · line 602 · raw

@k:Nat -> @st:Pair(Array<U32>, Is) -> Pair(Array<U32>, Is)

Every step reads at least one bit, so 8 steps per input byte always finish a valid stream.

def inf.fin source · line 623 · raw

@ok:Bool -> @b:Br -> @o:Ow -> Maybe<&2, Inflated>

def inf.result source · line 631 · raw

@st:Pair(Array<U32>, Is) -> Maybe<&2, Inflated>

def inflate.rest source · line 644 · raw

@+s:String -> Maybe<&2, Inflated>

def inflate.out source · line 647 · raw

@m:Maybe<&2, Inflated> -> Maybe<&2, String>

def inflate source · line 655 · raw

@+s:String -> Maybe<&2, String>

Raw DEFLATE. None: malformed or cut short.

def crc.bit source · line 659 · raw

@+c:U32 -> U32

CRC-32 (RFC 1952 §8), reflected, polynomial 0xEDB88320.

def crc.bits source · line 662 · raw

@k:Nat -> @+c:U32 -> U32

def crc.fill source · line 669 · raw

@k:Nat -> @+i:U32 -> @a:Array<U32> -> Array<U32>

def crc.table source · line 676 · raw

Array<U32>

def crc.mix source · line 679 · raw

@av:Pair(Array<U32>, U32) -> @+c:U32 -> Pair(Array<U32>, U32)

def crc.step source · line 683 · raw

@st:Pair(Array<U32>, U32) -> @+b:U32 -> Pair(Array<U32>, U32)

def crc.go source · line 687 · raw

@s:String -> @st:Pair(Array<U32>, U32) -> Pair(Array<U32>, U32)

def crc.of source · line 694 · raw

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

def crc32 source · line 698 · raw

@s:String -> U32

def adler.go source · line 702 · raw

@s:String -> @+a:U32 -> @+b:U32 -> U32

Adler-32 (RFC 1950 §9).

def adler32 source · line 710 · raw

@s:String -> U32

def le32 source · line 714 · raw

@s:String -> Maybe<&2, U32>

Little- and big-endian 32-bit words at the front of s.

def be32 source · line 723 · raw

@s:String -> Maybe<&2, U32>

def flag source · line 732 · raw

@+f:U32 -> @+bit:U32 -> Bool

def check source · line 735 · raw

@ok:Bool -> @+out:String -> Maybe<&2, String>

def gz.zstr source · line 744 · raw

@s:String -> @hit:Bool -> Maybe<&2, String>

RFC 1952 §2.3: after the fixed 10 bytes, optional FEXTRA, FNAME, FCOMMENT, FHCRC. hit: the byte just read was the terminating zero.

def gz.skip source · line 759 · raw

@k:Nat -> @s:String -> Maybe<&2, String>

def gz.extra.len source · line 770 · raw

@s:String -> Maybe<&2, String>

def gz.fextra source · line 779 · raw

@on:Bool -> @+s:String -> Maybe<&2, String>

def gz.fstr source · line 786 · raw

@on:Bool -> @+s:String -> Maybe<&2, String>

def gz.fhcrc source · line 793 · raw

@on:Bool -> @+s:String -> Maybe<&2, String>

def gz.flags source · line 800 · raw

@+f:U32 -> @s:String -> Maybe<&2, String>

def gz.head source · line 807 · raw

@s:String -> Maybe<&2, String>

def gz.trail2 source · line 816 · raw

@+out:String -> @+n:U32 -> @crc:Maybe<&2, U32> -> @size:Maybe<&2, U32> -> Maybe<&2, String>

def gz.trail source · line 822 · raw

@m:Maybe<&2, Inflated> -> Maybe<&2, String>

def gz.body source · line 829 · raw

@m:Maybe<&2, String> -> Maybe<&2, String>

def gunzip source · line 838 · raw

@s:String -> Maybe<&2, String>

One gzip member; the CRC-32 and ISIZE must match. None: malformed, cut short, or corrupt. ponytail: bytes after the first member are ignored; loop over members if a server concatenates them.

def zl.sum source · line 842 · raw

@+out:String -> @a:Maybe<&2, U32> -> Maybe<&2, String>

RFC 1950: CMF and FLG, then DEFLATE, then Adler-32, big-endian.

def zl.trail source · line 849 · raw

@m:Maybe<&2, Inflated> -> Maybe<&2, String>

def zl.ok source · line 856 · raw

@+cmf:U32 -> @+flg:U32 -> Bool

def unzlib source · line 859 · raw

@s:String -> Maybe<&2, String>