From 790b6cad833e459bfe44857ac17b0f075a9e3521 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 28 Aug 2024 09:45:05 +0200 Subject: [PATCH] prove inverse of encodeUnsignedInteger --- .../scala/asn1scala/asn1jvm_Bitstream.scala | 58 +++++++++---------- .../main/scala/asn1scala/asn1jvm_Codec.scala | 40 ++++++++----- .../scala/asn1scala/asn1jvm_Codec_ACN.scala | 34 +++++------ 3 files changed, 73 insertions(+), 59 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala index 7507a1dc..181089ed 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala @@ -229,15 +229,15 @@ object BitStream { }.ensuring(_ => BitStream.validate_offset_bytes(b2.buf.length.toLong, b2.currentByte.toLong, b2.currentBit.toLong,bytes - ((bits + 7) / 8).toInt)) } - // @ghost @pure @opaque @inlineOnce - // def validateOffsetImpliesMoveBits(b: BitStream, bits: Long): Unit = { - // require(0 <= bits && bits <= b.buf.length.toLong * 8L) - // require(BitStream.validate_offset_bits(b.buf.length.toLong, b.currentByte.toLong, b.currentBit.toLong, bits)) + @ghost @pure @opaque @inlineOnce + def validateOffsetImpliesMoveBits(b: BitStream, bits: Long): Unit = { + require(0 <= bits && bits <= b.buf.length.toLong * 8L) + require(BitStream.validate_offset_bits(b.buf.length.toLong, b.currentByte.toLong, b.currentBit.toLong, bits)) - // { - // () - // }.ensuring(_ => moveBitIndexPrecond(b, bits)) - // } + { + () + }.ensuring(_ => moveBitIndexPrecond(b, bits)) + } // For showing invertibility of encoding - not fully integrated yet @ghost @pure @opaque @inlineOnce @@ -520,28 +520,28 @@ object BitStream { } } - // @ghost @pure @opaque @inlineOnce - // def checkBitsLoopAndReadNLSB(bs: BitStream, nBits: Int, bit: Boolean, from: Int = 0): Unit = { - // require(0 < nBits && nBits <= 64) - // require(0 <= from && from <= nBits) - // require(BitStream.validate_offset_bits(bs.buf.length.toLong, bs.currentByte.toLong, bs.currentBit.toLong, nBits - from)) - // decreases(nBits - from) - // val (bs1Final, ok) = bs.checkBitsLoopPure(nBits, bit, from) - // require(ok) - // val acc = if (bit) onesLSBLong(from) << (nBits - from) else 0 - // val (bs2Final, vGot) = bs.readNLSBBitsMSBFirstLoopPure(nBits, from, acc) + @ghost @pure @opaque @inlineOnce + def checkBitsLoopAndReadNLSB(bs: BitStream, nBits: Int, bit: Boolean, from: Int = 0): Unit = { + require(0 < nBits && nBits <= 64) + require(0 <= from && from <= nBits) + require(BitStream.validate_offset_bits(bs.buf.length.toLong, bs.currentByte.toLong, bs.currentBit.toLong, nBits - from)) + decreases(nBits - from) + val (bs1Final, ok) = bs.checkBitsLoopPure(nBits, bit, from) + require(ok) + val acc = if (bit) onesLSBLong(from) << (nBits - from) else 0 + val (bs2Final, vGot) = bs.readNLSBBitsMSBFirstLoopPure(nBits, from, acc) - // { - // if (from == nBits) () - // else { - // val (bs1Rec, _) = bs.readBitPure() - // checkBitsLoopAndReadNLSB(bs1Rec, nBits, bit, from + 1) - // } - // }.ensuring { _ => - // if (!bit) vGot == 0 - // else vGot == onesLSBLong(nBits) - // } - // } + { + if (from == nBits) () + else { + val (bs1Rec, _) = bs.readBitPure() + checkBitsLoopAndReadNLSB(bs1Rec, nBits, bit, from + 1) + } + }.ensuring { _ => + if (!bit) vGot == 0 + else vGot == onesLSBLong(nBits) + } + } // TODO: Bad name @ghost @pure @opaque @inlineOnce diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala index dcc2d11d..26ecee81 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala @@ -149,8 +149,7 @@ object Codec { */ case class Codec(bitStream: BitStream) { import Codec.* - import BitStream.{reader => _, *} - export bitStream.{resetAt => _, withMovedByteIndex => _, withMovedBitIndex => _, isPrefixOf => _, *} + export bitStream.{resetAt => _, withMovedByteIndex => _, withMovedBitIndex => _, isPrefixOf => _, readNLSBBitsMSBFirstPure => _, *} @ghost @pure @inline def resetAt(other: Codec): Codec = { @@ -160,13 +159,13 @@ case class Codec(bitStream: BitStream) { @ghost @pure @inline def withMovedByteIndex(diffInBytes: Int): Codec = { - require(moveByteIndexPrecond(bitStream, diffInBytes)) + require(BitStream.moveByteIndexPrecond(bitStream, diffInBytes)) Codec(bitStream.withMovedByteIndex(diffInBytes)) } @ghost @pure @inline def withMovedBitIndex(diffInBits: Int): Codec = { - require(moveBitIndexPrecond(bitStream, diffInBits)) + require(BitStream.moveBitIndexPrecond(bitStream, diffInBits)) Codec(bitStream.withMovedBitIndex(diffInBits)) } @@ -195,17 +194,32 @@ 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))) + @ghost val w1 = snapshot(this) appendLSBBitsMSBFirst(v.toRaw, GetBitCountUnsigned(v)) + ghostExpr { + val nBits = GetBitCountUnsigned(v) + val w2 = this + assert( w1.bitStream.buf.length == w2.bitStream.buf.length + && BitStream.bitIndex(w2.bitStream.buf.length, w2.bitStream.currentByte, w2.bitStream.currentBit) == BitStream.bitIndex(w1.bitStream.buf.length, w1.bitStream.currentByte, w1.bitStream.currentBit) + nBits + && w1.isPrefixOf(w2) + ) + val (r1, r2) = reader(w1, w2) + BitStream.validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) + val (r2Got, vGot) = r1.bitStream.readNLSBBitsMSBFirstPure(nBits) + assert(vGot == v.toRaw && r2Got == r2.bitStream) + + } } .ensuring { _ => val w1 = old(this) val w2 = this val nBits = GetBitCountUnsigned(v) - w1.bitStream.buf.length == w2.bitStream.buf.length && BitStream.bitIndex(w2.bitStream.buf.length, w2.bitStream.currentByte, w2.bitStream.currentBit) == BitStream.bitIndex(w1.bitStream.buf.length, w1.bitStream.currentByte, w1.bitStream.currentBit) + nBits /*&& w1.isPrefixOf(w2) && { + w1.bitStream.buf.length == w2.bitStream.buf.length && BitStream.bitIndex(w2.bitStream.buf.length, w2.bitStream.currentByte, w2.bitStream.currentBit) == BitStream.bitIndex(w1.bitStream.buf.length, w1.bitStream.currentByte, w1.bitStream.currentBit) + nBits + && w1.isPrefixOf(w2) && { val (r1, r2) = reader(w1, w2) - validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) + BitStream.validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) val (r2Got, vGot) = r1.decodeUnsignedIntegerPure(nBits) vGot == v && r2Got == r2 - }*/ + } } /** @@ -215,7 +229,7 @@ case class Codec(bitStream: BitStream) { * @return Unsigned integer with nBits decoded from bitstream. * */ - @opaque @inlineOnce + // @opaque @inlineOnce def decodeUnsignedInteger(nBits: Int): ULong = { require(nBits >= 0 && nBits <= NO_OF_BITS_IN_LONG) require(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nBits)) @@ -266,7 +280,7 @@ case class Codec(bitStream: BitStream) { appendLSBBitsMSBFirst(encVal, nRangeBits) else ghostExpr { - lemmaIsPrefixRefl(bitStream) + BitStream.lemmaIsPrefixRefl(bitStream) } }.ensuring { _ => val w1 = old(this) @@ -275,7 +289,7 @@ case class Codec(bitStream: BitStream) { val nBits = GetBitCountUnsigned(range) w1.bitStream.buf.length == w2.bitStream.buf.length && BitStream.bitIndex(w2.bitStream.buf.length, w2.bitStream.currentByte, w2.bitStream.currentBit) == BitStream.bitIndex(w1.bitStream.buf.length, w1.bitStream.currentByte, w1.bitStream.currentBit) + nBits && w1.isPrefixOf(w2) && { val (r1, r2) = reader(w1, w2) - validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) + BitStream.validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) val (r2Got, vGot) = r1.decodeConstrainedPosWholeNumberPure(min, max) vGot == v && r2Got == r2 } @@ -357,7 +371,7 @@ case class Codec(bitStream: BitStream) { appendLSBBitsMSBFirst(encVal, nRangeBits) // else // ghostExpr { - // lemmaIsPrefixRefl(bitStream) + // BitStream.lemmaIsPrefixRefl(bitStream) // } }.ensuring { _ => val w1 = old(this) @@ -369,7 +383,7 @@ case class Codec(bitStream: BitStream) { w1.isPrefixOf(w2) && { val (r1, r2) = reader(w1, w2) - validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) + BitStream.validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) val (r2Got, vGot) = r1.decodeConstrainedWholeNumberPure(min, max) vGot == v && r2Got == r2 }*/ @@ -646,7 +660,7 @@ case class Codec(bitStream: BitStream) { val nBits = NO_OF_BITS_IN_BYTE + GetLengthForEncodingSigned(v) * NO_OF_BITS_IN_BYTE w1.bitStream.buf.length == w2.bitStream.buf.length && BitStream.bitIndex(w2.bitStream.buf.length, w2.bitStream.currentByte, w2.bitStream.currentBit) == BitStream.bitIndex(w1.bitStream.buf.length, w1.bitStream.currentByte, w1.bitStream.currentBit) + nBits /*&& w1.isPrefixOf(w2) && { val (r1, r2) = reader(w1, w2) - validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) + BitStream.validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) val (r2Got, vGot) = r1.decodeUnconstrainedWholeNumberPure() vGot == v && r2Got == r2 }*/ diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala index 56eaaf50..e2f70040 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala @@ -238,16 +238,16 @@ case class ACN(base: Codec) { /* put required zeros*/ val diff = encodedSizeInBits - nBits appendNZeroBits(diff) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) ghostExpr { - validateOffsetBitsDifferenceLemma(this1.base.bitStream, this.base.bitStream, encodedSizeInBits, diff) + BitStream.validateOffsetBitsDifferenceLemma(this1.base.bitStream, this.base.bitStream, encodedSizeInBits, diff) } /*Encode number */ encodeUnsignedInteger(intVal) - /*ghostExpr { + 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) + encodedSizeInBits) - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) val this2Reset = this2.resetAt(this1) val (r1_1, r3_1) = ACN.reader(this1, this) validateOffsetBitsContentIrrelevancyLemma(this1.base.bitStream, this.base.bitStream.buf, encodedSizeInBits) @@ -279,22 +279,22 @@ case class ACN(base: Codec) { check(iGot == intVal) check(r3Got == r3_1) } - }*/ - } /*else { + } + } else { ghostExpr { - validReflexiveLemma(bitStream) + lemmaIsPrefixRefl(bitStream) } - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this w1.base.bitStream.buf.length == w3.base.bitStream.buf.length && BitStream.bitIndex(w3.base.bitStream.buf.length, w3.base.bitStream.currentByte, w3.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + encodedSizeInBits - /*&& w1.isPrefixOf(w3) && { + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, encodedSizeInBits) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_pure(encodedSizeInBits) iGot == intVal && r3Got == r3 - }*/ + } } @ghost @pure @inline @@ -345,7 +345,7 @@ case class ACN(base: Codec) { appendByte(wrappingExpr { intVal.toByte.toRawUByte }) /*ghostExpr { // For isPrefix - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) // Reading back the first byte gives the same result whether we are reading from this2 or the end result this val this2Reset = this2.base.bitStream.resetAt(this1.base.bitStream) readBytePrefixLemma(this2Reset, this.base.bitStream) @@ -373,7 +373,7 @@ case class ACN(base: Codec) { enc_Int_PositiveInteger_ConstSize_big_endian_16(wrappingExpr { (intVal & 0xFFFFL).toRawULong }) /*ghostExpr { // For isPrefix - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) // Reading back the first integer gives the same result whether we are reading from this2 or the end result this val this2Reset = this2.resetAt(this1) dec_Int_PositiveInteger_ConstSize_big_endian_16_prefixLemma(this2Reset, this) @@ -399,7 +399,7 @@ case class ACN(base: Codec) { enc_Int_PositiveInteger_ConstSize_big_endian_32(wrappingExpr { (intVal & 0xFFFFFFFFL).toRawULong }) /*ghostExpr { // For isPrefix - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) // Reading back the first integer gives the same result whether we are reading from this2 or the end result this val this2Reset = this2.resetAt(this1) dec_Int_PositiveInteger_ConstSize_big_endian_32_prefixLemma(this2Reset, this) @@ -427,7 +427,7 @@ case class ACN(base: Codec) { appendByte(wrappingExpr { (intVal >> 8).toUByte }) /*ghostExpr { // For isPrefix - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) // Reading back the first byte gives the same result whether we are reading from this2 or the end result this val this2Reset = this2.resetAt(this1) readBytePrefixLemma(this2Reset.base.bitStream, this.base.bitStream) @@ -455,7 +455,7 @@ case class ACN(base: Codec) { enc_Int_PositiveInteger_ConstSize_little_endian_16(wrappingExpr { ((intVal >> 16) & 0xFFFFL).toRawULong }) /*ghostExpr { // For isPrefix - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) // Reading back the first integer gives the same result whether we are reading from this2 or the end result this val this2Reset = this2.resetAt(this1) dec_Int_PositiveInteger_ConstSize_little_endian_16_prefixLemma(this2Reset, this) @@ -481,7 +481,7 @@ case class ACN(base: Codec) { enc_Int_PositiveInteger_ConstSize_little_endian_32(wrappingExpr { ((intVal >> 32) & 0xFFFFFFFFL).toRawULong }) /*ghostExpr { // For isPrefix - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) // Reading back the first integer gives the same result whether we are reading from this2 or the end result this val this2Reset = this2.resetAt(this1) dec_Int_PositiveInteger_ConstSize_little_endian_32_prefixLemma(this2Reset, this) @@ -694,7 +694,7 @@ case class ACN(base: Codec) { /*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) - validTransitiveLemma(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) + lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) val this2Reset = this2.resetAt(this1) val (r1_1, r3_1) = ACN.reader(this1, this) validateOffsetBitsContentIrrelevancyLemma(this1.base.bitStream, this.base.bitStream.buf, formatBitLength)