Update ACN: Safety proof restored, adding invertibility (WIP)

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

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) = {

asn1scala/stainless.conf

@@ -1,9 +1,9 @@
 # The settings below correspond to the various
 # options listed by `stainless --help`
 
-vc-cache            = false
-debug               = ["smt"]
-timeout             = 1200
+vc-cache            = true
+# debug               = ["smt"]
+timeout             = 120
 check-models        = false
 print-ids           = false
 print-types         = false
@@ -12,5 +12,5 @@ strict-arithmetic   = true
 solvers             = "smt-cvc5,smt-z3,smt-cvc4"
 check-measures      = yes
 infer-measures      = true
-simplifier           = "ol"
-no-colors           = true
+simplifier           = "bland"
+no-colors           = false

asn1scala/used_acn_functions.txt

@@ -0,0 +1,65 @@
+initACNCodec
+reader
+dec_Int_PositiveInteger_ConstSize_big_endian_16_prefixLemma
+dec_Int_PositiveInteger_ConstSize_big_endian_32_prefixLemma
+dec_Int_PositiveInteger_ConstSize_big_endian_64_prefixLemma
+dec_Int_PositiveInteger_ConstSize_little_endian_16_prefixLemma
+dec_Int_PositiveInteger_ConstSize_little_endian_32_prefixLemma
+dec_Int_PositiveInteger_ConstSize_little_endian_64_prefixLemma
+enc_Int_PositiveInteger_ConstSize
+enc_Int_PositiveInteger_ConstSize
+resetAt
+withMovedByteIndex
+withMovedBitIndex
+isPrefixOf
+enc_Int_PositiveInteger_ConstSize_8
+enc_Int_PositiveInteger_ConstSize_big_endian_16
+enc_Int_PositiveInteger_ConstSize_big_endian_32
+enc_Int_PositiveInteger_ConstSize_big_endian_64
+dec_Int_PositiveInteger_ConstSize
+dec_Int_PositiveInteger_ConstSize_pure
+dec_Int_PositiveInteger_ConstSize_8
+dec_Int_PositiveInteger_ConstSize_8_pure
+dec_Int_PositiveInteger_ConstSize_big_endian_16
+dec_Int_PositiveInteger_ConstSize_big_endian_16_pure
+dec_Int_PositiveInteger_ConstSize_big_endian_32
+dec_Int_PositiveInteger_ConstSize_big_endian_32_pure
+dec_Int_PositiveInteger_ConstSize_big_endian_64
+dec_Int_PositiveInteger_ConstSize_big_endian_64_pure
+dec_Int_PositiveInteger_ConstSize_little_endian_16_pure
+dec_Int_PositiveInteger_ConstSize_little_endian_32_pure
+dec_Int_PositiveInteger_ConstSize_little_endian_64_pure
+enc_Int_TwosComplement_ConstSize
+enc_Int_TwosComplement_ConstSize_8
+enc_Int_TwosComplement_ConstSize_big_endian_16
+enc_Int_TwosComplement_ConstSize_big_endian_32
+enc_Int_TwosComplement_ConstSize_big_endian_64
+dec_Int_TwosComplement_ConstSize
+dec_Int_TwosComplement_ConstSize_pure
+dec_Int_TwosComplement_ConstSize_8
+dec_Int_TwosComplement_ConstSize_big_endian_16
+dec_Int_TwosComplement_ConstSize_big_endian_32
+dec_Int_TwosComplement_ConstSize_big_endian_64
+BitStream_ReadBitPattern
+BitStream_DecodeTrueFalseBoolean
+enc_Real_IEEE754_32_big_endian
+enc_Real_IEEE754_32_little_endian
+enc_Real_IEEE754_64_big_endian
+enc_Real_IEEE754_64_little_endian
+dec_Real_IEEE754_32_big_endian
+dec_Real_IEEE754_32_little_endian
+dec_Real_IEEE754_64_big_endian
+dec_Real_IEEE754_64_little_endian
+enc_String_Ascii_Null_Terminated_multVec
+enc_String_CharIndex_private
+enc_IA5String_CharIndex_External_Field_Determinant
+enc_IA5String_CharIndex_External_Field_DeterminantVec
+enc_IA5String_CharIndex_Internal_Field_DeterminantVec
+dec_String_Ascii_Null_Terminated_multVec
+dec_String_CharIndex_private
+dec_IA5String_CharIndex_External_Field_Determinant
+dec_IA5String_CharIndex_External_Field_DeterminantVec
+dec_IA5String_CharIndex_Internal_Field_Determinant
+dec_IA5String_CharIndex_Internal_Field_DeterminantVec
+milbus_encode
+milbus_decode

asn1scala/verify.sh

@@ -3,6 +3,9 @@ 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_Codec_ACN.scala \
+src/main/scala/asn1scala/asn1jvm_Vector.scala \
+src/main/scala/asn1scala/asn1jvm_Codec.scala \
 --config-file=stainless.conf \
 -D-parallel=5 \
 $1

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

asn1scala/verify_safety_acn.sh

@@ -0,0 +1,12 @@
+stainless-dotty \
+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_Codec_ACN.scala \
+src/main/scala/asn1scala/asn1jvm_Vector.scala \
+src/main/scala/asn1scala/asn1jvm_Codec.scala \
+--config-file=stainless.conf \
+-D-parallel=5 \
+--functions=initACNCodec,reader,dec_Int_PositiveInteger_ConstSize_big_endian_16_prefixLemma,dec_Int_PositiveInteger_ConstSize_big_endian_32_prefixLemma,dec_Int_PositiveInteger_ConstSize_big_endian_64_prefixLemma,dec_Int_PositiveInteger_ConstSize_little_endian_16_prefixLemma,dec_Int_PositiveInteger_ConstSize_little_endian_32_prefixLemma,dec_Int_PositiveInteger_ConstSize_little_endian_64_prefixLemma,enc_Int_PositiveInteger_ConstSize,enc_Int_PositiveInteger_ConstSize,resetAt,withMovedByteIndex,withMovedBitIndex,isPrefixOf,enc_Int_PositiveInteger_ConstSize_8,enc_Int_PositiveInteger_ConstSize_big_endian_16,enc_Int_PositiveInteger_ConstSize_big_endian_32,enc_Int_PositiveInteger_ConstSize_big_endian_64,dec_Int_PositiveInteger_ConstSize,dec_Int_PositiveInteger_ConstSize_pure,dec_Int_PositiveInteger_ConstSize_8,dec_Int_PositiveInteger_ConstSize_8_pure,dec_Int_PositiveInteger_ConstSize_big_endian_16,dec_Int_PositiveInteger_ConstSize_big_endian_16_pure,dec_Int_PositiveInteger_ConstSize_big_endian_32,dec_Int_PositiveInteger_ConstSize_big_endian_32_pure,dec_Int_PositiveInteger_ConstSize_big_endian_64,dec_Int_PositiveInteger_ConstSize_big_endian_64_pure,dec_Int_PositiveInteger_ConstSize_little_endian_16_pure,dec_Int_PositiveInteger_ConstSize_little_endian_32_pure,dec_Int_PositiveInteger_ConstSize_little_endian_64_pure,enc_Int_TwosComplement_ConstSize,enc_Int_TwosComplement_ConstSize_8,enc_Int_TwosComplement_ConstSize_big_endian_16,enc_Int_TwosComplement_ConstSize_big_endian_32,enc_Int_TwosComplement_ConstSize_big_endian_64,dec_Int_TwosComplement_ConstSize,dec_Int_TwosComplement_ConstSize_pure,dec_Int_TwosComplement_ConstSize_8,dec_Int_TwosComplement_ConstSize_big_endian_16,dec_Int_TwosComplement_ConstSize_big_endian_32,dec_Int_TwosComplement_ConstSize_big_endian_64,BitStream_ReadBitPattern,BitStream_DecodeTrueFalseBoolean,enc_Real_IEEE754_32_big_endian,enc_Real_IEEE754_32_little_endian,enc_Real_IEEE754_64_big_endian,enc_Real_IEEE754_64_little_endian,dec_Real_IEEE754_32_big_endian,dec_Real_IEEE754_32_little_endian,dec_Real_IEEE754_64_big_endian,dec_Real_IEEE754_64_little_endian,enc_String_Ascii_Null_Terminated_multVec,enc_String_CharIndex_private,enc_IA5String_CharIndex_External_Field_Determinant,enc_IA5String_CharIndex_External_Field_DeterminantVec,enc_IA5String_CharIndex_Internal_Field_DeterminantVec,dec_String_Ascii_Null_Terminated_multVec,dec_String_CharIndex_private,dec_IA5String_CharIndex_External_Field_Determinant,dec_IA5String_CharIndex_External_Field_DeterminantVec,dec_IA5String_CharIndex_Internal_Field_Determinant,dec_IA5String_CharIndex_Internal_Field_DeterminantVec,milbus_encode,milbus_decode \
+$1