diff --git a/qoi/images/Bridalveil_Fall_and_valley.png b/qoi/images/Bridalveil_Fall_and_valley.png
new file mode 100644
index 00000000..aae40b48
Binary files /dev/null and b/qoi/images/Bridalveil_Fall_and_valley.png differ
diff --git a/qoi/images/Bridalveil_Fall_and_valley.qoi b/qoi/images/Bridalveil_Fall_and_valley.qoi
new file mode 100644
index 00000000..04a21585
Binary files /dev/null and b/qoi/images/Bridalveil_Fall_and_valley.qoi differ
diff --git a/qoi/images/Chiffchaff_Phylloscopus_collybita.png b/qoi/images/Chiffchaff_Phylloscopus_collybita.png
new file mode 100644
index 00000000..69613f2e
Binary files /dev/null and b/qoi/images/Chiffchaff_Phylloscopus_collybita.png differ
diff --git a/qoi/images/Chiffchaff_Phylloscopus_collybita.qoi b/qoi/images/Chiffchaff_Phylloscopus_collybita.qoi
new file mode 100644
index 00000000..49df2b74
Binary files /dev/null and b/qoi/images/Chiffchaff_Phylloscopus_collybita.qoi differ
diff --git a/qoi/images/Linze_Zhangye_Gansu_China_panoramio_4.png b/qoi/images/Linze_Zhangye_Gansu_China_panoramio_4.png
new file mode 100644
index 00000000..30dba87e
Binary files /dev/null and b/qoi/images/Linze_Zhangye_Gansu_China_panoramio_4.png differ
diff --git a/qoi/images/Linze_Zhangye_Gansu_China_panoramio_4.qoi b/qoi/images/Linze_Zhangye_Gansu_China_panoramio_4.qoi
new file mode 100644
index 00000000..66045fb6
Binary files /dev/null and b/qoi/images/Linze_Zhangye_Gansu_China_panoramio_4.qoi differ
diff --git a/qoi/images/Plaigne_2.png b/qoi/images/Plaigne_2.png
new file mode 100644
index 00000000..94413534
Binary files /dev/null and b/qoi/images/Plaigne_2.png differ
diff --git a/qoi/images/Plaigne_2.qoi b/qoi/images/Plaigne_2.qoi
new file mode 100644
index 00000000..9620495e
Binary files /dev/null and b/qoi/images/Plaigne_2.qoi differ
diff --git a/qoi/images/README.md b/qoi/images/README.md
index 9244fd2c..1fcd045d 100644
--- a/qoi/images/README.md
+++ b/qoi/images/README.md
@@ -2,6 +2,14 @@
 
 (listed in alphabetical order)
 
