From 3b9323372d4e45e61e664acfa55641f42fe2e66d Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 28 Aug 2024 14:12:22 +0200 Subject: [PATCH] prove some invertibility in Codec ACN --- .../main/scala/asn1scala/asn1jvm_Codec.scala | 124 ++++++++++++++---- .../scala/asn1scala/asn1jvm_Codec_ACN.scala | 101 +++++++------- 2 files changed, 151 insertions(+), 74 deletions(-) diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala index 26ecee81..9c5ca030 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala @@ -365,28 +365,29 @@ case class Codec(bitStream: BitStream) { val encVal = stainless.math.wrapping(v - min).toRawULong @ghost val nEncValBits = GetBitCountUnsigned(encVal) - //SAMassert(nRangeBits >= nEncValBits) - //SAMassert(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nRangeBits)) + assert(nRangeBits >= nEncValBits) + assert(BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nRangeBits)) appendLSBBitsMSBFirst(encVal, nRangeBits) - // else - // ghostExpr { - // BitStream.lemmaIsPrefixRefl(bitStream) - // } + else + ghostExpr { + BitStream.lemmaIsPrefixRefl(bitStream) + } }.ensuring { _ => val w1 = old(this) val w2 = this val range = stainless.math.wrapping(max - min) val nBits = GetBitCountUnsigned(range.toRawULong) 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 /*&& + && 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.decodeConstrainedWholeNumberPure(min, max) vGot == v && r2Got == r2 - }*/ + } } /** @@ -404,7 +405,6 @@ case class Codec(bitStream: BitStream) { * SAM Changed to cap the value to the max/min value, so that the post condition holds * */ - @opaque @inlineOnce def decodeConstrainedWholeNumber(min: Long, max: Long): Long = { require(min <= max) staticRequire( @@ -500,6 +500,7 @@ case class Codec(bitStream: BitStream) { * This function writes full bytes to the bitstream. The length is written as * an signed byte in front of the bytes written for the number v. * + * Unused in PUS-C * @param v number that gets encoded to the bitstream. Must be bigger than min. * @param min lower boundary of range * @@ -513,21 +514,61 @@ case class Codec(bitStream: BitStream) { val encV: ULong = stainless.math.wrapping(v - min).toRawULong val nBytes = GetLengthForEncodingUnsigned(encV).toByte + val nBits = nBytes * NO_OF_BITS_IN_BYTE // need space for length and value assert(BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,nBytes + 1)) + @ghost val this1 = snapshot(this) // encode length appendByte(nBytes.toRawUByte) + + @ghost val this2 = snapshot(this) // encode value 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) + + ghostExpr(BitStream.lemmaIsPrefixTransitive(this1.bitStream, this2.bitStream, this.bitStream)) + + ghostExpr { + BitStream.lemmaIsPrefixRefl(bitStream) + } + + ghostExpr { + BitStream.lemmaIsPrefixTransitive(this1.bitStream, this2.bitStream, this.bitStream) + val this2Reset = this2.bitStream.resetAt(this1.bitStream) + BitStream.readBytePrefixLemma(this2Reset, this.bitStream) + assert(this2.bitStream.resetAt(this1.bitStream).readBytePure()._2.unsignedToInt == nBytes) + val (r1, r2) = reader(this1, this) + BitStream.validateOffsetBytesContentIrrelevancyLemma(this1.bitStream, this.bitStream.buf, nBytes + 1) + assert(r1 == Codec(BitStream(snapshot(this.bitStream.buf), this1.bitStream.currentByte, this1.bitStream.currentBit))) + assert(BitStream.validate_offset_bytes(r1.bitStream.buf.length, r1.bitStream.currentByte, r1.bitStream.currentBit, nBytes + 1)) + val (r2Got, vGot) = r1.decodeSemiConstrainedWholeNumberPure(min) + check(r2Got == r2) + assert((vGot & onesLSBLong(nBits)) == (v & onesLSBLong(nBits))) + check(vGot == v) + } + + }.ensuring(_ => + val w1 = old(this) + val w2 = this + val encV: ULong = stainless.math.wrapping(v - min).toRawULong + val nBits = GetLengthForEncodingUnsigned(stainless.math.wrapping(v - min).toRawULong) * 8L + 8L + 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 + &&& w1.isPrefixOf(w2) + &&& { + val (r1, r2) = reader(w1, w2) + BitStream.validateOffsetBitsContentIrrelevancyLemma(w1.bitStream, w2.bitStream.buf, nBits) + val (r2Got, vGot) = r1.decodeSemiConstrainedWholeNumberPure(min) + (vGot == v) && r2Got == r2 + } + ) /** * Decode number from bitstream that is in range [min, Long.MaxValue]. * This is the reversal function of encodeSemiConstrainedWholeNumber. * + * Unused in PUS-C * @param min lower boundary of range * @return value decoded from the bitstream. * @@ -555,14 +596,30 @@ case class Codec(bitStream: BitStream) { // SAM: here the post condition should be obvious, as ULong are always positive. But we can have // overflow, and ULong does not encode the unsigned nature in any way, so cannot work. - v + min - }// SAM .ensuring(x => x >= min) + val res = v + min + if(res < min) then Long.MaxValue else res + }.ensuring(res => res >= min) + + // Unused in PUS-C + @ghost @pure + def decodeSemiConstrainedWholeNumberPure(min: Long): (Codec, Long) = { + require(BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, 1)) + staticRequire { + val nBytes = bitStream.readBytePure()._2.unsignedToInt + BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, 1 + nBytes) && 0 <= nBytes && nBytes <= 8 + } + val cpy = snapshot(this) + val res = cpy.decodeSemiConstrainedWholeNumber(min) + (cpy, res) + } + /** * Encode number to the bitstream within the range [min, Long.Max_Value]. * This function writes full bytes to the bitstream. The length is written as * an signed byte in front of the bytes written for the number v. * + * Unused in PUS-C * @param v number that gets encoded to the bitstream. Must be bigger than min. * @param min lower unsigned boundary of range * @@ -589,6 +646,7 @@ case class Codec(bitStream: BitStream) { * Decode unsigned number from the bitstream * within the range [min, Long.Max_Value]. * + * Unused in PUS-C * @param min lower unsigned boundary of range * */ @@ -603,13 +661,18 @@ case class Codec(bitStream: BitStream) { val nBytesRaw = nBytes.toRaw val nBits = nBytesRaw * NO_OF_BITS_IN_BYTE // SAM GUARD - val v = if(!(nBits >= 0 && nBits <= 64) || !BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, nBits)){ + val v: ULong = if(!(nBits >= 0 && nBits <= 64) || !BitStream.validate_offset_bits(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit, nBits)){ 0L.toRawULong } else { readNLSBBitsMSBFirst(nBits).toRawULong } - val res: ULong = ULong.fromRaw(v + min) // For some reasons, the scala compiler chokes on this being returned - res + val res: ULong = ULong.fromRaw(v + min) + if(res < min) then + assert(ULong.fromRaw(-1L) >= min) + ULong.fromRaw(Long.MaxValue) + else + assert(res >= min) + res }//.ensuring(res => min <= res) /** @@ -618,6 +681,7 @@ case class Codec(bitStream: BitStream) { * The encoding of an integer value shall be primitive. * The contents octets shall consist of one or more octets. * + * Unused in PUS-C * @param v The value that is always encoded in the smallest possible number of octets. */ @opaque @inlineOnce @@ -639,31 +703,32 @@ case class Codec(bitStream: BitStream) { @ghost val this2 = snapshot(this) // encode number appendLSBBitsMSBFirst(v & onesLSBLong(nBits), nBits) - /* + ghostExpr { - validTransitiveLemma(this1.bitStream, this2.bitStream, this.bitStream) + BitStream.lemmaIsPrefixTransitive(this1.bitStream, this2.bitStream, this.bitStream) val this2Reset = this2.bitStream.resetAt(this1.bitStream) - readBytePrefixLemma(this2Reset, this.bitStream) + BitStream.readBytePrefixLemma(this2Reset, this.bitStream) assert(this2.bitStream.resetAt(this1.bitStream).readBytePure()._2.unsignedToInt == nBytes) val (r1, r2) = reader(this1, this) - validateOffsetBytesContentIrrelevancyLemma(this1.bitStream, this.bitStream.buf, nBytes + 1) + BitStream.validateOffsetBytesContentIrrelevancyLemma(this1.bitStream, this.bitStream.buf, nBytes + 1) assert(r1 == Codec(BitStream(snapshot(this.bitStream.buf), this1.bitStream.currentByte, this1.bitStream.currentBit))) assert(BitStream.validate_offset_bytes(r1.bitStream.buf.length, r1.bitStream.currentByte, r1.bitStream.currentBit, nBytes + 1)) val (r2Got, vGot) = r1.decodeUnconstrainedWholeNumberPure() check(r2Got == r2) - //SAM assert((vGot & onesLSBLong(nBits)) == (v & onesLSBLong(nBits))) - check(vGot == v) - }*/ + assert(vGot.isEmpty || (vGot.get & onesLSBLong(nBits)) == (v & onesLSBLong(nBits))) + check(vGot.isEmpty || vGot.get == v) + } }.ensuring { _ => val w1 = old(this) val w2 = this 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) && { + 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.decodeUnconstrainedWholeNumberPure() - vGot == v && r2Got == r2 - }*/ + (vGot.isEmpty || vGot.get == v) && r2Got == r2 + } } /** @@ -673,9 +738,9 @@ case class Codec(bitStream: BitStream) { * The length n is the first octet, n octets with the value follow * Values with n > 8 are not supported * + * Unused in PUS-C * @return decoded number */ - @opaque @inlineOnce def decodeUnconstrainedWholeNumber(): Option[Long] = { require(BitStream.validate_offset_bytes(bitStream.buf.length, bitStream.currentByte, bitStream.currentBit,1)) @@ -722,6 +787,9 @@ case class Codec(bitStream: BitStream) { /** * Facade function for real encoding + * + * Unused in PUS-C + * * @param vValDouble real input in IEEE754 double format */ @extern @@ -773,6 +841,8 @@ case class Codec(bitStream: BitStream) { * |1|S|0|0|a|b|c|d| * +-+-+-+-+-+-+-+-+ * + * + * */ private def encodeRealBitString(vVal: Long): Unit = { // Require from CalculateMantissaAndExponent diff --git a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala index ba513417..f0cb9624 100644 --- a/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala +++ b/asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala @@ -326,93 +326,97 @@ case class ACN(base: Codec) { }.ensuring { _ => val w1 = old(this) val w2 = this - w1.base.bufLength() == w2.base.bufLength() && BitStream.bitIndex(w2.base.bitStream.buf.length, w2.base.bitStream.currentByte, w2.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + 8 /*&& w1.isPrefixOf(w2) && { + w1.base.bufLength() == w2.base.bufLength() && BitStream.bitIndex(w2.base.bitStream.buf.length, w2.base.bitStream.currentByte, w2.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + 8 + && w1.isPrefixOf(w2) && { val (r1, r2) = ACN.reader(w1, w2) val (r2Got, vGot) = r1.dec_Int_PositiveInteger_ConstSize_8_pure() vGot == intVal && r2Got == r2 - }*/ + } } - @opaque @inlineOnce def enc_Int_PositiveInteger_ConstSize_big_endian_16(uintVal: ULong): Unit = { require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 16)) require(uintVal <= 65535) val intVal = uintVal.toRaw assert((intVal >> 16) == 0L) - // @ghost val this1 = snapshot(this) + @ghost val this1 = snapshot(this) appendByte(wrappingExpr { (intVal >> 8).toByte.toRawUByte }) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) appendByte(wrappingExpr { intVal.toByte.toRawUByte }) - /*ghostExpr { + ghostExpr { // For isPrefix 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) - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + 16 /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + 16 + && w1.isPrefixOf(w3) + && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 16) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_big_endian_16_pure() iGot == uintVal && r3Got == r3 - }*/ + } } - @opaque @inlineOnce + @inlineOnce @opaque def enc_Int_PositiveInteger_ConstSize_big_endian_32(uintVal: ULong): Unit = { require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 32)) require(uintVal <= 4294967295L) val intVal = uintVal.toRaw assert((intVal >> 32) == 0L) - // @ghost val this1 = snapshot(this) + @ghost val this1 = snapshot(this) enc_Int_PositiveInteger_ConstSize_big_endian_16(wrappingExpr { ((intVal >> 16) & 0xFFFFL).toRawULong }) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) enc_Int_PositiveInteger_ConstSize_big_endian_16(wrappingExpr { (intVal & 0xFFFFL).toRawULong }) - /*ghostExpr { + ghostExpr { // For isPrefix 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) - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + 32 /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + 32 + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 32) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_big_endian_32_pure() iGot == uintVal && r3Got == r3 - }*/ + } } @opaque @inlineOnce def enc_Int_PositiveInteger_ConstSize_big_endian_64(uintVal: ULong): Unit = { require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 64)) val intVal = uintVal.toRaw - // @ghost val this1 = snapshot(this) + @ghost val this1 = snapshot(this) enc_Int_PositiveInteger_ConstSize_big_endian_32(wrappingExpr { ((intVal >> 32) & 0xFFFFFFFFL).toRawULong }) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) enc_Int_PositiveInteger_ConstSize_big_endian_32(wrappingExpr { (intVal & 0xFFFFFFFFL).toRawULong }) - /*ghostExpr { + ghostExpr { // For isPrefix 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) - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + 64 /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + 64 + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 64) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_big_endian_64_pure() iGot == uintVal && r3Got == r3 - }*/ + } } @opaque @inlineOnce @@ -421,26 +425,27 @@ case class ACN(base: Codec) { require(uintVal <= 65535) val intVal = uintVal.toRaw assert((intVal >> 16) == 0L) - // @ghost val this1 = snapshot(this) + @ghost val this1 = snapshot(this) appendByte(wrappingExpr { intVal.toUByte }) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) appendByte(wrappingExpr { (intVal >> 8).toUByte }) - /*ghostExpr { + ghostExpr { // For isPrefix 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) - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + 16 /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + 16 + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 16) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_little_endian_16_pure() iGot == uintVal && r3Got == r3 - }*/ + } } @opaque @inlineOnce @@ -449,52 +454,54 @@ case class ACN(base: Codec) { require(uintVal <= 4294967295L) val intVal = uintVal.toRaw assert((intVal >> 32) == 0L) - // @ghost val this1 = snapshot(this) + @ghost val this1 = snapshot(this) enc_Int_PositiveInteger_ConstSize_little_endian_16(wrappingExpr { (intVal & 0xFFFFL).toRawULong }) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) enc_Int_PositiveInteger_ConstSize_little_endian_16(wrappingExpr { ((intVal >> 16) & 0xFFFFL).toRawULong }) - /*ghostExpr { + ghostExpr { // For isPrefix 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) - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + 32 /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + 32 + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 32) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_little_endian_32_pure() iGot == uintVal && r3Got == r3 - }*/ + } } @opaque @inlineOnce def enc_Int_PositiveInteger_ConstSize_little_endian_64(uintVal: ULong): Unit = { require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 64)) val intVal = uintVal.toRaw - // @ghost val this1 = snapshot(this) + @ghost val this1 = snapshot(this) enc_Int_PositiveInteger_ConstSize_little_endian_32(wrappingExpr { (intVal & 0xFFFFFFFFL).toRawULong }) - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) enc_Int_PositiveInteger_ConstSize_little_endian_32(wrappingExpr { ((intVal >> 32) & 0xFFFFFFFFL).toRawULong }) - /*ghostExpr { + ghostExpr { // For isPrefix 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) - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + 64 /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + 64 + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 64) val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_little_endian_64_pure() iGot == uintVal && r3Got == r3 - }*/ + } } def dec_Int_PositiveInteger_ConstSize(encodedSizeInBits: Int): ULong = { @@ -512,7 +519,6 @@ case class ACN(base: Codec) { (cpy, l) } - @opaque @inlineOnce def dec_Int_PositiveInteger_ConstSize_8(): ULong = { require(BitStream.validate_offset_byte(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit)) ULong.fromRaw(readByte().toRaw & 0xFF) @@ -677,7 +683,7 @@ case class ACN(base: Codec) { * @param v value that gets encoded * @param formatBitLength number of dataformat bits */ - @opaque @inlineOnce + // @opaque @inlineOnce def enc_Int_TwosComplement_ConstSize(v: Long, formatBitLength: Int): Unit = { val nBits = GetBitCountSigned(v) require(nBits <= formatBitLength && formatBitLength <= NO_OF_BITS_IN_LONG) @@ -689,9 +695,9 @@ case class ACN(base: Codec) { ghostExpr { validateOffsetBitsDifferenceLemma(this1.base.bitStream, this.base.bitStream, formatBitLength, addedBits) } - // @ghost val this2 = snapshot(this) + @ghost val this2 = snapshot(this) appendLSBBitsMSBFirst(v & onesLSBLong(nBits), nBits) - /*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) + formatBitLength) lemmaIsPrefixTransitive(this1.base.bitStream, this2.base.bitStream, this.base.bitStream) @@ -739,16 +745,17 @@ case class ACN(base: Codec) { check(vGot == v) check(r3Got == r3_1) } - }*/ + } }.ensuring { _ => val w1 = old(this) val w3 = this - w1.base.bufLength() == w3.base.bufLength() && 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) + formatBitLength /*&& w1.isPrefixOf(w3) && { + w1.base.bufLength() == w3.base.bufLength() && 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) + formatBitLength + && w1.isPrefixOf(w3) && { val (r1, r3) = ACN.reader(w1, w3) validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, formatBitLength) val (r3Got, vGot) = r1.dec_Int_TwosComplement_ConstSize_pure(formatBitLength) vGot == v && r3Got == r3 - }*/ + } } def enc_Int_TwosComplement_ConstSize_8(intVal: Long): Unit = {