diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml index af4af2ed2..1faa244b3 100644 --- a/.github/workflows/library_format.yml +++ b/.github/workflows/library_format.yml @@ -39,7 +39,7 @@ jobs: - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.8.0 with: - dafny-version: ${{ '4.2.0' }} + dafny-version: ${{ inputs.dafny }} - name: Check format of Java code et al run: | diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index 4700779b8..48fe485e0 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -143,7 +143,9 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald && output.value.branchKeyIdSupplier.ValidState() && output.value.branchKeyIdSupplier.Modifies !! {History} && fresh(output.value.branchKeyIdSupplier) - && fresh ( output.value.branchKeyIdSupplier.Modifies - Modifies - {History} - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) + && fresh ( output.value.branchKeyIdSupplier.Modifies + - Modifies - {History} + - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output) ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)] @@ -535,7 +537,9 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService && output.value.branchKeyIdSupplier.ValidState() && output.value.branchKeyIdSupplier.Modifies !! {History} && fresh(output.value.branchKeyIdSupplier) - && fresh ( output.value.branchKeyIdSupplier.Modifies - Modifies - {History} - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) + && fresh ( output.value.branchKeyIdSupplier.Modifies + - Modifies - {History} + - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output) ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)] { @@ -592,7 +596,9 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations { && ( output.Success? ==> && output.value.branchKeyIdSupplier.ValidState() && fresh(output.value.branchKeyIdSupplier) - && fresh ( output.value.branchKeyIdSupplier.Modifies - ModifiesInternalConfig(config) - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) + && fresh ( output.value.branchKeyIdSupplier.Modifies + - ModifiesInternalConfig(config) + - input.ddbKeyBranchKeyIdSupplier.Modifies ) ) ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output) 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..09f9393e2 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) @@ -137,14 +137,19 @@ module SearchConfigToInfo { else MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1)); - //= specification/searchable-encryption/search-config.md#key-store-cache - //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md) - //# MUST be created. - var input := MPT.CreateCryptographicMaterialsCacheInput( - cache := cacheType - ); - var maybeCache := mpl.CreateCryptographicMaterialsCache(input); - var cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e)); + var cache; + if cacheType.Shared? { + cache := cacheType.Shared; + } else { + //= specification/searchable-encryption/search-config.md#key-store-cache + //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md) + //# MUST be created. + var input := MPT.CreateCryptographicMaterialsCacheInput( + cache := cacheType + ); + var maybeCache := mpl.CreateCryptographicMaterialsCache(input); + cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e)); + } if config.multi? { :- Need(0 < config.multi.cacheTTL, E("Beacon Cache TTL must be at least 1.")); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index e1211b76a..92a730fad 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 @@ -71,11 +71,11 @@ module SearchableEncryptionInfo { //# MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation). var newKey :- GetBeaconKey(client, key, keysLeft[0]); reveal Seq.HasNoDuplicates(); - //= specification/searchable-encryption/search-config.md#get-beacon-key-materials - //# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated - //# with the [beacon key id](#beacon-key-id) equal to the `beacon key id` - //# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map - //# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key. + //= specification/searchable-encryption/search-config.md#get-beacon-key-materials + //# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated + //# with the [beacon key id](#beacon-key-id) equal to the `beacon key id` + //# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map + //# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key. output := GetHmacKeys(client, allKeys, keysLeft[1..], key, acc[keysLeft[0] := newKey]); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index 7244fa87a..bbf448e00 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 @@ -181,6 +181,9 @@ module BeaconTestFixtures { ensures output.keyStore.ValidState() ensures fresh(output.keyStore.Modifies) ensures output.version == 1 + ensures + && output.keySource.multi? + && output.keySource.multi.cache.None? { var store := GetKeyStore(); return BeaconVersion ( diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy index 1ffa8b553..b3a92716d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy @@ -759,62 +759,98 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService var tmps4 := set t4 | t4 in tmp3.search.value.versions; forall tmp4 :: tmp4 in tmps4 ==> tmp4.keyStore.ValidState() - modifies set tmps5 <- set t5 <- config.tableEncryptionConfigs.Values | true - && t5.keyring.Some? - :: t5.keyring.value, - obj <- tmps5.Modifies | obj in tmps5.Modifies :: obj - modifies set tmps6 <- set t6 <- config.tableEncryptionConfigs.Values | true - && t6.cmm.Some? - :: t6.cmm.value, - obj <- tmps6.Modifies | obj in tmps6.Modifies :: obj + requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values; + forall tmp5 :: tmp5 in tmps5 ==> + tmp5.search.Some? ==> + var tmps6 := set t6 | t6 in tmp5.search.value.versions; + forall tmp6 :: tmp6 in tmps6 ==> + tmp6.keySource.multi? ==> + tmp6.keySource.multi.cache.Some? ==> + tmp6.keySource.multi.cache.value.Shared? ==> + tmp6.keySource.multi.cache.value.Shared.ValidState() modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true - && t7.legacyOverride.Some? - :: t7.legacyOverride.value.encryptor, + && t7.keyring.Some? + :: t7.keyring.value, obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true - && t8.search.Some? - , t9 <- t8.search.value.versions :: t9.keyStore, + && t8.cmm.Some? + :: t8.cmm.value, obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj + modifies set tmps9 <- set t9 <- config.tableEncryptionConfigs.Values | true + && t9.legacyOverride.Some? + :: t9.legacyOverride.value.encryptor, + obj <- tmps9.Modifies | obj in tmps9.Modifies :: obj + modifies set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true + && t10.search.Some? + , t11 <- t10.search.value.versions | true + :: t11.keyStore, + obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj + modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true + && t12.search.Some? + , t13 <- t12.search.value.versions | true + && t13.keySource.multi? + && t13.keySource.multi.cache.Some? + && t13.keySource.multi.cache.value.Shared? + :: t13.keySource.multi.cache.value.Shared, + obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj ensures res.Success? ==> && fresh(res.value) && fresh(res.value.Modifies - - ( set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true - && t10.keyring.Some? - :: t10.keyring.value, - obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj - ) - ( set tmps11 <- set t11 <- config.tableEncryptionConfigs.Values | true - && t11.cmm.Some? - :: t11.cmm.value, - obj <- tmps11.Modifies | obj in tmps11.Modifies :: obj - ) - ( set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true - && t12.legacyOverride.Some? - :: t12.legacyOverride.value.encryptor, - obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj - ) - ( set tmps13 <- set t13 <- config.tableEncryptionConfigs.Values | true - && t13.search.Some? - , t14 <- t13.search.value.versions :: t14.keyStore, - obj <- tmps13.Modifies | obj in tmps13.Modifies :: obj + - ( set tmps14 <- set t14 <- config.tableEncryptionConfigs.Values | true + && t14.keyring.Some? + :: t14.keyring.value, + obj <- tmps14.Modifies | obj in tmps14.Modifies :: obj + ) - ( set tmps15 <- set t15 <- config.tableEncryptionConfigs.Values | true + && t15.cmm.Some? + :: t15.cmm.value, + obj <- tmps15.Modifies | obj in tmps15.Modifies :: obj + ) - ( set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true + && t16.legacyOverride.Some? + :: t16.legacyOverride.value.encryptor, + obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj + ) - ( set tmps17 <- set t17 <- config.tableEncryptionConfigs.Values | true + && t17.search.Some? + , t18 <- t17.search.value.versions | true + :: t18.keyStore, + obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj + ) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true + && t19.search.Some? + , t20 <- t19.search.value.versions | true + && t20.keySource.multi? + && t20.keySource.multi.cache.Some? + && t20.keySource.multi.cache.value.Shared? + :: t20.keySource.multi.cache.value.Shared, + obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj ) ) && fresh(res.value.History) && res.value.ValidState() - ensures var tmps15 := set t15 | t15 in config.tableEncryptionConfigs.Values; - forall tmp15 :: tmp15 in tmps15 ==> - tmp15.keyring.Some? ==> - tmp15.keyring.value.ValidState() - ensures var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values; - forall tmp16 :: tmp16 in tmps16 ==> - tmp16.cmm.Some? ==> - tmp16.cmm.value.ValidState() - ensures var tmps17 := set t17 | t17 in config.tableEncryptionConfigs.Values; - forall tmp17 :: tmp17 in tmps17 ==> - tmp17.legacyOverride.Some? ==> - tmp17.legacyOverride.value.encryptor.ValidState() - ensures var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values; - forall tmp18 :: tmp18 in tmps18 ==> - tmp18.search.Some? ==> - var tmps19 := set t19 | t19 in tmp18.search.value.versions; - forall tmp19 :: tmp19 in tmps19 ==> - tmp19.keyStore.ValidState() + ensures var tmps21 := set t21 | t21 in config.tableEncryptionConfigs.Values; + forall tmp21 :: tmp21 in tmps21 ==> + tmp21.keyring.Some? ==> + tmp21.keyring.value.ValidState() + ensures var tmps22 := set t22 | t22 in config.tableEncryptionConfigs.Values; + forall tmp22 :: tmp22 in tmps22 ==> + tmp22.cmm.Some? ==> + tmp22.cmm.value.ValidState() + ensures var tmps23 := set t23 | t23 in config.tableEncryptionConfigs.Values; + forall tmp23 :: tmp23 in tmps23 ==> + tmp23.legacyOverride.Some? ==> + tmp23.legacyOverride.value.encryptor.ValidState() + ensures var tmps24 := set t24 | t24 in config.tableEncryptionConfigs.Values; + forall tmp24 :: tmp24 in tmps24 ==> + tmp24.search.Some? ==> + var tmps25 := set t25 | t25 in tmp24.search.value.versions; + forall tmp25 :: tmp25 in tmps25 ==> + tmp25.keyStore.ValidState() + ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values; + forall tmp26 :: tmp26 in tmps26 ==> + tmp26.search.Some? ==> + var tmps27 := set t27 | t27 in tmp26.search.value.versions; + forall tmp27 :: tmp27 in tmps27 ==> + tmp27.keySource.multi? ==> + tmp27.keySource.multi.cache.Some? ==> + tmp27.keySource.multi.cache.value.Shared? ==> + tmp27.keySource.multi.cache.value.Shared.ValidState() // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result { 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/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy index 32c22df42..66169eea6 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy @@ -132,7 +132,7 @@ module StructuredEncryptionHeader { + SerializeLegend(legend) + SerializeContext(encContext) + SerializeDataKeys(dataKeys) - ) + ) { var context := SerializeContext(encContext); var keys := SerializeDataKeys(dataKeys); @@ -630,7 +630,7 @@ module StructuredEncryptionHeader { + k.keyProviderInfo + UInt16ToSeq(cipherSize) + k.ciphertext - ) + ) { UInt16ToSeq(|k.keyProviderId| as uint16) + k.keyProviderId 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/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs index a2a04f8ca..0044c6b7c 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs @@ -958,6 +958,11 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking); return converted; } + if (value.is_Shared) + { + converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared); + return converted; + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value) @@ -982,6 +987,10 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking)); } + if (value.IsSetShared()) + { + return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared)); + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(Dafny.ISequence value) @@ -1154,6 +1163,14 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(Dafny.ISequence value) { return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value); @@ -1324,6 +1341,18 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null; return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli)); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(Dafny.ISequence value) { return new string(value.Elements); diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs index 36226d34f..69852084b 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs @@ -5774,6 +5774,11 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking); return converted; } + if (value.is_Shared) + { + converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared); + return converted; + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value) @@ -5798,6 +5803,10 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking)); } + if (value.IsSetShared()) + { + return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared)); + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static int FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconBitLength(int value) @@ -5933,6 +5942,14 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S11_BeaconStyle__M8_partOnly(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPartOnly value) { return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S8_PartOnly(value); @@ -6039,6 +6056,18 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null; return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli)); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S8_PartOnly(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPartOnly value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PartOnly concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PartOnly)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly(); return converted; 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 diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs index d517f861e..009ce943e 100644 --- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs +++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs @@ -918,6 +918,11 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking); return converted; } + if (value.is_Shared) + { + converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared); + return converted; + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value) @@ -942,6 +947,10 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking)); } + if (value.IsSetShared()) + { + return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared)); + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(Dafny.ISequence value) @@ -1114,6 +1123,14 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(Dafny.ISequence value) { return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value); @@ -1284,6 +1301,18 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null; return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli)); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(Dafny.ISequence value) { return new string(value.Elements); diff --git a/project.properties b/project.properties index ecd5b08f4..421c38f5a 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,5 @@ projectJavaVersion=3.7.0-SNAPSHOT -mplDependencyJavaVersion=1.6.0 +mplDependencyJavaVersion=1.7.2-SNAPSHOT dafnyVersion=4.8.0 dafnyVerifyVersion=4.8.0 dafnyRuntimeJavaVersion=4.8.0 diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 66a04bf31..139f903e9 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 66a04bf31bcfd8fd514acea740d8e670ab565ed9 +Subproject commit 139f903e9ebfbb77ac6008f2b81b73565915835e diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index 98939e130..c47e0832b 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit 98939e130695095386059967509a19299dfac320 +Subproject commit c47e0832b9dfafaa112593dd493728823804cc9b