Skip to content

Commit

Permalink
Update the unannotated version as well
Browse files Browse the repository at this point in the history
  • Loading branch information
@mario-bucev @vkuncak
mario-bucev authored and vkuncak committed May 20, 2022
1 parent e44c5e4 commit 7ba5a3a
Show file tree
Hide file tree
Showing 4 changed files with 59 additions and 40 deletions.
13 changes: 13 additions & 0 deletions qoi/unannotated/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# Unannotated version of `verified`
This folder contains the same implementations as the one in `verified` with the following differences:
- Annotation, lemmas, etc. have been stripped
- Uses Scala's data structures (such as `Option`) instead of the one provided by Stainless' library

It allows to have a good overview of how many annotations are needed to prove correctness.

According to `cloc v1.82`, we have:
- `encoder.scala` 137 SLOC
- `decoder.scala` 136 SLOC
- `common.scala` 40 SLOC

For a total of 313 SLOC
34 changes: 17 additions & 17 deletions qoi/unannotated/decoder.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,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) {
def pixelsLen: Long = w * h * chan

def chunksLen: Long = bytes.length - Padding
Expand All @@ -20,33 +20,33 @@ object decoder {

/////////////////////////////////////////////////////////////////////////////////////////////////////

def decode(bytes: Array[Byte], to: Long): Option[DecodedResult] = {
if (!(bytes.length > HeaderSize + Padding && HeaderSize + Padding < to && to <= bytes.length)) {
def decode(bytes: Array[Byte], until: Long): Option[DecodedResult] = {
if (!(bytes.length > HeaderSize + Padding && HeaderSize + Padding < until && until <= bytes.length)) {
None
} else {
decodeHeader(bytes).map {
case (w, h, chan) =>
val index = Array.fill(64)(0)
val pixels = Array.fill(w.toInt * h.toInt * chan.toInt)(0: Byte)
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))
if (decIter.pxPos != pixels.length) {
writeRemainingPixels(pixels, decIter.px, decIter.pxPos)(using Ctx(bytes, w, h, chan))
writeRemainingPixels(pixels, decIter.px, decIter.pxPos)(using DecCtx(bytes, w, h, chan))
}
DecodedResult(pixels, w, h, chan)
}
}
}

def writeRemainingPixels(pixels: Array[Byte], pxPrev: Int, pxPos: Long)(using Ctx): Unit = {
def writeRemainingPixels(pixels: Array[Byte], pxPrev: Int, pxPos: Long)(using DecCtx): Unit = {
writePixel(pixels, pxPrev, pxPos)
if (pxPos + chan < pixels.length) {
writeRemainingPixels(pixels, pxPrev, pxPos + chan)
}
}

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 = {
val (res, decIter) = decodeNext(index, pixels, pxPrev, inPos0, pxPos0)

if (decIter.inPos < untilInPos && decIter.pxPos + chan <= pixels.length) {
Expand All @@ -56,7 +56,7 @@ object decoder {
}
}

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) = {
val (decRes, inPos) = doDecodeNext(index, pxPrev, inPos0)

decRes match {
Expand All @@ -71,7 +71,7 @@ object decoder {
}
}

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) = {
var px = pxPrev
var inPos = inPos0
var run = 0L
Expand Down Expand Up @@ -118,7 +118,7 @@ object decoder {
None
}

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 = {
writePixel(pixels, px, pxPos0)
if (run0 > 0 && pxPos0 + chan < pixels.length) {
writeRunPixels(pixels, px, run0 - 1, pxPos0 + chan)
Expand All @@ -127,7 +127,7 @@ object decoder {
}
}

def writePixel(pixels: Array[Byte], px: Int, pxPos: Long)(using Ctx): Unit = {
def writePixel(pixels: Array[Byte], px: Int, pxPos: Long)(using DecCtx): Unit = {
pixels(pxPos.toInt) = Pixel.r(px)
pixels(pxPos.toInt + 1) = Pixel.g(px)
pixels(pxPos.toInt + 2) = Pixel.b(px)
Expand Down Expand Up @@ -155,15 +155,15 @@ object decoder {

/////////////////////////////////////////////////////////////////////////////////////////////////////

def w(using ctx: Ctx): Long = ctx.w
def w(using ctx: DecCtx): Long = ctx.w

def h(using ctx: Ctx): Long = ctx.h
def h(using ctx: DecCtx): Long = ctx.h

def chan(using ctx: Ctx): Long = ctx.chan
def chan(using ctx: DecCtx): Long = ctx.chan

def pixelsLen(using ctx: Ctx): Long = ctx.pixelsLen
def pixelsLen(using ctx: DecCtx): Long = ctx.pixelsLen

def chunksLen(using ctx: Ctx): Long = ctx.chunksLen
def chunksLen(using ctx: DecCtx): Long = ctx.chunksLen

def bytes(using ctx: Ctx): Array[Byte] = ctx.bytes
def bytes(using ctx: DecCtx): Array[Byte] = ctx.bytes
}
43 changes: 20 additions & 23 deletions qoi/unannotated/encoder.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,15 @@ 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) {
def maxSize: Long = w * h * (chan + 1) + HeaderSize + Padding

def pxEnd: Long = pixels.length - chan
}

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)

Expand All @@ -27,31 +25,30 @@ object encoder {
3 <= chan && chan <= 4 &&
w * h * chan == pixels.length))
None
else doEncode(using Ctx(pixels, w, h, chan))
else Some(encode()(using EncCtx(pixels, w, h, chan)))
}

def doEncode(using Ctx): Option[EncodedResult] = {
def encode()(using EncCtx): EncodedResult = {
val bytes = Array.fill(maxSize.toInt)(0: Byte)
writeHeader(bytes)
val index = Array.fill(64)(0)
val pxPrev = Pixel.fromRgba(0, 0, 0, 255.toByte)
val EncodingIteration(pxRes, outPos) = encodeLoop(index, bytes, pxPrev, 0, HeaderSize, 0)
Some(EncodedResult(bytes, outPos + Padding))
val EncodingIteration(pxRes, outPos, _) = encodeLoop(index, bytes, pxPrev, 0, HeaderSize, 0)
EncodedResult(bytes, outPos + Padding)
}

def encodeLoop(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long)(using Ctx): EncodingIteration = {
val EncodeSingleStepResult(px, outPos2, run1) = encodeSingleStep(index, bytes, pxPrev, run0, outPos0, pxPos)
def encodeLoop(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long)(using EncCtx): EncodingIteration = {
val EncodingIteration(px, outPos2, run1) = encodeSingleStep(index, bytes, pxPrev, run0, outPos0, pxPos)

if (pxPos + chan < pixels.length) {
encodeLoop(index, bytes, px, run1, outPos2, pxPos + chan)
} else {
bytes(outPos2.toInt + Padding - 1) = 1
EncodingIteration(px, outPos2)
EncodingIteration(px, outPos2, run1)
}
}


def writeHeader(bytes: Array[Byte])(using Ctx): Unit = {
def writeHeader(bytes: Array[Byte])(using EncCtx): Unit = {
write32(bytes, 0, MagicNumber)
assert(read32(bytes, 0) == MagicNumber)

Expand All @@ -67,7 +64,7 @@ object encoder {
bytes(13) = 0 // Color-space (unused)
}

def encodeSingleStep(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long)(using Ctx): EncodeSingleStepResult = {
def encodeSingleStep(index: Array[Int], bytes: Array[Byte], pxPrev: Int, run0: Long, outPos0: Long, pxPos: Long)(using EncCtx): EncodingIteration = {
val px =
if (chan == 4) read32(pixels, pxPos.toInt)
else Pixel.fromRgba(pixels(pxPos.toInt), pixels(pxPos.toInt + 1), pixels(pxPos.toInt + 2), Pixel.a(pxPrev))
Expand All @@ -82,10 +79,10 @@ object encoder {
} else {
outPos1
}
EncodeSingleStepResult(px, outPos2, run1)
EncodingIteration(px, outPos2, run1)
}

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 = {
var run = run0
var outPos = outPos0

Expand All @@ -103,7 +100,7 @@ object encoder {
RunUpdate(runReset, run, outPos)
}

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 = {
val indexPos = colorPos(px)
var newOutPos = outPos1

Expand Down Expand Up @@ -160,17 +157,17 @@ object encoder {
newOutPos
}

def maxSize(using ctx: Ctx): Long = ctx.maxSize
def maxSize(using ctx: EncCtx): Long = ctx.maxSize

def pxEnd(using ctx: Ctx): Long = ctx.pxEnd
def pxEnd(using ctx: EncCtx): Long = ctx.pxEnd

def w(using ctx: Ctx): Long = ctx.w
def w(using ctx: EncCtx): Long = ctx.w

def h(using ctx: Ctx): Long = ctx.h
def h(using ctx: EncCtx): Long = ctx.h

def chan(using ctx: Ctx): Long = ctx.chan
def chan(using ctx: EncCtx): Long = ctx.chan

def pixels(using ctx: Ctx): Array[Byte] = ctx.pixels
def pixels(using ctx: EncCtx): Array[Byte] = ctx.pixels

def px(using li: LoopIter): Int = li.px

Expand Down
9 changes: 9 additions & 0 deletions qoi/verified/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
# Verified QOI
This folder contains the implementation of QOI alongside the proofs.

According to `cloc v1.82`, we have:
- `encoder.scala` 1303 SLOC
- `decoder.scala` 913 SLOC
- `common.scala` 573 SLOC

For a total of 2789 SLOC

0 comments on commit 7ba5a3a

Please sign in to comment.