Skip to content
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.

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

chore: Update MPL to 1.3.0 #972

Merged
merged 8 commits into from
Apr 30, 2024
Merged
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
@@ -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 {} )
10 changes: 5 additions & 5 deletions TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
Original file line number Diff line number Diff line change
@@ -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
@@ -298,7 +298,7 @@ module {:options "-functionSyntax:4"} JsonConfig {

var keys :- expect KeyVectors.KeyVectors(
KeyVectorsTypes.KeyVectorsConfig(
keyManifiestPath := DEFAULT_KEYS
keyManifestPath := DEFAULT_KEYS
)
);
var keyDescription :-
@@ -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(
@@ -402,7 +402,7 @@ module {:options "-functionSyntax:4"} JsonConfig {

var keys :- expect KeyVectors.KeyVectors(
KeyVectorsTypes.KeyVectorsConfig(
keyManifiestPath := DEFAULT_KEYS
keyManifestPath := DEFAULT_KEYS
)
);
var keyDescription :-
@@ -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(
4 changes: 0 additions & 4 deletions TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion project.properties
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

Unchanged files with check annotations Beta

{
System.Collections.Generic.List<Amazon.DynamoDBv2.Model.AttributeValue> var_parameters = value.Parameters != null ? value.Parameters : (System.Collections.Generic.List<Amazon.DynamoDBv2.Model.AttributeValue>)null;
bool? var_consistentRead = value.ConsistentRead != null ? value.ConsistentRead : (bool?)null;

Check warning on line 1311 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 1311 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'
string var_nextToken = value.NextToken != null ? value.NextToken : (string)null;
Amazon.DynamoDBv2.ReturnConsumedCapacity var_returnConsumedCapacity = value.ReturnConsumedCapacity != null ? value.ReturnConsumedCapacity : (Amazon.DynamoDBv2.ReturnConsumedCapacity)null;
int? var_limit = value.Limit != null ? value.Limit : (int?)null;

Check warning on line 1314 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'

Check warning on line 1314 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'
return new software.amazon.cryptography.services.dynamodb.internaldafny.types.ExecuteStatementInput(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ExecuteStatementInput__M9_Statement(value.Statement), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ExecuteStatementInput__M10_Parameters(var_parameters), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ExecuteStatementInput__M14_ConsistentRead(var_consistentRead), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ExecuteStatementInput__M9_NextToken(var_nextToken), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ExecuteStatementInput__M22_ReturnConsumedCapacity(var_returnConsumedCapacity), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ExecuteStatementInput__M5_Limit(var_limit));
}
public static Amazon.DynamoDBv2.Model.ExecuteStatementResponse FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S22_ExecuteStatementOutput(software.amazon.cryptography.services.dynamodb.internaldafny.types._IExecuteStatementOutput value)
{
System.Collections.Generic.List<string> var_attributesToGet = value.AttributesToGet != null ? value.AttributesToGet : (System.Collections.Generic.List<string>)null;
bool? var_consistentRead = value.ConsistentRead != null ? value.ConsistentRead : (bool?)null;

Check warning on line 1372 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 1372 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'
Amazon.DynamoDBv2.ReturnConsumedCapacity var_returnConsumedCapacity = value.ReturnConsumedCapacity != null ? value.ReturnConsumedCapacity : (Amazon.DynamoDBv2.ReturnConsumedCapacity)null;
string var_projectionExpression = value.ProjectionExpression != null ? value.ProjectionExpression : (string)null;
System.Collections.Generic.Dictionary<string, string> var_expressionAttributeNames = value.ExpressionAttributeNames != null ? value.ExpressionAttributeNames : (System.Collections.Generic.Dictionary<string, string>)null;
Amazon.DynamoDBv2.Select var_select = value.Select != null ? value.Select : (Amazon.DynamoDBv2.Select)null;
System.Collections.Generic.List<string> var_attributesToGet = value.AttributesToGet != null ? value.AttributesToGet : (System.Collections.Generic.List<string>)null;
int? var_limit = value.IsLimitSet ? value.Limit : (int?)null;
bool? var_consistentRead = value.ConsistentRead != null ? value.ConsistentRead : (bool?)null;

Check warning on line 1457 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 1457 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'
System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition> var_keyConditions = value.KeyConditions != null ? value.KeyConditions : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition>)null;
System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition> var_queryFilter = value.QueryFilter != null ? value.QueryFilter : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.Condition>)null;
Amazon.DynamoDBv2.ConditionalOperator var_conditionalOperator = value.ConditionalOperator != null ? value.ConditionalOperator : (Amazon.DynamoDBv2.ConditionalOperator)null;
bool? var_scanIndexForward = value.ScanIndexForward != null ? value.ScanIndexForward : (bool?)null;

Check warning on line 1461 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 1461 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'
System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue> var_exclusiveStartKey = value.ExclusiveStartKey != null ? value.ExclusiveStartKey : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)null;
Amazon.DynamoDBv2.ReturnConsumedCapacity var_returnConsumedCapacity = value.ReturnConsumedCapacity != null ? value.ReturnConsumedCapacity : (Amazon.DynamoDBv2.ReturnConsumedCapacity)null;
string var_projectionExpression = value.ProjectionExpression != null ? value.ProjectionExpression : (string)null;
{
System.Collections.Generic.List<System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>> var_items = value.Items != null ? value.Items : (System.Collections.Generic.List<System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>>)null;
int? var_count = value.Count != null ? value.Count : (int?)null;

Check warning on line 1483 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'

Check warning on line 1483 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'
int? var_scannedCount = value.ScannedCount != null ? value.ScannedCount : (int?)null;

Check warning on line 1484 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'

Check warning on line 1484 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'
System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue> var_lastEvaluatedKey = value.LastEvaluatedKey != null ? value.LastEvaluatedKey : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)null;
Amazon.DynamoDBv2.Model.ConsumedCapacity var_consumedCapacity = value.ConsumedCapacity != null ? value.ConsumedCapacity : (Amazon.DynamoDBv2.Model.ConsumedCapacity)null;
return new software.amazon.cryptography.services.dynamodb.internaldafny.types.QueryOutput(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S11_QueryOutput__M5_Items(var_items), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S11_QueryOutput__M5_Count(var_count), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S11_QueryOutput__M12_ScannedCount(var_scannedCount), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S11_QueryOutput__M16_LastEvaluatedKey(var_lastEvaluatedKey), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S11_QueryOutput__M16_ConsumedCapacity(var_consumedCapacity));
string var_filterExpression = value.FilterExpression != null ? value.FilterExpression : (string)null;
System.Collections.Generic.Dictionary<string, string> var_expressionAttributeNames = value.ExpressionAttributeNames != null ? value.ExpressionAttributeNames : (System.Collections.Generic.Dictionary<string, string>)null;
System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue> var_expressionAttributeValues = value.ExpressionAttributeValues != null ? value.ExpressionAttributeValues : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)null;
bool? var_consistentRead = value.ConsistentRead != null ? value.ConsistentRead : (bool?)null;

Check warning on line 1561 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 1561 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'bool' is never equal to 'null' of type 'bool?'
return new software.amazon.cryptography.services.dynamodb.internaldafny.types.ScanInput(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M9_TableName(value.TableName), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M9_IndexName(var_indexName), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M15_AttributesToGet(var_attributesToGet), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M5_Limit(var_limit), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M6_Select(var_select), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M10_ScanFilter(var_scanFilter), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M19_ConditionalOperator(var_conditionalOperator), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M17_ExclusiveStartKey(var_exclusiveStartKey), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M22_ReturnConsumedCapacity(var_returnConsumedCapacity), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M13_TotalSegments(var_totalSegments), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M7_Segment(var_segment), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M20_ProjectionExpression(var_projectionExpression), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M16_FilterExpression(var_filterExpression), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M24_ExpressionAttributeNames(var_expressionAttributeNames), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M25_ExpressionAttributeValues(var_expressionAttributeValues), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_ScanInput__M14_ConsistentRead(var_consistentRead));
}
public static Amazon.DynamoDBv2.Model.ScanResponse FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_ScanOutput(software.amazon.cryptography.services.dynamodb.internaldafny.types._IScanOutput value)
{
System.Collections.Generic.List<System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>> var_items = value.Items != null ? value.Items : (System.Collections.Generic.List<System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>>)null;
int? var_count = value.Count != null ? value.Count : (int?)null;

Check warning on line 1576 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, ubuntu-latest)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'

Check warning on line 1576 in DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs

GitHub Actions / testDotNet (DynamoDbEncryption, 6.0.x, macos-12)

The result of the expression is always 'true' since a value of type 'int' is never equal to 'null' of type 'int?'
int? var_scannedCount = value.ScannedCount != null ? value.ScannedCount : (int?)null;
System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue> var_lastEvaluatedKey = value.LastEvaluatedKey != null ? value.LastEvaluatedKey : (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)null;
Amazon.DynamoDBv2.Model.ConsumedCapacity var_consumedCapacity = value.ConsumedCapacity != null ? value.ConsumedCapacity : (Amazon.DynamoDBv2.Model.ConsumedCapacity)null;