chore(dafny): further performance enhancements

.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/SearchInfo.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/Util.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 : uint32 := 32
   const MAX_STRUCTURE_DEPTH_STR := "32"
 
   type HmacKeyMap = map<string, Bytes>

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.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/Util.dfy

@@ -18,7 +18,7 @@ module DynamoDbItemEncryptorUtil {
   const ReservedPrefix := "aws_dbe_"
   const BeaconPrefix := ReservedPrefix + "b_"
   const VersionPrefix := ReservedPrefix + "v_"
-  const MAX_ATTRIBUTE_COUNT := 100
+  const UINT32_MAX : uint32 := 0xFFFF_FFFF
 
   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);
+      :- Need(|terminal.value| < UINT32_MAX as int, "LEGEND_BINARY too big");
+      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32));
       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);
+    :- Need(|terminal.value| < UINT32_MAX as int, "Attribute Value too big");
+    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32));
 
     // Add to our AttributeMap
     Success(attrMap[ddbAttrName := ddbAttrValue.val])

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy

@@ -109,7 +109,6 @@ module DynamoDbItemEncryptorTest {
       "sign4" := DDB.AttributeValue.NULL(true),
       "nothing" := DDBS("baz")
     ];
-    var expectedOutputItem := inputItem["bar" := DDB.AttributeValue.N("1234")];
 
     var encryptRes := encryptor.EncryptItem(
       Types.EncryptItemInput(
@@ -122,7 +121,7 @@ module DynamoDbItemEncryptorTest {
     }
     expect encryptRes.Success?;
     expect encryptRes.value.encryptedItem.Keys == inputItem.Keys + {SE.HeaderField, SE.FooterField};
-    expect encryptRes.value.encryptedItem["bar"] == expectedOutputItem["bar"]; // because normalized
+    expect encryptRes.value.encryptedItem["bar"] == inputItem["bar"];
     expect encryptRes.value.encryptedItem["encrypt"] != inputItem["encrypt"];
     expect encryptRes.value.encryptedItem["sign"] == inputItem["sign"];
     expect encryptRes.value.encryptedItem["sign3"] == inputItem["sign3"];
@@ -142,11 +141,11 @@ module DynamoDbItemEncryptorTest {
       print "\n", decryptRes.error, "\n";
     }
     expect decryptRes.Success?;
-    if decryptRes.value.plaintextItem != expectedOutputItem {
-      print "\nexpectedOutputItem :\n", expectedOutputItem, "\n";
+    if decryptRes.value.plaintextItem != inputItem {
+      print "\ninputItem :\n", inputItem, "\n";
       print "\nOutput Item :\n", decryptRes.value.plaintextItem, "\n";
     }
-    expect decryptRes.value.plaintextItem == expectedOutputItem;
+    expect decryptRes.value.plaintextItem == inputItem;
 
     var parsedHeader := decryptRes.value.parsedHeader;
     expect parsedHeader.Some?;
@@ -605,10 +604,10 @@ module DynamoDbItemEncryptorTest {
     expect parsedHeader.value.selectorContext == map["bar" := DDB.AttributeValue.S("key")];
   }
 
-  method {:test} TestMaxRoundTrip() {
+  method {:test} TestLargeRoundTrip() {
     var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
     var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
-    for i := 0 to (MAX_ATTRIBUTE_COUNT-1) {
+    for i := 0 to 500 {
       var str := String.Base10Int2String(i);
       expect DDB.IsValid_AttributeName(str);
       inputItem := inputItem[str := DDBS(str)];
@@ -649,26 +648,4 @@ module DynamoDbItemEncryptorTest {
     expect PublicKeyUtf8 in parsedHeader.value.storedEncryptionContext.Keys;
     expect |parsedHeader.value.encryptedDataKeys| == 1;
   }
-
-  method {:test} TestTooManyAttributes() {
-    var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
-    var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
-    for i := 0 to MAX_ATTRIBUTE_COUNT {
-      var str := String.Base10Int2String(i);
-      expect DDB.IsValid_AttributeName(str);
-      inputItem := inputItem[str := DDBS(str)];
-      actions := actions[str := CSE.ENCRYPT_AND_SIGN];
-    }
-    var config := TestFixtures.GetEncryptorConfigFromActions(actions);
-    var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config);
-
-    var encryptRes := encryptor.EncryptItem(
-      Types.EncryptItemInput(
-        plaintextItem:=inputItem
-      )
-    );
-
-    expect encryptRes.Failure?;
-    expect encryptRes.error == E("Item to encrypt had 101 attributes, but maximum allowed is 100");
-  }
 }