Skip to content

Commit a5b4cea

Browse files
lavalerialex-chewrobin-aws
authored
chore: Upgrade to Dafny 4.0 (#112)
Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Robin Salkeld <[email protected]>
1 parent 4045e5d commit a5b4cea

29 files changed

+174
-83
lines changed

‎.github/workflows/ci_test_java.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -65,9 +65,9 @@ jobs:
6565
echo "CODEARTIFACT_AUTH_TOKEN=$TOKEN" >> $GITHUB_ENV
6666
6767
- name: Setup Dafny
68-
uses: dafny-lang/setup-dafny-action@v1.4.0
68+
uses: dafny-lang/setup-dafny-action@v1.6.1
6969
with:
70-
dafny-version: "3.10.0"
70+
dafny-version: "nightly-2023-04-12-f4836e9"
7171

7272
- name: Setup Java ${{ matrix.java-version }}
7373
uses: actions/setup-java@v3

‎.github/workflows/ci_test_net.yml

+5-5
Original file line numberDiff line numberDiff line change
@@ -43,16 +43,16 @@ jobs:
4343
git config --global --add url.https://github.com/.insteadOf [email protected]:
4444
git submodule update --init --recursive submodules/MaterialProviders
4545
46-
- name: Setup Dafny
47-
uses: dafny-lang/[email protected]
48-
with:
49-
dafny-version: "3.10.0"
50-
5146
- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
5247
uses: actions/setup-dotnet@v3
5348
with:
5449
dotnet-version: ${{ matrix.dotnet-version }}
5550

51+
- name: Setup Dafny
52+
uses: dafny-lang/[email protected]
53+
with:
54+
dafny-version: "nightly-2023-04-12-f4836e9"
55+
5656
- name: Download Dependencies
5757
working-directory: ./${{ matrix.library }}
5858
run: make setup_net

‎.github/workflows/ci_verification.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,9 @@ jobs:
4040
git submodule update --init --recursive submodules/MaterialProviders
4141
4242
- name: Setup Dafny
43-
uses: dafny-lang/setup-dafny-action@v1
43+
uses: dafny-lang/setup-dafny-action@v1.6.1
4444
with:
45-
dafny-version: "3.10.0"
45+
dafny-version: "nightly-2023-04-12-f4836e9"
4646

4747
- name: Verify ${{ matrix.library }} Dafny code
4848
shell: bash

‎DynamoDbEncryption/Makefile

+19-5
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ SERVICE_NAMESPACE_DynamoDbEncryption=aws.cryptography.dynamoDbEncryption
1818
SERVICE_NAMESPACE_DynamoDbItemEncryptor=aws.cryptography.dynamoDbEncryption.itemEncryptor
1919
SERVICE_NAMESPACE_DynamoDbEncryptionTransforms=aws.cryptography.dynamoDbEncryption.transforms
2020

21-
MAX_RESOURCE_COUNT=10000000
21+
MAX_RESOURCE_COUNT=20000000
2222
# Order is important
2323
# In java they MUST be built
2424
# in the order they depend on each other
@@ -30,30 +30,44 @@ PROJECT_DEPENDENCIES := \
3030
STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
3131
SMITHY_DEPS=submodules/MaterialProviders/model
3232

33+
# Since we are packaging projects differently, we cannot make assumptions
34+
# about where the files are located.
35+
# This is here to get unblocked but should be removed once we have migrated packages
36+
# to the new packaging format.
37+
PROJECT_INDEX := \
38+
submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy \
39+
submodules/MaterialProviders/ComAmazonawsKms/src/Index.dfy \
40+
submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy \
41+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy \
42+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy
43+
3344
# Dependencies for each local service
3445
SERVICE_DEPS_StructuredEncryption := \
3546
submodules/MaterialProviders/AwsCryptographyPrimitives \
3647
submodules/MaterialProviders/ComAmazonawsKms \
3748
submodules/MaterialProviders/ComAmazonawsDynamodb \
38-
submodules/MaterialProviders/AwsCryptographicMaterialProviders
49+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders
3950
SERVICE_DEPS_DynamoDbEncryption := \
4051
submodules/MaterialProviders/AwsCryptographyPrimitives \
4152
submodules/MaterialProviders/ComAmazonawsKms \
4253
submodules/MaterialProviders/ComAmazonawsDynamodb \
43-
submodules/MaterialProviders/AwsCryptographicMaterialProviders \
54+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
55+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
4456
DynamoDbEncryption/dafny/StructuredEncryption
4557
SERVICE_DEPS_DynamoDbItemEncryptor := \
4658
submodules/MaterialProviders/AwsCryptographyPrimitives \
4759
submodules/MaterialProviders/ComAmazonawsKms \
4860
submodules/MaterialProviders/ComAmazonawsDynamodb \
49-
submodules/MaterialProviders/AwsCryptographicMaterialProviders \
61+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
62+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
5063
DynamoDbEncryption/dafny/DynamoDbEncryption \
5164
DynamoDbEncryption/dafny/StructuredEncryption
5265
SERVICE_DEPS_DynamoDbEncryptionTransforms := \
5366
submodules/MaterialProviders/AwsCryptographyPrimitives \
5467
submodules/MaterialProviders/ComAmazonawsKms \
5568
submodules/MaterialProviders/ComAmazonawsDynamodb \
56-
submodules/MaterialProviders/AwsCryptographicMaterialProviders \
69+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
70+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
5771
DynamoDbEncryption/dafny/DynamoDbEncryption \
5872
DynamoDbEncryption/dafny/StructuredEncryption \
5973
DynamoDbEncryption/dafny/DynamoDbItemEncryptor

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDynamoDbEncryptionTypes.dfy

+4-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,10 @@
33
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
44
include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
55
include "../../StructuredEncryption/src/Index.dfy"
6-
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/src/Index.dfy"
6+
// TODO begin manual update
7+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy"
8+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
9+
// TODO end manual update
710
include "../../../../submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy"
811
include "../../../../submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy"
912
module {:extern "Dafny.Aws.Cryptography.DynamoDbEncryption.Types" } AwsCryptographyDynamoDbEncryptionTypes

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -251,7 +251,7 @@ module BaseBeacon {
251251
[HexChar(TruncateNibble(bytes[0] % 16, topBits))] + ToHexString(bytes[1..])
252252
}
253253

254-
lemma CheckBytesToHex()
254+
lemma {:vcs_split_on_every_assert} CheckBytesToHex()
255255
ensures
256256
&& var bytes := [1,2,3,4,5,6,7,0xb7];
257257
&& BytesToHex(bytes, 1) == "1"

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

+27-5
Original file line numberDiff line numberDiff line change
@@ -504,10 +504,8 @@ module DynamoToStruct {
504504
//# A Map MAY hold any DynamoDB Attribute Value data type,
505505
//# and MAY hold values of different types.
506506
var bytes := map kv <- m.Items | true :: kv.0 := AttrToBytes(kv.1, true);
507-
var bytes :- SimplifyMapValue(bytes);
508-
var keys := SortedSets.ComputeSetToOrderedSequence2(bytes.Keys, CharLess);
509507
var count :- U32ToBigEndian(|m|);
510-
var body :- CollectMap(keys, bytes);
508+
var body :- MapAttrToBytes(bytes);
511509
Success(count + body)
512510
case L(l) =>
513511
var count :- U32ToBigEndian(|l|);
@@ -524,6 +522,11 @@ module DynamoToStruct {
524522
Success(baseBytes)
525523
}
526524

525+
function method MapAttrToBytes(bytes: map<AttributeName, Result<seq<uint8>, string>>): (ret: Result<seq<uint8>, string>) {
526+
var bytes :- SimplifyMapValue(bytes);
527+
CollectMap(bytes)
528+
}
529+
527530
lemma BigEndianLemma()
528531
ensures U32ToBigEndian(3) == Success([0,0,0,3])
529532
ensures BigEndianToU32([0,0,0,3]) == Success(3)
@@ -712,6 +715,18 @@ module DynamoToStruct {
712715
// Map to Bytes
713716
// input sequence is already serialized
714717
function method {:tailrecursion} {:opaque} CollectMap(
718+
mapToSerialize : map<AttributeName, seq<uint8>>,
719+
serialized : seq<uint8> := []
720+
)
721+
: (ret : Result<seq<uint8>, string>)
722+
ensures (ret.Success? && |mapToSerialize| == 0) ==> (ret.value == serialized)
723+
ensures (ret.Success? && |mapToSerialize| == 0) ==> (|ret.value| == |serialized|)
724+
{
725+
var keys := SortedSets.ComputeSetToOrderedSequence2(mapToSerialize.Keys, CharLess);
726+
CollectOrderedMapSubset(keys, mapToSerialize, serialized)
727+
}
728+
729+
function method {:tailrecursion} {:opaque} CollectOrderedMapSubset(
715730
keys : seq<AttributeName>,
716731
mapToSerialize : map<AttributeName, seq<uint8>>,
717732
serialized : seq<uint8> := []
@@ -725,7 +740,7 @@ module DynamoToStruct {
725740
Success(serialized)
726741
else
727742
var data :- SerializeMapItem(keys[0], mapToSerialize[keys[0]]);
728-
CollectMap(keys[1..], mapToSerialize, serialized + data)
743+
CollectOrderedMapSubset(keys[1..], mapToSerialize, serialized + data)
729744
}
730745

731746
function method BoolToUint8(b : bool) : uint8
@@ -887,6 +902,8 @@ module DynamoToStruct {
887902
ensures ret.Success? ==> ret.value.len <= origSerializedSize
888903
decreases |serialized|
889904
{
905+
ghost var serializedInitial := serialized;
906+
890907
if remainingCount == 0 then
891908
Success(resultMap)
892909
else
@@ -903,6 +920,8 @@ module DynamoToStruct {
903920
var key :- UTF8.Decode(serialized[..len]);
904921
var serialized := serialized[len..];
905922

923+
assert |serialized| + 6 + len == |serializedInitial|;
924+
906925
// get typeId of value
907926
:- Need(2 <= |serialized|, "Out of bytes reading Map Value");
908927
:- Need(IsValid_AttributeName(key), "Key is not valid AttributeName");
@@ -911,6 +930,7 @@ module DynamoToStruct {
911930

912931
// get value and construct result
913932
var nval :- BytesToAttr(serialized, TerminalTypeId_value, true);
933+
var serialized := serialized[nval.len..];
914934

915935
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
916936
//# This sequence MUST NOT contain duplicate [Map Keys](#map-key).
@@ -919,7 +939,9 @@ module DynamoToStruct {
919939
//# - Conversion from a Structured Data Map MUST fail if it has duplicate keys
920940
:- Need(key !in resultMap.val.M, "Duplicate key in map.");
921941
var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]);
922-
DeserializeMap(serialized[nval.len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultMap.len + nval.len + 8 + len))
942+
var newResultMap := AttrValueAndLength(nattr, resultMap.len + nval.len + 8 + len);
943+
assert |serialized| + newResultMap.len == origSerializedSize;
944+
DeserializeMap(serialized, remainingCount - 1, origSerializedSize, newResultMap)
923945
}
924946

925947
// Bytes to AttributeValue

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy

+1-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0
3-
include "../../../../submodules/MaterialProviders/StandardLibrary/src/StandardLibrary.dfy"
4-
include "../../DynamoDbEncryption/src/Index.dfy"
5-
include "../../../../submodules/MaterialProviders/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy"
6-
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy"
3+
include "../src/Index.dfy"
74

85
module DynamoDbEncryptionBranchKeyIdSupplierTest {
96
import opened Wrappers

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy

+3-2
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ module TestDynamoDBFilterExpr {
112112
var exprString := ParsedExprToString(newContext.expr);
113113
expect exprString == "aws_dbe_b_std2 < :A AND #Field4 = :B";
114114
}
115-
method {:test} TestBasicBeacons() {
115+
method {:test} {:vcs_split_on_every_assert} TestBasicBeacons() {
116116
var context := ExprContext (
117117
expr := Some("std2 < :A AND #Field4 = :B"),
118118
values:= Some(map[
@@ -128,7 +128,8 @@ module TestDynamoDBFilterExpr {
128128
expect_equal(newContext.expr, Some("aws_dbe_b_std2 < :A AND #Field4 = :B"));
129129
var newName := "aws_dbe_b_std4";
130130
expect IsValid_AttributeName(newName);
131-
expect_equal(newContext.names, Some(map["#Field4" := newName]));
131+
var expectedNames: DDB.ExpressionAttributeNameMap := map["#Field4" := newName];
132+
expect_equal(newContext.names, Some(expectedNames));
132133
var itemBeacons :- expect beaconVersion.GenerateBeacons(SimpleItem);
133134
expect "aws_dbe_b_std2" in itemBeacons;
134135
expect "aws_dbe_b_std4" in itemBeacons;

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy

+12-7
Original file line numberDiff line numberDiff line change
@@ -104,26 +104,32 @@ Dafny decided it can't do this anymore
104104
var tableConfig := config.tableEncryptionConfigs[tableName];
105105
var decryptedItems : DDB.ItemList := [];
106106
var encryptedItems := input.sdkOutput.Items.value;
107-
ghost var historySize := |tableConfig.itemEncryptor.History.DecryptItem|;
107+
ghost var originalHistory := tableConfig.itemEncryptor.History.DecryptItem;
108+
ghost var historySize := |originalHistory|;
108109
for x := 0 to |encryptedItems|
109110
invariant |decryptedItems| == x
110111

111-
invariant
112-
&& (|tableConfig.itemEncryptor.History.DecryptItem| ==
113-
|old(tableConfig.itemEncryptor.History.DecryptItem)| + |decryptedItems|)
112+
invariant (|tableConfig.itemEncryptor.History.DecryptItem| == |originalHistory| + |decryptedItems|)
114113

115114
invariant (forall i : nat | historySize <= i < |decryptedItems|+historySize ::
116115
var item := tableConfig.itemEncryptor.History.DecryptItem[i];
117116
&& item.output.Success?
118-
&& item.input.encryptedItem == input.sdkOutput.Items.value[i-historySize]
117+
&& item.input.encryptedItem == encryptedItems[i-historySize]
119118
&& item.output.value.plaintextItem == decryptedItems[i-historySize])
119+
120+
invariant ValidConfig?(config)
120121
{
121122
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query
122123
//# Each of these entries on the original response MUST be replaced
123124
//# with the resulting decrypted [DynamoDB Item](./decrypt-item.md#dynamodb-item-1).
124-
var decryptRes := tableConfig.itemEncryptor.DecryptItem(EncTypes.DecryptItemInput(encryptedItem:=encryptedItems[x]));
125+
var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]);
126+
var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
127+
ghost var newHistoryEvent := tableConfig.itemEncryptor.History.DecryptItem[historySize + x];
128+
assert newHistoryEvent == EncTypes.DafnyCallEvent(decryptInput, decryptRes);
129+
125130
var decrypted :- MapError(decryptRes);
126131
decryptedItems := decryptedItems + [decrypted.plaintextItem];
132+
assert newHistoryEvent.output.value.plaintextItem == decrypted.plaintextItem;
127133
}
128134

129135
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query
@@ -133,4 +139,3 @@ Dafny decided it can't do this anymore
133139
return Success(QueryOutputTransformOutput(transformedOutput := finalResult));
134140
}
135141
}
136-

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy

+12-5
Original file line numberDiff line numberDiff line change
@@ -101,26 +101,33 @@ module ScanTransform {
101101
var tableConfig := config.tableEncryptionConfigs[tableName];
102102
var decryptedItems : DDB.ItemList := [];
103103
var encryptedItems := input.sdkOutput.Items.value;
104-
ghost var historySize := |tableConfig.itemEncryptor.History.DecryptItem|;
104+
ghost var originalHistory := tableConfig.itemEncryptor.History.DecryptItem;
105+
ghost var historySize := |originalHistory|;
105106
for x := 0 to |encryptedItems|
106107
invariant |decryptedItems| == x
107-
invariant
108-
&& (|tableConfig.itemEncryptor.History.DecryptItem| ==
109-
|old(tableConfig.itemEncryptor.History.DecryptItem)| + |decryptedItems|)
108+
invariant (|tableConfig.itemEncryptor.History.DecryptItem| == |originalHistory| + |decryptedItems|)
110109

111110
invariant (forall i : nat | historySize <= i < |decryptedItems|+historySize ::
112111
var item := tableConfig.itemEncryptor.History.DecryptItem[i];
113112
&& item.output.Success?
114113
&& item.input.encryptedItem == input.sdkOutput.Items.value[i-historySize]
115114
&& item.output.value.plaintextItem == decryptedItems[i-historySize])
115+
116+
invariant ValidConfig?(config)
116117
{
117118
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan
118119
//# Each of these entries on the original response MUST be replaced
119120
//# with the resulting decrypted
120121
//# [DynamoDB Item](./decrypt-item.md#dynamodb-item-1).
121-
var decryptRes := tableConfig.itemEncryptor.DecryptItem(EncTypes.DecryptItemInput(encryptedItem:=encryptedItems[x]));
122+
123+
var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]);
124+
var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
125+
ghost var newHistoryEvent := tableConfig.itemEncryptor.History.DecryptItem[historySize + x];
126+
assert newHistoryEvent == EncTypes.DafnyCallEvent(decryptInput, decryptRes);
127+
122128
var decrypted :- MapError(decryptRes);
123129
decryptedItems := decryptedItems + [decrypted.plaintextItem];
130+
assert newHistoryEvent.output.value.plaintextItem == decrypted.plaintextItem;
124131
}
125132
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan
126133
//# The resulting decrypted response MUST be [filtered](ddb-support.md#scanoutputforbeacons) from the result.

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactGetItemsTransform.dfy

+2-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ module TransactGetItemsTransform {
1919
return Success(TransactGetItemsInputTransformOutput(transformedInput := input.sdkInput));
2020
}
2121

22-
method Output(config: Config, input: TransactGetItemsOutputTransformInput)
22+
method {:vcs_split_on_every_assert} Output(config: Config, input: TransactGetItemsOutputTransformInput)
2323
returns (output: Result<TransactGetItemsOutputTransformOutput, Error>)
2424
requires ValidConfig?(config)
2525
ensures ValidConfig?(config)
@@ -43,6 +43,7 @@ module TransactGetItemsTransform {
4343
var encryptedItems := input.sdkOutput.Responses.value;
4444
for x := 0 to |encryptedItems|
4545
invariant |decryptedItems| == x
46+
invariant ValidConfig?(config)
4647
{
4748
var tableName := input.originalInput.TransactItems[x].Get.TableName;
4849
if tableName !in config.tableEncryptionConfigs {

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy

+1-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0
3-
include "../../DynamoDbEncryptionTransforms/src/Index.dfy"
4-
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy"
3+
include "../src/Index.dfy"
54

65
module TestFixtures {
76
import opened Wrappers

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDynamoDbEncryptionItemEncryptorTypes.dfy

+4-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,10 @@
33
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
44
include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
55
include "../../DynamoDbEncryption/src/Index.dfy"
6-
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/src/Index.dfy"
6+
// TODO begin manual update
7+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy"
8+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy"
9+
// TODO end manual update
710
include "../../../../submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy"
811
include "../../../../submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy"
912
module {:extern "Dafny.Aws.Cryptography.DynamoDbEncryption.ItemEncryptor.Types" } AwsCryptographyDynamoDbEncryptionItemEncryptorTypes

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbEncryptionItemEncryptorOperations.dfy

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0
33
include "../Model/AwsCryptographyDynamoDbEncryptionItemEncryptorTypes.dfy"
4-
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy"
4+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy"
55
include "../../DynamoDbEncryption/src/DynamoToStruct.dfy"
66
include "../../DynamoDbEncryption/src/SearchInfo.dfy"
77
include "Util.dfy"

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy

+5-2
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ module
4343
!(ReservedPrefix <= attr)
4444
}
4545

46-
method DynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig)
46+
method {:vcs_split_on_every_assert} DynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig)
4747
returns (res: Result<DynamoDbItemEncryptorClient, Error>)
4848
ensures res.Success? ==>
4949
&& res.value.config.tableName == config.tableName
@@ -227,7 +227,10 @@ module
227227
internalLegacyConfig := internalLegacyConfig,
228228
plaintextPolicy := plaintextPolicy
229229
);
230-
assert Operations.ValidInternalConfig?(internalConfig); // Dafny needs some extra help here
230+
231+
// Dafny needs some extra help here
232+
assert (forall attribute <- internalConfig.attributeActions.Keys :: !(ReservedPrefix <= attribute));
233+
assert Operations.ValidInternalConfig?(internalConfig);
231234

232235
var client := new DynamoDbItemEncryptorClient(internalConfig);
233236
return Success(client);

0 commit comments

Comments
 (0)