Compatability things

Author: seebees

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -19,7 +19,7 @@ module BaseBeacon {
 
   import DDB = ComAmazonawsDynamodbTypes
   import Prim = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import UTF8
   import SortedSets
   import TermLoc

DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

@@ -16,7 +16,7 @@ module CompoundBeacon {
   import opened DdbVirtualFields
 
   import Prim = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import UTF8
   import Seq
   import SortedSets

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -32,7 +32,7 @@ module SearchConfigToInfo {
   import CB = CompoundBeacon
   import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import MPT = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
 
   // convert configured SearchConfig to internal SearchInfo
   method Convert(outer : DynamoDbTableEncryptionConfig)

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy

@@ -70,7 +70,7 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
     // We expect this interface to be implemented in the native language,
     // so any errors thrown by the native implementation will appear as Opaque errors
     if err.Opaque? then
-      MPL.Opaque(obj:=err.obj)
+      MPL.Opaque(obj:=err.obj, alt_text:="")
     else
       MPL.AwsCryptographicMaterialProvidersException(message:="Unexpected error while getting Branch Key ID.")
   }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -21,7 +21,7 @@ module SearchableEncryptionInfo {
   import UTF8
   import opened Time
   import KeyStore = AwsCryptographyKeyStoreTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import Prim = AwsCryptographyPrimitivesTypes
   import MP = AwsCryptographyMaterialProvidersTypes
   import KeyStoreTypes = AwsCryptographyKeyStoreTypes

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -17,7 +17,7 @@ module BeaconTestFixtures {
   import DDBC = Com.Amazonaws.Dynamodb
   import KTypes = AwsCryptographyKeyStoreTypes
   import SI = SearchableEncryptionInfo
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MaterialProviders
   import MPT = AwsCryptographyMaterialProvidersTypes
   import SortedSets

DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

@@ -19,7 +19,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
   import Prim = AwsCryptographyPrimitivesTypes
   import StructuredEncryptionHeader
   import Random
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import Header = StructuredEncryptionHeader
   import Footer = StructuredEncryptionFooter
   import MaterialProviders

DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy

@@ -19,7 +19,7 @@ module StructuredEncryptionCrypt {
 
   import CMP = AwsCryptographyMaterialProvidersTypes
   import Prim = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import UTF8
   import Header = StructuredEncryptionHeader
   import HKDF

DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy

@@ -23,7 +23,7 @@ module StructuredEncryptionFooter {
   import opened StandardLibrary.UInt
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import Materials
   import Header = StructuredEncryptionHeader
 

DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy

@@ -9,7 +9,7 @@ module
 {
 
   import Operations = AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MaterialProviders
 
   function method DefaultStructuredEncryptionConfig(): StructuredEncryptionConfig

DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy

@@ -17,7 +17,7 @@ module TestHeader {
   import opened StructuredEncryptionHeader
   import opened StructuredEncryptionPaths
   import opened UTF8
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import AlgorithmSuites
   import Canonize
 

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

@@ -27,7 +27,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
   import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
   import KeyMaterial
   import UTF8
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import ParseJsonManifests
   import CreateInterceptedDDBClient
   import DynamoDbItemEncryptor

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -39,7 +39,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import SI = SearchableEncryptionInfo
   import MaterialProviders
   import MPT = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import ParseJsonManifests