Merge branch 'main' into jocorell/new-dafny-cli

ajewellamz · web-flow · commit 6429d3ccbffb · 2024-07-29T10:21:53.000-04:00
diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml
@@ -38,7 +38,7 @@ jobs:
       # and to translate version strings such as "nightly-latest"
       # to an actual DAFNY_VERSION.
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml
@@ -53,7 +53,7 @@ jobs:
           java-version: ${{ matrix.java-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_examples_net.yml b/.github/workflows/ci_examples_net.yml
@@ -46,7 +46,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml
@@ -47,7 +47,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml
@@ -47,7 +47,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml
@@ -56,7 +56,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
@@ -52,7 +52,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml
@@ -52,7 +52,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
@@ -73,7 +73,7 @@ jobs:
       # dafny-reportgenerator requires next6
       # but only 7.0 is installed on macos-12-large
       - name: Setup .NET Core SDK '6.0.x'
-        uses: actions/setup-dotnet@v3
+        uses: actions/setup-dotnet@v4
         with:
           dotnet-version: "6.0.x"
 
diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml
@@ -37,7 +37,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ '4.2.0' }}
 
diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
@@ -73,7 +73,7 @@ jobs:
     steps:
       # We need access to the role that is able to get CI Bot Creds
       - name: Configure AWS Credentials for Release
-        uses: aws-actions/configure-aws-credentials@v2
+        uses: aws-actions/configure-aws-credentials@v4
         with:
           aws-region: us-west-2
           role-to-assume: arn:aws:iam::587316601012:role/GitHub-CI-CI-Bot-Credential-Access-Role-us-west-2
@@ -90,8 +90,14 @@ jobs:
         env:
           GH_TOKEN: ${{ env.GITHUB_AWS_CRYPTO_TOOLS_CI_BOT_ESDK_RELEASE_TOKEN }}
         run: |
-          gh issue create \
-            --repo "dafny-lang/dafny" \
-            --title "[PRERELEASE REGRESSION] Dafny prerelease regression from ${{ github.repository }}" \
-            --body "Failure in ${{ github.workflow_ref }}. \
-            See ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
+          id=$(gh search issues -R dafny-lang/dafny --match title "[PRERELEASE REGRESSION] Dafny prerelease regression from ${{ github.repository }}" --json number,state -q '[.[] | select( .state=="open" )][0].number')
+           if [ -n "$id" ]; then
+             gh issue comment -R dafny-lang/dafny $id \
+               -b "Another failure in ${{ github.workflow_ref }}. \
+                 See ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
+           else
+             gh issue create -R dafny-lang/dafny \
+               -t "[PRERELEASE REGRESSION] Dafny prerelease regression from ${{ github.repository }}" \
+               -b "Failure in ${{ github.workflow_ref }}. \
+                 See ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}"
+           fi
diff --git a/.github/workflows/test_vector_verification.yml b/.github/workflows/test_vector_verification.yml
@@ -43,7 +43,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+        uses: dafny-lang/setup-dafny-action@v1.7.2
         with:
           dafny-version: ${{ inputs.dafny }}
 
@@ -64,7 +64,7 @@ jobs:
       # dafny-reportgenerator requires next6
       # but only 7.0 is installed on macos-12-large
       - name: Setup .NET Core SDK '6.0.x'
-        uses: actions/setup-dotnet@v3
+        uses: actions/setup-dotnet@v4
         with:
           dotnet-version: "6.0.x"
 
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,5 +1,24 @@
 # Changelog
 
