From 5849d8e12c8e092c150eb27639f7e5399553624c Mon Sep 17 00:00:00 2001 From: Shubham Chaturvedi Date: Mon, 20 Oct 2025 15:58:47 -0700 Subject: [PATCH 1/2] update submodules --- submodules/MaterialProviders | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 66a04bf31..70e580991 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 66a04bf31bcfd8fd514acea740d8e670ab565ed9 +Subproject commit 70e580991678387ce897a286c4f7f449aa616785 From 9cc29e39e6c35b613a39de1d2c6a010edb733a1b Mon Sep 17 00:00:00 2001 From: Shubham Chaturvedi Date: Mon, 20 Oct 2025 16:12:23 -0700 Subject: [PATCH 2/2] fix primitives --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy | 2 +- .../dafny/DynamoDbEncryption/src/CompoundBeacon.dfy | 2 +- .../dafny/DynamoDbEncryption/src/ConfigToInfo.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 +- 10 files changed, 10 insertions(+), 10 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/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index 810f880dc..e1299454f 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