chore: Forwards compatibility with Dafny > 4.2 (including pending 4.5) #195
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…iders-library-dafny into robin-aws/fix-nightly-dafny-build # Conflicts: # ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/Shim.java # SharedMakefileV2.mk # TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy # TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy
|
Fresh manual run on the refactored workflows against |
seebees
approved these changes
Mar 1, 2024
robin-aws
added a commit
to aws/aws-encryption-sdk-dafny
that referenced
this pull request
Mar 18, 2024
Replaces nearly all of the `SharedMakefile.mk` with the common `smithy-dafny/SmithyDafnyMakefile.mk` makefile, just retaining configuration variables specific to this repo (such as the path to the `smithy-dafny` submodule). Uses the new features in that makefile and `smithy-dafny` itself to make the projects forwards-compatible with the latest Dafny nightly prerelease, and hence will fix the nightly build once merged - [see here for a manual run](https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/8240077703/job/22534705434). Highlights of the changes: * Apply the same workflow changes as aws/aws-cryptographic-material-providers-library#195 to use `smithy-dafny` to regenerate code, either to check that the output matches what's checked in (in a new separate codegen workflow) or to be compatible with newer versions of Dafny in the nightly build (in existing workflows). * In this case we also have to locally update the MPL submodule to the latest, so that we can pick up the forwards-compatible changes to that repo, and regenerate code transitively. * Because the code in this repo wasn't formatted already, but applying newer `smithy-dafny` code generation automatically formats, all the generated code has trivial layout changes. * Also extracted a manual patch. * Applied a lot of [explicit client downcasting](https://github.com/aws/aws-encryption-sdk-dafny/pull/638/files#diff-b3d9cba935758528ac13c23c2f482d6a09d771122004103605b346e3da5f3cecR29-R33) to account for the change in `smithy-dafny` Note that this changes the Makefile targets as a result: * There is a default value for `CODEGEN_CLI_ROOT` (the `smithy-dafny` submodule copy) so that variable is now optional * Targets like `polymorph_codegen` also now apply to dependencies transitively, just like targets such as `transpile_java`. Because the current state of the MPL submodule doesn't use the same smithy-dafny version or Makefile targets, this doesn't work by default, so for working locally it will generally be better to only generate for the current library via `make polymorph_codegen PROJECT_DEPENDENCIES=`
robin-aws
added a commit
to aws/aws-database-encryption-sdk-dynamodb
that referenced
this pull request
Apr 19, 2024
…build (#797) Replaces nearly all of the `SharedMakefile.mk` with the common `smithy-dafny/SmithyDafnyMakefile.mk` makefile, just retaining configuration variables specific to this repo (such as the path to the `smithy-dafny` submodule). Uses the new features in that makefile and `smithy-dafny` itself to make the projects forwards-compatible with the latest Dafny nightly prerelease, and hence will MOSTLY fix the nightly build once merged. "Mostly" because I still need to fix some externs to make them use the pattern that avoids the Java TypeDescriptor differences between Dafny versions, but that can be fixed in a follow-up PR. Highlights of the changes: * Apply the same workflow changes as aws/aws-cryptographic-material-providers-library#195 to use `smithy-dafny` to regenerate code, either to check that the output matches what's checked in (in a new separate codegen workflow) or to be compatible with newer versions of Dafny in the nightly build (in existing workflows). * In this case we also have to locally update the MPL submodule to the latest, so that we can pick up the forwards-compatible changes to that repo, and regenerate code transitively. Generating code is unfortunately getting quite expensive, especially since the shared makefile logic isn't sophisticated enough to avoid regenerating the same code multiple times. * Because the code in this repo wasn't formatted already, but applying newer `smithy-dafny` code generation automatically formats, all the generated has trivial layout changes. * Also extracted a manual patch. * ~Applied a lot of [explicit client downcasting](https://github.com/aws/aws-database-encryption-sdk-dynamodb/pull/797/files#diff-692e2b06d124c9775e2fcd9cd9dbd10e0c8ea470e08174ed0b258b0301622581R182) to account for the change in `smithy-dafny` ~ (the change in smithy-dafny was undone so this isn't necessary any more) * Converted `Beacon.CheckBytesToHex()` from a "test lemma" to a dynamic test, because on the latest Dafny the verification got even more expensive, and this didn't seem to introduce any real additional risk.
lucasmcdonald3
pushed a commit
that referenced
this pull request
Jun 4, 2024
#195) Applies several fixes/improvements in order to work with newer Dafny versions. * Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI. * Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first) * Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did. * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too. * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. * Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files. * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges. * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :) * Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions. Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665 Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches
robin-aws
added a commit
to aws/aws-database-encryption-sdk-dynamodb
that referenced
this pull request
Jun 4, 2024
Makes the same changes around avoiding direct calls to instantiate parameterized datatypes in Java code as in aws/aws-cryptographic-material-providers-library#195, plus some CI configuration fixes. Dry runs of nightly builds: * [Library Java tests](https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/9104958211) * [Java Examples](https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/9106211948) * [test dotnet](https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/9100864042) Will leave fixing the verification for a separate PR since this was already a fair bit of work :)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description of changes:
Applies several fixes/improvements in order to work with newer Dafny versions.
This PR is currently using an unmerged branch ofsmithy-dafnyto test the fixes - smithy-lang/smithy-dafny#321 needs to be merged before this one.smithy-dafnyas a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI.--library-rootand--patch-files-dir, generate dependencies first)smithy-dafnyto abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as feat: add type descriptors for data constructors in Java, when necessary smithy-lang/smithy-dafny#301 did.__defaultclasses to use the above to avoid constructing Dafny datatypes directly.InternalResult<T, R>to replace some internal-only uses of Dafny's compiledResulttype, to avoid even more Dafny helper methods.smithy-dafny<library-root>/codegen-patches[/<service>]feature to extract out manual patch files.{:vcs_split_on_every_assert}onAwsKmsKeyring.OnDecrypt'that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :)Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665
Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches
Squash/merge commit message, if applicable:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.