Skip to content

Commit 2d36a34

Browse files
ajewellamzajewellamz
authored
feat: dotnet examples (#482)
* feat: dotnet examples
1 parent 8f8f37f commit 2d36a34

File tree

56 files changed

+9130
-2189
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+9130
-2189
lines changed

‎.github/workflows/ci_examples_net.yml

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
# This workflow performs tests in .NET.
2+
name: dotnet examples
3+
4+
on:
5+
pull_request:
6+
push:
7+
branches:
8+
- main
9+
10+
jobs:
11+
dotNetExamples:
12+
# Don't run the nightly build on forks
13+
if: (github.repository_owner == 'aws')
14+
strategy:
15+
matrix:
16+
library: [
17+
DynamoDbEncryption,
18+
]
19+
dotnet-version: [ '6.0.x' ]
20+
os: [
21+
# TODO windows-latest,
22+
# ubuntu-latest,
23+
macos-latest,
24+
]
25+
runs-on: ${{ matrix.os }}
26+
permissions:
27+
id-token: write
28+
contents: read
29+
env:
30+
DOTNET_CLI_TELEMETRY_OPTOUT: 1
31+
DOTNET_NOLOGO: 1
32+
steps:
33+
- uses: actions/checkout@v3
34+
with:
35+
submodules: recursive
36+
37+
- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
38+
uses: actions/setup-dotnet@v3
39+
with:
40+
dotnet-version: ${{ matrix.dotnet-version }}
41+
42+
- name: Setup Dafny
43+
uses: dafny-lang/[email protected]
44+
with:
45+
dafny-version: ${{ '4.2.0' }}
46+
47+
- name: Download Dependencies
48+
working-directory: ./${{ matrix.library }}
49+
run: make setup_net
50+
51+
- name: Configure AWS Credentials
52+
uses: aws-actions/configure-aws-credentials@v2
53+
with:
54+
aws-region: us-west-2
55+
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
56+
role-session-name: DDBEC-Dafny-Net-Tests
57+
58+
- name: Compile ${{ matrix.library }} implementation
59+
shell: bash
60+
working-directory: ./${{ matrix.library }}
61+
run: |
62+
# This works because `node` is installed by default on GHA runners
63+
CORES=$(node -e 'console.log(os.cpus().length)')
64+
make transpile_net CORES=$CORES
65+
- name: Run Examples
66+
working-directory: ./Examples/runtimes/net
67+
shell: bash
68+
run: |
69+
dotnet run

‎.github/workflows/ci_test_vector_net.yml

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
# This workflow performs test vectors in DotNet.
2+
name: Library DotNet Test Vectors
3+
4+
on:
5+
pull_request:
6+
push:
7+
branches:
8+
- main
9+
10+
jobs:
11+
testDotNet:
12+
strategy:
13+
matrix:
14+
dotnet-version: [ '6.0.x' ]
15+
os: [
16+
# Run on ubuntu image that comes pre-configured with docker
17+
ubuntu-latest
18+
]
19+
runs-on: ${{ matrix.os }}
20+
permissions:
21+
id-token: write
22+
contents: read
23+
steps:
24+
- name: Setup DynamoDB Local
25+
uses: rrainn/[email protected]
26+
with:
27+
port: 8000
28+
cors: '*'
29+
30+
- name: Configure AWS Credentials
31+
uses: aws-actions/configure-aws-credentials@v2
32+
with:
33+
aws-region: us-west-2
34+
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
35+
role-session-name: DDBEC-Dafny-DotNet-Tests
36+
37+
- uses: actions/checkout@v3
38+
with:
39+
submodules: recursive
40+
41+
- name: Setup Dafny
42+
uses: dafny-lang/[email protected]
43+
with:
44+
dafny-version: '4.2.0'
45+
46+
- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
47+
uses: actions/setup-dotnet@v3
48+
with:
49+
dotnet-version: ${{ matrix.dotnet-version }}
50+
51+
- name: Build TestVectors implementation
52+
shell: bash
53+
working-directory: ./TestVectors
54+
run: |
55+
# This works because `node` is installed by default on GHA runners
56+
make transpile_net
57+
58+
- name: Test TestVectors
59+
working-directory: ./TestVectors/runtimes/net
60+
run: |
61+
cp ../java/*.json .
62+
# dotnet run
63+
echo can't build until we make type conversions public
64+
echo can't run until we update MPL/ComAmazonawsDynamodb

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ module BatchGetItemTransform {
3030
&& output.value.transformedOutput.Responses.Some?
3131
// true but expensive -- input.sdkOutput.Responses.value.Keys == output.value.transformedOutput.Responses.value.Keys
3232
{
33-
if input.sdkOutput.Responses.None? {
33+
if NoMap(input.sdkOutput.Responses) {
3434
return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
3535
}
3636
var tableNames := input.sdkOutput.Responses.value.Keys;

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ module DeleteItemTransform {
2525
//= type=implication
2626
//# The DeleteItem request MUST NOT refer to any legacy parameters,
2727
//# specifically Expected and ConditionalOperator MUST NOT be set.
28-
&& input.sdkInput.Expected.None?
28+
&& NoMap(input.sdkInput.Expected)
2929
&& input.sdkInput.ConditionalOperator.None?
3030

3131
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#validate-before-deleteitem
@@ -52,7 +52,7 @@ module DeleteItemTransform {
5252

5353
{
5454
if input.sdkInput.TableName in config.tableEncryptionConfigs {
55-
:- Need(input.sdkInput.Expected.None?, E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
55+
:- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
5656
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
5757

5858
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
@@ -84,7 +84,7 @@ module DeleteItemTransform {
8484
ensures (
8585
&& output.Success?
8686
&& input.originalInput.TableName in config.tableEncryptionConfigs
87-
&& input.sdkOutput.Attributes.Some?
87+
&& !NoMap(input.sdkOutput.Attributes)
8888
) ==>
8989
&& var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
9090
&& var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
@@ -129,7 +129,7 @@ module DeleteItemTransform {
129129
modifies ModifiesConfig(config)
130130
{
131131
var tableName := input.originalInput.TableName;
132-
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
132+
if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Attributes)
133133
{
134134
return Success(DeleteItemOutputTransformOutput(transformedOutput := input.sdkOutput));
135135
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,17 @@ module DynamoDbMiddlewareSupport {
2323
import Util = DynamoDbEncryptionUtil
2424
import SI = SearchableEncryptionInfo
2525

26+
27+
predicate method NoMap<X,Y>(m : Option<map<X,Y>>)
28+
{
29+
m.None? || |m.value| == 0
30+
}
31+
32+
predicate method NoList<X>(m : Option<seq<X>>)
33+
{
34+
m.None? || |m.value| == 0
35+
}
36+
2637
// IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
2738
// Generally this means that no attribute names starts with "aws_dbe_"
2839
function method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap)

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,8 @@ module GetItemTransform {
3232
//# with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
3333
//# equal to the `TableName` on the GetItem request.
3434
ensures output.Success? && input.originalInput.TableName !in config.tableEncryptionConfigs ==> output.value.transformedOutput == input.sdkOutput
35-
ensures output.Success? && input.sdkOutput.Item.None? ==> output.value.transformedOutput.Item.None?
36-
ensures output.Success? && input.originalInput.TableName in config.tableEncryptionConfigs && input.sdkOutput.Item.Some? ==>
35+
ensures output.Success? && NoMap(input.sdkOutput.Item) ==> NoMap(output.value.transformedOutput.Item)
36+
ensures output.Success? && input.originalInput.TableName in config.tableEncryptionConfigs && !NoMap(input.sdkOutput.Item) ==>
3737
var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
3838
var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
3939
var newHistory := tableConfig.itemEncryptor.History.DecryptItem;
@@ -67,7 +67,7 @@ module GetItemTransform {
6767
modifies ModifiesConfig(config)
6868
{
6969
var tableName := input.originalInput.TableName;
70-
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Item.None? {
70+
if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Item) {
7171
return Success(GetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
7272
}
7373
var tableConfig := config.tableEncryptionConfigs[tableName];

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

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ module PutItemTransform {
3232
//= type=implication
3333
//# The PutItem request MUST NOT refer to any legacy parameters,
3434
//# specifically Expected and ConditionalOperator MUST NOT be set.
35-
&& input.sdkInput.Expected.None? && input.sdkInput.ConditionalOperator.None?
35+
&& NoMap(input.sdkInput.Expected) && input.sdkInput.ConditionalOperator.None?
3636

3737
// && var oldHistory := old(tableConfig.itemEncryptor.History.EncryptItem);
3838
// && var newHistory := tableConfig.itemEncryptor.History.EncryptItem;
@@ -60,12 +60,9 @@ module PutItemTransform {
6060
}
6161
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
6262

63-
if input.sdkInput.Expected.Some? {
64-
return MakeError("Legacy parameter 'Expected' not supported in PutItem with Encryption.");
65-
}
66-
if input.sdkInput.ConditionalOperator.Some? {
67-
return MakeError("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption.");
68-
}
63+
:- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in PutItem with Encryption."));
64+
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption."));
65+
6966
var _ :- IsWriteable(tableConfig, input.sdkInput.Item);
7067
var _ :- TestConditionExpression(tableConfig,
7168
input.sdkInput.ConditionExpression,
@@ -101,7 +98,7 @@ module PutItemTransform {
10198
ensures (
10299
&& output.Success?
103100
&& input.originalInput.TableName in config.tableEncryptionConfigs
104-
&& input.sdkOutput.Attributes.Some?
101+
&& !NoMap(input.sdkOutput.Attributes)
105102
) ==>
106103
&& var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
107104
&& var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
@@ -146,7 +143,7 @@ module PutItemTransform {
146143
modifies ModifiesConfig(config)
147144
{
148145
var tableName := input.originalInput.TableName;
149-
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
146+
if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Attributes)
150147
{
151148
return Success(PutItemOutputTransformOutput(transformedOutput := input.sdkOutput));
152149
}

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

Lines changed: 20 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -23,27 +23,28 @@ module QueryTransform {
2323
//# If the `TableName` in the request does not refer to an [encrypted-table](#encrypted-table),
2424
//# the Query request MUST be unchanged.
2525
ensures input.sdkInput.TableName !in config.tableEncryptionConfigs ==>
26-
&& output.Success?
27-
&& output.value.transformedInput == input.sdkInput
26+
&& output.Success?
27+
&& output.value.transformedInput == input.sdkInput
2828

2929
ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
30-
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#modify-before-query
31-
//= type=implication
32-
//# The Query request MUST NOT refer to any legacy parameters,
33-
//# specifically AttributesToGet, KeyConditions, QueryFilter and ConditionalOperator MUST NOT be set.
34-
&& input.sdkInput.AttributesToGet.None?
35-
&& input.sdkInput.KeyConditions.None?
36-
&& input.sdkInput.QueryFilter.None?
37-
&& input.sdkInput.ConditionalOperator.None?
30+
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#modify-before-query
31+
//= type=implication
32+
//# The Query request MUST NOT refer to any legacy parameters,
33+
//# specifically AttributesToGet, KeyConditions, QueryFilter and ConditionalOperator MUST NOT be set.
34+
&& NoList(input.sdkInput.AttributesToGet)
35+
&& NoMap(input.sdkInput.KeyConditions)
36+
&& NoMap(input.sdkInput.QueryFilter)
37+
&& input.sdkInput.ConditionalOperator.None?
3838
{
3939
if input.sdkInput.TableName !in config.tableEncryptionConfigs {
4040
return Success(QueryInputTransformOutput(transformedInput := input.sdkInput));
4141
} else {
42-
:- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
43-
:- Need(input.sdkInput.KeyConditions.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
44-
:- Need(input.sdkInput.QueryFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
45-
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
42+
:- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in Query with Encryption"));
43+
:- Need(NoMap(input.sdkInput.KeyConditions), E("Legacy parameter 'KeyConditions' not supported in Query with Encryption"));
44+
:- Need(NoMap(input.sdkInput.QueryFilter), E("Legacy parameter 'QueryFilter' not supported in Query with Encryption"));
45+
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in Query with Encryption"));
4646
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
47+
4748
var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput);
4849
return Success(QueryInputTransformOutput(transformedInput := finalResult));
4950
}
@@ -61,15 +62,15 @@ module QueryTransform {
6162
ensures ValidConfig?(config)
6263
modifies ModifiesConfig(config)
6364

64-
ensures input.originalInput.TableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? ==>
65-
&& output.Success?
66-
&& output.value.transformedOutput == input.sdkOutput
65+
ensures input.originalInput.TableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) ==>
66+
&& output.Success?
67+
&& output.value.transformedOutput == input.sdkOutput
6768

6869
ensures output.Success? && input.sdkOutput.Items.Some? ==> output.value.transformedOutput.Items.Some?
69-
ensures output.Success? && input.sdkOutput.Items.None? ==> output.value.transformedOutput.Items.None?
70+
ensures output.Success? && NoList(input.sdkOutput.Items) ==> NoList(output.value.transformedOutput.Items)
7071
{
7172
var tableName := input.originalInput.TableName;
72-
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? {
73+
if tableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) {
7374
return Success(QueryOutputTransformOutput(transformedOutput := input.sdkOutput));
7475
}
7576
var tableConfig := config.tableEncryptionConfigs[tableName];

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -31,17 +31,18 @@ module ScanTransform {
3131
//# The Scan request MUST NOT refer to any legacy parameters,
3232
//# specifically AttributesToGet, ScanFilter and ConditionalOperator MUST NOT be set.
3333
ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
34-
&& input.sdkInput.AttributesToGet.None?
35-
&& input.sdkInput.ScanFilter.None?
34+
&& NoList(input.sdkInput.AttributesToGet)
35+
&& NoMap(input.sdkInput.ScanFilter)
3636
&& input.sdkInput.ConditionalOperator.None?
3737
{
3838
if input.sdkInput.TableName !in config.tableEncryptionConfigs {
3939
return Success(ScanInputTransformOutput(transformedInput := input.sdkInput));
4040
} else {
41-
:- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
42-
:- Need(input.sdkInput.ScanFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
41+
:- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
42+
:- Need(NoMap(input.sdkInput.ScanFilter), E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
4343
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
4444
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
45+
4546
var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput);
4647
return Success(ScanInputTransformOutput(transformedInput := finalResult));
4748
}
@@ -59,15 +60,15 @@ module ScanTransform {
5960
ensures ValidConfig?(config)
6061
modifies ModifiesConfig(config)
6162

62-
ensures input.originalInput.TableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? ==>
63+
ensures input.originalInput.TableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) ==>
6364
&& output.Success?
6465
&& output.value.transformedOutput == input.sdkOutput
6566

66-
ensures output.Success? && input.sdkOutput.Items.None? ==> output.value.transformedOutput.Items.None?
67+
ensures output.Success? && NoList(input.sdkOutput.Items) ==> NoList(output.value.transformedOutput.Items)
6768
ensures output.Success? && input.sdkOutput.Items.Some? ==> output.value.transformedOutput.Items.Some?
6869
{
6970
var tableName := input.originalInput.TableName;
70-
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? {
71+
if tableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) {
7172
return Success(ScanOutputTransformOutput(transformedOutput := input.sdkOutput));
7273
}
7374
var tableConfig := config.tableEncryptionConfigs[tableName];

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,15 +25,15 @@ module TransactGetItemsTransform {
2525
ensures ValidConfig?(config)
2626
modifies ModifiesConfig(config)
2727

28-
ensures input.sdkOutput.Responses.None? ==>
28+
ensures NoList(input.sdkOutput.Responses) ==>
2929
&& output.Success?
3030
&& output.value.transformedOutput == input.sdkOutput
3131

3232
ensures output.Success? && input.sdkOutput.Responses.Some? ==>
3333
&& output.value.transformedOutput.Responses.Some?
3434
&& |output.value.transformedOutput.Responses.value| == |input.originalInput.TransactItems|
3535
{
36-
if input.sdkOutput.Responses.None? {
36+
if NoList(input.sdkOutput.Responses) {
3737
return Success(TransactGetItemsOutputTransformOutput(transformedOutput := input.sdkOutput));
3838
}
3939
if |input.sdkOutput.Responses.value| != |input.originalInput.TransactItems| {
@@ -50,7 +50,7 @@ module TransactGetItemsTransform {
5050
decryptedItems := decryptedItems + [encryptedItems[x]];
5151
} else {
5252
var tableConfig := config.tableEncryptionConfigs[tableName];
53-
if encryptedItems[x].Item.None? {
53+
if NoMap(encryptedItems[x].Item) {
5454
decryptedItems := decryptedItems + [DDB.ItemResponse(Item := None)];
5555
} else {
5656
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-transactgetitems

0 commit comments

Comments
 (0)