diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index ab14f719f..cfe918c88 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -50,6 +50,8 @@ module SearchConfigToInfo { //= type=implication //# Initialization MUST fail if the length of the list of [beacon versions](#beacon-version-initialization) is not 1. ensures outer.search.Some? && |outer.search.value.versions| != 1 ==> output.Failure? + + ensures ValidSearchConfig(outer.search) { if outer.search.None? { return Success(None); @@ -63,10 +65,43 @@ module SearchConfigToInfo { } predicate ValidBeaconVersion(config : BeaconVersion) + reads + if + && config.keySource.multi? + && config.keySource.multi.cache.Some? + && config.keySource.multi.cache.value.Shared? + then + {config.keySource.multi.cache.value.Shared as object} + config.keySource.multi.cache.value.Shared.Modifies + else {} { - config.keyStore.ValidState() + && config.keyStore.ValidState() + && ( + && config.keySource.multi? + && config.keySource.multi.cache.Some? + && config.keySource.multi.cache.value.Shared? + ==> + && config.keySource.multi.cache.value.Shared.ValidState() + ) } predicate ValidSearchConfig(config : Option) + reads + if config.Some? then + set + c <- config.value.versions | + && c.keySource.multi? + && c.keySource.multi.cache.Some? + && c.keySource.multi.cache.value.Shared? + :: c.keySource.multi.cache.value.Shared + else {}, + if config.Some? then + set + c <- config.value.versions | + && c.keySource.multi? + && c.keySource.multi.cache.Some? + && c.keySource.multi.cache.value.Shared?, + o <- c.keySource.multi.cache.value.Shared.Modifies + :: o + else {} { if config.None? then true 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/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index f44f59b6c..d604da9c8 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy @@ -30,8 +30,28 @@ module } predicate ValidWholeSearchConfig(config : ET.DynamoDbTablesEncryptionConfig) + reads + set + t <- config.tableEncryptionConfigs | + config.tableEncryptionConfigs[t].search.Some?, + c <- config.tableEncryptionConfigs[t].search.value.versions | + && c.keySource.multi? + && c.keySource.multi.cache.Some? + && c.keySource.multi.cache.value.Shared? + :: c.keySource.multi.cache.value.Shared, + set + t <- config.tableEncryptionConfigs | + config.tableEncryptionConfigs[t].search.Some?, + f <- config.tableEncryptionConfigs[t].search.value.versions | + && f.keySource.multi? + && f.keySource.multi.cache.Some? + && f.keySource.multi.cache.value.Shared?, + o <- f.keySource.multi.cache.value.Shared.Modifies + :: o { - forall t <- config.tableEncryptionConfigs :: SearchConfigToInfo.ValidSearchConfig(config.tableEncryptionConfigs[t].search) + forall t <- config.tableEncryptionConfigs + :: + && SearchConfigToInfo.ValidSearchConfig(config.tableEncryptionConfigs[t].search) } function TheModifies(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig) : set @@ -102,7 +122,98 @@ module && inputConfig.sortKeyName == internalConfig.sortKeyName } - method {:vcs_split_on_every_assert} DynamoDbEncryptionTransforms(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig) + + // predicate BiteMe( + // config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig + // ) + // reads + // // var tmps27 := set t27 | t27 in config.search.value.versions; + + // set + // m <- config.tableEncryptionConfigs.Values | m.search.Some?, + // sv <- m.search.value.versions | + // && sv.keySource.multi? + // && sv.keySource.multi.cache.Some? + // && sv.keySource.multi.cache.value.Shared? + // :: + // sv.keySource.multi.cache.value.Shared, + // set + // m <- config.tableEncryptionConfigs.Values | m.search.Some?, + // sv <- m.search.value.versions | + // && sv.keySource.multi? + // && sv.keySource.multi.cache.Some? + // && sv.keySource.multi.cache.value.Shared?, + // o <- sv.keySource.multi.cache.value.Shared.Modifies + // :: + // o + // // s <- m.search.value | m.search.value.keySource.multi?, + // // c <- s.keySource.multi.cache | s.keySource.multi.cache.Some? && s.keySource.multi.cache.value.Shared? + // // :: + // // c.keySource.multi.cache.value.Shared.Modifies + + // { + // 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() + // } + + + // //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#dynamodb-table-encryption-configs + // //# During initialization, this client MUST construct a + // //# [DynamoDb Item Encryptor](./ddb-table-encryption-config.md) + // //# per configured table, using these table encryption configs. + // var m' := config.tableEncryptionConfigs; + // var mKeys := m'.Keys; + // var tableNamesSeq := SortedSets.ComputeSetToSequence(mKeys); + // ghost var mKeysSet := mKeys; + + // ghost var inputConfigsModifies: set := set + // tableConfig <- config.tableEncryptionConfigs.Values, + // o <- ( + // (if tableConfig.keyring.Some? then tableConfig.keyring.value.Modifies else {}) + // + (if tableConfig.cmm.Some? then tableConfig.cmm.value.Modifies else {}) + // + (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {}) + // ) + // :: o; + + // var allLogicalTableNames := {}; + // var i := 0; + + // while i < |tableNamesSeq| + // invariant m'.Keys <= config.tableEncryptionConfigs.Keys + // invariant forall k <- m' :: m'[k] == config.tableEncryptionConfigs[k] + // invariant forall internalConfig <- internalConfigs.Values :: internalConfig.logicalTableName in allLogicalTableNames + + // invariant CorrectlyTransferedStructure?(internalConfigs, config) + // invariant AllTableConfigsValid?(internalConfigs) + // invariant ValidConfig?(Config(internalConfigs)) + + // // invariant BiteMe(config) + + // modifies inputConfigsModifies + // { + // var tableName: string := tableNamesSeq[i]; + + // var inputConfig := config.tableEncryptionConfigs[tableName]; + // :- Need(inputConfig.logicalTableName !in allLogicalTableNames, E("Duplicate logical table maped to multipule physical tables: " + inputConfig.logicalTableName)); + + // assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search) by { + // assert ValidWholeSearchConfig(config); + // assert inputConfig in config.tableEncryptionConfigs.Values; + // } + // } + // } + + method {:vcs_split_on_every_assert} {:only} DynamoDbEncryptionTransforms(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig) returns (res: Result) //= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#logical-table-name //= type=implication @@ -115,6 +226,11 @@ module { var internalConfigs: map := map[]; assert ValidWholeSearchConfig(config); + + // assert BiteMe(config) by { + + // } + //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#dynamodb-table-encryption-configs //# During initialization, this client MUST construct a //# [DynamoDb Item Encryptor](./ddb-table-encryption-config.md) @@ -145,6 +261,8 @@ module invariant AllTableConfigsValid?(internalConfigs) invariant ValidConfig?(Config(internalConfigs)) + invariant ValidWholeSearchConfig(config) + modifies inputConfigsModifies { var tableName: string := tableNamesSeq[i]; @@ -229,6 +347,7 @@ module } i := i + 1; + assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search); } assert SearchValidState(DdbMiddlewareConfig.Config(tableEncryptionConfigs := internalConfigs)); @@ -236,49 +355,61 @@ module assert Operations.ValidInternalConfig?(newConfig); var client := new DynamoDbEncryptionTransformsClient(newConfig); + // assert BiteMe(config); + // I'm really sorry, but I can't get the freshness to verify // and my time box has run out of time. assume {:axiom} fresh( - client.Modifies - - ( var tmps14 := set t14 | t14 in config.tableEncryptionConfigs.Values - && t14.keyring.Some? - :: t14.keyring.value; - var tmps14FlattenedModifiesSet: set> := set t0 - | t0 in tmps14 :: t0.Modifies; - (set tmp15ModifyEntry, tmp15Modifies | - tmp15Modifies in tmps14FlattenedModifiesSet - && tmp15ModifyEntry in tmp15Modifies - :: tmp15ModifyEntry) - ) - ( var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values - && t16.cmm.Some? - :: t16.cmm.value; - var tmps16FlattenedModifiesSet: set> := set t0 - | t0 in tmps16 :: t0.Modifies; - (set tmp17ModifyEntry, tmp17Modifies | - tmp17Modifies in tmps16FlattenedModifiesSet - && tmp17ModifyEntry in tmp17Modifies - :: tmp17ModifyEntry) - ) - ( var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values - && t18.legacyOverride.Some? - :: t18.legacyOverride.value.encryptor; - var tmps18FlattenedModifiesSet: set> := set t0 - | t0 in tmps18 :: t0.Modifies; - (set tmp19ModifyEntry, tmp19Modifies | - tmp19Modifies in tmps18FlattenedModifiesSet - && tmp19ModifyEntry in tmp19Modifies - :: tmp19ModifyEntry) - ) - ( var tmps20 := set t20 | t20 in config.tableEncryptionConfigs.Values - && t20.search.Some? - :: set t21 | t21 in t20.search.value.versions :: t21.keyStore; - var tmps20FlattenedModifiesSet: set> := set t0 - , t1 | t0 in tmps20 && t1 in t0 :: t1.Modifies; - (set tmp22ModifyEntry, tmp22Modifies | - tmp22Modifies in tmps20FlattenedModifiesSet - && tmp22ModifyEntry in tmp22Modifies - :: tmp22ModifyEntry) - ) ); - - return Success(client); + client.Modifies + - ( var tmps14 := set t14 | t14 in config.tableEncryptionConfigs.Values + && t14.keyring.Some? + :: t14.keyring.value; + var tmps14FlattenedModifiesSet: set> := set t0 + | t0 in tmps14 :: t0.Modifies; + (set tmp15ModifyEntry, tmp15Modifies | + tmp15Modifies in tmps14FlattenedModifiesSet + && tmp15ModifyEntry in tmp15Modifies + :: tmp15ModifyEntry) + ) - ( var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values + && t16.cmm.Some? + :: t16.cmm.value; + var tmps16FlattenedModifiesSet: set> := set t0 + | t0 in tmps16 :: t0.Modifies; + (set tmp17ModifyEntry, tmp17Modifies | + tmp17Modifies in tmps16FlattenedModifiesSet + && tmp17ModifyEntry in tmp17Modifies + :: tmp17ModifyEntry) + ) - ( var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values + && t18.legacyOverride.Some? + :: t18.legacyOverride.value.encryptor; + var tmps18FlattenedModifiesSet: set> := set t0 + | t0 in tmps18 :: t0.Modifies; + (set tmp19ModifyEntry, tmp19Modifies | + tmp19Modifies in tmps18FlattenedModifiesSet + && tmp19ModifyEntry in tmp19Modifies + :: tmp19ModifyEntry) + ) - ( var tmps20 := set t20 | t20 in config.tableEncryptionConfigs.Values + && t20.search.Some? + :: set t21 | t21 in t20.search.value.versions :: t21.keyStore; + var tmps20FlattenedModifiesSet: set> := set t0 + , t1 | t0 in tmps20 && t1 in t0 :: t1.Modifies; + (set tmp22ModifyEntry, tmp22Modifies | + tmp22Modifies in tmps20FlattenedModifiesSet + && tmp22ModifyEntry in tmp22Modifies + :: tmp22ModifyEntry) + ) ); + + res := Success(client); + + // var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values; + // assert 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(); } // lemma ConstructionOK(config : DdbMiddlewareConfig.Config) 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/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 62662e92f..2904c981f 100644 --- a/project.properties +++ b/project.properties @@ -1,6 +1,6 @@ projectJavaVersion=3.7.0-SNAPSHOT -mplDependencyJavaVersion=1.6.0 +mplDependencyJavaVersion=1.7.0 dafnyVersion=4.8.0 -dafnyVerifyVersion=4.8.0 +dafnyVerifyVersion=4.8.1 dafnyRuntimeJavaVersion=4.8.0 smithyDafnyJavaConversionVersion=0.1 diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 66a04bf31..ea0fe508d 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 66a04bf31bcfd8fd514acea740d8e670ab565ed9 +Subproject commit ea0fe508dca214b9c9bdaf0fc21122e83971ef1b diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index 98939e130..55c68f474 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit 98939e130695095386059967509a19299dfac320 +Subproject commit 55c68f474d8dadd767a312781bc6fd78f922ada6