From 1d836c9747a2dad5711517615518d082a805bc0f Mon Sep 17 00:00:00 2001 From: seebees Date: Sat, 26 Oct 2024 06:43:00 -0700 Subject: [PATCH] Compatability things --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy | 2 +- .../dafny/DynamoDbEncryption/src/CompoundBeacon.dfy | 2 +- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 2 +- .../src/DynamoDbEncryptionBranchKeyIdSupplier.dfy | 2 +- DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy | 2 +- .../dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy | 2 +- ...ryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy | 2 +- DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy | 2 +- DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy | 2 +- DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy | 2 +- DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy | 2 +- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 2 +- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 +- 13 files changed, 13 insertions(+), 13 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy index 93fe32e16..6d423cc91 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index f2ff84f45..e8fc00e35 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index ab14f719f..5a4062999 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/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) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy index 4533b8def..c79ca3294 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy +++ b/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.") } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index e1211b76a..deea2dd2d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index 7244fa87a..f4a1eadc6 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy index 38ffa9db7..e2aef0b72 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy index dca910df0..f8c178764 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy index 8d44ee51e..6c7f537ee 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy index c0ab990f1..19533014a 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy index 60242e1e1..be8905c86 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy +++ b/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 diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 3bd397aa1..650e9fd21 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/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 diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 09a490d7d..647249e30 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/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