diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml new file mode 100644 index 000000000..110dab3cc --- /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.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/read-properties@1.1.1 + with: + path: "./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..a4a7efed8 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/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/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