From 7ba5a3afeb21ee817f2a6f8ca51c1a6e54ffcca9 Mon Sep 17 00:00:00 2001 From: Mario Bucev Date: Thu, 12 May 2022 15:41:31 +0200 Subject: [PATCH] Update the unannotated version as well --- qoi/unannotated/README.md | 13 +++++++++++ qoi/unannotated/decoder.scala | 34 +++++++++++++-------------- qoi/unannotated/encoder.scala | 43 ++++++++++++++++------------------- qoi/verified/README.md | 9 ++++++++ 4 files changed, 59 insertions(+), 40 deletions(-) create mode 100644 qoi/unannotated/README.md create mode 100644 qoi/verified/README.md diff --git a/qoi/unannotated/README.md b/qoi/unannotated/README.md new file mode 100644 index 00000000..d1dd1a6f --- /dev/null +++ b/qoi/unannotated/README.md @@ -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 diff --git a/qoi/unannotated/decoder.scala b/qoi/unannotated/decoder.scala index fbae46c2..2d14f60c 100644 --- a/qoi/unannotated/decoder.scala +++ b/qoi/unannotated/decoder.scala @@ -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 @@ -20,8 +20,8 @@ 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 { @@ -29,16 +29,16 @@ object decoder { 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) @@ -46,7 +46,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 = { val (res, decIter) = decodeNext(index, pixels, pxPrev, inPos0, pxPos0) if (decIter.inPos < untilInPos && decIter.pxPos + chan <= pixels.length) { @@ -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 { @@ -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 @@ -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) @@ -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) @@ -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 } diff --git a/qoi/unannotated/encoder.scala b/qoi/unannotated/encoder.scala index b4b9f7b1..81439c7a 100644 --- a/qoi/unannotated/encoder.scala +++ b/qoi/unannotated/encoder.scala @@ -2,7 +2,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) { def maxSize: Long = w * h * (chan + 1) + HeaderSize + Padding def pxEnd: Long = pixels.length - chan @@ -10,9 +10,7 @@ object encoder { 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) @@ -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) @@ -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)) @@ -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 @@ -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 @@ -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 diff --git a/qoi/verified/README.md b/qoi/verified/README.md new file mode 100644 index 00000000..929e7f42 --- /dev/null +++ b/qoi/verified/README.md @@ -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