From 229a49e98ebca01afce0b27ad47aba55cce54da4 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 18 Jul 2024 12:16:35 -0700 Subject: [PATCH 1/5] chore: add dafnyVerifyVersion to properties --- .github/workflows/dafny_verify_version.yml | 26 ++++++++++++++++++++++ .github/workflows/dafny_version.yml | 26 ++++++++++++++++++++++ .github/workflows/manual.yml | 5 +++++ .github/workflows/pull.yml | 16 +++++++++---- .github/workflows/push.yml | 22 ++++++++++++------ AwsEncryptionSDK/project.properties | 1 + 6 files changed, 85 insertions(+), 11 deletions(-) create mode 100644 .github/workflows/dafny_verify_version.yml create mode 100644 .github/workflows/dafny_version.yml diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml new file mode 100644 index 000000000..e0274e1ba --- /dev/null +++ b/.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.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/read-properties@1.1.1 + with: + path: "./AwsEncryptionSDK/project.properties" + properties: "dafnyVerifyVersion" diff --git a/.github/workflows/dafny_version.yml b/.github/workflows/dafny_version.yml new file mode 100644 index 000000000..79c67f22a --- /dev/null +++ b/.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/read-properties@1.1.1 + with: + path: "./AwsEncryptionSDK/project.properties" + properties: "dafnyVersion" diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml index 74029c97d..9d59c9f89 100644 --- a/.github/workflows/manual.yml +++ b/.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 }} diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 523b5149b..6bd287d15 100644 --- a/.github/workflows/pull.yml +++ b/.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}} diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 98de8408c..32d835630 100644 --- a/.github/workflows/push.yml +++ b/.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}} diff --git a/AwsEncryptionSDK/project.properties b/AwsEncryptionSDK/project.properties index dd7eb37b9..93efed036 100644 --- a/AwsEncryptionSDK/project.properties +++ b/AwsEncryptionSDK/project.properties @@ -1,3 +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 From b51f467b9b3768e169de2cd463cd66e88f7627fd Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 18 Jul 2024 12:21:40 -0700 Subject: [PATCH 2/5] fix --- .github/workflows/dafny_verify_version.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml index e0274e1ba..11fa068b3 100644 --- a/.github/workflows/dafny_verify_version.yml +++ b/.github/workflows/dafny_verify_version.yml @@ -11,10 +11,10 @@ on: value: ${{ jobs.getDafnyVersion.outputs.version }} jobs: - getDafnyVersion: + getDafnyVerifyVersion: runs-on: ubuntu-latest outputs: - version: ${{ steps.read_property.outputs.dafnyVersion }} + version: ${{ steps.read_property.outputs.dafnyVerifyVersion }} steps: - uses: actions/checkout@v4 From 8fb9804e5fafc6f3faa2006daaf4a8e7f0a3e3e8 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 18 Jul 2024 12:28:46 -0700 Subject: [PATCH 3/5] a --- .github/workflows/pull.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 6bd287d15..a4a7efed8 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -13,12 +13,12 @@ jobs: needs: getVersion uses: ./.github/workflows/library_codegen.yml with: - dafny: ${{needs.getVersion.outputs.version}} + dafny: ${{ needs.getVersion.outputs.version }} pr-ci-verification: needs: getVerifyVersion uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: ${{needs.getVerifyVersion.outputs.version}} + dafny: ${{ needs.getVerifyVersion.outputs.version }} # pr-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: @@ -27,9 +27,9 @@ jobs: needs: getVersion uses: ./.github/workflows/library_net_tests.yml with: - dafny: ${{needs.getVersion.outputs.version}} + dafny: ${{ needs.getVersion.outputs.version }} pr-test-vectors: needs: getVersion uses: ./.github/workflows/library_interop_tests.yml with: - dafny: ${{needs.getVersion.outputs.version}} + dafny: ${{ needs.getVersion.outputs.version }} From 7b7b8a9e68001720466c78a013bbbffbdf3a9714 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 18 Jul 2024 12:31:19 -0700 Subject: [PATCH 4/5] fix --- .github/workflows/dafny_verify_version.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml index 11fa068b3..399809425 100644 --- a/.github/workflows/dafny_verify_version.yml +++ b/.github/workflows/dafny_verify_version.yml @@ -8,7 +8,7 @@ on: outputs: version: description: "The Dafny Verification version" - value: ${{ jobs.getDafnyVersion.outputs.version }} + value: ${{ jobs.getDafnyVerifyVersion.outputs.version }} jobs: getDafnyVerifyVersion: From c7b70805b87f6afd7ac7dc6ce07b488d6e4ce6e9 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 18 Jul 2024 12:48:10 -0700 Subject: [PATCH 5/5] fix --- .github/workflows/dafny_verify_version.yml | 2 +- .../AwsEncryptionSdk/dotnet/dafny-4.2.0.patch | 8 ++++---- AwsEncryptionSDK/project.properties | 1 - project.properties | 4 ++++ 4 files changed, 9 insertions(+), 6 deletions(-) create mode 100644 project.properties diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml index 399809425..110dab3cc 100644 --- a/.github/workflows/dafny_verify_version.yml +++ b/.github/workflows/dafny_verify_version.yml @@ -22,5 +22,5 @@ jobs: id: read_property uses: christian-draeger/read-properties@1.1.1 with: - path: "./AwsEncryptionSDK/project.properties" + path: "./project.properties" properties: "dafnyVerifyVersion" diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch index 6cc829983..9c0f8a188 100644 --- a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch +++ b/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 value) -@@ -115,13 +125,19 @@ namespace AWS.Cryptography.EncryptionSDK +@@ -120,13 +130,19 @@ namespace AWS.Cryptography.EncryptionSDK { return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); } diff --git a/AwsEncryptionSDK/project.properties b/AwsEncryptionSDK/project.properties index 93efed036..dd7eb37b9 100644 --- a/AwsEncryptionSDK/project.properties +++ b/AwsEncryptionSDK/project.properties @@ -1,4 +1,3 @@ # 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 diff --git a/project.properties b/project.properties new file mode 100644 index 000000000..93efed036 --- /dev/null +++ b/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