+## [3.6.0](https://github.com/aws/aws-database-encryption-sdk-dynamodb/compare/v3.5.0...v3.6.0) (2024-07-23)
+
+### Features
+
+- allow indirect attribute names with MultiKeyStore ([#1208](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1208)) ([4ab97bc](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/4ab97bcc43d0b906e45c487920bc7ef5ba66e505))
+
+### Maintenance
+
+- bump dafny verification version to 4.7 ([#1181](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1181)) ([e7801ec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/e7801ec42b1bb212af68f9dc0c8037eed9876b5c))
+- **CI/CD:** use latest conventional-changelog-conventionalcommits ([#1195](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1195)) ([510227e](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/510227eabb958ff4a17d55fc2eac83f964d6a945))
+- Fix nightly build (aside from verification) ([#1029](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1029)) ([862420e](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/862420ef12ef1e764327671d839be451a7579bda))
+- **GHA:** add action for testing against MPL HEAD ([#1187](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1187)) ([b2f70ca](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/b2f70ca6733ac522f622014ae6c93bd1a1c15d28))
+- **GHA:** fix daily ci ([#1194](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1194)) ([a1427e0](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/a1427e0f7febc10cddd2eccb08385afb2b964367))
+- **MPL:** Bump MPL to 1.5.1 ([#1201](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1201)) ([808a5b4](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/808a5b4ad1143ffb8c0bb223fde1e3770c7abe62))
+- Sonatype Migration to User Tokens ([#1216](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1216)) ([a3b4ef9](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/a3b4ef9aac11f4a1e1048d938d554c669befc0a6))
+- Try to update existing issues ([31c6b98](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/31c6b9806920d500861154eccca07bd8a5ac4454))
+- Try to update existing issues ([4471295](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/4471295aa2b7f10e88c3742a41c947d9ad9f4cd2))
+- update project.properties to be SNAPSHOT ([#1087](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1087)) ([6f2825e](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/6f2825e198c84a5b20d50e49188b5d9004a1b71a))
+
 ## [3.5.0](https://github.com/aws/aws-database-encryption-sdk-dynamodb/compare/v3.4.0...v3.5.0) (2024-05-30)
 
 ### Features
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
@@ -1533,7 +1533,7 @@ module DynamoDBFilterExpr {
     else
       var name := if names.Some? && attr.value.s in names.value then names.value[attr.value.s] else attr.value.s;
       var keyIdField := bv.keySource.keyLoc.keyName;
-      if keyIdField == attr.value.s then
+      if keyIdField == name then
         Some(value)
       else
         KeyIdFromPart(bv, keyIdField, attr.value.s, value)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy
@@ -130,9 +130,9 @@ module BeaconTestFixtures {
     var keyStoreConfig := KTypes.KeyStoreConfig(
       id := None,
       kmsConfiguration := kmsConfig,
-      logicalKeyStoreName := "foo",
+      logicalKeyStoreName := "KeyStoreDdbTable",
       grantTokens := None,
-      ddbTableName := "foo",
+      ddbTableName := "KeyStoreDdbTable",
       ddbClient := Some(ddbClient),
       kmsClient := Some(kmsClient)
     );
@@ -177,6 +177,24 @@ module BeaconTestFixtures {
       );
   }
 
+  method GetLotsaBeaconsMulti() returns (output : BeaconVersion)
+    ensures output.keyStore.ValidState()
+    ensures fresh(output.keyStore.Modifies)
+    ensures output.version == 1
+  {
+    var store := GetKeyStore();
+    return BeaconVersion (
+        version := 1,
+        keyStore := store,
+        keySource := multi(MultiKeyStore(keyFieldName := "TheKeyField", cacheTTL := 42)),
+        standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB],
+        compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]),
+        virtualFields := Some([NameTitleField]),
+        encryptedParts := None,
+        signedParts := None
+      );
+  }
+
   const EmptyTableConfig := DynamoDbTableEncryptionConfig (
                               logicalTableName := "Foo",
                               partitionKeyName := "foo",
@@ -200,7 +218,8 @@ module BeaconTestFixtures {
                              "Title" := SE.ENCRYPT_AND_SIGN,
                              "TooBad" := SE.ENCRYPT_AND_SIGN,
                              "Year" := SE.SIGN_ONLY,
-                             "Date" := SE.SIGN_ONLY
+                             "Date" := SE.SIGN_ONLY,
+                             "TheKeyField" := SE.SIGN_ONLY
                            ]
                            )
 
@@ -223,6 +242,21 @@ module BeaconTestFixtures {
     return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0);
   }
 
+  method GetMultiSource(keyName : string, version : BeaconVersion) returns (output : SI.KeySource)
+    requires version.keyStore.ValidState()
+    ensures output.ValidState()
+    ensures version.keyStore == output.store
+    ensures fresh(output.client.Modifies)
+  {
+    var client :- expect Primitives.AtomicPrimitives();
+    var mpl :- expect MaterialProviders.MaterialProviders();
+    var input := MPT.CreateCryptographicMaterialsCacheInput(
+      cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3))
+    );
+    var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
+    return SI.KeySource(client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0);
+  }
+
   const SimpleItem : DDB.AttributeMap := map[
                                            "std2" := Std2String,
                                            "std4" := Std4String,
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy
@@ -32,4 +32,60 @@ module TestDDBSupport {
     expect newItem == SimpleItem + expectedNew;
   }
 
+  // DynamoDB String :: cast string to DDB.AttributeValue.S
+  function method DS(x : string) : DDB.AttributeValue
+  {
+    DDB.AttributeValue.S(x)
+  }
+
+  method {:test} TestMulti() {
+    var version := GetLotsaBeaconsMulti();
+    var src := GetMultiSource("TheKeyField", version);
+    var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src);
+    var search := SI.SearchInfo([bv], 0);
+    var expressionAttributeValues : map<string, AttributeValue> := map[
+      ":value" := DS("0ad21413-51aa-42e1-9c3d-6a4b1edf7e10")
+    ];
+    var queryInput := DDB.QueryInput (
+      TableName := "SomeTable",
+      ExpressionAttributeValues := Some(expressionAttributeValues),
+      KeyConditionExpression := Some("TheKeyField = :value")
+    );
+    var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
+
+    // Verify Success with branch key id plus beacon
+    expressionAttributeValues := map[
+      ":value" := DS("0ad21413-51aa-42e1-9c3d-6a4b1edf7e10"),
+      ":other" := DS("junk")
+    ];
+    queryInput := DDB.QueryInput (
+      TableName := "foo",
+      ExpressionAttributeValues := Some(expressionAttributeValues),
+      KeyConditionExpression := Some("TheKeyField = :value AND std2 = :other")
+    );
+    result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
+
+    // Verify Failure with beacon but no branch key id
+    queryInput := DDB.QueryInput (
+      TableName := "foo",
+      ExpressionAttributeValues := Some(expressionAttributeValues),
+      KeyConditionExpression := Some("std2 = :other")
+    );
+    var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
+    expect result2 == Failure(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.DynamoDbEncryptionException(
+                                message := "Need KeyId because of beacon std2 but no KeyId found in query"));
+
+    // Verify Success, even when field names are indirect via ExpressionAttributeNames
+    var expressionAttributeNames := map[
+      "#beacon" := "std2",
+      "#keyfield" := "TheKeyField"
+    ];
+    queryInput := DDB.QueryInput (
+      TableName := "foo",
+      ExpressionAttributeNames := Some(expressionAttributeNames),
+      ExpressionAttributeValues := Some(expressionAttributeValues),
+      KeyConditionExpression := Some("#keyfield = :value AND #beacon = :other")
+    );
+    result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
+  }
 }
diff --git a/DynamoDbEncryption/runtimes/java/build.gradle.kts b/DynamoDbEncryption/runtimes/java/build.gradle.kts
@@ -83,7 +83,7 @@ dependencies {
     implementation("software.amazon.smithy.dafny:conversion:${smithyDafnyJavaConversionVersion}")
     implementation("software.amazon.cryptography:aws-cryptographic-material-providers:${mplVersion}")
 
-    implementation(platform("software.amazon.awssdk:bom:2.24.2"))
+    implementation(platform("software.amazon.awssdk:bom:2.26.25"))
     implementation("software.amazon.awssdk:dynamodb")
     implementation("software.amazon.awssdk:dynamodb-enhanced")
     implementation("software.amazon.awssdk:kms")
diff --git a/DynamoDbEncryption/runtimes/net/AssemblyInfo.cs b/DynamoDbEncryption/runtimes/net/AssemblyInfo.cs
@@ -3,5 +3,5 @@
 [assembly: AssemblyTitle("AWS.Cryptography.DbEncryptionSDK.DynamoDb")]
 
 // This should be kept in sync with the version number in MPL.csproj
-[assembly: AssemblyVersion("3.5.0")]
+[assembly: AssemblyVersion("3.6.0")]
 
diff --git a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj b/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
@@ -5,7 +5,7 @@
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
     <IsPackable>true</IsPackable>
 
-    <Version>3.5.0</Version>
+    <Version>3.6.0</Version>
 
     <AssemblyName>AWS.Cryptography.DbEncryptionSDK.DynamoDb</AssemblyName>
     <PackageId>AWS.Cryptography.DbEncryptionSDK.DynamoDb</PackageId>
@@ -58,7 +58,7 @@
 
   <ItemGroup>
     <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.303.14"/>
-    <PackageReference Include="AWSSDK.Core" Version="3.7.304.7"/>
+    <PackageReference Include="AWSSDK.Core" Version="3.7.304.16"/>
     <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
     <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
     <!--
diff --git a/Makefile b/Makefile
@@ -77,7 +77,7 @@ generate_properties_file:
 	";
 
 setup_semantic_release:
-	npm i --no-save semantic-release @semantic-release/changelog semantic-release-replace-plugin conventional-changelog-conventionalcommits@7.0.2 @semantic-release/git
+	npm i --no-save semantic-release @semantic-release/changelog semantic-release-replace-plugin conventional-changelog-conventionalcommits @semantic-release/git
 
 run_semantic_release:
 	npx semantic-release --no-ci
diff --git a/TestVectors/runtimes/java/build.gradle.kts b/TestVectors/runtimes/java/build.gradle.kts
@@ -28,8 +28,7 @@ var dafnyRuntimeJavaVersion = props.getProperty("dafnyRuntimeJavaVersion")
 var smithyDafnyJavaConversionVersion = props.getProperty("smithyDafnyJavaConversionVersion")
 
 group = "software.amazon.cryptography"
-// change to ${mplVersion} for next MPL update
-version = "1.0-SNAPSHOT"
+version = "${mplVersion}" 
 description = "TestVectorsDynamoDbEncryption"
 
 java {
@@ -91,13 +90,12 @@ dependencies {
     implementation("software.amazon.smithy.dafny:conversion:${smithyDafnyJavaConversionVersion}")
     implementation("software.amazon.cryptography:aws-cryptographic-material-providers:${mplVersion}")
     implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:${ddbecVersion}")
-    // change to ${mplVersion} for next MPL update
-    implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:1.0-SNAPSHOT")
+    implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:${mplVersion}")
 
-    implementation(platform("software.amazon.awssdk:bom:2.24.2"))
+    implementation(platform("software.amazon.awssdk:bom:2.26.25"))
     implementation("software.amazon.awssdk:dynamodb")
     implementation("software.amazon.awssdk:dynamodb-enhanced")
-    implementation("software.amazon.awssdk:core:2.24.7")
+    implementation("software.amazon.awssdk:core:2.26.25")
     implementation("software.amazon.awssdk:kms")
     testImplementation("com.amazonaws:DynamoDBLocal:2.+")
     // This is where we gather the SQLLite files to copy over
diff --git a/TestVectors/runtimes/net/DbEsdkTestVectors.csproj b/TestVectors/runtimes/net/DbEsdkTestVectors.csproj
@@ -8,11 +8,10 @@
     <LangVersion>10</LangVersion>
     <TargetFramework>net6.0</TargetFramework>
     <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+    <StartupObject>DbEsdkTestVectors.Program</StartupObject>
   </PropertyGroup>
 
   <ItemGroup>
-    <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.303.14"/>
-    <PackageReference Include="AWSSDK.Core" Version="3.7.304.7"/>
     <ProjectReference Include="../../../DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj" />
     <ProjectReference Include="../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj" />
     <Compile Include="*.cs"/>
diff --git a/cfn/CB-Staging.yml b/cfn/CB-Staging.yml
@@ -238,7 +238,7 @@ Resources:
                 "arn:aws:secretsmanager:us-west-2:${AWS::AccountId}:secret:Maven-GPG-Keys-CI-Credentials-eBrSNB",
                 "arn:aws:secretsmanager:us-west-2:${AWS::AccountId}:secret:Maven-GPG-Keys-Release-haLIjZ",
                 "arn:aws:secretsmanager:us-west-2:${AWS::AccountId}:secret:Maven-GPG-Keys-Release-Credentials-WgJanS",
-                "arn:aws:secretsmanager:us-west-2:${AWS::AccountId}:secret:Sonatype-Team-Account-0tWvZm",
+                "arn:aws:secretsmanager:us-west-2:${AWS::AccountId}:secret:Sonatype-User-Token-zK61bM",
                 "arn:aws:secretsmanager:us-west-2:${AWS::AccountId}:secret:Github/aws-crypto-tools-ci-bot-AGUB3U"
               ],
               "Action": "secretsmanager:GetSecretValue"
diff --git a/codebuild/release/release-prod.yml b/codebuild/release/release-prod.yml
diff --git a/project.properties b/project.properties
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders

-Original file line number
+Diff line change
           java-version: ${{ matrix.java-version }}
       - name: Setup Dafny
 -        uses: dafny-lang/[email protected].0
 +        uses: dafny-lang/[email protected].2
         with:
           dafny-version: ${{ inputs.dafny }}