chore: improve performance

.github/workflows/library_rust_tests.yml

@@ -202,9 +202,9 @@ jobs:
           unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0
 
       - name: Test Rust
-        working-directory: ${{ matrix.library }}
+        working-directory: ${{ matrix.library }}/runtimes/rust
         shell: bash
         run: |
           # Without this, running test vectors fails due to `fatal runtime error: stack overflow`
           export RUST_MIN_STACK=104857600
-          make test_rust
+          cargo test --release -- --test-threads 1 --nocapture

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy

@@ -147,6 +147,27 @@ module MessageBody {
     && MessageFramesAreForTheSameMessage(regularFrames)
   }
 
+  lemma IsMessageRegularFramesCanBeSplit(
+    regularFrames: seq<Frames.RegularFrame>
+  )
+    requires IsMessageRegularFrames(regularFrames)
+    ensures forall accumulator
+              | accumulator <= regularFrames
+              ::
+                && IsMessageRegularFrames(accumulator)
+  {
+    forall accumulator
+      | accumulator <= regularFrames
+      ensures
+        && IsMessageRegularFrames(accumulator)
+    {
+      assert |accumulator| <= |regularFrames|;
+      assert 0 <= |accumulator| < ENDFRAME_SEQUENCE_NUMBER as nat;
+      assume {:axiom} MessageFramesAreMonotonic(accumulator);
+      assert MessageFramesAreForTheSameMessage(accumulator);
+    }
+  }
+
   type NonFramedMessage = Frames.NonFramed
 
   datatype FramedMessageBody = FramedMessageBody(
@@ -939,7 +960,7 @@ module MessageBody {
     WriteMessageRegularFrames(body.regularFrames) + Frames.WriteFinalFrame(body.finalFrame)
   }
 
-  function method WriteMessageRegularFrames(
+  function WriteMessageRegularFrames(
     frames: MessageRegularFrames
   )
     :(ret: seq<uint8>)
@@ -954,6 +975,28 @@ module MessageBody {
       WriteMessageRegularFrames(Seq.DropLast(frames))
       + Frames.WriteRegularFrame(Seq.Last(frames))
   }
+  by method { // because Seq.DropLast makes a full copy
+    var result : seq<uint8> := [];
+    for i := 0 to |frames|
+      invariant IsMessageRegularFrames(frames)
+      invariant IsMessageRegularFrames(frames[..i])
+      invariant result == WriteMessageRegularFrames(frames[..i])
+    {
+      result := result + Frames.WriteRegularFrame(frames[i]);
+      assert result == WriteMessageRegularFrames(frames[..i]) + Frames.WriteRegularFrame(frames[i]);
+      assert Seq.DropLast(frames[..i+1]) == frames[..i];
+      assert result == WriteMessageRegularFrames(Seq.DropLast(frames[..i+1])) + Frames.WriteRegularFrame(Seq.Last(frames[..i+1]));
+      IsMessageRegularFramesCanBeSplit(frames);
+      assert IsMessageRegularFrames(frames[..i]);
+      assert IsMessageRegularFrames(frames[..i+1]);
+      assert result == WriteMessageRegularFrames(frames[..i+1]);
+
+    }
+    assert result == WriteMessageRegularFrames(frames[..|frames|]);
+    assert frames == frames[..|frames|];
+    assert result == WriteMessageRegularFrames(frames);
+    return result;
+  }
 
   function method {:recursive} {:vcs_split_on_every_assert} ReadFramedMessageBody(
     buffer: ReadableBuffer,

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

@@ -22,6 +22,8 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
     + WriteShortLengthSeq(edk.ciphertext)
   }
 
+  // Seq.DropLast makes a full copy, but we seldom have more than one or two data keys,
+  // so no point in optimizing away the copy.
   function {:tailrecursion} WriteEncryptedDataKeys(
     edks: ESDKEncryptedDataKeys
   ):

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

@@ -387,7 +387,7 @@ module {:options "/functionSyntax:4" } EncryptionContext {
     WriteUint16(|ec| as uint16) + WriteAADPairs(ec)
   }
 
-  function {:tailrecursion} WriteAADPairs(
+  function WriteAADPairs(
     ec: ESDKCanonicalEncryptionContext
   ):
     (ret: seq<uint8>)
@@ -406,6 +406,28 @@ module {:options "/functionSyntax:4" } EncryptionContext {
       assert LinearLength(Seq.DropLast(ec)) < LinearLength(ec);
       WriteAADPairs(Seq.DropLast(ec)) + WriteAADPair(Seq.Last(ec))
   }
+  by method { // because Seq.DropLast makes a full copy
+    var result : seq<uint8> := [];
+    for i := 0 to |ec|
+      invariant ESDKCanonicalEncryptionContext?(ec)
+      invariant ESDKCanonicalEncryptionContext?(ec[..i])
+      invariant result == WriteAADPairs(ec[..i])
+    {
+      result := result + WriteAADPair(ec[i]);
+      ESDKCanonicalEncryptionContextCanBeSplit(ec);
+      assert result == WriteAADPairs(ec[..i]) + WriteAADPair(ec[i]);
+      assert Seq.DropLast(ec[..i+1]) == ec[..i];
+      assert result == WriteAADPairs(Seq.DropLast(ec[..i+1])) + WriteAADPair(Seq.Last(ec[..i+1]));
+      assert ESDKCanonicalEncryptionContext?(ec[..i]);
+      assert ESDKCanonicalEncryptionContext?(ec[..i+1]);
+      assert result == WriteAADPairs(ec[..i+1]);
+
+    }
+    assert result == WriteAADPairs(ec[..|ec|]);
+    assert ec == ec[..|ec|];
+    assert result == WriteAADPairs(ec);
+    return result;
+  }
 
   //= compliance/data-format/message-header.txt#2.5.1.7.2.2
   //# The following table describes the fields that form each key value

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

@@ -149,7 +149,7 @@ module SerializableTypes {
           ==> pairs[i].key != pairs[j].key)
   }
 
-  function method {:tailrecursion} LinearLength(
+  function LinearLength(
     pairs: Linear<UTF8.ValidUTF8Bytes, UTF8.ValidUTF8Bytes>
   ):
     (ret: nat)
@@ -162,6 +162,24 @@ module SerializableTypes {
     else
       LinearLength(Seq.DropLast(pairs)) + PairLength(Seq.Last(pairs))
   }
+  by method { // because Seq.DropLast makes a full copy
+    var result : nat := 0;
+    for i := 0 to |pairs|
+      invariant result == LinearLength(pairs[..i])
+    {
+      result := result + PairLength(pairs[i]);
+      assert result == LinearLength(pairs[..i]) + PairLength(pairs[i]);
+      assert Seq.DropLast(pairs[..i+1]) == pairs[..i];
+      assert result == LinearLength(Seq.DropLast(pairs[..i+1])) + PairLength(Seq.Last(pairs[..i+1]));
+      assert result == LinearLength(pairs[..i+1]);
+
+    }
+    assert result == LinearLength(pairs[..|pairs|]);
+    assert pairs == pairs[..|pairs|];
+    assert result == LinearLength(pairs);
+    return result;
+  }
+
 
   function method PairLength(
     pair: Pair<UTF8.ValidUTF8Bytes, UTF8.ValidUTF8Bytes>