m

Author: josecorella

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy

@@ -237,31 +237,31 @@ module TestFixtures {
     assume {:axiom} fresh(encryption.Modifies);
   }
 
-  method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
-    returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
-    ensures encryption.ValidState()
-    ensures fresh(encryption)
-    ensures fresh(encryption.Modifies)
-  {
-    var keyring := GetKmsKeyring();
-    encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
-      DynamoDbTablesEncryptionConfig(
-        tableEncryptionConfigs := map[
-          "foo" := DynamoDbTableEncryptionConfig(
-            logicalTableName := "foo",
-            partitionKeyName := "bar",
-            sortKeyName := sortKey,
-            attributeActionsOnEncrypt := actions,
-            allowedUnsignedAttributes := Some(["plain"]),
-            allowedUnsignedAttributePrefix := None(),
-            algorithmSuiteId := None(),
-            keyring := Some(keyring)
-          )
-        ]
-      )
-    );
-    assume {:axiom} fresh(encryption.Modifies);
-  }
+  // method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
+  //   returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
+  //   ensures encryption.ValidState()
+  //   ensures fresh(encryption)
+  //   ensures fresh(encryption.Modifies)
+  // {
+  //   var keyring := GetKmsKeyring();
+  //   encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
+  //     DynamoDbTablesEncryptionConfig(
+  //       tableEncryptionConfigs := map[
+  //         "foo" := DynamoDbTableEncryptionConfig(
+  //           logicalTableName := "foo",
+  //           partitionKeyName := "bar",
+  //           sortKeyName := sortKey,
+  //           attributeActionsOnEncrypt := actions,
+  //           allowedUnsignedAttributes := Some(["plain"]),
+  //           allowedUnsignedAttributePrefix := None(),
+  //           algorithmSuiteId := None(),
+  //           keyring := Some(keyring)
+  //         )
+  //       ]
+  //     )
+  //   );
+  //   assume {:axiom} fresh(encryption.Modifies);
+  // }
 
   // type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
 

SharedMakefile.mk

@@ -13,9 +13,9 @@ include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 
 VERIFY_TIMEOUT := 250
 
-verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts
-verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts
-verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts
+verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
 
 transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
 transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts