Skip to content

Commit b2674a9

Browse files
lucasmcdonald3lucasmcdonald3
authored
chore: Bump to MPL HEAD, Smithy-Dafny HEAD (#1299)
1 parent b9333fb commit b2674a9

File tree

22 files changed

+217
-80
lines changed

22 files changed

+217
-80
lines changed

‎.github/workflows/library_format.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ jobs:
3939
- name: Setup Dafny
4040
uses: dafny-lang/setup-dafny-action@v1.8.0
4141
with:
42-
dafny-version: ${{ '4.2.0' }}
42+
dafny-version: ${{ inputs.dafny }}
4343

4444
- name: Check format of Java code et al
4545
run: |

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

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,9 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
143143
&& output.value.branchKeyIdSupplier.ValidState()
144144
&& output.value.branchKeyIdSupplier.Modifies !! {History}
145145
&& fresh(output.value.branchKeyIdSupplier)
146-
&& fresh ( output.value.branchKeyIdSupplier.Modifies - Modifies - {History} - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
146+
&& fresh ( output.value.branchKeyIdSupplier.Modifies
147+
- Modifies - {History}
148+
- input.ddbKeyBranchKeyIdSupplier.Modifies ) )
147149
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
148150
ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)]
149151

@@ -535,7 +537,9 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
535537
&& output.value.branchKeyIdSupplier.ValidState()
536538
&& output.value.branchKeyIdSupplier.Modifies !! {History}
537539
&& fresh(output.value.branchKeyIdSupplier)
538-
&& fresh ( output.value.branchKeyIdSupplier.Modifies - Modifies - {History} - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
540+
&& fresh ( output.value.branchKeyIdSupplier.Modifies
541+
- Modifies - {History}
542+
- input.ddbKeyBranchKeyIdSupplier.Modifies ) )
539543
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
540544
ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)]
541545
{
@@ -592,7 +596,9 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
592596
&& ( output.Success? ==>
593597
&& output.value.branchKeyIdSupplier.ValidState()
594598
&& fresh(output.value.branchKeyIdSupplier)
595-
&& fresh ( output.value.branchKeyIdSupplier.Modifies - ModifiesInternalConfig(config) - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
599+
&& fresh ( output.value.branchKeyIdSupplier.Modifies
600+
- ModifiesInternalConfig(config)
601+
- input.ddbKeyBranchKeyIdSupplier.Modifies ) )
596602
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
597603

598604

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ module BaseBeacon {
1919

2020
import DDB = ComAmazonawsDynamodbTypes
2121
import Prim = AwsCryptographyPrimitivesTypes
22-
import Aws.Cryptography.Primitives
22+
import Primitives = AtomicPrimitives
2323
import UTF8
2424
import SortedSets
2525
import TermLoc

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ module CompoundBeacon {
1616
import opened DdbVirtualFields
1717

1818
import Prim = AwsCryptographyPrimitivesTypes
19-
import Aws.Cryptography.Primitives
19+
import Primitives = AtomicPrimitives
2020
import UTF8
2121
import Seq
2222
import SortedSets

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

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ module SearchConfigToInfo {
3232
import CB = CompoundBeacon
3333
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
3434
import MPT = AwsCryptographyMaterialProvidersTypes
35-
import Aws.Cryptography.Primitives
35+
import Primitives = AtomicPrimitives
3636

3737
// convert configured SearchConfig to internal SearchInfo
3838
method Convert(outer : DynamoDbTableEncryptionConfig)
@@ -137,14 +137,19 @@ module SearchConfigToInfo {
137137
else
138138
MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
139139

140-
//= specification/searchable-encryption/search-config.md#key-store-cache
141-
//# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
142-
//# MUST be created.
143-
var input := MPT.CreateCryptographicMaterialsCacheInput(
144-
cache := cacheType
145-
);
146-
var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
147-
var cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
140+
var cache;
141+
if cacheType.Shared? {
142+
cache := cacheType.Shared;
143+
} else {
144+
//= specification/searchable-encryption/search-config.md#key-store-cache
145+
//# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
146+
//# MUST be created.
147+
var input := MPT.CreateCryptographicMaterialsCacheInput(
148+
cache := cacheType
149+
);
150+
var maybeCache := mpl.CreateCryptographicMaterialsCache(input);
151+
cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
152+
}
148153

149154
if config.multi? {
150155
:- Need(0 < config.multi.cacheTTL, E("Beacon Cache TTL must be at least 1."));

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ module SearchableEncryptionInfo {
2121
import UTF8
2222
import opened Time
2323
import KeyStore = AwsCryptographyKeyStoreTypes
24-
import Aws.Cryptography.Primitives
24+
import Primitives = AtomicPrimitives
2525
import Prim = AwsCryptographyPrimitivesTypes
2626
import MP = AwsCryptographyMaterialProvidersTypes
2727
import KeyStoreTypes = AwsCryptographyKeyStoreTypes
@@ -71,11 +71,11 @@ module SearchableEncryptionInfo {
7171
//# MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation).
7272
var newKey :- GetBeaconKey(client, key, keysLeft[0]);
7373
reveal Seq.HasNoDuplicates();
74-
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
75-
//# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
76-
//# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
77-
//# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
78-
//# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
74+
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
75+
//# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
76+
//# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
77+
//# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
78+
//# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
7979
output := GetHmacKeys(client, allKeys, keysLeft[1..], key, acc[keysLeft[0] := newKey]);
8080
}
8181
}

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ module BeaconTestFixtures {
1717
import DDBC = Com.Amazonaws.Dynamodb
1818
import KTypes = AwsCryptographyKeyStoreTypes
1919
import SI = SearchableEncryptionInfo
20-
import Aws.Cryptography.Primitives
20+
import Primitives = AtomicPrimitives
2121
import MaterialProviders
2222
import MPT = AwsCryptographyMaterialProvidersTypes
2323
import SortedSets
@@ -181,6 +181,9 @@ module BeaconTestFixtures {
181181
ensures output.keyStore.ValidState()
182182
ensures fresh(output.keyStore.Modifies)
183183
ensures output.version == 1
184+
ensures
185+
&& output.keySource.multi?
186+
&& output.keySource.multi.cache.None?
184187
{
185188
var store := GetKeyStore();
186189
return BeaconVersion (

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

Lines changed: 82 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -759,62 +759,98 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
759759
var tmps4 := set t4 | t4 in tmp3.search.value.versions;
760760
forall tmp4 :: tmp4 in tmps4 ==>
761761
tmp4.keyStore.ValidState()
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
762+
requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values;
763+
forall tmp5 :: tmp5 in tmps5 ==>
764+
tmp5.search.Some? ==>
765+
var tmps6 := set t6 | t6 in tmp5.search.value.versions;
766+
forall tmp6 :: tmp6 in tmps6 ==>
767+
tmp6.keySource.multi? ==>
768+
tmp6.keySource.multi.cache.Some? ==>
769+
tmp6.keySource.multi.cache.value.Shared? ==>
770+
tmp6.keySource.multi.cache.value.Shared.ValidState()
770771
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
771-
&& t7.legacyOverride.Some?
772-
:: t7.legacyOverride.value.encryptor,
772+
&& t7.keyring.Some?
773+
:: t7.keyring.value,
773774
obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj
774775
modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true
775-
&& t8.search.Some?
776-
, t9 <- t8.search.value.versions :: t9.keyStore,
776+
&& t8.cmm.Some?
777+
:: t8.cmm.value,
777778
obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj
779+
modifies set tmps9 <- set t9 <- config.tableEncryptionConfigs.Values | true
780+
&& t9.legacyOverride.Some?
781+
:: t9.legacyOverride.value.encryptor,
782+
obj <- tmps9.Modifies | obj in tmps9.Modifies :: obj
783+
modifies set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true
784+
&& t10.search.Some?
785+
, t11 <- t10.search.value.versions | true
786+
:: t11.keyStore,
787+
obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
788+
modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
789+
&& t12.search.Some?
790+
, t13 <- t12.search.value.versions | true
791+
&& t13.keySource.multi?
792+
&& t13.keySource.multi.cache.Some?
793+
&& t13.keySource.multi.cache.value.Shared?
794+
:: t13.keySource.multi.cache.value.Shared,
795+
obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
778796
ensures res.Success? ==>
779797
&& fresh(res.value)
780798
&& fresh(res.value.Modifies
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
799+
- ( set tmps14 <- set t14 <- config.tableEncryptionConfigs.Values | true
800+
&& t14.keyring.Some?
801+
:: t14.keyring.value,
802+
obj <- tmps14.Modifies | obj in tmps14.Modifies :: obj
803+
) - ( set tmps15 <- set t15 <- config.tableEncryptionConfigs.Values | true
804+
&& t15.cmm.Some?
805+
:: t15.cmm.value,
806+
obj <- tmps15.Modifies | obj in tmps15.Modifies :: obj
807+
) - ( set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true
808+
&& t16.legacyOverride.Some?
809+
:: t16.legacyOverride.value.encryptor,
810+
obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj
811+
) - ( set tmps17 <- set t17 <- config.tableEncryptionConfigs.Values | true
812+
&& t17.search.Some?
813+
, t18 <- t17.search.value.versions | true
814+
:: t18.keyStore,
815+
obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj
816+
) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
817+
&& t19.search.Some?
818+
, t20 <- t19.search.value.versions | true
819+
&& t20.keySource.multi?
820+
&& t20.keySource.multi.cache.Some?
821+
&& t20.keySource.multi.cache.value.Shared?
822+
:: t20.keySource.multi.cache.value.Shared,
823+
obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
797824
) )
798825
&& fresh(res.value.History)
799826
&& res.value.ValidState()
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()
827+
ensures var tmps21 := set t21 | t21 in config.tableEncryptionConfigs.Values;
828+
forall tmp21 :: tmp21 in tmps21 ==>
829+
tmp21.keyring.Some? ==>
830+
tmp21.keyring.value.ValidState()
831+
ensures var tmps22 := set t22 | t22 in config.tableEncryptionConfigs.Values;
832+
forall tmp22 :: tmp22 in tmps22 ==>
833+
tmp22.cmm.Some? ==>
834+
tmp22.cmm.value.ValidState()
835+
ensures var tmps23 := set t23 | t23 in config.tableEncryptionConfigs.Values;
836+
forall tmp23 :: tmp23 in tmps23 ==>
837+
tmp23.legacyOverride.Some? ==>
838+
tmp23.legacyOverride.value.encryptor.ValidState()
839+
ensures var tmps24 := set t24 | t24 in config.tableEncryptionConfigs.Values;
840+
forall tmp24 :: tmp24 in tmps24 ==>
841+
tmp24.search.Some? ==>
842+
var tmps25 := set t25 | t25 in tmp24.search.value.versions;
843+
forall tmp25 :: tmp25 in tmps25 ==>
844+
tmp25.keyStore.ValidState()
845+
ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
846+
forall tmp26 :: tmp26 in tmps26 ==>
847+
tmp26.search.Some? ==>
848+
var tmps27 := set t27 | t27 in tmp26.search.value.versions;
849+
forall tmp27 :: tmp27 in tmps27 ==>
850+
tmp27.keySource.multi? ==>
851+
tmp27.keySource.multi.cache.Some? ==>
852+
tmp27.keySource.multi.cache.value.Shared? ==>
853+
tmp27.keySource.multi.cache.value.Shared.ValidState()
818854

819855
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
820856
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {

‎DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
1919
import Prim = AwsCryptographyPrimitivesTypes
2020
import StructuredEncryptionHeader
2121
import Random
22-
import Aws.Cryptography.Primitives
22+
import Primitives = AtomicPrimitives
2323
import Header = StructuredEncryptionHeader
2424
import Footer = StructuredEncryptionFooter
2525
import MaterialProviders

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ module StructuredEncryptionCrypt {
1919

2020
import CMP = AwsCryptographyMaterialProvidersTypes
2121
import Prim = AwsCryptographyPrimitivesTypes
22-
import Aws.Cryptography.Primitives
22+
import Primitives = AtomicPrimitives
2323
import UTF8
2424
import Header = StructuredEncryptionHeader
2525
import HKDF

0 commit comments

Comments
 (0)