Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Remove uses of :| #618

Merged
merged 8 commits into from
Aug 22, 2024
Merged

fix: Remove uses of :| #618

merged 8 commits into from
Aug 22, 2024

Conversation

atomb
Copy link
Contributor

@atomb atomb commented Aug 21, 2024

Issue #, if available:

Description of changes:

Removes uses of :| in Dafny code, and updates the libraries submodule to a version that does not use it, either. This will eliminate failures when compiling with Dafny 4.8.0 and -definiteAssignment:3.

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.

@atomb atomb requested a review from a team as a code owner August 21, 2024 15:17
In conjunction with the update of the libraries submodule, this will
allow all code to be compiled with `-definiteAssignment:3` without
Failures with the upcoming Dafny 4.8.0.
@atomb atomb changed the title Update libraries submodule fix: Remove uses of :| Aug 21, 2024
@texastony texastony marked this pull request as draft August 21, 2024 16:13
@texastony
Copy link
Contributor

@atomb I put this PR in draft. Once verification and other CI is passing, you can mark it ready for review.

@atomb atomb marked this pull request as ready for review August 21, 2024 21:16
@@ -335,7 +335,7 @@ module StandardLibrary {
* The function is compilable, but will not exhibit enviable performance.
*/

function method {:tailrecursion} SetToOrderedSequence<T(!new,==)>(s: set<seq<T>>, less: (T, T) -> bool): (q: seq<seq<T>>)
function SetToOrderedSequence<T(!new,==)>(s: set<seq<T>>, less: (T, T) -> bool): (q: seq<seq<T>>)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This will be breaking for consumers of the MPL, since you're changing it from compiled to ghost, but there are compiled references to it already, e.g. https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy#L1091

Are you relying on assuming we can replace all such references with ComputeSetToSequence[2]?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I removed internal compiled references to it but didn't realize it was part of the exported API.

I suspect we should be able to replace them all, though it's possible there are complexities I'm not thinking of.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the two instances in that file are the only place it's used in a compiled context, and I think it can be replaced by the Compute version there.

Copy link
Contributor

@texastony texastony Aug 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While we can logically replace them, we cannot assume that the code on our customers computer will not be updated.

i.e: Our customers will still have references to the old version, and rely on the references being provided by the MPL.

Unless both of the references in the DB-ESDK, and any references in the ESDK, are only in ghost code and have ALWAYS been in only in ghost code.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@atomb Could you make this a function by method instead and use the ComputeSetToSequence2 implementation in the by method body?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I don't think you have to change this anyway, I don't get an error when I do dafny verify src/StandardLibrary.dfy --function-syntax:3 --enforce-determinism.

Since this :| is in an expression context it already has to be provably deterministic.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, you are indeed correct. I've changed it back.

josecorella
josecorella previously approved these changes Aug 21, 2024
Copy link
Contributor

@josecorella josecorella left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

starred long and hard at the change and believe this is a fine change.

Copy link
Contributor

@texastony texastony left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Blocking until breaking change issue is resolved.

@texastony texastony dismissed their stale review August 22, 2024 15:29

Breaking change has been resolved

seebees
seebees previously approved these changes Aug 22, 2024
Copy link
Contributor

@seebees seebees left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These changes look good.

Comment on lines 484 to 496
&& key in input.reproducedEncryptionContext.value
&& key in input.reproducedEncryptionContext.value.Keys
&& key in input.encryptionContext
&& key !in keysSet
:: input.reproducedEncryptionContext.value[key] == input.encryptionContext[key]
&& key !in keysSet'
:: input.encryptionContext[key] == input.reproducedEncryptionContext.value[key]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Slight nit, adjusting the verification makes it a little hard to verify the lack of change :)
This way would have made it clear that the only actual change was to change the invariant to use the ghost value.
and that everything else was additions.

                     && key in input.reproducedEncryptionContext.value
                     && key in input.encryptionContext
                     && key !in keysSet'
                     :: input.reproducedEncryptionContext.value[key] == input.encryptionContext[key]

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point. Those changes are an artifact of attempting to reduce brittleness, before I realized that it was actually missing information leading to failure here. They're not necessary, and I'd be happy to undo them.

