Skip to content

Commit 85cc676

Browse files
RitvikKapilaRitvikKapila
authored
Merge branch 'main' into rkapila/shared-cache-examples
2 parents d4b742e + 28d06fe commit 85cc676

39 files changed

+248
-100
lines changed

‎.github/workflows/check-files.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ jobs:
1414
env:
1515
# unfortunately we can't check if the approver is part of the CODEOWNERS. This is a subset of aws/aws-crypto-tools-team
1616
# to add more allowlisted approvers just modify this env variable
17-
maintainers: seebees, texastony, ShubhamChaturvedi7, lucasmcdonald3, josecorella, imabhichow, rishav-karanjit, antonf-amzn, justplaz, ajewellamz
17+
maintainers: seebees, texastony, ShubhamChaturvedi7, lucasmcdonald3, josecorella, imabhichow, rishav-karanjit, antonf-amzn, kessplas, ajewellamz, RitvikKapila
1818
steps:
1919
- uses: actions/checkout@v3
2020
with:

‎.github/workflows/ci_examples_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ jobs:
2929
max-parallel: 1
3030
matrix:
3131
java-version: [8, 11, 16, 17]
32-
os: [macos-12]
32+
os: [macos-13]
3333
runs-on: ${{ matrix.os }}
3434
permissions:
3535
id-token: write

‎.github/workflows/ci_examples_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ jobs:
2727
matrix:
2828
library: [DynamoDbEncryption]
2929
dotnet-version: ["6.0.x"]
30-
os: [macos-12]
30+
os: [macos-13]
3131
runs-on: ${{ matrix.os }}
3232
permissions:
3333
id-token: write

‎.github/workflows/ci_test_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ jobs:
2929
matrix:
3030
library: [DynamoDbEncryption]
3131
java-version: [8, 11, 16, 17]
32-
os: [macos-12]
32+
os: [macos-13]
3333
runs-on: ${{ matrix.os }}
3434
permissions:
3535
id-token: write

‎.github/workflows/ci_test_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
matrix:
2626
library: [DynamoDbEncryption]
2727
dotnet-version: ["6.0.x"]
28-
os: [macos-12, ubuntu-latest, windows-latest]
28+
os: [macos-13, ubuntu-latest, windows-latest]
2929
runs-on: ${{ matrix.os }}
3030
permissions:
3131
id-token: write

‎.github/workflows/ci_todos.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ on:
99

1010
jobs:
1111
findTodos:
12-
runs-on: macos-12
12+
runs-on: macos-13
1313
steps:
1414
- uses: actions/checkout@v3
1515

‎.github/workflows/dafny_interop_examples_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ jobs:
2828
max-parallel: 1
2929
matrix:
3030
java-version: [8, 11, 16, 17]
31-
os: [macos-12]
31+
os: [macos-13]
3232
runs-on: ${{ matrix.os }}
3333
permissions:
3434
id-token: write

‎.github/workflows/dafny_interop_examples_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ jobs:
2424
matrix:
2525
library: [DynamoDbEncryption]
2626
dotnet-version: ["6.0.x"]
27-
os: [macos-12]
27+
os: [macos-13]
2828
runs-on: ${{ matrix.os }}
2929
permissions:
3030
id-token: write

‎.github/workflows/dafny_interop_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ jobs:
2828
matrix:
2929
library: [DynamoDbEncryption]
3030
java-version: [8, 11, 16, 17]
31-
os: [macos-12]
31+
os: [macos-13]
3232
runs-on: ${{ matrix.os }}
3333
permissions:
3434
id-token: write

‎.github/workflows/dafny_interop_test_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ jobs:
2424
matrix:
2525
library: [DynamoDbEncryption]
2626
dotnet-version: ["6.0.x"]
27-
os: [macos-12, ubuntu-latest, windows-latest]
27+
os: [macos-13, ubuntu-latest, windows-latest]
2828
runs-on: ${{ matrix.os }}
2929
permissions:
3030
id-token: write

‎.github/workflows/library_dafny_verification.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ jobs:
3939
DynamoDbItemEncryptor,
4040
StructuredEncryption,
4141
]
42-
os: [macos-12]
42+
os: [macos-13]
4343
runs-on: ${{ matrix.os }}
4444
defaults:
4545
run:
@@ -72,7 +72,7 @@ jobs:
7272
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
7373
7474
# dafny-reportgenerator requires next6
75-
# but only 7.0 is installed on macos-12-large
75+
# but only 7.0 is installed on macos-13-large
7676
- name: Setup .NET Core SDK '6.0.x'
7777
uses: actions/setup-dotnet@v4
7878
with:

‎.github/workflows/library_format.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ jobs:
1919
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
2020
strategy:
2121
matrix:
22-
os: [macos-12]
22+
os: [macos-13]
2323
runs-on: ${{ matrix.os }}
2424
defaults:
2525
run:
@@ -39,7 +39,7 @@ jobs:
3939
- name: Setup Dafny
4040
uses: dafny-lang/[email protected]
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: |

‎.github/workflows/sem_ver.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ on:
66

77
jobs:
88
semantic-release:
9-
runs-on: macos-12
9+
runs-on: macos-13
1010
permissions:
1111
id-token: write
1212
contents: read

‎.github/workflows/semantic_release.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ jobs:
1414
# there is no easy way in gha to check if the actor is part of the team, running semantic release is a more
1515
# privileged operation, so we must make sure this list of users is a subset of the users labeled as maintainers of
1616
# https://github.com/orgs/aws/teams/aws-crypto-tools
17-
if: contains('["seebees","texastony","ShubhamChaturvedi7","lucasmcdonald3","josecorella","imabhichow","rishav-karanjit","antonf-amzn","justplaz","ajewellamz","RitvikKapila"]', github.actor)
18-
runs-on: macos-12
17+
if: contains('["seebees","texastony","ShubhamChaturvedi7","lucasmcdonald3","josecorella","imabhichow","rishav-karanjit","antonf-amzn","kessplas","ajewellamz","RitvikKapila"]', github.actor)
18+
runs-on: macos-13
1919
permissions:
2020
id-token: write
2121
contents: write

‎.github/workflows/test_vector_verification.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ jobs:
2929
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
3030
strategy:
3131
matrix:
32-
os: [macos-12]
32+
os: [macos-13]
3333
runs-on: ${{ matrix.os }}
3434
defaults:
3535
run:
@@ -62,7 +62,7 @@ jobs:
6262
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
6363
6464
# dafny-reportgenerator requires next6
65-
# but only 7.0 is installed on macos-12-large
65+
# but only 7.0 is installed on macos-13-large
6666
- name: Setup .NET Core SDK '6.0.x'
6767
uses: actions/setup-dotnet@v4
6868
with:

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

+9-3
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

+1-1
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

+1-1
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

+14-9
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

+6-6
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

+4-1
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 (

0 commit comments

Comments
 (0)