feat: dotnet examples (#482)

* feat: dotnet examples
aws · Nov 18, 2023 · 2d36a34 · 2d36a34
1 parent 8f8f37f
commit 2d36a34
Show file tree

Hide file tree

Showing 56 changed files with 9,130 additions and 2,189 deletions.
diff --git a/.github/workflows/ci_examples_net.yml b/.github/workflows/ci_examples_net.yml
@@ -0,0 +1,69 @@
+# This workflow performs tests in .NET.
+name: dotnet examples
+
+on: 
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  dotNetExamples:
+    # Don't run the nightly build on forks
+    if: (github.repository_owner == 'aws')
+    strategy:
+      matrix:
+        library: [
+          DynamoDbEncryption,
+        ]
+        dotnet-version: [ '6.0.x' ]
+        os: [
+          # TODO windows-latest,
+          # ubuntu-latest,
+          macos-latest,
+        ]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive        
+
+      - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: ${{ matrix.dotnet-version }}
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ '4.2.0' }}
+
+      - name: Download Dependencies 
+        working-directory: ./${{ matrix.library }}
+        run: make setup_net
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
+          role-session-name: DDBEC-Dafny-Net-Tests
+
+      - name: Compile ${{ matrix.library }} implementation
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_net CORES=$CORES
+      - name: Run Examples
+        working-directory: ./Examples/runtimes/net
+        shell: bash
+        run: |
+          dotnet run
diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
@@ -0,0 +1,64 @@
+# This workflow performs test vectors in DotNet.
+name: Library DotNet Test Vectors
+
+on: 
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  testDotNet:
+    strategy:
+      matrix:
+        dotnet-version: [ '6.0.x' ]
+        os: [
+          # Run on ubuntu image that comes pre-configured with docker
+          ubuntu-latest
+        ]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Setup DynamoDB Local
+        uses: rrainn/[email protected]
+        with:
+          port: 8000
+          cors: '*'
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
+          role-session-name: DDBEC-Dafny-DotNet-Tests
+
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: '4.2.0'
+
+      - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: ${{ matrix.dotnet-version }}
+
+      - name: Build TestVectors implementation
+        shell: bash
+        working-directory: ./TestVectors
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          make transpile_net
+
+      - name: Test TestVectors
+        working-directory: ./TestVectors/runtimes/net
+        run: |
+          cp ../java/*.json .
+          # dotnet run
+          echo can't build until we make type conversions public
+          echo can't run until we update MPL/ComAmazonawsDynamodb
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy
@@ -30,7 +30,7 @@ module BatchGetItemTransform {
       && output.value.transformedOutput.Responses.Some?
       // true but expensive -- input.sdkOutput.Responses.value.Keys == output.value.transformedOutput.Responses.value.Keys
   {
-    if input.sdkOutput.Responses.None? {
+    if NoMap(input.sdkOutput.Responses) {
       return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
     }
     var tableNames := input.sdkOutput.Responses.value.Keys;

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DeleteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DeleteItemTransform.dfy
@@ -25,7 +25,7 @@ module DeleteItemTransform {
       //= type=implication
       //# The DeleteItem request MUST NOT refer to any legacy parameters,
       //# specifically Expected and ConditionalOperator MUST NOT be set.
-      && input.sdkInput.Expected.None?
+      && NoMap(input.sdkInput.Expected)
       && input.sdkInput.ConditionalOperator.None?
 
       //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#validate-before-deleteitem
@@ -52,7 +52,7 @@ module DeleteItemTransform {
 
   {
     if input.sdkInput.TableName in config.tableEncryptionConfigs {
-      :- Need(input.sdkInput.Expected.None?, E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
+      :- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
       :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
 
       var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
@@ -84,7 +84,7 @@ module DeleteItemTransform {
     ensures (
       && output.Success?
       && input.originalInput.TableName in config.tableEncryptionConfigs
-      && input.sdkOutput.Attributes.Some?
+      && !NoMap(input.sdkOutput.Attributes)
     ) ==>
       && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
       && var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
@@ -129,7 +129,7 @@ module DeleteItemTransform {
     modifies ModifiesConfig(config)
   {
     var tableName := input.originalInput.TableName;
-    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
+    if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Attributes)
       {
       return Success(DeleteItemOutputTransformOutput(transformedOutput := input.sdkOutput));
     }

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
@@ -23,6 +23,17 @@ module DynamoDbMiddlewareSupport {
   import Util = DynamoDbEncryptionUtil
   import SI = SearchableEncryptionInfo
 
+
+  predicate method NoMap<X,Y>(m : Option<map<X,Y>>)
+  {
+    m.None? || |m.value| == 0
+  }
+
+  predicate method NoList<X>(m : Option<seq<X>>)
+  {
+    m.None? || |m.value| == 0
+  }
+
   // IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
   // Generally this means that no attribute names starts with "aws_dbe_"
   function method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/GetItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/GetItemTransform.dfy
@@ -32,8 +32,8 @@ module GetItemTransform {
     //# with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
     //# equal to the `TableName` on the GetItem request.
     ensures output.Success? && input.originalInput.TableName !in config.tableEncryptionConfigs ==> output.value.transformedOutput == input.sdkOutput
-    ensures output.Success? && input.sdkOutput.Item.None? ==> output.value.transformedOutput.Item.None?
-    ensures output.Success? && input.originalInput.TableName in config.tableEncryptionConfigs && input.sdkOutput.Item.Some? ==>
+    ensures output.Success? && NoMap(input.sdkOutput.Item) ==> NoMap(output.value.transformedOutput.Item)
+    ensures output.Success? && input.originalInput.TableName in config.tableEncryptionConfigs && !NoMap(input.sdkOutput.Item) ==>
       var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
       var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
       var newHistory := tableConfig.itemEncryptor.History.DecryptItem;
@@ -67,7 +67,7 @@ module GetItemTransform {
     modifies ModifiesConfig(config)
   {
     var tableName := input.originalInput.TableName;
-    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Item.None? {
+    if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Item) {
       return Success(GetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
     }
     var tableConfig := config.tableEncryptionConfigs[tableName];

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy
@@ -32,7 +32,7 @@ module PutItemTransform {
       //= type=implication
       //# The PutItem request MUST NOT refer to any legacy parameters,
       //# specifically Expected and ConditionalOperator MUST NOT be set.
-      && input.sdkInput.Expected.None? && input.sdkInput.ConditionalOperator.None?
+      && NoMap(input.sdkInput.Expected) && input.sdkInput.ConditionalOperator.None?
 
       // && var oldHistory := old(tableConfig.itemEncryptor.History.EncryptItem);
       // && var newHistory := tableConfig.itemEncryptor.History.EncryptItem;
@@ -60,12 +60,9 @@ module PutItemTransform {
     }
     var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
 
-    if input.sdkInput.Expected.Some? {
-      return MakeError("Legacy parameter 'Expected' not supported in PutItem with Encryption.");
-    }
-    if input.sdkInput.ConditionalOperator.Some? {
-      return MakeError("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption.");
-    }
+    :- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in PutItem with Encryption."));
+    :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption."));
+
     var _ :- IsWriteable(tableConfig, input.sdkInput.Item);
     var _ :- TestConditionExpression(tableConfig,
       input.sdkInput.ConditionExpression,
@@ -101,7 +98,7 @@ module PutItemTransform {
     ensures (
       && output.Success?
       && input.originalInput.TableName in config.tableEncryptionConfigs
-      && input.sdkOutput.Attributes.Some?
+      && !NoMap(input.sdkOutput.Attributes)
     ) ==>
       && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
       && var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
@@ -146,7 +143,7 @@ module PutItemTransform {
     modifies ModifiesConfig(config)
   {
     var tableName := input.originalInput.TableName;
-    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
+    if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Attributes)
       {
       return Success(PutItemOutputTransformOutput(transformedOutput := input.sdkOutput));
     }

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy
@@ -23,27 +23,28 @@ module QueryTransform {
     //# If the `TableName` in the request does not refer to an [encrypted-table](#encrypted-table),
     //# the Query request MUST be unchanged.
     ensures input.sdkInput.TableName !in config.tableEncryptionConfigs ==>
-      && output.Success?
-      && output.value.transformedInput == input.sdkInput
+              && output.Success?
+              && output.value.transformedInput == input.sdkInput
 
     ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
-      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#modify-before-query
-      //= type=implication
-      //# The Query request MUST NOT refer to any legacy parameters,
-      //# specifically AttributesToGet, KeyConditions, QueryFilter and ConditionalOperator MUST NOT be set.
-      && input.sdkInput.AttributesToGet.None?
-      && input.sdkInput.KeyConditions.None?
-      && input.sdkInput.QueryFilter.None?
-      && input.sdkInput.ConditionalOperator.None?
+              //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#modify-before-query
+              //= type=implication
+              //# The Query request MUST NOT refer to any legacy parameters,
+              //# specifically AttributesToGet, KeyConditions, QueryFilter and ConditionalOperator MUST NOT be set.
+              && NoList(input.sdkInput.AttributesToGet)
+              && NoMap(input.sdkInput.KeyConditions)
+              && NoMap(input.sdkInput.QueryFilter)
+              && input.sdkInput.ConditionalOperator.None?
   {
     if input.sdkInput.TableName !in config.tableEncryptionConfigs {
       return Success(QueryInputTransformOutput(transformedInput := input.sdkInput));
     } else {
-      :- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
-      :- Need(input.sdkInput.KeyConditions.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
-      :- Need(input.sdkInput.QueryFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
-      :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
+      :- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in Query with Encryption"));
+      :- Need(NoMap(input.sdkInput.KeyConditions), E("Legacy parameter 'KeyConditions' not supported in Query with Encryption"));
+      :- Need(NoMap(input.sdkInput.QueryFilter), E("Legacy parameter 'QueryFilter' not supported in Query with Encryption"));
+      :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in Query with Encryption"));
       var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
+
       var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput);
       return Success(QueryInputTransformOutput(transformedInput := finalResult));
     }
@@ -61,15 +62,15 @@ module QueryTransform {
     ensures ValidConfig?(config)
     modifies ModifiesConfig(config)
 
-    ensures input.originalInput.TableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? ==>
-      && output.Success?
-      && output.value.transformedOutput == input.sdkOutput
+    ensures input.originalInput.TableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) ==>
+              && output.Success?
+              && output.value.transformedOutput == input.sdkOutput
 
     ensures output.Success?  && input.sdkOutput.Items.Some? ==> output.value.transformedOutput.Items.Some?
-    ensures output.Success?  && input.sdkOutput.Items.None? ==> output.value.transformedOutput.Items.None?
+    ensures output.Success?  && NoList(input.sdkOutput.Items) ==> NoList(output.value.transformedOutput.Items)
   {
     var tableName := input.originalInput.TableName;
-    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? {
+    if tableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) {
       return Success(QueryOutputTransformOutput(transformedOutput := input.sdkOutput));
     }
     var tableConfig := config.tableEncryptionConfigs[tableName];

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
@@ -31,17 +31,18 @@ module ScanTransform {
     //# The Scan request MUST NOT refer to any legacy parameters,
     //# specifically AttributesToGet, ScanFilter and ConditionalOperator MUST NOT be set.
     ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
-              && input.sdkInput.AttributesToGet.None?
-              && input.sdkInput.ScanFilter.None?
+              && NoList(input.sdkInput.AttributesToGet)
+              && NoMap(input.sdkInput.ScanFilter)
               && input.sdkInput.ConditionalOperator.None?
   {
     if input.sdkInput.TableName !in config.tableEncryptionConfigs {
       return Success(ScanInputTransformOutput(transformedInput := input.sdkInput));
     } else {
-      :- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
-      :- Need(input.sdkInput.ScanFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
+      :- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
+      :- Need(NoMap(input.sdkInput.ScanFilter), E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
       :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
       var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
+
       var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput);
       return Success(ScanInputTransformOutput(transformedInput := finalResult));
     }
@@ -59,15 +60,15 @@ module ScanTransform {
     ensures ValidConfig?(config)
     modifies ModifiesConfig(config)
 
-    ensures input.originalInput.TableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? ==>
+    ensures input.originalInput.TableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) ==>
               && output.Success?
               && output.value.transformedOutput == input.sdkOutput
 
-    ensures output.Success?  && input.sdkOutput.Items.None?  ==> output.value.transformedOutput.Items.None?
+    ensures output.Success?  && NoList(input.sdkOutput.Items)  ==> NoList(output.value.transformedOutput.Items)
     ensures output.Success?  && input.sdkOutput.Items.Some?  ==> output.value.transformedOutput.Items.Some?
   {
     var tableName := input.originalInput.TableName;
-    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? {
+    if tableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) {
       return Success(ScanOutputTransformOutput(transformedOutput := input.sdkOutput));
     }
     var tableConfig := config.tableEncryptionConfigs[tableName];

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactGetItemsTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactGetItemsTransform.dfy
@@ -25,15 +25,15 @@ module TransactGetItemsTransform {
     ensures ValidConfig?(config)
     modifies ModifiesConfig(config)
 
-    ensures input.sdkOutput.Responses.None? ==>
+    ensures NoList(input.sdkOutput.Responses) ==>
       && output.Success?
       && output.value.transformedOutput == input.sdkOutput
 
     ensures output.Success? && input.sdkOutput.Responses.Some? ==>
       && output.value.transformedOutput.Responses.Some?
       && |output.value.transformedOutput.Responses.value| == |input.originalInput.TransactItems|
   {
-    if input.sdkOutput.Responses.None? {
+    if NoList(input.sdkOutput.Responses) {
       return Success(TransactGetItemsOutputTransformOutput(transformedOutput := input.sdkOutput));
     }
     if |input.sdkOutput.Responses.value| != |input.originalInput.TransactItems| {
@@ -50,7 +50,7 @@ module TransactGetItemsTransform {
         decryptedItems := decryptedItems + [encryptedItems[x]];
       } else {
         var tableConfig := config.tableEncryptionConfigs[tableName];
-        if encryptedItems[x].Item.None? {
+        if NoMap(encryptedItems[x].Item) {
           decryptedItems := decryptedItems + [DDB.ItemResponse(Item := None)];
         } else {
           //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-transactgetitems