Comment on lines 55 to 56
var keySeq := [];
while keySet != {}
invariant |keySeq| + |keySet| == |inputKeys|
invariant forall k <- keySeq
:: k in inputKeys
{
var key :| key in keySet;
keySeq := keySeq + [key];
keySet := keySet - {key};
}
var keySeq := SortedSets.ComputeSetToSequence(keySet);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly here, I think that we could see the diff more clearly as invariant by writing it this way.
(I checked the ensures clause)
This way the invariant changes to an assert.

var keySeq := SortedSets.ComputeSetToSequence(inputKeys);
assert |keySeq| == |inputKeys|;
assert forall k <- keySeq :: k in inputKeys;

Comment on lines -28 to +29
var keys := SetToOrderedSequence(encryptionContext.Keys, UInt.UInt8Less);
var keys := SortedSets.ComputeSetToOrderedSequence2(encryptionContext.Keys, UInt.UInt8Less);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at SortedSets.ComputeSetToOrderedSequence2 I can see ensures res == SetToOrderedSequence(s, less) so this MUST be the same.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These testing changes look fine.

Copy link
Contributor

@seebees seebees left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wonderful!

@robin-aws robin-aws merged commit f12fe5b into main Aug 22, 2024
70 checks passed
@robin-aws robin-aws deleted the new-libraries branch August 22, 2024 21:17
texastony pushed a commit that referenced this pull request Aug 23, 2024
Removes uses of :| in Dafny code, and updates the libraries submodule to a version that does not use it, either. This will eliminate failures when compiling with Dafny 4.8.0 and -definiteAssignment:3.
lucasmcdonald3 pushed a commit that referenced this pull request Aug 29, 2024
Removes uses of :| in Dafny code, and updates the libraries submodule to a version that does not use it, either. This will eliminate failures when compiling with Dafny 4.8.0 and -definiteAssignment:3.
josecorella pushed a commit that referenced this pull request Sep 10, 2024
* add ECDH error message for Rust ([#574](#574)) ([473a34a](473a34a))
* **DDB-Model:** DDB Supports 100 actions per Transaction ([#692](#692)) ([8a67843](8a67843))
* GetCurrentTimeStamp returns ISO8601 format ([#575](#575)) ([c07a51f](c07a51f))
* maintain order in test vectors for languages with parallel tests ([#641](#641)) ([8c8a38f](8c8a38f))
* Remove 4.4 DDB and KMS patches, abstract test to work on later Dafny versions ([#611](#611)) ([d51d648](d51d648))
* Remove uses of `:|` ([#618](#618)) ([f12fe5b](f12fe5b))
* test vector help text ([#657](#657)) ([0fedaf1](0fedaf1))

* bump dafny verification and code gen to dafny 4.8.0 ([#520](#520)) ([e16539e](e16539e))
* **post-release:** Change back to 1.5.1-SNAPSHOT ([09cd9a4](09cd9a4))
lucasmcdonald3 pushed a commit that referenced this pull request Sep 24, 2024
Removes uses of :| in Dafny code, and updates the libraries submodule to a version that does not use it, either. This will eliminate failures when compiling with Dafny 4.8.0 and -definiteAssignment:3.
lucasmcdonald3 pushed a commit to lucasmcdonald3/aws-cryptographic-material-providers-library that referenced this pull request Sep 26, 2024
Removes uses of :| in Dafny code, and updates the libraries submodule to a version that does not use it, either. This will eliminate failures when compiling with Dafny 4.8.0 and -definiteAssignment:3.
lucasmcdonald3 pushed a commit to lucasmcdonald3/aws-cryptographic-material-providers-library that referenced this pull request Oct 1, 2024
Removes uses of :| in Dafny code, and updates the libraries submodule to a version that does not use it, either. This will eliminate failures when compiling with Dafny 4.8.0 and -definiteAssignment:3.
ajewellamz pushed a commit that referenced this pull request Dec 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants