Skip to content

Commit c396dfb

Browse files
robin-awsrobin-aws
committed
Pull latest smithy-dafny, regenerate, undo client changes
1 parent 55514fc commit c396dfb

File tree

27 files changed

+231
-192
lines changed

27 files changed

+231
-192
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

+3-3
Original file line numberDiff line numberDiff line change
@@ -453,17 +453,17 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
453453
import Operations : AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations
454454
function method DefaultDynamoDbEncryptionConfig(): DynamoDbEncryptionConfig
455455
method DynamoDbEncryption(config: DynamoDbEncryptionConfig := DefaultDynamoDbEncryptionConfig())
456-
returns (res: Result<IDynamoDbEncryptionClient, Error>)
456+
returns (res: Result<DynamoDbEncryptionClient, Error>)
457457
ensures res.Success? ==>
458458
&& fresh(res.value)
459459
&& fresh(res.value.Modifies)
460460
&& fresh(res.value.History)
461461
&& res.value.ValidState()
462462

463-
// Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
463+
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
464464
function method CreateSuccessOfClient(client: IDynamoDbEncryptionClient): Result<IDynamoDbEncryptionClient, Error> {
465465
Success(client)
466-
} // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
466+
}
467467
function method CreateFailureOfError(error: Error): Result<IDynamoDbEncryptionClient, Error> {
468468
Failure(error)
469469
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

+1-4
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ module SearchConfigToInfo {
3232
import CB = CompoundBeacon
3333
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
3434
import MPT = AwsCryptographyMaterialProvidersTypes
35-
import PT = AwsCryptographyPrimitivesTypes
3635
import Aws.Cryptography.Primitives
3736

3837
// convert configured SearchConfig to internal SearchInfo
@@ -180,9 +179,7 @@ module SearchConfigToInfo {
180179
:- Need(0 < |config.standardBeacons|, E("At least one standard beacon must be configured."));
181180

182181
var maybePrimitives := Primitives.AtomicPrimitives();
183-
var primitivesX: PT.IAwsCryptographicPrimitivesClient :- maybePrimitives.MapFailure(e => AwsCryptographyPrimitives(e));
184-
assert primitivesX is Primitives.AtomicPrimitivesClient;
185-
var primitives := primitivesX as Primitives.AtomicPrimitivesClient;
182+
var primitives :- maybePrimitives.MapFailure(e => AwsCryptographyPrimitives(e));
186183
var source :- MakeKeySource(outer, config.keyStore, config.keySource, primitives);
187184
output := ConvertVersionWithSource(outer, config, source);
188185
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

+1-4
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,9 @@ module TestBaseBeacon {
1717
import SI = SearchableEncryptionInfo
1818
import DDB = ComAmazonawsDynamodbTypes
1919
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
20-
import AwsCryptographyPrimitivesTypes
2120

2221
method {:test} TestBeacon() {
23-
var primitivesX: AwsCryptographyPrimitivesTypes.IAwsCryptographicPrimitivesClient :- expect Primitives.AtomicPrimitives();
24-
assert primitivesX is Primitives.AtomicPrimitivesClient;
25-
var primitives := primitivesX as Primitives.AtomicPrimitivesClient;
22+
var primitives :- expect Primitives.AtomicPrimitives();
2623

2724
var bb := BeaconBase(client := primitives, name := "foo", beaconName := "aws_dbe_b_foo");
2825
var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

+1-3
Original file line numberDiff line numberDiff line change
@@ -210,9 +210,7 @@ module BeaconTestFixtures {
210210
ensures version.keyStore == output.store
211211
ensures fresh(output.client.Modifies)
212212
{
213-
var clientX: AwsCryptographyPrimitivesTypes.IAwsCryptographicPrimitivesClient :- expect Primitives.AtomicPrimitives();
214-
assert clientX is Primitives.AtomicPrimitivesClient;
215-
var client := clientX as Primitives.AtomicPrimitivesClient;
213+
var client :- expect Primitives.AtomicPrimitives();
216214

217215
var keyNameSet := set b <- version.standardBeacons :: b.name;
218216
var keyNames := SortedSets.ComputeSetToOrderedSequence2(keyNameSet, CharLess);

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

+54-96
Original file line numberDiff line numberDiff line change
@@ -740,8 +740,7 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
740740
import Operations : AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations
741741
function method DefaultDynamoDbTablesEncryptionConfig(): AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig
742742
method DynamoDbEncryptionTransforms(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig := DefaultDynamoDbTablesEncryptionConfig())
743-
returns (res: Result<IDynamoDbEncryptionTransformsClient, Error>)
744-
// BEGIN MANUAL EDIT
743+
returns (res: Result<DynamoDbEncryptionTransformsClient, Error>)
745744
requires var tmps0 := set t0 | t0 in config.tableEncryptionConfigs.Values;
746745
forall tmp0 :: tmp0 in tmps0 ==>
747746
tmp0.keyring.Some? ==>
@@ -760,108 +759,67 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
760759
var tmps4 := set t4 | t4 in tmp3.search.value.versions;
761760
forall tmp4 :: tmp4 in tmps4 ==>
762761
tmp4.keyStore.ValidState()
763-
modifies var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values
764-
&& t5.keyring.Some?
765-
:: t5.keyring.value;
766-
var tmps5FlattenedModifiesSet: set<set<object>> := set t0
767-
| t0 in tmps5 :: t0.Modifies;
768-
(set tmp6ModifyEntry, tmp6Modifies |
769-
tmp6Modifies in tmps5FlattenedModifiesSet
770-
&& tmp6ModifyEntry in tmp6Modifies
771-
:: tmp6ModifyEntry)
772-
modifies var tmps7 := set t7 | t7 in config.tableEncryptionConfigs.Values
773-
&& t7.cmm.Some?
774-
:: t7.cmm.value;
775-
var tmps7FlattenedModifiesSet: set<set<object>> := set t0
776-
| t0 in tmps7 :: t0.Modifies;
777-
(set tmp8ModifyEntry, tmp8Modifies |
778-
tmp8Modifies in tmps7FlattenedModifiesSet
779-
&& tmp8ModifyEntry in tmp8Modifies
780-
:: tmp8ModifyEntry)
781-
modifies var tmps9 := set t9 | t9 in config.tableEncryptionConfigs.Values
782-
&& t9.legacyOverride.Some?
783-
:: t9.legacyOverride.value.encryptor;
784-
var tmps9FlattenedModifiesSet: set<set<object>> := set t0
785-
| t0 in tmps9 :: t0.Modifies;
786-
(set tmp10ModifyEntry, tmp10Modifies |
787-
tmp10Modifies in tmps9FlattenedModifiesSet
788-
&& tmp10ModifyEntry in tmp10Modifies
789-
:: tmp10ModifyEntry)
790-
modifies var tmps11 := set t11 | t11 in config.tableEncryptionConfigs.Values
791-
&& t11.search.Some?
792-
:: set t12 | t12 in t11.search.value.versions :: t12.keyStore;
793-
var tmps11FlattenedModifiesSet: set<set<object>> := set t0
794-
, t1 | t0 in tmps11 && t1 in t0 :: t1.Modifies;
795-
(set tmp13ModifyEntry, tmp13Modifies |
796-
tmp13Modifies in tmps11FlattenedModifiesSet
797-
&& tmp13ModifyEntry in tmp13Modifies
798-
:: tmp13ModifyEntry)
762+
modifies set tmps5 <- set t5 <- config.tableEncryptionConfigs.Values | true
763+
&& t5.keyring.Some?
764+
:: t5.keyring.value,
765+
obj <- tmps5.Modifies | obj in tmps5.Modifies :: obj
766+
modifies set tmps6 <- set t6 <- config.tableEncryptionConfigs.Values | true
767+
&& t6.cmm.Some?
768+
:: t6.cmm.value,
769+
obj <- tmps6.Modifies | obj in tmps6.Modifies :: obj
770+
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
771+
&& t7.legacyOverride.Some?
772+
:: t7.legacyOverride.value.encryptor,
773+
obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj
774+
modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true
775+
&& t8.search.Some?
776+
, t9 <- t8.search.value.versions :: t9.keyStore,
777+
obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj
799778
ensures res.Success? ==>
800779
&& fresh(res.value)
801780
&& fresh(res.value.Modifies
802-
- ( var tmps14 := set t14 | t14 in config.tableEncryptionConfigs.Values
803-
&& t14.keyring.Some?
804-
:: t14.keyring.value;
805-
var tmps14FlattenedModifiesSet: set<set<object>> := set t0
806-
| t0 in tmps14 :: t0.Modifies;
807-
(set tmp15ModifyEntry, tmp15Modifies |
808-
tmp15Modifies in tmps14FlattenedModifiesSet
809-
&& tmp15ModifyEntry in tmp15Modifies
810-
:: tmp15ModifyEntry)
811-
) - ( var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values
812-
&& t16.cmm.Some?
813-
:: t16.cmm.value;
814-
var tmps16FlattenedModifiesSet: set<set<object>> := set t0
815-
| t0 in tmps16 :: t0.Modifies;
816-
(set tmp17ModifyEntry, tmp17Modifies |
817-
tmp17Modifies in tmps16FlattenedModifiesSet
818-
&& tmp17ModifyEntry in tmp17Modifies
819-
:: tmp17ModifyEntry)
820-
) - ( var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values
821-
&& t18.legacyOverride.Some?
822-
:: t18.legacyOverride.value.encryptor;
823-
var tmps18FlattenedModifiesSet: set<set<object>> := set t0
824-
| t0 in tmps18 :: t0.Modifies;
825-
(set tmp19ModifyEntry, tmp19Modifies |
826-
tmp19Modifies in tmps18FlattenedModifiesSet
827-
&& tmp19ModifyEntry in tmp19Modifies
828-
:: tmp19ModifyEntry)
829-
) - ( var tmps20 := set t20 | t20 in config.tableEncryptionConfigs.Values
830-
&& t20.search.Some?
831-
:: set t21 | t21 in t20.search.value.versions :: t21.keyStore;
832-
var tmps20FlattenedModifiesSet: set<set<object>> := set t0
833-
, t1 | t0 in tmps20 && t1 in t0 :: t1.Modifies;
834-
(set tmp22ModifyEntry, tmp22Modifies |
835-
tmp22Modifies in tmps20FlattenedModifiesSet
836-
&& tmp22ModifyEntry in tmp22Modifies
837-
:: tmp22ModifyEntry)
781+
- ( set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true
782+
&& t10.keyring.Some?
783+
:: t10.keyring.value,
784+
obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
785+
) - ( set tmps11 <- set t11 <- config.tableEncryptionConfigs.Values | true
786+
&& t11.cmm.Some?
787+
:: t11.cmm.value,
788+
obj <- tmps11.Modifies | obj in tmps11.Modifies :: obj
789+
) - ( set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
790+
&& t12.legacyOverride.Some?
791+
:: t12.legacyOverride.value.encryptor,
792+
obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
793+
) - ( set tmps13 <- set t13 <- config.tableEncryptionConfigs.Values | true
794+
&& t13.search.Some?
795+
, t14 <- t13.search.value.versions :: t14.keyStore,
796+
obj <- tmps13.Modifies | obj in tmps13.Modifies :: obj
838797
) )
839798
&& fresh(res.value.History)
840799
&& res.value.ValidState()
841-
ensures var tmps23 := set t23 | t23 in config.tableEncryptionConfigs.Values;
842-
forall tmp23 :: tmp23 in tmps23 ==>
843-
tmp23.keyring.Some? ==>
844-
tmp23.keyring.value.ValidState()
845-
ensures var tmps24 := set t24 | t24 in config.tableEncryptionConfigs.Values;
846-
forall tmp24 :: tmp24 in tmps24 ==>
847-
tmp24.cmm.Some? ==>
848-
tmp24.cmm.value.ValidState()
849-
ensures var tmps25 := set t25 | t25 in config.tableEncryptionConfigs.Values;
850-
forall tmp25 :: tmp25 in tmps25 ==>
851-
tmp25.legacyOverride.Some? ==>
852-
tmp25.legacyOverride.value.encryptor.ValidState()
853-
ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
854-
forall tmp26 :: tmp26 in tmps26 ==>
855-
tmp26.search.Some? ==>
856-
var tmps27 := set t27 | t27 in tmp26.search.value.versions;
857-
forall tmp27 :: tmp27 in tmps27 ==>
858-
tmp27.keyStore.ValidState()
859-
// END MANUAL EDIT
860-
861-
// Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
800+
ensures var tmps15 := set t15 | t15 in config.tableEncryptionConfigs.Values;
801+
forall tmp15 :: tmp15 in tmps15 ==>
802+
tmp15.keyring.Some? ==>
803+
tmp15.keyring.value.ValidState()
804+
ensures var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values;
805+
forall tmp16 :: tmp16 in tmps16 ==>
806+
tmp16.cmm.Some? ==>
807+
tmp16.cmm.value.ValidState()
808+
ensures var tmps17 := set t17 | t17 in config.tableEncryptionConfigs.Values;
809+
forall tmp17 :: tmp17 in tmps17 ==>
810+
tmp17.legacyOverride.Some? ==>
811+
tmp17.legacyOverride.value.encryptor.ValidState()
812+
ensures var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values;
813+
forall tmp18 :: tmp18 in tmps18 ==>
814+
tmp18.search.Some? ==>
815+
var tmps19 := set t19 | t19 in tmp18.search.value.versions;
816+
forall tmp19 :: tmp19 in tmps19 ==>
817+
tmp19.keyStore.ValidState()
818+
819+
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
862820
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {
863821
Success(client)
864-
} // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
822+
}
865823
function method CreateFailureOfError(error: Error): Result<IDynamoDbEncryptionTransformsClient, Error> {
866824
Failure(error)
867825
}

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

+2-10
Original file line numberDiff line numberDiff line change
@@ -6,25 +6,21 @@ module DdbMiddlewareConfig {
66
import opened Wrappers
77
import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
88
import DynamoDbItemEncryptor
9-
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
109
import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
1110
import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
1211
import SearchableEncryptionInfo
13-
import AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
1412

1513
datatype TableConfig = TableConfig(
1614
physicalTableName: ComAmazonawsDynamodbTypes.TableName,
1715
logicalTableName: string,
1816
partitionKeyName: string,
1917
sortKeyName: Option<string>,
20-
itemEncryptor: DynamoDbItemEncryptor.Types.IDynamoDbItemEncryptorClient,
18+
itemEncryptor: DynamoDbItemEncryptor.DynamoDbItemEncryptorClient,
2119
search : Option<SearchableEncryptionInfo.ValidSearchInfo>
2220
)
2321

2422
predicate ValidTableConfig?(config: TableConfig) {
25-
&& config.itemEncryptor is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient
26-
&& var itemEncryptorClient := config.itemEncryptor as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
27-
&& var encryptorConfig := itemEncryptorClient.config;
23+
var encryptorConfig := config.itemEncryptor.config;
2824
&& config.logicalTableName == encryptorConfig.logicalTableName
2925
&& config.partitionKeyName == encryptorConfig.partitionKeyName
3026
&& config.sortKeyName == encryptorConfig.sortKeyName
@@ -34,10 +30,6 @@ module DdbMiddlewareConfig {
3430

3531
type ValidTableConfig = c: TableConfig | ValidTableConfig?(c) witness *
3632

37-
function method ItemEncryptorClientConfig(config: ValidTableConfig): ENC.Config {
38-
(config.itemEncryptor as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config
39-
}
40-
4133
function OneSearchModifies(config : ValidTableConfig) : set<object>
4234
{
4335
if config.search.Some? then config.search.value.Modifies() else {}

0 commit comments

Comments
 (0)