Skip to content

[BLOCKS MPL 1.5.2+ UPGRADE] chore: Bump MPL submodule version, fix verification #1305

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

Closed
wants to merge 9 commits into from
Closed

[BLOCKS MPL 1.5.2+ UPGRADE] chore: Bump MPL submodule version, fix verification #1305

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
8adb90a
chore: Test with MPL main head
lucasmcdonald3 Aug 22, 2024
5920f6b
Merge branch 'main' into test-mpl-main
ajewellamz Aug 22, 2024
c54ed4c
remove unnecessary asserts
ajewellamz Aug 22, 2024
18cd605
m
ajewellamz Aug 22, 2024
b355293
m
ajewellamz Aug 22, 2024
201c4d4
Merge branch 'main' into test-mpl-main
ajewellamz Aug 22, 2024
c26e266
Merge branch 'main' into test-mpl-main
ajewellamz Aug 22, 2024
ab07c13
merge
lucasmcdonald3 Aug 23, 2024
79aea91
Update project.properties
lucasmcdonald3 Aug 23, 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
10 changes: 0 additions & 10 deletions DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,16 +92,6 @@ module QueryTransform {
var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
var decrypted :- MapError(decryptRes);

// If the decrypted result was plaintext, i.e. has no parsedHeader
// then this is expected IFF the table config allows plaintext read
assert decrypted.parsedHeader.None? ==>
&& EncOps.IsPlaintextItem(encryptedItems[x])
&& !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
&& (
|| tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
|| tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
);

if keyId.KeyId? && decrypted.parsedHeader.Some? {
:- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Query result has more than one Encrypted Data Key"));
if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {
Expand Down
10 changes: 0 additions & 10 deletions DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,16 +90,6 @@ module ScanTransform {
var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
var decrypted :- MapError(decryptRes);

// If the decrypted result was plaintext, i.e. has no parsedHeader
// then this is expected IFF the table config allows plaintext read
assert decrypted.parsedHeader.None? ==>
&& EncOps.IsPlaintextItem(encryptedItems[x])
&& !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
&& (
|| tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
|| tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
);

if keyId.KeyId? && decrypted.parsedHeader.Some? {
:- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key"));
if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {
Expand Down
1 change: 1 addition & 0 deletions DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,7 @@ module TestFixtures {
ensures fresh(encryption)
ensures fresh(encryption.Modifies)
{
expect sortKey.None? || DDB.IsValid_KeySchemaAttributeName(sortKey.value);
var keyring := GetKmsKeyring();
encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
DynamoDbTablesEncryptionConfig(
Expand Down
4 changes: 2 additions & 2 deletions project.properties
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
projectJavaVersion=3.6.2
mplDependencyJavaVersion=1.5.1
projectJavaVersion=3.6.2-SNAPSHOT
mplDependencyJavaVersion=1.5.1-SNAPSHOT
dafnyVersion=4.2.0
dafnyVerifyVersion=4.7.0
dafnyRuntimeJavaVersion=4.2.0
Expand Down
2 changes: 1 addition & 1 deletion submodules/MaterialProviders
Open in desktop
Submodule MaterialProviders updated from cdd488 to d51d64
Loading