Skip to content

chore: Update MPL to 1.3.0 #972

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Apr 30, 2024
Merged

chore: Update MPL to 1.3.0 #972

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
6a703de
chore: Update MPL to 1.3.0
ajewellamz Apr 29, 2024
1937d63
typos
ajewellamz Apr 29, 2024
f8e5ac3
verify
ajewellamz Apr 29, 2024
6299194
resolve issue with extra main entry point in dotnet
ajewellamz Apr 29, 2024
82c6bb6
m
ajewellamz Apr 29, 2024
0ae6235
m
ajewellamz Apr 29, 2024
ce32651
m
ajewellamz Apr 29, 2024
166a945
update to latest MPL
ajewellamz Apr 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .github/workflows/ci_test_vector_net.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,9 @@ jobs:
shell: bash
working-directory: ./TestVectors
run: |
# this is evil, but the MPL test vectors defines an extra Main
sed -i "s/method Main/method NotMain/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy
sed -i "s/<OutputType>Exe/<OutputType>Library/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj
# This works because `node` is installed by default on GHA runners
make transpile_net

Expand Down
7 changes: 7 additions & 0 deletions DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -214,6 +214,13 @@ module

var client := new DynamoDbItemEncryptorClient(internalConfig);

assert fresh(client.History);
assert client.Modifies == Operations.ModifiesInternalConfig(internalConfig) + {client.History};
assert Operations.ModifiesInternalConfig(internalConfig) ==
internalConfig.cmm.Modifies
+ internalConfig.structuredEncryption.Modifies
+ internalConfig.cmpClient.Modifies;

assert fresh(client.Modifies
- ( if config.keyring.Some? then config.keyring.value.Modifies else {})
- ( if config.cmm.Some? then config.cmm.value.Modifies else {} )
Expand Down
10 changes: 5 additions & 5 deletions TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
import DynamoDbItemEncryptor


const DEFAULT_KEYS := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"

predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
type ConfigName = string
Expand Down Expand Up @@ -298,7 +298,7 @@ module {:options "-functionSyntax:4"} JsonConfig {

var keys :- expect KeyVectors.KeyVectors(
KeyVectorsTypes.KeyVectorsConfig(
keyManifiestPath := DEFAULT_KEYS
keyManifestPath := DEFAULT_KEYS
)
);
var keyDescription :-
Expand All @@ -311,7 +311,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
.MapFailure(ParseJsonManifests.ErrorToString);
Success(keyOut.keyDescription);

var keyring :- expect keys.CreateWappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));
var keyring :- expect keys.CreateWrappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));

var encryptorConfig :=
ENC.DynamoDbItemEncryptorConfig(
Expand Down Expand Up @@ -402,7 +402,7 @@ module {:options "-functionSyntax:4"} JsonConfig {

var keys :- expect KeyVectors.KeyVectors(
KeyVectorsTypes.KeyVectorsConfig(
keyManifiestPath := DEFAULT_KEYS
keyManifestPath := DEFAULT_KEYS
)
);
var keyDescription :-
Expand All @@ -415,7 +415,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
.MapFailure(ParseJsonManifests.ErrorToString);
Success(keyOut.keyDescription);

var keyring :- expect keys.CreateWappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));
var keyring :- expect keys.CreateWrappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));

var config :=
Types.DynamoDbTableEncryptionConfig(
Expand Down
4 changes: 0 additions & 4 deletions TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
import DDB = ComAmazonawsDynamodbTypes
import Filter = DynamoDBFilterExpr
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
import SKS = CreateStaticKeyStores
import KeyMaterial
import UTF8
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
import CMP = AwsCryptographyMaterialProvidersTypes
import KeyVectors
import CreateInterceptedDDBClient
import SortedSets
import Seq
Expand Down
2 changes: 1 addition & 1 deletion project.properties
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
projectJavaVersion=3.3.0
mplDependencyJavaVersion=1.2.0
mplDependencyJavaVersion=1.3.0
dafnyRuntimeJavaVersion=4.2.0
smithyDafnyJavaConversionVersion=0.1
2 changes: 1 addition & 1 deletion submodules/MaterialProviders
Open in desktop
Submodule MaterialProviders updated from 3e2a16 to 0b9567