Skip to content

Commit

Permalink
prove inverse of encodeUnsignedInteger
Browse files Browse the repository at this point in the history
  • Loading branch information
@samuelchassot
samuelchassot committed Aug 28, 2024
1 parent d0a49c5 commit 790b6ca
Show file tree
Hide file tree
Showing 3 changed files with 73 additions and 59 deletions.
58 changes: 29 additions & 29 deletions asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
40 changes: 27 additions & 13 deletions asn1scala/src/main/scala/asn1scala/asn1jvm_Codec.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand All @@ -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))
}

Expand Down Expand Up @@ -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
}*/
}
}

/**
Expand All @@ -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))
Expand Down Expand Up @@ -266,7 +280,7 @@ case class Codec(bitStream: BitStream) {
appendLSBBitsMSBFirst(encVal, nRangeBits)
else
ghostExpr {
lemmaIsPrefixRefl(bitStream)
BitStream.lemmaIsPrefixRefl(bitStream)
}
}.ensuring { _ =>
val w1 = old(this)
Expand All @@ -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
}
Expand Down Expand Up @@ -357,7 +371,7 @@ case class Codec(bitStream: BitStream) {
appendLSBBitsMSBFirst(encVal, nRangeBits)
// else
// ghostExpr {
// lemmaIsPrefixRefl(bitStream)
// BitStream.lemmaIsPrefixRefl(bitStream)
// }
}.ensuring { _ =>
val w1 = old(this)
Expand All @@ -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
}*/
Expand Down Expand Up @@ -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
}*/
Expand Down
34 changes: 17 additions & 17 deletions asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 790b6ca

Please sign in to comment.