From 32707650ef2657aeb1a8e7ad75afc5377f76e265 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 23 Aug 2024 16:57:09 +0200 Subject: [PATCH 1/5] rename checkByteArrayBitContent to byteArrayBitContentSame --- .../scala/asn1scala/asn1jvm_Bitstream.scala | 23 ++++++++++--------- asn1scala/stainless.conf | 6 ++--- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index 325c68805..b3fdd64e1 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala @@ -1096,7 +1096,7 @@ case class BitStream private [asn1scala]( bGot == bit && r2Got == this && r2Got.bitIndex == this.bitIndex - // && checkByteArrayBitContent(Array(b.toUByte), vGot, bitNr, 0 , 1) + // && byteArrayBitContentSame(Array(b.toUByte), vGot, bitNr, 0 , 1) } ) @@ -1466,7 +1466,7 @@ case class BitStream private [asn1scala]( val (r1, r2) = reader(beforeAppend, this) val vGot = r1.readBits(to - i) assert(to - i == 0) - check(checkByteArrayBitContent(srcBuffer, vGot, i, 0, to - i)) + check(byteArrayBitContentSame(srcBuffer, vGot, i, 0, to - i)) }) }.ensuring( _ => @@ -1528,8 +1528,8 @@ case class BitStream private [asn1scala]( val (readerrr, _) = reader(w1, w2) assert(bitStreamReadBitsIntoList(readerrr, nBits) == byteArrayBitContentToList(srcBuffer, from, nBits)) // Should work - lemmaSameBitContentListThenCheckByteArrayBitContent(srcBuffer, vGot, from, 0, nBits) - assert(checkByteArrayBitContent(srcBuffer, vGot, from, 0, nBits) ) + lemmaSameBitContentListThenbyteArrayBitContentSame(srcBuffer, vGot, from, 0, nBits) + assert(byteArrayBitContentSame(srcBuffer, vGot, from, 0, nBits) ) }) }.ensuring(_ => @@ -1538,7 +1538,8 @@ case class BitStream private [asn1scala]( srcBuffer == old(srcBuffer) &&& BitStream.invariant(currentBit, currentByte, buf.length) &&& w1.buf.length == w2.buf.length - &&& BitStream.bitIndex(w2.buf.length, w2.currentByte, w2.currentBit) == BitStream.bitIndex(w1.buf.length, w1.currentByte, w1.currentBit) + nBits + &&& BitStream.bitIndex(w2.buf.length, w2.currentByte, w2.currentBit) == + BitStream.bitIndex(w1.buf.length, w1.currentByte, w1.currentBit) + nBits &&& w1.isPrefixOf(w2) &&& { @@ -1546,7 +1547,7 @@ case class BitStream private [asn1scala]( validateOffsetBitsContentIrrelevancyLemma(w1, w2.buf, nBits) val vGot = r1.readBits(nBits) - checkByteArrayBitContent(srcBuffer, vGot, from, 0, nBits) + byteArrayBitContentSame(srcBuffer, vGot, from, 0, nBits) } ) @@ -1634,7 +1635,7 @@ case class BitStream private [asn1scala]( */ @ghost @pure - def checkByteArrayBitContent(arr1: Array[UByte], arr2: Array[UByte], from1: Long, from2: Long, nBits: Long): Boolean = { + def byteArrayBitContentSame(arr1: Array[UByte], arr2: Array[UByte], from1: Long, from2: Long, nBits: Long): Boolean = { require(from1 >= 0) require(from2 >= 0) require(nBits >= 0) @@ -1657,13 +1658,13 @@ case class BitStream private [asn1scala]( if b1 != b2 then false else - checkByteArrayBitContent(arr1, arr2, from1 + 1, from2 + 1, nBits - 1) + byteArrayBitContentSame(arr1, arr2, from1 + 1, from2 + 1, nBits - 1) } @opaque @ghost @pure - def lemmaSameBitContentListThenCheckByteArrayBitContent(arr1: Array[UByte], arr2: Array[UByte], fromArr1: Long, fromArr2: Long, nBits: Long): Unit = { + def lemmaSameBitContentListThenbyteArrayBitContentSame(arr1: Array[UByte], arr2: Array[UByte], fromArr1: Long, fromArr2: Long, nBits: Long): Unit = { require(fromArr1 >= 0) require(fromArr2 >= 0) require(nBits >= 0) @@ -1675,8 +1676,8 @@ case class BitStream private [asn1scala]( decreases(nBits) if nBits > 0 then - lemmaSameBitContentListThenCheckByteArrayBitContent(arr1, arr2, fromArr1 + 1, fromArr2 + 1, nBits - 1) - } ensuring(_ => checkByteArrayBitContent(arr1, arr2, fromArr1, fromArr2, nBits)) + lemmaSameBitContentListThenbyteArrayBitContentSame(arr1, arr2, fromArr1 + 1, fromArr2 + 1, nBits - 1) + } ensuring(_ => byteArrayBitContentSame(arr1, arr2, fromArr1, fromArr2, nBits)) diff --git a/asn1scala/stainless.conf b/asn1scala/stainless.conf index 1910527d6..b0919113d 100644 --- a/asn1scala/stainless.conf +++ b/asn1scala/stainless.conf @@ -1,8 +1,8 @@ # The settings below correspond to the various # options listed by `stainless --help` -vc-cache = false -debug = ["smt"] +vc-cache = true +# debug = ["smt"] timeout = 1200 check-models = false print-ids = false @@ -13,4 +13,4 @@ solvers = "smt-cvc5,smt-z3,smt-cvc4" check-measures = yes infer-measures = true simplifier = "ol" -no-colors = true +no-colors = false From 4c2482d6b9044e8ac6a7616263c7e4148080a2e2 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 23 Aug 2024 17:00:52 +0200 Subject: [PATCH 2/5] rename 2 functions of bistream --- .../scala/asn1scala/asn1jvm_Bitstream.scala | 104 +++++++++--------- .../main/scala/asn1scala/asn1jvm_Codec.scala | 26 ++--- .../scala/asn1scala/asn1jvm_Codec_ACN.scala | 18 +-- 3 files changed, 74 insertions(+), 74 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index b3fdd64e1..14df5f2d8 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala @@ -334,17 +334,17 @@ object BitStream { // TODO: "loopPrefixLemma" is a bad name, it's not the same "prefix lemma" as the others!!! @ghost @pure @opaque @inlineOnce - def readNLeastSignificantBitsLoopPrefixLemma(bs: BitStream, nBits: Int, i: Int, acc: Long): Unit = { + def readNLSBBitsMSBFirstLoopPrefixLemma(bs: BitStream, nBits: Int, i: Int, acc: Long): Unit = { require(0 <= i && i < nBits && nBits <= 64) require(BitStream.validate_offset_bits(bs.buf.length.toLong, bs.currentByte.toLong, bs.currentBit.toLong, nBits - i)) require((acc & onesLSBLong(nBits - i)) == 0L) require((acc & onesLSBLong(nBits)) == acc) decreases(nBits - i) - val (bsFinal, vGot1) = bs.readNLeastSignificantBitsLoopPure(nBits, i, acc) + val (bsFinal, vGot1) = bs.readNLSBBitsMSBFirstLoopPure(nBits, i, acc) val readBit = bs.readBitPure()._2 val bs2 = bs.withMovedBitIndex(1) val newAcc = acc | (if readBit then 1L << (nBits - 1 - i) else 0) - val (bs2Final, vGot2) = bs2.readNLeastSignificantBitsLoopPure(nBits, i + 1, newAcc) + val (bs2Final, vGot2) = bs2.readNLSBBitsMSBFirstLoopPure(nBits, i + 1, newAcc) { () @@ -354,7 +354,7 @@ object BitStream { } @ghost @pure @opaque @inlineOnce - def readNLeastSignificantBitsLoopPrefixLemma2(bs1: BitStream, bs2: BitStream, nBits: Int, i: Int, acc: Long): Unit = { + def readNLSBBitsMSBFirstLoopPrefixLemma2(bs1: BitStream, bs2: BitStream, nBits: Int, i: Int, acc: Long): Unit = { require(bs1.buf.length == bs2.buf.length) require(0 <= i && i < nBits && nBits <= 64) require(BitStream.validate_offset_bits(bs1.buf.length.toLong, bs1.currentByte.toLong, bs1.currentBit.toLong, nBits - i)) @@ -369,8 +369,8 @@ object BitStream { decreases(nBits - i) val bs2Reset = bs2.resetAt(bs1) - val (bsFinal1, vGot1) = bs1.readNLeastSignificantBitsLoopPure(nBits, i, acc) - val (bsFinal2, vGot2) = bs2Reset.readNLeastSignificantBitsLoopPure(nBits, i, acc) + val (bsFinal1, vGot1) = bs1.readNLSBBitsMSBFirstLoopPure(nBits, i, acc) + val (bsFinal2, vGot2) = bs2Reset.readNLSBBitsMSBFirstLoopPure(nBits, i, acc) { val (bs1Rec, gotB1) = bs1.readBitPure() @@ -385,9 +385,9 @@ object BitStream { val accRec = acc | (if gotB1 then 1L << (nBits - 1 - i) else 0) assert(BitStream.bitIndex(bs1Rec.buf.length, bs1Rec.currentByte, bs1Rec.currentBit ) == BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + 1) validateOffsetBitsContentIrrelevancyLemma(bs1, bs1Rec.buf, 1) - readNLeastSignificantBitsLoopPrefixLemma2(bs1Rec, bs2Rec, nBits, i + 1, accRec) - val (_, vRecGot1) = bs1Rec.readNLeastSignificantBitsLoopPure(nBits, i + 1, accRec) - val (_, vRecGot2) = bs2Rec.readNLeastSignificantBitsLoopPure(nBits, i + 1, accRec) + readNLSBBitsMSBFirstLoopPrefixLemma2(bs1Rec, bs2Rec, nBits, i + 1, accRec) + val (_, vRecGot1) = bs1Rec.readNLSBBitsMSBFirstLoopPure(nBits, i + 1, accRec) + val (_, vRecGot2) = bs2Rec.readNLSBBitsMSBFirstLoopPure(nBits, i + 1, accRec) assert(vRecGot1 == vRecGot2) assert(vGot1 == vRecGot1) assert(vGot2 == vRecGot2) @@ -401,7 +401,7 @@ object BitStream { } @ghost @pure @opaque @inlineOnce - def readNLeastSignificantBitsPrefixLemma(bs1: BitStream, bs2: BitStream, nBits: Int): Unit = { + def readNLSBBitsMSBFirstPrefixLemma(bs1: BitStream, bs2: BitStream, nBits: Int): Unit = { require(bs1.buf.length == bs2.buf.length) require(0 <= nBits && nBits <= 64) require(BitStream.validate_offset_bits(bs1.buf.length.toLong, bs1.currentByte.toLong, bs1.currentBit.toLong, nBits)) @@ -413,19 +413,19 @@ object BitStream { )) val bs2Reset = bs2.resetAt(bs1) - val (bsFinal1, vGot1) = bs1.readNLeastSignificantBitsPure(nBits) - val (bsFinal2, vGot2) = bs2Reset.readNLeastSignificantBitsPure(nBits) + val (bsFinal1, vGot1) = bs1.readNLSBBitsMSBFirstPure(nBits) + val (bsFinal2, vGot2) = bs2Reset.readNLSBBitsMSBFirstPure(nBits) { if (nBits > 0) - readNLeastSignificantBitsLoopPrefixLemma2(bs1, bs2, nBits, 0, 0) + readNLSBBitsMSBFirstLoopPrefixLemma2(bs1, bs2, nBits, 0, 0) }.ensuring { _ => vGot1 == vGot2 && BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit ) } } @ghost @pure @opaque @inlineOnce - def readNLeastSignificantBitsLoopNextLemma(bs: BitStream, nBits: Int, i: Int, acc1: Long): Unit = { + def readNLSBBitsMSBFirstLoopNextLemma(bs: BitStream, nBits: Int, i: Int, acc1: Long): Unit = { require(0 <= i && i < nBits && nBits <= 64) require(1 <= nBits) require(BitStream.validate_offset_bits(bs.buf.length.toLong, bs.currentByte.toLong, bs.currentBit.toLong, nBits - i)) @@ -433,22 +433,22 @@ object BitStream { require((acc1 & onesLSBLong(nBits)) == acc1) decreases(nBits - i) - val (bsFinal1, vGot1) = bs.readNLeastSignificantBitsLoopPure(nBits, i, acc1) + val (bsFinal1, vGot1) = bs.readNLSBBitsMSBFirstLoopPure(nBits, i, acc1) val (bs2, bit) = bs.readBitPure() val mask = if bit then 1L << (nBits - 1 - i) else 0 val acc2 = (acc1 | mask) & onesLSBLong(nBits - 1) - val (bsFinal2, vGot2) = bs2.readNLeastSignificantBitsLoopPure(nBits - 1, i, acc2) + val (bsFinal2, vGot2) = bs2.readNLSBBitsMSBFirstLoopPure(nBits - 1, i, acc2) { if (i >= nBits - 2) () else { val acc1Rec = acc1 | mask - readNLeastSignificantBitsLoopNextLemma(bs2, nBits, i + 1, acc1Rec) - val (bsFinal1Rec, vGot1Rec) = bs2.readNLeastSignificantBitsLoopPure(nBits, i + 1, acc1Rec) + readNLSBBitsMSBFirstLoopNextLemma(bs2, nBits, i + 1, acc1Rec) + val (bsFinal1Rec, vGot1Rec) = bs2.readNLSBBitsMSBFirstLoopPure(nBits, i + 1, acc1Rec) val (bs2Rec, bitRec) = bs2.readBitPure() val maskRec = if bitRec then 1L << (nBits - 2 - i) else 0 val acc2Rec = (acc1Rec | maskRec) & onesLSBLong(nBits - 1) - val (bsFinal2Rec, vGot2Rec) = bs2Rec.readNLeastSignificantBitsLoopPure(nBits - 1, i + 1, acc2Rec) + val (bsFinal2Rec, vGot2Rec) = bs2Rec.readNLSBBitsMSBFirstLoopPure(nBits - 1, i + 1, acc2Rec) assert((vGot1Rec & onesLSBLong(nBits - 1)) == vGot2Rec) assert(bsFinal1Rec == bsFinal2Rec) @@ -467,49 +467,49 @@ object BitStream { } @ghost @pure @opaque @inlineOnce - def readNLeastSignificantBitsLeadingZerosLemma(bs: BitStream, nBits: Int, leadingZeros: Int): Unit = { + def readNLSBBitsMSBFirstLeadingZerosLemma(bs: BitStream, nBits: Int, leadingZeros: Int): Unit = { require(0 <= leadingZeros && leadingZeros <= nBits && nBits <= 64) require(BitStream.validate_offset_bits(bs.buf.length.toLong, bs.currentByte.toLong, bs.currentBit.toLong, nBits)) - require(bs.readNLeastSignificantBitsPure(leadingZeros)._2 == 0L) + require(bs.readNLSBBitsMSBFirstPure(leadingZeros)._2 == 0L) decreases(leadingZeros) - val (bsFinal1, vGot1) = bs.readNLeastSignificantBitsPure(nBits) - val (bsFinal2, vGot2) = bs.withMovedBitIndex(leadingZeros).readNLeastSignificantBitsPure(nBits - leadingZeros) + val (bsFinal1, vGot1) = bs.readNLSBBitsMSBFirstPure(nBits) + val (bsFinal2, vGot2) = bs.withMovedBitIndex(leadingZeros).readNLSBBitsMSBFirstPure(nBits - leadingZeros) { - readNLeastSignificantBitsLeadingBitsLemma(bs, false, nBits, leadingZeros) + readNLSBBitsMSBFirstLeadingBitsLemma(bs, false, nBits, leadingZeros) }.ensuring { _ => vGot1 == vGot2 && bsFinal1 == bsFinal2 } } @ghost @pure @opaque @inlineOnce - def readNLeastSignificantBitsLeadingBitsLemma(bs: BitStream, bit: Boolean, nBits: Int, leadingBits: Int): Unit = { + def readNLSBBitsMSBFirstLeadingBitsLemma(bs: BitStream, bit: Boolean, nBits: Int, leadingBits: Int): Unit = { require(0 <= leadingBits && leadingBits <= nBits && nBits <= 64) require(BitStream.validate_offset_bits(bs.buf.length.toLong, bs.currentByte.toLong, bs.currentBit.toLong, nBits)) - require(bs.readNLeastSignificantBitsPure(leadingBits)._2 == bitLSBLong(bit, leadingBits)) + require(bs.readNLSBBitsMSBFirstPure(leadingBits)._2 == bitLSBLong(bit, leadingBits)) decreases(leadingBits) - val (bsFinal1, vGot1) = bs.readNLeastSignificantBitsPure(nBits) - val (bsFinal2, vGot2) = bs.withMovedBitIndex(leadingBits).readNLeastSignificantBitsPure(nBits - leadingBits) + val (bsFinal1, vGot1) = bs.readNLSBBitsMSBFirstPure(nBits) + val (bsFinal2, vGot2) = bs.withMovedBitIndex(leadingBits).readNLSBBitsMSBFirstPure(nBits - leadingBits) { if (leadingBits == 0) () else { val (bsRec, gotBit) = bs.readBitPure() assert(gotBit == bit) - readNLeastSignificantBitsLoopNextLemma(bs, leadingBits, 0, 0L) - readNLeastSignificantBitsLeadingBitsLemma(bsRec, bit, nBits - 1, leadingBits - 1) + readNLSBBitsMSBFirstLoopNextLemma(bs, leadingBits, 0, 0L) + readNLSBBitsMSBFirstLeadingBitsLemma(bsRec, bit, nBits - 1, leadingBits - 1) eqBufAndBitIndexImpliesEq(bs.withMovedBitIndex(leadingBits), bsRec.withMovedBitIndex(leadingBits - 1)) - val (bsFinal1Rec, vGot1Rec) = bsRec.readNLeastSignificantBitsPure(nBits - 1) - val (bsFinal2Rec, vGot2Rec) = bsRec.withMovedBitIndex(leadingBits - 1).readNLeastSignificantBitsPure(nBits - leadingBits) + val (bsFinal1Rec, vGot1Rec) = bsRec.readNLSBBitsMSBFirstPure(nBits - 1) + val (bsFinal2Rec, vGot2Rec) = bsRec.withMovedBitIndex(leadingBits - 1).readNLSBBitsMSBFirstPure(nBits - leadingBits) assert(bsFinal1Rec == bsFinal2Rec) assert(vGot1Rec == ((bitLSBLong(bit, leadingBits - 1) << (nBits - leadingBits)) | vGot2Rec)) assert(bsFinal2 == bsFinal2Rec) assert(vGot2 == vGot2Rec) - readNLeastSignificantBitsLoopNextLemma(bs, nBits, 0, 0L) + readNLSBBitsMSBFirstLoopNextLemma(bs, nBits, 0, 0L) assert(bsFinal1Rec == bsFinal1) assert(vGot1 == (vGot1Rec | (if (bit) 1L << (nBits - 1) else 0L))) check(vGot1 == ((bitLSBLong(bit, leadingBits) << (nBits - leadingBits)) | vGot2)) @@ -529,7 +529,7 @@ object BitStream { // val (bs1Final, ok) = bs.checkBitsLoopPure(nBits, bit, from) // require(ok) // val acc = if (bit) onesLSBLong(from) << (nBits - from) else 0 - // val (bs2Final, vGot) = bs.readNLeastSignificantBitsLoopPure(nBits, from, acc) + // val (bs2Final, vGot) = bs.readNLSBBitsMSBFirstLoopPure(nBits, from, acc) // { // if (from == nBits) () @@ -1289,11 +1289,11 @@ case class BitStream private [asn1scala]( * After bit 24, bit 23 and so on get added * */ - def appendNLeastSignificantBits(v: Long, nBits: Int): Unit = { + def appendLSBBitsMSBFirst(v: Long, nBits: Int): Unit = { require(nBits >= 0 && nBits <= NO_OF_BITS_IN_LONG) require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits)) require((v & onesLSBLong(nBits)) == v) - appendNLeastSignificantBitsLoop(v, nBits, 0) + appendLSBBitsMSBFirstLoop(v, nBits, 0) }.ensuring { _ => val w1 = old(this) val w2 = this @@ -1301,12 +1301,12 @@ case class BitStream private [asn1scala]( && w1.isPrefixOf(w2) && { val (r1, r2) = reader(w1, w2) validateOffsetBitsContentIrrelevancyLemma(w1, w2.buf, nBits) - val (r2Got, vGot) = r1.readNLeastSignificantBitsPure(nBits) + val (r2Got, vGot) = r1.readNLSBBitsMSBFirstPure(nBits) vGot == v && r2Got == r2 } } - def appendNLeastSignificantBitsLoop(v: Long, nBits: Int, i: Int): Unit = { + def appendLSBBitsMSBFirstLoop(v: Long, nBits: Int, i: Int): Unit = { require(0 <= i && i <= nBits && nBits <= 64) require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits - i)) require((v & onesLSBLong(nBits)) == v) @@ -1317,7 +1317,7 @@ case class BitStream private [asn1scala]( @ghost val oldThis1 = snapshot(this) appendBit(b) @ghost val oldThis2 = snapshot(this) - appendNLeastSignificantBitsLoop(v, nBits, i + 1) + appendLSBBitsMSBFirstLoop(v, nBits, i + 1) ghostExpr { lemmaIsPrefixTransitive(oldThis1, oldThis2, this) @@ -1330,15 +1330,15 @@ case class BitStream private [asn1scala]( val zeroed = v & ~onesLSBLong(nBits - i) validateOffsetBitsContentIrrelevancyLemma(oldThis1, this.buf, nBits - i) - val (r3Got_13, resGot_13) = r1_13.readNLeastSignificantBitsLoopPure(nBits, i, zeroed) + val (r3Got_13, resGot_13) = r1_13.readNLSBBitsMSBFirstLoopPure(nBits, i, zeroed) val upd = zeroed | (if bitGot then 1L << (nBits - 1 - i) else 0) validateOffsetBitsContentIrrelevancyLemma(oldThis2, this.buf, nBits - i - 1) - val (r3Got_23, resGot_23) = r2_23.readNLeastSignificantBitsLoopPure(nBits, i + 1, upd) + val (r3Got_23, resGot_23) = r2_23.readNLSBBitsMSBFirstLoopPure(nBits, i + 1, upd) assert(r3Got_23 == r3_23) - readNLeastSignificantBitsLoopPrefixLemma(r1_13, nBits, i, zeroed) + readNLSBBitsMSBFirstLoopPrefixLemma(r1_13, nBits, i, zeroed) check(r1_13 == r3_13.withMovedBitIndex(BitStream.bitIndex(oldThis1.buf.length, oldThis1.currentByte, oldThis1.currentBit) - BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit) )) check(r2_23 == r3_23.withMovedBitIndex(BitStream.bitIndex(oldThis2.buf.length, oldThis2.currentByte, oldThis2.currentBit) - BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit) )) @@ -1362,7 +1362,7 @@ case class BitStream private [asn1scala]( val (r1, r2) = reader(w1, w2) val zeroed = v & ~onesLSBLong(nBits - i) validateOffsetBitsContentIrrelevancyLemma(w1, w2.buf, nBits - i) - val (r2Got, vGot) = r1.readNLeastSignificantBitsLoopPure(nBits, i, zeroed) + val (r2Got, vGot) = r1.readNLSBBitsMSBFirstLoopPure(nBits, i, zeroed) vGot == v && r2Got == r2 } } @@ -2206,29 +2206,29 @@ case class BitStream private [asn1scala]( } /** - * Counter Operation to appendNLeastSignificantBits + * Counter Operation to appendLSBBitsMSBFirst * @param nBits number of bits to read [0-64] * @return value that holds nBits from bitstream * * Remarks: * The last bit from the bitstream will get written into the LSB */ - def readNLeastSignificantBits(nBits: Int): Long = { + def readNLSBBitsMSBFirst(nBits: Int): Long = { require(nBits >= 0 && nBits <= 64) require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits)) - readNLeastSignificantBitsLoop(nBits, 0, 0L) + readNLSBBitsMSBFirstLoop(nBits, 0, 0L) }.ensuring(_ => buf == old(this).buf && BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit) == BitStream.bitIndex(old(this).buf.length, old(this).currentByte, old(this).currentBit) + nBits) @ghost @pure - def readNLeastSignificantBitsPure(nBits: Int): (BitStream, Long) = { + def readNLSBBitsMSBFirstPure(nBits: Int): (BitStream, Long) = { require(nBits >= 0 && nBits <= 64) require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits)) val cpy = snapshot(this) - val res = cpy.readNLeastSignificantBits(nBits) + val res = cpy.readNLSBBitsMSBFirst(nBits) (cpy, res) } - def readNLeastSignificantBitsLoop(nBits: Int, i: Int, acc: Long): Long = { + def readNLSBBitsMSBFirstLoop(nBits: Int, i: Int, acc: Long): Long = { require(0 <= i && i <= nBits && nBits <= 64) require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits - i)) require((acc & onesLSBLong(nBits - i)) == 0L) // The nBits - i LSBs must be 0 @@ -2239,7 +2239,7 @@ case class BitStream private [asn1scala]( } else { val bit = readBit() val newAcc = acc | (if bit then 1L << (nBits - 1 - i) else 0) - readNLeastSignificantBitsLoop(nBits, i + 1, newAcc) + readNLSBBitsMSBFirstLoop(nBits, i + 1, newAcc) } }.ensuring { res => buf == old(this).buf && @@ -2250,13 +2250,13 @@ case class BitStream private [asn1scala]( } @ghost @pure - def readNLeastSignificantBitsLoopPure(nBits: Int, i: Int, acc: Long): (BitStream, Long) = { + def readNLSBBitsMSBFirstLoopPure(nBits: Int, i: Int, acc: Long): (BitStream, Long) = { require(0 <= i && i <= nBits && nBits <= 64) require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits - i)) require((acc & onesLSBLong(nBits - i)) == 0L) // The nBits - i LSBs must be 0 require((acc & onesLSBLong(nBits)) == acc) val cpy = snapshot(this) - val res = cpy.readNLeastSignificantBitsLoop(nBits, i, acc) + val res = cpy.readNLSBBitsMSBFirstLoop(nBits, i, acc) (cpy, res) } diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala index a68eca4e6..3adb97ce5 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala @@ -111,7 +111,7 @@ object Codec { val (c1_2, nBytes1) = c1.bitStream.readBytePure() val (c2_2, nBytes2) = c2Reset.bitStream.readBytePure() assert(nBytes1 == nBytes2) - readNLeastSignificantBitsPrefixLemma(c1_2, c2_2, nBytes1.unsignedToInt * 8) + readNLSBBitsMSBFirstPrefixLemma(c1_2, c2_2, nBytes1.unsignedToInt * 8) }.ensuring { _ => l1 == l2 && BitStream.bitIndex(c1Res.bitStream.buf.length, c1Res.bitStream.currentByte, c1Res.bitStream.currentBit) == BitStream.bitIndex(c2Res.bitStream.buf.length, c2Res.bitStream.currentByte, c2Res.bitStream.currentBit) } @@ -135,7 +135,7 @@ object Codec { val (c2Res, l2) = c2Reset.decodeConstrainedPosWholeNumberPure(min, max) { - readNLeastSignificantBitsPrefixLemma(c1.bitStream, c2.bitStream, nBits) + readNLSBBitsMSBFirstPrefixLemma(c1.bitStream, c2.bitStream, nBits) }.ensuring { _ => l1 == l2 && BitStream.bitIndex(c1Res.bitStream.buf.length, c1Res.bitStream.currentByte, c1Res.bitStream.currentBit) == BitStream.bitIndex(c2Res.bitStream.buf.length, c2Res.bitStream.currentByte, c2Res.bitStream.currentBit) } @@ -196,7 +196,7 @@ case class Codec(bitStream: BitStream) { @opaque @inlineOnce def encodeUnsignedInteger(v: ULong): Unit = { require(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,GetBitCountUnsigned(v))) - appendNLeastSignificantBits(v.toRaw, GetBitCountUnsigned(v)) + appendLSBBitsMSBFirst(v.toRaw, GetBitCountUnsigned(v)) } .ensuring { _ => val w1 = old(this) val w2 = this @@ -221,7 +221,7 @@ case class Codec(bitStream: BitStream) { require(nBits >= 0 && nBits <= NO_OF_BITS_IN_LONG) require(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nBits)) - ULong.fromRaw(readNLeastSignificantBits(nBits)) + ULong.fromRaw(readNLSBBitsMSBFirst(nBits)) }.ensuring(_ => buf == old(this).buf && BitStream.bitIndex(this.bitStream.buf.length, this.bitStream.currentByte, this.bitStream.currentBit) == BitStream.bitIndex(old(this).bitStream.buf.length, old(this).bitStream.currentByte, old(this).bitStream.currentBit) + nBits) @ghost @pure @@ -264,7 +264,7 @@ case class Codec(bitStream: BitStream) { @ghost val nEncValBits = GetBitCountUnsigned(encVal) - appendNLeastSignificantBits(encVal, nRangeBits) + appendLSBBitsMSBFirst(encVal, nRangeBits) else ghostExpr { lemmaIsPrefixRefl(bitStream) @@ -355,7 +355,7 @@ case class Codec(bitStream: BitStream) { //SAMassert(nRangeBits >= nEncValBits) //SAMassert(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nRangeBits)) - appendNLeastSignificantBits(encVal, nRangeBits) + appendLSBBitsMSBFirst(encVal, nRangeBits) // else // ghostExpr { // lemmaIsPrefixRefl(bitStream) @@ -408,7 +408,7 @@ case class Codec(bitStream: BitStream) { else val nRangeBits = GetBitCountUnsigned(range.toRawULong) assert(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nRangeBits)) - val decVal = readNLeastSignificantBits(nRangeBits) + val decVal = readNLSBBitsMSBFirst(nRangeBits) // assert(min + decVal <= max) // TODO: Invalid @@ -507,7 +507,7 @@ case class Codec(bitStream: BitStream) { // encode length appendByte(nBytes.toRawUByte) // encode value - appendNLeastSignificantBits(encV.toRaw, nBytes * NO_OF_BITS_IN_BYTE) + appendLSBBitsMSBFirst(encV.toRaw, nBytes * NO_OF_BITS_IN_BYTE) }.ensuring(_ => buf.length == old(this).buf.length && BitStream.bitIndex(this.bitStream.buf.length, this.bitStream.currentByte, this.bitStream.currentBit) == BitStream.bitIndex(old(this).bitStream.buf.length, old(this).bitStream.currentByte, old(this).bitStream.currentBit) + GetLengthForEncodingUnsigned(stainless.math.wrapping(v - min).toRawULong) * 8L + 8L) @@ -536,7 +536,7 @@ case class Codec(bitStream: BitStream) { val v: ULong = if(!(nBits >= 0 && nBits <= 64) || !BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, nBits)){ 0L.toRawULong } else { - readNLeastSignificantBits(nBits).toRawULong + readNLSBBitsMSBFirst(nBits).toRawULong } // SAM: here the post condition should be obvious, as ULong are always positive. But we can have @@ -569,7 +569,7 @@ case class Codec(bitStream: BitStream) { /* encode length */ appendByte(nBytes.toRawUByte) /* encode number */ - appendNLeastSignificantBits(encV, nBytes * NO_OF_BITS_IN_BYTE) + appendLSBBitsMSBFirst(encV, nBytes * NO_OF_BITS_IN_BYTE) } /** @@ -593,7 +593,7 @@ case class Codec(bitStream: BitStream) { val v = if(!(nBits >= 0 && nBits <= 64) || !BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, nBits)){ 0L.toRawULong } else { - readNLeastSignificantBits(nBits).toRawULong + readNLSBBitsMSBFirst(nBits).toRawULong } val res: ULong = ULong.fromRaw(v + min) // For some reasons, the scala compiler chokes on this being returned res @@ -625,7 +625,7 @@ case class Codec(bitStream: BitStream) { @ghost val this2 = snapshot(this) // encode number - appendNLeastSignificantBits(v & onesLSBLong(nBits), nBits) + appendLSBBitsMSBFirst(v & onesLSBLong(nBits), nBits) /* ghostExpr { validTransitiveLemma(this1.bitStream, this2.bitStream, this.bitStream) @@ -675,7 +675,7 @@ case class Codec(bitStream: BitStream) { // check bitstream precondition //SAM assert(BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nBytes)) //SAM assert(0 <= nBytes && nBytes <= 8) - val read = readNLeastSignificantBits(nBits) + val read = readNLSBBitsMSBFirst(nBits) val res = if (read == 0 || nBits == 0 || nBits == 64 || (read & (1L << (nBits - 1))) == 0L) read else onesMSBLong(64 - nBits) | read // Sign extension diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala index 356335299..3cb66f74a 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala @@ -264,15 +264,15 @@ case class ACN(base: Codec) { validateOffsetImpliesMoveBits(r1_1.base.bitStream, diff) assert(r2_2 == r1_1.withMovedBitIndex(diff)) // TODO: Exported symbol not working - // val (r2Got_2, vGot_2) = r2_2.readNLeastSignificantBitsLoopPure(nBits, 0, 0L) - val (r2Got_2, vGot_2) = r2_2.base.bitStream.readNLeastSignificantBitsLoopPure(nBits, 0, 0L) + // val (r2Got_2, vGot_2) = r2_2.readNLSBBitsMSBFirstLoopPure(nBits, 0, 0L) + val (r2Got_2, vGot_2) = r2_2.base.bitStream.readNLSBBitsMSBFirstLoopPure(nBits, 0, 0L) assert(vGot_2 == intVal.toRaw) - val (r3Got_3, vGot_3) = r1_1.base.bitStream.readNLeastSignificantBitsLoopPure(encodedSizeInBits, 0, 0L) + val (r3Got_3, vGot_3) = r1_1.base.bitStream.readNLSBBitsMSBFirstLoopPure(encodedSizeInBits, 0, 0L) assert(iGot.toRaw == vGot_3) assert(r3Got.base.bitStream == r3Got_3) checkBitsLoopAndReadNLSB(r1_1.base.bitStream, diff, false) - readNLeastSignificantBitsLeadingZerosLemma(r1_1.base.bitStream, encodedSizeInBits, diff) + readNLSBBitsMSBFirstLeadingZerosLemma(r1_1.base.bitStream, encodedSizeInBits, diff) check(iGot == intVal) check(r3Got == r3_1) } else { @@ -693,7 +693,7 @@ case class ACN(base: Codec) { validateOffsetBitsDifferenceLemma(this1.base.bitStream, this.base.bitStream, formatBitLength, addedBits) } // @ghost val this2 = snapshot(this) - appendNLeastSignificantBits(v & onesLSBLong(nBits), nBits) + appendLSBBitsMSBFirst(v & onesLSBLong(nBits), nBits) /*ghostExpr { assert(BitStream.bitIndex(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit) == BitStream.bitIndex(this2.base.bitStream.buf.length, this2.base.bitStream.currentByte, this2.base.bitStream.currentBit) + nBits) assert(BitStream.bitIndex(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit) == BitStream.bitIndex(this1.base.bitStream.buf.length, this1.base.bitStream.currentByte, this1.base.bitStream.currentBit) + formatBitLength) @@ -710,13 +710,13 @@ case class ACN(base: Codec) { assert(r3_1 == r3_2) validateOffsetImpliesMoveBits(r1_1.base.bitStream, addedBits) assert(r2_2 == r1_1.withMovedBitIndex(addedBits)) - val (r2Got_2, vGot_2) = r2_2.base.bitStream.readNLeastSignificantBitsLoopPure(nBits, 0, 0L) + val (r2Got_2, vGot_2) = r2_2.base.bitStream.readNLSBBitsMSBFirstLoopPure(nBits, 0, 0L) assert(vGot_2 == (v & onesLSBLong(nBits))) - val (r3Got_3, vGot_3) = r1_1.base.bitStream.readNLeastSignificantBitsLoopPure(formatBitLength, 0, 0L) + val (r3Got_3, vGot_3) = r1_1.base.bitStream.readNLSBBitsMSBFirstLoopPure(formatBitLength, 0, 0L) checkBitsLoopAndReadNLSB(r1_1.base.bitStream, addedBits, v < 0) - readNLeastSignificantBitsLeadingBitsLemma(r1_1.base.bitStream, v < 0, formatBitLength, addedBits) + readNLSBBitsMSBFirstLeadingBitsLemma(r1_1.base.bitStream, v < 0, formatBitLength, addedBits) assert(vGot == (bitMSBLong(v < 0, NO_OF_BITS_IN_LONG - formatBitLength) | vGot_3)) assert(r3Got.base.bitStream == r3Got_3) assert(((vGot_3 & (1L << (formatBitLength - 1))) == 0L) == v >= 0) @@ -793,7 +793,7 @@ case class ACN(base: Codec) { require(encodedSizeInBits >= 0 && encodedSizeInBits <= NO_OF_BITS_IN_LONG) require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, encodedSizeInBits)) - val res = readNLeastSignificantBits(encodedSizeInBits) + val res = readNLSBBitsMSBFirst(encodedSizeInBits) if encodedSizeInBits == 0 || (res & (1L << (encodedSizeInBits - 1))) == 0L then res else onesMSBLong(NO_OF_BITS_IN_LONG - encodedSizeInBits) | res /* From ae41167454bfccd64c04d6267bf3e360b1b7a9b7 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 23 Aug 2024 17:16:41 +0200 Subject: [PATCH 3/5] renaming --- .../src/main/scala/asn1scala/asn1jvm.scala | 2 +- .../scala/asn1scala/asn1jvm_Bitstream.scala | 14 +++++------ .../main/scala/asn1scala/asn1jvm_Codec.scala | 24 +++++++++---------- .../asn1scala/asn1jvm_Verification.scala | 4 ++-- asn1scala/verify_bitStream.sh | 1 + 5 files changed, 23 insertions(+), 22 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm.scala index 5de9f1bc5..e8ecf8d46 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm.scala @@ -335,7 +335,7 @@ def GetCharIndex(ch: UByte, charSet: Array[UByte]): Int = i += 1 ).invariant(i >= 0 &&& i <= charSet.length && ret < charSet.length && ret >= 0) ret -} ensuring(res => charSet.length == 0 || res >= 0 && res < charSet.length) +}.ensuring(res => charSet.length == 0 || res >= 0 && res < charSet.length) def NullType_Initialize(): NullType = { 0 diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index 14df5f2d8..09c799ff4 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala @@ -106,7 +106,7 @@ object BitStream { lemmaIsPrefixTransitive(r1, w1, w2) lemmaIsPrefixTransitive(r1, w2, r2) (r1, r2) - } ensuring(res => + }.ensuring(res => res._1.isPrefixOf(res._2) && res._1.isPrefixOf(w1) && res._2.isPrefixOf(w2) @@ -840,7 +840,7 @@ case class BitStream private [asn1scala]( def resetAt(b: BitStream): BitStream = { require(b.buf.length == buf.length) BitStream(snapshot(buf), b.currentByte, b.currentBit) - } ensuring(res => invariant(res)) + }.ensuring(res => invariant(res)) // ****************** Append Bit Functions ********************** @@ -1568,7 +1568,7 @@ case class BitStream private [asn1scala]( else val bit = bitStreamSnap.readBit() Cons(bit, bitStreamReadBitsIntoList(bitStreamSnap, nBits - 1)) - } ensuring( res => if(nBits == 0) then res.isEmpty else res.length > 0 ) // we'd like to prove res.length == nBits but it's not possible because of type mismatch + }.ensuring( res => if(nBits == 0) then res.isEmpty else res.length > 0 ) // we'd like to prove res.length == nBits but it's not possible because of type mismatch @ghost @opaque @@ -1593,7 +1593,7 @@ case class BitStream private [asn1scala]( val bitStream1Snap = snapshot(bitStream1) assert(bitStream1.readBitPure()._2 == listBits.head) () - } ensuring(_ => + }.ensuring(_ => bitStreamReadBitsIntoList(bitStream2, nBits - 1) == listBits.tail ) @@ -1677,7 +1677,7 @@ case class BitStream private [asn1scala]( if nBits > 0 then lemmaSameBitContentListThenbyteArrayBitContentSame(arr1, arr2, fromArr1 + 1, fromArr2 + 1, nBits - 1) - } ensuring(_ => byteArrayBitContentSame(arr1, arr2, fromArr1, fromArr2, nBits)) + }.ensuring(_ => byteArrayBitContentSame(arr1, arr2, fromArr1, fromArr2, nBits)) @@ -2038,7 +2038,7 @@ case class BitStream private [asn1scala]( val arr: Array[Byte] = Array.fill(arrLen)(0 : Byte) readBitsLoop(nBits, arr, 0, nBits) UByte.fromArrayRaws(arr) - } ensuring(res => + }.ensuring(res => buf == old(this).buf &&& BitStream.bitIndex(old(this).buf.length, old(this).currentByte, old(this).currentBit) + nBits == BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit) &&& BitStream.invariant(this.currentBit, this.currentByte, this.buf.length) @@ -2106,7 +2106,7 @@ case class BitStream private [asn1scala]( require(BitStream.validate_offset_bits(buf.length.toLong, currentByte.toLong, currentBit.toLong, nBits)) val arr = readBits(nBits) Vector.fromScala(arr.toVector) - } ensuring(res => + }.ensuring(res => buf == old(this).buf && BitStream.bitIndex(old(this).buf.length, old(this).currentByte, old(this).currentBit) + nBits == BitStream.bitIndex(this.buf.length, this.currentByte, this.currentBit) && BitStream.invariant(this.currentBit, this.currentByte, this.buf.length) && res.length == ((nBits + NO_OF_BITS_IN_BYTE - 1) / NO_OF_BITS_IN_BYTE).toInt diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala index 3adb97ce5..ebd73d886 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala @@ -419,7 +419,7 @@ case class Codec(bitStream: BitStream) { min else res - } ensuring( res => + }.ensuring( res => buf == old(this).buf && res >= min && res <= max && BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) && @@ -1348,7 +1348,7 @@ case class Codec(bitStream: BitStream) { ghostExpr(check(nCurOffset1 >= 0 )) ghostExpr(check(nRemainingItemsVar1 <= 0x4000 )) (nRemainingItemsVar1, nCurOffset1) - } ensuring(res => + }.ensuring(res => BitStream.bitIndex(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit ) <= bitIndex + (nRemainingItemsVar1 / 0x4000) * 8 + nRemainingItemsVar1 * 8 - res._1 * 8 && BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, res._1 + 2) && BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) && @@ -1397,7 +1397,7 @@ case class Codec(bitStream: BitStream) { assert(bitIndexAfterRecursive == bitIndexBeforeRecursive + (to - from - 1) * NO_OF_BITS_IN_BYTE) assert(NO_OF_BITS_IN_BYTE + (to - from - 1) * NO_OF_BITS_IN_BYTE == (to - from) * NO_OF_BITS_IN_BYTE) assert(bitIndexAfterRecursive == bitIndexBeforeAppending + NO_OF_BITS_IN_BYTE + (to - from - 1) * NO_OF_BITS_IN_BYTE) - } ensuring(_ => + }.ensuring(_ => val oldBitStream = old(this).bitStream BitStream.bitIndex(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit ) == bitIndex + (to - from) * NO_OF_BITS_IN_BYTE && oldBitStream.buf.length == bitStream.buf.length @@ -1409,14 +1409,14 @@ case class Codec(bitStream: BitStream) { @inlineOnce def lemmaGetBitCountUnsignedFFEqualsEight(): Unit = { - } ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0xFF).toRawULong) == 8) + }.ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0xFF).toRawULong) == 8) @ghost @opaque @inlineOnce def lemmaGetBitCountUnsigned7FFFEquals15(): Unit = { - } ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0x7FFF).toRawULong) == 15) + }.ensuring(_ => GetBitCountUnsigned(stainless.math.wrapping(0x7FFF).toRawULong) == 15) @ghost @opaque @@ -1429,7 +1429,7 @@ case class Codec(bitStream: BitStream) { require(offsetBits == offsetBytes * 8) require(BitStream.validate_offset_bits(bufLength, currentByte, currentBit, offsetBits)) - } ensuring(_ => BitStream.validate_offset_bytes(bufLength, currentByte, currentBit, offsetBytes)) + }.ensuring(_ => BitStream.validate_offset_bytes(bufLength, currentByte, currentBit, offsetBytes)) /** * Takes more than 100sec to verify, that's why it is extracted to a lemma, even though it does not need a specific proof * @@ -1463,7 +1463,7 @@ case class Codec(bitStream: BitStream) { require(bitIndex2 - bitIndex1 <= offset1Bits - offset2Bits) require(BitStream.validate_offset_bits(bufLength, currentByte1, currentBit1, offset1Bits)) - } ensuring(_ => BitStream.validate_offset_bits(bufLength, currentByte2, currentBit2, offset2Bits)) + }.ensuring(_ => BitStream.validate_offset_bits(bufLength, currentByte2, currentBit2, offset2Bits)) /** @@ -1550,7 +1550,7 @@ case class Codec(bitStream: BitStream) { val newArr: Array[UByte] = Array.fill(nLengthTmp1.toInt)(0.toRawUByte) arrayCopyOffsetLen(arr, newArr, 0, 0, newArr.length) newArr - } ensuring(_ => BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length)) + }.ensuring(_ => BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length)) /** @@ -1654,7 +1654,7 @@ case class Codec(bitStream: BitStream) { assert(arr.length == asn1SizeMax.toInt) decodeOctetString_fragmentation_innerWhile(arr, asn1SizeMax, newNCurOffset1) - } ensuring(res => + }.ensuring(res => (res._2 >= 0 && res._2 <= asn1SizeMax || res == (-1L, -1L)) && BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) && old(this).bitStream.buf.length == bitStream.buf.length && @@ -1701,7 +1701,7 @@ case class Codec(bitStream: BitStream) { decodeOctetString_fragmentation_innerMostWhile(arr, asn1SizeMax, from + 1, to) () - } ensuring(_ => + }.ensuring(_ => old(this).buf.length == bitStream.buf.length && arr.length == asn1SizeMax.toInt && BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) && @@ -1887,7 +1887,7 @@ case class Codec(bitStream: BitStream) { assert(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, newRemaingItems + 8*(newRemaingItems / 0x4000) + 16)) encodeBitString_while(arr, nCount, asn1SizeMin, asn1SizeMax, newRemaingItems, newOffset, newBitIndex) - } ensuring (res => + }.ensuring (res => BitStream.invariant(bitStream.currentBit, bitStream.currentByte, bitStream.buf.length) && // BitStream.bitIndex(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit ) <= bitIndex + (nRemainingItemsVar1 / 0x4000) * 8 + nRemainingItemsVar1 - res._1 && BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, res._1 + 16) && @@ -2062,7 +2062,7 @@ case class Codec(bitStream: BitStream) { return (-1L, -1L) decodeBitString_while(asn1SizeMin, asn1SizeMax, newNCurOffset1, arr) - } ensuring (res => + }.ensuring (res => res == (-1L, -1L) || res._1 >= 0 && res._1 <= 0xFF && diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Verification.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Verification.scala index a4bf5780a..50e39ca95 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Verification.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Verification.scala @@ -33,14 +33,14 @@ def arrayCopyOffset[T](@pure src: Array[T], dst: Array[T], fromSrc: Int, toSrc: dst(fromDst) = src(fromSrc) arrayCopyOffset(src, dst, fromSrc + 1, toSrc, fromDst + 1) } -} ensuring ( _ => old(dst).length == dst.length) +}.ensuring ( _ => old(dst).length == dst.length) def arrayCopyOffsetLen[T](@pure src: Array[T], dst: Array[T], fromSrc: Int, fromDst: Int, len: Int): Unit = { require(0 <= len && len <= src.length && len <= dst.length) require(0 <= fromSrc && fromSrc <= src.length - len) require(0 <= fromDst && fromDst <= dst.length - len) arrayCopyOffset(src, dst, fromSrc, fromSrc + len, fromDst) -} ensuring ( _ => old(dst).length == dst.length) +}.ensuring ( _ => old(dst).length == dst.length) @pure def arrayBitIndices(fromBit: Long, toBit: Long): (Int, Int, Int, Int) = { diff --git a/asn1scala/verify_bitStream.sh b/asn1scala/verify_bitStream.sh index 41a81670b..ca58b4383 100755 --- a/asn1scala/verify_bitStream.sh +++ b/asn1scala/verify_bitStream.sh @@ -3,6 +3,7 @@ src/main/scala/asn1scala/asn1jvm.scala \ src/main/scala/asn1scala/asn1jvm_Verification.scala \ src/main/scala/asn1scala/asn1jvm_Helper.scala \ src/main/scala/asn1scala/asn1jvm_Bitstream.scala \ +src/main/scala/asn1scala/asn1jvm_Vector.scala \ --config-file=stainless.conf \ -D-parallel=5 \ $1 From 6a4a0cb9593279ce5c81d5344cafe103d881968e Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 23 Aug 2024 18:12:04 +0200 Subject: [PATCH 4/5] with lemma --- asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala | 2 +- asn1scala/stainless.conf | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index 09c799ff4..11bf44c3e 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala @@ -984,7 +984,7 @@ case class BitStream private [asn1scala]( assert(r3Got_23 == r3_23) - // checkBitsLoopPrefixLemma(r1_13, nBits, bit, from) // not needed but speed up verification + checkBitsLoopPrefixLemma(r1_13, nBits, bit, from) // not needed but speed up verification assert(r2_23 == r1_13.withMovedBitIndex(1)) check(resGot_13 == resGot_23) // timeout check(r3Got_13 == r3_13) diff --git a/asn1scala/stainless.conf b/asn1scala/stainless.conf index b0919113d..eaeb70164 100644 --- a/asn1scala/stainless.conf +++ b/asn1scala/stainless.conf @@ -12,5 +12,5 @@ strict-arithmetic = true solvers = "smt-cvc5,smt-z3,smt-cvc4" check-measures = yes infer-measures = true -simplifier = "ol" +simplifier = "bland" no-colors = false From 497e9b4dc022ed0abbe47430434c75be93ea8283 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 27 Aug 2024 10:01:43 +0200 Subject: [PATCH 5/5] new annotations for proof to pass --- .../scala/asn1scala/asn1jvm_Bitstream.scala | 128 +++++++++--------- 1 file changed, 67 insertions(+), 61 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index 11bf44c3e..695de0620 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala @@ -566,65 +566,65 @@ object BitStream { } } - // @ghost @pure @opaque @inlineOnce - // def checkBitsLoopPrefixLemma2(bs1: BitStream, bs2: BitStream, nBits: Int, expected: Boolean, from: Long): Unit = { - // require(bs1.buf.length == bs2.buf.length) - // require(0 < nBits && nBits <= Int.MaxValue.toLong * NO_OF_BITS_IN_BYTE.toLong) - // require(0 <= from && from < nBits) - // require(BitStream.validate_offset_bits(bs1.buf.length.toLong, bs1.currentByte.toLong, bs1.currentBit.toLong, nBits - from)) - // require(arrayBitRangesEq( - // bs1.buf, - // bs2.buf, - // 0, - // BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + nBits - from - // )) - // decreases(nBits - from) + @ghost @pure @opaque @inlineOnce + def checkBitsLoopPrefixLemma2(bs1: BitStream, bs2: BitStream, nBits: Int, expected: Boolean, from: Long): Unit = { + require(bs1.buf.length == bs2.buf.length) + require(0 < nBits && nBits <= Int.MaxValue.toLong * NO_OF_BITS_IN_BYTE.toLong) + require(0 <= from && from < nBits) + require(BitStream.validate_offset_bits(bs1.buf.length.toLong, bs1.currentByte.toLong, bs1.currentBit.toLong, nBits - from)) + require(arrayBitRangesEq( + bs1.buf, + bs2.buf, + 0, + BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + nBits - from + )) + decreases(nBits - from) - // val bs2Reset = bs2.resetAt(bs1) - // val (bsFinal1, vGot1) = bs1.checkBitsLoopPure(nBits, expected, from) - // val (bsFinal2, vGot2) = bs2Reset.checkBitsLoopPure(nBits, expected, from) + val bs2Reset = bs2.resetAt(bs1) + val (bsFinal1, vGot1) = bs1.checkBitsLoopPure(nBits, expected, from) + val (bsFinal2, vGot2) = bs2Reset.checkBitsLoopPure(nBits, expected, from) - // val bsFinal1PureBitIndex = BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) - // val bsFinal2PureBitIndex = BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit ) + val bsFinal1PureBitIndex = BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) + val bsFinal2PureBitIndex = BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit ) - // { - // val (bs1Rec, gotB1) = bs1.readBitPure() - // val (bs2Rec, gotB2) = bs2Reset.readBitPure() - // arrayBitRangesEqSlicedLemma(bs1.buf, bs2.buf, 0, BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + nBits - from, 0, BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + 1) - // readBitPrefixLemma(bs1, bs2) - // assert(gotB1 == gotB2) - // if (from == nBits - 1) { - // check(vGot1 == vGot2) - // assert(BitStream.invariant(bsFinal1)) - // check(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) - // } else { - // assert(BitStream.invariant(bs1Rec)) - // assert(BitStream.bitIndex(bs1Rec.buf.length, bs1Rec.currentByte, bs1Rec.currentBit ) == BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + 1) - // validateOffsetBitsContentIrrelevancyLemma(bs1, bs1Rec.buf, 1) - // assert(BitStream.invariant(bs1Rec)) - // assert((BitStream.validate_offset_bits(bs1Rec.buf.length.toLong, bs1Rec.currentByte.toLong, bs1Rec.currentBit.toLong, nBits - from - 1))) - // checkBitsLoopPrefixLemma2(bs1Rec, bs2Rec, nBits, expected, from + 1) - - // val (_, vRecGot1) = bs1Rec.checkBitsLoopPure(nBits, expected, from + 1) - // assert((BitStream.validate_offset_bits(bs2Rec.buf.length.toLong, bs2Rec.currentByte.toLong, bs2Rec.currentBit.toLong, nBits - from - 1))) - // val (_, vRecGot2) = bs2Rec.checkBitsLoopPure(nBits, expected, from + 1) - - // assert(vRecGot1 == vRecGot2) - // assert(vGot1 == ((gotB1 == expected) && vRecGot1)) - // assert(vGot2 == ((gotB1 == expected) && vRecGot2)) - - // check(vGot1 == vGot2) - // assert(BitStream.invariant(bsFinal2.currentBit, bsFinal2.currentByte, bsFinal2.buf.length)) - // assert(BitStream.invariant(bsFinal1.currentBit, bsFinal1.currentByte, bsFinal1.buf.length)) - // assert(bsFinal2PureBitIndex == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) - // assert(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == bsFinal1PureBitIndex) - // assert(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) // 200sec!!! - // check(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) - // } - // }.ensuring { _ => - // vGot1 == vGot2 && BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit ) - // } - // } + { + val (bs1Rec, gotB1) = bs1.readBitPure() + val (bs2Rec, gotB2) = bs2Reset.readBitPure() + arrayBitRangesEqSlicedLemma(bs1.buf, bs2.buf, 0, BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + nBits - from, 0, BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + 1) + readBitPrefixLemma(bs1, bs2) + assert(gotB1 == gotB2) + if (from == nBits - 1) { + check(vGot1 == vGot2) + assert(BitStream.invariant(bsFinal1)) + check(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) + } else { + assert(BitStream.invariant(bs1Rec)) + assert(BitStream.bitIndex(bs1Rec.buf.length, bs1Rec.currentByte, bs1Rec.currentBit ) == BitStream.bitIndex(bs1.buf.length, bs1.currentByte, bs1.currentBit ) + 1) + validateOffsetBitsContentIrrelevancyLemma(bs1, bs1Rec.buf, 1) + assert(BitStream.invariant(bs1Rec)) + assert((BitStream.validate_offset_bits(bs1Rec.buf.length.toLong, bs1Rec.currentByte.toLong, bs1Rec.currentBit.toLong, nBits - from - 1))) + checkBitsLoopPrefixLemma2(bs1Rec, bs2Rec, nBits, expected, from + 1) + + val (_, vRecGot1) = bs1Rec.checkBitsLoopPure(nBits, expected, from + 1) + assert((BitStream.validate_offset_bits(bs2Rec.buf.length.toLong, bs2Rec.currentByte.toLong, bs2Rec.currentBit.toLong, nBits - from - 1))) + val (_, vRecGot2) = bs2Rec.checkBitsLoopPure(nBits, expected, from + 1) + + assert(vRecGot1 == vRecGot2) + assert(vGot1 == ((gotB1 == expected) && vRecGot1)) + assert(vGot2 == ((gotB1 == expected) && vRecGot2)) + + check(vGot1 == vGot2) + assert(BitStream.invariant(bsFinal2.currentBit, bsFinal2.currentByte, bsFinal2.buf.length)) + assert(BitStream.invariant(bsFinal1.currentBit, bsFinal1.currentByte, bsFinal1.buf.length)) + assert(bsFinal2PureBitIndex == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) + assert(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == bsFinal1PureBitIndex) + assert(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) // 200sec!!! + check(BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit )) + } + }.ensuring { _ => + vGot1 == vGot2 && BitStream.bitIndex(bsFinal1.buf.length, bsFinal1.currentByte, bsFinal1.currentBit ) == BitStream.bitIndex(bsFinal2.buf.length, bsFinal2.currentByte, bsFinal2.currentBit ) + } + } // @ghost @pure @opaque @inlineOnce // def readByteArrayLoopAnyArraysLemma(bs: BitStream, arr1: Array[UByte], arr2: Array[UByte], from: Int, to: Int): Unit = { @@ -971,11 +971,15 @@ case class BitStream private [asn1scala]( lemmaIsPrefixTransitive(oldThis1, oldThis2, this) readBitPrefixLemma(oldThis2.resetAt(oldThis1), this) + check(BitStream.bitIndex(oldThis2.buf.length, oldThis2.currentByte, oldThis2.currentBit ) == BitStream.bitIndex(oldThis1.buf.length, oldThis1.currentByte, oldThis1.currentBit) + 1) + val (r1_13, r3_13) = reader(oldThis1, this) val (r2_23, r3_23) = reader(oldThis2, this) val (_, bitGot) = r1_13.readBitPure() check(bitGot == bit) + check(r2_23 == r1_13.withMovedBitIndex(1)) + validateOffsetBitsContentIrrelevancyLemma(oldThis1, this.buf, nBits - from) val (r3Got_13, resGot_13) = r1_13.checkBitsLoopPure(nBits, bit, from) @@ -984,10 +988,12 @@ case class BitStream private [asn1scala]( assert(r3Got_23 == r3_23) - checkBitsLoopPrefixLemma(r1_13, nBits, bit, from) // not needed but speed up verification + // checkBitsLoopPrefixLemma(r1_13, nBits, bit, from) // not needed but speed up verification + check(resGot_23) assert(r2_23 == r1_13.withMovedBitIndex(1)) check(resGot_13 == resGot_23) // timeout check(r3Got_13 == r3_13) + check(resGot_13) } @@ -1002,9 +1008,9 @@ case class BitStream private [asn1scala]( val w1 = old(this) val w2 = this w1.buf.length == w2.buf.length - && BitStream.bitIndex(w2.buf.length, w2.currentByte, w2.currentBit) == BitStream.bitIndex(w1.buf.length, w1.currentByte, w1.currentBit) + (nBits - from) - && w1.isPrefixOf(w2) - && { + &&& BitStream.bitIndex(w2.buf.length, w2.currentByte, w2.currentBit) == BitStream.bitIndex(w1.buf.length, w1.currentByte, w1.currentBit) + (nBits - from) + &&& w1.isPrefixOf(w2) + &&& { val (r1, r2) = reader(w1, w2) validateOffsetBitsContentIrrelevancyLemma(w1, w2.buf, nBits - from) val (r2Got, bGot) = r1.checkBitsLoopPure(nBits, bit, from) @@ -2112,7 +2118,7 @@ case class BitStream private [asn1scala]( res.length == ((nBits + NO_OF_BITS_IN_BYTE - 1) / NO_OF_BITS_IN_BYTE).toInt ) - @opaque @inlineOnce + // @opaque @inlineOnce def checkBitsLoop(nBits: Long, expected: Boolean, from: Long): Boolean = { require(0 <= nBits && nBits <= Int.MaxValue.toLong * NO_OF_BITS_IN_BYTE.toLong) require(0 <= from && from <= nBits)