1 # PNG decoder: chunks, filters, interlacing, palettes and bit depths. 2 import Base 3 import gralha-text-scan@0.1.0.0/scan.bend as U 4 import gralha-bytes@0.1.0.0/bytes.bend as Bin 5 import gralha-image@0.1.0.0/image.bend as Img 6 7 type PNGInfo is Data: 8 PNGInfo{width: U32, height: U32, depth: U32, kind: U32, interlace: U32, palette: Bin.Bytes, alpha: Bin.Bytes, compressed: Bin.Bytes, valid: Bool} 9 10 def png.empty() -> PNGInfo: 11 PNGInfo{0, 0, 0, 0, 0, Bin.bytes.empty(), Bin.bytes.empty(), Bin.bytes.empty(), False{}} 12 13 def png.invalid(info: PNGInfo) -> PNGInfo: 14 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 15 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, False{}} 16 17 def png.header(+src: Bin.Bytes, +at: U32) -> PNGInfo: 18 PNGInfo{Bin.bytes.be(src, at, 4n, 0), Bin.bytes.be(src, (at + 4 : U32), 4n, 0), Bin.bytes.get(src, (at + 8 : U32)), Bin.bytes.get(src, (at + 9 : U32)), Bin.bytes.get(src, (at + 12 : U32)), Bin.bytes.empty(), Bin.bytes.empty(), Bin.bytes.empty(), U32.is_eq(Bin.bytes.get(src, (at + 10 : U32)), 0) && U32.is_eq(Bin.bytes.get(src, (at + 11 : U32)), 0)} 19 20 def png.chunk(info: PNGInfo, +name: U32, +src: Bin.Bytes, +at: U32, +count: U32) -> PNGInfo: 21 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 22 +pal = palette 23 +trans = alpha 24 +data = compressed 25 PNGInfo{w, h, depth, kind, interlace, 26 U.branch(Bin.Bytes, U32.is_eq(name, 1347179589), _ => Bin.bytes.slice(U32.to_nat(count), src, at, Bin.bytes.empty()), _ => pal), 27 U.branch(Bin.Bytes, U32.is_eq(name, 1951551059), _ => Bin.bytes.slice(U32.to_nat(count), src, at, Bin.bytes.empty()), _ => trans), 28 U.branch(Bin.Bytes, U32.is_eq(name, 1229209940), _ => Bin.bytes.slice(U32.to_nat(count), src, at, data), _ => data), 29 valid && Bool.not(U32.is_eq(name, 1229472850)) && (U32.is_eq(name, 1347179589) || U32.is_eq(name, 1229209940) || U32.is_eq(U32.and(U32.shrn(name, 24n), 32), 32))} 30 31 @unsafe 32 def png.chunks(+src: Bin.Bytes, +at: U32, +info: PNGInfo, +table: Bin.Bytes) -> PNGInfo: 33 +size = Bin.bytes.size(src) 34 +count = Bin.bytes.be(src, at, 4n, 0) 35 +name = Bin.bytes.be(src, (at + 4 : U32), 4n, 0) 36 +next = (at + count + 12 : U32) 37 U.branch(PNGInfo, U32.is_le(at, size) && U32.is_ge((size - at : U32), 12) && U32.is_le(count, (size - at - 12 : U32)), 38 _ => U.branch(PNGInfo, U32.is_eq(Bin.checksum.crc.loop(U32.to_nat((count + 4 : U32)), src, (at + 4 : U32), table, 4294967295), Bin.bytes.be(src, (at + count + 8 : U32), 4n, 0)), 39 _ => U.branch(PNGInfo, U32.is_eq(name, 1229278788), _ => U.choose(PNGInfo, U32.is_eq(count, 0) && U32.is_eq(next, size), info, png.invalid(info)), 40 _ => png.chunks(src, next, png.chunk(info, name, src, (at + 8 : U32), count), table)), _ => png.invalid(info)), _ => png.invalid(info)) 41 42 def png.info(+src: Bin.Bytes) -> PNGInfo: 43 +table = Bin.checksum.crc.table(256n, 0, Bin.bytes.empty()) 44 U.branch(PNGInfo, U32.is_ge(Bin.bytes.size(src), 33) && U32.is_eq(Bin.bytes.be(src, 0, 4n, 0), 2303741511) && U32.is_eq(Bin.bytes.be(src, 4, 4n, 0), 218765834) && U32.is_eq(Bin.bytes.be(src, 8, 4n, 0), 13) && U32.is_eq(Bin.bytes.be(src, 12, 4n, 0), 1229472850) && U32.is_eq(Bin.checksum.crc.loop(17n, src, 12, table, 4294967295), Bin.bytes.be(src, 29, 4n, 0)), 45 _ => png.chunks(src, 33, png.header(src, 16), table), _ => png.empty()) 46 47 def png.channels(+kind: U32) -> U32: 48 U.choose(U32, U32.is_eq(kind, 2), 3, U.choose(U32, U32.is_eq(kind, 4), 2, U.choose(U32, U32.is_eq(kind, 6), 4, 1))) 49 50 def png.depth.valid(+kind: U32, +depth: U32) -> Bool: 51 +small = U32.is_eq(depth, 1) || U32.is_eq(depth, 2) || U32.is_eq(depth, 4) || U32.is_eq(depth, 8) 52 U.choose(Bool, U32.is_eq(kind, 0), small || U32.is_eq(depth, 16), U.choose(Bool, U32.is_eq(kind, 3), small, (U32.is_eq(kind, 2) || U32.is_eq(kind, 4) || U32.is_eq(kind, 6)) && (U32.is_eq(depth, 8) || U32.is_eq(depth, 16)))) 53 54 def png.valid(+info: PNGInfo) -> Bool: 55 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 56 valid && U32.is_gt(w, 0) && U32.is_gt(h, 0) && U32.is_le(w, 2048) && U32.is_le(h, 2048) && png.depth.valid(kind, depth) && U32.is_le(interlace, 1) && (Bool.not(U32.is_eq(kind, 3)) || (U32.is_gt(Bin.bytes.size(palette), 0) && U32.is_eq(U32.mod(Bin.bytes.size(palette), 3), 0) && U32.is_le(Bin.bytes.size(palette), 768))) 57 58 def png.paeth(+a: U32, +b: U32, +c: U32) -> U32: 59 +aa = U32.to_f32(a) 60 +bb = U32.to_f32(b) 61 +cc = U32.to_f32(c) 62 +pa = F32.abs((bb - cc : F32)) 63 +pb = F32.abs((aa - cc : F32)) 64 +pc = F32.abs((aa + bb - 2.0 * cc : F32)) 65 U.choose(U32, F32.is_le(pa, pb) && F32.is_le(pa, pc), a, U.choose(U32, F32.is_le(pb, pc), b, c)) 66 67 def png.predict(+kind: U32, +a: U32, +b: U32, +c: U32) -> U32: 68 U.choose(U32, U32.is_eq(kind, 1), a, U.choose(U32, U32.is_eq(kind, 2), b, U.choose(U32, U32.is_eq(kind, 3), ((a + b) / 2 : U32), U.choose(U32, U32.is_eq(kind, 4), png.paeth(a, b, c), 0)))) 69 70 def png.unfilter.row(n: Nat, +raw: Bin.Bytes, +at: U32, +x: U32, +stride: U32, +bpp: U32, +kind: U32, +out: Bin.Bytes) -> Bin.Bytes: 71 match n: 72 case 0n: out 73 case 1n+d: 74 +pos = Bin.bytes.size(out) 75 +a = U.choose(U32, U32.is_ge(x, bpp), Bin.bytes.get(out, (pos - bpp : U32)), 0) 76 +b = U.choose(U32, U32.is_ge(pos, stride), Bin.bytes.get(out, (pos - stride : U32)), 0) 77 +c = U.choose(U32, U32.is_ge(x, bpp) && U32.is_ge(pos, stride), Bin.bytes.get(out, (pos - stride - bpp : U32)), 0) 78 png.unfilter.row(d, raw, U32.inc(at), U32.inc(x), stride, bpp, kind, Bin.bytes.push(out, ((Bin.bytes.get(raw, at) + png.predict(kind, a, b, c)) % 256 : U32))) 79 80 def png.unfilter(n: Nat, +raw: Bin.Bytes, +at: U32, +stride: U32, +bpp: U32, +out: Bin.Bytes) -> Maybe<&2, Bin.Bytes>: 81 match n: 82 case 0n: Some{out} 83 case 1n+d: 84 +kind = Bin.bytes.get(raw, at) 85 U.branch(Maybe<&2, Bin.Bytes>, U32.is_le(kind, 4), _ => png.unfilter(d, raw, (at + stride + 1 : U32), stride, bpp, png.unfilter.row(U32.to_nat(stride), raw, U32.inc(at), 0, stride, bpp, kind, out)), _ => None{}) 86 87 def png.sample(+raw: Bin.Bytes, +row: U32, +index: U32, +depth: U32) -> U32: 88 +bit = (index * depth : U32) 89 +at = (row + bit / 8 : U32) 90 U.branch(U32, U32.is_eq(depth, 16), _ => Bin.bytes.be(raw, at, 2n, 0), _ => U32.and(U32.shrn(Bin.bytes.get(raw, at), U32.to_nat((8 - depth - bit % 8 : U32))), (U32.shln(1, U32.to_nat(depth)) - 1 : U32))) 91 92 def png.palette(+palette: Bin.Bytes, +alpha: Bin.Bytes, +index: U32) -> Img.Color: 93 +at = (index * 3 : U32) 94 U.branch(Img.Color, U32.is_lt((at + 2 : U32), Bin.bytes.size(palette)), 95 _ => Img.rgba((U32.to_f32(Bin.bytes.get(palette, at)) / 255.0 : F32), (U32.to_f32(Bin.bytes.get(palette, U32.inc(at))) / 255.0 : F32), (U32.to_f32(Bin.bytes.get(palette, (at + 2 : U32))) / 255.0 : F32), (U32.to_f32(U.choose(U32, U32.is_lt(index, Bin.bytes.size(alpha)), Bin.bytes.get(alpha, index), 255)) / 255.0 : F32)), _ => Img.clear()) 96 97 def png.pixel(info: PNGInfo, +raw: Bin.Bytes, stride: U32, x: U32, y: U32) -> Img.Color: 98 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 99 +bits = depth 100 +mode = kind 101 +trans = alpha 102 +row = (y * stride : U32) 103 +index = (x * png.channels(mode) : U32) 104 +top = U32.to_f32((U32.shln(1, U32.to_nat(bits)) - 1 : U32)) 105 +r = png.sample(raw, row, index, bits) 106 +g = png.sample(raw, row, U32.inc(index), bits) 107 +b = png.sample(raw, row, (index + 2 : U32), bits) 108 +a = png.sample(raw, row, (index + 3 : U32), bits) 109 +gray = U32.is_eq(mode, 0) || U32.is_eq(mode, 4) 110 +transparent = U.choose(Bool, gray, U32.is_eq(Bin.bytes.size(trans), 2) && U32.is_eq(r, Bin.bytes.be(trans, 0, 2n, 0)), U32.is_eq(Bin.bytes.size(trans), 6) && U32.is_eq(r, Bin.bytes.be(trans, 0, 2n, 0)) && U32.is_eq(g, Bin.bytes.be(trans, 2, 2n, 0)) && U32.is_eq(b, Bin.bytes.be(trans, 4, 2n, 0))) 111 U.branch(Img.Color, U32.is_eq(mode, 3), _ => png.palette(palette, trans, r), 112 _ => Img.rgba((U32.to_f32(r) / top : F32), (U32.to_f32(U.choose(U32, gray, r, g)) / top : F32), (U32.to_f32(U.choose(U32, gray, r, b)) / top : F32), 113 U.choose(F32, U32.is_eq(mode, 4), (U32.to_f32(g) / top : F32), U.choose(F32, U32.is_eq(mode, 6), (U32.to_f32(a) / top : F32), U.choose(F32, transparent, 0.0, 1.0))))) 114 115 type PNGPass is Data: 116 PNGPass{width: U32, height: U32, x: U32, y: U32, dx: U32, dy: U32, stride: U32, offset: U32} 117 118 def png.pass.size(+full: U32, +start: U32, +step: U32) -> U32: 119 U.choose(U32, U32.is_le(full, start), 0, ((full - start + step - 1) / step : U32)) 120 121 def png.pass(+w: U32, +h: U32, bits: U32, channels: U32, +index: U32, +interlaced: Bool, offset: U32) -> PNGPass: 122 +x = U.choose(U32, interlaced, U.uints.nth(Con{0, Con{4, Con{0, Con{2, Con{0, Con{1, Con{0, Nil{}}}}}}}}, U32.to_nat(index), 0), 0) 123 +y = U.choose(U32, interlaced, U.uints.nth(Con{0, Con{0, Con{4, Con{0, Con{2, Con{0, Con{1, Nil{}}}}}}}}, U32.to_nat(index), 0), 0) 124 +dx = U.choose(U32, interlaced, U.uints.nth(Con{8, Con{8, Con{4, Con{4, Con{2, Con{2, Con{1, Nil{}}}}}}}}, U32.to_nat(index), 1), 1) 125 +dy = U.choose(U32, interlaced, U.uints.nth(Con{8, Con{8, Con{8, Con{4, Con{4, Con{2, Con{2, Nil{}}}}}}}}, U32.to_nat(index), 1), 1) 126 +width = png.pass.size(w, x, dx) 127 PNGPass{width, png.pass.size(h, y, dy), x, y, dx, dy, ((width * channels * bits + 7) / 8 : U32), offset} 128 129 def png.pass.bytes(+pass: PNGPass) -> U32: 130 PNGPass{w, h, x, y, dx, dy, stride, offset} = pass 131 U.choose(U32, U32.is_eq(w, 0), 0, ((stride + 1) * h : U32)) 132 133 def png.passes(n: Nat, +info: PNGInfo, +index: U32, +offset: U32) -> List<&2, PNGPass>: 134 match n: 135 case 0n: Nil{} 136 case 1n+d: 137 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 138 +pass = png.pass(w, h, depth, png.channels(kind), index, U32.is_eq(interlace, 1), offset) 139 Con{pass, png.passes(d, info, U32.inc(index), (offset + png.pass.bytes(pass) : U32))} 140 141 def png.passes.bytes(xs: List<&2, PNGPass>, total: U32) -> U32: 142 match xs: 143 case Nil{}: total 144 case Con{h, t}: png.passes.bytes(t, (total + png.pass.bytes(h) : U32)) 145 146 def png.paint.row(n: Nat, +index: U32, +row: U32, +info: PNGInfo, +raw: Bin.Bytes, +pass: PNGPass, +depth: Nat, pixels: Img.Pixels) -> Img.Pixels: 147 match n: 148 case 0n: pixels 149 case 1n+d: 150 PNGPass{w, h, x, y, dx, dy, stride, offset} = pass 151 png.paint.row(d, U32.inc(index), row, info, raw, pass, depth, Img.pixels.set(pixels, depth, (x + index * dx : U32), (y + row * dy : U32), png.pixel(info, raw, stride, index, row))) 152 153 def png.paint.rows(n: Nat, +row: U32, +info: PNGInfo, +raw: Bin.Bytes, +pass: PNGPass, +depth: Nat, pixels: Img.Pixels) -> Img.Pixels: 154 match n: 155 case 0n: pixels 156 case 1n+d: 157 PNGPass{w, h, x, y, dx, dy, stride, offset} = pass 158 png.paint.rows(d, U32.inc(row), info, raw, pass, depth, png.paint.row(U32.to_nat(w), 0, row, info, raw, pass, depth, pixels)) 159 160 def png.paint(result: Maybe<&2, Bin.Bytes>, info: PNGInfo, +pass: PNGPass, depth: Nat, pixels: Img.Pixels, next: Img.Pixels -> Maybe<&2, Img.Pixels>) -> Maybe<&2, Img.Pixels>: 161 match result: 162 case None{}: None{} 163 case Some{raw}: 164 PNGPass{w, h, x, y, dx, dy, stride, offset} = pass 165 next(png.paint.rows(U32.to_nat(h), 0, info, raw, pass, depth, pixels)) 166 167 @unsafe 168 def png.decode.passes(+xs: List<&2, PNGPass>, +info: PNGInfo, +raw: Bin.Bytes, +bpp: U32, +depth: Nat, +pixels: Img.Pixels) -> Maybe<&2, Img.Pixels>: 169 match xs: 170 case Nil{}: Some{pixels} 171 case Con{PNGPass{w, h, x, y, dx, dy, stride, offset}, rest}: 172 +pass = {PNGPass{w, h, x, y, dx, dy, stride, offset} : PNGPass} 173 U.branch(Maybe<&2, Img.Pixels>, U32.is_eq(w, 0) || U32.is_eq(h, 0), _ => png.decode.passes(rest, info, raw, bpp, depth, pixels), 174 _ => png.paint(png.unfilter(U32.to_nat(h), raw, offset, stride, bpp, Bin.bytes.empty()), info, pass, depth, pixels, image => png.decode.passes(rest, info, raw, bpp, depth, image))) 175 176 def png.raster(result: Maybe<&2, Img.Pixels>, w: U32, h: U32, depth: Nat) -> Img.Picture: 177 match result: 178 case None{}: Img.Picture{0, 0, 0n, Img.Flat{Img.clear()}} 179 case Some{pixels}: Img.Picture{w, h, depth, pixels} 180 181 def png.inflate(result: Maybe<&2, Bin.Bytes>, +info: PNGInfo, passes: List<&2, PNGPass>) -> Img.Picture: 182 match result: 183 case None{}: Img.Picture{0, 0, 0n, Img.Flat{Img.clear()}} 184 case Some{raw}: 185 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 186 +dd = Img.picture.depth(U.choose(U32, U32.is_gt(w, h), w, h), 1, 0n) 187 png.raster(png.decode.passes(passes, info, raw, U.choose(U32, U32.is_lt(depth, 8), 1, (png.channels(kind) * depth / 8 : U32)), dd, Img.Flat{Img.clear()}), w, h, dd) 188 189 def png.decode.info(+info: PNGInfo) -> Img.Picture: 190 PNGInfo{w, h, depth, kind, interlace, palette, alpha, compressed, valid} = info 191 +passes = png.passes(U.choose(Nat, U32.is_eq(interlace, 1), 7n, 1n), info, 0, 0) 192 U.branch(Img.Picture, png.valid(info), _ => png.inflate(Bin.zlib(compressed, png.passes.bytes(passes, 0)), info, passes), _ => Img.Picture{0, 0, 0n, Img.Flat{Img.clear()}}) 193 194 def png.decode(src: Bin.Bytes) -> Img.Picture: 195 png.decode.info(png.info(src))