chore: add project.properties

.github/workflows/dafny_verify_version.yml

@@ -0,0 +1,26 @@
+# This workflow reads the AwsEncryptionSdk/project.properties
+# into the environment variables
+# and then creates an output variable for `dafnyVerifyVersion`
+name: Dafny Verify Version
+
+on:
+  workflow_call:
+    outputs:
+      version:
+        description: "The Dafny Verification version"
+        value: ${{ jobs.getDafnyVerifyVersion.outputs.version }}
+
+jobs:
+  getDafnyVerifyVersion:
+    runs-on: ubuntu-latest
+    outputs:
+      version: ${{ steps.read_property.outputs.dafnyVerifyVersion }}
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: Read version from Properties-file
+        id: read_property
+        uses: christian-draeger/[email protected]
+        with:
+          path: "./project.properties"
+          properties: "dafnyVerifyVersion"

.github/workflows/dafny_version.yml

@@ -0,0 +1,26 @@
+# This workflow reads the AwsEncryptionSdk/project.properties
+# into the environment variables
+# and then creates an output variable for `dafnyVersion`
+name: Dafny Version
+
+on:
+  workflow_call:
+    outputs:
+      version:
+        description: "The Dafny version"
+        value: ${{ jobs.getDafnyVersion.outputs.version }}
+
+jobs:
+  getDafnyVersion:
+    runs-on: ubuntu-latest
+    outputs:
+      version: ${{ steps.read_property.outputs.dafnyVersion }}
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: Read version from Properties-file
+        id: read_property
+        uses: christian-draeger/[email protected]
+        with:
+          path: "./AwsEncryptionSDK/project.properties"
+          properties: "dafnyVersion"

.github/workflows/manual.yml

@@ -32,3 +32,8 @@ jobs:
     with:
       dafny: ${{ inputs.dafny }}
       regenerate-code: ${{ inputs.regenerate-code }}
+  manual-test-vectors:
+    uses: ./.github/workflows/library_interop_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}
+      regenerate-code: ${{ inputs.regenerate-code }}

.github/workflows/pull.yml

@@ -5,23 +5,31 @@ on:
   pull_request:
 
 jobs:
+  getVersion:
+    uses: ./.github/workflows/dafny_version.yml
+  getVerifyVersion:
+    uses: ./.github/workflows/dafny_verify_version.yml
   pr-ci-codegen:
+    needs: getVersion
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.2.0'
+      dafny: ${{ needs.getVersion.outputs.version }}
   pr-ci-verification:
+    needs: getVerifyVersion
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.7.0'
+      dafny: ${{ needs.getVerifyVersion.outputs.version }}
   # pr-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
   #     dafny: '4.2.0'
   pr-ci-net:
+    needs: getVersion
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: ${{ needs.getVersion.outputs.version }}
   pr-test-vectors:
+    needs: getVersion
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: ${{ needs.getVersion.outputs.version }}

.github/workflows/push.yml

@@ -7,23 +7,31 @@ on:
       - main    
 
 jobs:
+  getVersion:
+    uses: ./.github/workflows/dafny_version.yml
+  getVerifyVersion:
+    uses: ./.github/workflows/dafny_verify_version.yml
   pr-ci-codegen:
+    needs: getVersion
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.2.0'
-  push-ci-verification:
+      dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-verification:
+    needs: getVerifyVersion
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.7.0'
-  # push-ci-java:
+      dafny: ${{needs.getVerifyVersion.outputs.version}}
+  # pr-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
   #     dafny: '4.2.0'
-  push-ci-net:
+  pr-ci-net:
+    needs: getVersion
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: ${{needs.getVersion.outputs.version}}
   pr-test-vectors:
+    needs: getVersion
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: ${{needs.getVersion.outputs.version}}

AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch

@@ -1,5 +1,5 @@
 diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs
-index 3135234..58b4154 100644
+index 1dc37f40..e2187b21 100644
 --- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs
 +++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs
 @@ -28,7 +28,7 @@ namespace AWS.Cryptography.EncryptionSDK
@@ -12,7 +12,7 @@ index 3135234..58b4154 100644
              get { return this._netV4_0_0_RetryPolicy; }
              set { this._netV4_0_0_RetryPolicy = value; }
 diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs
-index cc922a3..161bcf3 100644
+index 14d20a87..dc6e24f9 100644
 --- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs
 +++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs
 @@ -11,14 +11,18 @@ namespace AWS.Cryptography.EncryptionSDK
@@ -36,7 +36,7 @@ index cc922a3..161bcf3 100644
              return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy));
          }
          public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value)
-@@ -87,16 +91,22 @@ namespace AWS.Cryptography.EncryptionSDK
+@@ -92,16 +96,22 @@ namespace AWS.Cryptography.EncryptionSDK
 
              return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId));
          }
@@ -63,7 +63,7 @@ index cc922a3..161bcf3 100644
              throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value");
          }
          public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption<software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy> value)
-@@ -115,13 +125,19 @@ namespace AWS.Cryptography.EncryptionSDK
+@@ -120,13 +130,19 @@ namespace AWS.Cryptography.EncryptionSDK
          {
              return value == null ? Wrappers_Compile.Option<long>.create_None() : Wrappers_Compile.Option<long>.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value));
          }

project.properties

@@ -0,0 +1,4 @@
+# This file stores the top level dafny version information.
+# All elements of the project need to agree on this version.
+dafnyVersion=4.2.0
+dafnyVerifyVersion=4.7.0