chore(dafny): remove more usage of BigInteger

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy

@@ -36,6 +36,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
   import EncryptionContext
 
   import opened Seq
+  import opened StandardLibrary.MemoryMath
 
   datatype Config = Config(
     nameonly crypto: Primitives.AtomicPrimitivesClient,
@@ -160,9 +161,10 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
       .MapFailure(e => Types.AwsCryptographyMaterialProviders(e));
     }
 
-      // int64 fits 9 exabytes so we're never going to actually hit this. But if we don't
-      // include this the verifier is not convinced that we can cast the size to int64
-    :- Need(|input.plaintext| < INT64_MAX_LIMIT,
+    // int64 fits 9 exabytes so we're never going to actually hit this. But if we don't
+    // include this the verifier is not convinced that we can cast the size to int64
+    SequenceIsSafeBecauseItIsInMemory(input.plaintext);
+    :- Need(|input.plaintext| as uint64 < INT64_MAX_LIMIT as uint64,
             Types.AwsEncryptionSdkException(
               message := "Plaintext exceeds maximum allowed size"));
 
@@ -316,7 +318,8 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
       var bytes :- maybeBytes
       .MapFailure(e => Types.AwsCryptographyPrimitives(e));
 
-      :- Need(|bytes| < UINT16_LIMIT,
+      SequenceIsSafeBecauseItIsInMemory(bytes);
+      :- Need(|bytes| as uint64 < UINT16_LIMIT as uint64,
               Types.AwsEncryptionSdkException(
                 message := "Length of signature bytes is larger than the uint16 limit."));
 
@@ -527,7 +530,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
     //# This default CMM MUST obtain the decryption materials required for
     //# decryption.
     // TODO :: Consider removing "Default CMM MUST obtain" from spec.
-    // It is redundent and hard to prove.
+    // It is redundant and hard to prove.
 
     //= compliance/client-apis/decrypt.txt#2.7.2
     //# This operation MUST obtain this set of decryption materials
@@ -762,8 +765,8 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
       decMat,
       config.crypto
     );
-
-    :- Need(signature.start == |signature.bytes|,
+    SequenceIsSafeBecauseItIsInMemory(signature.bytes);
+    :- Need(signature.start == |signature.bytes| as uint64,
             Types.AwsEncryptionSdkException(
               message := "Data after message footer."));
 
@@ -818,7 +821,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
   )
     requires exists readRange: seq<uint8> :: SerializeFunctions.CorrectlyReadRange(buffer, verifiedTail, readRange)
     ensures
-      && buffer.start <= verifiedTail.start <= |buffer.bytes|
+      && buffer.start as nat <= verifiedTail.start as nat <= |buffer.bytes|
       && SerializeFunctions.CorrectlyReadRange(buffer, verifiedTail, buffer.bytes[buffer.start..verifiedTail.start])
       && buffer.bytes == verifiedTail.bytes
   {
@@ -830,7 +833,7 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp
     verifiedMid: SerializeFunctions.ReadableBuffer,
     verifiedTail: SerializeFunctions.ReadableBuffer
   )
-    requires buffer.start <= verifiedMid.start <= verifiedTail.start <= |buffer.bytes|
+    requires buffer.start as nat <= verifiedMid.start as nat <= verifiedTail.start as nat <= |buffer.bytes|
     requires SerializeFunctions.CorrectlyReadRange(buffer, verifiedMid, buffer.bytes[buffer.start..verifiedMid.start])
     requires SerializeFunctions.CorrectlyReadRange(verifiedMid, verifiedTail, buffer.bytes[verifiedMid.start..verifiedTail.start])
     ensures SerializeFunctions.CorrectlyReadRange(buffer, verifiedTail, buffer.bytes[buffer.start..verifiedTail.start])

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy

@@ -12,6 +12,7 @@ module EncryptDecryptHelpers {
   import opened Wrappers
   import opened StandardLibrary
   import opened UInt = StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
@@ -359,9 +360,10 @@ module EncryptDecryptHelpers {
       ==>
         output.Fail?
   {
+    SequenceIsSafeBecauseItIsInMemory(edks);
     if
       && maxEncryptedDataKeys.Some?
-      && |edks| > maxEncryptedDataKeys.value as int
+      && |edks| as uint64 > maxEncryptedDataKeys.value as uint64
     then
       Fail(Types.AwsEncryptionSdkException( message := "Encrypted data keys exceed maxEncryptedDataKeys"))
     else
@@ -385,13 +387,13 @@ module EncryptDecryptHelpers {
       && res.Success?
       && suite.messageVersion == 1
       ==>
-        |res.value| == HeaderTypes.MESSAGE_ID_LEN_V1
+        |res.value| == HeaderTypes.MESSAGE_ID_LEN_V1 as nat
 
     ensures
       && res.Success?
       && suite.messageVersion == 2
       ==>
-        |res.value| == HeaderTypes.MESSAGE_ID_LEN_V2
+        |res.value| == HeaderTypes.MESSAGE_ID_LEN_V2 as nat
   {
     var maybeId;
     if suite.messageVersion == 1 {
@@ -551,7 +553,7 @@ module EncryptDecryptHelpers {
                     encryptionContext := encryptionContext,
                     encryptedDataKeys := encryptedDataKeys,
                     contentType := HeaderTypes.ContentType.Framed,
-                    headerIvLength := SerializableTypes.GetIvLength(suite) as nat,
+                    headerIvLength := SerializableTypes.GetIvLength(suite) as uint64,
                     frameLength := frameLength
                   )
   {
@@ -570,7 +572,7 @@ module EncryptDecryptHelpers {
           encryptionContext := encryptionContext,
           encryptedDataKeys := encryptedDataKeys,
           contentType := contentType,
-          headerIvLength := SerializableTypes.GetIvLength(suite) as nat,
+          headerIvLength := SerializableTypes.GetIvLength(suite) as uint64,
           frameLength := frameLength
         );
       case HKDF(_) => return HeaderTypes.HeaderBody.V2HeaderBody(
@@ -606,13 +608,13 @@ module EncryptDecryptHelpers {
     //# algorithm (../framework/algorithm-suites.md#encryption-algorithm)
     //# specified by the algorithm suite (../framework/algorithm-suites.md),
     //# with the following inputs:
-    var keyLength := SerializableTypes.GetEncryptKeyLength(suite) as nat;
-    :- Need(|dataKey| == keyLength,
+    var keyLength := SerializableTypes.GetEncryptKeyLength(suite);
+    SequenceIsSafeBecauseItIsInMemory(dataKey);
+    :- Need(|dataKey| as uint64 == keyLength as uint64,
             Types.AwsEncryptionSdkException( message := "Incorrect data key length"));
 
-    var ivLength := SerializableTypes.GetIvLength(suite);
     //#*  The IV has a value of 0.
-    var iv: seq<uint8> := seq(ivLength, _ => 0);
+    var iv := SerializableTypes.GetIvLengthZeros(suite);
 
     var maybeEncryptionOutput := crypto.AESEncrypt(
       Primitives.Types.AESEncryptInput(
@@ -815,8 +817,9 @@ module EncryptDecryptHelpers {
     ensures header.suiteData != expectedSuiteData ==> res.Failure?
     ensures |header.suiteData| != suite.commitment.HKDF.outputKeyLength as int ==> res.Failure?
   {
+    SequenceIsSafeBecauseItIsInMemory(header.suiteData);
     :- Need(
-      |header.suiteData| == suite.commitment.HKDF.outputKeyLength as int,
+      |header.suiteData| as uint64 == suite.commitment.HKDF.outputKeyLength as uint64,
       Types.AwsEncryptionSdkException(
         message := "Commitment key is invalid")
     );
@@ -843,11 +846,11 @@ module EncryptDecryptHelpers {
     modifies crypto.Modifies
     ensures crypto.ValidState()
 
-    requires buffer.start <= |buffer.bytes|
+    requires buffer.start as nat <= |buffer.bytes|
     requires |key| == SerializableTypes.GetEncryptKeyLength(header.suite) as nat
     ensures res.Success? ==>
               var (plaintext, tail) := res.value;
-              && buffer.start <= tail.start <= |buffer.bytes|
+              && buffer.start as nat <= tail.start as nat <= |buffer.bytes|
               && SerializeFunctions.CorrectlyReadRange(buffer, tail, buffer.bytes[buffer.start..tail.start])
   {
     assert CorrectlyReadRange(buffer, buffer, []) by { reveal CorrectlyReadRange(); }
@@ -879,11 +882,11 @@ module EncryptDecryptHelpers {
     modifies crypto.Modifies
     ensures crypto.ValidState()
 
-    requires buffer.start <= |buffer.bytes|
+    requires buffer.start as nat <= |buffer.bytes|
     requires |key| == SerializableTypes.GetEncryptKeyLength(header.suite) as nat
     ensures res.Success? ==>
               var (plaintext, tail) := res.value;
-              && buffer.start <= tail.start <= |buffer.bytes|
+              && buffer.start as nat <= tail.start as nat <= |buffer.bytes|
               && SerializeFunctions.CorrectlyReadRange(buffer, tail, buffer.bytes[buffer.start..tail.start])
   {
     var messageBody :- MessageBody.ReadNonFramedMessageBody(buffer, header)

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy

@@ -260,7 +260,7 @@ module KeyDerivation {
 
       :- Need(
         && SerializableTypes.GetEncryptKeyLength(suite) == suite.kdf.HKDF.outputKeyLength
-        && |plaintextKey| == suite.kdf.HKDF.inputKeyLength as nat, Types.AwsEncryptionSdkException(
+        && |plaintextKey| as int32 == suite.kdf.HKDF.inputKeyLength as int32, Types.AwsEncryptionSdkException(
           message := "Invalid Materials"));
 
       keys :- ExpandKeyMaterial(messageId, plaintextKey, suite, crypto);
@@ -269,9 +269,9 @@ module KeyDerivation {
                 message := "Suites with message version 1 must not have commitment"));
 
       :- Need(match suite.kdf {
-                case IDENTITY(i) => |plaintextKey| == SerializableTypes.GetEncryptKeyLength(suite) as nat
+                case IDENTITY(i) => |plaintextKey| as int32 == SerializableTypes.GetEncryptKeyLength(suite)
                 case HKDF(hkdf) =>
-                  && |plaintextKey| == suite.kdf.HKDF.inputKeyLength as nat
+                  && |plaintextKey| as int32 == suite.kdf.HKDF.inputKeyLength
                   && suite.kdf.HKDF.outputKeyLength == SerializableTypes.GetEncryptKeyLength(suite)
                 case None => false
               }, Types.AwsEncryptionSdkException(

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy

@@ -20,6 +20,7 @@ module MessageBody {
 
   import opened Wrappers
   import opened UInt = StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import Primitives = AtomicPrimitives
@@ -49,7 +50,7 @@ module MessageBody {
   const ENDFRAME_SEQUENCE_NUMBER: uint32 := Frames.ENDFRAME_SEQUENCE_NUMBER
   const NONFRAMED_SEQUENCE_NUMBER: uint32 := Frames.NONFRAMED_SEQUENCE_NUMBER
 
-  function method IVSeq(suite: MPL.AlgorithmSuiteInfo, sequenceNumber: uint32)
+  function method {:opaque} IVSeq(suite: MPL.AlgorithmSuiteInfo, sequenceNumber: uint32)
     :(ret: seq<uint8>)
     requires 4 <= SerializableTypes.GetIvLength(suite)
     //= compliance/data-format/message-body.txt#2.5.2.1.2
@@ -64,7 +65,13 @@ module MessageBody {
     //# (../framework/algorithm-suites.md) that generated the message.
     ensures |ret| == SerializableTypes.GetIvLength(suite) as nat
   {
-    seq(SerializableTypes.GetIvLength(suite) as nat - 4, _ => 0) + UInt32ToSeq(sequenceNumber)
+    var len : uint8 := SerializableTypes.GetIvLength(suite);
+    var num  := UInt32ToSeq(sequenceNumber);
+    if len == 12 then
+      [0,0,0,0,0,0,0,0] + num
+    else
+      // We never actually get here, but maybe one day
+      seq(len as nat - 4, _ => 0) + num
   }
 
   //= compliance/data-format/message-body.txt#2.5.2.1.2
@@ -81,6 +88,7 @@ module MessageBody {
     ensures IVSeq(suite, m) != IVSeq(suite, n)
   {
     var paddingLength :=  SerializableTypes.GetIvLength(suite) as nat - 4;
+    reveal IVSeq;
     assert IVSeq(suite, m)[paddingLength..] == UInt32ToSeq(m);
     assert IVSeq(suite, n)[paddingLength..] == UInt32ToSeq(n);
     UInt32SeqSerializeDeserialize(m);
@@ -248,7 +256,7 @@ module MessageBody {
                       && frame.authTag == callEvent.output.value.authTag
               )
   {
-    var n : int, sequenceNumber := 0, START_SEQUENCE_NUMBER;
+    var n : uint64, sequenceNumber := 0, START_SEQUENCE_NUMBER;
     var regularFrames: MessageRegularFrames := [];
 
     //= compliance/client-apis/encrypt.txt#2.7
@@ -265,8 +273,9 @@ module MessageBody {
     // adding another frame puts us at < |plaintext|. This means we will never
     // consume the entire plaintext in this while loop, and will always construct
     // a final frame after exiting it.
-    while n + header.body.frameLength as nat < |plaintext|
-      invariant |plaintext| != 0 ==> 0 <= n < |plaintext|
+    SequenceIsSafeBecauseItIsInMemory(plaintext);
+    while Add(n, header.body.frameLength as uint64) < |plaintext| as uint64
+      invariant |plaintext| != 0 ==> 0 <= n as nat < |plaintext|
       invariant |plaintext| == 0 ==> 0 == n
       invariant START_SEQUENCE_NUMBER <= sequenceNumber <= ENDFRAME_SEQUENCE_NUMBER
       invariant |regularFrames| == (sequenceNumber - START_SEQUENCE_NUMBER) as nat
@@ -294,7 +303,7 @@ module MessageBody {
     {
       :- Need(sequenceNumber < ENDFRAME_SEQUENCE_NUMBER, Types.AwsEncryptionSdkException(
                 message := "too many frames"));
-      var plaintextFrame := plaintext[n..n + header.body.frameLength as nat];
+      var plaintextFrame := plaintext[n..Add(n, header.body.frameLength as uint64)];
 
       //= compliance/client-apis/encrypt.txt#2.7
       //# *  If there are enough input plaintext bytes consumable to create a
@@ -314,7 +323,7 @@ module MessageBody {
       LemmaAddingNextRegularFrame(regularFrames, regularFrame);
       regularFrames := regularFrames + [regularFrame];
 
-      n := n + header.body.frameLength as nat;
+      n := Add(n, header.body.frameLength as uint64);
 
       //= compliance/client-apis/encrypt.txt#2.7.1
       //# Otherwise, this value MUST be 1 greater than
@@ -710,7 +719,7 @@ module MessageBody {
     assert |AESDecryptHistory| == 0;
     assert SumDecryptCalls(AESDecryptHistory) == plaintext;
 
-    for i := 0 to |body.regularFrames|
+    for i : uint64 := 0 to |body.regularFrames| as uint64
       // // The goal is to assert FramesEncryptPlaintext.
       // // But this requires the final frame e.g. a FramedMessage.
       // // So I decompose this into parts
@@ -734,7 +743,7 @@ module MessageBody {
 
       AESDecryptHistory := AESDecryptHistory + [Seq.Last(crypto.History.AESDecrypt)];
       assert Seq.Last(AESDecryptHistory) == Seq.Last(crypto.History.AESDecrypt);
-      assert crypto.History.AESDecrypt[i + |old(crypto.History.AESDecrypt)|].input.iv == body.regularFrames[i].iv;
+      assert crypto.History.AESDecrypt[i as nat + |old(crypto.History.AESDecrypt)|].input.iv == body.regularFrames[i].iv;
     }
 
     var finalPlaintextSegment :- DecryptFrame(body.finalFrame, key, crypto);
@@ -977,7 +986,7 @@ module MessageBody {
   }
   by method { // because Seq.DropLast makes a full copy
     var result : seq<uint8> := [];
-    for i := 0 to |frames|
+    for i : uint64 := 0 to |frames| as uint64
       invariant IsMessageRegularFrames(frames)
       invariant IsMessageRegularFrames(frames[..i])
       invariant result == WriteMessageRegularFrames(frames[..i])
@@ -1008,7 +1017,7 @@ module MessageBody {
     requires forall frame: Frames.Frame | frame in regularFrames :: frame.header == header
     requires buffer.bytes == continuation.bytes
     requires buffer.start <= continuation.start
-    requires 0 <= continuation.start <= |buffer.bytes|
+    requires 0 <= continuation.start as nat <= |buffer.bytes|
     requires CorrectlyReadRange(buffer, continuation, buffer.bytes[buffer.start..continuation.start])
     requires CorrectlyRead(buffer, Success(SuccessfulRead(regularFrames, continuation)), WriteMessageRegularFrames)
     decreases ENDFRAME_SEQUENCE_NUMBER as nat - |regularFrames|
@@ -1024,7 +1033,7 @@ module MessageBody {
     //# data), this operation MUST use the first 4 bytes of a frame to
     //# determine if the frame MUST be deserialized as a final frame
     //# (../data-format/message-body.md#final-frame) or regular frame
-    //# (../fata-format/message-body/md#regular-frame).
+    //# (../data-format/message-body/md#regular-frame).
     if (sequenceNumber.data != ENDFRAME_SEQUENCE_NUMBER) then
 
       //= compliance/client-apis/decrypt.txt#2.7.4
@@ -1043,13 +1052,15 @@ module MessageBody {
       //# Otherwise, this
       //# value MUST be 1 greater than the value of the sequence number
       //# of the previous frame.
-      :- Need(regularFrame.data.seqNum as nat == |regularFrames| + 1, Error("Sequence number out of order."));
-
+      SequenceIsSafeBecauseItIsInMemory(regularFrames);
+      :- Need(regularFrame.data.seqNum as uint64 == |regularFrames| as uint64 + 1, Error("Sequence number out of order."));
+      assert regularFrame.data.seqNum as nat == |regularFrames| + 1;
       LemmaAddingNextRegularFrame(regularFrames, regularFrame.data);
 
       var nextRegularFrames: MessageRegularFrames := regularFrames + [regularFrame.data];
 
       CorrectlyReadByteRange(buffer, continuation, WriteMessageRegularFrames(regularFrames));
+      assert CorrectlyReadRange(continuation, regularFrame.tail, Frames.WriteRegularFrame(regularFrame.data));
       AppendToCorrectlyReadByteRange(buffer, continuation, regularFrame.tail, Frames.WriteRegularFrame(regularFrame.data));
       assert buffer.bytes == continuation.bytes == regularFrame.tail.bytes by {
         reveal CorrectlyReadRange();
@@ -1097,10 +1108,11 @@ module MessageBody {
 
       var finalFrame :- Frames.ReadFinalFrame(continuation, header);
       :- Need(
-           finalFrame.data.seqNum as nat == |regularFrames| + 1,
+           finalFrame.data.seqNum as uint64 == |regularFrames| as uint64 + 1,
            Error("Sequence number out of order.")
          );
 
+      assert finalFrame.data.seqNum as nat == |regularFrames| + 1;
       assert MessageFramesAreMonotonic(regularFrames + [finalFrame.data]);
       assert MessageFramesAreForTheSameMessage(regularFrames + [finalFrame.data]);
 

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy

@@ -29,7 +29,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
   ):
     (ret: seq<uint8>)
   {
-    if |edks| == 0 then []
+    if |edks| as uint64 == 0 then []
     else
       WriteEncryptedDataKeys(Seq.DropLast(edks)) + WriteEncryptedDataKey(Seq.Last(edks))
   }
@@ -84,7 +84,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
     ensures CorrectlyRead(buffer, res, WriteEncryptedDataKeys)
     ensures res.Success? ==> count as nat == |res.value.data|
   {
-    if count as int > |accumulator| then
+    if count as uint64 > |accumulator| as uint64 then
       var SuccessfulRead(edk, newPos) :- ReadEncryptedDataKey(nextEdkStart);
       var nextAcc := accumulator + [edk];
       assert CorrectlyReadRange(buffer, newPos, WriteEncryptedDataKeys(nextAcc)) by {
@@ -106,7 +106,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
 
     if
       && maxEdks.Some?
-      && count as int > maxEdks.value as int
+      && count as int64 > maxEdks.value
     then
       //= compliance/client-apis/decrypt.txt#2.7.1
       //# If the number of encrypted data keys (../framework/