Skip to content

Commit

Permalink
new annotations for proof to pass
Browse files Browse the repository at this point in the history
  • Loading branch information
@samuelchassot
samuelchassot committed Aug 27, 2024
1 parent 6a4a0cb commit 497e9b4
Showing 1 changed file with 67 additions and 61 deletions.
128 changes: 67 additions & 61 deletions asn1scala/src/main/scala/asn1scala/asn1jvm_Bitstream.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down Expand Up @@ -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)

Expand All @@ -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)

}

Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 497e9b4

Please sign in to comment.