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.

Sign up for GitHub

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

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
3732a7a
Update libraries submodule
atomb Aug 20, 2024
b7e3b48
fix: Remove uses of `:|`
atomb Aug 21, 2024
3263c42
Fix one more use of `:|`
atomb Aug 21, 2024
1a240ee
Call function form of ComputeSetToOrderedSequence
atomb Aug 21, 2024
53d3508
Fix proof of DecryptMaterials'
atomb Aug 21, 2024
a79e9f5
Make SetToOrderedSequence compilable again
atomb Aug 22, 2024
05d7945
Reduce and clarify difference in verification
atomb Aug 22, 2024
55c9f38
Fix formatting
atomb Aug 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 20 additions & 7 deletions ...ographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ module DefaultCMM {
import Defaults
import Commitment
import Seq
import SortedSets

class DefaultCMM
extends CMM.VerifiableInterface
Expand Down Expand Up @@ -329,7 +330,7 @@ module DefaultCMM {
//# - The operations made on the encryption context on the Get Encryption Materials call
//# SHOULD be inverted on the Decrypt Materials call.

method DecryptMaterials'(
method {:vcs_split_on_every_assert} DecryptMaterials'(
input: Types.DecryptMaterialsInput
)
returns (output: Result<Types.DecryptMaterialsOutput, Types.Error>)
Expand Down Expand Up @@ -372,6 +373,7 @@ module DefaultCMM {
//# the values MUST be equal or the operation MUST fail.
ensures
&& (output.Success? ==> CMM.ReproducedEncryptionContext?(input))
ensures
&& (!CMM.ReproducedEncryptionContext?(input) ==> output.Failure?)
//= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
//= type=implication
Expand Down Expand Up @@ -478,25 +480,36 @@ module DefaultCMM {
var requiredEncryptionContextKeys := [];
if input.reproducedEncryptionContext.Some? {
var keysSet := input.reproducedEncryptionContext.value.Keys;
while keysSet != {}
ghost var keysSet' := keysSet;
var keysSeq := SortedSets.ComputeSetToSequence(keysSet);
var i := 0;
while i < |keysSeq|
invariant Seq.HasNoDuplicates(keysSeq)
invariant forall j | 0 <= j < i && i < |keysSeq| :: keysSeq[j] !in keysSet'
invariant forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet'
invariant |keysSet'| == |keysSeq| - i
invariant forall key
|
&& 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.

invariant forall key <- requiredEncryptionContextKeys
:: key !in input.encryptionContext
{
var key :| key in keysSet;
var key := keysSeq[i];
if key in input.encryptionContext {
:- Need(input.reproducedEncryptionContext.value[key] == input.encryptionContext[key],
Types.AwsCryptographicMaterialProvidersException(
message := "Encryption context does not match reproduced encryption context."));
} else {
requiredEncryptionContextKeys := requiredEncryptionContextKeys + [key];
}
keysSet := keysSet - {key};
keysSet' := keysSet' - {key};
i := i + 1;
assert forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet' by {
reveal Seq.HasNoDuplicates();
}
}
}

Expand Down
12 changes: 2 additions & 10 deletions ...oviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module RequiredEncryptionContextCMM {
import UTF8
import Types = AwsCryptographyMaterialProvidersTypes
import Seq
import SortedSets

class RequiredEncryptionContextCMM
extends CMM.VerifiableInterface
Expand Down Expand Up @@ -52,16 +53,7 @@ module RequiredEncryptionContextCMM {
ensures Modifies == { History } + underlyingCMM.Modifies
{
var keySet := inputKeys;
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;


underlyingCMM := inputCMM;
requiredEncryptionContextKeys := keySeq;
Expand Down
3 changes: 2 additions & 1 deletion ...erialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module CanonicalEncryptionContext {
import Types = AwsCryptographyMaterialProvidersTypes
import opened Wrappers
import Seq
import SortedSets

//= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#onencrypt
//# The keyring MUST attempt to serialize the [encryption materials']
Expand All @@ -25,7 +26,7 @@ module CanonicalEncryptionContext {
{
:- Need(|encryptionContext| < UINT16_LIMIT,
Types.AwsCryptographicMaterialProvidersException( message := "Encryption Context is too large" ));
var keys := SetToOrderedSequence(encryptionContext.Keys, UInt.UInt8Less);
var keys := SortedSets.ComputeSetToOrderedSequence2(encryptionContext.Keys, UInt.UInt8Less);
Comment on lines -28 to +29
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.


if |keys| == 0 then
Success([])
Expand Down
15 changes: 8 additions & 7 deletions AwsCryptographyPrimitives/test/TestRSA.dfy
View file
Open in desktop
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.

Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
import opened Wrappers
import opened StandardLibrary.UInt
import UTF8
import SortedSets

const RSA_PUBLIC_2048 := "-----BEGIN PUBLIC KEY-----\n"
+ "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAqBvECLsPdF1J5DOkaA1n\n"
Expand Down Expand Up @@ -130,10 +131,11 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
lengthBits := 2048,
pem := PrivateKeyFromGenerateRSAKeyPairPemBytes
));

while allPadding != {}
var paddingSeq := SortedSets.ComputeSetToSequence(allPadding);
for paddingIdx := 0 to |paddingSeq|
{
var padding :| padding in allPadding;
var padding := paddingSeq[paddingIdx];

BasicRSAEncryptTest(
Primitives.Types.RSAEncryptInput(
padding := padding,
Expand All @@ -144,7 +146,6 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
KeyFromGenerateRSAKeyPair
);

allPadding := allPadding - {padding};
}
}

Expand All @@ -164,9 +165,10 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
pem := PrivateKeyFromTestVectorsPemBytes
));

while allPadding != {}
var paddingSeq := SortedSets.ComputeSetToSequence(allPadding);
for paddingIdx := 0 to |paddingSeq|
{
var padding :| padding in allPadding;
var padding := paddingSeq[paddingIdx];

BasicRSAEncryptTest(
Primitives.Types.RSAEncryptInput(
Expand All @@ -178,7 +180,6 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
KeyFromTestVectorsPair
);

allPadding := allPadding - {padding};
}
}

Expand Down
2 changes: 1 addition & 1 deletion StandardLibrary/src/StandardLibrary.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 •
edited
Loading

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.

requires Trichotomous(less) && Transitive(less)
ensures |s| == |q|
ensures forall i :: 0 <= i < |q| ==> q[i] in s
Expand Down
2 changes: 1 addition & 1 deletion libraries
Open in desktop
Submodule libraries updated 12 files
+1 −1 .github/workflows/check-examples-in-docs.yml
+1 −1 .github/workflows/tests.yml
+1 −1 Scripts/check-examples
+2 −2 src/Collections/Sequences/LittleEndianNat.dfy
+0 −61 src/Collections/Sequences/Seq.dfy
+1 −1 src/JSON/Tests.dfy
+68 −12 src/NonlinearArithmetic/Internals/ModInternals.dfy
+8 −1 src/NonlinearArithmetic/Mul.dfy
+1 −1 src/dafny/BoundedInts.dfy
+0 −62 src/dafny/Collections/Seqs.dfy
+1 −1 src/dafny/Collections/Sets.dfy
+4 −4 src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy
Loading