chore(dafny): further performance enhancements (#1834)

* chore(dafny): further performance enhancements

Author: ajewellamz

.github/workflows/ci_test_vector_net.yml

@@ -89,7 +89,7 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./${{matrix.library}}/runtimes/net
         run: |
-          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json .
+          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json ../java/large_records.json .
           dotnet run
           cp ../java/*.json .
           dotnet run --framework net6.0

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -9,6 +9,7 @@ include "DDBSupport.dfy"
 include "DynamoDbEncryptionBranchKeyIdSupplier.dfy"
 include "DynamoToStruct.dfy"
 include "FilterExpr.dfy"
+include "MemoryMath.dfy"
 include "NormalizeNumber.dfy"
 include "SearchInfo.dfy"
 include "TermLoc.dfy"

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy

@@ -0,0 +1,38 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+// When dealing with actual data in actual memory, we can be confident that
+// none of the numbers will exceed an exabyte, so we can use uint64, rather than nat.
+// To convince Dafny that this is true, we have the following functions
+// with assumptions as needed.
+
+
+include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy"
+
+module {:options "--function-syntax:4"} MemoryMath {
+
+  import opened BoundedInts
+
+
+  // This is safe because it is being held in memory
+  lemma {:axiom} ValueIsSafeBecauseItIsInMemory(value : nat)
+    ensures value < UINT64_MAX as nat
+
+  function {:opaque} Add(x : uint64, y : uint64) : (ret : uint64)
+    ensures ret < UINT64_MAX as uint64
+    ensures ret as nat == x as nat + y as nat
+  {
+    ValueIsSafeBecauseItIsInMemory(x as nat + y as nat);
+    x + y
+  }
+
+  function {:opaque} Add3(x : uint64, y : uint64, z : uint64) : (ret : uint64)
+    ensures ret < UINT64_MAX as uint64
+    ensures ret as nat == x as nat + y as nat + z as nat
+  {
+    ValueIsSafeBecauseItIsInMemory(x as nat + y as nat + z as nat);
+    x + y + z
+  }
+
+
+}

DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy

@@ -223,6 +223,25 @@ module SearchableEncryptionInfo {
       return Success(keyLoc.keys);
     }
 
+    function method PosLongAdd(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong
+    {
+      assert MP.IsValid_PositiveLong(x);
+      assert MP.IsValid_PositiveLong(y);
+      if x as nat + y as nat < INT64_MAX_LIMIT then
+        x + y
+      else
+        INT64_MAX_LIMIT as MP.PositiveLong
+    }
+    function method PosLongSub(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong
+    {
+      assert MP.IsValid_PositiveLong(x);
+      assert MP.IsValid_PositiveLong(y);
+      if x <= y then
+        0
+      else
+        x - y
+    }
+
     // Checks if (time_now - cache creation time of the extracted cache entry) is less than the allowed
     // TTL of the current Beacon Key Source calling the getEntry method from the cache.
     // Mitigates risk if another Beacon Key Source wrote the entry with a longer TTL.
@@ -232,7 +251,10 @@ module SearchableEncryptionInfo {
       ttlSeconds: MP.PositiveLong
     ): (output: bool)
     {
-      now - creationTime <= ttlSeconds as MP.PositiveLong
+      if now <= creationTime then
+        true
+      else
+        PosLongSub(now, creationTime) <= ttlSeconds as MP.PositiveLong
     }
 
     method getKeysCache(
@@ -406,7 +428,6 @@ module SearchableEncryptionInfo {
         var keyMap :- getAllKeys(stdNames, key.value);
         var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
 
-        expect now < UInt.BoundedInts.INT64_MAX - cacheTTL;
         //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
         //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
         //# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
@@ -415,7 +436,7 @@ module SearchableEncryptionInfo {
           identifier := cacheDigest,
           materials := MP.Materials.BeaconKey(beaconKeyMaterials),
           creationTime := now,
-          expiryTime := now + cacheTTL,
+          expiryTime := PosLongAdd(now, cacheTTL),
           messagesUsed := None,
           bytesUsed := None
         );

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -14,7 +14,7 @@ module DynamoDbEncryptionUtil {
   const BeaconPrefix := "aws_dbe_b_"
   const VersionPrefix := "aws_dbe_v_"
 
-  const MAX_STRUCTURE_DEPTH := 32
+  const MAX_STRUCTURE_DEPTH : uint64 := 32
   const MAX_STRUCTURE_DEPTH_STR := "32"
 
   type HmacKeyMap = map<string, Bytes>

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -417,6 +417,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     ensures version == 1 <==> ret == CSE.SIGN_ONLY
     ensures version == 2 <==> ret == CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
   {
+    assert StructuredEncryptionHeader.ValidVersion(version);
+    assert version == 1 || version == 2;
     if version == 2 then
       CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
     else
@@ -546,7 +548,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   // get CryptoSchema for this item
   function method ConfigToCryptoSchema(
     config : InternalConfig,
-    item : ComAmazonawsDynamodbTypes.AttributeMap)
+    item : DynamoToStruct.TerminalDataMap)
     : (ret : Result<CSE.CryptoSchemaMap, DDBE.Error>)
 
     //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
@@ -590,7 +592,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   // get AuthenticateSchema for this item
   function method ConfigToAuthenticateSchema(
     config : InternalConfig,
-    item : ComAmazonawsDynamodbTypes.AttributeMap)
+    item : DynamoToStruct.TerminalDataMap)
     : (ret : CSE.AuthenticateSchemaMap)
     requires ValidInternalConfig?(config)
 
@@ -636,6 +638,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     ensures ret.Success? ==> forall k <- ret.value.Keys :: InSignatureScope(config, k)
     ensures ret.Success? ==> forall k <- ret.value.Keys :: !ret.value[k].DO_NOTHING?
   {
+    assert forall k <- schema :: SE.IsAuthAttr(schema[k]);
+    assert forall k <- schema :: !schema[k].DO_NOTHING?;
     :- Need(forall k <- schema :: InSignatureScope(config, k),
             DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope"));
     :- Need(forall k <- schema :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k),
@@ -747,22 +751,22 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         && (|config.structuredEncryption.History.EncryptStructure| == |old(config.structuredEncryption.History.EncryptStructure)| + 1)
         && (Seq.Last(config.structuredEncryption.History.EncryptStructure).output.Success?)
 
-        //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
-        //= type=implication
-        //# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema)
-        //# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions).
-        && ConfigToCryptoSchema(config, input.plaintextItem).Success?
-        && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema
-           == ConfigToCryptoSchema(config, input.plaintextItem).value
-
         //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
         //= type=implication
         //# - Structured Data MUST be the Structured Data converted above.
-        && DynamoToStruct.ItemToStructured(input.plaintextItem).Success?
-        && var plaintextStructure := DynamoToStruct.ItemToStructured(input.plaintextItem).value;
+        && DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).Success?
+        && var plaintextStructure := DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).value;
         && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.plaintextStructure
            == plaintextStructure
 
+        //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
+        //= type=implication
+        //# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema)
+        //# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions).
+        && ConfigToCryptoSchema(config, plaintextStructure).Success?
+        && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema
+           == ConfigToCryptoSchema(config, plaintextStructure).value
+
         //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
         //= type=implication
         //# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context).
@@ -800,8 +804,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       ==>
         && output.value.encryptedItem == input.plaintextItem
         && output.value.parsedHeader == None
-
-    ensures output.Success? ==> |input.plaintextItem| <= MAX_ATTRIBUTE_COUNT
   {
     :- Need(
       && config.partitionKeyName in input.plaintextItem
@@ -811,12 +813,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     :- Need(ContextAttrsExist(config.attributeActionsOnEncrypt, input.plaintextItem),
             E(ContextMissingMsg(config.attributeActionsOnEncrypt, input.plaintextItem)));
 
-    if |input.plaintextItem| > MAX_ATTRIBUTE_COUNT {
-      var actCount := String.Base10Int2String(|input.plaintextItem|);
-      var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT);
-      return Failure(E("Item to encrypt had " + actCount + " attributes, but maximum allowed is " + maxCount));
-    }
-
     //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
     //# If a [Legacy Policy](./ddb-table-encryption-config.md#legacy-policy) of
     //# `FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT` is specified,
@@ -839,10 +835,10 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       return Success(passthroughOutput);
     }
 
-    var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem)
+    var plaintextStructure :- DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
     var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure);
-    var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem)
+    var cryptoSchema :- ConfigToCryptoSchema(config, plaintextStructure)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
@@ -893,7 +889,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
     var encryptedData := encryptVal.encryptedStructure;
     :- Need(forall k <- encryptedData :: DDB.IsValid_AttributeName(k), E(""));
-    var ddbKey :- DynamoToStruct.StructuredToItem(encryptedData)
+    var ddbKey :- DynamoToStruct.StructuredToItemEncrypt(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     var parsedActions :- ConvertCryptoSchemaToAttributeActions(config, encryptVal.cryptoSchema);
@@ -957,21 +953,21 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         && (|config.structuredEncryption.History.DecryptStructure| == |old(config.structuredEncryption.History.DecryptStructure)| + 1)
         && (Seq.Last(config.structuredEncryption.History.DecryptStructure).output.Success?)
 
-        //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
-        //= type=implication
-        //# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema)
-        //# built with the following requirements:
-        && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema
-           == ConfigToAuthenticateSchema(config, input.encryptedItem)
-
         //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
         //= type=implication
         //# - Encrypted Structured Data MUST be the Structured Data converted above.
-        && DynamoToStruct.ItemToStructured(input.encryptedItem).Success?
-        && var plaintextStructure := DynamoToStruct.ItemToStructured(input.encryptedItem).value;
+        && DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).Success?
+        && var plaintextStructure := DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).value;
         && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptedStructure
            == plaintextStructure
 
+        //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
+        //= type=implication
+        //# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema)
+        //# built with the following requirements:
+        && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema
+           == ConfigToAuthenticateSchema(config, plaintextStructure)
+
         //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
         //= type=implication
         //# The item to be encrypted MUST have an attribute named `aws_dbe_head`.
@@ -1037,13 +1033,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         && output.value.plaintextItem == input.encryptedItem
         && output.value.parsedHeader == None
   {
-    var realCount := |set k <- input.encryptedItem | !(ReservedPrefix <= k)|;
-    if realCount > MAX_ATTRIBUTE_COUNT {
-      var actCount := String.Base10Int2String(realCount);
-      var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT);
-      return Failure(E("Item to decrypt had " + actCount + " attributes, but maximum allowed is " + maxCount));
-    }
-
     :- Need(
       && config.partitionKeyName in input.encryptedItem
       && (config.sortKeyName.None? || config.sortKeyName.value in input.encryptedItem)
@@ -1081,15 +1070,15 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
             DynamoDbItemEncryptorException(
               message := "Encrypted item missing expected header and footer attributes"));
 
-    var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem)
+    var encryptedStructure :- DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
     :- Need(SE.HeaderField in input.encryptedItem, E("Header field, \"aws_dbe_head\", not in item."));
     var header := input.encryptedItem[SE.HeaderField];
     :- Need(header.B?, E("Header field, \"aws_dbe_head\", not binary"));
     assert header.B?;
     :- Need(0 < |header.B|, E("Unexpected empty header field."));
     var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
-    var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem);
+    var authenticateSchema := ConfigToAuthenticateSchema(config, encryptedStructure);
 
     //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
     //# This operation MUST create a
@@ -1123,7 +1112,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
     var decryptedData := decryptVal.plaintextStructure;
     :- Need(forall k <- decryptedData :: DDB.IsValid_AttributeName(k), E(""));
-    var ddbItem :- DynamoToStruct.StructuredToItem(decryptedData)
+    var ddbItem :- DynamoToStruct.StructuredToItemDecrypt(decryptedData, input.encryptedItem, decryptVal.cryptoSchema)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     var schemaToConvert := decryptVal.cryptoSchema;

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -14,11 +14,11 @@ module DynamoDbItemEncryptorUtil {
   import SortedSets
   import SE = StructuredEncryptionUtil
   import DynamoToStruct
+  import MemoryMath
 
   const ReservedPrefix := "aws_dbe_"
   const BeaconPrefix := ReservedPrefix + "b_"
   const VersionPrefix := ReservedPrefix + "v_"
-  const MAX_ATTRIBUTE_COUNT := 100
 
   function method E(msg : string) : Error
   {
@@ -181,7 +181,8 @@ module DynamoDbItemEncryptorUtil {
       Success(value)
     else if legend == SE.LEGEND_BINARY then
       var terminal :- SE.DecodeTerminal(ecValue);
-      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, false);
+      MemoryMath.ValueIsSafeBecauseItIsInMemory(|terminal.value|);
+      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint64));
       Success(ddbAttrValue.val)
     else
       Failure("Encryption Context Legend has unexpected character : '" + [legend] + "'.")
@@ -236,7 +237,8 @@ module DynamoDbItemEncryptorUtil {
 
     // Obtain attribute value from EC kvPair value
     var terminal :- SE.DecodeTerminal(encodedAttrValue);
-    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, false);
+    MemoryMath.ValueIsSafeBecauseItIsInMemory(|terminal.value|);
+    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint64));
 
     // Add to our AttributeMap
     Success(attrMap[ddbAttrName := ddbAttrValue.val])