+## `Bridalveil_Fall_and_valley`
+* Retrieved from https://commons.wikimedia.org/wiki/File:Bridalveil_Fall_and_valley.JPG
+* Author: [Amadscientist](https://commons.wikimedia.org/wiki/User:Amadscientist)
+* License: [Creative Commons](https://en.wikipedia.org/wiki/en:Creative_Commons) [Attribution-Share Alike 3.0 Unported](https://creativecommons.org/licenses/by-sa/3.0/deed.en)
+* Modifications:
+  * downscaled and exported from `.jpg` to `.png` through GIMP 2.10
+  * exported from `.png` to `.qoi` through [`qoiconv`](https://github.com/phoboslab/qoi/blob/master/qoiconv.c)
+
 ## `Central_Bern_from_north`
 * Retrieved from https://commons.wikimedia.org/wiki/File:Central_Bern_from_north.jpg
 * Author: [CucombreLibre](https://www.flickr.com/people/33200530@N04)
@@ -10,6 +18,15 @@
   * downscaled and exported from `.jpg` to `.png` through GIMP 2.10
   * exported from `.png` to `.qoi` through [`qoiconv`](https://github.com/phoboslab/qoi/blob/master/qoiconv.c)
 
+## `Chiffchaff_Phylloscopus_collybita`
+* Retrieved from https://commons.wikimedia.org/wiki/File:Chiffchaff_(Phylloscopus_collybita).jpg
+* Author: [א](https://commons.wikimedia.org/wiki/User:%D7%90)
+* License: [Creative Commons](https://en.wikipedia.org/wiki/en:Creative_Commons) [Attribution-Share Alike 2.5 Generic](https://creativecommons.org/licenses/by-sa/2.5/deed.en)
+* Modifications:
+  * renamed from `Chiffchaff_(Phylloscopus_collybita)` to `Chiffchaff_Phylloscopus_collybita`.
+  * downscaled and exported from `.jpg` to `.png` through GIMP 2.10
+  * exported from `.png` to `.qoi` through [`qoiconv`](https://github.com/phoboslab/qoi/blob/master/qoiconv.c)
+
 ## `Chocolate_Hills_overview`
 * Retrieved from https://commons.wikimedia.org/wiki/File:Chocolate_Hills_overview.JPG
 * Author: [P199](https://commons.wikimedia.org/wiki/User:P199)
@@ -26,3 +43,21 @@
   * renamed from `L'Eyjafjallajökull_sous_les_aurores_boréales` to `Eyjafjallajokull_sous_les_aurores_boreales`
   * downscaled and exported from `.jpg` to `.png` through GIMP 2.10
   * exported from `.png` to `.qoi` through [`qoiconv`](https://github.com/phoboslab/qoi/blob/master/qoiconv.c)
+
+## `Linze_Zhangye_Gansu_China_panoramio_4`
+* Retrieved from https://commons.wikimedia.org/wiki/File:Linze,_Zhangye,_Gansu,_China_-_panoramio_(4).jpg
+* Author: [Han Lei](https://web.archive.org/web/20161027200109/http://www.panoramio.com/user/1540469?with_photo_id=102251104)
+* License: [Creative Commons](https://en.wikipedia.org/wiki/en:Creative_Commons) [Attribution-Share Alike 3.0 Unported](https://creativecommons.org/licenses/by-sa/3.0/deed.en)
+* Modifications:
+  * renamed from `Linze,_Zhangye,_Gansu,_China_-_panoramio_(4)` to `Linze_Zhangye_Gansu_China_panoramio_4`.
+  * downscaled and exported from `.jpg` to `.png` through GIMP 2.10
+  * exported from `.png` to `.qoi` through [`qoiconv`](https://github.com/phoboslab/qoi/blob/master/qoiconv.c)
+
+## `Plaigne_2`
+* Retrieved from https://commons.wikimedia.org/wiki/File:Plaigne_(2).jpg
+* Author: [Jcb-caz-11](https://commons.wikimedia.org/wiki/User:Jcb-caz-11)
+* License: [Creative Commons](https://en.wikipedia.org/wiki/en:Creative_Commons) [Attribution 4.0 International](https://creativecommons.org/licenses/by/4.0/deed.en)
+* Modifications:
+  * renamed from `Plaigne_(2)` to `Plaigne_2`
+  * downscaled and exported from `.jpg` to `.png` through GIMP 2.10
+  * exported from `.png` to `.qoi` through [`qoiconv`](https://github.com/phoboslab/qoi/blob/master/qoiconv.c)
diff --git a/qoi/verified/decoder.scala b/qoi/verified/decoder.scala
index 045d375f..ce8d0766 100644
--- a/qoi/verified/decoder.scala
+++ b/qoi/verified/decoder.scala
@@ -8,7 +8,7 @@ import common.*
 
 object decoder {
 
-  case class Ctx(bytes: Array[Byte], w: Long, h: Long, chan: Long) {
+  case class DecCtx(bytes: Array[Byte], w: Long, h: Long, chan: Long) {
     require(0 < w && w <= MaxWidth &&
       0 < h && h <= MaxHeight &&
       3 <= chan && chan <= 4 &&
@@ -39,8 +39,8 @@ object decoder {
 
   @pure
   @cCode.`export`
-  def decode(bytes: Array[Byte], to: Long): OptionMut[DecodedResult] = {
-    if (!(bytes.length > HeaderSize + Padding && HeaderSize + Padding < to && to <= bytes.length))
+  def decode(bytes: Array[Byte], until: Long): OptionMut[DecodedResult] = {
+    if (!(bytes.length > HeaderSize + Padding && HeaderSize + Padding < until && until <= bytes.length))
       NoneMut()
     else {
       decodeHeader(bytes) match {
@@ -51,14 +51,14 @@ object decoder {
           val index = Array.fill(64)(0)
           val pixels = allocArray(w.toInt * h.toInt * chan.toInt)
           val px = Pixel.fromRgba(0, 0, 0, 255.toByte)
-          val decIter = decodeLoop(index, pixels, px, HeaderSize, to - Padding, 0)(using Ctx(bytes, w, h, chan))
+          val decIter = decodeLoop(index, pixels, px, HeaderSize, until - Padding, 0)(using DecCtx(bytes, w, h, chan))
           @ghost val pixelsPreWrite = freshCopy(pixels)
           ghostExpr {
             check(0 <= decIter.pxPos && decIter.pxPos <= pixels.length)
             check(decIter.pxPos % chan == 0)
           }
           if (decIter.pxPos != pixels.length) {
-            writeRemainingPixels(pixels, decIter.px, decIter.pxPos, decIter.pxPos)(using Ctx(bytes, w, h, chan))
+            writeRemainingPixels(pixels, decIter.px, decIter.pxPos, decIter.pxPos)(using DecCtx(bytes, w, h, chan))
           }
           ghostExpr {
             if (decIter.pxPos != pixels.length) {
@@ -78,7 +78,7 @@ object decoder {
 
   @opaque
   @inlineOnce
-  def writeRemainingPixels(pixels: Array[Byte], pxPrev: Int, pxPos: Long, @ghost pxPosOrig: Long)(using Ctx): Unit = {
+  def writeRemainingPixels(pixels: Array[Byte], pxPrev: Int, pxPos: Long, @ghost pxPosOrig: Long)(using DecCtx): Unit = {
     decreases(pixels.length - pxPos)
     require(pixels.length == pixelsLen)
     require(0 <= pxPos && pxPos < pixels.length)
@@ -162,7 +162,7 @@ object decoder {
   }
 
   def decodeLoop(index: Array[Int], pixels: Array[Byte], pxPrev: Int,
-                 inPos0: Long, untilInPos: Long, pxPos0: Long)(using Ctx): DecodingIteration = {
+                 inPos0: Long, untilInPos: Long, pxPos0: Long)(using DecCtx): DecodingIteration = {
     decreases(untilInPos - inPos0)
     require(index.length == 64)
     require(pixels.length == pixelsLen)
@@ -188,7 +188,7 @@ object decoder {
     HeaderSize <= decIter.inPos
   }
 
-  def decodeNext(index: Array[Int], pixels: Array[Byte], pxPrev: Int, inPos0: Long, pxPos0: Long)(using Ctx): (DecodedNext, DecodingIteration) = {
+  def decodeNext(index: Array[Int], pixels: Array[Byte], pxPrev: Int, inPos0: Long, pxPos0: Long)(using DecCtx): (DecodedNext, DecodingIteration) = {
     require(index.length == 64)
     require(pixels.length == pixelsLen)
     require(inPosInv(inPos0))
@@ -228,7 +228,7 @@ object decoder {
   }
 
   @pure
-  def doDecodeNext(index: Array[Int], pxPrev: Int, inPos0: Long)(using Ctx): (DecodedNext, Long) = {
+  def doDecodeNext(index: Array[Int], pxPrev: Int, inPos0: Long)(using DecCtx): (DecodedNext, Long) = {
     require(index.length == 64)
     require(HeaderSize <= inPos0 && inPos0 < chunksLen)
     var px = pxPrev
@@ -281,7 +281,7 @@ object decoder {
   }
 
   // Note: not opaque, as writeRunPixelsPureBytesEqLemma needs to see its definition.
-  def writeRunPixels(pixels: Array[Byte], px: Int, run0: Long, pxPos0: Long)(using Ctx): WriteRunPixelsResult = {
+  def writeRunPixels(pixels: Array[Byte], px: Int, run0: Long, pxPos0: Long)(using DecCtx): WriteRunPixelsResult = {
     decreases(pixelsLen - pxPos0)
     require(pixels.length == pixelsLen)
     require(runInv(run0))
@@ -389,7 +389,7 @@ object decoder {
   }
 
   // Note: not opaque, as writePixelPureBytesEqLemma needs to see its definition.
-  def writePixel(pixels: Array[Byte], px: Int, pxPos: Long)(using Ctx): Unit = {
+  def writePixel(pixels: Array[Byte], px: Int, pxPos: Long)(using DecCtx): Unit = {
     require(pixels.length == pixelsLen)
     require(pxPosInv(pxPos))
     require(pxPos + chan <= pixels.length)
@@ -452,26 +452,26 @@ object decoder {
     0 <= run && run <= 62
 
   @ghost
-  def pxPosInv(pxPos: Long)(using Ctx): Boolean =
+  def pxPosInv(pxPos: Long)(using DecCtx): Boolean =
     0 <= pxPos && pxPos <= pixelsLen && pxPos % chan == 0
 
   @ghost
-  def inPosInv(inPos: Long)(using Ctx): Boolean =
+  def inPosInv(inPos: Long)(using DecCtx): Boolean =
     HeaderSize <= inPos && inPos <= bytes.length - Padding
 
   @ghost
-  def rangesInv(run: Long, inPos: Long, pxPos: Long)(using Ctx): Boolean =
+  def rangesInv(run: Long, inPos: Long, pxPos: Long)(using DecCtx): Boolean =
     pxPosInv(pxPos) && runInv(run) && inPosInv(inPos)
 
   @ghost
-  def rangesInv(indexLen: Long, run: Long, inPos: Long, pxPos: Long)(using Ctx): Boolean =
+  def rangesInv(indexLen: Long, run: Long, inPos: Long, pxPos: Long)(using DecCtx): Boolean =
     pxPosInv(pxPos) && runInv(run) && inPosInv(inPos) && indexLen == 64
 
   /////////////////////////////////////////////////////////////////////////////////////////////////////
 
   @ghost
   @pure
-  def writePixelPure(pixels: Array[Byte], px: Int, pxPos: Long)(using Ctx): Array[Byte] = {
+  def writePixelPure(pixels: Array[Byte], px: Int, pxPos: Long)(using DecCtx): Array[Byte] = {
     require(pixels.length == pixelsLen)
     require(pxPosInv(pxPos))
     require(pxPos + chan <= pixels.length)
@@ -488,7 +488,7 @@ object decoder {
   @pure
   @opaque
   @inlineOnce
-  def writePixelPureBytesEqLemma(pixels: Array[Byte], px: Int, pxPos: Long, from: Long, until: Long, bytes2: Array[Byte])(using ctx1: Ctx): Unit = {
+  def writePixelPureBytesEqLemma(pixels: Array[Byte], px: Int, pxPos: Long, from: Long, until: Long, bytes2: Array[Byte])(using ctx1: DecCtx): Unit = {
     require(pixels.length == pixelsLen)
     require(pxPosInv(pxPos))
     require(pxPos + chan <= pixels.length)
@@ -496,7 +496,7 @@ object decoder {
     require(0 <= from && from <= until && until <= bytes.length)
     require(arraysEq(bytes, bytes2, from, until))
 
-    val ctx2 = Ctx(freshCopy(bytes2), w, h, chan)
+    val ctx2 = DecCtx(freshCopy(bytes2), w, h, chan)
     val pix1 = writePixelPure(pixels, px, pxPos)(using ctx1)
     val pix2 = writePixelPure(pixels, px, pxPos)(using ctx2)
 
@@ -506,7 +506,7 @@ object decoder {
   }
 
   @ghost
-  def writeRunPixelsInv(pxPos0: Long, run0: Long, pxPos2: Long, run2: Long)(using Ctx): Boolean = {
+  def writeRunPixelsInv(pxPos0: Long, run0: Long, pxPos2: Long, run2: Long)(using DecCtx): Boolean = {
     require(runInv(run0))
     require(pxPosInv(pxPos0))
     require(pxPos0 + chan <= pixelsLen)
@@ -515,7 +515,7 @@ object decoder {
 
   @ghost
   @pure
-  def writeRunPixelsPure(pixels: Array[Byte], px: Int, run0: Long, pxPos0: Long)(using Ctx): (Array[Byte], Long, Long) = {
+  def writeRunPixelsPure(pixels: Array[Byte], px: Int, run0: Long, pxPos0: Long)(using DecCtx): (Array[Byte], Long, Long) = {
     require(pixels.length == pixelsLen)
     require(runInv(run0))
     require(pxPosInv(pxPos0))
@@ -537,7 +537,7 @@ object decoder {
   @pure
   @opaque
   @inlineOnce
-  def writeRunPixelPureBytesEqLemma(pixels: Array[Byte], px: Int, run0: Long, pxPos0: Long, from: Long, until: Long, bytes2: Array[Byte])(using ctx1: Ctx): Unit = {
+  def writeRunPixelPureBytesEqLemma(pixels: Array[Byte], px: Int, run0: Long, pxPos0: Long, from: Long, until: Long, bytes2: Array[Byte])(using ctx1: DecCtx): Unit = {
     decreases(pixelsLen - pxPos0)
     require(pixels.length == pixelsLen)
     require(runInv(run0))
@@ -547,7 +547,7 @@ object decoder {
     require(0 <= from && from <= until && until <= bytes.length)
     require(arraysEq(bytes, bytes2, from, until))
 
-    val ctx2 = Ctx(freshCopy(bytes2), w, h, chan)
+    val ctx2 = DecCtx(freshCopy(bytes2), w, h, chan)
     val (pix1, run1, pxPos1) = writeRunPixelsPure(pixels, px, run0, pxPos0)(using ctx1)
     val (pix2, run2, pxPos2) = writeRunPixelsPure(pixels, px, run0, pxPos0)(using ctx2)
 
@@ -593,7 +593,7 @@ object decoder {
 
   @ghost
   @pure
-  def decodeNextPure(index: Array[Int], pixels: Array[Byte], pxPrev: Int, inPos0: Long, pxPos0: Long)(using Ctx): (Array[Int], Array[Byte], DecodedNext, DecodingIteration) = {
+  def decodeNextPure(index: Array[Int], pixels: Array[Byte], pxPrev: Int, inPos0: Long, pxPos0: Long)(using DecCtx): (Array[Int], Array[Byte], DecodedNext, DecodingIteration) = {
     require(index.length == 64)
     require(pixels.length == pixelsLen)
     require(inPosInv(inPos0))
@@ -636,7 +636,7 @@ object decoder {
   @pure
   @opaque
   @inlineOnce
-  def decodeLemma(until: Long)(using Ctx): Unit = {
+  def decodeLemma(until: Long)(using DecCtx): Unit = {
     require(HeaderSize + Padding < until && until <= bytes.length)
     val readMagic = read32(bytes, 0)
     val readW = read32(bytes, 4)
@@ -669,7 +669,7 @@ object decoder {
   @ghost
   @pure
   def decodeLoopPure(index: Array[Int], pixels: Array[Byte], pxPrev: Int,
-                      inPos0: Long, untilInPos: Long, pxPos0: Long)(using Ctx): (Array[Int], Array[Byte], DecodingIteration) = {
+                      inPos0: Long, untilInPos: Long, pxPos0: Long)(using DecCtx): (Array[Int], Array[Byte], DecodingIteration) = {
     require(index.length == 64)
     require(pixels.length == pixelsLen)
     require(inPosInv(inPos0))
@@ -697,7 +697,7 @@ object decoder {
                                pxPrev: Int,
                                inPos0: Long,
                                inPos1: Long,
-                               pxPos0: Long)(using Ctx): Unit = {
+                               pxPos0: Long)(using DecCtx): Unit = {
     require(index.length == 64)
     require(pixels.length == pixelsLen)
     require(inPosInv(inPos0))
@@ -738,7 +738,7 @@ object decoder {
                                  inPos0: Long,
                                  untilInPos: Long,
                                  pxPos0: Long,
-                                 bytes2: Array[Byte])(using ctx1: Ctx): Unit = {
+                                 bytes2: Array[Byte])(using ctx1: DecCtx): Unit = {
     decreases(untilInPos - inPos0)
     require(index.length == 64)
     require(pixels.length == pixelsLen)
@@ -749,7 +749,7 @@ object decoder {
     require(bytes.length == bytes2.length)
     require(arraysEq(bytes, bytes2, inPos0, untilInPos))
 
-    val ctx2 = Ctx(freshCopy(bytes2), w, h, chan)
+    val ctx2 = DecCtx(freshCopy(bytes2), w, h, chan)
     val res1 = decodeLoopPure(index, pixels, pxPrev, inPos0, untilInPos, pxPos0)(using ctx1)
     val ix1 = res1._1
     val pix1 = res1._2
@@ -824,7 +824,7 @@ object decoder {
                                 inPos0: Long,
                                 inPos1: Long,
                                 inPos2: Long,
-                                pxPos0: Long)(using Ctx): Unit = {
+                                pxPos0: Long)(using DecCtx): Unit = {
     decreases(inPos2 - inPos0)
     require(index.length == 64)
     require(pixels.length == pixelsLen)
@@ -897,7 +897,7 @@ object decoder {
   @opaque
   @inlineOnce
   @pure
-  def decodeNextPureBytesEqLemma(index: Array[Int], pixels: Array[Byte], pxPrev: Int, inPos0: Long, pxPos0: Long, bytes2: Array[Byte])(using ctx1: Ctx): Unit = {
+  def decodeNextPureBytesEqLemma(index: Array[Int], pixels: Array[Byte], pxPrev: Int, inPos0: Long, pxPos0: Long, bytes2: Array[Byte])(using ctx1: DecCtx): Unit = {
     require(index.length == 64)
     require(pixels.length == pixelsLen)
     require(inPosInv(inPos0))
@@ -905,7 +905,7 @@ object decoder {
     require(pxPos0 + chan <= pixels.length)
     require(inPos0 < chunksLen)
     require(bytes.length == bytes2.length)
-    val ctx2 = Ctx(freshCopy(bytes2), w, h, chan)
+    val ctx2 = DecCtx(freshCopy(bytes2), w, h, chan)
     val resNext1 = decodeNextPure(index, pixels, pxPrev, inPos0, pxPos0)(using ctx1)
     val ix1 = resNext1._1
     val pix1 = resNext1._2
@@ -994,13 +994,13 @@ object decoder {
   @opaque
   @inlineOnce
   @pure
-  def doDecodeNextBytesEqLemma(index: Array[Int], pxPrev: Int, inPos0: Long, bytes2: Array[Byte])(using ctx1: Ctx): Unit = {
+  def doDecodeNextBytesEqLemma(index: Array[Int], pxPrev: Int, inPos0: Long, bytes2: Array[Byte])(using ctx1: DecCtx): Unit = {
     require(index.length == 64)
     require(inPosInv(inPos0))
     require(inPos0 < chunksLen)
     require(bytes.length == bytes2.length)
 
-    val ctx2 = Ctx(freshCopy(bytes2), w, h, chan)
+    val ctx2 = DecCtx(freshCopy(bytes2), w, h, chan)
     val (res1, inPos1) = doDecodeNext(index, pxPrev, inPos0)(using ctx1)
     require(arraysEq(bytes, bytes2, inPos0, inPos1))
     val (res2, inPos2) = doDecodeNext(index, pxPrev, inPos0)(using ctx2)
@@ -1021,25 +1021,25 @@ object decoder {
 
   @inline
   @cCode.inline
-  def w(using ctx: Ctx): Long = ctx.w
+  def w(using ctx: DecCtx): Long = ctx.w
 
   @inline
   @cCode.inline
-  def h(using ctx: Ctx): Long = ctx.h
+  def h(using ctx: DecCtx): Long = ctx.h
 
   @inline
   @cCode.inline
-  def chan(using ctx: Ctx): Long = ctx.chan
+  def chan(using ctx: DecCtx): Long = ctx.chan
 
   @inline
   @cCode.inline
-  def pixelsLen(using ctx: Ctx): Long = ctx.pixelsLen
+  def pixelsLen(using ctx: DecCtx): Long = ctx.pixelsLen
 
   @inline
   @cCode.inline
-  def chunksLen(using ctx: Ctx): Long = ctx.chunksLen
+  def chunksLen(using ctx: DecCtx): Long = ctx.chunksLen
 
   @inline
   @cCode.inline
-  def bytes(using ctx: Ctx): Array[Byte] = ctx.bytes
+  def bytes(using ctx: DecCtx): Array[Byte] = ctx.bytes
 }
diff --git a/qoi/verified/encoder.scala b/qoi/verified/encoder.scala
index 071989ae..0fef3841 100644
--- a/qoi/verified/encoder.scala
+++ b/qoi/verified/encoder.scala
@@ -8,7 +8,7 @@ import common.*
 
 object encoder {
 
-  case class Ctx(pixels: Array[Byte], w: Long, h: Long, chan: Long) {
+  case class EncCtx(pixels: Array[Byte], w: Long, h: Long, chan: Long) {
     require(0 < w && w <= MaxWidth &&
       0 < h && h <= MaxHeight &&
       3 <= chan && chan <= 4 &&
@@ -24,9 +24,7 @@ object encoder {
   @cCode.`export`
   case class EncodedResult(encoded: Array[Byte], length: Long)
 
-  case class EncodeSingleStepResult(px: Int, outPos: Long, run: Long)
-
-  case class EncodingIteration(px: Int, outPos: Long)
+  case class EncodingIteration(px: Int, outPos: Long, run: Long)
 
   case class RunUpdate(reset: Boolean, run: Long, outPos: Long)
 
@@ -42,8 +40,8 @@ object encoder {
 
   @ghost
   @pure
-  def decodeEncodeIsIdentityThm(using Ctx): Boolean = {
-    val SomeMut(EncodedResult(bytes, outPos)) = doEncode
+  def decodeEncodeIsIdentityThm(using EncCtx): Boolean = {
+    val EncodedResult(bytes, outPos) = encode()
 
     decoder.decode(bytes, outPos) match {
       case SomeMut(decoder.DecodedResult(decodedPixels, ww, hh, cchan)) =>
@@ -66,11 +64,12 @@ object encoder {
       3 <= chan && chan <= 4 &&
       w * h * chan == pixels.length))
       NoneMut()
-    else doEncode(using Ctx(pixels, w, h, chan))
+    else SomeMut(encode()(using EncCtx(pixels, w, h, chan)))
   }
 
   @pure
-  def doEncode(using Ctx): OptionMut[EncodedResult] = {
+  @cCode.inline // To allow "returning" arrays
+  def encode()(using EncCtx): EncodedResult = {
     val bytes = allocArray(maxSize.toInt)
     writeHeader(bytes)
     val index = Array.fill(64)(0)
@@ -78,7 +77,7 @@ object encoder {
     @ghost val decoded = GhostDecoded(freshCopy(index), Array.fill(pixels.length)(0: Byte), HeaderSize, 0)
     @ghost val initDecoded = freshCopy(decoded)
     @ghost val oldBytes = freshCopy(bytes)
-    val EncodingIteration(pxRes, outPos) = encodeLoop(index, bytes, pxPrev, 0, HeaderSize, 0, decoded)
+    val EncodingIteration(pxRes, outPos, _) = encodeLoop(index, bytes, pxPrev, 0, HeaderSize, 0, decoded)
 
     ghostExpr {
       assert(decodeLoopEncodeProp(bytes, pxPrev, HeaderSize, outPos, initDecoded, pxRes, decoded))
@@ -88,7 +87,7 @@ object encoder {
       assert(arraysEq(oldBytes, bytes, 0, HeaderSize))
       assert(HeaderSize <= outPos && outPos <= maxSize - Padding)
 
-      given decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+      given decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
 
       assert(pixels.length == w * h * chan)
       val (decIndex, decPixels, decIter) = decoder.decodeLoopPure(initDecoded.index, initDecoded.pixels, pxPrev, HeaderSize, outPos, 0)
@@ -137,12 +136,12 @@ object encoder {
       assert(arraysEq(pixels, actuallyDecoded, 0, pixels.length))
     }
 
-    SomeMut(EncodedResult(bytes, outPos + Padding))
+    EncodedResult(bytes, outPos + Padding)
   }
 
   @opaque
   @inlineOnce
-  def encodeLoop(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long, @ghost decoded: GhostDecoded)(using Ctx): EncodingIteration = {
+  def encodeLoop(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long, @ghost decoded: GhostDecoded)(using EncCtx): EncodingIteration = {
     decreases(pixels.length - pxPos)
     require(rangesInv(index.length, bytes.length, run0, outPos0, pxPos))
     require(pxPos + chan <= pixels.length)
@@ -159,7 +158,7 @@ object encoder {
 
     @ghost val oldDecoded = freshCopy(decoded)
     @ghost val oldBytes = freshCopy(bytes)
-    val EncodeSingleStepResult(px, outPos2, run1) = encodeSingleStep(index, bytes, pxPrev, run0, outPos0, pxPos, decoded)
+    val EncodingIteration(px, outPos2, run1) = encodeSingleStep(index, bytes, pxPrev, run0, outPos0, pxPos, decoded)
     ghostExpr {
       assert(decoded.pixels.length == pixels.length)
       check(bytes.length == maxSize)
@@ -250,7 +249,7 @@ object encoder {
       val res = encodeLoop(index, bytes, px, run1, outPos2, pxPosPlusChan, decoded)
 
       ghostExpr {
-        val EncodingIteration(pxRes, outPosRes) = res
+        val EncodingIteration(pxRes, outPosRes, _) = res
         check(bytes.length == maxSize && index == decoded.index)
         check(decoded.pixels.length == pixels.length)
         check(oldBytes.length == bytes.length)
@@ -278,7 +277,7 @@ object encoder {
           decodeLoopEncodePropBytesEqLemma(bytesPreRec, bytes, pxPrev, outPos0, outPos2, oldDecoded, px, decodedPreRec)
           assert(decodeLoopEncodeProp(bytes, pxPrev, outPos0, outPos2, oldDecoded, px, decodedPreRec))
 
-          given decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+          given decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
 
           val (ix1, pix1, decIter1) = decoder.decodeLoopPure(oldDecoded.index, oldDecoded.pixels, pxPrev, outPos0, outPos2, oldDecoded.pxPos)
           assert(decIter1.pxPos == decodedPreRec.pxPos)
@@ -391,9 +390,9 @@ object encoder {
         decodeLoopEncodePropBytesEqLemma(bytesPrePadded, bytes, pxPrev, outPos0, outPos2, oldDecoded, px, decoded)
         check(decodeLoopEncodeProp(bytes, pxPrev, outPos0, outPos2, oldDecoded, px, decoded))
       }
-      EncodingIteration(px, outPos2)
+      EncodingIteration(px, outPos2, run1)
     }
-  }.ensuring { case EncodingIteration(pxRes, outPosRes) =>
+  }.ensuring { case EncodingIteration(pxRes, outPosRes, _) =>
     bytes.length == maxSize &&&
     index.length == 64 &&&
     index == decoded.index &&&
@@ -408,7 +407,7 @@ object encoder {
 
   @opaque
   @inlineOnce
-  def writeHeader(bytes: Array[Byte])(using Ctx): Unit = {
+  def writeHeader(bytes: Array[Byte])(using EncCtx): Unit = {
     require(bytes.length >= HeaderSize)
     write32(bytes, 0, MagicNumber)
     assert(read32(bytes, 0) == MagicNumber)
@@ -434,7 +433,7 @@ object encoder {
 
   @opaque
   @inlineOnce
-  def encodeSingleStep(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long, @ghost decoded: GhostDecoded)(using Ctx): EncodeSingleStepResult = {
+  def encodeSingleStep(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long, @ghost decoded: GhostDecoded)(using EncCtx): EncodingIteration = {
     require(rangesInv(index.length, bytes.length, run0, outPos0, pxPos))
     require(pxPos + chan <= pixels.length)
     require(positionsIneqInv(run0, outPos0, pxPos))
@@ -631,7 +630,7 @@ object encoder {
       }
 
 
-      given decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+      given decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
 
       val (ix3, pix3, decIter3) = {
         assert(decoded.pixels.length == pixels.length)
@@ -800,8 +799,8 @@ object encoder {
       check(index == decoded.index)
     }
 
-    EncodeSingleStepResult(px, outPos2, run1)
-  }.ensuring { case EncodeSingleStepResult(px, outPos2, run1) => // Wins the "slowest to verify" award (~210s)
+    EncodingIteration(px, outPos2, run1)
+  }.ensuring { case EncodingIteration(px, outPos2, run1) => // Wins the "slowest to verify" award (~210s)
     // Bytes and index length are unchanged
     bytes.length == maxSize &&&
     index.length == 64 &&&
@@ -828,7 +827,7 @@ object encoder {
   }
 
   @inline
-  def updateRun(bytes: Array[Byte], run0: Long, outPos0: Long)(using Ctx, LoopIter): RunUpdate = {
+  def updateRun(bytes: Array[Byte], run0: Long, outPos0: Long)(using EncCtx, LoopIter): RunUpdate = {
     require(bytes.length == maxSize)
     require(runInv(run0))
     require(outPosInv(outPos0))
@@ -885,7 +884,7 @@ object encoder {
 
   @opaque
   @inlineOnce
-  def encodeNoRun(index: Array[Int], bytes: Array[Byte], outPos1: Long)(using Ctx, LoopIter): Long = {
+  def encodeNoRun(index: Array[Int], bytes: Array[Byte], outPos1: Long)(using EncCtx, LoopIter): Long = {
     require(index.length == 64)
     require(bytes.length == maxSize)
     require(outPosInv(outPos1))
@@ -1025,7 +1024,7 @@ object encoder {
   /////////////////////////////////////////////////////////////////////////////////////////////////////
 
   @ghost
-  def positionsIneqInv(run: Long, outPos: Long, pxPos: Long)(using Ctx): Boolean =
+  def positionsIneqInv(run: Long, outPos: Long, pxPos: Long)(using EncCtx): Boolean =
     chan * (outPos - HeaderSize + chan * run) <= (chan + 1) * pxPos
 
   @ghost
@@ -1033,19 +1032,19 @@ object encoder {
     0 <= run && run < 62
 
   @ghost
-  def pxPosInv(pxPos: Long)(using Ctx): Boolean =
+  def pxPosInv(pxPos: Long)(using EncCtx): Boolean =
     0 <= pxPos && pxPos <= pixels.length && pxPos % chan == 0
 
   @ghost
-  def outPosInv(outPos: Long)(using Ctx): Boolean =
+  def outPosInv(outPos: Long)(using EncCtx): Boolean =
     HeaderSize <= outPos && outPos <= maxSize - Padding
 
   @ghost
-  def rangesInv(run: Long, outPos: Long, pxPos: Long)(using Ctx): Boolean =
+  def rangesInv(run: Long, outPos: Long, pxPos: Long)(using EncCtx): Boolean =
     pxPosInv(pxPos) && runInv(run) && outPosInv(outPos)
 
   @ghost
-  def rangesInv(indexLen: Long, bytesLen: Long, run: Long, outPos: Long, pxPos: Long)(using Ctx): Boolean =
+  def rangesInv(indexLen: Long, bytesLen: Long, run: Long, outPos: Long, pxPos: Long)(using EncCtx): Boolean =
     pxPosInv(pxPos) && runInv(run) && outPosInv(outPos) && bytesLen == maxSize && indexLen == 64
 
   /////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -1053,7 +1052,7 @@ object encoder {
   @ghost
   @opaque
   @inlineOnce
-  def withinBoundsLemma(run: Long, outPos: Long, pxPos: Long)(using Ctx): Unit = {
+  def withinBoundsLemma(run: Long, outPos: Long, pxPos: Long)(using EncCtx): Unit = {
     require(rangesInv(run, outPos, pxPos))
     require(positionsIneqInv(run, outPos, pxPos))
     require(pxPos + chan <= pixels.length)
@@ -1069,7 +1068,7 @@ object encoder {
   @ghost
   @opaque
   @inlineOnce
-  def withinBoundsLemma2(run: Long, outPos: Long, pxPos: Long)(using Ctx): Unit = {
+  def withinBoundsLemma2(run: Long, outPos: Long, pxPos: Long)(using EncCtx): Unit = {
     require(rangesInv(run, outPos, pxPos))
     require(positionsIneqInv(run, outPos, pxPos))
     assert(chan * (outPos - HeaderSize + chan * run + chan + 1) <= (chan + 1) * (pxPos + chan))
@@ -1089,7 +1088,7 @@ object encoder {
   @ghost
   @opaque
   @inlineOnce
-  def positionsIneqIncrementedLemma(run: Long, outPos: Long, pxPos: Long)(using Ctx): Unit = {
+  def positionsIneqIncrementedLemma(run: Long, outPos: Long, pxPos: Long)(using EncCtx): Unit = {
     require(rangesInv(run, outPos, pxPos))
     require(positionsIneqInv(run, outPos, pxPos))
   }.ensuring(_ => positionsIneqInv(run, outPos + chan + 1, pxPos + chan))
@@ -1097,7 +1096,7 @@ object encoder {
   @ghost
   @opaque
   @inlineOnce
-  def loopInvUpperOutPosLemma(run: Long, oldOutPos: Long, pxPos: Long, newOutPos: Long)(using Ctx): Unit = {
+  def loopInvUpperOutPosLemma(run: Long, oldOutPos: Long, pxPos: Long, newOutPos: Long)(using EncCtx): Unit = {
     require(rangesInv(run, oldOutPos, pxPos))
     require(HeaderSize <= newOutPos && newOutPos <= oldOutPos + chan + 1)
     require(positionsIneqInv(run, oldOutPos + chan + 1, pxPos))
@@ -1116,7 +1115,7 @@ object encoder {
                            outPos2: Long,
                            decoded: GhostDecoded,
                            px: Int,
-                           newDecoded: GhostDecoded)(using Ctx): Boolean = {
+                           newDecoded: GhostDecoded)(using EncCtx): Boolean = {
     require(bytes.length == maxSize)
     require(outPosInv(outPos0))
     require(outPosInv(outPos2))
@@ -1126,7 +1125,7 @@ object encoder {
     require(decoded.pxPos + chan <= decoded.pixels.length)
     require(outPos0 < outPos2)
 
-    given decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+    given decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
     assert(decoded.pixels.length == w * h * chan)
     assert(decoded.pixels.length % chan == 0)
     val (decIndex, decPixels, decIter) = decoder.decodeLoopPure(decoded.index, decoded.pixels, pxPrev, outPos0, outPos2, decoded.pxPos)
@@ -1155,7 +1154,7 @@ object encoder {
                                        outPos2: Long,
                                        decoded: GhostDecoded,
                                        px: Int,
-                                       newDecoded: GhostDecoded)(using Ctx): Unit = {
+                                       newDecoded: GhostDecoded)(using EncCtx): Unit = {
     require(bytes1.length == maxSize)
     require(outPosInv(outPos0))
     require(outPosInv(outPos2))
@@ -1169,7 +1168,7 @@ object encoder {
     require(arraysEq(bytes1, bytes2, outPos0, outPos2))
     require(pxPosInv(newDecoded.pxPos))
 
-    val ctx1 = decoder.Ctx(freshCopy(bytes1), w, h, chan)
+    val ctx1 = decoder.DecCtx(freshCopy(bytes1), w, h, chan)
     assert(decoded.pixels.length % chan == 0)
     assert(decoded.pixels.length == w * h * chan)
     assert(outPos0 <= bytes1.length)
@@ -1178,7 +1177,7 @@ object encoder {
     assert(decIter1.pxPos <= pixels.length)
     assert(decIter1.inPos == outPos2)
 
-    val ctx2 = decoder.Ctx(freshCopy(bytes2), w, h, chan)
+    val ctx2 = decoder.DecCtx(freshCopy(bytes2), w, h, chan)
     decoder.decodeLoopPureBytesEqLemma(decoded.index, decoded.pixels, pxPrev, outPos0, outPos2, decoded.pxPos, bytes2)(using ctx1)
     val (ix2, pix2, decIter2) = decoder.decodeLoopPure(decoded.index, decoded.pixels, pxPrev, outPos0, outPos2, decoded.pxPos)(using ctx2)
     assert(ix1 == ix2)
@@ -1191,7 +1190,7 @@ object encoder {
   @pure
   @opaque
   @inlineOnce
-  def decodeUpdateRunPass(bytes: Array[Byte], run0: Long, outPos0: Long, ru: RunUpdate, decoded: GhostDecoded)(using Ctx, LoopIter): GhostDecoded = {
+  def decodeUpdateRunPass(bytes: Array[Byte], run0: Long, outPos0: Long, ru: RunUpdate, decoded: GhostDecoded)(using EncCtx, LoopIter): GhostDecoded = {
     require(bytes.length == maxSize)
     require(runInv(run0))
     require(outPosInv(outPos0))
@@ -1216,7 +1215,7 @@ object encoder {
     assert(pxPos % chan == 0)
     assert(pixels.length % chan == 0)
 
-    given dctx: decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+    given dctx: decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
     assert(decoded.pixels.length == w * h * chan)
     assert(decoded.pixels.length % chan == 0)
     assert(HeaderSize <= outPos0 && outPos0 <= bytes.length)
@@ -1307,7 +1306,7 @@ object encoder {
 
   @ghost
   @pure
-  def updateRunProp(bytes: Array[Byte], run0: Long, outPos0: Long, ru: RunUpdate)(using Ctx, LoopIter): Boolean = {
+  def updateRunProp(bytes: Array[Byte], run0: Long, outPos0: Long, ru: RunUpdate)(using EncCtx, LoopIter): Boolean = {
     require(bytes.length == maxSize)
     require(runInv(run0))
     require(outPosInv(outPos0))
@@ -1316,7 +1315,7 @@ object encoder {
     require(run > 0)
 
     val dummyIndex = Array.fill(64)(0)
-    given decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+    given decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
     decoder.doDecodeNext(dummyIndex, pxPrev, outPos0) match {
       case (decoder.Run(r), inPos) => r + 1 == run && inPos == ru.outPos
       case _ => false
@@ -1327,7 +1326,7 @@ object encoder {
   @pure
   @opaque
   @inlineOnce
-  def updateRunPropAnyIndexLemma(bytes: Array[Byte], index: Array[Int], run0: Long, outPos0: Long, ru: RunUpdate)(using Ctx, LoopIter): Unit = {
+  def updateRunPropAnyIndexLemma(bytes: Array[Byte], index: Array[Int], run0: Long, outPos0: Long, ru: RunUpdate)(using EncCtx, LoopIter): Unit = {
     require(bytes.length == maxSize)
     require(runInv(run0))
     require(outPosInv(outPos0))
@@ -1336,7 +1335,7 @@ object encoder {
     require(run > 0)
     require(updateRunProp(bytes, run0, outPos0, ru))
     require(index.length == 64)
-    val ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+    val ctx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
     val decodedNextRes = decoder.doDecodeNext(index, pxPrev, outPos0)(using ctx)
 
     {
@@ -1350,7 +1349,7 @@ object encoder {
   @ghost
   @pure
   def updateRunPropBytesEqLemma(bytes: Array[Byte], run0: Long, outPos0: Long,
-                                ru: RunUpdate, bytes2: Array[Byte])(using Ctx, LoopIter): Unit = {
+                                ru: RunUpdate, bytes2: Array[Byte])(using EncCtx, LoopIter): Unit = {
     require(bytes.length == maxSize)
     require(runInv(run0))
     require(outPosInv(outPos0))
@@ -1364,8 +1363,8 @@ object encoder {
     require(arraysEq(bytes, bytes2, 0, ru.outPos))
     require(outPos0 + 1 <= ru.outPos)
 
-    val dctx1: decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
-    val dctx2: decoder.Ctx = decoder.Ctx(freshCopy(bytes2), w, h, chan)
+    val dctx1: decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
+    val dctx2: decoder.DecCtx = decoder.DecCtx(freshCopy(bytes2), w, h, chan)
     val dummyIndex = Array.fill(64)(0)
     val res1 = decoder.doDecodeNext(dummyIndex, pxPrev, outPos0)(using dctx1)
     val res2 = decoder.doDecodeNext(dummyIndex, pxPrev, outPos0)(using dctx2)
@@ -1382,7 +1381,7 @@ object encoder {
   @ghost
   @opaque
   @inlineOnce
-  def decodeEncodeNoRunPass(oldIndex: Array[Int], index: Array[Int], bytes: Array[Byte], outPos1: Long, outPos2: Long, decoded: GhostDecoded)(using Ctx, LoopIter): GhostDecoded = {
+  def decodeEncodeNoRunPass(oldIndex: Array[Int], index: Array[Int], bytes: Array[Byte], outPos1: Long, outPos2: Long, decoded: GhostDecoded)(using EncCtx, LoopIter): GhostDecoded = {
     require(oldIndex.length == 64)
     require(index.length == 64)
     require(bytes.length == maxSize)
@@ -1402,7 +1401,7 @@ object encoder {
     require(px != pxPrev)
 
     assert(pxPos % chan == 0 && pixels.length % chan == 0)
-    given decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+    given decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
     val (decIndex, decPixels, decIter) = decoder.decodeLoopPure(decoded.index, decoded.pixels, pxPrev, outPos1, outPos2, decoded.pxPos)
     check(decPixels.length == decoded.pixels.length)
     check(decoded.pxPos < decIter.pxPos)
@@ -1441,7 +1440,7 @@ object encoder {
 
   @ghost
   @pure
-  def encodeNoRunProp(oldIndex: Array[Int], index: Array[Int], bytes: Array[Byte], outPos1: Long, outPos2: Long)(using Ctx, LoopIter): Boolean = {
+  def encodeNoRunProp(oldIndex: Array[Int], index: Array[Int], bytes: Array[Byte], outPos1: Long, outPos2: Long)(using EncCtx, LoopIter): Boolean = {
     require(oldIndex.length == 64)
     require(index.length == 64)
     require(bytes.length == maxSize)
@@ -1452,7 +1451,7 @@ object encoder {
     require(positionsIneqInv(0, outPos1, pxPos))
     require(outPos1 < outPos2)
 
-    given dctx: decoder.Ctx = decoder.Ctx(freshCopy(bytes), w, h, chan)
+    given dctx: decoder.DecCtx = decoder.DecCtx(freshCopy(bytes), w, h, chan)
     withinBoundsLemma(0, outPos1, pxPos)
     assert(0 <= pxPos && pxPos <= pixels.length && w * h * chan == pixels.length && pixels.length % chan == 0)
 
@@ -1468,27 +1467,27 @@ object encoder {
 
   @inline
   @cCode.inline
-  def maxSize(using ctx: Ctx): Long = ctx.maxSize
+  def maxSize(using ctx: EncCtx): Long = ctx.maxSize
 
   @inline
   @cCode.inline
-  def pxEnd(using ctx: Ctx): Long = ctx.pxEnd
+  def pxEnd(using ctx: EncCtx): Long = ctx.pxEnd
 
   @inline
   @cCode.inline
-  def w(using ctx: Ctx): Long = ctx.w
+  def w(using ctx: EncCtx): Long = ctx.w
 
   @inline
   @cCode.inline
-  def h(using ctx: Ctx): Long = ctx.h
+  def h(using ctx: EncCtx): Long = ctx.h
 
   @inline
   @cCode.inline
-  def chan(using ctx: Ctx): Long = ctx.chan
+  def chan(using ctx: EncCtx): Long = ctx.chan
 
   @inline
   @cCode.inline
-  def pixels(using ctx: Ctx): Array[Byte] = ctx.pixels
+  def pixels(using ctx: EncCtx): Array[Byte] = ctx.pixels
 
   @inline
   @cCode.inline